Runtime checks

docs/dev-guide/src/config/flags.md

@@ -14,6 +14,7 @@
 | [`CHECK_PANICS`](#check_panics) | `bool` | `true` | A |
 | [`CHECK_TIMEOUT`](#check_timeout) | `Option<u32>` | `None` | A |
 | [`COUNTEREXAMPLE`](#counterexample) | `bool` | `false` | A |
+| [`DEBUG_RUNTIME_CHECKS`](#debug_runtime_checks) | `bool` | `false` | A |
 | [`DELETE_BASIC_BLOCKS`](#delete_basic_blocks) | `Vec<String>` | `vec![]` | A |
 | [`DISABLE_NAME_MANGLING`](#disable_name_mangling) | `bool` | `false` | A |
 | [`DUMP_BORROWCK_INFO`](#dump_borrowck_info) | `bool` | `false` | A |
@@ -34,6 +35,7 @@
 | [`FULL_COMPILATION`](#full_compilation) | `bool` | `false` | A* |
 | [`HIDE_UUIDS`](#hide_uuids) | `bool` | `false` | A |
 | [`IGNORE_REGIONS`](#ignore_regions) | `bool` | `false` | A |
+| [`INSERT_RUNTIME_CHECKS`](#insert_runtime_checks) | `string` | `"none"` | A |
 | [`INTERNAL_ERRORS_AS_WARNINGS`](#internal_errors_as_warnings) | `bool` | `false` | A |
 | [`INTERN_NAMES`](#intern_names) | `bool` | `true` | A |
 | [`JAVA_HOME`](#java_home) | `Option<String>` | `None` | A |
@@ -56,6 +58,7 @@
 | [`PRINT_HASH`](#print_hash) | `bool` | `false` | A |
 | [`PRINT_TYPECKD_SPECS`](#print_typeckd_specs) | `bool` | `false` | A |
 | [`QUIET`](#quiet) | `bool` | `false` | A* |
+| [`REMOVE_DEAD_CODE`](#remove_dead_code) | `bool` | `false` | A |
 | [`SERVER_ADDRESS`](#server_address) | `Option<String>` | `None` | A |
 | [`SERVER_MAX_CONCURRENCY`](#server_max_concurrency) | `Option<usize>` | `None` | A |
 | [`SERVER_MAX_STORED_VERIFIERS`](#server_max_stored_verifiers) | `Option<usize>` | `None` | A |
@@ -81,6 +84,7 @@
 | [`VIPER_HOME`](#viper_home) | `Option<String>` | `None` | A |
 | [`WRITE_SMT_STATISTICS`](#write_smt_statistics) | `bool` | `false` | A |
 
+
 ## `ALLOW_UNREACHABLE_UNSUPPORTED_CODE`
 
 When enabled, unsupported code is encoded as `assert false`. This way error messages are reported only for unsupported code that is actually reachable.
@@ -142,6 +146,10 @@ For more information see [here]( https://github.com/viperproject/silicon/blob/4c
 
 When enabled, Prusti will try to find and print a counterexample for any failed assertion or specification.
 
+## `DEBUG_RUNTIME_CHECKS`
+
+When enabled, functions generated for runtime checking will emit a message when they are executed.
+
 ## `DELETE_BASIC_BLOCKS`
 
 The given basic blocks will be replaced with `assume false`.
@@ -233,6 +241,15 @@ When enabled, UUIDs of expressions and specifications printed with [`PRINT_TYPEC
 
 When enabled, debug files dumped by `rustc` will not contain lifetime regions.
 
+## `INSERT_RUNTIME_CHECKS`
+
+Whether or not to enable runtime checks. Accepts one of the following values:
+
+- `"none"`: default option, no runtime checks will be inserted.
+- `"selective"`: only contracts marked with `#[insert_runtime_check]` will be checked.
+- `"all"`: all supported contracts will be runtime checked.
+
+
 ## `INTERNAL_ERRORS_AS_WARNINGS`
 
 When enabled, internal errors are presented as warnings.
@@ -358,6 +375,10 @@ When enabled, user messages are not printed. Otherwise, messages output into `st
 
 > **Note:** `cargo prusti` sets this flag with `DEFAULT_PRUSTI_QUIET=true`.
 
+## `REMOVE_DEAD_CODE`
+
+When enabled, Prusti will perform some optimizations on the generated executable by removing unreachable code and unneeded assertions and their corresponding checked operations.
+
 ## `SERVER_ADDRESS`
 
 When set to an address and port (e.g. `"127.0.0.1:2468"`), Prusti will connect to the given server and use it for its verification backend.

prusti-contracts/prusti-contracts-proc-macros/Cargo.toml

@@ -22,3 +22,6 @@ proc-macro2 = { version = "1.0", optional = true }
 # Are we being compiled by Prusti and should include dependency on
 # prusti-specs and proc-macro2?
 prusti = ["dep:prusti-specs", "dep:proc-macro2"]
+# If std is active, and prusti-specs is imported, forward the std flag
+# to prusti-specs.
+std = ["prusti-specs?/std"]

prusti-contracts/prusti-contracts-proc-macros/src/lib.rs

@@ -130,6 +130,18 @@ pub fn body_variant(_tokens: TokenStream) -> TokenStream {
     TokenStream::new()
 }
 
+#[cfg(not(feature = "prusti"))]
+#[proc_macro_attribute]
+pub fn quantifier_runtime_bounds(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
+    tokens
+}
+
+#[cfg(not(feature = "prusti"))]
+#[proc_macro_attribute]
+pub fn insert_runtime_check(_attr: TokenStream, _tokens: TokenStream) -> TokenStream {
+    TokenStream::new()
+}
+
 // ----------------------
 // --- PRUSTI ENABLED ---
 
@@ -273,5 +285,21 @@ pub fn body_variant(tokens: TokenStream) -> TokenStream {
     prusti_specs::body_variant(tokens.into()).into()
 }
 
+#[cfg(feature = "prusti")]
+#[proc_macro_attribute]
+pub fn quantifier_runtime_bounds(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
+    tokens
+}
+
+#[cfg(feature = "prusti")]
+#[proc_macro_attribute]
+pub fn insert_runtime_check(attr: TokenStream, tokens: TokenStream) -> TokenStream {
+    rewrite_prusti_attributes(
+        SpecAttributeKind::InsertRuntimeCheck,
+        attr.into(),
+        tokens.into(),
+    )
+    .into()
+}
 // Ensure that you've also crated a transparent `#[cfg(not(feature = "prusti"))]`
 // version of your new macro above!

prusti-contracts/prusti-contracts/Cargo.toml

@@ -19,4 +19,6 @@ trybuild = "1.0"
 
 # Forward "prusti" flag
 [features]
+default = ["std"]
 prusti = ["prusti-contracts-proc-macros/prusti"]
+std = ["prusti-contracts-proc-macros/std"]

prusti-contracts/prusti-contracts/src/lib.rs

@@ -1,4 +1,5 @@
-#![no_std]
+#![cfg_attr(not(feature = "std"), no_std)]
+// #![no_std]
 
 /// A macro for writing a precondition on a function.
 pub use prusti_contracts_proc_macros::requires;
@@ -66,6 +67,14 @@ pub use prusti_contracts_proc_macros::terminates;
 /// A macro to annotate body variant of a loop to prove termination
 pub use prusti_contracts_proc_macros::body_variant;
 
+/// A macro to explicitly annotate a quantifier with ranges for their
+/// runtime checks
+pub use prusti_contracts_proc_macros::quantifier_runtime_bounds;
+
+/// A macro to annotate contracts that should be checked
+/// at runtime
+pub use prusti_contracts_proc_macros::insert_runtime_check;
+
 #[cfg(not(feature = "prusti"))]
 mod private {
     use core::marker::PhantomData;
@@ -124,6 +133,9 @@ mod private {
 #[cfg(feature = "prusti")]
 pub mod core_spec;
 
+#[cfg(feature = "prusti")]
+pub mod runtime_check_internals;
+
 #[cfg(feature = "prusti")]
 mod private {
     use core::{marker::PhantomData, ops::*};

prusti-contracts/prusti-contracts/src/runtime_check_internals.rs

@@ -0,0 +1,59 @@
+#[cfg(not(feature = "std"))]
+use core::fmt::Write;
+
+#[cfg(not(feature = "std"))]
+struct SimpleFormatter<'a>(&'a mut [u8], usize);
+
+#[cfg(not(feature = "std"))]
+impl<'a> core::fmt::Write for SimpleFormatter<'a> {
+    fn write_str(&mut self, s: &str) -> core::fmt::Result {
+        let dest_len = self.0.len();
+        let copy_len = core::cmp::min(s.len(), dest_len);
+
+        self.0[..copy_len].copy_from_slice(&s.as_bytes()[..copy_len]);
+        self.1 = copy_len;
+
+        if s.len() > dest_len {
+            Err(core::fmt::Error)
+        } else {
+            Ok(())
+        }
+    }
+}
+
+#[cfg(not(feature = "std"))]
+pub fn num_to_str<T: core::fmt::Display>(n: T, buffer: &mut [u8]) -> &str {
+    let mut formatter = SimpleFormatter(buffer, 0);
+    write!(&mut formatter, "{}", n).expect("Failed to write number to buffer");
+    let bytes_written = formatter.1;
+    core::str::from_utf8(&buffer[..bytes_written]).unwrap()
+}
+
+// An internal function used for getting more precise error messages for runtime
+// checks.
+// Buffer manipulations because we cannot use std and need to operate on a buffer
+// that is allocated before this function is called.
+#[cfg(not(feature = "std"))]
+pub fn check_expr(expr: bool, added_info: &str, buffer: &mut [u8], buffer_len: &mut usize) -> bool {
+    if !expr {
+        // buffer already has contents up until buffer_len
+        let after_len = *buffer_len + added_info.len();
+        buffer[*buffer_len..after_len].copy_from_slice(added_info.as_bytes());
+        *buffer_len = after_len;
+        false
+    } else {
+        true
+    }
+}
+
+// If ctd is available, the check function can be a lot simpler, and doesn't
+// need to operate on a passed buffer.
+#[cfg(feature = "std")]
+pub fn check_expr(expr: bool, added_info: &str, message: &mut std::string::String) -> bool {
+    if !expr {
+        message.push_str(added_info);
+        false
+    } else {
+        true
+    }
+}

prusti-contracts/prusti-specs/Cargo.toml

@@ -21,3 +21,6 @@ proc-macro2 = "1.0"
 uuid = { version = "1.0", features = ["v4"] }
 itertools = "0.11"
 rustc-hash = "1.1.0"
+
+[features]
+std = []

prusti-contracts/prusti-specs/src/attribute_consumer.rs

@@ -0,0 +1,60 @@
+use proc_macro2::TokenStream;
+use quote::quote;
+use syn::parse::{Parse, ParseStream};
+
+// By default, attributes can only be attached to items like functions or closures.
+// The point of this is to allow attaching attributes to the contents of a
+// prusti_assert!() or similar (predicate).
+// Note: this kind of consuming is only necessary when we want to consume an
+// attribute at the beginning of a TokenStream without fully parsing it (mainly
+// because the rest still has to be parsed by prusti_parse)
+pub(crate) struct AttributeConsumer {
+    pub attributes: Vec<syn::Attribute>,
+    pub rest: TokenStream,
+}
+
+impl Parse for AttributeConsumer {
+    fn parse(input: ParseStream) -> syn::Result<Self> {
+        let attributes = input.call(syn::Attribute::parse_outer)?;
+        let rest: TokenStream = input.parse().unwrap();
+        Ok(Self { attributes, rest })
+    }
+}
+
+// maybe we can make this more generic so it can be used in other places..
+impl AttributeConsumer {
+    pub fn get_attribute(&mut self, name: &str) -> Option<syn::Attribute> {
+        if let Some(pos) = self.attributes.iter().position(|attr| {
+            if let Some(ident) = attr.path.get_ident() {
+                if *ident == name {
+                    return true;
+                }
+            }
+            false
+        }) {
+            Some(self.attributes.remove(pos))
+        } else {
+            None
+        }
+    }
+
+    // /// A function that can be used to check that all attributes have been
+    // /// consumed. Returns an error with the span of the first remaining attribute
+    // pub fn check_no_remaining_attrs(&self) -> syn::Result<()> {
+    //     if let Some(attr) = self.attributes.first() {
+    //         Err(syn::Error::new(
+    //             attr.span(),
+    //             "This attribute could not be processed and probably doesn't belong here",
+    //         ))
+    //     } else {
+    //         Ok(())
+    //     }
+    // }
+
+    pub fn tokens(self) -> TokenStream {
+        let Self { attributes, rest } = self;
+        let mut attrs: TokenStream = attributes.into_iter().map(|attr| quote!(#attr)).collect();
+        attrs.extend(quote!(#rest));
+        attrs
+    }
+}

prusti-contracts/prusti-specs/src/common.rs

@@ -709,3 +709,33 @@ mod tests {
         }
     }
 }
+
+pub enum RuntimeCheckMode {
+    All,
+    Selective,
+    Never,
+}
+
+impl RuntimeCheckMode {
+    pub fn determine() -> Self {
+        match std::env::var("PRUSTI_INSERT_RUNTIME_CHECKS")
+            .unwrap_or("never".to_string())
+            .as_str()
+        {
+            "all" => Self::All,
+            "selective" => Self::Selective,
+            "never" => Self::Never,
+            _ => Self::Never,
+        }
+    }
+
+    /// Depending on whether a contract has a #[insert_runtime_check] attribute
+    /// decide whether a check should actually be inserted
+    pub fn decide_insertion(&self, has_attr: bool) -> bool {
+        match (self, has_attr) {
+            (Self::All, _) => true,
+            (Self::Selective, b) => b,
+            (Self::Never, _) => false,
+        }
+    }
+}