GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/bitvector.cpp Lines: 171 171 100.0 %
Date: 2021-03-22 Branches: 178 316 56.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bitvector.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Liana Hadarean, Morgan Deters
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 A fixed-size bit-vector.
13
 **
14
 ** A fixed-size bit-vector, implemented as a wrapper around Integer.
15
 **
16
 ** \todo document this file
17
 **/
18
19
#include "util/bitvector.h"
20
21
#include "base/exception.h"
22
23
namespace CVC4 {
24
25
534131
unsigned BitVector::getSize() const { return d_size; }
26
27
115937
const Integer& BitVector::getValue() const { return d_value; }
28
29
36932
Integer BitVector::toInteger() const { return d_value; }
30
31
385852
Integer BitVector::toSignedInteger() const
32
{
33
385852
  unsigned size = d_size;
34
771704
  Integer sign_bit = d_value.extractBitRange(1, size - 1);
35
771704
  Integer val = d_value.extractBitRange(size - 1, 0);
36
385852
  Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
37
771704
  return res;
38
}
39
40
333763
std::string BitVector::toString(unsigned int base) const
41
{
42
667526
  std::string str = d_value.toString(base);
43
333763
  if (base == 2 && d_size > str.size())
44
  {
45
426
    std::string zeroes;
46
2248
    for (unsigned int i = 0; i < d_size - str.size(); ++i)
47
    {
48
2035
      zeroes.append("0");
49
    }
50
213
    return zeroes + str;
51
  }
52
  else
53
  {
54
333550
    return str;
55
  }
56
}
57
58
3625742
size_t BitVector::hash() const
59
{
60
3625742
  return d_value.hash() + d_size;
61
}
62
63
1811
BitVector& BitVector::setBit(uint32_t i, bool value)
64
{
65
1811
  CheckArgument(i < d_size, i);
66
1811
  d_value.setBit(i, value);
67
1811
  return *this;
68
}
69
70
73032
bool BitVector::isBitSet(uint32_t i) const
71
{
72
73032
  CheckArgument(i < d_size, i);
73
73032
  return d_value.isBitSet(i);
74
}
75
76
516697
unsigned BitVector::isPow2() const
77
{
78
516697
  return d_value.isPow2();
79
}
80
81
/* -----------------------------------------------------------------------
82
 ** Operators
83
 * ----------------------------------------------------------------------- */
84
85
/* String Operations ----------------------------------------------------- */
86
87
159457
BitVector BitVector::concat(const BitVector& other) const
88
{
89
159457
  return BitVector(d_size + other.d_size,
90
318914
                   (d_value.multiplyByPow2(other.d_size)) + other.d_value);
91
}
92
93
365157
BitVector BitVector::extract(unsigned high, unsigned low) const
94
{
95
365157
  CheckArgument(high < d_size, high);
96
365155
  CheckArgument(low <= high, low);
97
365153
  return BitVector(high - low + 1,
98
730306
                   d_value.extractBitRange(high - low + 1, low));
99
}
100
101
/* (Dis)Equality --------------------------------------------------------- */
102
103
23694925
bool BitVector::operator==(const BitVector& y) const
104
{
105
23694925
  if (d_size != y.d_size) return false;
106
22874664
  return d_value == y.d_value;
107
}
108
109
1018929
bool BitVector::operator!=(const BitVector& y) const
110
{
111
1018929
  if (d_size != y.d_size) return true;
112
1018929
  return d_value != y.d_value;
113
}
114
115
/* Unsigned Inequality --------------------------------------------------- */
116
117
8179974
bool BitVector::operator<(const BitVector& y) const
118
{
119
8179974
  return d_value < y.d_value;
120
}
121
122
935801
bool BitVector::operator<=(const BitVector& y) const
123
{
124
935801
  return d_value <= y.d_value;
125
}
126
127
3539
bool BitVector::operator>(const BitVector& y) const
128
{
129
3539
  return d_value > y.d_value;
130
}
131
132
794
bool BitVector::operator>=(const BitVector& y) const
133
{
134
794
  return d_value >= y.d_value;
135
}
136
137
7654
bool BitVector::unsignedLessThan(const BitVector& y) const
138
{
139
7654
  CheckArgument(d_size == y.d_size, y);
140
7652
  CheckArgument(d_value >= 0, this);
141
7652
  CheckArgument(y.d_value >= 0, y);
142
7652
  return d_value < y.d_value;
143
}
144
145
521
bool BitVector::unsignedLessThanEq(const BitVector& y) const
146
{
147
523
  CheckArgument(d_size == y.d_size, this);
148
519
  CheckArgument(d_value >= 0, this);
149
519
  CheckArgument(y.d_value >= 0, y);
150
519
  return d_value <= y.d_value;
151
}
152
153
/* Signed Inequality ----------------------------------------------------- */
154
155
9297
bool BitVector::signedLessThan(const BitVector& y) const
156
{
157
9297
  CheckArgument(d_size == y.d_size, y);
158
9295
  CheckArgument(d_value >= 0, this);
159
9295
  CheckArgument(y.d_value >= 0, y);
160
18590
  Integer a = (*this).toSignedInteger();
161
18590
  Integer b = y.toSignedInteger();
162
163
18590
  return a < b;
164
}
165
166
183626
bool BitVector::signedLessThanEq(const BitVector& y) const
167
{
168
183626
  CheckArgument(d_size == y.d_size, y);
169
183624
  CheckArgument(d_value >= 0, this);
170
183624
  CheckArgument(y.d_value >= 0, y);
171
367248
  Integer a = (*this).toSignedInteger();
172
367248
  Integer b = y.toSignedInteger();
173
174
367248
  return a <= b;
175
}
176
177
/* Bit-wise operations --------------------------------------------------- */
178
179
716
BitVector BitVector::operator^(const BitVector& y) const
180
{
181
716
  CheckArgument(d_size == y.d_size, y);
182
716
  return BitVector(d_size, d_value.bitwiseXor(y.d_value));
183
}
184
185
452453
BitVector BitVector::operator|(const BitVector& y) const
186
{
187
452453
  CheckArgument(d_size == y.d_size, y);
188
452453
  return BitVector(d_size, d_value.bitwiseOr(y.d_value));
189
}
190
191
280990
BitVector BitVector::operator&(const BitVector& y) const
192
{
193
280990
  CheckArgument(d_size == y.d_size, y);
194
280990
  return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
195
}
196
197
1351635
BitVector BitVector::operator~() const
198
{
199
1351635
  return BitVector(d_size, d_value.bitwiseNot());
200
}
201
202
/* Arithmetic operations ------------------------------------------------- */
203
204
7289649
BitVector BitVector::operator+(const BitVector& y) const
205
{
206
7289649
  CheckArgument(d_size == y.d_size, y);
207
14579294
  Integer sum = d_value + y.d_value;
208
14579294
  return BitVector(d_size, sum);
209
}
210
211
351984
BitVector BitVector::operator-(const BitVector& y) const
212
{
213
351984
  CheckArgument(d_size == y.d_size, y);
214
  // to maintain the invariant that we are only adding BitVectors of the
215
  // same size
216
703968
  BitVector one(d_size, Integer(1));
217
703968
  return *this + ~y + one;
218
}
219
220
826776
BitVector BitVector::operator-() const
221
{
222
1653552
  BitVector one(d_size, Integer(1));
223
1653552
  return ~(*this) + one;
224
}
225
226
446228
BitVector BitVector::operator*(const BitVector& y) const
227
{
228
446228
  CheckArgument(d_size == y.d_size, y);
229
892452
  Integer prod = d_value * y.d_value;
230
892452
  return BitVector(d_size, prod);
231
}
232
233
59879
BitVector BitVector::unsignedDivTotal(const BitVector& y) const
234
{
235
59879
  CheckArgument(d_size == y.d_size, y);
236
  /* d_value / 0 = -1 = 2^d_size - 1 */
237
59877
  if (y.d_value == 0)
238
  {
239
8008
    return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
240
  }
241
51869
  CheckArgument(d_value >= 0, this);
242
51869
  CheckArgument(y.d_value > 0, y);
243
51869
  return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
244
}
245
246
64876
BitVector BitVector::unsignedRemTotal(const BitVector& y) const
247
{
248
64876
  CheckArgument(d_size == y.d_size, y);
249
64874
  if (y.d_value == 0)
250
  {
251
7988
    return BitVector(d_size, d_value);
252
  }
253
56886
  CheckArgument(d_value >= 0, this);
254
56886
  CheckArgument(y.d_value > 0, y);
255
56886
  return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
256
}
257
258
/* Extend operations ----------------------------------------------------- */
259
260
58328
BitVector BitVector::zeroExtend(unsigned n) const
261
{
262
58328
  return BitVector(d_size + n, d_value);
263
}
264
265
803383
BitVector BitVector::signExtend(unsigned n) const
266
{
267
1606766
  Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
268
803383
  if (sign_bit == Integer(0))
269
  {
270
9635
    return BitVector(d_size + n, d_value);
271
  }
272
1587496
  Integer val = d_value.oneExtend(d_size, n);
273
793748
  return BitVector(d_size + n, val);
274
}
275
276
/* Shift operations ------------------------------------------------------ */
277
278
243277
BitVector BitVector::leftShift(const BitVector& y) const
279
{
280
243277
  if (y.d_value > Integer(d_size))
281
  {
282
1066
    return BitVector(d_size, Integer(0));
283
  }
284
242211
  if (y.d_value == 0)
285
  {
286
22270
    return *this;
287
  }
288
  // making sure we don't lose information casting
289
219941
  CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
290
219941
  uint32_t amount = y.d_value.toUnsignedInt();
291
439882
  Integer res = d_value.multiplyByPow2(amount);
292
219941
  return BitVector(d_size, res);
293
}
294
295
5386
BitVector BitVector::logicalRightShift(const BitVector& y) const
296
{
297
5386
  if (y.d_value > Integer(d_size))
298
  {
299
2
    return BitVector(d_size, Integer(0));
300
  }
301
  // making sure we don't lose information casting
302
5384
  CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
303
5384
  uint32_t amount = y.d_value.toUnsignedInt();
304
10768
  Integer res = d_value.divByPow2(amount);
305
5384
  return BitVector(d_size, res);
306
}
307
308
1868
BitVector BitVector::arithRightShift(const BitVector& y) const
309
{
310
3736
  Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
311
1868
  if (y.d_value > Integer(d_size))
312
  {
313
4
    if (sign_bit == Integer(0))
314
    {
315
2
      return BitVector(d_size, Integer(0));
316
    }
317
    else
318
    {
319
2
      return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) - 1);
320
    }
321
  }
322
323
1864
  if (y.d_value == 0)
324
  {
325
401
    return *this;
326
  }
327
328
  // making sure we don't lose information casting
329
1463
  CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
330
331
1463
  uint32_t amount = y.d_value.toUnsignedInt();
332
2926
  Integer rest = d_value.divByPow2(amount);
333
334
1463
  if (sign_bit == Integer(0))
335
  {
336
1161
    return BitVector(d_size, rest);
337
  }
338
604
  Integer res = rest.oneExtend(d_size - amount, amount);
339
302
  return BitVector(d_size, res);
340
}
341
342
/* -----------------------------------------------------------------------
343
 ** Static helpers.
344
 * ----------------------------------------------------------------------- */
345
346
82
BitVector BitVector::mkZero(unsigned size)
347
{
348
82
  CheckArgument(size > 0, size);
349
82
  return BitVector(size);
350
}
351
352
88
BitVector BitVector::mkOne(unsigned size)
353
{
354
88
  CheckArgument(size > 0, size);
355
88
  return BitVector(size, 1u);
356
}
357
358
784379
BitVector BitVector::mkOnes(unsigned size)
359
{
360
784379
  CheckArgument(size > 0, size);
361
784379
  return BitVector(1, Integer(1)).signExtend(size - 1);
362
}
363
364
122
BitVector BitVector::mkMinSigned(unsigned size)
365
{
366
122
  CheckArgument(size > 0, size);
367
122
  BitVector res(size);
368
122
  res.setBit(size - 1, true);
369
122
  return res;
370
}
371
372
66
BitVector BitVector::mkMaxSigned(unsigned size)
373
{
374
66
  CheckArgument(size > 0, size);
375
66
  return ~BitVector::mkMinSigned(size);
376
}
377
378
26676
}  // namespace CVC4