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

foundry_evm_symbolic/executor/
invariant.rs
