From baa66442c99d57ef29412fedbb4fbf62d635fcf0 Mon Sep 17 00:00:00 2001 From: Simon Hostettler Date: Wed, 27 Dec 2023 15:09:34 +0100 Subject: [PATCH 1/5] moved code to prusti-server --- prusti-server/Cargo.toml | 3 + prusti-server/src/lib.rs | 1 + prusti-server/src/process_verification.rs | 13 +++++ prusti-server/src/program_submitter.rs | 68 +++++++++++++++++++++++ prusti-utils/src/config.rs | 6 ++ 5 files changed, 91 insertions(+) create mode 100644 prusti-server/src/program_submitter.rs diff --git a/prusti-server/Cargo.toml b/prusti-server/Cargo.toml index 6fb906a0a10..b47de5cfeaf 100644 --- a/prusti-server/Cargo.toml +++ b/prusti-server/Cargo.toml @@ -24,6 +24,9 @@ prusti-utils = { path = "../prusti-utils" } tracing = { path = "../tracing" } env_logger = "0.10" clap = { version = "4.0", features = ["derive"] } +serde = { version = "1.0", features = ["derive"] } +serde_json = "1.0" +reqwest = {version = "0.11", features = ["blocking"] } bincode = "1.0" url = "2.2.2" num_cpus = "1.14" diff --git a/prusti-server/src/lib.rs b/prusti-server/src/lib.rs index 64b7b670ffd..b72f624b60b 100644 --- a/prusti-server/src/lib.rs +++ b/prusti-server/src/lib.rs @@ -9,6 +9,7 @@ mod client; mod process_verification; mod server; +mod program_submitter; mod verification_request; mod backend; diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs index 446407c5087..2600c421a89 100644 --- a/prusti-server/src/process_verification.rs +++ b/prusti-server/src/process_verification.rs @@ -5,6 +5,7 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. use crate::{Backend, VerificationRequest, ViperBackendConfig}; +use crate::program_submitter::ProgramSubmitter; use log::info; use once_cell::sync::Lazy; use prusti_common::{ @@ -115,6 +116,15 @@ pub fn process_verification_request<'v, 't: 'v>( }; stopwatch.start_next("backend verification"); + + let backend_name: String = match request.backend_config.backend { + VerificationBackend::Carbon => String::from("Carbon"), + VerificationBackend::Silicon => String::from("Silicion") + }; + + let mut submitter: ProgramSubmitter = ProgramSubmitter::new(true, String::from("undefined"), + ast_utils.to_string(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 +137,9 @@ pub fn process_verification_request<'v, 't: 'v>( cache.insert(hash, result.clone()); } + submitter.set_success(!result); + submitter.submit(); + normalization_info.denormalize_result(&mut result); result } diff --git a/prusti-server/src/program_submitter.rs b/prusti-server/src/program_submitter.rs new file mode 100644 index 00000000000..5f852f6d218 --- /dev/null +++ b/prusti-server/src/program_submitter.rs @@ -0,0 +1,68 @@ +use serde_json::json; +use std::time::SystemTime; + +const API_HOST: &str = "http://localhost:8080"; + +pub struct ProgramSubmitter { + allow_submission: bool, + program_name: String, + program: String, + original_frontend: String, + original_verifier: String, + args: Vec, + start_time: SystemTime, + succeeded: bool, +} + +impl ProgramSubmitter { + pub fn new( + allow_submission: bool, + program_name: String, + program: String, + original_frontend: String, + original_verifier: String, + args: Vec, + ) -> Self { + Self { + allow_submission, + program_name, + 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!({ + "originalName": self.program_name, + "program": &self.program, + "frontend": &self.original_frontend, + "args": self.args, + "originalVerifier": &self.original_verifier, + "success": self.succeeded, + "runtime": self.runtime(), + }); + + match reqwest::blocking::Client::new() + .post(&format!("{}/submit-program", API_HOST)) + .json(&submission) + .send() + { + Ok(_) => {} + Err(_) => eprintln!("Program couldn't be submitted"), + } + } + } +} diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index fe1528d1e0c..b2ac36af482 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -130,6 +130,7 @@ lazy_static::lazy_static! { settings.set_default::>("number_of_parallel_verifiers", None).unwrap(); settings.set_default::>("min_prusti_version", None).unwrap(); settings.set_default("num_errors_per_function", 1).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(); @@ -1030,3 +1031,8 @@ pub fn enable_type_invariants() -> bool { pub fn num_errors_per_function() -> u32 { read_setting("num_errors_per_function") } + +/// "Whether to allow storing the current program for future evaluation. +pub fn submit_for_evaluation() -> bool { + read_setting("submit_for_evaluation") +} From 59c62734b1f29f6c5adfcc87398f5accfdedb6fb Mon Sep 17 00:00:00 2001 From: Simon Hostettler Date: Wed, 27 Dec 2023 15:17:56 +0100 Subject: [PATCH 2/5] changed deps --- prusti-server/Cargo.toml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/prusti-server/Cargo.toml b/prusti-server/Cargo.toml index b47de5cfeaf..5bb43244c09 100644 --- a/prusti-server/Cargo.toml +++ b/prusti-server/Cargo.toml @@ -24,14 +24,12 @@ prusti-utils = { path = "../prusti-utils" } tracing = { path = "../tracing" } env_logger = "0.10" clap = { version = "4.0", features = ["derive"] } -serde = { version = "1.0", features = ["derive"] } -serde_json = "1.0" -reqwest = {version = "0.11", features = ["blocking"] } bincode = "1.0" url = "2.2.2" num_cpus = "1.14" serde = { version = "1.0", features = ["derive"] } -reqwest = { version = "0.11", default-features = false, features = ["json", "rustls-tls"] } +serde_json = "1.0" +reqwest = { version = "0.11", default-features = false, features = ["json", "rustls-tls, blocking"] } warp = "0.3" tokio = "1.20" rustc-hash = "1.1.0" From e1e4c32de7c8f3308de4eb48d6220303c73d4636 Mon Sep 17 00:00:00 2001 From: Simon Hostettler Date: Wed, 27 Dec 2023 15:28:25 +0100 Subject: [PATCH 3/5] changed reqwest client --- prusti-server/Cargo.toml | 2 +- prusti-server/src/process_verification.rs | 2 +- prusti-server/src/program_submitter.rs | 3 ++- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/prusti-server/Cargo.toml b/prusti-server/Cargo.toml index 5bb43244c09..4afe0e1ffa7 100644 --- a/prusti-server/Cargo.toml +++ b/prusti-server/Cargo.toml @@ -29,7 +29,7 @@ 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, blocking"] } +reqwest = { version = "0.11", default-features = false, features = ["json", "rustls-tls"] } warp = "0.3" tokio = "1.20" rustc-hash = "1.1.0" diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs index 2600c421a89..1f34b808799 100644 --- a/prusti-server/src/process_verification.rs +++ b/prusti-server/src/process_verification.rs @@ -122,7 +122,7 @@ pub fn process_verification_request<'v, 't: 'v>( VerificationBackend::Silicon => String::from("Silicion") }; - let mut submitter: ProgramSubmitter = ProgramSubmitter::new(true, String::from("undefined"), + let mut submitter: ProgramSubmitter = ProgramSubmitter::new(config::submit_for_evaluation(), String::from("undefined"), ast_utils.to_string(program), String::from("Prusti"), backend_name, vec![]); let mut result = backend.verify(&request.program); diff --git a/prusti-server/src/program_submitter.rs b/prusti-server/src/program_submitter.rs index 5f852f6d218..a61df24c972 100644 --- a/prusti-server/src/program_submitter.rs +++ b/prusti-server/src/program_submitter.rs @@ -55,10 +55,11 @@ impl ProgramSubmitter { "runtime": self.runtime(), }); - match reqwest::blocking::Client::new() + match reqwest::Client::new() .post(&format!("{}/submit-program", API_HOST)) .json(&submission) .send() + .await?; { Ok(_) => {} Err(_) => eprintln!("Program couldn't be submitted"), From 4ccf4c219ffb9f22d936da6d8a9a4c62d8cdded0 Mon Sep 17 00:00:00 2001 From: Simon Hostettler Date: Wed, 27 Dec 2023 15:48:21 +0100 Subject: [PATCH 4/5] changed submission logic --- prusti-server/src/lib.rs | 1 - prusti-server/src/process_verification.rs | 33 ++++++++++++------- prusti-utils/Cargo.toml | 2 ++ prusti-utils/src/lib.rs | 1 + .../src/program_submitter.rs | 8 ++--- 5 files changed, 29 insertions(+), 16 deletions(-) rename {prusti-server => prusti-utils}/src/program_submitter.rs (92%) diff --git a/prusti-server/src/lib.rs b/prusti-server/src/lib.rs index b72f624b60b..64b7b670ffd 100644 --- a/prusti-server/src/lib.rs +++ b/prusti-server/src/lib.rs @@ -9,7 +9,6 @@ mod client; mod process_verification; mod server; -mod program_submitter; mod verification_request; mod backend; diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs index 1f34b808799..6c00bbbc614 100644 --- a/prusti-server/src/process_verification.rs +++ b/prusti-server/src/process_verification.rs @@ -5,16 +5,16 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. use crate::{Backend, VerificationRequest, ViperBackendConfig}; -use crate::program_submitter::ProgramSubmitter; +use prusti_utils::program_submitter::ProgramSubmitter; use log::info; 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, ToViper, LoweringContext}, Stopwatch, }; -use std::{fs::create_dir_all, path::PathBuf}; +use std::{fs::create_dir_all, path::PathBuf, borrow::Borrow}; use viper::{ smt_manager::SmtManager, Cache, VerificationBackend, VerificationContext, VerificationResult, }; @@ -102,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 { @@ -117,13 +122,16 @@ pub fn process_verification_request<'v, 't: 'v>( stopwatch.start_next("backend verification"); - let backend_name: String = match request.backend_config.backend { - VerificationBackend::Carbon => String::from("Carbon"), - VerificationBackend::Silicon => String::from("Silicion") - }; - let mut submitter: ProgramSubmitter = ProgramSubmitter::new(config::submit_for_evaluation(), String::from("undefined"), - ast_utils.to_string(program), String::from("Prusti"), backend_name, vec![]); + 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, request.program.get_name().to_string(), + ast_utils.to_string(viper_program), String::from("Prusti"), backend_name, vec![])) + } let mut result = backend.verify(&request.program); @@ -137,8 +145,11 @@ pub fn process_verification_request<'v, 't: 'v>( cache.insert(hash, result.clone()); } - submitter.set_success(!result); - submitter.submit(); + 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/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-server/src/program_submitter.rs b/prusti-utils/src/program_submitter.rs similarity index 92% rename from prusti-server/src/program_submitter.rs rename to prusti-utils/src/program_submitter.rs index a61df24c972..a2a3b93cad5 100644 --- a/prusti-server/src/program_submitter.rs +++ b/prusti-utils/src/program_submitter.rs @@ -55,12 +55,12 @@ impl ProgramSubmitter { "runtime": self.runtime(), }); - match reqwest::Client::new() + let client = reqwest::blocking::Client::new(); + let response = client .post(&format!("{}/submit-program", API_HOST)) .json(&submission) - .send() - .await?; - { + .send(); + match response { Ok(_) => {} Err(_) => eprintln!("Program couldn't be submitted"), } From 75aaff5e977db9e94b1565f64df177b1e64f1d9f Mon Sep 17 00:00:00 2001 From: Simon Hostettler Date: Sat, 2 Mar 2024 12:07:44 +0100 Subject: [PATCH 5/5] updated submitter code --- prusti-server/src/process_verification.rs | 27 ++++++++++++++--------- prusti-utils/src/program_submitter.rs | 4 ---- 2 files changed, 16 insertions(+), 15 deletions(-) diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs index 6c00bbbc614..54d912eef05 100644 --- a/prusti-server/src/process_verification.rs +++ b/prusti-server/src/process_verification.rs @@ -5,16 +5,16 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. use crate::{Backend, VerificationRequest, ViperBackendConfig}; -use prusti_utils::program_submitter::ProgramSubmitter; use log::info; use once_cell::sync::Lazy; use prusti_common::{ config, report::log::{report, to_legal_file_name}, - vir::{program_normalization::NormalizationInfo, ToViper, LoweringContext}, + vir::{program_normalization::NormalizationInfo, LoweringContext, ToViper}, Stopwatch, }; -use std::{fs::create_dir_all, path::PathBuf, borrow::Borrow}; +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, }; @@ -104,7 +104,7 @@ pub fn process_verification_request<'v, 't: 'v>( let backend_name: String = match request.backend_config.backend.borrow() { VerificationBackend::Carbon => String::from("Carbon"), - VerificationBackend::Silicon => String::from("Silicion") + VerificationBackend::Silicon => String::from("Silicion"), }; // Create a new verifier each time. @@ -122,15 +122,20 @@ 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, request.program.get_name().to_string(), - ast_utils.to_string(viper_program), String::from("Prusti"), backend_name, vec![])) + 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); @@ -148,7 +153,7 @@ pub fn process_verification_request<'v, 't: 'v>( if submitter.is_some() { let mut s = submitter.unwrap(); s.set_success(result.is_success()); - s.submit(); + s.submit(); }; normalization_info.denormalize_result(&mut result); diff --git a/prusti-utils/src/program_submitter.rs b/prusti-utils/src/program_submitter.rs index a2a3b93cad5..1813fa6019e 100644 --- a/prusti-utils/src/program_submitter.rs +++ b/prusti-utils/src/program_submitter.rs @@ -5,7 +5,6 @@ const API_HOST: &str = "http://localhost:8080"; pub struct ProgramSubmitter { allow_submission: bool, - program_name: String, program: String, original_frontend: String, original_verifier: String, @@ -17,7 +16,6 @@ pub struct ProgramSubmitter { impl ProgramSubmitter { pub fn new( allow_submission: bool, - program_name: String, program: String, original_frontend: String, original_verifier: String, @@ -25,7 +23,6 @@ impl ProgramSubmitter { ) -> Self { Self { allow_submission, - program_name, program, original_frontend, original_verifier, @@ -46,7 +43,6 @@ impl ProgramSubmitter { pub fn submit(&self) { if !API_HOST.is_empty() && self.allow_submission { let submission = json!({ - "originalName": self.program_name, "program": &self.program, "frontend": &self.original_frontend, "args": self.args,