Skip to content

Commit c7e2e07

Browse files
ekiwiekiwi
committed
sca: wip
1 parent fcd4968 commit c7e2e07

File tree

3 files changed

+174
-147
lines changed

3 files changed

+174
-147
lines changed

‎patronus-sca/Cargo.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,4 +13,4 @@ rust-version.workspace = true
1313
patronus = { path = "../patronus" }
1414
baa = {version = "0.17.1", features = ["bigint"]}
1515
rustc-hash.workspace = true
16-
polysub = "0.1.10"
16+
polysub = "0.2.2"

‎patronus-sca/src/backwards.rs‎

Lines changed: 167 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,167 @@
1+
// Copyright 2026 Cornell University
2+
// released under BSD 3-Clause License
3+
// author: Kevin Laeufer <laeufer@cornell.edu>
4+
5+
use crate::{DefaultCoef, Poly, expr_to_var};
6+
use baa::BitVecOps;
7+
use patronus::expr::{
8+
Context, DenseExprSet, Expr, ExprRef, ExprSet, ForEachChild, count_expr_uses,
9+
};
10+
use polysub::{PhaseOptPolynom, VarIndex};
11+
use rustc_hash::FxHashSet;
12+
use std::collections::VecDeque;
13+
14+
/// Used for backwards substitution
15+
type PolyOpt = polysub::PhaseOptPolynom<DefaultCoef>;
16+
17+
pub fn backwards_sub(
18+
ctx: &Context,
19+
input_vars: &FxHashSet<VarIndex>,
20+
todo: Vec<(VarIndex, ExprRef)>,
21+
spec: Poly,
22+
) -> Poly {
23+
// empirically, it looks like we should not use a stack
24+
let mut todo: VecDeque<_> = todo.into();
25+
let mut spec: PolyOpt = spec.into();
26+
let mut var_roots: Vec<_> = todo.iter().map(|(v, _)| *v).collect();
27+
var_roots.sort();
28+
29+
// first, we count how often expressions are used
30+
let roots: Vec<_> = todo.iter().map(|(_, e)| *e).collect();
31+
let mut uses = count_expr_uses(ctx, roots);
32+
let mut replaced = vec![];
33+
let mut seen = DenseExprSet::default();
34+
35+
while !todo.is_empty() {
36+
//try_exhaustive(ctx, input_vars, &spec, todo.iter().cloned());
37+
38+
// chose variable to replace
39+
let (output_var, gate) = todo.pop_back().unwrap();
40+
41+
replaced.push(output_var);
42+
println!(
43+
"{output_var} {:?}: {}, {}",
44+
&ctx[gate],
45+
todo.len() + 1,
46+
spec.size()
47+
);
48+
49+
let add_children = replace_gate(ctx, input_vars, &mut spec, output_var, gate);
50+
51+
if add_children {
52+
ctx[gate].for_each_child(|&e| {
53+
// reduce the use by one
54+
let prev_uses = uses[e];
55+
assert!(prev_uses > 0);
56+
uses[e] = prev_uses - 1;
57+
// did the use count just go down to zero?
58+
let var = expr_to_var(e);
59+
if prev_uses == 1 && !input_vars.contains(&var) {
60+
todo.push_back((var, e));
61+
} else if !seen.contains(&e) {
62+
// try phase opt
63+
let old_size = spec.size();
64+
spec.invert(var);
65+
if spec.size() > old_size {
66+
spec.invert(var);
67+
} else {
68+
println!("INVERTING {var} {old_size} -> {}", spec.size());
69+
}
70+
}
71+
seen.insert(e);
72+
});
73+
}
74+
}
75+
76+
println!("Roots: {var_roots:?}");
77+
78+
replaced.sort();
79+
println!("Replaced variables: {replaced:?}");
80+
81+
// find any expressions where uses are not zero
82+
use patronus::expr::ExprMap;
83+
let mut still_used: Vec<_> = uses
84+
.iter()
85+
.filter(|(_, v)| **v > 0)
86+
.map(|(k, _)| expr_to_var(k))
87+
.collect();
88+
still_used.sort();
89+
println!("Still used: {still_used:?}");
90+
91+
let spec: Poly = spec.into();
92+
let mut remaining_vars: Vec<_> = spec
93+
.sorted_monom_vec()
94+
.iter()
95+
.flat_map(|(_, t)| t.vars().cloned().collect::<Vec<_>>())
96+
.collect();
97+
remaining_vars.sort();
98+
remaining_vars.dedup();
99+
println!("Remaining vars: {remaining_vars:?}");
100+
101+
spec
102+
}
103+
104+
fn replace_gate(
105+
ctx: &Context,
106+
input_vars: &FxHashSet<VarIndex>,
107+
spec: &mut PolyOpt,
108+
output_var: VarIndex,
109+
gate: ExprRef,
110+
) -> bool {
111+
match ctx[gate].clone() {
112+
Expr::BVOr(a, b, 1) => {
113+
spec.replace_or(output_var, expr_to_var(a), expr_to_var(b));
114+
true
115+
}
116+
Expr::BVXor(a, b, 1) => {
117+
spec.replace_xor(output_var, expr_to_var(a), expr_to_var(b));
118+
true
119+
}
120+
Expr::BVAnd(a, b, 1) => {
121+
spec.replace_and(output_var, expr_to_var(a), expr_to_var(b));
122+
true
123+
}
124+
Expr::BVNot(a, 1) => {
125+
spec.replace_not(output_var, expr_to_var(a));
126+
true
127+
}
128+
Expr::BVSlice { hi, lo, e } => {
129+
assert_eq!(hi, lo);
130+
assert!(
131+
input_vars.contains(&expr_to_var(e)),
132+
"Not actually an input: {e:?}"
133+
);
134+
// a bit slice normally marks an input, thus we should be done!
135+
false
136+
}
137+
Expr::BVLiteral(value) => {
138+
let value = value.get(ctx);
139+
debug_assert_eq!(value.width(), 1);
140+
if value.is_true() {
141+
spec.replace_true(output_var);
142+
} else {
143+
spec.replace_false(output_var);
144+
}
145+
false
146+
}
147+
other => todo!("add support for {other:?}"),
148+
}
149+
}
150+
151+
fn try_exhaustive(
152+
ctx: &Context,
153+
input_vars: &FxHashSet<VarIndex>,
154+
spec: &PolyOpt,
155+
todo: impl Iterator<Item = (VarIndex, ExprRef)>,
156+
) {
157+
for (ii, (output_var, gate)) in todo.enumerate() {
158+
let mut s = spec.clone();
159+
replace_gate(ctx, input_vars, &mut s, output_var, gate);
160+
println!(
161+
" {ii:>3}: {output_var} {:?}: {} -> {}",
162+
&ctx[gate],
163+
spec.size(),
164+
s.size()
165+
);
166+
}
167+
}

‎patronus-sca/src/lib.rs‎

Lines changed: 6 additions & 146 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,9 @@
22
// released under BSD 3-Clause License
33
// author: Kevin Laeufer <laeufer@cornell.edu>
44

5+
mod backwards;
6+
7+
use crate::backwards::backwards_sub;
58
use baa::{BitVecOps, BitVecValue, BitVecValueRef};
69
use patronus::expr::*;
710
use polysub::{Coef, Term, VarIndex};
@@ -153,166 +156,23 @@ fn extract_bit(ctx: &mut Context, e: ExprRef, bit: WidthInt) -> ExprRef {
153156
}
154157

155158
type DefaultCoef = polysub::ArrayCoef<8>;
159+
/// Used for building the word-level polynomial
156160
type Poly = polysub::Polynom<DefaultCoef>;
157161

158162
fn expr_to_var(e: ExprRef) -> polysub::VarIndex {
159163
(usize::from(e) as u32).into()
160164
}
161165

162-
/// converts the two expression references and ensures that the smallest var index is returned first
163-
#[inline]
164-
fn exprs_to_vars_commutative(a: ExprRef, b: ExprRef) -> (VarIndex, VarIndex) {
165-
let a = expr_to_var(a);
166-
let b = expr_to_var(b);
167-
if a > b { (b, a) } else { (a, b) }
168-
}
169-
170166
fn var_to_expr(v: polysub::VarIndex) -> ExprRef {
171167
usize::from(v).into()
172168
}
173169

174-
fn backwards_sub(
175-
ctx: &Context,
176-
input_vars: &FxHashSet<VarIndex>,
177-
mut todo: Vec<(VarIndex, ExprRef)>,
178-
mut spec: Poly,
179-
) -> Poly {
180-
let mut var_roots: Vec<_> = todo.iter().map(|(v, _)| *v).collect();
181-
var_roots.sort();
182-
183-
let m = spec.get_mod();
184-
let one: DefaultCoef = Coef::from_i64(1, m);
185-
let zero: DefaultCoef = Coef::from_i64(0, m);
186-
let minus_one: DefaultCoef = Coef::from_i64(-1, m);
187-
let minus_two: DefaultCoef = Coef::from_i64(-2, m);
188-
// first, we count how often expressions are used
189-
let roots: Vec<_> = todo.iter().map(|(_, e)| *e).collect();
190-
let mut uses = count_expr_uses(ctx, roots);
191-
let mut replaced = vec![];
192-
193-
let const_true_var = expr_to_var(ctx.get_true());
194-
195-
while let Some((output_var, gate)) = todo.pop() {
196-
replaced.push(output_var);
197-
println!("{output_var} {:?}: {}", &ctx[gate], spec.size());
198-
199-
let add_children = match ctx[gate].clone() {
200-
Expr::BVOr(a, b, 1) => {
201-
// a + b - ab
202-
let (x0, x1) = exprs_to_vars_commutative(a, b);
203-
let monoms = [
204-
(one.clone(), vec![x0].into()),
205-
(one.clone(), vec![x1].into()),
206-
(minus_one.clone(), vec![x0, x1].into()),
207-
];
208-
assert_ne!(gate, a);
209-
assert_ne!(gate, b);
210-
spec.replace_var(output_var, &monoms);
211-
true
212-
}
213-
Expr::BVXor(a, b, 1) => {
214-
// a + b - 2ab
215-
let (x0, x1) = exprs_to_vars_commutative(a, b);
216-
let monoms = [
217-
(one.clone(), vec![x0].into()),
218-
(one.clone(), vec![x1].into()),
219-
(minus_two.clone(), vec![x0, x1].into()),
220-
];
221-
assert_ne!(gate, a);
222-
assert_ne!(gate, b);
223-
spec.replace_var(output_var, &monoms);
224-
true
225-
}
226-
Expr::BVAnd(a, b, 1) => {
227-
// ab
228-
let (x0, x1) = exprs_to_vars_commutative(a, b);
229-
let monoms = [(one.clone(), vec![x0, x1].into())];
230-
assert_ne!(gate, a);
231-
assert_ne!(gate, b);
232-
spec.replace_var(output_var, &monoms);
233-
true
234-
}
235-
Expr::BVNot(a, 1) => {
236-
// 1 - a
237-
let x0 = expr_to_var(a);
238-
let monoms = [
239-
(one.clone(), vec![].into()),
240-
(minus_one.clone(), vec![x0].into()),
241-
];
242-
assert_ne!(gate, a);
243-
spec.replace_var(output_var, &monoms);
244-
true
245-
}
246-
Expr::BVSlice { hi, lo, e } => {
247-
assert_eq!(hi, lo);
248-
assert!(
249-
input_vars.contains(&expr_to_var(e)),
250-
"Not actually an input: {e:?}"
251-
);
252-
// a bit slice normally marks an input, thus we should be done!
253-
false
254-
}
255-
Expr::BVLiteral(value) => {
256-
let value = value.get(ctx);
257-
debug_assert_eq!(value.width(), 1);
258-
if value.is_true() {
259-
spec.replace_var(output_var, &[(one.clone(), vec![].into())]);
260-
} else {
261-
spec.replace_var(output_var, &[(zero.clone(), vec![].into())]);
262-
}
263-
false
264-
}
265-
other => todo!("add support for {other:?}"),
266-
};
267-
268-
if add_children {
269-
ctx[gate].for_each_child(|&e| {
270-
// reduce the use by one
271-
let prev_uses = uses[e];
272-
assert!(prev_uses > 0);
273-
uses[e] = prev_uses - 1;
274-
// did the use count just go down to zero?
275-
let var = expr_to_var(e);
276-
if prev_uses == 1 && !input_vars.contains(&var) {
277-
todo.push((var, e));
278-
}
279-
});
280-
}
281-
}
282-
283-
println!("Roots: {var_roots:?}");
284-
285-
replaced.sort();
286-
println!("Replaced variables: {replaced:?}");
287-
288-
// find any expressions where uses are not zero
289-
use patronus::expr::ExprMap;
290-
let mut still_used: Vec<_> = uses
291-
.iter()
292-
.filter(|(_, v)| **v > 0)
293-
.map(|(k, _)| expr_to_var(k))
294-
.collect();
295-
still_used.sort();
296-
println!("Still used: {still_used:?}");
297-
298-
let mut remaining_vars: Vec<_> = spec
299-
.sorted_monom_vec()
300-
.iter()
301-
.flat_map(|(_, t)| t.vars().cloned().collect::<Vec<_>>())
302-
.collect();
303-
remaining_vars.sort();
304-
remaining_vars.dedup();
305-
println!("Remaining vars: {remaining_vars:?}");
306-
307-
spec
308-
}
309-
310170
fn poly_for_bv_expr(ctx: &mut Context, e: ExprRef) -> Poly {
311171
let width = e
312172
.get_bv_type(ctx)
313173
.expect("function only works with bitvector expressions.");
314174
let m = polysub::Mod::from_bits(width);
315-
polysub::Polynom::from_monoms(
175+
Poly::from_monoms(
316176
m,
317177
(0..width).map(|ii| {
318178
// add an entry for each bit
@@ -332,7 +192,7 @@ fn poly_for_bv_literal(value: BitVecValueRef) -> Poly {
332192
let coef = Coef::from_big(&big_value, m);
333193
// now we create a polynomial with just this coefficient
334194
let monom = (coef, vec![].into());
335-
polysub::Polynom::from_monoms(m, vec![monom].into_iter())
195+
Poly::from_monoms(m, vec![monom].into_iter())
336196
}
337197

338198
/// Returns a polynomial representation of the expression + all input expressions if possible.

0 commit comments

Comments
 (0)