diff --git a/prusti-server/Cargo.toml b/prusti-server/Cargo.toml index 6fb906a0a10..4afe0e1ffa7 100644 --- a/prusti-server/Cargo.toml +++ b/prusti-server/Cargo.toml @@ -28,6 +28,7 @@ bincode = "1.0" url = "2.2.2" num_cpus = "1.14" serde = { version = "1.0", features = ["derive"] } +serde_json = "1.0" reqwest = { version = "0.11", default-features = false, features = ["json", "rustls-tls"] } warp = "0.3" tokio = "1.20" diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs index 446407c5087..54d912eef05 100644 --- a/prusti-server/src/process_verification.rs +++ b/prusti-server/src/process_verification.rs @@ -10,10 +10,11 @@ use once_cell::sync::Lazy; use prusti_common::{ config, report::log::{report, to_legal_file_name}, - vir::{program_normalization::NormalizationInfo, ToViper}, + vir::{program_normalization::NormalizationInfo, LoweringContext, ToViper}, Stopwatch, }; -use std::{fs::create_dir_all, path::PathBuf}; +use prusti_utils::program_submitter::ProgramSubmitter; +use std::{borrow::Borrow, fs::create_dir_all, path::PathBuf}; use viper::{ smt_manager::SmtManager, Cache, VerificationBackend, VerificationContext, VerificationResult, }; @@ -101,6 +102,11 @@ pub fn process_verification_request<'v, 't: 'v>( let mut stopwatch = Stopwatch::start("prusti-server", "verifier startup"); + let backend_name: String = match request.backend_config.backend.borrow() { + VerificationBackend::Carbon => String::from("Carbon"), + VerificationBackend::Silicon => String::from("Silicion"), + }; + // Create a new verifier each time. // Workaround for https://github.com/viperproject/prusti-dev/issues/744 let mut backend = match request.backend_config.backend { @@ -115,6 +121,23 @@ pub fn process_verification_request<'v, 't: 'v>( }; stopwatch.start_next("backend verification"); + + let mut submitter: Option = None; + if config::submit_for_evaluation() { + let ast_factory = verification_context.new_ast_factory(); + let viper_program = request + .program + .to_viper(LoweringContext::default(), &ast_factory); + + submitter = Some(ProgramSubmitter::new( + true, + ast_utils.to_string(viper_program), + String::from("Prusti"), + backend_name, + vec![], + )) + } + let mut result = backend.verify(&request.program); // Don't cache Java exceptions, which might be due to misconfigured paths. @@ -127,6 +150,12 @@ pub fn process_verification_request<'v, 't: 'v>( cache.insert(hash, result.clone()); } + if submitter.is_some() { + let mut s = submitter.unwrap(); + s.set_success(result.is_success()); + s.submit(); + }; + normalization_info.denormalize_result(&mut result); result } diff --git a/prusti-utils/Cargo.toml b/prusti-utils/Cargo.toml index 6e20eacfe3c..a4c17ab9464 100644 --- a/prusti-utils/Cargo.toml +++ b/prusti-utils/Cargo.toml @@ -12,6 +12,8 @@ log = { version = "0.4", features = ["release_max_level_info"] } config = "0.13" itertools = "0.11" serde = { version = "1.0", features = ["derive"] } +serde_json = "1.0" +reqwest = { version = "0.11", features = ["blocking"] } lazy_static = "1.4.0" uuid = { version = "1.0", features = ["v4"] } rustc-hash = "1.1.0" diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index 2e46d55519c..687d37208ba 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -131,6 +131,7 @@ lazy_static::lazy_static! { settings.set_default::>("min_prusti_version", None).unwrap(); settings.set_default("num_errors_per_function", 1).unwrap(); settings.set_default("ignore_deps_contracts", false).unwrap(); + settings.set_default("submit_for_evaluation", false).unwrap(); settings.set_default("print_desugared_specs", false).unwrap(); settings.set_default("print_typeckd_specs", false).unwrap(); @@ -1036,3 +1037,8 @@ pub fn num_errors_per_function() -> u32 { pub fn ignore_deps_contracts() -> bool { read_setting("ignore_deps_contracts") } + +/// "Whether to allow storing the current program for future evaluation. +pub fn submit_for_evaluation() -> bool { + read_setting("submit_for_evaluation") +} diff --git a/prusti-utils/src/lib.rs b/prusti-utils/src/lib.rs index 12116a3fe0f..943e25a8848 100644 --- a/prusti-utils/src/lib.rs +++ b/prusti-utils/src/lib.rs @@ -14,6 +14,7 @@ pub mod config; pub mod launch; pub mod report; +pub mod program_submitter; mod stopwatch; pub mod utils; diff --git a/prusti-utils/src/program_submitter.rs b/prusti-utils/src/program_submitter.rs new file mode 100644 index 00000000000..1813fa6019e --- /dev/null +++ b/prusti-utils/src/program_submitter.rs @@ -0,0 +1,65 @@ +use serde_json::json; +use std::time::SystemTime; + +const API_HOST: &str = "http://localhost:8080"; + +pub struct ProgramSubmitter { + allow_submission: bool, + program: String, + original_frontend: String, + original_verifier: String, + args: Vec, + start_time: SystemTime, + succeeded: bool, +} + +impl ProgramSubmitter { + pub fn new( + allow_submission: bool, + program: String, + original_frontend: String, + original_verifier: String, + args: Vec, + ) -> Self { + Self { + allow_submission, + program, + original_frontend, + original_verifier, + args, + start_time: SystemTime::now(), + succeeded: false, + } + } + + pub fn set_success(&mut self, success: bool) { + self.succeeded = success; + } + + fn runtime(&self) -> u64 { + self.start_time.elapsed().unwrap().as_millis() as u64 + } + + pub fn submit(&self) { + if !API_HOST.is_empty() && self.allow_submission { + let submission = json!({ + "program": &self.program, + "frontend": &self.original_frontend, + "args": self.args, + "originalVerifier": &self.original_verifier, + "success": self.succeeded, + "runtime": self.runtime(), + }); + + let client = reqwest::blocking::Client::new(); + let response = client + .post(&format!("{}/submit-program", API_HOST)) + .json(&submission) + .send(); + match response { + Ok(_) => {} + Err(_) => eprintln!("Program couldn't be submitted"), + } + } + } +}