Merge PR #60: VSCode Extension Timeout Handling

Cargo.toml

@@ -50,6 +50,7 @@ serde = "1.0.197"
 jani = { path = "./jani" }
 itertools = "0.13.0"
 stacker = "0.1.15"
+crossbeam-channel = "0.5.14"
 shlex = "1.3.0"
 clap = { version = "4.5.23", features = ["derive", "string"] }
 

src/driver.rs

@@ -335,19 +335,27 @@ impl SourceUnit {
     }
 
     /// Explain high-level verification conditions.
-    pub fn explain_vc(&self, tcx: &TyCtx, server: &mut dyn Server) -> Result<(), VerifyError> {
+    pub fn explain_vc(
+        &self,
+        tcx: &TyCtx,
+        server: &mut dyn Server,
+        limits_ref: &LimitsRef,
+    ) -> Result<(), VerifyError> {
         let explanation = match self {
-            SourceUnit::Decl(decl) => explain_decl_vc(tcx, decl),
+            SourceUnit::Decl(decl) => explain_decl_vc(tcx, decl, limits_ref),
             SourceUnit::Raw(block) => {
                 let builder = ExprBuilder::new(Span::dummy_span());
                 let post = builder.top_lit(tcx.spec_ty());
-                explain_raw_vc(tcx, block, post, Direction::Down).map(Some)
+                explain_raw_vc(tcx, block, post, Direction::Down, limits_ref).map(Some)
             }
         };
         match explanation {
             Ok(Some(explanation)) => server.add_vc_explanation(explanation),
             Ok(None) => Ok(()),
-            Err(diagnostic) => server.add_diagnostic(diagnostic.with_kind(ReportKind::Warning)),
+            Err(VerifyError::Diagnostic(diagnostic)) => {
+                server.add_diagnostic(diagnostic.with_kind(ReportKind::Warning))
+            }
+            Err(err) => Err(err),
         }
     }
 
@@ -539,17 +547,18 @@ impl QuantVcUnit {
             let mut unfolder = Unfolder::new(limits_ref.clone(), &smt_ctx);
             unfolder.visit_expr(&mut self.expr)
         } else {
-            apply_subst(tcx, &mut self.expr);
+            apply_subst(tcx, &mut self.expr, limits_ref)?;
             Ok(())
         }
     }
 
     /// Apply quantitative quantifier elimination.
-    pub fn qelim(&mut self, tcx: &mut TyCtx) {
+    pub fn qelim(&mut self, tcx: &mut TyCtx, limits_ref: &LimitsRef) -> Result<(), VerifyError> {
         let mut qelim = Qelim::new(tcx);
         qelim.qelim(self);
         // Apply/eliminate substitutions again
-        apply_subst(tcx, &mut self.expr);
+        apply_subst(tcx, &mut self.expr, limits_ref)?;
+        Ok(())
     }
 
     /// Trace some statistics about this vc expression.
@@ -951,7 +960,12 @@ impl<'ctx> SmtVcCheckResult<'ctx> {
             ProveResult::Unknown(reason) => {
                 server.add_diagnostic(
                     Diagnostic::new(ReportKind::Error, span)
-                        .with_message(format!("Unknown result: {}", reason)),
+                        .with_message(format!("Unknown result: SMT solver returned {}", reason))
+                        .with_note(
+                            "For many queries, the query to the SMT solver is inherently undecidable. \
+                             There are various tricks to help the SMT solver, which can be found in the Caesar documentation:
+                             https://www.caesarverifier.org/docs/caesar/debugging"
+                        ),
                 )?;
             }
         }

src/main.rs

@@ -11,7 +11,6 @@ use std::{
     path::PathBuf,
     process::ExitCode,
     sync::{Arc, Mutex},
-    time::{Duration, Instant},
 };
 
 use crate::{
@@ -23,13 +22,13 @@ use crate::{
     tyctx::TyCtx,
     vc::vcgen::Vcgen,
 };
-use ast::{Diagnostic, FileId};
+use ast::{DeclKind, Diagnostic, FileId};
 use clap::{Args, Parser, ValueEnum};
 use driver::{Item, SourceUnit, VerifyUnit};
 use intrinsic::{annotations::init_calculi, distributions::init_distributions, list::init_lists};
 use proof_rules::init_encodings;
 use resource_limits::{await_with_resource_limits, LimitError, LimitsRef};
-use servers::{CliServer, LspServer, Server, ServerError};
+use servers::{run_lsp_server, CliServer, LspServer, Server, ServerError};
 use slicing::init_slicing;
 use thiserror::Error;
 use timing::DispatchBuilder;
@@ -314,7 +313,7 @@ async fn main() -> ExitCode {
     if !options.lsp_options.language_server {
         run_cli(options).await
     } else {
-        run_server(&options).await
+        run_server(options).await
     }
 }
 
@@ -372,27 +371,33 @@ async fn run_cli(options: Options) -> ExitCode {
     }
 }
 
-async fn run_server(options: &Options) -> ExitCode {
-    let (mut server, _io_threads) = LspServer::connect_stdio(options);
+async fn run_server(options: Options) -> ExitCode {
+    let (mut server, _io_threads) = LspServer::connect_stdio(&options);
     server.initialize().unwrap();
-    let res = server.run_server(|server, user_files| {
-        let limits_ref = LimitsRef::new(Some(
-            Instant::now() + Duration::from_secs(options.rlimit_options.timeout),
-        ));
-        let res = verify_files_main(options, limits_ref, server, user_files);
-        match res {
-            Ok(_) => Ok(()),
-            Err(VerifyError::Diagnostic(diag)) => {
-                server.add_diagnostic(diag).unwrap();
-                Ok(())
+    let server = Arc::new(Mutex::new(server));
+    let options = Arc::new(options);
+
+    let res = run_lsp_server(server.clone(), |user_files| {
+        let server: Arc<Mutex<dyn Server>> = server.clone();
+        let options = options.clone();
+        Box::pin(async move {
+            let res = verify_files(&options, &server, user_files.to_vec()).await;
+            match res {
+                Ok(_) => Ok(()),
+                Err(VerifyError::Diagnostic(diag)) => {
+                    server.lock().unwrap().add_diagnostic(diag).unwrap();
+                    Ok(())
+                }
+                Err(err) => Err(err),
             }
-            Err(err) => Err(err),
-        }
-    });
+        })
+    })
+    .await;
+
     match res {
         Ok(()) => ExitCode::SUCCESS,
         Err(VerifyError::Diagnostic(diag)) => {
-            server.add_diagnostic(diag).unwrap();
+            server.lock().unwrap().add_diagnostic(diag).unwrap();
             ExitCode::FAILURE
         }
         Err(err) => panic!("{}", err), // TODO
@@ -589,11 +594,26 @@ fn verify_files_main(
         }
     }
 
+    // Register all relevant source units with the server
+    for source_unit in &mut source_units {
+        let source_unit = source_unit.enter();
+
+        match *source_unit {
+            SourceUnit::Decl(ref decl) => {
+                // only register procs since we do not check any other decls
+                if let DeclKind::ProcDecl(proc_decl) = decl {
+                    server.register_source_unit(proc_decl.borrow().span)?;
+                }
+            }
+            SourceUnit::Raw(ref block) => server.register_source_unit(block.span)?,
+        }
+    }
+
     // explain high-level HeyVL if requested
     if options.lsp_options.explain_vc {
         for source_unit in &mut source_units {
             let source_unit = source_unit.enter();
-            source_unit.explain_vc(&tcx, server)?;
+            source_unit.explain_vc(&tcx, server, &limits_ref)?;
         }
     }
 
@@ -640,6 +660,7 @@ fn verify_files_main(
     for verify_unit in &mut verify_units {
         let (name, mut verify_unit) = verify_unit.enter_with_name();
 
+        limits_ref.check_limits()?;
         // 4. Desugaring: transforming spec calls to procs
         verify_unit.desugar_spec_calls(&mut tcx, name.to_string())?;
 
@@ -656,7 +677,7 @@ fn verify_files_main(
             .lsp_options
             .explain_core_vc
             .then(|| VcExplanation::new(verify_unit.direction));
-        let mut vcgen = Vcgen::new(&tcx, explanations);
+        let mut vcgen = Vcgen::new(&tcx, &limits_ref, explanations);
         let mut vc_expr = verify_unit.vcgen(&mut vcgen)?;
         if let Some(explanation) = vcgen.explanation {
             server.add_vc_explanation(explanation)?;
@@ -667,7 +688,7 @@ fn verify_files_main(
 
         // 8. Quantifier elimination
         if !options.opt_options.no_qelim {
-            vc_expr.qelim(&mut tcx);
+            vc_expr.qelim(&mut tcx, &limits_ref)?;
         }
 
         // In-between, gather some stats about the vc expression
@@ -730,6 +751,7 @@ fn verify_files_main(
             ProveResult::Unknown(ReasonUnknown::Interrupted) => {
                 return Err(VerifyError::Interrupted)
             }
+
             ProveResult::Unknown(ReasonUnknown::Timeout) => return Err(LimitError::Timeout.into()),
             _ => {}
         }

src/opt/unfolder.rs

@@ -60,8 +60,8 @@ pub struct Unfolder<'smt, 'ctx> {
 impl<'smt, 'ctx> Unfolder<'smt, 'ctx> {
     pub fn new(limits_ref: LimitsRef, ctx: &'smt SmtCtx<'ctx>) -> Self {
         Unfolder {
-            limits_ref,
-            subst: Subst::new(ctx.tcx()),
+            limits_ref: limits_ref.clone(),
+            subst: Subst::new(ctx.tcx(), &limits_ref),
             translate: TranslateExprs::new(ctx),
             prover: Prover::new(ctx.ctx()),
         }

src/servers/cli.rs

@@ -77,6 +77,11 @@ impl Server for CliServer {
         Ok(())
     }
 
+    fn register_source_unit(&mut self, _span: Span) -> Result<(), VerifyError> {
+        // Not relevant for CLI
+        Ok(())
+    }
+
     fn handle_vc_check_result<'smt, 'ctx>(
         &mut self,
         name: &SourceUnitName,
@@ -87,6 +92,11 @@ impl Server for CliServer {
         result.print_prove_result(self, translate, name);
         Ok(())
     }
+
+    fn handle_not_checked(&mut self, _span: Span) -> Result<(), ServerError> {
+        // Not relevant for CLI
+        Ok(())
+    }
 }
 
 fn print_diagnostic(mut files: &Files, diagnostic: Diagnostic) -> io::Result<()> {