2dcbdbc75d
Preserve source, binary, and runtime evidence boundaries while making precision and performance regressions reproducible. - decompose analysis orchestration into bounded modules - add differential, metamorphic, organic, and Yams change-time gates - fix detector, P-Code, fuzz sanitizer, and report identity precision
117 lines
4.7 KiB
C++
117 lines
4.7 KiB
C++
// Matrix row Z10 — confirm Z3 pretty-printer let-bindings are enabled
|
|
// for serialised summaries so shared subterms collapse on the wire.
|
|
//
|
|
// Test pins:
|
|
// 1. A body with shared subterms serialises to a string containing
|
|
// `let ` (let-bindings are active).
|
|
// 2. The let-compacted body round-trips through deserialize() back
|
|
// to a structurally-equivalent expression (semantic-preserving).
|
|
// 3. A body with no shared structure does NOT bloat — same length
|
|
// class before vs after compaction.
|
|
|
|
#include <z3++.h>
|
|
|
|
#include <catch2/catch_test_macros.hpp>
|
|
#include <string>
|
|
|
|
#include "fold/symbolic/encoder.hpp"
|
|
#include "fold/symbolic/serialize.hpp"
|
|
#include "fold/symbolic/summary_encoder.hpp"
|
|
|
|
namespace {
|
|
|
|
// Build a synthetic FunctionSummarized whose return_value contains
|
|
// shared subterms ACROSS BRANCHES of an ite. simplify() can't collapse
|
|
// these into one occurrence (the branches are semantically distinct
|
|
// arithmetic), so the let-binding factor-out remains visible after
|
|
// adaptSerializedBody's terminal simplify.
|
|
fold::FunctionSummarized makeSharedSubtermSummary() {
|
|
auto env = fold::SymbolicEnv::create();
|
|
z3::context& c = env.ctx();
|
|
z3::expr a = c.bv_const("a", 64);
|
|
z3::expr b = c.bv_const("b", 64);
|
|
z3::expr sum = a + b;
|
|
z3::expr diff = a - b;
|
|
z3::expr cond = a > c.bv_val(0, 64);
|
|
// Two arithmetically-distinct ite arms each reuse sum + diff —
|
|
// simplify can rewrite within each arm but can't merge across.
|
|
z3::expr then_arm = sum * diff;
|
|
z3::expr else_arm = sum + diff;
|
|
z3::expr body = z3::ite(cond, then_arm * then_arm, else_arm + else_arm);
|
|
return fold::FunctionSummarized{
|
|
.env = std::move(env),
|
|
.inputs = {a, b},
|
|
.return_value = body,
|
|
.soundness = fold::SoundnessTag{},
|
|
};
|
|
}
|
|
|
|
} // namespace
|
|
|
|
TEST_CASE("serialize: shared subterms collapse via z3 `let` bindings", "[serialize][z10][let]") {
|
|
auto fs = makeSharedSubtermSummary();
|
|
auto serialized =
|
|
fold::serialize("test-id", "shared_test", "input.cpp", 1, 1, "signature_key", fs);
|
|
REQUIRE(serialized.body_smt.find("let ") != std::string::npos);
|
|
}
|
|
|
|
TEST_CASE("serialize: let-compacted body round-trips structurally", "[serialize][z10][roundtrip]") {
|
|
auto fs = makeSharedSubtermSummary();
|
|
auto serialized =
|
|
fold::serialize("test-id", "shared_test", "input.cpp", 1, 1, "signature_key", fs);
|
|
|
|
z3::context fresh;
|
|
auto restored = fold::deserialize(fresh, serialized);
|
|
REQUIRE(restored.has_value());
|
|
|
|
// Structural equality after simplification: both should reduce to
|
|
// the same canonical normal form. `to_string()` round-trips through
|
|
// the same printer config, so equal-after-simplify is the right
|
|
// invariant here.
|
|
z3::expr orig_simpl = const_cast<z3::expr&>(fs.return_value).simplify();
|
|
z3::expr restored_simpl = restored->return_value.simplify();
|
|
|
|
// Re-serialise both with let-bindings to compare canonical strings.
|
|
REQUIRE(orig_simpl.to_string() == restored_simpl.to_string());
|
|
}
|
|
|
|
TEST_CASE("serialize: simple non-shared body still serialises", "[serialize][z10][nonshared]") {
|
|
// A body with zero shared structure must remain serialisable. The
|
|
// let-binding param is opportunistic — when there's nothing to
|
|
// factor, output is identical to the un-tuned case (modulo any z3
|
|
// implementation drift). This test confirms the change doesn't
|
|
// break the simple path, not that the output matches a specific
|
|
// string.
|
|
auto makeFs = [] {
|
|
auto env = fold::SymbolicEnv::create();
|
|
z3::context& c = env.ctx();
|
|
z3::expr a = c.bv_const("a", 64);
|
|
z3::expr body = a + c.bv_val(1, 64);
|
|
return fold::FunctionSummarized{
|
|
.env = std::move(env),
|
|
.inputs = {a},
|
|
.return_value = body,
|
|
.soundness = fold::SoundnessTag{},
|
|
};
|
|
};
|
|
auto fs = makeFs();
|
|
auto serialized =
|
|
fold::serialize("simple-id", "simple_test", "input.cpp", 1, 1, "signature_key", fs);
|
|
REQUIRE_FALSE(serialized.body_smt.empty());
|
|
// Roundtrip is covered by the shared-subterm test above; this case
|
|
// only needs to confirm the simple path still serialises (no
|
|
// accidental let-related crash on the trivial input).
|
|
}
|
|
|
|
TEST_CASE("serialize: statement count survives worker NDJSON round-trip",
|
|
"[serialize][equiv][wire]") {
|
|
auto fs = makeSharedSubtermSummary();
|
|
auto serialized =
|
|
fold::serialize("test-id", "shared_test", "input.cpp", 1, 1, "signature_key", fs);
|
|
serialized.body_statement_count = 7;
|
|
|
|
const auto restored = fold::fromJson(fold::toJson(serialized));
|
|
CHECK(restored.body_statement_count == 7);
|
|
CHECK(restored.id == serialized.id);
|
|
CHECK(restored.body_smt == serialized.body_smt);
|
|
}
|