From 78e781a41b162f8f07ab9a735faff775f71939b9 Mon Sep 17 00:00:00 2001 From: Emil Date: Mon, 23 Dec 2024 20:23:00 +0100 Subject: [PATCH] Fixes after rebasing --- Cargo.lock | 16 ++++------------ src/driver.rs | 4 ++-- src/main.rs | 6 +++--- src/slicing/transform_test.rs | 4 ++-- src/smt/limited.rs | 3 ++- src/smt/translate_exprs.rs | 8 ++++++-- 6 files changed, 19 insertions(+), 22 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 0b3da94e..a658b584 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -155,16 +155,14 @@ checksum = "9d297deb1925b89f2ccc13d7635fa0714f12c87adce1c75356b39ca9b7178567" [[package]] name = "bindgen" -version = "0.69.5" +version = "0.70.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "271383c67ccabffb7381723dea0672a673f292304fcb45c01cc648c7a8d58088" +checksum = "f49d8fed880d473ea71efb9bf597651e77201bdd4893efe54c9e5d65ae04ce6f" dependencies = [ "bitflags 2.6.0", "cexpr", "clang-sys", "itertools 0.12.1", - "lazy_static", - "lazycell", "proc-macro2", "quote", "regex", @@ -1109,12 +1107,6 @@ version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" -[[package]] -name = "lazycell" -version = "1.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "830d08ce1d1d941e6b30645f1a0eb5643013d835ce3779a5fc208261dbe10f55" - [[package]] name = "libc" version = "0.2.169" @@ -2495,7 +2487,7 @@ dependencies = [ [[package]] name = "z3" version = "0.12.1" -source = "git+https://github.com/Philipp15b/z3.rs.git?rev=bdd501ca1e50785365b875b3438a0cf953cffbfc#bdd501ca1e50785365b875b3438a0cf953cffbfc" +source = "git+https://github.com/prove-rs/z3.rs.git?rev=60001b36fc8a7ab1d4f22595e80a3b6f7adc1bcf#60001b36fc8a7ab1d4f22595e80a3b6f7adc1bcf" dependencies = [ "log", "num", @@ -2505,7 +2497,7 @@ dependencies = [ [[package]] name = "z3-sys" version = "0.8.1" -source = "git+https://github.com/Philipp15b/z3.rs.git?rev=bdd501ca1e50785365b875b3438a0cf953cffbfc#bdd501ca1e50785365b875b3438a0cf953cffbfc" +source = "git+https://github.com/prove-rs/z3.rs.git?rev=60001b36fc8a7ab1d4f22595e80a3b6f7adc1bcf#60001b36fc8a7ab1d4f22595e80a3b6f7adc1bcf" dependencies = [ "bindgen", "cmake", diff --git a/src/driver.rs b/src/driver.rs index f59868e4..2fb277c6 100644 --- a/src/driver.rs +++ b/src/driver.rs @@ -683,10 +683,10 @@ impl<'ctx> SmtVcUnit<'ctx> { let _entered = span.enter(); let mut prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc); - if options.force_ematching { + if options.opt_options.force_ematching { prover.enforce_ematching(); } - if let Some(seed) = options.z3_seed { + if let Some(seed) = options.debug_options.z3_seed { prover.seed(seed); } diff --git a/src/main.rs b/src/main.rs index b8a2fba3..5d448907 100644 --- a/src/main.rs +++ b/src/main.rs @@ -249,7 +249,7 @@ pub struct DebugOptions { pub z3_trace: bool, /// An explicit seed used by Z3 for the final SAT check. - #[structopt(long)] + #[arg(long)] pub z3_seed: Option, } @@ -721,8 +721,8 @@ fn verify_files_main( &ctx, &tcx, SmtCtxOptions { - use_limited_functions: options.limited_functions, - lit_wrap: options.lit_wrap, + use_limited_functions: options.opt_options.limited_functions, + lit_wrap: options.opt_options.lit_wrap, }, ); let mut translate = TranslateExprs::new(&smt_ctx); diff --git a/src/slicing/transform_test.rs b/src/slicing/transform_test.rs index c8f4b4a2..32fd14b9 100644 --- a/src/slicing/transform_test.rs +++ b/src/slicing/transform_test.rs @@ -16,7 +16,7 @@ use crate::{ tyctx::TyCtx, vc::vcgen::Vcgen, }; - +use crate::smt::SmtCtxOptions; use super::{ selection::SliceSelection, transform::{SliceStmt, SliceStmts, StmtSliceVisitor}, @@ -121,7 +121,7 @@ fn prove_equiv( stmt2_vc.clone(), ); let ctx = z3::Context::new(&z3::Config::new()); - let smt_ctx = SmtCtx::new(&ctx, tcx); + let smt_ctx = SmtCtx::new(&ctx, tcx, SmtCtxOptions::default()); let mut translate = TranslateExprs::new(&smt_ctx); let eq_expr_z3 = translate.t_bool(&eq_expr); let mut prover = Prover::new(&ctx); diff --git a/src/smt/limited.rs b/src/smt/limited.rs index b224a9a8..abb34633 100644 --- a/src/smt/limited.rs +++ b/src/smt/limited.rs @@ -8,6 +8,7 @@ //! For this to work the SMT solver is not allowed to synthesis fuel values itself. //! Therefore, MBQI must be disabled. +use std::collections::HashSet; use crate::ast::visit::{walk_expr, VisitorMut}; use crate::ast::{ Expr, ExprBuilder, ExprData, ExprKind, FuncDecl, Ident, PointerHashShared, QuantVar, @@ -263,7 +264,7 @@ pub fn return_value_invariant<'smt, 'ctx>( type HashExpr = PointerHashShared; #[derive(Default)] -pub struct ConstantExprs(IndexSet); +pub struct ConstantExprs(HashSet); impl ConstantExprs { pub fn is_constant(&self, expr: &Expr) -> bool { diff --git a/src/smt/translate_exprs.rs b/src/smt/translate_exprs.rs index 99f9a25e..5b92610a 100644 --- a/src/smt/translate_exprs.rs +++ b/src/smt/translate_exprs.rs @@ -1,9 +1,9 @@ //! Translation of Caesar expressions to Z3 expressions. use itertools::Itertools; -use once_cell::unsync::OnceCell; use ref_cast::RefCast; use std::{collections::HashMap, convert::TryFrom, vec}; +use std::cell::OnceCell; use z3::{ ast::{Ast, Bool, Dynamic, Int, Real}, Pattern, @@ -813,7 +813,11 @@ impl<'ctx> QuantifiedFuel<'ctx> { pub fn new(value: Option>) -> Self { Self { lazy_fuel: match value { - Some(s) => OnceCell::with_value(s), + Some(s) => { + let cell = OnceCell::new(); + cell.set(s).unwrap_or_else(|_| unreachable!("Cell was newly constructed")); + cell + }, None => OnceCell::new(), }, }