Skip to content

Commit

Permalink
Add location information to check_sat calls
Browse files Browse the repository at this point in the history
  • Loading branch information
@Alasdair
Alasdair committed Jul 1, 2024
1 parent ee4743c commit 4ead56d
Show file tree
Hide file tree
Showing 8 changed files with 25 additions and 25 deletions.
2 changes: 1 addition & 1 deletion isla-axiomatic/src/page_table.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -984,7 +984,7 @@ impl<B: BV> CustomRegion<B> for ImmutablePageTables<B> {
(_, _) => return Err(ExecError::BadWrite("ill-typed descriptor")),
};

if skip_sat_check || solver.check_sat_with(&query) == SmtResult::Sat {
if skip_sat_check || solver.check_sat_with(&query, SourceLoc::unknown()) == SmtResult::Sat {
let value = solver.declare_const(Ty::Bool, SourceLoc::unknown());
solver.add_event(Event::WriteMem {
value,
Expand Down
2 changes: 1 addition & 1 deletion isla-axiomatic/src/page_table/setup.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1068,7 +1068,7 @@ fn eval_address_constraints<B: BV>(
}
}

if solver.check_sat() != Sat {
if solver.check_sat(SourceLoc::unknown()) != Sat {
return Err(AddressError("No satisfiable set of addresses".to_string()));
}

Expand Down
16 changes: 8 additions & 8 deletions isla-lib/src/executor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -738,7 +738,7 @@ pub fn reset_registers<'ir, B: BV>(
solver.add_event(Event::Assume(constraint.clone()));
solver.add(Def::Assert(assertion_exp));
}
if solver.check_sat().is_unsat()? {
if solver.check_sat(info).is_unsat()? {
return Err(ExecError::InconsistentRegisterReset);
}
}
Expand Down Expand Up @@ -1060,8 +1060,8 @@ fn run_loop<'ir, 'task, B: BV>(

let test_true = Var(v);
let test_false = Not(Box::new(Var(v)));
let can_be_true = solver.check_sat_with(&test_true).is_sat()?;
let can_be_false = solver.check_sat_with(&test_false).is_sat()?;
let can_be_true = solver.check_sat_with(&test_true, *info).is_sat()?;
let can_be_false = solver.check_sat_with(&test_false, *info).is_sat()?;

if can_be_true && can_be_false {
if_logging!(log::FORK, {
Expand Down Expand Up @@ -1219,7 +1219,7 @@ fn run_loop<'ir, 'task, B: BV>(
solver.check_sat_with(&smtlib::Exp::Eq(
Box::new(smtlib::Exp::Var(var)),
Box::new(smtlib::Exp::Bool(false)),
)) == SmtResult::Unsat
), *info) == SmtResult::Unsat
}
Val::Bool(b) => b,
_ => panic!("TODO"),
Expand Down Expand Up @@ -1341,7 +1341,7 @@ fn run_loop<'ir, 'task, B: BV>(
let sym = solver.declare_const(BitVec(len), *info);
solver.assert_eq(Var(v), Var(sym));

if solver.check_sat().is_unsat()? {
if solver.check_sat(*info).is_unsat()? {
return Ok(Run::Dead);
}

Expand Down Expand Up @@ -1777,7 +1777,7 @@ pub fn all_unsat_collector<'ir, B: BV>(
use smtlib::Def::*;
use smtlib::Exp::*;
solver.add(Assert(Not(Box::new(Var(v)))));
if solver.check_sat() != SmtResult::Unsat {
if solver.check_sat(SourceLoc::unknown()) != SmtResult::Unsat {
log_from!(tid, log::VERBOSE, "Got sat");
collected.store(false, Ordering::Release)
} else {
Expand Down Expand Up @@ -1879,7 +1879,7 @@ pub fn trace_collector<'ir, B: BV>(
for (f, pc) in backtrace.iter().rev() {
log_from!(tid, log::VERBOSE, format!(" {} @ {}", shared_state.symtab.to_str(*f), pc));
}
if solver.check_sat() == SmtResult::Sat {
if solver.check_sat(SourceLoc::unknown()) == SmtResult::Sat {
let model = Model::new(&solver);
collected.push(Err(TraceError::exec_model(err, model)))
} else {
Expand All @@ -1905,7 +1905,7 @@ pub fn trace_value_collector<'ir, B: BV>(
Ok((Run::Exit | Run::Suspended, _)) => (),
Ok((Run::Dead, _)) => (),
Err((err, _)) => {
if solver.check_sat() == SmtResult::Sat {
if solver.check_sat(SourceLoc::unknown()) == SmtResult::Sat {
let model = Model::new(&solver);
collected.push(Err(TraceError::exec_model(err, model)))
} else {
Expand Down
4 changes: 2 additions & 2 deletions isla-lib/src/memory.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -398,7 +398,7 @@ impl<B: BV> Memory<B> {

if let Some(r) = region_constraints.pop() {
let constraint = region_constraints.drain(..).fold(r, |r1, r2| Or(Box::new(r1), Box::new(r2)));
match solver.check_sat_with(&constraint) {
match solver.check_sat_with(&constraint, SourceLoc::unknown()) {
Sat => {
let sat_address = {
let mut model = Model::new(solver);
Expand All @@ -415,7 +415,7 @@ impl<B: BV> Memory<B> {
// case the caller could choose to treat it as a
// concrete value.
let uniqueness_constraint = Neq(Box::new(Var(address)), Box::new(Bits64(sat_address)));
match solver.check_sat_with(&uniqueness_constraint) {
match solver.check_sat_with(&uniqueness_constraint, SourceLoc::unknown()) {
Unsat => Ok(Overlap::Unique(sat_address.lower_u64())),
Unknown => Err(ExecError::Z3Unknown),
Sat => {
Expand Down
4 changes: 2 additions & 2 deletions isla-lib/src/primop.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,7 @@ fn optimistic_assert<B: BV>(
match x {
Val::Symbolic(v) => {
let test_true = Box::new(Exp::Var(v));
let can_be_true = solver.check_sat_with(&test_true).is_sat()?;
let can_be_true = solver.check_sat_with(&test_true, info).is_sat()?;
if can_be_true {
solver.add(Def::Assert(Exp::Var(v)));
Ok(Val::Unit)
Expand Down Expand Up @@ -212,7 +212,7 @@ fn pessimistic_assert<B: BV>(
match x {
Val::Symbolic(v) => {
let test_false = Exp::Not(Box::new(Exp::Var(v)));
let can_be_false = solver.check_sat_with(&test_false).is_sat()?;
let can_be_false = solver.check_sat_with(&test_false, info).is_sat()?;
if can_be_false {
Err(ExecError::AssertionFailure(message, info))
} else {
Expand Down
10 changes: 5 additions & 5 deletions isla-lib/src/simplify.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -964,22 +964,22 @@ pub fn eval_carefully_part<B: BV, E: BorrowMut<Event<B>>>(
Event::Smt(Def::DeclareFun(v, arg_tys, result_ty), _, _) => {
ftcx.to_mut().insert(*v, (arg_tys.clone(), result_ty.clone()));
}
Event::Smt(Def::DefineConst(v, exp), _, l) => {
Event::Smt(Def::DefineConst(v, exp), _, info) => {
let e = std::mem::replace(exp, Exp::Bool(false));
*exp = e.clone().eval();
match solver.check_sat_with(&Exp::Neq(Box::new(exp.clone()), Box::new(e.clone()))) {
match solver.check_sat_with(&Exp::Neq(Box::new(exp.clone()), Box::new(e.clone())), *info) {
Sat => panic!("Bad eval {:?} to {:?}", e, exp),
Unknown => panic!("Difficult to check eval (!) {:?} to {:?}", e, exp),
Unsat => (),
};
let ty = exp.infer(&tcx, &ftcx).unwrap();
solver.add_with_location(Def::DeclareConst(*v, ty.clone()), *l);
solver.add_with_location(Def::DeclareConst(*v, ty.clone()), *info);
tcx.to_mut().insert(*v, ty);
}
Event::Smt(Def::Assert(exp), _, _) => {
Event::Smt(Def::Assert(exp), _, info) => {
let e = std::mem::replace(exp, Exp::Bool(false));
*exp = e.clone().eval();
match solver.check_sat_with(&Exp::Neq(Box::new(exp.clone()), Box::new(e.clone()))) {
match solver.check_sat_with(&Exp::Neq(Box::new(exp.clone()), Box::new(e.clone())), *info) {
Sat => panic!("Bad eval {:?} to {:?}", e, exp),
Unknown => panic!("Difficult to check eval (!) {:?} to {:?}", e, exp),
Unsat => (),
Expand Down
8 changes: 4 additions & 4 deletions isla-lib/src/smt.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1835,7 +1835,7 @@ impl<'ctx, B: BV> Solver<'ctx, B> {
solver
}

pub fn check_sat_with(&mut self, exp: &Exp<Sym>) -> SmtResult {
pub fn check_sat_with(&mut self, exp: &Exp<Sym>, _info: SourceLoc) -> SmtResult {
let ast = self.translate_exp(exp);
unsafe {
let result = Z3_solver_check_assumptions(self.ctx.z3_ctx, self.z3_solver, 1, &ast.z3_ast);
Expand All @@ -1853,7 +1853,7 @@ impl<'ctx, B: BV> Solver<'ctx, B> {
&self.trace
}

pub fn check_sat(&mut self) -> SmtResult {
pub fn check_sat(&mut self, _info: SourceLoc) -> SmtResult {
unsafe {
let result = Z3_solver_check(self.ctx.z3_ctx, self.z3_solver);
if result == Z3_L_TRUE {
Expand Down Expand Up @@ -1954,7 +1954,7 @@ mod tests {
let ctx = Context::new(cfg);
let mut solver = Solver::<B64>::new(&ctx);
solver.add(Assert(Eq(Box::new(bv!("0110")), Box::new(bv!("1001")))));
assert!(solver.check_sat() == Unsat);
assert!(solver.check_sat(SourceLoc::unknown()) == Unsat);
}

#[test]
Expand All @@ -1972,7 +1972,7 @@ mod tests {
solver.add(Assert(Eq(Box::new(var(2)), Box::new(var(3)))));
let big_bv = Box::new(SignExtend(251, Box::new(Bits(vec![true, false, false, true, false, true]))));
solver.add(Assert(Eq(Box::new(var(4)), big_bv)));
assert!(solver.check_sat() == Sat);
assert!(solver.check_sat(SourceLoc::unknown()) == Sat);
let (v0, v2, v3, v4);
{
let mut model = Model::new(&solver);
Expand Down
4 changes: 2 additions & 2 deletions src/execute-function.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -310,7 +310,7 @@ fn model_collector<'ir, B: BV>(
let events: Vec<Event<B>> = if *trace { solver.trace().to_vec().drain(..).cloned().collect() } else { vec![] };
match result {
Ok((Run::Finished(val), _)) => {
if solver.check_sat() == SmtResult::Sat {
if solver.check_sat(SourceLoc::unknown()) == SmtResult::Sat {
let val = if *models {
let mut model = Model::new(&solver);
concrete_value(&mut model, &val)
Expand All @@ -330,7 +330,7 @@ fn model_collector<'ir, B: BV>(
for (f, pc) in backtrace.iter().rev() {
log_from!(tid, log::VERBOSE, format!(" {} @ {}", shared_state.symtab.to_str(*f), pc));
}
if solver.check_sat() == SmtResult::Sat {
if solver.check_sat(SourceLoc::unknown()) == SmtResult::Sat {
let model = Model::new(&solver);
collected.push(Err((format!("Error {:?}\n{:?}", err, model), events)))
} else {
Expand Down

0 comments on commit 4ead56d

Please sign in to comment.