From 04f12c715472798df59316ce482f12c3fea274fd Mon Sep 17 00:00:00 2001 From: Alexander Linz Date: Mon, 12 Oct 2020 13:43:46 +0200 Subject: [PATCH 1/9] broken first try (turned off checks) --- src/solver.rs | 27 ++++++++++++++++++++++++++- src/ternary.rs | 13 +++++++++++++ 2 files changed, 39 insertions(+), 1 deletion(-) diff --git a/src/solver.rs b/src/solver.rs index ffa85d87..af555e70 100644 --- a/src/solver.rs +++ b/src/solver.rs @@ -16,7 +16,7 @@ fn is_invertable( x: TernaryBitVector, s: BitVector, t: BitVector, - _d: ArgumentSide, + d: ArgumentSide, ) -> bool { match instruction { Instruction::Add(_) | Instruction::Addi(_) => x.mcb(t - s), @@ -30,6 +30,31 @@ fn is_invertable( && (s == BitVector(0) || (!s.odd() || x.mcb(t * s.modinverse().unwrap()))) && (s.odd() || (x << s.ctz()).mcb(y(s, t) << s.ctz())) } + Instruction::Divu(i) => { + if d == ArgumentSide::Lhs { + // x / s = t + let c = addo(BitVector(1), t); + if (s * t) / s == t { + if t == BitVector(0) { + if !(x.0 < s) { + false + } + } + + // assumed t == 0 => xlo < s + + if t != BitVector(0) && s != BitVector(0){ + + } + true + } else { + false + } + } else { + // s / x = t + + } + } _ => unimplemented!(), } } diff --git a/src/ternary.rs b/src/ternary.rs index 263c95ae..e3093f72 100644 --- a/src/ternary.rs +++ b/src/ternary.rs @@ -74,6 +74,19 @@ impl TernaryBitVector { } } +/// returns true iff s * x => overflow +pub fn mulo(s: BitVector, x: TernaryBitVector) -> bool { + s.0.overflowing_mul(x.0).1 +} + +pub fn addo(s: BitVector, x: TernaryBitVector) -> bool { + s.0.overflowing_add(x.0).1 +} + +pub fn addo(s: BitVector, t: BitVector) -> bool { + s.0.overflowing_add(t.0).1 +} + impl Shl for TernaryBitVector { type Output = TernaryBitVector; From 1ea518ae270b6c57eda09a87e661d2b2708e6a3e Mon Sep 17 00:00:00 2001 From: Alexander Linz Date: Thu, 15 Oct 2020 10:31:13 +0200 Subject: [PATCH 2/9] Divu Half way --- src/solver.rs | 80 +++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 77 insertions(+), 3 deletions(-) diff --git a/src/solver.rs b/src/solver.rs index af555e70..f54c92ea 100644 --- a/src/solver.rs +++ b/src/solver.rs @@ -33,7 +33,6 @@ fn is_invertable( Instruction::Divu(i) => { if d == ArgumentSide::Lhs { // x / s = t - let c = addo(BitVector(1), t); if (s * t) / s == t { if t == BitVector(0) { if !(x.0 < s) { @@ -41,18 +40,60 @@ fn is_invertable( } } - // assumed t == 0 => xlo < s + // assumed: t == 0 implies xlo < s if t != BitVector(0) && s != BitVector(0){ - + let c = mulo(s, t + BitVector(1)) || addo(BitVector(1), t); + if c { + true + } else { + let y = x.constant_bits(); + if y < s * t + BitVector(1) { + // assumed: c implies y <= ones + // where ones is lenght of x, this just checks that x and y have the same lenght + true + } + } } + true } else { false } } else { // s / x = t + if s / (s / t) == t { + if t != BitVector::ones() { + if !(x.1 > 0) { + false + } + + if s != BitVector(0) || t != BitVector(0) { + if !(s / x.1 < t) { + false + } + } + if t == BitVector::ones() { + let y = x.constant_bits(); + if !(y >= BitVector(0) && y <= s / t) { + false + } + } + + if t != BitVector::ones() { + let y = x.constant_bits(); + if !(y > t + 1 && y <= s / t) { + false + } + } + + true + } + + } else { + false + } } } _ => unimplemented!(), @@ -86,6 +127,39 @@ fn is_consistent(instruction: Instruction, x: TernaryBitVector, t: BitVector) -> && (!t.odd() || (x.1.lsb() != 0)) && (t.odd() || value_exists(x, t)) } + Instruction::Divu(_) => { + // x/s = t + if d == ArgumentSide::Lhs { + if t == BitVector::ones() { + if !(x.1 >= t) { + false + } + } + + if t == BitVector(0) { + if !(x.0 != BitVector::ones()){ + false + } + } + + if t != BitVector(0) { + if t != Bitvector::ones() { + if t != BitVector(1) { + if !x.mcb(t) { + if mulo(BitVector(2), t){ + false + } + if!() + } + } + } + } + + true + } else { + //s/x = t + } + } _ => unimplemented!(), } } From 6cd2e371ec343b2e4ccf6e81eea374f59016573b Mon Sep 17 00:00:00 2001 From: alexanderlackner <43965864+alexanderlackner@users.noreply.github.com> Date: Fri, 16 Oct 2020 11:36:22 +0200 Subject: [PATCH 3/9] First try at consistency condition of divu WIP --- src/solver.rs | 30 ++++++++++++++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/src/solver.rs b/src/solver.rs index f54c92ea..0310f5a3 100644 --- a/src/solver.rs +++ b/src/solver.rs @@ -83,7 +83,7 @@ fn is_invertable( if t != BitVector::ones() { let y = x.constant_bits(); - if !(y > t + 1 && y <= s / t) { + if !(y > t + BitVector(1) && y <= s / t) { false } } @@ -149,7 +149,33 @@ fn is_consistent(instruction: Instruction, x: TernaryBitVector, t: BitVector) -> if mulo(BitVector(2), t){ false } - if!() + //this currently only works for ranges NOT for ternary vectors + //TODO: adopt an EFFICIENT way to do this for ternary vectors + let y = t / x.1; + if t * y < x.0 { + let o = x.0 - t * y; + } else { + let o = BitVector(0); + } + let o = x.1 - t * y; + + if y == BitVector(0) { + false + } + + //c = min(y-1,x.1-y*t) + // o>=c + if o > y - BitVector(1) || o > x.1 - y * t { + false + } + + if mulo(y, t) { + false + } + + if addo(y*t, o) { + false + } } } } From c1f82c58b309b626a82431a836887f22de6e0775 Mon Sep 17 00:00:00 2001 From: alexanderlackner <43965864+alexanderlackner@users.noreply.github.com> Date: Mon, 19 Oct 2020 13:57:50 +0200 Subject: [PATCH 4/9] DIVU constraint condition almost working as intended --- src/bitvec.rs | 8 ++++++++ src/solver.rs | 26 ++++++++++++++++++++++++-- src/ternary.rs | 4 ---- 3 files changed, 32 insertions(+), 6 deletions(-) diff --git a/src/bitvec.rs b/src/bitvec.rs index 804fbbe2..fa504f06 100644 --- a/src/bitvec.rs +++ b/src/bitvec.rs @@ -109,6 +109,14 @@ impl Not for BitVector { } } +pub fn addo(s: BitVector, t: BitVector) -> bool { + s.0.overflowing_add(t.0).1 +} + +pub fn mulo(s: BitVector, t: BitVector) -> bool { + s.0.overflowing_mul(t.0).1 +} + impl fmt::Debug for BitVector { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { fn bit_to_char(x: &BitVector, b: u32) -> char { diff --git a/src/solver.rs b/src/solver.rs index 0310f5a3..c963e1fc 100644 --- a/src/solver.rs +++ b/src/solver.rs @@ -157,7 +157,6 @@ fn is_consistent(instruction: Instruction, x: TernaryBitVector, t: BitVector) -> } else { let o = BitVector(0); } - let o = x.1 - t * y; if y == BitVector(0) { false @@ -183,7 +182,30 @@ fn is_consistent(instruction: Instruction, x: TernaryBitVector, t: BitVector) -> true } else { - //s/x = t + // s/x = t + if t == BitVector::ones() { + if !(x.mcb(BitVector(0)) || x.mcb(BitVector(1))) { + false + } + } + if t != BitVector::ones() { + if mulo(x.0, t) { + false + } + let y = x.constant_bits(); + if y == BitVector(0) { + // (!x.1+BitVector(1) & x.1) is a BitVector with one the first set bit from x.1 set + // Which when added to x.0 is the next bigger BitVector with x.mcb(y) true + let y = y + (!x.1+BitVector(1) & x.1); + if y == BitVector(0) { + false + } + } + if mulo(y, t) { + false + } + true + } } } _ => unimplemented!(), diff --git a/src/ternary.rs b/src/ternary.rs index e3093f72..671ccfba 100644 --- a/src/ternary.rs +++ b/src/ternary.rs @@ -83,10 +83,6 @@ pub fn addo(s: BitVector, x: TernaryBitVector) -> bool { s.0.overflowing_add(x.0).1 } -pub fn addo(s: BitVector, t: BitVector) -> bool { - s.0.overflowing_add(t.0).1 -} - impl Shl for TernaryBitVector { type Output = TernaryBitVector; From a0404f0a7793b52c14b302f3f434757e52475235 Mon Sep 17 00:00:00 2001 From: linzalexander Date: Thu, 5 Nov 2020 12:42:08 +0100 Subject: [PATCH 5/9] reset to implement simple divu --- src/bitvec.rs | 16 ++-- src/solver.rs | 196 ++++++------------------------------------------- src/ternary.rs | 16 ++-- 3 files changed, 39 insertions(+), 189 deletions(-) diff --git a/src/bitvec.rs b/src/bitvec.rs index fa504f06..f74a4ac0 100644 --- a/src/bitvec.rs +++ b/src/bitvec.rs @@ -27,6 +27,14 @@ impl BitVector { None => None, } } + + pub fn addo(&self, t: BitVector) -> bool { + self.0.overflowing_add(t.0).1 + } + + pub fn mulo(&self, t: BitVector) -> bool { + self.0.overflowing_mul(t.0).1 + } } impl Neg for BitVector { @@ -109,14 +117,6 @@ impl Not for BitVector { } } -pub fn addo(s: BitVector, t: BitVector) -> bool { - s.0.overflowing_add(t.0).1 -} - -pub fn mulo(s: BitVector, t: BitVector) -> bool { - s.0.overflowing_mul(t.0).1 -} - impl fmt::Debug for BitVector { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { fn bit_to_char(x: &BitVector, b: u32) -> char { diff --git a/src/solver.rs b/src/solver.rs index c963e1fc..68b5b9c5 100644 --- a/src/solver.rs +++ b/src/solver.rs @@ -16,7 +16,7 @@ fn is_invertable( x: TernaryBitVector, s: BitVector, t: BitVector, - d: ArgumentSide, + _d: ArgumentSide, ) -> bool { match instruction { Instruction::Add(_) | Instruction::Addi(_) => x.mcb(t - s), @@ -30,71 +30,8 @@ fn is_invertable( && (s == BitVector(0) || (!s.odd() || x.mcb(t * s.modinverse().unwrap()))) && (s.odd() || (x << s.ctz()).mcb(y(s, t) << s.ctz())) } - Instruction::Divu(i) => { - if d == ArgumentSide::Lhs { - // x / s = t - if (s * t) / s == t { - if t == BitVector(0) { - if !(x.0 < s) { - false - } - } - - // assumed: t == 0 implies xlo < s - - if t != BitVector(0) && s != BitVector(0){ - let c = mulo(s, t + BitVector(1)) || addo(BitVector(1), t); - if c { - true - } else { - let y = x.constant_bits(); - if y < s * t + BitVector(1) { - // assumed: c implies y <= ones - // where ones is lenght of x, this just checks that x and y have the same lenght - true - } - } - } - - true - } else { - false - } - } else { - // s / x = t - if s / (s / t) == t { - if t != BitVector::ones() { - if !(x.1 > 0) { - false - } - - if s != BitVector(0) || t != BitVector(0) { - if !(s / x.1 < t) { - false - } - } - - if t == BitVector::ones() { - let y = x.constant_bits(); - if !(y >= BitVector(0) && y <= s / t) { - false - } - } - - if t != BitVector::ones() { - let y = x.constant_bits(); - if !(y > t + BitVector(1) && y <= s / t) { - false - } - } - - true - } - - } else { - false - } - } + Instruction::Divu(_i) => { + unimplemented!() } _ => unimplemented!(), } @@ -126,87 +63,9 @@ fn is_consistent(instruction: Instruction, x: TernaryBitVector, t: BitVector) -> (!(t != BitVector(0)) || (x.1 != BitVector(0))) && (!t.odd() || (x.1.lsb() != 0)) && (t.odd() || value_exists(x, t)) - } - Instruction::Divu(_) => { - // x/s = t - if d == ArgumentSide::Lhs { - if t == BitVector::ones() { - if !(x.1 >= t) { - false - } - } - - if t == BitVector(0) { - if !(x.0 != BitVector::ones()){ - false - } - } - - if t != BitVector(0) { - if t != Bitvector::ones() { - if t != BitVector(1) { - if !x.mcb(t) { - if mulo(BitVector(2), t){ - false - } - //this currently only works for ranges NOT for ternary vectors - //TODO: adopt an EFFICIENT way to do this for ternary vectors - let y = t / x.1; - if t * y < x.0 { - let o = x.0 - t * y; - } else { - let o = BitVector(0); - } - - if y == BitVector(0) { - false - } - - //c = min(y-1,x.1-y*t) - // o>=c - if o > y - BitVector(1) || o > x.1 - y * t { - false - } - - if mulo(y, t) { - false - } - - if addo(y*t, o) { - false - } - } - } - } - } - - true - } else { - // s/x = t - if t == BitVector::ones() { - if !(x.mcb(BitVector(0)) || x.mcb(BitVector(1))) { - false - } - } - if t != BitVector::ones() { - if mulo(x.0, t) { - false - } - let y = x.constant_bits(); - if y == BitVector(0) { - // (!x.1+BitVector(1) & x.1) is a BitVector with one the first set bit from x.1 set - // Which when added to x.0 is the next bigger BitVector with x.mcb(y) true - let y = y + (!x.1+BitVector(1) & x.1); - if y == BitVector(0) { - false - } - } - if mulo(y, t) { - false - } - true - } - } + }, + Instruction::Divu(_i) => { + unimplemented!() } _ => unimplemented!(), } @@ -635,6 +494,7 @@ mod tests { fn instr_to_str(i: Instruction) -> &'static str { match i { Instruction::Mul(_) => "*", + Instruction::Divu(_) => "/", _ => unimplemented!(), } } @@ -653,25 +513,9 @@ mod tests { let t = BitVector(t); if side == ArgumentSide::Lhs { - assert!( - is_invertable(op, x, s, t, side) == result, - "{:?} {} {:?} == {:?} {}", - x, - instr_to_str(op), - s, - t, - msg - ); + assert_eq!(is_invertable(op, x, s, t, side), result, "{:?} {} {:?} == {:?} {}", x, instr_to_str(op), s, t, msg); } else { - assert!( - is_invertable(op, x, s, t, side) == result, - "{:?} {} {:?} == {:?} {}", - s, - instr_to_str(op), - x, - t, - msg - ); + assert_eq!(is_invertable(op, x, s, t, side), result, "{:?} {} {:?} == {:?} {}", s, instr_to_str(op), x, t, msg); } } @@ -686,15 +530,7 @@ mod tests { let x = TernaryBitVector::lit(x); let s = BitVector(s); let t = BitVector(t); - assert!( - is_consistent(op, x, t) == result, - "{:?} {} {:?} == {:?} {}", - x, - instr_to_str(op), - s, - t, - msg - ); + assert_eq!(is_consistent(op, x, t), result, "{:?} {} {:?} == {:?} {}", x, instr_to_str(op), s, t, msg); } fn test_inverse_value_computation( @@ -780,6 +616,18 @@ mod tests { // TODO: add tests for ADD const MUL: Instruction = Instruction::Mul(RType(0)); + const DIVU: Instruction = Instruction::Divu(RType(0)); + + #[test] + fn check_invertability_condition_for_divu() { + test_invertability(DIVU, "1", 1, 1, ArgumentSide::Rhs, true, "trivial division"); + test_invertability(DIVU, "110", 1, 1, ArgumentSide::Rhs, true, "trivial division"); + + test_invertability(DIVU, "1", 1, 1, ArgumentSide::Lhs, true, "trivial division"); + test_invertability(DIVU, "110", 1, 1, ArgumentSide::Lhs, true, "trivial division"); + + test_invertability(DIVU, "10", 3, 2, ArgumentSide::Lhs, true, "trivial division"); + } #[test] fn check_invertability_condition_for_mul() { diff --git a/src/ternary.rs b/src/ternary.rs index 671ccfba..dbe41e9a 100644 --- a/src/ternary.rs +++ b/src/ternary.rs @@ -72,17 +72,19 @@ impl TernaryBitVector { pub fn constant_bits(&self) -> BitVector { self.0 & self.1 } -} -/// returns true iff s * x => overflow -pub fn mulo(s: BitVector, x: TernaryBitVector) -> bool { - s.0.overflowing_mul(x.0).1 -} -pub fn addo(s: BitVector, x: TernaryBitVector) -> bool { - s.0.overflowing_add(x.0).1 + /*pub fn mulo(s: BitVector, x: TernaryBitVector) -> bool { + s.0.overflowing_mul(x.0).1 + } + + pub fn addo(s: BitVector, x: TernaryBitVector) -> bool { + s.0.overflowing_add(x.0).1 + }*/ } + + impl Shl for TernaryBitVector { type Output = TernaryBitVector; From 5d22fe8054b5e01877af31bf35e456f3b32b1cc5 Mon Sep 17 00:00:00 2001 From: linzalexander Date: Sun, 8 Nov 2020 10:37:34 +0100 Subject: [PATCH 6/9] Arithmetic test added --- src/solver.rs | 86 +++++++++++++++++++++++++------------------ src/ternary.rs | 3 -- symbolic/arithmetic.c | 2 + 3 files changed, 53 insertions(+), 38 deletions(-) diff --git a/src/solver.rs b/src/solver.rs index bfd17545..62db36ae 100644 --- a/src/solver.rs +++ b/src/solver.rs @@ -6,7 +6,6 @@ use crate::ternary::*; use log::{debug, log_enabled, trace, Level}; use petgraph::{visit::EdgeRef, Direction}; use rand::{random, Rng}; -use crate::symbolic_state::Node::Operator; pub type Assignment = Vec; @@ -73,25 +72,26 @@ fn is_invertable( ((-s | s) & t == t) && (s == BitVector(0) || (!s.odd() || x.mcb(t * s.modinverse().unwrap()))) && (s.odd() || (x << s.ctz()).mcb(y(s, t) << s.ctz())) - }, + } BVOperator::Divu => { if d == OperandSide::Lhs { (s * t) / s == t } else { s / (s / t) == t } - }, + } BVOperator::Not => x.mcb(!t), BVOperator::BitwiseAnd => { let c = !(x.lo() ^ x.hi()); (t & s == t) && ((s & x.hi() & c) == (t & c)) - }, + } BVOperator::Equals => { implies(t != BitVector(0), || x.mcb(s)) && implies(t == BitVector(0), || (x.hi() != x.lo()) || (x.hi() != s)) - }, - _ => unimplemented!("can not check invertability for operator: {:?}", op), + } + // all operations are implemented for now + //_ => unimplemented!("can not check invertability for operator: {:?}", op), } } @@ -110,12 +110,13 @@ fn is_consistent(op: BVOperator, x: TernaryBitVector, t: BitVector) -> bool { implies(t != BitVector(0), || x.hi() != BitVector(0)) && implies(t.odd(), || x.hi().lsb() != 0) && implies(!t.odd(), || value_exists(x, t)) - }, + } BVOperator::Divu => { // This is only the case when NOT considering constant bits (see page 5: "Consistency Conditions." in the ternany pop-local-search paper) true - }, - _ => unimplemented!("can not check consistency for operator: {:?}", op), + } + // all operations are implemented for now + //_ => unimplemented!("can not check consistency for operator: {:?}", op), } } @@ -237,19 +238,17 @@ fn compute_inverse_value( let result_with_arbitrary = result | arbitrary_bits; (result_with_arbitrary & !x.constant_bit_mask()) | x.constant_bits() - }, - BVOperator::Divu => { - match d { - OperandSide::Lhs => t * s, - OperandSide::Rhs => s / t - } + } + BVOperator::Divu => match d { + OperandSide::Lhs => t * s, + OperandSide::Rhs => s / t, }, BVOperator::BitwiseAnd => { let fixed_bit_mask = x.constant_bit_mask() | s; let fixed_bits = x.constant_bits() | (s & t); (BitVector(random::()) & !fixed_bit_mask) | fixed_bits - }, + } BVOperator::Equals => { if t == BitVector(0) { loop { @@ -297,14 +296,10 @@ fn compute_consistent_value( BVOperator::Divu => { let v = BitVector(random::()); match d { - OperandSide::Lhs => { - t * v - } - OperandSide::Rhs => { - v / t - } + OperandSide::Lhs => t * v, + OperandSide::Rhs => v / t, } - }, + } BVOperator::BitwiseAnd => { (BitVector(random::()) & !x.constant_bit_mask()) | x.constant_bits() | t } @@ -476,6 +471,7 @@ fn propagate_assignment(f: &Formula, ab: &mut Assignment, n: NodeInde BVOperator::Add => update_binary(f, ab, n, "+", |l, r| l + r), BVOperator::Sub => update_binary(f, ab, n, "-", |l, r| l - r), BVOperator::Mul => update_binary(f, ab, n, "*", |l, r| l * r), + BVOperator::Divu => update_binary(f, ab, n, "/", |l, r| l / r), BVOperator::BitwiseAnd => update_binary(f, ab, n, "&", |l, r| l & r), BVOperator::Equals => update_binary(f, ab, n, "=", |l, r| { if l == r { @@ -491,7 +487,8 @@ fn propagate_assignment(f: &Formula, ab: &mut Assignment, n: NodeInde BitVector(0) } }), - _ => unimplemented!("propagation of operator: {:?}", op), + // all operations are implemented for now + //_ => unimplemented!("propagation of operator: {:?}", op), } f.neighbors_directed(n, Direction::Outgoing) .for_each(|n| propagate_assignment(f, ab, n)); @@ -603,7 +600,6 @@ fn sat( #[cfg(test)] mod tests { use super::*; - use crate::symbolic_state::Node::Operator; fn create_formula_with_input() -> (Formula, NodeIndex) { let mut formula = Formula::new(); @@ -688,10 +684,28 @@ mod tests { match d { OperandSide::Lhs => { - assert_eq!(is_invertable(op, x, s, t, d), result, "{:?} {:?} {:?} == {:?} {}", x, op, s, t, msg); + assert_eq!( + is_invertable(op, x, s, t, d), + result, + "{:?} {:?} {:?} == {:?} {}", + x, + op, + s, + t, + msg + ); } OperandSide::Rhs => { - assert_eq!(is_invertable(op, x, s, t, d), result, "{:?} {:?} {:?} == {:?} {}", s, op, x, t, msg); + assert_eq!( + is_invertable(op, x, s, t, d), + result, + "{:?} {:?} {:?} == {:?} {}", + s, + op, + x, + t, + msg + ); } } } @@ -699,7 +713,15 @@ mod tests { fn test_consistence(op: BVOperator, x: &'static str, t: u64, result: bool, msg: &'static str) { let x = TernaryBitVector::lit(x); let t = BitVector(t); - assert_eq!(is_consistent(op, x, t), result, "{:?} {:?} s == {:?} {}", x, op, t, msg); + assert_eq!( + is_consistent(op, x, t), + result, + "{:?} {:?} s == {:?} {}", + x, + op, + t, + msg + ); } fn test_inverse_value_computation( @@ -744,7 +766,6 @@ mod tests { ); } } - } fn test_consistent_value_computation( @@ -778,11 +799,9 @@ mod tests { "choose values which are invertable..." ); - compute_inverse_value(op, x, computed, t, d.other()) - }, - BVOperator::Divu => { compute_inverse_value(op, x, computed, t, d.other()) } + BVOperator::Divu => compute_inverse_value(op, x, computed, t, d.other()), _ => unimplemented!(), }; @@ -879,7 +898,6 @@ mod tests { #[test] fn compute_inverse_values_for_divu() { - fn f(l: BitVector, r: BitVector) -> BitVector { l / r } @@ -907,7 +925,6 @@ mod tests { test_inverse_value_computation(MUL, "**0", 0b10, 0b1100, side, f); } - #[test] fn check_consistency_condition_for_divu() { //always true till constant bits @@ -934,7 +951,6 @@ mod tests { #[test] fn compute_consistent_values_for_divu() { - fn f(l: BitVector, r: BitVector) -> BitVector { l / r } diff --git a/src/ternary.rs b/src/ternary.rs index e52be5c5..f5b8139f 100644 --- a/src/ternary.rs +++ b/src/ternary.rs @@ -81,7 +81,6 @@ impl TernaryBitVector { self.0 & self.1 } - /*pub fn mulo(s: BitVector, x: TernaryBitVector) -> bool { s.0.overflowing_mul(x.0).1 } @@ -91,8 +90,6 @@ impl TernaryBitVector { }*/ } - - impl Shl for TernaryBitVector { type Output = TernaryBitVector; diff --git a/symbolic/arithmetic.c b/symbolic/arithmetic.c index 9920275f..c8c82a96 100644 --- a/symbolic/arithmetic.c +++ b/symbolic/arithmetic.c @@ -16,6 +16,8 @@ uint64_t main() { b = b + a; + b = b / 2; + c = b - c; return c; From 4007f65ec09c229e7cf59b5f6056a443d50a1b5f Mon Sep 17 00:00:00 2001 From: LexMonster Date: Thu, 12 Nov 2020 13:16:56 +0100 Subject: [PATCH 7/9] Clearer panics and Z3 implementation --- src/solver.rs | 18 ++++++------------ src/z3.rs | 1 + 2 files changed, 7 insertions(+), 12 deletions(-) diff --git a/src/solver.rs b/src/solver.rs index 2531167e..cf566b3d 100644 --- a/src/solver.rs +++ b/src/solver.rs @@ -83,13 +83,13 @@ fn is_invertable( } BVOperator::Divu => { if s == BitVector(0) || t == BitVector(0) { - return false + return false; } if d == OperandSide::Lhs { (s * t) / s == t } else { if t > s { - return false + return false; } s / (s / t) == t } @@ -104,8 +104,6 @@ fn is_invertable( implies(t != BitVector(0), || x.mcb(s)) && implies(t == BitVector(0), || (x.hi() != x.lo()) || (x.hi() != s)) } - // all operations are implemented for now - //_ => unimplemented!("can not check invertability for operator: {:?}", op), } } @@ -129,8 +127,6 @@ fn is_consistent(op: BVOperator, x: TernaryBitVector, t: BitVector) -> bool { // This is only the case when NOT considering constant bits (see page 5: "Consistency Conditions." in the ternany pop-local-search paper) true } - // all operations are implemented for now - //_ => unimplemented!("can not check consistency for operator: {:?}", op), } } @@ -277,7 +273,7 @@ fn compute_inverse_value( s } } - _ => unimplemented!("compute inverse value for binary operator: {:?}", op), + _ => unreachable!("unkown operator or unary operator: {:?}", op), } } @@ -319,7 +315,7 @@ fn compute_consistent_value( BVOperator::BitwiseAnd => { (BitVector(random::()) & !x.constant_bit_mask()) | x.constant_bits() | t } - _ => unimplemented!("compute consitent value for binary operator: {:?}", op), + _ => unreachable!("unkown operator for consistent value: {:?}", op), } } @@ -327,7 +323,7 @@ fn compute_consistent_value( fn is_invertable_for_unary_op(op: BVOperator, x: TernaryBitVector, t: BitVector) -> bool { match op { BVOperator::Not => x.mcb(!t), - _ => unimplemented!("compute inverse value for unary operator: {:?}", op), + _ => unreachable!("not unary operator: {:?}", op), } } @@ -344,7 +340,7 @@ fn compute_inverse_value_for_unary_op( BitVector(0) } } - _ => unimplemented!("compute consistent value for unary operator: {:?}", op), + _ => unreachable!("not unary operator: {:?}", op), } } @@ -493,8 +489,6 @@ fn propagate_assignment(f: &Formula, ab: &mut Assignment, n: SymbolId BitVector(0) } }), - // all operations are implemented for now - //_ => unimplemented!("propagation of operator: {:?}", op), } f.neighbors_directed(n, Direction::Outgoing) .for_each(|n| propagate_assignment(f, ab, n)); diff --git a/src/z3.rs b/src/z3.rs index 93942336..96522c3c 100644 --- a/src/z3.rs +++ b/src/z3.rs @@ -91,6 +91,7 @@ fn traverse<'ctx>( BVOperator::Add => traverse_binary!(lhs, bvadd, rhs, graph, ctx, bvs), BVOperator::Sub => traverse_binary!(lhs, bvsub, rhs, graph, ctx, bvs), BVOperator::Mul => traverse_binary!(lhs, bvmul, rhs, graph, ctx, bvs), + BVOperator::Divu => traverse_binary!(lhs, bvudiv, rhs, graph, ctx, bvs), BVOperator::Equals => traverse_binary!(lhs, _eq, rhs, graph, ctx, bvs), BVOperator::BitwiseAnd => traverse_binary!(lhs, bvand, rhs, graph, ctx, bvs), i => unimplemented!("binary operator: {:?}", i), From efcb3bbc30f873801637df5f562bf5efaf9d82f1 Mon Sep 17 00:00:00 2001 From: alexanderlackner Date: Sat, 14 Nov 2020 10:20:47 +0100 Subject: [PATCH 8/9] sltu now working but divu needs some work done --- src/solver.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/solver.rs b/src/solver.rs index 09aff093..22f4351a 100644 --- a/src/solver.rs +++ b/src/solver.rs @@ -318,7 +318,7 @@ fn compute_inverse_value( // therefore we need a random x that's x.1>=x>s BitVector(thread_rng().sample(Uniform::new_inclusive(s.0 + 1, x.hi().0))) } - }, + } BVOperator::Divu => match d { OperandSide::Lhs => t * s, OperandSide::Rhs => s / t, @@ -379,7 +379,7 @@ fn compute_consistent_value( OperandSide::Lhs => t * v, OperandSide::Rhs => v / t, } - }, + } BVOperator::Sltu => { if d == OperandSide::Lhs { if t == BitVector(0) { @@ -907,29 +907,29 @@ mod tests { compute_inverse_value(op, x, computed, t, d.other()) } - BVOperator::Sltu => compute_inverse_value(op, x, computed, t, d.other()), + BVOperator::Sltu => compute_inverse_value(op, x, computed, t, d), BVOperator::Divu => compute_inverse_value(op, x, computed, t, d.other()), _ => unimplemented!(), }; if d == OperandSide::Lhs { assert_eq!( - f(computed, inverse), + f(inverse, computed), t, "{:?} {:?} {:?} == {:?}", - computed, - op, inverse, + op, + computed, t ); } else { assert_eq!( - f(inverse, computed), + f(computed, inverse), t, "{:?} {:?} {:?} == {:?}", - inverse, - op, computed, + op, + inverse, t ); } From b795d93b10962983a4c9fcd2b45e7ff3c3bd896c Mon Sep 17 00:00:00 2001 From: LexMonster Date: Sat, 14 Nov 2020 10:34:24 +0100 Subject: [PATCH 9/9] Inverse value fixed --- src/solver.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/solver.rs b/src/solver.rs index 22f4351a..1fe2c651 100644 --- a/src/solver.rs +++ b/src/solver.rs @@ -376,8 +376,8 @@ fn compute_consistent_value( BVOperator::Divu => { let v = BitVector(random::()); match d { - OperandSide::Lhs => t * v, - OperandSide::Rhs => v / t, + OperandSide::Lhs => v / t, + OperandSide::Rhs => t * v, } } BVOperator::Sltu => { @@ -901,14 +901,14 @@ mod tests { let x = TernaryBitVector::new(0, u64::max_value()); assert!( - is_invertable(op, x, computed, t, d.other()), + is_invertable(op, x, computed, t, d), "choose values which are invertable..." ); - compute_inverse_value(op, x, computed, t, d.other()) + 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.other()), + BVOperator::Divu => compute_inverse_value(op, x, computed, t, d), _ => unimplemented!(), };