From 96241d3e583dba9f7e5370101f6c77ab261bf4e9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Philipp=20Schro=CC=88er?= Date: Sun, 22 Dec 2024 00:14:10 +0100 Subject: [PATCH] smt: write smt-lib files also before smt call, add --no-verify option --- src/driver.rs | 94 +++++++++++++++++++++++++++++++++------------------ src/main.rs | 15 ++++---- 2 files changed, 70 insertions(+), 39 deletions(-) diff --git a/src/driver.rs b/src/driver.rs index eedc5377..a8003cbd 100644 --- a/src/driver.rs +++ b/src/driver.rs @@ -53,7 +53,7 @@ use crate::{ vcgen::Vcgen, }, version::write_detailed_version_info, - Options, SliceOptions, SliceVerifyMethod, VerifyError, + DebugOptions, Options, SliceOptions, SliceVerifyMethod, VerifyError, }; use ariadne::ReportKind; @@ -65,7 +65,7 @@ use z3::{ use z3rro::{ prover::{ProveResult, Prover}, smtlib::Smtlib, - util::PrefixWriter, + util::{PrefixWriter, ReasonUnknown}, }; use tracing::{info_span, instrument, trace}; @@ -664,6 +664,7 @@ impl<'ctx> SmtVcUnit<'ctx> { self, options: &Options, limits_ref: &LimitsRef, + name: &SourceUnitName, ctx: &'ctx Context, translate: &mut TranslateExprs<'smt, 'ctx>, slice_vars: &SliceStmts, @@ -672,7 +673,21 @@ impl<'ctx> SmtVcUnit<'ctx> { let _entered = span.enter(); let prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc); + let smtlib = get_smtlib(options, &prover); + if let Some(smtlib) = &smtlib { + write_smtlib(&options.debug_options, name, &smtlib, None)?; + } + + if options.debug_options.no_verify { + return Ok(SmtVcCheckResult { + prove_result: ProveResult::Unknown(ReasonUnknown::Other( + "verification skipped".to_owned(), + )), + quant_vc: self.quant_vc, + slice_model: None, + }); + } let mut slice_solver = SliceSolver::new(slice_vars.clone(), translate, prover); let failing_slice_options = SliceSolveOptions { @@ -715,11 +730,20 @@ impl<'ctx> SmtVcUnit<'ctx> { } } + if let Some(smtlib) = &smtlib { + // only print to the directory again + let options = DebugOptions { + print_smt: false, + smt_dir: options.debug_options.smt_dir.clone(), + ..options.debug_options + }; + write_smtlib(&options, name, &smtlib, Some(&result))?; + } + Ok(SmtVcCheckResult { prove_result: result, quant_vc: self.quant_vc, slice_model, - smtlib, }) } } @@ -773,12 +797,45 @@ fn get_smtlib(options: &Options, prover: &Prover) -> Option { } } +/// Write the SMT-LIB dump to a file if requested. +fn write_smtlib<'ctx>( + options: &DebugOptions, + name: &SourceUnitName, + smtlib: &Smtlib, + prove_result: Option<&ProveResult<'ctx>>, +) -> Result<(), VerifyError> { + if options.print_smt || options.smt_dir.is_some() { + let mut smtlib = smtlib.clone(); + smtlib.add_check_sat(); + if let Some(prove_result) = prove_result { + smtlib.add_details_query(&prove_result); + } + let smtlib = smtlib.into_string(); + if options.print_smt { + println!("\n; --- Solver SMT-LIB ---\n{}\n", smtlib); + } + if let Some(smt_dir) = &options.smt_dir { + let file_path = smt_dir.join(name.to_file_name("smt2")); + create_dir_all(file_path.parent().unwrap())?; + let mut file = File::create(&file_path)?; + let mut comment_writer = PrefixWriter::new("; ".as_bytes(), &mut file); + write_detailed_version_info(&mut comment_writer)?; + writeln!(comment_writer, "Source unit: {}", name)?; + if let Some(prove_result) = prove_result { + writeln!(comment_writer, "Prove result: {}", &prove_result)?; + } + file.write_all(smtlib.as_bytes())?; + tracing::info!(?file_path, "SMT-LIB query written to file"); + } + } + Ok(()) +} + /// The result of an SMT solver call for a [`SmtVcUnit`]. pub struct SmtVcCheckResult<'ctx> { pub prove_result: ProveResult<'ctx>, slice_model: Option, quant_vc: QuantVcUnit, - smtlib: Option, } impl<'ctx> SmtVcCheckResult<'ctx> { @@ -901,33 +958,4 @@ impl<'ctx> SmtVcCheckResult<'ctx> { Ok(()) } - - /// Write the SMT-LIB dump to a file if requested. - pub fn write_smtlib( - &self, - options: &Options, - name: &SourceUnitName, - ) -> Result<(), VerifyError> { - if options.debug_options.print_smt || options.debug_options.smt_dir.is_some() { - let mut smtlib = self.smtlib.clone().unwrap(); - smtlib.add_check_sat(); - smtlib.add_details_query(&self.prove_result); - let smtlib = smtlib.into_string(); - if options.debug_options.print_smt { - println!("\n; --- Solver SMT-LIB ---\n{}\n", smtlib); - } - if let Some(smt_dir) = &options.debug_options.smt_dir { - let file_path = smt_dir.join(name.to_file_name("smt2")); - create_dir_all(file_path.parent().unwrap())?; - let mut file = File::create(&file_path)?; - let mut comment_writer = PrefixWriter::new("; ".as_bytes(), &mut file); - write_detailed_version_info(&mut comment_writer)?; - writeln!(comment_writer, "Source unit: {}", name)?; - writeln!(comment_writer, "Prove result: {}", self.prove_result)?; - file.write_all(smtlib.as_bytes())?; - tracing::info!(?file_path, "SMT-LIB query written to file"); - } - } - Ok(()) - } } diff --git a/src/main.rs b/src/main.rs index 101b90b7..2a29cfc5 100644 --- a/src/main.rs +++ b/src/main.rs @@ -140,8 +140,9 @@ pub struct OptimizationOptions { #[arg(long)] pub egraph: bool, - /// Don't do reachability checks during unfolding of verification conditions - /// to eliminate unreachable branches. Instead, unfold all branches. + /// Don't do SMT-powered reachability checks during unfolding of + /// verification conditions to eliminate unreachable branches. Instead, + /// unfold all branches. #[arg(long)] pub strict: bool, @@ -223,6 +224,11 @@ pub struct DebugOptions { #[arg(long)] pub no_pretty_smtlib: bool, + /// Do not run the final SMT check to verify the program. This is useful to + /// obtain just the SMT-LIB output. + #[arg(long)] + pub no_verify: bool, + /// Enable Z3 tracing for the final SAT check. #[arg(long)] pub z3_trace: bool, @@ -703,15 +709,12 @@ fn verify_files_main( // 13. Create Z3 solver with axioms, solve let mut result = - vc_is_valid.run_solver(options, &limits_ref, &ctx, &mut translate, &slice_vars)?; + vc_is_valid.run_solver(options, &limits_ref,name, &ctx, &mut translate, &slice_vars)?; server .handle_vc_check_result(name, verify_unit.span, &mut result, &mut translate) .map_err(VerifyError::ServerError)?; - // If requested, write the SMT-LIB output. - result.write_smtlib(options, name)?; - if options.debug_options.z3_trace { info!("Z3 tracing output will be written to `z3.log`."); }