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::ONE)) };
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    pub(crate) fn symbol_name(&self, symbol: Symbol) -> &str {
79        self.symbols.resolve(symbol)
80    }
81
82    pub(crate) fn mark_replayable_input(&mut self, symbol: Symbol) {
83        self.replayable_inputs.insert(symbol);
84    }
85
86    pub(crate) fn is_replayable_input(&self, symbol: Symbol) -> bool {
87        self.replayable_inputs.contains(&symbol)
88    }
89
90    pub(in crate::runtime::expr) fn record_concrete_keccak_preimage(
91        &mut self,
92        hash: U256,
93        bytes: Arc<[SymExpr]>,
94    ) {
95        self.concrete_keccak_preimages.entry(hash).or_insert(bytes);
96    }
97
98    pub(in crate::runtime::expr) fn concrete_keccak_preimage(
99        &self,
100        hash: U256,
101    ) -> Option<Arc<[SymExpr]>> {
102        self.concrete_keccak_preimages.get(&hash).cloned()
103    }
104}
105
106impl fmt::Debug for SymCx {
107    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
108        f.debug_struct("SymCx").finish_non_exhaustive()
109    }
110}
111
112impl Default for SymCx {
113    fn default() -> Self {
114        Self::new()
115    }
116}
foundry_evm_symbolic/runtime/expr/cx.rs

foundry_evm_symbolic/runtime/expr/
cx.rs
