crucible/
sym_bytes.rs

1use core::ops::{Deref, DerefMut};
2use crate::crucible_assume;
3use crate::array::Array;
4use crate::symbolic::Symbolic;
5
6/// An array of symbolic bytes, backed by an SMT array.  In some cases, `crux-mir` can analyze
7/// tests using `SymBytes` more efficiently than tests that use `Vec<u8>`.  Otherwise, `SymBytes`
8/// and `Vec<u8>` are mostly equivalent.
9pub struct SymBytes {
10    arr: Array<u8>,
11    len: usize,
12}
13
14impl SymBytes {
15    /// Create a new byte array, filling slots `0 .. len` with zeros.
16    pub fn zeroed(len: usize) -> SymBytes {
17        SymBytes {
18            arr: Array::zeroed(),
19            len,
20        }
21    }
22
23    /// Create a new byte array, filling slots `0 .. len` with symbolic values.
24    ///
25    /// This is like the trait method `Symbolic::symbolic`, but takes an additional `len` argument.
26    pub fn symbolic(desc: &str, len: usize) -> SymBytes {
27        SymBytes {
28            arr: Array::symbolic(desc),
29            len,
30        }
31    }
32
33    /// Create a new byte array, filling slots `0 .. len` with symbolic values, and constraining
34    /// the result with `f`.
35    ///
36    /// This is like the trait method `Symbolic::symbolic`, but takes an additional `len` argument.
37    pub fn symbolic_where<F>(desc: &str, len: usize, f: F) -> SymBytes
38    where F: FnOnce(&Self) -> bool {
39        let s = Self::symbolic(desc, len);
40        crucible_assume!(f(&s));
41        s
42    }
43
44    pub fn len(&self) -> usize {
45        self.len
46    }
47}
48
49impl Deref for SymBytes {
50    type Target = [u8];
51    fn deref(&self) -> &[u8] {
52        self.arr.as_slice(0, self.len)
53    }
54}
55
56impl DerefMut for SymBytes {
57    fn deref_mut(&mut self) -> &mut [u8] {
58        self.arr.as_mut_slice(0, self.len)
59    }
60}
crucible/sym_bytes.rs

crucible/
sym_bytes.rs
