foundry_evm_symbolic/executor/
constraints.rs

1use super::*;
2use foundry_evm::revm::interpreter::instructions::i256::i256_cmp;
3
4impl SymbolicExecutor {
5    pub(super) fn handle_assume(
6        &mut self,
7        state: &mut PathState,
8        condition_offset: usize,
9    ) -> Result<CheatcodeOutcome, SymbolicError> {
10        let cond = state.memory.load_word(&mut self.cx, condition_offset)?;
11        let cond = cond.nonzero_bool(&mut self.cx);
12        self.assume_condition(state, cond)
13    }
14
15    pub(super) fn handle_skip(
16        &mut self,
17        state: &mut PathState,
18        condition_offset: usize,
19    ) -> Result<CheatcodeOutcome, SymbolicError> {
20        let cond = state.memory.load_word(&mut self.cx, condition_offset)?;
21        let cond = cond.nonzero_bool(&mut self.cx).not(&mut self.cx);
22        self.assume_condition(state, cond)
23    }
24
25    pub(super) fn assume_condition(
26        &mut self,
27        state: &mut PathState,
28        condition: SymBoolExpr,
29    ) -> Result<CheatcodeOutcome, SymbolicError> {
30        match condition.as_const() {
31            Some(true) => Ok(CheatcodeOutcome::Continue(Vec::new())),
32            Some(false) => Ok(CheatcodeOutcome::AssumeRejected),
33            None => {
34                state.constraints.push(condition);
35                if self.is_sat_with_state(state, &state.constraints)? {
36                    Ok(CheatcodeOutcome::Continue(Vec::new()))
37                } else {
38                    Ok(CheatcodeOutcome::AssumeRejected)
39                }
40            }
41        }
42    }
43
44    pub(super) fn solver_upper_bound_usize(
45        &mut self,
46        state: &PathState,
47        expr: &SymExpr,
48        max: usize,
49        reason: &'static str,
50    ) -> Result<usize, SymbolicError> {
51        let mut above_max = state.constraints.clone();
52        above_max.push(SymBoolExpr::cmp_word_const(
53            &mut self.cx,
54            SymCmpOp::Ugt,
55            expr,
56            U256::from(max),
57        ));
58        if self.is_sat_with_state(state, &above_max)? {
59            return Err(SymbolicError::Unsupported(reason));
60        }
61
62        let mut low = 0usize;
63        let mut high = max;
64        while low < high {
65            let mid = low + (high - low) / 2;
66            let mut above_mid = state.constraints.clone();
67            above_mid.push(SymBoolExpr::cmp_word_const(
68                &mut self.cx,
69                SymCmpOp::Ugt,
70                expr,
71                U256::from(mid),
72            ));
73            if self.is_sat_with_state(state, &above_mid)? {
74                low = mid + 1;
75            } else {
76                high = mid;
77            }
78        }
79        Ok(low)
80    }
81
82    pub(super) fn assume_expr_at_least(
83        &mut self,
84        state: &mut PathState,
85        expr: &SymExpr,
86        min: usize,
87    ) -> Result<bool, SymbolicError> {
88        let condition =
89            SymBoolExpr::cmp_word_const(&mut self.cx, SymCmpOp::Uge, expr, U256::from(min));
90        match condition.as_const() {
91            Some(value) => Ok(value),
92            None => {
93                let mut constraints = state.constraints.clone();
94                constraints.push(condition);
95                if self.is_sat_with_state(state, &constraints)? {
96                    state.constraints = constraints;
97                    Ok(true)
98                } else {
99                    Ok(false)
100                }
101            }
102        }
103    }
104
105    /// Proves that every feasible value is at least `min` without restricting the path.
106    pub(super) fn proves_expr_at_least(
107        &mut self,
108        state: &PathState,
109        expr: &SymExpr,
110        min: usize,
111    ) -> Result<bool, SymbolicError> {
112        if state.lower_bound_usize(expr) >= min {
113            return Ok(true);
114        }
115
116        let mut below_min = state.constraints.clone();
117        below_min.push(SymBoolExpr::cmp_word_const(
118            &mut self.cx,
119            SymCmpOp::Ult,
120            expr,
121            U256::from(min),
122        ));
123        Ok(!self.is_sat_with_state(state, &below_min)?)
124    }
125
126    /// Resolves a path-constant word and proves that no alternate value is feasible.
127    pub(super) fn constrained_word_with_solver(
128        &mut self,
129        state: &PathState,
130        expr: &SymExpr,
131    ) -> Result<Option<U256>, SymbolicError> {
132        if let Some(value) = state.constrained_word(&mut self.cx, expr) {
133            return Ok(Some(value));
134        }
135        if expr.contains_gasleft() {
136            return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
137        }
138
139        let replayable_storage = state.world.replay_storage_symbols();
140        let model = self.solver.model_with_replayable_storage(
141            &mut self.cx,
142            &state.constraints,
143            &replayable_storage,
144        )?;
145        let value = expr.eval_model(&model)?;
146        let differs = SymBoolExpr::eq_word_const(&mut self.cx, expr, value).not(&mut self.cx);
147        let mut constraints = state.constraints.clone();
148        constraints.push(differs);
149        if self.is_sat_with_state(state, &constraints)? { Ok(None) } else { Ok(Some(value)) }
150    }
151
152    /// Rejects symbolic integer bit widths outside the EVM word size.
153    pub(super) fn validate_symbolic_integer_bits(
154        bits: U256,
155        context: &'static str,
156    ) -> Result<(), SymbolicError> {
157        if bits <= U256::from(256) { Ok(()) } else { Err(SymbolicError::Unsupported(context)) }
158    }
159
160    pub(super) fn handle_bound_uint(
161        &mut self,
162        state: &mut PathState,
163        args_offset: usize,
164    ) -> Result<CheatcodeOutcome, SymbolicError> {
165        let value = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
166        let min = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
167        let max = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 2)?;
168
169        if let (Some(value), Some(min), Some(max)) =
170            (value.as_const(), min.as_const(), max.as_const())
171        {
172            if min >= max || value < min || value > max {
173                return Ok(CheatcodeOutcome::Failure);
174            }
175            let bounded = if value == min { max } else { min };
176            return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(&mut self.cx, bounded)]));
177        }
178
179        if let (Some(min), Some(max)) = (min.as_const(), max.as_const())
180            && min >= max
181        {
182            return Ok(CheatcodeOutcome::Failure);
183        }
184        let (Some(min_word), Some(max_word)) = (min.as_const(), max.as_const()) else {
185            return Err(SymbolicError::Unsupported("symbolic vm.bound range"));
186        };
187
188        let value_expr = value;
189        let min_value = SymExpr::constant(&mut self.cx, min_word);
190        let max_value = SymExpr::constant(&mut self.cx, max_word);
191        let min_condition =
192            SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Uge, value_expr.clone(), min_value);
193        let max_condition =
194            SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, value_expr.clone(), max_value);
195        let in_range = SymBoolExpr::and(&mut self.cx, vec![min_condition, max_condition]);
196        let (_in_range_constraints, in_range_sat) =
197            self.constraints_with_condition(state, in_range.clone())?;
198        if !in_range_sat {
199            return Ok(CheatcodeOutcome::Failure);
200        }
201        let out_of_range = in_range.not(&mut self.cx);
202        let (out_of_range_constraints, out_of_range_sat) =
203            self.constraints_with_condition(state, out_of_range)?;
204        if out_of_range_sat {
205            state.constraints = out_of_range_constraints;
206            return Ok(CheatcodeOutcome::Failure);
207        }
208
209        let bounded = state.fresh_word(&mut self.cx, "vmBoundUint");
210        let min_condition =
211            SymBoolExpr::cmp_word_const(&mut self.cx, SymCmpOp::Uge, &bounded, min_word);
212        let max_condition =
213            SymBoolExpr::cmp_word_const(&mut self.cx, SymCmpOp::Ule, &bounded, max_word);
214        state.constraints.push(min_condition);
215        state.constraints.push(max_condition);
216        let same_value = SymBoolExpr::eq(&mut self.cx, bounded.clone(), value_expr);
217        state.constraints.push(same_value.not(&mut self.cx));
218        Ok(CheatcodeOutcome::Continue(vec![bounded]))
219    }
220
221    pub(super) fn handle_bound_int(
222        &mut self,
223        state: &mut PathState,
224        args_offset: usize,
225    ) -> Result<CheatcodeOutcome, SymbolicError> {
226        let value = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
227        let min = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
228        let max = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 2)?;
229
230        if let (Some(value), Some(min), Some(max)) =
231            (value.as_const(), min.as_const(), max.as_const())
232        {
233            if !i256_cmp(&min, &max).is_lt()
234                || i256_cmp(&value, &min).is_lt()
235                || i256_cmp(&value, &max).is_gt()
236            {
237                return Ok(CheatcodeOutcome::Failure);
238            }
239            let bounded = if value == min { max } else { min };
240            return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(&mut self.cx, bounded)]));
241        }
242
243        if let (Some(min), Some(max)) = (min.as_const(), max.as_const())
244            && !i256_cmp(&min, &max).is_lt()
245        {
246            return Ok(CheatcodeOutcome::Failure);
247        }
248        let (Some(min_word), Some(max_word)) = (min.as_const(), max.as_const()) else {
249            return Err(SymbolicError::Unsupported("symbolic vm.bound range"));
250        };
251
252        let value_expr = value;
253        let min_value = SymExpr::constant(&mut self.cx, min_word);
254        let max_value = SymExpr::constant(&mut self.cx, max_word);
255        let below_min =
256            SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Slt, value_expr.clone(), min_value);
257        let above_max =
258            SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Sgt, value_expr.clone(), max_value);
259        let below_min = below_min.not(&mut self.cx);
260        let above_max = above_max.not(&mut self.cx);
261        let in_range = SymBoolExpr::and(&mut self.cx, vec![below_min, above_max]);
262        let (_in_range_constraints, in_range_sat) =
263            self.constraints_with_condition(state, in_range.clone())?;
264        if !in_range_sat {
265            return Ok(CheatcodeOutcome::Failure);
266        }
267        let out_of_range = in_range.not(&mut self.cx);
268        let (out_of_range_constraints, out_of_range_sat) =
269            self.constraints_with_condition(state, out_of_range)?;
270        if out_of_range_sat {
271            state.constraints = out_of_range_constraints;
272            return Ok(CheatcodeOutcome::Failure);
273        }
274
275        let bounded = state.fresh_word(&mut self.cx, "vmBoundInt");
276        let below_min =
277            SymBoolExpr::cmp_word_const(&mut self.cx, SymCmpOp::Slt, &bounded, min_word);
278        let above_max =
279            SymBoolExpr::cmp_word_const(&mut self.cx, SymCmpOp::Sgt, &bounded, max_word);
280        let below_min = below_min.not(&mut self.cx);
281        let above_max = above_max.not(&mut self.cx);
282        state.constraints.push(below_min);
283        state.constraints.push(above_max);
284        let same_value = SymBoolExpr::eq(&mut self.cx, bounded.clone(), value_expr);
285        state.constraints.push(same_value.not(&mut self.cx));
286        Ok(CheatcodeOutcome::Continue(vec![bounded]))
287    }
288}
foundry_evm_symbolic/executor/constraints.rs

foundry_evm_symbolic/executor/
constraints.rs
