Implement opt-in verification (closes viperproject#1187)

Author: Pointerbender

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

@@ -46,6 +46,7 @@
 | [`MIN_PRUSTI_VERSION`](#min_prusti_version) | `Option<String>` | `None` | A |
 | [`NO_VERIFY`](#no_verify) | `bool` | `false` | A |
 | [`NO_VERIFY_DEPS`](#no_verify_deps) | `bool` | `false` | B |
+| [`OPT_IN_VERIFICATION`](#opt_in_verification) | `bool` | `false` | A |
 | [`OPTIMIZATIONS`](#optimizations) | `Vec<String>` | "all" | A |
 | [`PRESERVE_SMT_TRACE_FILES`](#preserve_smt_trace_files) | `bool` | `false` | A |
 | [`PRINT_COLLECTED_VERIFICATION_ITEMS`](#print_collected_verification_items) | `bool` | `false` | A |
@@ -293,6 +294,9 @@ When enabled, verification is skipped for dependencies. Equivalent to enabling `
 
 > **Note:** applied to all dependency crates when running with `cargo prusti`.
 
+## `OPT_IN_VERIFICATION`
+When enabled, Prusti will only try to verify the functions annotated with `#[verified]`. All other functions are assumed to be `#[trusted]`, by default. Functions annotated with both `#[trusted]` and `#[verified]` will not be verified.
+
 ## `ONLY_MEMORY_SAFETY`
 
 When enabled, only the core proof is verified.

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

@@ -46,6 +46,12 @@ pub fn trusted(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
     tokens
 }
 
+#[cfg(not(feature = "prusti"))]
+#[proc_macro_attribute]
+pub fn verified(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
+    tokens
+}
+
 #[cfg(not(feature = "prusti"))]
 #[proc_macro]
 pub fn body_invariant(_tokens: TokenStream) -> TokenStream {
@@ -165,6 +171,12 @@ pub fn trusted(attr: TokenStream, tokens: TokenStream) -> TokenStream {
     prusti_specs::trusted(attr.into(), tokens.into()).into()
 }
 
+#[cfg(feature = "prusti")]
+#[proc_macro_attribute]
+pub fn verified(attr: TokenStream, tokens: TokenStream) -> TokenStream {
+    rewrite_prusti_attributes(SpecAttributeKind::Verified, attr.into(), tokens.into()).into()
+}
+
 #[cfg(feature = "prusti")]
 #[proc_macro]
 pub fn body_invariant(tokens: TokenStream) -> TokenStream {

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

@@ -18,6 +18,9 @@ pub use prusti_contracts_proc_macros::pure;
 /// A macro for marking a function as trusted.
 pub use prusti_contracts_proc_macros::trusted;
 
+/// A macro for marking a function as opted into verification.
+pub use prusti_contracts_proc_macros::verified;
+
 /// A macro for type invariants.
 pub use prusti_contracts_proc_macros::invariant;
 

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

@@ -86,7 +86,8 @@ fn extract_prusti_attributes(
                     SpecAttributeKind::Pure
                     | SpecAttributeKind::Terminates
                     | SpecAttributeKind::Trusted
-                    | SpecAttributeKind::Predicate => {
+                    | SpecAttributeKind::Predicate
+                    | SpecAttributeKind::Verified => {
                         assert!(attr.tokens.is_empty(), "Unexpected shape of an attribute.");
                         attr.tokens
                     }
@@ -165,6 +166,7 @@ fn generate_spec_and_assertions(
             SpecAttributeKind::AfterExpiry => generate_for_after_expiry(attr_tokens, item),
             SpecAttributeKind::AssertOnExpiry => generate_for_assert_on_expiry(attr_tokens, item),
             SpecAttributeKind::Pure => generate_for_pure(attr_tokens, item),
+            SpecAttributeKind::Verified => generate_for_verified(attr_tokens, item),
             SpecAttributeKind::Terminates => generate_for_terminates(attr_tokens, item),
             SpecAttributeKind::Trusted => generate_for_trusted(attr_tokens, item),
             // Predicates are handled separately below; the entry in the SpecAttributeKind enum
@@ -295,6 +297,23 @@ fn generate_for_pure(attr: TokenStream, item: &untyped::AnyFnItem) -> GeneratedR
     ))
 }
 
+/// Generate spec items and attributes to typecheck and later retrieve "verified" annotations.
+fn generate_for_verified(attr: TokenStream, item: &untyped::AnyFnItem) -> GeneratedResult {
+    if !attr.is_empty() {
+        return Err(syn::Error::new(
+            attr.span(),
+            "the `#[verified]` attribute does not take parameters",
+        ));
+    }
+
+    Ok((
+        vec![],
+        vec![parse_quote_spanned! {item.span()=>
+            #[prusti::verified]
+        }],
+    ))
+}
+
 /// Generate spec items and attributes to typecheck and later retrieve "pure" annotations, but encoded as a referenced separate function that type-conditional spec refinements can apply trait bounds to.
 fn generate_for_pure_refinements(item: &untyped::AnyFnItem) -> GeneratedResult {
     let mut rewriter = rewriter::AstRewriter::new();
@@ -830,6 +849,7 @@ fn extract_prusti_attributes_for_types(
                     SpecAttributeKind::AssertOnExpiry => unreachable!("assert_on_expiry on type"),
                     SpecAttributeKind::RefineSpec => unreachable!("refine_spec on type"),
                     SpecAttributeKind::Pure => unreachable!("pure on type"),
+                    SpecAttributeKind::Verified => unreachable!("verified on type"),
                     SpecAttributeKind::Invariant => unreachable!("invariant on type"),
                     SpecAttributeKind::Predicate => unreachable!("predicate on type"),
                     SpecAttributeKind::Terminates => unreachable!("terminates on type"),
@@ -873,6 +893,7 @@ fn generate_spec_and_assertions_for_types(
             SpecAttributeKind::AfterExpiry => unreachable!(),
             SpecAttributeKind::AssertOnExpiry => unreachable!(),
             SpecAttributeKind::Pure => unreachable!(),
+            SpecAttributeKind::Verified => unreachable!(),
             SpecAttributeKind::Predicate => unreachable!(),
             SpecAttributeKind::Invariant => unreachable!(),
             SpecAttributeKind::RefineSpec => unreachable!(),

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

@@ -17,6 +17,7 @@ pub enum SpecAttributeKind {
     RefineSpec = 9,
     Terminates = 10,
     PrintCounterexample = 11,
+    Verified = 12,
 }
 
 impl TryFrom<String> for SpecAttributeKind {
@@ -35,6 +36,7 @@ impl TryFrom<String> for SpecAttributeKind {
             "refine_spec" => Ok(SpecAttributeKind::RefineSpec),
             "model" => Ok(SpecAttributeKind::Model),
             "print_counterexample" => Ok(SpecAttributeKind::PrintCounterexample),
+            "verified" => Ok(SpecAttributeKind::Verified),
             _ => Err(name),
         }
     }

prusti-interface/src/specs/mod.rs

@@ -7,6 +7,7 @@ use crate::{
     PrustiError,
 };
 use log::debug;
+use prusti_common::config;
 use prusti_rustc_interface::{
     ast::ast,
     errors::MultiSpan,
@@ -364,7 +365,8 @@ fn get_procedure_spec_ids(def_id: DefId, attrs: &[ast::Attribute]) -> Option<Pro
     );
 
     let pure = has_prusti_attr(attrs, "pure");
-    let trusted = has_prusti_attr(attrs, "trusted");
+    let trusted = has_prusti_attr(attrs, "trusted")
+        || (config::opt_in_verification() && !has_prusti_attr(attrs, "verified"));
     let abstract_predicate = has_abstract_predicate_attr(attrs);
 
     if abstract_predicate || pure || trusted || !spec_id_refs.is_empty() {

prusti-tests/tests/verify_overflow/fail/issues/issue-1187-2.rs

@@ -0,0 +1,19 @@
+// compile-flags: -Popt_in_verification=true
+use prusti_contracts::*;
+
+fn main() {}
+
+fn i_am_not_verified() {
+    unreachable!();
+}
+
+#[verified]
+fn i_am_verified() {
+    assert!(1 == 2); //~ ERROR
+}
+
+#[verified]
+#[trusted]
+fn i_am_trusted() {
+    unreachable!();
+}

prusti-tests/tests/verify_overflow/fail/issues/issue-1187-3.rs

@@ -0,0 +1,19 @@
+// compile-flags: -Popt_in_verification=false
+use prusti_contracts::*;
+
+fn main() {}
+
+fn i_am_not_verified() {
+    unreachable!(); //~ ERROR
+}
+
+#[verified]
+fn i_am_verified() {
+    assert!(1 == 2); //~ ERROR
+}
+
+#[verified]
+#[trusted]
+fn i_am_trusted() {
+    unreachable!();
+}

prusti-tests/tests/verify_overflow/pass/issues/issue-1187-1.rs

@@ -0,0 +1,25 @@
+// compile-flags: -Popt_in_verification=true
+use prusti_contracts::*;
+
+fn main() {}
+
+fn i_am_not_verified() {
+    unreachable!();
+}
+
+#[verified]
+fn i_am_verified() {
+    assert!(1 != 2);
+}
+
+#[verified]
+#[pure]
+fn i_am_pure() {
+    assert!(true);
+}
+
+#[verified]
+#[trusted]
+fn i_am_trusted() {
+    unreachable!();
+}

prusti-utils/src/config.rs

@@ -107,6 +107,7 @@ lazy_static::lazy_static! {
         settings.set_default("allow_unreachable_unsupported_code", false).unwrap();
         settings.set_default("no_verify", false).unwrap();
         settings.set_default("no_verify_deps", false).unwrap();
+        settings.set_default("opt_in_verification", false).unwrap();
         settings.set_default("full_compilation", false).unwrap();
         settings.set_default("json_communication", false).unwrap();
         settings.set_default("optimizations", "all").unwrap();
@@ -981,6 +982,12 @@ pub fn no_verify_deps() -> bool {
     read_setting("no_verify_deps")
 }
 
+/// When enabled, verification is skipped for functions
+/// that do not have the `#[verified]` attribute.
+pub fn opt_in_verification() -> bool {
+    read_setting("opt_in_verification")
+}
+
 /// When enabled, compilation will continue and a binary will be generated
 /// after Prusti terminates.
 pub fn full_compilation() -> bool {