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/// Evaluates hash-consed expressions once per model.
31///
32/// Symbolic expressions form a DAG, so recursively evaluating both operands without caching can
33/// revisit the same node exponentially many times.
34struct ModelEvaluator<'a, M: ?Sized> {
35    model: &'a M,
36    words: HashMap<SymExpr, U256>,
37    bools: HashMap<SymBoolExpr, bool>,
38}
39
40impl<'a, M: SymbolicModelLookup + ?Sized> ModelEvaluator<'a, M> {
41    fn new(model: &'a M) -> Self {
42        Self { model, words: HashMap::default(), bools: HashMap::default() }
43    }
44
45    fn eval_word(&mut self, expr: &SymExpr) -> Result<U256, SymbolicError> {
46        let kind = expr.kind();
47        if let Some(var) = kind.get_eval_var() {
48            return Ok(self.model.value(var).unwrap_or_default());
49        }
50        if let SymExprKind::Const(value) = kind {
51            return Ok(*value);
52        }
53        if let Some(value) = self.words.get(expr) {
54            return Ok(*value);
55        }
56
57        let value = match kind {
58            SymExprKind::Const(_)
59            | SymExprKind::Var(_)
60            | SymExprKind::GasLeft(_)
61            | SymExprKind::Hash { .. } => unreachable!("symbolic eval leaf handled above"),
62            SymExprKind::Keccak { len, bytes, .. } => {
63                let len = self.eval_word(len)?;
64                let Ok(len) = usize::try_from(len) else {
65                    return Err(SymbolicError::Solver(
66                        "solver model uses an invalid keccak length".to_string(),
67                    ));
68                };
69                if len > bytes.len() {
70                    return Err(SymbolicError::Solver(
71                        "solver model uses an invalid keccak length".to_string(),
72                    ));
73                }
74
75                let mut input = Vec::with_capacity(len);
76                for byte in bytes.iter().take(len) {
77                    input.push((self.eval_word(byte)? & U256::from(0xff)).to::<u8>());
78                }
79                U256::from_be_bytes(keccak256(input).0)
80            }
81            SymExprKind::Not(value) => !self.eval_word(value)?,
82            SymExprKind::BinOp(op, left, right) => {
83                op.eval(self.eval_word(left)?, self.eval_word(right)?)
84            }
85            SymExprKind::TernOp(op, left, right, modulus) => {
86                op.eval(self.eval_word(left)?, self.eval_word(right)?, self.eval_word(modulus)?)
87            }
88            SymExprKind::Ite(condition, then_expr, else_expr) => {
89                if self.eval_bool(condition)? {
90                    self.eval_word(then_expr)?
91                } else {
92                    self.eval_word(else_expr)?
93                }
94            }
95        };
96        self.words.insert(expr.clone(), value);
97        Ok(value)
98    }
99
100    fn eval_bool(&mut self, expr: &SymBoolExpr) -> Result<bool, SymbolicError> {
101        let kind = expr.kind();
102        if let SymBoolExprKind::Const(value) = kind {
103            return Ok(*value);
104        }
105        // `Not` and `Cmp` cheaply recombine child results, so memoizing them adds one-use entries
106        // for ordinary path constraints. Conjunctions can share additional Boolean work.
107        let cache_result = matches!(kind, SymBoolExprKind::And(_));
108        if cache_result && let Some(value) = self.bools.get(expr) {
109            return Ok(*value);
110        }
111
112        let value = match kind {
113            SymBoolExprKind::Const(_) => unreachable!("symbolic eval leaf handled above"),
114            SymBoolExprKind::Not(value) => !self.eval_bool(value)?,
115            SymBoolExprKind::And(values) => {
116                let mut result = true;
117                for value in values.iter() {
118                    if !self.eval_bool(value)? {
119                        result = false;
120                        break;
121                    }
122                }
123                result
124            }
125            SymBoolExprKind::Cmp(op, left, right) => {
126                op.eval(self.eval_word(left)?, self.eval_word(right)?)
127            }
128        };
129        if cache_result {
130            self.bools.insert(expr.clone(), value);
131        }
132        Ok(value)
133    }
134}
135
136pub(crate) fn eval_model_constraints<M: SymbolicModelLookup + ?Sized>(
137    constraints: &[SymBoolExpr],
138    model: &M,
139) -> bool {
140    let mut evaluator = ModelEvaluator::new(model);
141    constraints.iter().all(|constraint| evaluator.eval_bool(constraint).unwrap_or(false))
142}
143
144#[cfg(test)]
145mod tests {
146    use super::*;
147
148    #[test]
149    fn model_evaluator_only_caches_conjunctions() {
150        let mut cx = SymCx::new();
151        let value = SymExpr::var(&mut cx, "value");
152        let one = SymExpr::constant(&mut cx, U256::from(1));
153        let condition = SymBoolExpr::eq(&mut cx, value, one).not(&mut cx);
154        let model = SymbolicModel::default();
155        let mut evaluator = ModelEvaluator::new(&model);
156
157        assert!(evaluator.eval_bool(&condition).unwrap());
158        assert!(evaluator.bools.is_empty());
159        let conjunction = SymBoolExpr::and(&mut cx, vec![condition.clone(), condition]);
160        assert!(evaluator.eval_bool(&conjunction).unwrap());
161        assert_eq!(evaluator.bools.len(), 1);
162    }
163}
foundry_evm_symbolic/runtime/expr/mod.rs

foundry_evm_symbolic/runtime/expr/
mod.rs
