Ugly commit 1.

prusti-utils/src/config.rs

@@ -122,6 +122,7 @@ lazy_static::lazy_static! {
         settings.set_default("custom_heap_encoding", false).unwrap();
         settings.set_default("trace_with_symbolic_execution", false).unwrap();
         settings.set_default("purify_with_symbolic_execution", false).unwrap();
+        settings.set_default("symbolic_execution_single_method", false).unwrap();
         settings.set_default("expand_quantifiers", false).unwrap();
         settings.set_default("report_symbolic_execution_failures", false).unwrap();
         settings.set_default("report_symbolic_execution_purification", false).unwrap();
@@ -922,7 +923,18 @@ pub fn trace_with_symbolic_execution() -> bool {
 /// **Note:** This option automatically enables
 /// `trace_with_symbolic_execution`.
 pub fn purify_with_symbolic_execution() -> bool {
-    read_setting("purify_with_symbolic_execution")
+    read_setting("purify_with_symbolic_execution") || symbolic_execution_single_method()
+}
+
+/// Puts all symbolic execution traces into a single method.
+///
+/// **Note:** This option is taken into account only when `unsafe_core_proof` is
+/// true.
+///
+/// **Note:** This option automatically enables
+/// `purify_with_symbolic_execution`.
+pub fn symbolic_execution_single_method() -> bool {
+    read_setting("symbolic_execution_single_method")
 }
 
 /// Whether to expand the asserted quantifiers (skolemize them out).

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/finalizer.rs

@@ -71,6 +71,14 @@ impl<'a, EC: EncoderContext> TraceFinalizer<'a, EC> {
         }
     }
 
+    pub(super) fn trace_len(&self) -> usize {
+        self.trace.len()
+    }
+
+    pub(super) fn trace_suffix(&self, checkpoint: usize) -> &[vir_low::Statement] {
+        self.trace[checkpoint..].as_ref()
+    }
+
     pub(super) fn add_variables(
         &mut self,
         new_variables: &[vir_low::VariableDecl],

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/mod.rs

@@ -192,9 +192,12 @@ impl<'a> ExecutionTraceBuilder<'a> {
         }
         trace_finalizer.add_variables(block.get_new_variables())?;
         trace_finalizer.add_labels(block.get_new_labels())?;
+        let trace_checkpoint = trace_finalizer.trace_len();
         for (entry_id, entry) in block.iter_entries().enumerate() {
             trace_finalizer.add_entry(Location { block_id, entry_id }, entry)?;
         }
+        let finalized_statements = trace_finalizer.trace_suffix(trace_checkpoint);
+        block.set_finalized_statements(finalized_statements);
         Ok(())
     }
 }

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/mod.rs

@@ -300,9 +300,19 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
             }
         }
         if config::purify_with_symbolic_execution() {
-            for (i, trace) in self.final_traces.into_iter().enumerate() {
-                let new_procedure = trace.into_procedure(i, &procedure);
+            if config::symbolic_execution_single_method() {
+                let new_procedure = self.execution_trace_builder.into_procedure(&procedure);
+                prusti_common::report::log::report_with_writer(
+                    "graphviz_method_vir_low_symbex_single_method",
+                    format!("{}.{}.dot", self.source_filename, new_procedure.name),
+                    |writer| new_procedure.to_graphviz(writer).unwrap(),
+                );
                 new_procedures.push(new_procedure);
+            } else {
+                for (i, trace) in self.final_traces.into_iter().enumerate() {
+                    let new_procedure = trace.into_procedure(i, &procedure);
+                    new_procedures.push(new_procedure);
+                }
             }
         } else {
             for (i, trace) in self.original_traces.into_iter().enumerate() {

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/trace_builder/heap_view.rs

@@ -50,4 +50,19 @@ impl<'a> BlockView<'a> {
     pub(in super::super) fn get_new_labels(&self) -> &[vir_low::Label] {
         &self.block.new_labels
     }
+
+    pub(crate) fn set_finalized_statements(&self, new_statements: &[vir_low::Statement]) {
+        let mut borrow = self.block.finalized_statements.borrow_mut();
+        if let Some(statements) = borrow.as_ref() {
+            // FIXME: This does not work because whether an inhale is purified
+            // out depends on whether a matching exhale is found, which depends
+            // on the executed trace.
+            for (old, new) in statements.iter().zip(new_statements.iter()) {
+                assert_eq!(old, new);
+            }
+            assert_eq!(statements.len(), new_statements.len());
+        } else {
+            *borrow = Some(new_statements.to_vec());
+        }
+    }
 }

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/trace_builder/mod.rs

@@ -16,7 +16,7 @@ use crate::encoder::{
 use rustc_hash::FxHashMap;
 use std::collections::BTreeMap;
 use vir_crate::{
-    common::graphviz::ToGraphviz,
+    common::{expression::BinaryOperationHelpers, graphviz::ToGraphviz},
     low::{self as vir_low},
 };
 
@@ -227,6 +227,70 @@ impl<'a> ExecutionTraceBuilder<'a> {
         assert_eq!(last_block.heap_statements.len(), 1);
         Ok(())
     }
+
+    pub(super) fn into_procedure(
+        mut self,
+        original_procedure: &vir_low::ProcedureDecl,
+    ) -> vir_low::ProcedureDecl {
+        let entry = vir_low::Label::new("trace_start");
+        let exit = vir_low::Label::new("trace_end");
+        let mut jump_targets = vec![Vec::new(); self.blocks.len()];
+        for (i, block) in self.blocks.iter().enumerate() {
+            if let Some(parent) = block.parent {
+                jump_targets[parent].push(i);
+            }
+        }
+        let mut locals = original_procedure.locals.clone();
+        let mut custom_labels = original_procedure.custom_labels.clone();
+        let mut basic_blocks = BTreeMap::new();
+        for (i, block) in std::mem::take(&mut self.blocks).into_iter().enumerate() {
+            let mut statements = block.finalized_statements.borrow_mut().take().unwrap();
+            let successor = match jump_targets[i].len() {
+                0 => vir_low::Successor::Goto(exit.clone()),
+                1 => vir_low::Successor::Goto(vir_low::Label::new(format!(
+                    "trace_block_{}",
+                    jump_targets[i][0]
+                ))),
+                _ => {
+                    let mut targets = Vec::new();
+                    let variable = vir_low::VariableDecl::new(
+                        format!("trace_block_{}_guard", i),
+                        vir_low::Type::Int,
+                    );
+                    for (j, target) in jump_targets[i].iter().enumerate() {
+                        let guard = vir_low::Expression::equals(variable.clone().into(), j.into());
+                        let label = vir_low::Label::new(format!("trace_block_{}", target));
+                        targets.push((guard, label));
+                    }
+                    statements.push(vir_low::Statement::assume(
+                        vir_low::Expression::and(
+                            vir_low::Expression::greater_equals(0.into(), variable.clone().into()),
+                            vir_low::Expression::less_than(
+                                variable.into(),
+                                jump_targets[i].len().into(),
+                            ),
+                        ),
+                        original_procedure.position,
+                    ));
+                    vir_low::Successor::GotoSwitch(targets)
+                }
+            };
+            let basic_block = vir_low::BasicBlock::new(statements, successor);
+            basic_blocks.insert(
+                vir_low::Label::new(format!("trace_block_{}", i)),
+                basic_block,
+            );
+        }
+        vir_low::ProcedureDecl::new_with_pos(
+            format!("{}$trace", original_procedure.name),
+            locals,
+            custom_labels,
+            entry,
+            exit,
+            basic_blocks,
+            original_procedure.position,
+        )
+    }
 }
 
 struct ExecutionTraceBlock {
@@ -240,6 +304,8 @@ struct ExecutionTraceBlock {
     original_statements: Vec<vir_low::Statement>,
     /// Statements that make the heap operations more explicit.
     heap_statements: Vec<HeapEntry>,
+    /// Statements after all the transformations.
+    finalized_statements: std::cell::RefCell<Option<Vec<vir_low::Statement>>>,
     /// The last heap state. If the block is fully executed, it is the state
     /// after the last statement.
     heap_state: HeapState,
@@ -260,6 +326,7 @@ impl ExecutionTraceBlock {
             new_labels: Vec::new(),
             original_statements: Vec::new(),
             heap_statements: Vec::new(),
+            finalized_statements: std::cell::RefCell::new(None),
             heap_state: HeapState::default(),
             egraph_state: Some(EGraphState::new(domains, bool_type, bool_domain_info)?),
         })
@@ -272,6 +339,7 @@ impl ExecutionTraceBlock {
             new_labels: Vec::new(),
             original_statements: Vec::new(),
             heap_statements: Vec::new(),
+            finalized_statements: std::cell::RefCell::new(None),
             heap_state: parent.heap_state.clone(),
             egraph_state: parent.egraph_state.clone(),
         }