varungandhi-apple updated this revision to Diff 274240.
varungandhi-apple added a comment.
Herald added subscribers: cfe-commits, martong.
Herald added a project: clang.
Include missing commit separating verbose and showOutput.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D82791/new/
https://reviews.llvm.org/D82791
Files:
clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
clang/lib/StaticAnalyzer/Core/BugReporter.cpp
clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
clang/test/CodeGen/aarch64-sve.c
clang/test/CodeGenCXX/aarch64-mangle-sve-vectors.cpp
clang/test/CodeGenCXX/aarch64-sve-typeinfo.cpp
clang/test/CodeGenObjC/aarch64-sve-types.m
clang/test/PCH/aarch64-sve-types.c
clang/test/Sema/aarch64-sve-types.c
clang/test/SemaObjC/aarch64-sve-types.m
clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
Index: clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
===================================================================
--- clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
+++ clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
@@ -170,6 +170,54 @@
"test.FalsePositiveGenerator:CAN_BE_TRUE\n");
}
+TEST(FalsePositiveRefutationBRVisitor,
+ UnSatAtErrorNodeDueToRefinedConstraintNoReport) {
+ SKIP_WITHOUT_Z3;
+ constexpr auto Code = R"(
+ void reportIfCanBeTrue(bool);
+ void reachedWithNoContradiction();
+ void test(unsigned x, unsigned n) {
+ if (n >= 1 && n <= 2) {
+ if (x >= 3)
+ return;
+ // x: [0,2] and n: [1,2]
+ int y = x + n; // y: '(x+n)' Which is in approximately between 1 and 4.
+
+ // Registers the symbol 'y' with the constraint [1, MAX] in the true
+ // branch.
+ if (y > 0) {
+ // Since the x: [0,2] and n: [1,2], the 'y' is indeed greater than
+ // zero. If we emit a warning here, the constraints on the BugPath is
+ // SAT. Therefore that report is NOT invalidated.
+ reachedWithNoContradiction(); // 'y' can be greater than zero. OK
+
+ // If we ask the analyzer whether the 'y' can be 5. It won't know,
+ // therefore, the state will be created where the 'y' expression is 5.
+ // Although, this assumption is false!
+ // 'y' can not be 5 if the maximal value of both x and n is 2.
+ // The BugPath which become UnSAT in the ErrorNode with a refined
+ // constraint, should be invalidated.
+ reportIfCanBeTrue(y == 5);
+ }
+ }
+ })";
+
+ std::string Diags;
+ EXPECT_TRUE(runCheckerOnCodeWithArgs<addFalsePositiveGenerator>(
+ Code, LazyAssumeAndCrossCheckArgs, Diags));
+ EXPECT_EQ(Diags,
+ "test.FalsePositiveGenerator:REACHED_WITH_NO_CONTRADICTION\n");
+ // Single warning. The second report was invalidated by the visitor.
+
+ // Without enabling the crosscheck-with-z3 both reports are displayed.
+ std::string Diags2;
+ EXPECT_TRUE(runCheckerOnCodeWithArgs<addFalsePositiveGenerator>(
+ Code, LazyAssumeArgs, Diags2));
+ EXPECT_EQ(Diags2,
+ "test.FalsePositiveGenerator:REACHED_WITH_NO_CONTRADICTION\n"
+ "test.FalsePositiveGenerator:CAN_BE_TRUE\n");
+}
+
} // namespace
} // namespace ento
} // namespace clang
Index: clang/test/SemaObjC/aarch64-sve-types.m
===================================================================
--- clang/test/SemaObjC/aarch64-sve-types.m
+++ clang/test/SemaObjC/aarch64-sve-types.m
@@ -18,5 +18,7 @@
@property(nullable) __SVFloat32_t f32; // expected-error {{cannot be applied to non-pointer type}}
@property(nullable) __SVFloat64_t f64; // expected-error {{cannot be applied to non-pointer type}}
+@property(nullable) __SVBFloat16_t bf16; // expected-error {{cannot be applied to non-pointer type}}
+
@property(nullable) __SVBool_t b8; // expected-error {{cannot be applied to non-pointer type}}
@end
Index: clang/test/Sema/aarch64-sve-types.c
===================================================================
--- clang/test/Sema/aarch64-sve-types.c
+++ clang/test/Sema/aarch64-sve-types.c
@@ -1,4 +1,4 @@
-// RUN: %clang_cc1 %s -triple aarch64-none-linux-gnu -target-feature +sve -fsyntax-only -verify
+// RUN: %clang_cc1 %s -triple aarch64-none-linux-gnu -target-feature +sve,+bf16 -fsyntax-only -verify
void f() {
int size_s8[sizeof(__SVInt8_t) == 0 ? 1 : -1]; // expected-error {{invalid application of 'sizeof' to sizeless type '__SVInt8_t'}}
@@ -34,6 +34,9 @@
int size_f64[sizeof(__SVFloat64_t) == 0 ? 1 : -1]; // expected-error {{invalid application of 'sizeof' to sizeless type '__SVFloat64_t'}}
int align_f64[__alignof__(__SVFloat64_t) == 16 ? 1 : -1]; // expected-error {{invalid application of '__alignof' to sizeless type '__SVFloat64_t'}}
+ int size_bf16[sizeof(__SVBFloat16_t) == 0 ? 1 : -1]; // expected-error {{invalid application of 'sizeof' to sizeless type '__SVBFloat16_t'}}
+ int align_bf16[__alignof__(__SVBFloat16_t) == 16 ? 1 : -1]; // expected-error {{invalid application of '__alignof' to sizeless type '__SVBFloat16_t'}}
+
int size_b8[sizeof(__SVBool_t) == 0 ? 1 : -1]; // expected-error {{invalid application of 'sizeof' to sizeless type '__SVBool_t'}}
int align_b8[__alignof__(__SVBool_t) == 2 ? 1 : -1]; // expected-error {{invalid application of '__alignof' to sizeless type '__SVBool_t'}}
}
Index: clang/test/PCH/aarch64-sve-types.c
===================================================================
--- clang/test/PCH/aarch64-sve-types.c
+++ clang/test/PCH/aarch64-sve-types.c
@@ -18,4 +18,6 @@
__SVFloat32_t *f32;
__SVFloat64_t *f64;
+__SVBFloat16_t *bf16;
+
__SVBool_t *b8;
Index: clang/test/CodeGenObjC/aarch64-sve-types.m
===================================================================
--- clang/test/CodeGenObjC/aarch64-sve-types.m
+++ clang/test/CodeGenObjC/aarch64-sve-types.m
@@ -1,7 +1,7 @@
// RUN: not %clang_cc1 -triple aarch64-none-linux-gnu %s -emit-llvm -o - \
// RUN: 2>&1 | FileCheck %s
// RUN: not %clang_cc1 -triple aarch64-none-linux-gnu %s -emit-llvm -o - \
-// RUN: -target-feature +sve 2>&1 | FileCheck %s
+// RUN: -target-feature +sve,+bf16 2>&1 | FileCheck %s
// CHECK: error: cannot yet @encode type __SVInt8_t
const char s8[] = @encode(__SVInt8_t);
@@ -28,5 +28,8 @@
// CHECK: error: cannot yet @encode type __SVFloat64_t
const char f64[] = @encode(__SVFloat64_t);
+// CHECK: error: cannot yet @encode type __SVBFloat16_t
+const char bf16[] = @encode(__SVBFloat16_t);
+
// CHECK: error: cannot yet @encode type __SVBool_t
const char b8[] = @encode(__SVBool_t);
Index: clang/test/CodeGenCXX/aarch64-sve-typeinfo.cpp
===================================================================
--- clang/test/CodeGenCXX/aarch64-sve-typeinfo.cpp
+++ clang/test/CodeGenCXX/aarch64-sve-typeinfo.cpp
@@ -1,7 +1,7 @@
// RUN: %clang_cc1 -triple aarch64-none-linux-gnu %s -emit-llvm -o - \
// RUN: | FileCheck %s
// RUN: %clang_cc1 -triple aarch64-none-linux-gnu %s -emit-llvm -o - \
-// RUN: -target-feature +sve | FileCheck %s
+// RUN: -target-feature +sve,+bf16 | FileCheck %s
namespace std { class type_info; };
@@ -19,6 +19,8 @@
auto &f32 = typeid(__SVFloat32_t);
auto &f64 = typeid(__SVFloat64_t);
+auto &bf16 = typeid(__SVBFloat16_t);
+
auto &b8 = typeid(__SVBool_t);
// CHECK-DAG: @_ZTSu10__SVInt8_t = {{.*}} c"u10__SVInt8_t\00"
@@ -53,6 +55,9 @@
// CHECK-DAG: @_ZTSu13__SVFloat64_t = {{.*}} c"u13__SVFloat64_t\00"
// CHECK-DAG: @_ZTIu13__SVFloat64_t = {{.*}} @_ZTVN10__cxxabiv123__fundamental_type_infoE, {{.*}} @_ZTSu13__SVFloat64_t
+//
+// CHECK-DAG: @_ZTSu14__SVBFloat16_t = {{.*}} c"u14__SVBFloat16_t\00"
+// CHECK-DAG: @_ZTIu14__SVBFloat16_t = {{.*}} @_ZTVN10__cxxabiv123__fundamental_type_infoE, {{.*}} @_ZTSu14__SVBFloat16_t
// CHECK-DAG: @_ZTSu10__SVBool_t = {{.*}} c"u10__SVBool_t\00"
// CHECK-DAG: @_ZTIu10__SVBool_t = {{.*}} @_ZTVN10__cxxabiv123__fundamental_type_infoE, {{.*}} @_ZTSu10__SVBool_t
Index: clang/test/CodeGenCXX/aarch64-mangle-sve-vectors.cpp
===================================================================
--- clang/test/CodeGenCXX/aarch64-mangle-sve-vectors.cpp
+++ clang/test/CodeGenCXX/aarch64-mangle-sve-vectors.cpp
@@ -1,7 +1,7 @@
// RUN: %clang_cc1 -triple aarch64-none-linux-gnu %s -emit-llvm -o - \
// RUN: | FileCheck %s
// RUN: %clang_cc1 -triple aarch64-none-linux-gnu %s -emit-llvm -o - \
-// RUN: -target-feature +sve | FileCheck %s
+// RUN: -target-feature +sve,+bf16 | FileCheck %s
template<typename T> struct S {};
@@ -27,8 +27,10 @@
void f10(S<__SVFloat32_t>) {}
// CHECK: _Z3f111SIu13__SVFloat64_tE
void f11(S<__SVFloat64_t>) {}
-// CHECK: _Z3f121SIu10__SVBool_tE
-void f12(S<__SVBool_t>) {}
+// CHECK: _Z3f121SIu14__SVBFloat16_tE
+void f12(S<__SVBFloat16_t>) {}
+// CHECK: _Z3f131SIu10__SVBool_tE
+void f13(S<__SVBool_t>) {}
// The tuple types don't use the internal name for mangling.
@@ -98,3 +100,9 @@
void f44(S<__clang_svfloat64x3_t>) {}
// CHECK: _Z3f451SI13svfloat64x4_tE
void f45(S<__clang_svfloat64x4_t>) {}
+// CHECK: _Z3f461SI14svbfloat16x2_tE
+void f46(S<__clang_svbfloat16x2_t>) {}
+// CHECK: _Z3f471SI14svbfloat16x3_tE
+void f47(S<__clang_svbfloat16x3_t>) {}
+// CHECK: _Z3f481SI14svbfloat16x4_tE
+void f48(S<__clang_svbfloat16x4_t>) {}
Index: clang/test/CodeGen/aarch64-sve.c
===================================================================
--- clang/test/CodeGen/aarch64-sve.c
+++ clang/test/CodeGen/aarch64-sve.c
@@ -14,6 +14,7 @@
// CHECK-DEBUG: cannot yet generate debug info for SVE type '__SVFloat16_t'
// CHECK-DEBUG: cannot yet generate debug info for SVE type '__SVFloat32_t'
// CHECK-DEBUG: cannot yet generate debug info for SVE type '__SVFloat64_t'
+// CHECK-DEBUG: cannot yet generate debug info for SVE type '__SVBFloat16_t'
// CHECK-DEBUG: cannot yet generate debug info for SVE type '__SVBool_t'
// CHECK: @ptr = global <vscale x 16 x i8>* null, align 8
@@ -28,6 +29,7 @@
// CHECK: %f16 = alloca <vscale x 8 x half>, align 16
// CHECK: %f32 = alloca <vscale x 4 x float>, align 16
// CHECK: %f64 = alloca <vscale x 2 x double>, align 16
+// CHECK: %bf16 = alloca <vscale x 8 x bfloat>, align 16
// CHECK: %b8 = alloca <vscale x 16 x i1>, align 2
__SVInt8_t *ptr;
@@ -47,5 +49,7 @@
__SVFloat32_t f32;
__SVFloat64_t f64;
+ __SVBFloat16_t bf16;
+
__SVBool_t b8;
}
Index: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2819,7 +2819,7 @@
BugReporterContext &BRC, const ExplodedNode *EndPathNode,
PathSensitiveBugReport &BR) {
// Collect new constraints
- VisitNode(EndPathNode, BRC, BR);
+ addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
// Create a refutation manager
llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
@@ -2830,30 +2830,30 @@
const SymbolRef Sym = I.first;
auto RangeIt = I.second.begin();
- llvm::SMTExprRef Constraints = SMTConv::getRangeExpr(
+ llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
/*InRange=*/true);
while ((++RangeIt) != I.second.end()) {
- Constraints = RefutationSolver->mkOr(
- Constraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
- RangeIt->From(), RangeIt->To(),
- /*InRange=*/true));
+ SMTConstraints = RefutationSolver->mkOr(
+ SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
+ RangeIt->From(), RangeIt->To(),
+ /*InRange=*/true));
}
- RefutationSolver->addConstraint(Constraints);
+ RefutationSolver->addConstraint(SMTConstraints);
}
// And check for satisfiability
- Optional<bool> isSat = RefutationSolver->check();
- if (!isSat.hasValue())
+ Optional<bool> IsSAT = RefutationSolver->check();
+ if (!IsSAT.hasValue())
return;
- if (!isSat.getValue())
+ if (!IsSAT.getValue())
BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
}
-PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
- const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) {
+void FalsePositiveRefutationBRVisitor::addConstraints(
+ const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
// Collect new constraints
const ConstraintRangeTy &NewCs = N->getState()->get<ConstraintRange>();
ConstraintRangeTy::Factory &CF =
@@ -2863,10 +2863,19 @@
for (auto const &C : NewCs) {
const SymbolRef &Sym = C.first;
if (!Constraints.contains(Sym)) {
+ // This symbol is new, just add the constraint.
+ Constraints = CF.add(Constraints, Sym, C.second);
+ } else if (OverwriteConstraintsOnExistingSyms) {
+ // Overwrite the associated constraint of the Symbol.
+ Constraints = CF.remove(Constraints, Sym);
Constraints = CF.add(Constraints, Sym, C.second);
}
}
+}
+PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
+ const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) {
+ addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false);
return nullptr;
}
Index: clang/lib/StaticAnalyzer/Core/BugReporter.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ clang/lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -38,6 +38,7 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
#include "llvm/ADT/ArrayRef.h"
@@ -2783,7 +2784,7 @@
R->clearVisitors();
R->addVisitor(std::make_unique<FalsePositiveRefutationBRVisitor>());
- // We don't overrite the notes inserted by other visitors because the
+ // We don't overwrite the notes inserted by other visitors because the
// refutation manager does not add any new note to the path
generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC);
}
Index: clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
@@ -386,6 +386,8 @@
void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
PathSensitiveBugReport &BR) override;
+ void addConstraints(const ExplodedNode *N,
+ bool OverwriteConstraintsOnExistingSyms);
};
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
