Implement SUB in the native solver (#62) (#63)

* Rename `smt` module to `boolector` and fix a bug * Implement SUB in the native solver (#62) - also add to `tests/engine.rs` - fix bug in symbolic read syscall Co-authored-by: finga <[email protected]> Co-authored-by: Alexander Lackner <[email protected]>
cksystemsgroup · Oct 29, 2020 · 22c4a55 · 22c4a55
1 parent 6627bab
commit 22c4a55
Show file tree

Hide file tree

Showing 7 changed files with 52 additions and 21 deletions.
diff --git a/src/smt.rs → src/boolector.rs b/src/smt.rs → src/boolector.rs
@@ -38,11 +38,9 @@ fn traverse<'a>(graph: &Formula, node: NodeIndex, solver: &'a Rc<Btor>) -> BV<Rc
             let (lhs, rhs) = get_operands(graph, node, solver);
 
             match i.instruction {
-                Inst::Sub(_i) => lhs.sub(&rhs),
-                Inst::Addi(_i) => lhs.add(&rhs),
-                Inst::Add(_i) => lhs.add(&rhs),
-                Inst::Mul(_i) => lhs.mul(&rhs),
-                Inst::Sltu(_i) => unimplemented!("fix this"),
+                Inst::Add(_) | Inst::Addi(_) => lhs.add(&rhs),
+                Inst::Sub(_) => lhs.sub(&rhs),
+                Inst::Mul(_) => lhs.mul(&rhs),
                 i => unimplemented!("instruction: {:?}", i),
             }
         }
@@ -60,7 +58,7 @@ fn traverse<'a>(graph: &Formula, node: NodeIndex, solver: &'a Rc<Btor>) -> BV<Rc
     }
 }
 
-pub fn smt(graph: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> {
+pub fn solve(graph: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> {
     let solver = Rc::new(Btor::new());
     solver.set_opt(BtorOption::ModelGen(ModelGen::All));
     solver.set_opt(BtorOption::Incremental(true));
@@ -75,7 +73,18 @@ pub fn smt(graph: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> {
         println!();
 
         // TODO: Extract assignment from boolector
-        Some(vec![])
+
+        let assignments = graph
+            .raw_nodes()
+            .iter()
+            .filter(|n| match n.weight {
+                Input(_) => true,
+                _ => false,
+            })
+            .map(|_| BitVector(0))
+            .collect::<Vec<_>>();
+
+        Some(assignments)
     } else {
         None
     }

diff --git a/src/engine.rs b/src/engine.rs
@@ -1,10 +1,11 @@
 use crate::{
     bitvec::BitVector,
+    boolector,
     candidate_path::create_candidate_paths,
     cfg::build_cfg_from_file,
     elf::ElfMetadata,
     formula_graph::{self, build_dataflow_graph, ExecutionResult, Formula},
-    smt, solver,
+    solver,
 };
 use riscv_decode::Instruction;
 use std::{collections::HashMap, path::Path};
@@ -47,7 +48,7 @@ fn execute_path(
             ExecutionResult::PathUnsat => None,
             ExecutionResult::PotentialError(root) => match with {
                 Backend::Monster => solver::solve(&formula, root),
-                Backend::Boolector => smt::smt(&formula, root),
+                Backend::Boolector => boolector::solve(&formula, root),
             },
         };
 

diff --git a/src/formula_graph.rs b/src/formula_graph.rs
@@ -403,7 +403,8 @@ impl<'a> DataFlowGraphBuilder<'a> {
                 //     "can only handle read syscalls with word width"
                 // );
                 // TODO: round up to word width.. not the best idea, right???
-                let to_add = 8 - (size % 8);
+
+                let to_add = if size % 8 == 0 { 0 } else { 8 - (size % 8) };
                 let words_read = (size + to_add) / 8;
 
                 for i in 0..words_read {

diff --git a/src/lib.rs b/src/lib.rs
@@ -1,4 +1,5 @@
 pub mod bitvec;
+pub mod boolector;
 pub mod candidate_path;
 pub mod cfg;
 pub mod dead_code_elimination;
@@ -9,6 +10,5 @@ pub mod engine;
 pub mod exploration_strategy;
 pub mod formula_graph;
 pub mod iterator;
-pub mod smt;
 pub mod solver;
 pub mod ternary;
diff --git a/src/solver.rs b/src/solver.rs
@@ -16,10 +16,14 @@ fn is_invertable(
     x: TernaryBitVector,
     s: BitVector,
     t: BitVector,
-    _d: ArgumentSide,
+    d: ArgumentSide,
 ) -> bool {
     match instruction {
         Instruction::Add(_) | Instruction::Addi(_) => x.mcb(t - s),
+        Instruction::Sub(_) => match d {
+            ArgumentSide::Lhs => x.mcb(t + s),
+            ArgumentSide::Rhs => x.mcb(s - t),
+        },
         Instruction::Mul(_) => {
             fn y(s: BitVector, t: BitVector) -> BitVector {
                 let c = s.ctz();
@@ -49,7 +53,7 @@ fn is_constraint_invertable(
 
 fn is_consistent(instruction: Instruction, x: TernaryBitVector, t: BitVector) -> bool {
     match instruction {
-        Instruction::Add(_) | Instruction::Addi(_) => true,
+        Instruction::Add(_) | Instruction::Addi(_) | Instruction::Sub(_) => true,
         Instruction::Mul(_) => {
             fn value_exists(x: TernaryBitVector, t: BitVector) -> bool {
                 let y = x.constant_bits() | (BitVector::ones() & !x.constant_bit_mask());
@@ -149,10 +153,14 @@ fn compute_inverse_value(
     x: TernaryBitVector,
     s: BitVector,
     t: BitVector,
-    _d: ArgumentSide,
+    d: ArgumentSide,
 ) -> BitVector {
     match i {
         Instruction::Add(_) | Instruction::Addi(_) => t - s,
+        Instruction::Sub(_) => match d {
+            ArgumentSide::Lhs => t + s,
+            ArgumentSide::Rhs => s - t,
+        },
         Instruction::Mul(_) => {
             let y = s >> s.ctz();
 
@@ -193,7 +201,9 @@ fn compute_consistent_value(
     _d: ArgumentSide,
 ) -> BitVector {
     match i {
-        Instruction::Add(_) | Instruction::Addi(_) => BitVector(random::<u64>()),
+        Instruction::Add(_) | Instruction::Addi(_) | Instruction::Sub(_) => {
+            BitVector(random::<u64>())
+        }
         Instruction::Mul(_) => BitVector({
             if t == BitVector(0) {
                 0
@@ -335,6 +345,7 @@ fn propagate_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeInde
         Node::Instruction(i) => {
             match i.instruction {
                 Instruction::Add(_) | Instruction::Addi(_) => update_binary(f, ab, n, |l, r| l + r),
+                Instruction::Sub(_) => update_binary(f, ab, n, |l, r| l - r),
                 Instruction::Mul(_) => update_binary(f, ab, n, |l, r| l * r),
                 _ => unimplemented!(),
             }
@@ -631,6 +642,7 @@ mod tests {
     }
 
     // TODO: add tests for ADD
+    // TODO: add tests for SUB
 
     const MUL: Instruction = Instruction::Mul(RType(0));
 

diff --git a/symbolic/arithmetic.c b/symbolic/arithmetic.c
@@ -1,18 +1,22 @@
 uint64_t main() {
   uint64_t  a;
   uint64_t  b;
+  uint64_t  c;
   uint64_t  i;
   uint64_t* x;
 
   a = 43;
   b = 2;
+  c = 432;
   x = malloc(8);
 
   read(0, x, 8);
 
   a = a * *x;
 
-  b = b + a; 
+  b = b + a;
 
-  return b;
+  c = b - c;
+
+  return c;
 }
diff --git a/tests/engine.rs b/tests/engine.rs
@@ -3,18 +3,22 @@ use std::path::Path;
 
 mod common;
 
-#[test]
-fn execute_riscu_with_monster_solver() {
-    let result = common::compile(Path::new("symbolic/arithmetic.c")).unwrap();
+fn execute_riscu_with_monster_solver_name(name: &str) {
+    let result = common::compile(Path::new(name)).unwrap();
 
     let input = Path::new(&result);
 
     let result = engine::execute(input, engine::Backend::Monster);
 
     assert!(
         result.is_ok(),
-        "can symbolically execute arithmetic.c without error"
+        format!("can symbolically execute '{}' without error", name)
     );
 
     assert!(std::fs::remove_file(input).is_ok());
 }
+
+#[test]
+fn execute_riscu_with_monster_solver() {
+    execute_riscu_with_monster_solver_name("symbolic/arithmetic.c");
+}