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

foundry_evm_symbolic/executor/
invariant.rs
