feat: eagerly evaluate PC in BEQ instructions

 - also fix a problem where a panic is created when building a witness

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<Option<Bug>, EngineError> {

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();
 

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<T> = Vec<T>;
+pub type Assignment<T> = HashMap<SymbolId, T>;
 
 pub trait Solver: Default {
     fn name() -> &'static str;

src/solver/monster.rs

@@ -108,15 +108,15 @@ 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<BitVector> {
+fn initialize_ab(formula: &Formula) -> Vec<BitVector> {
     // Initialize values for all input/const nodes
     let mut ab = formula
         .node_indices()
         .map(|i| match formula[i] {
             Node::Constant(c) => BitVector(c),
             _ => BitVector(random::<u64>()),
         })
-        .collect::<Assignment<BitVector>>();
+        .collect::<Vec<BitVector>>();
 
     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<BitVector>, n: SymbolId, v: BitVector) {
+fn update_assignment(f: &Formula, ab: &mut Vec<BitVector>, n: SymbolId, v: BitVector) {
     ab[n.index()] = v;
 
     assert!(
@@ -471,8 +471,8 @@ fn update_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId, v
         .for_each(|n| propagate_assignment(f, ab, n));
 }
 
-fn propagate_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId) {
-    fn update_binary<Op>(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId, s: &str, op: Op)
+fn propagate_assignment(f: &Formula, ab: &mut Vec<BitVector>, n: SymbolId) {
+    fn update_binary<Op>(f: &Formula, ab: &mut Vec<BitVector>, n: SymbolId, s: &str, op: Op)
     where
         Op: FnOnce(BitVector, BitVector) -> BitVector,
     {
@@ -497,7 +497,7 @@ fn propagate_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId
         }
     }
 
-    fn update_unary<Op>(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId, s: &str, op: Op)
+    fn update_unary<Op>(f: &Formula, ab: &mut Vec<BitVector>, n: SymbolId, s: &str, op: Op)
     where
         Op: FnOnce(BitVector) -> BitVector,
     {
@@ -562,7 +562,7 @@ fn propagate_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId
 fn sat(
     formula: &Formula,
     root: SymbolId,
-    mut ab: Assignment<BitVector>,
+    mut ab: Vec<BitVector>,
     timeout_time: Duration,
 ) -> Result<Option<Assignment<BitVector>>, 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"
         );

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<SymbolId, Dynamic<'ctx>>,
     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<BitVector> {
+    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
     }
 }
 

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<SymbolId, BitVector>) -> Witness {
         let mut visited = HashMap::<NodeIndex, usize>::new();
 
         let mut witness = Witness::new();
@@ -481,22 +481,41 @@ impl FormulaVisitor<SymbolId> for Printer {
 
 struct WitnessBuilder<'a> {
     witness: &'a mut Witness,
-    assignment: &'a [BitVector],
+    assignment: &'a HashMap<SymbolId, BitVector>,
 }
 
 impl<'a> FormulaVisitor<usize> 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"),
+        )
     }
 }