================
@@ -44,21 +47,43 @@ class Z3CrosscheckVisitor final : public BugReporterVisitor
{
/// Holds the constraints in a given path.
ConstraintMap Constraints;
Z3Result &Result;
+ const AnalyzerOptions &Opts;
};
/// The oracle will decide if a report should be accepted or rejected based on
-/// the results of the Z3 solver.
+/// the results of the Z3 solver and the statistics of the queries of a report
+/// equivalenece class.
class Z3CrosscheckOracle {
public:
+ explicit Z3CrosscheckOracle(const AnalyzerOptions &Opts) : Opts(Opts) {}
+
enum Z3Decision {
- AcceptReport, // The report was SAT.
- RejectReport, // The report was UNSAT or UNDEF.
+ AcceptReport, // The report was SAT.
+ RejectReport, // The report was UNSAT or UNDEF.
+ RejectEQClass, // The heuristic suggests to skip the current eqclass.
};
- /// Makes a decision for accepting or rejecting the report based on the
- /// result of the corresponding Z3 query.
- static Z3Decision
- interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Query);
+ /// Updates the internal state with the new Z3Result and makes a decision how
+ /// to proceed:
+ /// - Accept the report if the Z3Result was SAT.
+ /// - Suggest dropping the report equvalence class based on the accumulated
+ /// statistics.
+ /// - Otherwise, reject the report if the Z3Result was UNSAT or UNDEF.
+ ///
+ /// Conditions for dropping the equivalence class:
+ /// - Accumulative time spent in Z3 checks is more than 700ms in the eqclass.
+ /// - Hit the 300ms query timeout in the report eqclass.
+ /// - Hit the 400'000 rlimit in the report eqclass.
+ ///
+ /// Refer to
+ /// https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 to
+ /// see why this heuristic was chosen.
+ Z3Decision interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Meta);
+
+private:
+ const AnalyzerOptions &Opts;
+ unsigned NumZ3QueriesDoneInEqClass = 0;
----------------
steakhal wrote:
Hmm, I dont think I use this anymore.
https://github.com/llvm/llvm-project/pull/95129
_______________________________________________
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
