Add prusti_refute! macro (#1365)

* Add prusti_refute! macro

* Add macro to generate getters/setters for fields via JNI

* Resolve fmt-check and clippy errors, simplify naming, small refactoring

* Add test for field! macro

* Update field! macro to not ask for signature (WIP)

* Update field! macro to search all the class hierarchy for the field to determine its signature

* Rename variables, add comments, delete leftover commented code

* Follow update in master branch

* current code, just a snapshot of my working dir

* fix bug with env/ast_utils with_local_frame - calling wrong function

* add

* Remove unecessary changes

* additional temporary code removal

* Add "refute.failed:refutation.true" into error_manager

* Remove unnecessary code, fmt-all

* cargo lock update

* add frotend support also for carbon

* add assert.failed:assertion.false-PanicCause::Refute entry to the error manager

* Add field access via Scala methods, use SilFrontend wrapper and remove unecessary dispatch

* Remove empty line - fmt-all error

* add tests for prusti_refute!

* update docs (user guide) - add mention to refute

* Add disclaimer about soundness, formatting

* remove unecessary case in the error manager

* typo - remove blank line

---------

Co-authored-by: Simon Hrabec <[email protected]>
Co-authored-by: Jonáš Fiala <[email protected]>

docs/user-guide/src/SUMMARY.md

@@ -19,7 +19,7 @@
   - [Absence of panics](verify/panic.md)
   - [Overflow checks](verify/overflow.md)
   - [Pre- and postconditions](verify/prepost.md)
-  - [Assertions and assumptions](verify/assert_assume.md)
+  - [Assertions, refutations and assumptions](verify/assert_refute_assume.md)
   - [Trusted functions](verify/trusted.md)
   - [Pure functions](verify/pure.md)
   - [Predicates](verify/predicate.md)

docs/user-guide/src/verify/assert_assume.md → docs/user-guide/src/verify/assert_refute_assume.md

@@ -1,4 +1,4 @@
-# Assertions and Assumptions 
+# Assertions, Refutations and Assumptions 
 
 You can use Prusti to verify that a certain property holds at a certain point
 within the body of a function (via an assertion). It is also possible to
@@ -35,6 +35,41 @@ prusti_assert!(map.insert(5)); // error
 `assert_eq!` and `assert_ne!`, but the check is made for
 [snapshot equality](../syntax.md#snapshot-equality), resp. snapshot inequality.
 
+## Refutations
+
+> Refutation **should not be relied upon for soundness** as it may succeed even when it should fail; Prusti may not be able to prove the property being refuted and thus won't complain even though the property actually holds (e.g. if the property is difficult to prove).
+
+The `prusti_refute!` macro is similar to `prusti_assert!` in its format, conditions of use and what expressions it accepts. It instructs Prusti to verify that a certain property at a specific point within the body of a function might hold in some, but not all cases. For example the following code will verify:
+
+```rust,noplaypen
+#[ensures(val < 0 ==> result == -1)]
+#[ensures(val == 0 ==> result == 0)]
+#[ensures(val > 0 ==> result == 1)]
+fn sign(val: i32) -> i32 {
+  prusti_refute!(val <= 0);
+  prusti_refute!(val >= 0);
+  if val < 0 {
+    -1
+  } else if val > 0 {
+    1
+  } else {
+    prusti_refute!(false);
+    0
+  }
+}
+```
+
+But the following function would not:
+
+```rust,noplaypen
+#[requires(val < 0 && val > 0)]
+#[ensures(result == val/2)]
+fn half(val: i32) -> i32 {
+  prusti_refute!(false);
+  val/2
+}
+```
+
 ## Assumptions
 
 The `prusti_assume!` macro instructs Prusti to assume that a certain property

docs/user-guide/src/verify/summary.md

@@ -10,7 +10,7 @@ More intricate properties require users to write suitable [specifications](../sy
 The following features are either currently supported or planned to be supported in Prusti:
 
 - [Pre- and postconditions](prepost.md)
-- [Assertions and assumptions](assert_assume.md)
+- [Assertions, refutations and assumptions](assert_refute_assume.md)
 - [Trusted functions](trusted.md)
 - [Pure functions](pure.md)
 - [Predicates](predicate.md)

prusti-common/src/vir/to_viper.rs

@@ -178,6 +178,9 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for Stmt {
             Stmt::Assert(ref expr, ref pos) => {
                 ast.assert(expr.to_viper(context, ast), pos.to_viper(context, ast))
             }
+            Stmt::Refute(ref expr, ref pos) => {
+                ast.refute(expr.to_viper(context, ast), pos.to_viper(context, ast))
+            }
             Stmt::MethodCall(ref method_name, ref args, ref targets) => {
                 let fake_position = Position::default();
                 ast.method_call(

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

@@ -70,6 +70,12 @@ pub fn prusti_assume(_tokens: TokenStream) -> TokenStream {
     TokenStream::new()
 }
 
+#[cfg(not(feature = "prusti"))]
+#[proc_macro]
+pub fn prusti_refute(_tokens: TokenStream) -> TokenStream {
+    TokenStream::new()
+}
+
 #[cfg(not(feature = "prusti"))]
 #[proc_macro_attribute]
 pub fn refine_trait_spec(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
@@ -195,6 +201,12 @@ pub fn prusti_assume(tokens: TokenStream) -> TokenStream {
     prusti_specs::prusti_assume(tokens.into()).into()
 }
 
+#[cfg(feature = "prusti")]
+#[proc_macro]
+pub fn prusti_refute(tokens: TokenStream) -> TokenStream {
+    prusti_specs::prusti_refutation(tokens.into()).into()
+}
+
 #[cfg(feature = "prusti")]
 #[proc_macro]
 pub fn closure(tokens: TokenStream) -> TokenStream {

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

@@ -33,6 +33,9 @@ pub use prusti_contracts_proc_macros::prusti_assert;
 /// A macro for writing assumptions using prusti syntax
 pub use prusti_contracts_proc_macros::prusti_assume;
 
+/// A macro for writing refutations using prusti syntax
+pub use prusti_contracts_proc_macros::prusti_refute;
+
 /// A macro for impl blocks that refine trait specifications.
 pub use prusti_contracts_proc_macros::refine_trait_spec;
 

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

@@ -431,6 +431,10 @@ pub fn prusti_assume(tokens: TokenStream) -> TokenStream {
     generate_expression_closure(&AstRewriter::process_prusti_assumption, tokens)
 }
 
+pub fn prusti_refutation(tokens: TokenStream) -> TokenStream {
+    generate_expression_closure(&AstRewriter::process_prusti_refutation, tokens)
+}
+
 /// Generates the TokenStream encoding an expression using prusti syntax
 /// Used for body invariants, assertions, and assumptions
 fn generate_expression_closure(

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

@@ -255,6 +255,15 @@ impl AstRewriter {
         self.process_prusti_expression(quote! {prusti_assumption}, spec_id, tokens)
     }
 
+    /// Parse a prusti refute into a Rust expression
+    pub fn process_prusti_refutation(
+        &mut self,
+        spec_id: SpecificationId,
+        tokens: TokenStream,
+    ) -> syn::Result<TokenStream> {
+        self.process_prusti_expression(quote! {prusti_refutation}, spec_id, tokens)
+    }
+
     fn process_prusti_expression(
         &mut self,
         kind: TokenStream,

prusti-interface/src/specs/mod.rs

@@ -83,6 +83,7 @@ pub struct SpecCollector<'a, 'tcx> {
     type_specs: FxHashMap<LocalDefId, TypeSpecRefs>,
     prusti_assertions: Vec<LocalDefId>,
     prusti_assumptions: Vec<LocalDefId>,
+    prusti_refutations: Vec<LocalDefId>,
     ghost_begin: Vec<LocalDefId>,
     ghost_end: Vec<LocalDefId>,
 }
@@ -99,6 +100,7 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
             type_specs: FxHashMap::default(),
             prusti_assertions: vec![],
             prusti_assumptions: vec![],
+            prusti_refutations: vec![],
             ghost_begin: vec![],
             ghost_end: vec![],
         }
@@ -119,6 +121,7 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
         self.determine_type_specs(&mut def_spec);
         self.determine_prusti_assertions(&mut def_spec);
         self.determine_prusti_assumptions(&mut def_spec);
+        self.determine_prusti_refutations(&mut def_spec);
         self.determine_ghost_begin_ends(&mut def_spec);
         // TODO: remove spec functions (make sure none are duplicated or left over)
         // Load all local spec MIR bodies, for export and later use
@@ -275,6 +278,16 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
             );
         }
     }
+    fn determine_prusti_refutations(&self, def_spec: &mut typed::DefSpecificationMap) {
+        for local_id in self.prusti_refutations.iter() {
+            def_spec.prusti_refutations.insert(
+                local_id.to_def_id(),
+                typed::PrustiRefutation {
+                    refutation: *local_id,
+                },
+            );
+        }
+    }
     fn determine_ghost_begin_ends(&self, def_spec: &mut typed::DefSpecificationMap) {
         for local_id in self.ghost_begin.iter() {
             def_spec.ghost_begin.insert(
@@ -526,6 +539,10 @@ impl<'a, 'tcx> intravisit::Visitor<'tcx> for SpecCollector<'a, 'tcx> {
                 self.prusti_assumptions.push(local_id);
             }
 
+            if has_prusti_attr(attrs, "prusti_refutation") {
+                self.prusti_refutations.push(local_id);
+            }
+
             if has_prusti_attr(attrs, "ghost_begin") {
                 self.ghost_begin.push(local_id);
             }

prusti-interface/src/specs/typed.rs

@@ -17,6 +17,7 @@ pub struct DefSpecificationMap {
     pub type_specs: FxHashMap<DefId, TypeSpecification>,
     pub prusti_assertions: FxHashMap<DefId, PrustiAssertion>,
     pub prusti_assumptions: FxHashMap<DefId, PrustiAssumption>,
+    pub prusti_refutations: FxHashMap<DefId, PrustiRefutation>,
     pub ghost_begin: FxHashMap<DefId, GhostBegin>,
     pub ghost_end: FxHashMap<DefId, GhostEnd>,
 }
@@ -46,6 +47,10 @@ impl DefSpecificationMap {
         self.prusti_assumptions.get(def_id)
     }
 
+    pub fn get_refutation(&self, def_id: &DefId) -> Option<&PrustiRefutation> {
+        self.prusti_refutations.get(def_id)
+    }
+
     pub fn get_ghost_begin(&self, def_id: &DefId) -> Option<&GhostBegin> {
         self.ghost_begin.get(def_id)
     }
@@ -166,12 +171,18 @@ impl DefSpecificationMap {
             .values()
             .map(|spec| format!("{spec:?}"))
             .collect();
+        let refutations: Vec<_> = self
+            .prusti_refutations
+            .values()
+            .map(|spec| format!("{spec:?}"))
+            .collect();
         let mut values = Vec::new();
         values.extend(loop_specs);
         values.extend(proc_specs);
         values.extend(type_specs);
         values.extend(asserts);
         values.extend(assumptions);
+        values.extend(refutations);
         if hide_uuids {
             let uuid =
                 Regex::new("[a-z0-9]{8}-[a-z0-9]{4}-[a-z0-9]{4}-[a-z0-9]{4}-[a-z0-9]{12}").unwrap();
@@ -292,6 +303,11 @@ pub struct PrustiAssumption {
     pub assumption: LocalDefId,
 }
 
+#[derive(Debug, Clone)]
+pub struct PrustiRefutation {
+    pub refutation: LocalDefId,
+}
+
 #[derive(Debug, Clone)]
 pub struct GhostBegin {
     pub marker: LocalDefId,

prusti-tests/tests/verify_overflow/fail/assert_assume_refute/prusti_refute.rs

@@ -0,0 +1,30 @@
+#![allow(unused)]
+
+use prusti_contracts::*;
+
+fn refute1() {
+    prusti_refute!(false);
+}
+
+fn failing_refute() {
+    prusti_refute!(true); //~ ERROR
+}
+
+fn unreachable_branch_sign(val: i32) -> i32 {
+    if val <= 0 {
+        -1
+    } else if val >= 0 {
+        1
+    } else {
+        prusti_refute!(false); //~ ERROR
+        0
+    }
+}
+
+#[requires(val < 0 && val > 0)]
+fn no_valid_input(val: i32) -> i32 {
+    prusti_refute!(false); //~ ERROR
+    42
+}
+
+fn main() {}

prusti-viper/src/encoder/errors/error_manager.rs

@@ -30,6 +30,8 @@ pub enum PanicCause {
     Panic,
     /// Caused by an assert!()
     Assert,
+    /// Caused by an refute!()
+    Refute,
     /// Caused by an debug_assert!()
     DebugAssert,
     /// Caused by an unreachable!()
@@ -696,6 +698,13 @@ impl<'tcx> ErrorManager<'tcx> {
                 )
             }
 
+            ("refute.failed:refutation.true", ErrorCtxt::Panic(PanicCause::Refute)) => {
+                PrustiError::verification(
+                    "the refuted expression holds in all cases or could not be reached",
+                    error_span,
+                )
+            }
+
             (full_err_id, ErrorCtxt::Unexpected) => {
                 PrustiError::internal(
                     format!(

prusti-viper/src/encoder/foldunfold/requirements.rs

@@ -71,7 +71,11 @@ impl RequiredStmtPermissionsGetter for vir::Stmt {
                     .collect()
             }
 
-            &vir::Stmt::Assert(vir::Assert {
+            &vir::Stmt::Refute(vir::Refute {
+                ref expr,
+                ref position,
+            })
+            | &vir::Stmt::Assert(vir::Assert {
                 ref expr,
                 ref position,
             })

prusti-viper/src/encoder/foldunfold/semantics.rs

@@ -61,6 +61,7 @@ impl ApplyOnState for vir::Stmt {
             &vir::Stmt::Comment(_)
             | &vir::Stmt::Label(_)
             | &vir::Stmt::Assert(_)
+            | &vir::Stmt::Refute(_)
             | &vir::Stmt::Obtain(_) => {}
 
             &vir::Stmt::Inhale(vir::Inhale { ref expr }) => {

prusti-viper/src/encoder/mir/specifications/interface.rs

@@ -97,6 +97,9 @@ pub(crate) trait SpecificationsInterface<'tcx> {
     /// Get the prusti assumption
     fn get_prusti_assumption(&self, def_id: DefId) -> Option<typed::PrustiAssumption>;
 
+    /// Get the prusti refutation
+    fn get_prusti_refutation(&self, def_id: DefId) -> Option<typed::PrustiRefutation>;
+
     /// Get the begin marker of the ghost block
     fn get_ghost_begin(&self, def_id: DefId) -> Option<typed::GhostBegin>;
 
@@ -234,6 +237,14 @@ impl<'v, 'tcx: 'v> SpecificationsInterface<'tcx> for super::super::super::Encode
             .cloned()
     }
 
+    fn get_prusti_refutation(&self, def_id: DefId) -> Option<typed::PrustiRefutation> {
+        self.specifications_state
+            .specs
+            .borrow()
+            .get_refutation(&def_id)
+            .cloned()
+    }
+
     fn get_ghost_begin(&self, def_id: DefId) -> Option<typed::GhostBegin> {
         self.specifications_state
             .specs

prusti-viper/src/encoder/mir/specifications/specs.rs

@@ -11,7 +11,7 @@ use prusti_interface::{
     specs::typed::{
         DefSpecificationMap, GhostBegin, GhostEnd, LoopSpecification, ProcedureSpecification,
         ProcedureSpecificationKind, ProcedureSpecificationKindError, PrustiAssertion,
-        PrustiAssumption, Refinable, SpecificationItem, TypeSpecification,
+        PrustiAssumption, PrustiRefutation, Refinable, SpecificationItem, TypeSpecification,
     },
     PrustiError,
 };
@@ -91,6 +91,11 @@ impl<'tcx> Specifications<'tcx> {
         self.user_typed_specs.get_assumption(def_id)
     }
 
+    #[tracing::instrument(level = "trace", skip(self))]
+    pub(super) fn get_refutation(&self, def_id: &DefId) -> Option<&PrustiRefutation> {
+        self.user_typed_specs.get_refutation(def_id)
+    }
+
     #[tracing::instrument(level = "trace", skip(self))]
     pub(super) fn get_ghost_begin(&self, def_id: &DefId) -> Option<&GhostBegin> {
         self.user_typed_specs.get_ghost_begin(def_id)