Refactoring to allow for new verification back ends (#1329)

* Add Backend enum * Use the new Backend enum in prusti-server * Make clippy happy * Initialize Viper lazily * Update prusti-server/src/backend.rs Co-authored-by: Federico Poli <[email protected]> * Address change request * Clarify log message * Fix measurement of verification time --------- Co-authored-by: Federico Poli <[email protected]>
viperproject · Feb 27, 2023 · e4896c0 · e4896c0
1 parent 1c0d379
commit e4896c0
Show file tree

Hide file tree

Showing 8 changed files with 165 additions and 96 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/prusti-server/Cargo.toml b/prusti-server/Cargo.toml
@@ -31,6 +31,7 @@ reqwest = { version = "0.11", default-features = false, features = ["json", "rus
 warp = "0.3"
 tokio = "1.20"
 rustc-hash = "1.1.0"
+once_cell = "1.17.1"
 
 [dev-dependencies]
 lazy_static = "1.4.0"
diff --git a/prusti-server/src/backend.rs b/prusti-server/src/backend.rs
@@ -0,0 +1,41 @@
+use crate::dump_viper_program;
+use prusti_common::{
+    config,
+    vir::{LoweringContext, ToViper},
+    Stopwatch,
+};
+use viper::{VerificationContext, VerificationResult};
+
+pub enum Backend<'a> {
+    Viper(viper::Verifier<'a>, &'a VerificationContext<'a>),
+}
+
+impl<'a> Backend<'a> {
+    pub fn verify(&mut self, program: &prusti_common::vir::program::Program) -> VerificationResult {
+        match self {
+            Backend::Viper(viper, context) => {
+                let mut stopwatch =
+                    Stopwatch::start("prusti-server backend", "construction of JVM objects");
+
+                let ast_utils = context.new_ast_utils();
+
+                ast_utils.with_local_frame(16, || {
+                    let ast_factory = context.new_ast_factory();
+                    let viper_program = program.to_viper(LoweringContext::default(), &ast_factory);
+
+                    if config::dump_viper_program() {
+                        stopwatch.start_next("dumping viper program");
+                        dump_viper_program(
+                            &ast_utils,
+                            viper_program,
+                            &program.get_name_with_check_mode(),
+                        );
+                    }
+
+                    stopwatch.start_next("viper verification");
+                    viper.verify(viper_program)
+                })
+            }
+        }
+    }
+}
diff --git a/prusti-server/src/lib.rs b/prusti-server/src/lib.rs
@@ -10,7 +10,9 @@ mod client;
 mod process_verification;
 mod server;
 mod verification_request;
+mod backend;
 
+pub use backend::*;
 pub use client::*;
 pub use process_verification::*;
 pub use server::*;

diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs
@@ -4,8 +4,9 @@
 // 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::{VerificationRequest, ViperBackendConfig};
+use crate::{Backend, VerificationRequest, ViperBackendConfig};
 use log::info;
+use once_cell::sync::Lazy;
 use prusti_common::{
     config,
     report::log::{report, to_legal_file_name},
@@ -18,7 +19,7 @@ use viper::{
 };
 
 pub fn process_verification_request<'v, 't: 'v>(
-    verification_context: &'v VerificationContext<'t>,
+    verification_context: &'v Lazy<VerificationContext<'t>, impl Fn() -> VerificationContext<'t>>,
     mut request: VerificationRequest,
     cache: impl Cache,
 ) -> viper::VerificationResult {
@@ -97,35 +98,43 @@ 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 mut verifier =
-            new_viper_verifier(program_name, verification_context, request.backend_config);
+    let mut stopwatch = Stopwatch::start("prusti-server", "verifier startup");
+
+    // Create a new verifier each time.
+    // Workaround for https://github.com/viperproject/prusti-dev/issues/744
+    let mut backend = match request.backend_config.backend {
+        VerificationBackend::Carbon | VerificationBackend::Silicon => Backend::Viper(
+            new_viper_verifier(
+                request.program.get_name(),
+                verification_context,
+                request.backend_config,
+            ),
+            verification_context,
+        ),
+    };
 
-        stopwatch.start_next("verification");
-        let mut result = verifier.verify(viper_program);
+    stopwatch.start_next("backend verification");
+    let mut result = backend.verify(&request.program);
 
-        // Don't cache Java exceptions, which might be due to misconfigured paths.
-        if config::enable_cache() && !matches!(result, VerificationResult::JavaException(_)) {
-            info!(
-                "Storing new cached result {:?} for program {}",
-                &result,
-                request.program.get_name()
-            );
-            cache.insert(hash, result.clone());
-        }
+    // Don't cache Java exceptions, which might be due to misconfigured paths.
+    if config::enable_cache() && !matches!(result, VerificationResult::JavaException(_)) {
+        info!(
+            "Storing new cached result {:?} for program {}",
+            &result,
+            request.program.get_name()
+        );
+        cache.insert(hash, result.clone());
+    }
 
-        normalization_info.denormalize_result(&mut result);
-        result
-    })
+    normalization_info.denormalize_result(&mut result);
+    result
 }
 
-fn dump_viper_program(ast_utils: &viper::AstUtils, program: viper::Program, program_name: &str) {
+pub fn dump_viper_program(
+    ast_utils: &viper::AstUtils,
+    program: viper::Program,
+    program_name: &str,
+) {
     let namespace = "viper_program";
     let filename = format!("{program_name}.vpr");
     info!("Dumping Viper program to '{}/{}'", namespace, filename);

diff --git a/prusti-server/src/server.rs b/prusti-server/src/server.rs
@@ -6,6 +6,7 @@
 
 use crate::{process_verification_request, VerificationRequest};
 use log::info;
+use once_cell::sync::Lazy;
 use prusti_common::{config, Stopwatch};
 use std::{
     net::{Ipv4Addr, SocketAddr},
@@ -46,18 +47,18 @@ where
     F: FnOnce(SocketAddr),
 {
     let stopwatch = Stopwatch::start("prusti-server", "JVM startup");
-    let viper = Arc::new(Viper::new_with_args(
-        &config::viper_home(),
-        config::extra_jvm_args(),
-    ));
+    let viper = Arc::new(Lazy::new(|| {
+        Viper::new_with_args(&config::viper_home(), config::extra_jvm_args())
+    }));
+
     stopwatch.finish();
 
     let cache_data = PersistentCache::load_cache(config::cache_path());
     let cache = Arc::new(Mutex::new(cache_data));
-    let build_verification_request_handler = |viper_arc: Arc<Viper>, cache| {
+    let build_verification_request_handler = |viper_arc: Arc<Lazy<Viper, _>>, cache| {
         move |request: VerificationRequest| {
             let stopwatch = Stopwatch::start("prusti-server", "attach thread to JVM");
-            let viper_thread = viper_arc.attach_current_thread();
+            let viper_thread = Lazy::new(|| viper_arc.attach_current_thread());
             stopwatch.finish();
             process_verification_request(&viper_thread, request, &cache)
         }

diff --git a/prusti-viper/Cargo.toml b/prusti-viper/Cargo.toml
@@ -26,6 +26,7 @@ backtrace = "0.3"
 rustc-hash = "1.1.0"
 derive_more = "0.99.16"
 itertools = "0.10.3"
+once_cell = "1.17.1"
 
 [dev-dependencies]
 lazy_static = "1.4"