diff --git a/src/driver/commands/refinement.rs b/src/driver/commands/refinement.rs index 3f5c285e..6d29e8cd 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::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. diff --git a/src/driver/commands/verify.rs b/src/driver/commands/verify.rs index 4fcf54e7..2c6e8abc 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,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. diff --git a/src/driver/core_verify.rs b/src/driver/core_verify.rs index 16a7219e..9fc5b6d3 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::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(), }), } } diff --git a/src/driver/smt_proof.rs b/src/driver/smt_proof.rs index 098c5884..23a61527 100644 --- a/src/driver/smt_proof.rs +++ b/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 { 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) => { 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..cb802df0 --- /dev/null +++ b/src/proof_rules/calculus/soundness_checker.rs @@ -0,0 +1,425 @@ +use std::{ + collections::HashMap, + fmt, + ops::{BitAnd, BitOr, DerefMut}, + vec, +}; + +use itertools::Itertools; + +use crate::{ + ast::{Block, DeclKind, Direction, Label, ProcDecl, Span, Stmt, StmtKind}, + driver::{ + front::{Module, SourceUnit}, + item::SourceUnitName, + }, + intrinsic::annotations::{AnnotationKind, Calculus}, + proof_rules::{get_proc_calculus, infer_fixpoint_semantics_kind}, + tyctx::TyCtx, +}; + +#[derive(Debug, Clone)] +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 stmt_kind: StmtKindName, + pub kind: ApproximationKind, +} + +pub type ApproximationList = Vec; + +/// Compute the infimum of approximation kinds in the given approximation list. +/// +/// This is done by folding the list with the `BitAnd` operation defined for `ApproximationKind`. +/// +/// --- +/// +/// Examples: +/// +/// If `approximations` is empty, the default value is `ApproximationKind::EXACT` as an empty list means no approximations were made. +/// ``` +/// let approximations = vec![]; +/// assert_eq!(infimum_of_approximation_list(&approximations), ApproximationKind::EXACT); +/// ``` +/// +/// +/// If it contains only one entry, that entry's kind is returned. +/// +/// ``` +/// let approximations = vec![ +/// ApproximationRecord { span: Span::dummy_span(), stmt_kind: StmtKindName::Stmt, kind: ApproximationKind::OVER }, +/// ]; +/// assert_eq!(infimum_of_approximation_list(&approximations), ApproximationKind::OVER); +/// ``` +/// +/// If it contains two or more entries, the infimum of all their kinds is returned. +/// +/// ``` +/// let approximations = vec![ +/// ApproximationRecord { span: Span::dummy_span(), stmt_kind: StmtKindName::Stmt, kind: ApproximationKind::OVER }, +/// ApproximationRecord { span: Span::dummy_span(), stmt_kind: StmtKindName::Loop, kind: ApproximationKind::UNDER }, +/// ]; +/// assert_eq!(infimum_of_approximation_list(&approximations), ApproximationKind::UNKNOWN); +pub fn infimum_of_approximation_list(approximations: &ApproximationList) -> ApproximationKind { + approximations + .iter() + .fold(ApproximationKind::EXACT, |acc, approx_entry| { + acc & approx_entry.kind + }) +} + +#[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 { + // If the approximation list is empty, it means no approximations were made, therefore the infimum is EXACT + let approx = infimum_of_approximation_list(&approximations); + let (sound_proofs, sound_refutations) = match direction { + Direction::Down => match approx { + ApproximationKind::EXACT => (true, true), // Both proofs and refutations are sound + ApproximationKind::UNDER => (true, false), // Only proofs are guaranteed to be sound + ApproximationKind::OVER => (false, true), // Only refutations are guaranteed to be sound + ApproximationKind::UNKNOWN => (false, false), // Neither proofs nor refutations are sound + }, + Direction::Up => match approx { + ApproximationKind::EXACT => (true, true), // Both proofs and refutations are sound + ApproximationKind::UNDER => (false, true), // Only refutations are guaranteed to be sound + ApproximationKind::OVER => (true, false), // Only proofs are guaranteed to be sound + ApproximationKind::UNKNOWN => (false, false), // Neither proofs nor refutations are sound + }, + }; + Self { + sound_proofs, + sound_refutations, + approximations, + calculus, + } + } + + /// 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