diff --git a/src/engine.rs b/src/engine.rs index 6e9e84fb..3e7b16de 100644 --- a/src/engine.rs +++ b/src/engine.rs @@ -616,26 +616,38 @@ where self.symbolic_state .create_beq_path_condition(decision, lhs, rhs); - trace!( - "[{:#010x}] beq: x{}, x{} |- assume {}, pc <- {:#x}", - self.pc, - lhs.index(), - rhs.index(), - next_pc == false_branch, - next_pc, - ); + if let Ok(Some(_)) = self.symbolic_state.execute_query(Query::Reachable) { + trace!( + "[{:#010x}] beq: x{}, x{} |- assume {}, pc <- {:#x}", + self.pc, + lhs.index(), + rhs.index(), + next_pc == false_branch, + next_pc, + ); - self.pc = next_pc; + self.pc = next_pc; - let result = self.run(); + let result = self.run(); - if !matches!( - result, - Err(EngineError::ExecutionDepthReached(_)) | Ok(None) - ) { - return result; + if !matches!( + result, + Err(EngineError::ExecutionDepthReached(_)) | Ok(None) + ) { + return result; + } + } else { + trace!( + "[{:#010x}] beq: x{}, x{} |- assume {}, not reachable", + self.pc, + lhs.index(), + rhs.index(), + next_pc == false_branch, + ); } + let next_pc = if decision { false_branch } else { true_branch }; + self.is_running = true; self.memory = memory_snapshot; @@ -644,23 +656,35 @@ where self.program_break = brk_snapshot; self.execution_depth = execution_depth_snapshot; - let next_pc = if decision { false_branch } else { true_branch }; - self.symbolic_state .create_beq_path_condition(!decision, lhs, rhs); - trace!( - "[{:#010x}] beq: x{}, x{} |- assume {}, pc <- {:#x}", - self.pc, - lhs.index(), - rhs.index(), - next_pc == false_branch, - next_pc, - ); + if let Ok(Some(_)) = self.symbolic_state.execute_query(Query::Reachable) { + trace!( + "[{:#010x}] beq: x{}, x{} |- assume {}, pc <- {:#x}", + self.pc, + lhs.index(), + rhs.index(), + next_pc == false_branch, + next_pc, + ); - self.pc = next_pc; + self.pc = next_pc; - Ok(None) + Ok(None) + } else { + trace!( + "[{:#010x}] beq: x{}, x{} |- assume {}, not reachable", + self.pc, + lhs.index(), + rhs.index(), + next_pc == false_branch, + ); + + self.is_running = false; + + Ok(None) + } } fn execute_beq(&mut self, btype: BType) -> Result, EngineError> { diff --git a/src/solver/boolector.rs b/src/solver/boolector.rs index 7fdbce7e..404e6f27 100644 --- a/src/solver/boolector.rs +++ b/src/solver/boolector.rs @@ -50,14 +50,19 @@ impl Solver for Boolector { SolverResult::Sat => { let assignments = graph .node_indices() - .map(|i| { - let bv = bvs.get(&i).expect("every input must be part of bvs"); - - BitVector( - bv.get_a_solution() - .as_u64() - .expect("BV always fits in 64 bits for our machine"), - ) + .filter_map(|i| { + if let Some(bv) = bvs.get(&i) { + Some(( + i, + BitVector( + bv.get_a_solution() + .as_u64() + .expect("BV always fits in 64 bits for our machine"), + ), + )) + } else { + None + } }) .collect(); diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 88e8edcb..4f395a1f 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -10,10 +10,10 @@ use crate::{ symbolic_state::{Formula, SymbolId}, }; use log::debug; -use std::{convert::From, io}; +use std::{collections::HashMap, convert::From, io}; use thiserror::Error; -pub type Assignment = Vec; +pub type Assignment = HashMap; pub trait Solver: Default { fn name() -> &'static str; diff --git a/src/solver/monster.rs b/src/solver/monster.rs index 45f3a9b1..f288d9e6 100644 --- a/src/solver/monster.rs +++ b/src/solver/monster.rs @@ -108,7 +108,7 @@ fn is_leaf(formula: &Formula, idx: SymbolId) -> bool { // initialize bit vectors with a consistent intial assignment to the formula // inputs are initialized with random values -fn initialize_ab(formula: &Formula) -> Assignment { +fn initialize_ab(formula: &Formula) -> Vec { // Initialize values for all input/const nodes let mut ab = formula .node_indices() @@ -116,7 +116,7 @@ fn initialize_ab(formula: &Formula) -> Assignment { Node::Constant(c) => BitVector(c), _ => BitVector(random::()), }) - .collect::>(); + .collect::>(); if log_enabled!(Level::Trace) { formula @@ -457,7 +457,7 @@ fn get_operand(f: &Formula, n: SymbolId) -> SymbolId { .source() } -fn update_assignment(f: &Formula, ab: &mut Assignment, n: SymbolId, v: BitVector) { +fn update_assignment(f: &Formula, ab: &mut Vec, n: SymbolId, v: BitVector) { ab[n.index()] = v; assert!( @@ -471,8 +471,8 @@ fn update_assignment(f: &Formula, ab: &mut Assignment, n: SymbolId, v .for_each(|n| propagate_assignment(f, ab, n)); } -fn propagate_assignment(f: &Formula, ab: &mut Assignment, n: SymbolId) { - fn update_binary(f: &Formula, ab: &mut Assignment, n: SymbolId, s: &str, op: Op) +fn propagate_assignment(f: &Formula, ab: &mut Vec, n: SymbolId) { + fn update_binary(f: &Formula, ab: &mut Vec, n: SymbolId, s: &str, op: Op) where Op: FnOnce(BitVector, BitVector) -> BitVector, { @@ -497,7 +497,7 @@ fn propagate_assignment(f: &Formula, ab: &mut Assignment, n: SymbolId } } - fn update_unary(f: &Formula, ab: &mut Assignment, n: SymbolId, s: &str, op: Op) + fn update_unary(f: &Formula, ab: &mut Vec, n: SymbolId, s: &str, op: Op) where Op: FnOnce(BitVector) -> BitVector, { @@ -562,7 +562,7 @@ fn propagate_assignment(f: &Formula, ab: &mut Assignment, n: SymbolId fn sat( formula: &Formula, root: SymbolId, - mut ab: Assignment, + mut ab: Vec, timeout_time: Duration, ) -> Result>, SolverError> { let mut iterations = 0; @@ -640,7 +640,9 @@ fn sat( update_assignment(formula, &mut ab, n, t); } - Ok(Some(ab)) + let assignment: Assignment<_> = formula.node_indices().map(|i| (i, ab[i.index()])).collect(); + + Ok(Some(assignment)) } #[cfg(test)] @@ -692,7 +694,7 @@ mod tests { "has result for trivial equals constrain" ); assert_eq!( - unwrapped_result.unwrap()[input_idx.index()], + *unwrapped_result.unwrap().get(&input_idx).unwrap(), BitVector(10), "solver result of trivial equal constrain has right value" ); @@ -721,7 +723,7 @@ mod tests { assert!(unwrapped_result.is_some(), "has result for trivial add op"); assert_eq!( - unwrapped_result.unwrap()[input_idx.index()], + *unwrapped_result.unwrap().get(&input_idx).unwrap(), BitVector(7), "solver result of trivial add op has right value" ); diff --git a/src/solver/z3.rs b/src/solver/z3.rs index 9414048c..6369c21e 100644 --- a/src/solver/z3.rs +++ b/src/solver/z3.rs @@ -57,7 +57,10 @@ impl Solver for Z3 { Ok(Some( graph .node_indices() - .map(|i| bv_for_node_idx(i, translation, &model)) + .filter_map(|i| match bv_for_node_idx(i, translation, &model) { + Some(bv) => Some((i, bv)), + None => None, + }) .collect(), )) } @@ -71,33 +74,33 @@ fn bv_for_node_idx<'ctx>( i: SymbolId, translation: &HashMap>, m: &Model, -) -> BitVector { - let ast_node = translation - .get(&i) - .expect("input BV must be always assigned something once solved"); - - if let Some(bv) = ast_node.as_bv() { - let concrete_bv = m - .eval(&bv) - .expect("will always get a result because the formula is SAT"); - - let result_value = concrete_bv.as_u64().expect("type already checked here"); - - BitVector(result_value) - } else if let Some(b) = ast_node.as_bool() { - let concrete_bool = m - .eval(&b) - .expect("will always get a result because the formula is SAT"); - - let result_value = concrete_bool.as_bool().expect("type already checked here"); - - if result_value { - BitVector(1) +) -> Option { + if let Some(ast_node) = translation.get(&i) { + if let Some(bv) = ast_node.as_bv() { + let concrete_bv = m + .eval(&bv) + .expect("will always get a result because the formula is SAT"); + + let result_value = concrete_bv.as_u64().expect("type already checked here"); + + Some(BitVector(result_value)) + } else if let Some(b) = ast_node.as_bool() { + let concrete_bool = m + .eval(&b) + .expect("will always get a result because the formula is SAT"); + + let result_value = concrete_bool.as_bool().expect("type already checked here"); + + Some(if result_value { + BitVector(1) + } else { + BitVector(0) + }) } else { - BitVector(0) + panic!("only inputs of type BV and Bool are allowed"); } } else { - panic!("only inputs of type BV and Bool are allowed"); + None } } diff --git a/src/symbolic_state.rs b/src/symbolic_state.rs index b3ddfa96..06d122fe 100644 --- a/src/symbolic_state.rs +++ b/src/symbolic_state.rs @@ -377,7 +377,7 @@ where witness } - fn build_witness(&self, root: NodeIndex, assignment: &[BitVector]) -> Witness { + fn build_witness(&self, root: NodeIndex, assignment: &HashMap) -> Witness { let mut visited = HashMap::::new(); let mut witness = Witness::new(); @@ -481,22 +481,41 @@ impl FormulaVisitor for Printer { struct WitnessBuilder<'a> { witness: &'a mut Witness, - assignment: &'a [BitVector], + assignment: &'a HashMap, } impl<'a> FormulaVisitor for WitnessBuilder<'a> { fn input(&mut self, idx: SymbolId, name: &str) -> usize { - self.witness - .add_variable(name, self.assignment[idx.index()]) + self.witness.add_variable( + name, + *self + .assignment + .get(&idx) + .expect("assignment should be available"), + ) } fn constant(&mut self, _idx: SymbolId, v: BitVector) -> usize { self.witness.add_constant(v) } fn unary(&mut self, idx: SymbolId, op: BVOperator, v: usize) -> usize { - self.witness.add_unary(op, v, self.assignment[idx.index()]) + self.witness.add_unary( + op, + v, + *self + .assignment + .get(&idx) + .expect("assignment should be available"), + ) } fn binary(&mut self, idx: SymbolId, op: BVOperator, lhs: usize, rhs: usize) -> usize { - self.witness - .add_binary(lhs, op, rhs, self.assignment[idx.index()]) + self.witness.add_binary( + lhs, + op, + rhs, + *self + .assignment + .get(&idx) + .expect("assignment should be available"), + ) } }