Merge branch 'master' into free-pcs

.github/workflows/crates-io.yml

@@ -5,6 +5,13 @@ on:
   push:
     branches: 'master'
     paths:
+      - '.github/workflows/crates-io.yml'
+      - 'prusti-contracts/**'
+      - '!prusti-contracts/prusti-contracts-test/**'
+  pull_request:
+    branches: 'master'
+    paths:
+      - '.github/workflows/crates-io.yml'
       - 'prusti-contracts/**'
       - '!prusti-contracts/prusti-contracts-test/**'
 
@@ -15,10 +22,12 @@ jobs:
       - name: Check out the repo
         uses: actions/checkout@v2
       - name: Publish crates.io
-        uses: katyo/publish-crates@v1
+        uses: katyo/publish-crates@v2
         with:
           path: './prusti-contracts'
           registry-token: ${{ secrets.CARGO_REGISTRY_TOKEN }}
+          # Do dry run in PRs
+          dry-run: ${{ github.event_name != 'push' }}
           # Without the delay `prusti-std` fails to be published since it doesn't
           # yet see the new version of `prusti-contracts`
           publish-delay: 1000

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)

jni-gen/src/errors.rs

@@ -59,5 +59,10 @@ error_chain::error_chain! {
             description("no field")
             display("no field '{}' in class '{}'", field, class)
         }
+
+        TraitField(class: String, field: String, actually_trait: bool) {
+            description("no field")
+            display("no field '{}' in class '{}', try using `{}field!` instead", field, class, if *actually_trait { "trait_" } else { "" })
+        }
     }
 }

jni-gen/src/generators/class.rs

@@ -7,7 +7,10 @@
 use crate::{
     class_name::*,
     errors::*,
-    generators::{constructor::*, field_getter_setter::*, method::*, scala_object_getter::*},
+    generators::{
+        constructor::*, field_getter_setter::*, method::*, scala_object_getter::*,
+        trait_field_getter_setter::*,
+    },
     wrapper_spec::*,
 };
 use jni::JNIEnv;
@@ -131,7 +134,10 @@ impl<'a> ClassGenerator<'a> {
                     suffix.clone(),
                 )?,
                 ItemWrapperSpec::FieldGetterSetter { ref field_name } => {
-                    generate_field_getter_setter(self.env, &self.class, field_name)?
+                    generate_field_getter_setter_for_class(self.env, &self.class, field_name)?
+                }
+                ItemWrapperSpec::TraitFieldGetterSetter { ref field_name } => {
+                    generate_field_getter_setter_for_trait(self.env, &self.class, field_name)?
                 }
             };
             gen_items.push(gen)

jni-gen/src/generators/field_getter_setter.rs

@@ -10,31 +10,33 @@ use jni::{
     JNIEnv,
 };
 
+use super::trait_field_getter_setter;
+
 fn hierarchy_field_lookup<'a>(
     env: &JNIEnv<'a>,
     class: &ClassName,
     lookup_name: &str,
 ) -> Result<Option<JObject<'a>>> {
-    let mut clazz = env.find_class(class.path())?;
-    while !clazz.is_null() {
-        if let Some(field) = class_field_lookup(env, clazz, lookup_name)? {
+    let mut class = env.find_class(class.path())?;
+    while !class.is_null() {
+        if let Some(field) = class_field_lookup(env, class, lookup_name)? {
             return Ok(Some(field));
         }
 
-        clazz = env.get_superclass(clazz)?;
+        class = env.get_superclass(class)?;
     }
 
     Ok(None)
 }
 
 fn class_field_lookup<'a>(
     env: &JNIEnv<'a>,
-    clazz: JClass<'a>,
+    class: JClass<'a>,
     lookup_name: &str,
 ) -> Result<Option<JObject<'a>>> {
     let fields = env
         .call_method(
-            clazz,
+            class,
             "getDeclaredFields",
             "()[Ljava/lang/reflect/Field;",
             &[],
@@ -170,13 +172,16 @@ fn generate_field_setter(class: &ClassName, field_name: &str, type_signature: &s
 /// It determines the type of the field by iterating over the
 /// inheritance hierarchy and checking for a field with the matching name
 ///
-/// For class type fields it also generates runtime checks verifying
+/// It also generates runtime checks verifying
 /// that the given object is of the specified class (or its descendant)
-pub fn generate_field_getter_setter(
+pub fn generate_field_getter_setter_for_class(
     env: &JNIEnv,
     class: &ClassName,
     field_name: &str,
 ) -> Result<String> {
+    if trait_field_getter_setter::is_interface(env, class)? {
+        return Err(ErrorKind::TraitField(class.full_name(), field_name.into(), true).into());
+    }
     let field_signature = match hierarchy_field_lookup(env, class, field_name)? {
         Some(field) => {
             let field_type = env