Viper Data Collection changes

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"

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<ProgramSubmitter> = 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
 }

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"

prusti-utils/src/config.rs

@@ -131,6 +131,7 @@ lazy_static::lazy_static! {
         settings.set_default::<Option<String>>("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")
+}

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;
 

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<String>,
+    start_time: SystemTime,
+    succeeded: bool,
+}
+
+impl ProgramSubmitter {
+    pub fn new(
+        allow_submission: bool,
+        program: String,
+        original_frontend: String,
+        original_verifier: String,
+        args: Vec<String>,
+    ) -> 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"),
+            }
+        }
+    }
+}