GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/util/bitvector_black.cpp Lines: 124 124 100.0 %
Date: 2021-03-23 Branches: 476 1696 28.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bitvector_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Black box testing of CVC4::BitVector
13
 **
14
 ** Black box testing of CVC4::BitVector.
15
 **/
16
17
#include <sstream>
18
19
#include "test.h"
20
#include "util/bitvector.h"
21
22
namespace CVC4 {
23
namespace test {
24
25
40
class TestUtilBlackBitVector : public TestInternal
26
{
27
 protected:
28
20
  void SetUp() override
29
  {
30
20
    d_zero = BitVector(4);
31
20
    d_one = BitVector::mkOne(4);
32
20
    d_two = BitVector("0010", 2);
33
20
    d_neg_one = BitVector(4, Integer(-1));
34
20
    d_ones = BitVector::mkOnes(4);
35
20
  }
36
37
  BitVector d_zero;
38
  BitVector d_one;
39
  BitVector d_two;
40
  BitVector d_neg_one;
41
  BitVector d_ones;
42
};
43
44
19
TEST_F(TestUtilBlackBitVector, string_constructor)
45
{
46
4
  BitVector b1("0101", 2);
47
2
  ASSERT_EQ(4u, b1.getSize());
48
2
  ASSERT_EQ("0101", b1.toString());
49
2
  ASSERT_EQ("5", b1.toString(10));
50
2
  ASSERT_EQ("5", b1.toString(16));
51
52
4
  BitVector b2("000001", 2);
53
2
  ASSERT_EQ(6u, b2.getSize());
54
2
  ASSERT_EQ("000001", b2.toString());
55
2
  ASSERT_EQ("1", b2.toString(10));
56
2
  ASSERT_EQ("1", b2.toString(16));
57
58
4
  BitVector b3("7f", 16);
59
2
  ASSERT_EQ(8u, b3.getSize());
60
2
  ASSERT_EQ("01111111", b3.toString());
61
2
  ASSERT_EQ("127", b3.toString(10));
62
2
  ASSERT_EQ("7f", b3.toString(16));
63
64
4
  BitVector b4("01a", 16);
65
2
  ASSERT_EQ(12u, b4.getSize());
66
2
  ASSERT_EQ("000000011010", b4.toString());
67
2
  ASSERT_EQ("26", b4.toString(10));
68
2
  ASSERT_EQ("1a", b4.toString(16));
69
}
70
71
19
TEST_F(TestUtilBlackBitVector, conversions)
72
{
73
2
  ASSERT_EQ(d_two.toSignedInteger(), Integer(2));
74
2
  ASSERT_EQ(d_neg_one.toString(), "1111");
75
2
  ASSERT_EQ(d_neg_one.getValue(), Integer(15));
76
2
  ASSERT_EQ(d_neg_one.getSize(), 4);
77
2
  ASSERT_EQ(d_neg_one.toInteger(), Integer(15));
78
2
  ASSERT_EQ(d_neg_one.toSignedInteger(), Integer(-1));
79
80
2
  ASSERT_EQ(d_zero.hash(), (d_one - d_one).hash());
81
2
  ASSERT_NE(d_neg_one.hash(), d_zero.hash());
82
}
83
84
19
TEST_F(TestUtilBlackBitVector, setBit_getBit)
85
{
86
4
  BitVector ones(d_one);
87
2
  ASSERT_EQ(ones.setBit(1, true).setBit(2, true).setBit(3, true), d_ones);
88
89
4
  BitVector zero(d_ones);
90
2
  ASSERT_EQ(
91
      zero.setBit(0, false).setBit(1, false).setBit(2, false).setBit(3, false),
92
2
      d_zero);
93
94
2
  ones = d_ones;
95
2
  ASSERT_EQ(ones.setBit(0, false).setBit(0, true), d_ones);
96
97
4
  BitVector not_one(d_ones);
98
2
  ASSERT_EQ(not_one.setBit(0, false), ~BitVector::mkOne(d_one.getSize()));
99
100
2
  ASSERT_TRUE(d_ones.isBitSet(3));
101
2
  ASSERT_FALSE(d_two.isBitSet(3));
102
103
2
  ASSERT_EQ(d_one.getValue(), Integer(1));
104
2
  ASSERT_EQ(d_zero.isPow2(), 0);
105
2
  ASSERT_EQ(d_one.isPow2(), 1);
106
2
  ASSERT_EQ(d_two.isPow2(), 2);
107
2
  ASSERT_EQ(d_ones.isPow2(), 0);
108
}
109
110
19
TEST_F(TestUtilBlackBitVector, concat_extract)
111
{
112
4
  BitVector b = d_one.concat(d_zero);
113
2
  ASSERT_EQ(b.toString(), "00010000");
114
2
  ASSERT_EQ(b.extract(7, 4), d_one);
115
4
  ASSERT_THROW(b.extract(4, 7), IllegalArgumentException);
116
4
  ASSERT_THROW(b.extract(8, 3), IllegalArgumentException);
117
2
  ASSERT_EQ(b.concat(BitVector()), b);
118
}
119
120
19
TEST_F(TestUtilBlackBitVector, comparisons)
121
{
122
2
  ASSERT_NE(d_zero, d_one);
123
2
  ASSERT_TRUE(d_neg_one > d_zero);
124
2
  ASSERT_TRUE(d_neg_one >= d_zero);
125
2
  ASSERT_TRUE(d_neg_one >= d_neg_one);
126
2
  ASSERT_TRUE(d_neg_one == d_neg_one);
127
2
  ASSERT_TRUE(d_zero.unsignedLessThan(d_neg_one));
128
2
  ASSERT_TRUE(d_zero.unsignedLessThanEq(d_neg_one));
129
2
  ASSERT_TRUE(d_zero.unsignedLessThanEq(d_zero));
130
2
  ASSERT_TRUE(d_zero < d_neg_one);
131
2
  ASSERT_TRUE(d_zero <= d_neg_one);
132
2
  ASSERT_TRUE(d_zero <= d_zero);
133
2
  ASSERT_TRUE(d_neg_one.signedLessThan(d_zero));
134
2
  ASSERT_TRUE(d_neg_one.signedLessThanEq(d_zero));
135
2
  ASSERT_TRUE(d_neg_one.signedLessThanEq(d_neg_one));
136
137
4
  BitVector b = d_neg_one.concat(d_neg_one);
138
4
  ASSERT_THROW(b.unsignedLessThan(d_neg_one), IllegalArgumentException);
139
4
  ASSERT_THROW(d_neg_one.unsignedLessThanEq(b), IllegalArgumentException);
140
4
  ASSERT_THROW(b.signedLessThan(d_neg_one), IllegalArgumentException);
141
4
  ASSERT_THROW(d_neg_one.signedLessThanEq(b), IllegalArgumentException);
142
}
143
144
19
TEST_F(TestUtilBlackBitVector, bitwise_operators)
145
{
146
2
  ASSERT_EQ((d_one ^ d_neg_one).toString(), "1110");
147
2
  ASSERT_EQ((d_two | d_one).toString(), "0011");
148
2
  ASSERT_EQ((d_neg_one & d_two).toString(), "0010");
149
2
  ASSERT_EQ((~d_two).toString(), "1101");
150
}
151
152
19
TEST_F(TestUtilBlackBitVector, arithmetic)
153
{
154
2
  ASSERT_EQ(d_neg_one + d_one, d_zero);
155
2
  ASSERT_EQ((d_neg_one - d_one).getValue(), Integer(14));
156
2
  ASSERT_EQ((-d_neg_one).getValue(), Integer(1));
157
158
2
  ASSERT_EQ((d_two * (d_two + d_one)).getValue(), Integer(6));
159
160
2
  ASSERT_EQ(d_two.unsignedDivTotal(d_zero), d_neg_one);
161
2
  ASSERT_EQ(d_neg_one.unsignedDivTotal(d_two).getValue(), Integer(7));
162
163
2
  ASSERT_EQ(d_two.unsignedRemTotal(d_zero), d_two);
164
2
  ASSERT_EQ(d_neg_one.unsignedRemTotal(d_two), d_one);
165
166
4
  BitVector b = d_neg_one.concat(d_neg_one);
167
4
  ASSERT_THROW(b + d_neg_one, IllegalArgumentException);
168
4
  ASSERT_THROW(d_neg_one * b, IllegalArgumentException);
169
4
  ASSERT_THROW(b.unsignedDivTotal(d_neg_one), IllegalArgumentException);
170
4
  ASSERT_THROW(d_neg_one.unsignedRemTotal(b), IllegalArgumentException);
171
}
172
173
19
TEST_F(TestUtilBlackBitVector, extend_operators)
174
{
175
2
  ASSERT_EQ(d_one.zeroExtend(4), d_zero.concat(d_one));
176
2
  ASSERT_EQ(d_one.zeroExtend(0), d_one);
177
2
  ASSERT_EQ(d_neg_one.signExtend(4), d_neg_one.concat(d_neg_one));
178
2
  ASSERT_EQ(d_one.signExtend(4), d_zero.concat(d_one));
179
2
  ASSERT_EQ(d_one.signExtend(0), d_one);
180
}
181
182
19
TEST_F(TestUtilBlackBitVector, shift_operators)
183
{
184
2
  ASSERT_EQ(d_one.leftShift(d_one), d_two);
185
2
  ASSERT_EQ(d_one.leftShift(d_neg_one), d_zero);
186
2
  ASSERT_EQ(d_one.leftShift(d_zero), d_one);
187
188
2
  ASSERT_EQ(d_two.logicalRightShift(d_one), d_one);
189
2
  ASSERT_EQ(d_two.logicalRightShift(d_neg_one), d_zero);
190
191
2
  ASSERT_EQ(d_two.arithRightShift(d_one), d_one);
192
2
  ASSERT_EQ(d_neg_one.arithRightShift(d_one), d_neg_one);
193
2
  ASSERT_EQ(d_neg_one.arithRightShift(d_neg_one), d_neg_one);
194
2
  ASSERT_EQ(d_two.arithRightShift(d_neg_one), d_zero);
195
}
196
197
19
TEST_F(TestUtilBlackBitVector, static_helpers)
198
{
199
2
  ASSERT_EQ(BitVector::mkZero(4), d_zero);
200
2
  ASSERT_EQ(BitVector::mkOne(4), d_one);
201
2
  ASSERT_EQ(BitVector::mkOnes(4), d_neg_one);
202
2
  ASSERT_EQ(BitVector::mkMinSigned(4).toSignedInteger(), Integer(-8));
203
2
  ASSERT_EQ(BitVector::mkMaxSigned(4).toSignedInteger(), Integer(7));
204
}
205
}  // namespace test
206
33
}  // namespace CVC4