#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"
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);
}
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();
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 =
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;
}
"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