diff --git a/isla-axiomatic/src/page_table.rs b/isla-axiomatic/src/page_table.rs index 3fcd08d..e5dcc49 100644 --- a/isla-axiomatic/src/page_table.rs +++ b/isla-axiomatic/src/page_table.rs @@ -1266,18 +1266,24 @@ mod tests { tables.get_mut(l1)[va.level_index(1)] = Desc::new_table(l2); tables.get_mut(l0)[va.level_index(0)] = Desc::new_table(l1); - assert_eq!(Sat, solver.check_sat()); + assert_eq!(Sat, solver.check_sat(SourceLoc::unknown())); // Translate our concrete virtual address to a symbolic // physical address, and check it could be in either page if let Some(pa) = simple_translation_table_walk(&tables, l0, va, &mut solver) { - assert_eq!(Sat, solver.check_sat_with(&Eq(Box::new(Var(pa)), Box::new(bits64(0x8000_0EEF, 64))))); - assert_eq!(Sat, solver.check_sat_with(&Eq(Box::new(Var(pa)), Box::new(bits64(0x8000_1EEF, 64))))); + assert_eq!( + Sat, + solver.check_sat_with(&Eq(Box::new(Var(pa)), Box::new(bits64(0x8000_0EEF, 64))), SourceLoc::unknown()) + ); + assert_eq!( + Sat, + solver.check_sat_with(&Eq(Box::new(Var(pa)), Box::new(bits64(0x8000_1EEF, 64))), SourceLoc::unknown()) + ); // Additionally, it can't be anything other than those two addresses solver.add(Assert(Neq(Box::new(Var(pa)), Box::new(bits64(0x8000_0EEF, 64))))); solver.add(Assert(Neq(Box::new(Var(pa)), Box::new(bits64(0x8000_1EEF, 64))))); - assert_eq!(Unsat, solver.check_sat()); + assert_eq!(Unsat, solver.check_sat(SourceLoc::unknown())); } else { panic!("simple_translation_table_walk failed") } diff --git a/isla-lib/src/executor.rs b/isla-lib/src/executor.rs index 4bf881b..986240b 100644 --- a/isla-lib/src/executor.rs +++ b/isla-lib/src/executor.rs @@ -1226,10 +1226,13 @@ fn run_loop<'ir, 'task, B: BV>( primop::eq_anything(req.clone(), arg.clone(), solver, *info) .map(|v| match v { Val::Symbolic(var) => { - solver.check_sat_with(&smtlib::Exp::Eq( - Box::new(smtlib::Exp::Var(var)), - Box::new(smtlib::Exp::Bool(false)), - ), *info) == SmtResult::Unsat + solver.check_sat_with( + &smtlib::Exp::Eq( + Box::new(smtlib::Exp::Var(var)), + Box::new(smtlib::Exp::Bool(false)), + ), + *info, + ) == SmtResult::Unsat } Val::Bool(b) => b, _ => panic!("TODO"), diff --git a/isla-lib/src/ir.rs b/isla-lib/src/ir.rs index b622f80..52cf568 100644 --- a/isla-lib/src/ir.rs +++ b/isla-lib/src/ir.rs @@ -284,7 +284,7 @@ impl Val { SymbolicCtor(discriminant, vals) => { vars.insert(*discriminant); vals.iter().for_each(|(_, val)| val.collect_symbolic_variables(vars)) - }, + } } } diff --git a/isla-lib/src/primop.rs b/isla-lib/src/primop.rs index 2951ab5..0deed22 100644 --- a/isla-lib/src/primop.rs +++ b/isla-lib/src/primop.rs @@ -2750,7 +2750,7 @@ mod tests { SourceLoc::unknown(), ); - assert!(solver.check_sat() == SmtResult::Sat); + assert!(solver.check_sat(SourceLoc::unknown()) == SmtResult::Sat); Ok(()) } } diff --git a/isla-lib/src/smt.rs b/isla-lib/src/smt.rs index 8979ab8..023a1fd 100644 --- a/isla-lib/src/smt.rs +++ b/isla-lib/src/smt.rs @@ -42,12 +42,16 @@ use libc::{c_int, c_uint}; use serde::{Deserialize, Serialize}; #[cfg(feature = "smtperf")] -use petgraph::{Directed, graph::{Graph, NodeIndex}, visit::Dfs}; +use petgraph::{ + graph::{Graph, NodeIndex}, + visit::Dfs, + Directed, +}; use z3_sys::*; #[cfg(feature = "smtperf")] -use std::time::{Instant, Duration}; +use std::time::{Duration, Instant}; use std::collections::{HashMap, HashSet}; use std::convert::TryInto; @@ -304,7 +308,6 @@ impl Event { if let Some(tag_value) = tag_value { tag_value.collect_symbolic_variables(vars) } - } _ => (), } @@ -772,9 +775,12 @@ impl<'ctx> Ast<'ctx> { fn simplify(&mut self) { unsafe { let z3_params = Z3_mk_params(self.ctx.z3_ctx); - let push_ite_bv = Z3_mk_string_symbol(self.ctx.z3_ctx, CStr::from_bytes_with_nul_unchecked(PUSH_ITE_BV).as_ptr()); - let bv_le_extra = Z3_mk_string_symbol(self.ctx.z3_ctx, CStr::from_bytes_with_nul_unchecked(BV_LE_EXTRA).as_ptr()); - let bv_sort_ac = Z3_mk_string_symbol(self.ctx.z3_ctx, CStr::from_bytes_with_nul_unchecked(BV_SORT_AC).as_ptr()); + let push_ite_bv = + Z3_mk_string_symbol(self.ctx.z3_ctx, CStr::from_bytes_with_nul_unchecked(PUSH_ITE_BV).as_ptr()); + let bv_le_extra = + Z3_mk_string_symbol(self.ctx.z3_ctx, CStr::from_bytes_with_nul_unchecked(BV_LE_EXTRA).as_ptr()); + let bv_sort_ac = + Z3_mk_string_symbol(self.ctx.z3_ctx, CStr::from_bytes_with_nul_unchecked(BV_SORT_AC).as_ptr()); Z3_params_inc_ref(self.ctx.z3_ctx, z3_params); Z3_params_set_bool(self.ctx.z3_ctx, z3_params, push_ite_bv, true); Z3_params_set_bool(self.ctx.z3_ctx, z3_params, bv_le_extra, true); @@ -1261,7 +1267,6 @@ impl<'ctx> Drop for Ast<'ctx> { #[cfg(not(feature = "smtperf"))] struct PerformanceInfo {} - #[cfg(feature = "smtperf")] struct PerformanceInfo { vars: Graph<(Sym, SourceLoc), (), Directed>, @@ -1344,8 +1349,8 @@ impl PerformanceInfo { // Remove the edges and dummy root we added for edge in edges { - self.vars.remove_edge(edge); - } + self.vars.remove_edge(edge); + } self.vars.remove_node(root); } @@ -1368,10 +1373,16 @@ impl PerformanceInfo { for (n, (info, duration)) in times.iter().enumerate() { if n >= 10 { - break + break; } - msg += &info.message(dir.as_ref(), files, &format!("#{} time: {}ms", n + 1, duration.as_millis()), false, true); + msg += &info.message( + dir.as_ref(), + files, + &format!("#{} time: {}ms", n + 1, duration.as_millis()), + false, + true, + ); msg += "\n" } @@ -1386,6 +1397,7 @@ impl PerformanceInfo { /// For example: /// ``` /// # use isla_lib::bitvector::b64::B64; +/// # use isla_lib::source_loc::SourceLoc; /// # use isla_lib::smt::smtlib::Exp::*; /// # use isla_lib::smt::smtlib::Def::*; /// # use isla_lib::smt::smtlib::*; @@ -1399,7 +1411,7 @@ impl PerformanceInfo { /// // (assert v0) /// solver.add(Assert(Var(x))); /// // (check-sat) -/// assert!(solver.check_sat() == SmtResult::Sat) +/// assert!(solver.check_sat(SourceLoc::unknown()) == SmtResult::Sat) /// ``` /// /// The other thing the Solver type does is maintain a trace of @@ -1410,6 +1422,7 @@ impl PerformanceInfo { /// For example: /// ``` /// # use isla_lib::bitvector::b64::B64; +/// # use isla_lib::source_loc::SourceLoc; /// # use isla_lib::smt::smtlib::Exp::*; /// # use isla_lib::smt::smtlib::Def::*; /// # use isla_lib::smt::smtlib::*; @@ -1427,7 +1440,7 @@ impl PerformanceInfo { /// let cfg = Config::new(); /// let ctx = Context::new(cfg); /// let mut solver = Solver::from_checkpoint(&ctx, point); -/// assert!(solver.check_sat() == SmtResult::Unsat); +/// assert!(solver.check_sat(SourceLoc::unknown()) == SmtResult::Unsat); pub struct Solver<'ctx, B> { trace: Trace, next_var: u32, @@ -1456,6 +1469,7 @@ impl<'ctx, B> Drop for Solver<'ctx, B> { /// /// ``` /// # use isla_lib::bitvector::b64::B64; +/// # use isla_lib::source_loc::SourceLoc; /// # use isla_lib::smt::smtlib::Exp::*; /// # use isla_lib::smt::smtlib::Def::*; /// # use isla_lib::smt::smtlib::*; @@ -1467,7 +1481,7 @@ impl<'ctx, B> Drop for Solver<'ctx, B> { /// let mut solver = Solver::::new(&ctx); /// solver.add(DeclareConst(x, Ty::BitVec(4))); /// solver.add(Assert(Bvsgt(Box::new(Var(x)), Box::new(Bits(vec![false,false,true,false]))))); -/// assert!(solver.check_sat() == SmtResult::Sat); +/// assert!(solver.check_sat(SourceLoc::unknown()) == SmtResult::Sat); /// let mut model = Model::new(&solver); /// let var0 = model.get_var(x).unwrap().unwrap(); /// ``` @@ -1878,7 +1892,7 @@ impl<'ctx, B: BV> Solver<'ctx, B> { for used in exp.variables().iter() { self.performance_info.add_var_edge(v, used); self.performance_info.add_var_edge(used, v) - }; + } } let mut ast = self.translate_exp(exp); ast.simplify(); @@ -2267,7 +2281,7 @@ mod tests { solver.add(Assert(Eq(Box::new(var(2)), Box::new(v2)))); solver.add(Assert(Eq(Box::new(var(3)), Box::new(v3)))); solver.add(Assert(Eq(Box::new(var(4)), Box::new(v4)))); - match solver.check_sat() { + match solver.check_sat(SourceLoc::unknown()) { Sat => (), _ => panic!("Round-trip failed, trace {:?}", solver.trace()), } @@ -2284,7 +2298,7 @@ mod tests { let v1 = solver.declare_const(Ty::Enum(e), SourceLoc::unknown()); let v2 = solver.declare_const(Ty::Enum(e), SourceLoc::unknown()); solver.assert_eq(Var(v0), Var(v1)); - assert!(solver.check_sat() == Sat); + assert!(solver.check_sat(SourceLoc::unknown()) == Sat); let (m0, m1) = { let mut model = Model::new(&solver); assert!(model.get_var(v2).unwrap().is_none()); @@ -2292,7 +2306,7 @@ mod tests { }; solver.assert_eq(Var(v0), m0); solver.assert_eq(Var(v1), m1); - match solver.check_sat() { + match solver.check_sat(SourceLoc::unknown()) { Sat => (), _ => panic!("Round-trip failed, trace {:?}", solver.trace()), } @@ -2311,7 +2325,7 @@ mod tests { .add(Assert(Eq(Box::new(App(Sym::from_u32(0), vec![bv!("10"), bv!("0110")])), Box::new(bv!("01011011"))))); solver.add(Assert(Eq(Box::new(App(Sym::from_u32(0), vec![var(2), bv!("0110")])), Box::new(var(1))))); solver.add(Assert(Eq(Box::new(var(2)), Box::new(bv!("10"))))); - assert!(solver.check_sat() == Sat); + assert!(solver.check_sat(SourceLoc::unknown()) == Sat); let mut model = Model::new(&solver); let val = model.get_var(Sym::from_u32(1)).unwrap().unwrap(); assert!(match val { @@ -2334,6 +2348,6 @@ mod tests { )), Box::new(bv!("0101")), ))); - assert!(solver.check_sat() == Unsat); + assert!(solver.check_sat(SourceLoc::unknown()) == Unsat); } } diff --git a/isla-lib/src/smt/smtlib.rs b/isla-lib/src/smt/smtlib.rs index a7ae406..d54f14b 100644 --- a/isla-lib/src/smt/smtlib.rs +++ b/isla-lib/src/smt/smtlib.rs @@ -1143,6 +1143,7 @@ mod tests { use super::Exp::*; use super::*; use crate::smt::{Config, Context, Solver, Unsat}; + use crate::source_loc::SourceLoc; #[test] fn bits_to_i128_test() { @@ -1159,7 +1160,7 @@ mod tests { let post_eval = exp.clone().eval(); assert_ne!(exp, post_eval); solver.add(Assert(Neq(Box::new(exp.clone()), Box::new(post_eval.clone())))); - assert_eq!(solver.check_sat(), Unsat, "Mismatch {:?} and {:?}", exp, post_eval); + assert_eq!(solver.check_sat(SourceLoc::unknown()), Unsat, "Mismatch {:?} and {:?}", exp, post_eval); } fn exp_eval_unchanged(exp: Exp) { diff --git a/isla-lib/src/source_loc.rs b/isla-lib/src/source_loc.rs index c47fef7..2bf7e23 100644 --- a/isla-lib/src/source_loc.rs +++ b/isla-lib/src/source_loc.rs @@ -264,8 +264,11 @@ impl SourceLoc { let blue = if use_colors { BLUE } else { "" }; let no_color = if use_colors { NO_COLOR } else { "" }; - let (short_error, error_sep) = - if is_error { (format!("{}error{}: {}", red, no_color, message), "\n") } else { (message.to_string(), "\n") }; + let (short_error, error_sep) = if is_error { + (format!("{}error{}: {}", red, no_color, message), "\n") + } else { + (message.to_string(), "\n") + }; let file = TryInto::::try_into(self.file).ok().and_then(|i| files.get(i)); if file.is_none() { diff --git a/src/axiomatic.rs b/src/axiomatic.rs index b1aee5e..6f66fdb 100644 --- a/src/axiomatic.rs +++ b/src/axiomatic.rs @@ -75,8 +75,7 @@ fn main() { process::exit(code) } -type FinalState = - HashMap, Val>; +type FinalState = HashMap, Val>; #[derive(Debug)] enum AxResult {