Fix unfolding bugs.

.rustfmt.toml

@@ -1 +1,2 @@
 imports_granularity = "Crate"
+reorder_modules = false

prusti-interface/src/environment/mir_body/borrowck/facts/patch.rs

@@ -19,6 +19,7 @@ use rustc_hash::FxHashMap;
 ///     }
 /// }
 /// ```
+#[allow(clippy::needless_collect)] // False positive.
 pub fn apply_patch_to_borrowck<'tcx>(
     borrowck_input_facts: &mut AllInputFacts,
     location_table: &mut LocationTable,
@@ -103,6 +104,21 @@ pub fn apply_patch_to_borrowck<'tcx>(
             lt_patcher.start_point(loc.block.index(), loc.statement_index + 1);
         if loc.statement_index == 0 {
             predecessors_to_patch.push((loc, old_statement_start_point, statement_start_point));
+            if loc.block == mir::START_BLOCK {
+                assert_eq!(old_statement_start_point.index(), 0);
+                let old_subset_base: Vec<_> = borrowck_input_facts
+                    .subset_base
+                    .iter()
+                    .filter(|(_, _, point)| point == &old_statement_start_point)
+                    .cloned()
+                    .collect();
+                borrowck_input_facts.subset_base.extend(
+                    old_subset_base
+                        .into_iter()
+                        .map(|(subset, base, _)| (subset, base, statement_start_point)),
+                );
+                borrowck_input_facts.subset_base.sort();
+            }
         } else {
             // Insert the statement and patch the links with the previous and following statements.
             let previous_statement_mid_point =

prusti-launch/tests/test_binaries.rs

@@ -168,7 +168,7 @@ fn test_prusti_rustc_with_server() {
 
     // Preserve SYSTEMROOT on Windows.
     // See: https://travis-ci.community/t/socket-the-requested-service-provider-could-not-be-loaded-or-initialized/1127
-    let mut server_child = Command::new(&prusti_server)
+    let mut server_child = Command::new(prusti_server)
         .env("PRUSTI_LOG", "warn")
         .env("RUST_BACKTRACE", "1")
         .stdout(Stdio::piped())

prusti-tests/tests/verify_overflow/fail/core_proof/mutex.rs

@@ -0,0 +1,45 @@
+// compile-flags: -Punsafe_core_proof=true
+
+use prusti_contracts::*;
+
+use std::sync::Mutex;
+
+fn test1_fail<T>(m: &Mutex<T>) {
+    if let Ok(g1) = m.lock() {
+        assert!(false); //~ ERROR: the asserted expression might not hold
+    }
+}
+
+fn test2<T>(m: &Mutex<T>) {
+    if let Ok(g1) = m.lock() {
+    }
+}
+
+fn test3<T>(m: &Mutex<T>) {
+    if let Ok(g1) = m.lock() {
+        if let Ok(g2) = m.lock() {
+        }
+    }
+}
+
+fn test4<T>(m: &Mutex<T>) {
+    if let Ok(g1) = m.lock() {
+        if let Ok(g2) = m.lock() {
+            if let Ok(g3) = m.lock() {
+            }
+        }
+    }
+}
+
+fn test5<T>(m: &Mutex<T>) {
+    if let Ok(g1) = m.lock() {
+        if let Ok(g2) = m.lock() {
+            if let Ok(g3) = m.lock() {
+                if let Ok(g4) = m.lock() {
+                }
+            }
+        }
+    }
+}
+
+fn main() {}

prusti-utils/src/config.rs

@@ -133,6 +133,9 @@ lazy_static::lazy_static! {
         settings.set_default("hide_uuids", false).unwrap();
         settings.set_default("counterexample", false).unwrap();
         settings.set_default("print_counterexample_if_model_is_present", false).unwrap();
+        settings.set_default::<Option<String>>("save_failing_trace_to_file", None).unwrap();
+        settings.set_default::<Option<String>>("execute_only_failing_trace", None).unwrap();
+        settings.set_default::<Option<String>>("dump_fold_unfold_state_of_blocks", None).unwrap();
         settings.set_default("print_hash", false).unwrap();
         settings.set_default("enable_cache", true).unwrap();
         settings.set_default("enable_ghost_constraints", false).unwrap();
@@ -540,6 +543,62 @@ pub fn print_counterexample_if_model_is_present() -> bool {
     read_setting("print_counterexample_if_model_is_present")
 }
 
+/// If this is set to a path, Prusti will extract the information about the
+/// trace that led to the error and save it to the given file.
+///
+/// Note: This requires the `counterexample` and `unsafe_core_proof` options to
+/// be enabled.
+pub fn save_failing_trace_to_file() -> Option<String> {
+    let value: Option<String> = read_setting("save_failing_trace_to_file");
+    if value.is_some() {
+        assert!(
+            unsafe_core_proof(),
+            "Unsafe core proof needs to be enabled to save failing trace to file"
+        );
+        assert!(
+            counterexample(),
+            "Counterexamples need to be enabled to save failing trace to file"
+        );
+    }
+    value
+}
+
+/// Execute only the failing trace that was saved with
+/// `save_failing_trace_to_file`. This is done by replacing all non-executed
+/// basic blocks with `assume false`.
+///
+/// Note: This requires the `unsafe_core_proof` option to be enabled.
+///
+/// Note: This assumes that the program contains only a single method.
+pub fn execute_only_failing_trace() -> Option<String> {
+    let value: Option<String> = read_setting("execute_only_failing_trace");
+    if value.is_some() {
+        assert!(
+            unsafe_core_proof(),
+            "Unsafe core proof needs to be enabled to save failing trace to file"
+        );
+    }
+    value
+}
+
+/// Dump additional information about the fold-unfold state of the specified
+/// blocks. The blocks are expected to be generated by
+/// `save_failing_trace_to_file` (and potentially edited by hand if needed).
+///
+/// Note: This requires the `unsafe_core_proof` option to be enabled.
+///
+/// Note: This assumes that the program contains only a single method.
+pub fn dump_fold_unfold_state_of_blocks() -> Option<String> {
+    let value: Option<String> = read_setting("dump_fold_unfold_state_of_blocks");
+    if value.is_some() {
+        assert!(
+            unsafe_core_proof(),
+            "Unsafe core proof needs to be enabled to save failing trace to file"
+        );
+    }
+    value
+}
+
 /// When enabled, prints the hash of a verification request (the hash is used
 /// for caching). This is a debugging option which does not perform
 /// verification -- it is similar to `NO_VERIFY`, except that this flag stops

prusti-viper/Cargo.toml

@@ -21,6 +21,7 @@ vir-crate = { package = "vir", path = "../vir" }
 num-traits = "0.2"
 regex = "1.5"
 serde = "1.0"
+serde_json = "1.0"
 backtrace = "0.3"
 rustc-hash = "1.1.0"
 derive_more = "0.99.16"

prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs

@@ -31,7 +31,12 @@ pub fn backtranslate(
     let mut translator = CounterexampleTranslator::new(encoder, def_id, silicon_counterexample);
 
     translator.create_mapping(def_id, encoder); //creates the mapping between mir var and the corresponding snapshot var
-    let label_markers = translator.get_label_markers();
+    let label_markers = translator.get_label_markers(false);
+    if let Some(path) = config::save_failing_trace_to_file() {
+        let label_markers = translator.get_label_markers(true);
+        let mut file = std::fs::File::create(path).unwrap();
+        serde_json::to_writer_pretty(&mut file, &label_markers).unwrap();
+    }
 
     let counterexample_entry_vec = translator.process_entries(position_manager, &label_markers);
 
@@ -66,7 +71,13 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> {
         }
     }
     ///get all label markers and there value in the counterexample
-    fn get_label_markers(&self) -> FxHashMap<String, bool> {
+    ///
+    /// `default_for_not_found` – the value to use for labels that are not
+    /// found. For counterexamples, it should be `false` to show only the blocks
+    /// that were certainly visited to the user. For generating the failing
+    /// trace, it should be `true` to not delete blocks that were potentially
+    /// visited.
+    fn get_label_markers(&self, default_for_not_found: bool) -> FxHashMap<String, bool> {
         self.var_mapping
             .labels_successor_mapping
             .keys()
@@ -78,7 +89,7 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> {
                     .get(&format!("{}$marker", label))
                 {
                     Some(ModelEntry::LitBool(b)) => (label.clone(), *b),
-                    _ => (label.clone(), false), //if label marker is not found, we treat it like it was not visited (should be impossible)
+                    _ => (label.clone(), default_for_not_found),
                 }
             })
             .collect::<FxHashMap<String, bool>>()

prusti-viper/src/encoder/high/procedures/inference/action.rs

@@ -4,6 +4,7 @@ use vir_crate::{
     typed as vir_typed,
 };
 
+#[derive(Debug)]
 pub(in super::super) enum Action {
     Unfold(FoldingActionState),
     Fold(FoldingActionState),
@@ -33,6 +34,7 @@ impl std::fmt::Display for Action {
     }
 }
 
+#[derive(Debug)]
 pub(in super::super) struct FoldingActionState {
     pub(in super::super) kind: PermissionKind,
     pub(in super::super) place: vir_typed::Expression,
@@ -41,17 +43,20 @@ pub(in super::super) struct FoldingActionState {
     pub(in super::super) enum_variant: Option<vir_typed::ty::VariantIndex>,
 }
 
+#[derive(Debug)]
 pub(in super::super) struct ConversionState {
     pub(in super::super) place: vir_typed::Expression,
     pub(in super::super) condition: Option<vir_mid::BlockMarkerCondition>,
 }
 
+#[derive(Debug)]
 pub(in super::super) struct RestorationState {
     pub(in super::super) lifetime: vir_typed::ty::LifetimeConst,
     pub(in super::super) place: vir_typed::Expression,
     pub(in super::super) condition: Option<vir_mid::BlockMarkerCondition>,
 }
 
+#[derive(Debug)]
 pub(in super::super) struct UnreachableState {
     pub(in super::super) position: vir_typed::Position,
     pub(in super::super) condition: Option<vir_mid::BlockMarkerCondition>,