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::ExceptionalHalt);
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 = self.solver_upper_bound_usize(
35                    state,
36                    &size,
37                    max_limit,
38                    "symbolic CREATE initcode size",
39                )?;
40                BoundedCopySize::Symbolic { size, max_size }
41            }
42        };
43        let salt =
44            if matches!(kind, CreateKind::Create2) { Some(state.stack.pop()?) } else { None };
45
46        size.expand_memory(&mut self.cx, &mut state.memory, offset.clone());
47
48        let initcode = match &size {
49            BoundedCopySize::Concrete(size) => {
50                if let Some(offset) = state.constrained_usize(&mut self.cx, &offset) {
51                    let bytes = state.memory.read_bytes(&mut self.cx, offset, *size);
52                    SymCode::from_bytes(&mut self.cx, bytes)
53                } else {
54                    SymCode::from_memory_offset(&mut self.cx, &state.memory, offset, *size)
55                }
56            }
57            BoundedCopySize::Symbolic { size, max_size } => SymCode::from_memory_symbolic_size(
58                &mut self.cx,
59                &state.memory,
60                offset,
61                size.clone(),
62                *max_size,
63            ),
64        };
65        let (created_word, created) = match kind {
66            CreateKind::Create => {
67                let nonce = state.world.nonce(executor, state.address)?;
68                let address = state.address.create(nonce);
69                (SymExpr::constant(&mut self.cx, address_word(address)), address)
70            }
71            CreateKind::Create2 => create2_address_word(
72                &mut self.cx,
73                state,
74                state.address,
75                salt.expect("CREATE2 salt exists"),
76                &initcode,
77            )?,
78        };
79
80        if !self.prepare_create_value_transfer(executor, state, worklist, value.clone())? {
81            return Ok(StepOutcome::Continue);
82        }
83
84        let mut failure_world = state.world.clone();
85        failure_world.increment_nonce(executor, state.address)?;
86
87        if failure_world.has_code_or_nonce(&mut self.cx, executor, created)? {
88            state.world = failure_world;
89            state.return_data = SymReturnData::empty(&mut self.cx);
90            state.stack.push(SymExpr::zero(&mut self.cx))?;
91            return Ok(StepOutcome::Continue);
92        }
93
94        let calldata = SymBytes::empty(&mut self.cx);
95        let calldata = SymCalldata::from_bytes(&mut self.cx, calldata);
96        let mut frame = CallFrame::new(
97            &mut self.cx,
98            created,
99            created,
100            state.address,
101            value.clone(),
102            false,
103            calldata,
104        );
105        frame.address_word = created_word.clone();
106        frame.caller_word = state.address_word.clone();
107        let mut child = state.child(frame);
108        let pending_expected_creates = std::mem::take(&mut child.expected_creates);
109        child.world = failure_world.clone();
110        child.world.mark_current_transaction_created(created);
111        child.world.set_nonce(created, 1);
112        child.world.transfer(&mut self.cx, executor, state.address, created, value);
113
114        let outcomes = self.execute_external_call(executor, child, &initcode, completed_paths)?;
115        if outcomes.is_empty() {
116            return Ok(StepOutcome::AssumeRejected);
117        }
118
119        let mut parents = VecDeque::with_capacity(outcomes.len());
120        for mut outcome in outcomes {
121            let runtime = &outcome.state.frame.return_data;
122            let spec_id: SpecId = executor.spec_id().into();
123            let mut rejected_runtime = false;
124            if matches!(outcome.status, CallStatus::Success) {
125                if runtime_exceeds_code_size_limit(&executor.evm_env().cfg_env, spec_id, runtime) {
126                    outcome.status = CallStatus::Revert;
127                    outcome.state.frame.return_data = SymReturnData::empty(&mut self.cx);
128                } else if runtime_has_rejected_prefix(&mut self.cx, spec_id, runtime)? {
129                    outcome.status = CallStatus::Revert;
130                    rejected_runtime = true;
131                }
132            }
133            match self.join_call_outcome(state, outcome, created)? {
134                JoinedCallOutcome::Rejected => {}
135                JoinedCallOutcome::Failure(mut parent) => {
136                    parent.return_data = SymReturnData::empty(&mut self.cx);
137                    *state = parent;
138                    return Ok(StepOutcome::Failure);
139                }
140                JoinedCallOutcome::ExceptionalHalt(mut parent) => {
141                    parent.return_data = SymReturnData::empty(&mut self.cx);
142                    parent.world = failure_world.clone();
143                    parent.stack.push(SymExpr::zero(&mut self.cx))?;
144                    parents.push_back(parent);
145                }
146                JoinedCallOutcome::ExpectedRevert { mut parent, .. } => {
147                    parent.return_data = SymReturnData::empty(&mut self.cx);
148                    parent.expected_creates = pending_expected_creates.clone();
149                    parent.world = failure_world.clone();
150                    parent.stack.push(created_word.clone())?;
151                    parents.push_back(parent);
152                }
153                JoinedCallOutcome::Success { mut parent, child } => {
154                    parent.return_data = SymReturnData::empty(&mut self.cx);
155                    let runtime = &child.frame.return_data;
156                    parent.world = child.world;
157                    parent.expected_emit = child.expected_emit;
158                    parent.expected_creates = pending_expected_creates.clone();
159                    self.observe_expected_create(&mut parent, state.address, kind, runtime)?;
160                    if !parent.world.is_destroyed(created) {
161                        parent.world.install_code(created, runtime.to_code(&mut self.cx)?);
162                        parent.world.set_nonce(created, 1);
163                    }
164                    parent.stack.push(created_word.clone())?;
165                    parents.push_back(parent);
166                }
167                JoinedCallOutcome::Revert { mut parent, child } => {
168                    parent.return_data = SymReturnData::empty(&mut self.cx);
169                    parent.world = failure_world.clone();
170                    if !rejected_runtime {
171                        parent.return_data = child.frame.return_data;
172                    }
173                    parent.stack.push(SymExpr::zero(&mut self.cx))?;
174                    parents.push_back(parent);
175                }
176            }
177        }
178
179        Ok(self.resume_parent_paths(state, worklist, parents))
180    }
181
182    pub(super) fn execute_external_call<FEN: FoundryEvmNetwork>(
183        &mut self,
184        executor: &Executor<FEN>,
185        initial: PathState,
186        code: &SymCode,
187        completed_paths: &mut usize,
188    ) -> Result<Vec<CallOutcome>, SymbolicError> {
189        let mut worklist = VecDeque::from([initial]);
190        let mut deferred_worklist = VecDeque::new();
191        self.execute_call_path_batch(
192            executor,
193            code,
194            &mut worklist,
195            &mut deferred_worklist,
196            completed_paths,
197            CallPathKind::External,
198        )
199    }
200}
201
202fn runtime_exceeds_code_size_limit(
203    cfg: &impl Cfg,
204    spec_id: SpecId,
205    runtime: &SymReturnData,
206) -> bool {
207    spec_id >= SpecId::SPURIOUS_DRAGON
208        && runtime.len_word.as_const().is_some()
209        && runtime.len() > cfg.max_code_size()
210}
211
212fn runtime_has_rejected_prefix(
213    cx: &mut SymCx,
214    spec_id: SpecId,
215    runtime: &SymReturnData,
216) -> Result<bool, SymbolicError> {
217    if spec_id < SpecId::LONDON || runtime.len() == 0 {
218        return Ok(false);
219    }
220    let first_byte = runtime.byte(cx, 0);
221    let Some(first_byte) = first_byte.as_const() else {
222        return Err(SymbolicError::Unsupported("CREATE with symbolic runtime prefix not modeled"));
223    };
224    Ok(first_byte == U256::from(0xef))
225}
foundry_evm_symbolic/executor/create.rs

foundry_evm_symbolic/executor/
create.rs
