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