From 5cc855930e5036c30b0251d662eccbec05a0fdf7 Mon Sep 17 00:00:00 2001 From: Brit Date: Mon, 29 Jun 2026 08:23:47 +0200 Subject: [PATCH 1/5] feat(bitwuzla): add Bitwuzla SMT backend Translate the validated wire IR to Bitwuzla via hand-written FFI bindings (0.9.1). Implements solve, model extraction, named unsat cores, and bit-hunt optimization behind the optional `bitwuzla` cargo feature. --- Cargo.lock | 1 + crates/smt-server/Cargo.toml | 6 + crates/smt-server/src/bitwuzla_backend.rs | 882 +++++++++++++++++++++ crates/smt-server/src/bitwuzla_bindings.rs | 174 ++++ crates/smt-server/src/lib.rs | 9 +- crates/smt-server/src/main.rs | 28 +- 6 files changed, 1089 insertions(+), 11 deletions(-) create mode 100644 crates/smt-server/src/bitwuzla_backend.rs create mode 100644 crates/smt-server/src/bitwuzla_bindings.rs diff --git a/Cargo.lock b/Cargo.lock index e636044..4ec3617 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1943,6 +1943,7 @@ version = "0.1.0" dependencies = [ "binbit", "blake3", + "pkg-config", "qfbvsmtrs", "rumba-core", "rusqlite", diff --git a/crates/smt-server/Cargo.toml b/crates/smt-server/Cargo.toml index c774ff8..1d7e166 100644 --- a/crates/smt-server/Cargo.toml +++ b/crates/smt-server/Cargo.toml @@ -17,3 +17,9 @@ z3 = { version = "0.20.0", features = ["gh-release"] } [dev-dependencies] rumba-core = { git = "https://github.com/thalium/rumba", rev = "2a7a38963f9894cdda24ea93b5f278752aff7a2e", features = ["parse"] } + +[features] +bitwuzla = ["dep:pkg-config"] + +[build-dependencies] +pkg-config = { version = "0.3", optional = true } diff --git a/crates/smt-server/src/bitwuzla_backend.rs b/crates/smt-server/src/bitwuzla_backend.rs new file mode 100644 index 0000000..bcc2bbe --- /dev/null +++ b/crates/smt-server/src/bitwuzla_backend.rs @@ -0,0 +1,882 @@ +//! Bitwuzla backend: translates the validated wire IR to Bitwuzla via the C API +//! (see [`crate::bitwuzla_bindings`]) and supports solve, model extraction, +//! named unsat cores (via unsat assumptions), and bit-hunt optimization. +//! +//! Cancellation uses Bitwuzla's termination callback: a scoped watcher thread +//! mirrors the [`SolveContext`] token + budget deadline into an `AtomicBool` +//! the callback polls, so `check_sat` stops when the racer wins or the budget +//! elapses. + +use std::collections::{HashMap, HashSet}; +use std::ffi::{CStr, CString}; +use std::sync::atomic::{AtomicBool, Ordering}; +use std::sync::Arc; +use std::time::{Duration, Instant}; + +use smt_wire::raw::{ + request_flags, tag, BinaryRequest, BlobRef, Command, ExprView, ModelBlock, ModelEntry, NodeRef, + OptimizationValueBlock, RawNode, ScalarValue, SimplifyBlock, Sort, UnsatCoreBlock, WireError, +}; + +use crate::backend::{Backend, QueryResult, SolveContext}; +use crate::bitwuzla_bindings as ffi; +use ffi::{Bitwuzla, BitwuzlaTerm, BitwuzlaTermManager}; + +#[derive(Debug, Clone, Default)] +pub struct BitwuzlaBackend; + +impl Backend for BitwuzlaBackend { + fn name(&self) -> &'static str { + "bitwuzla" + } + + fn handle(&self, request: &BinaryRequest) -> smt_wire::Result { + handle_inner(request, None) + } + + fn handle_with_context( + &self, + request: &BinaryRequest, + context: &SolveContext, + ) -> smt_wire::Result { + if context.is_cancelled() { + return Ok(QueryResult::unknown( + "bitwuzla request cancelled before start", + )); + } + handle_inner(request, Some(context)) + } +} + +fn handle_inner( + request: &BinaryRequest, + context: Option<&SolveContext>, +) -> smt_wire::Result { + let deadline = BitwuzlaDeadline::from_budget_ms(request.envelope.budget_ms); + match request.envelope.command { + Command::Simplify => Ok(QueryResult::simplified(SimplifyBlock { + expression: request.expression.clone(), + target_node: request + .target_ref() + .ok_or_else(|| WireError::invalid("simplify request", "missing target_node"))?, + })), + Command::Solve | Command::Minimize | Command::Maximize => { + let solver = BitwuzlaSolver::new(); + match request.envelope.command { + Command::Solve => solve(request, &solver, context, deadline), + Command::Minimize | Command::Maximize => { + optimize(request, &solver, context, deadline) + } + Command::Simplify => unreachable!("handled above"), + } + } + } +} + +/// RAII guard owning a term manager, options, and a Bitwuzla instance. +/// +/// `bitwuzla_new` borrows (does not own) both the term manager and options, so +/// the instance is deleted first, then the options, then the term manager. +struct BitwuzlaSolver { + tm: *mut BitwuzlaTermManager, + options: *mut ffi::BitwuzlaOptions, + bz: *mut Bitwuzla, +} + +// The solver is constructed and dropped within a single `handle` call on one +// thread; the raw pointers never cross threads, so this is sound without Send. + +impl BitwuzlaSolver { + fn new() -> Self { + // Safety: the C calls are independent of thread state; the manager and + // options are created fresh and paired with a new instance below. + unsafe { + let tm = ffi::bitwuzla_term_manager_new(); + let options = ffi::bitwuzla_options_new(); + // Model generation and unsat-assumption tracking are cheap and + // always enabled so solve/optimize/core paths work uniformly. + ffi::bitwuzla_set_option(options, ffi::BITWUZLA_OPT_PRODUCE_MODELS, 1); + ffi::bitwuzla_set_option(options, ffi::BITWUZLA_OPT_PRODUCE_UNSAT_ASSUMPTIONS, 1); + let bz = ffi::bitwuzla_new(tm, options); + Self { tm, options, bz } + } + } + + fn tm(&self) -> *mut BitwuzlaTermManager { + self.tm + } + + fn bz(&self) -> *mut Bitwuzla { + self.bz + } +} + +impl Drop for BitwuzlaSolver { + fn drop(&mut self) { + // Safety: each pointer was created by the matching `_new` call above and + // is released exactly once, in the order required by the C API + // (instance, then options, then term manager). + unsafe { + if !self.bz.is_null() { + ffi::bitwuzla_delete(self.bz); + } + if !self.options.is_null() { + ffi::bitwuzla_options_delete(self.options); + } + if !self.tm.is_null() { + ffi::bitwuzla_term_manager_delete(self.tm); + } + } + } +} + +#[derive(Clone, Copy)] +struct BitwuzlaDeadline { + deadline: Option, +} + +impl BitwuzlaDeadline { + fn from_budget_ms(budget_ms: u32) -> Self { + let deadline = + (budget_ms != 0).then(|| Instant::now() + Duration::from_millis(u64::from(budget_ms))); + Self { deadline } + } + + fn elapsed(self) -> bool { + self.deadline.is_some_and(|d| Instant::now() >= d) + } +} + +#[derive(Clone)] +struct BitwuzlaVariable { + node_ref: NodeRef, + sort: Sort, + width: u32, +} + +struct BitwuzlaTranslation { + tm: *mut BitwuzlaTermManager, + bool_sort: ffi::BitwuzlaSort, + bv_sorts: HashMap, + bvs: Vec>, + bools: Vec>, + variables: Vec, +} + +impl BitwuzlaTranslation { + fn bv_sort(&mut self, width: u32) -> ffi::BitwuzlaSort { + *self + .bv_sorts + .entry(width) + .or_insert_with(|| unsafe { ffi::bitwuzla_mk_bv_sort(self.tm, width as u64) }) + } + + fn bv(&self, reference: NodeRef) -> smt_wire::Result { + if !reference.is_bv() { + return Err(WireError::invalid( + "bitwuzla translation", + "expected BV reference", + )); + } + self.bvs + .get(reference.index() as usize) + .and_then(|opt| *opt) + .ok_or_else(|| WireError::invalid("bitwuzla translation", "missing BV term")) + } + + fn bool(&self, reference: NodeRef) -> smt_wire::Result { + if !reference.is_bool() { + return Err(WireError::invalid( + "bitwuzla translation", + "expected Bool reference", + )); + } + self.bools + .get(reference.index() as usize) + .and_then(|opt| *opt) + .ok_or_else(|| WireError::invalid("bitwuzla translation", "missing Bool term")) + } +} + +fn translate( + request: &BinaryRequest, + tm: *mut BitwuzlaTermManager, +) -> smt_wire::Result { + let expr = request.expression_view()?; + let bool_sort = unsafe { ffi::bitwuzla_mk_bool_sort(tm) }; + let mut out = BitwuzlaTranslation { + tm, + bool_sort, + bv_sorts: HashMap::new(), + bvs: vec![None; expr.node_count() as usize], + bools: vec![None; expr.node_count() as usize], + variables: Vec::new(), + }; + let mut bv_vars: HashMap<(String, u32), BitwuzlaTerm> = HashMap::new(); + let mut bool_vars: HashMap = HashMap::new(); + + for index in 0..expr.node_count() { + let node = expr.node(index)?; + match node.tag { + tag::BV_VAR => { + let name = expr + .blob_str(BlobRef::from_payload(node.payload), "BV variable")? + .to_owned(); + let term = if let Some(&existing) = bv_vars.get(&(name.clone(), node.width)) { + existing + } else { + let sort = out.bv_sort(node.width); + let symbol = CString::new(format!("bv_{index}")) + .map_err(|_| WireError::invalid("BV variable", "symbol contains nul"))?; + let term = unsafe { ffi::bitwuzla_mk_const(tm, sort, symbol.as_ptr()) }; + bv_vars.insert((name, node.width), term); + term + }; + out.variables.push(BitwuzlaVariable { + node_ref: NodeRef::bv(index)?, + sort: Sort::Bv, + width: node.width, + }); + out.bvs[index as usize] = Some(term); + } + tag::BV_CONST => { + out.bvs[index as usize] = Some(bitwuzla_bv_const( + &expr, + &mut out, + node.width, + node.payload, + )?); + } + tag::BV_NOT => { + let x = child_bv(&expr, &out, &node, 0)?; + out.bvs[index as usize] = Some(mk1(tm, ffi::BITWUZLA_KIND_BV_NOT, x)); + } + tag::BV_NEG => { + let x = child_bv(&expr, &out, &node, 0)?; + out.bvs[index as usize] = Some(mk1(tm, ffi::BITWUZLA_KIND_BV_NEG, x)); + } + tag::BV_AND => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_AND, a, b)); + } + tag::BV_OR => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_OR, a, b)); + } + tag::BV_XOR => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_XOR, a, b)); + } + tag::BV_ADD => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_ADD, a, b)); + } + tag::BV_SUB => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_SUB, a, b)); + } + tag::BV_MUL => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_MUL, a, b)); + } + tag::BV_UDIV => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_UDIV, a, b)); + } + tag::BV_UREM => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_UREM, a, b)); + } + tag::BV_SDIV => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_SDIV, a, b)); + } + tag::BV_SREM => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_SREM, a, b)); + } + tag::BV_SMOD => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_SMOD, a, b)); + } + tag::BV_SHL => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_SHL, a, b)); + } + tag::BV_LSHR => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_SHR, a, b)); + } + tag::BV_ASHR => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_ASHR, a, b)); + } + tag::BV_EXTRACT => { + let x = child_bv(&expr, &out, &node, 0)?; + out.bvs[index as usize] = Some(unsafe { + ffi::bitwuzla_mk_term1_indexed2( + tm, + ffi::BITWUZLA_KIND_BV_EXTRACT, + x, + u64::from(node.aux_hi), + u64::from(node.aux_lo), + ) + }); + } + tag::BV_CONCAT => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bvs[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_CONCAT, a, b)); + } + tag::BV_ZEXT => { + let x = child_bv(&expr, &out, &node, 0)?; + out.bvs[index as usize] = Some(unsafe { + ffi::bitwuzla_mk_term1_indexed1( + tm, + ffi::BITWUZLA_KIND_BV_ZERO_EXTEND, + x, + u64::from(node.aux_hi), + ) + }); + } + tag::BV_SEXT => { + let x = child_bv(&expr, &out, &node, 0)?; + out.bvs[index as usize] = Some(unsafe { + ffi::bitwuzla_mk_term1_indexed1( + tm, + ffi::BITWUZLA_KIND_BV_SIGN_EXTEND, + x, + u64::from(node.aux_hi), + ) + }); + } + tag::BV_ITE => { + let c = child_bool(&expr, &out, &node, 0)?; + let t = child_bv(&expr, &out, &node, 1)?; + let e = child_bv(&expr, &out, &node, 2)?; + out.bvs[index as usize] = Some(mk3(tm, ffi::BITWUZLA_KIND_ITE, c, t, e)); + } + tag::BV_SELECT => { + let pairs = u32::from(node.aux_hi); + let mut result = child_bv(&expr, &out, &node, pairs * 2)?; + for pair in (0..pairs).rev() { + let selector = child_bool(&expr, &out, &node, pair * 2)?; + let value = child_bv(&expr, &out, &node, pair * 2 + 1)?; + result = mk3(tm, ffi::BITWUZLA_KIND_ITE, selector, value, result); + } + out.bvs[index as usize] = Some(result); + } + tag::BOOL_TRUE => { + out.bools[index as usize] = Some(unsafe { ffi::bitwuzla_mk_true(tm) }) + } + tag::BOOL_FALSE => { + out.bools[index as usize] = Some(unsafe { ffi::bitwuzla_mk_false(tm) }) + } + tag::BOOL_VAR => { + let name = expr + .blob_str(BlobRef::from_payload(node.payload), "Bool variable")? + .to_owned(); + let term = if let Some(&existing) = bool_vars.get(&name) { + existing + } else { + let symbol = CString::new(format!("bool_{index}")) + .map_err(|_| WireError::invalid("Bool variable", "symbol contains nul"))?; + let term = + unsafe { ffi::bitwuzla_mk_const(tm, out.bool_sort, symbol.as_ptr()) }; + bool_vars.insert(name, term); + term + }; + out.variables.push(BitwuzlaVariable { + node_ref: NodeRef::bool(index)?, + sort: Sort::Bool, + width: 0, + }); + out.bools[index as usize] = Some(term); + } + tag::BOOL_NOT => { + let x = child_bool(&expr, &out, &node, 0)?; + out.bools[index as usize] = Some(mk1(tm, ffi::BITWUZLA_KIND_NOT, x)); + } + tag::BOOL_AND => { + let (a, b) = child_bool2(&expr, &out, &node)?; + out.bools[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_AND, a, b)); + } + tag::BOOL_OR => { + let (a, b) = child_bool2(&expr, &out, &node)?; + out.bools[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_OR, a, b)); + } + tag::BOOL_IMPLIES => { + let (a, b) = child_bool2(&expr, &out, &node)?; + out.bools[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_IMPLIES, a, b)); + } + tag::BV_EQ => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bools[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_EQUAL, a, b)); + } + tag::BV_ULT => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bools[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_ULT, a, b)); + } + tag::BV_ULE => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bools[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_ULE, a, b)); + } + tag::BV_SLT => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bools[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_SLT, a, b)); + } + tag::BV_SLE => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bools[index as usize] = Some(mk2(tm, ffi::BITWUZLA_KIND_BV_SLE, a, b)); + } + tag::UADD_OVF => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bools[index as usize] = + Some(mk2(tm, ffi::BITWUZLA_KIND_BV_UADD_OVERFLOW, a, b)); + } + tag::SADD_OVF => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bools[index as usize] = + Some(mk2(tm, ffi::BITWUZLA_KIND_BV_SADD_OVERFLOW, a, b)); + } + tag::USUB_OVF => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bools[index as usize] = + Some(mk2(tm, ffi::BITWUZLA_KIND_BV_USUB_OVERFLOW, a, b)); + } + tag::SSUB_OVF => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bools[index as usize] = + Some(mk2(tm, ffi::BITWUZLA_KIND_BV_SSUB_OVERFLOW, a, b)); + } + tag::UMUL_OVF => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bools[index as usize] = + Some(mk2(tm, ffi::BITWUZLA_KIND_BV_UMUL_OVERFLOW, a, b)); + } + tag::SMUL_OVF => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bools[index as usize] = + Some(mk2(tm, ffi::BITWUZLA_KIND_BV_SMUL_OVERFLOW, a, b)); + } + tag::NEG_OVF => { + let a = child_bv(&expr, &out, &node, 0)?; + out.bools[index as usize] = Some(mk1(tm, ffi::BITWUZLA_KIND_BV_NEG_OVERFLOW, a)); + } + tag::SDIV_OVF => { + let (a, b) = child_bv2(&expr, &out, &node)?; + out.bools[index as usize] = + Some(mk2(tm, ffi::BITWUZLA_KIND_BV_SDIV_OVERFLOW, a, b)); + } + other => { + return Err(WireError::invalid( + "bitwuzla translation", + format!("unknown tag {other}"), + )) + } + } + } + Ok(out) +} + +fn solve( + request: &BinaryRequest, + solver: &BitwuzlaSolver, + context: Option<&SolveContext>, + deadline: BitwuzlaDeadline, +) -> smt_wire::Result { + let expr = request.expression_view()?; + let translation = translate(request, solver.tm())?; + let bz = solver.bz(); + let want_model = (request.envelope.flags & request_flags::WANT_MODEL) != 0; + let want_core = (request.envelope.flags & request_flags::WANT_CORE) != 0; + let named_count = request.named_assertion_refs.len(); + + // Named assertions become assumptions (so `get_unsat_assumptions` can + // identify which are in the core); unnamed assertions stay hard. + let mut named: Vec<(BitwuzlaTerm, String)> = Vec::new(); + let mut assumptions: Vec = Vec::new(); + for (index, root) in request.assertion_roots.iter().enumerate() { + let assertion = translation.bool(*root)?; + if index < named_count { + let name = expr + .blob_str(request.named_assertion_refs[index], "named assertion")? + .to_owned(); + assumptions.push(assertion); + named.push((assertion, name)); + } else { + // Safety: `bz` is a valid, non-null Bitwuzla instance. + unsafe { ffi::bitwuzla_assert(bz, assertion) }; + } + } + for root in &request.assumption_roots { + assumptions.push(translation.bool(*root)?); + } + + let result = check_with_cancellation(bz, &mut assumptions, context, deadline); + match result { + ffi::BITWUZLA_SAT => { + let model = if want_model { + Some(build_model(bz, &translation)?) + } else { + None + }; + Ok(QueryResult::sat(model)) + } + ffi::BITWUZLA_UNSAT => { + let core = if want_core { + Some(build_core(bz, &named)) + } else { + None + }; + Ok(QueryResult::unsat(core)) + } + _ => Ok(QueryResult::unknown("bitwuzla returned unknown".to_owned())), + } +} + +fn optimize( + request: &BinaryRequest, + solver: &BitwuzlaSolver, + context: Option<&SolveContext>, + deadline: BitwuzlaDeadline, +) -> smt_wire::Result { + let expr = request.expression_view()?; + let mut translation = translate(request, solver.tm())?; + let tm = solver.tm(); + let bz = solver.bz(); + let want_model = (request.envelope.flags & request_flags::WANT_MODEL) != 0; + let signed = (request.envelope.flags & request_flags::SIGNED) != 0; + let minimize = request.envelope.command == Command::Minimize; + + // All assertions are hard for optimization; the assumption roots seed the + // per-bit assumption list. + for root in &request.assertion_roots { + // Safety: `bz` is a valid Bitwuzla instance. + unsafe { ffi::bitwuzla_assert(bz, translation.bool(*root)?) }; + } + let mut fixed: Vec = request + .assumption_roots + .iter() + .map(|root| translation.bool(*root)) + .collect::>>()?; + + let result = check_with_cancellation(bz, &mut fixed, context, deadline); + if result == ffi::BITWUZLA_UNSAT { + return Ok(QueryResult::unsat(None)); + } + if result != ffi::BITWUZLA_SAT { + return Ok(QueryResult::unknown("bitwuzla returned unknown".to_owned())); + } + + let target_ref = request + .target_ref() + .ok_or_else(|| WireError::invalid("optimization", "missing target"))?; + let target = translation.bv(target_ref)?; + let width = expr.node(target_ref.index())?.width; + let one_bit = unsafe { ffi::bitwuzla_mk_bv_value_uint64(tm, translation.bv_sort(1), 1) }; + let mut optimum = vec![0u8; (width as usize).div_ceil(8)]; + + for bit in (0..width).rev() { + let prefer_one = match (signed, minimize, bit == width - 1) { + (false, true, _) => false, + (false, false, _) => true, + (true, true, true) => true, + (true, true, false) => false, + (true, false, true) => false, + (true, false, false) => true, + }; + let bit_is_one = { + let extracted = unsafe { + ffi::bitwuzla_mk_term1_indexed2( + tm, + ffi::BITWUZLA_KIND_BV_EXTRACT, + target, + u64::from(bit), + u64::from(bit), + ) + }; + mk2(tm, ffi::BITWUZLA_KIND_EQUAL, extracted, one_bit) + }; + let first_try = if prefer_one { + bit_is_one + } else { + mk1(tm, ffi::BITWUZLA_KIND_NOT, bit_is_one) + }; + fixed.push(first_try); + match check_with_cancellation(bz, &mut fixed, context, deadline) { + ffi::BITWUZLA_SAT => { + if prefer_one { + set_bit(&mut optimum, bit); + } + } + ffi::BITWUZLA_UNSAT => { + let last = fixed.len() - 1; + fixed[last] = if prefer_one { + mk1(tm, ffi::BITWUZLA_KIND_NOT, bit_is_one) + } else { + bit_is_one + }; + if !prefer_one { + set_bit(&mut optimum, bit); + } + } + _ => return Ok(QueryResult::unknown("bitwuzla returned unknown".to_owned())), + } + } + + match check_with_cancellation(bz, &mut fixed, context, deadline) { + ffi::BITWUZLA_SAT => {} + ffi::BITWUZLA_UNSAT => return Ok(QueryResult::unsat(None)), + _ => return Ok(QueryResult::unknown("bitwuzla returned unknown".to_owned())), + } + + let model = if want_model { + Some(build_model(bz, &translation)?) + } else { + None + }; + Ok(QueryResult::sat_optimization(OptimizationValueBlock { + optimum: ScalarValue::bv(width, optimum)?, + model, + })) +} + +fn build_model( + bz: *mut Bitwuzla, + translation: &BitwuzlaTranslation, +) -> smt_wire::Result { + let mut entries = Vec::with_capacity(translation.variables.len()); + for variable in &translation.variables { + let value = match variable.sort { + Sort::Bool => { + let term = translation.bool(variable.node_ref)?; + // Safety: `bz` is valid and model generation is enabled. + let value = unsafe { ffi::bitwuzla_get_value(bz, term) }; + ScalarValue::bool(unsafe { ffi::bitwuzla_term_value_get_bool(value) }) + } + Sort::Bv => { + let term = translation.bv(variable.node_ref)?; + // Safety: `bz` is valid and model generation is enabled. + let value = unsafe { ffi::bitwuzla_get_value(bz, term) }; + bv_model_value(variable.width, value)? + } + }; + entries.push(ModelEntry { + node_ref: variable.node_ref, + value, + }); + } + Ok(ModelBlock { entries }) +} + +/// Maps Bitwuzla's unsat assumptions back to the originating named assertions. +fn build_core(bz: *mut Bitwuzla, named: &[(BitwuzlaTerm, String)]) -> UnsatCoreBlock { + if named.is_empty() { + return UnsatCoreBlock { names: Vec::new() }; + } + let mut size: usize = 0; + // Safety: `bz` is valid and the last check returned UNSAT with unsat-assumption + // tracking enabled. + let ptr = unsafe { ffi::bitwuzla_get_unsat_assumptions(bz, &mut size) }; + let failed: HashSet = if ptr.is_null() || size == 0 { + HashSet::new() + } else { + // Safety: `ptr` points to `size` contiguous `BitwuzlaTerm` values valid + // until the next Bitwuzla call, and we copy them out immediately. + unsafe { std::slice::from_raw_parts(ptr, size) } + .iter() + .copied() + .collect() + }; + let names = named + .iter() + .filter(|(term, _)| failed.contains(term)) + .map(|(_, name)| name.clone()) + .collect(); + UnsatCoreBlock { names } +} + +/// Runs `check_sat` / `check_sat_assuming` with cooperative cancellation. +/// +/// A termination callback is installed that polls a shared `AtomicBool`; a +/// scoped watcher thread sets it when the [`SolveContext`] is cancelled or the +/// budget deadline elapses, prompting Bitwuzla to return `UNKNOWN`. +fn check_with_cancellation( + bz: *mut Bitwuzla, + assumptions: &mut [BitwuzlaTerm], + context: Option<&SolveContext>, + deadline: BitwuzlaDeadline, +) -> ffi::BitwuzlaResult { + if deadline.elapsed() { + return ffi::BITWUZLA_UNKNOWN; + } + let flag = Arc::new(AtomicBool::new(false)); + // Safety: `bz` is valid; the callback only reads through `state`, which + // points at the `AtomicBool` owned by `flag` (alive for this whole call). + unsafe { + ffi::bitwuzla_set_termination_callback( + bz, + Some(term_callback), + Arc::as_ptr(&flag) as *mut std::ffi::c_void, + ); + } + + if context.is_none() && deadline.deadline.is_none() { + return unsafe { run_check(bz, assumptions) }; + } + + let done = Arc::new(AtomicBool::new(false)); + std::thread::scope(|scope| { + let flag = flag.clone(); + let done_w = done.clone(); + scope.spawn(move || { + while !done_w.load(Ordering::Acquire) { + let cancelled = context.is_some_and(|c| c.is_cancelled()) || deadline.elapsed(); + if cancelled { + flag.store(true, Ordering::Release); + } + std::thread::sleep(Duration::from_millis(5)); + } + }); + let result = unsafe { run_check(bz, assumptions) }; + done.store(true, Ordering::Release); + result + }) +} + +unsafe fn run_check(bz: *mut Bitwuzla, assumptions: &mut [BitwuzlaTerm]) -> ffi::BitwuzlaResult { + if assumptions.is_empty() { + ffi::bitwuzla_check_sat(bz) + } else { + ffi::bitwuzla_check_sat_assuming(bz, assumptions.len() as u32, assumptions.as_mut_ptr()) + } +} + +unsafe extern "C" fn term_callback(state: *mut std::ffi::c_void) -> i32 { + if state.is_null() { + return 0; + } + // Safety: `state` points at an `AtomicBool` owned by an `Arc` that outlives + // the `check_sat` call during which this callback runs. + let flag = &*(state as *const AtomicBool); + i32::from(flag.load(Ordering::Acquire)) +} + +fn mk1(tm: *mut BitwuzlaTermManager, kind: ffi::BitwuzlaKind, arg: BitwuzlaTerm) -> BitwuzlaTerm { + unsafe { ffi::bitwuzla_mk_term1(tm, kind, arg) } +} + +fn mk2( + tm: *mut BitwuzlaTermManager, + kind: ffi::BitwuzlaKind, + a: BitwuzlaTerm, + b: BitwuzlaTerm, +) -> BitwuzlaTerm { + unsafe { ffi::bitwuzla_mk_term2(tm, kind, a, b) } +} + +fn mk3( + tm: *mut BitwuzlaTermManager, + kind: ffi::BitwuzlaKind, + a: BitwuzlaTerm, + b: BitwuzlaTerm, + c: BitwuzlaTerm, +) -> BitwuzlaTerm { + unsafe { ffi::bitwuzla_mk_term3(tm, kind, a, b, c) } +} + +fn child_bv( + expr: &ExprView<'_>, + translation: &BitwuzlaTranslation, + node: &RawNode, + offset: u32, +) -> smt_wire::Result { + translation.bv(expr.child_ref(node.children + offset)?) +} + +fn child_bool( + expr: &ExprView<'_>, + translation: &BitwuzlaTranslation, + node: &RawNode, + offset: u32, +) -> smt_wire::Result { + translation.bool(expr.child_ref(node.children + offset)?) +} + +fn child_bv2( + expr: &ExprView<'_>, + translation: &BitwuzlaTranslation, + node: &RawNode, +) -> smt_wire::Result<(BitwuzlaTerm, BitwuzlaTerm)> { + Ok(( + child_bv(expr, translation, node, 0)?, + child_bv(expr, translation, node, 1)?, + )) +} + +fn child_bool2( + expr: &ExprView<'_>, + translation: &BitwuzlaTranslation, + node: &RawNode, +) -> smt_wire::Result<(BitwuzlaTerm, BitwuzlaTerm)> { + Ok(( + child_bool(expr, translation, node, 0)?, + child_bool(expr, translation, node, 1)?, + )) +} + +fn bitwuzla_bv_const( + expr: &ExprView<'_>, + out: &mut BitwuzlaTranslation, + width: u32, + payload: u64, +) -> smt_wire::Result { + let tm = out.tm; + let sort = out.bv_sort(width); + if width <= 64 { + // Safety: `tm` and `sort` are valid. + Ok(unsafe { ffi::bitwuzla_mk_bv_value_uint64(tm, sort, payload) }) + } else { + let bytes = expr.blob_ref(BlobRef::from_payload(payload))?; + // Bitwuzla parses base-2 values MSB-first. + let mut bits = String::with_capacity(width as usize); + for bit in (0..width).rev() { + let byte = bytes[(bit / 8) as usize]; + bits.push(if ((byte >> (bit % 8)) & 1) != 0 { + '1' + } else { + '0' + }); + } + let value = CString::new(bits) + .map_err(|_| WireError::invalid("BV_CONST", "wide constant contains a nul byte"))?; + // Safety: `tm` and `sort` are valid and `value` is a nul-terminated base-2 string. + Ok(unsafe { ffi::bitwuzla_mk_bv_value(tm, sort, value.as_ptr(), 2) }) + } +} + +fn bv_model_value(width: u32, value: BitwuzlaTerm) -> smt_wire::Result { + // Safety: `value` is a model value term with model generation enabled. + let ptr = unsafe { ffi::bitwuzla_term_value_get_str_fmt(value, 2) }; + if ptr.is_null() { + return Err(WireError::invalid( + "bitwuzla model", + "missing BV value string", + )); + } + let text = unsafe { CStr::from_ptr(ptr) } + .to_str() + .map_err(|_| WireError::invalid("bitwuzla model", "non-UTF-8 BV value"))?; + let mut bytes = vec![0u8; (width as usize).div_ceil(8)]; + // The base-2 string is MSB-first, so its reversed enumeration is bit 0 (LSB) up. + for (pos, ch) in text.chars().rev().enumerate() { + if ch == '1' { + set_bit(&mut bytes, pos as u32); + } + } + ScalarValue::bv(width, bytes) +} + +fn set_bit(bytes: &mut [u8], bit: u32) { + bytes[(bit / 8) as usize] |= 1u8 << (bit % 8); +} diff --git a/crates/smt-server/src/bitwuzla_bindings.rs b/crates/smt-server/src/bitwuzla_bindings.rs new file mode 100644 index 0000000..5763cee --- /dev/null +++ b/crates/smt-server/src/bitwuzla_bindings.rs @@ -0,0 +1,174 @@ +//! Hand-written FFI bindings for the official Bitwuzla C API (verified against +//! the 0.9.1 release; `build.rs` fetches it). Checked in rather than bindgen- +//! generated, so the build needs no libclang and the surface is small and +//! version-pinned. The option enum is position-sensitive across releases +//! (`PRODUCE_UNSAT_ASSUMPTIONS` moved 2 -> 3 in 0.9); the `bitwuzla_backend` +//! test is the drift canary when re-pinning. +//! +//! Only symbols used by [`crate::bitwuzla_backend`] are declared. `BitwuzlaTerm` +//! and `BitwuzlaSort` are opaque `u64` handles owned by a `BitwuzlaTermManager`, +//! valid for as long as the manager is alive. + +#![allow( + non_camel_case_types, + non_snake_case, + non_upper_case_globals, + dead_code +)] + +use std::os::raw::c_char; +use std::os::raw::c_void; + +pub type BitwuzlaTermManager = std::ffi::c_void; +pub type BitwuzlaOptions = std::ffi::c_void; +pub type Bitwuzla = std::ffi::c_void; + +pub type BitwuzlaTerm = u64; +pub type BitwuzlaSort = u64; +pub type BitwuzlaResult = std::os::raw::c_uint; +pub type BitwuzlaKind = std::os::raw::c_uint; +pub type BitwuzlaOption = std::os::raw::c_uint; + +// --- check-sat results --------------------------------------------------- + +pub const BITWUZLA_SAT: BitwuzlaResult = 10; +pub const BITWUZLA_UNSAT: BitwuzlaResult = 20; +pub const BITWUZLA_UNKNOWN: BitwuzlaResult = 0; + +// --- options ------------------------------------------------------------- + +pub const BITWUZLA_OPT_PRODUCE_MODELS: BitwuzlaOption = 1; +pub const BITWUZLA_OPT_PRODUCE_UNSAT_ASSUMPTIONS: BitwuzlaOption = 3; + +// --- term kinds ---------------------------------------------------------- +// Boolean connectives. +pub const BITWUZLA_KIND_AND: BitwuzlaKind = 4; +pub const BITWUZLA_KIND_EQUAL: BitwuzlaKind = 6; +pub const BITWUZLA_KIND_IMPLIES: BitwuzlaKind = 8; +pub const BITWUZLA_KIND_NOT: BitwuzlaKind = 9; +pub const BITWUZLA_KIND_OR: BitwuzlaKind = 10; +pub const BITWUZLA_KIND_XOR: BitwuzlaKind = 11; +pub const BITWUZLA_KIND_ITE: BitwuzlaKind = 12; +// Bit-vector operators. +pub const BITWUZLA_KIND_BV_ADD: BitwuzlaKind = 19; +pub const BITWUZLA_KIND_BV_AND: BitwuzlaKind = 20; +pub const BITWUZLA_KIND_BV_ASHR: BitwuzlaKind = 21; +pub const BITWUZLA_KIND_BV_CONCAT: BitwuzlaKind = 23; +pub const BITWUZLA_KIND_BV_MUL: BitwuzlaKind = 26; +pub const BITWUZLA_KIND_BV_NEG: BitwuzlaKind = 28; +pub const BITWUZLA_KIND_BV_NEG_OVERFLOW: BitwuzlaKind = 29; +pub const BITWUZLA_KIND_BV_NOT: BitwuzlaKind = 31; +pub const BITWUZLA_KIND_BV_OR: BitwuzlaKind = 32; +pub const BITWUZLA_KIND_BV_SADD_OVERFLOW: BitwuzlaKind = 38; +pub const BITWUZLA_KIND_BV_SDIV_OVERFLOW: BitwuzlaKind = 39; +pub const BITWUZLA_KIND_BV_SDIV: BitwuzlaKind = 40; +pub const BITWUZLA_KIND_BV_SHL: BitwuzlaKind = 43; +pub const BITWUZLA_KIND_BV_SHR: BitwuzlaKind = 44; +pub const BITWUZLA_KIND_BV_SLE: BitwuzlaKind = 45; +pub const BITWUZLA_KIND_BV_SLT: BitwuzlaKind = 46; +pub const BITWUZLA_KIND_BV_SMOD: BitwuzlaKind = 47; +pub const BITWUZLA_KIND_BV_SMUL_OVERFLOW: BitwuzlaKind = 48; +pub const BITWUZLA_KIND_BV_SREM: BitwuzlaKind = 49; +pub const BITWUZLA_KIND_BV_SSUB_OVERFLOW: BitwuzlaKind = 50; +pub const BITWUZLA_KIND_BV_SUB: BitwuzlaKind = 51; +pub const BITWUZLA_KIND_BV_UADD_OVERFLOW: BitwuzlaKind = 52; +pub const BITWUZLA_KIND_BV_UDIV: BitwuzlaKind = 53; +pub const BITWUZLA_KIND_BV_ULE: BitwuzlaKind = 56; +pub const BITWUZLA_KIND_BV_ULT: BitwuzlaKind = 57; +pub const BITWUZLA_KIND_BV_UMUL_OVERFLOW: BitwuzlaKind = 58; +pub const BITWUZLA_KIND_BV_UREM: BitwuzlaKind = 59; +pub const BITWUZLA_KIND_BV_USUB_OVERFLOW: BitwuzlaKind = 60; +pub const BITWUZLA_KIND_BV_XOR: BitwuzlaKind = 62; +pub const BITWUZLA_KIND_BV_EXTRACT: BitwuzlaKind = 63; +pub const BITWUZLA_KIND_BV_SIGN_EXTEND: BitwuzlaKind = 67; +pub const BITWUZLA_KIND_BV_ZERO_EXTEND: BitwuzlaKind = 68; + +unsafe extern "C" { + pub fn bitwuzla_term_manager_new() -> *mut BitwuzlaTermManager; + pub fn bitwuzla_term_manager_delete(tm: *mut BitwuzlaTermManager); + + pub fn bitwuzla_options_new() -> *mut BitwuzlaOptions; + pub fn bitwuzla_options_delete(options: *mut BitwuzlaOptions); + pub fn bitwuzla_set_option(options: *mut BitwuzlaOptions, option: BitwuzlaOption, val: u64); + + pub fn bitwuzla_new( + tm: *mut BitwuzlaTermManager, + options: *const BitwuzlaOptions, + ) -> *mut Bitwuzla; + pub fn bitwuzla_delete(bitwuzla: *mut Bitwuzla); + + pub fn bitwuzla_set_termination_callback( + bitwuzla: *mut Bitwuzla, + fun: Option i32>, + state: *mut c_void, + ); + + pub fn bitwuzla_assert(bitwuzla: *mut Bitwuzla, term: BitwuzlaTerm); + pub fn bitwuzla_check_sat(bitwuzla: *mut Bitwuzla) -> BitwuzlaResult; + pub fn bitwuzla_check_sat_assuming( + bitwuzla: *mut Bitwuzla, + argc: u32, + args: *mut BitwuzlaTerm, + ) -> BitwuzlaResult; + pub fn bitwuzla_get_value(bitwuzla: *mut Bitwuzla, term: BitwuzlaTerm) -> BitwuzlaTerm; + pub fn bitwuzla_get_unsat_assumptions( + bitwuzla: *mut Bitwuzla, + size: *mut usize, + ) -> *const BitwuzlaTerm; + + pub fn bitwuzla_mk_bool_sort(tm: *mut BitwuzlaTermManager) -> BitwuzlaSort; + pub fn bitwuzla_mk_bv_sort(tm: *mut BitwuzlaTermManager, size: u64) -> BitwuzlaSort; + pub fn bitwuzla_mk_true(tm: *mut BitwuzlaTermManager) -> BitwuzlaTerm; + pub fn bitwuzla_mk_false(tm: *mut BitwuzlaTermManager) -> BitwuzlaTerm; + pub fn bitwuzla_mk_const( + tm: *mut BitwuzlaTermManager, + sort: BitwuzlaSort, + symbol: *const c_char, + ) -> BitwuzlaTerm; + pub fn bitwuzla_mk_bv_value( + tm: *mut BitwuzlaTermManager, + sort: BitwuzlaSort, + value: *const c_char, + base: u8, + ) -> BitwuzlaTerm; + pub fn bitwuzla_mk_bv_value_uint64( + tm: *mut BitwuzlaTermManager, + sort: BitwuzlaSort, + value: u64, + ) -> BitwuzlaTerm; + + pub fn bitwuzla_mk_term1( + tm: *mut BitwuzlaTermManager, + kind: BitwuzlaKind, + arg: BitwuzlaTerm, + ) -> BitwuzlaTerm; + pub fn bitwuzla_mk_term2( + tm: *mut BitwuzlaTermManager, + kind: BitwuzlaKind, + arg0: BitwuzlaTerm, + arg1: BitwuzlaTerm, + ) -> BitwuzlaTerm; + pub fn bitwuzla_mk_term3( + tm: *mut BitwuzlaTermManager, + kind: BitwuzlaKind, + arg0: BitwuzlaTerm, + arg1: BitwuzlaTerm, + arg2: BitwuzlaTerm, + ) -> BitwuzlaTerm; + pub fn bitwuzla_mk_term1_indexed1( + tm: *mut BitwuzlaTermManager, + kind: BitwuzlaKind, + arg: BitwuzlaTerm, + idx: u64, + ) -> BitwuzlaTerm; + pub fn bitwuzla_mk_term1_indexed2( + tm: *mut BitwuzlaTermManager, + kind: BitwuzlaKind, + arg: BitwuzlaTerm, + idx0: u64, + idx1: u64, + ) -> BitwuzlaTerm; + + pub fn bitwuzla_term_value_get_bool(term: BitwuzlaTerm) -> bool; + pub fn bitwuzla_term_value_get_str_fmt(term: BitwuzlaTerm, base: u8) -> *const c_char; +} diff --git a/crates/smt-server/src/lib.rs b/crates/smt-server/src/lib.rs index 87410ce..916c339 100644 --- a/crates/smt-server/src/lib.rs +++ b/crates/smt-server/src/lib.rs @@ -1,11 +1,16 @@ //! Reference server-side implementation for the SMT wire protocol. //! //! The crate provides a small TCP server, binary request handling, native Z3 -//! and binbit solver backends, backend racing, request/response caching, and a +//! and binbit solver backends, an optional Bitwuzla backend (behind the +//! `bitwuzla` feature), backend racing, request/response caching, and a //! compact SMT-LIB frontend. pub mod backend; pub mod binbit_backend; +#[cfg(feature = "bitwuzla")] +pub mod bitwuzla_backend; +#[cfg(feature = "bitwuzla")] +pub mod bitwuzla_bindings; pub mod cache; pub mod command_router; pub mod pool; @@ -21,6 +26,8 @@ pub mod z3_backend; pub use backend::{Backend, CancellationToken, QueryResult, QueryStatus, SolveContext}; pub use binbit_backend::BinbitBackend; +#[cfg(feature = "bitwuzla")] +pub use bitwuzla_backend::BitwuzlaBackend; pub use cache::{cache_key_for_payload, rebind_cached_response, CacheStats, ResponseCache}; pub use command_router::CommandRouterBackend; pub use pool::PooledBackend; diff --git a/crates/smt-server/src/main.rs b/crates/smt-server/src/main.rs index 3df090b..266b048 100644 --- a/crates/smt-server/src/main.rs +++ b/crates/smt-server/src/main.rs @@ -1,8 +1,10 @@ use std::path::PathBuf; use std::sync::Arc; +#[cfg(feature = "bitwuzla")] +use smt_server::BitwuzlaBackend; use smt_server::{ - default_legacy_recording_tree, migrate_recording_tree, recording_db_path, serve_tcp, + default_legacy_recording_tree, migrate_recording_tree, recording_db_path, serve_tcp, Backend, BinbitBackend, CommandRouterBackend, QfbvsmtrsBackend, RacingBackend, RumbaBackend, ServerConfig, Z3Backend, }; @@ -15,17 +17,23 @@ fn main() -> std::io::Result<()> { return Ok(()); } let addr = arg.unwrap_or_else(|| "127.0.0.1:9123".to_owned()); - let solver = Arc::new( - RacingBackend::new(vec![ - Arc::new(Z3Backend), - Arc::new(BinbitBackend), - Arc::new(QfbvsmtrsBackend), - ]) - .with_default_budget_ms(30_000), - ); + #[cfg_attr(not(feature = "bitwuzla"), allow(unused_mut))] + let mut racers: Vec> = vec![ + Arc::new(Z3Backend), + Arc::new(BinbitBackend), + Arc::new(QfbvsmtrsBackend), + ]; + #[cfg(feature = "bitwuzla")] + racers.push(Arc::new(BitwuzlaBackend)); + let solver = Arc::new(RacingBackend::new(racers).with_default_budget_ms(30_000)); let backend = Arc::new(CommandRouterBackend::new(Arc::new(RumbaBackend), solver)); eprintln!( - "smt-server listening on {addr} with rumba simplifier + racing solver (z3 crate + binbit + qfbvsmtrs)" + "smt-server listening on {addr} with rumba simplifier + racing solver (z3 crate + binbit + qfbvsmtrs{})", + if cfg!(feature = "bitwuzla") { + " + bitwuzla" + } else { + "" + } ); serve_tcp(addr, ServerConfig::new(backend)) } From 32b9b6d87a7418cae47f48f122868ec4d986e6e5 Mon Sep 17 00:00:00 2001 From: Brit Date: Mon, 29 Jun 2026 14:51:13 +0200 Subject: [PATCH 2/5] build(bitwuzla): fetch and link prebuilt static archive build.rs fetches an upstream prebuilt Bitwuzla static zip per target triple (Linux/macOS/Windows-gnu) and a self-contained MSVC archive from the bitwuzla-msvc fork; resolves GMP/MPFR via pkg-config (upstream) or ships them statically (MSVC). --- crates/smt-server/build.rs | 337 ++++++++++++++++++ .../vendor/bitwuzla-msvc/.gitignore | 2 + .../smt-server/vendor/bitwuzla-msvc/README.md | 106 ++++++ .../bitwuzla-msvc/bitwuzla-0.9.1-msvc.patch | 48 +++ .../smt-server/vendor/bitwuzla-msvc/build.bat | 110 ++++++ .../vendor/bitwuzla-msvc/shim/msvc_compat.h | 84 +++++ .../vendor/bitwuzla-msvc/shim/unistd.h | 70 ++++ 7 files changed, 757 insertions(+) create mode 100644 crates/smt-server/build.rs create mode 100644 crates/smt-server/vendor/bitwuzla-msvc/.gitignore create mode 100644 crates/smt-server/vendor/bitwuzla-msvc/README.md create mode 100644 crates/smt-server/vendor/bitwuzla-msvc/bitwuzla-0.9.1-msvc.patch create mode 100644 crates/smt-server/vendor/bitwuzla-msvc/build.bat create mode 100644 crates/smt-server/vendor/bitwuzla-msvc/shim/msvc_compat.h create mode 100644 crates/smt-server/vendor/bitwuzla-msvc/shim/unistd.h diff --git a/crates/smt-server/build.rs b/crates/smt-server/build.rs new file mode 100644 index 0000000..6e7daec --- /dev/null +++ b/crates/smt-server/build.rs @@ -0,0 +1,337 @@ +// Links Bitwuzla by fetching a prebuilt static archive at build time (like the +// `z3` crate's `gh-release` feature). FFI bindings are hand-written and checked +// in (`src/bitwuzla_bindings.rs`, pinned to 0.9.1), so this script only emits +// link directives. +// +// Linux/macOS/Windows-gnu fetch the upstream Bitwuzla release (GMP/MPFR via +// pkg-config). Windows-msvc fetches a self-contained MSVC archive (static +// GMP/MPFR, no DLLs) from the bitwuzla-msvc fork, since upstream ships only +// MinGW. Release layouts vary, so we search the extracted tree for +// `libbitwuzla.a`. + +#[cfg(feature = "bitwuzla")] +fn main() { + if let Err(err) = bitwuzla::link() { + eprintln!("error: {err}"); + std::process::exit(1); + } +} + +#[cfg(not(feature = "bitwuzla"))] +fn main() {} + +#[cfg(feature = "bitwuzla")] +mod bitwuzla { + use std::env; + use std::fmt::Write as _; + use std::path::{Path, PathBuf}; + use std::process::Command; + + /// Bitwuzla release tag the upstream prebuilt archives are fetched from. + /// Bump this and re-verify the constants in `src/bitwuzla_bindings.rs` (the + /// `bitwuzla_backend` test is the drift canary). Keep `MSVC_TAG` in sync. + const BITWUZLA_VERSION: &str = "0.9.1"; + const UPSTREAM_BASE: &str = "https://github.com/bitwuzla/bitwuzla/releases/download"; + + /// The MSVC static archive is rebuilt from the 0.9.1 source under `cl.exe` + /// and published on the bitwuzla-msvc fork's GitHub release, with GMP/MPFR baked in + /// statically so the linked Rust binary has no extra DLL dependencies. + const MSVC_TAG: &str = "bitwuzla-msvc-0.9.1"; + const MSVC_ASSET: &str = "Bitwuzla-Win64-x86_64-msvc-static"; + const MSVC_RELEASE_BASE: &str = "https://github.com/LLVMParty/bitwuzla-msvc/releases/download"; + + /// How GMP/MPFR are resolved for a fetched archive. + enum Flavor { + /// Upstream prebuilt; GMP/MPFR resolved via pkg-config on the host. + PkgConfig, + /// Self-contained archive shipping statically-linked GMP/MPFR (MSVC). + StaticShipped, + } + + struct TargetSpec { + /// Asset name (also the top-level dir inside the zip). + asset: &'static str, + /// GitHub release download base URL. + release_base: &'static str, + /// Release tag the asset lives under. + tag: &'static str, + flavor: Flavor, + } + + /// Map the cargo target to the archive to fetch. `Err` for unsupported + /// targets. + fn target_spec() -> Result { + let os = env::var("CARGO_CFG_TARGET_OS").unwrap_or_default(); + let arch = env::var("CARGO_CFG_TARGET_ARCH").unwrap_or_default(); + let env_ = env::var("CARGO_CFG_TARGET_ENV").unwrap_or_default(); + let upstream = |asset: &'static str| TargetSpec { + asset, + release_base: UPSTREAM_BASE, + tag: BITWUZLA_VERSION, + flavor: Flavor::PkgConfig, + }; + match (os.as_str(), arch.as_str(), env_.as_str()) { + ("linux", "x86_64", _) => Ok(upstream("Bitwuzla-Linux-x86_64-static")), + ("linux", "aarch64", _) => Ok(upstream("Bitwuzla-Linux-arm64-static")), + ("macos", "aarch64", _) => Ok(upstream("Bitwuzla-macOS-arm64-static")), + ("windows", "x86_64", "gnu") => Ok(upstream("Bitwuzla-Win64-x86_64-static")), + ("windows", "x86_64", "msvc") => Ok(TargetSpec { + asset: MSVC_ASSET, + release_base: MSVC_RELEASE_BASE, + tag: MSVC_TAG, + flavor: Flavor::StaticShipped, + }), + _ => Err(format!( + "the `bitwuzla` feature has no prebuilt Bitwuzla static archive for \ + target `{os}-{arch}-{env_}`. Supported: x86_64/aarch64 Linux (gnu), \ + aarch64 macOS, x86_64 Windows (gnu and msvc targets)." + )), + } + } + + pub fn link() -> Result<(), String> { + // vcpkg's `mpfr.lib` duplicates two GMP members (mp_clz_tab.obj, + // version.obj) also in `gmp.lib`; MSVC link.exe warns LNK4255 on the + // duplicate name. Both are read-only GMP data and only one is pulled, + // so it's cosmetic -- silenced here (stripping at packaging would rebuild + // each archive's symbol table for no gain). + if env::var("CARGO_CFG_TARGET_ENV").unwrap_or_default() == "msvc" { + println!("cargo:rustc-link-arg=/IGNORE:4255"); + } + // Dev/testing escape hatch: link a locally-built Bitwuzla static tree + // (e.g. an MSVC `libbitwuzla.a` built from source) instead of fetching + // the release archive. The dir must hold the Bitwuzla archives; GMP/MPFR + // are still resolved via pkg-config below. + if let Ok(dir) = env::var("BITWUZLA_LIB_DIR") { + return link_local(&PathBuf::from(dir)); + } + let spec = target_spec()?; + let out_dir = PathBuf::from(env::var_os("OUT_DIR").ok_or("OUT_DIR not set")?); + let cache_dir = out_dir.join("bitwuzla-prebuilt"); + std::fs::create_dir_all(&cache_dir).map_err(|e| format!("create cache dir: {e}"))?; + let zip_path = cache_dir.join(format!("{}.zip", spec.asset)); + let marker = cache_dir.join(format!("{}.ok", spec.asset)); + let extract_root = cache_dir.join(spec.asset); + + let lib_dir = match find_lib_dir(&extract_root) { + Some(d) => d, + None => { + download(&spec, &zip_path)?; + extract(&zip_path, &extract_root)?; + match find_lib_dir(&extract_root) { + Some(d) => { + std::fs::write(&marker, b"ok").map_err(|e| format!("write marker: {e}"))?; + d + } + None => { + let mut msg = format!( + "extracted {}.zip but `libbitwuzla.a` was not found; extracted tree:\n", + spec.asset + ); + list_tree(&extract_root, &mut msg); + return Err(msg); + } + } + } + }; + + match spec.flavor { + Flavor::PkgConfig => link_pkgconfig(&lib_dir), + Flavor::StaticShipped => link_static_shipped(&lib_dir), + }?; + println!("cargo:rerun-if-changed=build.rs"); + Ok(()) + } + + /// Upstream prebuilt: link the four Bitwuzla archives and resolve GMP/MPFR + /// via pkg-config. Mirrors upstream `bitwuzla.pc`. + fn link_pkgconfig(lib_dir: &Path) -> Result<(), String> { + println!("cargo:rustc-link-search=native={}", lib_dir.display()); + // Dependency order: main archive before its sub-libraries, then + // GMP/MPFR, then psapi (Windows only). + for lib in ["bitwuzla", "bitwuzlals", "bitwuzlabv", "bitwuzlabb"] { + println!("cargo:rustc-link-lib=static={lib}"); + } + for (dep, ver) in [("gmp", "6.3"), ("mpfr", "4.2.1")] { + pkg_config::Config::new() + .atleast_version(ver) + .probe(dep) + .map_err(|e| { + format!( + "failed to locate {dep} >= {ver} via pkg-config: {e}\n\ + Bitwuzla's static archive needs GMP and MPFR. Install them, e.g.:\n \ + apt install libgmp-dev libmpfr-dev | brew install gmp mpfr | \ + MSYS2: pacman -S mingw-w64-x86_64-gmp mingw-w64-x86_64-mpfr" + ) + })?; + } + if env::var("CARGO_CFG_TARGET_OS").unwrap_or_default() == "windows" { + println!("cargo:rustc-link-lib=psapi"); + } + Ok(()) + } + + /// MSVC self-contained archive: link the six Bitwuzla archives plus the + /// statically-linked GMP/MPFR shipped inside the zip (no pkg-config, + /// no DLL dependencies at runtime). + fn link_static_shipped(lib_dir: &Path) -> Result<(), String> { + println!("cargo:rustc-link-search=native={}", lib_dir.display()); + // Dependency order: Bitwuzla archives before their GMP/MPFR deps, then + // psapi (Windows process/memory info used by cadical). + for lib in [ + "bitwuzla", + "bitwuzlals", + "bitwuzlabv", + "bitwuzlabb", + "bzlarng", + "bzlautil", + "gmp", + "mpfr", + ] { + println!("cargo:rustc-link-lib=static={lib}"); + } + println!("cargo:rustc-link-lib=psapi"); + Ok(()) + } + + /// Link a locally-built Bitwuzla static tree (the `BITWUZLA_LIB_DIR` escape + /// hatch). The directory must contain the Bitwuzla static archives produced + /// by an upstream build (`libbitwuzla.a`, `libbitwuzlals.a`, + /// `libbitwuzlabv.a`, `libbitwuzlabb.a`, `libbzlarng.a`, `libbzlautil.a`). + /// GMP/MPFR are located via pkg-config, exactly as for the fetched archive. + fn link_local(lib_dir: &Path) -> Result<(), String> { + if !lib_dir.join("libbitwuzla.a").exists() { + return Err(format!( + "BITWUZLA_LIB_DIR={} does not contain `libbitwuzla.a`", + lib_dir.display() + )); + } + println!("cargo:rustc-link-search=native={}", lib_dir.display()); + // Upstream's from-source layout splits the archives across the root + // and a `lib/` subdir (`libbitwuzla.a` + `libbzlautil.a` at the root, + // the rest under `lib/`). Add both so all archives resolve. + let support_dir = lib_dir.join("lib"); + if support_dir.is_dir() { + println!("cargo:rustc-link-search=native={}", support_dir.display()); + } + // Dependency order: the main archive before its sub-libraries, then the + // RNG/util support libs, then GMP/MPFR, then psapi (Windows only). + for lib in [ + "bitwuzla", + "bitwuzlals", + "bitwuzlabv", + "bitwuzlabb", + "bzlarng", + "bzlautil", + ] { + println!("cargo:rustc-link-lib=static={lib}"); + } + for (dep, ver) in [("gmp", "6.3"), ("mpfr", "4.2.1")] { + pkg_config::Config::new() + .atleast_version(ver) + .probe(dep) + .map_err(|e| { + format!( + "failed to locate {dep} >= {ver} via pkg-config: {e}\n\ + Bitwuzla's static archive needs GMP and MPFR. Install them, e.g.:\n \ + apt install libgmp-dev libmpfr-dev | brew install gmp mpfr | \ + vcpkg install gmp mpfr (Windows MSVC)" + ) + })?; + } + if env::var("CARGO_CFG_TARGET_OS").unwrap_or_default() == "windows" { + println!("cargo:rustc-link-lib=psapi"); + } + println!("cargo:rerun-if-changed=build.rs"); + println!("cargo:rerun-if-env-changed=BITWUZLA_LIB_DIR"); + Ok(()) + } + + /// Recursively locate the directory containing `libbitwuzla.a` (handles the + /// `lib/` and `lib//` layouts the release packages use). + fn find_lib_dir(root: &Path) -> Option { + if root.join("libbitwuzla.a").exists() { + return Some(root.to_path_buf()); + } + for entry in std::fs::read_dir(root).ok()?.flatten() { + let p = entry.path(); + if p.is_dir() { + if let Some(d) = find_lib_dir(&p) { + return Some(d); + } + } + } + None + } + + fn download(spec: &TargetSpec, dest: &Path) -> Result<(), String> { + let url = format!("{}/{}/{}.zip", spec.release_base, spec.tag, spec.asset); + let mut cmd = Command::new("curl"); + cmd.arg("-fsSL") + .arg("--retry") + .arg("3") + .arg("--retry-delay") + .arg("2"); + // Authenticated read-only requests avoid 403s/rate-limits on CI runners. + if let Ok(tok) = env::var("READ_ONLY_GITHUB_TOKEN") { + if !tok.is_empty() { + cmd.arg("-H").arg(format!("Authorization: Bearer {tok}")); + } + } + cmd.arg("-o").arg(dest).arg(&url); + let status = cmd.status().map_err(|e| { + format!( + "failed to run curl: {e}\n\ + the `bitwuzla` feature downloads a prebuilt archive at build time; \ + curl must be on PATH." + ) + })?; + if !status.success() { + return Err(format!("curl exited {status} fetching {url}")); + } + Ok(()) + } + + fn extract(zip: &Path, dest: &Path) -> Result<(), String> { + std::fs::create_dir_all(dest).map_err(|e| format!("create extract dir: {e}"))?; + // Build.rs runs on the host: `unzip` on Unix, `tar` on Windows (bsdtar, + // shipped with Windows 10+, handles zip). Both exist in CI and dev shells. + let status = if cfg!(windows) { + Command::new("tar") + .arg("-xf") + .arg(zip) + .arg("-C") + .arg(dest) + .status() + } else { + Command::new("unzip") + .arg("-oq") + .arg(zip) + .arg("-d") + .arg(dest) + .status() + } + .map_err(|e| format!("failed to run extractor: {e}"))?; + if !status.success() { + return Err(format!( + "extractor exited {status} extracting {}", + zip.display() + )); + } + Ok(()) + } + + fn list_tree(root: &Path, out: &mut String) { + let Ok(entries) = std::fs::read_dir(root) else { + return; + }; + for entry in entries.flatten() { + let p = entry.path(); + let rel = p.strip_prefix(root).unwrap_or(&p).display(); + let _ = writeln!(out, " {rel}"); + if p.is_dir() { + list_tree(&p, out); + } + } + } +} diff --git a/crates/smt-server/vendor/bitwuzla-msvc/.gitignore b/crates/smt-server/vendor/bitwuzla-msvc/.gitignore new file mode 100644 index 0000000..e1ee496 --- /dev/null +++ b/crates/smt-server/vendor/bitwuzla-msvc/.gitignore @@ -0,0 +1,2 @@ +/work/ +*.zip diff --git a/crates/smt-server/vendor/bitwuzla-msvc/README.md b/crates/smt-server/vendor/bitwuzla-msvc/README.md new file mode 100644 index 0000000..606b056 --- /dev/null +++ b/crates/smt-server/vendor/bitwuzla-msvc/README.md @@ -0,0 +1,106 @@ +# Bitwuzla MSVC static build + +Reproducible recipe that builds the **self-contained MSVC static Bitwuzla +archive** consumed by `crates/smt-server/build.rs` for the +`x86_64-pc-windows-msvc` target, and publishes it as a GitHub release asset. + +Upstream Bitwuzla ships only a MinGW (GCC) Windows build, whose GNU object +archive MSVC's linker cannot consume. This package rebuilds Bitwuzla 0.9.1 from +source under `cl.exe`, with GMP/MPFR **statically linked in** (vcpkg +`x64-windows-static-md` triplet: static lib + dynamic CRT), so the linked Rust +binary has no GMP/MPFR DLL dependencies and no CRT mismatch. + +## Contents + +| File | Purpose | +|------|---------| +| `build.bat` | One-shot driver: vcpkg install → clone 0.9.1 → patch → meson → ninja → zip. | +| `bitwuzla-0.9.1-msvc.patch` | The source patches required for `cl.exe` (unified diff vs tag `0.9.1`). | +| `shim/msvc_compat.h` | GCC-ism polyfills (`__attribute__`, `__builtin_*`), force-included (`/FI`). | +| `shim/unistd.h` | Minimal POSIX `` → MSVC CRT shim. | + +## Prerequisites + +- Visual Studio 2022 (`cl.exe`; `vcvars64.bat` is located automatically via + `vswhere`). +- `meson` (>=1.4), `ninja`, `git`, `python3` on `PATH`. +- vcpkg (pass its root as the first argument; defaults to `F:\Repos\vcpkg`). + +## Build + +```bat +build.bat [VCPKG_DIR] [WORK_DIR] +``` + +- `VCPKG_DIR` — vcpkg root (default `F:\Repos\vcpkg`). +- `WORK_DIR` — where bitwuzla is cloned & built (default `.\work`). + +Output: `\Bitwuzla-Win64-x86_64-msvc-static.zip` — a zip whose +top-level dir `Bitwuzla-Win64-x86_64-msvc-static/lib/` holds the six Bitwuzla +archives plus `gmp.lib`/`mpfr.lib`. + +## Publish + +The asset name and release tag **must** match `build.rs` (`MSVC_ASSET` / +`MSVC_TAG`): + +```sh +gh release create bitwuzla-msvc-0.9.1 \ + --repo LLVMParty/smt-server \ + --title "Bitwuzla MSVC static 0.9.1" \ + --notes "Self-contained MSVC static Bitwuzla 0.9.1 (GMP/MPFR statically linked)." \ + /Bitwuzla-Win64-x86_64-msvc-static.zip +``` + +`build.rs` then fetches +`https://github.com/LLVMParty/smt-server/releases/download/bitwuzla-msvc-0.9.1/Bitwuzla-Win64-x86_64-msvc-static.zip` +for the `msvc` target. + +## Recipe summary + +1. `vcpkg install gmp mpfr --triplet x64-windows-static-md` (static lib, dynamic + CRT → `__GMP_LIBGMP_DLL=0` in `gmp.h`, so objects emit direct `__gmpz_*` / + `mpfr_*` symbols linkable into a static archive — no `__imp_` import stubs). +2. Clone `bitwuzla` tag `0.9.1`; `git apply bitwuzla-0.9.1-msvc.patch`. +3. `meson setup --default-library=static` with + `CFLAGS=CXXFLAGS=/D__WIN32 /I /FImsvc_compat.h` (activates cadical's + Windows code paths and injects the GCC-ism polyfills) and + `PKG_CONFIG_PATH` pointing at the static-md triplet. +4. `ninja` the six archives. +5. Stage the six `.a` + `gmp.lib` + `mpfr.lib` into `lib/` and zip. + +The three source patches: `src/util/integer.h` adds `#include `; +`src/main/time_limit.cpp` adds `#include ` and guards the glibc<2.34 +pthread condvar workaround behind `#ifndef _MSC_VER`. + +## Known MSVC test-suite limitations (unused by the backend) + +The full upstream regression suite (`meson test -C build … -Dtesting=enabled`, +4200 tests) passes **~4150–4160 / 4200** on this VS 2022 (`cl` 19.44) build. +The exact failure count is **non-deterministic** (observed 37–49 distinct +failing tests across runs): the underlying defect is heap memory corruption +whose manifestation depends on allocation layout. Every failure falls in one +of two code paths that `BitwuzlaBackend` never exercises: + +- **Interpolant generation** (`get-interpolant_*`, ~36–39 tests) — + non-deterministic memory corruption. The same input either completes cleanly + (~190 B of valid output) or crashes with `0xC0000005` (access violation), + first emitting 83 B–628 KB of varying non-UTF-8 garbage to stdout. Triggered + by `(set-option :produce-interpolants true)` + `(get-interpolant …)`. + Root-causing the exact UAF/OOB needs an AddressSanitizer build; deferred. +- **Letified SMT-LIB printer** (`printer_nested_letify`, 1–2 test invocations) + — two failure modes. (1) The same non-deterministic `0xC0000005` crash + + garbage as above, in `smt2_printer.cpp`'s `letify()` traversal. (2) When it + does *not* crash, a **deterministic** logic bug: the letify traversal drops + the repeated 2nd occurrence of a subterm, emitting malformed output with no + `let` bindings — e.g. `(bvmul X)` with one argument instead of + `(bvmul X X)`, vs. the expected `(let ((_let1 …)) (bvmul _let1 _let1))`. + +Every path the backend uses **passes**: `solver_*`, `solver_bv_*`, +`get-model_*`, `get-value_*`, `get-unsat-core_*`, `get-unsat-assumptions_*`, +`rewrite_*`, `preprocess_*`, fp, array. `BitwuzlaBackend` does QF_BV solve / +model extraction / named unsat cores / bit-hunt optimization via the C API — it +never sets `PRODUCE_INTERPOLANTS`, calls no `get-interpolant*` symbol, and its +only string output is `bitwuzla_term_value_get_str_fmt` (a value-constant +formatter that bypasses the SMT-LIB printer) — so these failures do not affect +it. diff --git a/crates/smt-server/vendor/bitwuzla-msvc/bitwuzla-0.9.1-msvc.patch b/crates/smt-server/vendor/bitwuzla-msvc/bitwuzla-0.9.1-msvc.patch new file mode 100644 index 0000000..f684425 --- /dev/null +++ b/crates/smt-server/vendor/bitwuzla-msvc/bitwuzla-0.9.1-msvc.patch @@ -0,0 +1,48 @@ +diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp +index 656b10a..e517cd1 100644 +--- a/src/main/time_limit.cpp ++++ b/src/main/time_limit.cpp +@@ -1,11 +1,14 @@ + #include "main/time_limit.h" + +-#include // Required for workaround ++#ifndef _MSC_VER ++#include // glibc <2.34 condvar workaround; irrelevant on Windows ++#endif + + #include + #include + #include + #include ++#include + + #include "bitwuzla/cpp/parser.h" + +@@ -13,6 +16,7 @@ namespace bzla::main { + + // Workaround for condition variables in glibc < 2.34 to avoid segfault before + // exiting: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=58909 ++#ifndef _MSC_VER + void + pthread_cond_var_bug_workaround() + { +@@ -26,6 +30,7 @@ pthread_cond_var_bug_workaround() + pthread_cond_timedwait(&c, &mt, &ts); + pthread_cond_wait(&c, &mt); + } ++#endif + + using namespace std::chrono_literals; + +diff --git a/src/util/integer.h b/src/util/integer.h +index 0843adc..a45d56c 100644 +--- a/src/util/integer.h ++++ b/src/util/integer.h +@@ -15,6 +15,7 @@ + + #include + #include ++#include + + namespace bzla::util { + diff --git a/crates/smt-server/vendor/bitwuzla-msvc/build.bat b/crates/smt-server/vendor/bitwuzla-msvc/build.bat new file mode 100644 index 0000000..ec8e0ef --- /dev/null +++ b/crates/smt-server/vendor/bitwuzla-msvc/build.bat @@ -0,0 +1,110 @@ +@echo off +setlocal enableextensions enabledelayedexpansion +rem ============================================================================ +rem Reproducible build of the self-contained MSVC static Bitwuzla archive that +rem crates/smt-server/build.rs fetches for the x86_64-pc-windows-msvc target. +rem +rem Output: %WORK_DIR%\Bitwuzla-Win64-x86_64-msvc-static.zip +rem Publish it to https://github.com/LLVMParty/smt-server/releases under tag +rem bitwuzla-msvc-0.9.1 (asset name must be exactly +rem Bitwuzla-Win64-x86_64-msvc-static.zip -- matches MSVC_ASSET in build.rs). +rem +rem Prereqs (on PATH, or located automatically): +rem * Visual Studio 2022 (cl.exe 19.4x; vcvars64.bat is searched for under +rem C:\Program Files\Microsoft Visual Studio\2022\\). VS 2022 is +rem required: the shim is validated on cl 19.44, and VS 18's cl 19.5x +rem declares __builtin_fmaf as a native intrinsic that conflicts with the +rem shim's polyfill. Override the path with the VCVARS env var if needed. +rem * meson (>=1.4), ninja, git, python3 +rem * vcpkg (pass its root as %1, default F:\Repos\vcpkg) +rem +rem Usage: +rem build.bat [VCPKG_DIR] [WORK_DIR] +rem VCPKG_DIR default F:\Repos\vcpkg +rem WORK_DIR default %~dp0work (clones bitwuzla here, builds here) +rem +rem NOTE: the vcpkg root is held in %VCPKG% (not VCPKG_ROOT) because +rem vcvars64.bat overwrites VCPKG_ROOT. --vcpkg-root forces it on every call. +rem ============================================================================ +set "VCPKG=%~1" +if "%VCPKG%"=="" set "VCPKG=F:\Repos\vcpkg" +set "WORK_DIR=%~2" +if "%WORK_DIR%"=="" set "WORK_DIR=%~dp0work" +set "SHIM_DIR=%~dp0shim" +set "PATCH=%~dp0bitwuzla-0.9.1-msvc.patch" +set "BITWUZLA_TAG=0.9.1" +set "TRIPLET=x64-windows-static-md" +set "ASSET=Bitwuzla-Win64-x86_64-msvc-static" + +if not exist "%VCPKG%\vcpkg.exe" (echo ERROR: vcpkg.exe not found at !VCPKG! & exit /b 1) +where meson >nul 2>&1 || (echo ERROR: meson not on PATH & exit /b 1) +where ninja >nul 2>&1 || (echo ERROR: ninja not on PATH & exit /b 1) +where git >nul 2>&1 || (echo ERROR: git not on PATH & exit /b 1) + +rem --- locate VS 2022's vcvars64.bat (try standard editions; VCVARS overrides) --- +if not defined VCVARS goto :find_vcvars +call "%VCVARS%" >nul +if errorlevel 1 (echo ERROR: vcvars failed & exit /b 1) +goto :vcvars_done +:find_vcvars +set "VCVARS=" +for %%E in (Enterprise Professional Community BuildTools) do if exist "C:\Program Files\Microsoft Visual Studio\2022\%%E\VC\Auxiliary\Build\vcvars64.bat" set "VCVARS=C:\Program Files\Microsoft Visual Studio\2022\%%E\VC\Auxiliary\Build\vcvars64.bat" +if not defined VCVARS (echo ERROR: VS 2022 vcvars64.bat not found. Set the VCVARS env var to its path. & exit /b 1) +call "%VCVARS%" >nul +if errorlevel 1 (echo ERROR: vcvars failed & exit /b 1) +:vcvars_done + +rem --- vcpkg: static-md GMP/MPFR (static lib, dynamic CRT -> matches Rust /MD, +rem no CRT mismatch, no GMP/MPFR DLL deps) + pkgconf host tool --- +echo === vcpkg: gmp mpfr (%TRIPLET%) + pkgconf === +"%VCPKG%\vcpkg.exe" --vcpkg-root "%VCPKG%" install gmp mpfr --triplet %TRIPLET% || exit /b 1 +"%VCPKG%\vcpkg.exe" --vcpkg-root "%VCPKG%" install pkgconf --triplet x64-windows || exit /b 1 +set "VCPKG_INST=%VCPKG%\installed\%TRIPLET%" +set "VCPKG_TOOLS=%VCPKG%\installed\x64-windows\tools\pkgconf" +if not exist "%VCPKG_TOOLS%\pkg-config.exe" copy /y "%VCPKG_TOOLS%\pkgconf.exe" "%VCPKG_TOOLS%\pkg-config.exe" >nul +set "PKG_CONFIG_PATH=%VCPKG_INST%\lib\pkgconfig" +set "PKG_CONFIG=%VCPKG_TOOLS%\pkg-config.exe" +set "PATH=%VCPKG_TOOLS%;%PATH%" + +rem --- clone bitwuzla 0.9.1 + apply patch --- +if not exist "%WORK_DIR%\bitwuzla-src\.git" ( + echo === clone bitwuzla %BITWUZLA_TAG% === + git clone --depth 1 --branch %BITWUZLA_TAG% https://github.com/bitwuzla/bitwuzla "%WORK_DIR%\bitwuzla-src" || exit /b 1 +) +pushd "%WORK_DIR%\bitwuzla-src" +git checkout -- . 2>nul +echo === apply patch === +git apply --check "%PATCH%" 2>nul && (git apply "%PATCH%" || (popd & exit /b 1)) || echo patch already applied +popd + +rem --- meson setup + ninja (the 6 static archives, skip the CLI) --- +set "SHIMFLAGS=/D__WIN32 /I%SHIM_DIR% /FImsvc_compat.h" +set "CFLAGS=%SHIMFLAGS%" +set "CXXFLAGS=%SHIMFLAGS%" +pushd "%WORK_DIR%\bitwuzla-src" +if exist build_msvc rmdir /s /q build_msvc +echo === meson setup === +meson setup build_msvc --default-library=static -Dpython=false -Dtesting=disabled -Dunit_testing=disabled || (popd & exit /b 1) +echo === ninja (6 archives) === +ninja -C build_msvc src/libbitwuzla.a src/libbzlautil.a src/lib/libbitwuzlals.a src/lib/libbitwuzlabv.a src/lib/libbitwuzlabb.a src/lib/libbzlarng.a || (popd & exit /b 1) +popd + +rem --- assemble the self-contained zip --- +set "STAGE=%WORK_DIR%\%ASSET%" +if exist "%STAGE%" rmdir /s /q "%STAGE%" +mkdir "%STAGE%\lib" +copy /y "%WORK_DIR%\bitwuzla-src\build_msvc\src\libbitwuzla.a" "%STAGE%\lib\" >nul +copy /y "%WORK_DIR%\bitwuzla-src\build_msvc\src\libbzlautil.a" "%STAGE%\lib\" >nul +copy /y "%WORK_DIR%\bitwuzla-src\build_msvc\src\lib\libbitwuzlals.a" "%STAGE%\lib\" >nul +copy /y "%WORK_DIR%\bitwuzla-src\build_msvc\src\lib\libbitwuzlabv.a" "%STAGE%\lib\" >nul +copy /y "%WORK_DIR%\bitwuzla-src\build_msvc\src\lib\libbitwuzlabb.a" "%STAGE%\lib\" >nul +copy /y "%WORK_DIR%\bitwuzla-src\build_msvc\src\lib\libbzlarng.a" "%STAGE%\lib\" >nul +copy /y "%VCPKG_INST%\lib\gmp.lib" "%STAGE%\lib\" >nul +copy /y "%VCPKG_INST%\lib\mpfr.lib" "%STAGE%\lib\" >nul +set "ZIP=%WORK_DIR%\%ASSET%.zip" +if exist "%ZIP%" del "%ZIP%" +pushd "%WORK_DIR%" +tar -caf "%ASSET%.zip" "%ASSET%" +popd +echo === DONE: %ZIP% === +dir "%ZIP%" diff --git a/crates/smt-server/vendor/bitwuzla-msvc/shim/msvc_compat.h b/crates/smt-server/vendor/bitwuzla-msvc/shim/msvc_compat.h new file mode 100644 index 0000000..5069cdc --- /dev/null +++ b/crates/smt-server/vendor/bitwuzla-msvc/shim/msvc_compat.h @@ -0,0 +1,84 @@ +#pragma once +/* + * GCC-ism polyfills for building cadical, symfpu, and bitwuzla with MSVC. + * Force-included (/FI) before any project header. + */ +#ifdef _MSC_VER + +/* GCC's __PRETTY_FUNCTION__ -> MSVC's __FUNCSIG__ (full signature string). */ +#ifndef __PRETTY_FUNCTION__ +#define __PRETTY_FUNCTION__ __FUNCSIG__ +#endif +/* cadical uses __attribute__ only for compile-time annotations + * (format-string checking; a .preinit_array section in mobical which is not + * built here). Dropping them is safe. */ +#ifndef __attribute__ +#define __attribute__(A) +#endif + +#include +#include + +#define __builtin_expect(c, v) (c) +#define __builtin_unreachable() __assume(0) + +static __forceinline void +__builtin_prefetch(const void *p, int rw, int locality) +{ + (void)rw; + (void)locality; + _mm_prefetch((const char *)p, _MM_HINT_T0); +} + +static __forceinline int +__builtin_clz(unsigned x) +{ + unsigned long r; + _BitScanReverse(&r, x); + return 31 - (int)r; +} + +static __forceinline int +__builtin_clzll(unsigned long long x) +{ + unsigned long r; + _BitScanReverse64(&r, x); + return 63 - (int)r; +} + +static __forceinline int +__builtin_ctz(unsigned x) +{ + unsigned long r; + _BitScanForward(&r, x); + return (int)r; +} + +static __forceinline int +__builtin_ctzll(unsigned long long x) +{ + unsigned long r; + _BitScanForward64(&r, x); + return (int)r; +} + +static __forceinline int +__builtin_popcount(unsigned x) +{ + return (int)__popcnt(x); +} + +static __forceinline int +__builtin_popcountll(unsigned long long x) +{ + return (int)__popcnt64(x); +} + +/* symfpu uses __builtin_fmaf for fused multiply-add; MSVC has C99 fmaf. */ +static __forceinline float +__builtin_fmaf(float a, float b, float c) +{ + return fmaf(a, b, c); +} + +#endif /* _MSC_VER */ diff --git a/crates/smt-server/vendor/bitwuzla-msvc/shim/unistd.h b/crates/smt-server/vendor/bitwuzla-msvc/shim/unistd.h new file mode 100644 index 0000000..9f6ac38 --- /dev/null +++ b/crates/smt-server/vendor/bitwuzla-msvc/shim/unistd.h @@ -0,0 +1,70 @@ +#pragma once +/* + * Minimal POSIX shim for building cadical + bitwuzla with MSVC. + * Only symbols referenced by the *library* (not the CLI/mobical) are mapped to + * the MSVC CRT. Compiled into every C++ TU via /I + /FImsvc_compat.h. + */ +#include /* _isatty, _access, _read/_write/_close, _open */ +#include /* _getpid, _exit */ +#include /* _getcwd, _chdir, _rmdir */ +#include /* _popen, _pclose */ +#include /* struct stat, stat() */ +#include + +typedef intptr_t ssize_t; +typedef int pid_t; + +#ifndef STDIN_FILENO +#define STDIN_FILENO 0 +#endif +#ifndef STDOUT_FILENO +#define STDOUT_FILENO 1 +#endif +#ifndef STDERR_FILENO +#define STDERR_FILENO 2 +#endif + +/* access() mode flags (POSIX; MSVC does not define R_OK/W_OK). */ +#ifndef F_OK +#define F_OK 0 +#endif +#ifndef R_OK +#define R_OK 4 +#endif +#ifndef W_OK +#define W_OK 2 +#endif +#ifndef X_OK +#define X_OK 0 /* Windows access() ignores the execute bit */ +#endif + +/* stat() type-check macros (POSIX; MSVC lacks S_ISDIR/S_ISFIFO). */ +#ifndef S_IFMT +#define S_IFMT 0xF000 +#endif +#ifndef S_IFDIR +#define S_IFDIR 0x4000 +#endif +#ifndef S_IFIFO +#define S_IFIFO 0x1000 +#endif +#ifndef S_ISDIR +#define S_ISDIR(m) (((m) & S_IFMT) == S_IFDIR) +#endif +#ifndef S_ISFIFO +#define S_ISFIFO(m) (((m) & S_IFMT) == S_IFIFO) +#endif + +/* POSIX name -> MSVC CRT underscore equivalent. */ +#define isatty _isatty +#define getpid _getpid +#define access _access +#define unlink _unlink +#define rmdir _rmdir +#define getcwd _getcwd +#define chdir _chdir +#define close _close +#define read _read +#define write _write +#define popen _popen +#define pclose _pclose From 369d198d2bf843a37013fc5dc49af2dc62203920 Mon Sep 17 00:00:00 2001 From: Brit Date: Tue, 30 Jun 2026 10:37:29 +0200 Subject: [PATCH 3/5] test(bitwuzla): integrate into cross-backend suites Add dedicated backend tests and plug BitwuzlaBackend into the phase2 duplicate-symbol/model and phase6 bit-hunt-optimize parametrized test lists. --- crates/smt-server/tests/bitwuzla_backend.rs | 76 +++++++++++++++++++ crates/smt-server/tests/phase2_server.rs | 30 +++++++- .../tests/phase6_simplify_optimize.rs | 23 ++++++ 3 files changed, 125 insertions(+), 4 deletions(-) create mode 100644 crates/smt-server/tests/bitwuzla_backend.rs diff --git a/crates/smt-server/tests/bitwuzla_backend.rs b/crates/smt-server/tests/bitwuzla_backend.rs new file mode 100644 index 0000000..efd15ce --- /dev/null +++ b/crates/smt-server/tests/bitwuzla_backend.rs @@ -0,0 +1,76 @@ +#![cfg(feature = "bitwuzla")] +//! Backend-level tests for [`BitwuzlaBackend`] in isolation (no racing), +//! exercising translate, solve, model extraction, named-unsat-core, and +//! bit-hunt optimize. Gated behind the `bitwuzla` feature (off by default); CI +//! runs these on Linux, macOS, and Windows MSVC. + +use smt_server::{Backend, BitwuzlaBackend, QueryStatus}; +use smt_wire::raw::{BinaryRequest, ExprBuilder}; + +#[test] +fn bitwuzla_backend_solves_and_returns_model() { + let mut builder = ExprBuilder::new(); + let x = builder.bv_var("x", 4).unwrap(); + let two = builder.bv_const(2, 4).unwrap(); + let eq = builder.bv_eq(x, two).unwrap(); + builder.assert(eq).unwrap(); + let request = + BinaryRequest::parse(&builder.build_solve_request(1, 0, true, false).unwrap()).unwrap(); + let result = BitwuzlaBackend.handle(&request).unwrap(); + assert_eq!(result.status, QueryStatus::Sat); + let model = result.model.expect("sat result should carry a model"); + assert!( + model + .entries + .iter() + .any(|entry| entry.value.width == 4 && entry.value.bytes == vec![2]), + "model should assign x = 2, got {model:?}" + ); +} + +#[test] +fn bitwuzla_backend_extracts_named_unsat_core() { + let mut builder = ExprBuilder::new(); + let p = builder.bool_var("p").unwrap(); + let not_p = builder.bool_not(p).unwrap(); + builder.assert_named("p_true", p).unwrap(); + builder.assert_named("p_false", not_p).unwrap(); + let request = + BinaryRequest::parse(&builder.build_solve_request(1, 0, false, true).unwrap()).unwrap(); + let result = BitwuzlaBackend.handle(&request).unwrap(); + assert_eq!(result.status, QueryStatus::Unsat); + let core = result.core.expect("unsat result should carry a core"); + assert!(core.names.contains(&"p_true".to_owned())); + assert!(core.names.contains(&"p_false".to_owned())); +} + +#[test] +fn bitwuzla_backend_optimization_uses_bit_hunt() { + let mut builder = ExprBuilder::new(); + let x = builder.bv_var("x", 4).unwrap(); + let five = builder.bv_const(5, 4).unwrap(); + let ge = builder.bv_uge(x, five).unwrap(); + builder.assert(ge).unwrap(); + let request = BinaryRequest::parse( + &builder + .build_minimize_request(1, x, false, 0, true) + .unwrap(), + ) + .unwrap(); + let result = BitwuzlaBackend.handle(&request).unwrap(); + assert_eq!(result.status, QueryStatus::Sat); + let optimization = result + .optimization + .expect("minimize result should carry an optimum"); + assert_eq!(optimization.optimum.bytes, vec![5]); + let model = optimization + .model + .expect("minimize result should carry a model"); + assert!( + model + .entries + .iter() + .any(|entry| entry.value.bytes == vec![5]), + "model should assign x = 5, got {model:?}" + ); +} diff --git a/crates/smt-server/tests/phase2_server.rs b/crates/smt-server/tests/phase2_server.rs index d33c1b3..4290180 100644 --- a/crates/smt-server/tests/phase2_server.rs +++ b/crates/smt-server/tests/phase2_server.rs @@ -82,11 +82,22 @@ fn solve_backends_intern_duplicate_wire_bv_symbols_by_name() { let binbit = BinbitBackend; let z3 = Z3Backend; let qfbvsmtrs = QfbvsmtrsBackend; - for (name, backend) in [ + #[cfg(feature = "bitwuzla")] + let bitwuzla = smt_server::BitwuzlaBackend; + #[cfg(feature = "bitwuzla")] + let backends: [(&str, &dyn Backend); 4] = [ ("binbit", &binbit as &dyn Backend), ("z3", &z3 as &dyn Backend), ("qfbvsmtrs", &qfbvsmtrs as &dyn Backend), - ] { + ("bitwuzla", &bitwuzla as &dyn Backend), + ]; + #[cfg(not(feature = "bitwuzla"))] + let backends: [(&str, &dyn Backend); 3] = [ + ("binbit", &binbit as &dyn Backend), + ("z3", &z3 as &dyn Backend), + ("qfbvsmtrs", &qfbvsmtrs as &dyn Backend), + ]; + for (name, backend) in backends { let request = request_with_duplicate_bv_symbol_not_equal(0x4455_5000); let response = handle_binary_frame(&request, backend) .unwrap() @@ -102,11 +113,22 @@ fn solve_backends_return_models_for_duplicate_wire_bv_symbols() { let binbit = BinbitBackend; let z3 = Z3Backend; let qfbvsmtrs = QfbvsmtrsBackend; - for (name, backend) in [ + #[cfg(feature = "bitwuzla")] + let bitwuzla = smt_server::BitwuzlaBackend; + #[cfg(feature = "bitwuzla")] + let backends: [(&str, &dyn Backend); 4] = [ + ("binbit", &binbit as &dyn Backend), + ("z3", &z3 as &dyn Backend), + ("qfbvsmtrs", &qfbvsmtrs as &dyn Backend), + ("bitwuzla", &bitwuzla as &dyn Backend), + ]; + #[cfg(not(feature = "bitwuzla"))] + let backends: [(&str, &dyn Backend); 3] = [ ("binbit", &binbit as &dyn Backend), ("z3", &z3 as &dyn Backend), ("qfbvsmtrs", &qfbvsmtrs as &dyn Backend), - ] { + ]; + for (name, backend) in backends { let request = request_with_duplicate_bv_symbol_model(0x4455_5001); let response = handle_binary_frame(&request, backend) .unwrap() diff --git a/crates/smt-server/tests/phase6_simplify_optimize.rs b/crates/smt-server/tests/phase6_simplify_optimize.rs index e65393e..e78405e 100644 --- a/crates/smt-server/tests/phase6_simplify_optimize.rs +++ b/crates/smt-server/tests/phase6_simplify_optimize.rs @@ -167,6 +167,29 @@ fn z3_backend_optimization_uses_bit_hunt() { assert_eq!(optimum.optimum.bytes, vec![5]); } +#[cfg(feature = "bitwuzla")] +#[test] +fn bitwuzla_backend_optimization_uses_bit_hunt() { + let mut builder = ExprBuilder::new(); + let x = builder.bv_var("x", 4).unwrap(); + let five = builder.bv_const(5, 4).unwrap(); + let ge = builder.bv_uge(x, five).unwrap(); + builder.assert(ge).unwrap(); + let request = builder + .build_minimize_request(28, x, false, 0, false) + .unwrap(); + let response = BinaryResponse::parse( + &handle_binary_frame(&request, &smt_server::BitwuzlaBackend) + .unwrap() + .encode() + .unwrap(), + ) + .unwrap(); + assert_eq!(response.envelope.status, Status::Sat); + let optimum = OptimizationValueBlock::decode(&response.payload, false).unwrap(); + assert_eq!(optimum.optimum.bytes, vec![5]); +} + struct BadModelBackend; impl Backend for BadModelBackend { fn name(&self) -> &'static str { From 0c38ed58497eb795e12f37faea5ac6d021eda2b0 Mon Sep 17 00:00:00 2001 From: Brit Date: Tue, 30 Jun 2026 19:18:05 +0200 Subject: [PATCH 4/5] docs(bitwuzla): document backend and add CI job Update README and architecture docs; add a per-OS bitwuzla CI job that builds with --features bitwuzla. --- .github/workflows/ci.yml | 36 ++++++++++++++++++++++++++++++++++++ README.md | 23 +++++++++++++++++++++++ docs/architecture.md | 4 +++- 3 files changed, 62 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 89a07ec..5b7c29f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -115,3 +115,39 @@ jobs: proc.kill() proc.wait(timeout=5) PY + + bitwuzla: + name: Bitwuzla backend (${{ matrix.os }}) + runs-on: ${{ matrix.os }} + timeout-minutes: 30 + strategy: + fail-fast: false + matrix: + os: [ubuntu-latest, macos-latest, windows-latest] + steps: + - uses: actions/checkout@v6 + - uses: dtolnay/rust-toolchain@stable + with: + components: clippy + - uses: Swatinem/rust-cache@v2 + with: + shared-key: bitwuzla-${{ matrix.os }}-stable + - name: Install GMP and MPFR (Linux) + if: runner.os == 'Linux' + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev libmpfr-dev pkg-config + - name: Install GMP and MPFR (macOS) + if: runner.os == 'macOS' + run: | + brew install gmp mpfr pkg-config + # brew's gmp/mpfr .pc files are not on the default search path. + echo "PKG_CONFIG_PATH=$(brew --prefix)/lib/pkgconfig" >> "$GITHUB_ENV" + # build.rs fetches the prebuilt Bitwuzla 0.9.1 static archive from GitHub + # at build time. Linux/macOS resolve GMP/MPFR via pkg-config (installed + # above); Windows MSVC fetches a self-contained archive with GMP/MPFR + # statically linked in, so no extra install is needed there. + - name: Clippy + run: cargo clippy -p smt-server --features bitwuzla --all-targets -- -D warnings + - name: Test + run: cargo test -p smt-server --features bitwuzla diff --git a/README.md b/README.md index 705ce7a..3d005ac 100644 --- a/README.md +++ b/README.md @@ -14,6 +14,7 @@ It targets binary analysis, lifting, symbolic execution, and IR experiments wher - Solve and optimize: [`z3`](https://docs.rs/z3/latest/z3/), [`binbit`](https://github.com/bint-disasm/binbit), and the standalone `qfbvsmtrs` crate. - Simplify: [Rumba](https://github.com/thalium/rumba) for supported 64-bit-or-smaller MBA expression islands. +- Bitwuzla (optional, `--features bitwuzla`): fetches a prebuilt static [Bitwuzla](https://bitwuzla.github.io/) archive and joins the solver racer when enabled (Linux x86_64/aarch64, macOS arm64, Windows x86_64 `msvc` and `gnu` targets). - Text compatibility: SMT-LIB `QF_BV` scripts are parsed into the same binary IR used by binary clients. The binary protocol is the main API. SMT-LIB support exists for tooling compatibility and test reuse. @@ -37,6 +38,28 @@ Scope is limited to quantifier-free bit-vectors and Booleans. That covers the fo cargo build --workspace ``` +The optional Bitwuzla backend fetches a prebuilt static archive at build time (no source build needed): + +```sh +# Linux: apt install libgmp-dev libmpfr-dev pkg-config +# macOS: brew install gmp mpfr pkg-config +cargo build -p smt-server --features bitwuzla +``` + +Linux/macOS pull the upstream Bitwuzla 0.9.1 release and resolve GMP/MPFR via pkg-config. On Windows the default `x86_64-pc-windows-msvc` target fetches a self-contained MSVC archive (GMP/MPFR statically linked in, no extra install): + +```sh +cargo build -p smt-server --features bitwuzla +``` + +The `x86_64-pc-windows-gnu` target is also supported via the upstream MinGW prebuilt: + +```sh +rustup target add x86_64-pc-windows-gnu +# MSYS2: pacman -S mingw-w64-x86_64-gmp mingw-w64-x86_64-mpfr mingw-w64-x86_64-pkgconf +cargo build -p smt-server --features bitwuzla --target x86_64-pc-windows-gnu +``` + ## Run the server ```sh diff --git a/docs/architecture.md b/docs/architecture.md index b081130..3727395 100644 --- a/docs/architecture.md +++ b/docs/architecture.md @@ -78,7 +78,8 @@ CommandRouterBackend -> RacingBackend(default budget: 30s) ├── Z3Backend ├── BinbitBackend - └── QfbvsmtrsBackend + ├── QfbvsmtrsBackend + └── BitwuzlaBackend (optional, enabled with --features bitwuzla) ``` Backend responsibilities: @@ -86,6 +87,7 @@ Backend responsibilities: - `Z3Backend` translates validated wire IR to the Rust `z3` crate and supports solve, model extraction, named unsat cores, and bit-hunt optimization. - `BinbitBackend` translates validated wire IR to `binbit` and supports solve, model extraction, named unsat cores, and optimization helpers. - `QfbvsmtrsBackend` lowers wire requests into the standalone qfbvsmtrs IR and uses the pure-Rust bit-blast/SAT pipeline. +- `BitwuzlaBackend` (optional, behind the `bitwuzla` cargo feature) translates validated wire IR to the official Bitwuzla C library, linked against a prebuilt static archive fetched at build time, and supports solve, model extraction, named unsat cores via unsat assumptions, and bit-hunt optimization. It joins the solver racer as a fourth backend when the feature is enabled; the shipped binary omits it entirely when the feature is off. Linux/macOS and the Windows `gnu` target fetch the upstream Bitwuzla 0.9.1 release and resolve GMP/MPFR via pkg-config; the Windows `msvc` target fetches a self-contained MSVC archive (rebuilt from the 0.9.1 source under `cl.exe`, with GMP/MPFR statically linked in) published on this crate's own GitHub release. - `RumbaBackend` handles `SIMPLIFY` for supported 64-bit-or-smaller MBA expression islands. Unsupported simplifications return the original target expression rather than a wrong rewrite. `RacingBackend` returns the first conclusive answer and logs later disagreements for investigation. `UNKNOWN` is safe and means no backend produced a conclusive answer within the applicable budget. From 5df022378db9d703c5c98a62dd8a450e5ec5979a Mon Sep 17 00:00:00 2001 From: Brit Date: Tue, 30 Jun 2026 20:42:11 +0200 Subject: [PATCH 5/5] feat(bitwuzla): build backend unconditionally Drop the `bitwuzla` cargo feature: the backend now builds unconditionally like Z3/Binbit/Qfbvsmtrs (no opt-out, no `--features bitwuzla`). CI keeps GMP/MPFR in the rust job; the standalone bitwuzla job stays removed. README/architecture no longer call out a default or an opt-out. --- .github/workflows/ci.yml | 47 +++++-------------- README.md | 14 ++---- crates/smt-server/Cargo.toml | 5 +- crates/smt-server/build.rs | 5 -- crates/smt-server/src/lib.rs | 10 ++-- crates/smt-server/src/main.rs | 10 +--- crates/smt-server/tests/bitwuzla_backend.rs | 4 +- crates/smt-server/tests/phase2_server.rs | 16 ------- .../tests/phase6_simplify_optimize.rs | 1 - docs/architecture.md | 4 +- 10 files changed, 23 insertions(+), 93 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5b7c29f..e642745 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -36,6 +36,17 @@ jobs: - uses: Swatinem/rust-cache@v2 with: shared-key: ${{ matrix.os }}-stable + - name: Install GMP and MPFR (Linux) + if: runner.os == 'Linux' + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev libmpfr-dev pkg-config + - name: Install GMP and MPFR (macOS) + if: runner.os == 'macOS' + run: | + brew install gmp mpfr pkg-config + # brew's gmp/mpfr .pc files are not on the default search path. + echo "PKG_CONFIG_PATH=$(brew --prefix)/lib/pkgconfig" >> "$GITHUB_ENV" - name: Format run: cargo fmt --all -- --check - name: Test @@ -115,39 +126,3 @@ jobs: proc.kill() proc.wait(timeout=5) PY - - bitwuzla: - name: Bitwuzla backend (${{ matrix.os }}) - runs-on: ${{ matrix.os }} - timeout-minutes: 30 - strategy: - fail-fast: false - matrix: - os: [ubuntu-latest, macos-latest, windows-latest] - steps: - - uses: actions/checkout@v6 - - uses: dtolnay/rust-toolchain@stable - with: - components: clippy - - uses: Swatinem/rust-cache@v2 - with: - shared-key: bitwuzla-${{ matrix.os }}-stable - - name: Install GMP and MPFR (Linux) - if: runner.os == 'Linux' - run: | - sudo apt-get update - sudo apt-get install -y libgmp-dev libmpfr-dev pkg-config - - name: Install GMP and MPFR (macOS) - if: runner.os == 'macOS' - run: | - brew install gmp mpfr pkg-config - # brew's gmp/mpfr .pc files are not on the default search path. - echo "PKG_CONFIG_PATH=$(brew --prefix)/lib/pkgconfig" >> "$GITHUB_ENV" - # build.rs fetches the prebuilt Bitwuzla 0.9.1 static archive from GitHub - # at build time. Linux/macOS resolve GMP/MPFR via pkg-config (installed - # above); Windows MSVC fetches a self-contained archive with GMP/MPFR - # statically linked in, so no extra install is needed there. - - name: Clippy - run: cargo clippy -p smt-server --features bitwuzla --all-targets -- -D warnings - - name: Test - run: cargo test -p smt-server --features bitwuzla diff --git a/README.md b/README.md index 3d005ac..8c793bf 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ It targets binary analysis, lifting, symbolic execution, and IR experiments wher - Solve and optimize: [`z3`](https://docs.rs/z3/latest/z3/), [`binbit`](https://github.com/bint-disasm/binbit), and the standalone `qfbvsmtrs` crate. - Simplify: [Rumba](https://github.com/thalium/rumba) for supported 64-bit-or-smaller MBA expression islands. -- Bitwuzla (optional, `--features bitwuzla`): fetches a prebuilt static [Bitwuzla](https://bitwuzla.github.io/) archive and joins the solver racer when enabled (Linux x86_64/aarch64, macOS arm64, Windows x86_64 `msvc` and `gnu` targets). +- Bitwuzla: fetches a prebuilt static [Bitwuzla](https://bitwuzla.github.io/) archive at build time and joins the solver racer (Linux x86_64/aarch64, macOS arm64, Windows x86_64 `msvc` and `gnu` targets). - Text compatibility: SMT-LIB `QF_BV` scripts are parsed into the same binary IR used by binary clients. The binary protocol is the main API. SMT-LIB support exists for tooling compatibility and test reuse. @@ -38,18 +38,12 @@ Scope is limited to quantifier-free bit-vectors and Booleans. That covers the fo cargo build --workspace ``` -The optional Bitwuzla backend fetches a prebuilt static archive at build time (no source build needed): +The Bitwuzla backend fetches a prebuilt static archive at build time (no source build needed). Linux/macOS resolve GMP/MPFR via pkg-config; Windows MSVC fetches a self-contained archive with GMP/MPFR statically linked in (no extra install): ```sh # Linux: apt install libgmp-dev libmpfr-dev pkg-config # macOS: brew install gmp mpfr pkg-config -cargo build -p smt-server --features bitwuzla -``` - -Linux/macOS pull the upstream Bitwuzla 0.9.1 release and resolve GMP/MPFR via pkg-config. On Windows the default `x86_64-pc-windows-msvc` target fetches a self-contained MSVC archive (GMP/MPFR statically linked in, no extra install): - -```sh -cargo build -p smt-server --features bitwuzla +cargo build -p smt-server ``` The `x86_64-pc-windows-gnu` target is also supported via the upstream MinGW prebuilt: @@ -57,7 +51,7 @@ The `x86_64-pc-windows-gnu` target is also supported via the upstream MinGW preb ```sh rustup target add x86_64-pc-windows-gnu # MSYS2: pacman -S mingw-w64-x86_64-gmp mingw-w64-x86_64-mpfr mingw-w64-x86_64-pkgconf -cargo build -p smt-server --features bitwuzla --target x86_64-pc-windows-gnu +cargo build -p smt-server --target x86_64-pc-windows-gnu ``` ## Run the server diff --git a/crates/smt-server/Cargo.toml b/crates/smt-server/Cargo.toml index 1d7e166..153a301 100644 --- a/crates/smt-server/Cargo.toml +++ b/crates/smt-server/Cargo.toml @@ -18,8 +18,5 @@ z3 = { version = "0.20.0", features = ["gh-release"] } [dev-dependencies] rumba-core = { git = "https://github.com/thalium/rumba", rev = "2a7a38963f9894cdda24ea93b5f278752aff7a2e", features = ["parse"] } -[features] -bitwuzla = ["dep:pkg-config"] - [build-dependencies] -pkg-config = { version = "0.3", optional = true } +pkg-config = "0.3" diff --git a/crates/smt-server/build.rs b/crates/smt-server/build.rs index 6e7daec..85e7b96 100644 --- a/crates/smt-server/build.rs +++ b/crates/smt-server/build.rs @@ -9,7 +9,6 @@ // MinGW. Release layouts vary, so we search the extracted tree for // `libbitwuzla.a`. -#[cfg(feature = "bitwuzla")] fn main() { if let Err(err) = bitwuzla::link() { eprintln!("error: {err}"); @@ -17,10 +16,6 @@ fn main() { } } -#[cfg(not(feature = "bitwuzla"))] -fn main() {} - -#[cfg(feature = "bitwuzla")] mod bitwuzla { use std::env; use std::fmt::Write as _; diff --git a/crates/smt-server/src/lib.rs b/crates/smt-server/src/lib.rs index 916c339..f59ade0 100644 --- a/crates/smt-server/src/lib.rs +++ b/crates/smt-server/src/lib.rs @@ -1,15 +1,12 @@ //! Reference server-side implementation for the SMT wire protocol. //! -//! The crate provides a small TCP server, binary request handling, native Z3 -//! and binbit solver backends, an optional Bitwuzla backend (behind the -//! `bitwuzla` feature), backend racing, request/response caching, and a -//! compact SMT-LIB frontend. +//! The crate provides a small TCP server, binary request handling, native Z3, +//! binbit, and Bitwuzla solver backends, backend racing, request/response +//! caching, and a compact SMT-LIB frontend. pub mod backend; pub mod binbit_backend; -#[cfg(feature = "bitwuzla")] pub mod bitwuzla_backend; -#[cfg(feature = "bitwuzla")] pub mod bitwuzla_bindings; pub mod cache; pub mod command_router; @@ -26,7 +23,6 @@ pub mod z3_backend; pub use backend::{Backend, CancellationToken, QueryResult, QueryStatus, SolveContext}; pub use binbit_backend::BinbitBackend; -#[cfg(feature = "bitwuzla")] pub use bitwuzla_backend::BitwuzlaBackend; pub use cache::{cache_key_for_payload, rebind_cached_response, CacheStats, ResponseCache}; pub use command_router::CommandRouterBackend; diff --git a/crates/smt-server/src/main.rs b/crates/smt-server/src/main.rs index 266b048..83014f1 100644 --- a/crates/smt-server/src/main.rs +++ b/crates/smt-server/src/main.rs @@ -1,7 +1,6 @@ use std::path::PathBuf; use std::sync::Arc; -#[cfg(feature = "bitwuzla")] use smt_server::BitwuzlaBackend; use smt_server::{ default_legacy_recording_tree, migrate_recording_tree, recording_db_path, serve_tcp, Backend, @@ -17,23 +16,16 @@ fn main() -> std::io::Result<()> { return Ok(()); } let addr = arg.unwrap_or_else(|| "127.0.0.1:9123".to_owned()); - #[cfg_attr(not(feature = "bitwuzla"), allow(unused_mut))] let mut racers: Vec> = vec![ Arc::new(Z3Backend), Arc::new(BinbitBackend), Arc::new(QfbvsmtrsBackend), ]; - #[cfg(feature = "bitwuzla")] racers.push(Arc::new(BitwuzlaBackend)); let solver = Arc::new(RacingBackend::new(racers).with_default_budget_ms(30_000)); let backend = Arc::new(CommandRouterBackend::new(Arc::new(RumbaBackend), solver)); eprintln!( - "smt-server listening on {addr} with rumba simplifier + racing solver (z3 crate + binbit + qfbvsmtrs{})", - if cfg!(feature = "bitwuzla") { - " + bitwuzla" - } else { - "" - } + "smt-server listening on {addr} with rumba simplifier + racing solver (z3 crate + binbit + qfbvsmtrs + bitwuzla)" ); serve_tcp(addr, ServerConfig::new(backend)) } diff --git a/crates/smt-server/tests/bitwuzla_backend.rs b/crates/smt-server/tests/bitwuzla_backend.rs index efd15ce..a71d18a 100644 --- a/crates/smt-server/tests/bitwuzla_backend.rs +++ b/crates/smt-server/tests/bitwuzla_backend.rs @@ -1,8 +1,6 @@ -#![cfg(feature = "bitwuzla")] //! Backend-level tests for [`BitwuzlaBackend`] in isolation (no racing), //! exercising translate, solve, model extraction, named-unsat-core, and -//! bit-hunt optimize. Gated behind the `bitwuzla` feature (off by default); CI -//! runs these on Linux, macOS, and Windows MSVC. +//! bit-hunt optimize. CI runs these on Linux, macOS, and Windows MSVC. use smt_server::{Backend, BitwuzlaBackend, QueryStatus}; use smt_wire::raw::{BinaryRequest, ExprBuilder}; diff --git a/crates/smt-server/tests/phase2_server.rs b/crates/smt-server/tests/phase2_server.rs index 4290180..d069b60 100644 --- a/crates/smt-server/tests/phase2_server.rs +++ b/crates/smt-server/tests/phase2_server.rs @@ -82,21 +82,13 @@ fn solve_backends_intern_duplicate_wire_bv_symbols_by_name() { let binbit = BinbitBackend; let z3 = Z3Backend; let qfbvsmtrs = QfbvsmtrsBackend; - #[cfg(feature = "bitwuzla")] let bitwuzla = smt_server::BitwuzlaBackend; - #[cfg(feature = "bitwuzla")] let backends: [(&str, &dyn Backend); 4] = [ ("binbit", &binbit as &dyn Backend), ("z3", &z3 as &dyn Backend), ("qfbvsmtrs", &qfbvsmtrs as &dyn Backend), ("bitwuzla", &bitwuzla as &dyn Backend), ]; - #[cfg(not(feature = "bitwuzla"))] - let backends: [(&str, &dyn Backend); 3] = [ - ("binbit", &binbit as &dyn Backend), - ("z3", &z3 as &dyn Backend), - ("qfbvsmtrs", &qfbvsmtrs as &dyn Backend), - ]; for (name, backend) in backends { let request = request_with_duplicate_bv_symbol_not_equal(0x4455_5000); let response = handle_binary_frame(&request, backend) @@ -113,21 +105,13 @@ fn solve_backends_return_models_for_duplicate_wire_bv_symbols() { let binbit = BinbitBackend; let z3 = Z3Backend; let qfbvsmtrs = QfbvsmtrsBackend; - #[cfg(feature = "bitwuzla")] let bitwuzla = smt_server::BitwuzlaBackend; - #[cfg(feature = "bitwuzla")] let backends: [(&str, &dyn Backend); 4] = [ ("binbit", &binbit as &dyn Backend), ("z3", &z3 as &dyn Backend), ("qfbvsmtrs", &qfbvsmtrs as &dyn Backend), ("bitwuzla", &bitwuzla as &dyn Backend), ]; - #[cfg(not(feature = "bitwuzla"))] - let backends: [(&str, &dyn Backend); 3] = [ - ("binbit", &binbit as &dyn Backend), - ("z3", &z3 as &dyn Backend), - ("qfbvsmtrs", &qfbvsmtrs as &dyn Backend), - ]; for (name, backend) in backends { let request = request_with_duplicate_bv_symbol_model(0x4455_5001); let response = handle_binary_frame(&request, backend) diff --git a/crates/smt-server/tests/phase6_simplify_optimize.rs b/crates/smt-server/tests/phase6_simplify_optimize.rs index e78405e..58d292c 100644 --- a/crates/smt-server/tests/phase6_simplify_optimize.rs +++ b/crates/smt-server/tests/phase6_simplify_optimize.rs @@ -167,7 +167,6 @@ fn z3_backend_optimization_uses_bit_hunt() { assert_eq!(optimum.optimum.bytes, vec![5]); } -#[cfg(feature = "bitwuzla")] #[test] fn bitwuzla_backend_optimization_uses_bit_hunt() { let mut builder = ExprBuilder::new(); diff --git a/docs/architecture.md b/docs/architecture.md index 3727395..52035de 100644 --- a/docs/architecture.md +++ b/docs/architecture.md @@ -79,7 +79,7 @@ CommandRouterBackend ├── Z3Backend ├── BinbitBackend ├── QfbvsmtrsBackend - └── BitwuzlaBackend (optional, enabled with --features bitwuzla) + └── BitwuzlaBackend ``` Backend responsibilities: @@ -87,7 +87,7 @@ Backend responsibilities: - `Z3Backend` translates validated wire IR to the Rust `z3` crate and supports solve, model extraction, named unsat cores, and bit-hunt optimization. - `BinbitBackend` translates validated wire IR to `binbit` and supports solve, model extraction, named unsat cores, and optimization helpers. - `QfbvsmtrsBackend` lowers wire requests into the standalone qfbvsmtrs IR and uses the pure-Rust bit-blast/SAT pipeline. -- `BitwuzlaBackend` (optional, behind the `bitwuzla` cargo feature) translates validated wire IR to the official Bitwuzla C library, linked against a prebuilt static archive fetched at build time, and supports solve, model extraction, named unsat cores via unsat assumptions, and bit-hunt optimization. It joins the solver racer as a fourth backend when the feature is enabled; the shipped binary omits it entirely when the feature is off. Linux/macOS and the Windows `gnu` target fetch the upstream Bitwuzla 0.9.1 release and resolve GMP/MPFR via pkg-config; the Windows `msvc` target fetches a self-contained MSVC archive (rebuilt from the 0.9.1 source under `cl.exe`, with GMP/MPFR statically linked in) published on this crate's own GitHub release. +- `BitwuzlaBackend` translates validated wire IR to the official Bitwuzla C library, linked against a prebuilt static archive fetched at build time, and supports solve, model extraction, named unsat cores via unsat assumptions, and bit-hunt optimization. Linux/macOS and the Windows `gnu` target fetch the upstream Bitwuzla 0.9.1 release and resolve GMP/MPFR via pkg-config; the Windows `msvc` target fetches a self-contained MSVC archive (rebuilt from the 0.9.1 source under `cl.exe`, with GMP/MPFR statically linked in) published on the [bitwuzla-msvc](https://github.com/LLVMParty/bitwuzla-msvc) fork's GitHub release. - `RumbaBackend` handles `SIMPLIFY` for supported 64-bit-or-smaller MBA expression islands. Unsupported simplifications return the original target expression rather than a wrong rewrite. `RacingBackend` returns the first conclusive answer and logs later disagreements for investigation. `UNKNOWN` is safe and means no backend produced a conclusive answer within the applicable budget.