diff --git a/prusti-server/src/backend.rs b/prusti-server/src/backend.rs index 131536ac92c..37c9a91f0db 100644 --- 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 index c8f3c9076e4..0a6ccbeb658 100644 --- 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);