Implement soundness checking & corresponding diagnostics in lsp

src/driver/commands/refinement.rs

@@ -24,6 +24,7 @@ use crate::{
         quant_proof::{lower_quant_prove_task, QuantVcProveTask},
         smt_proof::run_smt_prove_task,
     },
+    proof_rules::calculus::ProcSoundness,
     resource_limits::{LimitError, LimitsRef},
     servers::SharedServer,
 };
@@ -163,6 +164,7 @@ async fn verify_entailment(
             server,
             slice_vars,
             vc_is_valid,
+            &ProcSoundness::default(),
         )?;
 
         // Handle reasons to stop the verifier.

src/driver/commands/verify.rs

@@ -22,6 +22,7 @@ use crate::{
         quant_proof::lower_quant_prove_task,
         smt_proof::{run_smt_prove_task, set_global_z3_params},
     },
+    proof_rules::calculus::get_soundness_map,
     resource_limits::{await_with_resource_limits, LimitError, LimitsRef},
     servers::{Server, SharedServer},
 };
@@ -186,6 +187,8 @@ fn verify_files_main(
     // based on the provided calculus annotations
     module.check_calculus_rules(&mut tcx)?;
 
+    let soundness_map = get_soundness_map(&mut module, &mut tcx);
+
     // Desugar encodings from source units.
     module.apply_encodings(&mut tcx, server)?;
 
@@ -215,7 +218,14 @@ fn verify_files_main(
         .items
         .into_iter()
         .flat_map(|item| {
-            item.flat_map(|unit| CoreVerifyTask::from_source_unit(unit, &mut depgraph))
+            let soundness_blame = soundness_map.get(item.name()).cloned().unwrap_or_default();
+            item.flat_map(|unit| {
+                let core_verify_task = CoreVerifyTask::from_source_unit(unit, &mut depgraph);
+                core_verify_task.map(|mut task| {
+                    task.proc_soundness = soundness_blame.clone();
+                    task
+                })
+            })
         })
         .collect();
 
@@ -254,6 +264,8 @@ fn verify_files_main(
         // (depending on options).
         let vc_is_valid = lower_quant_prove_task(options, &limits_ref, &mut tcx, name, vc_expr)?;
 
+        let soundness_blame = &verify_unit.proc_soundness;
+
         // Running the SMT prove task: translating to Z3, running the solver.
         let result = run_smt_prove_task(
             options,
@@ -264,6 +276,7 @@ fn verify_files_main(
             server,
             slice_vars,
             vc_is_valid,
+            soundness_blame,
         )?;
 
         // Handle reasons to stop the verifier.

src/driver/core_verify.rs

@@ -24,6 +24,7 @@ use crate::{
         proc_verify::{encode_proc_verify, to_direction_lower_bounds},
         SpecCall,
     },
+    proof_rules::calculus::ProcSoundness,
     resource_limits::LimitsRef,
     servers::Server,
     slicing::{
@@ -70,6 +71,7 @@ pub struct CoreVerifyTask {
     pub deps: Dependencies,
     pub direction: Direction,
     pub block: Block,
+    pub proc_soundness: ProcSoundness,
 }
 
 impl CoreVerifyTask {
@@ -96,6 +98,7 @@ impl CoreVerifyTask {
                             deps,
                             direction,
                             block,
+                            proc_soundness: ProcSoundness::default(),
                         })
                     }
                     DeclKind::DomainDecl(_domain_decl) => None, // TODO: check that the axioms are not contradictions
@@ -107,6 +110,7 @@ impl CoreVerifyTask {
                 deps,
                 direction: Direction::Down,
                 block,
+                proc_soundness: ProcSoundness::default(),
             }),
         }
     }

src/driver/smt_proof.rs

@@ -28,6 +28,7 @@ use crate::driver::commands::verify::VerifyCommand;
 use crate::driver::error::CaesarError;
 use crate::driver::item::SourceUnitName;
 use crate::driver::quant_proof::{BoolVcProveTask, QuantVcProveTask};
+use crate::proof_rules::calculus::ProcSoundness;
 use crate::slicing::transform::SliceStmts;
 use crate::smt::funcs::axiomatic::{AxiomInstantiation, AxiomaticFunctionEncoder, PartialEncoding};
 use crate::smt::funcs::fuel::literals::LiteralExprCollector;
@@ -141,6 +142,7 @@ pub fn run_smt_prove_task(
     server: &mut dyn Server,
     slice_vars: SliceStmts,
     vc_is_valid: BoolVcProveTask,
+    proc_soundness: &ProcSoundness,
 ) -> Result<ProveResult, CaesarError> {
     let ctx = Context::new(&z3::Config::default());
     let function_encoder = mk_function_encoder(tcx, depgraph, options)?;
@@ -161,7 +163,7 @@ pub fn run_smt_prove_task(
         vc_is_valid.run_solver(options, limits_ref, name, &ctx, &mut translate, &slice_vars)?;
 
     server
-        .handle_vc_check_result(name, &mut result, &mut translate)
+        .handle_vc_check_result(name, &mut result, &mut translate, proc_soundness)
         .map_err(CaesarError::ServerError)?;
 
     Ok(result.prove_result)
@@ -558,6 +560,7 @@ impl<'ctx> SmtVcProveResult<'ctx> {
         span: Span,
         server: &mut dyn Server,
         translate: &mut TranslateExprs<'smt, 'ctx>,
+        proc_soundness: &ProcSoundness,
     ) -> Result<(), CaesarError> {
         // TODO: batch all those messages
 
@@ -567,8 +570,25 @@ impl<'ctx> SmtVcProveResult<'ctx> {
             }
         }
 
+        let approximation_labels = proc_soundness.diagnostic_labels();
+        let approx_note = proc_soundness.diagnostic_note();
+
         match &mut self.prove_result {
-            ProveResult::Proof => {}
+            ProveResult::Proof => {
+                if !proc_soundness.sound_proofs() {
+                    let msg = if let Some(note) = approx_note {
+                        format!("The verification result might be unsound because {}", note)
+                    } else {
+                        "The verification result might be unsound.".to_string()
+                    };
+
+                    let diag = Diagnostic::new(ReportKind::Warning, span)
+                        .with_message(msg)
+                        .with_labels(approximation_labels);
+
+                    server.add_diagnostic(diag)?;
+                }
+            }
             ProveResult::Counterexample => {
                 let model = self.model.as_ref().unwrap();
                 let mut labels = vec![];
@@ -618,6 +638,14 @@ impl<'ctx> SmtVcProveResult<'ctx> {
                 let diagnostic = Diagnostic::new(ReportKind::Error, span)
                     .with_message(text)
                     .with_labels(labels);
+
+                let diagnostic = if proc_soundness.sound_refutations() {
+                    diagnostic
+                } else {
+                    diagnostic
+                        .with_note("This counter-example might be spurious and might not apply to the real program.")
+                        .with_labels(approximation_labels)
+                };
                 server.add_diagnostic(diagnostic)?;
             }
             ProveResult::Unknown(reason) => {

src/intrinsic/annotations.rs

@@ -12,8 +12,7 @@ use crate::{
         resolve::{Resolve, ResolveError},
         tycheck::{Tycheck, TycheckError},
     },
-    proof_rules::calculus::RecursiveProcBlame,
-    proof_rules::Encoding,
+    proof_rules::{calculus::RecursiveProcBlame, Encoding, FixpointSemanticsKind},
     slicing::selection::SliceAnnotation,
     tyctx::TyCtx,
 };
@@ -54,12 +53,6 @@ pub enum AnnotationUnsoundnessError {
         span: Span,
         enc_name: Ident,
     },
-    CalculusEncodingMismatch {
-        direction: Direction,
-        span: Span,
-        calculus_name: Ident,
-        enc_name: Ident,
-    },
     CalculusCallMismatch {
         span: Span,
         context_calculus: Ident,
@@ -125,16 +118,6 @@ impl AnnotationUnsoundnessError {
                         "There must not be any statements after this annotated statement (and the annotated statement must not be nested in a block).",
                     ))
             }
-            AnnotationUnsoundnessError::CalculusEncodingMismatch{direction, span, calculus_name, enc_name } => {
-                Diagnostic::new(ReportKind::Error, span)
-                    .with_message(format!(
-                        "In {}s, the `{}` calculus does not support the `{}` proof rule.",
-                        direction.prefix("proc"), calculus_name.name, enc_name.name
-                    ))
-                    .with_label(Label::new(span).with_message(
-                        "The calculus, proof rule, and direction are incompatible.",
-                    ))
-            }
             AnnotationUnsoundnessError::CalculusCallMismatch{span,context_calculus,call_calculus} => {
                 Diagnostic::new(ReportKind::Error, span)
                     .with_message(format!(
@@ -175,13 +158,29 @@ pub struct Calculus {
     pub calculus_type: CalculusType,
 }
 
+impl std::fmt::Display for Calculus {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{}", self.name)
+    }
+}
+
 #[derive(Debug, Clone, Copy, PartialEq)]
 pub enum CalculusType {
     Wp,
     Wlp,
     Ert,
 }
 
+impl std::fmt::Display for CalculusType {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        match self {
+            CalculusType::Wp => write!(f, "wp"),
+            CalculusType::Wlp => write!(f, "wlp"),
+            CalculusType::Ert => write!(f, "ert"),
+        }
+    }
+}
+
 impl CalculusType {
     pub fn is_induction_allowed(&self, direction: Direction) -> bool {
         matches!(
@@ -191,6 +190,13 @@ impl CalculusType {
                 | (CalculusType::Ert, Direction::Up)
         )
     }
+
+    pub fn to_fixed_point_semantics_kind(self) -> FixpointSemanticsKind {
+        match self {
+            CalculusType::Wp | CalculusType::Ert => FixpointSemanticsKind::LeastFixedPoint,
+            CalculusType::Wlp => FixpointSemanticsKind::GreatestFixedPoint,
+        }
+    }
 }
 
 #[derive(Debug, Clone)]

src/proof_rules/calculus/calculus_checker.rs

@@ -1,10 +1,7 @@
 use std::{collections::HashMap, ops::DerefMut};
 
 use crate::{
-    ast::{
-        visit::{walk_stmt, VisitorMut},
-        DeclKind, DeclRef, Diagnostic, Expr, ExprKind, Ident, ProcDecl, Stmt, StmtKind,
-    },
+    ast::{visit::VisitorMut, DeclKind, DeclRef, Diagnostic, Expr, ExprKind, Ident, ProcDecl},
     intrinsic::annotations::{
         AnnotationError, AnnotationKind, AnnotationUnsoundnessError, Calculus,
     },
@@ -143,50 +140,4 @@ impl<'tcx> VisitorMut for CalculusVisitor<'tcx> {
 
         res
     }
-
-    fn visit_stmt(&mut self, s: &mut Stmt) -> Result<(), Self::Err> {
-        match &mut s.node {
-            // If the statement is an annotation, transform it
-            StmtKind::Annotation(_, ident, _, inner_stmt) => {
-                // First visit the statement that is annotated and handle inner annotations
-                self.visit_stmt(inner_stmt)?;
-
-                if let DeclKind::AnnotationDecl(AnnotationKind::Encoding(anno_ref)) =
-                    self.tcx.get(*ident).unwrap().as_ref()
-                {
-                    // Try to get the current procedure context
-                    let proc_context = self
-                        .proc_context
-                        .as_ref()
-                        // If there is no procedure context, throw an error
-                        .ok_or(CalculusVisitorError::AnnotationError(
-                            AnnotationError::NotInProcedure {
-                                span: s.span,
-                                annotation_name: *ident,
-                            },
-                        ))?;
-
-                    // Unpack the current procedure context
-                    let direction = proc_context.direction;
-
-                    // Check if the calculus annotation is compatible with the encoding annotation
-                    if let Some(calculus) = proc_context.calculus {
-                        // If calculus is not allowed, return an error
-                        if !anno_ref.is_calculus_allowed(calculus, direction) {
-                            return Err(CalculusVisitorError::UnsoundnessError(
-                                AnnotationUnsoundnessError::CalculusEncodingMismatch {
-                                    direction,
-                                    span: s.span,
-                                    calculus_name: calculus.name,
-                                    enc_name: anno_ref.name(),
-                                },
-                            ));
-                        };
-                    }
-                }
-            }
-            _ => walk_stmt(self, s)?,
-        }
-        Ok(())
-    }
 }

src/proof_rules/calculus/mod.rs

@@ -2,6 +2,8 @@ mod calculus_checker;
 pub use calculus_checker::*;
 mod recursion_checker;
 pub use recursion_checker::*;
+mod soundness_checker;
+pub use soundness_checker::*;
 
 #[cfg(test)]
 mod tests;