foundry_evm_symbolic/runtime/expr/
mod.rs

1use super::*;
2
3mod bool;
4mod cx;
5pub(super) mod hashcons;
6#[path = "expr.rs"]
7mod word;
8
9pub(crate) use bool::*;
10pub(crate) use cx::*;
11pub(crate) use word::*;
12
13struct NoopModel;
14
15impl SymbolicModelLookup for NoopModel {
16    fn value(&self, _name: Symbol) -> Option<U256> {
17        None
18    }
19}
20
21/// Results from one deterministic bottom-up expression fold.
22///
23/// Keys borrow the original DAG so the memo table does not add strong references to source nodes.
24#[derive(Default)]
25struct ExpressionFoldCache<'a> {
26    words: HashMap<&'a SymExpr, SymExpr>,
27    bools: HashMap<&'a SymBoolExpr, SymBoolExpr>,
28}
29
30/// Structural digests that identify expressions in stable symbol names.
31///
32/// Each distinct hash-consed node is digested once. Formatting a node with `Debug` instead
33/// prints the DAG as a tree, which grows exponentially when subexpressions are shared, as in a
34/// chain of hashes over the previous hash.
35#[derive(Default)]
36pub(crate) struct ExpressionDigests<'a> {
37    words: HashMap<&'a SymExpr, B256>,
38    bools: HashMap<&'a SymBoolExpr, B256>,
39}
40
41impl<'a> ExpressionDigests<'a> {
42    /// Returns one digest that identifies a sequence of expressions.
43    pub(crate) fn identity(exprs: impl IntoIterator<Item = &'a SymExpr>) -> B256 {
44        let mut digests = Self::default();
45        let mut hasher = Keccak256::new();
46        for expr in exprs {
47            hasher.update(digests.digest(DigestNode::Word(expr)));
48        }
49        hasher.finalize()
50    }
51
52    /// Digests a node in post-order with an explicit stack, because expressions can be deeper
53    /// than the thread stack allows for recursion.
54    fn digest(&mut self, root: DigestNode<'a>) -> B256 {
55        let mut stack = vec![(root, false)];
56        while let Some((node, children_done)) = stack.pop() {
57            if self.get(node).is_some() {
58                continue;
59            }
60            if !children_done {
61                stack.push((node, true));
62                stack.extend(node.children().into_iter().map(|child| (child, false)));
63                continue;
64            }
65            let mut hasher = Keccak256::new();
66            match node {
67                DigestNode::Word(expr) => {
68                    match expr.kind() {
69                        SymExprKind::Const(value) => {
70                            hasher.update([0]);
71                            hasher.update(value.to_be_bytes::<32>());
72                        }
73                        SymExprKind::Var(symbol) => {
74                            hasher.update([1]);
75                            hasher.update(symbol.id().get().to_be_bytes());
76                        }
77                        SymExprKind::GasLeft(symbol) => {
78                            hasher.update([2]);
79                            hasher.update(symbol.id().get().to_be_bytes());
80                        }
81                        // A hash name is already a digest of its preimage.
82                        SymExprKind::Keccak { name, .. } => {
83                            hasher.update([3]);
84                            hasher.update(name.id().get().to_be_bytes());
85                        }
86                        SymExprKind::Hash { name, algorithm, .. } => {
87                            hasher.update([4]);
88                            hasher.update(algorithm.as_bytes());
89                            hasher.update(name.id().get().to_be_bytes());
90                        }
91                        SymExprKind::Not(_) => hasher.update([5]),
92                        SymExprKind::BinOp(op, _, _) => hasher.update([6, *op as u8]),
93                        SymExprKind::TernOp(op, _, _, _) => hasher.update([7, *op as u8]),
94                        SymExprKind::Ite(_, _, _) => hasher.update([8]),
95                    }
96                }
97                DigestNode::Bool(expr) => match expr.kind() {
98                    SymBoolExprKind::Const(value) => hasher.update([9, u8::from(*value)]),
99                    SymBoolExprKind::Not(_) => hasher.update([10]),
100                    SymBoolExprKind::And(_) => hasher.update([11]),
101                    SymBoolExprKind::Cmp(op, _, _) => hasher.update([12, *op as u8]),
102                },
103            }
104            for child in node.children() {
105                hasher.update(self.get(child).expect("children are digested first"));
106            }
107            let digest = hasher.finalize();
108            match node {
109                DigestNode::Word(expr) => self.words.insert(expr, digest),
110                DigestNode::Bool(expr) => self.bools.insert(expr, digest),
111            };
112        }
113        self.get(root).expect("root is digested")
114    }
115
116    fn get(&self, node: DigestNode<'a>) -> Option<B256> {
117        match node {
118            DigestNode::Word(expr) => self.words.get(expr).copied(),
119            DigestNode::Bool(expr) => self.bools.get(expr).copied(),
120        }
121    }
122}
123
124#[derive(Clone, Copy)]
125enum DigestNode<'a> {
126    Word(&'a SymExpr),
127    Bool(&'a SymBoolExpr),
128}
129
130impl<'a> DigestNode<'a> {
131    /// Returns the operands that contribute to the digest. Hash preimages are left out, because
132    /// the hash name already commits to them.
133    fn children(self) -> Vec<Self> {
134        match self {
135            Self::Word(expr) => match expr.kind() {
136                SymExprKind::Const(_)
137                | SymExprKind::Var(_)
138                | SymExprKind::GasLeft(_)
139                | SymExprKind::Keccak { .. }
140                | SymExprKind::Hash { .. } => vec![],
141                SymExprKind::Not(value) => vec![Self::Word(value)],
142                SymExprKind::BinOp(_, left, right) => vec![Self::Word(left), Self::Word(right)],
143                SymExprKind::TernOp(_, first, second, third) => {
144                    vec![Self::Word(first), Self::Word(second), Self::Word(third)]
145                }
146                SymExprKind::Ite(condition, then, otherwise) => {
147                    vec![Self::Bool(condition), Self::Word(then), Self::Word(otherwise)]
148                }
149            },
150            Self::Bool(expr) => match expr.kind() {
151                SymBoolExprKind::Const(_) => vec![],
152                SymBoolExprKind::Not(value) => vec![Self::Bool(value)],
153                SymBoolExprKind::And(values) => values.iter().map(Self::Bool).collect(),
154                SymBoolExprKind::Cmp(_, left, right) => vec![Self::Word(left), Self::Word(right)],
155            },
156        }
157    }
158}
159
160/// Evaluates hash-consed expressions once per model.
161///
162/// Symbolic expressions form a DAG, so recursively evaluating both operands without caching can
163/// revisit the same node exponentially many times.
164struct ModelEvaluator<'a, M: ?Sized> {
165    model: &'a M,
166    words: HashMap<SymExpr, U256>,
167    bools: HashMap<SymBoolExpr, bool>,
168}
169
170impl<'a, M: SymbolicModelLookup + ?Sized> ModelEvaluator<'a, M> {
171    fn new(model: &'a M) -> Self {
172        Self { model, words: HashMap::default(), bools: HashMap::default() }
173    }
174
175    fn eval_word(&mut self, expr: &SymExpr) -> Result<U256, SymbolicError> {
176        let kind = expr.kind();
177        if let Some(var) = kind.get_eval_var() {
178            return Ok(self.model.value(var).unwrap_or_default());
179        }
180        if let SymExprKind::Const(value) = kind {
181            return Ok(*value);
182        }
183        if let Some(value) = self.words.get(expr) {
184            return Ok(*value);
185        }
186
187        let value = match kind {
188            SymExprKind::Const(_)
189            | SymExprKind::Var(_)
190            | SymExprKind::GasLeft(_)
191            | SymExprKind::Hash { .. } => unreachable!("symbolic eval leaf handled above"),
192            SymExprKind::Keccak { len, bytes, .. } => {
193                let len = self.eval_word(len)?;
194                let Ok(len) = usize::try_from(len) else {
195                    return Err(SymbolicError::Solver(
196                        "solver model uses an invalid keccak length".to_string(),
197                    ));
198                };
199                if len > bytes.len() {
200                    return Err(SymbolicError::Solver(
201                        "solver model uses an invalid keccak length".to_string(),
202                    ));
203                }
204
205                let mut input = Vec::with_capacity(len);
206                for byte in bytes.iter().take(len) {
207                    input.push((self.eval_word(byte)? & U256::from(0xff)).to::<u8>());
208                }
209                keccak256(input).into()
210            }
211            SymExprKind::Not(value) => !self.eval_word(value)?,
212            SymExprKind::BinOp(op, left, right) => {
213                op.eval(self.eval_word(left)?, self.eval_word(right)?)
214            }
215            SymExprKind::TernOp(op, left, right, modulus) => {
216                op.eval(self.eval_word(left)?, self.eval_word(right)?, self.eval_word(modulus)?)
217            }
218            SymExprKind::Ite(condition, then_expr, else_expr) => {
219                if self.eval_bool(condition)? {
220                    self.eval_word(then_expr)?
221                } else {
222                    self.eval_word(else_expr)?
223                }
224            }
225        };
226        self.words.insert(expr.clone(), value);
227        Ok(value)
228    }
229
230    fn eval_bool(&mut self, expr: &SymBoolExpr) -> Result<bool, SymbolicError> {
231        let kind = expr.kind();
232        if let SymBoolExprKind::Const(value) = kind {
233            return Ok(*value);
234        }
235        // `Not` and `Cmp` cheaply recombine child results, so memoizing them adds one-use entries
236        // for ordinary path constraints. Conjunctions can share additional Boolean work.
237        let cache_result = matches!(kind, SymBoolExprKind::And(_));
238        if cache_result && let Some(value) = self.bools.get(expr) {
239            return Ok(*value);
240        }
241
242        let value = match kind {
243            SymBoolExprKind::Const(_) => unreachable!("symbolic eval leaf handled above"),
244            SymBoolExprKind::Not(value) => !self.eval_bool(value)?,
245            SymBoolExprKind::And(values) => {
246                let mut result = true;
247                for value in values.iter() {
248                    if !self.eval_bool(value)? {
249                        result = false;
250                        break;
251                    }
252                }
253                result
254            }
255            SymBoolExprKind::Cmp(op, left, right) => {
256                op.eval(self.eval_word(left)?, self.eval_word(right)?)
257            }
258        };
259        if cache_result {
260            self.bools.insert(expr.clone(), value);
261        }
262        Ok(value)
263    }
264}
265
266pub(crate) fn eval_model_constraints<M: SymbolicModelLookup + ?Sized>(
267    constraints: &[SymBoolExpr],
268    model: &M,
269) -> bool {
270    let mut evaluator = ModelEvaluator::new(model);
271    constraints.iter().all(|constraint| evaluator.eval_bool(constraint).unwrap_or(false))
272}
foundry_evm_symbolic/runtime/expr/mod.rs

foundry_evm_symbolic/runtime/expr/
mod.rs
