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)
96 lines
3.6 KiB
C++
96 lines
3.6 KiB
C++
#include <catch2/catch_test_macros.hpp>
|
|
#include <vector>
|
|
|
|
#include "fold/symbolic/encoder.hpp"
|
|
#include "fold/symbolic/theory.hpp"
|
|
|
|
TEST_CASE("instantiateSummaryPredicateInContext substitutes positional args",
|
|
"[encoder][summary]") {
|
|
z3::context ctx;
|
|
std::vector<z3::expr> args;
|
|
args.push_back(ctx.bv_val(7, fold::kBitvecWidth));
|
|
args.push_back(ctx.bv_val(3, fold::kBitvecWidth));
|
|
|
|
// The body uses the formal argument naming the summary parser expects.
|
|
auto result = fold::instantiateSummaryPredicateInContext("(bvuge arg0 arg1)", args, ctx);
|
|
REQUIRE(result.has_value());
|
|
REQUIRE(result->simplify().is_true());
|
|
}
|
|
|
|
TEST_CASE("instantiateSummaryPredicateInContext returns false when predicate fails",
|
|
"[encoder][summary]") {
|
|
z3::context ctx;
|
|
std::vector<z3::expr> args;
|
|
args.push_back(ctx.bv_val(1, fold::kBitvecWidth));
|
|
args.push_back(ctx.bv_val(2, fold::kBitvecWidth));
|
|
|
|
auto result = fold::instantiateSummaryPredicateInContext("(bvuge arg0 arg1)", args, ctx);
|
|
REQUIRE(result.has_value());
|
|
REQUIRE(result->simplify().is_false());
|
|
}
|
|
|
|
TEST_CASE("instantiateSummaryPredicateInContext returns nullopt on empty body",
|
|
"[encoder][summary]") {
|
|
z3::context ctx;
|
|
std::vector<z3::expr> args;
|
|
args.push_back(ctx.bv_val(0, fold::kBitvecWidth));
|
|
|
|
auto result = fold::instantiateSummaryPredicateInContext("", args, ctx);
|
|
REQUIRE_FALSE(result.has_value());
|
|
}
|
|
|
|
TEST_CASE("instantiateSummaryPredicateInContext returns nullopt on syntactically invalid body",
|
|
"[encoder][summary]") {
|
|
z3::context ctx;
|
|
std::vector<z3::expr> args;
|
|
args.push_back(ctx.bv_val(0, fold::kBitvecWidth));
|
|
|
|
auto result = fold::instantiateSummaryPredicateInContext("(((not smtlib", args, ctx);
|
|
REQUIRE_FALSE(result.has_value());
|
|
}
|
|
|
|
TEST_CASE("instantiateSummaryPredicateInContext widens narrow bv args to BV-64",
|
|
"[encoder][summary]") {
|
|
z3::context ctx;
|
|
std::vector<z3::expr> args;
|
|
// 8-bit -1 (0xFF) should sign-extend to 0xFFFF'FFFF'FFFF'FFFF when widened
|
|
// to BV-64 by normalizeSummaryArg.
|
|
args.push_back(ctx.bv_val(-1, 8));
|
|
|
|
auto result =
|
|
fold::instantiateSummaryPredicateInContext("(= arg0 #xFFFFFFFFFFFFFFFF)", args, ctx);
|
|
REQUIRE(result.has_value());
|
|
REQUIRE(result->simplify().is_true());
|
|
}
|
|
|
|
TEST_CASE("instantiateSummaryExpr substitutes into a value expression", "[encoder][summary]") {
|
|
auto env = fold::SymbolicEnv::create();
|
|
std::vector<z3::expr> args;
|
|
args.push_back(env.ctx().bv_val(10, fold::kBitvecWidth));
|
|
args.push_back(env.ctx().bv_val(5, fold::kBitvecWidth));
|
|
|
|
auto result = fold::instantiateSummaryExpr("(bvadd arg0 arg1)", args, env);
|
|
REQUIRE(result.has_value());
|
|
REQUIRE(result->is_bv());
|
|
z3::expr expected = env.ctx().bv_val(15, fold::kBitvecWidth);
|
|
REQUIRE((result.value() == expected).simplify().is_true());
|
|
}
|
|
|
|
TEST_CASE("instantiateSummaryExpr returns nullopt on empty body", "[encoder][summary]") {
|
|
auto env = fold::SymbolicEnv::create();
|
|
std::vector<z3::expr> args;
|
|
auto result = fold::instantiateSummaryExpr("", args, env);
|
|
REQUIRE_FALSE(result.has_value());
|
|
}
|
|
|
|
TEST_CASE("instantiateSummaryPredicate evaluates an equality predicate over args",
|
|
"[encoder][summary]") {
|
|
auto env = fold::SymbolicEnv::create();
|
|
std::vector<z3::expr> args;
|
|
args.push_back(env.ctx().bv_val(42, fold::kBitvecWidth));
|
|
args.push_back(env.ctx().bv_val(42, fold::kBitvecWidth));
|
|
|
|
auto result = fold::instantiateSummaryPredicate("(= arg0 arg1)", args, env);
|
|
REQUIRE(result.has_value());
|
|
REQUIRE(result->simplify().is_true());
|
|
}
|