From 8f6db3aabb78528264b67b75d8791dd2be14b948 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 12 Dec 2024 16:30:38 -0500 Subject: [PATCH] smt: small bitwuzla solver example working --- .gitignore | 1 + patronus/src/smt/serialize.rs | 3 +- patronus/src/smt/solver.rs | 167 +++++++++++++++++++++++++++------- 3 files changed, 136 insertions(+), 35 deletions(-) diff --git a/.gitignore b/.gitignore index e355b0b..93c8763 100644 --- a/.gitignore +++ b/.gitignore @@ -6,3 +6,4 @@ Cargo.lock /flamegraph.svg /perf.data /perf.data.old +replay.smt diff --git a/patronus/src/smt/serialize.rs b/patronus/src/smt/serialize.rs index c46b757..abb9bc6 100644 --- a/patronus/src/smt/serialize.rs +++ b/patronus/src/smt/serialize.rs @@ -12,7 +12,6 @@ pub type Result = std::io::Result; pub fn serialize_expr(out: &mut impl Write, ctx: &Context, expr: ExprRef) -> Result<()> { // we need to visit each expression "number of children + 1" times let mut todo: Vec<(ExprRef, u32)> = vec![(expr, 0)]; - let mut child_vec: Vec = Vec::with_capacity(4); while let Some((e, pc)) = todo.pop() { let expr = &ctx[e]; @@ -36,7 +35,7 @@ pub fn serialize_expr(out: &mut impl Write, ctx: &Context, expr: ExprRef) -> Res Expr::BVSlice { .. } => todo!(), Expr::BVNot(_, _) => todo!(), Expr::BVNegate(_, _) => todo!(), - Expr::BVEqual(_, _) => todo!(), + Expr::BVEqual(_, _) => write!(out, "(=")?, Expr::BVImplies(_, _) => todo!(), Expr::BVGreater(_, _) => todo!(), Expr::BVGreaterSigned(_, _, _) => todo!(), diff --git a/patronus/src/smt/solver.rs b/patronus/src/smt/solver.rs index 2f227c2..19283e5 100644 --- a/patronus/src/smt/solver.rs +++ b/patronus/src/smt/solver.rs @@ -3,8 +3,9 @@ // author: Kevin Laeufer use crate::expr::{Context, ExprRef}; -use std::io::Write; +use crate::smt::serialize::serialize_expr; use std::io::{BufRead, BufReader, BufWriter}; +use std::io::{Read, Write}; use std::process::{ChildStdin, Command, Stdio}; use thiserror::Error; @@ -32,7 +33,7 @@ pub enum Logic { } /// The result of a `(check-sat)` command. -#[derive(Debug, Clone)] +#[derive(Debug, Clone, Eq, PartialEq)] pub enum CheckSatResponse { Sat, Unsat, @@ -47,48 +48,58 @@ pub trait Solver { fn define_const(&mut self, ctx: &Context, symbol: ExprRef, expr: ExprRef) -> Result<()>; fn check_sat_assuming( &mut self, + ctx: &Context, props: impl IntoIterator, ) -> Result; - fn check_sat(&mut self) -> Result { - self.check_sat_assuming([]) - } + fn check_sat(&mut self) -> Result; fn push(&mut self) -> Result<()>; fn pop(&mut self) -> Result<()>; } /// Launches an SMT solver and communicates through `stdin` using SMTLib commands. -pub struct SmtLibSolver { +pub struct SmtLibSolver { name: String, proc: std::process::Child, stdin: BufWriter, stdout: BufReader, + stderr: std::process::ChildStderr, stack_depth: usize, response: String, + replay_file: Option, + /// keeps track of whether there was an error from the solver which might make regular shutdown + /// impossible + has_error: bool, } -impl SmtLibSolver { - pub fn bitwuzla() -> Result { - Self::create(&BITWUZLA_CMD) +impl SmtLibSolver { + pub fn bitwuzla(replay_file: Option) -> Result { + Self::create(&BITWUZLA_CMD, replay_file) } - fn create(cmd: &SmtSolverCmd) -> Result { + fn create(cmd: &SmtSolverCmd, replay_file: Option) -> Result { let mut proc = Command::new(cmd.name) .args(cmd.args) .stdin(Stdio::piped()) .stdout(Stdio::piped()) + .stderr(Stdio::piped()) .spawn()?; let stdin = BufWriter::new(proc.stdin.take().unwrap()); let stdout = BufReader::new(proc.stdout.take().unwrap()); + let stderr = proc.stderr.take().unwrap(); let name = cmd.name.to_string(); let mut solver = Self { name, proc, stdin, stdout, + stderr, stack_depth: 0, response: String::new(), + replay_file, + has_error: false, }; for option in cmd.options.iter() { + solver.write_cmd_replay(|o| writeln!(o, "(set-option :{} true)", option))?; solver.write_cmd(|o| writeln!(o, "(set-option :{} true)", option))?; } Ok(solver) @@ -96,19 +107,32 @@ impl SmtLibSolver { #[inline] fn write_cmd_str(&mut self, cmd: &str) -> Result<()> { + self.write_cmd_replay(|stdin| writeln!(stdin, "{}", cmd))?; self.write_cmd(|stdin| writeln!(stdin, "{}", cmd)) } #[inline] fn write_cmd( &mut self, - cmd: impl Fn(&mut BufWriter) -> std::result::Result<(), std::io::Error>, + cmd: impl FnOnce(&mut BufWriter) -> std::result::Result<(), std::io::Error>, ) -> Result<()> { cmd(&mut self.stdin)?; self.stdin.flush()?; Ok(()) } + #[inline] + fn write_cmd_replay( + &mut self, + cmd: impl FnOnce(&mut R) -> std::result::Result<(), std::io::Error>, + ) -> Result<()> { + if let Some(rf) = self.replay_file.as_mut() { + cmd(rf)?; + rf.flush()?; + } + Ok(()) + } + /// after this function executes, the result will be available in `self.result`. fn read_response(&mut self) -> Result<()> { self.stdin.flush()?; // make sure that the commands reached the solver @@ -121,16 +145,41 @@ impl SmtLibSolver { self.response.push(' '); self.stdout.read_line(&mut self.response)?; } - // check to see if there was an error + // check stderr + let mut err = vec![]; + self.stderr.read_to_end(&mut err)?; + if !err.is_empty() { + self.has_error = true; + return Err(Error::FromSolver( + self.name.clone(), + String::from_utf8_lossy(&err).to_string(), + )); + } + + // check to see if there was an error reported on stdout if self.response.trim_start().starts_with("(error") { let trimmed = self.response.trim(); let start = "(error ".len(); let msg = &trimmed[start..(trimmed.len() - start - 1)]; + self.has_error = true; Err(Error::FromSolver(self.name.clone(), msg.to_string())) } else { Ok(()) } } + + fn read_sat_response(&mut self) -> Result { + self.read_response()?; + let response = self.response.trim(); + match response { + "sat" => Ok(CheckSatResponse::Sat), + "unsat" => Ok(CheckSatResponse::Unsat), + other => Err(Error::UnexpectedResponse( + self.name.clone(), + other.to_string(), + )), + } + } } fn count_parens(s: &str) -> i64 { @@ -141,39 +190,59 @@ fn count_parens(s: &str) -> i64 { }) } -impl Drop for SmtLibSolver { +impl Drop for SmtLibSolver { fn drop(&mut self) { // try to close the child process as not to leak resources - self.write_cmd_str("(exit)") - .expect("failed to send exit command"); + if self.write_cmd_str("(exit)").is_err() { + if self.has_error { + return; + } else { + panic!("failed to send exit command"); + } + } let status = self .proc .wait() .expect("failed to wait for SMT solver to exit"); - assert!( - status.success(), - "There was an error with the solver exiting: {:?}", - status - ); + if !self.has_error { + // if everything has gone smoothly so far, we expect a successful exit + assert!( + status.success(), + "There was an error with the solver exiting: {:?}", + status + ); + } } } -impl Solver for SmtLibSolver { +impl Solver for SmtLibSolver { fn set_logic(&mut self, logic: Logic) -> Result<()> { let logic = match logic { Logic::All => "ALL", Logic::QfAufbv => "QF_AUFBV", Logic::QfAbv => "QF_ABV", }; + self.write_cmd_replay(|o| writeln!(o, "(set-logic {})", logic))?; self.write_cmd(|o| writeln!(o, "(set-logic {})", logic)) } fn assert(&mut self, ctx: &Context, e: ExprRef) -> Result<()> { - todo!() + self.write_cmd_replay(|out| { + write!(out, "(assert ")?; + serialize_expr(out, ctx, e)?; + writeln!(out, ")") + })?; + self.write_cmd(|out| { + write!(out, "(assert ")?; + serialize_expr(out, ctx, e)?; + writeln!(out, ")") + }) } fn declare_const(&mut self, ctx: &Context, symbol: ExprRef) -> Result<()> { - todo!() + todo!( + "we should change hoow write_cmd works to take &str and a list of expressions or types" + ) } fn define_const(&mut self, ctx: &Context, symbol: ExprRef, expr: ExprRef) -> Result<()> { @@ -182,22 +251,34 @@ impl Solver for SmtLibSolver { fn check_sat_assuming( &mut self, + ctx: &Context, props: impl IntoIterator, ) -> Result { - todo!() + let props: Vec = props.into_iter().collect(); + self.write_cmd_replay(|out| { + write!(out, "(check-sat-assuming")?; + let mut is_first = true; + for &prop in props.iter() { + write!(out, " ")?; + serialize_expr(out, ctx, prop)?; + } + writeln!(out, ")") + })?; + self.write_cmd(|out| { + write!(out, "(check-sat-assuming")?; + let mut is_first = true; + for &prop in props.iter() { + write!(out, " ")?; + serialize_expr(out, ctx, prop)?; + } + writeln!(out, ")") + })?; + self.read_sat_response() } fn check_sat(&mut self) -> Result { self.write_cmd_str("(check-sat)")?; - self.read_response()?; - match self.response.trim() { - "sat" => Ok(CheckSatResponse::Sat), - "unsat" => Ok(CheckSatResponse::Unsat), - other => Err(Error::UnexpectedResponse( - self.name.clone(), - other.to_string(), - )), - } + self.read_sat_response() } fn push(&mut self) -> Result<()> { @@ -241,3 +322,23 @@ const YICES2_CMD: SmtSolverCmd = SmtSolverCmd { supports_uf: false, // actually true, but ignoring for now supports_check_assuming: false, }; + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_bitwuzla() { + let mut ctx = Context::default(); + let replay = Some(std::fs::File::create("replay.smt").unwrap()); + let mut solver = SmtLibSolver::bitwuzla(replay).unwrap(); + let a = ctx.bv_symbol("a", 3); + let e = ctx.build(|c| c.equal(a, c.bit_vec_val(3, 3))); + solver.assert(&ctx, e).unwrap(); + let res = solver.check_sat(); + assert!(res.is_err(), "a was not declared!"); + solver.declare_const(&ctx, a).unwrap(); + let res = solver.check_sat(); + assert_eq!(res.unwrap(), CheckSatResponse::Sat); + } +}