a51cdf5748
Multi-phase work merged into one commit:
* M19: flow-sensitive guard tracking (stmtAlwaysExits, walkIf early-exit)
* M20–M27: non-null marking across deref, addr-of, callsite preconds,
if/while/switch guards, AddrOf-of-subexpr, CFG-block-scoped maps
* M30 Phase A: dialect-agnostic SourceLoc + LocationMapper + frontend/
boundary marker; ClangLocationMapper wired through SafetyObserver
* M30 Phase B v2: QueryTracer + 13 SafetyObserver hooks migrated to
ir::Expr / ir::Call / ir::MemberRef / ir::Symbol / ir::SourceLoc
* M30 Phase C/D/D2/D3: ir::Symbol, ir::Expr (with Kind), ir::Call,
ir::MemberRef opaque types; ir_expr_clang.cpp houses the clang
adapters; encodeExpr migrated to switch(kind) dispatch
Scout-rule extractions from encoder.cpp (2800 → 2371 lines):
* encoder_callee_predicates.{hpp,cpp} — isMallocLikeCall, isFreeCall,
isAssertCall as pure std::string_view predicates
* encoder_type_queries.{hpp,cpp} — typeSizeBytes, sourceWidth,
isUnsignedLike, byteWidthExpr
* encoder_callee_names.{hpp,cpp} — calleeName, qualifiedFunctionName,
qualifiedCalleeName (with internal-linkage @-suffix)
* encoder_coerce.{hpp,cpp} — coerceToBv, coerceToExactBv, coerceToBool,
coerceToType (BV-64 storage model documented at the boundary)
* encoder_reachability.{hpp,cpp} — ReachabilityCounter impl, markEncoded,
recordEncoded, recordBailedNode, public profiling glue
* encoder_summary_instantiate.cpp — SMT-LIB summary substitution
(instantiateSummaryExpr / Predicate / PredicateInContext +
applySummaryParamPost; kills the redundant *Impl pass-through layer)
100 lines
4.1 KiB
C++
100 lines
4.1 KiB
C++
#include <catch2/catch_test_macros.hpp>
|
|
|
|
#include "fold/symbolic/encoder.hpp"
|
|
#include "fold/symbolic/encoder_coerce.hpp"
|
|
#include "fold/symbolic/theory.hpp"
|
|
|
|
namespace {
|
|
|
|
fold::SymbolicEnv make_env() { return fold::SymbolicEnv::create(); }
|
|
|
|
z3::expr bv(fold::SymbolicEnv& env, std::uint64_t value, unsigned width) {
|
|
return env.ctx().bv_val(value, width);
|
|
}
|
|
|
|
bool bv_eq(const z3::expr& lhs, std::uint64_t expected, unsigned width) {
|
|
z3::expr target = lhs.ctx().bv_val(expected, width);
|
|
z3::expr eq = (lhs == target).simplify();
|
|
return eq.is_true();
|
|
}
|
|
|
|
} // namespace
|
|
|
|
TEST_CASE("coerceToBv: bv already at kBitvecWidth round-trips unchanged", "[encoder][coerce][bv]") {
|
|
auto env = make_env();
|
|
z3::expr v = bv(env, 0xDEAD'BEEF'CAFE'BABEULL, fold::kBitvecWidth);
|
|
z3::expr out = fold::coerceToBv(env, v);
|
|
REQUIRE(out.is_bv());
|
|
REQUIRE(out.get_sort().bv_size() == fold::kBitvecWidth);
|
|
REQUIRE(bv_eq(out, 0xDEAD'BEEF'CAFE'BABEULL, fold::kBitvecWidth));
|
|
}
|
|
|
|
TEST_CASE("coerceToBv: narrow signed bv sign-extends to kBitvecWidth", "[encoder][coerce][bv]") {
|
|
auto env = make_env();
|
|
// 8-bit two's-complement -1
|
|
z3::expr v = bv(env, 0xFF, 8);
|
|
z3::expr out = fold::coerceToBv(env, v, /*width=*/8, /*is_unsigned=*/false);
|
|
REQUIRE(out.get_sort().bv_size() == fold::kBitvecWidth);
|
|
// Sign-extended -1 in 64-bit = 0xFFFF'FFFF'FFFF'FFFF
|
|
REQUIRE(bv_eq(out, 0xFFFF'FFFF'FFFF'FFFFULL, fold::kBitvecWidth));
|
|
}
|
|
|
|
TEST_CASE("coerceToBv: narrow unsigned bv zero-extends to kBitvecWidth", "[encoder][coerce][bv]") {
|
|
auto env = make_env();
|
|
z3::expr v = bv(env, 0xFF, 8);
|
|
z3::expr out = fold::coerceToBv(env, v, /*width=*/8, /*is_unsigned=*/true);
|
|
REQUIRE(out.get_sort().bv_size() == fold::kBitvecWidth);
|
|
REQUIRE(bv_eq(out, 0xFFULL, fold::kBitvecWidth));
|
|
}
|
|
|
|
TEST_CASE("coerceToBv: wide bv truncates at the requested width then re-widens",
|
|
"[encoder][coerce][bv]") {
|
|
auto env = make_env();
|
|
// 64-bit value with bits set above the source-width-32 truncation point.
|
|
z3::expr v = bv(env, 0xFFFF'FFFF'AAAA'BBBBULL, fold::kBitvecWidth);
|
|
z3::expr out = fold::coerceToBv(env, v, /*width=*/32, /*is_unsigned=*/true);
|
|
REQUIRE(out.get_sort().bv_size() == fold::kBitvecWidth);
|
|
// Truncated to 32 bits → 0xAAAABBBB, then zero-extended → 0xAAAABBBB.
|
|
REQUIRE(bv_eq(out, 0xAAAA'BBBBULL, fold::kBitvecWidth));
|
|
}
|
|
|
|
TEST_CASE("coerceToBv: bool maps to 1/0 at width then widens", "[encoder][coerce][bv]") {
|
|
auto env = make_env();
|
|
z3::expr out_true = fold::coerceToBv(env, env.ctx().bool_val(true));
|
|
z3::expr out_false = fold::coerceToBv(env, env.ctx().bool_val(false));
|
|
REQUIRE(out_true.get_sort().bv_size() == fold::kBitvecWidth);
|
|
REQUIRE(bv_eq(out_true, 1, fold::kBitvecWidth));
|
|
REQUIRE(bv_eq(out_false, 0, fold::kBitvecWidth));
|
|
}
|
|
|
|
TEST_CASE("coerceToExactBv: leaves narrow result at exact width", "[encoder][coerce][exact]") {
|
|
auto env = make_env();
|
|
z3::expr v = bv(env, 0xFFFF'FFFF'AAAA'BBBBULL, fold::kBitvecWidth);
|
|
z3::expr out = fold::coerceToExactBv(env, v, /*width=*/32, /*is_unsigned=*/true);
|
|
REQUIRE(out.is_bv());
|
|
REQUIRE(out.get_sort().bv_size() == 32);
|
|
REQUIRE(bv_eq(out, 0xAAAA'BBBBULL, 32));
|
|
}
|
|
|
|
TEST_CASE("coerceToExactBv: bool widens to requested bv width", "[encoder][coerce][exact]") {
|
|
auto env = make_env();
|
|
z3::expr out = fold::coerceToExactBv(env, env.ctx().bool_val(true),
|
|
/*width=*/16, /*is_unsigned=*/true);
|
|
REQUIRE(out.get_sort().bv_size() == 16);
|
|
REQUIRE(bv_eq(out, 1, 16));
|
|
}
|
|
|
|
TEST_CASE("coerceToBool: bv compares against zero at its own width", "[encoder][coerce][bool]") {
|
|
auto env = make_env();
|
|
z3::expr zero8 = bv(env, 0, 8);
|
|
z3::expr one8 = bv(env, 1, 8);
|
|
REQUIRE(fold::coerceToBool(env, zero8).simplify().is_false());
|
|
REQUIRE(fold::coerceToBool(env, one8).simplify().is_true());
|
|
}
|
|
|
|
TEST_CASE("coerceToBool: identity on a bool expression", "[encoder][coerce][bool]") {
|
|
auto env = make_env();
|
|
z3::expr t = env.ctx().bool_val(true);
|
|
REQUIRE(fold::coerceToBool(env, t).is_bool());
|
|
REQUIRE(fold::coerceToBool(env, t).simplify().is_true());
|
|
}
|