trevon/fold
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
fold/tests/unit/test_pcode_encoder.cpp
trvon fd4a68dfff
 test: add coverage for project graph, pcode encoder, and detector behaviors 
Unit + integration coverage for the session's work: incremental project
graph/index, pcode encoder, unreachable/dead-branch, equiv/cross-TU,
div-by-zero/sign-conversion/int-truncation, use-after-free, quality-precision,
scan-router profile, source TU runner, detector plan, and the eval fixtures.
2026-08-16 16:46:07 -06:00

510 lines
20 KiB
C++
Raw Permalink Blame History

// Unit tests for the P-Code → Z3 encoder (encodePcodeFunction). Builds
// synthetic ir::pcode::Function inputs (no Ghidra, no r2) and runs them through
// the encoder + BinaryBBObserver, asserting the expected findings. This is the
// targeted regression coverage for the Z3 hazard hooks driven from P-Code.
#include <z3++.h>
#include <catch2/catch_test_macros.hpp>
#include <memory>
#include <string>
#include <vector>
#include "fold/binary/binary_bb_observer.hpp"
#include "fold/ir/pcode.hpp"
#include "fold/report/finding.hpp"
#include "fold/symbolic/pcode_encoder.hpp"
namespace {
using namespace fold::ir::pcode;
Varnode reg(std::uint64_t off, std::uint32_t size = 4) { return {Space::Register, off, size}; }
Varnode con(std::uint64_t val, std::uint32_t size = 4) { return {Space::Constant, val, size}; }
PcodeOp mk(Op op, Varnode out, std::vector<Varnode> in) {
PcodeOp p;
p.op = op;
p.address = 0x1000;
p.out = out;
p.in = std::move(in);
return p;
}
PcodeOp mkNoOut(Op op, std::vector<Varnode> in) {
PcodeOp p;
p.op = op;
p.address = 0x1000;
p.in = std::move(in);
return p;
}
std::vector<fold::Finding> encode(const Function& fn) {
std::vector<fold::Finding> out;
auto ctx = std::make_shared<z3::context>();
fold::binary::BinaryBBObserver obs(out, "test.bin", ctx);
fold::symbolic::encodePcodeFunction(fn, *ctx, obs);
return out;
}
bool hasDivByZero(const std::vector<fold::Finding>& fs) {
for (const auto& f : fs)
if (f.kind == fold::FindingKind::DivByZero)
return true;
return false;
}
bool hasNullDeref(const std::vector<fold::Finding>& fs) {
for (const auto& f : fs)
if (f.kind == fold::FindingKind::NullDeref)
return true;
return false;
}
bool hasBufferOverflow(const std::vector<fold::Finding>& fs) {
for (const auto& f : fs)
if (f.kind == fold::FindingKind::OOBAccess &&
f.evidence.detector_name == "binary-buffer-overflow")
return true;
return false;
}
// Build a sink CALL: in[0] is the target address, in[1..] are the args.
// `buf_sizes` is parallel to `in` (index 0 = target, -1; arg i = in[i+1]).
PcodeOp mkCall(const std::string& callee, std::vector<Varnode> args,
std::vector<std::int64_t> buf_sizes) {
PcodeOp p;
p.op = Op::Call;
p.address = 0x1000;
p.call_target = callee;
p.in.push_back(con(0x2000, 8)); // target address
for (auto& a : args)
p.in.push_back(a);
p.in_buffer_sizes = std::move(buf_sizes);
return p;
}
Varnode uniq(std::uint64_t off, std::uint32_t size = 8) { return {Space::Unique, off, size}; }
// space-id const operand for LOAD/STORE (encoder ignores in[0]).
Varnode spaceId() { return con(1, 8); }
} // namespace
TEST_CASE("pcode-encoder: sdiv by a constant-zero divisor is division by zero", "[pcode][divz]") {
// w9 = COPY const 0 ; tmp = INT_SDIV(w8, w9)
Function fn;
fn.name = "div0";
fn.source = Source::Raw;
fn.ops.push_back(mk(Op::Copy, reg(0x48), {con(0)}));
fn.ops.push_back(mk(Op::IntSDiv, reg(0x100), {reg(0x40), reg(0x48)}));
REQUIRE(hasDivByZero(encode(fn)));
}
TEST_CASE("pcode-encoder: binary provenance preserves a full 64-bit address",
"[pcode][provenance]") {
Function fn;
fn.name = "high_address_div0";
auto div = mk(Op::IntSDiv, reg(0x100), {reg(0x40), con(0)});
div.address = 0x1'0000'1000ULL;
fn.ops.push_back(div);
auto findings = encode(fn);
REQUIRE(findings.size() == 1);
REQUIRE(findings[0].confidence == fold::Confidence::Heuristic);
REQUIRE(findings[0].evidence.proof_mode == "binary-pcode-z3-heuristic");
REQUIRE(findings[0].evidence.binary_vaddr == 0x1'0000'1000ULL);
REQUIRE(findings[0].id.find("4294971392") != std::string::npos);
}
TEST_CASE("pcode-encoder: sdiv by a non-zero constant is not flagged", "[pcode][divz]") {
Function fn;
fn.name = "div5";
fn.ops.push_back(mk(Op::Copy, reg(0x48), {con(5)}));
fn.ops.push_back(mk(Op::IntSDiv, reg(0x100), {reg(0x40), reg(0x48)}));
REQUIRE_FALSE(hasDivByZero(encode(fn)));
}
TEST_CASE("pcode-encoder: zero divisor propagated through COPY chain is caught", "[pcode][divz]") {
// w9 = COPY const 0 ; w10 = COPY w9 ; tmp = INT_SREM(w8, w10)
Function fn;
fn.name = "mod0";
fn.ops.push_back(mk(Op::Copy, reg(0x48), {con(0)}));
fn.ops.push_back(mk(Op::Copy, reg(0x50), {reg(0x48)}));
fn.ops.push_back(mk(Op::IntSRem, reg(0x100), {reg(0x40), reg(0x50)}));
REQUIRE(hasDivByZero(encode(fn)));
}
TEST_CASE("pcode-encoder: full-register zero write is seen by a sub-register divisor read",
"[pcode][divz]") {
// Mirrors real ARM64 lifting: `mov w9,#0` zero-extends to x9, so the lifter
// writes (reg X, size 8) = 0, but INT_SDIV reads the 4-byte sub-register
// (reg X, size 4). The value map must alias them by offset.
Function fn;
fn.name = "div0_subreg";
fn.ops.push_back(mk(Op::Copy, Varnode{Space::Register, 0x48, 8}, {con(0, 8)}));
fn.ops.push_back(mk(Op::IntSDiv, reg(0x100), {reg(0x40), Varnode{Space::Register, 0x48, 4}}));
REQUIRE(hasDivByZero(encode(fn)));
}
TEST_CASE("pcode-encoder: divisor that is a fresh (unconstrained) input is not flagged",
"[pcode][divz]") {
// No definition of the divisor reg → fresh symbolic. The MVP gate fires
// div-by-zero only for a provably-zero divisor, so a bare symbolic divisor
// must NOT be reported (no FP on ordinary `a / b`).
Function fn;
fn.name = "divsym";
fn.ops.push_back(mk(Op::IntSDiv, reg(0x100), {reg(0x40), reg(0x48)}));
REQUIRE_FALSE(hasDivByZero(encode(fn)));
}
TEST_CASE("pcode-encoder: raw div hazards are gated by real machine div addresses",
"[pcode][divz]") {
Function fn;
fn.name = "artifact_div0";
fn.source = Source::Raw;
fn.machine_division_addresses_known = true;
fn.machine_division_addresses = {0x2000};
auto div = mk(Op::IntSDiv, reg(0x100), {reg(0x40), con(0)});
div.address = 0x1000;
fn.ops.push_back(div);
REQUIRE_FALSE(hasDivByZero(encode(fn)));
fn.ops.clear();
div.address = 0x2000;
fn.ops.push_back(div);
REQUIRE(hasDivByZero(encode(fn)));
}
TEST_CASE("pcode-encoder: fallthrough branch guard suppresses div-by-zero", "[pcode][divz]") {
// if (den < 1) bail; num / den. CBRANCH is taken on the bad path, so the
// fallthrough path reaching division has !(den < 1), which implies den != 0.
Function fn;
fn.name = "guarded_udiv";
fn.source = Source::Raw;
fn.machine_division_addresses_known = true;
fn.machine_division_addresses = {0x2000};
auto cmp = mk(Op::IntLess, uniq(0x200, 1), {reg(0x48), con(1)});
cmp.address = 0x1000;
fn.ops.push_back(cmp);
auto br = mkNoOut(Op::CBranch, {con(0x3000, 8), uniq(0x200, 1)});
br.address = 0x1004;
fn.ops.push_back(br);
auto div = mk(Op::IntDiv, reg(0x100), {reg(0x40), reg(0x48)});
div.address = 0x2000;
fn.ops.push_back(div);
REQUIRE_FALSE(hasDivByZero(encode(fn)));
}
TEST_CASE("pcode-encoder: fallthrough branch can prove symbolic divisor zero",
"[pcode][divz][path]") {
// if (den != 0) bail; num / den. The fallthrough path implies den == 0, so
// the symbolic divisor is no longer a bare unconstrained input.
Function fn;
fn.name = "branch_proves_zero";
fn.source = Source::Raw;
fn.machine_division_addresses_known = true;
fn.machine_division_addresses = {0x2000};
auto cmp = mk(Op::IntNotEqual, uniq(0x200, 1), {reg(0x48), con(0)});
cmp.address = 0x1000;
fn.ops.push_back(cmp);
auto br = mkNoOut(Op::CBranch, {con(0x3000, 8), uniq(0x200, 1)});
br.address = 0x1004;
fn.ops.push_back(br);
auto div = mk(Op::IntDiv, reg(0x100), {reg(0x40), reg(0x48)});
div.address = 0x2000;
fn.ops.push_back(div);
REQUIRE(hasDivByZero(encode(fn)));
}
TEST_CASE("pcode-encoder: infeasible fallthrough prunes constant div-by-zero",
"[pcode][divz][path]") {
Function fn;
fn.name = "infeasible_fallthrough";
fn.source = Source::Raw;
fn.machine_division_addresses_known = true;
fn.machine_division_addresses = {0x2000};
auto br = mkNoOut(Op::CBranch, {con(0x3000, 8), con(1, 1)});
br.address = 0x1004;
fn.ops.push_back(br);
auto div = mk(Op::IntDiv, reg(0x100), {reg(0x40), con(0)});
div.address = 0x2000;
fn.ops.push_back(div);
REQUIRE_FALSE(hasDivByZero(encode(fn)));
}
TEST_CASE("pcode-encoder: taken block ordered next keeps taken-path hazard",
"[pcode][divz][path]") {
// if (den == 0) goto 0x2000; else return; 0x2000: num / den.
// Some lifted streams place the taken target immediately after CBRANCH.
// The encoder must not globally force the next op onto the fallthrough
// (!cond) path and suppress this real taken-path division.
Function fn;
fn.name = "taken_next_has_hazard";
fn.source = Source::Raw;
fn.machine_division_addresses_known = true;
fn.machine_division_addresses = {0x2000};
auto cmp = mk(Op::IntEqual, uniq(0x200, 1), {reg(0x48), con(0)});
cmp.address = 0x1000;
fn.ops.push_back(cmp);
auto br = mkNoOut(Op::CBranch, {con(0x2000, 8), uniq(0x200, 1)});
br.address = 0x1004;
fn.ops.push_back(br);
auto div = mk(Op::IntDiv, reg(0x100), {reg(0x40), reg(0x48)});
div.address = 0x2000;
fn.ops.push_back(div);
auto ret = mkNoOut(Op::Return, {});
ret.address = 0x2004;
fn.ops.push_back(ret);
REQUIRE(hasDivByZero(encode(fn)));
}
TEST_CASE("pcode-encoder: unconditional branch stops fallthrough hazards", "[pcode][divz][path]") {
Function fn;
fn.name = "branch_skips_hazard";
fn.source = Source::Raw;
fn.machine_division_addresses_known = true;
fn.machine_division_addresses = {0x2000};
auto branch = mkNoOut(Op::Branch, {con(0x3000, 8)});
branch.address = 0x1000;
fn.ops.push_back(branch);
auto div = mk(Op::IntDiv, reg(0x100), {reg(0x40), con(0)});
div.address = 0x2000;
fn.ops.push_back(div);
auto ret = mkNoOut(Op::Return, {});
ret.address = 0x3000;
fn.ops.push_back(ret);
REQUIRE_FALSE(hasDivByZero(encode(fn)));
}
TEST_CASE("pcode-encoder: store-0-to-slot then load then deref is null-deref",
"[pcode][nullderef]") {
// Mirrors null_deref_direct lifting: addr = sp + 8 (recomputed identically),
// STORE(spaceid, sp+8, 0); ldr x8 = LOAD(spaceid, sp+8) -> 0;
// ldr w0 = LOAD(spaceid, x8) -> deref of 0.
const Varnode sp = reg(0x20, 8);
Function fn;
fn.name = "nulld";
fn.ops.push_back(mk(Op::IntAdd, uniq(0xc000), {sp, con(8, 8)}));
fn.ops.push_back(mkNoOut(Op::Store, {spaceId(), uniq(0xc000), con(0, 8)}));
fn.ops.push_back(mk(Op::IntAdd, uniq(0xc000), {sp, con(8, 8)}));
fn.ops.push_back(mk(Op::Load, reg(0x48, 8), {spaceId(), uniq(0xc000)}));
fn.ops.push_back(mk(Op::Load, reg(0x100, 4), {spaceId(), reg(0x48, 8)}));
REQUIRE(hasNullDeref(encode(fn)));
}
TEST_CASE("pcode-encoder: deref of an ordinary stack slot is not null-deref",
"[pcode][nullderef]") {
// Load a (non-zero, unknown) value from sp+8 and deref it: sp+8 is not 0 and
// the loaded value is fresh symbolic, so neither deref is reported.
const Varnode sp = reg(0x20, 8);
Function fn;
fn.name = "nulld_neg";
fn.ops.push_back(mk(Op::IntAdd, uniq(0xc000), {sp, con(8, 8)}));
fn.ops.push_back(mk(Op::Load, reg(0x48, 8), {spaceId(), uniq(0xc000)}));
fn.ops.push_back(mk(Op::Load, reg(0x100, 4), {spaceId(), reg(0x48, 8)}));
REQUIRE_FALSE(hasNullDeref(encode(fn)));
}
// ── Stack buffer overflow ─────────────────────────────────────────
TEST_CASE("pcode-encoder: strcpy into a recovered finite buffer overflows", "[pcode][bof]") {
// strcpy(dst, src) — unbounded; dst is a recovered 64-byte stack buffer.
Function fn;
fn.name = "bof_strcpy";
fn.source = Source::SSA;
fn.ops.push_back(mkCall("strcpy", {reg(0x0, 8), reg(0x8, 8)}, {-1, 64, -1}));
REQUIRE(hasBufferOverflow(encode(fn)));
}
TEST_CASE("pcode-encoder: strcpy with no recovered buffer size does not fire", "[pcode][bof]") {
// No size recovered (raw stream / unrecovered local) -> FN, never FP.
Function fn;
fn.name = "bof_strcpy_nosize";
fn.ops.push_back(mkCall("strcpy", {reg(0x0, 8), reg(0x8, 8)}, {-1, -1, -1}));
REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}
TEST_CASE("pcode-encoder: fgets with size larger than the buffer overflows", "[pcode][bof]") {
// fgets(dst, 128, stream) into a 64-byte buffer: 128 > 64.
Function fn;
fn.name = "bof_fgets";
fn.source = Source::SSA;
fn.ops.push_back(mkCall("fgets", {reg(0x0, 8), con(128, 8), reg(0x8, 8)}, {-1, 64, -1, -1}));
REQUIRE(hasBufferOverflow(encode(fn)));
}
TEST_CASE("pcode-encoder: fgets with size equal to the buffer is safe", "[pcode][bof]") {
// fgets(dst, 64, stream) into a 64-byte buffer: 64 == 64, not > cap.
Function fn;
fn.name = "fgets_ok";
fn.source = Source::SSA;
fn.ops.push_back(mkCall("fgets", {reg(0x0, 8), con(64, 8), reg(0x8, 8)}, {-1, 64, -1, -1}));
REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}
TEST_CASE("pcode-encoder: memcpy within the buffer bound is safe", "[pcode][bof]") {
// memcpy(dst, src, 16) into a 64-byte buffer: 16 <= 64.
Function fn;
fn.name = "memcpy_ok";
fn.source = Source::SSA;
fn.ops.push_back(mkCall("memcpy", {reg(0x0, 8), reg(0x8, 8), con(16, 8)}, {-1, 64, -1, -1}));
REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}
TEST_CASE("pcode-encoder: read-only scanners are not buffer-copy sinks", "[pcode][bof]") {
for (const std::string callee : {"memchr", "strchr", "strstr"}) {
Function fn;
fn.name = "scanner_" + callee;
fn.source = Source::SSA;
fn.ops.push_back(mkCall(callee, {reg(0x0, 8), reg(0x8, 8), con(128, 8)}, {-1, 64, -1, -1}));
REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}
}
TEST_CASE("pcode-encoder: fortified chk wrappers are not modeled as unchecked copies",
"[pcode][bof]") {
Function fn;
fn.name = "strncpy_chk_guarded";
fn.source = Source::SSA;
fn.ops.push_back(mkCall("strncpy_chk", {reg(0x0, 8), reg(0x8, 8), reg(0x10, 8), con(26, 8)},
{-1, 26, -1, -1, -1}));
REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}
TEST_CASE("pcode-encoder: non-sink call does not fire buffer overflow", "[pcode][bof]") {
Function fn;
fn.name = "call_printf";
fn.source = Source::SSA;
fn.ops.push_back(mkCall("printf", {reg(0x0, 8)}, {-1, 64}));
REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}
TEST_CASE("pcode-encoder: switch-state-machine dispatch reaches a case-body strcpy sink",
"[pcode][switchvm][bof]") {
// A switch-state-machine dispatch: the strcpy sink sits in a case body that
// is only reachable through a Memory-space CBRANCH target (the SSA lifter
// encodes branch targets in ram space and can fold the first instruction(s)
// of a case body, so the target address differs from the case body's first
// op address). An unconditional Branch separates the dispatch from the case
// body, so the sink is NOT on the linear fallthrough path.
Function fn;
fn.name = "vm_dispatch";
fn.source = Source::SSA;
Varnode state = {Space::StackBase, 0x10, 4}; // dispatch state slot
Varnode b1 = uniq(0x100, 1);
Varnode b2 = uniq(0x101, 1);
PcodeOp o0 = mk(Op::Copy, state, {con(0x41)});
o0.address = 0x1000;
PcodeOp o1 = mk(Op::IntEqual, b1, {state, con(0x41)});
o1.address = 0x1001;
PcodeOp o2 = mkNoOut(Op::CBranch, {Varnode{Space::Memory, 0x2000, 8}, b1});
o2.address = 0x1002;
PcodeOp o3 = mk(Op::IntEqual, b2, {state, con(0x93)});
o3.address = 0x1003;
PcodeOp o4 = mkNoOut(Op::CBranch, {Varnode{Space::Memory, 0x3000, 8}, b2});
o4.address = 0x1004;
// Default arm: unconditional jump past the case bodies — ends the linear
// walk, so the strcpy below is only reachable via the dispatch CBRANCH.
PcodeOp o5 = mkNoOut(Op::Branch, {Varnode{Space::Memory, 0x4000, 8}});
o5.address = 0x1005;
// Case body: the strcpy sink at address 0x3000 (the CBRANCH targets 0x3000 —
// the folded `lea`), dst buffer recovered as 64 bytes.
PcodeOp o6 = mkCall("strcpy", {reg(0x20, 8), reg(0x28, 8)}, {-1, 64, -1});
o6.address = 0x3000;
PcodeOp o7 = mkNoOut(Op::Return, {});
o7.address = 0x3001;
fn.ops = {o0, o1, o2, o3, o4, o5, o6, o7};
REQUIRE(hasBufferOverflow(encode(fn)));
}
TEST_CASE("pcode-encoder: raw stream does not follow Memory-space branch targets",
"[pcode][switchvm][bof]") {
// The raw stream encodes branch targets as Constant-space; Memory-space
// targets (SSA-only) must NOT be followed in a raw-lifted function, so a
// sink that sits behind a dispatch is unreachable in the raw lane.
Function fn;
fn.name = "vm_dispatch_raw";
fn.source = Source::Raw;
Varnode b1 = uniq(0x100, 1);
Varnode b2 = uniq(0x101, 1);
PcodeOp o0 = mk(Op::IntEqual, b1, {reg(0x0), con(0x41)});
o0.address = 0x1000;
PcodeOp o1 = mkNoOut(Op::CBranch, {Varnode{Space::Memory, 0x2000, 8}, b1});
o1.address = 0x1001;
PcodeOp o2 = mk(Op::IntEqual, b2, {reg(0x0), con(0x93)});
o2.address = 0x1002;
PcodeOp o3 = mkNoOut(Op::CBranch, {Varnode{Space::Memory, 0x3000, 8}, b2});
o3.address = 0x1003;
PcodeOp o4 = mkNoOut(Op::Branch, {Varnode{Space::Memory, 0x4000, 8}});
o4.address = 0x1004;
PcodeOp o5 = mkCall("strcpy", {reg(0x20, 8), reg(0x28, 8)}, {-1, 64, -1});
o5.address = 0x3000;
PcodeOp o6 = mkNoOut(Op::Return, {});
o6.address = 0x3001;
fn.ops = {o0, o1, o2, o3, o4, o5, o6};
// Raw stream: Memory-space targets are rejected, so the strcpy (behind the
// dispatch, past the unconditional Branch) is NOT reached.
REQUIRE_FALSE(hasBufferOverflow(encode(fn)));
}
TEST_CASE("pcode-encoder: MBA select (a & c) | (b & ~c) is already the bitwise-select form",
"[pcode][mba]") {
// The bitwise-select is itself the canonical form for a general mask; no
// simpler Z3 representation exists, so simplifyMba leaves it unchanged.
z3::context ctx;
z3::expr a = ctx.bv_const("a", 8);
z3::expr b = ctx.bv_const("b", 8);
z3::expr c = ctx.bv_const("c", 8);
z3::expr e = (a & c) | (b & ~c);
z3::expr s = fold::symbolic::simplifyMba(e);
REQUIRE(z3::eq(s, e)); // structurally unchanged
}
TEST_CASE("pcode-encoder: MBA xor (x | y) - (x & y) reduces to x ^ y", "[pcode][mba]") {
z3::context ctx;
z3::expr x = ctx.bv_const("x", 8);
z3::expr y = ctx.bv_const("y", 8);
z3::expr e = (x | y) - (x & y);
z3::expr s = fold::symbolic::simplifyMba(e);
REQUIRE(s.is_app());
REQUIRE(s.decl().decl_kind() == Z3_OP_BXOR);
z3::solver sol(ctx);
sol.add(s != e);
REQUIRE(sol.check() == z3::unsat);
}
TEST_CASE("pcode-encoder: MBA and (x + y) - (x | y) reduces to x & y", "[pcode][mba]") {
z3::context ctx;
z3::expr x = ctx.bv_const("x", 8);
z3::expr y = ctx.bv_const("y", 8);
z3::expr e = (x + y) - (x | y);
z3::expr s = fold::symbolic::simplifyMba(e);
REQUIRE(s.is_app());
REQUIRE(s.decl().decl_kind() == Z3_OP_BAND);
z3::solver sol(ctx);
sol.add(s != e);
REQUIRE(sol.check() == z3::unsat);
}
TEST_CASE("pcode-encoder: MBA or (x + y) - (x & y) reduces to x | y", "[pcode][mba]") {
z3::context ctx;
z3::expr x = ctx.bv_const("x", 8);
z3::expr y = ctx.bv_const("y", 8);
z3::expr e = (x + y) - (x & y);
z3::expr s = fold::symbolic::simplifyMba(e);
REQUIRE(s.is_app());
REQUIRE(s.decl().decl_kind() == Z3_OP_BOR);
z3::solver sol(ctx);
sol.add(s != e);
REQUIRE(sol.check() == z3::unsat);
}
TEST_CASE("pcode-encoder: non-MBA expression is unchanged", "[pcode][mba]") {
z3::context ctx;
z3::expr x = ctx.bv_const("x", 8);
z3::expr y = ctx.bv_const("y", 8);
z3::expr e = (x & y) | (x ^ y); // not a known MBA identity
z3::expr s = fold::symbolic::simplifyMba(e);
REQUIRE(z3::eq(s, e)); // structurally unchanged
}
Reference in a new issue View git blame Copy permalink