Refactor VerificationService

Author: fpoli

prusti-common/src/verification_service.rs

@@ -5,13 +5,12 @@ use viper::{self, VerificationBackend};
 use crate::vir::Program;
 
 pub trait VerificationService {
-    fn verify(&self, request: VerificationRequest) -> viper::ProgramVerificationResult;
+    fn verify(&self, request: VerificationRequest) -> viper::VerificationResult;
 }
 
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct VerificationRequest {
-    pub programs: Vec<Program>,
-    pub program_name: String,
+    pub program: Program,
     pub backend_config: ViperBackendConfig,
 }
 

prusti-server/src/driver.rs

@@ -15,9 +15,7 @@ use clap::{App, Arg};
 use prusti_server::ServerSideService;
 
 fn main() {
-    env_logger::init_from_env(
-        env_logger::Env::new().filter_or("RUST_LOG", "info"), // seems to be the cleanest way to set an overridable default for this
-    );
+    env_logger::init_from_env(env_logger::Env::new().filter_or("PRUSTI_LOG", "info"));
 
     let matches = App::new("Prusti Server")
         .arg(

prusti-server/src/lib.rs

@@ -32,11 +32,11 @@ use std::{
 };
 pub use verifier_runner::*;
 use verifier_thread::*;
-use viper::ProgramVerificationResult;
+use viper::VerificationResult;
 
 #[derive(Debug, Serialize, Deserialize)]
 pub struct VerifierPanicked;
-pub type RemoteVerificationResult = Result<ProgramVerificationResult, VerifierPanicked>;
+pub type RemoteVerificationResult = Result<VerificationResult, VerifierPanicked>;
 
 pub struct PrustiServer {
     verifier_builder: Arc<VerifierBuilder>,
@@ -75,10 +75,8 @@ impl PrustiServer {
             )
         });
 
-        match thread
-            .verify(request.programs, request.program_name.clone())
-            .wait()
-        {
+        let program_name = request.program.name.clone();
+        match thread.verify(request.program).wait() {
             Ok(result) => {
                 // put back the thread for later reuse
                 let mut threads = self.threads.write().unwrap();
@@ -92,8 +90,8 @@ impl PrustiServer {
             Err(_) => {
                 // canceled—the verifier thread panicked
                 error!(
-                    "Panic while handling verification request {}",
-                    request.program_name
+                    "Panic while handling verification request for {}",
+                    program_name
                 );
                 Err(VerifierPanicked)
             }

prusti-server/src/service.rs

@@ -17,7 +17,7 @@ use std::{
     thread,
 };
 use tokio;
-use viper::ProgramVerificationResult;
+use viper::VerificationResult;
 use warp::{self, Buf, Filter};
 
 #[derive(Clone)]
@@ -34,14 +34,11 @@ impl Default for ServerSideService {
 
 impl ServerSideService {
     pub fn new() -> Self {
-        // FIXME: since viper seems to dislike using verifiers in parallel, this is what we're doing to ensure correctness for now.
-        // Eventually, we should lock only specific parts, instantiate multiple JVMs, or even address the root cause.
-        let _max_concurrency = config::server_max_concurrency().unwrap_or_else(num_cpus::get);
-        let max_concurrency = 1;
+        let max_concurrency = config::server_max_concurrency().unwrap_or_else(num_cpus::get);
 
         let cache_size = config::server_max_stored_verifiers().unwrap_or(max_concurrency);
         if cache_size < max_concurrency {
-            warn!("PRUSTI_SERVER_MAX_STORED_VERIFIERS is lower than PRUSTI_SERVER_MAX_CONCURRENCY—you probably don't want to do this, since it means the server will likely have to keep creating new verifiers, reducing the performance gained from reuse.");
+            warn!("PRUSTI_SERVER_MAX_STORED_VERIFIERS is lower than PRUSTI_SERVER_MAX_CONCURRENCY. You probably don't want to do this, since it means the server will likely have to keep creating new verifiers, reducing the performance gained from reuse.");
         }
 
         Self {
@@ -130,7 +127,7 @@ impl ServerSideService {
     }
 
     fn verify(&self, request: VerificationRequest) -> RemoteVerificationResult {
-        info!("Handling verification request for {}", request.program_name);
+        info!("Handling verification request for {}", request.program.name);
         self.server.run_verifier(request)
     }
 }
@@ -179,7 +176,7 @@ impl PrustiServerConnection {
 
 impl VerificationService for PrustiServerConnection {
     /// panics if the verification request fails
-    fn verify(&self, request: VerificationRequest) -> ProgramVerificationResult {
+    fn verify(&self, request: VerificationRequest) -> VerificationResult {
         self.verify_checked(request)
             .expect("Verification request to server failed!")
             .expect("Server panicked while processing request!")

prusti-server/src/verifier_runner.rs

@@ -12,9 +12,6 @@ use prusti_common::{
     vir::{Program, ToViper},
     Stopwatch,
 };
-use viper::{
-    self, ConsistencyError, JavaExceptionWithOrigin, ProgramVerificationResult, VerificationResult,
-};
 
 pub struct VerifierRunner<'v> {
     verifier: viper::Verifier<'v, viper::state::Started>,
@@ -57,43 +54,20 @@ impl<'v> VerifierRunner<'v> {
         }
     }
 
-    pub fn verify(&self, programs: Vec<Program>, program_name: &str) -> ProgramVerificationResult {
-        let mut results = ProgramVerificationResult::default();
-        for program in programs {
-            let mut stopwatch = Stopwatch::start("prusti-server", "construction of JVM objects");
-            let viper_program = program.to_viper(&self.ast_factory);
-            if config::dump_viper_program() {
-                stopwatch.start_next("dumping viper program");
-                self.dump(viper_program, program_name, &program.name);
-            }
-            stopwatch.start_next("verification");
-            match self.verifier.verify(viper_program) {
-                VerificationResult::Success => {}
-                VerificationResult::Failure(errors) => {
-                    results.verification_errors.extend(errors);
-                }
-                VerificationResult::ConsistencyErrors(errors) => {
-                    results
-                        .consistency_errors
-                        .extend(errors.into_iter().map(|error| ConsistencyError {
-                            method: program.name.clone(),
-                            error,
-                        }));
-                }
-                VerificationResult::JavaException(exception) => {
-                    results.java_exceptions.push(JavaExceptionWithOrigin {
-                        method: program.name.clone(),
-                        exception,
-                    });
-                }
-            }
+    pub fn verify(&self, program: Program) -> viper::VerificationResult {
+        let mut stopwatch = Stopwatch::start("prusti-server", "construction of JVM objects");
+        let viper_program = program.to_viper(&self.ast_factory);
+        if config::dump_viper_program() {
+            stopwatch.start_next("dumping viper program");
+            self.dump(viper_program, &program.name);
         }
-        results
+        stopwatch.start_next("verification");
+        self.verifier.verify(viper_program)
     }
 
-    fn dump(&self, program: viper::Program, program_name: &str, method_name: &str) {
+    fn dump(&self, program: viper::Program, program_name: &str) {
         let namespace = "viper_program";
-        let filename = format!("{}-{}.vpr", program_name, method_name);
+        let filename = format!("{}.vpr", program_name);
         info!("Dumping Viper program to '{}/{}'", namespace, filename);
         log::report(namespace, filename, self.ast_utils.pretty_print(program));
     }

prusti-server/src/verifier_thread.rs

@@ -13,25 +13,23 @@ use std::{
     sync::{mpsc, Arc, Mutex},
     thread,
 };
-use viper::ProgramVerificationResult;
+use viper::VerificationResult;
 
-pub type FutVerificationResult =
-    Box<dyn Future<Item = ProgramVerificationResult, Error = Canceled>>;
+pub type FutVerificationResult = Box<dyn Future<Item = VerificationResult, Error = Canceled>>;
 
-struct VerificationRequest {
-    pub programs: Vec<Program>,
-    pub program_name: String,
-    pub sender: oneshot::Sender<ProgramVerificationResult>,
+struct SenderVerificationRequest {
+    pub program: Program,
+    pub sender: oneshot::Sender<VerificationResult>,
 }
 
 pub struct VerifierThread {
     pub backend_config: ViperBackendConfig,
-    request_sender: Mutex<mpsc::Sender<VerificationRequest>>,
+    request_sender: Mutex<mpsc::Sender<SenderVerificationRequest>>,
 }
 
 impl VerifierThread {
     pub fn new(verifier_builder: Arc<VerifierBuilder>, backend_config: ViperBackendConfig) -> Self {
-        let (request_sender, request_receiver) = mpsc::channel::<VerificationRequest>();
+        let (request_sender, request_receiver) = mpsc::channel::<SenderVerificationRequest>();
 
         let builder = thread::Builder::new().name(format!(
             "Verifier thread running {}",
@@ -55,10 +53,10 @@ impl VerifierThread {
 
     fn listen_for_requests(
         runner: VerifierRunner,
-        request_receiver: mpsc::Receiver<VerificationRequest>,
+        request_receiver: mpsc::Receiver<SenderVerificationRequest>,
     ) {
         while let Ok(request) = request_receiver.recv() {
-            let result = runner.verify(request.programs, request.program_name.as_str());
+            let result = runner.verify(request.program);
             request.sender.send(result).unwrap_or_else(|err| {
                 error!(
                     "verifier thread attempting to send result to dropped receiver: {:?}",
@@ -68,14 +66,13 @@ impl VerifierThread {
         }
     }
 
-    pub fn verify(&self, programs: Vec<Program>, program_name: String) -> FutVerificationResult {
+    pub fn verify(&self, program: Program) -> FutVerificationResult {
         let (tx, rx) = oneshot::channel();
         self.request_sender
             .lock()
             .unwrap()
-            .send(VerificationRequest {
-                programs,
-                program_name,
+            .send(SenderVerificationRequest {
+                program,
                 sender: tx,
             })
             .unwrap();

prusti-server/tests/basic_requests.rs

@@ -9,7 +9,7 @@ use prusti_common::{
     vir::*,
 };
 use prusti_server::{PrustiServerConnection, ServerSideService};
-use viper::ProgramVerificationResult;
+use viper::VerificationResult;
 
 lazy_static! {
     // only start the jvm & server once
@@ -25,43 +25,37 @@ fn consistency_error() {
         });
     });
 
-    let ProgramVerificationResult {
-        verification_errors,
-        mut consistency_errors,
-        java_exceptions,
-    } = result;
-
-    assert!(verification_errors.is_empty());
-    assert!(java_exceptions.is_empty());
-    let consistency_error = consistency_errors.pop().unwrap();
-    assert!(consistency_errors.is_empty());
-    println!("consistency error: {:?}", consistency_error);
+    match result {
+        VerificationResult::ConsistencyErrors(errors) => assert_eq!(errors.len(), 1),
+        other => panic!(
+            "consistency errors not identified, instead found {:?}",
+            other
+        ),
+    }
 }
 
 #[test]
 fn empty_program() {
     let result = process_program(|_| ());
 
-    let ProgramVerificationResult {
-        verification_errors,
-        consistency_errors,
-        java_exceptions,
-    } = result;
-
-    assert!(verification_errors.is_empty());
-    assert!(java_exceptions.is_empty());
-    assert!(consistency_errors.is_empty());
+    match result {
+        VerificationResult::Success => {}
+        other => panic!(
+            "empty program not verified successfully, instead found {:?}",
+            other
+        ),
+    }
 }
 
-fn process_program<F>(configure: F) -> ProgramVerificationResult
+fn process_program<F>(configure: F) -> VerificationResult
 where
     F: FnOnce(&mut Program),
 {
     let service =
         PrustiServerConnection::new(SERVER_ADDRESS.clone()).expect("Could not connect to server!");
 
     let mut program = Program {
-        name: "very_dummy".to_string(),
+        name: "dummy".to_string(),
         domains: vec![],
         fields: vec![],
         builtin_methods: vec![],
@@ -72,8 +66,7 @@ where
     configure(&mut program);
 
     let request = VerificationRequest {
-        programs: vec![program],
-        program_name: "dummy".to_string(),
+        program,
         backend_config: Default::default(),
     };