215 lines · cpp
1//===- unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp ----------------===//2//3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.4// See https://llvm.org/LICENSE.txt for license information.5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception6//7//===----------------------------------------------------------------------===//8 9#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"10#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"11#include "gtest/gtest.h"12 13using namespace clang;14using namespace ento;15 16using Z3Result = Z3CrosscheckVisitor::Z3Result;17using Z3Decision = Z3CrosscheckOracle::Z3Decision;18 19static constexpr Z3Decision AcceptReport = Z3Decision::AcceptReport;20static constexpr Z3Decision RejectReport = Z3Decision::RejectReport;21static constexpr Z3Decision RejectEQClass = Z3Decision::RejectEQClass;22 23static constexpr std::optional<bool> SAT = true;24static constexpr std::optional<bool> UNSAT = false;25static constexpr std::optional<bool> UNDEF = std::nullopt;26 27static unsigned operator""_ms(unsigned long long ms) { return ms; }28static unsigned operator""_step(unsigned long long rlimit) { return rlimit; }29 30static const AnalyzerOptions DefaultOpts = [] {31 AnalyzerOptions Config;32#define ANALYZER_OPTION_DEPENDS_ON_USER_MODE(TYPE, NAME, CMDFLAG, DESC, \33 SHALLOW_VAL, DEEP_VAL) \34 ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEEP_VAL)35#define ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEFAULT_VAL) \36 Config.NAME = DEFAULT_VAL;37#include "clang/StaticAnalyzer/Core/AnalyzerOptions.def"38 39 // Remember to update the tests in this file when these values change.40 // Also update the doc comment of `interpretQueryResult`.41 assert(Config.Z3CrosscheckRLimitThreshold == 0);42 assert(Config.Z3CrosscheckTimeoutThreshold == 15'000_ms);43 // Usually, when the timeout/rlimit threshold is reached, Z3 only slightly44 // overshoots until it realizes that it overshoot and needs to back off.45 // Consequently, the measured timeout should be fairly close to the threshold.46 // Same reasoning applies to the rlimit too.47 return Config;48}();49 50static const AnalyzerOptions LimitedOpts = [] {51 AnalyzerOptions Config = DefaultOpts;52 Config.Z3CrosscheckEQClassTimeoutThreshold = 700_ms;53 Config.Z3CrosscheckTimeoutThreshold = 300_step;54 Config.Z3CrosscheckRLimitThreshold = 400'000_step;55 return Config;56}();57 58namespace {59 60template <const AnalyzerOptions &Opts>61class Z3CrosscheckOracleTest : public testing::Test {62public:63 Z3Decision interpretQueryResult(const Z3Result &Result) {64 return Oracle.interpretQueryResult(Result);65 }66 67private:68 Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(Opts);69};70 71using DefaultZ3CrosscheckOracleTest = Z3CrosscheckOracleTest<DefaultOpts>;72using LimitedZ3CrosscheckOracleTest = Z3CrosscheckOracleTest<LimitedOpts>;73 74TEST_F(DefaultZ3CrosscheckOracleTest, AcceptsFirstSAT) {75 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));76}77TEST_F(LimitedZ3CrosscheckOracleTest, AcceptsFirstSAT) {78 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));79}80 81TEST_F(DefaultZ3CrosscheckOracleTest, AcceptsSAT) {82 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));83 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));84}85TEST_F(LimitedZ3CrosscheckOracleTest, AcceptsSAT) {86 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));87 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));88}89 90TEST_F(DefaultZ3CrosscheckOracleTest, SATWhenItGoesOverTime) {91 // Even if it times out, if it is SAT, we should accept it.92 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 15'010_ms, 1000_step}));93}94TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItGoesOverTime) {95 // Even if it times out, if it is SAT, we should accept it.96 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 310_ms, 1000_step}));97}98 99TEST_F(DefaultZ3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {100 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 15'010_ms, 1000_step}));101}102TEST_F(LimitedZ3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {103 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));104}105 106TEST_F(DefaultZ3CrosscheckOracleTest, RejectsTimeout) {107 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));108 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));109 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 15'010_ms, 1000_step}));110}111TEST_F(LimitedZ3CrosscheckOracleTest, RejectsTimeout) {112 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));113 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));114 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 310_ms, 1000_step}));115}116 117TEST_F(DefaultZ3CrosscheckOracleTest, RejectsUNSATs) {118 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));119 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));120 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));121 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));122}123TEST_F(LimitedZ3CrosscheckOracleTest, RejectsUNSATs) {124 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));125 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));126 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));127 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));128}129 130// Testing cut heuristics of the two configurations:131// =================================================132 133TEST_F(DefaultZ3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) {134 // Simulate long queries, that barely doesn't trigger the timeout.135 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));136 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));137 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));138}139TEST_F(LimitedZ3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) {140 // Simulate long queries, that barely doesn't trigger the timeout.141 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));142 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));143 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 290_ms, 1000_step}));144}145 146TEST_F(DefaultZ3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) {147 // Simulate long queries, that barely doesn't trigger the timeout.148 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));149 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));150 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 14'990_ms, 1000_step}));151}152TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) {153 // Simulate long queries, that barely doesn't trigger the timeout.154 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));155 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));156 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 290_ms, 1000_step}));157}158 159// Z3CrosscheckEQClassTimeoutThreshold is disabled in default configuration, so160// it doesn't make sense to test that.161TEST_F(LimitedZ3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) {162 // Simulate quick, but many queries: 35 quick UNSAT queries.163 // 35*20ms = 700ms, which is equal to the 700ms threshold.164 for (int i = 0; i < 35; ++i) {165 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step}));166 }167 // Do one more to trigger the heuristic.168 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 1_ms, 1000_step}));169}170 171// Z3CrosscheckEQClassTimeoutThreshold is disabled in default configuration, so172// it doesn't make sense to test that.173TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItAttemptsManySmallQueries) {174 // Simulate quick, but many queries: 35 quick UNSAT queries.175 // 35*20ms = 700ms, which is equal to the 700ms threshold.176 for (int i = 0; i < 35; ++i) {177 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step}));178 }179 // Do one more to trigger the heuristic, but given this was SAT, we still180 // accept the query.181 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 200_ms, 1000_step}));182}183 184// Z3CrosscheckRLimitThreshold is disabled in default configuration, so it185// doesn't make sense to test that.186TEST_F(LimitedZ3CrosscheckOracleTest, RejectEQClassIfExhaustsRLimit) {187 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));188 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));189 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 25_ms, 405'000_step}));190}191 192// Z3CrosscheckRLimitThreshold is disabled in default configuration, so it193// doesn't make sense to test that.194TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItExhaustsRLimit) {195 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));196 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));197 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 405'000_step}));198}199 200// Demonstrate the weaknesses of the default configuration:201// ========================================================202 203TEST_F(DefaultZ3CrosscheckOracleTest, ManySlowQueriesHangTheAnalyzer) {204 // Simulate many slow queries: 250 slow UNSAT queries.205 // 250*14000ms = 3500s, ~1 hour. Since we disabled the total time limitation,206 // this eqclass would take roughly 1 hour to process.207 // It doesn't matter what rlimit the queries consume.208 for (int i = 0; i < 250; ++i) {209 ASSERT_EQ(RejectReport,210 interpretQueryResult({UNSAT, 14'000_ms, 1'000'000_step}));211 }212}213 214} // namespace215