Move the native back end to a separate crate

backend-common/Cargo.toml

@@ -6,4 +6,5 @@ edition = "2021"
 
 [dependencies]
 serde = { version = "1.0", features = ["derive"] }
-rustc-hash = "1.1.0"
+rustc-hash = "1.1.0"
+vir = { path = "../vir" }

backend-common/src/lib.rs

@@ -1,5 +1,9 @@
 mod verification_result;
 mod java_exception;
 pub mod silicon_counterexample;
+pub mod verifier;
+pub mod program;
 
-pub use crate::{silicon_counterexample::*, java_exception::*, verification_result::*};
+pub use crate::{
+    java_exception::*, program::*, silicon_counterexample::*, verification_result::*, verifier::*,
+};

prusti-common/src/vir/program.rs → backend-common/src/program.rs

@@ -1,6 +1,3 @@
-use super::low_to_viper::{Context, ToViper};
-use viper::{self, AstFactory};
-
 #[derive(Debug, Clone, serde::Serialize, serde::Deserialize, Hash, Eq, PartialEq)]
 pub enum Program {
     Legacy(vir::legacy::Program),
@@ -31,11 +28,4 @@ impl Program {
     }
 }
 
-impl<'v> ToViper<'v, viper::Program<'v>> for Program {
-    fn to_viper(&self, context: Context, ast: &AstFactory<'v>) -> viper::Program<'v> {
-        match self {
-            Program::Legacy(program) => program.to_viper(context, ast),
-            Program::Low(program) => program.to_viper(context, ast),
-        }
-    }
-}
+

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

@@ -1,17 +1,15 @@
-// © 2019, ETH Zurich
+// © 2023, Jakub Janaszkiewicz, DTU
 //
 // 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 backend_common::VerificationResult;
+use crate::{Program, VerificationResult};
 
 pub trait Verifier<'a> {
     fn parse_command_line(&mut self, args: &[String]);
 
     fn start(&mut self);
 
-    fn verify(&mut self, program: crate::Program) -> VerificationResult;
-
-    fn verify_vir(&mut self, program: &vir::low::Program) -> VerificationResult;
+    fn verify_vir(&mut self, program: &Program) -> VerificationResult;
 }

native-verifier/Cargo.toml

@@ -0,0 +1,19 @@
+[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"
+vir = { path = "../vir" }
+uuid = { version = "1.0", features = ["v4"] }
+serde = { version = "1.0", features = ["derive"] }
+prusti-utils = { path = "../prusti-utils" }
+lazy_static = "1.4"
+regex = "1.7.1"
+backend-common = { path = "../backend-common" }

native-verifier/src/lib.rs

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

native-verifier/src/main.rs

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

viper/src/native_backend/native_verifier.rs → native-verifier/src/native_verifier.rs

@@ -4,16 +4,16 @@
 // 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::{native_backend::smt_lib::*, verifier::Verifier};
-use backend_common::{VerificationError, VerificationResult};
+use crate::smt_lib::*;
+use backend_common::{verifier::Verifier, Program, VerificationError, VerificationResult};
+use core::panic;
 use log::{self, debug, info, warn};
-use prusti_utils::report::log::report_with_writer;
+use prusti_utils::{report::log::report_with_writer, run_timed};
 use std::{
     error::Error,
     io::Write,
     process::{Command, Stdio},
 };
-use vir::low::Program;
 
 pub struct NativeVerifier {
     z3_exe: String,
@@ -34,14 +34,10 @@ impl<'a> Verifier<'a> for NativeVerifier {
         // TODO: Start the verifier
     }
 
-    fn verify(&mut self, _program: crate::Program) -> VerificationResult {
-        panic!("Viper verification not supported by Lithium");
-    }
-
     fn verify_vir(&mut self, program: &Program) -> VerificationResult {
-        // info!("Program AST to be verified:\n{}", program);
-
-        // TODO: Consistency checks?
+        let Program::Low(program) = program else {
+            panic!("Lithium backend only supports low programs");
+        };
 
         run_timed!("Translation to SMT-LIB", debug,
             let mut smt = SMTLib::new();

prusti-common/src/vir/mod.rs

@@ -4,18 +4,11 @@
 // 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/.
 
-pub use self::{
-    low_to_viper::{ToViper, ToViperDecl},
-    to_graphviz::ToGraphViz,
-};
-pub use low_to_viper::Context as LoweringContext;
+pub use self::to_graphviz::ToGraphViz;
 pub use vir::{high as vir_high, legacy::*, polymorphic as polymorphic_vir};
 
 pub mod fixes;
 pub mod optimizations;
-mod to_viper;
-mod low_to_viper;
 mod to_graphviz;
-pub mod program;
 pub mod macros;
 pub mod program_normalization;

prusti-common/src/vir/program_normalization.rs

@@ -4,10 +4,10 @@
 // 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::vir::{program::Program, Position};
+use crate::vir::Position;
+use backend_common::VerificationResult;
 use log::{debug, trace};
 use rustc_hash::{FxHashMap, FxHashSet};
-use backend_common::VerificationResult;
 
 pub enum NormalizationInfo {
     LegacyProgram { original_position_ids: Vec<u64> },
@@ -16,13 +16,13 @@ pub enum NormalizationInfo {
 
 impl NormalizationInfo {
     /// Normalize a vir::legacy program. Do nothing for vir::low programs.
-    pub fn normalize_program(program: &mut Program) -> Self {
+    pub fn normalize_program(program: &mut backend_common::Program) -> Self {
         match program {
-            Program::Low(_) => {
+            backend_common::Program::Low(_) => {
                 debug!("No normalization is done for vir::low programs.");
                 NormalizationInfo::LowProgram
             }
-            Program::Legacy(legacy_program) => {
+            backend_common::Program::Legacy(legacy_program) => {
                 // Collect positions
                 let mut position_ids: FxHashSet<u64> = FxHashSet::default();
                 position_ids.insert(Position::default().id()); // Generated by the to_viper pass
@@ -81,10 +81,12 @@ impl NormalizationInfo {
     }
 
     /// Denormalize the verification result.
-    pub fn denormalize_program(&self, program: &mut Program) {
+    pub fn denormalize_program(&self, program: &mut backend_common::Program) {
         match program {
-            Program::Low(_) => debug!("No denormalization is done for vir::low programs."),
-            Program::Legacy(legacy_program) => {
+            backend_common::Program::Low(_) => {
+                debug!("No denormalization is done for vir::low programs.")
+            }
+            backend_common::Program::Legacy(legacy_program) => {
                 legacy_program.visit_expressions_mut(|e| {
                     e.visit_positions_mut(|p| *p = self.denormalize_position(*p))
                 });

prusti-server/Cargo.toml

@@ -7,7 +7,7 @@ license = "MPL-2.0"
 description = "Server-side logic & handling for Prusti"
 
 [lib]
-test = true # we have unit tests
+test = true     # we have unit tests
 doctest = false # but no doc tests
 
 [[bin]]
@@ -27,11 +27,15 @@ bincode = "1.0"
 url = "2.2.2"
 num_cpus = "1.14"
 serde = { version = "1.0", features = ["derive"] }
-reqwest = { version = "0.11", default-features = false, features = ["json", "rustls-tls"] }
+reqwest = { version = "0.11", default-features = false, features = [
+    "json",
+    "rustls-tls",
+] }
 warp = "0.3"
 tokio = "1.20"
 rustc-hash = "1.1.0"
 backend-common = { path = "../backend-common" }
+native-verifier = { path = "../native-verifier" }
 
 [dev-dependencies]
 lazy_static = "1.4.0"

prusti-server/src/process_verification.rs

@@ -5,18 +5,18 @@
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 use crate::{VerificationRequest, ViperBackendConfig};
-use backend_common::VerificationResult;
+use backend_common::{VerificationResult, Verifier};
 use log::info;
+use native_verifier::NativeVerifier;
 use prusti_common::{
     config,
     report::log::{report, to_legal_file_name},
-    vir::{program_normalization::NormalizationInfo, ToViper},
+    vir::program_normalization::NormalizationInfo,
     Stopwatch,
 };
-use std::{fs::create_dir_all, path::PathBuf};
+use std::{env, fs::create_dir_all, path::PathBuf};
 use viper::{
-    native_backend::native_verifier::NativeVerifier, smt_manager::SmtManager, Cache,
-    VerificationBackend, VerificationContext, Verifier,
+    low_to_viper::ToViper, smt_manager::SmtManager, Cache, VerificationBackend, VerificationContext,
 };
 
 pub fn process_native_verification_request(
@@ -75,13 +75,8 @@ pub fn process_native_verification_request(
     let mut stopwatch = Stopwatch::start("prusti-server", "verifier startup");
     let mut verifier: Box<dyn Verifier> = Box::new(NativeVerifier::new(config::smt_solver_path()));
 
-    let mut result =
-        if let prusti_common::vir::program::Program::Low(ref low_program) = request.program {
-            stopwatch.start_next("verification");
-            verifier.verify_vir(low_program)
-        } else {
-            panic!("Lithium backend can only verify vir::low programs");
-        };
+    stopwatch.start_next("verification");
+    let mut result = verifier.verify_vir(&request.program);
 
     // Cache results
     if config::enable_cache() {
@@ -129,7 +124,7 @@ pub fn process_verification_request<'v, 't: 'v>(
         let ast_factory = verification_context.new_ast_factory();
         let viper_program = request
             .program
-            .to_viper(prusti_common::vir::LoweringContext::default(), &ast_factory);
+            .to_viper(viper::low_to_viper::Context::default(), &ast_factory);
 
         if config::dump_viper_program() {
             stopwatch.start_next("dumping viper program");
@@ -178,27 +173,16 @@ pub fn process_verification_request<'v, 't: 'v>(
     };
 
     ast_utils.with_local_frame(16, || {
-        let viper_program = build_or_dump_viper_program();
         let program_name = request.program.get_name();
 
         // Create a new verifier each time.
         // Workaround for https://github.com/viperproject/prusti-dev/issues/744
         let mut stopwatch = Stopwatch::start("prusti-server", "verifier startup");
-        let backend = request.backend_config.backend;
         let mut verifier =
             new_viper_verifier(program_name, verification_context, request.backend_config);
 
         stopwatch.start_next("verification");
-        let mut result = if let VerificationBackend::Lithium = backend {
-            if let prusti_common::vir::program::Program::Low(ref low_program) = request.program {
-                stopwatch.start_next("verification");
-                verifier.verify_vir(low_program)
-            } else {
-                panic!("Lithium backend can only verify vir::low programs");
-            }
-        } else {
-            verifier.verify(viper_program)
-        };
+        let mut result = verifier.verify_vir(&request.program);
 
         // Don't cache Java exceptions, which might be due to misconfigured paths.
         if config::enable_cache() && !matches!(result, VerificationResult::JavaException(_)) {
@@ -226,7 +210,7 @@ fn new_viper_verifier<'v, 't: 'v>(
     program_name: &str,
     verification_context: &'v viper::VerificationContext<'t>,
     backend_config: ViperBackendConfig,
-) -> Box<dyn viper::Verifier<'v> + 'v> {
+) -> Box<dyn Verifier<'v> + 'v> {
     let mut verifier_args: Vec<String> = backend_config.verifier_args;
     let report_path: Option<PathBuf>;
     if config::dump_debug_info() {
@@ -292,12 +276,18 @@ fn new_viper_verifier<'v, 't: 'v>(
         std::env::set_var("PRUSTI_SMT_QI_BOUND_GLOBAL", bound.to_string());
     }
 
-    verification_context.new_verifier(
-        backend_config.backend,
-        verifier_args,
-        report_path,
-        smt_solver,
-        boogie_path,
-        smt_manager,
-    )
+    if let VerificationBackend::Lithium = backend_config.backend {
+        let z3_exe =
+            env::var("Z3_EXE").expect("the Z3_EXE environment variable should not be empty");
+        Box::new(NativeVerifier::new(z3_exe))
+    } else {
+        Box::new(verification_context.new_verifier(
+            backend_config.backend,
+            verifier_args,
+            report_path,
+            smt_solver,
+            boogie_path,
+            smt_manager,
+        ))
+    }
 }

prusti-server/src/verification_request.rs

@@ -4,14 +4,14 @@
 // 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 prusti_common::{config, vir::program::Program};
+use prusti_common::{config};
 use rustc_hash::FxHasher;
 use std::hash::{Hash, Hasher};
 use viper::{self, VerificationBackend};
 
 #[derive(Debug, Clone, serde::Serialize, serde::Deserialize, Hash)]
 pub struct VerificationRequest {
-    pub program: Program,
+    pub program: backend_common::Program,
     pub backend_config: ViperBackendConfig,
 }