1use super::{expr::hashcons::HashConsed, *};
2
3#[derive(Clone, PartialEq, Eq, Hash)]
4pub(crate) struct SymBytes {
5 pub(in crate::runtime) kind: HashConsed<SymBytesKind>,
6}
7
8impl fmt::Debug for SymBytes {
9 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
10 self.kind().fmt(f)
11 }
12}
13
14#[derive(Debug, PartialEq, Eq, Hash)]
15pub(in crate::runtime) enum SymBytesKind {
16 Concrete(Vec<u8>),
17 Exprs(Vec<SymExpr>),
18 Word(SymExpr),
19 Concat(Vec<SymBytes>),
20 Slice { bytes: SymBytes, offset: SymExpr, len: usize },
21 Sized { bytes: SymBytes, size: SymExpr, max_size: usize },
22}
23
24impl SymBytes {
25 fn from_kind(cx: &mut SymCx, kind: SymBytesKind) -> Self {
26 cx.mk_bytes_kind(kind)
27 }
28
29 fn kind(&self) -> &SymBytesKind {
30 self.kind.value()
31 }
32
33 pub(crate) fn empty(cx: &mut SymCx) -> Self {
34 Self::from_kind(cx, SymBytesKind::Concrete(Vec::new()))
35 }
36
37 pub(crate) fn concrete(cx: &mut SymCx, bytes: Vec<u8>) -> Self {
38 Self::from_kind(cx, SymBytesKind::Concrete(bytes))
39 }
40
41 pub(crate) fn as_concrete_slice(&self) -> Option<&[u8]> {
42 match self.kind() {
43 SymBytesKind::Concrete(bytes) => Some(bytes),
44 _ => None,
45 }
46 }
47
48 pub(crate) fn exprs(cx: &mut SymCx, bytes: Vec<SymExpr>) -> Self {
49 if let Ok(concrete) = concrete_expr_bytes(&bytes, "symbolic bytes") {
50 Self::concrete(cx, concrete)
51 } else {
52 Self::from_kind(cx, SymBytesKind::Exprs(bytes))
53 }
54 }
55
56 pub(crate) fn word(cx: &mut SymCx, word: SymExpr) -> Self {
57 if let Some(word) = word.as_const() {
58 Self::concrete(cx, word.to_be_bytes::<32>().to_vec())
59 } else {
60 Self::from_kind(cx, SymBytesKind::Word(word))
61 }
62 }
63
64 pub(crate) fn concat(cx: &mut SymCx, bytes: impl IntoIterator<Item = Self>) -> Self {
65 let mut out = Vec::new();
66 for bytes in bytes {
67 match bytes.kind() {
68 SymBytesKind::Concrete(values) if values.is_empty() => {}
69 SymBytesKind::Concat(values) => out.extend(values.iter().cloned()),
70 _ => out.push(bytes),
71 }
72 }
73 match out.len() {
74 0 => Self::empty(cx),
75 1 => out.pop().expect("single item exists"),
76 _ => Self::from_kind(cx, SymBytesKind::Concat(out)),
77 }
78 }
79
80 pub(crate) fn slice(cx: &mut SymCx, bytes: Self, offset: SymExpr, len: usize) -> Self {
81 if len == 0 {
82 return Self::empty(cx);
83 }
84 if let Some(offset) = offset.eval() {
85 let Ok(offset) = usize::try_from(offset) else {
86 return Self::concrete(cx, vec![0; len]);
87 };
88 return bytes.slice_concrete(cx, offset, len);
89 }
90 Self::slice_node(cx, bytes, offset, len)
91 }
92
93 fn slice_node(cx: &mut SymCx, bytes: Self, offset: SymExpr, len: usize) -> Self {
94 Self::from_kind(cx, SymBytesKind::Slice { bytes, offset, len })
95 }
96
97 pub(crate) fn sized(cx: &mut SymCx, bytes: Self, size: SymExpr, max_size: usize) -> Self {
98 if max_size == 0 {
99 return Self::empty(cx);
100 }
101 if let Some(size) = size.eval() {
102 let size = usize::try_from(size).map_or(max_size, |size| size.min(max_size));
103 let bytes = bytes.slice_concrete(cx, 0, size);
104 let padding = Self::concrete(cx, vec![0; max_size - size]);
105 return Self::concat(cx, [bytes, padding]);
106 }
107 Self::from_kind(cx, SymBytesKind::Sized { bytes, size, max_size })
108 }
109
110 pub(crate) fn len(&self) -> usize {
111 match self.kind() {
112 SymBytesKind::Concrete(bytes) => bytes.len(),
113 SymBytesKind::Exprs(bytes) => bytes.len(),
114 SymBytesKind::Word(_) => 32,
115 SymBytesKind::Concat(values) => {
116 values.iter().fold(0usize, |len, bytes| len.saturating_add(bytes.len()))
117 }
118 SymBytesKind::Slice { len, .. } => *len,
119 SymBytesKind::Sized { max_size, .. } => *max_size,
120 }
121 }
122
123 pub(crate) fn is_empty(&self) -> bool {
124 self.len() == 0
125 }
126
127 pub(crate) fn byte(&self, cx: &mut SymCx, offset: usize) -> SymExpr {
128 match self.kind() {
129 SymBytesKind::Concrete(bytes) => bytes
130 .get(offset)
131 .copied()
132 .map(|byte| SymExpr::constant(cx, U256::from(byte)))
133 .unwrap_or_else(|| SymExpr::zero(cx)),
134 SymBytesKind::Exprs(bytes) => {
135 bytes.get(offset).cloned().unwrap_or_else(|| SymExpr::zero(cx))
136 }
137 SymBytesKind::Word(word) => {
138 if offset >= 32 {
139 SymExpr::zero(cx)
140 } else if let Some(byte) = word.known_byte(offset) {
141 SymExpr::constant(cx, U256::from(byte))
142 } else {
143 word.extracted_byte(cx, offset)
144 }
145 }
146 SymBytesKind::Concat(values) => {
147 let mut offset = offset;
148 for bytes in values {
149 if offset < bytes.len() {
150 return bytes.byte(cx, offset);
151 }
152 offset = offset.saturating_sub(bytes.len());
153 }
154 SymExpr::zero(cx)
155 }
156 SymBytesKind::Slice { bytes, offset: base_offset, len } => {
157 if offset >= *len {
158 SymExpr::zero(cx)
159 } else if let Some(base_offset) = base_offset.eval() {
160 let Ok(base_offset) = usize::try_from(base_offset) else {
161 return SymExpr::zero(cx);
162 };
163 let Some(offset) = base_offset.checked_add(offset) else {
164 return SymExpr::zero(cx);
165 };
166 bytes.byte(cx, offset)
167 } else {
168 bytes.byte_dynamic_with_delta(cx, base_offset, offset)
169 }
170 }
171 SymBytesKind::Sized { bytes, size, max_size } => {
172 if offset >= *max_size {
173 return SymExpr::zero(cx);
174 }
175 let source = bytes.byte(cx, offset);
176 let offset = SymExpr::constant(cx, U256::from(offset));
177 let condition = SymBoolExpr::cmp(cx, SymCmpOp::Ult, offset, size.clone());
178 let zero = SymExpr::zero(cx);
179 SymExpr::ite(cx, condition, source, zero)
180 }
181 }
182 }
183
184 pub(crate) fn byte_dynamic_with_delta(
185 &self,
186 cx: &mut SymCx,
187 offset: &SymExpr,
188 delta: usize,
189 ) -> SymExpr {
190 let mut result = SymExpr::zero(cx);
191 for candidate in (delta..self.len()).rev() {
192 let candidate_offset = candidate - delta;
193 let candidate_expr = SymExpr::constant(cx, U256::from(candidate_offset));
194 let condition = SymBoolExpr::eq(cx, offset.clone(), candidate_expr);
195 let byte = self.byte(cx, candidate);
196 result = SymExpr::ite(cx, condition, byte, result);
197 }
198 result
199 }
200
201 pub(crate) fn slice_concrete(&self, cx: &mut SymCx, offset: usize, len: usize) -> Self {
202 if len == 0 {
203 return Self::empty(cx);
204 }
205 if offset == 0 && len == self.len() {
206 return self.clone();
207 }
208 match self.kind() {
209 SymBytesKind::Concrete(bytes) => {
210 let out = if offset.checked_add(len).is_some_and(|end| end <= bytes.len()) {
211 bytes[offset..offset + len].to_vec()
212 } else {
213 (0..len)
214 .map(|idx| bytes.get(offset + idx).copied().unwrap_or_default())
215 .collect()
216 };
217 Self::concrete(cx, out)
218 }
219 SymBytesKind::Exprs(bytes) => {
220 let bytes = (0..len)
221 .map(|idx| {
222 bytes.get(offset + idx).cloned().unwrap_or_else(|| SymExpr::zero(cx))
223 })
224 .collect();
225 Self::exprs(cx, bytes)
226 }
227 SymBytesKind::Word(word) if offset == 0 && len == 32 => Self::word(cx, word.clone()),
228 SymBytesKind::Word(_) | SymBytesKind::Sized { .. } => {
229 let offset = SymExpr::constant(cx, U256::from(offset));
230 Self::slice_node(cx, self.clone(), offset, len)
231 }
232 SymBytesKind::Slice { bytes, offset: base_offset, .. } => {
233 if let Some(base_offset) = base_offset.eval()
234 && let Ok(base_offset) = usize::try_from(base_offset)
235 && let Some(offset) = base_offset.checked_add(offset)
236 {
237 bytes.slice_concrete(cx, offset, len)
238 } else {
239 let offset = SymExpr::constant(cx, U256::from(offset));
240 Self::slice_node(cx, self.clone(), offset, len)
241 }
242 }
243 SymBytesKind::Concat(values) => {
244 let mut offset = offset;
245 let mut len = len;
246 let mut out = Vec::new();
247 for bytes in values {
248 if len == 0 {
249 break;
250 }
251
252 let bytes_len = bytes.len();
253 if offset >= bytes_len {
254 offset -= bytes_len;
255 continue;
256 }
257
258 let take = (bytes_len - offset).min(len);
259 if offset == 0 && take == bytes_len {
260 out.push(bytes.clone());
261 } else {
262 out.push(bytes.slice_concrete(cx, offset, take));
263 }
264 len -= take;
265 offset = 0;
266 }
267
268 if len != 0 {
269 out.push(Self::concrete(cx, vec![0; len]));
270 }
271 Self::concat(cx, out)
272 }
273 }
274 }
275
276 pub(crate) fn read_offset(&self, cx: &mut SymCx, offset: SymExpr, len: usize) -> Self {
277 Self::slice(cx, self.clone(), offset, len)
278 }
279
280 pub(crate) fn word_at(&self, cx: &mut SymCx, offset: usize) -> SymExpr {
281 if let Some(word) = self.word_fragment_at(cx, offset, 32, 0) {
282 return word;
283 }
284
285 match self.kind() {
286 SymBytesKind::Concrete(bytes) => {
287 let mut word = [0u8; 32];
288 if offset < bytes.len() {
289 let take = (bytes.len() - offset).min(32);
290 word[..take].copy_from_slice(&bytes[offset..offset + take]);
291 }
292 SymExpr::constant(cx, U256::from_be_bytes(word))
293 }
294 SymBytesKind::Exprs(bytes) => {
295 let bytes = (0..32)
296 .map(|idx| {
297 bytes.get(offset + idx).cloned().unwrap_or_else(|| SymExpr::zero(cx))
298 })
299 .collect::<Vec<_>>();
300 SymExpr::from_bytes(cx, bytes)
301 }
302 SymBytesKind::Word(word) if offset == 0 => word.clone(),
303 SymBytesKind::Word(_) if offset >= 32 => SymExpr::zero(cx),
304 SymBytesKind::Slice { bytes, offset: base_offset, len } => {
305 if offset.checked_add(32).is_some_and(|end| end <= *len)
306 && let Some(base_offset) = base_offset.eval()
307 && let Ok(base_offset) = usize::try_from(base_offset)
308 && let Some(base_offset) = base_offset.checked_add(offset)
309 {
310 return bytes.word_at(cx, base_offset);
311 }
312 let bytes = (0..32).map(|idx| self.byte(cx, offset + idx)).collect::<Vec<_>>();
313 SymExpr::from_bytes(cx, bytes)
314 }
315 _ => {
316 let bytes = (0..32).map(|idx| self.byte(cx, offset + idx)).collect::<Vec<_>>();
317 SymExpr::from_bytes(cx, bytes)
318 }
319 }
320 }
321
322 pub(crate) fn right_aligned_word(&self, cx: &mut SymCx, offset: usize, len: usize) -> SymExpr {
323 debug_assert!(len <= 32);
324 let len = len.min(32);
325 if let Some(word) = self.word_fragment_at(cx, offset, len, 32 - len) {
326 return word;
327 }
328
329 let mut bytes = Vec::with_capacity(32);
330 for _ in 0..32 - len {
331 bytes.push(SymExpr::zero(cx));
332 }
333 bytes.extend((0..len).map(|idx| self.byte(cx, offset + idx)));
334 SymExpr::from_bytes(cx, bytes)
335 }
336
337 fn word_fragment_at(
338 &self,
339 cx: &mut SymCx,
340 offset: usize,
341 len: usize,
342 out_offset: usize,
343 ) -> Option<SymExpr> {
344 debug_assert!(len <= 32);
345 debug_assert!(out_offset <= 32);
346 debug_assert!(out_offset + len <= 32);
347
348 if len == 0 {
349 return Some(SymExpr::zero(cx));
350 }
351
352 match self.kind() {
353 SymBytesKind::Concrete(bytes) => {
354 let mut word = [0u8; 32];
355 if offset < bytes.len() {
356 let take = (bytes.len() - offset).min(len);
357 word[out_offset..out_offset + take]
358 .copy_from_slice(&bytes[offset..offset + take]);
359 }
360 Some(SymExpr::constant(cx, U256::from_be_bytes(word)))
361 }
362 SymBytesKind::Word(word) => {
363 Self::word_expr_fragment(cx, word.clone(), offset, len, out_offset)
364 }
365 SymBytesKind::Slice { bytes, offset: base_offset, len: slice_len } => {
366 let available = slice_len.saturating_sub(offset).min(len);
367 if available == 0 {
368 return Some(SymExpr::zero(cx));
369 }
370 let base_offset =
371 base_offset.eval().and_then(|offset| usize::try_from(offset).ok())?;
372 bytes.word_fragment_at(cx, base_offset.checked_add(offset)?, available, out_offset)
373 }
374 SymBytesKind::Concat(values) => {
375 let mut offset = offset;
376 let mut out_offset = out_offset;
377 let mut remaining = len;
378 let mut out = SymExpr::zero(cx);
379
380 for bytes in values {
381 if remaining == 0 {
382 break;
383 }
384
385 let bytes_len = bytes.len();
386 if offset >= bytes_len {
387 offset -= bytes_len;
388 continue;
389 }
390
391 let take = (bytes_len - offset).min(remaining);
392 let fragment = bytes.word_fragment_at(cx, offset, take, out_offset)?;
393 out = SymExpr::binop(cx, SymBinOp::Or, out, fragment);
394 out_offset += take;
395 remaining -= take;
396 offset = 0;
397 }
398
399 Some(out)
400 }
401 SymBytesKind::Exprs(_) | SymBytesKind::Sized { .. } => None,
402 }
403 }
404
405 fn word_expr_fragment(
406 cx: &mut SymCx,
407 word: SymExpr,
408 offset: usize,
409 len: usize,
410 out_offset: usize,
411 ) -> Option<SymExpr> {
412 let len = 32usize.checked_sub(offset)?.min(len);
413 if len == 0 {
414 return Some(SymExpr::zero(cx));
415 }
416 if offset == 0 && len == 32 && out_offset == 0 {
417 return Some(word);
418 }
419
420 let src_trailing_bits = (32 - (offset + len)) * 8;
421 let dst_trailing_bits = (32 - (out_offset + len)) * 8;
422 let mask = mask_bits(U256::MAX, len * 8);
423
424 let src_trailing_bits = SymExpr::constant(cx, U256::from(src_trailing_bits));
425 let expr = SymExpr::binop(cx, SymBinOp::Shr, word, src_trailing_bits);
426 let mask = SymExpr::constant(cx, mask);
427 let expr = SymExpr::binop(cx, SymBinOp::And, expr, mask);
428 let dst_trailing_bits = SymExpr::constant(cx, U256::from(dst_trailing_bits));
429 Some(SymExpr::binop(cx, SymBinOp::Shl, expr, dst_trailing_bits))
430 }
431
432 pub(crate) fn materialize(&self, cx: &mut SymCx) -> Vec<SymExpr> {
433 (0..self.len()).map(|idx| self.byte(cx, idx)).collect()
434 }
435
436 pub(crate) fn same_bytes(&self, cx: &mut SymCx, other: &Self) -> bool {
437 self.len() == other.len()
438 && (0..self.len()).all(|idx| self.byte(cx, idx) == other.byte(cx, idx))
439 }
440
441 pub(crate) fn prefix_condition(&self, cx: &mut SymCx, prefix: &Self) -> Option<SymBoolExpr> {
442 if prefix.len() > self.len() {
443 return None;
444 }
445 let mut conditions = Vec::new();
446 for idx in 0..prefix.len() {
447 let actual = self.byte(cx, idx);
448 let expected = prefix.byte(cx, idx);
449 if actual == expected {
450 continue;
451 }
452 match (actual.as_const(), expected.as_const()) {
453 (Some(actual), Some(expected)) if actual.to::<u8>() == expected.to::<u8>() => {}
454 (Some(_), Some(_)) => return None,
455 _ => conditions.push(SymBoolExpr::eq(cx, actual, expected)),
456 }
457 }
458 Some(SymBoolExpr::and(cx, conditions))
459 }
460
461 pub(crate) fn eval_model<M: SymbolicModelLookup + ?Sized>(
462 &self,
463 cx: &mut SymCx,
464 model: &M,
465 ) -> Result<Vec<u8>, SymbolicError> {
466 match self.kind() {
467 SymBytesKind::Concrete(bytes) => Ok(bytes.clone()),
468 _ => (0..self.len())
469 .map(|idx| Ok(self.byte(cx, idx).eval_model(model)?.to::<u8>()))
470 .collect(),
471 }
472 }
473
474 pub(crate) fn concrete_bytes(
475 &self,
476 cx: &mut SymCx,
477 reason: &'static str,
478 ) -> Result<Vec<u8>, SymbolicError> {
479 let mut out = Vec::with_capacity(self.len());
480 self.append_concrete_range(cx, 0, self.len(), &mut out, reason)?;
481 Ok(out)
482 }
483
484 fn append_concrete_range(
485 &self,
486 cx: &mut SymCx,
487 mut offset: usize,
488 mut len: usize,
489 out: &mut Vec<u8>,
490 reason: &'static str,
491 ) -> Result<(), SymbolicError> {
492 if len == 0 {
493 return Ok(());
494 }
495
496 match self.kind() {
497 SymBytesKind::Concrete(bytes) => {
498 if offset >= bytes.len() {
499 out.resize(out.len() + len, 0);
500 return Ok(());
501 }
502
503 let take = (bytes.len() - offset).min(len);
504 out.extend_from_slice(&bytes[offset..offset + take]);
505 if len > take {
506 out.resize(out.len() + len - take, 0);
507 }
508 Ok(())
509 }
510 SymBytesKind::Exprs(bytes) => {
511 for idx in 0..len {
512 let Some(byte) = offset.checked_add(idx).and_then(|idx| bytes.get(idx)) else {
513 out.push(0);
514 continue;
515 };
516 let Some(byte) = byte.as_const() else {
517 return Err(SymbolicError::Unsupported(reason));
518 };
519 out.push(byte.to::<u8>());
520 }
521 Ok(())
522 }
523 SymBytesKind::Concat(values) => {
524 for bytes in values {
525 if len == 0 {
526 break;
527 }
528
529 let bytes_len = bytes.len();
530 if offset >= bytes_len {
531 offset -= bytes_len;
532 continue;
533 }
534
535 let take = (bytes_len - offset).min(len);
536 bytes.append_concrete_range(cx, offset, take, out, reason)?;
537 len -= take;
538 offset = 0;
539 }
540
541 if len != 0 {
542 out.resize(out.len() + len, 0);
543 }
544 Ok(())
545 }
546 SymBytesKind::Slice { bytes, offset: base_offset, len: slice_len } => {
547 if offset >= *slice_len {
548 out.resize(out.len() + len, 0);
549 return Ok(());
550 }
551
552 let take = (*slice_len - offset).min(len);
553 if let Some(base_offset) = base_offset.eval()
554 && let Ok(base_offset) = usize::try_from(base_offset)
555 && let Some(offset) = base_offset.checked_add(offset)
556 {
557 bytes.append_concrete_range(cx, offset, take, out, reason)?;
558 if len > take {
559 out.resize(out.len() + len - take, 0);
560 }
561 } else {
562 let bytes = self.slice_concrete(cx, offset, len).materialize(cx);
563 out.extend(concrete_expr_bytes(&bytes, reason)?);
564 }
565 Ok(())
566 }
567 _ => {
568 let bytes = self.slice_concrete(cx, offset, len).materialize(cx);
569 out.extend(concrete_expr_bytes(&bytes, reason)?);
570 Ok(())
571 }
572 }
573 }
574}