feat: implement bit vector remainder operand in monster solver (#107)

cksystemsgroup · Jan 19, 2021 · 5cb4f26 · 5cb4f26
1 parent 24a5080
commit 5cb4f26
Show file tree

Hide file tree

Showing 10 changed files with 178 additions and 12 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -38,6 +38,7 @@ bytesize = "~1.0.1"
 itertools = "~0.9.0"
 anyhow = "~1.0.34"
 thiserror = "~1.0.22"
+divisors = "~0.2.1"
 
 [dev-dependencies]
 rayon = "~1.5.0"

diff --git a/examples/arithmetic.c b/examples/arithmetic.c
@@ -22,5 +22,7 @@ uint64_t main() {
 
   c = b - c;
 
+  c = c % b;
+
   return c;
 }
diff --git a/src/bitvec.rs b/src/bitvec.rs
@@ -1,5 +1,5 @@
 use std::fmt;
-use std::ops::{Add, BitAnd, BitOr, BitXor, Div, Mul, Neg, Not, Shl, Shr, Sub};
+use std::ops::{Add, BitAnd, BitOr, BitXor, Div, Mul, Neg, Not, Rem, Shl, Shr, Sub};
 
 #[derive(Clone, Copy, Eq, Hash, PartialEq, PartialOrd)]
 pub struct BitVector(pub u64);
@@ -81,6 +81,18 @@ impl Div<BitVector> for BitVector {
     }
 }
 
+impl Rem<BitVector> for BitVector {
+    type Output = BitVector;
+
+    fn rem(self, other: BitVector) -> Self::Output {
+        if other == BitVector(0) {
+            self
+        } else {
+            Self(self.0.wrapping_rem(other.0))
+        }
+    }
+}
+
 impl BitOr<BitVector> for BitVector {
     type Output = BitVector;
 

diff --git a/src/boolector.rs b/src/boolector.rs
@@ -93,6 +93,8 @@ fn traverse<'a>(
                             .and(&traverse(graph, rhs, solver, bvs)),
                         BVOperator::Divu => traverse(graph, lhs, solver, bvs)
                             .udiv(&traverse(graph, rhs, solver, bvs)),
+                        BVOperator::Remu => traverse(graph, lhs, solver, bvs)
+                            .urem(&traverse(graph, rhs, solver, bvs)),
                         BVOperator::Sltu => traverse(graph, lhs, solver, bvs)
                             .ult(&traverse(graph, rhs, solver, bvs))
                             .uext(63),

diff --git a/src/engine.rs b/src/engine.rs
@@ -1,3 +1,5 @@
+
+
 use crate::{
     boolector::Boolector,
     bug::{BasicInfo, Bug},
@@ -323,29 +325,39 @@ where
         Ok(None)
     }
 
-    fn execute_divu(
+    fn execute_divu_remu<Op>(
         &mut self,
         instruction: Instruction,
         rtype: RType,
-    ) -> Result<Option<Bug>, EngineError> {
+        op: Op,
+    ) -> Result<Option<Bug>, EngineError>
+    where
+        Op: FnOnce(u64, u64) -> u64,
+    {
         let bug = match self.regs[rtype.rs2() as usize] {
             Value::Symbolic(divisor) => {
-                trace!("divu: symbolic divisor -> find input for divisor == 0");
+                trace!(
+                    "{}: symbolic divisor -> find input for divisor == 0",
+                    instruction_to_str(instruction)
+                );
 
                 self.execute_query(Query::Equals((divisor, 0)), |info| Bug::DivisionByZero {
                     info,
                 })?
             }
             Value::Concrete(divisor) if divisor == 0 => {
-                trace!("divu: divisor == 0 -> compute reachability");
+                trace!(
+                    "{}: divisor == 0 -> compute reachability",
+                    instruction_to_str(instruction)
+                );
 
                 self.execute_query(Query::Reachable, |info| Bug::DivisionByZero { info })?
             }
             _ => None,
         };
 
         if bug.is_none() {
-            self.execute_rtype(instruction, rtype, u64::wrapping_div)
+            self.execute_rtype(instruction, rtype, op)
         } else {
             Ok(bug)
         }
@@ -614,7 +626,10 @@ where
 
         let result = self.run();
 
-        if !matches!(result, Err(EngineError::ExecutionDepthReached(_)) | Ok(None)) {
+        if !matches!(
+            result,
+            Err(EngineError::ExecutionDepthReached(_)) | Ok(None)
+        ) {
             return result;
         }
 
@@ -895,8 +910,12 @@ where
             Instruction::Add(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_add),
             Instruction::Sub(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_sub),
             Instruction::Mul(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_mul),
-            Instruction::Divu(rtype) => self.execute_divu(instruction, rtype),
-            Instruction::Remu(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_rem),
+            Instruction::Divu(rtype) => {
+                self.execute_divu_remu(instruction, rtype, u64::wrapping_div)
+            }
+            Instruction::Remu(rtype) => {
+                self.execute_divu_remu(instruction, rtype, u64::wrapping_rem)
+            }
             Instruction::Sltu(rtype) => {
                 self.execute_rtype(instruction, rtype, |l, r| if l < r { 1 } else { 0 })
             }

diff --git a/src/solver.rs b/src/solver.rs
@@ -6,9 +6,10 @@ use crate::{
     bitvec::*,
     symbolic_state::{get_operands, BVOperator, Formula, Node, OperandSide, SymbolId},
 };
+use divisors::get_divisors;
 use log::{debug, log_enabled, trace, Level};
 use petgraph::{visit::EdgeRef, Direction};
-use rand::{distributions::Uniform, random, thread_rng, Rng};
+use rand::{distributions::Uniform, random, seq::SliceRandom, thread_rng, Rng};
 use std::time::{Duration, Instant};
 use thiserror::Error;
 
@@ -120,6 +121,12 @@ fn is_invertable(op: BVOperator, s: BitVector, t: BitVector, d: OperandSide) ->
                 true
             }
         }
+        BVOperator::Remu => match d {
+            OperandSide::Lhs => !(s <= t),
+            OperandSide::Rhs => {
+                !(s < t) || ((t != BitVector(0)) && t == s - BitVector(1)) || (s - t <= t)
+            }
+        },
         BVOperator::Not => true,
         BVOperator::BitwiseAnd => (t & s) == t,
         BVOperator::Equals => true,
@@ -277,6 +284,36 @@ fn compute_inverse_value(op: BVOperator, s: BitVector, t: BitVector, d: OperandS
                 }
             }
         },
+        BVOperator::Remu => match d {
+            OperandSide::Lhs => {
+                let y = BitVector(
+                    thread_rng().sample(Uniform::new_inclusive(1, (BitVector::ones() - t / s).0)),
+                );
+                if !(s.0.overflowing_mul(y.0).1) && !(t.0.overflowing_add(y.0 * s.0).1) {
+                    return y;
+                }
+                panic!("Big Error in REMU Inverse Value (LHS)")
+            }
+            OperandSide::Rhs => {
+                if s == t {
+                    let x = BitVector(
+                        thread_rng().sample(Uniform::new_inclusive(t.0, BitVector::ones().0)),
+                    );
+                    if x == t {
+                        BitVector(0)
+                    } else {
+                        x
+                    }
+                } else {
+                    let mut v = get_divisors(s.0 - t.0);
+                    v.push(1);
+                    v.push(s.0 - t.0);
+                    v = v.into_iter().filter(|x| x > &t.0).collect();
+
+                    return BitVector(*v.choose(&mut rand::thread_rng()).unwrap());
+                }
+            }
+        },
         BVOperator::BitwiseAnd => BitVector(random::<u64>()) | t,
         BVOperator::Equals => {
             if t == BitVector(0) {
@@ -357,6 +394,24 @@ fn compute_consistent_value(op: BVOperator, t: BitVector, d: OperandSide) -> Bit
                 BitVector(thread_rng().sample(Uniform::new(1, BitVector::ones().0)))
             }
         }
+        BVOperator::Remu => match d {
+            OperandSide::Lhs => {
+                if t == BitVector::ones() {
+                    BitVector::ones()
+                } else {
+                    BitVector(thread_rng().sample(Uniform::new_inclusive(t.0, BitVector::ones().0)))
+                }
+            }
+            OperandSide::Rhs => {
+                if t == BitVector::ones() {
+                    BitVector(0)
+                } else {
+                    BitVector(
+                        thread_rng().sample(Uniform::new_inclusive(t.0 + 1, BitVector::ones().0)),
+                    )
+                }
+            }
+        },
         BVOperator::BitwiseAnd => BitVector(random::<u64>()) | t,
         _ => unreachable!("unknown operator for consistent value: {:?}", op),
     }
@@ -513,6 +568,7 @@ fn propagate_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId
                         BitVector(0)
                     }
                 }),
+                BVOperator::Remu => update_binary(f, ab, n, "%", |l, r| l % r),
                 BVOperator::Equals => update_binary(f, ab, n, "=", |l, r| {
                     if l == r {
                         BitVector(1)

diff --git a/src/symbolic_state.rs b/src/symbolic_state.rs
@@ -32,6 +32,7 @@ pub enum BVOperator {
     Mul,
     Divu,
     Sltu,
+    Remu,
     Not,
     Equals,
     BitwiseAnd,
@@ -57,6 +58,7 @@ impl fmt::Display for BVOperator {
                 BVOperator::Mul => "*",
                 BVOperator::Divu => "/",
                 BVOperator::Not => "!",
+                BVOperator::Remu => "%",
                 BVOperator::Equals => "=",
                 BVOperator::BitwiseAnd => "&",
                 BVOperator::Sltu => "<",
@@ -87,6 +89,7 @@ fn instruction_to_bv_operator(instruction: Instruction) -> BVOperator {
         Instruction::Sub(_) => BVOperator::Sub,
         Instruction::Mul(_) => BVOperator::Mul,
         Instruction::Divu(_) => BVOperator::Divu,
+        Instruction::Remu(_) => BVOperator::Remu,
         Instruction::Sltu(_) => BVOperator::Sltu,
         _ => unimplemented!("can not translate {:?} to Operator", instruction),
     }

diff --git a/src/z3.rs b/src/z3.rs
@@ -152,6 +152,7 @@ impl<'a, 'ctx> Z3Translator<'a, 'ctx> {
                     BVOperator::Sub => traverse_binary!(self, lhs, bvsub, rhs),
                     BVOperator::Mul => traverse_binary!(self, lhs, bvmul, rhs),
                     BVOperator::Divu => traverse_binary!(self, lhs, bvudiv, rhs),
+                    BVOperator::Remu => traverse_binary!(self, lhs, bvurem, rhs),
                     BVOperator::Equals => traverse_binary!(self, lhs, _eq, rhs)
                         .as_bool()
                         .unwrap()

diff --git a/tests/engine.rs b/tests/engine.rs
@@ -58,7 +58,8 @@ fn execute_riscu(names: &'static [&str], solver: Backend) {
         let bug = possible_bug.unwrap();
 
         assert!(
-            matches!((file_name, bug.clone()),
+            matches!(
+                (file_name, bug.clone()),
                 ("arithmetic.c", Bug::ExitCodeGreaterZero { .. }) |
                 ("invalid-memory-access-2-35.c", Bug::AccessToOutOfRangeAddress { .. }) |
                 ("if-else.c", Bug::ExitCodeGreaterZero { .. }) |
@@ -73,7 +74,8 @@ fn execute_riscu(names: &'static [&str], solver: Backend) {
                 ("recursive-fibonacci-1-10.c", Bug::ExitCodeGreaterZero { .. }) |
                 ("simple-if-else-1-35.c", Bug::ExitCodeGreaterZero { .. }) |
                 ("simple-increasing-loop-1-35.c", Bug::ExitCodeGreaterZero { .. }) |
-                ("two-level-nested-loop-1-35.c", Bug::ExitCodeGreaterZero { .. })),
+                ("two-level-nested-loop-1-35.c", Bug::ExitCodeGreaterZero { .. })
+            ),
             "found right bug type (actual: {}) for {}",
             bug,
             file_name