From 4e6cc8a22920c60af8643c88129cebab62bf9378 Mon Sep 17 00:00:00 2001 From: trk Date: Wed, 12 Jun 2024 19:15:19 +0200 Subject: [PATCH] Change prusti-server workflow Port basic functionality for the new prusti-server work flow according to PR https://github.com/viperproject/prusti-dev/pull/1334 . --- Cargo.lock | 121 ++++++++++++- prusti-server/Cargo.toml | 14 +- prusti-server/src/backend.rs | 29 +++- prusti-server/src/client.rs | 103 ++++++----- prusti-server/src/lib.rs | 198 +++++++++++++++++----- prusti-server/src/process_verification.rs | 160 +++++++++++++++-- prusti-server/src/server.rs | 93 +++++----- prusti-server/src/server_message.rs | 33 ++++ prusti-server/src/verification_request.rs | 20 ++- prusti/Cargo.toml | 2 + prusti/src/callbacks.rs | 60 +++++-- prusti/src/driver.rs | 1 + prusti/src/ide_helper/fake_error.rs | 16 ++ prusti/src/verifier.rs | 26 +-- viper-sys/build.rs | 14 ++ viper/src/lib.rs | 6 +- viper/src/verification_context.rs | 4 + viper/src/verifier.rs | 11 +- 18 files changed, 722 insertions(+), 189 deletions(-) create mode 100644 prusti-server/src/server_message.rs create mode 100644 prusti/src/ide_helper/fake_error.rs diff --git a/Cargo.lock b/Cargo.lock index 2fc7185a20d..03f49bed973 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -304,6 +304,28 @@ dependencies = [ "wasm-bindgen-futures", ] +[[package]] +name = "async-stream" +version = "0.3.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cd56dd203fef61ac097dd65721a419ddccb106b2d2b70ba60a6b529f03961a51" +dependencies = [ + "async-stream-impl", + "futures-core", + "pin-project-lite", +] + +[[package]] +name = "async-stream-impl" +version = "0.3.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "16e62a023e7c117e27523144c5d2459f4397fcc3cab0085af8e2224f643a0193" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.39", +] + [[package]] name = "async-task" version = "4.5.0" @@ -387,6 +409,15 @@ version = "2.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "327762f6e5a765692301e5bb513e0d9fef63be86bbc14528052b1cd3e6f03e07" +[[package]] +name = "block-buffer" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4152116fd6e9dadb291ae18fc1ec3575ed6d84c29642d97890f4b4a3417297e4" +dependencies = [ + "generic-array", +] + [[package]] name = "block-buffer" version = "0.10.4" @@ -662,13 +693,22 @@ dependencies = [ "syn 1.0.109", ] +[[package]] +name = "digest" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d3dd60d1080a57a05ab032377049e0591415d2b31afd7028356dbf3cc6dcb066" +dependencies = [ + "generic-array", +] + [[package]] name = "digest" version = "0.10.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292" dependencies = [ - "block-buffer", + "block-buffer 0.10.4", "crypto-common", ] @@ -1194,6 +1234,15 @@ dependencies = [ "hashbrown 0.14.2", ] +[[package]] +name = "input_buffer" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f97967975f448f1a7ddb12b0bc41069d09ed6a1c161a92687e057325db35d413" +dependencies = [ + "bytes", +] + [[package]] name = "instant" version = "0.1.12" @@ -1550,6 +1599,12 @@ version = "1.18.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d" +[[package]] +name = "opaque-debug" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c08d65885ee38876c4f86fa503fb49d7b507c2b62552df7c70b2fce627e06381" + [[package]] name = "openssl" version = "0.10.59" @@ -1791,6 +1846,8 @@ dependencies = [ "prusti-server", "prusti-utils", "prusti-viper", + "serde", + "serde_json", "tracing 0.1.0", "tracing-chrome", "tracing-subscriber", @@ -1855,22 +1912,31 @@ version = "0.1.0" name = "prusti-server" version = "0.1.0" dependencies = [ + "async-stream", "bincode", "clap", "env_logger", + "futures", + "futures-util", + "jni", "lazy_static", "log", "num_cpus", "once_cell", + "prusti-interface", + "prusti-rustc-interface", "prusti-utils", "prusti-viper", "reqwest", "rustc-hash", "serde", + "serde_json", "tokio", + "tokio-tungstenite 0.13.0", "tracing 0.1.0", "url", "viper", + "viper-sys", "vir", "warp", ] @@ -2304,6 +2370,19 @@ dependencies = [ "serde", ] +[[package]] +name = "sha-1" +version = "0.9.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "99cd6713db3cf16b6c84e06321e049a9b9f699826e16096d23bbcc44d15d51a6" +dependencies = [ + "block-buffer 0.9.0", + "cfg-if", + "cpufeatures", + "digest 0.9.0", + "opaque-debug", +] + [[package]] name = "sha1" version = "0.10.6" @@ -2312,7 +2391,7 @@ checksum = "e3bf829a2d51ab4a5ddf1352d8470c140cadc8301b2ae1789db023f01cedd6ba" dependencies = [ "cfg-if", "cpufeatures", - "digest", + "digest 0.10.7", ] [[package]] @@ -2323,7 +2402,7 @@ checksum = "793db75ad2bcafc3ffa7c68b215fee268f537982cd901d132f89c6343f3a3dc8" dependencies = [ "cfg-if", "cpufeatures", - "digest", + "digest 0.10.7", ] [[package]] @@ -2563,6 +2642,19 @@ dependencies = [ "tokio", ] +[[package]] +name = "tokio-tungstenite" +version = "0.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e1a5f475f1b9d077ea1017ecbc60890fda8e54942d680ca0b1d2b47cfa2d861b" +dependencies = [ + "futures-util", + "log", + "pin-project", + "tokio", + "tungstenite 0.12.0", +] + [[package]] name = "tokio-tungstenite" version = "0.20.1" @@ -2572,7 +2664,7 @@ dependencies = [ "futures-util", "log", "tokio", - "tungstenite", + "tungstenite 0.20.1", ] [[package]] @@ -2725,6 +2817,25 @@ version = "0.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3528ecfd12c466c6f163363caf2d02a71161dd5e1cc6ae7b34207ea2d42d81ed" +[[package]] +name = "tungstenite" +version = "0.12.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8ada8297e8d70872fa9a551d93250a9f407beb9f37ef86494eb20012a2ff7c24" +dependencies = [ + "base64 0.13.1", + "byteorder", + "bytes", + "http", + "httparse", + "input_buffer", + "log", + "rand", + "sha-1", + "url", + "utf-8", +] + [[package]] name = "tungstenite" version = "0.20.1" @@ -2977,7 +3088,7 @@ dependencies = [ "serde_urlencoded", "tokio", "tokio-stream", - "tokio-tungstenite", + "tokio-tungstenite 0.20.1", "tokio-util", "tower-service", "tracing 0.1.40", diff --git a/prusti-server/Cargo.toml b/prusti-server/Cargo.toml index 053afaf0784..7e510584dcc 100644 --- a/prusti-server/Cargo.toml +++ b/prusti-server/Cargo.toml @@ -20,8 +20,11 @@ doctest = false log = { version = "0.4", features = ["release_max_level_info"] } vir = { path = "../vir" } viper = { path = "../viper" } +prusti-interface = { path = "../prusti-interface" } prusti-viper = { path = "../prusti-viper" } prusti-utils = { path = "../prusti-utils" } +prusti-rustc-interface = { path = "../prusti-rustc-interface" } +viper-sys = { path = "../viper-sys" } tracing = { path = "../tracing" } env_logger = "0.10" clap = { version = "4.0", features = ["derive"] } @@ -29,11 +32,20 @@ bincode = "1.0" url = "2.2.2" num_cpus = "1.14" serde = { version = "1.0", features = ["derive"] } +serde_json = { version = "1.0" } +jni = { version = "0.20", features = ["invocation"] } +# the tungstenite version used by warp 0.3 +tokio-tungstenite = "0.13" +futures = "0.3.25" +futures-util = "0.3.25" +async-stream = "0.3.3" reqwest = { version = "0.11", default-features = false, features = ["json", "rustls-tls"] } warp = "0.3" -tokio = "1.20" +# tokio = "1.20" +tokio = { version = "1.20", features = ["io-util", "net", "rt", "sync"] } rustc-hash = "1.1.0" once_cell = "1.17.1" + [dev-dependencies] lazy_static = "1.4.0" diff --git a/prusti-server/src/backend.rs b/prusti-server/src/backend.rs index 3da934253a1..d0445f233a5 100644 --- a/prusti-server/src/backend.rs +++ b/prusti-server/src/backend.rs @@ -1,18 +1,32 @@ -use crate::dump_viper_program; +use crate::{dump_viper_program, ServerMessage}; +use log::{debug, info}; use prusti_utils::{ config, Stopwatch, }; -use viper::{VerificationContext, VerificationResultKind}; +use std::{ + sync::{mpsc, Arc}, + thread, time, +}; +use viper::{jni_utils::JniUtils, VerificationContext, VerificationResultKind, Viper}; +use viper_sys::wrappers::{java, viper::*}; pub enum Backend<'a> { - Viper(viper::Verifier<'a>, &'a VerificationContext<'a>), + Viper( + viper::Verifier<'a>, + &'a VerificationContext<'a>, + &'a Arc, + ), } impl<'a> Backend<'a> { - pub fn verify(&mut self, program: vir::ProgramRef) -> VerificationResultKind { + pub fn verify( + &mut self, + program: vir::ProgramRef, + sender: mpsc::Sender, + ) -> VerificationResultKind { match self { - Backend::Viper(viper, context) => { + Backend::Viper(ref mut verifier, context, viper_arc) => { let mut stopwatch = Stopwatch::start("prusti-server backend", "construction of JVM objects"); @@ -36,9 +50,10 @@ impl<'a> Backend<'a> { } stopwatch.start_next("viper verification"); - viper.verify(viper_program) + + verifier.verify(viper_program) }) } } } -} +} \ No newline at end of file diff --git a/prusti-server/src/client.rs b/prusti-server/src/client.rs index 61549e0dd80..838529c14cd 100644 --- a/prusti-server/src/client.rs +++ b/prusti-server/src/client.rs @@ -4,58 +4,75 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -use crate::VerificationRequest; +use crate::{ServerMessage, VerificationRequest}; +use futures_util::{ + sink::SinkExt, + stream::{Stream, StreamExt}, +}; use prusti_utils::config; -use reqwest::Client; -use url::{ParseError, Url}; -use viper::VerificationResult; +use tokio_tungstenite::{ + connect_async, + tungstenite::{error::Error, Message}, +}; +use url::Url; -pub struct PrustiClient { - client: Client, - server_url: Url, -} +pub struct PrustiClient; impl PrustiClient { - pub fn new(server_address: S) -> Result { + pub async fn verify( + server_address: S, + request: VerificationRequest, + ) -> impl Stream { let mut address = server_address.to_string(); - if !address.starts_with("http") { - address = format!("http://{address}"); + if !address.starts_with("ws") { + address = format!("ws://{address}"); } - Ok(Self { - client: Client::new(), - server_url: Url::parse(address.as_str())?, - }) - } - pub async fn verify( - &self, - request: VerificationRequest, - ) -> reqwest::Result { + let server_url = Url::parse(address.as_str()).unwrap(); let use_json = config::json_communication(); - let base = self.client.post( - self.server_url - .join(if use_json { "json/" } else { "bincode/" }) - .unwrap() - .join("verify/") - .unwrap(), - ); - let response = if use_json { - base.json(&request) - .send() - .await? - .error_for_status()? - .json() - .await? + + let uri = server_url + .join(if use_json { "json/" } else { "bincode/" }) + .unwrap() + .join("verify/") + .unwrap(); + let (mut socket, _) = connect_async(uri).await.unwrap(); + let msg = if use_json { + Message::text( + serde_json::to_string(&request) + .expect("error encoding verification request in json"), + ) } else { - let bytes = base - .body(bincode::serialize(&request).expect("error encoding verification request")) - .send() - .await? - .error_for_status()? - .bytes() - .await?; - bincode::deserialize(&bytes).expect("error decoding verification result") + Message::binary( + bincode::serialize(&request) + .expect("error encoding verification request as binary"), + ) + }; + socket.send(msg).await.unwrap(); + let json_map = |ws_msg| { + if let Message::Text(json) = ws_msg { + serde_json::from_str(&json).expect("error decoding verification result from json") + } else { + panic!("Invalid response from the server."); + } + }; + let bin_map = |ws_msg| { + if let Message::Binary(bytes) = ws_msg { + bincode::deserialize(&bytes).expect("error decoding verification result") + } else { + panic!("Invalid response from the server."); + } + }; + let filter_close = |msg_result: Result| async { + let msg = msg_result.unwrap(); + match msg { + Message::Close(_) => None, + _ => Some(msg), + } }; - Ok(response) + + socket + .filter_map(filter_close) + .map(if use_json { json_map } else { bin_map }) } } diff --git a/prusti-server/src/lib.rs b/prusti-server/src/lib.rs index 30a62485943..c03bdae7322 100644 --- a/prusti-server/src/lib.rs +++ b/prusti-server/src/lib.rs @@ -5,15 +5,32 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. #![warn(clippy::disallowed_types)] +#![feature(rustc_private)] -use log::info; +// use log::info; +use ::log::{debug, error, info}; +use crate::{ + spawn_server_thread, PrustiClient, ServerMessage, VerificationRequest, + VerificationRequestProcessing, ViperBackendConfig, +}; use prusti_utils::{config, Stopwatch}; -use viper::{PersistentCache, Viper}; +use prusti_interface::{ + data::{VerificationResult, VerificationTask}, + environment::EnvDiagnostic, + specs::typed, + PrustiError, +}; +use prusti_rustc_interface::{ + span::DUMMY_SP, + errors::MultiSpan, +}; +use viper::{self, PersistentCache, Viper}; use once_cell::sync::Lazy; mod client; mod process_verification; mod server; +mod server_message; mod verification_request; mod backend; @@ -21,14 +38,23 @@ pub use backend::*; pub use client::*; pub use process_verification::*; pub use server::*; +pub use server_message::*; pub use verification_request::*; // Futures returned by `Client` need to be executed in a compatible tokio runtime. pub use tokio; +use tokio::runtime::Builder; +use rustc_hash::FxHashMap; +use serde_json::json; +use async_stream::stream; +use futures_util::{pin_mut, Stream, StreamExt}; /// Verify a list of programs. /// Returns a list of (program_name, verification_result) tuples. -pub fn verify_programs(programs: Vec) -> Vec<(String, viper::VerificationResult)> { +pub fn verify_programs( + env_diagnostic: &EnvDiagnostic<'_>, + programs: Vec + ) -> VerificationResult { let verification_requests = programs.into_iter().map(|mut program| { let rust_program_name = program.get_rust_name().to_string(); let program_name = program.get_name().to_string(); @@ -41,47 +67,133 @@ pub fn verify_programs(programs: Vec) -> Vec<(String, viper::Ve }; (program_name, request) }); - if let Some(server_address) = config::server_address() { - let server_address = if server_address == "MOCK" { - spawn_server_thread().to_string() + + let mut stopwatch = Stopwatch::start("prusti-server", "verifying Viper program"); + // runtime used either for client connecting to server sequentially + // or to sequentially verify the requests -> single thread is sufficient + // why single thread if everything is asynchronous? VerificationRequestProcessing in + // prusti-server/src/process_verification.rs only has a single thread and the underlying + // viper instance already uses as many cores as possible + let rt = Builder::new_current_thread() + .thread_name("prusti-viper") + .enable_all() + .build() + .expect("failed to construct Tokio runtime"); + + let overall_result = rt.block_on(async { + if let Some(server_address) = config::server_address() { + let verification_messages = verify_requests_server(verification_requests.collect(), server_address); + handle_stream(env_diagnostic, verification_messages).await } else { - server_address - }; - info!("Connecting to Prusti server at {}", server_address); - let client = PrustiClient::new(&server_address).unwrap_or_else(|error| { - panic!("Could not parse server address ({server_address}) due to {error:?}") - }); - // Here we construct a Tokio runtime to block until completion of the futures returned by - // `client.verify`. However, to report verification errors as early as possible, - // `verify_programs` should return an asynchronous stream of verification results. - let runtime = tokio::runtime::Builder::new_current_thread() - .thread_name("prusti-viper") - .enable_all() - .build() - .expect("failed to construct Tokio runtime"); - verification_requests - .map(|(program_name, request)| { - let remote_result = runtime.block_on(client.verify(request)); - let result = remote_result.unwrap_or_else(|error| { - panic!("Verification request of program {program_name} failed: {error:?}") - }); - (program_name, result) - }) - .collect() - } else { - let mut stopwatch = Stopwatch::start("prusti-viper", "JVM startup"); - stopwatch.start_next("attach current thread to the JVM"); - let viper = - Lazy::new(|| Viper::new_with_args(&config::viper_home(), config::extra_jvm_args())); - let viper_thread = Lazy::new(|| viper.attach_current_thread()); - stopwatch.finish(); + let vrp = VerificationRequestProcessing::new(); + let verification_messages = verify_requests_local(verification_requests.collect(), &vrp); + handle_stream(env_diagnostic, verification_messages).await + } + }); + stopwatch.finish(); + overall_result +} + +async fn handle_stream( + env_diagnostic: &EnvDiagnostic<'_>, + verification_messages: impl Stream, +) -> VerificationResult { + let mut overall_result = VerificationResult::Success; + let mut prusti_errors: Vec<_> = vec![]; + + pin_mut!(verification_messages); + + while let Some((program_name, server_msg)) = verification_messages.next().await { + match server_msg { + ServerMessage::Termination(result) => handle_termination_message(env_diagnostic, program_name, result, &mut prusti_errors, &mut overall_result), + } + } + + overall_result +} - let mut cache = PersistentCache::load_cache(config::cache_path()); - verification_requests - .map(|(program_name, request)| { - let result = process_verification_request(&viper_thread, request, &mut cache); - (program_name, result) - }) - .collect() +fn handle_termination_message( + env_diagnostic: &EnvDiagnostic<'_>, + // &self, + program_name: String, + result: viper::VerificationResult, + prusti_errors: &mut Vec, + overall_result: &mut VerificationResult +) { + debug!("Received termination message with result {result:?} in verification of {program_name}"); + match result.kind { + // nothing to do + viper::VerificationResultKind::Success => (), + viper::VerificationResultKind::ConsistencyErrors(errors) => { + for error in errors { + PrustiError::internal( + format!("consistency error in {program_name}: {error:?}"), + DUMMY_SP.into(), + ) + .emit(env_diagnostic); + } + *overall_result = VerificationResult::Failure; + } + viper::VerificationResultKind::Failure(errors) => { + for verification_error in errors { + debug!( + "Verification error in {}: {:?}", + program_name.clone(), + verification_error + ); + // temporary error emition, delete when verification errors can be backtranslated again + env_diagnostic.span_err_with_help_and_notes( + MultiSpan::new(), + &format!( + "Verification error in {}: {:?}", + program_name.clone(), + verification_error + ), + &None, + &[], + ); + } + *overall_result = VerificationResult::Failure; + } + viper::VerificationResultKind::JavaException(exception) => { + error!("Java exception: {}", exception.get_stack_trace()); + PrustiError::internal( + format!("in {program_name}: {exception}"), + DUMMY_SP.into(), + ) + .emit(env_diagnostic); + // .emit(&self.env.diagnostic); + *overall_result = VerificationResult::Failure; + } } } + +fn verify_requests_server( + verification_requests: Vec<(String, VerificationRequest)>, + server_address: String, +) -> impl Stream { + let server_address = if server_address == "MOCK" { + spawn_server_thread().to_string() + } else { + server_address + }; + info!("Connecting to Prusti server at {}", server_address); + let verification_stream = stream! { + for (program_name, request) in verification_requests { + yield PrustiClient::verify(server_address.clone(), request).await.map(move |msg| (program_name.clone(), msg)); + } + }; + verification_stream.flatten() +} + +fn verify_requests_local<'a>( + verification_requests: Vec<(String, VerificationRequest)>, + vrp: &'a VerificationRequestProcessing, +) -> impl Stream + 'a { + let verification_stream = stream! { + for (program_name, request) in verification_requests { + yield vrp.verify(request).map(move |msg| (program_name.clone(), msg)); + } + }; + verification_stream.flatten() +} diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs index 1e7a687d754..c572711d064 100644 --- a/prusti-server/src/process_verification.rs +++ b/prusti-server/src/process_verification.rs @@ -4,25 +4,148 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -use crate::{Backend, VerificationRequest, ViperBackendConfig}; -use log::info; +use crate::{Backend, ServerMessage, VerificationRequest, ViperBackendConfig}; +use futures::{lock, stream::Stream}; +use log::{debug, info}; use once_cell::sync::Lazy; use prusti_utils::{ config, report::log::{report, to_legal_file_name}, Stopwatch, }; -use std::{fs::create_dir_all, path::PathBuf}; +use std::{ + fs::create_dir_all, + path::PathBuf, + sync::{self, mpsc, Arc}, + thread, +}; use viper::{ - smt_manager::SmtManager, Cache, VerificationBackend, VerificationContext, VerificationResult, VerificationResultKind + smt_manager::SmtManager, Cache, PersistentCache, VerificationBackend, VerificationContext, + VerificationResult, VerificationResultKind, Viper, }; +enum ServerRequest { + Verification(VerificationRequest), + SaveCache, +} + +struct ThreadJoin { + handle: Option>, +} + +// we join the thread after dropping the sender for the ServerRequests, so +// that the verification thread actually terminates +impl Drop for ThreadJoin { + fn drop(&mut self) { + self.handle.take().unwrap().join().unwrap(); + } +} + +pub struct VerificationRequestProcessing { + mtx_rx_servermsg: lock::Mutex>, + mtx_tx_verreq: sync::Mutex>, + // mtx_tx_verreq has to be dropped before thread_join + #[allow(dead_code)] + thread_join: ThreadJoin, +} + +impl Default for VerificationRequestProcessing { + fn default() -> Self { + Self::new() + } +} + +/// A structure that lives for all the requests and has a single thread working on all the +/// requests sequentially. +/// On reception of a verification request, we send it through a channel to the already running +/// thread. +impl VerificationRequestProcessing { + pub fn new() -> Self { + let (tx_servermsg, rx_servermsg) = mpsc::channel(); + let (tx_verreq, rx_verreq) = mpsc::channel(); + let mtx_rx_servermsg = lock::Mutex::new(rx_servermsg); + let mtx_tx_verreq = sync::Mutex::new(tx_verreq); + + let handle = thread::spawn(move || verification_thread(rx_verreq, tx_servermsg)); + Self { + mtx_rx_servermsg, + mtx_tx_verreq, + thread_join: ThreadJoin { + handle: Some(handle), + }, + } + } + + pub fn verify(&self, request: VerificationRequest) -> impl Stream + '_ { + self.mtx_tx_verreq + .lock() + .unwrap() + .send(ServerRequest::Verification(request)) + .unwrap(); + // return a stream that has as last non-None message the ServerMessage::Termination + futures::stream::unfold(false, move |done: bool| async move { + if done { + return None; + } + let msg = self.mtx_rx_servermsg.lock().await.recv().unwrap(); + let mut done = false; + if let ServerMessage::Termination(_) = msg { + done = true; + } + Some((msg, done)) + }) + } + + pub fn save_cache(&self) { + self.mtx_tx_verreq + .lock() + .unwrap() + .send(ServerRequest::SaveCache) + .unwrap(); + } +} + +fn verification_thread( + rx_verreq: mpsc::Receiver, + tx_servermsg: mpsc::Sender, +) { + debug!("Verification thread started."); + // The vcx is thread local, so we need to initialize it anew for this thread + vir::init_vcx(vir::VirCtxt::new_without_tcx()); + let viper = Lazy::new(|| { + Arc::new(Viper::new_with_args( + &config::viper_home(), + config::extra_jvm_args(), + )) + }); + let viper_thread = Lazy::new(|| viper.attach_current_thread()); + let mut cache = PersistentCache::load_cache(config::cache_path()); + + while let Ok(request) = rx_verreq.recv() { + match request { + ServerRequest::Verification(verification_request) => process_verification_request( + &viper, + &viper_thread, + &mut cache, + &tx_servermsg, + verification_request, + ), + ServerRequest::SaveCache => cache.save(), + } + } + debug!("Verification thread finished."); +} + #[tracing::instrument(level = "debug", skip_all, fields(program = %request.program.get_name()))] pub fn process_verification_request<'v, 't: 'v>( + viper_arc: &Lazy, impl Fn() -> Arc>, verification_context: &'v Lazy, impl Fn() -> VerificationContext<'t>>, - request: VerificationRequest, cache: impl Cache, -) -> viper::VerificationResult { + sender: &mpsc::Sender, + mut request: VerificationRequest, +) { + // TODO: if I'm not mistaken, this currently triggers the creation of the JVM on every request, + // so this should be changed once there are actually backends that not use a JVM /* let ast_utils = verification_context.new_ast_utils(); @@ -79,12 +202,18 @@ pub fn process_verification_request<'v, 't: 'v>( let _ = build_or_dump_viper_program(); }); } - return viper::VerificationResult::Success; + // return viper::VerificationResult::Success; + sender + .send(ServerMessage::Termination( + VerificationResult::dummy_success(), + )) + .unwrap(); + return; } */ // Early return in case of cache hit if config::enable_cache() { - if let Some(result) = cache.get(hash) { + if let Some(mut result) = cache.get(hash) { info!( "Using cached result {:?} for program {}", &result, @@ -96,7 +225,9 @@ pub fn process_verification_request<'v, 't: 'v>( }); } normalization_info.denormalize_result(&mut result);*/ - return result; + result.cached = true; + sender.send(ServerMessage::Termination(result)).unwrap(); + return; } }; @@ -112,19 +243,18 @@ pub fn process_verification_request<'v, 't: 'v>( request.backend_config, ), verification_context, + Lazy::force(viper_arc), ), }; - stopwatch.start_next("backend verification"); - // let result = backend.verify(request.program); let mut result = VerificationResult { item_name: request.program.get_name().to_string(), kind: VerificationResultKind::Success, cached: false, time_ms: 0, }; - // result.kind = backend.verify(request.program, sender.clone()); - result.kind = backend.verify(request.program); + stopwatch.start_next("backend verification"); + result.kind = backend.verify(request.program, sender.clone()); result.time_ms = stopwatch.finish().as_millis(); // Don't cache Java exceptions, which might be due to misconfigured paths. @@ -137,8 +267,8 @@ pub fn process_verification_request<'v, 't: 'v>( cache.insert(hash, result.clone()); } - /*normalization_info.denormalize_result(&mut result);*/ - result + /*normalization_info.denormalize_result(&mut result.kind);*/ + sender.send(ServerMessage::Termination(result)).unwrap(); } pub fn dump_viper_program( diff --git a/prusti-server/src/server.rs b/prusti-server/src/server.rs index 3f412ffde84..2f32a20ec6f 100644 --- a/prusti-server/src/server.rs +++ b/prusti-server/src/server.rs @@ -4,13 +4,13 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -use crate::{process_verification_request, VerificationRequest}; +use crate::VerificationRequestProcessing; +use futures_util::{pin_mut, SinkExt, StreamExt}; use log::info; use once_cell::sync::Lazy; -use prusti_utils::{config, Stopwatch}; use std::{ net::{Ipv4Addr, SocketAddr}, - sync::{mpsc, Arc, Mutex}, + sync::mpsc, thread, }; use tokio::runtime::Builder; @@ -42,64 +42,81 @@ pub fn spawn_server_thread() -> SocketAddr { receiver.recv().unwrap() } +// This VerificationRequestProcessing object is starting the verification thread (for more details +// see the file process_verification.rs). +// It has to have a static lifetime because warp websockets need their closures to have a static +// lifetime and we need to access this object in them. +static VERIFICATION_REQUEST_PROCESSING: Lazy = + Lazy::new(VerificationRequestProcessing::new); + fn listen_on_port_with_address_callback(port: u16, address_callback: F) -> ! where F: FnOnce(SocketAddr), { - let stopwatch = Stopwatch::start("prusti-server", "JVM startup"); - let viper = Arc::new(Lazy::new(|| { - Viper::new_with_args(&config::viper_home(), config::extra_jvm_args()) - })); - - stopwatch.finish(); - - let cache_data = PersistentCache::load_cache(config::cache_path()); - let cache = Arc::new(Mutex::new(cache_data)); fn init_vcx(data: T) -> T { // initialise a new arena every time, so the data from previous // verification runs is deallocated vir::init_vcx(vir::VirCtxt::new_without_tcx()); data } - let build_verification_request_handler = |viper_arc: Arc>, cache| { - move |request: VerificationRequest| { - let stopwatch = Stopwatch::start("prusti-server", "attach thread to JVM"); - let viper_thread = Lazy::new(|| viper_arc.attach_current_thread()); - stopwatch.finish(); - process_verification_request(&viper_thread, request, &cache) - } - }; let json_verify = warp::path!("json" / "verify") - .and(warp::body::json()) + .and(warp::filters::ws::ws()) + // unsure why these are needed since the thread encoding the viper program is a different one .map(init_vcx) - .map(build_verification_request_handler( - viper.clone(), - cache.clone(), - )) - .map(|response| warp::reply::json(&response)); + .map(|ws: warp::filters::ws::Ws| { + ws.on_upgrade(|websocket| async { + let (mut ws_send, mut ws_recv) = websocket.split(); + let req_msg = ws_recv.next().await.unwrap().unwrap(); + let verification_request = req_msg + .to_str() + .and_then(|s: &str| serde_json::from_str(s).unwrap()) + .unwrap(); + let stream = VERIFICATION_REQUEST_PROCESSING.verify(verification_request); + pin_mut!(stream); + while let Some(server_msg) = stream.next().await { + ws_send + .send(warp::filters::ws::Message::text( + serde_json::to_string(&server_msg).unwrap(), + )) + .await + .unwrap(); + } + ws_send.close().await.unwrap(); + // receive the client close to complete the handshake + ws_recv.next().await.unwrap().unwrap(); + }) + }); let bincode_verify = warp::path!("bincode" / "verify") - .and(warp::body::bytes()) + .and(warp::filters::ws::ws()) .map(init_vcx) - .and_then(|buf: warp::hyper::body::Bytes| async move { - bincode::deserialize(&buf).map_err(|err| { - info!("request bincode body error: {}", err); - warp::reject::custom(BincodeReject(err)) + .map(|ws: warp::filters::ws::Ws| { + ws.on_upgrade(|websocket| async { + let (mut ws_send, mut ws_recv) = websocket.split(); + let req_msg = ws_recv.next().await.unwrap().unwrap(); + let verification_request = bincode::deserialize(req_msg.as_bytes()).unwrap(); + let stream = VERIFICATION_REQUEST_PROCESSING.verify(verification_request); + pin_mut!(stream); + while let Some(server_msg) = stream.next().await { + ws_send + .send(warp::filters::ws::Message::binary( + bincode::serialize(&server_msg).unwrap(), + )) + .await + .unwrap(); + } + ws_send.close().await.unwrap(); + // receive the client close to complete the handshake + ws_recv.next().await.unwrap().unwrap(); }) - }) - .map(build_verification_request_handler(viper, cache.clone())) - .map(|result| { - warp::http::Response::new( - bincode::serialize(&result).expect("could not encode verification result"), - ) }); let save_cache = warp::post() .and(warp::path("save")) .and(warp::path::end()) .map(move || { - cache.lock().unwrap().save(); + VERIFICATION_REQUEST_PROCESSING.save_cache(); warp::reply::html("Saved") }); diff --git a/prusti-server/src/server_message.rs b/prusti-server/src/server_message.rs new file mode 100644 index 00000000000..5cbdda94a2f --- /dev/null +++ b/prusti-server/src/server_message.rs @@ -0,0 +1,33 @@ +// © 2023, ETH Zurich +// +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. + +use viper::VerificationResult; + +#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)] +/// A message from a Prusti server to a Prusti client. It may contain a result +/// of a verification or anything a server might send to a client. +pub enum ServerMessage { + /// Contains the result of a verification and signals that this verification + /// has terminated. + Termination(VerificationResult), + + // /// A message created by the Viper backend with Z3 about + // /// the number of instantiations of the named quantifier. + // QuantifierInstantiation { + // q_name: String, + // insts: u64, + // pos_id: u64, + // }, + + // /// Also created by the Viper backend. The viper_quant is the expression the + // /// quantifier was translated to in silver syntax while the triggers are the + // /// triggers provided or automatically derived for this quantifier. + // QuantifierChosenTriggers { + // viper_quant: String, + // triggers: String, + // pos_id: u64, + // }, +} \ No newline at end of file diff --git a/prusti-server/src/verification_request.rs b/prusti-server/src/verification_request.rs index dc73215db10..17222b410f1 100644 --- a/prusti-server/src/verification_request.rs +++ b/prusti-server/src/verification_request.rs @@ -49,16 +49,18 @@ impl ViperBackendConfig { "--assertTimeout".to_string(), config::assert_timeout().to_string(), "--proverConfigArgs".to_string(), - // model.partial changes the default case of functions in counterexamples - // to #unspecified - format!( - "smt.qi.eager_threshold={} model.partial={}", - config::smt_qi_eager_threshold(), - config::counterexample() - ), - "--logLevel".to_string(), - "ERROR".to_string(), ]); + // model.partial changes the default case of functions in counterexamples + // to #unspecified + let mut prover_args = format!( + "smt.qi.eager_threshold={} model.partial={}", + config::smt_qi_eager_threshold(), + config::counterexample() + ); + + verifier_args.push(prover_args); + + verifier_args.extend(vec!["--logLevel".to_string(), "ERROR".to_string()]); if let Some(check_timeout) = config::check_timeout() { verifier_args.push("--checkTimeout".to_string()); diff --git a/prusti/Cargo.toml b/prusti/Cargo.toml index 6f76df4c703..040a5b6a080 100644 --- a/prusti/Cargo.toml +++ b/prusti/Cargo.toml @@ -20,6 +20,8 @@ prusti-viper = { path = "../prusti-viper" } prusti-rustc-interface = { path = "../prusti-rustc-interface" } log = { version = "0.4", features = ["release_max_level_info"] } lazy_static = "1.4.0" +serde = { version = "1.0", features = ["derive"] } +serde_json = "1.0" tracing = { path = "../tracing" } tracing-subscriber = { version = "0.3", features = ["env-filter"] } tracing-chrome = "0.7" diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index bddd1bb9fd3..af4a7eb9e8a 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -1,9 +1,14 @@ -use crate::verifier::verify; +use crate::{ + ide_helper::fake_error::fake_error, + verifier::verify, +}; use mir_state_analysis::test_free_pcs; use prusti_utils::config; use prusti_interface::{ + data::VerificationTask, environment::{mir_storage, Environment}, specs::{self, cross_crate::CrossCrateSpecs, is_spec_fn}, + PrustiError, }; use prusti_rustc_interface::{ borrowck::consumers, @@ -22,6 +27,7 @@ use prusti_rustc_interface::{ ty::TyCtxt, }, session::{EarlyErrorHandler, Session}, + span::DUMMY_SP, }; #[derive(Default)] @@ -161,20 +167,46 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls { } } CrossCrateSpecs::import_export_cross_crate(&mut env, &mut def_spec); - if !config::no_verify() { - /* - if config::test_free_pcs() { - for proc_id in env.get_annotated_procedures_and_types().0.iter() { - let name = env.name.get_unique_item_name(*proc_id); - println!("Calculating FPCS for: {name}"); + // if !config::no_verify() { + // /* + // if config::test_free_pcs() { + // for proc_id in env.get_annotated_procedures_and_types().0.iter() { + // let name = env.name.get_unique_item_name(*proc_id); + // println!("Calculating FPCS for: {name}"); + + // let current_procedure = env.get_procedure(*proc_id); + // let mir = current_procedure.get_mir_rc(); + // test_free_pcs(&mir, tcx); + // } + // } else {*/ + // verify(env, def_spec); + // //} + // } + + // TODO: can we replace `get_annotated_procedures` with information + // that is already in `def_spec`? + let (annotated_procedures, types) = env.get_annotated_procedures_and_types(); - let current_procedure = env.get_procedure(*proc_id); - let mir = current_procedure.get_mir_rc(); - test_free_pcs(&mir, tcx); - } - } else {*/ - verify(env, def_spec); - //} + // if config::show_ide_info() && !config::no_verify() { + // let compiler_info = + // compiler_info::IdeInfo::collect(&env, &annotated_procedures, &def_spec); + // let out = serde_json::to_string(&compiler_info).unwrap(); + // PrustiError::message(format!("compilerInfo{out}"), DUMMY_SP.into()) + // .emit(&env.diagnostic); + // } + // as long as we have to throw a fake error we need to check this + let is_primary_package = std::env::var("CARGO_PRIMARY_PACKAGE").is_ok(); + + // collect and output Information used by IDE: + if !config::no_verify() { + let verification_task = VerificationTask { + procedures: annotated_procedures, + types, + }; + verify(env, def_spec, verification_task); + } else if !config::no_verify() && is_primary_package { + // add a fake error, reason explained in issue #1261 + fake_error(&env); } }); diff --git a/prusti/src/driver.rs b/prusti/src/driver.rs index d606454aa9a..02a8cdac644 100644 --- a/prusti/src/driver.rs +++ b/prusti/src/driver.rs @@ -12,6 +12,7 @@ mod arg_value; mod callbacks; mod verifier; +mod ide_helper; use arg_value::arg_value; use callbacks::PrustiCompilerCalls; diff --git a/prusti/src/ide_helper/fake_error.rs b/prusti/src/ide_helper/fake_error.rs new file mode 100644 index 00000000000..d33919cdaa3 --- /dev/null +++ b/prusti/src/ide_helper/fake_error.rs @@ -0,0 +1,16 @@ +use prusti_interface::environment::Environment; +use prusti_rustc_interface::{errors::MultiSpan, span::DUMMY_SP}; + +/// This error will be thrown when skipping verification (which is done +/// when we just collect information for prusti-assistant), because then +/// a successful result will be cached and subsequent actual verifications succeed +/// (see issue #1261) +pub fn fake_error(env: &Environment) { + let sp = MultiSpan::from_span(DUMMY_SP); + let message = String::from("[Prusti: FakeError]"); + let help = None; + let notes = []; + + env.diagnostic + .span_err_with_help_and_notes(sp, &message, &help, ¬es); +} \ No newline at end of file diff --git a/prusti/src/verifier.rs b/prusti/src/verifier.rs index 1b4f37267e5..6834ed4f685 100644 --- a/prusti/src/verifier.rs +++ b/prusti/src/verifier.rs @@ -10,18 +10,22 @@ use prusti_interface::{ use prusti_rustc_interface::errors::MultiSpan; #[tracing::instrument(name = "prusti::verify", level = "debug", skip(env))] -pub fn verify(env: Environment<'_>, def_spec: typed::DefSpecificationMap) { +pub fn verify<'tcx>( + env: Environment<'tcx>, + def_spec: typed::DefSpecificationMap, + verification_task: VerificationTask<'tcx>, +) { if env.diagnostic.has_errors() { warn!("The compiler reported an error, so the program will not be verified."); } else { debug!("Prepare verification task..."); - // TODO: can we replace `get_annotated_procedures` with information - // that is already in `def_spec`? - let (annotated_procedures, types) = env.get_annotated_procedures_and_types(); - let verification_task = VerificationTask { - procedures: annotated_procedures, - types, - }; + // // TODO: can we replace `get_annotated_procedures` with information + // // that is already in `def_spec`? + // let (annotated_procedures, types) = env.get_annotated_procedures_and_types(); + // let verification_task = VerificationTask { + // procedures: annotated_procedures, + // types, + // }; debug!("Verification task: {:?}", &verification_task); user::message(format!( @@ -53,9 +57,9 @@ pub fn verify(env: Environment<'_>, def_spec: typed::DefSpecificationMap) { ); let program = request.program; - let results = prusti_server::verify_programs(vec![program]); - println!("verification results: {results:?}"); - if !results.iter().all(|(_, r)| matches!(r.kind, viper::VerificationResultKind::Success)) { + let result = prusti_server::verify_programs(&env.diagnostic, vec![program]); + println!("verification result: {result:?}"); + if !matches!(result, VerificationResult::Success) { // TODO: This will be unnecessary if diagnostic errors are emitted // earlier, it's useful for now to ensure that Prusti returns an // error code when verification fails diff --git a/viper-sys/build.rs b/viper-sys/build.rs index 6d8dfd70785..75438f39952 100644 --- a/viper-sys/build.rs +++ b/viper-sys/build.rs @@ -158,6 +158,19 @@ fn main() { java_class!("viper.silver.reporter.NoopReporter$", vec![ object_getter!(), ]), + java_class!("viper.silver.reporter.PollingReporter", vec![ + constructor!("(Ljava/lang/String;Lviper/silver/reporter/Reporter;)V"), + method!("hasNewMessage"), + method!("getNewMessage"), + ]), + // java_class!("viper.silver.reporter.QuantifierChosenTriggersMessage", vec![ + // method!("quantifier"), + // method!("triggers_string"), + // ]), + // java_class!("viper.silver.reporter.QuantifierInstantiationsMessage", vec![ + // method!("quantifier"), + // method!("instantiations"), + // ]), java_class!("viper.silver.verifier.Verifier", vec![ method!("name"), method!("buildVersion"), @@ -165,6 +178,7 @@ fn main() { method!("start"), method!("stop"), method!("verify"), + method!("reporter"), ]), java_class!("viper.silver.frontend.DefaultStates", vec![ method!("ConsistencyCheck"), diff --git a/viper/src/lib.rs b/viper/src/lib.rs index 747f7fc1261..a46f8f0b7a1 100644 --- a/viper/src/lib.rs +++ b/viper/src/lib.rs @@ -10,11 +10,13 @@ mod ast_factory; mod ast_utils; pub mod errors; -mod jni_utils; +// used by prusti-server +pub mod jni_utils; #[macro_use] pub mod utils; mod cache; -mod java_exception; +// used by prusti-server +pub mod java_exception; pub mod silicon_counterexample; pub mod smt_manager; mod verification_backend; diff --git a/viper/src/verification_context.rs b/viper/src/verification_context.rs index 2537431c837..09d44ac535a 100644 --- a/viper/src/verification_context.rs +++ b/viper/src/verification_context.rs @@ -25,6 +25,10 @@ impl<'a> VerificationContext<'a> { VerificationContext { env: env_guard } } + pub fn env(&self) -> &AttachGuard<'a> { + &self.env + } + pub fn new_ast_factory(&self) -> AstFactory { AstFactory::new(&self.env) } diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs index 467898241a8..f3d17bac8ea 100644 --- a/viper/src/verifier.rs +++ b/viper/src/verifier.rs @@ -42,7 +42,7 @@ impl<'a> Verifier<'a> { let frontend_wrapper = silver::frontend::SilFrontend::with(env); let frontend_instance = jni.unwrap_result(env.with_local_frame(16, || { - let reporter = if let Some(real_report_path) = report_path { + let pass_through_reporter = if let Some(real_report_path) = report_path { jni.unwrap_result(silver::reporter::CSVReporter::with(env).new( jni.new_string("csv_reporter"), jni.new_string(real_report_path.to_str().unwrap()), @@ -51,6 +51,11 @@ impl<'a> Verifier<'a> { jni.unwrap_result(silver::reporter::NoopReporter_object::with(env).singleton()) }; + let reporter = jni.unwrap_result( + silver::reporter::PollingReporter::with(env) + .new(jni.new_string("polling_reporter"), pass_through_reporter), + ); + let debug_info = jni.new_seq(&[]); let backend_unwrapped = Self::instantiate_verifier(backend, env, reporter, debug_info); @@ -405,6 +410,10 @@ impl<'a> Verifier<'a> { } }) } + + pub fn verifier_instance(&self) -> &JObject<'a> { + &self.verifier_instance + } } impl<'a> Drop for Verifier<'a> {