186 lines
7.7 KiB
Python
186 lines
7.7 KiB
Python
"""Unit tests for skills/exe-reverse/scripts/trace_reduce.py, the bit-vector reducer.
|
|
|
|
Three layers, each held separately because they make different promises:
|
|
|
|
* the rewriting core -- the classic mixed-boolean-arithmetic substitutions reduce to `x + y` and
|
|
survive a sampling check, and a genuinely different pair is caught with a counterexample;
|
|
* the SMT emitter -- pure text, checked exactly, because the solver will execute it verbatim and a
|
|
proof about wrongly-encoded semantics is worse than no proof. The shift-count mask is the case
|
|
that matters: `evaluate()` masks a count to six bits, and the encoding must do the same or the
|
|
solver proves a cleaner function than the one the samples ran on;
|
|
* the proof path -- driven against a stub solver (one line of output) and against a missing path,
|
|
never against a real solver: CI has none, and a test that needs one is a test that skips.
|
|
"""
|
|
import sys
|
|
|
|
import pytest
|
|
|
|
pytestmark = pytest.mark.unit
|
|
|
|
|
|
def parse(tr, text):
|
|
return tr.Parser(tr.tokenize(text)).parse()
|
|
|
|
|
|
# --- the rewriting core ---------------------------------------------------------
|
|
|
|
|
|
def test_the_two_classic_substitutions_reduce_to_add(load_script):
|
|
tr = load_script("trace_reduce.py")
|
|
for obfuscated in ("(x | y) + (x & y)", "(x ^ y) + 2 * (x & y)"):
|
|
tree = parse(tr, obfuscated)
|
|
reduced, steps = tr.reduce_all(tree, tr.MASK[32])
|
|
assert reduced.text() == "x + y"
|
|
assert steps, "a reduction with no recorded steps changed nothing"
|
|
equal, counter, _ = tr.verify(tree, reduced, tr.MASK[32], 64)
|
|
assert equal, "counterexample: %r" % (counter,)
|
|
|
|
|
|
def test_a_genuinely_different_pair_is_refuted_with_a_witness(load_script):
|
|
tr = load_script("trace_reduce.py")
|
|
original, other = parse(tr, "x + y"), parse(tr, "x | y")
|
|
equal, counter, checked = tr.verify(original, other, tr.MASK[32], 64)
|
|
assert checked > 0
|
|
assert not equal
|
|
# The witness is re-checked here rather than trusted: the point of a counterexample is that it
|
|
# can be substituted by hand.
|
|
env = counter["env"]
|
|
assert tr.evaluate(original, env, tr.MASK[32]) != tr.evaluate(other, env, tr.MASK[32])
|
|
|
|
|
|
# --- the SMT emitter ------------------------------------------------------------
|
|
|
|
|
|
def test_a_constant_is_emitted_at_the_full_word_width(load_script):
|
|
tr = load_script("trace_reduce.py")
|
|
term = parse(tr, "0x2a")
|
|
assert tr.smt2_term(term, 32) == "#x0000002a"
|
|
assert tr.smt2_term(term, 8) == "#x2a"
|
|
|
|
|
|
def test_every_operator_maps_to_its_bit_vector_counterpart(load_script):
|
|
tr = load_script("trace_reduce.py")
|
|
assert tr.smt2_term(parse(tr, "x + y"), 32) == "(bvadd x y)"
|
|
assert tr.smt2_term(parse(tr, "x - y"), 32) == "(bvsub x y)"
|
|
assert tr.smt2_term(parse(tr, "x * y"), 32) == "(bvmul x y)"
|
|
assert tr.smt2_term(parse(tr, "x & y"), 32) == "(bvand x y)"
|
|
assert tr.smt2_term(parse(tr, "x | y"), 32) == "(bvor x y)"
|
|
assert tr.smt2_term(parse(tr, "x ^ y"), 32) == "(bvxor x y)"
|
|
assert tr.smt2_term(parse(tr, "~x"), 32) == "(bvnot x)"
|
|
assert tr.smt2_term(parse(tr, "-x"), 32) == "(bvneg x)"
|
|
|
|
|
|
def test_a_shift_count_is_masked_exactly_as_evaluate_masks_it(load_script):
|
|
tr = load_script("trace_reduce.py")
|
|
# evaluate() shifts by `count & 63`; the encoding must assert the same thing, or the solver
|
|
# proves a different function than the one the samples ran on.
|
|
assert tr.smt2_term(parse(tr, "x << y"), 32) == "(bvshl x (bvand y #x0000003f))"
|
|
assert tr.smt2_term(parse(tr, "x >> y"), 64) == "(bvlshr x (bvand y #x000000000000003f))"
|
|
|
|
|
|
def test_the_script_declares_variables_asserts_a_difference_and_asks(load_script):
|
|
tr = load_script("trace_reduce.py")
|
|
script = tr.smt2_for(parse(tr, "y + x"), parse(tr, "x + y"), 32)
|
|
lines = script.strip().splitlines()
|
|
assert lines[0] == "(set-logic QF_BV)"
|
|
assert "(declare-fun x () (_ BitVec 32))" in lines
|
|
assert "(declare-fun y () (_ BitVec 32))" in lines
|
|
assert any(line.startswith("(assert (distinct") for line in lines)
|
|
assert "(check-sat)" in lines
|
|
assert "(get-model)" in lines
|
|
|
|
|
|
def test_a_model_is_read_into_an_environment_and_masked(load_script):
|
|
tr = load_script("trace_reduce.py")
|
|
model = """
|
|
sat
|
|
(
|
|
(define-fun x () (_ BitVec 32) #x00000001)
|
|
(define-fun y () (_ BitVec 32) #x00000003)
|
|
(define-fun ignored () Int 7)
|
|
)
|
|
"""
|
|
assert tr.model_env(model, tr.MASK[32]) == {"x": 1, "y": 3}
|
|
assert tr.model_env("unsat", tr.MASK[32]) == {}
|
|
|
|
|
|
# --- the proof path, against stubs ----------------------------------------------
|
|
|
|
|
|
@pytest.fixture
|
|
def unsat_solver(tmp_path):
|
|
"""A stand-in solver that answers `unsat`: one line, no matter the question."""
|
|
if sys.platform == "win32":
|
|
path = tmp_path / "unsat.bat"
|
|
path.write_text("@echo unsat\r\n", encoding="ascii")
|
|
else:
|
|
path = tmp_path / "unsat.sh"
|
|
path.write_text("#!/bin/sh\necho unsat\n", encoding="ascii")
|
|
path.chmod(0o755)
|
|
return str(path)
|
|
|
|
|
|
@pytest.fixture
|
|
def lying_sat_solver(tmp_path):
|
|
"""A stand-in that says `sat` and shows a witness that does not distinguish the forms.
|
|
|
|
The reducer's own rules are identities, so a real sat never appears in a run of this tool; a
|
|
lying one is the case that must not be trusted on arrival, and this stub is how that is held.
|
|
"""
|
|
body = ("sat\n(\n(define-fun x () (_ BitVec 32) #x00000000)\n"
|
|
"(define-fun y () (_ BitVec 32) #x00000000)\n)\n")
|
|
if sys.platform == "win32":
|
|
path = tmp_path / "sat.bat"
|
|
path.write_text("@echo sat\r\n@echo (\r\n@echo (define-fun x () (_ BitVec 32) "
|
|
"#x00000000)\r\n@echo (define-fun y () (_ BitVec 32) #x00000000)\r\n"
|
|
"@echo )\r\n", encoding="ascii")
|
|
else:
|
|
path = tmp_path / "sat.sh"
|
|
path.write_text("#!/bin/sh\ncat <<'EOF'\n%s\nEOF\n" % body, encoding="ascii")
|
|
path.chmod(0o755)
|
|
return str(path)
|
|
|
|
|
|
def test_an_unsat_answer_upgrades_the_verdict_to_proved(load_script, unsat_solver):
|
|
tr = load_script("trace_reduce.py")
|
|
original, reduced = parse(tr, "(x ^ y) + 2 * (x & y)"), parse(tr, "x + y")
|
|
verdict, info = tr.prove(original, reduced, tr.MASK[32], 32, unsat_solver, 10)
|
|
assert verdict == "proved"
|
|
|
|
|
|
def test_a_witness_that_does_not_distinguish_is_not_believed(load_script, lying_sat_solver):
|
|
tr = load_script("trace_reduce.py")
|
|
original, reduced = parse(tr, "(x ^ y) + 2 * (x & y)"), parse(tr, "x + y")
|
|
verdict, info = tr.prove(original, reduced, tr.MASK[32], 32, lying_sat_solver, 10)
|
|
assert verdict == "no-verdict"
|
|
assert "does not distinguish" in info["reason"]
|
|
|
|
|
|
def test_a_missing_solver_path_is_reported_not_crashed(load_script, tmp_path):
|
|
tr = load_script("trace_reduce.py")
|
|
original, reduced = parse(tr, "x + y"), parse(tr, "x + y")
|
|
verdict, info = tr.prove(original, reduced, tr.MASK[32], 32,
|
|
str(tmp_path / "not-there.exe"), 10)
|
|
assert verdict == "no-verdict"
|
|
assert "does not exist" in info["reason"]
|
|
|
|
|
|
def test_prove_with_a_missing_path_is_a_usage_error_at_the_cli(load_script, monkeypatch, capsys,
|
|
tmp_path):
|
|
tr = load_script("trace_reduce.py")
|
|
monkeypatch.setattr(sys, "argv", ["trace_reduce.py", "x + 0",
|
|
"--prove", str(tmp_path / "absent.exe")])
|
|
assert tr.main() == 2
|
|
out = capsys.readouterr()
|
|
assert "RESULT=usage_error" in out.out
|
|
|
|
|
|
def test_a_proved_run_reports_the_proved_token(load_script, monkeypatch, capsys, unsat_solver):
|
|
tr = load_script("trace_reduce.py")
|
|
monkeypatch.setattr(sys, "argv", ["trace_reduce.py", "(x ^ y) + 2 * (x & y)",
|
|
"--prove", unsat_solver])
|
|
assert tr.main() == 0
|
|
out = capsys.readouterr().out
|
|
assert "RESULT=reduce_proved" in out
|
|
assert "every input" in out
|