foundry_evm_symbolic/runtime/expr/
bool.rs

1use super::{hashcons::HashConsed, *};
2
3#[derive(Clone, PartialEq, Eq, Hash)]
4pub(crate) struct SymBoolExpr {
5    pub(in crate::runtime::expr) kind: HashConsed<SymBoolExprKind>,
6}
7
8impl fmt::Debug for SymBoolExpr {
9    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
10        self.kind().fmt(f)
11    }
12}
13
14#[derive(Clone, Debug, PartialEq, Eq, Hash)]
15pub(in crate::runtime) enum SymBoolExprKind {
16    Const(bool),
17    Not(SymBoolExpr),
18    And(Arc<[SymBoolExpr]>),
19    Cmp(SymCmpOp, SymExpr, SymExpr),
20}
21
22impl SymBoolExpr {
23    pub(in crate::runtime) fn kind(&self) -> &SymBoolExprKind {
24        self.kind.value()
25    }
26
27    pub(in crate::runtime) fn into_kind(self) -> SymBoolExprKind {
28        self.kind.into_value()
29    }
30
31    pub(in crate::runtime) fn from_kind(cx: &mut SymCx, kind: SymBoolExprKind) -> Self {
32        cx.mk_bool_kind(kind)
33    }
34
35    pub(crate) fn constant(cx: &mut SymCx, value: bool) -> Self {
36        cx.cached_bool(value)
37    }
38
39    pub(crate) fn cmp_word_const(
40        cx: &mut SymCx,
41        op: SymCmpOp,
42        word: &SymExpr,
43        value: U256,
44    ) -> Self {
45        if let Some(word) = word.as_const() {
46            Self::constant(cx, op.eval(word, value))
47        } else {
48            let value = SymExpr::constant(cx, value);
49            Self::cmp(cx, op, word.clone(), value)
50        }
51    }
52
53    pub(crate) fn eq_word_const(cx: &mut SymCx, word: &SymExpr, value: U256) -> Self {
54        if let Some(word) = word.as_const() {
55            Self::constant(cx, word == value)
56        } else {
57            let value = SymExpr::constant(cx, value);
58            Self::eq(cx, word.clone(), value)
59        }
60    }
61
62    pub(crate) fn eq(cx: &mut SymCx, left: SymExpr, right: SymExpr) -> Self {
63        Self::cmp(cx, SymCmpOp::Eq, left, right)
64    }
65
66    pub(crate) fn cmp(cx: &mut SymCx, op: SymCmpOp, left: SymExpr, right: SymExpr) -> Self {
67        match op {
68            SymCmpOp::Eq => match (left.kind(), right.kind()) {
69                // `a == a => true`.
70                _ if left == right => Self::constant(cx, true),
71                (SymExprKind::Const(left), SymExprKind::Const(right)) => {
72                    // `const == const => const`.
73                    Self::constant(cx, left == right)
74                }
75                (_, SymExprKind::Const(right_value)) => {
76                    if let Some(condition) = Self::bool_word_eq_const(cx, &left, *right_value) {
77                        return condition;
78                    }
79                    if let Some(left_value) = left.known_word() {
80                        // `known(a) == const => const`.
81                        return Self::constant(cx, left_value == *right_value);
82                    }
83                    // `a == b => ordered(a, b)`.
84                    let (left, right) = SymExpr::ordered_commutative_operands(left, right);
85                    Self::from_kind(cx, SymBoolExprKind::Cmp(SymCmpOp::Eq, left, right))
86                }
87                (SymExprKind::Const(left_value), _) => {
88                    if let Some(condition) = Self::bool_word_eq_const(cx, &right, *left_value) {
89                        return condition;
90                    }
91                    if let Some(right_value) = right.known_word() {
92                        // `const == known(a) => const`.
93                        return Self::constant(cx, *left_value == right_value);
94                    }
95                    // `a == b => ordered(a, b)`.
96                    let (left, right) = SymExpr::ordered_commutative_operands(left, right);
97                    Self::from_kind(cx, SymBoolExprKind::Cmp(SymCmpOp::Eq, left, right))
98                }
99                (
100                    SymExprKind::Keccak { len: left_len, bytes: left_bytes, .. },
101                    SymExprKind::Keccak { len: right_len, bytes: right_bytes, .. },
102                ) if left_bytes.len() == right_bytes.len() => {
103                    // `keccak(a) == keccak(b) => len(a) == len(b) && bytes(a) == bytes(b)`.
104                    let mut conditions = vec![Self::eq(cx, left_len.clone(), right_len.clone())];
105                    conditions.extend(
106                        left_bytes
107                            .iter()
108                            .cloned()
109                            .zip(right_bytes.iter().cloned())
110                            .map(|(left, right)| Self::eq(cx, left, right)),
111                    );
112                    Self::and(cx, conditions)
113                }
114                (
115                    SymExprKind::Hash { algorithm: left_algorithm, bytes: left_bytes, .. },
116                    SymExprKind::Hash { algorithm: right_algorithm, bytes: right_bytes, .. },
117                ) if left_algorithm == right_algorithm && left_bytes.len() == right_bytes.len() => {
118                    // `hash(a) == hash(b) => bytes(a) == bytes(b)`.
119                    let conditions = left_bytes
120                        .iter()
121                        .cloned()
122                        .zip(right_bytes.iter().cloned())
123                        .map(|(left, right)| Self::eq(cx, left, right))
124                        .collect();
125                    Self::and(cx, conditions)
126                }
127                _ => {
128                    // `a == b => ordered(a, b)`.
129                    let (left, right) = SymExpr::ordered_commutative_operands(left, right);
130                    Self::from_kind(cx, SymBoolExprKind::Cmp(SymCmpOp::Eq, left, right))
131                }
132            },
133            SymCmpOp::Ult => match (left.kind(), right.kind()) {
134                // `a < a => false`.
135                _ if left == right => Self::constant(cx, false),
136                (SymExprKind::Const(left), SymExprKind::Const(right)) => {
137                    // `const < const => const`.
138                    Self::constant(cx, op.eval(*left, *right))
139                }
140                // `a < 0 => false`.
141                (_, SymExprKind::Const(value)) if value.is_zero() => Self::constant(cx, false),
142                // `MAX < a => false`.
143                (SymExprKind::Const(value), _) if *value == U256::MAX => Self::constant(cx, false),
144                // `a < a & low_mask => false`.
145                _ if low_masked_source_any(&right) == Some(&left) => Self::constant(cx, false),
146                _ => Self::from_kind(cx, SymBoolExprKind::Cmp(op, left, right)),
147            },
148            SymCmpOp::Ugt => match (left.kind(), right.kind()) {
149                // `a > a => false`.
150                _ if left == right => Self::constant(cx, false),
151                (SymExprKind::Const(left), SymExprKind::Const(right)) => {
152                    // `const > const => const`.
153                    Self::constant(cx, op.eval(*left, *right))
154                }
155                // `0 > a => false`.
156                (SymExprKind::Const(value), _) if value.is_zero() => Self::constant(cx, false),
157                // `a > MAX => false`.
158                (_, SymExprKind::Const(value)) if *value == U256::MAX => Self::constant(cx, false),
159                // `a & low_mask > a => false`.
160                _ if low_masked_source_any(&left) == Some(&right) => Self::constant(cx, false),
161                _ => Self::from_kind(cx, SymBoolExprKind::Cmp(op, left, right)),
162            },
163            SymCmpOp::Ule => match (left.kind(), right.kind()) {
164                // `a <= a => true`.
165                _ if left == right => Self::constant(cx, true),
166                (SymExprKind::Const(left), SymExprKind::Const(right)) => {
167                    // `const <= const => const`.
168                    Self::constant(cx, op.eval(*left, *right))
169                }
170                // `0 <= a => true`.
171                (SymExprKind::Const(value), _) if value.is_zero() => Self::constant(cx, true),
172                // `a <= MAX => true`.
173                (_, SymExprKind::Const(value)) if *value == U256::MAX => Self::constant(cx, true),
174                // `a & low_mask <= a => true`.
175                _ if low_masked_source_any(&left) == Some(&right) => Self::constant(cx, true),
176                _ => Self::from_kind(cx, SymBoolExprKind::Cmp(op, left, right)),
177            },
178            SymCmpOp::Uge => match (left.kind(), right.kind()) {
179                // `a >= a => true`.
180                _ if left == right => Self::constant(cx, true),
181                (SymExprKind::Const(left), SymExprKind::Const(right)) => {
182                    // `const >= const => const`.
183                    Self::constant(cx, op.eval(*left, *right))
184                }
185                // `a >= 0 => true`.
186                (_, SymExprKind::Const(value)) if value.is_zero() => Self::constant(cx, true),
187                // `MAX >= a => true`.
188                (SymExprKind::Const(value), _) if *value == U256::MAX => Self::constant(cx, true),
189                // `a >= a & low_mask => true`.
190                _ if low_masked_source_any(&right) == Some(&left) => Self::constant(cx, true),
191                _ => Self::from_kind(cx, SymBoolExprKind::Cmp(op, left, right)),
192            },
193            SymCmpOp::Slt | SymCmpOp::Sgt => match (left.kind(), right.kind()) {
194                // `a <s a => false`, `a >s a => false`.
195                _ if left == right => Self::constant(cx, false),
196                (SymExprKind::Const(left), SymExprKind::Const(right)) => {
197                    // `const <s const => const`.
198                    Self::constant(cx, op.eval(*left, *right))
199                }
200                _ => Self::from_kind(cx, SymBoolExprKind::Cmp(op, left, right)),
201            },
202        }
203    }
204
205    pub(crate) fn and(cx: &mut SymCx, values: Vec<Self>) -> Self {
206        let mut out = Vec::new();
207        for value in values {
208            match value.kind() {
209                // `true && a => a`.
210                SymBoolExprKind::Const(true) => {}
211                // `false && a => false`.
212                SymBoolExprKind::Const(false) => return Self::constant(cx, false),
213                // `(a && b) && c => a && b && c`.
214                SymBoolExprKind::And(values) => out.extend(values.iter().cloned()),
215                _ => out.push(value),
216            }
217        }
218        if out.is_empty() {
219            // `and() => true`.
220            Self::constant(cx, true)
221        } else if out.len() == 1 {
222            // `and(a) => a`.
223            out.pop().expect("single item exists")
224        } else {
225            Self::from_kind(cx, SymBoolExprKind::And(out.into()))
226        }
227    }
228
229    pub(crate) fn or(cx: &mut SymCx, values: Vec<Self>) -> Self {
230        let mut out = Vec::new();
231        for value in values {
232            match value.kind() {
233                // `false || a => a`.
234                SymBoolExprKind::Const(false) => {}
235                // `true || a => true`.
236                SymBoolExprKind::Const(true) => return Self::constant(cx, true),
237                _ => out.push(value),
238            }
239        }
240        if out.is_empty() {
241            // `or() => false`.
242            Self::constant(cx, false)
243        } else if out.len() == 1 {
244            // `or(a) => a`.
245            out.pop().expect("single item exists")
246        } else {
247            // `a || b => !(!a && !b)`.
248            let values = out.into_iter().map(|value| Self::not_bool(cx, value)).collect();
249            let and = Self::and(cx, values);
250            Self::not_bool(cx, and)
251        }
252    }
253
254    pub(crate) fn not_bool(cx: &mut SymCx, value: Self) -> Self {
255        match value.kind() {
256            // `!const => const`.
257            SymBoolExprKind::Const(value) => Self::constant(cx, !*value),
258            // `!!a => a`.
259            SymBoolExprKind::Not(value) => value.clone(),
260            _ => Self::from_kind(cx, SymBoolExprKind::Not(value)),
261        }
262    }
263
264    fn bool_word_eq_const(cx: &mut SymCx, word: &SymExpr, value: U256) -> Option<Self> {
265        let SymExprKind::Ite(condition, then_expr, else_expr) = word.kind() else { return None };
266        match (then_expr.as_const(), else_expr.as_const()) {
267            (Some(then_value), Some(else_value))
268                if then_value == U256::from(1) && else_value.is_zero() =>
269            {
270                Some(if value.is_zero() {
271                    Self::not_bool(cx, condition.clone())
272                } else if value == U256::from(1) {
273                    condition.clone()
274                } else {
275                    Self::constant(cx, false)
276                })
277            }
278            (Some(then_value), Some(else_value))
279                if then_value.is_zero() && else_value == U256::from(1) =>
280            {
281                Some(if value.is_zero() {
282                    condition.clone()
283                } else if value == U256::from(1) {
284                    Self::not_bool(cx, condition.clone())
285                } else {
286                    Self::constant(cx, false)
287                })
288            }
289            _ => None,
290        }
291    }
292
293    pub(crate) fn as_const(&self) -> Option<bool> {
294        match self.kind() {
295            SymBoolExprKind::Const(value) => Some(*value),
296            _ => None,
297        }
298    }
299
300    pub(in crate::runtime) fn zero_check_operand(&self) -> Option<&SymExpr> {
301        match self.kind() {
302            SymBoolExprKind::Cmp(SymCmpOp::Eq, left, right)
303                if right.as_const().is_some_and(|value| value.is_zero()) =>
304            {
305                Some(left)
306            }
307            _ => None,
308        }
309    }
310
311    pub(crate) fn contains_keccak(&self) -> bool {
312        self.visit_bool(|expr| matches!(expr.kind(), SymExprKind::Keccak { .. }))
313    }
314
315    pub(crate) fn contains_gasleft(&self) -> bool {
316        self.visit_bool(|expr| matches!(expr.kind(), SymExprKind::GasLeft(_)))
317    }
318
319    pub(crate) fn contains_udiv(&self) -> bool {
320        self.visit_bool(|expr| expr.contains_udiv())
321    }
322
323    pub(crate) fn forces_expr_const_with_context(
324        &self,
325        expr: &SymExpr,
326        context: &[Self],
327    ) -> Option<U256> {
328        match self.kind() {
329            SymBoolExprKind::Cmp(SymCmpOp::Eq, left, right) => match right.kind() {
330                SymExprKind::Const(value) => left.equality_forces_const(*value, expr, context),
331                _ => None,
332            },
333            SymBoolExprKind::Not(value) => match value.kind() {
334                SymBoolExprKind::Cmp(SymCmpOp::Eq, left, right) => match right.kind() {
335                    SymExprKind::Const(value) if value.is_zero() => {
336                        left.nonzero_forces_const(expr, context)
337                    }
338                    _ => None,
339                },
340                SymBoolExprKind::Not(value) => value.forces_expr_const_with_context(expr, context),
341                _ => None,
342            },
343            SymBoolExprKind::And(values) => {
344                values.iter().find_map(|value| value.forces_expr_const_with_context(expr, context))
345            }
346            _ => None,
347        }
348    }
349
350    pub(crate) fn upper_bound_usize(&self, expr: &SymExpr) -> Option<usize> {
351        match self.kind() {
352            SymBoolExprKind::Const(_) | SymBoolExprKind::Not(_) => None,
353            SymBoolExprKind::And(values) => {
354                let mut bound: Option<usize> = None;
355                for value in values.iter() {
356                    if let Some(candidate) = value.upper_bound_usize(expr) {
357                        bound = Some(bound.map_or(candidate, |bound| bound.min(candidate)));
358                    }
359                }
360                bound
361            }
362            SymBoolExprKind::Cmp(op, left, right) => {
363                if *op == SymCmpOp::Eq {
364                    return match (left == expr, right == expr) {
365                        (true, _) => right.eval().and_then(|value| usize::try_from(value).ok()),
366                        (_, true) => left.eval().and_then(|value| usize::try_from(value).ok()),
367                        _ => None,
368                    };
369                }
370                if left == expr {
371                    match *op {
372                        SymCmpOp::Ult => right
373                            .eval()
374                            .and_then(|bound| (!bound.is_zero()).then(|| bound - U256::from(1)))
375                            .and_then(|value| usize::try_from(value).ok()),
376                        SymCmpOp::Ule => right.eval().and_then(|value| usize::try_from(value).ok()),
377                        _ => None,
378                    }
379                } else if right == expr {
380                    match *op {
381                        SymCmpOp::Ugt => left
382                            .eval()
383                            .and_then(|bound| (!bound.is_zero()).then(|| bound - U256::from(1)))
384                            .and_then(|value| usize::try_from(value).ok()),
385                        SymCmpOp::Uge => left.eval().and_then(|value| usize::try_from(value).ok()),
386                        _ => None,
387                    }
388                } else {
389                    None
390                }
391            }
392        }
393    }
394
395    pub(crate) fn eval_model<M: SymbolicModelLookup + ?Sized>(
396        &self,
397        model: &M,
398    ) -> Result<bool, SymbolicError> {
399        Ok(match self.kind() {
400            SymBoolExprKind::Const(value) => *value,
401            SymBoolExprKind::Not(value) => !value.eval_model(model)?,
402            SymBoolExprKind::And(values) => {
403                for value in values.iter() {
404                    if !value.eval_model(model)? {
405                        return Ok(false);
406                    }
407                }
408                true
409            }
410            SymBoolExprKind::Cmp(op, left, right) => {
411                op.eval(left.eval_model(model)?, right.eval_model(model)?)
412            }
413        })
414    }
415
416    pub(crate) fn eval_model_if_complete<M: SymbolicModelLookup + ?Sized>(
417        &self,
418        model: &M,
419    ) -> Result<Option<bool>, SymbolicError> {
420        let mut vars = SymbolicVars::default();
421        self.collect_eval_vars(&mut vars);
422        if vars.iter().copied().all(|var| model.contains_name(var)) {
423            self.eval_model(model).map(Some)
424        } else {
425            Ok(None)
426        }
427    }
428
429    /// Visits all word expressions contained in this boolean expression.
430    pub(crate) fn visit_exprs<B>(
431        &self,
432        visitor: &mut impl FnMut(&SymExpr) -> ControlFlow<B>,
433    ) -> ControlFlow<B> {
434        match self.kind() {
435            SymBoolExprKind::Const(_) => {}
436            SymBoolExprKind::Not(value) => value.visit_exprs(visitor)?,
437            SymBoolExprKind::And(values) => {
438                for value in values.iter() {
439                    value.visit_exprs(visitor)?;
440                }
441            }
442            SymBoolExprKind::Cmp(_, left, right) => {
443                left.visit(visitor)?;
444                right.visit(visitor)?;
445            }
446        }
447        ControlFlow::Continue(())
448    }
449
450    pub(crate) fn visit_bool(&self, mut visitor: impl FnMut(&SymExpr) -> bool) -> bool {
451        self.visit_exprs(&mut |expr| {
452            if visitor(expr) { ControlFlow::Break(()) } else { ControlFlow::Continue(()) }
453        })
454        .is_break()
455    }
456
457    pub(crate) fn fold(
458        self,
459        cx: &mut SymCx,
460        folder: &mut impl FnMut(&mut SymCx, Self) -> Self,
461    ) -> Self {
462        if matches!(self.kind(), SymBoolExprKind::Const(_)) {
463            return folder(cx, self);
464        }
465
466        let expr = match self.into_kind() {
467            SymBoolExprKind::Not(value) => {
468                let value = value.fold(cx, folder);
469                Self::not_bool(cx, value)
470            }
471            SymBoolExprKind::And(values) => {
472                let values = values.iter().cloned().map(|value| value.fold(cx, folder)).collect();
473                Self::and(cx, values)
474            }
475            SymBoolExprKind::Cmp(op, left, right) => Self::cmp(cx, op, left, right),
476            SymBoolExprKind::Const(_) => unreachable!("leaf boolean returned before folding"),
477        };
478        folder(cx, expr)
479    }
480
481    pub(crate) fn fold_exprs(
482        self,
483        cx: &mut SymCx,
484        folder: &mut impl FnMut(&mut SymCx, SymExpr) -> SymExpr,
485    ) -> Self {
486        if matches!(self.kind(), SymBoolExprKind::Const(_)) {
487            return self;
488        }
489
490        match self.into_kind() {
491            SymBoolExprKind::Not(value) => {
492                let value = value.fold_exprs(cx, folder);
493                Self::not_bool(cx, value)
494            }
495            SymBoolExprKind::And(values) => {
496                let values =
497                    values.iter().cloned().map(|value| value.fold_exprs(cx, folder)).collect();
498                Self::and(cx, values)
499            }
500            SymBoolExprKind::Cmp(op, left, right) => {
501                let left = left.fold(cx, folder);
502                let right = right.fold(cx, folder);
503                Self::cmp(cx, op, left, right)
504            }
505            SymBoolExprKind::Const(_) => unreachable!("leaf boolean returned before folding exprs"),
506        }
507    }
508
509    #[cfg(test)]
510    pub(crate) fn raw_and(cx: &mut SymCx, values: Vec<Self>) -> Self {
511        Self::from_kind(cx, SymBoolExprKind::And(values.into()))
512    }
513
514    pub(crate) fn cmp_word_expr(
515        cx: &mut SymCx,
516        op: SymCmpOp,
517        word: &SymExpr,
518        expr: SymExpr,
519    ) -> Self {
520        Self::cmp(cx, op, word.clone(), expr)
521    }
522
523    pub(crate) fn not(self, cx: &mut SymCx) -> Self {
524        Self::not_bool(cx, self)
525    }
526
527    pub(crate) fn collect_vars(&self, vars: &mut SymbolicVars) {
528        let _ = self.visit_exprs(&mut |expr| {
529            if let Some(var) = expr.kind().get_var() {
530                vars.insert(var);
531            }
532            ControlFlow::<()>::Continue(())
533        });
534    }
535
536    pub(crate) fn collect_eval_vars(&self, vars: &mut SymbolicVars) {
537        let _ = self.visit_exprs(&mut |expr| {
538            if let Some(var) = expr.kind().get_eval_var() {
539                vars.insert(var);
540            }
541            ControlFlow::<()>::Continue(())
542        });
543    }
544
545    pub(crate) fn smt(&self, cx: &SymCx) -> String {
546        let mut smt = String::new();
547        self.write_smt(cx, &mut smt);
548        smt
549    }
550
551    pub(in crate::runtime::expr) fn write_smt(&self, cx: &SymCx, out: &mut String) {
552        match self.kind() {
553            SymBoolExprKind::Const(value) => out.push_str(if *value { "true" } else { "false" }),
554            SymBoolExprKind::Not(value) => {
555                out.push_str("(not ");
556                value.write_smt(cx, out);
557                out.push(')');
558            }
559            SymBoolExprKind::And(values) => {
560                out.push_str("(and");
561                for value in values.iter() {
562                    out.push(' ');
563                    value.write_smt(cx, out);
564                }
565                out.push(')');
566            }
567            SymBoolExprKind::Cmp(op, left, right) => {
568                let _ = write!(out, "({} ", op.smt());
569                left.write_smt(cx, out);
570                out.push(' ');
571                right.write_smt(cx, out);
572                out.push(')');
573            }
574        }
575    }
576}
577
578#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
579pub(crate) enum SymCmpOp {
580    Eq,
581    Ult,
582    Ugt,
583    Ule,
584    Uge,
585    Slt,
586    Sgt,
587}
588
589impl SymCmpOp {
590    pub(crate) const fn smt(self) -> &'static str {
591        match self {
592            Self::Eq => "=",
593            Self::Ult => "bvult",
594            Self::Ugt => "bvugt",
595            Self::Ule => "bvule",
596            Self::Uge => "bvuge",
597            Self::Slt => "bvslt",
598            Self::Sgt => "bvsgt",
599        }
600    }
601
602    pub(crate) fn eval(self, left: U256, right: U256) -> bool {
603        match self {
604            Self::Eq => left == right,
605            Self::Ult => left < right,
606            Self::Ugt => left > right,
607            Self::Ule => left <= right,
608            Self::Uge => left >= right,
609            Self::Slt => slt(left, right),
610            Self::Sgt => slt(right, left),
611        }
612    }
613}
foundry_evm_symbolic/runtime/expr/bool.rs

foundry_evm_symbolic/runtime/expr/
bool.rs
