Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/bitvector.cpp	Lines:	171	171	100.0 %
Date:	2021-09-21	Branches:	178	316	56.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Liana Hadarean, Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * A fixed-size bit-vector, implemented as a wrapper around Integer.
 */

#include "util/bitvector.h"

#include "base/exception.h"

namespace cvc5 {

unsigned BitVector::getSize() const { return d_size; }

const Integer& BitVector::getValue() const { return d_value; }

Integer BitVector::toInteger() const { return d_value; }

Integer BitVector::toSignedInteger() const
{
  unsigned size = d_size;
  Integer sign_bit = d_value.extractBitRange(1, size - 1);
  Integer val = d_value.extractBitRange(size - 1, 0);
  Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
  return res;
}

std::string BitVector::toString(unsigned int base) const
{
  std::string str = d_value.toString(base);
  if (base == 2 && d_size > str.size())
  {
    std::string zeroes;
    for (unsigned int i = 0; i < d_size - str.size(); ++i)
    {
      zeroes.append("0");
    }
    return zeroes + str;
  }
  else
  {
    return str;
  }
}

size_t BitVector::hash() const
{
  return d_value.hash() + d_size;
}

BitVector& BitVector::setBit(uint32_t i, bool value)
{
  CheckArgument(i < d_size, i);
  d_value.setBit(i, value);
  return *this;
}

bool BitVector::isBitSet(uint32_t i) const
{
  CheckArgument(i < d_size, i);
  return d_value.isBitSet(i);
}

unsigned BitVector::isPow2() const
{
  return d_value.isPow2();
}

/* -----------------------------------------------------------------------
 * Operators
 * ----------------------------------------------------------------------- */

/* String Operations ----------------------------------------------------- */

BitVector BitVector::concat(const BitVector& other) const
{
  return BitVector(d_size + other.d_size,
                   (d_value.multiplyByPow2(other.d_size)) + other.d_value);
}

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));
}

/* (Dis)Equality --------------------------------------------------------- */

bool BitVector::operator==(const BitVector& y) const
{
  if (d_size != y.d_size) return false;
  return d_value == y.d_value;
}

bool BitVector::operator!=(const BitVector& y) const
{
  if (d_size != y.d_size) return true;
  return d_value != y.d_value;
}

/* Unsigned Inequality --------------------------------------------------- */

bool BitVector::operator<(const BitVector& y) const
{
  return d_value < y.d_value;
}

bool BitVector::operator<=(const BitVector& y) const
{
  return d_value <= y.d_value;
}

bool BitVector::operator>(const BitVector& y) const
{
  return d_value > y.d_value;
}

bool BitVector::operator>=(const BitVector& y) const
{
  return d_value >= y.d_value;
}

bool BitVector::unsignedLessThan(const BitVector& y) const
{
  CheckArgument(d_size == y.d_size, y);
  CheckArgument(d_value >= 0, this);
  CheckArgument(y.d_value >= 0, y);
  return d_value < y.d_value;
}

bool BitVector::unsignedLessThanEq(const BitVector& y) const
{
  CheckArgument(d_size == y.d_size, this);
  CheckArgument(d_value >= 0, this);
  CheckArgument(y.d_value >= 0, y);
  return d_value <= y.d_value;
}

/* Signed Inequality ----------------------------------------------------- */

bool BitVector::signedLessThan(const BitVector& y) const
{
  CheckArgument(d_size == y.d_size, y);
  CheckArgument(d_value >= 0, this);
  CheckArgument(y.d_value >= 0, y);
  Integer a = (*this).toSignedInteger();
  Integer b = y.toSignedInteger();

  return a < b;
}

bool BitVector::signedLessThanEq(const BitVector& y) const
{
  CheckArgument(d_size == y.d_size, y);
  CheckArgument(d_value >= 0, this);
  CheckArgument(y.d_value >= 0, y);
  Integer a = (*this).toSignedInteger();
  Integer b = y.toSignedInteger();

  return a <= b;
}

/* Bit-wise operations --------------------------------------------------- */

BitVector BitVector::operator^(const BitVector& y) const
{
  CheckArgument(d_size == y.d_size, y);
  return BitVector(d_size, d_value.bitwiseXor(y.d_value));
}

BitVector BitVector::operator|(const BitVector& y) const
{
  CheckArgument(d_size == y.d_size, y);
  return BitVector(d_size, d_value.bitwiseOr(y.d_value));
}

BitVector BitVector::operator&(const BitVector& y) const
{
  CheckArgument(d_size == y.d_size, y);
  return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
}

BitVector BitVector::operator~() const
{
  return BitVector(d_size, d_value.bitwiseNot());
}

/* Arithmetic operations ------------------------------------------------- */

BitVector BitVector::operator+(const BitVector& y) const
{
  CheckArgument(d_size == y.d_size, y);
  Integer sum = d_value + y.d_value;
  return BitVector(d_size, sum);
}

BitVector BitVector::operator-(const BitVector& y) const
{
  CheckArgument(d_size == y.d_size, y);
  // to maintain the invariant that we are only adding BitVectors of the
  // same size
  BitVector one(d_size, Integer(1));
  return *this + ~y + one;
}

BitVector BitVector::operator-() const
{
  BitVector one(d_size, Integer(1));
  return ~(*this) + one;
}

BitVector BitVector::operator*(const BitVector& y) const
{
  CheckArgument(d_size == y.d_size, y);
  Integer prod = d_value * y.d_value;
  return BitVector(d_size, prod);
}

BitVector BitVector::unsignedDivTotal(const BitVector& y) const
{
  CheckArgument(d_size == y.d_size, y);
  /* d_value / 0 = -1 = 2^d_size - 1 */
  if (y.d_value == 0)
  {
    return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
  }
  CheckArgument(d_value >= 0, this);
  CheckArgument(y.d_value > 0, y);
  return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
}

BitVector BitVector::unsignedRemTotal(const BitVector& y) const
{
  CheckArgument(d_size == y.d_size, y);
  if (y.d_value == 0)
  {
    return BitVector(d_size, d_value);
  }
  CheckArgument(d_value >= 0, this);
  CheckArgument(y.d_value > 0, y);
  return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
}

/* Extend operations ----------------------------------------------------- */

BitVector BitVector::zeroExtend(unsigned n) const
{
  return BitVector(d_size + n, d_value);
}

BitVector BitVector::signExtend(unsigned n) const
{
  Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
  if (sign_bit == Integer(0))
  {
    return BitVector(d_size + n, d_value);
  }
  Integer val = d_value.oneExtend(d_size, n);
  return BitVector(d_size + n, val);
}

/* Shift operations ------------------------------------------------------ */

BitVector BitVector::leftShift(const BitVector& y) const
{
  if (y.d_value > Integer(d_size))
  {
    return BitVector(d_size, Integer(0));
  }
  if (y.d_value == 0)
  {
    return *this;
  }
  // making sure we don't lose information casting
  CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
  uint32_t amount = y.d_value.toUnsignedInt();
  Integer res = d_value.multiplyByPow2(amount);
  return BitVector(d_size, res);
}

BitVector BitVector::logicalRightShift(const BitVector& y) const
{
  if (y.d_value > Integer(d_size))
  {
    return BitVector(d_size, Integer(0));
  }
  // making sure we don't lose information casting
  CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
  uint32_t amount = y.d_value.toUnsignedInt();
  Integer res = d_value.divByPow2(amount);
  return BitVector(d_size, res);
}

BitVector BitVector::arithRightShift(const BitVector& y) const
{
  Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
  if (y.d_value > Integer(d_size))
  {
    if (sign_bit == Integer(0))
    {
      return BitVector(d_size, Integer(0));
    }
    else
    {
      return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) - 1);
    }
  }

  if (y.d_value == 0)
  {
    return *this;
  }

  // making sure we don't lose information casting
  CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);

  uint32_t amount = y.d_value.toUnsignedInt();
  Integer rest = d_value.divByPow2(amount);

  if (sign_bit == Integer(0))
  {
    return BitVector(d_size, rest);
  }
  Integer res = rest.oneExtend(d_size - amount, amount);
  return BitVector(d_size, res);
}

/* -----------------------------------------------------------------------
 * Static helpers.
 * ----------------------------------------------------------------------- */

BitVector BitVector::mkZero(unsigned size)
{
  CheckArgument(size > 0, size);
  return BitVector(size);
}

BitVector BitVector::mkOne(unsigned size)
{
  CheckArgument(size > 0, size);
  return BitVector(size, 1u);
}

BitVector BitVector::mkOnes(unsigned size)
{
  CheckArgument(size > 0, size);
  return BitVector(1, Integer(1)).signExtend(size - 1);
}

BitVector BitVector::mkMinSigned(unsigned size)
{
  CheckArgument(size > 0, size);
  BitVector res(size);
  res.setBit(size - 1, true);
  return res;
}

BitVector BitVector::mkMaxSigned(unsigned size)
{
  CheckArgument(size > 0, size);
  return ~BitVector::mkMinSigned(size);
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Liana Hadarean, Morgan Deters
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* A fixed-size bit-vector, implemented as a wrapper around Integer.
14		*/
15
16		#include "util/bitvector.h"
17
18		#include "base/exception.h"
19
20		namespace cvc5 {
21
22	487226	unsigned BitVector::getSize() const { return d_size; }
23
24	166368	const Integer& BitVector::getValue() const { return d_value; }
25
26	32035	Integer BitVector::toInteger() const { return d_value; }
27
28	370624	Integer BitVector::toSignedInteger() const
29		{
30	370624	unsigned size = d_size;
31	741248	Integer sign_bit = d_value.extractBitRange(1, size - 1);
32	741248	Integer val = d_value.extractBitRange(size - 1, 0);
33	370624	Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
34	741248	return res;
35		}
36
37	286	std::string BitVector::toString(unsigned int base) const
38		{
39	572	std::string str = d_value.toString(base);
40	286	if (base == 2 && d_size > str.size())
41		{
42	382	std::string zeroes;
43	2008	for (unsigned int i = 0; i < d_size - str.size(); ++i)
44		{
45	1817	zeroes.append("0");
46		}
47	191	return zeroes + str;
48		}
49		else
50		{
51	95	return str;
52		}
53		}
54
55	3036138	size_t BitVector::hash() const
56		{
57	3036138	return d_value.hash() + d_size;
58		}
59
60	2040	BitVector& BitVector::setBit(uint32_t i, bool value)
61		{
62	2040	CheckArgument(i < d_size, i);
63	2040	d_value.setBit(i, value);
64	2040	return *this;
65		}
66
67	57507	bool BitVector::isBitSet(uint32_t i) const
68		{
69	57507	CheckArgument(i < d_size, i);
70	57507	return d_value.isBitSet(i);
71		}
72
73	407289	unsigned BitVector::isPow2() const
74		{
75	407289	return d_value.isPow2();
76		}
77
78		/* -----------------------------------------------------------------------
79		* Operators
80		* ----------------------------------------------------------------------- */
81
82		/* String Operations ----------------------------------------------------- */
83
84	121053	BitVector BitVector::concat(const BitVector& other) const
85		{
86	121053	return BitVector(d_size + other.d_size,
87	242106	(d_value.multiplyByPow2(other.d_size)) + other.d_value);
88		}
89
90	324428	BitVector BitVector::extract(unsigned high, unsigned low) const
91		{
92	324428	CheckArgument(high < d_size, high);
93	324426	CheckArgument(low <= high, low);
94	324424	return BitVector(high - low + 1,
95	648848	d_value.extractBitRange(high - low + 1, low));
96		}
97
98		/* (Dis)Equality --------------------------------------------------------- */
99
100	16825691	bool BitVector::operator==(const BitVector& y) const
101		{
102	16825691	if (d_size != y.d_size) return false;
103	16437806	return d_value == y.d_value;
104		}
105
106	857213	bool BitVector::operator!=(const BitVector& y) const
107		{
108	857213	if (d_size != y.d_size) return true;
109	857213	return d_value != y.d_value;
110		}
111
112		/* Unsigned Inequality --------------------------------------------------- */
113
114	1049	bool BitVector::operator<(const BitVector& y) const
115		{
116	1049	return d_value < y.d_value;
117		}
118
119	1838	bool BitVector::operator<=(const BitVector& y) const
120		{
121	1838	return d_value <= y.d_value;
122		}
123
124	2680	bool BitVector::operator>(const BitVector& y) const
125		{
126	2680	return d_value > y.d_value;
127		}
128
129	763	bool BitVector::operator>=(const BitVector& y) const
130		{
131	763	return d_value >= y.d_value;
132		}
133
134	8993	bool BitVector::unsignedLessThan(const BitVector& y) const
135		{
136	8993	CheckArgument(d_size == y.d_size, y);
137	8991	CheckArgument(d_value >= 0, this);
138	8991	CheckArgument(y.d_value >= 0, y);
139	8991	return d_value < y.d_value;
140		}
141
142	467	bool BitVector::unsignedLessThanEq(const BitVector& y) const
143		{
144	469	CheckArgument(d_size == y.d_size, this);
145	465	CheckArgument(d_value >= 0, this);
146	465	CheckArgument(y.d_value >= 0, y);
147	465	return d_value <= y.d_value;
148		}
149
150		/* Signed Inequality ----------------------------------------------------- */
151
152	9027	bool BitVector::signedLessThan(const BitVector& y) const
153		{
154	9027	CheckArgument(d_size == y.d_size, y);
155	9025	CheckArgument(d_value >= 0, this);
156	9025	CheckArgument(y.d_value >= 0, y);
157	18050	Integer a = (*this).toSignedInteger();
158	18050	Integer b = y.toSignedInteger();
159
160	18050	return a < b;
161		}
162
163	176259	bool BitVector::signedLessThanEq(const BitVector& y) const
164		{
165	176259	CheckArgument(d_size == y.d_size, y);
166	176257	CheckArgument(d_value >= 0, this);
167	176257	CheckArgument(y.d_value >= 0, y);
168	352514	Integer a = (*this).toSignedInteger();
169	352514	Integer b = y.toSignedInteger();
170
171	352514	return a <= b;
172		}
173
174		/* Bit-wise operations --------------------------------------------------- */
175
176	601	BitVector BitVector::operator^(const BitVector& y) const
177		{
178	601	CheckArgument(d_size == y.d_size, y);
179	601	return BitVector(d_size, d_value.bitwiseXor(y.d_value));
180		}
181
182	297300	BitVector BitVector::operator\|(const BitVector& y) const
183		{
184	297300	CheckArgument(d_size == y.d_size, y);
185	297300	return BitVector(d_size, d_value.bitwiseOr(y.d_value));
186		}
187
188	210563	BitVector BitVector::operator&(const BitVector& y) const
189		{
190	210563	CheckArgument(d_size == y.d_size, y);
191	210563	return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
192		}
193
194	1179433	BitVector BitVector::operator~() const
195		{
196	1179433	return BitVector(d_size, d_value.bitwiseNot());
197		}
198
199		/* Arithmetic operations ------------------------------------------------- */
200
201	1627109	BitVector BitVector::operator+(const BitVector& y) const
202		{
203	1627109	CheckArgument(d_size == y.d_size, y);
204	3254214	Integer sum = d_value + y.d_value;
205	3254214	return BitVector(d_size, sum);
206		}
207
208	338901	BitVector BitVector::operator-(const BitVector& y) const
209		{
210	338901	CheckArgument(d_size == y.d_size, y);
211		// to maintain the invariant that we are only adding BitVectors of the
212		// same size
213	677802	BitVector one(d_size, Integer(1));
214	677802	return *this + ~y + one;
215		}
216
217	724077	BitVector BitVector::operator-() const
218		{
219	1448154	BitVector one(d_size, Integer(1));
220	1448154	return ~(*this) + one;
221		}
222
223	329038	BitVector BitVector::operator*(const BitVector& y) const
224		{
225	329038	CheckArgument(d_size == y.d_size, y);
226	658072	Integer prod = d_value * y.d_value;
227	658072	return BitVector(d_size, prod);
228		}
229
230	30721	BitVector BitVector::unsignedDivTotal(const BitVector& y) const
231		{
232	30721	CheckArgument(d_size == y.d_size, y);
233		/* d_value / 0 = -1 = 2^d_size - 1 */
234	30719	if (y.d_value == 0)
235		{
236	4028	return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
237		}
238	26691	CheckArgument(d_value >= 0, this);
239	26691	CheckArgument(y.d_value > 0, y);
240	26691	return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
241		}
242
243	33169	BitVector BitVector::unsignedRemTotal(const BitVector& y) const
244		{
245	33169	CheckArgument(d_size == y.d_size, y);
246	33167	if (y.d_value == 0)
247		{
248	4270	return BitVector(d_size, d_value);
249		}
250	28897	CheckArgument(d_value >= 0, this);
251	28897	CheckArgument(y.d_value > 0, y);
252	28897	return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
253		}
254
255		/* Extend operations ----------------------------------------------------- */
256
257	55919	BitVector BitVector::zeroExtend(unsigned n) const
258		{
259	55919	return BitVector(d_size + n, d_value);
260		}
261
262	647159	BitVector BitVector::signExtend(unsigned n) const
263		{
264	1294318	Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
265	647159	if (sign_bit == Integer(0))
266		{
267	10140	return BitVector(d_size + n, d_value);
268		}
269	1274038	Integer val = d_value.oneExtend(d_size, n);
270	637019	return BitVector(d_size + n, val);
271		}
272
273		/* Shift operations ------------------------------------------------------ */
274
275	236117	BitVector BitVector::leftShift(const BitVector& y) const
276		{
277	236117	if (y.d_value > Integer(d_size))
278		{
279	994	return BitVector(d_size, Integer(0));
280		}
281	235123	if (y.d_value == 0)
282		{
283	20732	return *this;
284		}
285		// making sure we don't lose information casting
286	214391	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
287	214391	uint32_t amount = y.d_value.toUnsignedInt();
288	428782	Integer res = d_value.multiplyByPow2(amount);
289	214391	return BitVector(d_size, res);
290		}
291
292	6159	BitVector BitVector::logicalRightShift(const BitVector& y) const
293		{
294	6159	if (y.d_value > Integer(d_size))
295		{
296	2	return BitVector(d_size, Integer(0));
297		}
298		// making sure we don't lose information casting
299	6157	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
300	6157	uint32_t amount = y.d_value.toUnsignedInt();
301	12314	Integer res = d_value.divByPow2(amount);
302	6157	return BitVector(d_size, res);
303		}
304
305	2168	BitVector BitVector::arithRightShift(const BitVector& y) const
306		{
307	4336	Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
308	2168	if (y.d_value > Integer(d_size))
309		{
310	29	if (sign_bit == Integer(0))
311		{
312	10	return BitVector(d_size, Integer(0));
313		}
314		else
315		{
316	19	return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) - 1);
317		}
318		}
319
320	2139	if (y.d_value == 0)
321		{
322	354	return *this;
323		}
324
325		// making sure we don't lose information casting
326	1785	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
327
328	1785	uint32_t amount = y.d_value.toUnsignedInt();
329	3570	Integer rest = d_value.divByPow2(amount);
330
331	1785	if (sign_bit == Integer(0))
332		{
333	1453	return BitVector(d_size, rest);
334		}
335	664	Integer res = rest.oneExtend(d_size - amount, amount);
336	332	return BitVector(d_size, res);
337		}
338
339		/* -----------------------------------------------------------------------
340		* Static helpers.
341		* ----------------------------------------------------------------------- */
342
343	94	BitVector BitVector::mkZero(unsigned size)
344		{
345	94	CheckArgument(size > 0, size);
346	94	return BitVector(size);
347		}
348
349	720	BitVector BitVector::mkOne(unsigned size)
350		{
351	720	CheckArgument(size > 0, size);
352	720	return BitVector(size, 1u);
353		}
354
355	628397	BitVector BitVector::mkOnes(unsigned size)
356		{
357	628397	CheckArgument(size > 0, size);
358	628397	return BitVector(1, Integer(1)).signExtend(size - 1);
359		}
360
361	132	BitVector BitVector::mkMinSigned(unsigned size)
362		{
363	132	CheckArgument(size > 0, size);
364	132	BitVector res(size);
365	132	res.setBit(size - 1, true);
366	132	return res;
367		}
368
369	74	BitVector BitVector::mkMaxSigned(unsigned size)
370		{
371	74	CheckArgument(size > 0, size);
372	74	return ~BitVector::mkMinSigned(size);
373		}
374
375	29589	} // namespace cvc5