Skip to main content

foundry_evm_symbolic/executor/
cheatcodes.rs

1use foundry_cheatcodes_spec::Vm::*;
2
3use super::*;
4
5impl SymbolicExecutor {
6    pub(super) fn handle_assertion(
7        &mut self,
8        state: &mut PathState,
9        pass: SymBoolExpr,
10    ) -> Result<CheatcodeOutcome, SymbolicError> {
11        let fail = pass.clone().not(&mut self.cx);
12        match fail.as_const() {
13            Some(true) => return Ok(CheatcodeOutcome::Failure),
14            Some(false) => return Ok(CheatcodeOutcome::Continue(Vec::new())),
15            None => {}
16        }
17
18        let mut fail_constraints = state.constraints.clone();
19        fail_constraints.push(fail);
20        if self.solver.is_sat(&mut self.cx, &fail_constraints)? {
21            state.constraints = fail_constraints;
22            return Ok(CheatcodeOutcome::Failure);
23        }
24
25        state.constraints.push(pass);
26        Ok(CheatcodeOutcome::Continue(Vec::new()))
27    }
28
29    pub(super) fn set_expected_revert(
30        &mut self,
31        state: &mut PathState,
32        data: ExpectedRevertData,
33        reverter: Option<SymExpr>,
34        remaining: u64,
35    ) -> CheatcodeOutcome {
36        state.expected_revert = Some(ExpectedRevert::new(data, reverter, remaining));
37        CheatcodeOutcome::Continue(Vec::new())
38    }
39
40    pub(super) fn set_expected_emit(
41        &mut self,
42        state: &mut PathState,
43        checks: ExpectedEmitChecks,
44        emitter: Option<SymExpr>,
45        remaining: u64,
46    ) -> CheatcodeOutcome {
47        state.expected_emit = Some(ExpectedEmit::new(checks, emitter, remaining));
48        CheatcodeOutcome::Continue(Vec::new())
49    }
50
51    #[expect(clippy::too_many_arguments)]
52    pub(super) fn set_expected_call(
53        &mut self,
54        state: &mut PathState,
55        callee: SymExpr,
56        value: Option<U256>,
57        gas: Option<u64>,
58        min_gas: Option<u64>,
59        data: SymBytes,
60        count: Option<u64>,
61    ) -> CheatcodeOutcome {
62        state.expected_calls.push(ExpectedCall::new(callee, value, gas, min_gas, data, count));
63        CheatcodeOutcome::Continue(Vec::new())
64    }
65
66    pub(super) fn set_expected_create(
67        &mut self,
68        state: &mut PathState,
69        bytecode: Vec<u8>,
70        deployer: SymExpr,
71        kind: CreateKind,
72    ) -> CheatcodeOutcome {
73        state.expected_creates.push(ExpectedCreate::new(bytecode, deployer, kind));
74        CheatcodeOutcome::Continue(Vec::new())
75    }
76
77    #[expect(clippy::too_many_arguments)]
78    pub(super) fn deploy_code_cheatcode_if_needed<FEN: FoundryEvmNetwork>(
79        &mut self,
80        executor: &Executor<FEN>,
81        state: &mut PathState,
82        worklist: &mut VecDeque<PathState>,
83        completed_paths: &mut usize,
84        selector: [u8; 4],
85        in_offset: usize,
86        out_offset: SymExpr,
87        out_size: &BoundedCopySize,
88    ) -> Result<Option<StepOutcome>, SymbolicError> {
89        let args_offset = in_offset + 4;
90        let (artifact, constructor_args) = if selector == deployCode_0Call::SELECTOR {
91            let artifact = read_abi_string_arg(
92                &mut self.cx,
93                &state.memory,
94                args_offset,
95                0,
96                "symbolic vm.deployCode",
97            )?;
98            (artifact, Vec::new())
99        } else if selector == deployCode_1Call::SELECTOR {
100            let artifact = read_abi_string_arg(
101                &mut self.cx,
102                &state.memory,
103                args_offset,
104                0,
105                "symbolic vm.deployCode",
106            )?;
107            let args = read_abi_dynamic_bytes_arg(
108                &mut self.cx,
109                &state.memory,
110                args_offset,
111                1,
112                "symbolic vm.deployCode args",
113            )?;
114            (artifact, args)
115        } else {
116            return Ok(None);
117        };
118
119        self.deploy_code_cheatcode_call(
120            executor,
121            state,
122            worklist,
123            completed_paths,
124            artifact,
125            constructor_args,
126            out_offset,
127            out_size,
128        )
129        .map(Some)
130    }
131
132    #[expect(clippy::too_many_arguments)]
133    pub(super) fn deploy_code_cheatcode_call<FEN: FoundryEvmNetwork>(
134        &mut self,
135        executor: &Executor<FEN>,
136        state: &mut PathState,
137        worklist: &mut VecDeque<PathState>,
138        completed_paths: &mut usize,
139        artifact: String,
140        constructor_args: Vec<u8>,
141        out_offset: SymExpr,
142        out_size: &BoundedCopySize,
143    ) -> Result<StepOutcome, SymbolicError> {
144        if state.is_static {
145            state.return_data = SymReturnData::empty(&mut self.cx);
146            return Ok(StepOutcome::Revert);
147        }
148
149        let mut initcode = artifact_code(&artifact, false)?;
150        initcode.extend_from_slice(&constructor_args);
151        let initcode = SymCode::concrete(&mut self.cx, initcode);
152
153        let nonce = state.world.nonce(executor, state.address)?;
154        let created = state.address.create(nonce);
155        let created_word = SymExpr::constant(&mut self.cx, address_word(created));
156
157        let mut failure_world = state.world.clone();
158        failure_world.increment_nonce(executor, state.address)?;
159        if failure_world.has_code_or_nonce(&mut self.cx, executor, created)? {
160            state.world = failure_world;
161            let zero = SymExpr::zero(&mut self.cx);
162            let return_data = SymReturnData::from_words(&mut self.cx, vec![zero]);
163            complete_cheatcode_call(&mut self.cx, state, out_offset, out_size, return_data)?;
164            return Ok(StepOutcome::Continue);
165        }
166
167        let zero = SymExpr::zero(&mut self.cx);
168        let calldata = SymBytes::empty(&mut self.cx);
169        let calldata = SymCalldata::from_bytes(&mut self.cx, calldata);
170        let mut frame = CallFrame::new(
171            &mut self.cx,
172            created,
173            created,
174            created,
175            state.address,
176            zero,
177            false,
178            calldata,
179        );
180        frame.address_word = created_word.clone();
181        frame.caller_word = state.address_word.clone();
182        let mut child = state.child(frame);
183        let pending_expected_creates = std::mem::take(&mut child.expected_creates);
184        child.world = failure_world.clone();
185        child.world.mark_current_transaction_created(created);
186        child.world.set_nonce(created, 1);
187        child.expected_revert = None;
188        child.assume_no_revert_next_call = None;
189
190        let outcomes = self.execute_external_call(executor, child, &initcode, completed_paths)?;
191        let Some((first, rest)) = outcomes.split_first() else {
192            return Ok(StepOutcome::AssumeRejected);
193        };
194
195        let mut parents = VecDeque::with_capacity(outcomes.len());
196        for outcome in std::iter::once(first).chain(rest.iter()) {
197            let mut parent = state.clone();
198            parent.constraints = outcome.state.constraints.clone();
199            parent.next_symbol = outcome.state.next_symbol;
200            parent.inherit_branch_target_progress(&outcome.state);
201
202            if let Some(assumption) = parent.assume_no_revert_next_call.take()
203                && matches!(outcome.status, TopLevelCallStatus::Revert)
204                && self.assume_no_revert_rejects(
205                    &mut parent,
206                    &assumption,
207                    created,
208                    &outcome.return_data,
209                )?
210            {
211                continue;
212            }
213
214            if let Some(mut expected) = parent.expected_revert.clone() {
215                match outcome.status {
216                    TopLevelCallStatus::Success => {
217                        *state = parent;
218                        return Ok(StepOutcome::Failure);
219                    }
220                    TopLevelCallStatus::Revert | TopLevelCallStatus::Failure => {
221                        if !self.expected_revert_matches(
222                            &mut parent,
223                            &expected,
224                            created,
225                            &outcome.return_data,
226                        )? {
227                            *state = parent;
228                            return Ok(StepOutcome::Failure);
229                        }
230                        if expected.consume_one() {
231                            parent.expected_revert = None;
232                        } else {
233                            parent.expected_revert = Some(expected);
234                        }
235                        parent.access_record = outcome.state.access_record.clone();
236                        parent.expected_calls = outcome.state.expected_calls.clone();
237                        parent.expected_creates = pending_expected_creates.clone();
238                        parent.call_mocks = outcome.state.call_mocks.clone();
239                        parent.function_mocks = outcome.state.function_mocks.clone();
240                        parent.world = failure_world.clone();
241                        let zero = SymExpr::zero(&mut self.cx);
242                        let return_data = SymReturnData::from_words(&mut self.cx, vec![zero]);
243                        complete_cheatcode_call(
244                            &mut self.cx,
245                            &mut parent,
246                            out_offset.clone(),
247                            out_size,
248                            return_data,
249                        )?;
250                        parents.push_back(parent);
251                        continue;
252                    }
253                }
254            }
255
256            match outcome.status {
257                TopLevelCallStatus::Success => {
258                    parent.world = outcome.state.world.clone();
259                    parent.block = outcome.state.block.clone();
260                    parent.recorded_logs = outcome.state.recorded_logs.clone();
261                    parent.access_record = outcome.state.access_record.clone();
262                    parent.expected_emit = outcome.state.expected_emit.clone();
263                    parent.expected_calls = outcome.state.expected_calls.clone();
264                    parent.expected_creates = pending_expected_creates.clone();
265                    parent.call_mocks = outcome.state.call_mocks.clone();
266                    parent.function_mocks = outcome.state.function_mocks.clone();
267                    self.observe_expected_create(
268                        &mut parent,
269                        state.address,
270                        CreateKind::Create,
271                        &outcome.return_data,
272                    )?;
273                    if !parent.world.is_destroyed(created) {
274                        parent
275                            .world
276                            .install_code(created, outcome.return_data.to_code(&mut self.cx)?);
277                        parent.world.set_nonce(created, 1);
278                    }
279                    let return_data =
280                        SymReturnData::from_words(&mut self.cx, vec![created_word.clone()]);
281                    complete_cheatcode_call(
282                        &mut self.cx,
283                        &mut parent,
284                        out_offset.clone(),
285                        out_size,
286                        return_data,
287                    )?;
288                }
289                TopLevelCallStatus::Revert => {
290                    parent.world = failure_world.clone();
291                    parent.return_data = outcome.return_data.clone();
292                    parent.copy_call_output_offset(&mut self.cx, out_offset.clone(), out_size)?;
293                    parent.stack.push(SymExpr::zero(&mut self.cx))?;
294                }
295                TopLevelCallStatus::Failure => {
296                    *state = parent;
297                    return Ok(StepOutcome::Failure);
298                }
299            }
300
301            parents.push_back(parent);
302        }
303
304        let Some(first) = self.pop_next_path(&mut parents) else {
305            return Ok(StepOutcome::AssumeRejected);
306        };
307        *state = first;
308        worklist.extend(parents);
309        Ok(StepOutcome::Continue)
310    }
311
312    pub(super) fn observe_expected_create(
313        &mut self,
314        state: &mut PathState,
315        deployer: Address,
316        kind: CreateKind,
317        runtime: &SymReturnData,
318    ) -> Result<(), SymbolicError> {
319        if state.expected_creates.is_empty() {
320            return Ok(());
321        }
322        let bytecode = runtime.read_concrete(&mut self.cx, "symbolic expected create bytecode")?;
323        let mut mismatch_constraints = None;
324        for idx in 0..state.expected_creates.len() {
325            let Some(condition) = state.expected_creates[idx].match_condition(
326                &mut self.cx,
327                deployer,
328                kind,
329                &bytecode,
330            ) else {
331                continue;
332            };
333            let (match_constraints, match_sat) =
334                self.constraints_with_condition(state, condition.clone())?;
335            let mismatch_condition = condition.not(&mut self.cx);
336            let (candidate_mismatch_constraints, mismatch_sat) =
337                self.constraints_with_condition(state, mismatch_condition)?;
338
339            if match_sat && !mismatch_sat {
340                state.constraints = match_constraints;
341                state.expected_creates.swap_remove(idx);
342                return Ok(());
343            }
344
345            if mismatch_sat {
346                mismatch_constraints.get_or_insert(candidate_mismatch_constraints);
347            }
348        }
349
350        if let Some(constraints) = mismatch_constraints {
351            state.constraints = constraints;
352        }
353        Ok(())
354    }
355
356    pub(super) fn branch_accesses_cheatcode_if_needed(
357        &mut self,
358        state: &mut PathState,
359        worklist: &mut VecDeque<PathState>,
360        selector: [u8; 4],
361        in_offset: usize,
362        out_offset: SymExpr,
363        out_size: &BoundedCopySize,
364    ) -> Result<Option<StepOutcome>, SymbolicError> {
365        if selector != accessesCall::SELECTOR {
366            return Ok(None);
367        }
368
369        let Some(record) = state.access_record.clone() else {
370            return Ok(None);
371        };
372        let target = read_abi_word_arg(&mut self.cx, &state.memory, in_offset + 4, 0)?;
373        if target.as_const().is_some() {
374            return Ok(None);
375        }
376
377        let addresses = record.addresses();
378        if addresses.is_empty() {
379            return Ok(None);
380        }
381
382        let mut branches = VecDeque::new();
383        let mut matched_conditions = Vec::new();
384        for address in addresses {
385            let condition = target.address_match_condition(&mut self.cx, address);
386            matched_conditions.push(condition.clone());
387            if let Some(constraints) = self.constraints_for_condition(state, condition)? {
388                let mut branch = state.clone();
389                branch.constraints = constraints;
390                let return_data = accesses_return_data(&mut self.cx, Some(&record), address);
391                complete_cheatcode_call(
392                    &mut self.cx,
393                    &mut branch,
394                    out_offset.clone(),
395                    out_size,
396                    return_data,
397                )?;
398                branches.push_back(branch);
399            }
400        }
401
402        let unmatched_conditions =
403            matched_conditions.into_iter().map(|condition| condition.not(&mut self.cx)).collect();
404        let unmatched_condition = SymBoolExpr::and(&mut self.cx, unmatched_conditions);
405        if let Some(constraints) = self.constraints_for_condition(state, unmatched_condition)? {
406            let mut branch = state.clone();
407            branch.constraints = constraints;
408            let return_data = accesses_return_data(&mut self.cx, Some(&record), Address::ZERO);
409            complete_cheatcode_call(&mut self.cx, &mut branch, out_offset, out_size, return_data)?;
410            branches.push_back(branch);
411        }
412
413        let Some(first_branch) = self.pop_next_path(&mut branches) else {
414            return Ok(Some(StepOutcome::AssumeRejected));
415        };
416        *state = first_branch;
417        worklist.extend(branches);
418        Ok(Some(StepOutcome::Continue))
419    }
420
421    pub(super) fn accesses_return_data_for_target(
422        &mut self,
423        state: &mut PathState,
424        target: SymExpr,
425    ) -> Result<SymReturnData, SymbolicError> {
426        let Some(record) = state.access_record.clone() else {
427            return Ok(accesses_return_data(&mut self.cx, None, Address::ZERO));
428        };
429
430        if let Some(target) = target.as_const() {
431            return Ok(accesses_return_data(&mut self.cx, Some(&record), word_to_address(target)));
432        }
433
434        let addresses = record.addresses();
435        if addresses.is_empty() {
436            return Ok(accesses_return_data(&mut self.cx, Some(&record), Address::ZERO));
437        }
438
439        for address in addresses {
440            let condition = target.address_match_condition(&mut self.cx, address);
441            let (match_constraints, match_sat) =
442                self.constraints_with_condition(state, condition.clone())?;
443            let mismatch_condition = condition.not(&mut self.cx);
444            let (_, mismatch_sat) = self.constraints_with_condition(state, mismatch_condition)?;
445
446            match (match_sat, mismatch_sat) {
447                (true, false) => {
448                    state.constraints = match_constraints;
449                    return Ok(accesses_return_data(&mut self.cx, Some(&record), address));
450                }
451                (true, true) => {
452                    return Err(SymbolicError::Unsupported("symbolic vm.accesses address"));
453                }
454                (false, _) => {}
455            }
456        }
457
458        Ok(accesses_return_data(&mut self.cx, Some(&record), Address::ZERO))
459    }
460
461    pub(super) fn add_call_mock(
462        &mut self,
463        state: &mut PathState,
464        callee: SymExpr,
465        value: Option<U256>,
466        data: SymBytes,
467        returns: Vec<SymReturnData>,
468        reverts: bool,
469    ) -> CheatcodeOutcome {
470        state.call_mocks.push(CallMock::new(callee, value, data, returns, reverts));
471        CheatcodeOutcome::Continue(Vec::new())
472    }
473
474    pub(super) fn set_function_mock(
475        &mut self,
476        state: &mut PathState,
477        callee: SymExpr,
478        target: Address,
479        data: SymBytes,
480    ) -> CheatcodeOutcome {
481        if let Some(mock) = state
482            .function_mocks
483            .iter_mut()
484            .find(|mock| mock.matches_definition(&mut self.cx, &callee, &data))
485        {
486            mock.set_target(target);
487        } else {
488            state.function_mocks.push(FunctionMock::new(callee, target, data));
489        }
490        CheatcodeOutcome::Continue(Vec::new())
491    }
492
493    pub(super) fn handle_foundry_cheatcode<FEN: FoundryEvmNetwork>(
494        &mut self,
495        executor: &Executor<FEN>,
496        state: &mut PathState,
497        selector: [u8; 4],
498        in_offset: usize,
499        in_size: usize,
500    ) -> Result<CheatcodeOutcome, SymbolicError> {
501        let args_offset = in_offset + 4;
502        match selector {
503            assumeCall::SELECTOR => {
504                return self.handle_assume(state, in_offset + 4);
505            }
506            assumeNoRevert_0Call::SELECTOR => {
507                if state.assume_no_revert_next_call.is_some() {
508                    return Err(SymbolicError::Unsupported("symbolic vm.assumeNoRevert overlap"));
509                }
510                state.assume_no_revert_next_call = Some(AssumeNoRevert::Any);
511                return Ok(CheatcodeOutcome::Continue(Vec::new()));
512            }
513            assumeNoRevert_1Call::SELECTOR => {
514                if state.assume_no_revert_next_call.is_some() {
515                    return Err(SymbolicError::Unsupported("symbolic vm.assumeNoRevert overlap"));
516                }
517                let mut values = decode_cheatcode_args(
518                    &mut self.cx,
519                    state,
520                    in_offset,
521                    in_size,
522                    vec![DynSolType::Tuple(vec![
523                        DynSolType::Address,
524                        DynSolType::Bool,
525                        DynSolType::Bytes,
526                    ])],
527                )?;
528                let value = values
529                    .pop()
530                    .ok_or(SymbolicError::Unsupported("symbolic vm.assumeNoRevert decode"))?;
531                state.assume_no_revert_next_call =
532                    Some(AssumeNoRevert::Filtered(vec![dyn_potential_revert(
533                        &mut self.cx,
534                        &value,
535                    )?]));
536                return Ok(CheatcodeOutcome::Continue(Vec::new()));
537            }
538            assumeNoRevert_2Call::SELECTOR => {
539                if state.assume_no_revert_next_call.is_some() {
540                    return Err(SymbolicError::Unsupported("symbolic vm.assumeNoRevert overlap"));
541                }
542                let mut values = decode_cheatcode_args(
543                    &mut self.cx,
544                    state,
545                    in_offset,
546                    in_size,
547                    vec![DynSolType::Array(Box::new(DynSolType::Tuple(vec![
548                        DynSolType::Address,
549                        DynSolType::Bool,
550                        DynSolType::Bytes,
551                    ])))],
552                )?;
553                let value = values
554                    .pop()
555                    .ok_or(SymbolicError::Unsupported("symbolic vm.assumeNoRevert decode"))?;
556                state.assume_no_revert_next_call =
557                    Some(AssumeNoRevert::Filtered(dyn_potential_reverts(&mut self.cx, &value)?));
558                return Ok(CheatcodeOutcome::Continue(Vec::new()));
559            }
560            skip_0Call::SELECTOR | skip_1Call::SELECTOR => {
561                return self.handle_skip(state, in_offset + 4);
562            }
563            recordLogsCall::SELECTOR => {
564                state.recorded_logs = Some(Vec::new());
565                return Ok(CheatcodeOutcome::Continue(Vec::new()));
566            }
567            recordCall::SELECTOR => {
568                state.access_record = Some(AccessRecord::default());
569                return Ok(CheatcodeOutcome::Continue(Vec::new()));
570            }
571            stopRecordCall::SELECTOR => {
572                state.access_record = None;
573                return Ok(CheatcodeOutcome::Continue(Vec::new()));
574            }
575            accessesCall::SELECTOR => {
576                let target = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
577                return Ok(CheatcodeOutcome::ContinueData(
578                    self.accesses_return_data_for_target(state, target)?,
579                ));
580            }
581            getRecordedLogsCall::SELECTOR => {
582                let logs = state.recorded_logs.replace(Vec::new()).unwrap_or_default();
583                return Ok(CheatcodeOutcome::ContinueData(recorded_logs_return_data(
584                    &mut self.cx,
585                    logs,
586                )));
587            }
588            getRecordedLogsJsonCall::SELECTOR => {
589                let logs = state.recorded_logs.replace(Vec::new()).unwrap_or_default();
590                return Ok(CheatcodeOutcome::ContinueData(recorded_logs_json_return_data(
591                    &mut self.cx,
592                    logs,
593                )?));
594            }
595            expectRevert_0Call::SELECTOR => {
596                return Ok(self.set_expected_revert(state, ExpectedRevertData::Any, None, 1));
597            }
598            expectRevert_1Call::SELECTOR => {
599                let selector =
600                    read_abi_bytes4_words_arg(&mut self.cx, &state.memory, args_offset, 0);
601                let data = SymBytes::exprs(&mut self.cx, selector);
602                return Ok(self.set_expected_revert(
603                    state,
604                    ExpectedRevertData::prefix(data),
605                    None,
606                    1,
607                ));
608            }
609            expectRevert_2Call::SELECTOR => {
610                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
611                    &mut self.cx,
612                    state,
613                    args_offset,
614                    0,
615                    self.config.max_calldata_bytes as usize,
616                    "symbolic vm.expectRevert",
617                )?;
618                let data = SymBytes::exprs(&mut self.cx, data);
619                return Ok(self.set_expected_revert(
620                    state,
621                    ExpectedRevertData::exact(data),
622                    None,
623                    1,
624                ));
625            }
626            expectRevert_3Call::SELECTOR => {
627                let reverter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
628                return Ok(self.set_expected_revert(
629                    state,
630                    ExpectedRevertData::Any,
631                    Some(reverter),
632                    1,
633                ));
634            }
635            expectRevert_4Call::SELECTOR => {
636                let selector =
637                    read_abi_bytes4_words_arg(&mut self.cx, &state.memory, args_offset, 0);
638                let reverter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
639                let data = SymBytes::exprs(&mut self.cx, selector);
640                return Ok(self.set_expected_revert(
641                    state,
642                    ExpectedRevertData::prefix(data),
643                    Some(reverter),
644                    1,
645                ));
646            }
647            expectRevert_5Call::SELECTOR => {
648                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
649                    &mut self.cx,
650                    state,
651                    args_offset,
652                    0,
653                    self.config.max_calldata_bytes as usize,
654                    "symbolic vm.expectRevert",
655                )?;
656                let reverter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
657                let data = SymBytes::exprs(&mut self.cx, data);
658                return Ok(self.set_expected_revert(
659                    state,
660                    ExpectedRevertData::exact(data),
661                    Some(reverter),
662                    1,
663                ));
664            }
665            expectRevert_6Call::SELECTOR => {
666                let count = read_abi_u64_arg(
667                    &mut self.cx,
668                    &state.memory,
669                    args_offset,
670                    0,
671                    "symbolic vm.expectRevert",
672                )?;
673                return Ok(self.set_expected_revert(state, ExpectedRevertData::Any, None, count));
674            }
675            expectRevert_7Call::SELECTOR => {
676                let selector =
677                    read_abi_bytes4_words_arg(&mut self.cx, &state.memory, args_offset, 0);
678                let count = read_abi_u64_arg(
679                    &mut self.cx,
680                    &state.memory,
681                    args_offset,
682                    1,
683                    "symbolic vm.expectRevert",
684                )?;
685                let data = SymBytes::exprs(&mut self.cx, selector);
686                return Ok(self.set_expected_revert(
687                    state,
688                    ExpectedRevertData::prefix(data),
689                    None,
690                    count,
691                ));
692            }
693            expectRevert_8Call::SELECTOR => {
694                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
695                    &mut self.cx,
696                    state,
697                    args_offset,
698                    0,
699                    self.config.max_calldata_bytes as usize,
700                    "symbolic vm.expectRevert",
701                )?;
702                let count = read_abi_u64_arg(
703                    &mut self.cx,
704                    &state.memory,
705                    args_offset,
706                    1,
707                    "symbolic vm.expectRevert",
708                )?;
709                let data = SymBytes::exprs(&mut self.cx, data);
710                return Ok(self.set_expected_revert(
711                    state,
712                    ExpectedRevertData::exact(data),
713                    None,
714                    count,
715                ));
716            }
717            expectRevert_9Call::SELECTOR => {
718                let reverter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
719                let count = read_abi_u64_arg(
720                    &mut self.cx,
721                    &state.memory,
722                    args_offset,
723                    1,
724                    "symbolic vm.expectRevert",
725                )?;
726                return Ok(self.set_expected_revert(
727                    state,
728                    ExpectedRevertData::Any,
729                    Some(reverter),
730                    count,
731                ));
732            }
733            expectRevert_10Call::SELECTOR => {
734                let selector =
735                    read_abi_bytes4_words_arg(&mut self.cx, &state.memory, args_offset, 0);
736                let reverter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
737                let count = read_abi_u64_arg(
738                    &mut self.cx,
739                    &state.memory,
740                    args_offset,
741                    2,
742                    "symbolic vm.expectRevert",
743                )?;
744                let data = SymBytes::exprs(&mut self.cx, selector);
745                return Ok(self.set_expected_revert(
746                    state,
747                    ExpectedRevertData::prefix(data),
748                    Some(reverter),
749                    count,
750                ));
751            }
752            expectRevert_11Call::SELECTOR => {
753                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
754                    &mut self.cx,
755                    state,
756                    args_offset,
757                    0,
758                    self.config.max_calldata_bytes as usize,
759                    "symbolic vm.expectRevert",
760                )?;
761                let reverter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
762                let count = read_abi_u64_arg(
763                    &mut self.cx,
764                    &state.memory,
765                    args_offset,
766                    2,
767                    "symbolic vm.expectRevert",
768                )?;
769                let data = SymBytes::exprs(&mut self.cx, data);
770                return Ok(self.set_expected_revert(
771                    state,
772                    ExpectedRevertData::exact(data),
773                    Some(reverter),
774                    count,
775                ));
776            }
777            expectPartialRevert_0Call::SELECTOR => {
778                let selector =
779                    read_abi_bytes4_words_arg(&mut self.cx, &state.memory, args_offset, 0);
780                let data = SymBytes::exprs(&mut self.cx, selector);
781                return Ok(self.set_expected_revert(
782                    state,
783                    ExpectedRevertData::prefix(data),
784                    None,
785                    1,
786                ));
787            }
788            expectPartialRevert_1Call::SELECTOR => {
789                let selector =
790                    read_abi_bytes4_words_arg(&mut self.cx, &state.memory, args_offset, 0);
791                let reverter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
792                let data = SymBytes::exprs(&mut self.cx, selector);
793                return Ok(self.set_expected_revert(
794                    state,
795                    ExpectedRevertData::prefix(data),
796                    Some(reverter),
797                    1,
798                ));
799            }
800            expectEmit_2Call::SELECTOR => {
801                return Ok(self.set_expected_emit(
802                    state,
803                    ExpectedEmitChecks::default_non_anonymous(),
804                    None,
805                    1,
806                ));
807            }
808            expectEmit_3Call::SELECTOR => {
809                let emitter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
810                return Ok(self.set_expected_emit(
811                    state,
812                    ExpectedEmitChecks::default_non_anonymous(),
813                    Some(emitter),
814                    1,
815                ));
816            }
817            expectEmit_6Call::SELECTOR => {
818                let count = read_abi_u64_arg(
819                    &mut self.cx,
820                    &state.memory,
821                    args_offset,
822                    0,
823                    "symbolic vm.expectEmit",
824                )?;
825                return Ok(self.set_expected_emit(
826                    state,
827                    ExpectedEmitChecks::default_non_anonymous(),
828                    None,
829                    count,
830                ));
831            }
832            expectEmit_7Call::SELECTOR => {
833                let emitter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
834                let count = read_abi_u64_arg(
835                    &mut self.cx,
836                    &state.memory,
837                    args_offset,
838                    1,
839                    "symbolic vm.expectEmit",
840                )?;
841                return Ok(self.set_expected_emit(
842                    state,
843                    ExpectedEmitChecks::default_non_anonymous(),
844                    Some(emitter),
845                    count,
846                ));
847            }
848            expectEmit_0Call::SELECTOR => {
849                let checks = ExpectedEmitChecks::from_non_anonymous_args(
850                    &mut self.cx,
851                    &state.memory,
852                    args_offset,
853                )?;
854                return Ok(self.set_expected_emit(state, checks, None, 1));
855            }
856            expectEmit_1Call::SELECTOR => {
857                let checks = ExpectedEmitChecks::from_non_anonymous_args(
858                    &mut self.cx,
859                    &state.memory,
860                    args_offset,
861                )?;
862                let emitter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 4)?;
863                return Ok(self.set_expected_emit(state, checks, Some(emitter), 1));
864            }
865            expectEmit_4Call::SELECTOR => {
866                let checks = ExpectedEmitChecks::from_non_anonymous_args(
867                    &mut self.cx,
868                    &state.memory,
869                    args_offset,
870                )?;
871                let count = read_abi_u64_arg(
872                    &mut self.cx,
873                    &state.memory,
874                    args_offset,
875                    4,
876                    "symbolic vm.expectEmit",
877                )?;
878                return Ok(self.set_expected_emit(state, checks, None, count));
879            }
880            expectEmit_5Call::SELECTOR => {
881                let checks = ExpectedEmitChecks::from_non_anonymous_args(
882                    &mut self.cx,
883                    &state.memory,
884                    args_offset,
885                )?;
886                let emitter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 4)?;
887                let count = read_abi_u64_arg(
888                    &mut self.cx,
889                    &state.memory,
890                    args_offset,
891                    5,
892                    "symbolic vm.expectEmit",
893                )?;
894                return Ok(self.set_expected_emit(state, checks, Some(emitter), count));
895            }
896            expectEmitAnonymous_2Call::SELECTOR => {
897                return Ok(self.set_expected_emit(
898                    state,
899                    ExpectedEmitChecks::default_anonymous(),
900                    None,
901                    1,
902                ));
903            }
904            expectEmitAnonymous_3Call::SELECTOR => {
905                let emitter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
906                return Ok(self.set_expected_emit(
907                    state,
908                    ExpectedEmitChecks::default_anonymous(),
909                    Some(emitter),
910                    1,
911                ));
912            }
913            expectEmitAnonymous_0Call::SELECTOR => {
914                let checks = ExpectedEmitChecks::from_anonymous_args(
915                    &mut self.cx,
916                    &state.memory,
917                    args_offset,
918                )?;
919                return Ok(self.set_expected_emit(state, checks, None, 1));
920            }
921            expectEmitAnonymous_1Call::SELECTOR => {
922                let checks = ExpectedEmitChecks::from_anonymous_args(
923                    &mut self.cx,
924                    &state.memory,
925                    args_offset,
926                )?;
927                let emitter = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 5)?;
928                return Ok(self.set_expected_emit(state, checks, Some(emitter), 1));
929            }
930            expectCall_0Call::SELECTOR => {
931                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
932                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
933                    &mut self.cx,
934                    state,
935                    args_offset,
936                    1,
937                    self.config.max_calldata_bytes as usize,
938                    "symbolic vm.expectCall",
939                )?;
940                let data = SymBytes::exprs(&mut self.cx, data);
941                return Ok(self.set_expected_call(state, callee, None, None, None, data, None));
942            }
943            expectCall_1Call::SELECTOR => {
944                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
945                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
946                    &mut self.cx,
947                    state,
948                    args_offset,
949                    1,
950                    self.config.max_calldata_bytes as usize,
951                    "symbolic vm.expectCall",
952                )?;
953                let count = read_abi_u64_arg(
954                    &mut self.cx,
955                    &state.memory,
956                    args_offset,
957                    2,
958                    "symbolic vm.expectCall",
959                )?;
960                let data = SymBytes::exprs(&mut self.cx, data);
961                return Ok(self.set_expected_call(
962                    state,
963                    callee,
964                    None,
965                    None,
966                    None,
967                    data,
968                    Some(count),
969                ));
970            }
971            expectCall_2Call::SELECTOR => {
972                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
973                let value = read_abi_concrete_word_arg(
974                    &mut self.cx,
975                    &state.memory,
976                    args_offset,
977                    1,
978                    "symbolic vm.expectCall",
979                )?;
980                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
981                    &mut self.cx,
982                    state,
983                    args_offset,
984                    2,
985                    self.config.max_calldata_bytes as usize,
986                    "symbolic vm.expectCall",
987                )?;
988                let data = SymBytes::exprs(&mut self.cx, data);
989                return Ok(self.set_expected_call(
990                    state,
991                    callee,
992                    Some(value),
993                    None,
994                    None,
995                    data,
996                    None,
997                ));
998            }
999            expectCall_3Call::SELECTOR => {
1000                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1001                let value = read_abi_concrete_word_arg(
1002                    &mut self.cx,
1003                    &state.memory,
1004                    args_offset,
1005                    1,
1006                    "symbolic vm.expectCall",
1007                )?;
1008                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
1009                    &mut self.cx,
1010                    state,
1011                    args_offset,
1012                    2,
1013                    self.config.max_calldata_bytes as usize,
1014                    "symbolic vm.expectCall",
1015                )?;
1016                let count = read_abi_u64_arg(
1017                    &mut self.cx,
1018                    &state.memory,
1019                    args_offset,
1020                    3,
1021                    "symbolic vm.expectCall",
1022                )?;
1023                let data = SymBytes::exprs(&mut self.cx, data);
1024                return Ok(self.set_expected_call(
1025                    state,
1026                    callee,
1027                    Some(value),
1028                    None,
1029                    None,
1030                    data,
1031                    Some(count),
1032                ));
1033            }
1034            expectCall_4Call::SELECTOR => {
1035                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1036                let value = read_abi_concrete_word_arg(
1037                    &mut self.cx,
1038                    &state.memory,
1039                    args_offset,
1040                    1,
1041                    "symbolic vm.expectCall",
1042                )?;
1043                let gas = read_abi_u64_arg(
1044                    &mut self.cx,
1045                    &state.memory,
1046                    args_offset,
1047                    2,
1048                    "symbolic vm.expectCall",
1049                )?;
1050                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
1051                    &mut self.cx,
1052                    state,
1053                    args_offset,
1054                    3,
1055                    self.config.max_calldata_bytes as usize,
1056                    "symbolic vm.expectCall",
1057                )?;
1058                let data = SymBytes::exprs(&mut self.cx, data);
1059                return Ok(self.set_expected_call(
1060                    state,
1061                    callee,
1062                    Some(value),
1063                    Some(gas),
1064                    None,
1065                    data,
1066                    None,
1067                ));
1068            }
1069            expectCall_5Call::SELECTOR => {
1070                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1071                let value = read_abi_concrete_word_arg(
1072                    &mut self.cx,
1073                    &state.memory,
1074                    args_offset,
1075                    1,
1076                    "symbolic vm.expectCall",
1077                )?;
1078                let gas = read_abi_u64_arg(
1079                    &mut self.cx,
1080                    &state.memory,
1081                    args_offset,
1082                    2,
1083                    "symbolic vm.expectCall",
1084                )?;
1085                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
1086                    &mut self.cx,
1087                    state,
1088                    args_offset,
1089                    3,
1090                    self.config.max_calldata_bytes as usize,
1091                    "symbolic vm.expectCall",
1092                )?;
1093                let count = read_abi_u64_arg(
1094                    &mut self.cx,
1095                    &state.memory,
1096                    args_offset,
1097                    4,
1098                    "symbolic vm.expectCall",
1099                )?;
1100                let data = SymBytes::exprs(&mut self.cx, data);
1101                return Ok(self.set_expected_call(
1102                    state,
1103                    callee,
1104                    Some(value),
1105                    Some(gas),
1106                    None,
1107                    data,
1108                    Some(count),
1109                ));
1110            }
1111            expectCallMinGas_0Call::SELECTOR => {
1112                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1113                let value = read_abi_concrete_word_arg(
1114                    &mut self.cx,
1115                    &state.memory,
1116                    args_offset,
1117                    1,
1118                    "symbolic vm.expectCall",
1119                )?;
1120                let min_gas = read_abi_u64_arg(
1121                    &mut self.cx,
1122                    &state.memory,
1123                    args_offset,
1124                    2,
1125                    "symbolic vm.expectCall",
1126                )?;
1127                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
1128                    &mut self.cx,
1129                    state,
1130                    args_offset,
1131                    3,
1132                    self.config.max_calldata_bytes as usize,
1133                    "symbolic vm.expectCall",
1134                )?;
1135                let data = SymBytes::exprs(&mut self.cx, data);
1136                return Ok(self.set_expected_call(
1137                    state,
1138                    callee,
1139                    Some(value),
1140                    None,
1141                    Some(min_gas),
1142                    data,
1143                    None,
1144                ));
1145            }
1146            expectCallMinGas_1Call::SELECTOR => {
1147                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1148                let value = read_abi_concrete_word_arg(
1149                    &mut self.cx,
1150                    &state.memory,
1151                    args_offset,
1152                    1,
1153                    "symbolic vm.expectCall",
1154                )?;
1155                let min_gas = read_abi_u64_arg(
1156                    &mut self.cx,
1157                    &state.memory,
1158                    args_offset,
1159                    2,
1160                    "symbolic vm.expectCall",
1161                )?;
1162                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
1163                    &mut self.cx,
1164                    state,
1165                    args_offset,
1166                    3,
1167                    self.config.max_calldata_bytes as usize,
1168                    "symbolic vm.expectCall",
1169                )?;
1170                let count = read_abi_u64_arg(
1171                    &mut self.cx,
1172                    &state.memory,
1173                    args_offset,
1174                    4,
1175                    "symbolic vm.expectCall",
1176                )?;
1177                let data = SymBytes::exprs(&mut self.cx, data);
1178                return Ok(self.set_expected_call(
1179                    state,
1180                    callee,
1181                    Some(value),
1182                    None,
1183                    Some(min_gas),
1184                    data,
1185                    Some(count),
1186                ));
1187            }
1188            expectCreateCall::SELECTOR | expectCreate2Call::SELECTOR => {
1189                let bytecode = read_abi_dynamic_bytes_arg(
1190                    &mut self.cx,
1191                    &state.memory,
1192                    args_offset,
1193                    0,
1194                    "symbolic vm.expectCreate bytecode",
1195                )?;
1196                let deployer = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
1197                let kind = if selector == expectCreateCall::SELECTOR {
1198                    CreateKind::Create
1199                } else {
1200                    CreateKind::Create2
1201                };
1202                return Ok(self.set_expected_create(state, bytecode, deployer, kind));
1203            }
1204            clearMockedCallsCall::SELECTOR => {
1205                state.call_mocks.clear();
1206                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1207            }
1208            mockCall_0Call::SELECTOR => {
1209                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1210                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
1211                    &mut self.cx,
1212                    state,
1213                    args_offset,
1214                    1,
1215                    self.config.max_calldata_bytes as usize,
1216                    "symbolic vm.mockCall",
1217                )?;
1218                let ret = read_abi_dynamic_return_data_arg(
1219                    &mut self.cx,
1220                    state,
1221                    args_offset,
1222                    2,
1223                    self.config.max_calldata_bytes as usize,
1224                    "symbolic vm.mockCall",
1225                )?;
1226                let data = SymBytes::exprs(&mut self.cx, data);
1227                return Ok(self.add_call_mock(state, callee, None, data, vec![ret], false));
1228            }
1229            mockCall_1Call::SELECTOR => {
1230                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1231                let value = read_abi_concrete_word_arg(
1232                    &mut self.cx,
1233                    &state.memory,
1234                    args_offset,
1235                    1,
1236                    "symbolic vm.mockCall",
1237                )?;
1238                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
1239                    &mut self.cx,
1240                    state,
1241                    args_offset,
1242                    2,
1243                    self.config.max_calldata_bytes as usize,
1244                    "symbolic vm.mockCall",
1245                )?;
1246                let ret = read_abi_dynamic_return_data_arg(
1247                    &mut self.cx,
1248                    state,
1249                    args_offset,
1250                    3,
1251                    self.config.max_calldata_bytes as usize,
1252                    "symbolic vm.mockCall",
1253                )?;
1254                let data = SymBytes::exprs(&mut self.cx, data);
1255                return Ok(self.add_call_mock(state, callee, Some(value), data, vec![ret], false));
1256            }
1257            mockCall_2Call::SELECTOR => {
1258                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1259                let data = read_abi_bytes4_words_arg(&mut self.cx, &state.memory, args_offset, 1);
1260                let ret = read_abi_dynamic_return_data_arg(
1261                    &mut self.cx,
1262                    state,
1263                    args_offset,
1264                    2,
1265                    self.config.max_calldata_bytes as usize,
1266                    "symbolic vm.mockCall",
1267                )?;
1268                let data = SymBytes::exprs(&mut self.cx, data);
1269                return Ok(self.add_call_mock(state, callee, None, data, vec![ret], false));
1270            }
1271            mockCall_3Call::SELECTOR => {
1272                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1273                let value = read_abi_concrete_word_arg(
1274                    &mut self.cx,
1275                    &state.memory,
1276                    args_offset,
1277                    1,
1278                    "symbolic vm.mockCall",
1279                )?;
1280                let data = read_abi_bytes4_words_arg(&mut self.cx, &state.memory, args_offset, 2);
1281                let ret = read_abi_dynamic_return_data_arg(
1282                    &mut self.cx,
1283                    state,
1284                    args_offset,
1285                    3,
1286                    self.config.max_calldata_bytes as usize,
1287                    "symbolic vm.mockCall",
1288                )?;
1289                let data = SymBytes::exprs(&mut self.cx, data);
1290                return Ok(self.add_call_mock(state, callee, Some(value), data, vec![ret], false));
1291            }
1292            mockCalls_0Call::SELECTOR | mockCalls_1Call::SELECTOR => {
1293                let has_value = selector == mockCalls_1Call::SELECTOR;
1294                let (value, data_idx, ret_idx) = if has_value {
1295                    let value = read_abi_concrete_word_arg(
1296                        &mut self.cx,
1297                        &state.memory,
1298                        args_offset,
1299                        1,
1300                        "symbolic vm.mockCalls",
1301                    )?;
1302                    (Some(value), 2, 3)
1303                } else {
1304                    (None, 1, 2)
1305                };
1306                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1307                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
1308                    &mut self.cx,
1309                    state,
1310                    args_offset,
1311                    data_idx,
1312                    self.config.max_calldata_bytes as usize,
1313                    "symbolic vm.mockCalls data",
1314                )?;
1315                let returns = read_abi_symbolic_dynamic_bytes_array_arg(
1316                    &mut self.cx,
1317                    state,
1318                    args_offset,
1319                    ret_idx,
1320                    self.config.max_dynamic_length as usize,
1321                    self.config.max_calldata_bytes as usize,
1322                )?;
1323                let data = SymBytes::exprs(&mut self.cx, data);
1324                return Ok(self.add_call_mock(state, callee, value, data, returns, false));
1325            }
1326            mockCallRevert_0Call::SELECTOR => {
1327                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1328                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
1329                    &mut self.cx,
1330                    state,
1331                    args_offset,
1332                    1,
1333                    self.config.max_calldata_bytes as usize,
1334                    "symbolic vm.mockCallRevert",
1335                )?;
1336                let ret = read_abi_dynamic_return_data_arg(
1337                    &mut self.cx,
1338                    state,
1339                    args_offset,
1340                    2,
1341                    self.config.max_calldata_bytes as usize,
1342                    "symbolic vm.mockCallRevert",
1343                )?;
1344                let data = SymBytes::exprs(&mut self.cx, data);
1345                return Ok(self.add_call_mock(state, callee, None, data, vec![ret], true));
1346            }
1347            mockCallRevert_1Call::SELECTOR => {
1348                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1349                let value = read_abi_concrete_word_arg(
1350                    &mut self.cx,
1351                    &state.memory,
1352                    args_offset,
1353                    1,
1354                    "symbolic vm.mockCallRevert",
1355                )?;
1356                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
1357                    &mut self.cx,
1358                    state,
1359                    args_offset,
1360                    2,
1361                    self.config.max_calldata_bytes as usize,
1362                    "symbolic vm.mockCallRevert",
1363                )?;
1364                let ret = read_abi_dynamic_return_data_arg(
1365                    &mut self.cx,
1366                    state,
1367                    args_offset,
1368                    3,
1369                    self.config.max_calldata_bytes as usize,
1370                    "symbolic vm.mockCallRevert",
1371                )?;
1372                let data = SymBytes::exprs(&mut self.cx, data);
1373                return Ok(self.add_call_mock(state, callee, Some(value), data, vec![ret], true));
1374            }
1375            mockCallRevert_2Call::SELECTOR => {
1376                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1377                let data = read_abi_bytes4_words_arg(&mut self.cx, &state.memory, args_offset, 1);
1378                let ret = read_abi_dynamic_return_data_arg(
1379                    &mut self.cx,
1380                    state,
1381                    args_offset,
1382                    2,
1383                    self.config.max_calldata_bytes as usize,
1384                    "symbolic vm.mockCallRevert",
1385                )?;
1386                let data = SymBytes::exprs(&mut self.cx, data);
1387                return Ok(self.add_call_mock(state, callee, None, data, vec![ret], true));
1388            }
1389            mockCallRevert_3Call::SELECTOR => {
1390                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1391                let value = read_abi_concrete_word_arg(
1392                    &mut self.cx,
1393                    &state.memory,
1394                    args_offset,
1395                    1,
1396                    "symbolic vm.mockCallRevert",
1397                )?;
1398                let data = read_abi_bytes4_words_arg(&mut self.cx, &state.memory, args_offset, 2);
1399                let ret = read_abi_dynamic_return_data_arg(
1400                    &mut self.cx,
1401                    state,
1402                    args_offset,
1403                    3,
1404                    self.config.max_calldata_bytes as usize,
1405                    "symbolic vm.mockCallRevert",
1406                )?;
1407                let data = SymBytes::exprs(&mut self.cx, data);
1408                return Ok(self.add_call_mock(state, callee, Some(value), data, vec![ret], true));
1409            }
1410            mockFunctionCall::SELECTOR => {
1411                let callee = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1412                let target = read_abi_address_arg(
1413                    &mut self.cx,
1414                    &state.memory,
1415                    args_offset,
1416                    1,
1417                    "symbolic vm.mockFunction",
1418                )?;
1419                let data = read_abi_symbolic_dynamic_byte_exprs_arg(
1420                    &mut self.cx,
1421                    state,
1422                    args_offset,
1423                    2,
1424                    self.config.max_calldata_bytes as usize,
1425                    "symbolic vm.mockFunction",
1426                )?;
1427                let data = SymBytes::exprs(&mut self.cx, data);
1428                return Ok(self.set_function_mock(state, callee, target, data));
1429            }
1430            prank_0Call::SELECTOR => {
1431                let caller = read_abi_address_word_or_symbolic_slot_arg(
1432                    &mut self.cx,
1433                    state,
1434                    args_offset,
1435                    0,
1436                )?;
1437                state.prank.set_next(caller, None);
1438                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1439            }
1440            prank_1Call::SELECTOR => {
1441                let caller = read_abi_address_word_or_symbolic_slot_arg(
1442                    &mut self.cx,
1443                    state,
1444                    args_offset,
1445                    0,
1446                )?;
1447                let origin = read_abi_address_word_or_symbolic_slot_arg(
1448                    &mut self.cx,
1449                    state,
1450                    args_offset,
1451                    1,
1452                )?;
1453                state.prank.set_next(caller, Some(origin));
1454                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1455            }
1456            prank_2Call::SELECTOR => {
1457                let delegate_call = read_abi_bool_arg(
1458                    &mut self.cx,
1459                    &state.memory,
1460                    args_offset,
1461                    1,
1462                    "symbolic vm.prank",
1463                )?;
1464                if delegate_call {
1465                    return Err(SymbolicError::Unsupported("symbolic vm.prank delegatecall"));
1466                }
1467                let caller = read_abi_address_word_or_symbolic_slot_arg(
1468                    &mut self.cx,
1469                    state,
1470                    args_offset,
1471                    0,
1472                )?;
1473                state.prank.set_next(caller, None);
1474                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1475            }
1476            prank_3Call::SELECTOR => {
1477                let delegate_call = read_abi_bool_arg(
1478                    &mut self.cx,
1479                    &state.memory,
1480                    args_offset,
1481                    2,
1482                    "symbolic vm.prank",
1483                )?;
1484                if delegate_call {
1485                    return Err(SymbolicError::Unsupported("symbolic vm.prank delegatecall"));
1486                }
1487                let caller = read_abi_address_word_or_symbolic_slot_arg(
1488                    &mut self.cx,
1489                    state,
1490                    args_offset,
1491                    0,
1492                )?;
1493                let origin = read_abi_address_word_or_symbolic_slot_arg(
1494                    &mut self.cx,
1495                    state,
1496                    args_offset,
1497                    1,
1498                )?;
1499                state.prank.set_next(caller, Some(origin));
1500                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1501            }
1502            startPrank_0Call::SELECTOR => {
1503                let caller = read_abi_address_word_or_symbolic_slot_arg(
1504                    &mut self.cx,
1505                    state,
1506                    args_offset,
1507                    0,
1508                )?;
1509                state.prank.set_persistent(caller, None);
1510                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1511            }
1512            startPrank_1Call::SELECTOR => {
1513                let caller = read_abi_address_word_or_symbolic_slot_arg(
1514                    &mut self.cx,
1515                    state,
1516                    args_offset,
1517                    0,
1518                )?;
1519                let origin = read_abi_address_word_or_symbolic_slot_arg(
1520                    &mut self.cx,
1521                    state,
1522                    args_offset,
1523                    1,
1524                )?;
1525                state.prank.set_persistent(caller, Some(origin));
1526                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1527            }
1528            startPrank_2Call::SELECTOR => {
1529                let delegate_call = read_abi_bool_arg(
1530                    &mut self.cx,
1531                    &state.memory,
1532                    args_offset,
1533                    1,
1534                    "symbolic vm.startPrank",
1535                )?;
1536                if delegate_call {
1537                    return Err(SymbolicError::Unsupported("symbolic vm.startPrank delegatecall"));
1538                }
1539                let caller = read_abi_address_word_or_symbolic_slot_arg(
1540                    &mut self.cx,
1541                    state,
1542                    args_offset,
1543                    0,
1544                )?;
1545                state.prank.set_persistent(caller, None);
1546                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1547            }
1548            startPrank_3Call::SELECTOR => {
1549                let delegate_call = read_abi_bool_arg(
1550                    &mut self.cx,
1551                    &state.memory,
1552                    args_offset,
1553                    2,
1554                    "symbolic vm.startPrank",
1555                )?;
1556                if delegate_call {
1557                    return Err(SymbolicError::Unsupported("symbolic vm.startPrank delegatecall"));
1558                }
1559                let caller = read_abi_address_word_or_symbolic_slot_arg(
1560                    &mut self.cx,
1561                    state,
1562                    args_offset,
1563                    0,
1564                )?;
1565                let origin = read_abi_address_word_or_symbolic_slot_arg(
1566                    &mut self.cx,
1567                    state,
1568                    args_offset,
1569                    1,
1570                )?;
1571                state.prank.set_persistent(caller, Some(origin));
1572                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1573            }
1574            stopPrankCall::SELECTOR => {
1575                state.prank = SymbolicPrank::default();
1576                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1577            }
1578            readCallersCall::SELECTOR => {
1579                return Ok(CheatcodeOutcome::Continue(state.read_callers_words(&mut self.cx)));
1580            }
1581            addrCall::SELECTOR => {
1582                let private_key = read_abi_constrained_word_arg(
1583                    &mut self.cx,
1584                    state,
1585                    args_offset,
1586                    0,
1587                    "symbolic vm.addr",
1588                )?;
1589                let address = private_key_address(private_key)?;
1590                let address = SymExpr::constant(&mut self.cx, address_word(address));
1591                return Ok(CheatcodeOutcome::Continue(vec![address]));
1592            }
1593            sign_1Call::SELECTOR => {
1594                let private_key = read_abi_constrained_word_arg(
1595                    &mut self.cx,
1596                    state,
1597                    args_offset,
1598                    0,
1599                    "symbolic vm.sign",
1600                )?;
1601                let digest = read_abi_constrained_word_arg(
1602                    &mut self.cx,
1603                    state,
1604                    args_offset,
1605                    1,
1606                    "symbolic vm.sign",
1607                )?;
1608                return Ok(CheatcodeOutcome::Continue(sign_hash_words(
1609                    &mut self.cx,
1610                    private_key,
1611                    digest,
1612                )?));
1613            }
1614            signCompact_1Call::SELECTOR => {
1615                let private_key = read_abi_constrained_word_arg(
1616                    &mut self.cx,
1617                    state,
1618                    args_offset,
1619                    0,
1620                    "symbolic vm.signCompact",
1621                )?;
1622                let digest = read_abi_constrained_word_arg(
1623                    &mut self.cx,
1624                    state,
1625                    args_offset,
1626                    1,
1627                    "symbolic vm.signCompact",
1628                )?;
1629                return Ok(CheatcodeOutcome::Continue(sign_compact_hash_words(
1630                    &mut self.cx,
1631                    private_key,
1632                    digest,
1633                )?));
1634            }
1635            deriveKey_0Call::SELECTOR => {
1636                let mnemonic = read_abi_string_arg(
1637                    &mut self.cx,
1638                    &state.memory,
1639                    args_offset,
1640                    0,
1641                    "symbolic vm.deriveKey",
1642                )?;
1643                let index = read_abi_u32_arg(
1644                    &mut self.cx,
1645                    &state.memory,
1646                    args_offset,
1647                    1,
1648                    "symbolic vm.deriveKey",
1649                )?;
1650                let private_key = derive_private_key::<English>(
1651                    &mnemonic,
1652                    DEFAULT_DERIVATION_PATH_PREFIX,
1653                    index,
1654                )?;
1655                let private_key = SymExpr::constant(&mut self.cx, private_key);
1656                return Ok(CheatcodeOutcome::Continue(vec![private_key]));
1657            }
1658            deriveKey_1Call::SELECTOR => {
1659                let mnemonic = read_abi_string_arg(
1660                    &mut self.cx,
1661                    &state.memory,
1662                    args_offset,
1663                    0,
1664                    "symbolic vm.deriveKey",
1665                )?;
1666                let path = read_abi_string_arg(
1667                    &mut self.cx,
1668                    &state.memory,
1669                    args_offset,
1670                    1,
1671                    "symbolic vm.deriveKey",
1672                )?;
1673                let index = read_abi_u32_arg(
1674                    &mut self.cx,
1675                    &state.memory,
1676                    args_offset,
1677                    2,
1678                    "symbolic vm.deriveKey",
1679                )?;
1680                let private_key = derive_private_key::<English>(&mnemonic, &path, index)?;
1681                let private_key = SymExpr::constant(&mut self.cx, private_key);
1682                return Ok(CheatcodeOutcome::Continue(vec![private_key]));
1683            }
1684            deriveKey_2Call::SELECTOR => {
1685                let mnemonic = read_abi_string_arg(
1686                    &mut self.cx,
1687                    &state.memory,
1688                    args_offset,
1689                    0,
1690                    "symbolic vm.deriveKey",
1691                )?;
1692                let index = read_abi_u32_arg(
1693                    &mut self.cx,
1694                    &state.memory,
1695                    args_offset,
1696                    1,
1697                    "symbolic vm.deriveKey",
1698                )?;
1699                let language = read_abi_string_arg(
1700                    &mut self.cx,
1701                    &state.memory,
1702                    args_offset,
1703                    2,
1704                    "symbolic vm.deriveKey",
1705                )?;
1706                let private_key = derive_private_key_with_language(
1707                    &mnemonic,
1708                    DEFAULT_DERIVATION_PATH_PREFIX,
1709                    index,
1710                    &language,
1711                )?;
1712                let private_key = SymExpr::constant(&mut self.cx, private_key);
1713                return Ok(CheatcodeOutcome::Continue(vec![private_key]));
1714            }
1715            deriveKey_3Call::SELECTOR => {
1716                let mnemonic = read_abi_string_arg(
1717                    &mut self.cx,
1718                    &state.memory,
1719                    args_offset,
1720                    0,
1721                    "symbolic vm.deriveKey",
1722                )?;
1723                let path = read_abi_string_arg(
1724                    &mut self.cx,
1725                    &state.memory,
1726                    args_offset,
1727                    1,
1728                    "symbolic vm.deriveKey",
1729                )?;
1730                let index = read_abi_u32_arg(
1731                    &mut self.cx,
1732                    &state.memory,
1733                    args_offset,
1734                    2,
1735                    "symbolic vm.deriveKey",
1736                )?;
1737                let language = read_abi_string_arg(
1738                    &mut self.cx,
1739                    &state.memory,
1740                    args_offset,
1741                    3,
1742                    "symbolic vm.deriveKey",
1743                )?;
1744                let private_key =
1745                    derive_private_key_with_language(&mnemonic, &path, index, &language)?;
1746                let private_key = SymExpr::constant(&mut self.cx, private_key);
1747                return Ok(CheatcodeOutcome::Continue(vec![private_key]));
1748            }
1749            rememberKeyCall::SELECTOR => {
1750                let private_key = read_abi_constrained_word_arg(
1751                    &mut self.cx,
1752                    state,
1753                    args_offset,
1754                    0,
1755                    "symbolic vm.rememberKey",
1756                )?;
1757                let address = private_key_address(private_key)?;
1758                state.wallets.insert(address);
1759                let address = SymExpr::constant(&mut self.cx, address_word(address));
1760                return Ok(CheatcodeOutcome::Continue(vec![address]));
1761            }
1762            rememberKeys_0Call::SELECTOR | rememberKeys_1Call::SELECTOR => {
1763                let mnemonic = read_abi_string_arg(
1764                    &mut self.cx,
1765                    &state.memory,
1766                    args_offset,
1767                    0,
1768                    "symbolic vm.rememberKeys",
1769                )?;
1770                let path = read_abi_string_arg(
1771                    &mut self.cx,
1772                    &state.memory,
1773                    args_offset,
1774                    1,
1775                    "symbolic vm.rememberKeys",
1776                )?;
1777                let (language, count_index) = if selector == rememberKeys_1Call::SELECTOR {
1778                    (
1779                        Some(read_abi_string_arg(
1780                            &mut self.cx,
1781                            &state.memory,
1782                            args_offset,
1783                            2,
1784                            "symbolic vm.rememberKeys",
1785                        )?),
1786                        3,
1787                    )
1788                } else {
1789                    (None, 2)
1790                };
1791                let count = read_abi_u32_arg(
1792                    &mut self.cx,
1793                    &state.memory,
1794                    args_offset,
1795                    count_index,
1796                    "symbolic vm.rememberKeys",
1797                )?;
1798                if count > MAX_REMEMBER_KEYS {
1799                    return Err(SymbolicError::Unsupported("symbolic vm.rememberKeys count"));
1800                }
1801                let mut addresses = Vec::with_capacity(count as usize);
1802                for index in 0..count {
1803                    let private_key = if let Some(language) = &language {
1804                        derive_private_key_with_language(&mnemonic, &path, index, language)?
1805                    } else {
1806                        derive_private_key::<English>(&mnemonic, &path, index)?
1807                    };
1808                    let address = private_key_address(private_key)?;
1809                    state.wallets.insert(address);
1810                    addresses.push(DynSolValue::Address(address));
1811                }
1812                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_value_return(
1813                    &mut self.cx,
1814                    DynSolValue::Array(addresses),
1815                )));
1816            }
1817            getWalletsCall::SELECTOR => {
1818                let wallets = DynSolValue::Array(
1819                    state.wallets.iter().copied().map(DynSolValue::Address).collect(),
1820                );
1821                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_value_return(
1822                    &mut self.cx,
1823                    wallets,
1824                )));
1825            }
1826            storeCall::SELECTOR => {
1827                let target =
1828                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
1829                let slot = state.memory.load_word(&mut self.cx, in_offset + 36)?;
1830                let value = state.memory.load_word(&mut self.cx, in_offset + 68)?;
1831                let failed_slot = SymExpr::constant(&mut self.cx, failed_slot());
1832                let one = SymExpr::one(&mut self.cx);
1833                if target == CHEATCODE_ADDRESS && slot == failed_slot && value == one {
1834                    return Ok(CheatcodeOutcome::Failure);
1835                }
1836                state.world.sstore(target, slot, value);
1837                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1838            }
1839            loadCall::SELECTOR => {
1840                let target =
1841                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
1842                let slot = state.memory.load_word(&mut self.cx, in_offset + 36)?;
1843                let concrete_slot = state.constrained_word(&mut self.cx, &slot);
1844                let value =
1845                    state.world.sload(&mut self.cx, executor, target, slot, concrete_slot)?;
1846                return Ok(CheatcodeOutcome::Continue(vec![value]));
1847            }
1848            getNonce_0Call::SELECTOR => {
1849                let target =
1850                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
1851                let nonce = state.world.nonce(executor, target)?;
1852                let nonce = SymExpr::constant(&mut self.cx, U256::from(nonce));
1853                return Ok(CheatcodeOutcome::Continue(vec![nonce]));
1854            }
1855            computeCreateAddressCall::SELECTOR => {
1856                let deployer = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1857                let nonce = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
1858                let address = compute_create_address_word(&mut self.cx, state, deployer, nonce)?;
1859                return Ok(CheatcodeOutcome::Continue(vec![address]));
1860            }
1861            computeCreate2Address_0Call::SELECTOR => {
1862                let salt = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1863                let init_code_hash =
1864                    read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
1865                let deployer = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 2)?;
1866                let address = compute_create2_address_word(
1867                    &mut self.cx,
1868                    state,
1869                    deployer,
1870                    salt,
1871                    init_code_hash,
1872                )?;
1873                return Ok(CheatcodeOutcome::Continue(vec![address]));
1874            }
1875            computeCreate2Address_1Call::SELECTOR => {
1876                let salt = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
1877                let init_code_hash =
1878                    read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
1879                let deployer =
1880                    SymExpr::constant(&mut self.cx, address_word(DEFAULT_CREATE2_DEPLOYER));
1881                let address = compute_create2_address_word(
1882                    &mut self.cx,
1883                    state,
1884                    deployer,
1885                    salt,
1886                    init_code_hash,
1887                )?;
1888                return Ok(CheatcodeOutcome::Continue(vec![address]));
1889            }
1890            etchCall::SELECTOR => {
1891                let target =
1892                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
1893                let code = read_abi_symbolic_dynamic_byte_exprs_arg(
1894                    &mut self.cx,
1895                    state,
1896                    args_offset,
1897                    1,
1898                    self.config.max_dynamic_length as usize,
1899                    "symbolic vm.etch",
1900                )?;
1901                let code = SymCode::from_byte_exprs(&mut self.cx, code);
1902                state.world.install_code(target, code);
1903                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1904            }
1905            getCodeCall::SELECTOR | getDeployedCodeCall::SELECTOR => {
1906                let artifact = read_abi_string_arg(
1907                    &mut self.cx,
1908                    &state.memory,
1909                    args_offset,
1910                    0,
1911                    "symbolic vm.getCode",
1912                )?;
1913                let code = artifact_code(&artifact, selector == getDeployedCodeCall::SELECTOR)?;
1914                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
1915                    &mut self.cx,
1916                    &code,
1917                )));
1918            }
1919            dealCall::SELECTOR => {
1920                let target =
1921                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
1922                let value = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
1923                if value.contains_gasleft() {
1924                    return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
1925                }
1926                let value = state
1927                    .constrained_word(&mut self.cx, &value)
1928                    .map(|value| SymExpr::constant(&mut self.cx, value))
1929                    .unwrap_or(value);
1930                state.world.set_balance_word(target, value);
1931                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1932            }
1933            setNonceCall::SELECTOR | setNonceUnsafeCall::SELECTOR => {
1934                let target =
1935                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
1936                let nonce = read_abi_constrained_word_arg(
1937                    &mut self.cx,
1938                    state,
1939                    args_offset,
1940                    1,
1941                    "symbolic vm.setNonce",
1942                )?;
1943                let Ok(nonce) = u64::try_from(nonce) else {
1944                    return Err(SymbolicError::Unsupported("symbolic vm.setNonce nonce"));
1945                };
1946                if selector == setNonceCall::SELECTOR
1947                    && nonce < state.world.nonce(executor, target)?
1948                {
1949                    return Ok(CheatcodeOutcome::Failure);
1950                }
1951                state.world.set_nonce(target, nonce);
1952                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1953            }
1954            resetNonceCall::SELECTOR => {
1955                let target =
1956                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
1957                let nonce = if state.world.extcode(&mut self.cx, executor, target)?.is_empty() {
1958                    0
1959                } else {
1960                    1
1961                };
1962                state.world.set_nonce(target, nonce);
1963                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1964            }
1965            allowCheatcodesCall::SELECTOR => {
1966                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1967            }
1968            makePersistent_0Call::SELECTOR => {
1969                let account =
1970                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
1971                state.persistent_accounts.insert(account);
1972                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1973            }
1974            makePersistent_1Call::SELECTOR => {
1975                let account0 =
1976                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
1977                let account1 =
1978                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 1)?;
1979                state.persistent_accounts.insert(account0);
1980                state.persistent_accounts.insert(account1);
1981                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1982            }
1983            makePersistent_2Call::SELECTOR => {
1984                let account0 =
1985                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
1986                let account1 =
1987                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 1)?;
1988                let account2 =
1989                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 2)?;
1990                state.persistent_accounts.insert(account0);
1991                state.persistent_accounts.insert(account1);
1992                state.persistent_accounts.insert(account2);
1993                return Ok(CheatcodeOutcome::Continue(Vec::new()));
1994            }
1995            makePersistent_3Call::SELECTOR => {
1996                let values = decode_cheatcode_args(
1997                    &mut self.cx,
1998                    state,
1999                    in_offset,
2000                    in_size,
2001                    vec![DynSolType::Array(Box::new(DynSolType::Address))],
2002                )?;
2003                for account in dyn_address_array(&values[0])? {
2004                    state.persistent_accounts.insert(account);
2005                }
2006                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2007            }
2008            revokePersistent_0Call::SELECTOR => {
2009                let account =
2010                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
2011                state.persistent_accounts.remove(&account);
2012                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2013            }
2014            revokePersistent_1Call::SELECTOR => {
2015                let values = decode_cheatcode_args(
2016                    &mut self.cx,
2017                    state,
2018                    in_offset,
2019                    in_size,
2020                    vec![DynSolType::Array(Box::new(DynSolType::Address))],
2021                )?;
2022                for account in dyn_address_array(&values[0])? {
2023                    state.persistent_accounts.remove(&account);
2024                }
2025                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2026            }
2027            isPersistentCall::SELECTOR => {
2028                let account =
2029                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
2030                let exists = SymExpr::constant(
2031                    &mut self.cx,
2032                    U256::from(state.persistent_accounts.contains(&account)),
2033                );
2034                return Ok(CheatcodeOutcome::Continue(vec![exists]));
2035            }
2036            activeForkCall::SELECTOR => {
2037                let id = executor.backend().active_fork_id().ok_or(SymbolicError::Unsupported(
2038                    "symbolic vm.activeFork requires an active forked executor",
2039                ))?;
2040                let id = SymExpr::constant(&mut self.cx, id);
2041                return Ok(CheatcodeOutcome::Continue(vec![id]));
2042            }
2043            selectForkCall::SELECTOR => {
2044                let id = read_abi_constrained_word_arg(
2045                    &mut self.cx,
2046                    state,
2047                    args_offset,
2048                    0,
2049                    "symbolic vm.selectFork id",
2050                )?;
2051                if executor.backend().is_active_fork(id) {
2052                    return Ok(CheatcodeOutcome::Continue(Vec::new()));
2053                }
2054                return Err(SymbolicError::Unsupported(
2055                    "symbolic vm.selectFork can only select the already active fork",
2056                ));
2057            }
2058            rollFork_0Call::SELECTOR => {
2059                let block_number = read_abi_constrained_word_arg(
2060                    &mut self.cx,
2061                    state,
2062                    args_offset,
2063                    0,
2064                    "symbolic vm.rollFork block number",
2065                )?;
2066                let current =
2067                    state.block.number.as_const_or("symbolic vm.rollFork current block")?;
2068                if block_number == current {
2069                    return Ok(CheatcodeOutcome::Continue(Vec::new()));
2070                }
2071                return Err(SymbolicError::Unsupported(
2072                    "symbolic vm.rollFork cannot change the active fork block during symbolic execution",
2073                ));
2074            }
2075            rollFork_2Call::SELECTOR => {
2076                let id = read_abi_constrained_word_arg(
2077                    &mut self.cx,
2078                    state,
2079                    args_offset,
2080                    0,
2081                    "symbolic vm.rollFork id",
2082                )?;
2083                let block_number = read_abi_constrained_word_arg(
2084                    &mut self.cx,
2085                    state,
2086                    args_offset,
2087                    1,
2088                    "symbolic vm.rollFork block number",
2089                )?;
2090                let current =
2091                    state.block.number.as_const_or("symbolic vm.rollFork current block")?;
2092                if executor.backend().is_active_fork(id) && block_number == current {
2093                    return Ok(CheatcodeOutcome::Continue(Vec::new()));
2094                }
2095                return Err(SymbolicError::Unsupported(
2096                    "symbolic vm.rollFork cannot change the active fork block during symbolic execution",
2097                ));
2098            }
2099            createFork_0Call::SELECTOR
2100            | createFork_1Call::SELECTOR
2101            | createFork_2Call::SELECTOR
2102            | createSelectFork_0Call::SELECTOR
2103            | createSelectFork_1Call::SELECTOR
2104            | createSelectFork_2Call::SELECTOR
2105            | rollFork_1Call::SELECTOR
2106            | rollFork_3Call::SELECTOR => {
2107                return Err(SymbolicError::Unsupported(
2108                    "symbolic fork creation and fork block mutation must happen before symbolic execution",
2109                ));
2110            }
2111            snapshotCall::SELECTOR | snapshotStateCall::SELECTOR => {
2112                let id = state.world.snapshot_state();
2113                let id = SymExpr::constant(&mut self.cx, id);
2114                return Ok(CheatcodeOutcome::Continue(vec![id]));
2115            }
2116            revertToCall::SELECTOR
2117            | revertToStateCall::SELECTOR
2118            | revertToAndDeleteCall::SELECTOR
2119            | revertToStateAndDeleteCall::SELECTOR => {
2120                let id = read_abi_constrained_word_arg(
2121                    &mut self.cx,
2122                    state,
2123                    args_offset,
2124                    0,
2125                    "symbolic vm.revertToState snapshot",
2126                )?;
2127                let success = state.world.restore_snapshot(id);
2128                if success
2129                    && (selector == revertToAndDeleteCall::SELECTOR
2130                        || selector == revertToStateAndDeleteCall::SELECTOR)
2131                {
2132                    state.world.delete_snapshot(id);
2133                }
2134                let success = SymExpr::constant(&mut self.cx, U256::from(success));
2135                return Ok(CheatcodeOutcome::Continue(vec![success]));
2136            }
2137            deleteSnapshotCall::SELECTOR | deleteStateSnapshotCall::SELECTOR => {
2138                let id = read_abi_constrained_word_arg(
2139                    &mut self.cx,
2140                    state,
2141                    args_offset,
2142                    0,
2143                    "symbolic vm.deleteStateSnapshot snapshot",
2144                )?;
2145                let success = state.world.delete_snapshot(id);
2146                let success = SymExpr::constant(&mut self.cx, U256::from(success));
2147                return Ok(CheatcodeOutcome::Continue(vec![success]));
2148            }
2149            deleteSnapshotsCall::SELECTOR | deleteStateSnapshotsCall::SELECTOR => {
2150                state.world.delete_snapshots();
2151                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2152            }
2153            warpCall::SELECTOR => {
2154                state.block.timestamp = state.memory.load_word(&mut self.cx, in_offset + 4)?;
2155                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2156            }
2157            rollCall::SELECTOR => {
2158                state.block.number = state.memory.load_word(&mut self.cx, in_offset + 4)?;
2159                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2160            }
2161            setBlockhashCall::SELECTOR => {
2162                let block_number = read_abi_constrained_word_arg(
2163                    &mut self.cx,
2164                    state,
2165                    args_offset,
2166                    0,
2167                    "symbolic vm.setBlockhash block number",
2168                )?;
2169                let block_hash = state.memory.load_word(&mut self.cx, in_offset + 36)?;
2170                state.block.set_block_hash(block_number, block_hash)?;
2171                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2172            }
2173            prevrandao_0Call::SELECTOR | prevrandao_1Call::SELECTOR => {
2174                state.block.difficulty = state.memory.load_word(&mut self.cx, in_offset + 4)?;
2175                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2176            }
2177            blobhashesCall::SELECTOR => {
2178                let values = decode_cheatcode_args(
2179                    &mut self.cx,
2180                    state,
2181                    in_offset,
2182                    in_size,
2183                    vec![DynSolType::Array(Box::new(DynSolType::FixedBytes(32)))],
2184                )?;
2185                state.block.set_blob_hashes(dyn_bytes32_array(&values[0])?);
2186                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2187            }
2188            getBlobhashesCall::SELECTOR => {
2189                let value = DynSolValue::Array(
2190                    state
2191                        .block
2192                        .blob_hashes
2193                        .iter()
2194                        .copied()
2195                        .map(|hash| DynSolValue::FixedBytes(hash, 32))
2196                        .collect(),
2197                );
2198                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_value_return(
2199                    &mut self.cx,
2200                    value,
2201                )));
2202            }
2203            feeCall::SELECTOR => {
2204                state.block.basefee = state.memory.load_word(&mut self.cx, in_offset + 4)?;
2205                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2206            }
2207            blobBaseFeeCall::SELECTOR => {
2208                state.block.blob_basefee = state.memory.load_word(&mut self.cx, in_offset + 4)?;
2209                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2210            }
2211            getBlobBaseFeeCall::SELECTOR => {
2212                return Ok(CheatcodeOutcome::Continue(vec![state.block.blob_basefee.clone()]));
2213            }
2214            chainIdCall::SELECTOR => {
2215                state.block.chain_id = state.memory.load_word(&mut self.cx, in_offset + 4)?;
2216                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2217            }
2218            getChainIdCall::SELECTOR => {
2219                return Ok(CheatcodeOutcome::Continue(vec![state.block.chain_id.clone()]));
2220            }
2221            difficultyCall::SELECTOR => {
2222                state.block.difficulty = state.memory.load_word(&mut self.cx, in_offset + 4)?;
2223                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2224            }
2225            coinbaseCall::SELECTOR => {
2226                let coinbase = read_abi_constrained_address_arg(
2227                    &mut self.cx,
2228                    state,
2229                    args_offset,
2230                    0,
2231                    "symbolic vm.coinbase value",
2232                )?;
2233                state.block.coinbase = coinbase;
2234                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2235            }
2236            getBlockNumberCall::SELECTOR => {
2237                return Ok(CheatcodeOutcome::Continue(vec![state.block.number.clone()]));
2238            }
2239            txGasPriceCall::SELECTOR => {
2240                state.gas_price = state.memory.load_word(&mut self.cx, in_offset + 4)?;
2241                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2242            }
2243            getBlockTimestampCall::SELECTOR => {
2244                return Ok(CheatcodeOutcome::Continue(vec![state.block.timestamp.clone()]));
2245            }
2246            labelCall::SELECTOR => {
2247                let values = decode_cheatcode_args(
2248                    &mut self.cx,
2249                    state,
2250                    in_offset,
2251                    in_size,
2252                    vec![DynSolType::Address, DynSolType::String],
2253                )?;
2254                let account = dyn_address(&values[0])?;
2255                let label = dyn_string(&values[1])?;
2256                state.labels.insert(account, label);
2257                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2258            }
2259            getLabelCall::SELECTOR => {
2260                let account = read_abi_address_arg(
2261                    &mut self.cx,
2262                    &state.memory,
2263                    args_offset,
2264                    0,
2265                    "symbolic vm.getLabel",
2266                )?;
2267                let label = state
2268                    .labels
2269                    .get(&account)
2270                    .cloned()
2271                    .unwrap_or_else(|| format!("unlabeled:{account}"));
2272                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2273                    &mut self.cx,
2274                    label.as_bytes(),
2275                )));
2276            }
2277            expectSafeMemoryCall::SELECTOR => {
2278                return Err(SymbolicError::Unsupported("symbolic vm.expectSafeMemory not modeled"));
2279            }
2280            expectSafeMemoryCallCall::SELECTOR => {
2281                return Err(SymbolicError::Unsupported(
2282                    "symbolic vm.expectSafeMemoryCall not modeled",
2283                ));
2284            }
2285            stopExpectSafeMemoryCall::SELECTOR => {
2286                return Err(SymbolicError::Unsupported(
2287                    "symbolic vm.stopExpectSafeMemory not modeled",
2288                ));
2289            }
2290            lastCallGasCall::SELECTOR => {
2291                return Err(SymbolicError::Unsupported("symbolic vm.lastCallGas not modeled"));
2292            }
2293            lastFrameGasCall::SELECTOR => {
2294                return Err(SymbolicError::Unsupported("symbolic vm.lastFrameGas not modeled"));
2295            }
2296            snapshotGasLastCall_0Call::SELECTOR | snapshotGasLastCall_1Call::SELECTOR => {
2297                return Err(SymbolicError::Unsupported(
2298                    "symbolic vm.snapshotGasLastCall not modeled",
2299                ));
2300            }
2301            snapshotGasLastFrame_0Call::SELECTOR | snapshotGasLastFrame_1Call::SELECTOR => {
2302                return Err(SymbolicError::Unsupported(
2303                    "symbolic vm.snapshotGasLastFrame not modeled",
2304                ));
2305            }
2306            stopSnapshotGas_0Call::SELECTOR
2307            | stopSnapshotGas_1Call::SELECTOR
2308            | stopSnapshotGas_2Call::SELECTOR => {
2309                return Err(SymbolicError::Unsupported("symbolic vm.stopSnapshotGas not modeled"));
2310            }
2311            pauseGasMeteringCall::SELECTOR
2312            | resumeGasMeteringCall::SELECTOR
2313            | resetGasMeteringCall::SELECTOR
2314            | breakpoint_0Call::SELECTOR
2315            | breakpoint_1Call::SELECTOR
2316            | snapshotValue_0Call::SELECTOR
2317            | snapshotValue_1Call::SELECTOR
2318            | startSnapshotGas_0Call::SELECTOR
2319            | startSnapshotGas_1Call::SELECTOR
2320            | sleepCall::SELECTOR
2321            | coolCall::SELECTOR
2322            | accessListCall::SELECTOR
2323            | warmSlotCall::SELECTOR
2324            | coolSlotCall::SELECTOR
2325            | noAccessListCall::SELECTOR => {
2326                return Ok(CheatcodeOutcome::Continue(Vec::new()));
2327            }
2328            setEvmVersionCall::SELECTOR => {
2329                return Err(SymbolicError::Unsupported("symbolic vm.setEvmVersion not modeled"));
2330            }
2331            getEvmVersionCall::SELECTOR => {
2332                return Err(SymbolicError::Unsupported("symbolic vm.getEvmVersion not modeled"));
2333            }
2334            getFoundryVersionCall::SELECTOR => {
2335                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2336                    &mut self.cx,
2337                    env!("CARGO_PKG_VERSION").as_bytes(),
2338                )));
2339            }
2340            projectRootCall::SELECTOR => {
2341                let root = std::env::current_dir()
2342                    .map_err(|_| SymbolicError::Unsupported("symbolic vm.projectRoot"))?;
2343                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2344                    &mut self.cx,
2345                    root.display().to_string().as_bytes(),
2346                )));
2347            }
2348            unixTimeCall::SELECTOR => {
2349                let milliseconds = SystemTime::now()
2350                    .duration_since(UNIX_EPOCH)
2351                    .map_err(|_| SymbolicError::Unsupported("symbolic vm.unixTime"))?
2352                    .as_millis();
2353                let value = U256::try_from(milliseconds)
2354                    .map_err(|_| SymbolicError::Unsupported("symbolic vm.unixTime"))?;
2355                let value = SymExpr::constant(&mut self.cx, value);
2356                return Ok(CheatcodeOutcome::Continue(vec![value]));
2357            }
2358            isIsolateModeCall::SELECTOR => {
2359                let isolate = executor
2360                    .inspector()
2361                    .cheatcodes
2362                    .as_ref()
2363                    .is_some_and(|cheats| cheats.config.isolate);
2364                let isolate = SymExpr::constant(&mut self.cx, U256::from(isolate));
2365                return Ok(CheatcodeOutcome::Continue(vec![isolate]));
2366            }
2367            isContextCall::SELECTOR => {
2368                let context = read_abi_concrete_word_arg(
2369                    &mut self.cx,
2370                    &state.memory,
2371                    args_offset,
2372                    0,
2373                    "symbolic vm.isContext",
2374                )?;
2375                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2376                    &mut self.cx,
2377                    U256::from(context == U256::ZERO || context == U256::from(1)),
2378                )]));
2379            }
2380            toString_0Call::SELECTOR => {
2381                let address = read_abi_address_arg(
2382                    &mut self.cx,
2383                    &state.memory,
2384                    args_offset,
2385                    0,
2386                    "symbolic vm.toString",
2387                )?;
2388                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2389                    &mut self.cx,
2390                    format!("{address:?}").as_bytes(),
2391                )));
2392            }
2393            toString_1Call::SELECTOR => {
2394                let bytes = read_abi_dynamic_bytes_arg(
2395                    &mut self.cx,
2396                    &state.memory,
2397                    args_offset,
2398                    0,
2399                    "symbolic vm.toString",
2400                )?;
2401                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2402                    &mut self.cx,
2403                    format!("0x{}", hex::encode(bytes)).as_bytes(),
2404                )));
2405            }
2406            toString_2Call::SELECTOR => {
2407                let value = read_abi_concrete_word_arg(
2408                    &mut self.cx,
2409                    &state.memory,
2410                    args_offset,
2411                    0,
2412                    "symbolic vm.toString",
2413                )?;
2414                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2415                    &mut self.cx,
2416                    format!("0x{}", hex::encode(value.to_be_bytes::<32>())).as_bytes(),
2417                )));
2418            }
2419            toString_3Call::SELECTOR => {
2420                let value = read_abi_bool_arg(
2421                    &mut self.cx,
2422                    &state.memory,
2423                    args_offset,
2424                    0,
2425                    "symbolic vm.toString",
2426                )?;
2427                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2428                    &mut self.cx,
2429                    if value { "true" } else { "false" }.as_bytes(),
2430                )));
2431            }
2432            toString_4Call::SELECTOR => {
2433                let value = read_abi_concrete_word_arg(
2434                    &mut self.cx,
2435                    &state.memory,
2436                    args_offset,
2437                    0,
2438                    "symbolic vm.toString",
2439                )?;
2440                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2441                    &mut self.cx,
2442                    value.to_string().as_bytes(),
2443                )));
2444            }
2445            toString_5Call::SELECTOR => {
2446                let value = read_abi_concrete_word_arg(
2447                    &mut self.cx,
2448                    &state.memory,
2449                    args_offset,
2450                    0,
2451                    "symbolic vm.toString",
2452                )?;
2453                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2454                    &mut self.cx,
2455                    I256::from_raw(value).to_string().as_bytes(),
2456                )));
2457            }
2458            parseBytesCall::SELECTOR => {
2459                let value = read_abi_string_arg(
2460                    &mut self.cx,
2461                    &state.memory,
2462                    args_offset,
2463                    0,
2464                    "symbolic vm.parseBytes",
2465                )?;
2466                let bytes = parse_env_bytes(&value)?;
2467                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2468                    &mut self.cx,
2469                    &bytes,
2470                )));
2471            }
2472            parseAddressCall::SELECTOR => {
2473                let value = read_abi_string_arg(
2474                    &mut self.cx,
2475                    &state.memory,
2476                    args_offset,
2477                    0,
2478                    "symbolic vm.parseAddress",
2479                )?;
2480                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2481                    &mut self.cx,
2482                    address_word(parse_env_address(&value)?),
2483                )]));
2484            }
2485            parseUintCall::SELECTOR => {
2486                let value = read_abi_string_arg(
2487                    &mut self.cx,
2488                    &state.memory,
2489                    args_offset,
2490                    0,
2491                    "symbolic vm.parseUint",
2492                )?;
2493                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2494                    &mut self.cx,
2495                    parse_env_uint(&value)?,
2496                )]));
2497            }
2498            parseIntCall::SELECTOR => {
2499                let value = read_abi_string_arg(
2500                    &mut self.cx,
2501                    &state.memory,
2502                    args_offset,
2503                    0,
2504                    "symbolic vm.parseInt",
2505                )?;
2506                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2507                    &mut self.cx,
2508                    parse_env_int(&value)?,
2509                )]));
2510            }
2511            parseBytes32Call::SELECTOR => {
2512                let value = read_abi_string_arg(
2513                    &mut self.cx,
2514                    &state.memory,
2515                    args_offset,
2516                    0,
2517                    "symbolic vm.parseBytes32",
2518                )?;
2519                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2520                    &mut self.cx,
2521                    parse_env_bytes32(&value)?,
2522                )]));
2523            }
2524            parseBoolCall::SELECTOR => {
2525                let value = read_abi_string_arg(
2526                    &mut self.cx,
2527                    &state.memory,
2528                    args_offset,
2529                    0,
2530                    "symbolic vm.parseBool",
2531                )?;
2532                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2533                    &mut self.cx,
2534                    U256::from(parse_env_bool(&value)?),
2535                )]));
2536            }
2537            toLowercaseCall::SELECTOR | toUppercaseCall::SELECTOR | trimCall::SELECTOR => {
2538                let value = read_abi_string_arg(
2539                    &mut self.cx,
2540                    &state.memory,
2541                    args_offset,
2542                    0,
2543                    "symbolic vm.string",
2544                )?;
2545                let output = if selector == toLowercaseCall::SELECTOR {
2546                    value.to_lowercase()
2547                } else if selector == toUppercaseCall::SELECTOR {
2548                    value.to_uppercase()
2549                } else {
2550                    value.trim().to_string()
2551                };
2552                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2553                    &mut self.cx,
2554                    output.as_bytes(),
2555                )));
2556            }
2557            replaceCall::SELECTOR => {
2558                let values = decode_cheatcode_args(
2559                    &mut self.cx,
2560                    state,
2561                    in_offset,
2562                    in_size,
2563                    vec![DynSolType::String, DynSolType::String, DynSolType::String],
2564                )?;
2565                let output = dyn_string(&values[0])?
2566                    .replace(&dyn_string(&values[1])?, &dyn_string(&values[2])?);
2567                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2568                    &mut self.cx,
2569                    output.as_bytes(),
2570                )));
2571            }
2572            splitCall::SELECTOR => {
2573                let values = decode_cheatcode_args(
2574                    &mut self.cx,
2575                    state,
2576                    in_offset,
2577                    in_size,
2578                    vec![DynSolType::String, DynSolType::String],
2579                )?;
2580                let input = dyn_string(&values[0])?;
2581                let delimiter = dyn_string(&values[1])?;
2582                let parts = if delimiter.is_empty() {
2583                    input.chars().map(|ch| DynSolValue::String(ch.to_string())).collect()
2584                } else {
2585                    input
2586                        .split(&delimiter)
2587                        .map(|part| DynSolValue::String(part.to_string()))
2588                        .collect()
2589                };
2590                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_value_return(
2591                    &mut self.cx,
2592                    DynSolValue::Array(parts),
2593                )));
2594            }
2595            indexOfCall::SELECTOR => {
2596                let values = decode_cheatcode_args(
2597                    &mut self.cx,
2598                    state,
2599                    in_offset,
2600                    in_size,
2601                    vec![DynSolType::String, DynSolType::String],
2602                )?;
2603                let input = dyn_string(&values[0])?;
2604                let needle = dyn_string(&values[1])?;
2605                let index = input.find(&needle).map(U256::from).unwrap_or(U256::MAX);
2606                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2607                    &mut self.cx,
2608                    index,
2609                )]));
2610            }
2611            containsCall::SELECTOR => {
2612                let values = decode_cheatcode_args(
2613                    &mut self.cx,
2614                    state,
2615                    in_offset,
2616                    in_size,
2617                    vec![DynSolType::String, DynSolType::String],
2618                )?;
2619                let contains = dyn_string(&values[0])?.contains(&dyn_string(&values[1])?);
2620                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2621                    &mut self.cx,
2622                    U256::from(contains),
2623                )]));
2624            }
2625            toBase64_0Call::SELECTOR
2626            | toBase64_1Call::SELECTOR
2627            | toBase64URL_0Call::SELECTOR
2628            | toBase64URL_1Call::SELECTOR => {
2629                let data = read_abi_dynamic_bytes_arg(
2630                    &mut self.cx,
2631                    &state.memory,
2632                    args_offset,
2633                    0,
2634                    "symbolic vm.toBase64",
2635                )?;
2636                let encoded = if selector == toBase64URL_0Call::SELECTOR
2637                    || selector == toBase64URL_1Call::SELECTOR
2638                {
2639                    BASE64_URL_SAFE.encode(data)
2640                } else {
2641                    BASE64_STANDARD.encode(data)
2642                };
2643                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2644                    &mut self.cx,
2645                    encoded.as_bytes(),
2646                )));
2647            }
2648            bound_0Call::SELECTOR => {
2649                return self.handle_bound_uint(state, args_offset);
2650            }
2651            bound_1Call::SELECTOR => {
2652                return self.handle_bound_int(state, args_offset);
2653            }
2654            envExistsCall::SELECTOR => {
2655                let name = read_abi_string_arg(
2656                    &mut self.cx,
2657                    &state.memory,
2658                    args_offset,
2659                    0,
2660                    "symbolic vm.envExists",
2661                )?;
2662                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2663                    &mut self.cx,
2664                    U256::from(std::env::var_os(name).is_some()),
2665                )]));
2666            }
2667            envBool_0Call::SELECTOR => {
2668                let name = read_abi_string_arg(
2669                    &mut self.cx,
2670                    &state.memory,
2671                    args_offset,
2672                    0,
2673                    "symbolic vm.envBool",
2674                )?;
2675                let value = std::env::var(name)
2676                    .map_err(|_| SymbolicError::Unsupported("symbolic env var missing"))?;
2677                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2678                    &mut self.cx,
2679                    U256::from(parse_env_bool(&value)?),
2680                )]));
2681            }
2682            envUint_0Call::SELECTOR => {
2683                let name = read_abi_string_arg(
2684                    &mut self.cx,
2685                    &state.memory,
2686                    args_offset,
2687                    0,
2688                    "symbolic vm.envUint",
2689                )?;
2690                let value = std::env::var(name)
2691                    .map_err(|_| SymbolicError::Unsupported("symbolic env var missing"))?;
2692                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2693                    &mut self.cx,
2694                    parse_env_uint(&value)?,
2695                )]));
2696            }
2697            envInt_0Call::SELECTOR => {
2698                let name = read_abi_string_arg(
2699                    &mut self.cx,
2700                    &state.memory,
2701                    args_offset,
2702                    0,
2703                    "symbolic vm.envInt",
2704                )?;
2705                let value = std::env::var(name)
2706                    .map_err(|_| SymbolicError::Unsupported("symbolic env var missing"))?;
2707                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2708                    &mut self.cx,
2709                    parse_env_int(&value)?,
2710                )]));
2711            }
2712            envAddress_0Call::SELECTOR => {
2713                let name = read_abi_string_arg(
2714                    &mut self.cx,
2715                    &state.memory,
2716                    args_offset,
2717                    0,
2718                    "symbolic vm.envAddress",
2719                )?;
2720                let value = std::env::var(name)
2721                    .map_err(|_| SymbolicError::Unsupported("symbolic env var missing"))?;
2722                let address = parse_env_address(&value)?;
2723                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2724                    &mut self.cx,
2725                    address_word(address),
2726                )]));
2727            }
2728            envBytes32_0Call::SELECTOR => {
2729                let name = read_abi_string_arg(
2730                    &mut self.cx,
2731                    &state.memory,
2732                    args_offset,
2733                    0,
2734                    "symbolic vm.envBytes32",
2735                )?;
2736                let value = std::env::var(name)
2737                    .map_err(|_| SymbolicError::Unsupported("symbolic env var missing"))?;
2738                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2739                    &mut self.cx,
2740                    parse_env_bytes32(&value)?,
2741                )]));
2742            }
2743            envString_0Call::SELECTOR => {
2744                let name = read_abi_string_arg(
2745                    &mut self.cx,
2746                    &state.memory,
2747                    args_offset,
2748                    0,
2749                    "symbolic vm.envString",
2750                )?;
2751                let value = std::env::var(name)
2752                    .map_err(|_| SymbolicError::Unsupported("symbolic env var missing"))?;
2753                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2754                    &mut self.cx,
2755                    value.as_bytes(),
2756                )));
2757            }
2758            envBytes_0Call::SELECTOR => {
2759                let name = read_abi_string_arg(
2760                    &mut self.cx,
2761                    &state.memory,
2762                    args_offset,
2763                    0,
2764                    "symbolic vm.envBytes",
2765                )?;
2766                let value = std::env::var(name)
2767                    .map_err(|_| SymbolicError::Unsupported("symbolic env var missing"))?;
2768                let bytes = parse_env_bytes(&value)?;
2769                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2770                    &mut self.cx,
2771                    &bytes,
2772                )));
2773            }
2774            envBool_1Call::SELECTOR
2775            | envUint_1Call::SELECTOR
2776            | envInt_1Call::SELECTOR
2777            | envAddress_1Call::SELECTOR
2778            | envBytes32_1Call::SELECTOR
2779            | envString_1Call::SELECTOR
2780            | envBytes_1Call::SELECTOR => {
2781                let values = decode_cheatcode_args(
2782                    &mut self.cx,
2783                    state,
2784                    in_offset,
2785                    in_size,
2786                    vec![DynSolType::String, DynSolType::String],
2787                )?;
2788                let name = dyn_string(&values[0])?;
2789                let delimiter = dyn_string(&values[1])?;
2790                let value = std::env::var(name)
2791                    .map_err(|_| SymbolicError::Unsupported("symbolic env var missing"))?;
2792                let value = if selector == envBool_1Call::SELECTOR {
2793                    parse_env_array(&value, &delimiter, parse_env_bool_value)?
2794                } else if selector == envUint_1Call::SELECTOR {
2795                    parse_env_array(&value, &delimiter, parse_env_uint_value)?
2796                } else if selector == envInt_1Call::SELECTOR {
2797                    parse_env_array(&value, &delimiter, parse_env_int_value)?
2798                } else if selector == envAddress_1Call::SELECTOR {
2799                    parse_env_array(&value, &delimiter, parse_env_address_value)?
2800                } else if selector == envBytes32_1Call::SELECTOR {
2801                    parse_env_array(&value, &delimiter, parse_env_bytes32_value)?
2802                } else if selector == envString_1Call::SELECTOR {
2803                    parse_env_array(&value, &delimiter, parse_env_string_value)?
2804                } else {
2805                    parse_env_array(&value, &delimiter, parse_env_bytes_value)?
2806                };
2807                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_value_return(
2808                    &mut self.cx,
2809                    value,
2810                )));
2811            }
2812            envOr_0Call::SELECTOR => {
2813                let name = read_abi_string_arg(
2814                    &mut self.cx,
2815                    &state.memory,
2816                    args_offset,
2817                    0,
2818                    "symbolic vm.envOr",
2819                )?;
2820                let value = match std::env::var(name) {
2821                    Ok(value) => U256::from(parse_env_bool(&value)?),
2822                    Err(_) => read_abi_concrete_word_arg(
2823                        &mut self.cx,
2824                        &state.memory,
2825                        args_offset,
2826                        1,
2827                        "symbolic vm.envOr",
2828                    )?,
2829                };
2830                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2831                    &mut self.cx,
2832                    value,
2833                )]));
2834            }
2835            envOr_1Call::SELECTOR
2836            | envOr_2Call::SELECTOR
2837            | envOr_3Call::SELECTOR
2838            | envOr_4Call::SELECTOR => {
2839                let name = read_abi_string_arg(
2840                    &mut self.cx,
2841                    &state.memory,
2842                    args_offset,
2843                    0,
2844                    "symbolic vm.envOr",
2845                )?;
2846                let default = read_abi_concrete_word_arg(
2847                    &mut self.cx,
2848                    &state.memory,
2849                    args_offset,
2850                    1,
2851                    "symbolic vm.envOr",
2852                )?;
2853                let value = match std::env::var(name) {
2854                    Ok(value) if selector == envOr_1Call::SELECTOR => parse_env_uint(&value)?,
2855                    Ok(value) if selector == envOr_2Call::SELECTOR => parse_env_int(&value)?,
2856                    Ok(value) if selector == envOr_3Call::SELECTOR => {
2857                        address_word(parse_env_address(&value)?)
2858                    }
2859                    Ok(value) => parse_env_bytes32(&value)?,
2860                    Err(_) => default,
2861                };
2862                return Ok(CheatcodeOutcome::Continue(vec![SymExpr::constant(
2863                    &mut self.cx,
2864                    value,
2865                )]));
2866            }
2867            envOr_5Call::SELECTOR => {
2868                let values = decode_cheatcode_args(
2869                    &mut self.cx,
2870                    state,
2871                    in_offset,
2872                    in_size,
2873                    vec![DynSolType::String, DynSolType::String],
2874                )?;
2875                let name = dyn_string(&values[0])?;
2876                let value = std::env::var(name).unwrap_or(dyn_string(&values[1])?);
2877                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2878                    &mut self.cx,
2879                    value.as_bytes(),
2880                )));
2881            }
2882            envOr_6Call::SELECTOR => {
2883                let values = decode_cheatcode_args(
2884                    &mut self.cx,
2885                    state,
2886                    in_offset,
2887                    in_size,
2888                    vec![DynSolType::String, DynSolType::Bytes],
2889                )?;
2890                let name = dyn_string(&values[0])?;
2891                let value = match std::env::var(name) {
2892                    Ok(value) => parse_env_bytes(&value)?,
2893                    Err(_) => dyn_bytes(&values[1])?,
2894                };
2895                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2896                    &mut self.cx,
2897                    &value,
2898                )));
2899            }
2900            envOr_7Call::SELECTOR
2901            | envOr_8Call::SELECTOR
2902            | envOr_9Call::SELECTOR
2903            | envOr_10Call::SELECTOR
2904            | envOr_11Call::SELECTOR
2905            | envOr_12Call::SELECTOR
2906            | envOr_13Call::SELECTOR => {
2907                let element_ty = if selector == envOr_7Call::SELECTOR {
2908                    DynSolType::Bool
2909                } else if selector == envOr_8Call::SELECTOR {
2910                    DynSolType::Uint(256)
2911                } else if selector == envOr_9Call::SELECTOR {
2912                    DynSolType::Int(256)
2913                } else if selector == envOr_10Call::SELECTOR {
2914                    DynSolType::Address
2915                } else if selector == envOr_11Call::SELECTOR {
2916                    DynSolType::FixedBytes(32)
2917                } else if selector == envOr_12Call::SELECTOR {
2918                    DynSolType::String
2919                } else {
2920                    DynSolType::Bytes
2921                };
2922                let values = decode_cheatcode_args(
2923                    &mut self.cx,
2924                    state,
2925                    in_offset,
2926                    in_size,
2927                    vec![
2928                        DynSolType::String,
2929                        DynSolType::String,
2930                        DynSolType::Array(Box::new(element_ty)),
2931                    ],
2932                )?;
2933                let name = dyn_string(&values[0])?;
2934                let delimiter = dyn_string(&values[1])?;
2935                let value = match std::env::var(name) {
2936                    Ok(value) if selector == envOr_7Call::SELECTOR => {
2937                        parse_env_array(&value, &delimiter, parse_env_bool_value)?
2938                    }
2939                    Ok(value) if selector == envOr_8Call::SELECTOR => {
2940                        parse_env_array(&value, &delimiter, parse_env_uint_value)?
2941                    }
2942                    Ok(value) if selector == envOr_9Call::SELECTOR => {
2943                        parse_env_array(&value, &delimiter, parse_env_int_value)?
2944                    }
2945                    Ok(value) if selector == envOr_10Call::SELECTOR => {
2946                        parse_env_array(&value, &delimiter, parse_env_address_value)?
2947                    }
2948                    Ok(value) if selector == envOr_11Call::SELECTOR => {
2949                        parse_env_array(&value, &delimiter, parse_env_bytes32_value)?
2950                    }
2951                    Ok(value) if selector == envOr_12Call::SELECTOR => {
2952                        parse_env_array(&value, &delimiter, parse_env_string_value)?
2953                    }
2954                    Ok(value) => parse_env_array(&value, &delimiter, parse_env_bytes_value)?,
2955                    Err(_) => values[2].clone(),
2956                };
2957                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_value_return(
2958                    &mut self.cx,
2959                    value,
2960                )));
2961            }
2962            ffiCall::SELECTOR => {
2963                if !state.ffi_enabled {
2964                    return Err(SymbolicError::Unsupported("symbolic ffi disabled"));
2965                }
2966                let values = decode_cheatcode_args(
2967                    &mut self.cx,
2968                    state,
2969                    in_offset,
2970                    in_size,
2971                    vec![DynSolType::Array(Box::new(DynSolType::String))],
2972                )?;
2973                let args = dyn_string_array(&values[0])?;
2974                if args.is_empty() || args[0].is_empty() {
2975                    return Err(SymbolicError::Unsupported("symbolic ffi empty command"));
2976                }
2977                let output = Command::new(&args[0])
2978                    .args(&args[1..])
2979                    .output()
2980                    .map_err(|_| SymbolicError::Unsupported("symbolic ffi command"))?;
2981                if !output.status.success() {
2982                    return Err(SymbolicError::Unsupported("symbolic ffi command failed"));
2983                }
2984                let stdout = String::from_utf8(output.stdout)
2985                    .map_err(|_| SymbolicError::Unsupported("symbolic ffi stdout"))?;
2986                let trimmed = stdout.trim();
2987                let bytes = hex::decode(trimmed).unwrap_or_else(|_| trimmed.as_bytes().to_vec());
2988                return Ok(CheatcodeOutcome::ContinueData(abi_concrete_bytes_return(
2989                    &mut self.cx,
2990                    &bytes,
2991                )));
2992            }
2993            assertTrue_0Call::SELECTOR | assertTrue_1Call::SELECTOR => {
2994                let word = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
2995                let condition = word.nonzero_bool(&mut self.cx);
2996                return self.handle_assertion(state, condition);
2997            }
2998            assertFalse_0Call::SELECTOR | assertFalse_1Call::SELECTOR => {
2999                let word = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3000                let condition = word.into_zero_bool(&mut self.cx);
3001                return self.handle_assertion(state, condition);
3002            }
3003            assertEq_2Call::SELECTOR
3004            | assertEq_3Call::SELECTOR
3005            | assertEq_4Call::SELECTOR
3006            | assertEq_5Call::SELECTOR
3007            | assertEq_6Call::SELECTOR
3008            | assertEq_7Call::SELECTOR
3009            | assertEq_8Call::SELECTOR
3010            | assertEq_9Call::SELECTOR
3011            | assertEq_0Call::SELECTOR
3012            | assertEq_1Call::SELECTOR => {
3013                let left = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3014                let right = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
3015                let condition = SymBoolExpr::eq(&mut self.cx, left, right);
3016                return self.handle_assertion(state, condition);
3017            }
3018            assertEq_10Call::SELECTOR | assertEq_11Call::SELECTOR => {
3019                let values = decode_cheatcode_args(
3020                    &mut self.cx,
3021                    state,
3022                    in_offset,
3023                    in_size,
3024                    if selector == assertEq_10Call::SELECTOR {
3025                        vec![DynSolType::String, DynSolType::String]
3026                    } else {
3027                        vec![DynSolType::String, DynSolType::String, DynSolType::String]
3028                    },
3029                )?;
3030                let condition = SymBoolExpr::constant(
3031                    &mut self.cx,
3032                    dyn_string(&values[0])? == dyn_string(&values[1])?,
3033                );
3034                return self.handle_assertion(state, condition);
3035            }
3036            assertEq_12Call::SELECTOR | assertEq_13Call::SELECTOR => {
3037                let values = decode_cheatcode_args(
3038                    &mut self.cx,
3039                    state,
3040                    in_offset,
3041                    in_size,
3042                    if selector == assertEq_12Call::SELECTOR {
3043                        vec![DynSolType::Bytes, DynSolType::Bytes]
3044                    } else {
3045                        vec![DynSolType::Bytes, DynSolType::Bytes, DynSolType::String]
3046                    },
3047                )?;
3048                let condition = SymBoolExpr::constant(
3049                    &mut self.cx,
3050                    dyn_bytes(&values[0])? == dyn_bytes(&values[1])?,
3051                );
3052                return self.handle_assertion(state, condition);
3053            }
3054            assertEq_14Call::SELECTOR
3055            | assertEq_15Call::SELECTOR
3056            | assertEq_16Call::SELECTOR
3057            | assertEq_17Call::SELECTOR
3058            | assertEq_18Call::SELECTOR
3059            | assertEq_19Call::SELECTOR
3060            | assertEq_20Call::SELECTOR
3061            | assertEq_21Call::SELECTOR
3062            | assertEq_22Call::SELECTOR
3063            | assertEq_23Call::SELECTOR
3064            | assertEq_24Call::SELECTOR
3065            | assertEq_25Call::SELECTOR
3066            | assertEq_26Call::SELECTOR
3067            | assertEq_27Call::SELECTOR => {
3068                let element_ty = array_assertion_element_type(selector)?;
3069                let values = decode_cheatcode_args(
3070                    &mut self.cx,
3071                    state,
3072                    in_offset,
3073                    in_size,
3074                    if selector_has_string_reason(selector) {
3075                        vec![
3076                            DynSolType::Array(Box::new(element_ty.clone())),
3077                            DynSolType::Array(Box::new(element_ty)),
3078                            DynSolType::String,
3079                        ]
3080                    } else {
3081                        vec![
3082                            DynSolType::Array(Box::new(element_ty.clone())),
3083                            DynSolType::Array(Box::new(element_ty)),
3084                        ]
3085                    },
3086                )?;
3087                let condition = SymBoolExpr::constant(&mut self.cx, values[0] == values[1]);
3088                return self.handle_assertion(state, condition);
3089            }
3090            assertEqDecimal_0Call::SELECTOR
3091            | assertEqDecimal_1Call::SELECTOR
3092            | assertEqDecimal_2Call::SELECTOR
3093            | assertEqDecimal_3Call::SELECTOR => {
3094                let left = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3095                let right = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
3096                let condition = SymBoolExpr::eq(&mut self.cx, left, right);
3097                return self.handle_assertion(state, condition);
3098            }
3099            assertNotEq_2Call::SELECTOR
3100            | assertNotEq_3Call::SELECTOR
3101            | assertNotEq_4Call::SELECTOR
3102            | assertNotEq_5Call::SELECTOR
3103            | assertNotEq_6Call::SELECTOR
3104            | assertNotEq_7Call::SELECTOR
3105            | assertNotEq_8Call::SELECTOR
3106            | assertNotEq_9Call::SELECTOR
3107            | assertNotEq_0Call::SELECTOR
3108            | assertNotEq_1Call::SELECTOR => {
3109                let left = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3110                let right = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
3111                let condition = SymBoolExpr::eq(&mut self.cx, left, right);
3112                let condition = condition.not(&mut self.cx);
3113                return self.handle_assertion(state, condition);
3114            }
3115            assertNotEq_10Call::SELECTOR | assertNotEq_11Call::SELECTOR => {
3116                let values = decode_cheatcode_args(
3117                    &mut self.cx,
3118                    state,
3119                    in_offset,
3120                    in_size,
3121                    if selector == assertNotEq_10Call::SELECTOR {
3122                        vec![DynSolType::String, DynSolType::String]
3123                    } else {
3124                        vec![DynSolType::String, DynSolType::String, DynSolType::String]
3125                    },
3126                )?;
3127                let condition = SymBoolExpr::constant(
3128                    &mut self.cx,
3129                    dyn_string(&values[0])? != dyn_string(&values[1])?,
3130                );
3131                return self.handle_assertion(state, condition);
3132            }
3133            assertNotEq_12Call::SELECTOR | assertNotEq_13Call::SELECTOR => {
3134                let values = decode_cheatcode_args(
3135                    &mut self.cx,
3136                    state,
3137                    in_offset,
3138                    in_size,
3139                    if selector == assertNotEq_12Call::SELECTOR {
3140                        vec![DynSolType::Bytes, DynSolType::Bytes]
3141                    } else {
3142                        vec![DynSolType::Bytes, DynSolType::Bytes, DynSolType::String]
3143                    },
3144                )?;
3145                let condition = SymBoolExpr::constant(
3146                    &mut self.cx,
3147                    dyn_bytes(&values[0])? != dyn_bytes(&values[1])?,
3148                );
3149                return self.handle_assertion(state, condition);
3150            }
3151            assertNotEq_14Call::SELECTOR
3152            | assertNotEq_15Call::SELECTOR
3153            | assertNotEq_16Call::SELECTOR
3154            | assertNotEq_17Call::SELECTOR
3155            | assertNotEq_18Call::SELECTOR
3156            | assertNotEq_19Call::SELECTOR
3157            | assertNotEq_20Call::SELECTOR
3158            | assertNotEq_21Call::SELECTOR
3159            | assertNotEq_22Call::SELECTOR
3160            | assertNotEq_23Call::SELECTOR
3161            | assertNotEq_24Call::SELECTOR
3162            | assertNotEq_25Call::SELECTOR
3163            | assertNotEq_26Call::SELECTOR
3164            | assertNotEq_27Call::SELECTOR => {
3165                let element_ty = array_assertion_element_type(selector)?;
3166                let values = decode_cheatcode_args(
3167                    &mut self.cx,
3168                    state,
3169                    in_offset,
3170                    in_size,
3171                    if selector_has_string_reason(selector) {
3172                        vec![
3173                            DynSolType::Array(Box::new(element_ty.clone())),
3174                            DynSolType::Array(Box::new(element_ty)),
3175                            DynSolType::String,
3176                        ]
3177                    } else {
3178                        vec![
3179                            DynSolType::Array(Box::new(element_ty.clone())),
3180                            DynSolType::Array(Box::new(element_ty)),
3181                        ]
3182                    },
3183                )?;
3184                let condition = SymBoolExpr::constant(&mut self.cx, values[0] != values[1]);
3185                return self.handle_assertion(state, condition);
3186            }
3187            assertLt_0Call::SELECTOR | assertLt_1Call::SELECTOR => {
3188                let left = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3189                let right = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
3190                let condition = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ult, left, right);
3191                return self.handle_assertion(state, condition);
3192            }
3193            assertLe_0Call::SELECTOR | assertLe_1Call::SELECTOR => {
3194                let left = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3195                let right = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
3196                let condition = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, left, right);
3197                return self.handle_assertion(state, condition);
3198            }
3199            assertGt_0Call::SELECTOR | assertGt_1Call::SELECTOR => {
3200                let left = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3201                let right = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
3202                let condition = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ugt, left, right);
3203                return self.handle_assertion(state, condition);
3204            }
3205            assertGe_0Call::SELECTOR | assertGe_1Call::SELECTOR => {
3206                let left = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3207                let right = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
3208                let condition = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Uge, left, right);
3209                return self.handle_assertion(state, condition);
3210            }
3211            assertLt_2Call::SELECTOR | assertLt_3Call::SELECTOR => {
3212                let left = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3213                let right = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
3214                let condition = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Slt, left, right);
3215                return self.handle_assertion(state, condition);
3216            }
3217            assertGt_2Call::SELECTOR | assertGt_3Call::SELECTOR => {
3218                let left = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3219                let right = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
3220                let condition = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Sgt, left, right);
3221                return self.handle_assertion(state, condition);
3222            }
3223            assertLe_2Call::SELECTOR | assertLe_3Call::SELECTOR => {
3224                let left = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3225                let right = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
3226                let condition = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Sgt, left, right);
3227                let condition = condition.not(&mut self.cx);
3228                return self.handle_assertion(state, condition);
3229            }
3230            assertGe_2Call::SELECTOR | assertGe_3Call::SELECTOR => {
3231                let left = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3232                let right = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 1)?;
3233                let condition = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Slt, left, right);
3234                let condition = condition.not(&mut self.cx);
3235                return self.handle_assertion(state, condition);
3236            }
3237            randomUint_0Call::SELECTOR => {
3238                return Ok(CheatcodeOutcome::Continue(vec![
3239                    state.fresh_word(&mut self.cx, "vmRandomUint"),
3240                ]));
3241            }
3242            randomUint_2Call::SELECTOR => {
3243                let bits = read_abi_constrained_word_arg(
3244                    &mut self.cx,
3245                    state,
3246                    args_offset,
3247                    0,
3248                    "symbolic randomUint bits",
3249                )?;
3250                Self::validate_symbolic_integer_bits(bits, "symbolic randomUint bits")?;
3251                return Ok(CheatcodeOutcome::Continue(vec![
3252                    state.fresh_bounded_uint(&mut self.cx, bits),
3253                ]));
3254            }
3255            randomUint_1Call::SELECTOR => {
3256                let min = state.memory.load_word(&mut self.cx, in_offset + 4)?;
3257                let max = state.memory.load_word(&mut self.cx, in_offset + 36)?;
3258                let value = state.fresh_word(&mut self.cx, "vmRandomUintRange");
3259                state.constraints.push(SymBoolExpr::cmp_word_expr(
3260                    &mut self.cx,
3261                    SymCmpOp::Uge,
3262                    &value,
3263                    min,
3264                ));
3265                state.constraints.push(SymBoolExpr::cmp_word_expr(
3266                    &mut self.cx,
3267                    SymCmpOp::Ule,
3268                    &value,
3269                    max,
3270                ));
3271                return Ok(CheatcodeOutcome::Continue(vec![value]));
3272            }
3273            randomInt_0Call::SELECTOR => {
3274                return Ok(CheatcodeOutcome::Continue(vec![
3275                    state.fresh_word(&mut self.cx, "vmRandomInt"),
3276                ]));
3277            }
3278            randomInt_1Call::SELECTOR => {
3279                let bits = read_abi_constrained_word_arg(
3280                    &mut self.cx,
3281                    state,
3282                    args_offset,
3283                    0,
3284                    "symbolic randomInt bits",
3285                )?;
3286                Self::validate_symbolic_integer_bits(bits, "symbolic randomInt bits")?;
3287                return Ok(CheatcodeOutcome::Continue(vec![
3288                    state.fresh_bounded_int(&mut self.cx, bits),
3289                ]));
3290            }
3291            randomAddressCall::SELECTOR => {
3292                let value = state.fresh_bounded_uint(&mut self.cx, U256::from(160));
3293                return Ok(CheatcodeOutcome::Continue(vec![value]));
3294            }
3295            randomBoolCall::SELECTOR => {
3296                let value = state.fresh_bounded_uint(&mut self.cx, U256::from(1));
3297                return Ok(CheatcodeOutcome::Continue(vec![value]));
3298            }
3299            randomBytesCall::SELECTOR => {
3300                let len = read_abi_word_arg(&mut self.cx, &state.memory, args_offset, 0)?;
3301                let max_limit = self.config.max_dynamic_length as usize;
3302                let max_len = state
3303                    .upper_bound_usize(&mut self.cx, &len)
3304                    .filter(|len| *len <= max_limit)
3305                    .map(Ok)
3306                    .unwrap_or_else(|| {
3307                        self.solver_upper_bound_usize(
3308                            state,
3309                            &len,
3310                            max_limit,
3311                            "symbolic randomBytes length",
3312                        )
3313                    })?;
3314                let bytes = state.fresh_bytes(&mut self.cx, max_len);
3315                return Ok(CheatcodeOutcome::ContinueData(abi_bytes_return_with_len(
3316                    &mut self.cx,
3317                    len,
3318                    bytes,
3319                )));
3320            }
3321            randomBytes4Call::SELECTOR => {
3322                let value = state.fresh_bounded_uint(&mut self.cx, U256::from(32));
3323                return Ok(CheatcodeOutcome::Continue(vec![shift_left(&mut self.cx, value, 224)]));
3324            }
3325            randomBytes8Call::SELECTOR => {
3326                let value = state.fresh_bounded_uint(&mut self.cx, U256::from(64));
3327                return Ok(CheatcodeOutcome::Continue(vec![shift_left(&mut self.cx, value, 192)]));
3328            }
3329
3330            _ => {}
3331        }
3332
3333        Err(SymbolicError::Unsupported("symbolic Foundry cheatcode"))
3334    }
3335
3336    pub(super) fn handle_symbolic_vm_cheatcode(
3337        &mut self,
3338        state: &mut PathState,
3339        selector: [u8; 4],
3340        in_offset: usize,
3341    ) -> Result<SymReturnData, SymbolicError> {
3342        let Some(cheatcode) = SymbolicVmCheatcode::from_selector(selector) else {
3343            return Err(SymbolicError::Unsupported("symbolic VM compatibility cheatcode"));
3344        };
3345        let args_offset = in_offset + 4;
3346
3347        match cheatcode {
3348            SymbolicVmCheatcode::CreateUintBits(bits) => {
3349                let value = if bits == 256 {
3350                    state.fresh_word(&mut self.cx, "svm")
3351                } else {
3352                    state.fresh_bounded_uint(&mut self.cx, U256::from(bits))
3353                };
3354                Ok(SymReturnData::from_words(&mut self.cx, vec![value]))
3355            }
3356            SymbolicVmCheatcode::CreateIntBits(bits) => {
3357                let value = if bits == 256 {
3358                    state.fresh_word(&mut self.cx, "svm")
3359                } else {
3360                    state.fresh_bounded_int(&mut self.cx, U256::from(bits))
3361                };
3362                Ok(SymReturnData::from_words(&mut self.cx, vec![value]))
3363            }
3364            SymbolicVmCheatcode::CreateBytesFixed(bytes) => {
3365                let value = if bytes == 32 {
3366                    state.fresh_word(&mut self.cx, "svm")
3367                } else {
3368                    let value = state.fresh_bounded_uint(&mut self.cx, U256::from(bytes * 8));
3369                    shift_left(&mut self.cx, value, (32 - bytes) * 8)
3370                };
3371                Ok(SymReturnData::from_words(&mut self.cx, vec![value]))
3372            }
3373            SymbolicVmCheatcode::CreateUint => {
3374                let bits = read_abi_constrained_word_arg(
3375                    &mut self.cx,
3376                    state,
3377                    args_offset,
3378                    0,
3379                    "symbolic svm.create integer bits",
3380                )?;
3381                Self::validate_symbolic_integer_bits(bits, "symbolic svm.create integer bits")?;
3382                let value = state.fresh_bounded_uint(&mut self.cx, bits);
3383                Ok(SymReturnData::from_words(&mut self.cx, vec![value]))
3384            }
3385            SymbolicVmCheatcode::CreateInt => {
3386                let bits = read_abi_constrained_word_arg(
3387                    &mut self.cx,
3388                    state,
3389                    args_offset,
3390                    0,
3391                    "symbolic svm.create integer bits",
3392                )?;
3393                Self::validate_symbolic_integer_bits(bits, "symbolic svm.create integer bits")?;
3394                let value = state.fresh_bounded_int(&mut self.cx, bits);
3395                Ok(SymReturnData::from_words(&mut self.cx, vec![value]))
3396            }
3397            SymbolicVmCheatcode::CreateAddress => {
3398                let value = state.fresh_bounded_uint(&mut self.cx, U256::from(160));
3399                Ok(SymReturnData::from_words(&mut self.cx, vec![value]))
3400            }
3401            SymbolicVmCheatcode::CreateBool => {
3402                let value = state.fresh_bounded_uint(&mut self.cx, U256::from(1));
3403                Ok(SymReturnData::from_words(&mut self.cx, vec![value]))
3404            }
3405            SymbolicVmCheatcode::CreateBytes => {
3406                let bytes =
3407                    state.fresh_bytes(&mut self.cx, self.config.default_dynamic_length as usize);
3408                Ok(abi_bytes_return(&mut self.cx, bytes))
3409            }
3410            SymbolicVmCheatcode::CreateBytesSized => {
3411                let len = read_abi_constrained_word_arg(
3412                    &mut self.cx,
3413                    state,
3414                    args_offset,
3415                    0,
3416                    "symbolic svm.createBytes length",
3417                )?;
3418                let len = usize::try_from(len)
3419                    .ok()
3420                    .filter(|len| *len <= self.config.max_calldata_bytes as usize)
3421                    .ok_or(SymbolicError::Unsupported("symbolic svm.createBytes length"))?;
3422                let bytes = state.fresh_bytes(&mut self.cx, len);
3423                Ok(abi_bytes_return(&mut self.cx, bytes))
3424            }
3425            SymbolicVmCheatcode::CreateString => {
3426                let bytes = state.fresh_printable_ascii_bytes(
3427                    &mut self.cx,
3428                    self.config.default_dynamic_length as usize,
3429                );
3430                Ok(abi_bytes_return(&mut self.cx, bytes))
3431            }
3432            SymbolicVmCheatcode::CreateStringSized => {
3433                let len = read_abi_constrained_word_arg(
3434                    &mut self.cx,
3435                    state,
3436                    args_offset,
3437                    0,
3438                    "symbolic svm.createString length",
3439                )?;
3440                let len = usize::try_from(len)
3441                    .ok()
3442                    .filter(|len| *len <= self.config.max_calldata_bytes as usize)
3443                    .ok_or(SymbolicError::Unsupported("symbolic svm.createString length"))?;
3444                let bytes = state.fresh_printable_ascii_bytes(&mut self.cx, len);
3445                Ok(abi_bytes_return(&mut self.cx, bytes))
3446            }
3447            SymbolicVmCheatcode::CreateCalldata => {
3448                let max = self.config.max_calldata_bytes as usize;
3449                let len = if max < 4 {
3450                    max
3451                } else {
3452                    (self.config.default_dynamic_length as usize).max(4).min(max)
3453                };
3454                let bytes = state.fresh_bytes(&mut self.cx, len);
3455                Ok(abi_bytes_return(&mut self.cx, bytes))
3456            }
3457            SymbolicVmCheatcode::EnableSymbolicStorage => {
3458                let target =
3459                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
3460                state.world.enable_arbitrary_storage(target, false);
3461                Ok(SymReturnData::empty(&mut self.cx))
3462            }
3463            SymbolicVmCheatcode::SnapshotStorage => {
3464                let _target =
3465                    read_abi_address_or_symbolic_slot_arg(&mut self.cx, state, args_offset, 0)?;
3466                let id = state.world.snapshot_state();
3467                let id = SymExpr::constant(&mut self.cx, id);
3468                Ok(SymReturnData::from_words(&mut self.cx, vec![id]))
3469            }
3470            SymbolicVmCheatcode::SnapshotState => {
3471                let id = state.world.snapshot_state();
3472                let id = SymExpr::constant(&mut self.cx, id);
3473                Ok(SymReturnData::from_words(&mut self.cx, vec![id]))
3474            }
3475        }
3476    }
3477}