foundry_evm_symbolic/executor/
create.rs

1use super::*;
2
3impl SymbolicExecutor {
4    pub(super) fn create<FEN: FoundryEvmNetwork>(
5        &mut self,
6        executor: &Executor<FEN>,
7        state: &mut PathState,
8        worklist: &mut VecDeque<PathState>,
9        completed_paths: &mut usize,
10        kind: CreateKind,
11    ) -> Result<StepOutcome, SymbolicError> {
12        if state.is_static {
13            state.return_data = SymReturnData::empty(&mut self.cx);
14            return Ok(StepOutcome::Revert);
15        }
16
17        let offset = state.stack.peek(1)?.clone();
18        let size = state.stack.peek(2)?.clone();
19        if let Some(outcome) = self.guard_memory_range(executor, state, worklist, &offset, &size)? {
20            return Ok(outcome);
21        }
22
23        let value = state.stack.pop()?;
24        let offset = state.stack.pop()?;
25        let size = state.stack.pop()?;
26        let size = match state.constrained_usize_checked(&mut self.cx, &size) {
27            Some(Ok(size)) => BoundedCopySize::Concrete(size),
28            Some(Err(_)) => {
29                state.return_data = SymReturnData::empty(&mut self.cx);
30                return Ok(StepOutcome::Revert);
31            }
32            None => {
33                let max_limit = self.config.max_calldata_bytes as usize;
34                let max_size = state
35                    .upper_bound_usize(&mut self.cx, &size)
36                    .filter(|size| *size <= max_limit)
37                    .map(Ok)
38                    .unwrap_or_else(|| {
39                        self.solver_upper_bound_usize(
40                            state,
41                            &size,
42                            max_limit,
43                            "symbolic CREATE initcode size",
44                        )
45                    })?;
46                BoundedCopySize::Symbolic { size, max_size }
47            }
48        };
49        let salt =
50            if matches!(kind, CreateKind::Create2) { Some(state.stack.pop()?) } else { None };
51
52        size.expand_memory(&mut self.cx, &mut state.memory, offset.clone());
53
54        let initcode = match &size {
55            BoundedCopySize::Concrete(size) => {
56                if let Some(offset) = state.constrained_usize(&mut self.cx, &offset) {
57                    let bytes = state.memory.read_bytes(&mut self.cx, offset, *size);
58                    SymCode::from_bytes(&mut self.cx, bytes)
59                } else {
60                    SymCode::from_memory_offset(&mut self.cx, &state.memory, offset, *size)
61                }
62            }
63            BoundedCopySize::Symbolic { size, max_size } => SymCode::from_memory_symbolic_size(
64                &mut self.cx,
65                &state.memory,
66                offset,
67                size.clone(),
68                *max_size,
69            ),
70        };
71        let (created_word, created) = match kind {
72            CreateKind::Create => {
73                let nonce = state.world.nonce(executor, state.address)?;
74                let address = state.address.create(nonce);
75                (SymExpr::constant(&mut self.cx, address_word(address)), address)
76            }
77            CreateKind::Create2 => create2_address_word(
78                &mut self.cx,
79                state,
80                state.address,
81                salt.expect("CREATE2 salt exists"),
82                &initcode,
83            )?,
84        };
85
86        if !self.prepare_create_value_transfer(executor, state, worklist, value.clone())? {
87            return Ok(StepOutcome::Continue);
88        }
89
90        let mut failure_world = state.world.clone();
91        failure_world.increment_nonce(executor, state.address)?;
92
93        if failure_world.has_code_or_nonce(&mut self.cx, executor, created)? {
94            state.world = failure_world;
95            state.return_data = SymReturnData::empty(&mut self.cx);
96            state.stack.push(SymExpr::zero(&mut self.cx))?;
97            return Ok(StepOutcome::Continue);
98        }
99
100        let calldata = SymBytes::empty(&mut self.cx);
101        let calldata = SymCalldata::from_bytes(&mut self.cx, calldata);
102        let mut frame = CallFrame::new(
103            &mut self.cx,
104            created,
105            created,
106            state.address,
107            value.clone(),
108            false,
109            calldata,
110        );
111        frame.address_word = created_word.clone();
112        frame.caller_word = state.address_word.clone();
113        let mut child = state.child(frame);
114        let pending_expected_creates = std::mem::take(&mut child.expected_creates);
115        child.world = failure_world.clone();
116        child.world.mark_current_transaction_created(created);
117        child.world.set_nonce(created, 1);
118        child.world.transfer(&mut self.cx, executor, state.address, created, value);
119
120        let outcomes = self.execute_external_call(executor, child, &initcode, completed_paths)?;
121        if outcomes.is_empty() {
122            return Ok(StepOutcome::AssumeRejected);
123        }
124
125        let mut parents = VecDeque::with_capacity(outcomes.len());
126        for mut outcome in outcomes {
127            let runtime = &outcome.state.frame.return_data;
128            let spec_id: SpecId = executor.spec_id().into();
129            let mut rejected_runtime = false;
130            if matches!(outcome.status, CallStatus::Success) {
131                if runtime_exceeds_code_size_limit(&executor.evm_env().cfg_env, spec_id, runtime) {
132                    outcome.status = CallStatus::Revert;
133                    outcome.state.frame.return_data = SymReturnData::empty(&mut self.cx);
134                } else if runtime_has_rejected_prefix(&mut self.cx, spec_id, runtime)? {
135                    outcome.status = CallStatus::Revert;
136                    rejected_runtime = true;
137                }
138            }
139            match self.join_call_outcome(state, outcome, created)? {
140                JoinedCallOutcome::Rejected => {}
141                JoinedCallOutcome::Failure(mut parent) => {
142                    parent.return_data = SymReturnData::empty(&mut self.cx);
143                    *state = parent;
144                    return Ok(StepOutcome::Failure);
145                }
146                JoinedCallOutcome::ExceptionalHalt(mut parent) => {
147                    parent.return_data = SymReturnData::empty(&mut self.cx);
148                    parent.world = failure_world.clone();
149                    parent.stack.push(SymExpr::zero(&mut self.cx))?;
150                    parents.push_back(parent);
151                }
152                JoinedCallOutcome::ExpectedRevert { mut parent, child } => {
153                    parent.return_data = SymReturnData::empty(&mut self.cx);
154                    parent.block = child.block.clone();
155                    parent.expected_calls = child.expected_calls;
156                    parent.expected_creates = pending_expected_creates.clone();
157                    parent.call_mocks = child.call_mocks;
158                    parent.function_mocks = child.function_mocks;
159                    parent.world = failure_world.clone();
160                    parent.stack.push(created_word.clone())?;
161                    parents.push_back(parent);
162                }
163                JoinedCallOutcome::Success { mut parent, child } => {
164                    parent.return_data = SymReturnData::empty(&mut self.cx);
165                    parent.block = child.block.clone();
166                    let runtime = &child.frame.return_data;
167                    parent.world = child.world;
168                    parent.expected_emit = child.expected_emit;
169                    parent.expected_calls = child.expected_calls;
170                    parent.expected_creates = pending_expected_creates.clone();
171                    parent.call_mocks = child.call_mocks;
172                    parent.function_mocks = child.function_mocks;
173                    self.observe_expected_create(&mut parent, state.address, kind, runtime)?;
174                    if !parent.world.is_destroyed(created) {
175                        parent.world.install_code(created, runtime.to_code(&mut self.cx)?);
176                        parent.world.set_nonce(created, 1);
177                    }
178                    parent.stack.push(created_word.clone())?;
179                    parents.push_back(parent);
180                }
181                JoinedCallOutcome::Revert { mut parent, child } => {
182                    parent.return_data = SymReturnData::empty(&mut self.cx);
183                    parent.world = failure_world.clone();
184                    if rejected_runtime {
185                        parent.block = child.block;
186                        parent.expected_calls = child.expected_calls;
187                        parent.call_mocks = child.call_mocks;
188                        parent.function_mocks = child.function_mocks;
189                    } else {
190                        parent.return_data = child.frame.return_data;
191                    }
192                    parent.stack.push(SymExpr::zero(&mut self.cx))?;
193                    parents.push_back(parent);
194                }
195            }
196        }
197
198        Ok(self.resume_parent_paths(state, worklist, parents))
199    }
200
201    pub(super) fn execute_external_call<FEN: FoundryEvmNetwork>(
202        &mut self,
203        executor: &Executor<FEN>,
204        initial: PathState,
205        code: &SymCode,
206        completed_paths: &mut usize,
207    ) -> Result<Vec<CallOutcome>, SymbolicError> {
208        let mut worklist = VecDeque::from([initial]);
209        let mut deferred_worklist = VecDeque::new();
210        self.execute_call_path_batch(
211            executor,
212            code,
213            &mut worklist,
214            &mut deferred_worklist,
215            completed_paths,
216            CallPathKind::External,
217        )
218    }
219}
220
221fn runtime_exceeds_code_size_limit(
222    cfg: &impl Cfg,
223    spec_id: SpecId,
224    runtime: &SymReturnData,
225) -> bool {
226    spec_id >= SpecId::SPURIOUS_DRAGON
227        && !runtime.has_symbolic_len()
228        && runtime.len() > cfg.max_code_size()
229}
230
231fn runtime_has_rejected_prefix(
232    cx: &mut SymCx,
233    spec_id: SpecId,
234    runtime: &SymReturnData,
235) -> Result<bool, SymbolicError> {
236    if spec_id < SpecId::LONDON || runtime.len() == 0 {
237        return Ok(false);
238    }
239    let first_byte = runtime.byte(cx, 0);
240    let Some(first_byte) = first_byte.as_const() else {
241        return Err(SymbolicError::Unsupported("CREATE with symbolic runtime prefix not modeled"));
242    };
243    Ok(first_byte == U256::from(0xef))
244}
245
246#[cfg(test)]
247mod tests {
248    use super::*;
249    use foundry_evm::revm::context::CfgEnv;
250
251    #[test]
252    fn runtime_code_limit_uses_fork_default_without_override() {
253        let mut cx = SymCx::default();
254        let runtime = SymReturnData::from_concrete_bytes(&mut cx, vec![0; 24_577]);
255        let cfg = CfgEnv::<SpecId>::default();
256
257        assert!(runtime_exceeds_code_size_limit(&cfg, SpecId::SHANGHAI, &runtime));
258        assert!(!runtime_exceeds_code_size_limit(&cfg, SpecId::HOMESTEAD, &runtime));
259    }
260}
foundry_evm_symbolic/executor/create.rs

foundry_evm_symbolic/executor/
create.rs
