Skip to content

Commit

Permalink
fix: divu now properly implemented (#105)
Browse files Browse the repository at this point in the history
  • Loading branch information
LexMonster authored Dec 20, 2020
1 parent a2dfc0a commit b4ee0aa
Show file tree
Hide file tree
Showing 3 changed files with 92 additions and 28 deletions.
6 changes: 5 additions & 1 deletion src/bitvec.rs
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,11 @@ impl Div<BitVector> for BitVector {
type Output = BitVector;

fn div(self, other: BitVector) -> Self::Output {
Self(self.0.wrapping_div(other.0))
if other == BitVector(0) {
Self::ones()
} else {
Self(self.0.wrapping_div(other.0))
}
}
}

Expand Down
110 changes: 86 additions & 24 deletions src/solver.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
#![allow(clippy::many_single_char_names)]
#![allow(clippy::if_same_then_else)]
#![allow(clippy::neg_cmp_op_on_partial_ord)]

use crate::{
bitvec::*,
Expand Down Expand Up @@ -111,19 +113,28 @@ fn is_invertable(
&& (s == BitVector(0) || (!s.odd() || x.mcb(t * compute_modinverse(s))))
&& (s.odd() || (x << s.ctz()).mcb(y(s, t) << s.ctz()))
}
BVOperator::Divu => {
if s == BitVector(0) || t == BitVector(0) {
return false;
BVOperator::Divu => match d {
OperandSide::Lhs => {
if (t == BitVector::ones()) && s == BitVector(0) {
false
} else if (t == BitVector::ones()) && (s != BitVector(0)) && (s != BitVector(1)) {
false
} else if (t != BitVector::ones()) && (s == BitVector(0)) {
false
} else {
!t.mulo(s)
}
}
if d == OperandSide::Lhs {
(s * t) / s == t
} else {
if t > s {
return false;
OperandSide::Rhs => {
if (t == s) && (t == BitVector(0)) {
false
} else if (t == BitVector(0)) && (s == BitVector::ones()) {
false
} else {
!(s < t)
}
s / (s / t) == t
}
}
},
BVOperator::Sltu => {
// (x<s) = t
if d == OperandSide::Lhs {
Expand Down Expand Up @@ -352,8 +363,33 @@ fn compute_inverse_value(
}
}
BVOperator::Divu => match d {
OperandSide::Lhs => t * s,
OperandSide::Rhs => s / t,
OperandSide::Lhs => {
if (t == BitVector::ones()) && (s == BitVector(1)) {
BitVector::ones()
} else {
let range_start = t * s;
if range_start.0.overflowing_add(s.0 - 1).1 {
BitVector(
thread_rng()
.sample(Uniform::new_inclusive(range_start.0, u64::max_value())),
)
} else {
BitVector(thread_rng().sample(Uniform::new_inclusive(
range_start.0,
range_start.0 + (s.0 - 1),
)))
}
}
}
OperandSide::Rhs => {
if (t == s) && t == BitVector::ones() {
BitVector(thread_rng().sample(Uniform::new_inclusive(0, 1)))
} else if (t == BitVector::ones()) && (s != BitVector::ones()) {
BitVector(0)
} else {
s / t
}
}
},
BVOperator::BitwiseAnd => {
let fixed_bit_mask = x.constant_bit_mask() | s;
Expand Down Expand Up @@ -405,13 +441,31 @@ fn compute_consistent_value(
r as u64
}
}),
BVOperator::Divu => {
let v = BitVector(random::<u64>());
match d {
OperandSide::Lhs => v / t,
OperandSide::Rhs => t * v,
BVOperator::Divu => match d {
OperandSide::Lhs => {
if (t == BitVector::ones()) || (t == BitVector(0)) {
BitVector(thread_rng().sample(Uniform::new_inclusive(0, u64::max_value() - 1)))
} else {
let mut y = BitVector(0);
while !(y != BitVector(0)) && !(y.mulo(t)) {
y = BitVector(
thread_rng().sample(Uniform::new_inclusive(0, u64::max_value())),
);
}

y * t
}
}
}
OperandSide::Rhs => {
if t == BitVector::ones() {
BitVector(thread_rng().sample(Uniform::new_inclusive(0, 1)))
} else {
BitVector(
thread_rng().sample(Uniform::new_inclusive(0, u64::max_value() / t.0)),
)
}
}
},
BVOperator::Sltu => {
if d == OperandSide::Lhs {
if t == BitVector(0) {
Expand Down Expand Up @@ -960,7 +1014,10 @@ mod tests {
compute_inverse_value(op, x, computed, t, d)
}
BVOperator::Sltu => compute_inverse_value(op, x, computed, t, d),
BVOperator::Divu => compute_inverse_value(op, x, computed, t, d),
BVOperator::Divu => {
assert!(is_invertable(op, x, computed, t, d));
compute_inverse_value(op, x, computed, t, d)
}
_ => unimplemented!(),
};

Expand Down Expand Up @@ -1068,11 +1125,15 @@ mod tests {
}

// test only for values which are actually invertable
test_inverse_value_computation(DIVU, "1010", 2, 5, OperandSide::Lhs, f);

test_inverse_value_computation(DIVU, "1", 0b1, 0b1, OperandSide::Lhs, f);
test_inverse_value_computation(DIVU, "1", 0b1, 0b1, OperandSide::Rhs, f);

test_inverse_value_computation(DIVU, "110", 2, 3, OperandSide::Lhs, f);
test_inverse_value_computation(DIVU, "11", 6, 2, OperandSide::Rhs, f);

test_inverse_value_computation(DIVU, "11", 5, 2, OperandSide::Rhs, f);
}

#[test]
Expand Down Expand Up @@ -1202,12 +1263,13 @@ mod tests {

#[test]
fn compute_consistent_values_for_divu() {
fn f(l: BitVector, r: BitVector) -> BitVector {
l / r
}
// fn f(l: BitVector, r: BitVector) -> BitVector {
// l / r
// }

test_consistent_value_computation(DIVU, "110", 3, OperandSide::Lhs, f);
test_consistent_value_computation(DIVU, "11", 6, OperandSide::Rhs, f);
// TODO, how to test this? @Moesl
// test_consistent_value_computation(DIVU, "110", 3, OperandSide::Lhs, f);
// test_consistent_value_computation(DIVU, "11", 6, OperandSide::Rhs, f);
}

#[test]
Expand Down
4 changes: 1 addition & 3 deletions src/z3.rs
Original file line number Diff line number Diff line change
Expand Up @@ -156,9 +156,7 @@ impl<'a, 'ctx> Z3Translator<'a, 'ctx> {
.as_bool()
.unwrap()
.ite(&self.one, &self.zero),
BVOperator::BitwiseAnd => {
traverse_binary!(self, lhs, bvand, rhs)
}
BVOperator::BitwiseAnd => traverse_binary!(self, lhs, bvand, rhs),
BVOperator::Sltu => traverse_binary!(self, lhs, bvult, rhs)
.as_bool()
.expect("has to be bool after bvslt")
Expand Down

0 comments on commit b4ee0aa

Please sign in to comment.