crucible/method_spec/
mod.rs

1//! Provides the `MethodSpec` type, used for compositional reasoning.  Also provides
2//! `MethodSpecBuilder`, which is used internally by the compositional reasoning macros to
3//! construct a `MethodSpec` from a symbolic test.
4//!
5//! Note that these types work only when running under `crux-mir-comp`.  Trying to use them under
6//! ordinary `crux-mir` will produce an error.
7use core::fmt;
8
9mod raw;
10
11pub use self::raw::clobber_globals;
12
13
14/// The specification of a function.  This can be used when verifying callers of the function to
15/// avoid simulating the entire function itself.
16#[derive(Clone, Copy)]
17pub struct MethodSpec {
18    raw: raw::MethodSpec,
19}
20
21impl MethodSpec {
22    /// Enable this `MethodSpec` to be used as an override for its subject function.
23    pub fn enable(&self) {
24        raw::spec_enable(self.raw);
25    }
26
27    pub fn pretty_print(&self) -> &'static str {
28        raw::spec_pretty_print(self.raw)
29    }
30}
31
32impl fmt::Debug for MethodSpec {
33    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
34        let s = raw::spec_pretty_print(self.raw);
35        fmt.write_str("MethodSpec {")?;
36        for (i, chunk) in s.split("\n").enumerate() {
37            if i > 0 {
38                fmt.write_str(", ")?;
39            }
40            fmt.write_str(chunk);
41        }
42        fmt.write_str("}")?;
43        Ok(())
44    }
45}
46
47
48/// Helper type used to incrementally construct a `MethodSpec` for a function.
49pub struct MethodSpecBuilder {
50    raw: raw::MethodSpecBuilder,
51}
52
53impl fmt::Debug for MethodSpecBuilder {
54    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
55        write!(fmt, "MethodSpecBuilder {{ .. }}")
56    }
57}
58
59impl MethodSpecBuilder {
60    pub fn new<Args: core::marker::Tuple, F: Fn<Args>>(f: F) -> MethodSpecBuilder {
61        MethodSpecBuilder {
62            raw: raw::builder_new::<F>(),
63        }
64    }
65
66    pub fn add_arg<T>(&mut self, x: &T) {
67        self.raw = raw::builder_add_arg(self.raw, x);
68    }
69
70    pub fn gather_assumes(&mut self) {
71        self.raw = raw::builder_gather_assumes(self.raw);
72    }
73
74    pub fn set_return<T>(&mut self, x: &T) {
75        self.raw = raw::builder_set_return(self.raw, x);
76    }
77
78    pub fn gather_asserts(&mut self) {
79        self.raw = raw::builder_gather_asserts(self.raw);
80    }
81
82    pub fn finish(self) -> MethodSpec {
83        MethodSpec {
84            raw: raw::builder_finish(self.raw),
85        }
86    }
87}
crucible/method_spec/mod.rs

crucible/method_spec/
mod.rs
