From 0bb5eb17d2dac57ccf329297caf24d0499de1968 Mon Sep 17 00:00:00 2001 From: Sara Seidl Date: Tue, 1 Jun 2021 21:16:07 +0200 Subject: [PATCH] fix: invertibility conditions DIVU and REMU --- src/solver/monster.rs | 113 +++++++++++++++++++++++------------------- 1 file changed, 63 insertions(+), 50 deletions(-) diff --git a/src/solver/monster.rs b/src/solver/monster.rs index b4807944..bc0c35a3 100644 --- a/src/solver/monster.rs +++ b/src/solver/monster.rs @@ -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) } } }, @@ -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, @@ -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; @@ -422,7 +420,7 @@ fn value( 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; @@ -451,7 +449,7 @@ fn is_essential( 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, } @@ -734,7 +732,7 @@ mod tests { ); } - fn test_invertability( + fn test_invertibility( op: BVOperator, s: u64, t: u64, @@ -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, @@ -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, @@ -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!(), @@ -873,26 +871,26 @@ 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, @@ -900,7 +898,7 @@ mod tests { true, "operand with undetermined bits and possible invsere", ); - test_invertability( + test_invertibility( MUL, 0b10, 0b10, @@ -908,7 +906,7 @@ mod tests { true, "operand with undetermined bits and no inverse value", ); - test_invertability( + test_invertibility( MUL, 0b100, 0b100, @@ -916,7 +914,7 @@ mod tests { true, "operand with undetermined bits and no inverse value", ); - test_invertability( + test_invertibility( MUL, 0b10, 0b1100, @@ -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, @@ -943,9 +941,9 @@ 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, @@ -953,7 +951,7 @@ mod tests { false, "max_value < x == 1 FALSE", ); - test_invertability( + test_invertibility( SLTU, u64::max_value(), 0, @@ -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; @@ -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); @@ -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); @@ -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); @@ -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, @@ -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]