foundry_evm_symbolic/executor/
invariant.rs

1use super::*;
2
3fn record_candidate_limitation(
4    limitation: &mut Option<SymbolicInvariantSearchLimitation>,
5    error: SymbolicError,
6) -> bool {
7    let search_exhausted = matches!(
8        error,
9        SymbolicError::Timeout(_) | SymbolicError::Solver(_) | SymbolicError::SolverQueryLimit(_)
10    );
11    if search_exhausted {
12        *limitation = Some(error.into());
13    } else {
14        limitation.get_or_insert_with(|| error.into());
15    }
16    search_exhausted
17}
18
19impl SymbolicExecutor {
20    #[expect(clippy::too_many_arguments)]
21    pub(super) fn execute_invariant_check(
22        &mut self,
23        executor: &ExecutorView<'_>,
24        state: &PathState,
25        invariant_address: Address,
26        sender: Address,
27        invariant: &Function,
28        after_invariant: Option<&Function>,
29        completed_paths: &mut usize,
30    ) -> Result<Vec<InvariantCheckOutcome>, SymbolicError> {
31        let mut call = self.prepare_invariant_call(
32            executor,
33            state.clone(),
34            invariant_address,
35            sender,
36            invariant,
37        )?;
38
39        let mut checked = Vec::new();
40        while let Some(mut outcome) =
41            self.execute_sequence_call_next(executor, &mut call, completed_paths)?
42        {
43            if !matches!(outcome.status, CallStatus::Success) {
44                return Ok(vec![InvariantCheckOutcome { failed: true, state: outcome.state }]);
45            }
46
47            let Some(after_invariant) = after_invariant else {
48                checked.push(InvariantCheckOutcome { failed: false, state: outcome.state });
49                continue;
50            };
51
52            // Concrete invariant checks do not commit predicate state before invoking
53            // `afterInvariant`. Retain the predicate's path state while restoring the unchanged
54            // post-handler world.
55            let mut after_state = state.clone();
56            after_state.take_noncommitting_check_state(&mut outcome.state);
57            let mut after_call = self.prepare_invariant_call(
58                executor,
59                after_state,
60                invariant_address,
61                sender,
62                after_invariant,
63            )?;
64            while let Some(after_outcome) =
65                self.execute_sequence_call_next(executor, &mut after_call, completed_paths)?
66            {
67                let failed = !matches!(after_outcome.status, CallStatus::Success);
68                let checked_outcome = InvariantCheckOutcome { failed, state: after_outcome.state };
69                if failed {
70                    return Ok(vec![checked_outcome]);
71                }
72                checked.push(checked_outcome);
73            }
74        }
75        Ok(checked)
76    }
77
78    fn prepare_invariant_call(
79        &mut self,
80        executor: &ExecutorView<'_>,
81        mut state: PathState,
82        invariant_address: Address,
83        sender: Address,
84        invariant: &Function,
85    ) -> Result<SequenceCall, SymbolicError> {
86        state.invariant_predicate = true;
87        let calldata = SymbolicCalldata::selector_only(&mut self.cx, invariant)?;
88        let call_data = calldata.call_data(&mut self.cx);
89        let constraints = calldata.into_constraints();
90        self.prepare_sequence_call(
91            executor,
92            state,
93            invariant_address,
94            sender,
95            invariant,
96            call_data,
97            constraints,
98        )
99    }
100
101    pub(super) fn search_invariant_candidates_inner(
102        &mut self,
103        input: &SymbolicInvariantCandidateInput<'_>,
104        candidates: &mut Vec<SymbolicInvariantCandidate>,
105        limitation: &mut Option<SymbolicInvariantSearchLimitation>,
106    ) -> Result<(), SymbolicError> {
107        if input.invariants.is_empty() {
108            return Err(SymbolicError::Unsupported("symbolic invariant has no predicates"));
109        }
110        let mut completed_paths = 0;
111
112        let mut initial_state = PathState::empty(
113            &mut self.cx,
114            input.invariant_address,
115            input.handler_sender,
116            input.ffi_enabled,
117        );
118        initial_state.apply_executor_env(&mut self.cx, &input.executor);
119        initial_state.world.set_storage_layout(self.config.storage_layout);
120
121        let calldatas = SymbolicCalldata::variants_with_prefix(
122            &input.target.function,
123            &self.config,
124            &mut self.cx,
125            "frontier_handler",
126        )?;
127        'variants: for calldata in calldatas {
128            self.check_timeout()?;
129            let step = SequenceStepTemplate {
130                sender: input.handler_sender,
131                address: input.target.address,
132                contract_name: input.target.contract_name.clone(),
133                function: input.target.function.clone(),
134                calldata,
135            };
136            let call_data = step.calldata.call_data(&mut self.cx);
137            let constraints = step.calldata.constraints().to_vec();
138            let mut handler = match self.prepare_sequence_call(
139                &input.executor,
140                initial_state.clone(),
141                input.target.address,
142                input.handler_sender,
143                &input.target.function,
144                call_data,
145                constraints,
146            ) {
147                Ok(call) => call,
148                Err(error) => {
149                    if record_candidate_limitation(limitation, error) {
150                        break;
151                    }
152                    continue;
153                }
154            };
155            let mut stop_after_handler = false;
156            loop {
157                let outcome = match self.execute_sequence_call_next(
158                    &input.executor,
159                    &mut handler,
160                    &mut completed_paths,
161                ) {
162                    Ok(Some(outcome)) => outcome,
163                    Ok(None) => break,
164                    Err(error) => {
165                        stop_after_handler = record_candidate_limitation(limitation, error);
166                        break;
167                    }
168                };
169                if !matches!(outcome.status, CallStatus::Success) {
170                    continue;
171                }
172                let handler_state = outcome.state;
173                for (invariant_idx, invariant) in input.invariants.iter().enumerate() {
174                    self.check_timeout()?;
175                    let mut predicate = match self.prepare_invariant_call(
176                        &input.executor,
177                        handler_state.clone(),
178                        input.invariant_address,
179                        CALLER,
180                        invariant,
181                    ) {
182                        Ok(call) => call,
183                        Err(error) => {
184                            if record_candidate_limitation(limitation, error) {
185                                break 'variants;
186                            }
187                            continue;
188                        }
189                    };
190                    let mut stop_after_predicate = false;
191                    let mut candidate_states = Vec::new();
192                    loop {
193                        let mut predicate_outcome = match self.execute_sequence_call_next(
194                            &input.executor,
195                            &mut predicate,
196                            &mut completed_paths,
197                        ) {
198                            Ok(Some(outcome)) => outcome,
199                            Ok(None) => break,
200                            Err(error) => {
201                                stop_after_predicate =
202                                    record_candidate_limitation(limitation, error);
203                                break;
204                            }
205                        };
206                        if !matches!(predicate_outcome.status, CallStatus::Success) {
207                            candidate_states.push(predicate_outcome.state);
208                            continue;
209                        }
210                        let Some(after_invariant) = input.after_invariant else {
211                            continue;
212                        };
213
214                        // Concrete invariant checks do not commit predicate state before invoking
215                        // `afterInvariant`. Retain the predicate's path state while restoring the
216                        // unchanged post-handler world.
217                        let mut after_state = handler_state.clone();
218                        after_state.take_noncommitting_check_state(&mut predicate_outcome.state);
219                        let mut after = match self.prepare_invariant_call(
220                            &input.executor,
221                            after_state,
222                            input.invariant_address,
223                            CALLER,
224                            after_invariant,
225                        ) {
226                            Ok(call) => call,
227                            Err(error) => {
228                                if record_candidate_limitation(limitation, error) {
229                                    stop_after_predicate = true;
230                                    break;
231                                }
232                                continue;
233                            }
234                        };
235                        loop {
236                            match self.execute_sequence_call_next(
237                                &input.executor,
238                                &mut after,
239                                &mut completed_paths,
240                            ) {
241                                Ok(Some(outcome)) => {
242                                    if !matches!(outcome.status, CallStatus::Success) {
243                                        candidate_states.push(outcome.state);
244                                    }
245                                }
246                                Ok(None) => break,
247                                Err(error) => {
248                                    if record_candidate_limitation(limitation, error) {
249                                        stop_after_predicate = true;
250                                    }
251                                    break;
252                                }
253                            }
254                        }
255                        if stop_after_predicate {
256                            break;
257                        }
258                    }
259
260                    for state in candidate_states {
261                        match self.materialize_sequence(std::slice::from_ref(&step), &state) {
262                            Ok((mut sequence, storage)) => {
263                                let step =
264                                    sequence.pop().expect("one handler template produces one step");
265                                candidates.push(SymbolicInvariantCandidate {
266                                    invariant_idx,
267                                    step,
268                                    storage,
269                                });
270                            }
271                            Err(error) => {
272                                if record_candidate_limitation(limitation, error) {
273                                    break 'variants;
274                                }
275                            }
276                        }
277                    }
278                    if stop_after_predicate {
279                        break 'variants;
280                    }
281                }
282            }
283            if stop_after_handler {
284                break;
285            }
286        }
287
288        Ok(())
289    }
290
291    #[expect(clippy::too_many_arguments)]
292    pub(super) fn prepare_sequence_call(
293        &mut self,
294        executor: &ExecutorView<'_>,
295        mut state: PathState,
296        target: Address,
297        sender: Address,
298        _function: &Function,
299        calldata: SymCalldata,
300        constraints: Vec<SymBoolExpr>,
301    ) -> Result<SequenceCall, SymbolicError> {
302        state.world.clear_transaction_scoped_state();
303        state.mapping_hook_keccak_preimages.clear();
304        let code = state.world.extcode(&mut self.cx, executor, target)?;
305        state.call_depth = 0;
306        state.origin = sender;
307        state.origin_word = SymExpr::constant(&mut self.cx, address_word(sender));
308        let callvalue = SymExpr::zero(&mut self.cx);
309        state.frame =
310            CallFrame::new(&mut self.cx, target, target, sender, callvalue, false, calldata);
311        state.constraints.extend(constraints);
312        Ok(SequenceCall {
313            code,
314            worklist: VecDeque::from([state]),
315            deferred_worklist: VecDeque::new(),
316        })
317    }
318
319    pub(super) fn execute_sequence_call_next(
320        &mut self,
321        executor: &ExecutorView<'_>,
322        call: &mut SequenceCall,
323        completed_paths: &mut usize,
324    ) -> Result<Option<CallOutcome>, SymbolicError> {
325        if call.worklist.is_empty() && call.deferred_worklist.is_empty() {
326            return Ok(None);
327        }
328        let mut outcomes = self.execute_call_path_batch(
329            executor,
330            &call.code,
331            &mut call.worklist,
332            &mut call.deferred_worklist,
333            completed_paths,
334            CallPathKind::Sequence,
335        )?;
336        debug_assert!(outcomes.len() <= 1);
337        Ok(outcomes.pop())
338    }
339
340    pub(super) fn materialize_sequence(
341        &mut self,
342        steps: &[SequenceStepTemplate],
343        state: &PathState,
344    ) -> Result<(Vec<SymbolicInvariantStep>, Vec<SymbolicStorageAssignment>), SymbolicError> {
345        let replayable_storage = state.world.replay_storage_symbols();
346        let model = self.solver.model_with_replayable_storage(
347            &mut self.cx,
348            &state.constraints,
349            &replayable_storage,
350        )?;
351        let sequence = steps
352            .iter()
353            .map(|step| {
354                let args = step.calldata.model_to_args(&mut self.cx, &model)?;
355                let calldata = Bytes::from(step.function.abi_encode_input(&args)?);
356                Ok(SymbolicInvariantStep {
357                    sender: step.sender,
358                    address: step.address,
359                    contract_name: step.contract_name.clone(),
360                    function_name: step.function.name.clone(),
361                    signature: step.function.signature(),
362                    args,
363                    calldata,
364                })
365            })
366            .collect::<Result<Vec<_>, SymbolicError>>()?;
367        let storage = state.world.replay_storage_assignments(&model)?;
368        Ok((sequence, storage))
369    }
370}
foundry_evm_symbolic/executor/invariant.rs

foundry_evm_symbolic/executor/
invariant.rs
