foundry_evm_symbolic/executor/
constraints.rs

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

foundry_evm_symbolic/executor/
constraints.rs
