Merge #887

887: Automatically add loop guards without preconditions as invariants r=JonasAlaif a=JonasAlaif

Currently, when encoding loops:
```rust
while { g = G; g } { B1; invariant!(I); B2 }
```
Prusti will translate this into the Viper:
```boogie
// Encoding 1
g = G
if (g) {
  B1
  exhale I
  // ... havoc local variables modified in G, B1, or B2
  inhale I
  B2
  g = G
  if (g) {
    B1
    exhale I
    assume false
  }
  // We know !g at this point
}
```
We can try to assume the loop guard by adding the following:
```boogie
// Encoding 2
g = G
if (g) {
  B1
  exhale I
  // ... havoc local variables modified in G, B1, or B2

  g = G
  assume g
  B1

  inhale I
  ...
}
```
This works great, except for when `G` or `B1` include `exhale`/`assert` statements (including function calls with preconditions). In such a case, these statements would very likely fail (everything has been havoced, and we have-not/cannot yet assume the invariant) resulting in an unavoidable verification failure. The solution I take is to use encoding `2` if we find no such preconditions, and otherwise fall back to encoding `1` with a warning to the user.
Fixes #448, fixes #995

Co-authored-by: Jonas <jonas.fiala.cardiff@gmail.com>

prusti-interface/src/environment/mod.rs

@@ -16,7 +16,7 @@ use rustc_middle::ty::subst::{Subst, SubstsRef};
 use rustc_trait_selection::infer::{InferCtxtExt, TyCtxtInferExt};
 use std::path::PathBuf;
 
-use rustc_errors::MultiSpan;
+use rustc_errors::{DiagnosticBuilder, EmissionGuarantee, MultiSpan};
 use rustc_span::{Span, symbol::Symbol};
 use std::collections::HashSet;
 use log::{debug, trace};
@@ -76,6 +76,7 @@ pub struct Environment<'tcx> {
     bodies: RefCell<HashMap<LocalDefId, CachedBody<'tcx>>>,
     external_bodies: RefCell<HashMap<DefId, CachedExternalBody<'tcx>>>,
     tcx: TyCtxt<'tcx>,
+    warn_buffer: RefCell<Vec<rustc_errors::Diagnostic>>,
 }
 
 impl<'tcx> Environment<'tcx> {
@@ -85,6 +86,7 @@ impl<'tcx> Environment<'tcx> {
             tcx,
             bodies: RefCell::new(HashMap::new()),
             external_bodies: RefCell::new(HashMap::new()),
+            warn_buffer: RefCell::new(Vec::new()),
         }
     }
 
@@ -142,15 +144,12 @@ impl<'tcx> Environment<'tcx> {
     //     self.state.session.span_err(sp, msg);
     // }
 
-    /// Emits an error message.
-    pub fn span_err_with_help_and_notes<S: Into<MultiSpan> + Clone>(
-        &self,
+    fn configure_diagnostic<S: Into<MultiSpan> + Clone, T: EmissionGuarantee>(
+        diagnostic: &mut DiagnosticBuilder<T>,
         sp: S,
-        msg: &str,
         help: &Option<String>,
-        notes: &[(String, Option<S>)],
+        notes: &[(String, Option<S>)]
     ) {
-        let mut diagnostic = self.tcx.sess.struct_err(msg);
         diagnostic.set_span(sp);
         if let Some(help_msg) = help {
             diagnostic.help(help_msg);
@@ -162,10 +161,25 @@ impl<'tcx> Environment<'tcx> {
                 diagnostic.note(note_msg);
             }
         }
-        diagnostic.emit();
     }
 
     /// Emits an error message.
+    pub fn span_err_with_help_and_notes<S: Into<MultiSpan> + Clone>(
+        &self,
+        sp: S,
+        msg: &str,
+        help: &Option<String>,
+        notes: &[(String, Option<S>)],
+    ) {
+        let mut diagnostic = self.tcx.sess.struct_err(msg);
+        Self::configure_diagnostic(&mut diagnostic, sp, help, notes);
+        for warn in self.warn_buffer.borrow_mut().iter_mut() {
+            self.tcx.sess.diagnostic().emit_diagnostic(warn);
+        }
+        diagnostic.emit();
+    }
+
+    /// Emits a warning message.
     pub fn span_warn_with_help_and_notes<S: Into<MultiSpan> + Clone>(
         &self,
         sp: S,
@@ -174,20 +188,23 @@ impl<'tcx> Environment<'tcx> {
         notes: &[(String, Option<S>)],
     ) {
         let mut diagnostic = self.tcx.sess.struct_warn(msg);
-        diagnostic.set_span(sp);
-        if let Some(help_msg) = help {
-            diagnostic.help(help_msg);
-        }
-        for (note_msg, opt_note_sp) in notes {
-            if let Some(note_sp) = opt_note_sp {
-                diagnostic.span_note(note_sp.clone(), note_msg);
-            } else {
-                diagnostic.note(note_msg);
-            }
-        }
+        Self::configure_diagnostic(&mut diagnostic, sp, help, notes);
         diagnostic.emit();
     }
 
+    /// Buffers a warning message, to be emitted on error.
+    pub fn span_warn_on_err_with_help_and_notes<S: Into<MultiSpan> + Clone>(
+        &self,
+        sp: S,
+        msg: &str,
+        help: &Option<String>,
+        notes: &[(String, Option<S>)],
+    ) {
+        let mut diagnostic = self.tcx.sess.struct_warn(msg);
+        Self::configure_diagnostic(&mut diagnostic, sp, help, notes);
+        diagnostic.buffer(&mut self.warn_buffer.borrow_mut());
+    }
+
     /// Returns true if an error has been emitted
     pub fn has_errors(&self) -> bool {
         self.tcx.sess.has_errors().is_some()

prusti-interface/src/prusti_error.rs

@@ -21,7 +21,7 @@ use ::log::warn;
 /// `SpannedEncodingError` and similar types to something less confusing.)
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub struct PrustiError {
-    is_error: bool,
+    kind: PrustiErrorKind,
     /// If `true`, it should not be reported to the user. We need this in cases
     /// when the same error could be reported twice.
     ///
@@ -34,6 +34,13 @@ pub struct PrustiError {
     help: Option<String>,
     notes: Vec<(String, Option<MultiSpan>)>,
 }
+/// Determines how a `PrustiError` is reported.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum PrustiErrorKind {
+    Error, Warning,
+    /// A warning which is only shown if at least one error is emitted.
+    WarningOnError,
+}
 
 impl PartialOrd for PrustiError {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
@@ -51,7 +58,7 @@ impl PrustiError {
     /// Private constructor. Use one of the following methods.
     fn new(message: String, span: MultiSpan) -> Self {
         PrustiError {
-            is_error: true,
+            kind: PrustiErrorKind::Error,
             is_disabled: false,
             message,
             span,
@@ -101,6 +108,29 @@ impl PrustiError {
         )
     }
 
+    /// Report a non-fatal issue
+    pub fn warning<S: ToString>(message: S, span: MultiSpan) -> Self {
+        check_message(message.to_string());
+        let mut err = PrustiError::new(
+            format!("[Prusti: warning] {}", message.to_string()),
+            span
+        );
+        err.kind = PrustiErrorKind::Warning;
+        err
+    }
+
+    /// Report a non-fatal issue only if there are errors
+    /// (e.g. cannot automatically include loop guard as an invariant)
+    pub fn warning_on_error<S: ToString>(message: S, span: MultiSpan) -> Self {
+        check_message(message.to_string());
+        let mut err = PrustiError::new(
+            format!("[Prusti: warning] {}", message.to_string()),
+            span
+        );
+        err.kind = PrustiErrorKind::WarningOnError;
+        err
+    }
+
     /// Report an internal error of Prusti (e.g. failure of the fold-unfold)
     pub fn internal<S: ToString>(message: S, span: MultiSpan) -> Self {
         check_message(message.to_string());
@@ -122,11 +152,11 @@ impl PrustiError {
 
     /// Set that this Prusti error should be reported as a warning to the user
     pub fn set_warning(&mut self) {
-        self.is_error = false;
+        self.kind = PrustiErrorKind::Warning;
     }
 
     pub fn is_error(&self) -> bool {
-        self.is_error
+        matches!(self.kind, PrustiErrorKind::Error)
     }
 
     // FIXME: This flag is a temporary workaround for having duplicate errors
@@ -152,24 +182,31 @@ impl PrustiError {
         self.notes.push((message.to_string(), opt_span));
     }
 
-    /// Report the encoding error using the compiler's interface
+    /// Report the encoding error using the compiler's interface.
+    /// Warnings are not immediately emitted, but buffered and only shown
+    /// if an error is emitted (i.e. verification failure)
     pub fn emit(self, env: &Environment) {
         assert!(!self.is_disabled);
-        if self.is_error {
-            env.span_err_with_help_and_notes(
+        match self.kind {
+            PrustiErrorKind::Error => env.span_err_with_help_and_notes(
                 self.span,
                 &self.message,
                 &self.help,
                 &self.notes,
-            );
-        } else {
-            env.span_warn_with_help_and_notes(
+            ),
+            PrustiErrorKind::Warning => env.span_warn_with_help_and_notes(
                 self.span,
                 &self.message,
                 &self.help,
                 &self.notes,
-            );
-        }
+            ),
+            PrustiErrorKind::WarningOnError => env.span_warn_on_err_with_help_and_notes(
+                self.span,
+                &self.message,
+                &self.help,
+                &self.notes,
+            ),
+        };
     }
 
     /// Cancel the error.

prusti-tests/tests/verify_overflow/fail/optimizations/purification/test1.rs

@@ -5,20 +5,20 @@ use prusti_contracts::*;
 fn test1() {
     let mut i = 0;
     while i < 5 {
-        i += 1;     //~ ERROR: attempt to add with overflow
+        i += 1;
     }
     let mut j = 0;
-    assert!(i == j);
+    assert!(i == j);     //~ ERROR: the asserted expression might not hold
 }
 
 fn test2() {
     let mut i = 0;
     while i < 5 {
-        assert!(i < 5);  //~ ERROR: the asserted expression might not hold
+        assert!(i < 5);
         i += 1;
     }
     let mut j = 0;
-    assert!(i == j);
+    assert!(i == j);     //~ ERROR: the asserted expression might not hold
 }
 
 fn test3() {
@@ -35,7 +35,7 @@ fn test4(v: &mut[i32]) {
     let mut zero_num_start = 0;
     let mut i = 0;
     while i < v.len() {
-        assert!(i < v.len()); //~ ERROR: the asserted expression might not hold
+        assert!(i < v.len());
         i += 1;
     }
 }
@@ -44,8 +44,8 @@ fn test5(v: &mut[i32]) {
     let mut zero_num_start = 0;
     let mut i = 0;
     while i < v.len() {
-        if v[i] == 0 {  //~ ERROR: the array or slice index may be out of bounds
-            zero_num_start += 1;
+        if v[i] == 0 {
+            zero_num_start += 1; //~ ERROR: attempt to add with overflow
         }
         i += 1;
     }