Add Lithium back end

backend-common/Cargo.toml

@@ -0,0 +1,10 @@
+[package]
+name = "backend-common"
+version = "0.1.0"
+authors = ["Prusti Devs <[email protected]>"]
+edition = "2021"
+
+[dependencies]
+serde = { version = "1.0", features = ["derive"] }
+rustc-hash = "1.1.0"
+vir = { path = "../vir" }

backend-common/src/lib.rs

@@ -0,0 +1,7 @@
+mod verification_result;
+mod java_exception;
+mod silicon_counterexample;
+
+pub use crate::{
+    java_exception::*, silicon_counterexample::*, verification_result::*,
+};

backend-common/src/silicon_counterexample.rs

@@ -0,0 +1,70 @@
+use rustc_hash::FxHashMap;
+use serde;
+
+#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
+pub struct SiliconCounterexample {
+    //pub heap: Heap,
+    //pub old_heaps: FxHashMap<String, Heap>,
+    pub model: Model,
+    pub functions: Functions,
+    pub domains: Domains,
+    pub old_models: FxHashMap<String, Model>,
+    // label_order because HashMaps do not guarantee order of elements
+    // whereas the Map used in scala does guarantee it
+    pub label_order: Vec<String>,
+}
+
+// Model Definitions
+#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
+pub struct Model {
+    pub entries: FxHashMap<String, ModelEntry>,
+}
+
+#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
+pub enum ModelEntry {
+    LitInt(String),
+    LitFloat(String),
+    LitBool(bool),
+    LitPerm(String),
+    Ref(String, FxHashMap<String, ModelEntry>),
+    NullRef(String),
+    RecursiveRef(String),
+    Var(String),
+    Seq(String, Vec<ModelEntry>),
+    Other(String, String),
+    DomainValue(String, String),
+    UnprocessedModel, //used for Silicon's Snap type
+}
+
+#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
+pub struct Functions {
+    pub entries: FxHashMap<String, FunctionEntry>,
+}
+
+#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
+pub struct FunctionEntry {
+    pub options: Vec<(Vec<Option<ModelEntry>>, Option<ModelEntry>)>,
+    pub default: Option<ModelEntry>,
+}
+
+#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
+pub struct Domains {
+    pub entries: FxHashMap<String, DomainEntry>,
+}
+
+#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
+pub struct DomainEntry {
+    pub functions: Functions,
+}
+
+impl FunctionEntry {
+    /// Given a vec of params it finds the correct entry in a function.
+    pub fn get_function_value(&self, params: &Vec<Option<ModelEntry>>) -> &Option<ModelEntry> {
+        for option in &self.options {
+            if &option.0 == params {
+                return &option.1;
+            }
+        }
+        &None
+    }
+}

viper/src/verification_result.rs → backend-common/src/verification_result.rs

@@ -4,7 +4,7 @@
 // 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 crate::{silicon_counterexample::SiliconCounterexample, JavaException};
+use crate::{SiliconCounterexample, JavaException};
 
 /// The result of a verification request on a Viper program.
 #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
@@ -57,21 +57,3 @@ impl VerificationError {
         }
     }
 }
-
-/// The consistency error reported by the verifier.
-#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
-pub struct ConsistencyError {
-    /// To which method corresponds the program that triggered the error.
-    pub method: String,
-    /// The actual error.
-    pub error: String,
-}
-
-/// The Java exception reported by the verifier.
-#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
-pub struct JavaExceptionWithOrigin {
-    /// To which method corresponds the program that triggered the exception.
-    pub method: String,
-    /// The actual exception.
-    pub exception: JavaException,
-}

native-verifier/Cargo.toml

@@ -0,0 +1,20 @@
+[package]
+name = "native-verifier"
+version = "0.1.0"
+authors = ["Prusti Devs <[email protected]>"]
+edition = "2021"
+readme = "README.md"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+log = { version = "0.4", features = ["release_max_level_info"] }
+error-chain = "0.12"
+uuid = { version = "1.0", features = ["v4"] }
+serde = { version = "1.0", features = ["derive"] }
+prusti-common = { path = "../prusti-common" }
+backend-common = { path = "../backend-common" }
+prusti-utils = { path = "../prusti-utils" }
+vir = { path = "../vir" }
+lazy_static = "1.4"
+regex = "1.7.1"

native-verifier/src/fol.rs

@@ -0,0 +1,141 @@
+use std::collections::HashMap;
+use vir::low::{
+    ast::{expression::*, statement::*},
+    *,
+};
+
+pub enum FolStatement {
+    Comment(String),
+    Assume(Expression),
+    Assert(Expression),
+}
+
+fn vir_statement_to_fol_statements(
+    statement: &Statement,
+    known_methods: &HashMap<String, MethodDecl>,
+) -> Vec<FolStatement> {
+    match statement {
+        Statement::Assert(expr) => vec![FolStatement::Assert(expr.expression.clone())],
+        Statement::Assume(expr) => vec![FolStatement::Assume(expr.expression.clone())],
+        Statement::Inhale(expr) => vec![FolStatement::Assume(expr.expression.clone())],
+        Statement::Exhale(expr) => vec![FolStatement::Assert(expr.expression.clone())],
+        Statement::Assign(assign) => {
+            let eq = Expression::BinaryOp(BinaryOp {
+                op_kind: BinaryOpKind::EqCmp,
+                left: Box::new(Expression::Local(Local {
+                    variable: assign.target.clone(),
+                    position: assign.position,
+                })),
+                right: Box::new(assign.value.clone()),
+                position: assign.position,
+            });
+
+            vec![FolStatement::Assume(eq)]
+        }
+        Statement::MethodCall(method_call) => {
+            let method_decl = known_methods
+                .get(&method_call.method_name)
+                .expect("Method not found");
+
+            let mut params_to_args = method_decl
+                .parameters
+                .iter()
+                .zip(method_call.arguments.iter())
+                .map(|(target, arg)| (target.clone(), arg.clone()))
+                .collect::<HashMap<_, _>>();
+
+            let returns_to_targets = method_decl
+                .targets
+                .iter()
+                .zip(method_call.targets.iter())
+                .map(|(target, arg)| (target.clone(), arg.clone()))
+                .collect::<HashMap<_, _>>();
+
+            params_to_args.extend(returns_to_targets);
+
+            fn substitute(
+                expr: &Expression,
+                mapping: &HashMap<VariableDecl, Expression>,
+            ) -> Expression {
+                match expr {
+                    Expression::Local(local) => {
+                        if let Some(arg) = mapping.get(&local.variable) {
+                            arg.clone()
+                        } else {
+                            Expression::Local(local.clone())
+                        }
+                    }
+                    Expression::BinaryOp(op) => Expression::BinaryOp(BinaryOp {
+                        op_kind: op.op_kind,
+                        left: Box::new(substitute(&op.left, mapping)),
+                        right: Box::new(substitute(&op.right, mapping)),
+                        position: op.position,
+                    }),
+                    Expression::UnaryOp(op) => Expression::UnaryOp(UnaryOp {
+                        op_kind: op.op_kind.clone(), // TODO: Copy trait derivation
+                        argument: Box::new(substitute(&op.argument, mapping)),
+                        position: op.position,
+                    }),
+                    Expression::ContainerOp(op) => Expression::ContainerOp(ContainerOp {
+                        kind: op.kind.clone(), // TODO: Copy trait derivation
+                        container_type: op.container_type.clone(),
+                        operands: op
+                            .operands
+                            .iter()
+                            .map(|arg| substitute(arg, mapping))
+                            .collect(),
+                        position: op.position,
+                    }),
+                    Expression::Constant(constant) => Expression::Constant(constant.clone()),
+                    Expression::DomainFuncApp(func) => Expression::DomainFuncApp(DomainFuncApp {
+                        domain_name: func.domain_name.clone(),
+                        function_name: func.function_name.clone(),
+                        arguments: func
+                            .arguments
+                            .iter()
+                            .map(|arg| substitute(arg, mapping))
+                            .collect(),
+                        parameters: func.parameters.clone(),
+                        return_type: func.return_type.clone(),
+                        position: func.position,
+                    }),
+                    Expression::MagicWand(magic_wand) => Expression::MagicWand(MagicWand {
+                        left: Box::new(substitute(&magic_wand.left, mapping)),
+                        right: Box::new(substitute(&magic_wand.right, mapping)),
+                        position: magic_wand.position,
+                    }),
+                    _ => unimplemented!("substitute not implemented for {:?}", expr),
+                }
+            }
+
+            let preconds = method_decl.pres.iter().map(|pre| {
+                // substitute parameters for arguments
+                FolStatement::Assert(substitute(pre, &params_to_args))
+            });
+
+            let postconds = method_decl.posts.iter().map(|post| {
+                // substitute parameters for arguments
+                FolStatement::Assume(substitute(post, &params_to_args))
+            });
+
+            preconds.chain(postconds).collect::<Vec<_>>()
+        }
+        Statement::Comment(comment) => vec![FolStatement::Comment(comment.comment.clone())],
+        Statement::LogEvent(_) => vec![], // TODO: Embed in SMT-LIB code
+        _ => {
+            log::warn!("Statement {:?} not yet supported", statement);
+            vec![]
+        }
+    }
+}
+
+pub fn vir_to_fol(
+    statements: &Vec<Statement>,
+    known_methods: &HashMap<String, MethodDecl>,
+) -> Vec<FolStatement> {
+    // reduce so that the order in the vector is now the Sequence operator
+    statements
+        .iter()
+        .flat_map(|s| vir_statement_to_fol_statements(s, known_methods))
+        .collect()
+}

native-verifier/src/lib.rs

@@ -0,0 +1,9 @@
+#![feature(try_blocks)]
+#![feature(let_chains)]
+
+pub mod verifier;
+mod smt_lib;
+mod theory_provider;
+mod fol;
+
+pub use crate::verifier::*;

native-verifier/src/main.rs

@@ -0,0 +1,3 @@
+fn main() {
+    unimplemented!("This is a dummy main function.");
+}