105 lines
4.4 KiB
C++
105 lines
4.4 KiB
C++
#include <z3++.h>
|
|
|
|
#include <catch2/catch_test_macros.hpp>
|
|
|
|
#include "fold/report/finding.hpp"
|
|
#include "fold/symbolic/assumption_provenance.hpp"
|
|
#include "fold/symbolic/encoder.hpp"
|
|
#include "fold/symbolic/modeling_options.hpp"
|
|
|
|
using fold::Confidence;
|
|
using fold::ModelingOptions;
|
|
using fold::SymbolicEnv;
|
|
namespace sym = fold::symbolic;
|
|
|
|
namespace {
|
|
|
|
z3::expr bv(SymbolicEnv& env, const char* name) { return env.ctx().bv_const(name, 64); }
|
|
z3::expr bv(SymbolicEnv& env, int v) { return env.ctx().bv_val(v, 64); }
|
|
|
|
} // namespace
|
|
|
|
TEST_CASE("proveUnsat: empty ledger proves without provenance", "[provenance]") {
|
|
SymbolicEnv env = SymbolicEnv::create();
|
|
z3::solver solver(env.ctx(), "QF_BV");
|
|
z3::expr x = bv(env, "x");
|
|
// `x == x` is always true, so the negated goal `x != x` is UNSAT.
|
|
auto r = sym::proveUnsat(solver, env, x != x);
|
|
REQUIRE(r.proved);
|
|
REQUIRE(r.leaned_on.empty());
|
|
// No approximation => confidence stays Proved.
|
|
REQUIRE(sym::downgradeForProvenance(Confidence::Proved, r.leaned_on) == Confidence::Proved);
|
|
}
|
|
|
|
TEST_CASE("proveUnsat: proof that leans on a loop-bound pin is attributed", "[provenance]") {
|
|
SymbolicEnv env = SymbolicEnv::create();
|
|
z3::solver solver(env.ctx(), "QF_BV");
|
|
z3::expr iv = bv(env, "iv");
|
|
// Bounded unrolling pins the induction variable to iteration 0.
|
|
env.addTrackedAssumption(iv == bv(env, 0), sym::AssumptionKind::LoopBoundUnroll,
|
|
"loop iv 'iv' pinned to 0");
|
|
|
|
// The in-bound guard `iv < 6` is "always true" ONLY because of the pin, so
|
|
// the negated goal `iv >= 6` is UNSAT only under the tracked assumption.
|
|
auto r = sym::proveUnsat(solver, env, !(z3::slt(iv, bv(env, 6))));
|
|
REQUIRE(r.proved);
|
|
REQUIRE_FALSE(r.leaned_on.empty());
|
|
REQUIRE(r.leaned_on.front().kind == sym::AssumptionKind::LoopBoundUnroll);
|
|
|
|
// Provenance downgrades Proved -> Heuristic.
|
|
REQUIRE(sym::downgradeForProvenance(Confidence::Proved, r.leaned_on) == Confidence::Heuristic);
|
|
}
|
|
|
|
TEST_CASE("proveUnsat: a pin present but not needed keeps Proved", "[provenance]") {
|
|
SymbolicEnv env = SymbolicEnv::create();
|
|
z3::solver solver(env.ctx(), "QF_BV");
|
|
z3::expr iv = bv(env, "iv");
|
|
env.addTrackedAssumption(iv == bv(env, 0), sym::AssumptionKind::LoopBoundUnroll,
|
|
"loop iv 'iv' pinned to 0");
|
|
|
|
// A proof about an unrelated variable that holds regardless of the pin: the
|
|
// UNSAT core must NOT include the loop-bound tracker.
|
|
z3::expr y = bv(env, "y");
|
|
auto r = sym::proveUnsat(solver, env, y != y);
|
|
REQUIRE(r.proved);
|
|
REQUIRE(r.leaned_on.empty());
|
|
REQUIRE(sym::downgradeForProvenance(Confidence::Proved, r.leaned_on) == Confidence::Proved);
|
|
}
|
|
|
|
TEST_CASE("proveUnsat: a satisfiable goal is not proved", "[provenance]") {
|
|
SymbolicEnv env = SymbolicEnv::create();
|
|
z3::solver solver(env.ctx(), "QF_BV");
|
|
z3::expr iv = bv(env, "iv");
|
|
env.addTrackedAssumption(iv == bv(env, 0), sym::AssumptionKind::LoopBoundUnroll, "pin");
|
|
// `iv < 6` is satisfiable (iv could be anything if the pin isn't forced as a
|
|
// hard fact — and even with the pin, the goal `iv < 6` is SAT), so the
|
|
// negated-goal-style query on a non-tautology is not proved.
|
|
auto r = sym::proveUnsat(solver, env, z3::slt(iv, bv(env, 6)));
|
|
REQUIRE_FALSE(r.proved);
|
|
REQUIRE(r.leaned_on.empty());
|
|
}
|
|
|
|
TEST_CASE("shouldSuppressProof honours the loop-bound toggle", "[provenance]") {
|
|
std::vector<sym::AssumptionProvenance> leaned{{sym::AssumptionKind::LoopBoundUnroll, "pin"}};
|
|
|
|
ModelingOptions off; // all false
|
|
REQUIRE_FALSE(sym::shouldSuppressProof(leaned, off));
|
|
|
|
ModelingOptions on;
|
|
on.suppress_loop_bound_always_conditions = true;
|
|
REQUIRE(sym::shouldSuppressProof(leaned, on));
|
|
|
|
// A non-loop approximation is not suppressed by the loop-bound toggle.
|
|
std::vector<sym::AssumptionProvenance> ext{
|
|
{sym::AssumptionKind::ExternalSymbolConcretized, "edata"}};
|
|
REQUIRE_FALSE(sym::shouldSuppressProof(ext, on));
|
|
}
|
|
|
|
TEST_CASE("annotateMessageWithProvenance names the approximation", "[provenance]") {
|
|
std::vector<sym::AssumptionProvenance> leaned{{sym::AssumptionKind::LoopBoundUnroll, "pin"}};
|
|
const std::string msg = sym::annotateMessageWithProvenance("Condition is always true", leaned);
|
|
REQUIRE(msg.find("bounded-unroll loop bound") != std::string::npos);
|
|
|
|
// Empty leaned_on leaves the message untouched.
|
|
REQUIRE(sym::annotateMessageWithProvenance("unchanged", {}) == "unchanged");
|
|
}
|