================
@@ -17,43 +18,126 @@ using Z3Decision = Z3CrosscheckOracle::Z3Decision;
static constexpr Z3Decision AcceptReport = Z3Decision::AcceptReport;
static constexpr Z3Decision RejectReport = Z3Decision::RejectReport;
+static constexpr Z3Decision RejectEQClass = Z3Decision::RejectEQClass;
static constexpr std::optional<bool> SAT = true;
static constexpr std::optional<bool> UNSAT = false;
static constexpr std::optional<bool> UNDEF = std::nullopt;
+static unsigned operator""_ms(unsigned long long ms) { return ms; }
+static unsigned operator""_step(unsigned long long rlimit) { return rlimit; }
+
+static const AnalyzerOptions DefaultOpts = [] {
+ AnalyzerOptions Config;
+#define ANALYZER_OPTION_DEPENDS_ON_USER_MODE(TYPE, NAME, CMDFLAG, DESC,
\
+ SHALLOW_VAL, DEEP_VAL)
\
+ ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEEP_VAL)
+#define ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEFAULT_VAL)
\
+ Config.NAME = DEFAULT_VAL;
+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.def"
+
+ // Remember to update the tests in this file when these values change.
+ // Also update the doc comment of `interpretQueryResult`.
+ assert(Config.Z3CrosscheckRLimitThreshold == 400'000);
+ assert(Config.Z3CrosscheckTimeoutThreshold == 300 /*ms*/);
+ // Usually, when the timeout/rlimit threshold is reached, Z3 only slightly
+ // overshoots until it realizes that it overshoot and needs to back off.
+ // Consequently, the measured timeout should be fairly close to the
threshold.
+ // Same reasoning applies to the rlimit too.
+ return Config;
+}();
+
namespace {
-struct Z3CrosscheckOracleTest : public testing::Test {
- Z3Decision interpretQueryResult(const Z3Result &Result) const {
- return Z3CrosscheckOracle::interpretQueryResult(Result);
+class Z3CrosscheckOracleTest : public testing::Test {
+public:
+ Z3Decision interpretQueryResult(const Z3Result &Result) {
+ return Oracle.interpretQueryResult(Result);
}
+
+private:
+ Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(DefaultOpts);
};
TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) {
- ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
}
TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) {
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
- ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, SATWhenItGoesOverTime) {
+ // Even if it times out, if it is SAT, we should accept it.
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 310_ms, 1000_step}));
}
-TEST_F(Z3CrosscheckOracleTest, AcceptsFirstTimeout) {
- ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF}));
+TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
+ ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
}
-TEST_F(Z3CrosscheckOracleTest, AcceptsTimeout) {
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
- ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF}));
+TEST_F(Z3CrosscheckOracleTest, RejectsTimeout) {
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+ ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 310_ms, 1000_step}));
}
TEST_F(Z3CrosscheckOracleTest, RejectsUNSATs) {
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+}
+
+// Testing cut heuristics:
+// =======================
+
+TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) {
+ // Simulate long queries, that barely doesn't trigger the timeout.
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
+ ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) {
+ // Simulate long queries, that barely doesn't trigger the timeout.
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 290_ms, 1000_step}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) {
+ // Simulate quick, but many queries: 35 quick UNSAT queries.
+ // 35*20ms = 700ms, which is equal to the 700ms threshold.
+ for (int i = 0; i < 35; ++i) {
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step}));
+ }
+ // Do one more to trigger the heuristic.
+ ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 1_ms, 1000_step}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, SATWhenIfAttemptsManySmallQueries) {
+ // Simulate quick, but many queries: 35 quick UNSAT queries.
+ // 35*20ms = 700ms, which is equal to the 700ms threshold.
+ for (int i = 0; i < 35; ++i) {
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step}));
+ }
+ // Do one more to trigger the heuristic, but given this was SAT, we still
+ // accept the query.
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 200_ms, 1000_step}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfHitsRLimitTooManyTimes) {
----------------
NagyDonat wrote:
The name `"HitsRLimitTooManyTimes"` is a leftover from the earlier plan where
one `rlimit` overrun wasn't enough to discard the eqclass. (This also applies
for the next TC.)
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
