GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/bitvector.h Lines: 66 72 91.7 %
Date: 2021-03-22 Branches: 22 33 66.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bitvector.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andres Noetzli, Dejan Jovanovic
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
17
#include "cvc4_public.h"
18
19
#ifndef CVC4__BITVECTOR_H
20
#define CVC4__BITVECTOR_H
21
22
#include <iosfwd>
23
#include <iostream>
24
25
#include "base/exception.h"
26
#include "util/integer.h"
27
28
namespace CVC4 {
29
30
29967134
class BitVector
31
{
32
 public:
33
13982270
  BitVector(unsigned size, const Integer& val)
34
13982270
      : d_size(size), d_value(val.modByPow2(size))
35
  {
36
13982270
  }
37
38
4358264
  BitVector(unsigned size = 0) : d_size(size), d_value(0) {}
39
40
  /**
41
   * BitVector constructor using a 32-bit unsigned integer for the value.
42
   *
43
   * Note: we use an explicit bit-width here to be consistent across
44
   * platforms (long is 32-bit when compiling 64-bit binaries on
45
   * Windows but 64-bit on Linux) and to prevent ambiguous overloads.
46
   */
47
8777357
  BitVector(unsigned size, uint32_t z) : d_size(size), d_value(z)
48
  {
49
8777357
    d_value = d_value.modByPow2(size);
50
8777357
  }
51
52
  /**
53
   * BitVector constructor using a 64-bit unsigned integer for the value.
54
   *
55
   * Note: we use an explicit bit-width here to be consistent across
56
   * platforms (long is 32-bit when compiling 64-bit binaries on
57
   * Windows but 64-bit on Linux) and to prevent ambiguous overloads.
58
   */
59
77
  BitVector(unsigned size, uint64_t z) : d_size(size), d_value(z)
60
  {
61
77
    d_value = d_value.modByPow2(size);
62
77
  }
63
64
1860
  BitVector(unsigned size, const BitVector& q)
65
1860
      : d_size(size), d_value(q.d_value)
66
  {
67
1860
  }
68
69
  /**
70
   * BitVector constructor.
71
   *
72
   * The value of the bit-vector is passed in as string of base 2, 10 or 16.
73
   * The size of resulting bit-vector is
74
   * - base  2: the size of the binary string
75
   * - base 10: the min. size required to represent the decimal as a bit-vector
76
   * - base 16: the max. size required to represent the hexadecimal as a
77
   *            bit-vector (4 * size of the given value string)
78
   *
79
   * @param num The value of the bit-vector in string representation.
80
   * @param base The base of the string representation.
81
   */
82
122780
  BitVector(const std::string& num, unsigned base = 2)
83
122782
  {
84
122780
    CheckArgument(base == 2 || base == 10 || base == 16, base);
85
122780
    d_value = Integer(num, base);
86
122778
    switch (base)
87
    {
88
6
      case 10: d_size = d_value.length(); break;
89
4501
      case 16: d_size = num.size() * 4; break;
90
118271
      default: d_size = num.size();
91
    }
92
122778
  }
93
94
57209729
  ~BitVector() {}
95
96
7786157
  BitVector& operator=(const BitVector& x)
97
  {
98
7786157
    if (this == &x) return *this;
99
7785965
    d_size = x.d_size;
100
7785965
    d_value = x.d_value;
101
7785965
    return *this;
102
  }
103
104
  /* Get size (bit-width). */
105
  unsigned getSize() const;
106
  /* Get value. */
107
  const Integer& getValue() const;
108
109
  /* Return value. */
110
  Integer toInteger() const;
111
  /* Return Integer corresponding to two's complement interpretation of this. */
112
  Integer toSignedInteger() const;
113
  /* Return (binary) string representation. */
114
  std::string toString(unsigned int base = 2) const;
115
116
  /* Return hash value. */
117
  size_t hash() const;
118
119
  /**
120
   * Set bit at index 'i' to given value.
121
   * Returns a reference to this bit-vector to allow for chaining.
122
   *
123
   * value: True to set bit to 1, and false to set it to 0.
124
   *
125
   * Note: Least significant bit is at index 0.
126
   */
127
  BitVector& setBit(uint32_t i, bool value);
128
129
  /** Return true if bit at index 'i' is 1, and false otherwise. */
130
  bool isBitSet(uint32_t i) const;
131
132
  /* Return k if the value of this is equal to 2^{k-1}, and zero otherwise. */
133
  unsigned isPow2() const;
134
135
  /* -----------------------------------------------------------------------
136
   ** Operators
137
   * ----------------------------------------------------------------------- */
138
139
  /* String Operations ----------------------------------------------------- */
140
141
  /* Return the concatenation of this and bit-vector 'other'. */
142
  BitVector concat(const BitVector& other) const;
143
144
  /* Return the bit range from index 'high' to index 'low'. */
145
  BitVector extract(unsigned high, unsigned low) const;
146
147
  /* (Dis)Equality --------------------------------------------------------- */
148
149
  /* Return true if this is equal to 'y'. */
150
  bool operator==(const BitVector& y) const;
151
152
  /* Return true if this is not equal to 'y'. */
153
  bool operator!=(const BitVector& y) const;
154
155
  /* Unsigned Inequality --------------------------------------------------- */
156
157
  /* Return true if this is unsigned less than bit-vector 'y'. */
158
  bool operator<(const BitVector& y) const;
159
160
  /* Return true if this is unsigned less than or equal to bit-vector 'y'. */
161
  bool operator<=(const BitVector& y) const;
162
163
  /* Return true if this is unsigned greater than bit-vector 'y'. */
164
  bool operator>(const BitVector& y) const;
165
166
  /* Return true if this is unsigned greater than or equal to bit-vector 'y'. */
167
  bool operator>=(const BitVector& y) const;
168
169
  /* Return true if this is unsigned less than bit-vector 'y'.
170
   * This function is a synonym for operator < but performs additional
171
   * argument checks.*/
172
  bool unsignedLessThan(const BitVector& y) const;
173
174
  /* Return true if this is unsigned less than or equal to bit-vector 'y'.
175
   * This function is a synonym for operator >= but performs additional
176
   * argument checks.*/
177
  bool unsignedLessThanEq(const BitVector& y) const;
178
179
  /* Signed Inequality ----------------------------------------------------- */
180
181
  /* Return true if this is signed less than bit-vector 'y'. */
182
  bool signedLessThan(const BitVector& y) const;
183
184
  /* Return true if this is signed less than or equal to bit-vector 'y'. */
185
  bool signedLessThanEq(const BitVector& y) const;
186
187
  /* Bit-wise operations --------------------------------------------------- */
188
189
  /* Return a bit-vector representing the bit-wise xor (this ^ y). */
190
  BitVector operator^(const BitVector& y) const;
191
192
  /* Return a bit-vector representing the bit-wise or (this | y). */
193
  BitVector operator|(const BitVector& y) const;
194
195
  /* Return a bit-vector representing the bit-wise and (this & y). */
196
  BitVector operator&(const BitVector& y) const;
197
198
  /* Return a bit-vector representing the bit-wise not of this. */
199
  BitVector operator~() const;
200
201
  /* Arithmetic operations ------------------------------------------------- */
202
203
  /* Return a bit-vector representing the addition (this + y). */
204
  BitVector operator+(const BitVector& y) const;
205
206
  /* Return a bit-vector representing the subtraction (this - y). */
207
  BitVector operator-(const BitVector& y) const;
208
209
  /* Return a bit-vector representing the negation of this. */
210
  BitVector operator-() const;
211
212
  /* Return a bit-vector representing the multiplication (this * y). */
213
  BitVector operator*(const BitVector& y) const;
214
215
  /* Total division function.
216
   * Returns a bit-vector representing 2^d_size-1 (signed: -1) when the
217
   * denominator is zero, and a bit-vector representing the unsigned division
218
   * (this / y), otherwise.  */
219
  BitVector unsignedDivTotal(const BitVector& y) const;
220
221
  /* Total remainder function.
222
   * Returns this when the denominator is zero, and the unsigned remainder
223
   * (this % y), otherwise.  */
224
  BitVector unsignedRemTotal(const BitVector& y) const;
225
226
  /* Extend operations ----------------------------------------------------- */
227
228
  /* Return a bit-vector representing this extended by 'n' zero bits. */
229
  BitVector zeroExtend(unsigned n) const;
230
231
  /* Return a bit-vector representing this extended by 'n' bits of the value
232
   * of the signed bit. */
233
  BitVector signExtend(unsigned n) const;
234
235
  /* Shift operations ------------------------------------------------------ */
236
237
  /* Return a bit-vector representing a left shift of this by 'y'. */
238
  BitVector leftShift(const BitVector& y) const;
239
240
  /* Return a bit-vector representing a logical right shift of this by 'y'. */
241
  BitVector logicalRightShift(const BitVector& y) const;
242
243
  /* Return a bit-vector representing an arithmetic right shift of this
244
   * by 'y'.*/
245
  BitVector arithRightShift(const BitVector& y) const;
246
247
  /* -----------------------------------------------------------------------
248
   ** Static helpers.
249
   * ----------------------------------------------------------------------- */
250
251
  /* Create zero bit-vector of given size. */
252
  static BitVector mkZero(unsigned size);
253
254
  /* Create bit-vector representing value 1 of given size. */
255
  static BitVector mkOne(unsigned size);
256
257
  /* Create bit-vector of ones of given size. */
258
  static BitVector mkOnes(unsigned size);
259
260
  /* Create bit-vector representing the minimum signed value of given size. */
261
  static BitVector mkMinSigned(unsigned size);
262
263
  /* Create bit-vector representing the maximum signed value of given size. */
264
  static BitVector mkMaxSigned(unsigned size);
265
266
 private:
267
  /**
268
   * Class invariants:
269
   *  - no overflows: 2^d_size < d_value
270
   *  - no negative numbers: d_value >= 0
271
   */
272
273
  unsigned d_size;
274
  Integer d_value;
275
276
}; /* class BitVector */
277
278
/* -----------------------------------------------------------------------
279
 ** BitVector structs
280
 * ----------------------------------------------------------------------- */
281
282
/**
283
 * The structure representing the extraction operation for bit-vectors. The
284
 * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
285
 * by taking the bits at indices <code>high ... low</code>
286
 */
287
struct BitVectorExtract
288
{
289
  /** The high bit of the range for this extract */
290
  unsigned d_high;
291
  /** The low bit of the range for this extract */
292
  unsigned d_low;
293
294
199779
  BitVectorExtract(unsigned high, unsigned low) : d_high(high), d_low(low) {}
295
296
206626
  bool operator==(const BitVectorExtract& extract) const
297
  {
298
206626
    return d_high == extract.d_high && d_low == extract.d_low;
299
  }
300
}; /* struct BitVectorExtract */
301
302
/**
303
 * The structure representing the extraction of one Boolean bit.
304
 */
305
struct BitVectorBitOf
306
{
307
  /** The index of the bit */
308
  unsigned d_bitIndex;
309
184013
  BitVectorBitOf(unsigned i) : d_bitIndex(i) {}
310
311
200369
  bool operator==(const BitVectorBitOf& other) const
312
  {
313
200369
    return d_bitIndex == other.d_bitIndex;
314
  }
315
}; /* struct BitVectorBitOf */
316
317
struct BitVectorSize
318
{
319
  unsigned d_size;
320
536811
  BitVectorSize(unsigned size) : d_size(size) {}
321
7255822
  operator unsigned() const { return d_size; }
322
}; /* struct BitVectorSize */
323
324
struct BitVectorRepeat
325
{
326
  unsigned d_repeatAmount;
327
3286
  BitVectorRepeat(unsigned repeatAmount) : d_repeatAmount(repeatAmount) {}
328
11591
  operator unsigned() const { return d_repeatAmount; }
329
}; /* struct BitVectorRepeat */
330
331
struct BitVectorZeroExtend
332
{
333
  unsigned d_zeroExtendAmount;
334
48934
  BitVectorZeroExtend(unsigned zeroExtendAmount)
335
48934
      : d_zeroExtendAmount(zeroExtendAmount)
336
  {
337
48934
  }
338
164731
  operator unsigned() const { return d_zeroExtendAmount; }
339
}; /* struct BitVectorZeroExtend */
340
341
struct BitVectorSignExtend
342
{
343
  unsigned d_signExtendAmount;
344
28820
  BitVectorSignExtend(unsigned signExtendAmount)
345
28820
      : d_signExtendAmount(signExtendAmount)
346
  {
347
28820
  }
348
115875
  operator unsigned() const { return d_signExtendAmount; }
349
}; /* struct BitVectorSignExtend */
350
351
struct BitVectorRotateLeft
352
{
353
  unsigned d_rotateLeftAmount;
354
1597
  BitVectorRotateLeft(unsigned rotateLeftAmount)
355
1597
      : d_rotateLeftAmount(rotateLeftAmount)
356
  {
357
1597
  }
358
5823
  operator unsigned() const { return d_rotateLeftAmount; }
359
}; /* struct BitVectorRotateLeft */
360
361
struct BitVectorRotateRight
362
{
363
  unsigned d_rotateRightAmount;
364
1840
  BitVectorRotateRight(unsigned rotateRightAmount)
365
1840
      : d_rotateRightAmount(rotateRightAmount)
366
  {
367
1840
  }
368
6750
  operator unsigned() const { return d_rotateRightAmount; }
369
}; /* struct BitVectorRotateRight */
370
371
struct IntToBitVector
372
{
373
  unsigned d_size;
374
567
  IntToBitVector(unsigned size) : d_size(size) {}
375
3340
  operator unsigned() const { return d_size; }
376
}; /* struct IntToBitVector */
377
378
/* -----------------------------------------------------------------------
379
 ** Hash Function structs
380
 * ----------------------------------------------------------------------- */
381
382
/*
383
 * Hash function for the BitVector constants.
384
 */
385
struct BitVectorHashFunction
386
{
387
3625734
  inline size_t operator()(const BitVector& bv) const { return bv.hash(); }
388
}; /* struct BitVectorHashFunction */
389
390
/**
391
 * Hash function for the BitVectorExtract objects.
392
 */
393
struct BitVectorExtractHashFunction
394
{
395
226951
  size_t operator()(const BitVectorExtract& extract) const
396
  {
397
226951
    size_t hash = extract.d_low;
398
226951
    hash ^= extract.d_high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
399
226951
    return hash;
400
  }
401
}; /* struct BitVectorExtractHashFunction */
402
403
/**
404
 * Hash function for the BitVectorBitOf objects.
405
 */
406
struct BitVectorBitOfHashFunction
407
{
408
249485
  size_t operator()(const BitVectorBitOf& b) const { return b.d_bitIndex; }
409
}; /* struct BitVectorBitOfHashFunction */
410
411
template <typename T>
412
struct UnsignedHashFunction
413
{
414
668176
  inline size_t operator()(const T& x) const { return (size_t)x; }
415
}; /* struct UnsignedHashFunction */
416
417
/* -----------------------------------------------------------------------
418
 ** Output stream
419
 * ----------------------------------------------------------------------- */
420
421
inline std::ostream& operator<<(std::ostream& os, const BitVector& bv);
422
inline std::ostream& operator<<(std::ostream& os, const BitVector& bv)
423
{
424
  return os << bv.toString();
425
}
426
427
inline std::ostream& operator<<(std::ostream& os, const BitVectorExtract& bv);
428
4
inline std::ostream& operator<<(std::ostream& os, const BitVectorExtract& bv)
429
{
430
4
  return os << "[" << bv.d_high << ":" << bv.d_low << "]";
431
}
432
433
inline std::ostream& operator<<(std::ostream& os, const BitVectorBitOf& bv);
434
inline std::ostream& operator<<(std::ostream& os, const BitVectorBitOf& bv)
435
{
436
  return os << "[" << bv.d_bitIndex << "]";
437
}
438
439
inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv);
440
inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv)
441
{
442
  return os << "[" << bv.d_size << "]";
443
}
444
445
}  // namespace CVC4
446
447
#endif /* CVC4__BITVECTOR_H */