foundry_evm_symbolic/executor/
opcodes.rs

1use super::*;
2
3enum MappingStorageProvenance {
4    None,
5    Exact(SymbolicMappingProvenance),
6    Fork { equality: Vec<SymBoolExpr>, inequality: Vec<SymBoolExpr> },
7}
8
9impl SymbolicExecutor {
10    fn classify_mapping_match(
11        &mut self,
12        state: &PathState,
13        matches: SymBoolExpr,
14        provenance: SymbolicMappingProvenance,
15    ) -> Result<Option<MappingStorageProvenance>, SymbolicError> {
16        let does_not_match = matches.clone().not(&mut self.cx);
17        let (inequality, inequality_is_sat) =
18            self.constraints_with_condition(state, does_not_match)?;
19        if !inequality_is_sat {
20            return Ok(Some(MappingStorageProvenance::Exact(provenance)));
21        }
22        let (equality, equality_is_sat) = self.constraints_with_condition(state, matches)?;
23        Ok(equality_is_sat.then_some(MappingStorageProvenance::Fork { equality, inequality }))
24    }
25
26    fn observed_mapping_chain(
27        &mut self,
28        state: &PathState,
29        hash: &SymExpr,
30    ) -> Option<(SymExpr, Vec<SymExpr>)> {
31        let account = state.storage_address;
32        let mut current = hash.clone();
33        let mut keys = Vec::new();
34        let mut visited = Vec::new();
35        loop {
36            if visited.contains(&current) {
37                return None;
38            }
39            visited.push(current.clone());
40            let Some(bytes) =
41                state.mapping_hook_keccak_preimages.get(&(account, current.clone())).cloned()
42            else {
43                keys.reverse();
44                return Some((current, keys));
45            };
46            if bytes.len() != 64 {
47                return None;
48            }
49            keys.push(SymExpr::from_bytes(&mut self.cx, bytes[..32].iter().cloned()));
50            current = SymExpr::from_bytes(&mut self.cx, bytes[32..64].iter().cloned());
51        }
52    }
53
54    fn mapping_storage_provenance(
55        &mut self,
56        state: &PathState,
57        key: &SymExpr,
58    ) -> Result<MappingStorageProvenance, SymbolicError> {
59        let account = state.storage_address;
60        let observed = |hash: &SymExpr| {
61            state.mapping_hook_keccak_preimages.get(&(account, hash.clone())).cloned()
62        };
63        if let Some(provenance) =
64            key.storage_mapping_provenance_observed_with(&mut self.cx, observed)
65        {
66            return Ok(MappingStorageProvenance::Exact(provenance));
67        }
68        let mut hashes = state
69            .mapping_hook_keccak_preimages
70            .keys()
71            .filter(|(address, _)| *address == account)
72            .map(|(_, hash)| hash.clone())
73            .collect::<Vec<_>>();
74        let contains_observed_hash =
75            hashes.iter().any(|hash| key.visit_bool(|candidate| candidate == hash));
76        let key_is_const = key.as_const().is_some();
77        let key_contains_keccak = key.contains_keccak();
78        let key_is_storage_mapping_key = key.storage_mapping_key(&mut self.cx).is_some();
79        let roots = state
80            .mapping_storage_store_hooks
81            .keys()
82            .filter(|(address, _)| *address == account)
83            .map(|(_, root)| *root)
84            .collect::<Vec<_>>();
85        hashes.sort_by_key(|hash| hash != key);
86        for hash in hashes {
87            if contains_observed_hash && !key.visit_bool(|candidate| candidate == &hash) {
88                continue;
89            }
90            let use_legacy_match = contains_observed_hash || !key_contains_keccak;
91            if use_legacy_match
92                && let Some(provenance) =
93                    hash.storage_mapping_provenance_observed_with(&mut self.cx, |candidate| {
94                        state
95                            .mapping_hook_keccak_preimages
96                            .get(&(account, candidate.clone()))
97                            .cloned()
98                    })
99            {
100                if !state.mapping_storage_store_hooks.contains_key(&(account, provenance.root_slot))
101                {
102                    continue;
103                }
104                let equality = SymBoolExpr::eq(&mut self.cx, key.clone(), hash.clone());
105                if key_is_const {
106                    let inequality = equality.not(&mut self.cx);
107                    let (_, inequality_is_sat) =
108                        self.constraints_with_condition(state, inequality)?;
109                    if !inequality_is_sat {
110                        return Ok(MappingStorageProvenance::Exact(provenance));
111                    }
112                    continue;
113                }
114                if let Some(provenance) =
115                    self.classify_mapping_match(state, equality, provenance)?
116                {
117                    return Ok(provenance);
118                }
119                continue;
120            }
121            if (key_is_const || key_contains_keccak) && !key_is_storage_mapping_key {
122                continue;
123            }
124            let Some((root, keys)) = self.observed_mapping_chain(state, &hash) else {
125                continue;
126            };
127            for &root_slot in &roots {
128                let slot_matches = if key_is_const || key.visit_bool(|candidate| candidate == &hash)
129                {
130                    SymBoolExpr::eq(&mut self.cx, key.clone(), hash.clone())
131                } else {
132                    key.storage_key_eq(&mut self.cx, &hash)
133                };
134                let matches = if let Some(constrained_root) =
135                    state.constrained_word(&mut self.cx, &root)
136                {
137                    if constrained_root != root_slot {
138                        continue;
139                    }
140                    slot_matches
141                } else {
142                    let root_slot_expr = SymExpr::constant(&mut self.cx, root_slot);
143                    let root_matches = SymBoolExpr::eq(&mut self.cx, root.clone(), root_slot_expr);
144                    SymBoolExpr::and(&mut self.cx, vec![slot_matches, root_matches])
145                };
146                let provenance = SymbolicMappingProvenance { root_slot, keys: keys.clone() };
147                if let Some(provenance) = self.classify_mapping_match(state, matches, provenance)? {
148                    return Ok(provenance);
149                }
150            }
151        }
152        Ok(MappingStorageProvenance::None)
153    }
154
155    fn storage_hook_calldata(
156        &mut self,
157        selector: [u8; 4],
158        words: impl IntoIterator<Item = SymExpr>,
159    ) -> SymCalldata {
160        let selector = SymBytes::concrete(&mut self.cx, selector.to_vec());
161        let words = words.into_iter().map(|word| word.into_bytes(&mut self.cx)).collect::<Vec<_>>();
162        let bytes = SymBytes::concat(&mut self.cx, std::iter::once(selector).chain(words));
163        SymCalldata::from_bytes(&mut self.cx, bytes)
164    }
165
166    fn mapping_storage_hook_calldata(
167        &mut self,
168        selector: [u8; 4],
169        [account, computed_slot, root_slot, old_value, new_value]: [SymExpr; 5],
170        keys: Vec<SymExpr>,
171    ) -> SymCalldata {
172        let selector = SymBytes::concrete(&mut self.cx, selector.to_vec());
173        let keys_offset = SymExpr::constant(&mut self.cx, U256::from(6 * 32));
174        let mut words = vec![account, computed_slot, root_slot, keys_offset, old_value, new_value];
175        words.push(SymExpr::constant(&mut self.cx, U256::from(keys.len())));
176        words.extend(keys);
177        let words = words.into_iter().map(|word| word.into_bytes(&mut self.cx)).collect::<Vec<_>>();
178        let bytes = SymBytes::concat(&mut self.cx, std::iter::once(selector).chain(words));
179        SymCalldata::from_bytes(&mut self.cx, bytes)
180    }
181
182    fn invoke_storage_hook<FEN: FoundryEvmNetwork>(
183        &mut self,
184        executor: &Executor<FEN>,
185        state: &mut PathState,
186        worklist: &mut VecDeque<PathState>,
187        completed_paths: &mut usize,
188        hook: SymbolicStorageHook,
189        calldata: SymCalldata,
190    ) -> Result<StepOutcome, SymbolicError> {
191        let code = state.world.extcode(&mut self.cx, executor, hook.callback_target)?;
192        if code.is_empty() {
193            return Ok(StepOutcome::Continue);
194        }
195
196        let callvalue = SymExpr::zero(&mut self.cx);
197        let frame = CallFrame::new(
198            &mut self.cx,
199            hook.callback_target,
200            hook.callback_target,
201            CHEATCODE_ADDRESS,
202            callvalue,
203            false,
204            calldata,
205        );
206        let child = state.storage_hook_child(frame);
207        let outcomes = self.execute_external_call(executor, child, &code, completed_paths)?;
208        if outcomes.is_empty() {
209            return Ok(StepOutcome::AssumeRejected);
210        }
211
212        let mut parents = VecDeque::with_capacity(outcomes.len());
213        for mut outcome in outcomes {
214            let mut parent = state.clone();
215            parent.constraints = std::mem::take(&mut outcome.state.constraints);
216            parent.next_symbol = outcome.state.next_symbol;
217            parent.storage_load_hooks = std::mem::take(&mut outcome.state.storage_load_hooks);
218            parent.storage_store_hooks = std::mem::take(&mut outcome.state.storage_store_hooks);
219            parent.mapping_storage_store_hooks =
220                std::mem::take(&mut outcome.state.mapping_storage_store_hooks);
221            parent.mapping_hook_keccak_preimages =
222                std::mem::take(&mut outcome.state.mapping_hook_keccak_preimages);
223            parent.storage_hook_active = false;
224
225            match outcome.status {
226                CallStatus::Success => {
227                    parent.world = outcome.state.world;
228                    parent.block = outcome.state.block;
229                }
230                CallStatus::Revert | CallStatus::ExceptionalHalt | CallStatus::Failure => {
231                    parent.return_data = outcome.state.frame.return_data;
232                    parent.pending_storage_hook_revert = true;
233                }
234            }
235            parents.push_back(parent);
236        }
237
238        let Some(first) = self.pop_next_path(&mut parents) else {
239            return Ok(StepOutcome::AssumeRejected);
240        };
241        *state = first;
242        worklist.extend(parents);
243        Ok(if std::mem::take(&mut state.pending_storage_hook_revert) {
244            StepOutcome::Revert
245        } else {
246            StepOutcome::Continue
247        })
248    }
249
250    fn push_comparison_result(
251        &mut self,
252        state: &mut PathState,
253        op_pc: usize,
254        opcode: u8,
255        condition: SymBoolExpr,
256    ) -> Result<StepOutcome, SymbolicError> {
257        if !self.apply_branch_target_constraint(state, op_pc, opcode, &condition)? {
258            return Ok(StepOutcome::AssumeRejected);
259        }
260        let value = SymExpr::bool_word(&mut self.cx, condition);
261        state.stack.push(value)?;
262        Ok(StepOutcome::Continue)
263    }
264
265    fn apply_branch_target_constraint(
266        &mut self,
267        state: &mut PathState,
268        op_pc: usize,
269        opcode: u8,
270        condition: &SymBoolExpr,
271    ) -> Result<bool, SymbolicError> {
272        let Some(target) = state.branch_target() else {
273            return Ok(true);
274        };
275        if state.satisfies_branch_target() {
276            return Ok(true);
277        }
278        if !target.matches(state.address, op_pc, opcode) {
279            return Ok(true);
280        }
281
282        let desired =
283            if target.result() { condition.clone().not(&mut self.cx) } else { condition.clone() };
284        let mut constraints = state.constraints.clone();
285        constraints.push(desired);
286        if !self.branch_is_sat_or_defer(state, &constraints)? {
287            return Ok(false);
288        }
289        state.constraints = constraints;
290        state.mark_branch_target_reached();
291        Ok(true)
292    }
293
294    fn guard_fixed_memory_access<FEN: FoundryEvmNetwork>(
295        &mut self,
296        executor: &Executor<FEN>,
297        state: &mut PathState,
298        worklist: &mut VecDeque<PathState>,
299        offset: &SymExpr,
300        size: usize,
301    ) -> Result<Option<StepOutcome>, SymbolicError> {
302        let memory_limit = executor.evm_env().cfg_env.memory_limit();
303        let host_max_offset = (usize::MAX & !31usize).checked_sub(size);
304        let constrained_offset = state.constrained_usize_checked(&mut self.cx, offset);
305        if constrained_offset.as_ref().is_some_and(|offset| match offset {
306            Ok(offset) => host_max_offset.is_none_or(|max| *offset > max),
307            Err(_) => true,
308        }) {
309            state.return_data = SymReturnData::empty(&mut self.cx);
310            return Ok(Some(StepOutcome::Revert));
311        }
312
313        let expanded_size_bound = state
314            .upper_bound_usize(&mut self.cx, offset)
315            .and_then(|offset| offset.checked_add(size))
316            .and_then(|end| end.checked_add(31))
317            .and_then(|end| u64::try_from(end & !31usize).ok());
318        if expanded_size_bound.is_some_and(|size| size <= memory_limit) {
319            return Ok(None);
320        }
321
322        let representable = if let Some(host_max_offset) = host_max_offset {
323            let host_max_offset = SymExpr::constant(&mut self.cx, U256::from(host_max_offset));
324            SymBoolExpr::cmp_word_expr(&mut self.cx, SymCmpOp::Ule, offset, host_max_offset)
325        } else {
326            SymBoolExpr::constant(&mut self.cx, false)
327        };
328        let size = SymExpr::constant(&mut self.cx, U256::from(size));
329        let local_size =
330            state.memory.size_after_range_expansion_word(&mut self.cx, offset.clone(), size);
331        if let Some(local_size) = local_size.as_const() {
332            if local_size <= U256::from(memory_limit) {
333                return Ok(None);
334            }
335            state.return_data = SymReturnData::empty(&mut self.cx);
336            return Ok(Some(StepOutcome::Revert));
337        }
338        let memory_limit = SymExpr::constant(&mut self.cx, U256::from(memory_limit));
339        let within_limit = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, local_size, memory_limit);
340        let valid_access = SymBoolExpr::and(&mut self.cx, vec![representable, within_limit]);
341        self.apply_memory_access_guard(state, worklist, valid_access)
342    }
343
344    fn apply_memory_access_guard(
345        &mut self,
346        state: &mut PathState,
347        worklist: &mut VecDeque<PathState>,
348        valid_access: SymBoolExpr,
349    ) -> Result<Option<StepOutcome>, SymbolicError> {
350        let (valid_constraints, valid_sat) =
351            self.constraints_with_condition(state, valid_access.clone())?;
352        let invalid = valid_access.clone().not(&mut self.cx);
353        let (invalid_constraints, invalid_sat) = self.constraints_with_condition(state, invalid)?;
354        match (valid_sat, invalid_sat) {
355            (true, true) => {
356                let (valid_seed_models, invalid_seed_models) =
357                    state.split_corpus_seed_models(&valid_access);
358                let mut valid = state.clone();
359                valid.pc = valid.pc.saturating_sub(1);
360                valid.depth = valid.depth.saturating_sub(1);
361                valid.constraints = valid_constraints;
362                valid.set_corpus_seed_models(valid_seed_models);
363                worklist.push_back(valid);
364                state.constraints = invalid_constraints;
365                state.set_corpus_seed_models(invalid_seed_models);
366                state.return_data = SymReturnData::empty(&mut self.cx);
367                Ok(Some(StepOutcome::Revert))
368            }
369            (true, false) => {
370                state.constraints = valid_constraints;
371                Ok(None)
372            }
373            (false, true) => {
374                state.constraints = invalid_constraints;
375                state.return_data = SymReturnData::empty(&mut self.cx);
376                Ok(Some(StepOutcome::Revert))
377            }
378            (false, false) => Ok(Some(StepOutcome::AssumeRejected)),
379        }
380    }
381
382    pub(super) fn guard_memory_range<FEN: FoundryEvmNetwork>(
383        &mut self,
384        executor: &Executor<FEN>,
385        state: &mut PathState,
386        worklist: &mut VecDeque<PathState>,
387        offset: &SymExpr,
388        size: &SymExpr,
389    ) -> Result<Option<StepOutcome>, SymbolicError> {
390        let memory_limit = executor.evm_env().cfg_env.memory_limit();
391        if let (Some(offset_value), Some(size_value)) = (offset.as_const(), size.as_const()) {
392            let valid = size_value.is_zero()
393                || usize::try_from(offset_value)
394                    .ok()
395                    .zip(usize::try_from(size_value).ok())
396                    .and_then(|(offset, size)| offset.checked_add(size))
397                    .and_then(|end| end.checked_add(31))
398                    .and_then(|end| u64::try_from(end & !31usize).ok())
399                    .is_some_and(|end| end <= memory_limit);
400            if !valid {
401                state.return_data = SymReturnData::empty(&mut self.cx);
402                return Ok(Some(StepOutcome::Revert));
403            }
404            state.memory.expand_range(&mut self.cx, offset.clone(), size.clone());
405            return Ok(None);
406        }
407
408        let offset_bound = state.upper_bound_usize(&mut self.cx, offset);
409        let size_bound = state.upper_bound_usize(&mut self.cx, size);
410        if offset_bound
411            .zip(size_bound)
412            .and_then(|(offset, size)| offset.checked_add(size))
413            .and_then(|end| end.checked_add(31))
414            .and_then(|end| u64::try_from(end & !31usize).ok())
415            .is_some_and(|end| end <= memory_limit)
416        {
417            state.memory.expand_range(&mut self.cx, offset.clone(), size.clone());
418            return Ok(None);
419        }
420
421        let zero_size = SymBoolExpr::eq_word_const(&mut self.cx, size, U256::ZERO);
422        let host_max = SymExpr::constant(&mut self.cx, U256::from(usize::MAX & !31usize));
423        let size_fits =
424            SymBoolExpr::cmp_word_expr(&mut self.cx, SymCmpOp::Ule, size, host_max.clone());
425        let max_offset = SymExpr::binop(&mut self.cx, SymBinOp::Sub, host_max, size.clone());
426        let offset_fits =
427            SymBoolExpr::cmp_word_expr(&mut self.cx, SymCmpOp::Ule, offset, max_offset);
428
429        let local_size = state.memory.size_after_range_expansion_word(
430            &mut self.cx,
431            offset.clone(),
432            size.clone(),
433        );
434        let memory_limit = SymExpr::constant(&mut self.cx, U256::from(memory_limit));
435        let local_fits = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, local_size, memory_limit);
436        let nonzero_valid =
437            SymBoolExpr::and(&mut self.cx, vec![size_fits, offset_fits, local_fits]);
438        let valid_access = SymBoolExpr::or(&mut self.cx, vec![zero_size, nonzero_valid]);
439
440        let outcome = self.apply_memory_access_guard(state, worklist, valid_access)?;
441        if outcome.is_none() {
442            state.memory.expand_range(&mut self.cx, offset.clone(), size.clone());
443        }
444        Ok(outcome)
445    }
446
447    #[expect(clippy::too_many_arguments)]
448    pub(super) fn step<FEN: FoundryEvmNetwork>(
449        &mut self,
450        executor: &Executor<FEN>,
451        code: &SymCode,
452        jumpdests: &JumpTable,
453        state: &mut PathState,
454        worklist: &mut VecDeque<PathState>,
455        completed_paths: &mut usize,
456        op: u8,
457    ) -> Result<StepOutcome, SymbolicError> {
458        state.pc += 1;
459
460        if Into::<SpecId>::into(executor.spec_id()) < opcode_activation(op) {
461            state.return_data = SymReturnData::empty(&mut self.cx);
462            return Ok(StepOutcome::ExceptionalHalt);
463        }
464
465        match op {
466            opcode::PUSH0 => {
467                state.stack.push(SymExpr::zero(&mut self.cx))?;
468            }
469            opcode::PUSH1..=opcode::PUSH32 => {
470                let n = (op - opcode::PUSH1 + 1) as usize;
471                let end = state.pc.saturating_add(n);
472                if end > code.len() {
473                    return Err(SymbolicError::InvalidBytecode("truncated PUSH data"));
474                }
475                let value = code.push_data_word(&mut self.cx, state.pc, n);
476                state.pc = end;
477                state.stack.push(value)?;
478            }
479            opcode::DUP1..=opcode::DUP16 => {
480                let n = (op - opcode::DUP1 + 1) as usize;
481                let value = state.stack.peek(n - 1)?.clone();
482                state.stack.push(value)?;
483            }
484            opcode::SWAP1..=opcode::SWAP16 => {
485                let n = (op - opcode::SWAP1 + 1) as usize;
486                state.stack.swap(n)?;
487            }
488            opcode::STOP => return Ok(StepOutcome::Halt),
489            opcode::ADD | opcode::SUB | opcode::MUL | opcode::AND | opcode::OR | opcode::XOR => {
490                let bin_op = match op {
491                    opcode::ADD => SymBinOp::Add,
492                    opcode::SUB => SymBinOp::Sub,
493                    opcode::MUL => SymBinOp::Mul,
494                    opcode::AND => SymBinOp::And,
495                    opcode::OR => SymBinOp::Or,
496                    _ => SymBinOp::Xor,
497                };
498                state.bin_word(&mut self.cx, bin_op)?
499            }
500            opcode::EXP => state.exp_word(&mut self.cx)?,
501            opcode::DIV | opcode::SDIV | opcode::MOD | opcode::SMOD => {
502                let bin_op = match op {
503                    opcode::DIV => SymBinOp::UDiv,
504                    opcode::SDIV => SymBinOp::SDiv,
505                    opcode::MOD => SymBinOp::URem,
506                    _ => SymBinOp::SRem,
507                };
508                state.bin_word_div_zero_guard(&mut self.cx, bin_op)?
509            }
510            opcode::ADDMOD | opcode::MULMOD => {
511                let a = state.stack.pop()?;
512                let b = state.stack.pop()?;
513                let n = state.stack.pop()?;
514                let tern_op =
515                    if op == opcode::ADDMOD { SymTernOp::AddMod } else { SymTernOp::MulMod };
516                state.stack.push(SymExpr::ternop(&mut self.cx, tern_op, a, b, n))?;
517            }
518            opcode::LT | opcode::GT | opcode::SLT | opcode::SGT => {
519                let op_pc = state.pc - 1;
520                let cmp_op = match op {
521                    opcode::LT => SymCmpOp::Ult,
522                    opcode::GT => SymCmpOp::Ugt,
523                    opcode::SLT => SymCmpOp::Slt,
524                    _ => SymCmpOp::Sgt,
525                };
526                let condition = state.cmp_word_condition(&mut self.cx, cmp_op)?;
527                return self.push_comparison_result(state, op_pc, op, condition);
528            }
529            opcode::EQ => {
530                let op_pc = state.pc - 1;
531                let a = state.stack.pop()?;
532                let b = state.stack.pop()?;
533                let condition = SymBoolExpr::eq(&mut self.cx, b, a);
534                return self.push_comparison_result(state, op_pc, op, condition);
535            }
536            opcode::ISZERO => {
537                let op_pc = state.pc - 1;
538                let value = state.stack.pop()?;
539                let value = value.into_zero_bool(&mut self.cx);
540                return self.push_comparison_result(state, op_pc, op, value);
541            }
542            opcode::NOT => {
543                let value = state.stack.pop()?;
544                state.stack.push(SymExpr::not(&mut self.cx, value))?;
545            }
546            opcode::SIGNEXTEND => {
547                let byte_index = state.stack.pop()?;
548                let value = state.stack.pop()?;
549                state.stack.push(signextend_word_dynamic(&mut self.cx, byte_index, value))?;
550            }
551            opcode::BYTE => {
552                let index = state.stack.pop()?;
553                let word = state.stack.pop()?;
554                state.stack.push(byte_word_dynamic(&mut self.cx, index, word))?;
555            }
556            opcode::SHL => state.shift_word(&mut self.cx, SymBinOp::Shl)?,
557            opcode::SHR => state.shift_word(&mut self.cx, SymBinOp::Shr)?,
558            opcode::SAR => state.shift_word(&mut self.cx, SymBinOp::Sar)?,
559            opcode::KECCAK256 => {
560                let offset = state.stack.peek(0)?.clone();
561                let size = state.stack.peek(1)?.clone();
562                if let Some(outcome) =
563                    self.guard_memory_range(executor, state, worklist, &offset, &size)?
564                {
565                    return Ok(outcome);
566                }
567                let offset = state.stack.pop()?;
568                let size = state.stack.pop()?;
569                match state.constrained_usize_checked(&mut self.cx, &size) {
570                    Some(Ok(size)) => {
571                        let bytes = state.memory.read_byte_exprs_offset(&mut self.cx, offset, size);
572                        let hash = keccak_word(&mut self.cx, bytes.clone());
573                        let has_mapping_hook = state
574                            .mapping_storage_store_hooks
575                            .keys()
576                            .any(|(address, _)| *address == state.storage_address);
577                        if has_mapping_hook && !state.storage_hook_active && size == 64 {
578                            state
579                                .mapping_hook_keccak_preimages
580                                .entry((state.storage_address, hash.clone()))
581                                .or_insert_with(|| bytes.into());
582                        }
583                        state.stack.push(hash)?;
584                    }
585                    Some(Err(_)) => {
586                        return Ok(StepOutcome::Revert);
587                    }
588                    None => {
589                        let has_mapping_hook = state
590                            .mapping_storage_store_hooks
591                            .keys()
592                            .any(|(address, _)| *address == state.storage_address);
593                        if has_mapping_hook && !state.storage_hook_active {
594                            let mapping_size = SymExpr::constant(&mut self.cx, U256::from(64));
595                            let mapping_size_feasible =
596                                SymBoolExpr::eq(&mut self.cx, size.clone(), mapping_size);
597                            let (_, mapping_size_feasible) =
598                                self.constraints_with_condition(state, mapping_size_feasible)?;
599                            if mapping_size_feasible {
600                                self.defer_incomplete(
601                                    "symbolic KECCAK256 size may conceal mapping provenance",
602                                );
603                            }
604                        }
605                        let max_limit = self.config.max_calldata_bytes as usize;
606                        let max_size = self.solver_upper_bound_usize(
607                            state,
608                            &size,
609                            max_limit,
610                            "symbolic SHA3 size",
611                        )?;
612                        let bytes = state.memory.read_byte_exprs_symbolic_size(
613                            &mut self.cx,
614                            offset,
615                            size.clone(),
616                            max_size,
617                        );
618                        state.stack.push(keccak_word_with_len(&mut self.cx, bytes, size))?;
619                    }
620                }
621            }
622            opcode::ADDRESS | opcode::CALLER | opcode::ORIGIN | opcode::CALLVALUE => {
623                let value = match op {
624                    opcode::ADDRESS => state.address_word.clone(),
625                    opcode::CALLER => state.caller_word.clone(),
626                    opcode::ORIGIN => state.origin_word.clone(),
627                    _ => state.callvalue.clone(),
628                };
629                state.stack.push(value)?;
630            }
631            opcode::BLOCKHASH => {
632                let number = state.stack.pop()?;
633                let hash = state.block.block_hash_word(&mut self.cx, executor, number)?;
634                state.stack.push(hash)?;
635            }
636            opcode::BALANCE => {
637                let target = state.stack.pop()?;
638                let balance = state.balance_word(&mut self.cx, executor, target)?;
639                state.stack.push(balance)?;
640            }
641            opcode::SELFBALANCE => {
642                let balance = state.balance(&mut self.cx, executor, state.address);
643                state.stack.push(balance)?;
644            }
645            opcode::EXTCODESIZE => {
646                let target = state.stack.pop()?;
647                let size = state.extcode_size_word(&mut self.cx, executor, target)?;
648                state.stack.push(size)?;
649            }
650            opcode::EXTCODEHASH => {
651                let target = state.stack.pop()?;
652                let hash = state.extcode_hash_word(&mut self.cx, executor, target)?;
653                state.stack.push(hash)?;
654            }
655            opcode::EXTCODECOPY => {
656                let dest = state.stack.peek(1)?.clone();
657                let size = state.stack.peek(3)?.clone();
658                if let Some(outcome) =
659                    self.guard_memory_range(executor, state, worklist, &dest, &size)?
660                {
661                    return Ok(outcome);
662                }
663                let target = state.stack.pop()?;
664                let dest = state.stack.pop()?;
665                let offset = state.stack.pop()?;
666                let size = state.stack.pop()?;
667                match state.constrained_usize_checked(&mut self.cx, &size) {
668                    Some(Ok(size)) => {
669                        let bytes = state.extcode_bytes_word(
670                            &mut self.cx,
671                            executor,
672                            target,
673                            offset,
674                            size,
675                        )?;
676                        state.memory.store_bytes_offset(&mut self.cx, dest, bytes);
677                    }
678                    Some(Err(_)) => {
679                        return Ok(StepOutcome::Revert);
680                    }
681                    None => {
682                        let max_limit = self.config.max_calldata_bytes as usize;
683                        let max_size = self.solver_upper_bound_usize(
684                            state,
685                            &size,
686                            max_limit,
687                            "symbolic EXTCODECOPY size",
688                        )?;
689                        if max_size != 0 {
690                            let bytes = state.extcode_bytes_word(
691                                &mut self.cx,
692                                executor,
693                                target,
694                                offset,
695                                max_size,
696                            )?;
697                            state.memory.copy_bytes_size_offset(&mut self.cx, dest, size, bytes)?;
698                        }
699                    }
700                }
701            }
702            opcode::CALLDATALOAD => {
703                let offset = state.stack.pop()?;
704                let value = state.calldata.load_word(&mut self.cx, offset);
705                state.stack.push(value)?;
706            }
707            opcode::CALLDATASIZE => {
708                let size = state.calldata.size_word();
709                state.stack.push(size)?;
710            }
711            opcode::CALLDATACOPY => {
712                let dest = state.stack.peek(0)?.clone();
713                let size = state.stack.peek(2)?.clone();
714                if let Some(outcome) =
715                    self.guard_memory_range(executor, state, worklist, &dest, &size)?
716                {
717                    return Ok(outcome);
718                }
719                let dest = state.stack.pop()?;
720                let offset = state.stack.pop()?;
721                let size = state.stack.pop()?;
722                match state.constrained_usize_checked(&mut self.cx, &size) {
723                    Some(Ok(size)) => {
724                        if size != 0 {
725                            let CallFrame { memory, calldata, .. } = &mut state.frame;
726                            memory.copy_calldata_to_offset(
727                                &mut self.cx,
728                                dest,
729                                offset,
730                                size,
731                                calldata,
732                            );
733                        }
734                    }
735                    Some(Err(_)) => {
736                        return Ok(StepOutcome::Revert);
737                    }
738                    None => {
739                        let max_limit = self.config.max_calldata_bytes as usize;
740                        let max_size = self.solver_upper_bound_usize(
741                            state,
742                            &size,
743                            max_limit,
744                            "symbolic CALLDATACOPY size",
745                        )?;
746                        if max_size != 0 {
747                            let CallFrame { memory, calldata, .. } = &mut state.frame;
748                            memory.copy_calldata_symbolic_size(
749                                &mut self.cx,
750                                dest,
751                                offset,
752                                size,
753                                max_size,
754                                calldata,
755                            )?;
756                        }
757                    }
758                }
759            }
760            opcode::CODESIZE => {
761                let value = SymExpr::constant(&mut self.cx, U256::from(code.len()));
762                state.stack.push(value)?;
763            }
764            opcode::CODECOPY => {
765                let dest = state.stack.peek(0)?.clone();
766                let size = state.stack.peek(2)?.clone();
767                if let Some(outcome) =
768                    self.guard_memory_range(executor, state, worklist, &dest, &size)?
769                {
770                    return Ok(outcome);
771                }
772                let dest = state.stack.pop()?;
773                let offset = state.stack.pop()?;
774                let size = state.stack.pop()?;
775                match state.constrained_usize_checked(&mut self.cx, &size) {
776                    Some(Ok(size)) => {
777                        let bytes = code.read_bytes_offset(&mut self.cx, offset, size);
778                        state.memory.store_bytes_offset(&mut self.cx, dest, bytes);
779                    }
780                    Some(Err(_)) => {
781                        return Ok(StepOutcome::Revert);
782                    }
783                    None => {
784                        let max_limit = self.config.max_calldata_bytes as usize;
785                        let max_size = self.solver_upper_bound_usize(
786                            state,
787                            &size,
788                            max_limit,
789                            "symbolic CODECOPY size",
790                        )?;
791                        if max_size != 0 {
792                            let bytes = code.read_bytes_offset(&mut self.cx, offset, max_size);
793                            state.memory.copy_bytes_size_offset(&mut self.cx, dest, size, bytes)?;
794                        }
795                    }
796                }
797            }
798            opcode::RETURNDATASIZE => {
799                let size = state.return_data.len_word.clone();
800                state.stack.push(size)?;
801            }
802            opcode::RETURNDATACOPY => {
803                let dest = state.stack.peek(0)?.clone();
804                let offset = state.stack.peek(1)?.clone();
805                let size = state.stack.peek(2)?.clone();
806                if let Some(outcome) =
807                    self.guard_memory_range(executor, state, worklist, &dest, &size)?
808                {
809                    return Ok(outcome);
810                }
811                if let Some(outcome) =
812                    self.guard_returndata_copy_range(state, worklist, &offset, &size)?
813                {
814                    return Ok(outcome);
815                }
816                let dest = state.stack.pop()?;
817                let offset = state.stack.pop()?;
818                let size = state.stack.pop()?;
819                match state.constrained_usize_checked(&mut self.cx, &size) {
820                    Some(Ok(size)) => {
821                        let CallFrame { memory, return_data, .. } = &mut state.frame;
822                        memory.copy_return_data_to_offset(
823                            &mut self.cx,
824                            dest,
825                            offset,
826                            size,
827                            return_data,
828                        )?;
829                    }
830                    Some(Err(_)) => {
831                        return Ok(StepOutcome::Revert);
832                    }
833                    None => {
834                        let available = state
835                            .constrained_usize(&mut self.cx, &offset)
836                            .map(|offset| state.return_data.len().saturating_sub(offset))
837                            .unwrap_or(state.return_data.len());
838                        let max_limit = available.min(self.config.max_calldata_bytes as usize);
839                        let max_size = self.solver_upper_bound_usize(
840                            state,
841                            &size,
842                            max_limit,
843                            "symbolic RETURNDATACOPY size",
844                        )?;
845                        let CallFrame { memory, return_data, .. } = &mut state.frame;
846                        memory.copy_return_data_symbolic_size(
847                            &mut self.cx,
848                            dest,
849                            offset,
850                            size,
851                            max_size,
852                            return_data,
853                        )?;
854                    }
855                }
856            }
857            opcode::POP => {
858                state.stack.pop()?;
859            }
860            opcode::MLOAD => {
861                let offset = state.stack.peek(0)?.clone();
862                if let Some(outcome) =
863                    self.guard_fixed_memory_access(executor, state, worklist, &offset, 32)?
864                {
865                    return Ok(outcome);
866                }
867                let offset = state.stack.pop()?;
868                let value = state.memory.load_word_offset(&mut self.cx, offset)?;
869                state.stack.push(value)?;
870            }
871            opcode::MSTORE => {
872                let offset = state.stack.peek(0)?.clone();
873                if let Some(outcome) =
874                    self.guard_fixed_memory_access(executor, state, worklist, &offset, 32)?
875                {
876                    return Ok(outcome);
877                }
878                let offset = state.stack.pop()?;
879                let value = state.stack.pop()?;
880                let minimum_offset = state.lower_bound_usize(&offset);
881                state.memory.store_word_offset(&mut self.cx, offset, value, minimum_offset);
882            }
883            opcode::MSTORE8 => {
884                let offset = state.stack.peek(0)?.clone();
885                if let Some(outcome) =
886                    self.guard_fixed_memory_access(executor, state, worklist, &offset, 1)?
887                {
888                    return Ok(outcome);
889                }
890                let offset = state.stack.pop()?;
891                let value = state.stack.pop()?;
892                let minimum_offset = state.lower_bound_usize(&offset);
893                state.memory.store_byte_offset(&mut self.cx, offset, value, minimum_offset);
894            }
895            opcode::SLOAD => {
896                let key = state.stack.pop()?;
897                state.record_sload(state.storage_address, key.clone());
898                let concrete_key = state.constrained_word(&mut self.cx, &key);
899                let value = state.world.sload(
900                    &mut self.cx,
901                    executor,
902                    state.storage_address,
903                    key.clone(),
904                    concrete_key,
905                )?;
906                state.stack.push(value.clone())?;
907                if !state.storage_hook_active
908                    && let Some(hook) =
909                        state.storage_load_hooks.get(&state.storage_address).copied()
910                {
911                    let account =
912                        SymExpr::constant(&mut self.cx, address_word(state.storage_address));
913                    let calldata =
914                        self.storage_hook_calldata(hook.callback_selector, [account, key, value]);
915                    return self.invoke_storage_hook(
916                        executor,
917                        state,
918                        worklist,
919                        completed_paths,
920                        hook,
921                        calldata,
922                    );
923                }
924            }
925            opcode::SSTORE => {
926                if state.is_static {
927                    state.return_data = SymReturnData::empty(&mut self.cx);
928                    return Ok(StepOutcome::ExceptionalHalt);
929                }
930                let key = state.stack.peek(0)?.clone();
931                state.stack.peek(1)?;
932                let hook = (!state.storage_hook_active)
933                    .then(|| state.storage_store_hooks.get(&state.storage_address).copied())
934                    .flatten();
935                let mapping = if state.storage_hook_active {
936                    MappingStorageProvenance::None
937                } else {
938                    self.mapping_storage_provenance(state, &key)?
939                };
940                let mapping = match mapping {
941                    MappingStorageProvenance::None => None,
942                    MappingStorageProvenance::Exact(provenance) => state
943                        .mapping_storage_store_hooks
944                        .get(&(state.storage_address, provenance.root_slot))
945                        .copied()
946                        .map(|hook| (hook, provenance)),
947                    MappingStorageProvenance::Fork { equality, inequality } => {
948                        let store_pc = state.pc - 1;
949                        let mut equality_state = state.clone();
950                        equality_state.pc = store_pc;
951                        equality_state.depth = equality_state.depth.saturating_sub(1);
952                        equality_state.constraints = equality;
953                        let mut inequality_state = state.clone();
954                        inequality_state.pc = store_pc;
955                        inequality_state.depth = inequality_state.depth.saturating_sub(1);
956                        inequality_state.constraints = inequality;
957                        worklist.push_back(equality_state);
958                        worklist.push_back(inequality_state);
959                        return Ok(StepOutcome::Forked);
960                    }
961                };
962                state.stack.pop()?;
963                let value = state.stack.pop()?;
964                state.record_sstore(state.storage_address, key.clone());
965                let old_value = if hook.is_some() || mapping.is_some() {
966                    let concrete_key = state.constrained_word(&mut self.cx, &key);
967                    Some(state.world.sload(
968                        &mut self.cx,
969                        executor,
970                        state.storage_address,
971                        key.clone(),
972                        concrete_key,
973                    )?)
974                } else {
975                    None
976                };
977                state.world.sstore(state.storage_address, key.clone(), value.clone());
978                if let Some(hook) = hook {
979                    let account =
980                        SymExpr::constant(&mut self.cx, address_word(state.storage_address));
981                    let calldata = self.storage_hook_calldata(
982                        hook.callback_selector,
983                        [
984                            account,
985                            key,
986                            old_value.expect("old value loaded for storage hook"),
987                            value,
988                        ],
989                    );
990                    return self.invoke_storage_hook(
991                        executor,
992                        state,
993                        worklist,
994                        completed_paths,
995                        hook,
996                        calldata,
997                    );
998                } else if let Some((hook, provenance)) = mapping {
999                    let account =
1000                        SymExpr::constant(&mut self.cx, address_word(state.storage_address));
1001                    let root = SymExpr::constant(&mut self.cx, provenance.root_slot);
1002                    let calldata = self.mapping_storage_hook_calldata(
1003                        hook.callback_selector,
1004                        [
1005                            account,
1006                            key,
1007                            root,
1008                            old_value.expect("old value loaded for mapping storage hook"),
1009                            value,
1010                        ],
1011                        provenance.keys,
1012                    );
1013                    return self.invoke_storage_hook(
1014                        executor,
1015                        state,
1016                        worklist,
1017                        completed_paths,
1018                        hook,
1019                        calldata,
1020                    );
1021                }
1022            }
1023            opcode::TLOAD => {
1024                let key = state.stack.pop()?;
1025                let value = state.world.tload(&mut self.cx, state.storage_address, key);
1026                state.stack.push(value)?;
1027            }
1028            opcode::TSTORE => {
1029                if state.is_static {
1030                    state.return_data = SymReturnData::empty(&mut self.cx);
1031                    return Ok(StepOutcome::ExceptionalHalt);
1032                }
1033                let key = state.stack.pop()?;
1034                let value = state.stack.pop()?;
1035                state.world.tstore(state.storage_address, key, value);
1036            }
1037            opcode::JUMP => {
1038                let dest = state.stack.pop()?;
1039                let Some(dest) = self.resolve_jump_destination(
1040                    state,
1041                    jumpdests,
1042                    dest,
1043                    "symbolic JUMP destination",
1044                )?
1045                else {
1046                    state.return_data = SymReturnData::empty(&mut self.cx);
1047                    return Ok(StepOutcome::ExceptionalHalt);
1048                };
1049                if !self.take_loop_jump(state, state.pc, dest) {
1050                    return Ok(StepOutcome::AssumeRejected);
1051                }
1052                state.pc = dest;
1053            }
1054            opcode::JUMPI => {
1055                let dest = state.stack.pop()?;
1056                let cond = state.stack.pop()?;
1057                match cond.as_const().map(|value| !value.is_zero()) {
1058                    Some(true) => {
1059                        let Some(dest) = self.resolve_jump_destination(
1060                            state,
1061                            jumpdests,
1062                            dest,
1063                            "symbolic JUMPI destination",
1064                        )?
1065                        else {
1066                            state.return_data = SymReturnData::empty(&mut self.cx);
1067                            return Ok(StepOutcome::ExceptionalHalt);
1068                        };
1069                        if !self.take_loop_jump(state, state.pc, dest) {
1070                            return Ok(StepOutcome::AssumeRejected);
1071                        }
1072                        state.pc = dest;
1073                    }
1074                    Some(false) => {}
1075                    None => {
1076                        let true_cond = cond.nonzero_bool(&mut self.cx);
1077                        let dest = match self.resolve_jump_destination(
1078                            state,
1079                            jumpdests,
1080                            dest,
1081                            "symbolic JUMPI destination",
1082                        ) {
1083                            Ok(Some(dest)) => dest,
1084                            Ok(None) => {
1085                                return self.branch_invalid_jumpi(state, worklist, true_cond);
1086                            }
1087                            Err(err) => {
1088                                let (_, taken_sat) =
1089                                    self.constraints_with_condition(state, true_cond.clone())?;
1090                                if taken_sat {
1091                                    return Err(err);
1092                                }
1093                                let (_, not_taken_seed_models) =
1094                                    state.split_corpus_seed_models(&true_cond);
1095                                state.constraints.push(true_cond.not(&mut self.cx));
1096                                state.set_corpus_seed_models(not_taken_seed_models);
1097                                return Ok(StepOutcome::Continue);
1098                            }
1099                        };
1100                        let op_pc = state.pc.saturating_sub(1);
1101                        let _branch_span = trace_span!("jumpi_branch", pc = op_pc, dest).entered();
1102                        let false_cond = true_cond.clone().not(&mut self.cx);
1103                        let fallthrough = state.pc;
1104                        let (true_seed_models, false_seed_models) =
1105                            state.split_corpus_seed_models(&true_cond);
1106                        let mut true_state = state.clone();
1107                        true_state.constraints.push(true_cond);
1108                        true_state.set_corpus_seed_models(true_seed_models);
1109                        true_state.pc = dest;
1110                        let mut false_state = state.clone();
1111                        false_state.constraints.push(false_cond);
1112                        false_state.set_corpus_seed_models(false_seed_models);
1113                        false_state.pc = fallthrough;
1114
1115                        let true_pending = self.take_loop_jump(&mut true_state, fallthrough, dest);
1116                        if true_pending {
1117                            true_state.defer_feasibility_check();
1118                        }
1119                        false_state.defer_feasibility_check();
1120                        trace!(true_pending, false_pending = true, "JUMPI symbolic branch");
1121                        if true_pending {
1122                            let true_seed_count = true_state.corpus_seed_model_count();
1123                            let false_seed_count = false_state.corpus_seed_model_count();
1124                            match (
1125                                false_seed_count.cmp(&true_seed_count),
1126                                self.config.exploration_order,
1127                            ) {
1128                                (std::cmp::Ordering::Greater, SymbolicExplorationOrder::Bfs)
1129                                | (std::cmp::Ordering::Less, SymbolicExplorationOrder::Dfs) => {
1130                                    worklist.push_back(false_state);
1131                                    worklist.push_back(true_state);
1132                                }
1133                                (std::cmp::Ordering::Greater, SymbolicExplorationOrder::Dfs)
1134                                | (std::cmp::Ordering::Less, SymbolicExplorationOrder::Bfs)
1135                                | (std::cmp::Ordering::Equal, _) => {
1136                                    worklist.push_back(true_state);
1137                                    worklist.push_back(false_state);
1138                                }
1139                            }
1140                        } else {
1141                            worklist.push_back(false_state);
1142                        }
1143                        return Ok(StepOutcome::Forked);
1144                    }
1145                }
1146            }
1147            opcode::PC => {
1148                let pc = state.pc - 1;
1149                let pc = SymExpr::constant(&mut self.cx, U256::from(pc));
1150                state.stack.push(pc)?;
1151            }
1152            opcode::MSIZE => {
1153                let size = state.memory.size_word(&mut self.cx);
1154                state.stack.push(size)?;
1155            }
1156            opcode::GAS => {
1157                let gas = state.fresh_gasleft(&mut self.cx);
1158                state.stack.push(gas)?;
1159            }
1160            opcode::JUMPDEST => {}
1161            opcode::MCOPY => {
1162                let dest = state.stack.peek(0)?.clone();
1163                let src = state.stack.peek(1)?.clone();
1164                let size = state.stack.peek(2)?.clone();
1165                if let Some(outcome) =
1166                    self.guard_memory_range(executor, state, worklist, &dest, &size)?
1167                {
1168                    return Ok(outcome);
1169                }
1170                if let Some(outcome) =
1171                    self.guard_memory_range(executor, state, worklist, &src, &size)?
1172                {
1173                    return Ok(outcome);
1174                }
1175                let dest = state.stack.pop()?;
1176                let src = state.stack.pop()?;
1177                let size = state.stack.pop()?;
1178                match state.constrained_usize_checked(&mut self.cx, &size) {
1179                    Some(Ok(size)) => {
1180                        state.memory.copy_memory_to_offset(&mut self.cx, dest, src, size)?;
1181                    }
1182                    Some(Err(_)) => {
1183                        return Ok(StepOutcome::Revert);
1184                    }
1185                    None => {
1186                        let max_limit = self.config.max_calldata_bytes as usize;
1187                        let max_size = self.solver_upper_bound_usize(
1188                            state,
1189                            &size,
1190                            max_limit,
1191                            "symbolic MCOPY size",
1192                        )?;
1193                        if max_size != 0 {
1194                            state.memory.copy_memory_symbolic_size(
1195                                &mut self.cx,
1196                                dest,
1197                                src,
1198                                size,
1199                                max_size,
1200                            )?;
1201                        }
1202                    }
1203                }
1204            }
1205            opcode::RETURN | opcode::REVERT => {
1206                let offset = state.stack.peek(0)?.clone();
1207                let size = state.stack.peek(1)?.clone();
1208                if let Some(outcome) =
1209                    self.guard_memory_range(executor, state, worklist, &offset, &size)?
1210                {
1211                    return Ok(outcome);
1212                }
1213                return self.return_or_revert(state, op == opcode::REVERT);
1214            }
1215            opcode::INVALID => return Ok(StepOutcome::ExceptionalHalt),
1216            opcode::CALL => {
1217                return self.call(executor, state, worklist, completed_paths, CallKind::Call);
1218            }
1219            opcode::CALLCODE => {
1220                return self.call(executor, state, worklist, completed_paths, CallKind::CallCode);
1221            }
1222            opcode::DELEGATECALL => {
1223                return self.call(
1224                    executor,
1225                    state,
1226                    worklist,
1227                    completed_paths,
1228                    CallKind::DelegateCall,
1229                );
1230            }
1231            opcode::STATICCALL => {
1232                return self.call(executor, state, worklist, completed_paths, CallKind::StaticCall);
1233            }
1234            opcode::CREATE => {
1235                return self.create(executor, state, worklist, completed_paths, CreateKind::Create);
1236            }
1237            opcode::CREATE2 => {
1238                return self.create(
1239                    executor,
1240                    state,
1241                    worklist,
1242                    completed_paths,
1243                    CreateKind::Create2,
1244                );
1245            }
1246            opcode::SELFDESTRUCT => {
1247                if state.is_static {
1248                    state.return_data = SymReturnData::empty(&mut self.cx);
1249                    return Ok(StepOutcome::ExceptionalHalt);
1250                }
1251                let spec_id: SpecId = executor.spec_id().into();
1252                let (beneficiary_word, beneficiary) =
1253                    state.pop_address_word_or_symbolic_slot(&mut self.cx)?;
1254                if spec_id < SpecId::CANCUN
1255                    || state.world.was_created_in_current_transaction(state.address)
1256                {
1257                    state.world.selfdestruct_legacy(
1258                        &mut self.cx,
1259                        executor,
1260                        state.address,
1261                        beneficiary,
1262                    )?;
1263                } else {
1264                    if state.constrained_word(&mut self.cx, &beneficiary_word).is_none() {
1265                        return Err(SymbolicError::Unsupported(
1266                            "symbolic SELFDESTRUCT beneficiary",
1267                        ));
1268                    }
1269                    state.world.selfdestruct_cancun_existing(
1270                        &mut self.cx,
1271                        executor,
1272                        state.address,
1273                        beneficiary,
1274                    );
1275                }
1276                state.return_data = SymReturnData::empty(&mut self.cx);
1277                return Ok(StepOutcome::Halt);
1278            }
1279            opcode::CHAINID => {
1280                let value = state.block.chain_id.clone();
1281                state.stack.push(value)?;
1282            }
1283            opcode::BASEFEE => {
1284                let value = state.block.basefee.clone();
1285                state.stack.push(value)?;
1286            }
1287            opcode::GASPRICE => {
1288                let gas_price = state.gas_price.clone();
1289                state.stack.push(gas_price)?;
1290            }
1291            opcode::BLOBHASH => {
1292                let index = state.stack.pop()?;
1293                let index = state.expect_constrained_usize(
1294                    &mut self.cx,
1295                    index,
1296                    "symbolic BLOBHASH index",
1297                )?;
1298                let hash = state.block.blob_hashes.get(index).copied().unwrap_or_default();
1299                let hash = SymExpr::constant(&mut self.cx, U256::from_be_slice(hash.as_slice()));
1300                state.stack.push(hash)?;
1301            }
1302            opcode::COINBASE => {
1303                let coinbase = state.block.coinbase;
1304                let coinbase = SymExpr::constant(&mut self.cx, address_word(coinbase));
1305                state.stack.push(coinbase)?;
1306            }
1307            opcode::TIMESTAMP => {
1308                let value = state.block.timestamp.clone();
1309                state.stack.push(value)?;
1310            }
1311            opcode::NUMBER => {
1312                let value = state.block.number.clone();
1313                state.stack.push(value)?;
1314            }
1315            opcode::DIFFICULTY => {
1316                let value = state.block.difficulty.clone();
1317                state.stack.push(value)?;
1318            }
1319            opcode::GASLIMIT => {
1320                let value = state.block.gaslimit.clone();
1321                state.stack.push(value)?;
1322            }
1323            opcode::BLOBBASEFEE => {
1324                let value = state.block.blob_basefee.clone();
1325                state.stack.push(value)?;
1326            }
1327            opcode::LOG0 | opcode::LOG1 | opcode::LOG2 | opcode::LOG3 | opcode::LOG4 => {
1328                if state.is_static {
1329                    state.return_data = SymReturnData::empty(&mut self.cx);
1330                    return Ok(StepOutcome::ExceptionalHalt);
1331                }
1332                let topics = (op - opcode::LOG0) as usize;
1333                let offset = state.stack.peek(0)?.clone();
1334                let size = state.stack.peek(1)?.clone();
1335                if let Some(outcome) =
1336                    self.guard_memory_range(executor, state, worklist, &offset, &size)?
1337                {
1338                    return Ok(outcome);
1339                }
1340                let offset = state.stack.pop()?;
1341                if offset.contains_gasleft() {
1342                    return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
1343                }
1344                let size = state.stack.pop()?;
1345                if size.contains_gasleft() {
1346                    return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
1347                }
1348                let (data_len, data) = match state.constrained_usize_checked(&mut self.cx, &size) {
1349                    Some(Ok(size)) => (
1350                        SymExpr::constant(&mut self.cx, U256::from(size)),
1351                        state.memory.read_bytes_offset(&mut self.cx, offset, size),
1352                    ),
1353                    Some(Err(_)) => {
1354                        return Ok(StepOutcome::Revert);
1355                    }
1356                    None => {
1357                        let max_limit = self.config.max_calldata_bytes as usize;
1358                        let max_size = self.solver_upper_bound_usize(
1359                            state,
1360                            &size,
1361                            max_limit,
1362                            "symbolic LOG size",
1363                        )?;
1364                        let data = state.memory.read_bytes_symbolic_size(
1365                            &mut self.cx,
1366                            offset,
1367                            size.clone(),
1368                            max_size,
1369                        );
1370                        (size, data)
1371                    }
1372                };
1373                let mut log_topics = Vec::with_capacity(topics);
1374                for _ in 0..topics {
1375                    let topic = state.stack.pop()?;
1376                    if topic.contains_gasleft() {
1377                        return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
1378                    }
1379                    log_topics.push(topic);
1380                }
1381                return self.handle_log(
1382                    state,
1383                    SymbolicLog::new(log_topics, data_len, data, state.address),
1384                );
1385            }
1386            _ => return Err(SymbolicError::UnsupportedOpcode(op)),
1387        };
1388
1389        Ok(StepOutcome::Continue)
1390    }
1391
1392    fn resolve_jump_destination(
1393        &mut self,
1394        state: &PathState,
1395        jumpdests: &JumpTable,
1396        dest: SymExpr,
1397        unsupported: &'static str,
1398    ) -> Result<Option<usize>, SymbolicError> {
1399        let dest = state.expect_constrained_word(&mut self.cx, dest, unsupported)?;
1400        let Ok(dest) = usize::try_from(dest) else { return Ok(None) };
1401        Ok(jumpdests.is_valid(dest).then_some(dest))
1402    }
1403
1404    fn branch_invalid_jumpi(
1405        &mut self,
1406        state: &mut PathState,
1407        worklist: &mut VecDeque<PathState>,
1408        taken: SymBoolExpr,
1409    ) -> Result<StepOutcome, SymbolicError> {
1410        let (taken_constraints, taken_sat) =
1411            self.constraints_with_condition(state, taken.clone())?;
1412        let not_taken = taken.clone().not(&mut self.cx);
1413        let (taken_seed_models, not_taken_seed_models) = state.split_corpus_seed_models(&taken);
1414        if !taken_sat {
1415            state.constraints.push(not_taken);
1416            state.set_corpus_seed_models(not_taken_seed_models);
1417            return Ok(StepOutcome::Continue);
1418        }
1419
1420        let (not_taken_constraints, not_taken_sat) =
1421            self.constraints_with_condition(state, not_taken)?;
1422        if not_taken_sat {
1423            let mut fallthrough = state.clone();
1424            fallthrough.constraints = not_taken_constraints;
1425            fallthrough.set_corpus_seed_models(not_taken_seed_models);
1426            worklist.push_back(fallthrough);
1427        }
1428        state.constraints = taken_constraints;
1429        state.set_corpus_seed_models(taken_seed_models);
1430        state.return_data = SymReturnData::empty(&mut self.cx);
1431        Ok(StepOutcome::ExceptionalHalt)
1432    }
1433
1434    fn guard_returndata_copy_range(
1435        &mut self,
1436        state: &mut PathState,
1437        worklist: &mut VecDeque<PathState>,
1438        offset: &SymExpr,
1439        size: &SymExpr,
1440    ) -> Result<Option<StepOutcome>, SymbolicError> {
1441        if offset.contains_gasleft() || size.contains_gasleft() {
1442            return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
1443        }
1444        let return_data_len = state.return_data.len_word.clone();
1445        let offset_in_bounds = SymBoolExpr::cmp_word_expr(
1446            &mut self.cx,
1447            SymCmpOp::Ule,
1448            offset,
1449            return_data_len.clone(),
1450        );
1451        let remaining =
1452            SymExpr::binop(&mut self.cx, SymBinOp::Sub, return_data_len, offset.clone());
1453        let size_in_bounds =
1454            SymBoolExpr::cmp_word_expr(&mut self.cx, SymCmpOp::Ule, size, remaining);
1455        let valid_access = SymBoolExpr::and(&mut self.cx, vec![offset_in_bounds, size_in_bounds]);
1456        self.apply_memory_access_guard(state, worklist, valid_access)
1457    }
1458
1459    pub(super) fn return_or_revert(
1460        &mut self,
1461        state: &mut PathState,
1462        is_revert: bool,
1463    ) -> Result<StepOutcome, SymbolicError> {
1464        let offset = state.stack.pop()?;
1465        let size = state.stack.pop()?;
1466        match state.constrained_usize_checked(&mut self.cx, &size) {
1467            Some(Ok(size)) => {
1468                state.return_data = state.memory.return_data(&mut self.cx, offset.clone(), size)?;
1469                if is_revert {
1470                    Ok(self.classify_revert(state, offset, size))
1471                } else {
1472                    Ok(StepOutcome::Halt)
1473                }
1474            }
1475            Some(Err(_)) => Ok(StepOutcome::Revert),
1476            None => {
1477                let max_limit = self.config.max_calldata_bytes as usize;
1478                let reason =
1479                    if is_revert { "symbolic REVERT size" } else { "symbolic RETURN size" };
1480                let max_size = self.solver_upper_bound_usize(state, &size, max_limit, reason)?;
1481                state.return_data =
1482                    state.memory.return_data_symbolic_size(&mut self.cx, offset, size, max_size)?;
1483                Ok(if is_revert { StepOutcome::Revert } else { StepOutcome::Halt })
1484            }
1485        }
1486    }
1487
1488    pub(super) fn classify_revert(
1489        &mut self,
1490        state: &PathState,
1491        offset: SymExpr,
1492        size: usize,
1493    ) -> StepOutcome {
1494        if state.call_depth == 0
1495            && let Some(offset) = offset.as_const()
1496            && let Ok(offset) = usize::try_from(offset)
1497            && let Ok(data) = state.memory.read_concrete(&mut self.cx, offset, size)
1498            && is_assertion_revert(&data)
1499        {
1500            StepOutcome::Failure
1501        } else {
1502            StepOutcome::Revert
1503        }
1504    }
1505}
1506
1507/// Returns the activation fork for opcodes implemented by the symbolic executor.
1508const fn opcode_activation(op: u8) -> SpecId {
1509    match op {
1510        opcode::DELEGATECALL => SpecId::HOMESTEAD,
1511        opcode::RETURNDATASIZE | opcode::RETURNDATACOPY | opcode::STATICCALL | opcode::REVERT => {
1512            SpecId::BYZANTIUM
1513        }
1514        opcode::SHL | opcode::SHR | opcode::SAR | opcode::EXTCODEHASH | opcode::CREATE2 => {
1515            SpecId::PETERSBURG
1516        }
1517        opcode::CHAINID | opcode::SELFBALANCE => SpecId::ISTANBUL,
1518        opcode::BASEFEE => SpecId::LONDON,
1519        opcode::PUSH0 => SpecId::SHANGHAI,
1520        opcode::TLOAD | opcode::TSTORE | opcode::MCOPY | opcode::BLOBHASH | opcode::BLOBBASEFEE => {
1521            SpecId::CANCUN
1522        }
1523        _ => SpecId::FRONTIER,
1524    }
1525}
foundry_evm_symbolic/executor/opcodes.rs

foundry_evm_symbolic/executor/
opcodes.rs
