foundry_evm_symbolic/runtime/expr/
cx.rs

1use super::{hashcons::HashCons, *};
2use alloy_primitives::map::DefaultHashBuilder;
3use inturn::unsync::Interner;
4
5pub(crate) struct SymCx {
6    words: HashCons<SymExprKind>,
7    bools: HashCons<SymBoolExprKind>,
8    bytes: HashCons<SymBytesKind>,
9    symbols: Interner<Symbol, DefaultHashBuilder>,
10    replayable_inputs: SymbolicVars,
11    concrete_keccak_preimages: HashMap<U256, Arc<[SymExpr]>>,
12    cache: SymCxCache,
13}
14
15struct SymCxCache {
16    zero: SymExpr,
17    one: SymExpr,
18    bool_true: SymBoolExpr,
19    bool_false: SymBoolExpr,
20    bytes_empty: SymBytes,
21}
22
23impl SymCx {
24    pub(crate) fn new() -> Self {
25        let mut words = HashCons::new();
26        let zero = SymExpr { kind: words.make(SymExprKind::Const(U256::ZERO)) };
27        let one = SymExpr { kind: words.make(SymExprKind::Const(U256::from(1))) };
28
29        let mut bools = HashCons::new();
30        let bool_true = SymBoolExpr { kind: bools.make(SymBoolExprKind::Const(true)) };
31        let bool_false = SymBoolExpr { kind: bools.make(SymBoolExprKind::Const(false)) };
32
33        let mut bytes = HashCons::new();
34        let bytes_empty = SymBytes { kind: bytes.make(SymBytesKind::Concrete(Vec::new())) };
35
36        Self {
37            words,
38            bools,
39            bytes,
40            symbols: Interner::with_hasher(DefaultHashBuilder::default()),
41            replayable_inputs: SymbolicVars::default(),
42            concrete_keccak_preimages: HashMap::default(),
43            cache: SymCxCache { zero, one, bool_true, bool_false, bytes_empty },
44        }
45    }
46
47    pub(in crate::runtime) fn mk_expr_kind(&mut self, expr: SymExprKind) -> SymExpr {
48        SymExpr { kind: self.words.make(expr) }
49    }
50
51    pub(in crate::runtime) fn mk_bool_kind(&mut self, expr: SymBoolExprKind) -> SymBoolExpr {
52        SymBoolExpr { kind: self.bools.make(expr) }
53    }
54
55    pub(in crate::runtime) fn mk_bytes_kind(&mut self, bytes: SymBytesKind) -> SymBytes {
56        if matches!(&bytes, SymBytesKind::Concrete(bytes) if bytes.is_empty()) {
57            return self.cache.bytes_empty.clone();
58        }
59        SymBytes { kind: self.bytes.make(bytes) }
60    }
61
62    pub(in crate::runtime::expr) fn cached_zero(&self) -> SymExpr {
63        self.cache.zero.clone()
64    }
65
66    pub(in crate::runtime::expr) fn cached_one(&self) -> SymExpr {
67        self.cache.one.clone()
68    }
69
70    pub(in crate::runtime::expr) fn cached_bool(&self, value: bool) -> SymBoolExpr {
71        if value { self.cache.bool_true.clone() } else { self.cache.bool_false.clone() }
72    }
73
74    pub(crate) fn intern(&mut self, name: &str) -> Symbol {
75        self.symbols.intern_mut(name)
76    }
77
78    #[cfg(test)]
79    pub(crate) fn symbol(&self, name: &str) -> Symbol {
80        self.symbols.intern(name)
81    }
82
83    pub(crate) fn symbol_name(&self, symbol: Symbol) -> &str {
84        self.symbols.resolve(symbol)
85    }
86
87    pub(crate) fn mark_replayable_input(&mut self, symbol: Symbol) {
88        self.replayable_inputs.insert(symbol);
89    }
90
91    pub(crate) fn is_replayable_input(&self, symbol: Symbol) -> bool {
92        self.replayable_inputs.contains(&symbol)
93    }
94
95    pub(in crate::runtime::expr) fn record_concrete_keccak_preimage(
96        &mut self,
97        hash: U256,
98        bytes: Arc<[SymExpr]>,
99    ) {
100        self.concrete_keccak_preimages.entry(hash).or_insert(bytes);
101    }
102
103    pub(in crate::runtime::expr) fn concrete_keccak_preimage(
104        &self,
105        hash: U256,
106    ) -> Option<Arc<[SymExpr]>> {
107        self.concrete_keccak_preimages.get(&hash).cloned()
108    }
109}
110
111impl fmt::Debug for SymCx {
112    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
113        f.debug_struct("SymCx").finish_non_exhaustive()
114    }
115}
116
117impl Default for SymCx {
118    fn default() -> Self {
119        Self::new()
120    }
121}
122
123#[cfg(test)]
124mod tests {
125    use super::*;
126
127    #[test]
128    fn hashconses_word_constants() {
129        let mut cx = SymCx::new();
130        let first = SymExpr::constant(&mut cx, U256::from(42));
131        let second = SymExpr::constant(&mut cx, U256::from(42));
132
133        assert_eq!(first, second);
134    }
135
136    #[test]
137    fn hashconses_word_expressions() {
138        let mut cx = SymCx::new();
139        let x = SymExpr::var(&mut cx, "x");
140        let y = SymExpr::var(&mut cx, "y");
141
142        let first = SymExpr::binop(&mut cx, SymBinOp::Add, x.clone(), y.clone());
143        let second = SymExpr::binop(&mut cx, SymBinOp::Add, x, y);
144
145        assert_eq!(first, second);
146    }
147
148    #[test]
149    fn commutative_ops_place_constants_on_rhs() {
150        let mut cx = SymCx::new();
151        let constant_value = U256::from(7);
152
153        for op in [SymBinOp::Add, SymBinOp::Mul, SymBinOp::And, SymBinOp::Or, SymBinOp::Xor] {
154            let x = SymExpr::var(&mut cx, "x");
155            let constant = SymExpr::constant(&mut cx, constant_value);
156            let expr = SymExpr::binop(&mut cx, op, constant, x.clone());
157            let SymExprKind::BinOp(actual_op, left, right) = expr.kind() else {
158                panic!("expected binary expression");
159            };
160            assert_eq!(*actual_op, op);
161            assert_eq!(left, &x);
162            assert_eq!(right.as_const(), Some(constant_value));
163        }
164    }
165
166    #[test]
167    fn hashconses_bool_expressions() {
168        let mut cx = SymCx::new();
169        let x = SymExpr::var(&mut cx, "x");
170
171        let upper = SymExpr::constant(&mut cx, U256::from(7));
172        let first = SymBoolExpr::cmp(&mut cx, SymCmpOp::Ult, x.clone(), upper.clone());
173        let second = SymBoolExpr::cmp(&mut cx, SymCmpOp::Ult, x, upper);
174
175        assert_eq!(first, second);
176    }
177
178    #[test]
179    fn simplifies_shift_right_over_or_at_construction() {
180        let mut cx = SymCx::new();
181        let x = SymExpr::var(&mut cx, "x").low_byte(&mut cx);
182        let low = SymExpr::constant(&mut cx, U256::from(0xff));
183        let shift = SymExpr::constant(&mut cx, U256::from(8));
184        let high = SymExpr::binop(&mut cx, SymBinOp::Shl, x.clone(), shift.clone());
185        let word = SymExpr::binop(&mut cx, SymBinOp::Or, high, low);
186        let shifted = SymExpr::binop(&mut cx, SymBinOp::Shr, word, shift);
187
188        assert_eq!(shifted, x);
189    }
190
191    #[test]
192    fn simplifies_masked_or_at_construction() {
193        let mut cx = SymCx::new();
194        let x = SymExpr::var(&mut cx, "x").low_byte(&mut cx);
195        let y = SymExpr::var(&mut cx, "y").low_byte(&mut cx);
196        let shift = SymExpr::constant(&mut cx, U256::from(8));
197        let high = SymExpr::binop(&mut cx, SymBinOp::Shl, x, shift);
198        let word = SymExpr::binop(&mut cx, SymBinOp::Or, high, y.clone());
199        let mask = SymExpr::constant(&mut cx, U256::from(0xff));
200        let masked = SymExpr::binop(&mut cx, SymBinOp::And, word, mask);
201
202        assert_eq!(masked, y);
203    }
204}
foundry_evm_symbolic/runtime/expr/cx.rs

foundry_evm_symbolic/runtime/expr/
cx.rs
