Ugly commit.

.github/workflows/test.yml

@@ -110,7 +110,7 @@ jobs:
   # Run a subset of the tests with the purification optimization enabled
   # to ensure that we do not introduce regressions.
   purification-tests:
-    needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
+    #needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
     runs-on: ubuntu-latest
     env:
       PRUSTI_ENABLE_PURIFICATION_OPTIMIZATION: true
@@ -162,6 +162,36 @@ jobs:
           # python x.py test --all pass/pure-fn/ref-mut-arg.rs
           # python x.py test --all pass/rosetta/Ackermann_function.rs
           # python x.py test --all pass/rosetta/Heapsort.rs
+      - name: custom_heap_encoding
+        env:
+          PRUSTI_VIPER_BACKEND: carbon
+          PRUSTI_CUSTOM_HEAP_ENCODING: true
+          PRUSTI_TRACE_WITH_SYMBOLIC_EXECUTION: false
+          PRUSTI_PURIFY_WITH_SYMBOLIC_EXECUTION: false
+        run: |
+          python x.py test custom_heap_encoding
+      - name: purify_with_symbolic_execution
+        env:
+          PRUSTI_VIPER_BACKEND: carbon
+          PRUSTI_CUSTOM_HEAP_ENCODING: false
+          PRUSTI_PURIFY_WITH_SYMBOLIC_EXECUTION: true
+        run: |
+          python x.py test custom_heap_encoding
+      - name: custom_heap_encoding and purify_with_symbolic_execution
+        env:
+          PRUSTI_VIPER_BACKEND: carbon
+          PRUSTI_CUSTOM_HEAP_ENCODING: true
+          PRUSTI_PURIFY_WITH_SYMBOLIC_EXECUTION: true
+        run: |
+          python x.py test custom_heap_encoding
+      - name: trace_with_symbolic_execution
+        env:
+          PRUSTI_VIPER_BACKEND: silicon
+          PRUSTI_CUSTOM_HEAP_ENCODING: false
+          PRUSTI_TRACE_WITH_SYMBOLIC_EXECUTION: false
+          PRUSTI_PURIFY_WITH_SYMBOLIC_EXECUTION: false
+        run: |
+          python x.py test custom_heap_encoding
       - name: Run with purification.
         env:
           PRUSTI_VIPER_BACKEND: silicon

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

@@ -46,6 +46,7 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for Statement {
     fn to_viper(&self, context: Context, ast: &AstFactory<'v>) -> viper::Stmt<'v> {
         match self {
             Statement::Comment(statement) => statement.to_viper(context, ast),
+            Statement::Label(statement) => statement.to_viper(context, ast),
             Statement::LogEvent(statement) => statement.to_viper(context, ast),
             Statement::Assume(statement) => statement.to_viper(context, ast),
             Statement::Assert(statement) => statement.to_viper(context, ast),
@@ -67,6 +68,12 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for statement::Comment {
     }
 }
 
+impl<'v> ToViper<'v, viper::Stmt<'v>> for statement::Label {
+    fn to_viper(&self, _context: Context, ast: &AstFactory<'v>) -> viper::Stmt<'v> {
+        ast.label(&self.label, &[])
+    }
+}
+
 impl<'v> ToViper<'v, viper::Stmt<'v>> for statement::LogEvent {
     fn to_viper(&self, context: Context, ast: &AstFactory<'v>) -> viper::Stmt<'v> {
         assert!(
@@ -135,6 +142,11 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for statement::Fold {
             !self.position.is_default(),
             "Statement with default position: {self}"
         );
+        assert!(
+            self.expression.is_predicate_access_predicate(),
+            "fold {}",
+            self.expression
+        );
         ast.fold_with_pos(
             self.expression.to_viper(context, ast),
             self.position.to_viper(context, ast),
@@ -148,6 +160,11 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for statement::Unfold {
             !self.position.is_default(),
             "Statement with default position: {self}"
         );
+        assert!(
+            self.expression.is_predicate_access_predicate(),
+            "unfold {}",
+            self.expression
+        );
         ast.unfold_with_pos(
             self.expression.to_viper(context, ast),
             self.position.to_viper(context, ast),
@@ -199,6 +216,10 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for statement::MethodCall {
 
 impl<'v> ToViper<'v, viper::Stmt<'v>> for statement::Assign {
     fn to_viper(&self, context: Context, ast: &AstFactory<'v>) -> viper::Stmt<'v> {
+        assert!(
+            !self.position.is_default(),
+            "Statement with default position: {self}"
+        );
         let target_expression = Expression::local(self.target.clone(), self.position);
         ast.abstract_assign(
             target_expression.to_viper(context, ast),
@@ -225,7 +246,7 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expression {
             Expression::MagicWand(expression) => expression.to_viper(context, ast),
             Expression::PredicateAccessPredicate(expression) => expression.to_viper(context, ast),
             // Expression::FieldAccessPredicate(expression) => expression.to_viper(context, ast),
-            // Expression::Unfolding(expression) => expression.to_viper(context, ast),
+            Expression::Unfolding(expression) => expression.to_viper(context, ast),
             Expression::UnaryOp(expression) => expression.to_viper(context, ast),
             Expression::BinaryOp(expression) => expression.to_viper(context, ast),
             Expression::PermBinaryOp(expression) => expression.to_viper(context, ast),
@@ -351,6 +372,16 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for expression::PredicateAccessPredicate {
     }
 }
 
+impl<'v> ToViper<'v, viper::Expr<'v>> for expression::Unfolding {
+    fn to_viper(&self, context: Context, ast: &AstFactory<'v>) -> viper::Expr<'v> {
+        ast.unfolding_with_pos(
+            self.predicate.to_viper(context, ast),
+            self.base.to_viper(context, ast),
+            self.position.to_viper(context, ast),
+        )
+    }
+}
+
 impl<'v> ToViper<'v, viper::Expr<'v>> for expression::UnaryOp {
     fn to_viper(&self, context: Context, ast: &AstFactory<'v>) -> viper::Expr<'v> {
         match self.op_kind {

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

@@ -15,14 +15,19 @@ impl<'a, 'v> ToViper<'v, viper::Method<'v>> for &'a ProcedureDecl {
         for local in &self.locals {
             declarations.push(local.to_viper_decl(context, ast).into());
         }
-        for block in &self.basic_blocks {
-            declarations.push(block.label.to_viper_decl(context, ast).into());
-            statements.push(block.label.to_viper(context, ast));
+        let traversal_order = self.get_topological_sort();
+        for label in &traversal_order {
+            let block = self.basic_blocks.get(label).unwrap();
+            declarations.push(label.to_viper_decl(context, ast).into());
+            statements.push(label.to_viper(context, ast));
             statements.extend(block.statements.to_viper(context, ast));
             statements.push(block.successor.to_viper(context, ast));
         }
         statements.push(ast.label(RETURN_LABEL, &[]));
         declarations.push(ast.label(RETURN_LABEL, &[]).into());
+        for label in &self.custom_labels {
+            declarations.push(label.to_viper_decl(context, ast).into());
+        }
         let body = Some(ast.seqn(&statements, &declarations));
         ast.method(&self.name, &[], &[], &[], &[], body)
     }

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

@@ -1,13 +1,15 @@
 use super::{Context, ToViper, ToViperDecl};
 use viper::{self, AstFactory};
-use vir::low::{DomainAxiomDecl, DomainDecl, DomainFunctionDecl};
+use vir::low::{DomainAxiomDecl, DomainDecl, DomainFunctionDecl, DomainRewriteRuleDecl};
 
 impl<'a, 'v> ToViper<'v, viper::Domain<'v>> for &'a DomainDecl {
     fn to_viper(&self, context: Context, ast: &AstFactory<'v>) -> viper::Domain<'v> {
+        let mut axioms = (&self.name, &self.axioms).to_viper(context, ast);
+        axioms.extend((&self.name, &self.rewrite_rules).to_viper(context, ast));
         ast.domain(
             &self.name,
             &(&self.name, &self.functions).to_viper(context, ast),
-            &(&self.name, &self.axioms).to_viper(context, ast),
+            &axioms,
             &[],
         )
     }
@@ -61,3 +63,31 @@ impl<'a, 'v> ToViper<'v, viper::NamedDomainAxiom<'v>> for (&'a String, &'a Domai
         }
     }
 }
+
+impl<'a, 'v> ToViper<'v, Vec<viper::NamedDomainAxiom<'v>>>
+    for (&'a String, &'a Vec<DomainRewriteRuleDecl>)
+{
+    fn to_viper(&self, context: Context, ast: &AstFactory<'v>) -> Vec<viper::NamedDomainAxiom<'v>> {
+        self.1
+            .iter()
+            .map(|axiom| (self.0, axiom).to_viper(context, ast))
+            .collect()
+    }
+}
+
+impl<'a, 'v> ToViper<'v, viper::NamedDomainAxiom<'v>> for (&'a String, &'a DomainRewriteRuleDecl) {
+    fn to_viper(&self, context: Context, ast: &AstFactory<'v>) -> viper::NamedDomainAxiom<'v> {
+        let (domain_name, rewrite_rule) = self;
+        let axiom = rewrite_rule.convert_into_axiom();
+        if let Some(comment) = &axiom.comment {
+            ast.named_domain_axiom_with_comment(
+                &axiom.name,
+                axiom.body.to_viper(context, ast),
+                domain_name,
+                comment,
+            )
+        } else {
+            ast.named_domain_axiom(&axiom.name, axiom.body.to_viper(context, ast), domain_name)
+        }
+    }
+}

prusti-common/src/vir/program.rs

@@ -21,12 +21,14 @@ impl Program {
         }
     }
     pub fn get_check_mode(&self) -> vir::common::check_mode::CheckMode {
+        // FIXME: Remove because this is not needed anymore.
         match self {
-            Program::Legacy(_) => vir::common::check_mode::CheckMode::Both,
+            Program::Legacy(_) => vir::common::check_mode::CheckMode::MemorySafetyWithFunctional,
             Program::Low(program) => program.check_mode,
         }
     }
     pub fn get_name_with_check_mode(&self) -> String {
+        // FIXME: Remove because this is not needed anymore.
         format!("{}-{}", self.get_name(), self.get_check_mode())
     }
 }