foundry_evm_symbolic/executor/
constraints.rs

1use super::*;
2
3impl SymbolicExecutor {
4    pub(super) fn handle_assume(
5        &mut self,
6        state: &mut PathState,
7        condition_offset: usize,
8    ) -> Result<CheatcodeOutcome, SymbolicError> {
9        let cond = state.memory.load_word(&mut self.cx, condition_offset)?;
10        let cond = cond.nonzero_bool(&mut self.cx);
11        self.assume_condition(state, cond)
12    }
13
14    pub(super) fn handle_skip(
15        &mut self,
16        state: &mut PathState,
17        condition_offset: usize,
18    ) -> Result<CheatcodeOutcome, SymbolicError> {
19        let cond = state.memory.load_word(&mut self.cx, condition_offset)?;
20        let cond = cond.nonzero_bool(&mut self.cx).not(&mut self.cx);
21        self.assume_condition(state, cond)
22    }
23
24    pub(super) fn assume_condition(
25        &mut self,
26        state: &mut PathState,
27        condition: SymBoolExpr,
28    ) -> Result<CheatcodeOutcome, SymbolicError> {
29        match condition.as_const() {
30            Some(true) => Ok(CheatcodeOutcome::Continue(Vec::new())),
31            Some(false) => Ok(CheatcodeOutcome::AssumeRejected),
32            None => {
33                state.constraints.push(condition);
34                if self.solver.is_sat(&mut self.cx, &state.constraints)? {
35                    Ok(CheatcodeOutcome::Continue(Vec::new()))
36                } else {
37                    Ok(CheatcodeOutcome::AssumeRejected)
38                }
39            }
40        }
41    }
42
43    pub(super) fn solver_upper_bound_usize(
44        &mut self,
45        state: &PathState,
46        expr: &SymExpr,
47        max: usize,
48        reason: &'static str,
49    ) -> Result<usize, SymbolicError> {
50        let mut above_max = state.constraints.clone();
51        above_max.push(SymBoolExpr::cmp_word_const(
52            &mut self.cx,
53            SymCmpOp::Ugt,
54            expr,
55            U256::from(max),
56        ));
57        if self.solver.is_sat(&mut self.cx, &above_max)? {
58            return Err(SymbolicError::Unsupported(reason));
59        }
60
61        let mut low = 0usize;
62        let mut high = max;
63        while low < high {
64            let mid = low + (high - low) / 2;
65            let mut above_mid = state.constraints.clone();
66            above_mid.push(SymBoolExpr::cmp_word_const(
67                &mut self.cx,
68                SymCmpOp::Ugt,
69                expr,
70                U256::from(mid),
71            ));
72            if self.solver.is_sat(&mut self.cx, &above_mid)? {
73                low = mid + 1;
74            } else {
75                high = mid;
76            }
77        }
78        Ok(low)
79    }
80
81    pub(super) fn assume_expr_at_least(
82        &mut self,
83        state: &mut PathState,
84        expr: &SymExpr,
85        min: usize,
86    ) -> Result<bool, SymbolicError> {
87        let condition =
88            SymBoolExpr::cmp_word_const(&mut self.cx, SymCmpOp::Uge, expr, U256::from(min));
89        match condition.as_const() {
90            Some(value) => Ok(value),
91            None => {
92                let mut constraints = state.constraints.clone();
93                constraints.push(condition);
94                if self.solver.is_sat(&mut self.cx, &constraints)? {
95                    state.constraints = constraints;
96                    Ok(true)
97                } else {
98                    Ok(false)
99                }
100            }
101        }
102    }
103
104    /// Rejects symbolic integer bit widths outside the EVM word size.
105    pub(super) fn validate_symbolic_integer_bits(
106        bits: U256,
107        context: &'static str,
108    ) -> Result<(), SymbolicError> {
109        if bits <= U256::from(256) { Ok(()) } else { Err(SymbolicError::Unsupported(context)) }
110    }
111
112    pub(super) fn handle_bound_uint(
113        &mut self,
114        state: &mut PathState,
115        args_offset: usize,
116    ) -> Result<CheatcodeOutcome, SymbolicError> {
117        let value = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
118        let min = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
119        let max = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 2)?;
120
121        if let (Some(value), Some(min), Some(max)) =
122            (value.as_const(), min.as_const(), max.as_const())
123        {
124            if min >= max || value < min || value > max {
125                return Ok(CheatcodeOutcome::Failure);
126            }
127            let bounded = if value == min { max } else { min };
128            return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(&mut self.cx, bounded)]));
129        }
130
131        if let (Some(min), Some(max)) = (min.as_const(), max.as_const())
132            && min >= max
133        {
134            return Ok(CheatcodeOutcome::Failure);
135        }
136        let (Some(min_word), Some(max_word)) = (min.as_const(), max.as_const()) else {
137            return Err(SymbolicError::Unsupported("symbolic vm.bound range"));
138        };
139
140        let value_expr = value;
141        let min_value = SymExpr::constant(&mut self.cx, min_word);
142        let max_value = SymExpr::constant(&mut self.cx, max_word);
143        let min_condition =
144            SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Uge, value_expr.clone(), min_value);
145        let max_condition =
146            SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, value_expr.clone(), max_value);
147        let in_range = SymBoolExpr::and(&mut self.cx, vec![min_condition, max_condition]);
148        let (_in_range_constraints, in_range_sat) =
149            self.constraints_with_condition(state, in_range.clone())?;
150        if !in_range_sat {
151            return Ok(CheatcodeOutcome::Failure);
152        }
153        let out_of_range = in_range.not(&mut self.cx);
154        let (_out_of_range_constraints, out_of_range_sat) =
155            self.constraints_with_condition(state, out_of_range)?;
156        if out_of_range_sat {
157            return Ok(CheatcodeOutcome::Failure);
158        }
159
160        let bounded = state.fresh_word(&mut self.cx, "vmBoundUint");
161        let min_condition =
162            SymBoolExpr::cmp_word_const(&mut self.cx, SymCmpOp::Uge, &bounded, min_word);
163        let max_condition =
164            SymBoolExpr::cmp_word_const(&mut self.cx, SymCmpOp::Ule, &bounded, max_word);
165        state.constraints.push(min_condition);
166        state.constraints.push(max_condition);
167        let same_value = SymBoolExpr::eq(&mut self.cx, bounded.clone(), value_expr);
168        state.constraints.push(same_value.not(&mut self.cx));
169        Ok(CheatcodeOutcome::Continue(vec![bounded]))
170    }
171
172    pub(super) fn handle_bound_int(
173        &mut self,
174        state: &mut PathState,
175        args_offset: usize,
176    ) -> Result<CheatcodeOutcome, SymbolicError> {
177        let value = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
178        let min = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
179        let max = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 2)?;
180
181        if let (Some(value), Some(min), Some(max)) =
182            (value.as_const(), min.as_const(), max.as_const())
183        {
184            if !slt(min, max) || slt(value, min) || slt(max, value) {
185                return Ok(CheatcodeOutcome::Failure);
186            }
187            let bounded = if value == min { max } else { min };
188            return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(&mut self.cx, bounded)]));
189        }
190
191        if let (Some(min), Some(max)) = (min.as_const(), max.as_const())
192            && !slt(min, max)
193        {
194            return Ok(CheatcodeOutcome::Failure);
195        }
196        let (Some(min_word), Some(max_word)) = (min.as_const(), max.as_const()) else {
197            return Err(SymbolicError::Unsupported("symbolic vm.bound range"));
198        };
199
200        let value_expr = value;
201        let min_value = SymExpr::constant(&mut self.cx, min_word);
202        let max_value = SymExpr::constant(&mut self.cx, max_word);
203        let below_min =
204            SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Slt, value_expr.clone(), min_value);
205        let above_max =
206            SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Sgt, value_expr.clone(), max_value);
207        let below_min = below_min.not(&mut self.cx);
208        let above_max = above_max.not(&mut self.cx);
209        let in_range = SymBoolExpr::and(&mut self.cx, vec![below_min, above_max]);
210        let (_in_range_constraints, in_range_sat) =
211            self.constraints_with_condition(state, in_range.clone())?;
212        if !in_range_sat {
213            return Ok(CheatcodeOutcome::Failure);
214        }
215        let out_of_range = in_range.not(&mut self.cx);
216        let (_out_of_range_constraints, out_of_range_sat) =
217            self.constraints_with_condition(state, out_of_range)?;
218        if out_of_range_sat {
219            return Ok(CheatcodeOutcome::Failure);
220        }
221
222        let bounded = state.fresh_word(&mut self.cx, "vmBoundInt");
223        let below_min =
224            SymBoolExpr::cmp_word_const(&mut self.cx, SymCmpOp::Slt, &bounded, min_word);
225        let above_max =
226            SymBoolExpr::cmp_word_const(&mut self.cx, SymCmpOp::Sgt, &bounded, max_word);
227        let below_min = below_min.not(&mut self.cx);
228        let above_max = above_max.not(&mut self.cx);
229        state.constraints.push(below_min);
230        state.constraints.push(above_max);
231        let same_value = SymBoolExpr::eq(&mut self.cx, bounded.clone(), value_expr);
232        state.constraints.push(same_value.not(&mut self.cx));
233        Ok(CheatcodeOutcome::Continue(vec![bounded]))
234    }
235}
foundry_evm_symbolic/executor/constraints.rs

foundry_evm_symbolic/executor/
constraints.rs
