From aa357770d78d3258fd3f9713ded79be4d004f000 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Umut=20Yi=C4=9Fit=20Dural?= Date: Wed, 12 Nov 2025 17:52:11 +0300 Subject: [PATCH 1/6] Implement soundness checking & corresponding diagnostics in lsp --- src/driver/commands/refinement.rs | 2 + src/driver/commands/verify.rs | 12 +- src/driver/core_verify.rs | 8 + src/driver/smt_proof.rs | 114 +++++++- src/intrinsic/annotations.rs | 42 +-- src/proof_rules/calculus/calculus_checker.rs | 51 +--- src/proof_rules/calculus/mod.rs | 2 + src/proof_rules/calculus/soundness_checker.rs | 261 ++++++++++++++++++ src/proof_rules/calculus/tests.rs | 41 +-- src/proof_rules/induction.rs | 39 +++ src/proof_rules/mciver_ast.rs | 18 ++ src/proof_rules/mod.rs | 111 +++++--- src/proof_rules/omega.rs | 20 ++ src/proof_rules/ost.rs | 21 ++ src/proof_rules/past.rs | 21 ++ src/proof_rules/unroll.rs | 20 ++ src/servers/cli.rs | 2 + src/servers/lsp.rs | 4 +- src/servers/mod.rs | 2 + src/servers/test.rs | 2 + src/vc/explain.rs | 1 + 21 files changed, 650 insertions(+), 144 deletions(-) create mode 100644 src/proof_rules/calculus/soundness_checker.rs diff --git a/src/driver/commands/refinement.rs b/src/driver/commands/refinement.rs index 3f5c285e..3f41f6d5 100644 --- a/src/driver/commands/refinement.rs +++ b/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::SoundnessBlame, resource_limits::{LimitError, LimitsRef}, servers::SharedServer, }; @@ -163,6 +164,7 @@ async fn verify_entailment( server, slice_vars, vc_is_valid, + &SoundnessBlame::default(), )?; // Handle reasons to stop the verifier. diff --git a/src/driver/commands/verify.rs b/src/driver/commands/verify.rs index 4fcf54e7..222d88ff 100644 --- a/src/driver/commands/verify.rs +++ b/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,11 @@ 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(|task| task.with_soundness_blame(soundness_blame)) + }) }) .collect(); @@ -254,6 +261,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.soundness_blame.take().unwrap_or_default(); + // Running the SMT prove task: translating to Z3, running the solver. let result = run_smt_prove_task( options, @@ -264,6 +273,7 @@ fn verify_files_main( server, slice_vars, vc_is_valid, + &soundness_blame, )?; // Handle reasons to stop the verifier. diff --git a/src/driver/core_verify.rs b/src/driver/core_verify.rs index 16a7219e..1eaf74c4 100644 --- a/src/driver/core_verify.rs +++ b/src/driver/core_verify.rs @@ -24,6 +24,7 @@ use crate::{ proc_verify::{encode_proc_verify, to_direction_lower_bounds}, SpecCall, }, + proof_rules::calculus::SoundnessBlame, resource_limits::LimitsRef, servers::Server, slicing::{ @@ -70,6 +71,7 @@ pub struct CoreVerifyTask { pub deps: Dependencies, pub direction: Direction, pub block: Block, + pub soundness_blame: Option, } impl CoreVerifyTask { @@ -96,6 +98,7 @@ impl CoreVerifyTask { deps, direction, block, + soundness_blame: None, }) } DeclKind::DomainDecl(_domain_decl) => None, // TODO: check that the axioms are not contradictions @@ -107,10 +110,15 @@ impl CoreVerifyTask { deps, direction: Direction::Down, block, + soundness_blame: None, }), } } + pub fn with_soundness_blame(mut self, soundness_blame: SoundnessBlame) -> Self { + self.soundness_blame = Some(soundness_blame); + self + } /// Desugar assignments with procedure calls. #[instrument(skip_all)] pub fn desugar_spec_calls(&mut self, tcx: &mut TyCtx, name: String) -> Result<(), CaesarError> { diff --git a/src/driver/smt_proof.rs b/src/driver/smt_proof.rs index 098c5884..66148506 100644 --- a/src/driver/smt_proof.rs +++ b/src/driver/smt_proof.rs @@ -28,6 +28,9 @@ 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::{ + infimum_approximation_list, ApproximationKind, Soundness, SoundnessBlame, +}; use crate::slicing::transform::SliceStmts; use crate::smt::funcs::axiomatic::{AxiomInstantiation, AxiomaticFunctionEncoder, PartialEncoding}; use crate::smt::funcs::fuel::literals::LiteralExprCollector; @@ -141,6 +144,7 @@ pub fn run_smt_prove_task( server: &mut dyn Server, slice_vars: SliceStmts, vc_is_valid: BoolVcProveTask, + soundness_blame: &SoundnessBlame, ) -> Result { let ctx = Context::new(&z3::Config::default()); let function_encoder = mk_function_encoder(tcx, depgraph, options)?; @@ -161,7 +165,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, soundness_blame) .map_err(CaesarError::ServerError)?; Ok(result.prove_result) @@ -558,6 +562,7 @@ impl<'ctx> SmtVcProveResult<'ctx> { span: Span, server: &mut dyn Server, translate: &mut TranslateExprs<'smt, 'ctx>, + soundness_blame: &SoundnessBlame, ) -> Result<(), CaesarError> { // TODO: batch all those messages @@ -567,8 +572,103 @@ impl<'ctx> SmtVcProveResult<'ctx> { } } + let approximation_labels = soundness_blame + .approximations + .iter() + .map(|approx| { + let mut label = Label::new(approx.span).with_message(format!( + "This statement is an {} of the real program behavior", + approx.kind + )); + + if let Some(calculus) = soundness_blame.calculus { + let statement_str = match approx.is_loop { + true => "loop", + false => "statement", + }; + + match &approx.kind { + ApproximationKind::Over => { + label = label.with_message(format!( + "For this {} S, {} is over-approximated i.e., vc[S] ≥ {}[S]", + statement_str, calculus, calculus + )) + } + ApproximationKind::Under => { + label = label.with_message(format!( + "For this {} S, {} is under-approximated i.e., vc[S] ≤ {}[S]", + statement_str, calculus, calculus + )); + } + _ => {} + } + } + label + }) + .collect_vec(); + + let overall_approx = infimum_approximation_list(&soundness_blame.approximations); + + let is_both_over_and_under = soundness_blame + .approximations + .iter() + .any(|approx| approx.kind == ApproximationKind::Over) + && soundness_blame + .approximations + .iter() + .any(|approx| approx.kind == ApproximationKind::Under); + + let approx_note: Option = if let Some(calculus) = soundness_blame.calculus { + match overall_approx { + ApproximationKind::Over => Some(format!( + "the {} of the program is over-approximated, i.e., vc[program] ≥ {}[program]", + calculus, calculus + )), + ApproximationKind::Under => Some(format!( + "the {} of the program is under-approximated, i.e., vc[program] ≤ {}[program]", + calculus, calculus + )), + ApproximationKind::Unknown => { + if is_both_over_and_under { + Some(format!( + "the {} of the program is both over- and under-approximated in different parts of the program, therefore the approximation relationship for the whole program is unknown.", + calculus, + )) + } else { + Some(format!( + "the approximation relationship of the vc and the {} of the program is unknown.", + calculus, + )) + } + } + _ => None, + } + } else { + None + }; + match &mut self.prove_result { - ProveResult::Proof => {} + ProveResult::Proof => { + if matches!( + soundness_blame.soundness, + Soundness::Refutation | Soundness::Unknown + ) { + let msg = if approx_note.is_some() { + format!( + "The verification result might be unsound because {}", + approx_note.unwrap() + ) + } else { + "The verification result is 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 +718,16 @@ impl<'ctx> SmtVcProveResult<'ctx> { let diagnostic = Diagnostic::new(ReportKind::Error, span) .with_message(text) .with_labels(labels); + + let diagnostic = match soundness_blame.soundness { + Soundness::Proof | Soundness::Unknown => { + // This counter-example might be spurious, add a diagnostic + diagnostic + .with_note("This counter-example might be spurious and might not apply to the real program.") + .with_labels(approximation_labels) + } + Soundness::Refutation | Soundness::Exact => diagnostic, + }; server.add_diagnostic(diagnostic)?; } ProveResult::Unknown(reason) => { diff --git a/src/intrinsic/annotations.rs b/src/intrinsic/annotations.rs index 27f44856..afdfdf97 100644 --- a/src/intrinsic/annotations.rs +++ b/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,6 +158,12 @@ 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, @@ -182,6 +171,16 @@ pub enum CalculusType { 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)] diff --git a/src/proof_rules/calculus/calculus_checker.rs b/src/proof_rules/calculus/calculus_checker.rs index 6dfcb905..f0dea30d 100644 --- a/src/proof_rules/calculus/calculus_checker.rs +++ b/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(()) - } } diff --git a/src/proof_rules/calculus/mod.rs b/src/proof_rules/calculus/mod.rs index ae226a29..5ac3927e 100644 --- a/src/proof_rules/calculus/mod.rs +++ b/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; diff --git a/src/proof_rules/calculus/soundness_checker.rs b/src/proof_rules/calculus/soundness_checker.rs new file mode 100644 index 00000000..dcae1980 --- /dev/null +++ b/src/proof_rules/calculus/soundness_checker.rs @@ -0,0 +1,261 @@ +use std::{collections::HashMap, fmt, ops::DerefMut, vec}; + +use crate::{ + ast::{Block, DeclKind, Direction, ProcDecl, Span, Stmt, StmtKind}, + driver::{ + front::{Module, SourceUnit}, + item::SourceUnitName, + }, + intrinsic::annotations::{AnnotationKind, Calculus}, + proof_rules::{get_calculus, infer_fixpoint_semantics_kind}, + tyctx::TyCtx, +}; + +#[derive(Debug, Clone)] +pub struct ApproximationListEntry { + pub span: Span, + pub is_loop: bool, + pub kind: ApproximationKind, +} +pub type ApproximationList = Vec; + +// pub type SoundnessBlame = (Soundness, ApproximationList); + +#[derive(Debug, Clone, Default)] +pub struct SoundnessBlame { + pub soundness: Soundness, + pub approximations: ApproximationList, + pub calculus: Option, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)] +pub enum ApproximationKind { + #[default] + Exact, + Under, + Over, + Unknown, +} + +impl ApproximationKind { + pub fn supremum(self, other: ApproximationKind) -> ApproximationKind { + match self.partial_cmp(&other) { + Some(std::cmp::Ordering::Equal) => self, + Some(std::cmp::Ordering::Less) => other, + Some(std::cmp::Ordering::Greater) => self, + None => ApproximationKind::Exact, // If they are incomparable, return Exact (which is the top element) + } + } + pub fn infimum(self, other: ApproximationKind) -> ApproximationKind { + match self.partial_cmp(&other) { + Some(std::cmp::Ordering::Equal) => self, + Some(std::cmp::Ordering::Less) => self, + Some(std::cmp::Ordering::Greater) => other, + None => ApproximationKind::Unknown, // If they are incomparable, return Unknown (which is the bottom element) + } + } +} + +impl PartialOrd for ApproximationKind { + fn partial_cmp(&self, other: &Self) -> Option { + match (self, other) { + (ApproximationKind::Exact, ApproximationKind::Exact) => Some(std::cmp::Ordering::Equal), + (ApproximationKind::Under, ApproximationKind::Under) => Some(std::cmp::Ordering::Equal), + (ApproximationKind::Over, ApproximationKind::Over) => Some(std::cmp::Ordering::Equal), + (ApproximationKind::Unknown, ApproximationKind::Unknown) => { + Some(std::cmp::Ordering::Equal) + } + (_, ApproximationKind::Exact) => Some(std::cmp::Ordering::Less), + (ApproximationKind::Exact, _) => Some(std::cmp::Ordering::Greater), + (ApproximationKind::Unknown, _) => Some(std::cmp::Ordering::Less), + (_, ApproximationKind::Unknown) => Some(std::cmp::Ordering::Greater), + (ApproximationKind::Under, ApproximationKind::Over) + | (ApproximationKind::Over, ApproximationKind::Under) => None, + } + } +} + +impl fmt::Display for ApproximationKind { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + ApproximationKind::Exact => write!(f, "exact approximation"), + ApproximationKind::Under => write!(f, "under-approximation"), + ApproximationKind::Over => write!(f, "over-approximation"), + ApproximationKind::Unknown => write!(f, "unknown approximation"), + } + } +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)] +pub enum Soundness { + #[default] + Exact, + Proof, + Refutation, + Unknown, +} + +impl Soundness { + pub fn from_approximation(approx: ApproximationKind, direction: Direction) -> Self { + match approx { + ApproximationKind::Exact => Soundness::Exact, + ApproximationKind::Under => match direction { + Direction::Down => Soundness::Proof, + Direction::Up => Soundness::Refutation, + }, + ApproximationKind::Over => match direction { + Direction::Down => Soundness::Refutation, + Direction::Up => Soundness::Proof, + }, + ApproximationKind::Unknown => Soundness::Unknown, + } + } +} + +pub fn get_soundness_map( + module: &mut Module, + tcx: &mut TyCtx, +) -> HashMap { + let mut soundness_map = HashMap::new(); + let source_units = &mut module.items; + + for source_unit in source_units { + let soundness = match source_unit.enter_mut().deref_mut() { + SourceUnit::Decl(decl) => match decl { + DeclKind::ProcDecl(proc_decl) => soundness_blame_of_proc(&proc_decl.borrow(), tcx), + _ => None, + }, + SourceUnit::Raw(ref block) => Some(soundness_blame_of_raw(block, tcx)), + }; + if let Some(soundness_blame) = soundness { + soundness_map.insert(source_unit.name().clone(), soundness_blame); + } + } + soundness_map +} + +/// Track under-, over- and unknown approximating statements in a block +/// +/// Returns a list of spans and their corresponding approximation kinds of non-exact approximating statements +fn track_approximation_in_block( + block: &Block, + direction: Direction, + calculus: Option, + tcx: &mut TyCtx, +) -> ApproximationList { + block.node.iter().fold(Vec::new(), |mut acc, stmt| { + acc.extend(track_approximation_in_statement( + stmt, direction, calculus, tcx, + )); + acc + }) +} + +/// Determine the approximation kind of a statement and track approximation in its sub-statements +fn track_approximation_in_statement( + s: &Stmt, + direction: Direction, + calculus: Option, + tcx: &mut TyCtx, +) -> ApproximationList { + match &s.node { + // First handle the composite statements for recursion + StmtKind::Seq(stmts) => stmts.iter().fold(Vec::new(), |mut acc, stmt| { + let stmt_approx_kind = track_approximation_in_statement(stmt, direction, calculus, tcx); + acc.extend(stmt_approx_kind); + acc + }), + + StmtKind::If(_, ref block1, ref block2) + | StmtKind::Demonic(ref block1, ref block2) + | StmtKind::Angelic(ref block1, ref block2) => { + let mut acc = track_approximation_in_block(block1, direction, calculus, tcx); + acc.extend(track_approximation_in_block( + block2, direction, calculus, tcx, + )); + acc + } + StmtKind::While(_, ref block) => { + track_approximation_in_block(block, direction, calculus, tcx) + } + // Under-and over-approximations from annotations + StmtKind::Annotation(_, ident, _, inner_stmt) => { + let mut inner_approximation_list = + track_approximation_in_statement(inner_stmt, direction, calculus, tcx); + + // If the annotation is an encoding annotation + if let DeclKind::AnnotationDecl(AnnotationKind::Encoding(anno_ref)) = + tcx.get(*ident).unwrap().as_ref() + { + let semantics_type = infer_fixpoint_semantics_kind( + // Qualified because of the RefCell::borrow naming clash + std::borrow::Borrow::borrow(anno_ref), + calculus, + direction, + ); + + let inner_approximation = infimum_approximation_list(&inner_approximation_list); + + // Handle the inner approximation kind according to the encoding annotation and get the overall approximation + let approximation = anno_ref.get_approximation(semantics_type, inner_approximation); + inner_approximation_list.push(ApproximationListEntry { + span: s.span, + is_loop: true, + kind: approximation, + }); + } + inner_approximation_list + } + // Negations lead to unknown approximations + StmtKind::Negate(_) => vec![ApproximationListEntry { + span: s.span, + is_loop: false, + kind: ApproximationKind::Unknown, + }], + // All other statements do not change the approximation kind + _ => Vec::new(), + } +} + +pub fn soundness_blame_of_proc(decl: &ProcDecl, tcx: &mut TyCtx) -> Option { + if let Some(block) = decl.body.borrow_mut().as_mut() { + // Get the calculus of the procedure + let calculus = get_calculus(decl, tcx).ok().flatten(); + let direction = decl.direction; + + let approx_list = track_approximation_in_block(block, direction, calculus, tcx); + let infimum_approx = infimum_approximation_list(&approx_list); + + return Some(SoundnessBlame { + soundness: Soundness::from_approximation(infimum_approx, direction), + approximations: approx_list, + calculus, + }); + } + None +} + +pub fn soundness_blame_of_raw(block: &Block, tcx: &mut TyCtx) -> SoundnessBlame { + let approx_list = track_approximation_in_block(block, Direction::Down, None, tcx); + let meet_approx = infimum_approximation_list(&approx_list); + // Insert the soundness into the map + SoundnessBlame { + soundness: Soundness::from_approximation(meet_approx, Direction::Down), + approximations: approx_list, + calculus: None, + } +} + +pub fn _supremum_approximation_list(list: &ApproximationList) -> ApproximationKind { + list.iter() + .fold(ApproximationKind::Unknown, |acc, approx_entry| { + acc.supremum(approx_entry.kind) + }) +} + +pub fn infimum_approximation_list(list: &ApproximationList) -> ApproximationKind { + list.iter() + .fold(ApproximationKind::Exact, |acc, approx_entry| { + acc.infimum(approx_entry.kind) + }) +} diff --git a/src/proof_rules/calculus/tests.rs b/src/proof_rules/calculus/tests.rs index 47c76843..85096ec6 100644 --- a/src/proof_rules/calculus/tests.rs +++ b/src/proof_rules/calculus/tests.rs @@ -1,21 +1,4 @@ -use crate::driver::{commands::verify::verify_test, error::CaesarError}; - -#[test] -fn test_wp_with_kind_fail() { - let source = r#" - @wp - proc main() -> () { - var x: UInt - @k_induction(1, x) - while 1 <= x { - x = x - 1 - } - } - "#; - let res = matches!(verify_test(source).0, Err(CaesarError::Diagnostic(_))); - - assert!(res); -} +use crate::driver::commands::verify::verify_test; #[test] fn test_wp_with_kind_ok() { @@ -49,28 +32,6 @@ fn test_wlp_with_kind_ok() { assert!(!res) } -#[test] -fn test_calculus_encoding_mismatch() { - // this should produce an error - let source = r#" - @wp - proc main() -> () { - var x: UInt - @invariant(x) // invariant encoding within wp reasoning is not sound! - while 1 <= x { - x = x - 1 - } - } - "#; - let res = verify_test(source).0; - assert!(res.is_err()); - let err = res.unwrap_err(); - assert_eq!( - err.to_string(), - "Error: In procs, the `wp` calculus does not support the `invariant` proof rule." - ); -} - #[test] fn test_wrong_annotation_usage() { // this should produce an error diff --git a/src/proof_rules/induction.rs b/src/proof_rules/induction.rs index fd1c83be..6015a9cb 100644 --- a/src/proof_rules/induction.rs +++ b/src/proof_rules/induction.rs @@ -21,6 +21,7 @@ use crate::{ intrinsic::annotations::{ tycheck_annotation_call, AnnotationDecl, AnnotationError, Calculus, CalculusType, }, + proof_rules::{calculus::ApproximationKind, FixpointSemanticsKind}, slicing::{wrap_with_error_message, wrap_with_success_message}, tyctx::TyCtx, }; @@ -93,6 +94,25 @@ impl Encoding for InvariantAnnotation { ) } + fn get_approximation( + &self, + fixpoint_semantics: FixpointSemanticsKind, + inner_approximation_kind: ApproximationKind, + ) -> ApproximationKind { + match fixpoint_semantics { + FixpointSemanticsKind::LeastFixedPoint => ApproximationKind::Over, + FixpointSemanticsKind::GreatestFixedPoint => ApproximationKind::Under, + } + .infimum(inner_approximation_kind) + } + + fn sound_fixpoint_semantics_kind(&self, direction: Direction) -> FixpointSemanticsKind { + match direction { + Direction::Up => FixpointSemanticsKind::LeastFixedPoint, + Direction::Down => FixpointSemanticsKind::GreatestFixedPoint, + } + } + fn transform( &self, tcx: &TyCtx, @@ -177,6 +197,25 @@ impl Encoding for KIndAnnotation { ) } + fn get_approximation( + &self, + fixpoint_semantics: FixpointSemanticsKind, + inner_approximation_kind: ApproximationKind, + ) -> ApproximationKind { + match fixpoint_semantics { + FixpointSemanticsKind::LeastFixedPoint => ApproximationKind::Over, + FixpointSemanticsKind::GreatestFixedPoint => ApproximationKind::Under, + } + .infimum(inner_approximation_kind) + } + + fn sound_fixpoint_semantics_kind(&self, direction: Direction) -> FixpointSemanticsKind { + match direction { + Direction::Up => FixpointSemanticsKind::LeastFixedPoint, + Direction::Down => FixpointSemanticsKind::GreatestFixedPoint, + } + } + fn transform( &self, tcx: &TyCtx, diff --git a/src/proof_rules/mciver_ast.rs b/src/proof_rules/mciver_ast.rs index d95afb30..d030ff25 100644 --- a/src/proof_rules/mciver_ast.rs +++ b/src/proof_rules/mciver_ast.rs @@ -25,6 +25,7 @@ use crate::{ intrinsic::annotations::{ tycheck_annotation_call, AnnotationDecl, AnnotationError, Calculus, CalculusType, }, + proof_rules::{calculus::ApproximationKind, FixpointSemanticsKind}, tyctx::TyCtx, }; @@ -131,6 +132,23 @@ impl Encoding for ASTAnnotation { matches!(calculus.calculus_type, CalculusType::Wp) && direction == Direction::Down } + fn get_approximation( + &self, + fixpoint_semantics: FixpointSemanticsKind, + inner_approximation_kind: ApproximationKind, + ) -> ApproximationKind { + match (fixpoint_semantics, inner_approximation_kind) { + (FixpointSemanticsKind::LeastFixedPoint, ApproximationKind::Exact) => { + ApproximationKind::Exact + } + _ => ApproximationKind::Unknown, + } + } + + fn sound_fixpoint_semantics_kind(&self, _direction: Direction) -> FixpointSemanticsKind { + FixpointSemanticsKind::LeastFixedPoint + } + fn transform( &self, tcx: &TyCtx, diff --git a/src/proof_rules/mod.rs b/src/proof_rules/mod.rs index 44587a1c..faa163f3 100644 --- a/src/proof_rules/mod.rs +++ b/src/proof_rules/mod.rs @@ -37,6 +37,7 @@ use crate::{ intrinsic::annotations::{ AnnotationError, AnnotationKind, AnnotationUnsoundnessError, Calculus, }, + proof_rules::calculus::ApproximationKind, tyctx::TyCtx, }; @@ -63,6 +64,34 @@ pub struct EncodingEnvironment { pub stmt_span: Span, pub call_span: Span, pub direction: Direction, + pub calculus: Option, +} + +/// The type of loop semantics used in the encoding annotations +pub enum FixpointSemanticsKind { + LeastFixedPoint, + GreatestFixedPoint, +} + +/// Determine the loop semantics type based on the annotation, calculus, and direction +/// The semantics are determined by the provided calculus if available; otherwise, +/// they are inferred from the annotation and direction. +/// +/// The semantics are primarily determined by the calculus type: +/// - `CalculusType::Wp` and `CalculusType::Ert` use least fixed point semantics, +/// - `CalculusType::Wlp` uses greatest fixed point semantics. +/// +/// If no calculus is provided, the semantics are inferred from the annotation's +/// default (sound) behavior based on the direction. +pub fn infer_fixpoint_semantics_kind( + encoding: &dyn Encoding, + calculus: Option, + direction: Direction, +) -> FixpointSemanticsKind { + match calculus { + Some(calculus) => calculus.calculus_type.to_fixed_point_semantics_kind(), + None => encoding.sound_fixpoint_semantics_kind(direction), + } } /// The trait that all encoding annotations must implement @@ -97,6 +126,18 @@ pub trait Encoding: fmt::Debug { /// Check if the given calculus annotation is compatible with the encoding annotation fn is_calculus_allowed(&self, calculus: Calculus, direction: Direction) -> bool; + /// Select an approximation kind based on the semantics type used. + fn get_approximation( + &self, + fixpoint_semantics: FixpointSemanticsKind, + inner_approximation_kind: ApproximationKind, + ) -> ApproximationKind; + + /// Get the sound fixpoint semantics kind for this encoding annotation based on the direction + /// + /// This function is used when there is no calculus annotation present on the procedure + fn sound_fixpoint_semantics_kind(&self, direction: Direction) -> FixpointSemanticsKind; + /// Indicates if the encoding annotation is required to be the last statement of a procedure fn is_terminator(&self) -> bool; @@ -174,15 +215,15 @@ impl<'tcx> EncodingVisitor<'tcx> { /// UnsoundnessError are thrown when the usage of an annotation is unsound (e.g. mismatched calculus, not a terminator, etc.) #[derive(Debug)] pub enum EncodingVisitorError { - AnnotationError(AnnotationError), - UnsoundnessError(AnnotationUnsoundnessError), + Annotation(AnnotationError), + Unsoundness(AnnotationUnsoundnessError), } impl EncodingVisitorError { pub fn diagnostic(self) -> Diagnostic { match self { - EncodingVisitorError::AnnotationError(err) => err.diagnostic(), - EncodingVisitorError::UnsoundnessError(err) => err.diagnostic(), + EncodingVisitorError::Annotation(err) => err.diagnostic(), + EncodingVisitorError::Unsoundness(err) => err.diagnostic(), } } } @@ -194,28 +235,8 @@ impl<'tcx> VisitorMut for EncodingVisitor<'tcx> { let proc_ref = proc_ref.clone(); // lose the reference to &mut self let proc = proc_ref.borrow(); - let mut curr_calculus: Option = None; - // If the procedure has a calculus annotation, store it as the current calculus - if let Some(ident) = proc.calculus.as_ref() { - match self.tcx.get(*ident) { - Some(decl) => { - if let DeclKind::AnnotationDecl(AnnotationKind::Calculus(calculus)) = - decl.as_ref() - { - curr_calculus = Some(*calculus); - } - } - None => { - // If there isn't any calculus declaration that matches the annotation, throw an error - return Err(EncodingVisitorError::AnnotationError( - AnnotationError::UnknownAnnotation { - span: proc.span, - annotation_name: *ident, - }, - )); - } - } - } + let curr_calculus = + get_calculus(&proc, self.tcx).map_err(EncodingVisitorError::Annotation)?; // Store the current procedure context self.proc_context = Some(ProcContext { @@ -252,7 +273,7 @@ impl<'tcx> VisitorMut for EncodingVisitor<'tcx> { .proc_context .as_ref() // If there is no procedure context, throw an error - .ok_or(EncodingVisitorError::AnnotationError( + .ok_or(EncodingVisitorError::Annotation( AnnotationError::NotInProcedure { span: s.span, annotation_name: *ident, @@ -267,7 +288,7 @@ impl<'tcx> VisitorMut for EncodingVisitor<'tcx> { // Check whether the calculus annotation is actually on a while loop (annotations can only be on while loops) if let StmtKind::While(_, _) = inner_stmt.node { } else { - return Err(EncodingVisitorError::AnnotationError( + return Err(EncodingVisitorError::Annotation( AnnotationError::NotOnWhile { span: annotation_span, annotation_name: *ident, @@ -278,7 +299,7 @@ impl<'tcx> VisitorMut for EncodingVisitor<'tcx> { // A terminator annotation can't be nested in a block if anno_ref.is_terminator() && self.nesting_level > 0 { - return Err(EncodingVisitorError::UnsoundnessError( + return Err(EncodingVisitorError::Unsoundness( AnnotationUnsoundnessError::NotTerminator { span: s.span, enc_name: anno_ref.name(), @@ -291,12 +312,13 @@ impl<'tcx> VisitorMut for EncodingVisitor<'tcx> { stmt_span: s.span, call_span: annotation_span, // TODO: if I change this to stmt_span, explain core vc works :( direction, + calculus: proc_context.calculus, }; // Generate new statements (and declarations) from the annotated loop let mut enc_gen = anno_ref .transform(self.tcx, inputs, inner_stmt, enc_env) - .map_err(EncodingVisitorError::AnnotationError)?; + .map_err(EncodingVisitorError::Annotation)?; // Visit generated statements self.visit_block(&mut enc_gen.block)?; @@ -340,7 +362,7 @@ impl<'tcx> VisitorMut for EncodingVisitor<'tcx> { | StmtKind::Demonic(_, _) | StmtKind::Seq(_) => { if let Some(anno_name) = self.terminator_annotation { - return Err(EncodingVisitorError::UnsoundnessError( + return Err(EncodingVisitorError::Unsoundness( AnnotationUnsoundnessError::NotTerminator { span: s.span, enc_name: anno_name, @@ -355,7 +377,7 @@ impl<'tcx> VisitorMut for EncodingVisitor<'tcx> { _ => { // If there was a terminator annotation before, don't allow further statements if let Some(anno_name) = self.terminator_annotation { - return Err(EncodingVisitorError::UnsoundnessError( + return Err(EncodingVisitorError::Unsoundness( AnnotationUnsoundnessError::NotTerminator { span: s.span, enc_name: anno_name, @@ -369,3 +391,28 @@ impl<'tcx> VisitorMut for EncodingVisitor<'tcx> { Ok(()) } } + +/// Get the calculus from a procedure declaration if it exists +/// Returns an error if the annotation is not valid +pub fn get_calculus(proc: &ProcDecl, tcx: &TyCtx) -> Result, AnnotationError> { + // If the procedure has a calculus annotation, try to extract it + if let Some(ident) = proc.calculus.as_ref() { + match tcx.get(*ident) { + Some(decl) => { + // If the declaration is a calculus annotation, return it + if let DeclKind::AnnotationDecl(AnnotationKind::Calculus(calculus)) = decl.as_ref() + { + return Ok(Some(*calculus)); + } + } + None => { + // If there isn't any calculus declaration that matches the annotation, throw an error + return Err(AnnotationError::UnknownAnnotation { + span: proc.span, + annotation_name: *ident, + }); + } + } + } + Ok(None) +} diff --git a/src/proof_rules/omega.rs b/src/proof_rules/omega.rs index 0e9a8f4f..9ddd52a6 100644 --- a/src/proof_rules/omega.rs +++ b/src/proof_rules/omega.rs @@ -21,6 +21,7 @@ use crate::{ intrinsic::annotations::{ tycheck_annotation_call, AnnotationDecl, AnnotationError, Calculus, CalculusType, }, + proof_rules::{calculus::ApproximationKind, FixpointSemanticsKind}, tyctx::TyCtx, }; @@ -109,6 +110,25 @@ impl Encoding for OmegaInvAnnotation { ) } + fn get_approximation( + &self, + fixpoint_semantics: FixpointSemanticsKind, + inner_approximation_kind: ApproximationKind, + ) -> ApproximationKind { + match fixpoint_semantics { + FixpointSemanticsKind::LeastFixedPoint => ApproximationKind::Under, + FixpointSemanticsKind::GreatestFixedPoint => ApproximationKind::Over, + } + .infimum(inner_approximation_kind) + } + + fn sound_fixpoint_semantics_kind(&self, direction: Direction) -> FixpointSemanticsKind { + match direction { + Direction::Up => FixpointSemanticsKind::GreatestFixedPoint, + Direction::Down => FixpointSemanticsKind::LeastFixedPoint, + } + } + fn transform( &self, tcx: &TyCtx, diff --git a/src/proof_rules/ost.rs b/src/proof_rules/ost.rs index 33c8d687..a17e5074 100644 --- a/src/proof_rules/ost.rs +++ b/src/proof_rules/ost.rs @@ -23,6 +23,7 @@ use crate::{ intrinsic::annotations::{ tycheck_annotation_call, AnnotationDecl, AnnotationError, Calculus, CalculusType, }, + proof_rules::{calculus::ApproximationKind, FixpointSemanticsKind}, tyctx::TyCtx, }; @@ -96,6 +97,26 @@ impl Encoding for OSTAnnotation { matches!(calculus.calculus_type, CalculusType::Wp) && direction == Direction::Down } + fn get_approximation( + &self, + fixpoint_semantics: FixpointSemanticsKind, + inner_approximation_kind: ApproximationKind, + ) -> ApproximationKind { + match (fixpoint_semantics, inner_approximation_kind) { + (FixpointSemanticsKind::LeastFixedPoint, ApproximationKind::Exact) => { + ApproximationKind::Exact + } + _ => ApproximationKind::Unknown, + } + } + + fn sound_fixpoint_semantics_kind(&self, direction: Direction) -> FixpointSemanticsKind { + match direction { + Direction::Up => FixpointSemanticsKind::LeastFixedPoint, + Direction::Down => FixpointSemanticsKind::GreatestFixedPoint, + } + } + fn transform( &self, tcx: &TyCtx, diff --git a/src/proof_rules/past.rs b/src/proof_rules/past.rs index ac6124f8..bf7e4482 100644 --- a/src/proof_rules/past.rs +++ b/src/proof_rules/past.rs @@ -24,6 +24,7 @@ use crate::{ intrinsic::annotations::{ tycheck_annotation_call, AnnotationDecl, AnnotationError, Calculus, CalculusType, }, + proof_rules::{calculus::ApproximationKind, FixpointSemanticsKind}, tyctx::TyCtx, }; @@ -89,6 +90,26 @@ impl Encoding for PASTAnnotation { matches!(calculus.calculus_type, CalculusType::Ert) && direction == Direction::Up } + fn get_approximation( + &self, + fixpoint_semantics: FixpointSemanticsKind, + inner_approximation_kind: ApproximationKind, + ) -> ApproximationKind { + match (fixpoint_semantics, inner_approximation_kind) { + (FixpointSemanticsKind::LeastFixedPoint, ApproximationKind::Exact) => { + ApproximationKind::Exact + } + _ => ApproximationKind::Unknown, + } + } + + fn sound_fixpoint_semantics_kind(&self, direction: Direction) -> FixpointSemanticsKind { + match direction { + Direction::Up => FixpointSemanticsKind::LeastFixedPoint, + Direction::Down => FixpointSemanticsKind::GreatestFixedPoint, + } + } + fn transform( &self, tcx: &TyCtx, diff --git a/src/proof_rules/unroll.rs b/src/proof_rules/unroll.rs index 0d8bf048..fb7dbb94 100644 --- a/src/proof_rules/unroll.rs +++ b/src/proof_rules/unroll.rs @@ -20,6 +20,7 @@ use crate::{ intrinsic::annotations::{ tycheck_annotation_call, AnnotationDecl, AnnotationError, Calculus, CalculusType, }, + proof_rules::{calculus::ApproximationKind, FixpointSemanticsKind}, tyctx::TyCtx, }; @@ -90,6 +91,25 @@ impl Encoding for UnrollAnnotation { ) } + fn get_approximation( + &self, + fixpoint_semantics: FixpointSemanticsKind, + inner_approximation_kind: ApproximationKind, + ) -> ApproximationKind { + match fixpoint_semantics { + FixpointSemanticsKind::LeastFixedPoint => ApproximationKind::Under, + FixpointSemanticsKind::GreatestFixedPoint => ApproximationKind::Over, + } + .infimum(inner_approximation_kind) + } + + fn sound_fixpoint_semantics_kind(&self, direction: Direction) -> FixpointSemanticsKind { + match direction { + Direction::Up => FixpointSemanticsKind::GreatestFixedPoint, + Direction::Down => FixpointSemanticsKind::LeastFixedPoint, + } + } + fn transform( &self, tcx: &TyCtx, diff --git a/src/servers/cli.rs b/src/servers/cli.rs index b96b8299..fa3dcadb 100644 --- a/src/servers/cli.rs +++ b/src/servers/cli.rs @@ -16,6 +16,7 @@ use crate::{ item::{Item, SourceUnitName}, smt_proof::SmtVcProveResult, }, + proof_rules::calculus::SoundnessBlame, smt::translate_exprs::TranslateExprs, vc::explain::VcExplanation, }; @@ -112,6 +113,7 @@ impl Server for CliServer { name: &SourceUnitName, result: &mut SmtVcProveResult<'ctx>, translate: &mut TranslateExprs<'smt, 'ctx>, + _soundness_blame: &SoundnessBlame, ) -> Result<(), ServerError> { result.print_prove_result(self, translate, name); Ok(()) diff --git a/src/servers/lsp.rs b/src/servers/lsp.rs index 089ab525..c99f107c 100644 --- a/src/servers/lsp.rs +++ b/src/servers/lsp.rs @@ -28,6 +28,7 @@ use crate::{ item::{Item, SourceUnitName}, smt_proof::SmtVcProveResult, }, + proof_rules::calculus::SoundnessBlame, servers::{FileStatus, FileStatusType}, smt::translate_exprs::TranslateExprs, vc::explain::VcExplanation, @@ -427,8 +428,9 @@ impl Server for LspServer { name: &SourceUnitName, result: &mut SmtVcProveResult<'ctx>, translate: &mut TranslateExprs<'smt, 'ctx>, + soundness_blame: &SoundnessBlame, ) -> Result<(), ServerError> { - result.emit_diagnostics(name.span(), self, translate)?; + result.emit_diagnostics(name.span(), self, translate, soundness_blame)?; let statuses = &mut self .file_statuses .entry(name.span().file) diff --git a/src/servers/mod.rs b/src/servers/mod.rs index 4316516a..f46e3b2f 100644 --- a/src/servers/mod.rs +++ b/src/servers/mod.rs @@ -12,6 +12,7 @@ use crate::{ item::{Item, SourceUnitName}, smt_proof::SmtVcProveResult, }, + proof_rules::calculus::SoundnessBlame, smt::translate_exprs::TranslateExprs, vc::explain::VcExplanation, }; @@ -191,6 +192,7 @@ pub trait Server: Send { name: &SourceUnitName, result: &mut SmtVcProveResult<'ctx>, translate: &mut TranslateExprs<'smt, 'ctx>, + soundness_blame: &SoundnessBlame, ) -> Result<(), ServerError>; /// Return an exit code for the process. diff --git a/src/servers/test.rs b/src/servers/test.rs index 371a0371..24fe4828 100644 --- a/src/servers/test.rs +++ b/src/servers/test.rs @@ -13,6 +13,7 @@ use crate::{ item::{Item, SourceUnitName}, smt_proof::SmtVcProveResult, }, + proof_rules::calculus::SoundnessBlame, servers::FileStatus, smt::translate_exprs::TranslateExprs, vc::explain::VcExplanation, @@ -105,6 +106,7 @@ impl Server for TestServer { name: &SourceUnitName, result: &mut SmtVcProveResult<'ctx>, _translate: &mut TranslateExprs<'smt, 'ctx>, + _soundness_blame: &SoundnessBlame, ) -> Result<(), ServerError> { let statuses = &mut self .file_statuses diff --git a/src/vc/explain.rs b/src/vc/explain.rs index 9fcde836..4837a4e9 100644 --- a/src/vc/explain.rs +++ b/src/vc/explain.rs @@ -270,6 +270,7 @@ fn explain_unroll( stmt_span, call_span, direction, + calculus: None, }; // 1. generate the explanations for the loop body in k-1 iterations From fec92f252b742a5b70d828a99ffa6df50d80901a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Umut=20Yi=C4=9Fit=20Dural?= Date: Fri, 28 Nov 2025 03:35:22 +0100 Subject: [PATCH 2/6] Refactor SoundnessBlame and ApproximationKind --- src/driver/commands/refinement.rs | 4 +- src/driver/commands/verify.rs | 9 +- src/driver/core_verify.rs | 12 +- src/driver/smt_proof.rs | 114 +---- src/proof_rules/calculus/soundness_checker.rs | 444 +++++++++++++----- src/proof_rules/induction.rs | 24 +- src/proof_rules/mciver_ast.rs | 8 +- src/proof_rules/mod.rs | 31 +- src/proof_rules/omega.rs | 12 +- src/proof_rules/ost.rs | 8 +- src/proof_rules/past.rs | 8 +- src/proof_rules/unroll.rs | 12 +- src/servers/cli.rs | 4 +- src/servers/lsp.rs | 6 +- src/servers/mod.rs | 4 +- src/servers/test.rs | 4 +- src/vc/explain.rs | 2 +- 17 files changed, 409 insertions(+), 297 deletions(-) diff --git a/src/driver/commands/refinement.rs b/src/driver/commands/refinement.rs index 3f41f6d5..6d29e8cd 100644 --- a/src/driver/commands/refinement.rs +++ b/src/driver/commands/refinement.rs @@ -24,7 +24,7 @@ use crate::{ quant_proof::{lower_quant_prove_task, QuantVcProveTask}, smt_proof::run_smt_prove_task, }, - proof_rules::calculus::SoundnessBlame, + proof_rules::calculus::ProcSoundness, resource_limits::{LimitError, LimitsRef}, servers::SharedServer, }; @@ -164,7 +164,7 @@ async fn verify_entailment( server, slice_vars, vc_is_valid, - &SoundnessBlame::default(), + &ProcSoundness::default(), )?; // Handle reasons to stop the verifier. diff --git a/src/driver/commands/verify.rs b/src/driver/commands/verify.rs index 222d88ff..2c6e8abc 100644 --- a/src/driver/commands/verify.rs +++ b/src/driver/commands/verify.rs @@ -221,7 +221,10 @@ fn verify_files_main( 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(|task| task.with_soundness_blame(soundness_blame)) + core_verify_task.map(|mut task| { + task.proc_soundness = soundness_blame.clone(); + task + }) }) }) .collect(); @@ -261,7 +264,7 @@ 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.soundness_blame.take().unwrap_or_default(); + let soundness_blame = &verify_unit.proc_soundness; // Running the SMT prove task: translating to Z3, running the solver. let result = run_smt_prove_task( @@ -273,7 +276,7 @@ fn verify_files_main( server, slice_vars, vc_is_valid, - &soundness_blame, + soundness_blame, )?; // Handle reasons to stop the verifier. diff --git a/src/driver/core_verify.rs b/src/driver/core_verify.rs index 1eaf74c4..9fc5b6d3 100644 --- a/src/driver/core_verify.rs +++ b/src/driver/core_verify.rs @@ -24,7 +24,7 @@ use crate::{ proc_verify::{encode_proc_verify, to_direction_lower_bounds}, SpecCall, }, - proof_rules::calculus::SoundnessBlame, + proof_rules::calculus::ProcSoundness, resource_limits::LimitsRef, servers::Server, slicing::{ @@ -71,7 +71,7 @@ pub struct CoreVerifyTask { pub deps: Dependencies, pub direction: Direction, pub block: Block, - pub soundness_blame: Option, + pub proc_soundness: ProcSoundness, } impl CoreVerifyTask { @@ -98,7 +98,7 @@ impl CoreVerifyTask { deps, direction, block, - soundness_blame: None, + proc_soundness: ProcSoundness::default(), }) } DeclKind::DomainDecl(_domain_decl) => None, // TODO: check that the axioms are not contradictions @@ -110,15 +110,11 @@ impl CoreVerifyTask { deps, direction: Direction::Down, block, - soundness_blame: None, + proc_soundness: ProcSoundness::default(), }), } } - pub fn with_soundness_blame(mut self, soundness_blame: SoundnessBlame) -> Self { - self.soundness_blame = Some(soundness_blame); - self - } /// Desugar assignments with procedure calls. #[instrument(skip_all)] pub fn desugar_spec_calls(&mut self, tcx: &mut TyCtx, name: String) -> Result<(), CaesarError> { diff --git a/src/driver/smt_proof.rs b/src/driver/smt_proof.rs index 66148506..23a61527 100644 --- a/src/driver/smt_proof.rs +++ b/src/driver/smt_proof.rs @@ -28,9 +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::{ - infimum_approximation_list, ApproximationKind, Soundness, SoundnessBlame, -}; +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; @@ -144,7 +142,7 @@ pub fn run_smt_prove_task( server: &mut dyn Server, slice_vars: SliceStmts, vc_is_valid: BoolVcProveTask, - soundness_blame: &SoundnessBlame, + proc_soundness: &ProcSoundness, ) -> Result { let ctx = Context::new(&z3::Config::default()); let function_encoder = mk_function_encoder(tcx, depgraph, options)?; @@ -165,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, soundness_blame) + .handle_vc_check_result(name, &mut result, &mut translate, proc_soundness) .map_err(CaesarError::ServerError)?; Ok(result.prove_result) @@ -562,7 +560,7 @@ impl<'ctx> SmtVcProveResult<'ctx> { span: Span, server: &mut dyn Server, translate: &mut TranslateExprs<'smt, 'ctx>, - soundness_blame: &SoundnessBlame, + proc_soundness: &ProcSoundness, ) -> Result<(), CaesarError> { // TODO: batch all those messages @@ -572,94 +570,16 @@ impl<'ctx> SmtVcProveResult<'ctx> { } } - let approximation_labels = soundness_blame - .approximations - .iter() - .map(|approx| { - let mut label = Label::new(approx.span).with_message(format!( - "This statement is an {} of the real program behavior", - approx.kind - )); - - if let Some(calculus) = soundness_blame.calculus { - let statement_str = match approx.is_loop { - true => "loop", - false => "statement", - }; - - match &approx.kind { - ApproximationKind::Over => { - label = label.with_message(format!( - "For this {} S, {} is over-approximated i.e., vc[S] ≥ {}[S]", - statement_str, calculus, calculus - )) - } - ApproximationKind::Under => { - label = label.with_message(format!( - "For this {} S, {} is under-approximated i.e., vc[S] ≤ {}[S]", - statement_str, calculus, calculus - )); - } - _ => {} - } - } - label - }) - .collect_vec(); - - let overall_approx = infimum_approximation_list(&soundness_blame.approximations); - - let is_both_over_and_under = soundness_blame - .approximations - .iter() - .any(|approx| approx.kind == ApproximationKind::Over) - && soundness_blame - .approximations - .iter() - .any(|approx| approx.kind == ApproximationKind::Under); - - let approx_note: Option = if let Some(calculus) = soundness_blame.calculus { - match overall_approx { - ApproximationKind::Over => Some(format!( - "the {} of the program is over-approximated, i.e., vc[program] ≥ {}[program]", - calculus, calculus - )), - ApproximationKind::Under => Some(format!( - "the {} of the program is under-approximated, i.e., vc[program] ≤ {}[program]", - calculus, calculus - )), - ApproximationKind::Unknown => { - if is_both_over_and_under { - Some(format!( - "the {} of the program is both over- and under-approximated in different parts of the program, therefore the approximation relationship for the whole program is unknown.", - calculus, - )) - } else { - Some(format!( - "the approximation relationship of the vc and the {} of the program is unknown.", - calculus, - )) - } - } - _ => None, - } - } else { - None - }; + let approximation_labels = proc_soundness.diagnostic_labels(); + let approx_note = proc_soundness.diagnostic_note(); match &mut self.prove_result { ProveResult::Proof => { - if matches!( - soundness_blame.soundness, - Soundness::Refutation | Soundness::Unknown - ) { - let msg = if approx_note.is_some() { - format!( - "The verification result might be unsound because {}", - approx_note.unwrap() - ) + 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 is unsound.".to_string() + "The verification result might be unsound.".to_string() }; let diag = Diagnostic::new(ReportKind::Warning, span) @@ -719,14 +639,12 @@ impl<'ctx> SmtVcProveResult<'ctx> { .with_message(text) .with_labels(labels); - let diagnostic = match soundness_blame.soundness { - Soundness::Proof | Soundness::Unknown => { - // This counter-example might be spurious, add a diagnostic - diagnostic - .with_note("This counter-example might be spurious and might not apply to the real program.") - .with_labels(approximation_labels) - } - Soundness::Refutation | Soundness::Exact => diagnostic, + 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)?; } diff --git a/src/proof_rules/calculus/soundness_checker.rs b/src/proof_rules/calculus/soundness_checker.rs index dcae1980..f3e62b9c 100644 --- a/src/proof_rules/calculus/soundness_checker.rs +++ b/src/proof_rules/calculus/soundness_checker.rs @@ -1,121 +1,310 @@ -use std::{collections::HashMap, fmt, ops::DerefMut, vec}; +use std::{ + collections::HashMap, + fmt, + ops::{BitAnd, BitOr, DerefMut}, + vec, +}; + +use itertools::Itertools; use crate::{ - ast::{Block, DeclKind, Direction, ProcDecl, Span, Stmt, StmtKind}, + ast::{Block, DeclKind, Direction, Label, ProcDecl, Span, Stmt, StmtKind}, driver::{ front::{Module, SourceUnit}, item::SourceUnitName, }, intrinsic::annotations::{AnnotationKind, Calculus}, - proof_rules::{get_calculus, infer_fixpoint_semantics_kind}, + proof_rules::{get_proc_calculus, infer_fixpoint_semantics_kind}, tyctx::TyCtx, }; #[derive(Debug, Clone)] -pub struct ApproximationListEntry { +pub enum StmtKindName { + Stmt, + Loop, +} + +impl fmt::Display for StmtKindName { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + StmtKindName::Stmt => write!(f, "statement"), + StmtKindName::Loop => write!(f, "loop"), + } + } +} + +#[derive(Debug, Clone)] +pub struct ApproximationRecord { pub span: Span, - pub is_loop: bool, + pub stmt_kind: StmtKindName, pub kind: ApproximationKind, } -pub type ApproximationList = Vec; +#[derive(Debug, Clone, Default)] +pub struct ApproximationList(pub Vec); -// pub type SoundnessBlame = (Soundness, ApproximationList); +impl IntoIterator for ApproximationList { + type Item = ApproximationRecord; + type IntoIter = std::vec::IntoIter; + fn into_iter(self) -> Self::IntoIter { + self.0.into_iter() + } +} -#[derive(Debug, Clone, Default)] -pub struct SoundnessBlame { - pub soundness: Soundness, - pub approximations: ApproximationList, - pub calculus: Option, +impl<'a> IntoIterator for &'a ApproximationList { + type Item = &'a ApproximationRecord; + type IntoIter = std::slice::Iter<'a, ApproximationRecord>; + fn into_iter(self) -> Self::IntoIter { + self.0.iter() + } } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)] -pub enum ApproximationKind { - #[default] - Exact, - Under, - Over, - Unknown, +impl<'a> IntoIterator for &'a mut ApproximationList { + type Item = &'a mut ApproximationRecord; + type IntoIter = std::slice::IterMut<'a, ApproximationRecord>; + fn into_iter(self) -> Self::IntoIter { + self.0.iter_mut() + } } -impl ApproximationKind { - pub fn supremum(self, other: ApproximationKind) -> ApproximationKind { - match self.partial_cmp(&other) { - Some(std::cmp::Ordering::Equal) => self, - Some(std::cmp::Ordering::Less) => other, - Some(std::cmp::Ordering::Greater) => self, - None => ApproximationKind::Exact, // If they are incomparable, return Exact (which is the top element) +impl ApproximationList { + pub fn infimum(&self) -> ApproximationKind { + self.0 + .iter() + .fold(ApproximationKind::EXACT, |acc, approx_entry| { + acc & approx_entry.kind + }) + } + + // convenience helpers + pub fn push(&mut self, rec: ApproximationRecord) { + self.0.push(rec) + } + + pub fn iter(&self) -> std::slice::Iter<'_, ApproximationRecord> { + self.0.iter() + } +} + +impl From> for ApproximationList { + fn from(v: Vec) -> Self { + ApproximationList(v) + } +} + +impl std::ops::Deref for ApproximationList { + type Target = Vec; + fn deref(&self) -> &Self::Target { + &self.0 + } +} + +impl std::ops::DerefMut for ApproximationList { + fn deref_mut(&mut self) -> &mut Self::Target { + &mut self.0 + } +} + +#[derive(Debug, Clone, Default)] +pub struct ProcSoundness { + sound_proofs: bool, + sound_refutations: bool, + approximations: ApproximationList, + calculus: Option, +} + +impl ProcSoundness { + /// Create a new ProcSoundness instance by analyzing the given approximations and calculus in the given direction. + pub fn new( + direction: Direction, + approximations: ApproximationList, + calculus: Option, + ) -> Self { + let approx = approximations.infimum(); + // The mapping between approximation kinds and soundness is as follows: + // (approximation.under, approximation.over) -> (sound_proofs, sound_refutations) + // Direction::Down: + // exact = (false,false) -> (true, true) + // (true,false) -> (true, false) + // (false,true) -> (false, true) + // unknown = (true,true) -> (false, false) + // Direction::Up : + // exact = (false,false) -> (true, true) + // (true,false) -> (false, true) + // (false,true) -> (true, false) + // unknown = (true,true) -> (false, false) + + // XOR with "approx.over == approx.under" to only flip (false,false) and (true,true) (see mapping above). + let over_approx = approx.over ^ (approx.over == approx.under); + let under_approx = approx.under ^ (approx.over == approx.under); + let (sound_proofs, sound_refutations) = match direction { + Direction::Down => (under_approx, over_approx), + Direction::Up => (over_approx, under_approx), + }; + Self { + sound_proofs, + sound_refutations, + approximations, + calculus, } } - pub fn infimum(self, other: ApproximationKind) -> ApproximationKind { - match self.partial_cmp(&other) { - Some(std::cmp::Ordering::Equal) => self, - Some(std::cmp::Ordering::Less) => self, - Some(std::cmp::Ordering::Greater) => other, - None => ApproximationKind::Unknown, // If they are incomparable, return Unknown (which is the bottom element) + + /// Get whether proofs for this procedure are sound. + pub fn sound_proofs(&self) -> bool { + self.sound_proofs + } + + /// Get whether refutations for this procedure are sound. + pub fn sound_refutations(&self) -> bool { + self.sound_refutations + } + + /// Generate diagnostic labels for all approximating statements in the procedure. + pub fn diagnostic_labels(&self) -> Vec