From 0d5c8ebfb60f90cb8e074bdacfa70b403727efb2 Mon Sep 17 00:00:00 2001 From: db Date: Wed, 8 Jul 2026 14:29:57 +0200 Subject: [PATCH] chore(deps): bump z3 to 0.20 in /rust z3 0.13+ removed the explicit-context API: the `'ctx` lifetime is gone and constructors run against an implicit thread-local context. Rewrite the solver in findchars-solver accordingly: - feature static-link-z3 -> vendored (builds Z3 4.16 from the z3-src crate) - drop Context; wrap solve_one in with_z3_config(&cfg, ..) with a fresh Config per group (set_timeout_msec replaces the old Params timeout), preserving the per-group context isolation - drop the leading &ctx arg from BV::new_const / BV::from_u64 - _eq -> fully-qualified Ast::eq (the bare .eq() now collides with PartialEq on BV, and _eq is deprecated) - assert() now takes Borrow, so pass the Bool by value (no outer &) Public API (LiteralCompiler::solve / solve_with_auto_split) and AsciiFindMask are unchanged. Verified: cargo test -p findchars-solver (7/7), cargo test -p findchars -p findchars-csv, and clippy --all-targets -D warnings. --- rust/Cargo.lock | 137 +++------------- rust/findchars-solver/Cargo.toml | 2 +- rust/findchars-solver/src/solver.rs | 236 ++++++++++++++-------------- 3 files changed, 141 insertions(+), 234 deletions(-) diff --git a/rust/Cargo.lock b/rust/Cargo.lock index 4aea77e..aa31b8f 100644 --- a/rust/Cargo.lock +++ b/rust/Cargo.lock @@ -38,32 +38,6 @@ version = "1.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53" -[[package]] -name = "bindgen" -version = "0.66.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f2b84e06fc203107bfbad243f4aba2af864eb7db3b1cf46ea0a023b0b433d2a7" -dependencies = [ - "bitflags", - "cexpr", - "clang-sys", - "lazy_static", - "lazycell", - "peeking_take_while", - "proc-macro2", - "quote", - "regex", - "rustc-hash", - "shlex 1.3.0", - "syn", -] - -[[package]] -name = "bitflags" -version = "2.13.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4388bee8683e3d04af747c73422af53102d2bd24d9eadb6cbc100baef4b43f8" - [[package]] name = "bumpalo" version = "3.20.3" @@ -83,16 +57,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f5d6cac793997bd970000024b2934968efe83b382de4fdcf4fcb46b6ee4ad996" dependencies = [ "find-msvc-tools", - "shlex 2.0.1", -] - -[[package]] -name = "cexpr" -version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6fac387a98bb7c37292057cffc56d62ecb629900026402633ae9160df93a8766" -dependencies = [ - "nom", + "shlex", ] [[package]] @@ -139,17 +104,6 @@ dependencies = [ "half", ] -[[package]] -name = "clang-sys" -version = "1.8.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b023947811758c97c59bf9d1c188fd619ad4718dcaa767947df1cadb14f39f4" -dependencies = [ - "glob", - "libc", - "libloading", -] - [[package]] name = "clap" version = "4.6.1" @@ -350,12 +304,6 @@ dependencies = [ "rand_core", ] -[[package]] -name = "glob" -version = "0.3.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0cc23270f6e1808e30a928bdc84dea0b9b4136a8bc82338574f23baf47bbd280" - [[package]] name = "half" version = "2.7.1" @@ -393,34 +341,12 @@ dependencies = [ "wasm-bindgen", ] -[[package]] -name = "lazy_static" -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.186" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66" -[[package]] -name = "libloading" -version = "0.8.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d7c4b02199fee7c5d21a5ae7d8cfa79a6ef5bb2fc834d6e9058e89c825efdc55" -dependencies = [ - "cfg-if", - "windows-link", -] - [[package]] name = "log" version = "0.4.33" @@ -433,22 +359,6 @@ version = "2.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "88904434abc2901f197fe8cc55f0445e7ded921dba5911dad2e2b39b48e663c4" -[[package]] -name = "minimal-lexical" -version = "0.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" - -[[package]] -name = "nom" -version = "7.1.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a" -dependencies = [ - "memchr", - "minimal-lexical", -] - [[package]] name = "num-traits" version = "0.2.19" @@ -480,18 +390,18 @@ dependencies = [ "winapi", ] -[[package]] -name = "peeking_take_while" -version = "0.1.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "19b17cddbe7ec3f8bc800887bab5e717348c95ea2ca0b1bf0837fb964dc67099" - [[package]] name = "pin-project-lite" version = "0.2.17" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" +[[package]] +name = "pkg-config" +version = "0.3.33" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "19f132c84eca552bf34cab8ec81f1c1dcc229b811638f9d283dceabe58c5569e" + [[package]] name = "plotters" version = "0.3.7" @@ -610,12 +520,6 @@ version = "0.8.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d6f6ff9a378485b298a5286656da665ba74413d36db0979633275d2e708145d4" -[[package]] -name = "rustc-hash" -version = "1.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2" - [[package]] name = "rustversion" version = "1.0.23" @@ -674,12 +578,6 @@ dependencies = [ "zmij", ] -[[package]] -name = "shlex" -version = "1.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" - [[package]] name = "shlex" version = "2.0.1" @@ -852,24 +750,33 @@ dependencies = [ [[package]] name = "z3" -version = "0.12.1" +version = "0.20.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4a7ff5718c079e7b813378d67a5bed32ccc2086f151d6185074a7e24f4a565e8" +checksum = "80c4de445f5c9e3013703a6b8a40c80b4a64c925f0a19e7d0a23a7a9b70e854d" dependencies = [ "log", "z3-sys", ] [[package]] -name = "z3-sys" -version = "0.8.1" +name = "z3-src" +version = "416.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d7cf70fdbc0de3f42b404f49b0d4686a82562254ea29ff0a155eef2f5430f4b0" +checksum = "f2af0c6527de39877cf55cb87f233016573eeeb7cf77afdc1469e4b32faef832" dependencies = [ - "bindgen", "cmake", ] +[[package]] +name = "z3-sys" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c18b0a91a13522d21b3414847667de2b2056a721a3edcb5b6ee6858352d58db4" +dependencies = [ + "pkg-config", + "z3-src", +] + [[package]] name = "zerocopy" version = "0.8.53" diff --git a/rust/findchars-solver/Cargo.toml b/rust/findchars-solver/Cargo.toml index 71d91ec..43c537d 100644 --- a/rust/findchars-solver/Cargo.toml +++ b/rust/findchars-solver/Cargo.toml @@ -8,4 +8,4 @@ license.workspace = true repository.workspace = true [dependencies] -z3 = { version = "0.12", features = ["static-link-z3"] } +z3 = { version = "0.20", features = ["vendored"] } diff --git a/rust/findchars-solver/src/solver.rs b/rust/findchars-solver/src/solver.rs index 2bec6f6..6fba5dc 100644 --- a/rust/findchars-solver/src/solver.rs +++ b/rust/findchars-solver/src/solver.rs @@ -4,7 +4,7 @@ //! target character. Uses Z3's bitvector theory for constraint solving. use z3::ast::{Ast, BV}; -use z3::{Config, Context, SatResult, Solver}; +use z3::{Config, SatResult, Solver, with_z3_config}; use crate::literal::{AsciiFindMask, AsciiLiteralGroup, ByteLiteral}; @@ -49,140 +49,140 @@ impl LiteralCompiler { vector_byte_size: usize, group: &AsciiLiteralGroup, ) -> Result { - let cfg = Config::new(); - let ctx = Context::new(&cfg); - let solver = Solver::new(&ctx); - // Timeout: 5 seconds per solve attempt. If Z3 can't solve in 5s, - // the group is likely too large and should be split. - let mut params = z3::Params::new(&ctx); - params.set_u32("timeout", 5000); - solver.set_params(¶ms); - - let num_literals = group.literals.len(); - - // Create Z3 bitvector variables for the two 16-entry LUTs - let low_nibbles: Vec = (0..16) - .map(|i| BV::new_const(&ctx, format!("lo_{i}"), 8)) - .collect(); - let high_nibbles: Vec = (0..16) - .map(|i| BV::new_const(&ctx, format!("hi_{i}"), 8)) - .collect(); - - // Create Z3 variables for each literal's assigned byte value - let lit_vars: Vec = (0..num_literals) - .map(|i| BV::new_const(&ctx, format!("lit_{i}"), 8)) - .collect(); - - // Constraint: each literal > 0 - let zero = BV::from_u64(&ctx, 0, 8); - for lv in &lit_vars { - solver.assert(&lv.bvugt(&zero)); - } - - // Constraint: each literal < vector_byte_size - let max_lit = BV::from_u64(&ctx, vector_byte_size as u64, 8); - for lv in &lit_vars { - solver.assert(&lv.bvult(&max_lit)); - } - - // Constraint: literals are distinct - for i in 0..num_literals { - for j in (i + 1)..num_literals { - solver.assert(&lit_vars[i]._eq(&lit_vars[j]).not()); + // Timeout: 5 seconds per solve attempt. If Z3 can't solve in 5s, the + // group is likely too large and should be split. A fresh config — and + // thus a fresh implicit context — isolates each group's solve. + let mut cfg = Config::new(); + cfg.set_timeout_msec(5000); + + with_z3_config(&cfg, || { + let solver = Solver::new(); + + let num_literals = group.literals.len(); + + // Create Z3 bitvector variables for the two 16-entry LUTs + let low_nibbles: Vec = (0..16).map(|i| BV::new_const(format!("lo_{i}"), 8)).collect(); + let high_nibbles: Vec = + (0..16).map(|i| BV::new_const(format!("hi_{i}"), 8)).collect(); + + // Create Z3 variables for each literal's assigned byte value + let lit_vars: Vec = (0..num_literals) + .map(|i| BV::new_const(format!("lit_{i}"), 8)) + .collect(); + + // Constraint: each literal > 0 + let zero = BV::from_u64(0, 8); + for lv in &lit_vars { + solver.assert(lv.bvugt(&zero)); } - } - // Constraint: literals not in used set - for lv in &lit_vars { - for &used in used_literals { - let used_bv = BV::from_u64(&ctx, used as u64, 8); - solver.assert(&lv._eq(&used_bv).not()); + // Constraint: each literal < vector_byte_size + let max_lit = BV::from_u64(vector_byte_size as u64, 8); + for lv in &lit_vars { + solver.assert(lv.bvult(&max_lit)); } - } - // Matching constraints: for each literal and each target byte, - // lo[byte & 0xF] AND hi[byte >> 4] == literal_value - for (lit_idx, literal) in group.literals.iter().enumerate() { - for &target_byte in &literal.chars { - let lo_idx = (target_byte & 0x0F) as usize; - let hi_idx = ((target_byte >> 4) & 0x0F) as usize; - let and_result = low_nibbles[lo_idx].bvand(&high_nibbles[hi_idx]); - solver.assert(&and_result._eq(&lit_vars[lit_idx])); + // Constraint: literals are distinct + for i in 0..num_literals { + for j in (i + 1)..num_literals { + solver.assert(Ast::eq(&lit_vars[i], &lit_vars[j]).not()); + } } - } - // Exclusion constraints: for all non-target nibble pairs, - // lo[i] AND hi[j] must not equal any literal - let mut target_nibble_pairs = std::collections::HashSet::new(); - for literal in &group.literals { - for &target_byte in &literal.chars { - let lo = (target_byte & 0x0F) as usize; - let hi = ((target_byte >> 4) & 0x0F) as usize; - target_nibble_pairs.insert((lo, hi)); + // Constraint: literals not in used set + for lv in &lit_vars { + for &used in used_literals { + let used_bv = BV::from_u64(used as u64, 8); + solver.assert(Ast::eq(lv, &used_bv).not()); + } } - } - #[allow(clippy::needless_range_loop)] - for i in 0..16 { - for j in 0..16 { - if target_nibble_pairs.contains(&(i, j)) { - continue; - } - let and_result = low_nibbles[i].bvand(&high_nibbles[j]); - // The AND result must be zero OR must not match any literal - // Simplest: require AND result to be zero for non-target pairs - // when masked to vector_byte_size - let masked = if vector_byte_size < 256 { - let mask = BV::from_u64(&ctx, (vector_byte_size - 1) as u64, 8); - and_result.bvand(&mask) - } else { - and_result - }; - - // For non-target pairs: the masked result must not equal any literal - for lv in &lit_vars { - solver.assert(&masked._eq(lv).not()); + // Matching constraints: for each literal and each target byte, + // lo[byte & 0xF] AND hi[byte >> 4] == literal_value + for (lit_idx, literal) in group.literals.iter().enumerate() { + for &target_byte in &literal.chars { + let lo_idx = (target_byte & 0x0F) as usize; + let hi_idx = ((target_byte >> 4) & 0x0F) as usize; + let and_result = low_nibbles[lo_idx].bvand(&high_nibbles[hi_idx]); + solver.assert(Ast::eq(&and_result, &lit_vars[lit_idx])); } } - } - // Solve - match solver.check() { - SatResult::Sat => { - let model = solver.get_model().unwrap(); - - // Extract LUT values - let mut low_mask = [0u8; 16]; - let mut high_mask = [0u8; 16]; - for i in 0..16 { - low_mask[i] = - model.eval(&low_nibbles[i], true).unwrap().as_u64().unwrap() as u8; - high_mask[i] = - model.eval(&high_nibbles[i], true).unwrap().as_u64().unwrap() as u8; + // Exclusion constraints: for all non-target nibble pairs, + // lo[i] AND hi[j] must not equal any literal + let mut target_nibble_pairs = std::collections::HashSet::new(); + for literal in &group.literals { + for &target_byte in &literal.chars { + let lo = (target_byte & 0x0F) as usize; + let hi = ((target_byte >> 4) & 0x0F) as usize; + target_nibble_pairs.insert((lo, hi)); } + } - // Extract literal assignments - let mut literal_map = Vec::new(); - let mut name_literal_map = std::collections::HashMap::new(); - for (lit_idx, literal) in group.literals.iter().enumerate() { - let lit_val = - model.eval(&lit_vars[lit_idx], true).unwrap().as_u64().unwrap() as u8; - name_literal_map.insert(literal.name.clone(), lit_val); - for &target_byte in &literal.chars { - literal_map.push((target_byte, lit_val)); + #[allow(clippy::needless_range_loop)] + for i in 0..16 { + for j in 0..16 { + if target_nibble_pairs.contains(&(i, j)) { + continue; + } + let and_result = low_nibbles[i].bvand(&high_nibbles[j]); + // The AND result must be zero OR must not match any literal + // Simplest: require AND result to be zero for non-target pairs + // when masked to vector_byte_size + let masked = if vector_byte_size < 256 { + let mask = BV::from_u64((vector_byte_size - 1) as u64, 8); + and_result.bvand(&mask) + } else { + and_result + }; + + // For non-target pairs: the masked result must not equal any literal + for lv in &lit_vars { + solver.assert(Ast::eq(&masked, lv).not()); } } + } + + // Solve + match solver.check() { + SatResult::Sat => { + let model = solver.get_model().unwrap(); + + // Extract LUT values + let mut low_mask = [0u8; 16]; + let mut high_mask = [0u8; 16]; + for i in 0..16 { + low_mask[i] = + model.eval(&low_nibbles[i], true).unwrap().as_u64().unwrap() as u8; + high_mask[i] = + model.eval(&high_nibbles[i], true).unwrap().as_u64().unwrap() as u8; + } + + // Extract literal assignments + let mut literal_map = Vec::new(); + let mut name_literal_map = std::collections::HashMap::new(); + for (lit_idx, literal) in group.literals.iter().enumerate() { + let lit_val = + model.eval(&lit_vars[lit_idx], true).unwrap().as_u64().unwrap() as u8; + name_literal_map.insert(literal.name.clone(), lit_val); + for &target_byte in &literal.chars { + literal_map.push((target_byte, lit_val)); + } + } - Ok(AsciiFindMask { - low_nibble_mask: low_mask, - high_nibble_mask: high_mask, - literal_map, - name_literal_map, - }) + Ok(AsciiFindMask { + low_nibble_mask: low_mask, + high_nibble_mask: high_mask, + literal_map, + name_literal_map, + }) + } + SatResult::Unsat => { + Err("unsatisfiable: no valid LUT pair exists for this group".into()) + } + SatResult::Unknown => Err("solver returned unknown".into()), } - SatResult::Unsat => Err("unsatisfiable: no valid LUT pair exists for this group".into()), - SatResult::Unknown => Err("solver returned unknown".into()), - } + }) } /// Solve with auto-split: if a single group fails, partition and recurse.