70 lines
2.5 KiB
C++
70 lines
2.5 KiB
C++
#include <catch2/catch_test_macros.hpp>
|
|
|
|
#include "fold/symbolic/constraint_slice.hpp"
|
|
|
|
TEST_CASE("constraint slicing follows symbol-connected fixed points", "[symbolic][slice]") {
|
|
z3::context ctx;
|
|
const z3::expr x = ctx.bv_const("x", 64);
|
|
const z3::expr y = ctx.bv_const("y", 64);
|
|
const z3::expr z = ctx.bv_const("z", 64);
|
|
const z3::expr unrelated = ctx.bv_const("unrelated", 64);
|
|
z3::solver solver(ctx, "QF_BV");
|
|
solver.add(x == y);
|
|
solver.add(y == z);
|
|
solver.add(unrelated == ctx.bv_val(9, 64));
|
|
|
|
const z3::expr focus = x == ctx.bv_val(0, 64);
|
|
const z3::expr predicate = focus && z == ctx.bv_val(1, 64);
|
|
const auto slice = fold::symbolic::sliceConstraintsForPredicate(solver, predicate, focus);
|
|
|
|
CHECK(slice.input_terms == 5);
|
|
CHECK(slice.selected_terms == 4);
|
|
CHECK(slice.assertions.size() == 2);
|
|
CHECK(slice.assumptions.size() == 2);
|
|
CHECK(slice.reduced());
|
|
}
|
|
|
|
TEST_CASE("constraint slice unsat proves full conjunction", "[symbolic][slice]") {
|
|
z3::context ctx;
|
|
const z3::expr x = ctx.bv_const("x", 64);
|
|
const z3::expr y = ctx.bv_const("y", 64);
|
|
z3::solver full(ctx, "QF_BV");
|
|
full.add(x == ctx.bv_val(1, 64));
|
|
full.add(y == ctx.bv_val(2, 64));
|
|
const z3::expr focus = x == ctx.bv_val(0, 64);
|
|
const auto slice = fold::symbolic::sliceConstraintsForPredicate(full, focus, focus);
|
|
|
|
z3::solver reduced(ctx, "QF_BV");
|
|
for (const auto& assertion : slice.assertions)
|
|
reduced.add(assertion);
|
|
z3::expr_vector assumptions(ctx);
|
|
for (const auto& assumption : slice.assumptions)
|
|
assumptions.push_back(assumption);
|
|
|
|
CHECK(reduced.check(assumptions) == z3::unsat);
|
|
full.add(focus);
|
|
CHECK(full.check() == z3::unsat);
|
|
}
|
|
|
|
TEST_CASE("slice satisfiability does not prove full feasibility", "[symbolic][slice]") {
|
|
z3::context ctx;
|
|
const z3::expr x = ctx.bv_const("x", 64);
|
|
const z3::expr y = ctx.bv_const("y", 64);
|
|
z3::solver full(ctx, "QF_BV");
|
|
full.add(y == ctx.bv_val(1, 64));
|
|
full.add(y == ctx.bv_val(2, 64));
|
|
const z3::expr focus = x == ctx.bv_val(0, 64);
|
|
const auto slice = fold::symbolic::sliceConstraintsForPredicate(full, focus, focus);
|
|
|
|
z3::solver reduced(ctx, "QF_BV");
|
|
for (const auto& assertion : slice.assertions)
|
|
reduced.add(assertion);
|
|
z3::expr_vector assumptions(ctx);
|
|
for (const auto& assumption : slice.assumptions)
|
|
assumptions.push_back(assumption);
|
|
|
|
CHECK(reduced.check(assumptions) == z3::sat);
|
|
full.add(focus);
|
|
CHECK(full.check() == z3::unsat);
|
|
CHECK(slice.reduced());
|
|
}
|