mirror of
https://github.com/llvm/llvm-project.git
synced 2025-04-26 22:56:05 +00:00
5f6b714507
This simplifies #120239 Addresses my comment at: https://github.com/llvm/llvm-project/pull/120239#issuecomment-2574600543 CPP-5920
215 lines
9.6 KiB
C++
215 lines
9.6 KiB
C++
//===- unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp ----------------===//
|
|
//
|
|
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
|
// See https://llvm.org/LICENSE.txt for license information.
|
|
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
|
//
|
|
//===----------------------------------------------------------------------===//
|
|
|
|
#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
|
|
#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
|
|
#include "gtest/gtest.h"
|
|
|
|
using namespace clang;
|
|
using namespace ento;
|
|
|
|
using Z3Result = Z3CrosscheckVisitor::Z3Result;
|
|
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 == 0);
|
|
assert(Config.Z3CrosscheckTimeoutThreshold == 15'000_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;
|
|
}();
|
|
|
|
static const AnalyzerOptions LimitedOpts = [] {
|
|
AnalyzerOptions Config = DefaultOpts;
|
|
Config.Z3CrosscheckEQClassTimeoutThreshold = 700_ms;
|
|
Config.Z3CrosscheckTimeoutThreshold = 300_step;
|
|
Config.Z3CrosscheckRLimitThreshold = 400'000_step;
|
|
return Config;
|
|
}();
|
|
|
|
namespace {
|
|
|
|
template <const AnalyzerOptions &Opts>
|
|
class Z3CrosscheckOracleTest : public testing::Test {
|
|
public:
|
|
Z3Decision interpretQueryResult(const Z3Result &Result) {
|
|
return Oracle.interpretQueryResult(Result);
|
|
}
|
|
|
|
private:
|
|
Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(Opts);
|
|
};
|
|
|
|
using DefaultZ3CrosscheckOracleTest = Z3CrosscheckOracleTest<DefaultOpts>;
|
|
using LimitedZ3CrosscheckOracleTest = Z3CrosscheckOracleTest<LimitedOpts>;
|
|
|
|
TEST_F(DefaultZ3CrosscheckOracleTest, AcceptsFirstSAT) {
|
|
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
|
|
}
|
|
TEST_F(LimitedZ3CrosscheckOracleTest, AcceptsFirstSAT) {
|
|
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
|
|
}
|
|
|
|
TEST_F(DefaultZ3CrosscheckOracleTest, AcceptsSAT) {
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
|
|
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
|
|
}
|
|
TEST_F(LimitedZ3CrosscheckOracleTest, AcceptsSAT) {
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
|
|
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
|
|
}
|
|
|
|
TEST_F(DefaultZ3CrosscheckOracleTest, SATWhenItGoesOverTime) {
|
|
// Even if it times out, if it is SAT, we should accept it.
|
|
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 15'010_ms, 1000_step}));
|
|
}
|
|
TEST_F(LimitedZ3CrosscheckOracleTest, 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(DefaultZ3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
|
|
ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 15'010_ms, 1000_step}));
|
|
}
|
|
TEST_F(LimitedZ3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
|
|
ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
|
|
}
|
|
|
|
TEST_F(DefaultZ3CrosscheckOracleTest, RejectsTimeout) {
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
|
|
ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 15'010_ms, 1000_step}));
|
|
}
|
|
TEST_F(LimitedZ3CrosscheckOracleTest, 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(DefaultZ3CrosscheckOracleTest, RejectsUNSATs) {
|
|
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}));
|
|
}
|
|
TEST_F(LimitedZ3CrosscheckOracleTest, RejectsUNSATs) {
|
|
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 of the two configurations:
|
|
// =================================================
|
|
|
|
TEST_F(DefaultZ3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) {
|
|
// Simulate long queries, that barely doesn't trigger the timeout.
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));
|
|
}
|
|
TEST_F(LimitedZ3CrosscheckOracleTest, 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(DefaultZ3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) {
|
|
// Simulate long queries, that barely doesn't trigger the timeout.
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));
|
|
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 14'990_ms, 1000_step}));
|
|
}
|
|
TEST_F(LimitedZ3CrosscheckOracleTest, 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}));
|
|
}
|
|
|
|
// Z3CrosscheckEQClassTimeoutThreshold is disabled in default configuration, so
|
|
// it doesn't make sense to test that.
|
|
TEST_F(LimitedZ3CrosscheckOracleTest, 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}));
|
|
}
|
|
|
|
// Z3CrosscheckEQClassTimeoutThreshold is disabled in default configuration, so
|
|
// it doesn't make sense to test that.
|
|
TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItAttemptsManySmallQueries) {
|
|
// 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}));
|
|
}
|
|
|
|
// Z3CrosscheckRLimitThreshold is disabled in default configuration, so it
|
|
// doesn't make sense to test that.
|
|
TEST_F(LimitedZ3CrosscheckOracleTest, RejectEQClassIfExhaustsRLimit) {
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
|
|
ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 25_ms, 405'000_step}));
|
|
}
|
|
|
|
// Z3CrosscheckRLimitThreshold is disabled in default configuration, so it
|
|
// doesn't make sense to test that.
|
|
TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItExhaustsRLimit) {
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
|
|
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
|
|
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 405'000_step}));
|
|
}
|
|
|
|
// Demonstrate the weaknesses of the default configuration:
|
|
// ========================================================
|
|
|
|
TEST_F(DefaultZ3CrosscheckOracleTest, ManySlowQueriesHangTheAnalyzer) {
|
|
// Simulate many slow queries: 250 slow UNSAT queries.
|
|
// 250*14000ms = 3500s, ~1 hour. Since we disabled the total time limitation,
|
|
// this eqclass would take roughly 1 hour to process.
|
|
// It doesn't matter what rlimit the queries consume.
|
|
for (int i = 0; i < 250; ++i) {
|
|
ASSERT_EQ(RejectReport,
|
|
interpretQueryResult({UNSAT, 14'000_ms, 1'000'000_step}));
|
|
}
|
|
}
|
|
|
|
} // namespace
|