From 5ad0c060a578de0550bfaa80593c73722eccd3db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Fri, 13 Dec 2024 12:14:29 -0500 Subject: [PATCH] smt: serialize command and deal with failed solver --- patronus/src/smt/serialize.rs | 51 ++++++++++- patronus/src/smt/solver.rs | 168 +++++++++++++++++----------------- 2 files changed, 136 insertions(+), 83 deletions(-) diff --git a/patronus/src/smt/serialize.rs b/patronus/src/smt/serialize.rs index abb9bc6..d7e8656 100644 --- a/patronus/src/smt/serialize.rs +++ b/patronus/src/smt/serialize.rs @@ -3,7 +3,8 @@ // released under BSD 3-Clause License // author: Kevin Laeufer -use crate::expr::{Context, Expr, ExprRef, ForEachChild, Type}; +use crate::expr::{Context, Expr, ExprRef, ForEachChild, Type, TypeCheck}; +use crate::smt::solver::SmtCommand; use baa::BitVecOps; use std::io::Write; @@ -89,6 +90,54 @@ fn find_next_child(pos: u32, e: &Expr) -> Option { out } +pub fn serialize_cmd(out: &mut impl Write, ctx: Option<&Context>, cmd: &SmtCommand) -> Result<()> { + match cmd { + SmtCommand::Exit => writeln!(out, "(exit)"), + SmtCommand::CheckSat => writeln!(out, "(check-sat)"), + SmtCommand::SetLogic(logic) => writeln!(out, "(set-logic {})", logic.to_smt_str()), + SmtCommand::SetOption(name, value) => writeln!(out, "(set-option :{name} {value})"), + SmtCommand::Assert(e) => { + write!(out, "(assert ")?; + serialize_expr(out, ctx.unwrap(), *e)?; + writeln!(out, ")") + } + SmtCommand::DeclareConst(symbol) => { + let ctx = ctx.unwrap(); + write!( + out, + "(declare-const {} ", + ctx.get_symbol_name(*symbol).unwrap() + )?; + serialize_type(out, symbol.get_type(ctx))?; + writeln!(out, ")") + } + SmtCommand::DefineConst(symbol, value) => { + let ctx = ctx.unwrap(); + // name, then empty arguments + write!( + out, + "(define-fun {} () ", + ctx.get_symbol_name(*symbol).unwrap() + )?; + serialize_type(out, symbol.get_type(ctx))?; + write!(out, " ")?; + serialize_expr(out, ctx, *value)?; + writeln!(out, ")") + } + SmtCommand::CheckSatAssuming(exprs) => { + let ctx = ctx.unwrap(); + write!(out, "(check-sat-assuming")?; + for &e in exprs.iter() { + write!(out, " ")?; + serialize_expr(out, ctx, e)?; + } + writeln!(out, ")") + } + SmtCommand::Push(n) => writeln!(out, "(push {n})"), + SmtCommand::Pop(n) => writeln!(out, "(pop {n})"), + } +} + pub fn serialize_type(out: &mut impl Write, tpe: Type) -> Result<()> { match tpe { Type::BV(1) => write!(out, "Bool"), diff --git a/patronus/src/smt/solver.rs b/patronus/src/smt/solver.rs index 19283e5..10b12b2 100644 --- a/patronus/src/smt/solver.rs +++ b/patronus/src/smt/solver.rs @@ -3,10 +3,10 @@ // author: Kevin Laeufer use crate::expr::{Context, ExprRef}; -use crate::smt::serialize::serialize_expr; +use crate::smt::serialize::serialize_cmd; use std::io::{BufRead, BufReader, BufWriter}; use std::io::{Read, Write}; -use std::process::{ChildStdin, Command, Stdio}; +use std::process::{Command, Stdio}; use thiserror::Error; /// A SMT Solver Error. @@ -18,6 +18,8 @@ pub enum Error { StackUnderflow, #[error("[smt] {0} reported an error:\n{1}")] FromSolver(String, String), + #[error("[smt]{0} is unreachable, the process might have died")] + SolverDead(String), #[error("[smt] {0} returned an unexpected response:\n{1}")] UnexpectedResponse(String, String), } @@ -25,13 +27,38 @@ pub enum Error { pub type Result = std::result::Result; /// An SMT Logic. -#[derive(Debug, Clone)] +#[derive(Debug, Clone, Eq, PartialEq)] pub enum Logic { All, QfAufbv, QfAbv, } +impl Logic { + pub(crate) fn to_smt_str(&self) -> &'static str { + match self { + Logic::All => "ALL", + Logic::QfAufbv => "QF_AUFBV", + Logic::QfAbv => "QF_ABV", + } + } +} + +/// A command to an SMT solver. +#[derive(Debug, Clone, Eq, PartialEq)] +pub enum SmtCommand { + Exit, + CheckSat, + SetLogic(Logic), + SetOption(String, String), + Assert(ExprRef), + DeclareConst(ExprRef), + DefineConst(ExprRef, ExprRef), + CheckSatAssuming(Vec), + Push(u64), + Pop(u64), +} + /// The result of a `(check-sat)` command. #[derive(Debug, Clone, Eq, PartialEq)] pub enum CheckSatResponse { @@ -99,38 +126,32 @@ impl SmtLibSolver { 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))?; + solver.write_cmd( + None, + &SmtCommand::SetOption(option.to_string(), "true".to_string()), + )? } Ok(solver) } #[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 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<()> { + fn write_cmd(&mut self, ctx: Option<&Context>, cmd: &SmtCommand) -> Result<()> { + if let Some(rf) = self.replay_file.as_mut() { + serialize_cmd(rf, ctx, cmd)?; + } + serialize_cmd(&mut self.stdin, ctx, cmd)?; if let Some(rf) = self.replay_file.as_mut() { - cmd(rf)?; rf.flush()?; } - Ok(()) + match self.stdin.flush() { + Err(e) if e.kind() == std::io::ErrorKind::BrokenPipe => { + // make sure we drop the replay file + self.replay_file.take(); + Err(Error::SolverDead(self.name.clone())) + } + Err(other) => Err(other.into()), + Ok(_) => Ok(()), + } } /// after this function executes, the result will be available in `self.result`. @@ -145,16 +166,6 @@ impl SmtLibSolver { self.response.push(' '); self.stdout.read_line(&mut self.response)?; } - // 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") { @@ -164,7 +175,21 @@ impl SmtLibSolver { self.has_error = true; Err(Error::FromSolver(self.name.clone(), msg.to_string())) } else { - Ok(()) + // check if the process is still alive + match self.proc.try_wait() { + Ok(Some(status)) if !status.success() => { + // solver terminated with error return code + // check for output on stderror + let mut err = vec![]; + self.stderr.read_to_end(&mut err)?; + self.has_error = true; + Err(Error::FromSolver( + self.name.clone(), + String::from_utf8_lossy(&err).to_string(), + )) + } + _ => Ok(()), + } } } @@ -193,7 +218,7 @@ fn count_parens(s: &str) -> i64 { impl Drop for SmtLibSolver { fn drop(&mut self) { // try to close the child process as not to leak resources - if self.write_cmd_str("(exit)").is_err() { + if self.write_cmd(None, &SmtCommand::Exit).is_err() { if self.has_error { return; } else { @@ -217,36 +242,19 @@ impl Drop 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)) + self.write_cmd(None, &SmtCommand::SetLogic(logic)) } fn assert(&mut self, ctx: &Context, e: ExprRef) -> Result<()> { - 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, ")") - }) + self.write_cmd(Some(ctx), &SmtCommand::Assert(e)) } fn declare_const(&mut self, ctx: &Context, symbol: ExprRef) -> Result<()> { - todo!( - "we should change hoow write_cmd works to take &str and a list of expressions or types" - ) + self.write_cmd(Some(ctx), &SmtCommand::DeclareConst(symbol)) } fn define_const(&mut self, ctx: &Context, symbol: ExprRef, expr: ExprRef) -> Result<()> { - todo!() + self.write_cmd(Some(ctx), &SmtCommand::DefineConst(symbol, expr)) } fn check_sat_assuming( @@ -255,41 +263,24 @@ impl Solver for SmtLibSolver { props: impl IntoIterator, ) -> Result { 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.write_cmd(Some(ctx), &SmtCommand::CheckSatAssuming(props))?; self.read_sat_response() } fn check_sat(&mut self) -> Result { - self.write_cmd_str("(check-sat)")?; + self.write_cmd(None, &SmtCommand::CheckSat)?; self.read_sat_response() } fn push(&mut self) -> Result<()> { - self.write_cmd_str("(push 1)")?; + self.write_cmd(None, &SmtCommand::Push(1))?; self.stack_depth += 1; Ok(()) } fn pop(&mut self) -> Result<()> { if self.stack_depth > 0 { - self.write_cmd_str("(pop 1)")?; + self.write_cmd(None, &SmtCommand::Pop(1))?; self.stack_depth -= 1; Ok(()) } else { @@ -328,7 +319,7 @@ mod tests { use super::*; #[test] - fn test_bitwuzla() { + fn test_bitwuzla_error() { let mut ctx = Context::default(); let replay = Some(std::fs::File::create("replay.smt").unwrap()); let mut solver = SmtLibSolver::bitwuzla(replay).unwrap(); @@ -337,6 +328,19 @@ mod tests { solver.assert(&ctx, e).unwrap(); let res = solver.check_sat(); assert!(res.is_err(), "a was not declared!"); + // after this error, the solver is dead and won't respond! + let res = solver.declare_const(&ctx, a); + assert!(res.is_err()); + } + + #[test] + fn test_bitwuzla() { + let mut ctx = Context::default(); + let a = ctx.bv_symbol("a", 3); + let e = ctx.build(|c| c.equal(a, c.bit_vec_val(3, 3))); + + let replay = Some(std::fs::File::create("replay.smt").unwrap()); + let mut solver = SmtLibSolver::bitwuzla(replay).unwrap(); solver.declare_const(&ctx, a).unwrap(); let res = solver.check_sat(); assert_eq!(res.unwrap(), CheckSatResponse::Sat);