Ugly commit 30.54

prusti-utils/src/config.rs

@@ -205,6 +205,7 @@ lazy_static::lazy_static! {
         settings.set_default::<Option<String>>("svirpti_smt_solver_log", None).unwrap();
         settings.set_default("svirpti_stop_on_first_error", false).unwrap();
         settings.set_default("svirpti_use_pseudo_boolean_heap", false).unwrap();
+        settings.set_default("svirpti_enable_smoke_check", false).unwrap();
 
         // Get the list of all allowed flags.
         let mut allowed_keys = get_keys(&settings);
@@ -1312,6 +1313,11 @@ pub fn svirpti_use_pseudo_boolean_heap() -> bool {
     read_setting("svirpti_use_pseudo_boolean_heap")
 }
 
+/// Try asserting `false` after each statement and report an error if succeed.
+pub fn svirpti_enable_smoke_check() -> bool {
+    read_setting("svirpti_enable_smoke_check")
+}
+
 /// When enabled, features not supported by Prusti will be reported as warnings
 /// rather than errors.
 pub fn skip_unsupported_features() -> bool {

prusti-viper/src/encoder/middle/core_proof/svirpti/procedure_verifier/heap/boolean_mask_log_with_heap.rs

@@ -107,7 +107,8 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
             for definition in guard_definitions {
                 self.assume(&definition)?;
             }
-            self.assume(&check)?;
+            let negated_check = vir_low::Expression::not(check.clone());
+            self.assume(&negated_check)?;
         }
 
         // Update the global heap.
@@ -262,7 +263,7 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
         Ok(())
     }
 
-    fn create_permission_check(
+    pub(super) fn create_permission_check(
         &mut self,
         predicate_name: &str,
         predicate_arguments: &[vir_low::Expression],
@@ -313,7 +314,7 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
             LogEntry::InhaleQuantified(entry) => unimplemented!(),
             LogEntry::ExhaleFull(_) | LogEntry::ExhaleQuantified(_) => unreachable!(),
         };
-        for (entry, mut guard) in entry_iterator {
+        for (entry, guard) in entry_iterator {
             match entry {
                 LogEntry::InhaleFull(entry) => {
                     let arguments_equal = arguments_equal(&predicate_arguments, &entry.arguments);

prusti-viper/src/encoder/middle/core_proof/svirpti/procedure_verifier/heap/boolean_mask_log_without_heap.rs

@@ -10,7 +10,7 @@ use crate::encoder::{
 use prusti_common::config;
 use rustc_hash::FxHashMap;
 use vir_crate::{
-    common::expression::{BinaryOperationHelpers, ExpressionIterator},
+    common::expression::{BinaryOperationHelpers, ExpressionIterator, UnaryOperationHelpers},
     low as vir_low,
 };
 
@@ -55,6 +55,17 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
         *log_entry += 1;
         let new_log_entry = *log_entry;
 
+        // Update Z3 state.
+        if !config::svirpti_use_pseudo_boolean_heap() && old_log_entry > 0 {
+            let (guard_definitions, check) =
+                self.create_permission_check(&predicate.name, &predicate.arguments, old_log_entry)?;
+            for definition in guard_definitions {
+                self.assume(&definition)?;
+            }
+            let negated_check = vir_low::Expression::not(check.clone());
+            self.assume(&negated_check)?;
+        }
+
         // Update the global heap.
         let entries = self
             .global_heap
@@ -151,66 +162,8 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
         full_error_id: &str,
         position: vir_low::Position,
     ) -> SpannedEncodingResult<()> {
-        use vir_low::macros::*;
-        assert!(
-            entry_id > 0,
-            "TODO: A proper error message that we are exhaling for an empty heap."
-        );
-        let mut guards = Vec::with_capacity(entry_id);
-        for _ in 0..entry_id {
-            let guard_id = self.generate_fresh_id();
-            let guard_name = format!("guard${}", guard_id);
-            let guard = vir_low::VariableDecl::new(guard_name, vir_low::Type::Bool);
-            self.declare_variable(&guard)?;
-            guards.push(guard);
-        }
-        fn arguments_equal(
-            predicate_arguments: &[vir_low::Expression],
-            entry_arguments: &[vir_low::Expression],
-        ) -> vir_low::Expression {
-            use vir_low::macros::*;
-            predicate_arguments
-                .iter()
-                .zip(entry_arguments.iter())
-                .map(|(predicate_argument, entry_argument)| {
-                    expr! { [predicate_argument.clone()] == [entry_argument.clone()] }
-                })
-                .conjoin()
-        }
-        let entries = self
-            .global_heap
-            .boolean_mask_log
-            .entries
-            .get_mut(predicate_name)
-            .unwrap();
-        let mut entry_iterator = entries.iter().take(entry_id).zip(guards.into_iter());
-        let mut guard_definitions = Vec::with_capacity(entry_id);
-        let (first_entry, first_guard) = entry_iterator.next().unwrap();
-        let mut check_permissions: vir_low::Expression = match first_entry {
-            LogEntry::InhaleFull(entry) => {
-                let arguments_equal = arguments_equal(&predicate_arguments, &entry.arguments);
-                guard_definitions.push(expr! { first_guard == [arguments_equal] });
-                first_guard.into()
-            }
-            LogEntry::InhaleQuantified(entry) => unimplemented!(),
-            LogEntry::ExhaleFull(_) | LogEntry::ExhaleQuantified(_) => unreachable!(),
-        };
-        for (entry, guard) in entry_iterator {
-            match entry {
-                LogEntry::InhaleFull(entry) => {
-                    let arguments_equal = arguments_equal(&predicate_arguments, &entry.arguments);
-                    guard_definitions.push(expr! { guard == [arguments_equal] });
-                    check_permissions = vir_low::Expression::or(check_permissions, guard.into());
-                }
-                LogEntry::ExhaleFull(entry) => {
-                    let arguments_equal = arguments_equal(&predicate_arguments, &entry.arguments);
-                    guard_definitions.push(expr! { guard == [arguments_equal] });
-                    check_permissions = vir_low::Expression::and(check_permissions, guard.into());
-                }
-                LogEntry::InhaleQuantified(_) => todo!(),
-                LogEntry::ExhaleQuantified(_) => todo!(),
-            }
-        }
+        let (guard_definitions, mut check_permissions) =
+            self.create_permission_check(predicate_name, predicate_arguments, entry_id)?;
         if let Some(guard) = guard {
             check_permissions = vir_low::Expression::implies(guard, check_permissions);
         }

prusti-viper/src/encoder/middle/core_proof/svirpti/procedure_verifier/mod.rs

@@ -131,6 +131,12 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
 
     fn execute_block(&mut self, block: &vir_low::BasicBlock) -> SpannedEncodingResult<()> {
         eprintln!("Executing block: {}", self.current_frame().label());
+        self.smt_solver
+            .comment(&format!(
+                "Executing block: {}",
+                self.current_frame().label()
+            ))
+            .unwrap(); // FIXME: Handle errors
         for statement in &block.statements {
             self.execute_statement(statement)?;
             if self.reached_contradiction {

prusti-viper/src/encoder/middle/core_proof/svirpti/procedure_verifier/solver.rs

@@ -23,6 +23,12 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
         Ok(())
     }
 
+    pub(super) fn smoke_check(&mut self) -> SpannedEncodingResult<()> {
+        let result = self.smt_solver.check_sat().unwrap(); // TODO: handle error
+        assert!(!result.is_unsat(), "Smoke check failed");
+        Ok(())
+    }
+
     pub(super) fn assert(
         &mut self,
         expression: vir_low::Expression,

prusti-viper/src/encoder/middle/core_proof/svirpti/procedure_verifier/statements/mod.rs

@@ -1,5 +1,6 @@
 use super::{super::super::transformations::encoder_context::EncoderContext, ProcedureExecutor};
 use crate::encoder::errors::SpannedEncodingResult;
+use prusti_common::config;
 use vir_crate::{common::expression::SyntacticEvaluation, low as vir_low};
 
 mod exhale;
@@ -50,6 +51,9 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
                 self.execute_case_split(statement)?;
             }
         }
+        if config::svirpti_enable_smoke_check() {
+            self.smoke_check()?;
+        }
         Ok(())
     }