From cb8e3b305ecf83cde0380f9198fa6d3f795362cd Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 23 Feb 2018 18:02:53 -0800 Subject: [PATCH] Add unit tests for BitVector, minor BV rewrite fix (#1622) This commit adds unit tests for the BitVector class and adds some additional argument checks. Additionally, it fixes a minor issue in the ZeroExtendUltConst rule if the zero_extend was by 0 bits. In that case, the rule was calling BitVector::extract() with high < low. --- .../theory_bv_rewrite_rules_simplification.h | 9 +- src/util/bitvector.cpp | 2 + test/unit/util/bitvector_black.h | 183 +++++++++++++++--- 3 files changed, 167 insertions(+), 27 deletions(-) diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index d91067d1e..a4be19253 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1303,10 +1303,13 @@ inline bool RewriteRule::applies(TNode node) { t = node[1][0]; c = node[0]; } - BitVector bv_c = c.getConst(); - BitVector bv_max = - BitVector(utils::getSize(c)).setBit(utils::getSize(t) - 1); + if (utils::getSize(t) == utils::getSize(c)) + { + return false; + } + + BitVector bv_c = c.getConst(); BitVector c_hi = c.getConst().extract(utils::getSize(c) - 1, utils::getSize(t)); BitVector zero = BitVector(c_hi.getSize(), Integer(0)); diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index 2d94be875..549c94dc9 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -90,6 +90,8 @@ BitVector BitVector::concat(const BitVector& other) const BitVector BitVector::extract(unsigned high, unsigned low) const { + CheckArgument(high < d_size, high); + CheckArgument(low <= high, low); return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low)); } diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h index 254abc905..98d148185 100644 --- a/test/unit/util/bitvector_black.h +++ b/test/unit/util/bitvector_black.h @@ -26,30 +26,165 @@ class BitVectorBlack : public CxxTest::TestSuite { public: + void setUp() + { + zero = BitVector(4); + one = zero.setBit(0); + two = BitVector("0010", 2); + negOne = BitVector(4, Integer(-1)); + } - void testStringConstructor() { - BitVector b1("0101",2); - TS_ASSERT_EQUALS( 4u, b1.getSize() ); - TS_ASSERT_EQUALS( "0101", b1.toString() ); - TS_ASSERT_EQUALS( "5", b1.toString(10) ); - TS_ASSERT_EQUALS( "5", b1.toString(16) ); - - BitVector b2("000001", 2); - TS_ASSERT_EQUALS( 6u, b2.getSize() ); - TS_ASSERT_EQUALS( "000001", b2.toString() ); - TS_ASSERT_EQUALS( "1", b2.toString(10) ); - TS_ASSERT_EQUALS( "1", b2.toString(16) ); - - BitVector b3("7f", 16); - TS_ASSERT_EQUALS( 8u, b3.getSize() ); - TS_ASSERT_EQUALS( "01111111", b3.toString() ); - TS_ASSERT_EQUALS( "127", b3.toString(10) ); - TS_ASSERT_EQUALS( "7f", b3.toString(16) ); - - BitVector b4("01a", 16); - TS_ASSERT_EQUALS( 12u, b4.getSize() ); - TS_ASSERT_EQUALS( "000000011010", b4.toString() ); - TS_ASSERT_EQUALS( "26", b4.toString(10) ); - TS_ASSERT_EQUALS( "1a", b4.toString(16) ); + void testStringConstructor() + { + BitVector b1("0101", 2); + TS_ASSERT_EQUALS(4u, b1.getSize()); + TS_ASSERT_EQUALS("0101", b1.toString()); + TS_ASSERT_EQUALS("5", b1.toString(10)); + TS_ASSERT_EQUALS("5", b1.toString(16)); + + BitVector b2("000001", 2); + TS_ASSERT_EQUALS(6u, b2.getSize()); + TS_ASSERT_EQUALS("000001", b2.toString()); + TS_ASSERT_EQUALS("1", b2.toString(10)); + TS_ASSERT_EQUALS("1", b2.toString(16)); + + BitVector b3("7f", 16); + TS_ASSERT_EQUALS(8u, b3.getSize()); + TS_ASSERT_EQUALS("01111111", b3.toString()); + TS_ASSERT_EQUALS("127", b3.toString(10)); + TS_ASSERT_EQUALS("7f", b3.toString(16)); + + BitVector b4("01a", 16); + TS_ASSERT_EQUALS(12u, b4.getSize()); + TS_ASSERT_EQUALS("000000011010", b4.toString()); + TS_ASSERT_EQUALS("26", b4.toString(10)); + TS_ASSERT_EQUALS("1a", b4.toString(16)); + } + + void testConversions() + { + TS_ASSERT_EQUALS(two.toSignedInteger(), Integer(2)); + TS_ASSERT_EQUALS(negOne.toString(), "1111"); + TS_ASSERT_EQUALS(negOne.getValue(), Integer(15)); + TS_ASSERT_EQUALS(negOne.getSize(), 4); + TS_ASSERT_EQUALS(negOne.toInteger(), Integer(15)); + TS_ASSERT_EQUALS(negOne.toSignedInteger(), Integer(-1)); + + TS_ASSERT_EQUALS(zero.hash(), (one - one).hash()); + TS_ASSERT_DIFFERS(negOne.hash(), zero.hash()); + } + + void testSetGetBit() + { + TS_ASSERT_EQUALS(one.setBit(1).setBit(2).setBit(3), negOne); + + TS_ASSERT(negOne.isBitSet(3)); + TS_ASSERT(!two.isBitSet(3)); + + TS_ASSERT_EQUALS(one.getValue(), Integer(1)); + TS_ASSERT_EQUALS(zero.isPow2(), 0); + TS_ASSERT_EQUALS(one.isPow2(), 1); + TS_ASSERT_EQUALS(two.isPow2(), 2); + TS_ASSERT_EQUALS(negOne.isPow2(), 0); + } + + void testConcatExtract() + { + BitVector b = one.concat(zero); + TS_ASSERT_EQUALS(b.toString(), "00010000"); + TS_ASSERT_EQUALS(b.extract(7, 4), one); + TS_ASSERT_THROWS(b.extract(4, 7), IllegalArgumentException); + TS_ASSERT_THROWS(b.extract(8, 3), IllegalArgumentException); + TS_ASSERT_EQUALS(b.concat(BitVector()), b); + } + + void testComparisons() + { + TS_ASSERT_DIFFERS(zero, one); + TS_ASSERT(negOne > zero); + TS_ASSERT(negOne >= zero); + TS_ASSERT(negOne >= negOne); + TS_ASSERT(negOne == negOne); + TS_ASSERT(zero.unsignedLessThan(negOne)); + TS_ASSERT(zero.unsignedLessThanEq(negOne)); + TS_ASSERT(zero.unsignedLessThanEq(zero)); + TS_ASSERT(zero < negOne); + TS_ASSERT(zero <= negOne); + TS_ASSERT(zero <= zero); + TS_ASSERT(negOne.signedLessThan(zero)); + TS_ASSERT(negOne.signedLessThanEq(zero)); + TS_ASSERT(negOne.signedLessThanEq(negOne)); + + BitVector b = negOne.concat(negOne); + TS_ASSERT_THROWS(b.unsignedLessThan(negOne), IllegalArgumentException); + TS_ASSERT_THROWS(negOne.unsignedLessThanEq(b), IllegalArgumentException); + TS_ASSERT_THROWS(b.signedLessThan(negOne), IllegalArgumentException); + TS_ASSERT_THROWS(negOne.signedLessThanEq(b), IllegalArgumentException); + } + + void testBitwiseOps() + { + TS_ASSERT_EQUALS((one ^ negOne).toString(), "1110"); + TS_ASSERT_EQUALS((two | one).toString(), "0011"); + TS_ASSERT_EQUALS((negOne & two).toString(), "0010"); + TS_ASSERT_EQUALS((~two).toString(), "1101"); + } + + void testArithmetic() + { + TS_ASSERT_EQUALS(negOne + one, zero); + TS_ASSERT_EQUALS((negOne - one).getValue(), Integer(14)); + TS_ASSERT_EQUALS((-negOne).getValue(), Integer(1)); + + TS_ASSERT_EQUALS((two * (two + one)).getValue(), Integer(6)); + + TS_ASSERT_EQUALS(two.unsignedDivTotal(zero), negOne); + TS_ASSERT_EQUALS(negOne.unsignedDivTotal(two).getValue(), Integer(7)); + + TS_ASSERT_EQUALS(two.unsignedRemTotal(zero), two); + TS_ASSERT_EQUALS(negOne.unsignedRemTotal(two), one); + + BitVector b = negOne.concat(negOne); + TS_ASSERT_THROWS(b + negOne, IllegalArgumentException); + TS_ASSERT_THROWS(negOne * b, IllegalArgumentException); + TS_ASSERT_THROWS(b.unsignedDivTotal(negOne), IllegalArgumentException); + TS_ASSERT_THROWS(negOne.unsignedRemTotal(b), IllegalArgumentException); + } + + void testExtendOps() + { + TS_ASSERT_EQUALS(one.zeroExtend(4), zero.concat(one)); + TS_ASSERT_EQUALS(one.zeroExtend(0), one); + TS_ASSERT_EQUALS(negOne.signExtend(4), negOne.concat(negOne)); + TS_ASSERT_EQUALS(one.signExtend(4), zero.concat(one)); + TS_ASSERT_EQUALS(one.signExtend(0), one); + } + + void testShifts() + { + TS_ASSERT_EQUALS(one.leftShift(one), two); + TS_ASSERT_EQUALS(one.leftShift(negOne), zero); + TS_ASSERT_EQUALS(one.leftShift(zero), one); + + TS_ASSERT_EQUALS(two.logicalRightShift(one), one); + TS_ASSERT_EQUALS(two.logicalRightShift(negOne), zero); + + TS_ASSERT_EQUALS(two.arithRightShift(one), one); + TS_ASSERT_EQUALS(negOne.arithRightShift(one), negOne); + TS_ASSERT_EQUALS(negOne.arithRightShift(negOne), negOne); + TS_ASSERT_EQUALS(two.arithRightShift(negOne), zero); + } + + void testStaticHelpers() + { + TS_ASSERT_EQUALS(BitVector::mkOnes(4), negOne); + TS_ASSERT_EQUALS(BitVector::mkMinSigned(4).toSignedInteger(), Integer(-8)); + TS_ASSERT_EQUALS(BitVector::mkMaxSigned(4).toSignedInteger(), Integer(7)); } + + private: + BitVector zero; + BitVector one; + BitVector two; + BitVector negOne; }; -- 2.30.2