Sif extension

docs/dev-guide/src/config/flags.md

@@ -59,6 +59,7 @@
 | [`SERVER_ADDRESS`](#server_address) | `Option<String>` | `None` | A |
 | [`SERVER_MAX_CONCURRENCY`](#server_max_concurrency) | `Option<usize>` | `None` | A |
 | [`SERVER_MAX_STORED_VERIFIERS`](#server_max_stored_verifiers) | `Option<usize>` | `None` | A |
+| [`SIF`](#sif) | `bool` | `false`| A |
 | [`SIMPLIFY_ENCODING`](#simplify_encoding) | `bool` | `true` | A |
 | [`SKIP_UNSUPPORTED_FEATURES`](#skip_unsupported_features) | `bool` | `false` | A |
 | [`SMT_QI_BOUND_GLOBAL`](#smt_qi_bound_global) | `Option<u64>` | `None` | A |
@@ -373,6 +374,10 @@ Maximum amount of instantiated Viper verifiers the server will keep around for r
 
 > **Note:** This does _not_ limit how many verification requests the server handles concurrently, only the size of what is essentially its verifier cache.
 
+## `SIF`
+
+When enabled, check the program for secure information flow.
+
 ## `SIMPLIFY_ENCODING`
 
 When enabled, the encoded program is simplified before it is passed to the Viper backend.

prusti-common/src/vir/optimizations/folding/expressions.rs

@@ -399,6 +399,13 @@ impl ast::FallibleExprFolder for ExprOptimizer {
         Err(())
     }
 
+    fn fallible_fold_low(
+        &mut self,
+        _expr: vir::polymorphic::Low,
+    ) -> Result<vir::polymorphic::Expr, Self::Error> {
+        Err(())
+    }
+
     fn fallible_fold_predicate_access_predicate(
         &mut self,
         _predicate_access_predicate: ast::PredicateAccessPredicate,

prusti-common/src/vir/optimizations/functions/simplifier.rs

@@ -19,8 +19,9 @@ impl Simplifier for ast::Function {
     /// <https://github.com/viperproject/silicon/issues/387>
     #[tracing::instrument(level = "debug", skip(self), fields(self = %self), ret(Display))]
     fn simplify(mut self) -> Self {
-        let new_body = self.body.map(|b| b.simplify());
-        self.body = new_body;
+        self.body = self.body.map(|b| b.simplify());
+        self.posts = self.posts.into_iter().map(|p| p.simplify()).collect();
+        self.pres = self.pres.into_iter().map(|p| p.simplify()).collect();
         self
     }
 }
@@ -29,7 +30,8 @@ impl Simplifier for ast::Expr {
     #[must_use]
     fn simplify(self) -> Self {
         let mut folder = ExprSimplifier {};
-        folder.fold(self)
+        let res = folder.fold(self);
+        res
     }
 }
 
@@ -44,134 +46,115 @@ impl ExprSimplifier {
                 argument:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
                 position: pos,
             }) => ast::Expr::Const(ast::ConstExpr {
                 value: ast::Const::Bool(!b),
                 position: pos,
-            }),
+            })
+            .set_default_pos(inner_pos),
             ast::Expr::UnaryOp(ast::UnaryOp {
                 op_kind: ast::UnaryOpKind::Not,
                 argument:
                     box ast::Expr::BinOp(ast::BinOp {
                         op_kind: ast::BinaryOpKind::EqCmp,
                         box left,
                         box right,
-                        ..
+                        position: inner_pos,
                     }),
                 position: pos,
-            }) => ast::Expr::BinOp(ast::BinOp {
+            }) if !matches!(left.get_type(), ast::Type::Float(_)) => ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::NeCmp,
                 left: box left,
                 right: box right,
                 position: pos,
-            }),
-            ast::Expr::BinOp(ast::BinOp {
-                op_kind: ast::BinaryOpKind::And,
-                left:
-                    box ast::Expr::Const(ast::ConstExpr {
-                        value: ast::Const::Bool(b1),
-                        ..
-                    }),
-                right:
-                    box ast::Expr::Const(ast::ConstExpr {
-                        value: ast::Const::Bool(b2),
-                        ..
-                    }),
-                position: pos,
-            }) => ast::Expr::Const(ast::ConstExpr {
-                value: ast::Const::Bool(b1 && b2),
-                position: pos,
-            }),
+            })
+            .set_default_pos(inner_pos),
             ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::And,
                 left:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
                 right: box conjunct,
-                ..
+                position: pos,
             })
             | ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::And,
                 left: box conjunct,
                 right:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
-                ..
-            }) => {
-                if b {
-                    conjunct
-                } else {
-                    false.into()
-                }
+                position: pos,
+            }) => if b {
+                conjunct
+            } else {
+                Into::<ast::Expr>::into(false).set_pos(inner_pos)
             }
+            .set_default_pos(pos),
             ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::Or,
                 left:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
                 right: box disjunct,
-                ..
+                position: pos,
             })
             | ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::Or,
                 left: box disjunct,
                 right:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
-                ..
-            }) => {
-                if b {
-                    true.into()
-                } else {
-                    disjunct
-                }
+                position: pos,
+            }) => if b {
+                Into::<ast::Expr>::into(true).set_pos(inner_pos)
+            } else {
+                disjunct
             }
+            .set_default_pos(pos),
             ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::Implies,
                 left: guard,
                 right:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
                 position: pos,
-            }) => {
-                if b {
-                    true.into()
-                } else {
-                    ast::Expr::UnaryOp(ast::UnaryOp {
-                        op_kind: ast::UnaryOpKind::Not,
-                        argument: guard,
-                        position: pos,
-                    })
-                }
+            }) => if b {
+                Into::<ast::Expr>::into(true).set_pos(pos)
+            } else {
+                ast::Expr::UnaryOp(ast::UnaryOp {
+                    op_kind: ast::UnaryOpKind::Not,
+                    argument: guard,
+                    position: pos,
+                })
             }
+            .set_default_pos(inner_pos),
             ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::Implies,
                 left:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
                 right: box body,
-                ..
-            }) => {
-                if b {
-                    body
-                } else {
-                    true.into()
-                }
+                position: pos,
+            }) => if b {
+                body
+            } else {
+                Into::<ast::Expr>::into(true).set_pos(inner_pos)
             }
+            .set_default_pos(pos),
             ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::And,
                 left: box op1,

prusti-common/src/vir/optimizations/methods/mod.rs

@@ -13,14 +13,15 @@ mod purifier;
 mod quantifier_fixer;
 mod unfolding_fixer;
 mod var_remover;
+mod simplifier;
 
 use super::log_method;
 use crate::{config::Optimizations, vir::polymorphic_vir::cfg::CfgMethod};
 
 use self::{
     assert_remover::remove_trivial_assertions, cfg_cleaner::clean_cfg,
     empty_if_remover::remove_empty_if, purifier::purify_vars, quantifier_fixer::fix_quantifiers,
-    unfolding_fixer::fix_unfoldings, var_remover::remove_unused_vars,
+    simplifier::simplify_exprs, unfolding_fixer::fix_unfoldings, var_remover::remove_unused_vars,
 };
 
 #[allow(clippy::let_and_return)]
@@ -58,6 +59,7 @@ pub fn optimize_method_encoding(
     };
     let cfg = apply!(fix_unfoldings, cfg);
     let cfg = apply!(fix_quantifiers, cfg);
+    let cfg = apply!(simplify_exprs, cfg);
     let cfg = apply!(remove_empty_if, cfg);
     let cfg = apply!(remove_unused_vars, cfg);
     let cfg = apply!(remove_trivial_assertions, cfg);

prusti-common/src/vir/optimizations/methods/simplifier.rs

@@ -0,0 +1,45 @@
+// © 2022, ETH Zurich
+//
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+
+use log::debug;
+use std::mem;
+use vir::polymorphic::*;
+
+use crate::vir::optimizations::functions::Simplifier;
+
+/// This optimization simplifies all expressions in a method.
+/// It is required when resource access predicates appear on the RHS of
+/// implications as implications are transformed into ors which need to be
+/// transformed back into implications otherwise, we would have an impure
+/// expression in ors which is disallowed in Viper.
+
+pub fn simplify_exprs(mut cfg: CfgMethod) -> CfgMethod {
+    debug!("Simplifying exprs in {}", cfg.name());
+    let mut sentinel_stmt = Stmt::comment("moved out stmt");
+    for block in &mut cfg.basic_blocks {
+        for stmt in &mut block.stmts {
+            mem::swap(&mut sentinel_stmt, stmt);
+            sentinel_stmt = sentinel_stmt.simplify();
+            mem::swap(&mut sentinel_stmt, stmt);
+        }
+    }
+    cfg
+}
+
+struct StmtSimplifier;
+
+impl Simplifier for Stmt {
+    fn simplify(self) -> Self {
+        let mut folder = StmtSimplifier;
+        folder.fold(self)
+    }
+}
+
+impl StmtFolder for StmtSimplifier {
+    fn fold_expr(&mut self, expr: Expr) -> Expr {
+        expr.simplify()
+    }
+}

prusti-common/src/vir/to_viper.rs

@@ -750,6 +750,10 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expr {
                     ast.int_to_backend_bv(size, base.to_viper(context, ast))
                 }
             },
+            Expr::Low(expr, position) => {
+                ast.low_with_pos(expr.to_viper(context, ast), position.to_viper(context, ast))
+            }
+            Expr::LowEvent => ast.low_event(),
         };
         if config::simplify_encoding() {
             ast.simplified_expression(expr)
@@ -1055,9 +1059,11 @@ impl<'a, 'v> ToViper<'v, viper::Method<'v>> for &'a CfgMethod {
             // self.convert_basic_block_path(path, ast, &mut blocks_ast, &mut declarations);
         } else {
             // Sort blocks by label, except for the first block
-            let mut blocks: Vec<_> = self.basic_blocks.iter().enumerate().skip(1).collect();
-            blocks.sort_by_key(|(index, _)| index_to_label(self.basic_blocks_labels(), *index));
-            blocks.insert(0, (0, &self.basic_blocks[0]));
+            // let mut blocks: Vec<_> = self.basic_blocks.iter().enumerate().skip(1).collect();
+            // blocks.sort_by_key(|(index, _)| index_to_label(self.basic_blocks_labels(), *index));
+            // blocks.insert(0, (0, &self.basic_blocks[0]));
+
+            let blocks = topologicaly_sort_blocks(&self.basic_blocks);
 
             for (index, block) in blocks.into_iter() {
                 blocks_ast.push(block_to_viper(
@@ -1094,6 +1100,55 @@ impl<'a, 'v> ToViper<'v, viper::Method<'v>> for &'a CfgMethod {
     }
 }
 
+fn topologicaly_sort_blocks(blocks: &[CfgBlock]) -> Vec<(usize, &CfgBlock)> {
+    let mut added_blocks: Vec<bool> = (0..blocks.len()).map(|_| false).collect();
+    let mut traversed_blocks: Vec<bool> = (0..blocks.len()).map(|_| false).collect();
+    let mut res = Vec::new();
+
+    topo_rec(
+        blocks,
+        0,
+        &mut res,
+        &mut added_blocks,
+        &mut traversed_blocks,
+    );
+
+    res.into_iter()
+        .rev()
+        .map(|idx| (idx, &blocks[idx]))
+        .collect()
+}
+
+fn topo_rec(
+    blocks: &[CfgBlock],
+    curr: usize,
+    res: &mut Vec<usize>,
+    added_blocks: &mut [bool],
+    traversed_blocks: &mut [bool],
+) {
+    debug_assert!(!traversed_blocks[curr], "Found a back edge!");
+    if added_blocks[curr] {
+        return;
+    }
+
+    traversed_blocks[curr] = true;
+    match &blocks[curr].successor {
+        Successor::Undefined => unreachable!("Undefined edge!"),
+        Successor::Return => (),
+        Successor::Goto(to) => topo_rec(blocks, to.index(), res, added_blocks, traversed_blocks),
+        Successor::GotoSwitch(tos, default) => {
+            for (_, to) in tos.iter() {
+                topo_rec(blocks, to.index(), res, added_blocks, traversed_blocks);
+            }
+            topo_rec(blocks, default.index(), res, added_blocks, traversed_blocks);
+        }
+    }
+    traversed_blocks[curr] = false;
+
+    res.push(curr);
+    added_blocks[curr] = true;
+}
+
 fn cfg_method_convert_basic_block_path<'v>(
     cfg_method: &CfgMethod,
     mut path: Vec<String>,