From 3851b1314626eef4083aa11cd3e5238a3abea9f9 Mon Sep 17 00:00:00 2001 From: madita Date: Tue, 7 Oct 2025 16:51:55 +0200 Subject: [PATCH 01/10] get-models: Add command to get models for preexpectations --- src/driver/commands/get_pre_models.rs | 177 ++++++++++++++++++++++++++ src/driver/commands/mod.rs | 7 + src/driver/commands/refinement.rs | 5 +- src/driver/commands/verify.rs | 3 +- src/driver/core_verify.rs | 15 ++- src/driver/smt_proof.rs | 48 ++++++- src/procs/proc_verify.rs | 75 ++++++++++- src/servers/cli.rs | 7 +- src/servers/lsp.rs | 1 + src/servers/mod.rs | 3 +- src/servers/test.rs | 1 + 11 files changed, 331 insertions(+), 11 deletions(-) create mode 100644 src/driver/commands/get_pre_models.rs diff --git a/src/driver/commands/get_pre_models.rs b/src/driver/commands/get_pre_models.rs new file mode 100644 index 00000000..47aa0d7e --- /dev/null +++ b/src/driver/commands/get_pre_models.rs @@ -0,0 +1,177 @@ +use std::{ops::DerefMut, process::ExitCode, sync::Arc}; + +use z3rro::{prover::ProveResult, util::ReasonUnknown}; + +use crate::{ + ast::FileId, + driver::{ + commands::{mk_cli_server, print_timings, verify::VerifyCommand}, + core_verify::{lower_core_verify_task, CoreVerifyTask}, + error::{finalize_caesar_result, CaesarError}, + front::parse_and_tycheck, + item::Item, + quant_proof::lower_quant_prove_task, + smt_proof::set_global_z3_params, + }, + resource_limits::{await_with_resource_limits, LimitError, LimitsRef}, + servers::{Server, SharedServer}, +}; + +pub async fn run_get_model_command(options: VerifyCommand) -> ExitCode { + let (user_files, server) = match mk_cli_server(&options.input_options) { + Ok(value) => value, + Err(value) => return value, + }; + let options = Arc::new(options); + let get_models_result = get_model_files(&options, &server, user_files).await; + + if options.debug_options.timing { + print_timings(); + } + + finalize_caesar_result(server, &options.rlimit_options, get_models_result) +} + +/// This is just like verify_files() +pub async fn get_model_files( + options: &Arc, + server: &SharedServer, + user_files: Vec, +) -> Result { + let handle = |limits_ref: LimitsRef| { + let options = options.clone(); + let server = server.clone(); + tokio::task::spawn_blocking(move || { + // execute the verifier with a larger stack size of 50MB. the + // default stack size might be quite small and we need to do quite a + // lot of recursion. + let stack_size = 50 * 1024 * 1024; + stacker::maybe_grow(stack_size, stack_size, move || { + let mut server = server.lock().unwrap(); + get_model_files_main(&options, limits_ref, server.deref_mut(), &user_files) + }) + }) + }; + // Unpacking lots of Results with `.await??` :-) + await_with_resource_limits( + Some(options.rlimit_options.timeout()), + Some(options.rlimit_options.mem_limit()), + handle, + ) + .await?? +} + +fn get_model_files_main( + options: &VerifyCommand, + limits_ref: LimitsRef, + server: &mut dyn Server, + user_files: &[FileId], +) -> Result { + let (mut module, mut tcx) = parse_and_tycheck( + &options.input_options, + &options.debug_options, + server, + user_files, + )?; + + // Register all relevant source units with the server + module.register_with_server(server)?; + + // explain high-level HeyVL if requested + if options.lsp_options.explain_vc { + module.explain_high_level_vc(&tcx, &limits_ref, server)?; + } + + // Desugar encodings from source units. + module.apply_encodings(&mut tcx, server)?; + + if options.debug_options.print_core_procs { + println!("HeyVL get model task with generated procs:"); + println!("{module}"); + } + + // generate dependency graph to determine which declarations are needed for + // the SMT translation later + let mut depgraph = module.generate_depgraph(&options.opt_options.function_encoding)?; + + // here the translation from the program to the relevant preexpectation conditions happens + let mut verify_units: Vec> = module + .items + .into_iter() + .flat_map(|item| { + item.flat_map(|unit| CoreVerifyTask::from_source_unit(unit, &mut depgraph, true)) + }) + .collect(); + + if options.debug_options.z3_trace && verify_units.len() > 1 { + tracing::warn!("Z3 tracing is enabled with multiple units. Intermediate tracing results will be overwritten."); + } + // set requested global z3 options + set_global_z3_params(options, &limits_ref); + + let mut num_sat: usize = 0; + let mut num_unsat: usize = 0; + + for verify_unit in &mut verify_units { + limits_ref.check_limits()?; + + let (name, mut verify_unit) = verify_unit.enter_with_name(); + + // Set the current unit as ongoing + server.set_ongoing_unit(name)?; + + // no slicing + let mut new_options = VerifyCommand::default(); + new_options.slice_options.no_slice_error = true; + + let (vc_expr, slice_vars) = lower_core_verify_task( + &mut tcx, + name, + &new_options, + &limits_ref, + server, + &mut verify_unit, + )?; + // Lowering the quantitative task to a Boolean one. This contains (lazy) + // unfolding, quantifier elimination, and various optimizations + // (depending on options). + let vc_is_valid = lower_quant_prove_task(options, &limits_ref, &mut tcx, name, vc_expr)?; + + // Running the SMT prove task: translating to Z3, running the solver. + let result = crate::driver::smt_proof::run_smt_prove_task( + options, + &limits_ref, + &tcx, + &depgraph, + name, + server, + slice_vars, + vc_is_valid, + true, + )?; + + // Handle reasons to stop the verifier. + match result { + ProveResult::Unknown(ReasonUnknown::Interrupted) => { + return Err(CaesarError::Interrupted) + } + ProveResult::Unknown(ReasonUnknown::Timeout) => return Err(LimitError::Timeout.into()), + _ => {} + } + + // Increment counters. + match result { + ProveResult::Counterexample => num_sat += 1, + ProveResult::Proof | ProveResult::Unknown(_) => num_unsat += 1, + } + } + + if !options.lsp_options.language_server { + println!(); + println!( + "Found models for {num_sat} (co)procedures, No models for {num_unsat} (co)procedures." + ); + } + + Ok(num_unsat == 0) +} diff --git a/src/driver/commands/mod.rs b/src/driver/commands/mod.rs index b09d0318..61973165 100644 --- a/src/driver/commands/mod.rs +++ b/src/driver/commands/mod.rs @@ -1,5 +1,6 @@ //! (CLI) command and option declarations to run Caesar with. +pub mod get_pre_models; pub mod model_check; pub mod options; pub mod refinement; @@ -19,6 +20,7 @@ use clap::{crate_description, Args, CommandFactory, Parser, Subcommand}; use crate::{ ast::FileId, driver::commands::{ + get_pre_models::run_get_model_command, model_check::{run_model_checking_command, ModelCheckCommand}, options::{DebugOptions, InputOptions}, refinement::run_verify_entailment_command, @@ -65,6 +67,7 @@ impl CaesarCli { CaesarCommand::Mc(options) => run_model_checking_command(options), CaesarCommand::Lsp(options) => run_lsp_command(options).await, CaesarCommand::ShellCompletions(options) => run_shell_completions_command(options), + CaesarCommand::GetPreModels(options) => run_get_model_command(options).await, CaesarCommand::Other(_) => unreachable!(), } } @@ -98,6 +101,9 @@ pub enum CaesarCommand { Lsp(VerifyCommand), /// Generate shell completions for the Caesar binary. ShellCompletions(ShellCompletionsCommand), + /// Get non-trivial models for preexpectation. + #[clap(visible_alias = "get-models")] + GetPreModels(VerifyCommand), /// This is to support the default `verify` command. #[command(external_subcommand)] #[command(hide(true))] @@ -112,6 +118,7 @@ impl CaesarCommand { CaesarCommand::Lsp(verify_options) => Some(&verify_options.debug_options), CaesarCommand::Mc(mc_options) => Some(&mc_options.debug_options), CaesarCommand::ShellCompletions(_) => None, + CaesarCommand::GetPreModels(verify_options) => Some(&verify_options.debug_options), CaesarCommand::Other(_vec) => unreachable!(), } } diff --git a/src/driver/commands/refinement.rs b/src/driver/commands/refinement.rs index 3f5c285e..a715edaf 100644 --- a/src/driver/commands/refinement.rs +++ b/src/driver/commands/refinement.rs @@ -121,10 +121,10 @@ async fn verify_entailment( }; let mut first_verify_unit = first - .flat_map(|u| CoreVerifyTask::from_source_unit(u, &mut depgraph)) + .flat_map(|u| CoreVerifyTask::from_source_unit(u, &mut depgraph, false)) .unwrap(); let mut second_verify_unit = second - .flat_map(|u| CoreVerifyTask::from_source_unit(u, &mut depgraph)) + .flat_map(|u| CoreVerifyTask::from_source_unit(u, &mut depgraph, false)) .unwrap(); let (first_vc, first_slice_stmts) = lower_core_verify_task( @@ -163,6 +163,7 @@ async fn verify_entailment( server, slice_vars, vc_is_valid, + false, )?; // Handle reasons to stop the verifier. diff --git a/src/driver/commands/verify.rs b/src/driver/commands/verify.rs index 4fcf54e7..0bbd3a77 100644 --- a/src/driver/commands/verify.rs +++ b/src/driver/commands/verify.rs @@ -215,7 +215,7 @@ fn verify_files_main( .items .into_iter() .flat_map(|item| { - item.flat_map(|unit| CoreVerifyTask::from_source_unit(unit, &mut depgraph)) + item.flat_map(|unit| CoreVerifyTask::from_source_unit(unit, &mut depgraph, false)) }) .collect(); @@ -264,6 +264,7 @@ fn verify_files_main( server, slice_vars, vc_is_valid, + false, )?; // Handle reasons to stop the verifier. diff --git a/src/driver/core_verify.rs b/src/driver/core_verify.rs index 16a7219e..c78716d8 100644 --- a/src/driver/core_verify.rs +++ b/src/driver/core_verify.rs @@ -21,7 +21,7 @@ use crate::{ }, pretty::{Doc, SimplePretty}, procs::{ - proc_verify::{encode_proc_verify, to_direction_lower_bounds}, + proc_verify::{encode_pre_get_model, encode_proc_verify, to_direction_lower_bounds}, SpecCall, }, resource_limits::LimitsRef, @@ -76,7 +76,11 @@ impl CoreVerifyTask { /// Convert this source unit into a [`CoreVerifyTask`]. Some declarations, /// such as domains or functions, do not generate any verify units. In these /// cases, `None` is returned. - pub fn from_source_unit(mut source_unit: SourceUnit, depgraph: &mut DepGraph) -> Option { + pub fn from_source_unit( + mut source_unit: SourceUnit, + depgraph: &mut DepGraph, + is_get_model_task: bool, + ) -> Option { let deps = match &mut source_unit { SourceUnit::Decl(decl) => depgraph.get_reachable([decl.name()]), SourceUnit::Raw(block) => { @@ -91,7 +95,12 @@ impl CoreVerifyTask { SourceUnit::Decl(decl) => { match decl { DeclKind::ProcDecl(proc_decl) => { - let (direction, block) = encode_proc_verify(&proc_decl.borrow())?; + let (direction, block) = if is_get_model_task { + encode_pre_get_model(&proc_decl.borrow())? + } else { + encode_proc_verify(&proc_decl.borrow())? + }; + Some(CoreVerifyTask { deps, direction, diff --git a/src/driver/smt_proof.rs b/src/driver/smt_proof.rs index 098c5884..b9a74b1d 100644 --- a/src/driver/smt_proof.rs +++ b/src/driver/smt_proof.rs @@ -141,6 +141,7 @@ pub fn run_smt_prove_task( server: &mut dyn Server, slice_vars: SliceStmts, vc_is_valid: BoolVcProveTask, + is_get_model_task: bool, ) -> Result { let ctx = Context::new(&z3::Config::default()); let function_encoder = mk_function_encoder(tcx, depgraph, options)?; @@ -161,7 +162,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, is_get_model_task) .map_err(CaesarError::ServerError)?; Ok(result.prove_result) @@ -282,7 +283,6 @@ impl<'ctx> SmtVcProveTask<'ctx> { vc: bool_vc, } } - /// Simplify the SMT formula using Z3's simplifier. pub fn simplify(&mut self) { let span = info_span!("simplify query"); @@ -636,3 +636,47 @@ impl<'ctx> SmtVcProveResult<'ctx> { Ok(()) } } + +impl<'ctx> SmtVcProveResult<'ctx> { + /// Print the result of the query to stdout. + pub fn print_prove_result_get_model<'smt>( + &mut self, + server: &mut dyn Server, + translate: &mut TranslateExprs<'smt, 'ctx>, + name: &SourceUnitName, + ) { + let files = server.get_files_internal().lock().unwrap(); + match &mut self.prove_result { + ProveResult::Proof => { + println!("{name}: The bound introduced by the preexpectations is always trivial (bottom for proc/top for coproc)"); + } + ProveResult::Counterexample => { + let model = self.model.as_ref().unwrap(); + println!( + "{name}: A non-trivial bound is given for example by the following model:" + ); + let mut w = Vec::new(); + let doc = pretty_model( + &files, + self.slice_model.as_ref().unwrap(), + &self.quant_vc, + translate, + model, + ); + doc.nest(4).render(120, &mut w).unwrap(); + println!(" {}", String::from_utf8(w).unwrap()); + } + ProveResult::Unknown(reason) => { + println!("{name}: Unknown result! (reason: {reason})"); + if let Some(slice_model) = &self.slice_model { + let doc = pretty_slice(&files, slice_model); + if let Some(doc) = doc { + let mut w = Vec::new(); + doc.nest(4).render(120, &mut w).unwrap(); + println!(" {}", String::from_utf8(w).unwrap()); + } + } + } + } + } +} diff --git a/src/procs/proc_verify.rs b/src/procs/proc_verify.rs index 5e8bad7d..b2f79743 100644 --- a/src/procs/proc_verify.rs +++ b/src/procs/proc_verify.rs @@ -1,9 +1,82 @@ use crate::{ - ast::{Block, Direction, ProcDecl, SpanVariant, Spanned, StmtKind}, + ast::{ + self, BinOpKind, Block, Direction, ExprData, ExprKind, ProcDecl, Shared, Span, SpanVariant, + Spanned, StmtKind, TyKind, UnOpKind, + }, driver::core_verify::CoreVerifyTask, slicing::{wrap_with_error_message, wrap_with_success_message}, }; +/// Encode the preexpectations as a formula for which counterexamples are satisfying valuations +/// of the preexpectations. +/// For proc: +/// goal: Find a model such that (pre1 ⊓ pre2 ⊓...) > 0 +/// (pre1 ⊓ pre2 ⊓...) = 0 iff !(pre1 ⊓ pre2 ⊓...) = top +/// (pre1 ⊓ pre2 ⊓...) > 0 iff !(pre1 ⊓ pre2 ⊓...) = 0 +/// find cex for: !(pre1 ⊓ pre2 ⊓...) +/// For coproc: +/// goal: Find a model such that (pre1 ⊔ pre2 ⊔...) < top +/// (pre1 ⊔ pre2 ⊔...) = top iff ~(pre1 ⊔ pre2 ⊔...) = 0 +/// (pre1 ⊔ pre2 ⊔...) < top iff ~(pre1 ⊔ pre2 ⊔...) = top +/// find cex for: ~(pre1 ⊔ pre2 ⊔...) +pub fn encode_pre_get_model(proc: &ProcDecl) -> Option<(Direction, Block)> { + let direction = proc.direction; + + let body_ref = proc.body.borrow(); + let body = match &*body_ref { + Some(body) => body, + None => return None, + }; + let mut block = Spanned::new(body.span, vec![]); + + fn get_combination(direction: Direction) -> ast::expr::BinOpKind { + let combination = match direction { + Direction::Down => BinOpKind::Inf, + Direction::Up => BinOpKind::Sup, + }; + combination + } + + fn get_negation_type(direction: Direction) -> ast::expr::UnOpKind { + let negation_type = match direction { + Direction::Down => UnOpKind::Not, + Direction::Up => UnOpKind::Non, + }; + negation_type + } + + // push the assume statement for each requires + let mut build_expr = proc + .requires() + .next() + .expect("No preconditions to check") + .clone(); + for expr in proc.requires().skip(1) { + build_expr = Shared::new(ExprData { + kind: ExprKind::Binary( + Spanned::with_dummy_span(get_combination(direction)), + build_expr, + expr.clone(), + ), + ty: Some(TyKind::EUReal), + span: Span::dummy_span(), + }); + } + + build_expr = Shared::new(ExprData { + kind: ExprKind::Unary( + Spanned::with_dummy_span(get_negation_type(direction)), + build_expr, + ), + ty: Some(TyKind::EUReal), + span: Span::dummy_span(), + }); + block.node.push(Spanned::new( + Span::dummy_span(), + StmtKind::Assert(direction, build_expr), + )); + Some((direction, block)) +} /// Generates the HeyVL code to verify a procedure implementation. Returns /// `None` if the proc has no body does not need verification. /// diff --git a/src/servers/cli.rs b/src/servers/cli.rs index b96b8299..dab38ee7 100644 --- a/src/servers/cli.rs +++ b/src/servers/cli.rs @@ -112,8 +112,13 @@ impl Server for CliServer { name: &SourceUnitName, result: &mut SmtVcProveResult<'ctx>, translate: &mut TranslateExprs<'smt, 'ctx>, + is_get_model_task: bool, ) -> Result<(), ServerError> { - result.print_prove_result(self, translate, name); + if is_get_model_task { + result.print_prove_result_get_model(self, translate, name); + } else { + result.print_prove_result(self, translate, name); + } Ok(()) } diff --git a/src/servers/lsp.rs b/src/servers/lsp.rs index 089ab525..283d812d 100644 --- a/src/servers/lsp.rs +++ b/src/servers/lsp.rs @@ -427,6 +427,7 @@ impl Server for LspServer { name: &SourceUnitName, result: &mut SmtVcProveResult<'ctx>, translate: &mut TranslateExprs<'smt, 'ctx>, + _is_get_model_task: bool, ) -> Result<(), ServerError> { result.emit_diagnostics(name.span(), self, translate)?; let statuses = &mut self diff --git a/src/servers/mod.rs b/src/servers/mod.rs index 4316516a..76d41ee4 100644 --- a/src/servers/mod.rs +++ b/src/servers/mod.rs @@ -191,8 +191,9 @@ pub trait Server: Send { name: &SourceUnitName, result: &mut SmtVcProveResult<'ctx>, translate: &mut TranslateExprs<'smt, 'ctx>, + is_get_model_task: bool, ) -> Result<(), ServerError>; - + /// Return an exit code for the process. /// /// Default implementation returns `ExitCode::SUCCESS`. diff --git a/src/servers/test.rs b/src/servers/test.rs index 371a0371..9253a632 100644 --- a/src/servers/test.rs +++ b/src/servers/test.rs @@ -105,6 +105,7 @@ impl Server for TestServer { name: &SourceUnitName, result: &mut SmtVcProveResult<'ctx>, _translate: &mut TranslateExprs<'smt, 'ctx>, + _is_get_model_task: bool, ) -> Result<(), ServerError> { let statuses = &mut self .file_statuses From 257c3c7073943a0778468a9e42067189a1d16d40 Mon Sep 17 00:00:00 2001 From: madita Date: Mon, 20 Oct 2025 13:40:20 +0200 Subject: [PATCH 02/10] get-models: Add pretty models --- src/driver/smt_proof.rs | 3 +- src/smt/pretty_model.rs | 144 +++++++++++++++++++++++++++++++++++++++- 2 files changed, 145 insertions(+), 2 deletions(-) diff --git a/src/driver/smt_proof.rs b/src/driver/smt_proof.rs index b9a74b1d..6d242fd5 100644 --- a/src/driver/smt_proof.rs +++ b/src/driver/smt_proof.rs @@ -35,6 +35,7 @@ use crate::smt::funcs::fuel::{ FuelEncodingOptions, FuelMonoFunctionEncoder, FuelParamFunctionEncoder, }; use crate::smt::funcs::{FunctionEncoder, RecFunFunctionEncoder}; +use crate::smt::pretty_model::pretty_get_models_model; use crate::smt::{DepConfig, SmtCtx}; use crate::tyctx::TyCtx; use crate::{ @@ -656,7 +657,7 @@ impl<'ctx> SmtVcProveResult<'ctx> { "{name}: A non-trivial bound is given for example by the following model:" ); let mut w = Vec::new(); - let doc = pretty_model( + let doc = pretty_get_models_model( &files, self.slice_model.as_ref().unwrap(), &self.quant_vc, diff --git a/src/smt/pretty_model.rs b/src/smt/pretty_model.rs index 00c2f72f..3d56b129 100644 --- a/src/smt/pretty_model.rs +++ b/src/smt/pretty_model.rs @@ -8,7 +8,8 @@ use z3rro::model::{InstrumentedModel, ModelConsistency, SmtEvalError}; use crate::{ ast::{ decl::{DeclKind, DeclKindName}, - ExprBuilder, Files, Ident, Span, VarKind, + BinOpKind, Expr, ExprBuilder, ExprData, ExprKind, Files, Ident, LitKind, Shared, Span, + UnOpKind, VarKind, }, driver::quant_proof::QuantVcProveTask, pretty::Doc, @@ -47,6 +48,147 @@ pub fn pretty_model<'smt, 'ctx>( Doc::intersperse(res, Doc::line_().append(Doc::line_())).append(Doc::line_()) } +/// Pretty-print a model for get models. +pub fn pretty_get_models_model<'smt, 'ctx>( + files: &Files, + slice_model: &SliceModel, + vc_expr: &QuantVcProveTask, + translate: &mut TranslateExprs<'smt, 'ctx>, + model: &InstrumentedModel<'ctx>, +) -> Doc { + let mut res: Vec = vec![]; + + // Print the values of the global variables in the model. + pretty_globals(translate, model, files, &mut res); + + let slice_lines = pretty_slice(files, slice_model); + + // Print the unaccessed definitions. + if let Some(unaccessed) = pretty_unaccessed(model) { + res.push(unaccessed); + } + + if let Some(slice_lines) = slice_lines { + res.push(slice_lines); + } + + res.push(pretty_get_models_value( + vc_expr, + translate, + model, + slice_model, + )); + + Doc::intersperse(res, Doc::line_().append(Doc::line_())).append(Doc::line_()) +} + +fn deref_cast(e: &Expr) -> &Expr { + match &e.kind { + ExprKind::Cast(inner) => deref_cast(inner), + _ => e, + } +} + +fn is_infinity_or_negated_infinity(expr: &Shared) -> bool { + match &expr.clone().kind { + ExprKind::Lit(lit) if matches!(lit.node, LitKind::Infinity) => true, + ExprKind::Unary(op, inner) if matches!(op.node, UnOpKind::Not | UnOpKind::Non) => { + matches!(&inner.clone().kind, ExprKind::Lit(lit) if matches!(lit.node, LitKind::Infinity)) + } + _ => false, + } +} + +fn strip_outer_negation(expr: &Shared) -> Shared { + match &expr.clone().kind { + ExprKind::Unary(op, inner) if op.node == UnOpKind::Not || op.node == UnOpKind::Non => { + inner.clone() + } + _ => expr.clone(), + } +} + +fn strip_inf_or_sup_with_infinity(expr: &Expr) -> Option> { + match &deref_cast(expr).kind { + ExprKind::Binary(op, left, right) + if op.node == BinOpKind::Inf || op.node == BinOpKind::Sup => + { + let left_expr = left.clone(); + let right_expr = right.clone(); + + let is_left_infinity = is_infinity_or_negated_infinity(&left_expr); + let is_right_infinity = is_infinity_or_negated_infinity(&right_expr); + + match (is_left_infinity, is_right_infinity) { + (true, false) => Some(right_expr), + (false, true) => Some(left_expr), + (true, true) => Some(expr.clone()), // both sides are (negated) ∞ + (false, false) => Some(expr.clone()), // neither side is (negated) ∞ (should not happen) + } + } + _ => Some(expr.clone()), // not an Inf/Sup — return as-is + } +} + +pub fn pretty_get_models_value<'smt, 'ctx>( + vc_expr: &QuantVcProveTask, + translate: &mut TranslateExprs<'smt, 'ctx>, + model: &InstrumentedModel<'ctx>, + slice_model: &SliceModel, +) -> Doc { + let original_program_vc = if slice_model.count_sliced_stmts() == 0 { + vc_expr.expr.clone() + } else { + // reconstruct the original program's vc by substituting the slice + // variables by `true`. + let builder = ExprBuilder::new(Span::dummy_span()); + let expr_true = builder.bool_lit(true); + let subst_expr = builder.subst_by( + vc_expr.expr.clone(), + slice_model.iter_variables(), + |_ident| expr_true.clone(), + ); + let mut res = subst_expr; + + // The limit error is not handled here, therefore discard the result + apply_subst(translate.ctx.tcx(), &mut res, &LimitsRef::new(None, None)).unwrap(); + + res + }; + + let mut lines = vec![]; + + let stripped = strip_outer_negation( + &strip_inf_or_sup_with_infinity(&original_program_vc.clone()).unwrap(), + ); + let ast = translate.t_symbolic(&stripped); + let value = ast.eval(model); + let res = pretty_eval_result(value); + lines.push( + Doc::text("the pre-quantity evaluated to:").append(Doc::hardline().append(res).nest(4)), + ); + + let num_sliced_stmts = slice_model.count_sliced_stmts(); + if num_sliced_stmts > 0 { + let ast = translate.t_symbolic(&vc_expr.expr); + let value = ast.eval(model); + let slice_pre = pretty_eval_result(value) + .append(Doc::line_()) + .append(Doc::text(format!( + "(slicing removed {}/{} assertions)", + num_sliced_stmts, + slice_model.len() + ))); + lines.push(Doc::nil()); + lines.push( + Doc::text("in the sliced program, the pre-quantity evaluated to:") + .append(Doc::hardline().append(slice_pre).nest(4)), + ); + } + + Doc::intersperse(lines, Doc::line()) +} + pub fn pretty_vc_value<'smt, 'ctx>( vc_expr: &QuantVcProveTask, translate: &mut TranslateExprs<'smt, 'ctx>, From 73c32d2db082ca77cd18aa51ea94c64bcbaf20ad Mon Sep 17 00:00:00 2001 From: madita Date: Tue, 21 Oct 2025 16:54:17 +0200 Subject: [PATCH 03/10] get-models: Linearize flow The steps should be separated back into functions, this is just for my understanding --- src/driver/commands/get_pre_models.rs | 190 ++++++++++++++++++++------ src/driver/commands/mod.rs | 4 +- src/driver/commands/refinement.rs | 1 - src/driver/commands/verify.rs | 1 - src/driver/core_verify.rs | 4 +- src/driver/smt_proof.rs | 54 +------- src/procs/proc_verify.rs | 31 +---- src/servers/cli.rs | 7 +- src/servers/lsp.rs | 1 - src/servers/mod.rs | 1 - src/servers/test.rs | 1 - src/smt/pretty_model.rs | 112 +-------------- 12 files changed, 169 insertions(+), 238 deletions(-) diff --git a/src/driver/commands/get_pre_models.rs b/src/driver/commands/get_pre_models.rs index 47aa0d7e..7dffb4e9 100644 --- a/src/driver/commands/get_pre_models.rs +++ b/src/driver/commands/get_pre_models.rs @@ -1,39 +1,45 @@ use std::{ops::DerefMut, process::ExitCode, sync::Arc}; -use z3rro::{prover::ProveResult, util::ReasonUnknown}; +use z3::{Context, SatResult}; +use z3rro::prover::{IncrementalMode, Prover}; use crate::{ - ast::FileId, + ast::{BinOpKind, Direction, ExprBuilder, FileId, Span, TyKind}, driver::{ commands::{mk_cli_server, print_timings, verify::VerifyCommand}, core_verify::{lower_core_verify_task, CoreVerifyTask}, error::{finalize_caesar_result, CaesarError}, front::parse_and_tycheck, item::Item, - quant_proof::lower_quant_prove_task, - smt_proof::set_global_z3_params, + quant_proof::BoolVcProveTask, + smt_proof::{ + get_smtlib, mk_function_encoder, set_global_z3_params, write_smtlib, SmtVcProveTask, + }, }, - resource_limits::{await_with_resource_limits, LimitError, LimitsRef}, + resource_limits::{await_with_resource_limits, LimitsRef}, servers::{Server, SharedServer}, + smt::{ + pretty_model::pretty_nontrivial_models_model, translate_exprs::TranslateExprs, DepConfig, SmtCtx, + }, }; -pub async fn run_get_model_command(options: VerifyCommand) -> ExitCode { +pub async fn run_nontrivial_model_command(options: VerifyCommand) -> ExitCode { let (user_files, server) = match mk_cli_server(&options.input_options) { Ok(value) => value, Err(value) => return value, }; let options = Arc::new(options); - let get_models_result = get_model_files(&options, &server, user_files).await; + let nontrivial_models_result = nontrivial_model_files(&options, &server, user_files).await; if options.debug_options.timing { print_timings(); } - finalize_caesar_result(server, &options.rlimit_options, get_models_result) + finalize_caesar_result(server, &options.rlimit_options, nontrivial_models_result) } /// This is just like verify_files() -pub async fn get_model_files( +pub async fn nontrivial_model_files( options: &Arc, server: &SharedServer, user_files: Vec, @@ -48,7 +54,7 @@ pub async fn get_model_files( let stack_size = 50 * 1024 * 1024; stacker::maybe_grow(stack_size, stack_size, move || { let mut server = server.lock().unwrap(); - get_model_files_main(&options, limits_ref, server.deref_mut(), &user_files) + nontrivial_model_files_main(&options, limits_ref, server.deref_mut(), &user_files) }) }) }; @@ -61,7 +67,7 @@ pub async fn get_model_files( .await?? } -fn get_model_files_main( +fn nontrivial_model_files_main( options: &VerifyCommand, limits_ref: LimitsRef, server: &mut dyn Server, @@ -86,7 +92,7 @@ fn get_model_files_main( module.apply_encodings(&mut tcx, server)?; if options.debug_options.print_core_procs { - println!("HeyVL get model task with generated procs:"); + println!("HeyVL get nontrivial model task with generated procs:"); println!("{module}"); } @@ -94,7 +100,7 @@ fn get_model_files_main( // the SMT translation later let mut depgraph = module.generate_depgraph(&options.opt_options.function_encoding)?; - // here the translation from the program to the relevant preexpectation conditions happens + // translate program to relevant preexpectation conditions let mut verify_units: Vec> = module .items .into_iter() @@ -124,7 +130,7 @@ fn get_model_files_main( let mut new_options = VerifyCommand::default(); new_options.slice_options.no_slice_error = true; - let (vc_expr, slice_vars) = lower_core_verify_task( + let (vc_expr, _slice_vars) = lower_core_verify_task( &mut tcx, name, &new_options, @@ -132,37 +138,143 @@ fn get_model_files_main( server, &mut verify_unit, )?; - // Lowering the quantitative task to a Boolean one. This contains (lazy) - // unfolding, quantifier elimination, and various optimizations - // (depending on options). - let vc_is_valid = lower_quant_prove_task(options, &limits_ref, &mut tcx, name, vc_expr)?; - - // Running the SMT prove task: translating to Z3, running the solver. - let result = crate::driver::smt_proof::run_smt_prove_task( - options, - &limits_ref, - &tcx, - &depgraph, - name, - server, - slice_vars, - vc_is_valid, - true, - )?; - // Handle reasons to stop the verifier. - match result { - ProveResult::Unknown(ReasonUnknown::Interrupted) => { - return Err(CaesarError::Interrupted) + // Lowering the quantitative task to a Boolean one. + let mut quant_task = vc_expr; + + // 1. Unfolding (applies substitutions) + quant_task.unfold(options, &limits_ref, &tcx)?; + + // TODO: How to deal with quantifier? + // 2. Quantifier elimination + // if !options.opt_options.no_qelim { + // quant_task.qelim(&mut tcx, &limits_ref)?; + // } + + // In-between, gather some stats about the vc expression + quant_task.trace_expr_stats(); + + + // 3. Now turn this quantitative formula into a Boolean one + let builder = ExprBuilder::new(Span::dummy_span()); + let top = builder.top_lit(quant_task.expr.ty.as_ref().unwrap()); + let bot = builder.bot_lit(quant_task.expr.ty.as_ref().unwrap()); + let expr = quant_task.expr.clone(); + + // Construct the condition based on quantifier direction + let res = match quant_task.direction { + Direction::Up => { + // For coprocs, check if expr < top + builder.binary(BinOpKind::Lt, Some(TyKind::Bool), expr, top) + } + Direction::Down => { + // For procs, check if expr > bot + builder.binary(BinOpKind::Gt, Some(TyKind::Bool), expr, bot) } - ProveResult::Unknown(ReasonUnknown::Timeout) => return Err(LimitError::Timeout.into()), + }; + + // Create a Boolean verification task with the comparison + let mut bool_task = BoolVcProveTask { + quant_vc: quant_task, + vc: res, + }; + + + // 4. Optimizations + // 4.1. Remove parentheses if needed + if !options.opt_options.no_boolify || options.opt_options.opt_rel { + bool_task.remove_parens(); + } + // 4.2 Boolify (enabled by default) + if !options.opt_options.no_boolify { + bool_task.opt_boolify(); + } + // 4.3. Relational optimization (disabled by default) + if options.opt_options.opt_rel { + bool_task.opt_relational(); + } + + // print theorem to prove if requested + if options.debug_options.print_theorem { + bool_task.print_theorem(name); + } + + + let ctx = Context::new(&z3::Config::default()); + let function_encoder = mk_function_encoder(&tcx, &depgraph, options)?; + let dep_config = DepConfig::Set(bool_task.get_dependencies()); + let smt_ctx = SmtCtx::new(&ctx, &tcx, function_encoder, dep_config); + let mut translate = TranslateExprs::new(&smt_ctx); + let mut vc_is_valid = SmtVcProveTask::translate(bool_task, &mut translate); + + if !options.opt_options.no_simplify { + vc_is_valid.simplify(); + } + + if options.debug_options.z3_trace { + tracing::info!("Z3 tracing output will be written to `z3.log`."); + } + + let mut prover = Prover::new(&ctx, IncrementalMode::Native); + + if let Some(remaining) = limits_ref.time_left() { + prover.set_timeout(remaining); + } + + // add the definition of all used Lit marker functions + translate.ctx.add_lit_axioms_to_prover(&mut prover); + // add assumptions (from axioms and locals) to the prover + translate + .ctx + .uninterpreteds() + .add_axioms_to_prover(&mut prover); + translate + .local_scope() + .add_assumptions_to_prover(&mut prover); + + // add the requirement for the preexpectation + prover.add_assumption(&vc_is_valid.vc); + + let smtlib = get_smtlib(options, &prover); + if let Some(smtlib) = &smtlib { + write_smtlib(&options.debug_options, name, smtlib, None)?; + } + + let mut sat_result = prover.check_sat(); + let model = prover.get_model(); + + let files = server.get_files_internal().lock().unwrap(); + match &mut sat_result { + SatResult::Sat => { + println!( + "{name}: A non-trivial bound is given for example by the following model:" + ); + let model = model.as_ref().unwrap(); + let mut w = Vec::new(); + let doc = + pretty_nontrivial_models_model(&files, &vc_is_valid.quant_vc, &mut translate, model); + doc.nest(4).render(120, &mut w).unwrap(); + println!(" {}", String::from_utf8(w).unwrap()); + } + SatResult::Unsat => { + println!( + "{name}: The bound introduced by the preexpectations is always trivial (bottom for proc/top for coproc)" + ); + } + SatResult::Unknown => { + println!("{name}: Unknown result!"); + } + } + // Handle reasons to stop the verifier. + match sat_result { + SatResult::Unknown => return Err(CaesarError::Interrupted), _ => {} } // Increment counters. - match result { - ProveResult::Counterexample => num_sat += 1, - ProveResult::Proof | ProveResult::Unknown(_) => num_unsat += 1, + match sat_result { + SatResult::Sat => num_sat += 1, + SatResult::Unsat | SatResult::Unknown => num_unsat += 1, } } diff --git a/src/driver/commands/mod.rs b/src/driver/commands/mod.rs index 61973165..6e4984d3 100644 --- a/src/driver/commands/mod.rs +++ b/src/driver/commands/mod.rs @@ -20,7 +20,7 @@ use clap::{crate_description, Args, CommandFactory, Parser, Subcommand}; use crate::{ ast::FileId, driver::commands::{ - get_pre_models::run_get_model_command, + get_pre_models::run_nontrivial_model_command, model_check::{run_model_checking_command, ModelCheckCommand}, options::{DebugOptions, InputOptions}, refinement::run_verify_entailment_command, @@ -67,7 +67,7 @@ impl CaesarCli { CaesarCommand::Mc(options) => run_model_checking_command(options), CaesarCommand::Lsp(options) => run_lsp_command(options).await, CaesarCommand::ShellCompletions(options) => run_shell_completions_command(options), - CaesarCommand::GetPreModels(options) => run_get_model_command(options).await, + CaesarCommand::GetPreModels(options) => run_nontrivial_model_command(options).await, CaesarCommand::Other(_) => unreachable!(), } } diff --git a/src/driver/commands/refinement.rs b/src/driver/commands/refinement.rs index a715edaf..c1c526a1 100644 --- a/src/driver/commands/refinement.rs +++ b/src/driver/commands/refinement.rs @@ -163,7 +163,6 @@ async fn verify_entailment( server, slice_vars, vc_is_valid, - false, )?; // Handle reasons to stop the verifier. diff --git a/src/driver/commands/verify.rs b/src/driver/commands/verify.rs index 0bbd3a77..74071852 100644 --- a/src/driver/commands/verify.rs +++ b/src/driver/commands/verify.rs @@ -264,7 +264,6 @@ fn verify_files_main( server, slice_vars, vc_is_valid, - false, )?; // Handle reasons to stop the verifier. diff --git a/src/driver/core_verify.rs b/src/driver/core_verify.rs index c78716d8..09b164bc 100644 --- a/src/driver/core_verify.rs +++ b/src/driver/core_verify.rs @@ -21,7 +21,7 @@ use crate::{ }, pretty::{Doc, SimplePretty}, procs::{ - proc_verify::{encode_pre_get_model, encode_proc_verify, to_direction_lower_bounds}, + proc_verify::{encode_preexpectation, encode_proc_verify, to_direction_lower_bounds}, SpecCall, }, resource_limits::LimitsRef, @@ -96,7 +96,7 @@ impl CoreVerifyTask { match decl { DeclKind::ProcDecl(proc_decl) => { let (direction, block) = if is_get_model_task { - encode_pre_get_model(&proc_decl.borrow())? + encode_preexpectation(&proc_decl.borrow())? } else { encode_proc_verify(&proc_decl.borrow())? }; diff --git a/src/driver/smt_proof.rs b/src/driver/smt_proof.rs index 6d242fd5..82b48fc2 100644 --- a/src/driver/smt_proof.rs +++ b/src/driver/smt_proof.rs @@ -35,7 +35,6 @@ use crate::smt::funcs::fuel::{ FuelEncodingOptions, FuelMonoFunctionEncoder, FuelParamFunctionEncoder, }; use crate::smt::funcs::{FunctionEncoder, RecFunFunctionEncoder}; -use crate::smt::pretty_model::pretty_get_models_model; use crate::smt::{DepConfig, SmtCtx}; use crate::tyctx::TyCtx; use crate::{ @@ -142,7 +141,6 @@ pub fn run_smt_prove_task( server: &mut dyn Server, slice_vars: SliceStmts, vc_is_valid: BoolVcProveTask, - is_get_model_task: bool, ) -> Result { let ctx = Context::new(&z3::Config::default()); let function_encoder = mk_function_encoder(tcx, depgraph, options)?; @@ -163,7 +161,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, is_get_model_task) + .handle_vc_check_result(name, &mut result, &mut translate) .map_err(CaesarError::ServerError)?; Ok(result.prove_result) @@ -444,7 +442,7 @@ fn mk_valid_query_prover<'smt, 'ctx>( prover } -fn get_smtlib(options: &VerifyCommand, prover: &Prover) -> Option { +pub fn get_smtlib(options: &VerifyCommand, prover: &Prover) -> Option { if options.debug_options.print_smt || options.debug_options.smt_dir.is_some() { let mut smtlib = prover.get_smtlib(); if !options.debug_options.no_pretty_smtlib { @@ -460,7 +458,7 @@ fn get_smtlib(options: &VerifyCommand, prover: &Prover) -> Option { } /// Write the SMT-LIB dump to a file if requested. -fn write_smtlib( +pub fn write_smtlib( options: &DebugOptions, name: &SourceUnitName, smtlib: &Smtlib, @@ -636,48 +634,4 @@ impl<'ctx> SmtVcProveResult<'ctx> { Ok(()) } -} - -impl<'ctx> SmtVcProveResult<'ctx> { - /// Print the result of the query to stdout. - pub fn print_prove_result_get_model<'smt>( - &mut self, - server: &mut dyn Server, - translate: &mut TranslateExprs<'smt, 'ctx>, - name: &SourceUnitName, - ) { - let files = server.get_files_internal().lock().unwrap(); - match &mut self.prove_result { - ProveResult::Proof => { - println!("{name}: The bound introduced by the preexpectations is always trivial (bottom for proc/top for coproc)"); - } - ProveResult::Counterexample => { - let model = self.model.as_ref().unwrap(); - println!( - "{name}: A non-trivial bound is given for example by the following model:" - ); - let mut w = Vec::new(); - let doc = pretty_get_models_model( - &files, - self.slice_model.as_ref().unwrap(), - &self.quant_vc, - translate, - model, - ); - doc.nest(4).render(120, &mut w).unwrap(); - println!(" {}", String::from_utf8(w).unwrap()); - } - ProveResult::Unknown(reason) => { - println!("{name}: Unknown result! (reason: {reason})"); - if let Some(slice_model) = &self.slice_model { - let doc = pretty_slice(&files, slice_model); - if let Some(doc) = doc { - let mut w = Vec::new(); - doc.nest(4).render(120, &mut w).unwrap(); - println!(" {}", String::from_utf8(w).unwrap()); - } - } - } - } - } -} +} \ No newline at end of file diff --git a/src/procs/proc_verify.rs b/src/procs/proc_verify.rs index b2f79743..e262faa8 100644 --- a/src/procs/proc_verify.rs +++ b/src/procs/proc_verify.rs @@ -1,25 +1,18 @@ use crate::{ ast::{ self, BinOpKind, Block, Direction, ExprData, ExprKind, ProcDecl, Shared, Span, SpanVariant, - Spanned, StmtKind, TyKind, UnOpKind, + Spanned, StmtKind, TyKind, }, driver::core_verify::CoreVerifyTask, slicing::{wrap_with_error_message, wrap_with_success_message}, }; -/// Encode the preexpectations as a formula for which counterexamples are satisfying valuations -/// of the preexpectations. +/// Encode the preexpectations as a formula for which a model is a nontrivial bound /// For proc: /// goal: Find a model such that (pre1 ⊓ pre2 ⊓...) > 0 -/// (pre1 ⊓ pre2 ⊓...) = 0 iff !(pre1 ⊓ pre2 ⊓...) = top -/// (pre1 ⊓ pre2 ⊓...) > 0 iff !(pre1 ⊓ pre2 ⊓...) = 0 -/// find cex for: !(pre1 ⊓ pre2 ⊓...) /// For coproc: /// goal: Find a model such that (pre1 ⊔ pre2 ⊔...) < top -/// (pre1 ⊔ pre2 ⊔...) = top iff ~(pre1 ⊔ pre2 ⊔...) = 0 -/// (pre1 ⊔ pre2 ⊔...) < top iff ~(pre1 ⊔ pre2 ⊔...) = top -/// find cex for: ~(pre1 ⊔ pre2 ⊔...) -pub fn encode_pre_get_model(proc: &ProcDecl) -> Option<(Direction, Block)> { +pub fn encode_preexpectation(proc: &ProcDecl) -> Option<(Direction, Block)> { let direction = proc.direction; let body_ref = proc.body.borrow(); @@ -37,15 +30,7 @@ pub fn encode_pre_get_model(proc: &ProcDecl) -> Option<(Direction, Block)> { combination } - fn get_negation_type(direction: Direction) -> ast::expr::UnOpKind { - let negation_type = match direction { - Direction::Down => UnOpKind::Not, - Direction::Up => UnOpKind::Non, - }; - negation_type - } - - // push the assume statement for each requires + // connect the preexpectations through the correct operator let mut build_expr = proc .requires() .next() @@ -63,14 +48,6 @@ pub fn encode_pre_get_model(proc: &ProcDecl) -> Option<(Direction, Block)> { }); } - build_expr = Shared::new(ExprData { - kind: ExprKind::Unary( - Spanned::with_dummy_span(get_negation_type(direction)), - build_expr, - ), - ty: Some(TyKind::EUReal), - span: Span::dummy_span(), - }); block.node.push(Spanned::new( Span::dummy_span(), StmtKind::Assert(direction, build_expr), diff --git a/src/servers/cli.rs b/src/servers/cli.rs index dab38ee7..b96b8299 100644 --- a/src/servers/cli.rs +++ b/src/servers/cli.rs @@ -112,13 +112,8 @@ impl Server for CliServer { name: &SourceUnitName, result: &mut SmtVcProveResult<'ctx>, translate: &mut TranslateExprs<'smt, 'ctx>, - is_get_model_task: bool, ) -> Result<(), ServerError> { - if is_get_model_task { - result.print_prove_result_get_model(self, translate, name); - } else { - result.print_prove_result(self, translate, name); - } + result.print_prove_result(self, translate, name); Ok(()) } diff --git a/src/servers/lsp.rs b/src/servers/lsp.rs index 283d812d..089ab525 100644 --- a/src/servers/lsp.rs +++ b/src/servers/lsp.rs @@ -427,7 +427,6 @@ impl Server for LspServer { name: &SourceUnitName, result: &mut SmtVcProveResult<'ctx>, translate: &mut TranslateExprs<'smt, 'ctx>, - _is_get_model_task: bool, ) -> Result<(), ServerError> { result.emit_diagnostics(name.span(), self, translate)?; let statuses = &mut self diff --git a/src/servers/mod.rs b/src/servers/mod.rs index 76d41ee4..c6d19dfc 100644 --- a/src/servers/mod.rs +++ b/src/servers/mod.rs @@ -191,7 +191,6 @@ pub trait Server: Send { name: &SourceUnitName, result: &mut SmtVcProveResult<'ctx>, translate: &mut TranslateExprs<'smt, 'ctx>, - is_get_model_task: bool, ) -> Result<(), ServerError>; /// Return an exit code for the process. diff --git a/src/servers/test.rs b/src/servers/test.rs index 9253a632..371a0371 100644 --- a/src/servers/test.rs +++ b/src/servers/test.rs @@ -105,7 +105,6 @@ impl Server for TestServer { name: &SourceUnitName, result: &mut SmtVcProveResult<'ctx>, _translate: &mut TranslateExprs<'smt, 'ctx>, - _is_get_model_task: bool, ) -> Result<(), ServerError> { let statuses = &mut self .file_statuses diff --git a/src/smt/pretty_model.rs b/src/smt/pretty_model.rs index 3d56b129..bea6b1fc 100644 --- a/src/smt/pretty_model.rs +++ b/src/smt/pretty_model.rs @@ -8,8 +8,7 @@ use z3rro::model::{InstrumentedModel, ModelConsistency, SmtEvalError}; use crate::{ ast::{ decl::{DeclKind, DeclKindName}, - BinOpKind, Expr, ExprBuilder, ExprData, ExprKind, Files, Ident, LitKind, Shared, Span, - UnOpKind, VarKind, + ExprBuilder, Files, Ident, Span, VarKind, }, driver::quant_proof::QuantVcProveTask, pretty::Doc, @@ -49,9 +48,8 @@ pub fn pretty_model<'smt, 'ctx>( } /// Pretty-print a model for get models. -pub fn pretty_get_models_model<'smt, 'ctx>( +pub fn pretty_nontrivial_models_model<'smt, 'ctx>( files: &Files, - slice_model: &SliceModel, vc_expr: &QuantVcProveTask, translate: &mut TranslateExprs<'smt, 'ctx>, model: &InstrumentedModel<'ctx>, @@ -61,131 +59,31 @@ pub fn pretty_get_models_model<'smt, 'ctx>( // Print the values of the global variables in the model. pretty_globals(translate, model, files, &mut res); - let slice_lines = pretty_slice(files, slice_model); - // Print the unaccessed definitions. if let Some(unaccessed) = pretty_unaccessed(model) { res.push(unaccessed); } - if let Some(slice_lines) = slice_lines { - res.push(slice_lines); - } - - res.push(pretty_get_models_value( - vc_expr, - translate, - model, - slice_model, - )); + res.push(pretty_get_models_value(vc_expr, translate, model)); Doc::intersperse(res, Doc::line_().append(Doc::line_())).append(Doc::line_()) } -fn deref_cast(e: &Expr) -> &Expr { - match &e.kind { - ExprKind::Cast(inner) => deref_cast(inner), - _ => e, - } -} - -fn is_infinity_or_negated_infinity(expr: &Shared) -> bool { - match &expr.clone().kind { - ExprKind::Lit(lit) if matches!(lit.node, LitKind::Infinity) => true, - ExprKind::Unary(op, inner) if matches!(op.node, UnOpKind::Not | UnOpKind::Non) => { - matches!(&inner.clone().kind, ExprKind::Lit(lit) if matches!(lit.node, LitKind::Infinity)) - } - _ => false, - } -} - -fn strip_outer_negation(expr: &Shared) -> Shared { - match &expr.clone().kind { - ExprKind::Unary(op, inner) if op.node == UnOpKind::Not || op.node == UnOpKind::Non => { - inner.clone() - } - _ => expr.clone(), - } -} - -fn strip_inf_or_sup_with_infinity(expr: &Expr) -> Option> { - match &deref_cast(expr).kind { - ExprKind::Binary(op, left, right) - if op.node == BinOpKind::Inf || op.node == BinOpKind::Sup => - { - let left_expr = left.clone(); - let right_expr = right.clone(); - - let is_left_infinity = is_infinity_or_negated_infinity(&left_expr); - let is_right_infinity = is_infinity_or_negated_infinity(&right_expr); - - match (is_left_infinity, is_right_infinity) { - (true, false) => Some(right_expr), - (false, true) => Some(left_expr), - (true, true) => Some(expr.clone()), // both sides are (negated) ∞ - (false, false) => Some(expr.clone()), // neither side is (negated) ∞ (should not happen) - } - } - _ => Some(expr.clone()), // not an Inf/Sup — return as-is - } -} - pub fn pretty_get_models_value<'smt, 'ctx>( vc_expr: &QuantVcProveTask, translate: &mut TranslateExprs<'smt, 'ctx>, model: &InstrumentedModel<'ctx>, - slice_model: &SliceModel, ) -> Doc { - let original_program_vc = if slice_model.count_sliced_stmts() == 0 { - vc_expr.expr.clone() - } else { - // reconstruct the original program's vc by substituting the slice - // variables by `true`. - let builder = ExprBuilder::new(Span::dummy_span()); - let expr_true = builder.bool_lit(true); - let subst_expr = builder.subst_by( - vc_expr.expr.clone(), - slice_model.iter_variables(), - |_ident| expr_true.clone(), - ); - let mut res = subst_expr; - - // The limit error is not handled here, therefore discard the result - apply_subst(translate.ctx.tcx(), &mut res, &LimitsRef::new(None, None)).unwrap(); - - res - }; - + let original_program_vc = vc_expr.expr.clone(); let mut lines = vec![]; - let stripped = strip_outer_negation( - &strip_inf_or_sup_with_infinity(&original_program_vc.clone()).unwrap(), - ); - let ast = translate.t_symbolic(&stripped); + let ast = translate.t_symbolic(&original_program_vc); let value = ast.eval(model); let res = pretty_eval_result(value); lines.push( Doc::text("the pre-quantity evaluated to:").append(Doc::hardline().append(res).nest(4)), ); - let num_sliced_stmts = slice_model.count_sliced_stmts(); - if num_sliced_stmts > 0 { - let ast = translate.t_symbolic(&vc_expr.expr); - let value = ast.eval(model); - let slice_pre = pretty_eval_result(value) - .append(Doc::line_()) - .append(Doc::text(format!( - "(slicing removed {}/{} assertions)", - num_sliced_stmts, - slice_model.len() - ))); - lines.push(Doc::nil()); - lines.push( - Doc::text("in the sliced program, the pre-quantity evaluated to:") - .append(Doc::hardline().append(slice_pre).nest(4)), - ); - } - Doc::intersperse(lines, Doc::line()) } From 5b09fdb401237258fc8ff38fefcb1e836eaf85b6 Mon Sep 17 00:00:00 2001 From: madita Date: Thu, 30 Oct 2025 09:11:03 +0100 Subject: [PATCH 04/10] get-models: Change name of command to "get-pre-models" --- src/driver/commands/mod.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/src/driver/commands/mod.rs b/src/driver/commands/mod.rs index 6e4984d3..33af01fa 100644 --- a/src/driver/commands/mod.rs +++ b/src/driver/commands/mod.rs @@ -102,7 +102,6 @@ pub enum CaesarCommand { /// Generate shell completions for the Caesar binary. ShellCompletions(ShellCompletionsCommand), /// Get non-trivial models for preexpectation. - #[clap(visible_alias = "get-models")] GetPreModels(VerifyCommand), /// This is to support the default `verify` command. #[command(external_subcommand)] From 11586a5f24e90ebd0c4a5123d5d158306bf90455 Mon Sep 17 00:00:00 2001 From: madita Date: Thu, 30 Oct 2025 10:32:00 +0100 Subject: [PATCH 05/10] get-models: Extract "run_smt_check_sat" function --- src/driver/commands/get_pre_models.rs | 107 +++++--------------------- src/driver/smt_proof.rs | 86 ++++++++++++++++++++- src/servers/mod.rs | 2 +- src/smt/pretty_model.rs | 2 +- 4 files changed, 102 insertions(+), 95 deletions(-) diff --git a/src/driver/commands/get_pre_models.rs b/src/driver/commands/get_pre_models.rs index 7dffb4e9..dcd2eae9 100644 --- a/src/driver/commands/get_pre_models.rs +++ b/src/driver/commands/get_pre_models.rs @@ -1,8 +1,5 @@ use std::{ops::DerefMut, process::ExitCode, sync::Arc}; -use z3::{Context, SatResult}; -use z3rro::prover::{IncrementalMode, Prover}; - use crate::{ ast::{BinOpKind, Direction, ExprBuilder, FileId, Span, TyKind}, driver::{ @@ -12,16 +9,12 @@ use crate::{ front::parse_and_tycheck, item::Item, quant_proof::BoolVcProveTask, - smt_proof::{ - get_smtlib, mk_function_encoder, set_global_z3_params, write_smtlib, SmtVcProveTask, - }, + smt_proof::{run_smt_check_sat, set_global_z3_params}, }, resource_limits::{await_with_resource_limits, LimitsRef}, servers::{Server, SharedServer}, - smt::{ - pretty_model::pretty_nontrivial_models_model, translate_exprs::TranslateExprs, DepConfig, SmtCtx, - }, }; +use z3::SatResult; pub async fn run_nontrivial_model_command(options: VerifyCommand) -> ExitCode { let (user_files, server) = match mk_cli_server(&options.input_options) { @@ -142,20 +135,15 @@ fn nontrivial_model_files_main( // Lowering the quantitative task to a Boolean one. let mut quant_task = vc_expr; - // 1. Unfolding (applies substitutions) + // Unfolding (applies substitutions) quant_task.unfold(options, &limits_ref, &tcx)?; - // TODO: How to deal with quantifier? - // 2. Quantifier elimination - // if !options.opt_options.no_qelim { - // quant_task.qelim(&mut tcx, &limits_ref)?; - // } + // TODO: How to deal with inf/sup quantifier? + // Should there be a warning if they are used? - // In-between, gather some stats about the vc expression quant_task.trace_expr_stats(); - - // 3. Now turn this quantitative formula into a Boolean one + // Turn quantitative formula into a Boolean one let builder = ExprBuilder::new(Span::dummy_span()); let top = builder.top_lit(quant_task.expr.ty.as_ref().unwrap()); let bot = builder.bot_lit(quant_task.expr.ty.as_ref().unwrap()); @@ -179,92 +167,33 @@ fn nontrivial_model_files_main( vc: res, }; - - // 4. Optimizations - // 4.1. Remove parentheses if needed + // Optimizations if !options.opt_options.no_boolify || options.opt_options.opt_rel { bool_task.remove_parens(); } - // 4.2 Boolify (enabled by default) if !options.opt_options.no_boolify { bool_task.opt_boolify(); } - // 4.3. Relational optimization (disabled by default) if options.opt_options.opt_rel { bool_task.opt_relational(); } - // print theorem to prove if requested if options.debug_options.print_theorem { bool_task.print_theorem(name); } + // Running the SMT check sat task: translating to Z3, running the solver. + // This also handles printing the result + let sat_result = run_smt_check_sat( + &options, + &limits_ref, + &tcx, + &depgraph, + &name, + bool_task, + server, + )?; - let ctx = Context::new(&z3::Config::default()); - let function_encoder = mk_function_encoder(&tcx, &depgraph, options)?; - let dep_config = DepConfig::Set(bool_task.get_dependencies()); - let smt_ctx = SmtCtx::new(&ctx, &tcx, function_encoder, dep_config); - let mut translate = TranslateExprs::new(&smt_ctx); - let mut vc_is_valid = SmtVcProveTask::translate(bool_task, &mut translate); - - if !options.opt_options.no_simplify { - vc_is_valid.simplify(); - } - - if options.debug_options.z3_trace { - tracing::info!("Z3 tracing output will be written to `z3.log`."); - } - - let mut prover = Prover::new(&ctx, IncrementalMode::Native); - - if let Some(remaining) = limits_ref.time_left() { - prover.set_timeout(remaining); - } - - // add the definition of all used Lit marker functions - translate.ctx.add_lit_axioms_to_prover(&mut prover); - // add assumptions (from axioms and locals) to the prover - translate - .ctx - .uninterpreteds() - .add_axioms_to_prover(&mut prover); - translate - .local_scope() - .add_assumptions_to_prover(&mut prover); - - // add the requirement for the preexpectation - prover.add_assumption(&vc_is_valid.vc); - - let smtlib = get_smtlib(options, &prover); - if let Some(smtlib) = &smtlib { - write_smtlib(&options.debug_options, name, smtlib, None)?; - } - - let mut sat_result = prover.check_sat(); - let model = prover.get_model(); - - let files = server.get_files_internal().lock().unwrap(); - match &mut sat_result { - SatResult::Sat => { - println!( - "{name}: A non-trivial bound is given for example by the following model:" - ); - let model = model.as_ref().unwrap(); - let mut w = Vec::new(); - let doc = - pretty_nontrivial_models_model(&files, &vc_is_valid.quant_vc, &mut translate, model); - doc.nest(4).render(120, &mut w).unwrap(); - println!(" {}", String::from_utf8(w).unwrap()); - } - SatResult::Unsat => { - println!( - "{name}: The bound introduced by the preexpectations is always trivial (bottom for proc/top for coproc)" - ); - } - SatResult::Unknown => { - println!("{name}: Unknown result!"); - } - } // Handle reasons to stop the verifier. match sat_result { SatResult::Unknown => return Err(CaesarError::Interrupted), diff --git a/src/driver/smt_proof.rs b/src/driver/smt_proof.rs index 82b48fc2..e2b215e8 100644 --- a/src/driver/smt_proof.rs +++ b/src/driver/smt_proof.rs @@ -6,6 +6,7 @@ use std::io::Write; use ariadne::ReportKind; use itertools::Itertools; use tracing::info_span; +use z3::SatResult; use z3::{ ast::{Ast, Bool}, Context, Goal, @@ -48,7 +49,8 @@ use crate::{ }, smt::{ pretty_model::{ - pretty_model, pretty_slice, pretty_unaccessed, pretty_var_value, pretty_vc_value, + pretty_model, pretty_nontrivial_model, pretty_slice, pretty_unaccessed, + pretty_var_value, pretty_vc_value, }, translate_exprs::TranslateExprs, }, @@ -167,6 +169,81 @@ pub fn run_smt_prove_task( Ok(result.prove_result) } +pub fn run_smt_check_sat<'tcx>( + options: &VerifyCommand, + limits_ref: &LimitsRef, + tcx: &'tcx TyCtx, + depgraph: &DepGraph, + name: &SourceUnitName, + bool_task: BoolVcProveTask, + server: &mut dyn Server, +) -> Result { + let ctx = Context::new(&z3::Config::default()); + let function_encoder = mk_function_encoder(tcx, depgraph, options)?; + let dep_config = DepConfig::Set(bool_task.get_dependencies()); + let smt_ctx = SmtCtx::new(&ctx, tcx, function_encoder, dep_config); + let mut translate = TranslateExprs::new(&smt_ctx); + let mut vc_is_valid = SmtVcProveTask::translate(bool_task, &mut translate); + + if !options.opt_options.no_simplify { + vc_is_valid.simplify(); + } + + if options.debug_options.z3_trace { + tracing::info!("Z3 tracing output will be written to `z3.log`."); + } + + let mut prover = Prover::new(&ctx, IncrementalMode::Native); + + if let Some(remaining) = limits_ref.time_left() { + prover.set_timeout(remaining); + } + + // Add axioms and assumptions + translate.ctx.add_lit_axioms_to_prover(&mut prover); + translate + .ctx + .uninterpreteds() + .add_axioms_to_prover(&mut prover); + translate + .local_scope() + .add_assumptions_to_prover(&mut prover); + + // Add the verification condition + prover.add_assumption(&vc_is_valid.vc); + + // Optionally dump SMT-LIB representation + if let Some(smtlib) = get_smtlib(options, &prover) { + write_smtlib(&options.debug_options, name, &smtlib, None)?; + } + + // Run solver & retrieve model if available + let sat_result = prover.check_sat(); + let model = prover.get_model(); + + let files = server.get_files_internal().lock().unwrap(); + match &sat_result { + SatResult::Sat => { + println!("{name}: A non-trivial bound is given for example by the following model:"); + let model = model.as_ref().unwrap(); + let mut w = Vec::new(); + let doc = pretty_nontrivial_model(&files, &vc_is_valid.quant_vc, &mut translate, model); + doc.nest(4).render(120, &mut w).unwrap(); + println!(" {}", String::from_utf8(w).unwrap()); + } + SatResult::Unsat => { + println!( + "{name}: The bound introduced by the preexpectations is always trivial (bottom for proc/top for coproc)" + ); + } + SatResult::Unknown => { + println!("{name}: Unknown result!"); + } + } + + Ok(sat_result) +} + /// Create the function encoder based on the given command's options. pub fn mk_function_encoder<'ctx>( tcx: &TyCtx, @@ -282,6 +359,7 @@ impl<'ctx> SmtVcProveTask<'ctx> { vc: bool_vc, } } + /// Simplify the SMT formula using Z3's simplifier. pub fn simplify(&mut self) { let span = info_span!("simplify query"); @@ -442,7 +520,7 @@ fn mk_valid_query_prover<'smt, 'ctx>( prover } -pub fn get_smtlib(options: &VerifyCommand, prover: &Prover) -> Option { +fn get_smtlib(options: &VerifyCommand, prover: &Prover) -> Option { if options.debug_options.print_smt || options.debug_options.smt_dir.is_some() { let mut smtlib = prover.get_smtlib(); if !options.debug_options.no_pretty_smtlib { @@ -458,7 +536,7 @@ pub fn get_smtlib(options: &VerifyCommand, prover: &Prover) -> Option { } /// Write the SMT-LIB dump to a file if requested. -pub fn write_smtlib( +fn write_smtlib( options: &DebugOptions, name: &SourceUnitName, smtlib: &Smtlib, @@ -634,4 +712,4 @@ impl<'ctx> SmtVcProveResult<'ctx> { Ok(()) } -} \ No newline at end of file +} diff --git a/src/servers/mod.rs b/src/servers/mod.rs index c6d19dfc..4316516a 100644 --- a/src/servers/mod.rs +++ b/src/servers/mod.rs @@ -192,7 +192,7 @@ pub trait Server: Send { result: &mut SmtVcProveResult<'ctx>, translate: &mut TranslateExprs<'smt, 'ctx>, ) -> Result<(), ServerError>; - + /// Return an exit code for the process. /// /// Default implementation returns `ExitCode::SUCCESS`. diff --git a/src/smt/pretty_model.rs b/src/smt/pretty_model.rs index bea6b1fc..e8fd9a4a 100644 --- a/src/smt/pretty_model.rs +++ b/src/smt/pretty_model.rs @@ -48,7 +48,7 @@ pub fn pretty_model<'smt, 'ctx>( } /// Pretty-print a model for get models. -pub fn pretty_nontrivial_models_model<'smt, 'ctx>( +pub fn pretty_nontrivial_model<'smt, 'ctx>( files: &Files, vc_expr: &QuantVcProveTask, translate: &mut TranslateExprs<'smt, 'ctx>, From de104f61139c9ec0f3c675a0cd8af5eab02744d4 Mon Sep 17 00:00:00 2001 From: madita Date: Mon, 3 Nov 2025 10:16:53 +0100 Subject: [PATCH 06/10] get-model: Rename CoreVerifyTask to CoreHeyVLTask & refactor This struct now has two constructors so that it can be used for both verify and pre-model tasks. --- src/driver/commands/get_pre_models.rs | 8 +- src/driver/commands/refinement.rs | 10 +-- src/driver/commands/verify.rs | 8 +- src/driver/{core_verify.rs => core_heyvl.rs} | 82 +++++++++++++------- src/driver/mod.rs | 2 +- src/procs/proc_verify.rs | 4 +- 6 files changed, 69 insertions(+), 45 deletions(-) rename src/driver/{core_verify.rs => core_heyvl.rs} (76%) diff --git a/src/driver/commands/get_pre_models.rs b/src/driver/commands/get_pre_models.rs index dcd2eae9..70ab68f1 100644 --- a/src/driver/commands/get_pre_models.rs +++ b/src/driver/commands/get_pre_models.rs @@ -4,7 +4,7 @@ use crate::{ ast::{BinOpKind, Direction, ExprBuilder, FileId, Span, TyKind}, driver::{ commands::{mk_cli_server, print_timings, verify::VerifyCommand}, - core_verify::{lower_core_verify_task, CoreVerifyTask}, + core_heyvl::{lower_core_heyvl_task, CoreHeyVLTask}, error::{finalize_caesar_result, CaesarError}, front::parse_and_tycheck, item::Item, @@ -94,11 +94,11 @@ fn nontrivial_model_files_main( let mut depgraph = module.generate_depgraph(&options.opt_options.function_encoding)?; // translate program to relevant preexpectation conditions - let mut verify_units: Vec> = module + let mut verify_units: Vec> = module .items .into_iter() .flat_map(|item| { - item.flat_map(|unit| CoreVerifyTask::from_source_unit(unit, &mut depgraph, true)) + item.flat_map(|unit| CoreHeyVLTask::from_proc_pre_model(unit, &mut depgraph)) }) .collect(); @@ -123,7 +123,7 @@ fn nontrivial_model_files_main( let mut new_options = VerifyCommand::default(); new_options.slice_options.no_slice_error = true; - let (vc_expr, _slice_vars) = lower_core_verify_task( + let (vc_expr, _slice_vars) = lower_core_heyvl_task( &mut tcx, name, &new_options, diff --git a/src/driver/commands/refinement.rs b/src/driver/commands/refinement.rs index c1c526a1..48c9c913 100644 --- a/src/driver/commands/refinement.rs +++ b/src/driver/commands/refinement.rs @@ -17,7 +17,7 @@ use crate::{ }, driver::{ commands::{mk_cli_server, print_timings, verify::VerifyCommand}, - core_verify::{lower_core_verify_task, CoreVerifyTask}, + core_heyvl::{lower_core_heyvl_task, CoreHeyVLTask}, error::{finalize_caesar_result, CaesarError}, front::{parse_and_tycheck, SourceUnit}, item::Item, @@ -121,13 +121,13 @@ async fn verify_entailment( }; let mut first_verify_unit = first - .flat_map(|u| CoreVerifyTask::from_source_unit(u, &mut depgraph, false)) + .flat_map(|u| CoreHeyVLTask::from_proc_verify(u, &mut depgraph)) .unwrap(); let mut second_verify_unit = second - .flat_map(|u| CoreVerifyTask::from_source_unit(u, &mut depgraph, false)) + .flat_map(|u| CoreHeyVLTask::from_proc_verify(u, &mut depgraph)) .unwrap(); - let (first_vc, first_slice_stmts) = lower_core_verify_task( + let (first_vc, first_slice_stmts) = lower_core_heyvl_task( &mut tcx, &first_name, options, @@ -135,7 +135,7 @@ async fn verify_entailment( server, &mut first_verify_unit.enter_mut(), )?; - let (second_vc, second_slice_stmts) = lower_core_verify_task( + let (second_vc, second_slice_stmts) = lower_core_heyvl_task( &mut tcx, &first_name, options, diff --git a/src/driver/commands/verify.rs b/src/driver/commands/verify.rs index 74071852..c8dfeef9 100644 --- a/src/driver/commands/verify.rs +++ b/src/driver/commands/verify.rs @@ -15,7 +15,7 @@ use crate::{ }, print_timings, }, - core_verify::{lower_core_verify_task, CoreVerifyTask}, + core_heyvl::{lower_core_heyvl_task, CoreHeyVLTask}, error::{finalize_caesar_result, CaesarError}, front::parse_and_tycheck, item::Item, @@ -211,11 +211,11 @@ fn verify_files_main( // the SMT translation later let mut depgraph = module.generate_depgraph(&options.opt_options.function_encoding)?; - let mut verify_units: Vec> = module + let mut verify_units: Vec> = module .items .into_iter() .flat_map(|item| { - item.flat_map(|unit| CoreVerifyTask::from_source_unit(unit, &mut depgraph, false)) + item.flat_map(|unit| CoreHeyVLTask::from_proc_verify(unit, &mut depgraph)) }) .collect(); @@ -240,7 +240,7 @@ fn verify_files_main( // Lowering the core verify task to a quantitative prove task: applying // spec call desugaring, preparing slicing, and verification condition // generation. - let (vc_expr, slice_vars) = lower_core_verify_task( + let (vc_expr, slice_vars) = lower_core_heyvl_task( &mut tcx, name, options, diff --git a/src/driver/core_verify.rs b/src/driver/core_heyvl.rs similarity index 76% rename from src/driver/core_verify.rs rename to src/driver/core_heyvl.rs index 09b164bc..78bad721 100644 --- a/src/driver/core_verify.rs +++ b/src/driver/core_heyvl.rs @@ -39,13 +39,13 @@ use tracing::instrument; /// Lower a core verification task into a quantitative vc prove task: apply /// desugaring for spec calls, preparing slicing, and verification condition /// generation. -pub fn lower_core_verify_task( +pub fn lower_core_heyvl_task( tcx: &mut TyCtx, name: &SourceUnitName, options: &VerifyCommand, limits_ref: &LimitsRef, server: &mut dyn Server, - task: &mut CoreVerifyTask, + task: &mut CoreHeyVLTask, ) -> Result<(QuantVcProveTask, SliceStmts), CaesarError> { // 1. Desugaring task.desugar_spec_calls(tcx, name.to_string())?; @@ -66,42 +66,53 @@ pub fn lower_core_verify_task( /// A block of HeyVL statements to be verified with a certain [`Direction`]. #[derive(Debug, Clone)] -pub struct CoreVerifyTask { +pub struct CoreHeyVLTask { pub deps: Dependencies, pub direction: Direction, pub block: Block, } -impl CoreVerifyTask { - /// Convert this source unit into a [`CoreVerifyTask`]. Some declarations, +impl CoreHeyVLTask { + /// Convert proc_verify into a [`CoreHeyVLTask`]. Some declarations, /// such as domains or functions, do not generate any verify units. In these /// cases, `None` is returned. - pub fn from_source_unit( - mut source_unit: SourceUnit, - depgraph: &mut DepGraph, - is_get_model_task: bool, - ) -> Option { - let deps = match &mut source_unit { - SourceUnit::Decl(decl) => depgraph.get_reachable([decl.name()]), - SourceUnit::Raw(block) => { - assert!(depgraph.current_deps.is_empty()); - depgraph.visit_block(block).unwrap(); - let current_deps = std::mem::take(&mut depgraph.current_deps); - depgraph.get_reachable(current_deps) - } - }; + pub fn from_proc_verify(mut proc_verify: SourceUnit, depgraph: &mut DepGraph) -> Option { + let deps = Self::compute_deps(&mut proc_verify, depgraph); - match source_unit { + match proc_verify { SourceUnit::Decl(decl) => { match decl { DeclKind::ProcDecl(proc_decl) => { - let (direction, block) = if is_get_model_task { - encode_preexpectation(&proc_decl.borrow())? - } else { - encode_proc_verify(&proc_decl.borrow())? - }; + let (direction, block) = encode_proc_verify(&proc_decl.borrow())?; + Some(CoreHeyVLTask { + deps, + direction, + block, + }) + } + DeclKind::DomainDecl(_domain_decl) => None, // TODO: check that the axioms are not contradictions + DeclKind::FuncDecl(_func_decl) => None, + _ => unreachable!(), // axioms and variable declarations are not allowed on the top level + } + } + SourceUnit::Raw(block) => Some(CoreHeyVLTask { + deps, + direction: Direction::Down, + block, + }), + } + } - Some(CoreVerifyTask { + /// Same as [`from_proc_verify`] but translating from proc_pre_model. + /// For this the preexpectations need to be translated + pub fn from_proc_pre_model(mut proc_pre_model: SourceUnit, depgraph: &mut DepGraph) -> Option { + let deps = Self::compute_deps(&mut proc_pre_model, depgraph); + match proc_pre_model { + SourceUnit::Decl(decl) => { + match decl { + DeclKind::ProcDecl(proc_decl) => { + let (direction, block) = encode_preexpectation(&proc_decl.borrow())?; + Some(CoreHeyVLTask { deps, direction, block, @@ -112,7 +123,7 @@ impl CoreVerifyTask { _ => unreachable!(), // axioms and variable declarations are not allowed on the top level } } - SourceUnit::Raw(block) => Some(CoreVerifyTask { + SourceUnit::Raw(block) => Some(CoreHeyVLTask { deps, direction: Direction::Down, block, @@ -120,6 +131,19 @@ impl CoreVerifyTask { } } + /// Compute the dependency closure for a given source unit. + fn compute_deps(source_unit: &mut SourceUnit, depgraph: &mut DepGraph) -> Dependencies { + match source_unit { + SourceUnit::Decl(decl) => depgraph.get_reachable([decl.name()]), + SourceUnit::Raw(block) => { + assert!(depgraph.current_deps.is_empty()); + depgraph.visit_block(block).unwrap(); + let current_deps = std::mem::take(&mut depgraph.current_deps); + depgraph.get_reachable(current_deps) + } + } + } + /// Desugar assignments with procedure calls. #[instrument(skip_all)] pub fn desugar_spec_calls(&mut self, tcx: &mut TyCtx, name: String) -> Result<(), CaesarError> { @@ -205,7 +229,7 @@ fn top_lit_in_lattice(dir: Direction, ty: &TyKind) -> Expr { } } -impl SimplePretty for CoreVerifyTask { +impl SimplePretty for CoreHeyVLTask { fn pretty(&self) -> Doc { let lower_bounds = to_direction_lower_bounds(self.clone()); assert_eq!(lower_bounds.direction, Direction::Down); @@ -213,7 +237,7 @@ impl SimplePretty for CoreVerifyTask { } } -impl fmt::Display for CoreVerifyTask { +impl fmt::Display for CoreHeyVLTask { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { self.pretty().render_fmt(80, f) } diff --git a/src/driver/mod.rs b/src/driver/mod.rs index 10b862c3..43580107 100644 --- a/src/driver/mod.rs +++ b/src/driver/mod.rs @@ -1,7 +1,7 @@ //! This module glues all components of Caesar together. pub mod commands; -pub mod core_verify; +pub mod core_heyvl; pub mod error; pub mod front; pub mod item; diff --git a/src/procs/proc_verify.rs b/src/procs/proc_verify.rs index e262faa8..005b235e 100644 --- a/src/procs/proc_verify.rs +++ b/src/procs/proc_verify.rs @@ -3,7 +3,7 @@ use crate::{ self, BinOpKind, Block, Direction, ExprData, ExprKind, ProcDecl, Shared, Span, SpanVariant, Spanned, StmtKind, TyKind, }, - driver::core_verify::CoreVerifyTask, + driver::core_heyvl::CoreHeyVLTask, slicing::{wrap_with_error_message, wrap_with_success_message}, }; @@ -121,7 +121,7 @@ pub fn encode_proc_verify(proc: &ProcDecl) -> Option<(Direction, Block)> { /// This is currently not used in the code anymore as we want to track the /// direction explicitly to have better error messages, but exists for the sake /// of completeness. -pub fn to_direction_lower_bounds(mut verify_unit: CoreVerifyTask) -> CoreVerifyTask { +pub fn to_direction_lower_bounds(mut verify_unit: CoreHeyVLTask) -> CoreHeyVLTask { if verify_unit.direction == Direction::Up { verify_unit.direction = Direction::Down; verify_unit.block.node.insert( From c8ad8f6c2a3771f0c28fb976f51ebf4f397887ac Mon Sep 17 00:00:00 2001 From: madita Date: Mon, 3 Nov 2025 10:47:13 +0100 Subject: [PATCH 07/10] get-models: Improve comments --- src/driver/commands/get_pre_models.rs | 3 --- src/driver/commands/mod.rs | 2 +- src/driver/smt_proof.rs | 4 ++++ src/procs/proc_verify.rs | 3 ++- 4 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/driver/commands/get_pre_models.rs b/src/driver/commands/get_pre_models.rs index 70ab68f1..135d950d 100644 --- a/src/driver/commands/get_pre_models.rs +++ b/src/driver/commands/get_pre_models.rs @@ -138,9 +138,6 @@ fn nontrivial_model_files_main( // Unfolding (applies substitutions) quant_task.unfold(options, &limits_ref, &tcx)?; - // TODO: How to deal with inf/sup quantifier? - // Should there be a warning if they are used? - quant_task.trace_expr_stats(); // Turn quantitative formula into a Boolean one diff --git a/src/driver/commands/mod.rs b/src/driver/commands/mod.rs index 33af01fa..730ded53 100644 --- a/src/driver/commands/mod.rs +++ b/src/driver/commands/mod.rs @@ -101,7 +101,7 @@ pub enum CaesarCommand { Lsp(VerifyCommand), /// Generate shell completions for the Caesar binary. ShellCompletions(ShellCompletionsCommand), - /// Get non-trivial models for preexpectation. + /// Compute a non-trivial model for the preconditions of each (co)proc. GetPreModels(VerifyCommand), /// This is to support the default `verify` command. #[command(external_subcommand)] diff --git a/src/driver/smt_proof.rs b/src/driver/smt_proof.rs index e2b215e8..07d9d61d 100644 --- a/src/driver/smt_proof.rs +++ b/src/driver/smt_proof.rs @@ -169,6 +169,10 @@ pub fn run_smt_prove_task( Ok(result.prove_result) } +/// Run the SMT satisfiability check: translate the verification condition to Z3, +/// add axioms and assumptions, check if its sat and find a model, +/// print the result and model and return the result. + pub fn run_smt_check_sat<'tcx>( options: &VerifyCommand, limits_ref: &LimitsRef, diff --git a/src/procs/proc_verify.rs b/src/procs/proc_verify.rs index 005b235e..3d5c8eb1 100644 --- a/src/procs/proc_verify.rs +++ b/src/procs/proc_verify.rs @@ -7,7 +7,8 @@ use crate::{ slicing::{wrap_with_error_message, wrap_with_success_message}, }; -/// Encode the preexpectations as a formula for which a model is a nontrivial bound +/// Encode the preexpectations as a formula for which a model is a nontrivial bound. +/// /// For proc: /// goal: Find a model such that (pre1 ⊓ pre2 ⊓...) > 0 /// For coproc: From 891a4a5494acf7418af3467a8af91f7523d724e2 Mon Sep 17 00:00:00 2001 From: madita Date: Mon, 3 Nov 2025 10:49:04 +0100 Subject: [PATCH 08/10] get-models: Import BinOpKind normally --- src/procs/proc_verify.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/procs/proc_verify.rs b/src/procs/proc_verify.rs index 3d5c8eb1..29ad1138 100644 --- a/src/procs/proc_verify.rs +++ b/src/procs/proc_verify.rs @@ -1,6 +1,6 @@ use crate::{ ast::{ - self, BinOpKind, Block, Direction, ExprData, ExprKind, ProcDecl, Shared, Span, SpanVariant, + BinOpKind, Block, Direction, ExprData, ExprKind, ProcDecl, Shared, Span, SpanVariant, Spanned, StmtKind, TyKind, }, driver::core_heyvl::CoreHeyVLTask, @@ -8,7 +8,7 @@ use crate::{ }; /// Encode the preexpectations as a formula for which a model is a nontrivial bound. -/// +/// /// For proc: /// goal: Find a model such that (pre1 ⊓ pre2 ⊓...) > 0 /// For coproc: @@ -23,7 +23,7 @@ pub fn encode_preexpectation(proc: &ProcDecl) -> Option<(Direction, Block)> { }; let mut block = Spanned::new(body.span, vec![]); - fn get_combination(direction: Direction) -> ast::expr::BinOpKind { + fn get_combination(direction: Direction) -> BinOpKind { let combination = match direction { Direction::Down => BinOpKind::Inf, Direction::Up => BinOpKind::Sup, From db7f15af61d13538d7d7338b941eee62c4484766 Mon Sep 17 00:00:00 2001 From: madita Date: Mon, 3 Nov 2025 11:11:49 +0100 Subject: [PATCH 09/10] get-models: Use reduce in encode-preexpectation --- src/procs/proc_verify.rs | 31 +++++++++++++++---------------- 1 file changed, 15 insertions(+), 16 deletions(-) diff --git a/src/procs/proc_verify.rs b/src/procs/proc_verify.rs index 29ad1138..adcc9a27 100644 --- a/src/procs/proc_verify.rs +++ b/src/procs/proc_verify.rs @@ -31,23 +31,22 @@ pub fn encode_preexpectation(proc: &ProcDecl) -> Option<(Direction, Block)> { combination } - // connect the preexpectations through the correct operator - let mut build_expr = proc + // Combine the preexpectations using the correct operator + let build_expr = proc .requires() - .next() - .expect("No preconditions to check") - .clone(); - for expr in proc.requires().skip(1) { - build_expr = Shared::new(ExprData { - kind: ExprKind::Binary( - Spanned::with_dummy_span(get_combination(direction)), - build_expr, - expr.clone(), - ), - ty: Some(TyKind::EUReal), - span: Span::dummy_span(), - }); - } + .cloned() + .reduce(|lhs, rhs| { + Shared::new(ExprData { + kind: ExprKind::Binary( + Spanned::with_dummy_span(get_combination(direction)).clone(), + lhs, + rhs, + ), + ty: Some(TyKind::EUReal), + span: Span::dummy_span(), + }) + }) + .expect("No preconditions to check"); block.node.push(Spanned::new( Span::dummy_span(), From e2bdae07a6dc44796f9324cda1d0e89bee2b315e Mon Sep 17 00:00:00 2001 From: madita Date: Mon, 3 Nov 2025 11:14:35 +0100 Subject: [PATCH 10/10] get-models: Move def. of top/bot to relevant branches --- src/driver/commands/get_pre_models.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/driver/commands/get_pre_models.rs b/src/driver/commands/get_pre_models.rs index 135d950d..3a663875 100644 --- a/src/driver/commands/get_pre_models.rs +++ b/src/driver/commands/get_pre_models.rs @@ -142,18 +142,18 @@ fn nontrivial_model_files_main( // Turn quantitative formula into a Boolean one let builder = ExprBuilder::new(Span::dummy_span()); - let top = builder.top_lit(quant_task.expr.ty.as_ref().unwrap()); - let bot = builder.bot_lit(quant_task.expr.ty.as_ref().unwrap()); let expr = quant_task.expr.clone(); // Construct the condition based on quantifier direction let res = match quant_task.direction { Direction::Up => { // For coprocs, check if expr < top + let top = builder.top_lit(quant_task.expr.ty.as_ref().unwrap()); builder.binary(BinOpKind::Lt, Some(TyKind::Bool), expr, top) } Direction::Down => { // For procs, check if expr > bot + let bot = builder.bot_lit(quant_task.expr.ty.as_ref().unwrap()); builder.binary(BinOpKind::Gt, Some(TyKind::Bool), expr, bot) } };