240 lines
9 KiB
C++
240 lines
9 KiB
C++
#include <array>
|
|
#include <catch2/catch_test_macros.hpp>
|
|
#include <cstddef>
|
|
|
|
#include "fold/ir/access_path.hpp"
|
|
#include "fold/symbolic/encoder.hpp"
|
|
#include "fold/symbolic/guarded_facts.hpp"
|
|
|
|
namespace {
|
|
|
|
fold::ir::Symbol synthSymbol(std::size_t id) {
|
|
static const std::array<int, 16> slots{};
|
|
return fold::ir::Symbol{static_cast<const void*>(&slots.at(id))};
|
|
}
|
|
|
|
fold::ir::AccessPath synthPath(std::size_t id) {
|
|
return fold::ir::AccessPath::local(synthSymbol(id), "value", "test").field("count");
|
|
}
|
|
|
|
} // namespace
|
|
|
|
TEST_CASE("GuardedFactStore returns unguarded range facts as fallback",
|
|
"[symbolic][guarded-facts]") {
|
|
z3::context ctx;
|
|
fold::symbolic::GuardedFactStore store;
|
|
const auto subject = synthPath(1);
|
|
|
|
store.setRange(subject, fold::IntInterval{2, 8, false});
|
|
|
|
auto range = store.range(subject, ctx.bool_val(true));
|
|
REQUIRE(range.has_value());
|
|
CHECK(range->lo == 2);
|
|
CHECK(range->hi == 8);
|
|
}
|
|
|
|
TEST_CASE("GuardedFactStore returns facts when current path implies guard",
|
|
"[symbolic][guarded-facts]") {
|
|
z3::context ctx;
|
|
fold::symbolic::GuardedFactStore store;
|
|
const auto subject = synthPath(2);
|
|
z3::expr x = ctx.bv_const("x", fold::kBitvecWidth);
|
|
z3::expr zero = ctx.bv_val(0, fold::kBitvecWidth);
|
|
z3::expr five = ctx.bv_val(5, fold::kBitvecWidth);
|
|
|
|
store.markNonNull(subject, fold::symbolic::FactGuard::when(x != zero));
|
|
store.setRange(subject, fold::IntInterval{1, 10, false},
|
|
fold::symbolic::FactGuard::when(x != zero));
|
|
|
|
z3::expr current_path = x == five;
|
|
CHECK(store.isNonNull(subject, current_path, 100));
|
|
auto range = store.range(subject, current_path, 100);
|
|
REQUIRE(range.has_value());
|
|
CHECK(range->lo == 1);
|
|
}
|
|
|
|
TEST_CASE("GuardedFactStore ignores guarded facts not implied by current path",
|
|
"[symbolic][guarded-facts]") {
|
|
z3::context ctx;
|
|
fold::symbolic::GuardedFactStore store;
|
|
const auto subject = synthPath(3);
|
|
z3::expr flag = ctx.bool_const("flag");
|
|
|
|
store.markNonZero(subject, fold::symbolic::FactGuard::when(flag));
|
|
store.setRange(subject, fold::IntInterval{4, 4, false}, fold::symbolic::FactGuard::when(flag));
|
|
|
|
CHECK_FALSE(store.isNonZero(subject, !flag, 100));
|
|
CHECK_FALSE(store.range(subject, !flag, 100).has_value());
|
|
}
|
|
|
|
TEST_CASE("GuardedFactStore resolves latest matching fact and preserves subjects",
|
|
"[symbolic][guarded-facts]") {
|
|
z3::context ctx;
|
|
fold::symbolic::GuardedFactStore store;
|
|
const auto subject = synthPath(4);
|
|
const auto other = synthPath(5);
|
|
|
|
store.setRange(subject, fold::IntInterval{1, 2, false});
|
|
store.setRange(subject, fold::IntInterval{7, 9, false});
|
|
store.setRange(other, fold::IntInterval{20, 30, false});
|
|
|
|
auto range = store.range(subject, ctx.bool_val(true));
|
|
REQUIRE(range.has_value());
|
|
CHECK(range->lo == 7);
|
|
CHECK(range->hi == 9);
|
|
|
|
auto other_range = store.range(other, ctx.bool_val(true));
|
|
REQUIRE(other_range.has_value());
|
|
CHECK(other_range->lo == 20);
|
|
}
|
|
|
|
TEST_CASE("GuardedFactStore stores equality and member value facts", "[symbolic][guarded-facts]") {
|
|
z3::context ctx;
|
|
fold::symbolic::GuardedFactStore store;
|
|
const auto eq_subject = synthPath(6);
|
|
const auto member_subject = synthPath(7);
|
|
z3::expr eq_value = ctx.bv_val(42, fold::kBitvecWidth);
|
|
z3::expr member_value = ctx.bv_val(99, fold::kBitvecWidth);
|
|
|
|
store.setEquality(eq_subject, eq_value);
|
|
store.setMemberValue(member_subject, member_value);
|
|
|
|
auto equality = store.equality(eq_subject, ctx.bool_val(true));
|
|
auto member = store.memberValue(member_subject, ctx.bool_val(true));
|
|
REQUIRE(equality.has_value());
|
|
REQUIRE(member.has_value());
|
|
CHECK(z3::eq(*equality, eq_value));
|
|
CHECK(z3::eq(*member, member_value));
|
|
}
|
|
|
|
TEST_CASE("GuardedFactStore join collapses facts proved by both branches",
|
|
"[symbolic][guarded-facts][join]") {
|
|
z3::context ctx;
|
|
fold::symbolic::GuardedFactStore then_store;
|
|
fold::symbolic::GuardedFactStore else_store;
|
|
const auto subject = synthPath(8);
|
|
z3::expr cond = ctx.bool_const("cond");
|
|
|
|
then_store.markNonNull(subject);
|
|
else_store.markNonNull(subject);
|
|
then_store.setRange(subject, fold::IntInterval{1, 3, false});
|
|
else_store.setRange(subject, fold::IntInterval{1, 3, false});
|
|
|
|
auto joined = fold::symbolic::GuardedFactStore::joinBranches(
|
|
then_store, fold::symbolic::FactGuard::when(cond), else_store,
|
|
fold::symbolic::FactGuard::when(!cond));
|
|
|
|
CHECK(joined.isNonNull(subject, ctx.bool_val(true), 100));
|
|
auto range = joined.range(subject, ctx.bool_val(true), 100);
|
|
REQUIRE(range.has_value());
|
|
CHECK(range->lo == 1);
|
|
CHECK(range->hi == 3);
|
|
}
|
|
|
|
TEST_CASE("GuardedFactStore join retains branch-specific alternatives under guards",
|
|
"[symbolic][guarded-facts][join]") {
|
|
z3::context ctx;
|
|
fold::symbolic::GuardedFactStore then_store;
|
|
fold::symbolic::GuardedFactStore else_store;
|
|
const auto subject = synthPath(9);
|
|
z3::expr cond = ctx.bool_const("cond");
|
|
|
|
then_store.setRange(subject, fold::IntInterval{1, 2, false});
|
|
else_store.setRange(subject, fold::IntInterval{7, 8, false});
|
|
|
|
auto joined = fold::symbolic::GuardedFactStore::joinBranches(
|
|
then_store, fold::symbolic::FactGuard::when(cond), else_store,
|
|
fold::symbolic::FactGuard::when(!cond));
|
|
|
|
CHECK_FALSE(joined.range(subject, ctx.bool_val(true), 100).has_value());
|
|
|
|
auto then_range = joined.range(subject, cond, 100);
|
|
REQUIRE(then_range.has_value());
|
|
CHECK(then_range->lo == 1);
|
|
CHECK(then_range->hi == 2);
|
|
|
|
auto else_range = joined.range(subject, !cond, 100);
|
|
REQUIRE(else_range.has_value());
|
|
CHECK(else_range->lo == 7);
|
|
CHECK(else_range->hi == 8);
|
|
}
|
|
|
|
TEST_CASE("GuardedFactStore join conjoins original fact guards with branch guards",
|
|
"[symbolic][guarded-facts][join]") {
|
|
z3::context ctx;
|
|
fold::symbolic::GuardedFactStore then_store;
|
|
fold::symbolic::GuardedFactStore else_store;
|
|
const auto subject = synthPath(10);
|
|
z3::expr cond = ctx.bool_const("cond");
|
|
z3::expr local_guard = ctx.bool_const("local_guard");
|
|
|
|
then_store.markNonZero(subject, fold::symbolic::FactGuard::when(local_guard));
|
|
|
|
auto joined = fold::symbolic::GuardedFactStore::joinBranches(
|
|
then_store, fold::symbolic::FactGuard::when(cond), else_store,
|
|
fold::symbolic::FactGuard::when(!cond));
|
|
|
|
CHECK(joined.isNonZero(subject, cond && local_guard, 100));
|
|
CHECK_FALSE(joined.isNonZero(subject, cond && !local_guard, 100));
|
|
CHECK_FALSE(joined.isNonZero(subject, !cond && local_guard, 100));
|
|
}
|
|
|
|
TEST_CASE("GuardedFactStore degrades precision when guard feasibility is unknown",
|
|
"[symbolic][guarded-facts]") {
|
|
z3::context guard_ctx;
|
|
z3::context path_ctx;
|
|
fold::symbolic::GuardedFactStore store;
|
|
fold::EncodingPrecisionContext precision;
|
|
const auto subject = synthPath(11);
|
|
store.markNonNull(subject,
|
|
fold::symbolic::FactGuard::when(guard_ctx.bool_const("foreign_guard")));
|
|
|
|
CHECK_FALSE(store.isNonNull(subject, path_ctx.bool_val(true), 100, &precision));
|
|
CHECK(precision.isImprecise());
|
|
}
|
|
|
|
TEST_CASE("SymbolicEnv exposes guarded fact reads against current path",
|
|
"[symbolic][guarded-facts][env]") {
|
|
auto env = fold::SymbolicEnv::create();
|
|
const auto subject = synthPath(12);
|
|
z3::expr x = env.ctx().bv_const("env_guard_x", fold::kBitvecWidth);
|
|
z3::expr zero = env.ctx().bv_val(0, fold::kBitvecWidth);
|
|
|
|
env.markFactNonZero(subject, fold::symbolic::FactGuard::when(x != zero));
|
|
env.setFactRange(subject, fold::IntInterval{1, 32, false},
|
|
fold::symbolic::FactGuard::when(x != zero));
|
|
|
|
env.setPath(x == env.ctx().bv_val(7, fold::kBitvecWidth));
|
|
CHECK(env.isFactNonZero(subject, 100));
|
|
auto range = env.factRange(subject, 100);
|
|
REQUIRE(range.has_value());
|
|
CHECK(range->lo == 1);
|
|
CHECK(range->hi == 32);
|
|
|
|
env.setPath(x == zero);
|
|
CHECK_FALSE(env.isFactNonZero(subject, 100));
|
|
CHECK_FALSE(env.factRange(subject, 100).has_value());
|
|
}
|
|
|
|
TEST_CASE("SymbolicEnv clears only AccessPath facts below a mutated root",
|
|
"[symbolic][guarded-facts][env][havoc]") {
|
|
auto env = fold::SymbolicEnv::create();
|
|
auto root = fold::ir::AccessPath::synthetic("doc");
|
|
auto size = root.field("sections").stableQuery(fold::ir::AccessKind::Size);
|
|
auto title = root.field("title");
|
|
auto other = fold::ir::AccessPath::synthetic("other").field("sections");
|
|
|
|
env.setRange(size, fold::IntInterval{1, 8, false});
|
|
env.setFactRange(size, fold::IntInterval{1, 8, false});
|
|
env.markDefinitelyNonNull(title);
|
|
env.setRange(other, fold::IntInterval{2, 9, false});
|
|
env.setFactRange(other, fold::IntInterval{2, 9, false});
|
|
|
|
env.clearAccessPathFacts(root);
|
|
|
|
CHECK_FALSE(env.tryGetRange(size).has_value());
|
|
CHECK_FALSE(env.factRange(size, 100).has_value());
|
|
CHECK_FALSE(env.isDefinitelyNonNull(title));
|
|
REQUIRE(env.tryGetRange(other).has_value());
|
|
REQUIRE(env.factRange(other, 100).has_value());
|
|
}
|