[WIP] Various IDE improvements and new features

prusti-common/src/vir/program_normalization.rs

@@ -7,8 +7,9 @@
 use crate::vir::{program::Program, Position};
 use log::{debug, trace};
 use rustc_hash::{FxHashMap, FxHashSet};
-use viper::VerificationResult;
+use viper::VerificationResultKind;
 
+#[derive(Clone)]
 pub enum NormalizationInfo {
     LegacyProgram { original_position_ids: Vec<u64> },
     LowProgram,
@@ -80,7 +81,7 @@ impl NormalizationInfo {
         )
     }
 
-    /// Denormalize the verification result.
+    /// Denormalize the program
     pub fn denormalize_program(&self, program: &mut Program) {
         match program {
             Program::Low(_) => debug!("No denormalization is done for vir::low programs."),
@@ -101,8 +102,8 @@ impl NormalizationInfo {
     }
 
     /// Denormalize a verification result.
-    pub fn denormalize_result(&self, result: &mut VerificationResult) {
-        if let VerificationResult::Failure(ref mut ver_errors) = result {
+    pub fn denormalize_result(&self, result: &mut VerificationResultKind) {
+        if let VerificationResultKind::Failure(ref mut ver_errors) = result {
             ver_errors.iter_mut().for_each(|ver_error| {
                 if let Some(pos) = ver_error.pos_id.as_mut() {
                     self.denormalize_position_string(pos);

prusti-interface/src/environment/diagnostic.rs

@@ -78,6 +78,11 @@ impl<'tcx> EnvDiagnostic<'tcx> {
         diagnostic.buffer(&mut self.warn_buffer.borrow_mut());
     }
 
+    /// Emits a note
+    pub fn span_note<S: Into<MultiSpan> + Clone>(&self, sp: S, msg: &str) {
+        self.tcx.sess.span_note_without_error(sp, msg);
+    }
+
     /// Returns true if an error has been emitted
     pub fn has_errors(&self) -> bool {
         self.tcx.sess.has_errors().is_some()

prusti-interface/src/prusti_error.rs

@@ -40,6 +40,7 @@ pub enum PrustiErrorKind {
     Warning,
     /// A warning which is only shown if at least one error is emitted.
     WarningOnError,
+    Message,
 }
 
 impl PartialOrd for PrustiError {
@@ -146,6 +147,14 @@ impl PrustiError {
         error
     }
 
+    /// Report a message
+    pub fn message<S: ToString>(message: S, span: MultiSpan) -> Self {
+        check_message(message.to_string());
+        let mut msg = PrustiError::new(message.to_string(), span);
+        msg.kind = PrustiErrorKind::Message;
+        msg
+    }
+
     /// Set that this Prusti error should be reported as a warning to the user
     pub fn set_warning(&mut self) {
         self.kind = PrustiErrorKind::Warning;
@@ -203,6 +212,7 @@ impl PrustiError {
                 &self.help,
                 &self.notes,
             ),
+            PrustiErrorKind::Message => env_diagnostic.span_note(*self.span, &self.message),
         };
     }
 

prusti-server/Cargo.toml

@@ -19,6 +19,7 @@ doctest = false
 [dependencies]
 log = { version = "0.4", features = ["release_max_level_info"] }
 viper = { path = "../viper" }
+viper-sys = { path = "../viper-sys" }
 prusti-common = { path = "../prusti-common" }
 prusti-utils = { path = "../prusti-utils" }
 env_logger = "0.10"
@@ -27,9 +28,17 @@ bincode = "1.0"
 url = "2.2.2"
 num_cpus = "1.14"
 serde = { version = "1.0", features = ["derive"] }
+serde_json = { version = "1.0" }
+tokio = "1.20"
+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"
+once_cell = "1.17.0"
 reqwest = { version = "0.11", default-features = false, features = ["json", "rustls-tls"] }
 warp = "0.3"
-tokio = "1.20"
 rustc-hash = "1.1.0"
 
 [dev-dependencies]

prusti-server/src/client.rs

@@ -4,58 +4,76 @@
 // 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_common::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<S: ToString>(server_address: S) -> Result<Self, ParseError> {
+    pub async fn verify<S: ToString>(
+        server_address: S,
+        request: VerificationRequest,
+    ) -> impl Stream<Item = ServerMessage> {
+        // TODO: do proper error handling
         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<VerificationResult> {
+        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<Message, Error>| 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 })
     }
 }

prusti-server/src/lib.rs

@@ -9,11 +9,13 @@
 mod client;
 mod process_verification;
 mod server;
+mod server_message;
 mod verification_request;
 
 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.