Skip to main content

foundry_evm_symbolic/executor/
cheatcodes.rs

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