Merge pull request #64: LSP server fix & animations

Fixes concurrency issues in the LSP server and adds animations for VSCode

Author: Philipp15b

src/main.rs

@@ -856,6 +856,10 @@ fn verify_files_main(
         let (name, mut verify_unit) = verify_unit.enter_with_name();
 
         limits_ref.check_limits()?;
+
+        // Set the current unit as ongoing
+        server.set_ongoing_unit(verify_unit.span)?;
+
         // 4. Desugaring: transforming spec calls to procs
         verify_unit.desugar_spec_calls(&mut tcx, name.to_string())?;
 
@@ -933,10 +937,6 @@ fn verify_files_main(
             &slice_vars,
         )?;
 
-        server
-            .handle_vc_check_result(name, verify_unit.span, &mut result, &mut translate)
-            .map_err(VerifyError::ServerError)?;
-
         if options.debug_options.z3_trace {
             info!("Z3 tracing output will be written to `z3.log`.");
         }
@@ -956,6 +956,12 @@ fn verify_files_main(
             ProveResult::Proof => num_proven += 1,
             ProveResult::Counterexample | ProveResult::Unknown(_) => num_failures += 1,
         }
+
+        limits_ref.check_limits()?;
+
+        server
+            .handle_vc_check_result(name, verify_unit.span, &mut result, &mut translate)
+            .map_err(VerifyError::ServerError)?;
     }
 
     if !options.lsp_options.language_server {

src/resource_limits.rs

@@ -163,8 +163,19 @@ impl LimitsRef {
 
     /// Check whether the monitoring thread has indicated a timeout or an OOM.
     pub fn check_limits(&self) -> Result<(), LimitError> {
+        // Timeout flag is set to 1 by `await_with_resource_limits`, only if the hard timeout is reached.
         match self.0.done.load(Ordering::Relaxed) {
-            0 => Ok(()),
+            0 => {
+                // Normal timeout might be reached even though the hard timeout is not reached yet.
+                // Check for timeout by checking the remaining time
+                if let Some(timeout) = self.0.timeout {
+                    if Instant::now() >= timeout {
+                        self.set_error(LimitError::Timeout);
+                        return Err(LimitError::Timeout);
+                    }
+                }
+                Ok(())
+            }
             1 => Err(LimitError::Timeout),
             2 => Err(LimitError::Oom),
             _ => unreachable!(),

src/servers/cli.rs

@@ -89,6 +89,11 @@ impl Server for CliServer {
         Ok(())
     }
 
+    fn set_ongoing_unit(&mut self, _span: Span) -> Result<(), VerifyError> {
+        // Not relevant for CLI
+        Ok(())
+    }
+
     fn handle_vc_check_result<'smt, 'ctx>(
         &mut self,
         name: &SourceUnitName,
@@ -100,11 +105,6 @@ impl Server for CliServer {
         Ok(())
     }
 
-    fn handle_not_checked(&mut self, _span: Span) -> Result<(), ServerError> {
-        // Not relevant for CLI
-        Ok(())
-    }
-
     fn exit_code(&self) -> ExitCode {
         if self.has_emitted_errors {
             ExitCode::FAILURE

src/servers/lsp.rs

@@ -5,6 +5,7 @@ use std::{
     sync::{Arc, Mutex},
 };
 
+use ariadne::ReportKind;
 use crossbeam_channel::Sender;
 
 use lsp_server::{Connection, IoThreads, Message, Request, Response};
@@ -249,6 +250,40 @@ impl LspServer {
         Ok(())
     }
 
+    /// Convert `VerifyResult::Todo` and `VerifyResult::Verifying` statuses to `VerifyResult::Timeout`, send the results to the client and emit diagnostics for them.
+    fn handle_timeout_for_results(&mut self) -> Result<(), ServerError> {
+        let mut diagnostics: Vec<Diagnostic> = Vec::new();
+
+        // Transform results and collect diagnostics for timed out procedures
+        for (span, status) in &mut self.statuses {
+            match status {
+                VerifyResult::Ongoing => {
+                    diagnostics.push(
+                        Diagnostic::new(ReportKind::Error, *span)
+                            .with_message("Timed out while verifying this procedure"),
+                    );
+                    *status = VerifyResult::Timeout;
+                }
+                VerifyResult::Todo => {
+                    diagnostics.push(
+                        Diagnostic::new(ReportKind::Warning, *span)
+                            .with_message("Skipped this procedure due to timeout"),
+                    );
+                    *status = VerifyResult::Timeout;
+                }
+                _ => {}
+            }
+        }
+
+        // Add the collected diagnostics to the server
+        for diagnostic in diagnostics {
+            self.add_diagnostic(diagnostic)?;
+        }
+
+        self.publish_verify_statuses()?;
+        Ok(())
+    }
+
     fn clear_file_information(&mut self, file_id: &FileId) -> Result<(), ServerError> {
         if let Some(diag) = self.diagnostics.get_mut(file_id) {
             diag.clear();
@@ -317,6 +352,15 @@ impl Server for LspServer {
 
     fn register_source_unit(&mut self, span: Span) -> Result<(), VerifyError> {
         self.statuses.insert(span, VerifyResult::Todo);
+        self.publish_verify_statuses()
+            .map_err(VerifyError::ServerError)?;
+        Ok(())
+    }
+
+    fn set_ongoing_unit(&mut self, span: Span) -> Result<(), VerifyError> {
+        self.statuses.insert(span, VerifyResult::Ongoing);
+        self.publish_verify_statuses()
+            .map_err(VerifyError::ServerError)?;
         Ok(())
     }
 
@@ -335,13 +379,6 @@ impl Server for LspServer {
         self.publish_verify_statuses()?;
         Ok(())
     }
-
-    fn handle_not_checked(&mut self, span: Span) -> Result<(), ServerError> {
-        let prev = self.statuses.insert(span, VerifyResult::Unknown);
-        assert!(prev.is_some());
-        self.publish_verify_statuses()?;
-        Ok(())
-    }
 }
 
 /// A type alias representing an asynchronous closure that returns a `Result<(), VerifyError>`.
@@ -440,29 +477,29 @@ async fn handle_verify_request(
     };
 
     let result = verify(&[file_id]).await;
-    let res = match &result {
-        Ok(_) => Response::new_ok(id, Value::Null),
-        Err(err) => Response::new_err(id, 0, format!("{}", err)),
+
+    let response = match result {
+        Ok(()) => Response::new_ok(id.clone(), Value::Null),
+        Err(err) => match err {
+            VerifyError::Diagnostic(diagnostic) => {
+                server.lock().unwrap().add_diagnostic(diagnostic)?;
+                Response::new_ok(id.clone(), Value::Null)
+            }
+            VerifyError::Interrupted | VerifyError::LimitError(_) => {
+                server
+                    .lock()
+                    .unwrap()
+                    .handle_timeout_for_results()
+                    .map_err(VerifyError::ServerError)?;
+                Response::new_ok(id.clone(), Value::Null)
+            }
+            _ => Response::new_err(id, 0, format!("{}", err)),
+        },
     };
+
     sender
-        .send(Message::Response(res))
+        .send(Message::Response(response))
         .map_err(|e| VerifyError::ServerError(e.into()))?;
-    match result {
-        Ok(()) => {}
-        Err(VerifyError::Diagnostic(diagnostic)) => {
-            server.lock().unwrap().add_diagnostic(diagnostic)?;
-        }
-        Err(VerifyError::Interrupted) | Err(VerifyError::LimitError(_)) => {
-            // If the verification is interrupted or a limit is reached before the verification starts, no verification statuses are published yet.
-            // In this case, the client needs to be notified about the registered source units that are not checked yet (marked with VerifyResult::Todo).
-            // This acts as a fallback mechanism for this case.
-            server
-                .lock()
-                .unwrap()
-                .publish_verify_statuses()
-                .map_err(VerifyError::ServerError)?;
-        }
-        Err(err) => Err(err)?,
-    }
+
     Ok(())
 }

src/servers/mod.rs

@@ -33,9 +33,11 @@ pub type ServerError = Box<dyn Error + Send + Sync>;
 pub enum VerifyResult {
     // If the verification is not done yet the result is Todo
     Todo,
+    Ongoing,
     Verified,
     Failed,
     Unknown,
+    Timeout,
 }
 
 impl VerifyResult {
@@ -71,6 +73,9 @@ pub trait Server: Send {
     /// Register a source unit span with the server.
     fn register_source_unit(&mut self, span: Span) -> Result<(), VerifyError>;
 
+    /// Register a verify unit span as the current verifying with the server.
+    fn set_ongoing_unit(&mut self, span: Span) -> Result<(), VerifyError>;
+
     /// Send a verification status message to the client (a custom notification).
     fn handle_vc_check_result<'smt, 'ctx>(
         &mut self,
@@ -80,9 +85,6 @@ pub trait Server: Send {
         translate: &mut TranslateExprs<'smt, 'ctx>,
     ) -> Result<(), ServerError>;
 
-    /// Sends an unknown verification result for the not checked proc with the given span.
-    fn handle_not_checked(&mut self, span: Span) -> Result<(), ServerError>;
-
     /// Return an exit code for the process.
     ///
     /// Default implementation returns `ExitCode::SUCCESS`.

src/servers/test.rs

@@ -64,6 +64,10 @@ impl Server for TestServer {
         Ok(())
     }
 
+    fn set_ongoing_unit(&mut self, _span: Span) -> Result<(), VerifyError> {
+        Ok(())
+    }
+
     fn handle_vc_check_result<'smt, 'ctx>(
         &mut self,
         _name: &SourceUnitName,
@@ -75,9 +79,4 @@ impl Server for TestServer {
             .insert(span, VerifyResult::from_prove_result(&result.prove_result));
         Ok(())
     }
-
-    fn handle_not_checked(&mut self, span: Span) -> Result<(), ServerError> {
-        self.statuses.insert(span, VerifyResult::Unknown);
-        Ok(())
-    }
 }

src/slicing/transform_test.rs

@@ -1,7 +1,5 @@
 //! *Prove* using the SMT solver that our transformations are correct.
 
-use std::time::{Duration, Instant};
-
 use itertools::Itertools;
 use z3rro::{
     model::SmtEval,
@@ -109,8 +107,7 @@ fn prove_equiv(
     let tcx = &transform_tcx.tcx;
     let builder = ExprBuilder::new(Span::dummy_span());
 
-    let deadline = Instant::now() + Duration::from_millis(1);
-    let mut vcgen = Vcgen::new(tcx, &LimitsRef::new(Some(deadline), None), None);
+    let mut vcgen = Vcgen::new(tcx, &LimitsRef::new(None, None), None);
     let stmt1_vc = vcgen
         .vcgen_stmts(stmt1, transform_tcx.post.clone())
         .unwrap();

src/smt/pretty_model.rs

@@ -1,11 +1,6 @@
 //! Pretty-printing an SMT model.
 
-use std::{
-    collections::BTreeMap,
-    fmt::Display,
-    rc::Rc,
-    time::{Duration, Instant},
-};
+use std::{collections::BTreeMap, fmt::Display, rc::Rc};
 
 use itertools::Itertools;
 use z3rro::model::{InstrumentedModel, ModelConsistency, SmtEvalError};
@@ -72,15 +67,9 @@ pub fn pretty_vc_value<'smt, 'ctx>(
         );
         let mut res = subst_expr;
 
-        // This deadline is not actually used. It is used to create a dummy [`LimitsRef`] object below
-        let deadline = Instant::now() + Duration::from_millis(1);
-
         // The limit error is not handled here, therefore discard the result
-        let _ = apply_subst(
-            translate.ctx.tcx(),
-            &mut res,
-            &LimitsRef::new(Some(deadline), None),
-        );
+        apply_subst(translate.ctx.tcx(), &mut res, &LimitsRef::new(None, None)).unwrap();
+
         res
     };