Refactoring

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!(
@@ -141,6 +148,11 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for statement::Fold {
             "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),
@@ -155,6 +167,11 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for statement::Unfold {
             "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),
@@ -235,7 +252,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),
@@ -361,6 +378,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/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())
     }
 }