crucible/method_spec/
raw.rs

1//! Bindings for low-level MethodSpec APIs.
2//!
3//! Like most functions in the `crucible` crate, these functions are left unimplemented in Rust
4//! and are replaced by a real implementation via the Crucible override mechanism.  However, unlike
5//! most other functions, the necessary overrides are not provided by `crux-mir`; instead, they are
6//! provided by the `crux-mir-comp` package in the `saw-script` repository, which extends ordinary
7//! `crux-mir` with additional overrides using `crux-mir`'s new `mainWithExtraOverrides` entry
8//! point.  Trying to use these APIs under ordinary `crux-mir` will produce an error.
9
10/// Crucible `MethodSpecType`, exposed to Rust.
11///
12/// As usual for Crucible types, this implements `Copy`, since it's backed by a boxed,
13/// garbage-collected Haskell value.  It contains a dummy field to ensure the Rust compiler sees it
14/// as having non-zero size.  The representation is overridden within `crux-mir`, so the field
15/// should not be accessed when running symbolically.
16#[derive(Clone, Copy)]
17pub struct MethodSpec(u8);
18
19// We only have `libcore` available, so we can't return `String` here.  Instead, the override for
20// this function within `crux-mir` will construct and leak a `str`.
21pub fn spec_pretty_print(ms: MethodSpec) -> &'static str {
22    "(unknown MethodSpec)"
23}
24
25/// Enable using `ms` in place of calls to the actual function.  The function to override is
26/// determined by the `F` type parameter of `builder_new` during the construction of the
27/// `MethodSpec`.
28pub fn spec_enable(ms: MethodSpec) {
29}
30
31
32/// Crucible `MethodSpecBuilderType`, exposed to Rust.
33#[derive(Clone, Copy)]
34pub struct MethodSpecBuilder(u8);
35
36pub fn builder_new<F>() -> MethodSpecBuilder {
37    // If the program is running under ordinary `crux-mir` instead of `crux-mir-comp`, then the
38    // override for this function will be missing.  We could provide a dummy implementation for
39    // that case, but it's better to fail early.  Otherwise users will get cryptic errors when
40    // invoking their spec functions, as `builder_finish` won't have its usual effect of discarding
41    // any new goals added by the spec function.
42    unimplemented!("MethodSpecBuilder is not supported on this version of crux-mir")
43}
44
45pub fn builder_add_arg<T>(msb: MethodSpecBuilder, x: &T) -> MethodSpecBuilder {
46    let _ = x;
47    msb
48}
49
50pub fn builder_gather_assumes(msb: MethodSpecBuilder) -> MethodSpecBuilder {
51    msb
52}
53
54pub fn builder_set_return<T>(msb: MethodSpecBuilder, x: &T) -> MethodSpecBuilder {
55    let _ = x;
56    msb
57}
58
59pub fn builder_gather_asserts(msb: MethodSpecBuilder) -> MethodSpecBuilder {
60    msb
61}
62
63pub fn builder_finish(msb: MethodSpecBuilder) -> MethodSpec {
64    let _ = msb;
65    MethodSpec(0)
66}
67
68
69/// Replace all mutable global data with arbitrary values.  This is used at the start of tests to
70/// ensure that the property holds in any context.
71pub fn clobber_globals() {
72    unimplemented!("MethodSpecBuilder is not supported on this version of crux-mir")
73}
crucible/method_spec/raw.rs

crucible/method_spec/
raw.rs
