Lithium: a Rust-native back end

.gitignore

@@ -10,6 +10,7 @@ callgrind.*
 core
 report.csv
 *.profraw
+.DS_Store
 
 *.lock
 !/Cargo.lock

backend-common/Cargo.toml

@@ -0,0 +1,10 @@
+[package]
+name = "backend-common"
+version = "0.1.0"
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
+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,5 @@
+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,69 @@
+use rustc_hash::FxHashMap;
+
+#[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::{JavaException, SiliconCounterexample};
 
 /// 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 <prusti_developers@sympa.ethz.ch>"]
+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"