Address change request

viperproject · Feb 24, 2023 · 87a11c9 · 87a11c9
1 parent d30ad20
commit 87a11c9
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 6 deletions.
diff --git a/prusti-server/src/backend.rs b/prusti-server/src/backend.rs
@@ -1,4 +1,6 @@
+use crate::dump_viper_program;
 use prusti_common::{
+    config,
     vir::{LoweringContext, ToViper},
     Stopwatch,
 };
@@ -12,13 +14,24 @@ 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 mut stopwatch =
+                    Stopwatch::start("prusti-server backend", "construction of JVM objects");
 
-                let ast_factory = context.new_ast_factory();
-                let viper_program = program.to_viper(LoweringContext::default(), &ast_factory);
+                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(),
+                        );
+                    }
 
-                context.new_ast_utils().with_local_frame(16, || {
-                    stopwatch.start_next("verification");
                     viper.verify(viper_program)
                 })
             }

diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs
@@ -98,6 +98,8 @@ pub fn process_verification_request<'v, 't: 'v>(
         }
     };
 
+    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 {
@@ -111,6 +113,7 @@ pub fn process_verification_request<'v, 't: 'v>(
         ),
     };
 
+    stopwatch.start_next("verification");
     let mut result = backend.verify(&request.program);
 
     // Don't cache Java exceptions, which might be due to misconfigured paths.
@@ -127,7 +130,11 @@ pub fn process_verification_request<'v, 't: 'v>(
     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);