clang::ento::Z3CrosscheckOracle Class Reference

The oracle will decide if a report should be accepted or rejected based on the results of the Z3 solver and the statistics of the queries of a report equivalenece class. More...

#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"

Public Types
enum	Z3Decision { AcceptReport , RejectReport , RejectEQClass }

Public Member Functions
	Z3CrosscheckOracle (const AnalyzerOptions &Opts)
Z3Decision	interpretQueryResult (const Z3CrosscheckVisitor::Z3Result &Meta)
	Updates the internal state with the new Z3Result and makes a decision how to proceed:

Detailed Description

The oracle will decide if a report should be accepted or rejected based on the results of the Z3 solver and the statistics of the queries of a report equivalenece class.

Definition at line 56 of file Z3CrosscheckVisitor.h.

Member Enumeration Documentation

Z3Decision

enum clang::ento::Z3CrosscheckOracle::Z3Decision

Enumerator
AcceptReport
RejectReport
RejectEQClass

Definition at line 60 of file Z3CrosscheckVisitor.h.

Constructor & Destructor Documentation

Z3CrosscheckOracle()

clang::ento::Z3CrosscheckOracle::Z3CrosscheckOracle ( const AnalyzerOptions &  Opts )

inlineexplicit

Definition at line 58 of file Z3CrosscheckVisitor.h.

Member Function Documentation

interpretQueryResult()

Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult

(

const Z3CrosscheckVisitor::Z3Result &

Meta

)

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.

All these thresholds are configurable via the analyzer options.

Refer to https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 to see why this heuristic was chosen.

Definition at line 123 of file Z3CrosscheckVisitor.cpp.

References AcceptReport, clang::ento::Z3CrosscheckVisitor::Z3Result::IsSAT, RejectEQClass, RejectReport, clang::ento::Z3CrosscheckVisitor::Z3Result::UsedRLimit, and clang::ento::Z3CrosscheckVisitor::Z3Result::Z3QueryTimeMilliseconds.

---

The documentation for this class was generated from the following files:

• include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
• lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp