From 3780832b01c23d219206f974df4f2c432d8f94dd Mon Sep 17 00:00:00 2001 From: Zhengyang Liu Date: Fri, 2 Jan 2026 08:44:14 -0800 Subject: [PATCH] [constsyn] bias the model toward poison reserved constants This is implemented as a *greedy* post-SAT refinement: we add constraints that flip reserved constant(s) to poison (or specific lanes to poison) as long as the formula remains satisfiable. --- lib/alive-interface.cpp | 60 +++++++++++++++++++++- tests/datamovements/insertelement10.syn.ll | 4 +- tests/datamovements/insertelement11.syn.ll | 4 +- tests/datamovements/insertelement6.syn.ll | 4 +- 4 files changed, 65 insertions(+), 7 deletions(-) diff --git a/lib/alive-interface.cpp b/lib/alive-interface.cpp index e4483be..359f806 100644 --- a/lib/alive-interface.cpp +++ b/lib/alive-interface.cpp @@ -281,7 +281,15 @@ AliveEngine::find_model(Transform &t, // TODO: dom check seems redundant // TODO: add memory back here - auto r = check_expr(mk_fml(poison_cnstr && value_cnstr), "synthesis"); + // + // Prefer synthesizing *non-poison* reserved constants when possible: + // after finding a SAT model, greedily add constraints that force reserved + // constant(s) to be non-poison (or non-poison lanes) as long as the formula + // remains SAT. This is purely a model-preference heuristic. + expr base = mk_fml(poison_cnstr && value_cnstr); + smt::Solver solver; + solver.add(base); + auto r = solver.check("synthesis"); if (r.isInvalid()) { errs.add("Invalid expr", false); @@ -308,6 +316,56 @@ AliveEngine::find_model(Transform &t, return errs; } + // Try to bias the model toward poison reserved constants (or poison lanes). + // + // This is implemented as a *greedy* post-SAT refinement: we add constraints + // that flip reserved constant(s) to poison (or specific lanes to poison) as + // long as the formula remains satisfiable. + // + // NOTE: We only do this for %_reservedc* inputs (existential vars). + if (r.isSat()) { + auto try_add_cnstr = [&](expr cnstr, const char *tag) { + smt::SolverPush push(solver); + solver.add(cnstr); + auto r2 = solver.check(tag); + if (r2.isSat()) { + r = std::move(r2); + // Keep the constraint if it is satisfiable, so later attempts build on it. + solver.add(std::move(cnstr)); + return; + } + }; + + for (auto &i : tgt_state.getFn().getInputs()) { + if (!dynamic_cast(&i)) + continue; + if (i.getName().rfind("%_reservedc", 0) != 0) + continue; + auto *val = tgt_state.at(i); + if (!val) + continue; + + const expr &np = val->val.non_poison; + + // Scalar poison: force non_poison=false if it's a bool. + if (np.isBool()) { + try_add_cnstr(!np, "synthesis_prefer_poison"); + continue; + } + + // Vector poison: if non_poison is a bitvector with 1 bit per lane, + // try to force each lane to be poison (bit=0) greedily. + unsigned bw = np.bits(); + if (bw > 1) { + for (unsigned bit = 0; bit < bw; ++bit) { + auto np_bit = np.extract(bit, bit); // 1-bit BV + try_add_cnstr(np_bit == expr::mkInt(0, np_bit), + "synthesis_prefer_poison_lane"); + } + } + } + } + stringstream s; auto &m = r.getModel(); s << ";result\n"; diff --git a/tests/datamovements/insertelement10.syn.ll b/tests/datamovements/insertelement10.syn.ll index e127cd7..8c1f1ca 100644 --- a/tests/datamovements/insertelement10.syn.ll +++ b/tests/datamovements/insertelement10.syn.ll @@ -1,4 +1,4 @@ -; CHECK: insertelement <2 x i64> bitcast (<4 x i32> to <2 x i64>) +; CHECK: insertelement <2 x i64> bitcast (<4 x i32> to <2 x i64>) define <4 x i32> @extractelement_out_of_range(<4 x i32> %x, i64 %i) { %f = trunc i64 %i to i32 %g = lshr i64 %i, 32 @@ -6,4 +6,4 @@ define <4 x i32> @extractelement_out_of_range(<4 x i32> %x, i64 %i) { %b = insertelement <4 x i32> zeroinitializer, i32 %f, i32 0 %c = insertelement <4 x i32> %b, i32 %h, i32 1 ret <4 x i32> %c -} \ No newline at end of file +} diff --git a/tests/datamovements/insertelement11.syn.ll b/tests/datamovements/insertelement11.syn.ll index d4a104e..0a0735b 100644 --- a/tests/datamovements/insertelement11.syn.ll +++ b/tests/datamovements/insertelement11.syn.ll @@ -1,4 +1,4 @@ -; CHECK: insertelement <2 x i64> bitcast (<4 x i32> to <2 x i64>) +; CHECK: insertelement <2 x i64> bitcast (<4 x i32> to <2 x i64>) define <4 x i32> @extractelement_out_of_range(<4 x i32> %x, i64 %i) { %f = trunc i64 %i to i32 %g = lshr i64 %i, 32 @@ -6,4 +6,4 @@ define <4 x i32> @extractelement_out_of_range(<4 x i32> %x, i64 %i) { %b = insertelement <4 x i32> , i32 %f, i32 0 %c = insertelement <4 x i32> %b, i32 %h, i32 1 ret <4 x i32> %c -} \ No newline at end of file +} diff --git a/tests/datamovements/insertelement6.syn.ll b/tests/datamovements/insertelement6.syn.ll index 1e7446f..ecd735c 100644 --- a/tests/datamovements/insertelement6.syn.ll +++ b/tests/datamovements/insertelement6.syn.ll @@ -1,6 +1,6 @@ -; CHECK: insertelement <2 x half> , half %f, i16 0 +; CHECK: insertelement <2 x half> , half %f, i16 0 define <2 x half> @extractelement_out_of_range(<2 x half> %x, half %f) { %b = insertelement <2 x half> undef, half %f, i32 0 %c = insertelement <2 x half> %b, half 0xH7C00, i32 1 ret <2 x half> %c -} \ No newline at end of file +}