crucible/
symbolic.rs

1use core::array;
2use core::num::{NonZero, Saturating, Wrapping, ZeroablePrimitive};
3use crate::crucible_assume_unreachable;
4
5
6pub trait Symbolic: Sized {
7    /// Create a new symbolic value of this type.  `desc` is used to refer to this symbolic value
8    /// when printing counterexamples.
9    fn symbolic(desc: &str) -> Self;
10
11    /// Create a new symbolic value, subject to constraints.  The result is a symbolic value of
12    /// this type on which `f` returns `true`.
13    fn symbolic_where<F: FnOnce(&Self) -> bool>(desc: &str, f: F) -> Self {
14        let x = Self::symbolic(desc);
15        super::crucible_assume!(f(&x));
16        x
17    }
18}
19
20
21macro_rules! core_impls {
22    ($($ty:ty, $func:ident;)*) => {
23        $(
24            /// Hook for a crucible override that creates a symbolic instance of $ty.
25            #[allow(unused)]
26            fn $func(desc: &str) -> $ty { unimplemented!(stringify!($func)); }
27
28            impl Symbolic for $ty {
29                fn symbolic(desc: &str) -> $ty { $func(desc) }
30            }
31        )*
32    };
33}
34
35core_impls! {
36    bool, symbolic_bool;
37    u8, symbolic_u8;
38    u16, symbolic_u16;
39    u32, symbolic_u32;
40    u64, symbolic_u64;
41    u128, symbolic_u128;
42}
43
44
45macro_rules! usize_impls {
46    ($($ty:ty, $width:expr;)*) => {
47        $(
48            #[cfg(target_pointer_width = $width)]
49            impl Symbolic for usize {
50                fn symbolic(desc: &str) -> usize { <$ty>::symbolic(desc) as usize }
51            }
52        )*
53    };
54}
55
56usize_impls! {
57    u8, "8";
58    u16, "16";
59    u32, "32";
60    u64, "64";
61    u128, "128";
62}
63
64
65macro_rules! int_impls {
66    ($($ty:ty, $uty:ty;)*) => {
67        $(
68            impl Symbolic for $ty {
69                fn symbolic(desc: &str) -> $ty { <$uty>::symbolic(desc) as $ty }
70            }
71        )*
72    };
73}
74
75int_impls! {
76    i8, u8;
77    i16, u16;
78    i32, u32;
79    i64, u64;
80    i128, u128;
81    isize, usize;
82}
83
84
85impl<T: Symbolic, const N: usize> Symbolic for [T; N] {
86    fn symbolic(desc: &str) -> [T; N] {
87        array::from_fn(|_i| T::symbolic(desc))
88    }
89}
90
91
92macro_rules! tuple_impls {
93    ($($($name:ident)*;)*) => {
94        $(
95            #[allow(unused)] #[allow(bad_style)]
96            impl<$($name: Symbolic,)*> Symbolic for ($($name,)*) {
97                fn symbolic(desc: &str) -> ($($name,)*) {
98                    (
99                        $($name::symbolic(desc),)*
100                    )
101                }
102            }
103        )*
104    };
105}
106
107tuple_impls! {
108    ;
109    A;
110    A B;
111    A B C;
112    A B C D;
113    A B C D E;
114    A B C D E F;
115    A B C D E F G;
116    A B C D E F G H;
117    A B C D E F G H I;
118    A B C D E F G H I J;
119    A B C D E F G H I J K;
120    A B C D E F G H I J K L;
121}
122
123impl<T: Symbolic> Symbolic for Saturating<T> {
124    fn symbolic(desc: &str) -> Saturating<T> {
125        Saturating(T::symbolic(desc))
126    }
127}
128
129impl<T: Symbolic> Symbolic for Wrapping<T> {
130    fn symbolic(desc: &str) -> Wrapping<T> {
131        Wrapping(T::symbolic(desc))
132    }
133}
134
135impl<T: Symbolic + ZeroablePrimitive> Symbolic for NonZero<T> {
136    fn symbolic(desc: &str) -> NonZero<T> {
137        match NonZero::new(T::symbolic(desc)) {
138            Some(x) => x,
139            None => crucible_assume_unreachable!(),
140        }
141    }
142}
143
144/// Take a symbolic-length prefix of `xs`.  The length of the returned slice can be anywhere in the
145/// range `0 ..= xs.len()`.
146pub fn prefix<'a, T>(xs: &'a [T]) -> &'a [T] {
147    let len = usize::symbolic_where("prefix_len", |&n| n < xs.len());
148    &xs[..len]
149}
crucible/symbolic.rs

crucible/
symbolic.rs
