class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor {
private:
/// Holds the constraints in a given path
- // TODO: should we use a set?
- llvm::SmallVector<ConstraintRangeTy, 32> Constraints;
+ ConstraintRangeTy Constraints;
public:
- FalsePositiveRefutationBRVisitor() = default;
+ FalsePositiveRefutationBRVisitor();
void Profile(llvm::FoldingSetNodeID &ID) const override;
const ExplodedNode *PrevN,
BugReporterContext &BRC,
BugReport &BR) override;
+
+ void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
+ BugReport &BR) override;
};
namespace bugreporter {
return std::make_shared<PathDiagnosticEventPiece>(L, "Taint originated here");
}
-static bool
-areConstraintsUnfeasible(BugReporterContext &BRC,
- const llvm::SmallVector<ConstraintRangeTy, 32> &Cs) {
+static bool areConstraintsUnfeasible(BugReporterContext &BRC,
+ const ConstraintRangeTy &Cs) {
// Create a refutation manager
std::unique_ptr<ConstraintManager> RefutationMgr = CreateZ3ConstraintManager(
BRC.getStateManager(), BRC.getStateManager().getOwningEngine());
static_cast<SMTConstraintManager *>(RefutationMgr.get());
// Add constraints to the solver
- for (const auto &C : Cs)
- SMTRefutationMgr->addRangeConstraints(C);
+ SMTRefutationMgr->addRangeConstraints(Cs);
// And check for satisfiability
return SMTRefutationMgr->isModelFeasible().isConstrainedFalse();
}
+static void addNewConstraints(ConstraintRangeTy &Cs,
+ const ConstraintRangeTy &NewCs,
+ ConstraintRangeTy::Factory &CF) {
+ // Add constraints if we don't have them yet
+ for (auto const &C : NewCs) {
+ const SymbolRef &Sym = C.first;
+ if (!Cs.contains(Sym)) {
+ Cs = CF.add(Cs, Sym, C.second);
+ }
+ }
+}
+
+FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
+ : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
+
+void FalsePositiveRefutationBRVisitor::finalizeVisitor(
+ BugReporterContext &BRC, const ExplodedNode *EndPathNode, BugReport &BR) {
+ // Collect new constraints
+ VisitNode(EndPathNode, nullptr, BRC, BR);
+
+ // Create a new refutation manager and check feasibility
+ if (areConstraintsUnfeasible(BRC, Constraints))
+ BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
+}
+
std::shared_ptr<PathDiagnosticPiece>
FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N,
const ExplodedNode *PrevN,
BugReporterContext &BRC,
BugReport &BR) {
- // Collect the constraint for the current state
- const ConstraintRangeTy &CR = N->getState()->get<ConstraintRange>();
- Constraints.push_back(CR);
-
- // If there are no predecessor, we reached the root node. In this point,
- // a new refutation manager will be created and the path will be checked
- // for reachability
- if (PrevN->pred_size() == 0 && areConstraintsUnfeasible(BRC, Constraints)) {
- BR.markInvalid("Infeasible constraints", N->getLocationContext());
- }
+ // Collect new constraints
+ addNewConstraints(Constraints, N->getState()->get<ConstraintRange>(),
+ N->getState()->get_context<ConstraintRange>());
return nullptr;
}