1use super::*;
2
3#[derive(Clone, Debug, Default)]
4pub(crate) struct SymStack(Vec<SymExpr>);
5
6impl SymStack {
7 pub(crate) fn push(&mut self, value: SymExpr) -> Result<(), SymbolicError> {
8 if self.0.len() >= EVM_STACK_LIMIT {
9 return Err(SymbolicError::StackOverflow);
10 }
11 self.0.push(value);
12 Ok(())
13 }
14
15 pub(crate) fn pop(&mut self) -> Result<SymExpr, SymbolicError> {
16 self.0.pop().ok_or(SymbolicError::StackUnderflow)
17 }
18
19 pub(crate) fn peek(&self, index_from_top: usize) -> Result<&SymExpr, SymbolicError> {
20 self.0
21 .get(
22 self.0
23 .len()
24 .checked_sub(index_from_top + 1)
25 .ok_or(SymbolicError::StackUnderflow)?,
26 )
27 .ok_or(SymbolicError::StackUnderflow)
28 }
29
30 pub(crate) fn swap(&mut self, index_from_top: usize) -> Result<(), SymbolicError> {
31 let len = self.0.len();
32 let other = len.checked_sub(index_from_top + 1).ok_or(SymbolicError::StackUnderflow)?;
33 self.0.swap(len - 1, other);
34 Ok(())
35 }
36}
37
38#[derive(Clone, Debug)]
39pub(crate) enum BoundedCopySize {
40 Concrete(usize),
41 Symbolic { size: SymExpr, max_size: usize },
42}
43
44#[derive(Clone, Debug, Default)]
45pub(crate) struct SymMemory {
46 symbolic_writes: Vec<SymbolicMemoryWrite>,
47 size: usize,
48}
49
50#[derive(Clone, Debug)]
51struct SymbolicMemoryWrite {
52 offset: SymExpr,
53 bytes: SymBytes,
54}
55
56impl SymbolicMemoryWrite {
57 fn size_after_access(&self, cx: &mut SymCx) -> SymExpr {
58 let len = SymExpr::constant(cx, U256::from(self.bytes.len()));
59 let end = SymExpr::binop(cx, SymBinOp::Add, self.offset.clone(), len);
60 let round = SymExpr::constant(cx, U256::from(31));
61 let rounded = SymExpr::binop(cx, SymBinOp::Add, end, round);
62 let mask = SymExpr::constant(cx, !U256::from(31));
63 SymExpr::binop(cx, SymBinOp::And, rounded, mask)
64 }
65
66 fn concrete_offset(&self) -> Option<usize> {
67 self.offset.eval().and_then(|offset| usize::try_from(offset).ok())
68 }
69
70 fn concrete_byte_index(&self, offset: usize) -> Option<usize> {
71 let write_offset = self.concrete_offset()?;
72 let idx = offset.checked_sub(write_offset)?;
73 (idx < self.bytes.len()).then_some(idx)
74 }
75
76 fn concrete_byte(&self, cx: &mut SymCx, offset: usize) -> Option<SymExpr> {
77 self.concrete_byte_index(offset).map(|idx| self.bytes.byte(cx, idx))
78 }
79}
80
81impl SymMemory {
82 fn size_after_access(offset: usize, len: usize) -> usize {
83 let Some(end) = offset.checked_add(len) else {
84 return usize::MAX & !31usize;
85 };
86 end.checked_add(31).map(|size| size & !31usize).unwrap_or(usize::MAX & !31usize)
87 }
88
89 fn max_size_word(cx: &mut SymCx, left: SymExpr, right: SymExpr) -> SymExpr {
90 if let (Some(left_value), Some(right_value)) = (left.as_const(), right.as_const()) {
91 return SymExpr::constant(cx, left_value.max(right_value));
92 }
93 if left == right {
94 left
95 } else {
96 let condition = SymBoolExpr::cmp(cx, SymCmpOp::Ult, left.clone(), right.clone());
97 SymExpr::ite(cx, condition, right, left)
98 }
99 }
100
101 pub(crate) fn store_word(&mut self, cx: &mut SymCx, offset: usize, value: SymExpr) {
102 let bytes = value.into_bytes(cx);
103 self.store_bytes(cx, offset, bytes);
104 }
105
106 pub(crate) fn store_word_offset(&mut self, cx: &mut SymCx, offset: SymExpr, value: SymExpr) {
107 if let Some(offset) = offset.as_const() {
108 if let Ok(offset) = usize::try_from(offset) {
109 self.store_word(cx, offset, value);
110 }
111 } else {
112 self.store_symbolic_bytes(offset, value.into_bytes(cx));
113 }
114 }
115
116 pub(crate) fn store_byte(&mut self, cx: &mut SymCx, offset: usize, value: SymExpr) {
117 let byte = value.low_byte(cx);
118 let bytes = SymBytes::exprs(cx, vec![byte]);
119 self.store_bytes(cx, offset, bytes);
120 }
121
122 pub(crate) fn store_byte_offset(&mut self, cx: &mut SymCx, offset: SymExpr, value: SymExpr) {
123 if let Some(offset) = offset.as_const() {
124 if let Ok(offset) = usize::try_from(offset) {
125 self.store_byte(cx, offset, value);
126 }
127 } else {
128 let byte = value.low_byte(cx);
129 let bytes = SymBytes::exprs(cx, vec![byte]);
130 self.store_symbolic_bytes(offset, bytes);
131 }
132 }
133
134 pub(crate) fn store_bytes(&mut self, cx: &mut SymCx, offset: usize, bytes: SymBytes) {
135 if bytes.is_empty() {
136 return;
137 }
138 self.size = self.size.max(Self::size_after_access(offset, bytes.len()));
139 let offset = SymExpr::constant(cx, U256::from(offset));
140 self.store_symbolic_bytes(offset, bytes);
141 }
142
143 pub(crate) fn store_symbolic_bytes(&mut self, offset: SymExpr, bytes: SymBytes) {
144 if bytes.is_empty() {
145 return;
146 }
147 self.symbolic_writes.push(SymbolicMemoryWrite { offset, bytes });
148 }
149
150 pub(crate) fn store_bytes_offset(&mut self, cx: &mut SymCx, offset: SymExpr, bytes: SymBytes) {
151 if let Some(offset) = offset.as_const() {
152 if let Ok(offset) = usize::try_from(offset) {
153 self.store_bytes(cx, offset, bytes);
154 }
155 } else {
156 self.store_symbolic_bytes(offset, bytes);
157 }
158 }
159
160 pub(crate) fn load_word(
161 &self,
162 cx: &mut SymCx,
163 offset: usize,
164 ) -> Result<SymExpr, SymbolicError> {
165 let offset = SymExpr::constant(cx, U256::from(offset));
166 Ok(self.read_bytes_offset(cx, offset, 32).word_at(cx, 0))
167 }
168
169 pub(crate) fn load_word_offset(
170 &self,
171 cx: &mut SymCx,
172 offset: SymExpr,
173 ) -> Result<SymExpr, SymbolicError> {
174 if let Some(offset) = offset.as_const() {
175 let Ok(offset) = usize::try_from(offset) else { return Ok(SymExpr::zero(cx)) };
176 self.load_word(cx, offset)
177 } else {
178 self.load_word_dynamic(cx, &offset)
179 }
180 }
181
182 fn load_word_dynamic(
183 &self,
184 cx: &mut SymCx,
185 offset: &SymExpr,
186 ) -> Result<SymExpr, SymbolicError> {
187 let mut result = SymExpr::zero(cx);
188 for candidate in (0..self.size).rev() {
189 let candidate_expr = SymExpr::constant(cx, U256::from(candidate));
190 let condition = SymBoolExpr::eq(cx, offset.clone(), candidate_expr);
191 let word = self.load_word(cx, candidate)?;
192 result = SymExpr::ite(cx, condition, word, result);
193 }
194 Ok(result)
195 }
196
197 pub(crate) fn read_concrete(
198 &self,
199 cx: &mut SymCx,
200 offset: usize,
201 size: usize,
202 ) -> Result<Vec<u8>, SymbolicError> {
203 if let Some(bytes) = self.read_stored_bytes(cx, offset, size) {
204 return bytes.concrete_bytes(cx, "symbolic memory read");
205 }
206
207 let mut out = vec![0u8; size];
208 for (idx, byte) in out.iter_mut().enumerate() {
209 if let Some(value) = self.byte(cx, offset + idx).as_const() {
210 *byte = value.to::<u8>();
211 } else {
212 return Err(SymbolicError::Unsupported("symbolic memory read"));
213 }
214 }
215 Ok(out)
216 }
217
218 pub(crate) fn read_byte_exprs(
219 &self,
220 cx: &mut SymCx,
221 offset: usize,
222 size: usize,
223 ) -> Vec<SymExpr> {
224 self.read_bytes(cx, offset, size).materialize(cx)
225 }
226
227 pub(crate) fn read_byte_exprs_offset(
228 &self,
229 cx: &mut SymCx,
230 offset: SymExpr,
231 size: usize,
232 ) -> Vec<SymExpr> {
233 self.read_bytes_offset(cx, offset, size).materialize(cx)
234 }
235
236 pub(crate) fn read_bytes(&self, cx: &mut SymCx, offset: usize, size: usize) -> SymBytes {
237 let offset = SymExpr::constant(cx, U256::from(offset));
238 self.read_bytes_offset(cx, offset, size)
239 }
240
241 pub(crate) fn read_bytes_offset(
242 &self,
243 cx: &mut SymCx,
244 offset: SymExpr,
245 size: usize,
246 ) -> SymBytes {
247 if let Some(offset) = offset.as_const() {
248 let Ok(offset) = usize::try_from(offset) else {
249 return SymBytes::concrete(cx, vec![0; size]);
250 };
251 if let Some(bytes) = self.read_stored_bytes(cx, offset, size) {
252 return bytes;
253 }
254 let bytes = (0..size).map(|idx| self.byte(cx, offset + idx)).collect();
255 SymBytes::exprs(cx, bytes)
256 } else {
257 let bytes =
258 (0..size).map(|idx| self.byte_dynamic_with_delta(cx, &offset, idx)).collect();
259 SymBytes::exprs(cx, bytes)
260 }
261 }
262
263 fn read_stored_bytes(&self, cx: &mut SymCx, offset: usize, size: usize) -> Option<SymBytes> {
264 if size == 0 {
265 return Some(SymBytes::empty(cx));
266 }
267 let end = offset.checked_add(size)?;
268
269 let mut unresolved = vec![(offset, end)];
270 let mut pieces = Vec::new();
271
272 for write in self.symbolic_writes.iter().rev() {
273 if unresolved.is_empty() {
274 break;
275 }
276
277 let write_offset = write.concrete_offset()?;
278 let write_end = write_offset.checked_add(write.bytes.len())?;
279
280 if write_end <= offset || end <= write_offset {
281 continue;
282 }
283
284 let mut next_unresolved = Vec::new();
285 for (start, end) in unresolved {
286 let overlap_start = start.max(write_offset);
287 let overlap_end = end.min(write_end);
288
289 if overlap_start >= overlap_end {
290 next_unresolved.push((start, end));
291 continue;
292 }
293
294 if start < overlap_start {
295 next_unresolved.push((start, overlap_start));
296 }
297
298 pieces.push((
299 overlap_start - offset,
300 write.bytes.slice_concrete(
301 cx,
302 overlap_start - write_offset,
303 overlap_end - overlap_start,
304 ),
305 ));
306
307 if overlap_end < end {
308 next_unresolved.push((overlap_end, end));
309 }
310 }
311 unresolved = next_unresolved;
312 }
313
314 pieces.extend(
315 unresolved
316 .into_iter()
317 .map(|(start, end)| (start - offset, SymBytes::concrete(cx, vec![0; end - start]))),
318 );
319 pieces.sort_by_key(|(offset, _)| *offset);
320
321 Some(SymBytes::concat(cx, pieces.into_iter().map(|(_, bytes)| bytes)))
322 }
323
324 pub(crate) fn read_byte_exprs_symbolic_size(
325 &self,
326 cx: &mut SymCx,
327 offset: SymExpr,
328 size: SymExpr,
329 max_size: usize,
330 ) -> Vec<SymExpr> {
331 self.read_bytes_symbolic_size(cx, offset, size, max_size).materialize(cx)
332 }
333
334 pub(crate) fn read_bytes_symbolic_size(
335 &self,
336 cx: &mut SymCx,
337 offset: SymExpr,
338 size: SymExpr,
339 max_size: usize,
340 ) -> SymBytes {
341 if let Some(size) = size.eval() {
342 let size = usize::try_from(size).map_or(max_size, |size| size.min(max_size));
343 let bytes = self.read_bytes_offset(cx, offset, size);
344 let padding = SymBytes::concrete(cx, vec![0; max_size - size]);
345 return SymBytes::concat(cx, [bytes, padding]);
346 }
347
348 let bytes = self.read_bytes_offset(cx, offset, max_size);
349 SymBytes::sized(cx, bytes, size, max_size)
350 }
351
352 pub(crate) fn byte(&self, cx: &mut SymCx, offset: usize) -> SymExpr {
353 let mut writes = self.symbolic_writes.as_slice();
354 let mut result = if let Some(base_idx) =
355 writes.iter().rposition(|write| write.concrete_byte_index(offset).is_some())
356 {
357 let write = &writes[base_idx];
358 let byte = write.concrete_byte(cx, offset).expect("concrete byte index is present");
359 writes = &writes[base_idx + 1..];
360 byte
361 } else {
362 SymExpr::zero(cx)
363 };
364
365 for write in writes {
366 if let Some(byte) = write.concrete_byte(cx, offset) {
367 result = byte;
368 continue;
369 }
370 if write.concrete_offset().is_some() {
371 continue;
372 }
373 for idx in 0..write.bytes.len() {
374 let write_offset = SymExpr::add_const(cx, write.offset.clone(), U256::from(idx));
375 let offset = SymExpr::constant(cx, U256::from(offset));
376 let condition = SymBoolExpr::eq(cx, write_offset, offset);
377 let byte = write.bytes.byte(cx, idx);
378 result = SymExpr::ite(cx, condition, byte, result);
379 }
380 }
381 result
382 }
383
384 pub(crate) fn byte_dynamic_with_delta(
385 &self,
386 cx: &mut SymCx,
387 offset: &SymExpr,
388 delta: usize,
389 ) -> SymExpr {
390 let mut result = SymExpr::zero(cx);
391 for candidate in (delta..self.size).rev() {
392 let candidate_expr = SymExpr::constant(cx, U256::from(candidate - delta));
393 let condition = SymBoolExpr::eq(cx, offset.clone(), candidate_expr);
394 let byte = self.byte(cx, candidate);
395 result = SymExpr::ite(cx, condition, byte, result);
396 }
397 result
398 }
399
400 pub(crate) fn size_word(&self, cx: &mut SymCx) -> SymExpr {
401 let mut size = SymExpr::constant(cx, U256::from(self.size));
402 for write in &self.symbolic_writes {
403 if write.concrete_offset().is_some() {
404 continue;
405 }
406 let write_size = write.size_after_access(cx);
407 size = Self::max_size_word(cx, size, write_size);
408 }
409 size
410 }
411
412 pub(crate) fn copy_bytes_offset(&mut self, cx: &mut SymCx, dest: SymExpr, src: SymBytes) {
413 self.store_bytes_offset(cx, dest, src);
414 }
415
416 pub(crate) fn copy_bytes_size_offset(
417 &mut self,
418 cx: &mut SymCx,
419 dest: SymExpr,
420 size: SymExpr,
421 src: SymBytes,
422 ) -> Result<(), SymbolicError> {
423 if src.is_empty() {
424 return Ok(());
425 }
426 if let Some(size) = size.eval() {
427 let size = usize::try_from(size).map_or(src.len(), |size| size.min(src.len()));
428 if size != 0 {
429 let src = src.slice_concrete(cx, 0, size);
430 self.store_bytes_offset(cx, dest, src);
431 }
432 return Ok(());
433 }
434
435 if let Some(dest) = dest.as_const() {
436 if let Ok(dest) = usize::try_from(dest) {
437 let bytes = (0..src.len())
438 .map(|idx| {
439 let source = src.byte(cx, idx);
440 self.copy_size_byte_at(cx, dest + idx, idx, &size, source)
441 })
442 .collect::<Vec<_>>();
443 let bytes = SymBytes::exprs(cx, bytes);
444 self.store_bytes(cx, dest, bytes);
445 }
446 } else {
447 let bytes = (0..src.len())
448 .map(|idx| {
449 let existing = self.byte_dynamic_with_delta(cx, &dest, idx);
450 let source = src.byte(cx, idx);
451 Self::copy_size_byte(cx, idx, &size, source, existing)
452 })
453 .collect();
454 let bytes = SymBytes::exprs(cx, bytes);
455 self.store_symbolic_bytes(dest, bytes);
456 }
457 Ok(())
458 }
459
460 pub(crate) fn copy_calldata_to_offset(
461 &mut self,
462 cx: &mut SymCx,
463 dest: SymExpr,
464 offset: SymExpr,
465 size: usize,
466 calldata: &SymCalldata,
467 ) -> Result<(), SymbolicError> {
468 if let Some(offset) = offset.as_const() {
469 let Ok(offset) = usize::try_from(offset) else {
470 let bytes = SymBytes::concrete(cx, vec![0; size]);
471 self.copy_bytes_offset(cx, dest, bytes);
472 return Ok(());
473 };
474 let offset = SymExpr::constant(cx, U256::from(offset));
475 let bytes = calldata.read_bytes_offset(cx, offset, size);
476 self.store_bytes_offset(cx, dest, bytes);
477 } else {
478 let bytes = calldata.read_bytes_offset(cx, offset, size);
479 self.store_bytes_offset(cx, dest, bytes);
480 }
481 Ok(())
482 }
483
484 pub(crate) fn copy_calldata_symbolic_size(
485 &mut self,
486 cx: &mut SymCx,
487 dest: SymExpr,
488 offset: SymExpr,
489 size: SymExpr,
490 max_size: usize,
491 calldata: &SymCalldata,
492 ) -> Result<(), SymbolicError> {
493 let bytes = if let Some(offset) = offset.as_const()
494 && let Ok(offset) = usize::try_from(offset)
495 {
496 let offset = SymExpr::constant(cx, U256::from(offset));
497 calldata.read_bytes_offset(cx, offset, max_size)
498 } else {
499 calldata.read_bytes_offset(cx, offset, max_size)
500 };
501 self.copy_bytes_size_offset(cx, dest, size, bytes)
502 }
503
504 fn copy_size_byte_at(
505 &self,
506 cx: &mut SymCx,
507 dest: usize,
508 idx: usize,
509 size: &SymExpr,
510 source: SymExpr,
511 ) -> SymExpr {
512 let existing = self.byte(cx, dest);
513 Self::copy_size_byte(cx, idx, size, source, existing)
514 }
515
516 fn copy_size_byte(
517 cx: &mut SymCx,
518 idx: usize,
519 size: &SymExpr,
520 source: SymExpr,
521 existing: SymExpr,
522 ) -> SymExpr {
523 let idx = SymExpr::constant(cx, U256::from(idx));
524 let condition = SymBoolExpr::cmp(cx, SymCmpOp::Ult, idx, size.clone());
525 SymExpr::ite(cx, condition, source, existing)
526 }
527
528 pub(crate) fn copy_return_data_to_offset(
529 &mut self,
530 cx: &mut SymCx,
531 dest: SymExpr,
532 offset: SymExpr,
533 size: usize,
534 return_data: &SymReturnData,
535 ) -> Result<(), SymbolicError> {
536 if size == 0 {
537 return Ok(());
538 }
539 if let Some(offset) = offset.as_const() {
540 let Ok(offset) = usize::try_from(offset) else {
541 return Err(SymbolicError::Unsupported("out-of-bounds symbolic RETURNDATACOPY"));
542 };
543 if offset.saturating_add(size) > return_data.len() {
544 return Err(SymbolicError::Unsupported("out-of-bounds symbolic RETURNDATACOPY"));
545 }
546 }
547 let bytes = return_data.read_bytes_offset(cx, offset, size);
548 self.store_bytes_offset(cx, dest, bytes);
549 Ok(())
550 }
551
552 pub(crate) fn copy_return_data_symbolic_size(
553 &mut self,
554 cx: &mut SymCx,
555 dest: SymExpr,
556 offset: SymExpr,
557 size: SymExpr,
558 max_size: usize,
559 return_data: &SymReturnData,
560 ) -> Result<(), SymbolicError> {
561 if max_size == 0 {
562 return Ok(());
563 }
564 if let Some(offset) = offset.as_const() {
565 let Ok(offset) = usize::try_from(offset) else {
566 return Err(SymbolicError::Unsupported("out-of-bounds symbolic RETURNDATACOPY"));
567 };
568 if offset.saturating_add(max_size) > return_data.len() {
569 return Err(SymbolicError::Unsupported("out-of-bounds symbolic RETURNDATACOPY"));
570 }
571 }
572 let bytes = return_data.read_bytes_offset(cx, offset, max_size);
573 self.copy_bytes_size_offset(cx, dest, size, bytes)
574 }
575
576 pub(crate) fn copy_call_output_offset(
577 &mut self,
578 cx: &mut SymCx,
579 dest: SymExpr,
580 size: &BoundedCopySize,
581 return_data: &SymReturnData,
582 ) -> Result<(), SymbolicError> {
583 match size {
584 BoundedCopySize::Concrete(size) => {
585 let size = (*size).min(return_data.len());
586 if size != 0 {
587 if return_data.has_symbolic_len() {
588 let bytes = (0..size)
589 .map(|idx| self.call_output_byte(cx, &dest, idx, None, return_data))
590 .collect::<Vec<_>>();
591 let bytes = SymBytes::exprs(cx, bytes);
592 self.store_bytes_offset(cx, dest, bytes);
593 } else {
594 let offset = SymExpr::zero(cx);
595 let bytes = return_data.read_bytes_offset(cx, offset, size);
596 self.store_bytes_offset(cx, dest, bytes);
597 }
598 }
599 }
600 BoundedCopySize::Symbolic { size, max_size } => {
601 let output_size = size.clone();
602 let max_size = (*max_size).min(return_data.len());
603 if max_size != 0 {
604 let bytes = (0..max_size)
605 .map(|idx| {
606 self.call_output_byte(cx, &dest, idx, Some(&output_size), return_data)
607 })
608 .collect::<Vec<_>>();
609 let bytes = SymBytes::exprs(cx, bytes);
610 self.store_bytes_offset(cx, dest, bytes);
611 }
612 }
613 }
614 Ok(())
615 }
616
617 pub(crate) fn call_output_byte(
618 &self,
619 cx: &mut SymCx,
620 dest: &SymExpr,
621 idx: usize,
622 output_size: Option<&SymExpr>,
623 return_data: &SymReturnData,
624 ) -> SymExpr {
625 let mut guards = Vec::new();
626 if let Some(output_size) = output_size {
627 let idx_expr = SymExpr::constant(cx, U256::from(idx));
628 guards.push(SymBoolExpr::cmp(cx, SymCmpOp::Ult, idx_expr, output_size.clone()));
629 }
630 if return_data.has_symbolic_len() {
631 let idx_expr = SymExpr::constant(cx, U256::from(idx));
632 guards.push(SymBoolExpr::cmp(cx, SymCmpOp::Ult, idx_expr, return_data.len_expr()));
633 }
634 let guard = SymBoolExpr::and(cx, guards);
635 match guard.as_const() {
636 Some(true) => return_data.byte(cx, idx),
637 Some(false) => self.call_output_existing_byte(cx, dest, idx),
638 None => {
639 let byte = return_data.byte(cx, idx);
640 let existing = self.call_output_existing_byte(cx, dest, idx);
641 SymExpr::ite(cx, guard, byte, existing)
642 }
643 }
644 }
645
646 pub(crate) fn call_output_existing_byte(
647 &self,
648 cx: &mut SymCx,
649 dest: &SymExpr,
650 idx: usize,
651 ) -> SymExpr {
652 if let Some(dest) = dest.as_const() {
653 match usize::try_from(dest) {
654 Ok(dest) => self.byte(cx, dest + idx),
655 Err(_) => SymExpr::zero(cx),
656 }
657 } else {
658 self.byte_dynamic_with_delta(cx, dest, idx)
659 }
660 }
661
662 pub(crate) fn copy_memory_to_offset(
663 &mut self,
664 cx: &mut SymCx,
665 dest: SymExpr,
666 src: SymExpr,
667 size: usize,
668 ) -> Result<(), SymbolicError> {
669 if size == 0 {
670 return Ok(());
671 }
672 let bytes = self.read_bytes_offset(cx, src, size);
673 self.store_bytes_offset(cx, dest, bytes);
674 Ok(())
675 }
676
677 pub(crate) fn copy_memory_symbolic_size(
678 &mut self,
679 cx: &mut SymCx,
680 dest: SymExpr,
681 src: SymExpr,
682 size: SymExpr,
683 max_size: usize,
684 ) -> Result<(), SymbolicError> {
685 if max_size == 0 {
686 return Ok(());
687 }
688 let source = self.read_bytes_offset(cx, src, max_size);
689 self.copy_bytes_size_offset(cx, dest, size, source)
690 }
691
692 pub(crate) fn return_data(
693 &self,
694 cx: &mut SymCx,
695 offset: SymExpr,
696 size: usize,
697 ) -> Result<SymReturnData, SymbolicError> {
698 let bytes = self.read_bytes_offset(cx, offset, size);
699 Ok(SymReturnData::from_bytes(cx, bytes))
700 }
701
702 pub(crate) fn return_data_symbolic_size(
703 &self,
704 cx: &mut SymCx,
705 offset: SymExpr,
706 size: SymExpr,
707 max_size: usize,
708 ) -> Result<SymReturnData, SymbolicError> {
709 Ok(SymReturnData::from_bytes_with_len(
710 self.read_bytes_symbolic_size(cx, offset, size.clone(), max_size),
711 size,
712 ))
713 }
714}
715
716#[derive(Clone, Debug, PartialEq, Eq)]
717pub(crate) struct SymCode {
718 bytes: SymBytes,
719 jump_table: JumpTable,
720}
721
722#[derive(Clone, Debug, PartialEq, Eq)]
723pub(crate) enum GuardedOpcode {
724 End,
725 Concrete(u8),
726 SymbolicSize { condition: SymBoolExpr, opcode: u8 },
727}
728
729impl SymCode {
730 pub(crate) fn empty(cx: &mut SymCx) -> Self {
731 Self { bytes: SymBytes::empty(cx), jump_table: JumpTable::default() }
732 }
733
734 pub(crate) fn from_byte_exprs(cx: &mut SymCx, bytes: Vec<SymExpr>) -> Self {
735 let bytes = SymBytes::exprs(cx, bytes);
736 Self::from_bytes(cx, bytes)
737 }
738
739 pub(crate) fn from_bytes(cx: &mut SymCx, bytes: SymBytes) -> Self {
740 let analysis = if let Some(bytes) = bytes.as_concrete_slice() {
741 bytes.to_vec()
742 } else {
743 (0..bytes.len())
744 .map(|idx| {
745 bytes.byte(cx, idx).as_const().map_or(opcode::STOP, |value| value.to::<u8>())
746 })
747 .collect::<Vec<_>>()
748 };
749 let analyzed = Bytecode::new_legacy(Bytes::from(analysis));
750 let jump_table = analyzed.legacy_jump_table().cloned().unwrap_or_default();
751 Self { bytes, jump_table }
752 }
753
754 pub(crate) fn concrete(cx: &mut SymCx, bytes: Vec<u8>) -> Self {
755 Self::from_bytecode(cx, &Bytecode::new_legacy(Bytes::from(bytes)))
756 }
757
758 pub(crate) fn from_bytecode(cx: &mut SymCx, bytecode: &Bytecode) -> Self {
759 let bytes = SymBytes::concrete(cx, bytecode.original_byte_slice().to_vec());
760 let jump_table = bytecode.legacy_jump_table().cloned().unwrap_or_default();
761 Self { bytes, jump_table }
762 }
763
764 pub(crate) fn from_memory_offset(
765 cx: &mut SymCx,
766 memory: &SymMemory,
767 offset: SymExpr,
768 size: usize,
769 ) -> Self {
770 let bytes = memory.read_bytes_offset(cx, offset, size);
771 Self::from_bytes(cx, bytes)
772 }
773
774 pub(crate) fn from_memory_symbolic_size(
775 cx: &mut SymCx,
776 memory: &SymMemory,
777 offset: SymExpr,
778 size: SymExpr,
779 max_size: usize,
780 ) -> Self {
781 let bytes = memory.read_bytes_symbolic_size(cx, offset, size, max_size);
782 Self::from_bytes(cx, bytes)
783 }
784
785 pub(crate) fn len(&self) -> usize {
786 self.bytes.len()
787 }
788
789 pub(crate) fn is_empty(&self) -> bool {
790 self.bytes.is_empty()
791 }
792
793 pub(crate) const fn jump_table(&self) -> &JumpTable {
794 &self.jump_table
795 }
796
797 pub(crate) fn opcode(&self, cx: &mut SymCx, pc: usize) -> Result<Option<u8>, SymbolicError> {
798 if pc >= self.len() {
799 return Ok(None);
800 }
801 match self.bytes.byte(cx, pc).as_const() {
802 Some(value) => Ok(Some(value.to::<u8>())),
803 None => Err(SymbolicError::Unsupported("symbolic bytecode opcode")),
804 }
805 }
806
807 pub(crate) fn guarded_opcode(
808 &self,
809 cx: &mut SymCx,
810 pc: usize,
811 ) -> Result<GuardedOpcode, SymbolicError> {
812 if pc >= self.len() {
813 return Ok(GuardedOpcode::End);
814 }
815 let byte = self.bytes.byte(cx, pc);
816 match byte.as_const() {
817 Some(value) => Ok(GuardedOpcode::Concrete(value.to::<u8>())),
818 None => {
819 if let SymExprKind::Ite(condition, then_expr, else_expr) = byte.kind()
820 && else_expr.as_const().is_some_and(|value| value.is_zero())
821 {
822 match then_expr.as_const() {
823 Some(value) if value.is_zero() => Ok(GuardedOpcode::Concrete(0)),
824 Some(value) => Ok(GuardedOpcode::SymbolicSize {
825 condition: condition.clone(),
826 opcode: value.to::<u8>(),
827 }),
828 None => Err(SymbolicError::Unsupported("symbolic bytecode opcode")),
829 }
830 } else {
831 Err(SymbolicError::Unsupported("symbolic bytecode opcode"))
832 }
833 }
834 }
835 }
836
837 pub(crate) fn concrete_range(
838 &self,
839 cx: &mut SymCx,
840 offset: usize,
841 size: usize,
842 reason: &'static str,
843 ) -> Result<Vec<u8>, SymbolicError> {
844 if let Some(bytes) = self.bytes.as_concrete_slice() {
845 let mut out = Vec::with_capacity(size);
846 let end = offset.saturating_add(size).min(bytes.len());
847 if offset < end {
848 out.extend_from_slice(&bytes[offset..end]);
849 }
850 out.resize(size, 0);
851 return Ok(out);
852 }
853
854 let mut out = Vec::with_capacity(size);
855 for idx in 0..size {
856 if offset + idx >= self.len() {
857 out.push(0);
858 continue;
859 }
860 match self.bytes.byte(cx, offset + idx).as_const() {
861 Some(value) => out.push(value.to::<u8>()),
862 None => return Err(SymbolicError::Unsupported(reason)),
863 }
864 }
865 Ok(out)
866 }
867
868 pub(crate) fn read_byte_exprs(
869 &self,
870 cx: &mut SymCx,
871 offset: usize,
872 size: usize,
873 ) -> Vec<SymExpr> {
874 self.read_bytes(cx, offset, size).materialize(cx)
875 }
876
877 pub(crate) fn read_byte_exprs_offset(
878 &self,
879 cx: &mut SymCx,
880 offset: SymExpr,
881 size: usize,
882 ) -> Vec<SymExpr> {
883 self.read_bytes_offset(cx, offset, size).materialize(cx)
884 }
885
886 pub(crate) fn read_bytes(&self, cx: &mut SymCx, offset: usize, size: usize) -> SymBytes {
887 self.bytes.slice_concrete(cx, offset, size)
888 }
889
890 pub(crate) fn read_bytes_offset(
891 &self,
892 cx: &mut SymCx,
893 offset: SymExpr,
894 size: usize,
895 ) -> SymBytes {
896 self.bytes.read_offset(cx, offset, size)
897 }
898
899 pub(crate) fn push_data_word(&self, cx: &mut SymCx, offset: usize, len: usize) -> SymExpr {
900 self.bytes.right_aligned_word(cx, offset, len)
901 }
902
903 pub(crate) fn concrete_bytes(
904 &self,
905 cx: &mut SymCx,
906 reason: &'static str,
907 ) -> Result<Vec<u8>, SymbolicError> {
908 self.concrete_range(cx, 0, self.len(), reason)
909 }
910}
911
912#[derive(Clone, Debug)]
913pub(crate) struct SymReturnData {
914 len_word: SymExpr,
915 bytes: SymBytes,
916}
917
918impl SymReturnData {
919 pub(crate) fn empty(cx: &mut SymCx) -> Self {
920 Self { len_word: SymExpr::zero(cx), bytes: SymBytes::empty(cx) }
921 }
922
923 pub(crate) fn from_words(cx: &mut SymCx, words: Vec<SymExpr>) -> Self {
924 let bytes = words.into_iter().map(|word| word.into_bytes(cx)).collect::<Vec<_>>();
925 let bytes = SymBytes::concat(cx, bytes);
926 Self::from_bytes(cx, bytes)
927 }
928
929 pub(crate) fn from_concrete_bytes(cx: &mut SymCx, bytes: Vec<u8>) -> Self {
930 let bytes = SymBytes::concrete(cx, bytes);
931 Self::from_bytes(cx, bytes)
932 }
933
934 pub(crate) fn from_byte_exprs(cx: &mut SymCx, bytes: Vec<SymExpr>) -> Self {
935 let bytes = SymBytes::exprs(cx, bytes);
936 Self::from_bytes(cx, bytes)
937 }
938
939 pub(crate) fn from_bytes(cx: &mut SymCx, bytes: SymBytes) -> Self {
940 let len = bytes.len();
941 Self { len_word: SymExpr::constant(cx, U256::from(len)), bytes }
942 }
943
944 pub(crate) const fn from_bytes_with_len(bytes: SymBytes, len_word: SymExpr) -> Self {
945 Self { len_word, bytes }
946 }
947
948 pub(crate) fn len_word(&self) -> SymExpr {
949 self.len_word.clone()
950 }
951
952 pub(crate) fn len(&self) -> usize {
953 self.bytes.len()
954 }
955
956 pub(crate) fn len_expr(&self) -> SymExpr {
957 self.len_word.clone()
958 }
959
960 pub(crate) fn has_symbolic_len(&self) -> bool {
961 self.len_word.as_const().is_none()
962 }
963
964 pub(crate) fn byte(&self, cx: &mut SymCx, offset: usize) -> SymExpr {
965 self.bytes.byte(cx, offset)
966 }
967
968 pub(crate) fn read_bytes_offset(
969 &self,
970 cx: &mut SymCx,
971 offset: SymExpr,
972 size: usize,
973 ) -> SymBytes {
974 self.bytes.read_offset(cx, offset, size)
975 }
976
977 pub(crate) fn load_word(
978 &self,
979 cx: &mut SymCx,
980 offset: usize,
981 ) -> Result<SymExpr, SymbolicError> {
982 if offset.saturating_add(32) > self.len() {
983 return Err(SymbolicError::Unsupported("out-of-bounds symbolic returndata word"));
984 }
985 Ok(self.bytes.word_at(cx, offset))
986 }
987
988 pub(crate) fn read_concrete(
989 &self,
990 cx: &mut SymCx,
991 reason: &'static str,
992 ) -> Result<Vec<u8>, SymbolicError> {
993 self.bytes.concrete_bytes(cx, reason)
994 }
995
996 pub(crate) fn to_code(&self, cx: &mut SymCx) -> Result<SymCode, SymbolicError> {
997 if self.has_symbolic_len() {
998 return Err(SymbolicError::Unsupported(
999 "CREATE with symbolic runtime size not modeled",
1000 ));
1001 }
1002 Ok(SymCode::from_bytes(cx, self.bytes.clone()))
1003 }
1004}