Ugly commit 22.9.

prusti-common/src/vir/low_to_viper/ast.rs

@@ -272,7 +272,7 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expression {
             Expression::ContainerOp(expression) => expression.to_viper(context, ast),
             Expression::Conditional(expression) => expression.to_viper(context, ast),
             Expression::Quantifier(expression) => expression.to_viper(context, ast),
-            // Expression::LetExpr(expression) => expression.to_viper(context, ast),
+            Expression::LetExpr(expression) => expression.to_viper(context, ast),
             Expression::FuncApp(expression) => expression.to_viper(context, ast),
             Expression::DomainFuncApp(expression) => expression.to_viper(context, ast),
             // Expression::InhaleExhale(expression) => expression.to_viper(context, ast),
@@ -562,6 +562,17 @@ impl<'v, 'a> ToViper<'v, viper::Trigger<'v>> for (&'a expression::Trigger, Posit
     }
 }
 
+impl<'v> ToViper<'v, viper::Expr<'v>> for expression::LetExpr {
+    fn to_viper(&self, context: &mut Context<'v>, ast: &AstFactory<'v>) -> viper::Expr<'v> {
+        ast.let_expr_with_pos(
+            self.variable.to_viper_decl(context, ast),
+            self.def.to_viper(context, ast),
+            self.body.to_viper(context, ast),
+            self.position.to_viper(context, ast),
+        )
+    }
+}
+
 impl<'v> ToViper<'v, viper::Expr<'v>> for expression::FuncApp {
     fn to_viper(&self, context: &mut Context<'v>, ast: &AstFactory<'v>) -> viper::Expr<'v> {
         ast.func_app(

prusti-viper/src/encoder/middle/core_proof/interface.rs

@@ -100,12 +100,6 @@ impl<'v, 'tcx: 'v> MidCoreProofEncoderInterface<'tcx> for super::super::super::E
                     &mut program,
                 );
             }
-            if config::expand_quantifiers() {
-                program = super::transformations::expand_quantifiers::expand_quantifiers(
-                    &source_filename,
-                    program,
-                );
-            }
             if config::trace_with_symbolic_execution() {
                 if config::trace_with_symbolic_execution_new() {
                     program =
@@ -158,6 +152,12 @@ impl<'v, 'tcx: 'v> MidCoreProofEncoderInterface<'tcx> for super::super::super::E
                     predicates_info.owned_predicates_info,
                 )?;
             }
+            if config::expand_quantifiers() {
+                program = super::transformations::expand_quantifiers::expand_quantifiers(
+                    &source_filename,
+                    program,
+                );
+            }
             // We have to execute this pass because some of the transformations
             // generate nested old expressions, which cause problems when
             // triggering.

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution_new/procedure_executor/expressions.rs

@@ -1,4 +1,4 @@
-use super::{constraints::BlockConstraints, ProcedureExecutor};
+use super::{constraints::BlockConstraints, heap::PurificationResult, ProcedureExecutor};
 use crate::{
     encoder::{
         errors::{SpannedEncodingError, SpannedEncodingResult},
@@ -23,7 +23,14 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
         expression: &vir_low::Expression,
         position: vir_low::Position,
     ) -> SpannedEncodingResult<vir_low::Expression> {
-        let (expression, guarded_assertions) = self.purify_snap_function_calls(expression)?;
+        // self.add_statement(vir_low::Statement::comment(format!(
+        //     "simplify expression: {expression}"
+        // )))?;
+        let PurificationResult {
+            expression,
+            guarded_assertions,
+            bindings,
+        } = self.purify_snap_function_calls(expression)?;
         let current_block = self.current_block.as_ref().unwrap();
         let current_constraints = &mut self.state_keeper.get_state_mut(current_block).constraints;
         let mut simplifier = Simplifier {
@@ -32,6 +39,25 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
             expression_interner: &mut self.expression_interner,
         };
         let expression = simplifier.fallible_fold_expression(expression)?;
+        if !bindings.is_empty() {
+            self.add_statement(vir_low::Statement::comment(
+                "Let bindings for conditional snapshots".to_string(),
+            ))?;
+        }
+        for (variable, definition) in bindings {
+            self.add_statement(
+                vir_low::Statement::assume_no_pos(vir_low::Expression::equals(
+                    variable.into(),
+                    definition,
+                ))
+                .set_default_position(position),
+            )?;
+        }
+        if !guarded_assertions.is_empty() {
+            self.add_statement(vir_low::Statement::comment(
+                "Guarded assertions for snap function preconditions".to_string(),
+            ))?;
+        }
         for assertion in guarded_assertions {
             self.add_statement(
                 vir_low::Statement::assert_no_pos(assertion).set_default_position(position),

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution_new/procedure_executor/heap/common/mod.rs

@@ -11,6 +11,7 @@ pub(super) use self::{
         AliasedFractionalBool,
         //  AliasedFractionalBoundedPerm,
         AliasedWholeBool,
+        FindSnapshotResult,
         //    AliasedWholeNat,
         PredicateInstances,
     },

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution_new/procedure_executor/heap/common/named_predicate_instances.rs

@@ -1,5 +1,7 @@
 use super::{
-    predicate_instance::SnapshotType, predicate_instances::PermissionType, PredicateInstances,
+    predicate_instance::SnapshotType,
+    predicate_instances::{FindSnapshotResult, PermissionType},
+    PredicateInstances,
 };
 use crate::encoder::{
     errors::SpannedEncodingResult,
@@ -61,7 +63,7 @@ impl<P: PermissionType> NamedPredicateInstances<P, vir_low::VariableDecl> {
         constraints: &mut BlockConstraints,
         expression_interner: &mut ExpressionInterner,
         program_context: &ProgramContext<impl EncoderContext>,
-    ) -> SpannedEncodingResult<Option<(vir_low::Expression, Option<vir_low::Expression>)>> {
+    ) -> SpannedEncodingResult<FindSnapshotResult> {
         if let Some(predicate_instances) = self.predicates.get(predicate_name) {
             predicate_instances.find_snapshot(
                 predicate_name,
@@ -72,7 +74,7 @@ impl<P: PermissionType> NamedPredicateInstances<P, vir_low::VariableDecl> {
                 program_context,
             )
         } else {
-            Ok(None)
+            Ok(FindSnapshotResult::NotFound)
         }
     }
 }

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution_new/procedure_executor/heap/common/predicate_instances.rs

@@ -386,6 +386,18 @@ impl<P: PermissionType, S: std::fmt::Display + SnapshotType> std::fmt::Display
     }
 }
 
+pub(in super::super) enum FindSnapshotResult {
+    NotFound,
+    FoundGuarded {
+        snapshot: vir_low::VariableDecl,
+        precondition: Option<vir_low::Expression>,
+    },
+    FoundConditional {
+        binding: vir_low::VariableDecl,
+        definition: vir_low::Expression,
+    },
+}
+
 impl<P: PermissionType> PredicateInstances<P, vir_low::VariableDecl> {
     pub(in super::super) fn find_snapshot(
         &self,
@@ -395,7 +407,7 @@ impl<P: PermissionType> PredicateInstances<P, vir_low::VariableDecl> {
         constraints: &mut BlockConstraints,
         expression_interner: &mut ExpressionInterner,
         program_context: &ProgramContext<impl EncoderContext>,
-    ) -> SpannedEncodingResult<Option<(vir_low::Expression, Option<vir_low::Expression>)>> {
+    ) -> SpannedEncodingResult<FindSnapshotResult> {
         assert!(
             all_heap_independent(arguments),
             "arguments: {}",
@@ -414,16 +426,16 @@ impl<P: PermissionType> PredicateInstances<P, vir_low::VariableDecl> {
                     constraints,
                 )? {
                     MatchesResult::MatchesConditionally { assert } => {
-                        return Ok(Some((
-                            predicate_instance.snapshot_variable.clone().into(),
-                            Some(assert),
-                        )));
+                        return Ok(FindSnapshotResult::FoundGuarded {
+                            snapshot: predicate_instance.snapshot_variable.clone(),
+                            precondition: Some(assert),
+                        });
                     }
                     MatchesResult::MatchesUnonditionally => {
-                        return Ok(Some((
-                            predicate_instance.snapshot_variable.clone().into(),
-                            None,
-                        )));
+                        return Ok(FindSnapshotResult::FoundGuarded {
+                            snapshot: predicate_instance.snapshot_variable.clone(),
+                            precondition: None,
+                        });
                     }
                     MatchesResult::DoesNotMatch => {}
                 }
@@ -434,7 +446,10 @@ impl<P: PermissionType> PredicateInstances<P, vir_low::VariableDecl> {
                 program_context,
                 heap_variables,
             )?;
-            return Ok(Some((fresh_variable.into(), Some(false.into()))));
+            return Ok(FindSnapshotResult::FoundGuarded {
+                snapshot: fresh_variable,
+                precondition: Some(false.into()),
+            });
         }
 
         for predicate_instance in &self.aliased_predicate_instances {
@@ -448,39 +463,47 @@ impl<P: PermissionType> PredicateInstances<P, vir_low::VariableDecl> {
                 if predicate_instance.is_unconditional {
                     // We know for sure that we have a heap chunk and, therefore, this snapshot
                     // is unique and valid.
-                    return Ok(Some((
-                        predicate_instance.snapshot_variable.clone().into(),
-                        None,
-                    )));
+                    return Ok(FindSnapshotResult::FoundGuarded {
+                        snapshot: predicate_instance.snapshot_variable.clone(),
+                        precondition: None,
+                    });
                 }
                 if predicate_instance.is_materialized {
                     // The chunk is potentially aliased by a QP chunk. We cannot purify it out.
-                    return Ok(None);
+                    return Ok(FindSnapshotResult::NotFound);
                 }
             }
         }
         // We do not know which of the heap chunks is the one we need. Therefore, we return
         // a conditional.
-        let mut expression = <vir_low::VariableDecl as SnapshotType>::create_snapshot_variable(
+        let mut definition = <vir_low::VariableDecl as SnapshotType>::create_snapshot_variable(
             predicate_name,
             program_context,
             heap_variables,
         )?
         .into();
+        let binding = <vir_low::VariableDecl as SnapshotType>::create_snapshot_variable(
+            predicate_name,
+            program_context,
+            heap_variables,
+        )?;
         let mut predicate_instances = self
             .aliased_predicate_instances
             .iter()
             .filter(|predicate_instance| !predicate_instance.is_materialized);
         while let Some(predicate_instance) = predicate_instances.next() {
             let guard = predicate_instance
                 .create_matches_check(arguments, &predicate_instance.permission_amount)?;
-            expression = vir_low::Expression::conditional_no_pos(
+            definition = vir_low::Expression::conditional_no_pos(
                 guard,
                 predicate_instance.snapshot_variable.clone().into(),
-                expression,
+                definition,
             );
         }
-        Ok(Some((expression, None)))
+        Ok(FindSnapshotResult::FoundConditional {
+            binding,
+            definition,
+        })
     }
 }
 

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution_new/procedure_executor/heap/memory_block.rs

@@ -1,5 +1,5 @@
 use super::{
-    common::{AliasedFractionalBool, PredicateInstances},
+    common::{AliasedFractionalBool, FindSnapshotResult, PredicateInstances},
     global_heap_state::HeapVariables,
     merge_report::HeapMergeReport,
     GlobalHeapState,
@@ -133,7 +133,7 @@ impl MemoryBlock {
         constraints: &mut BlockConstraints,
         expression_interner: &mut ExpressionInterner,
         program_context: &ProgramContext<impl EncoderContext>,
-    ) -> SpannedEncodingResult<Option<(vir_low::Expression, Option<vir_low::Expression>)>> {
+    ) -> SpannedEncodingResult<FindSnapshotResult> {
         self.predicates.find_snapshot(
             MEMORY_BLOCK_PREDICATE_NAME,
             arguments,

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

@@ -1,6 +1,6 @@
 use self::{
     close_frac_ref::ClosedFracRef,
-    common::{AliasedWholeBool, NamedPredicateInstances, NoSnapshot},
+    common::{AliasedWholeBool, FindSnapshotResult, NamedPredicateInstances, NoSnapshot},
     dead_lifetimes::DeadLifetimeTokens,
     global_heap_state::HeapVariables,
     lifetimes::LifetimeTokens,
@@ -36,7 +36,10 @@ mod purification;
 mod merge_report;
 mod global_heap_state;
 
-pub(super) use self::{global_heap_state::GlobalHeapState, merge_report::HeapMergeReport};
+pub(super) use self::{
+    global_heap_state::GlobalHeapState, merge_report::HeapMergeReport,
+    purification::PurificationResult,
+};
 
 impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
     pub(super) fn save_state(&mut self, label: String) -> SpannedEncodingResult<()> {
@@ -50,7 +53,7 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> {
     pub(super) fn purify_snap_function_calls(
         &mut self,
         expression: &vir_low::Expression,
-    ) -> SpannedEncodingResult<(vir_low::Expression, Vec<vir_low::Expression>)> {
+    ) -> SpannedEncodingResult<PurificationResult> {
         let current_block = self.current_block.as_ref().unwrap();
         let current_state = self.state_keeper.get_state_mut(current_block);
         self::purification::purify_snap_function_calls(
@@ -740,7 +743,7 @@ impl<'a> HeapRef<'a> {
         constraints: &mut BlockConstraints,
         expression_interner: &mut ExpressionInterner,
         program_context: &ProgramContext<impl EncoderContext>,
-    ) -> SpannedEncodingResult<Option<(vir_low::Expression, Option<vir_low::Expression>)>> {
+    ) -> SpannedEncodingResult<FindSnapshotResult> {
         match self {
             HeapRef::Current(heap) => match program_context.get_predicate_kind(predicate_name) {
                 vir_low::PredicateKind::MemoryBlock => {

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution_new/procedure_executor/heap/owned.rs

@@ -1,5 +1,5 @@
 use super::{
-    common::{AliasedFractionalBool, NamedPredicateInstances},
+    common::{AliasedFractionalBool, FindSnapshotResult, NamedPredicateInstances},
     global_heap_state::HeapVariables,
     merge_report::HeapMergeReport,
     GlobalHeapState,
@@ -132,7 +132,7 @@ impl Owned {
         constraints: &mut BlockConstraints,
         expression_interner: &mut ExpressionInterner,
         program_context: &ProgramContext<impl EncoderContext>,
-    ) -> SpannedEncodingResult<Option<(vir_low::Expression, Option<vir_low::Expression>)>> {
+    ) -> SpannedEncodingResult<FindSnapshotResult> {
         self.predicates.find_snapshot(
             predicate_name,
             arguments,