Skip to content

Commit

Permalink
fix: invertibility conditions DIVU and REMU (#141)
Browse files Browse the repository at this point in the history
  • Loading branch information
@saraseidl
saraseidl authored Jun 7, 2021
1 parent 886be18 commit 9c03995
Showing 1 changed file with 63 additions and 50 deletions.
113 changes: 63 additions & 50 deletions src/solver/monster.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,31 +38,25 @@ impl Solver for MonsterSolver {
}
}

// check if invertability condition is met
fn is_invertable(op: BVOperator, s: BitVector, t: BitVector, d: OperandSide) -> bool {
// check if invertibility condition is met
fn is_invertible(op: BVOperator, s: BitVector, t: BitVector, d: OperandSide) -> bool {
match op {
BVOperator::Add => true,
BVOperator::Sub => true,
BVOperator::Mul => (-s | s) & t == t,
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
if s == BitVector(0) {
t == BitVector::ones()
} else {
!t.mulo(s)
}
}
OperandSide::Rhs => {
if (t == s) && (t == BitVector(0)) {
false
} else if (t == BitVector(0)) && (s == BitVector::ones()) {
false
if t == BitVector(0) {
s != BitVector::ones()
} else {
!(s < t)
t == BitVector::ones() || !(s < t)
}
}
},
Expand All @@ -85,7 +79,11 @@ fn is_invertable(op: BVOperator, s: BitVector, t: BitVector, d: OperandSide) ->
BVOperator::Remu => match d {
OperandSide::Lhs => !(s <= t),
OperandSide::Rhs => {
!(s < t) || ((t != BitVector(0)) && t == s - BitVector(1)) || (s - t <= t)
if s == t {
true
} else {
!((s < t) || ((t != BitVector(0)) && t == s - BitVector(1)) || (s - t <= t))
}
}
},
BVOperator::Not => true,
Expand Down Expand Up @@ -182,7 +180,7 @@ fn compute_inverse_value(op: BVOperator, s: BitVector, t: BitVector, d: OperandS

let y_inv = y
.modinverse()
.expect("a modular inverse has to exist iff operator is invertable");
.expect("a modular inverse has to exist iff operator is invertible");

let result = (t >> s.ctz()) * y_inv;

Expand Down Expand Up @@ -422,7 +420,7 @@ fn value<F: Formula>(
Symbol::Operator(op) => {
let consistent = compute_consistent_value(*op, t, side);

if is_invertable(*op, s, t, side) {
if is_invertible(*op, s, t, side) {
let inverse = compute_inverse_value(*op, s, t, side);
let choose_inverse =
rand::thread_rng().gen_range(0.0_f64..=1.0_f64) < CHOOSE_INVERSE;
Expand Down Expand Up @@ -451,7 +449,7 @@ fn is_essential<F: Formula>(
let ab_nx = ab[this];

match &formula[other] {
Symbol::Operator(op) => !is_invertable(*op, ab_nx, t, on_side.other()),
Symbol::Operator(op) => !is_invertible(*op, ab_nx, t, on_side.other()),
// TODO: not mentioned in paper => improvised. is that really true?
Symbol::Constant(_) | Symbol::Input(_) => false,
}
Expand Down Expand Up @@ -734,7 +732,7 @@ mod tests {
);
}

fn test_invertability(
fn test_invertibility(
op: BVOperator,
s: u64,
t: u64,
Expand All @@ -748,7 +746,7 @@ mod tests {
match d {
OperandSide::Lhs => {
assert_eq!(
is_invertable(op, s, t, d),
is_invertible(op, s, t, d),
result,
"x {:?} {:?} == {:?} {}",
op,
Expand All @@ -759,7 +757,7 @@ mod tests {
}
OperandSide::Rhs => {
assert_eq!(
is_invertable(op, s, t, d),
is_invertible(op, s, t, d),
result,
"{:?} {:?} x == {:?} {}",
s,
Expand Down Expand Up @@ -827,15 +825,15 @@ mod tests {
BVOperator::Add => t - computed,
BVOperator::Mul => {
assert!(
is_invertable(op, computed, t, d),
"choose values which are invertable..."
is_invertible(op, computed, t, d),
"choose values which are invertible..."
);

compute_inverse_value(op, computed, t, d)
}
BVOperator::Sltu => compute_inverse_value(op, computed, t, d),
BVOperator::Divu => {
assert!(is_invertable(op, computed, t, d));
assert!(is_invertible(op, computed, t, d));
compute_inverse_value(op, computed, t, d)
}
_ => unimplemented!(),
Expand Down Expand Up @@ -873,50 +871,50 @@ mod tests {
const REMU: BVOperator = BVOperator::Remu;

#[test]
fn check_invertability_condition_for_divu() {
test_invertability(DIVU, 0b1, 0b1, OperandSide::Lhs, true, "trivial divu");
test_invertability(DIVU, 0b1, 0b1, OperandSide::Rhs, true, "trivial divu");
fn check_invertibility_condition_for_divu() {
test_invertibility(DIVU, 0b1, 0b1, OperandSide::Lhs, true, "trivial divu");
test_invertibility(DIVU, 0b1, 0b1, OperandSide::Rhs, true, "trivial divu");

test_invertability(DIVU, 3, 2, OperandSide::Lhs, true, "x / 3 = 2");
test_invertability(DIVU, 6, 2, OperandSide::Rhs, true, "6 / x = 2");
test_invertibility(DIVU, 3, 2, OperandSide::Lhs, true, "x / 3 = 2");
test_invertibility(DIVU, 6, 2, OperandSide::Rhs, true, "6 / x = 2");

test_invertability(DIVU, 0, 2, OperandSide::Lhs, false, "x / 0 = 2");
test_invertability(DIVU, 0, 2, OperandSide::Rhs, false, "0 / x = 2");
test_invertibility(DIVU, 0, 2, OperandSide::Lhs, false, "x / 0 = 2");
test_invertibility(DIVU, 0, 2, OperandSide::Rhs, false, "0 / x = 2");

test_invertability(DIVU, 5, 6, OperandSide::Rhs, false, "5 / x = 6");
test_invertibility(DIVU, 5, 6, OperandSide::Rhs, false, "5 / x = 6");
}

#[test]
fn check_invertability_condition_for_mul() {
fn check_invertibility_condition_for_mul() {
let side = OperandSide::Lhs;

test_invertability(MUL, 0b1, 0b1, side, true, "trivial multiplication");
test_invertability(MUL, 0b10, 0b1, side, false, "operand bigger than result");
test_invertability(
test_invertibility(MUL, 0b1, 0b1, side, true, "trivial multiplication");
test_invertibility(MUL, 0b10, 0b1, side, false, "operand bigger than result");
test_invertibility(
MUL,
0b10,
0b10,
side,
true,
"operand with undetermined bits and possible invsere",
);
test_invertability(
test_invertibility(
MUL,
0b10,
0b10,
side,
true,
"operand with undetermined bits and no inverse value",
);
test_invertability(
test_invertibility(
MUL,
0b100,
0b100,
side,
true,
"operand with undetermined bits and no inverse value",
);
test_invertability(
test_invertibility(
MUL,
0b10,
0b1100,
Expand All @@ -927,12 +925,12 @@ mod tests {
}

#[test]
fn check_invertability_condition_for_sltu() {
fn check_invertibility_condition_for_sltu() {
let mut side = OperandSide::Lhs;

test_invertability(SLTU, 0, 1, side, false, "x < 0 == 1 FALSE");
test_invertability(SLTU, 1, 1, side, true, "x < 1 == 1 TRUE");
test_invertability(
test_invertibility(SLTU, 0, 1, side, false, "x < 0 == 1 FALSE");
test_invertibility(SLTU, 1, 1, side, true, "x < 1 == 1 TRUE");
test_invertibility(
SLTU,
u64::max_value(),
0,
Expand All @@ -943,17 +941,17 @@ mod tests {

side = OperandSide::Rhs;

test_invertability(SLTU, 0, 1, side, true, "0 < x == 1 TRUE");
test_invertability(SLTU, 0, 0, side, true, "0 < x == 0 TRUE");
test_invertability(
test_invertibility(SLTU, 0, 1, side, true, "0 < x == 1 TRUE");
test_invertibility(SLTU, 0, 0, side, true, "0 < x == 0 TRUE");
test_invertibility(
SLTU,
u64::max_value(),
1,
side,
false,
"max_value < x == 1 FALSE",
);
test_invertability(
test_invertibility(
SLTU,
u64::max_value(),
0,
Expand All @@ -963,6 +961,20 @@ mod tests {
);
}

#[test]
fn check_invertibility_condition_for_remu() {
let mut side = OperandSide::Lhs;

test_invertibility(REMU, 3, 2, side, true, "x mod 3 = 2 TRUE");
test_invertibility(REMU, 3, 3, side, false, "x mod 3 = 3 FALSE");

side = OperandSide::Rhs;

test_invertibility(REMU, 3, 3, side, true, "3 mod x = 3 TRUE");
test_invertibility(REMU, 3, 2, side, false, "3 mod x = 2 FALSE");
test_invertibility(REMU, 5, 3, side, false, "5 mod x = 3 FALSE");
}

#[test]
fn compute_inverse_values_for_mul() {
let side = OperandSide::Lhs;
Expand All @@ -971,7 +983,7 @@ mod tests {
l * r
}

// test only for values which are actually invertable
// test only for values which are actually invertible
test_inverse_value_computation(MUL, 0b1, 0b1, side, f);
test_inverse_value_computation(MUL, 0b10, 0b10, side, f);
test_inverse_value_computation(MUL, 0b100, 0b100, side, f);
Expand All @@ -990,7 +1002,7 @@ mod tests {
}
}

// test only for values which are actually invertable
// test only for values which are actually invertible
test_inverse_value_computation(SLTU, u64::max_value(), 0, side, f);
test_inverse_value_computation(SLTU, 0, 0, side, f);
test_inverse_value_computation(SLTU, 1, 1, side, f);
Expand All @@ -1008,7 +1020,7 @@ mod tests {
l / r
}

// test only for values which are actually invertable
// test only for values which are actually invertible
test_inverse_value_computation(DIVU, 0b1, 0b1, OperandSide::Lhs, f);
test_inverse_value_computation(DIVU, 0b1, 0b1, OperandSide::Rhs, f);

Expand All @@ -1022,7 +1034,7 @@ mod tests {
l % r
}

// test only for values which are actually invertable
// test only for values which are actually invertible
test_inverse_value_computation(REMU, u64::max_value(), 0, OperandSide::Lhs, f);
test_inverse_value_computation(
REMU,
Expand All @@ -1033,6 +1045,7 @@ mod tests {
);
test_inverse_value_computation(REMU, 3, 2, OperandSide::Lhs, f);
test_inverse_value_computation(REMU, 5, 2, OperandSide::Rhs, f);
test_inverse_value_computation(REMU, 3, 3, OperandSide::Rhs, f);
}

#[test]
Expand Down

0 comments on commit 9c03995

Please sign in to comment.