Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/bitvector.cpp	Lines:	171	171	100.0 %
Date:	2021-08-20	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	482891	unsigned BitVector::getSize() const { return d_size; }
23
24	165179	const Integer& BitVector::getValue() const { return d_value; }
25
26	29520	Integer BitVector::toInteger() const { return d_value; }
27
28	346454	Integer BitVector::toSignedInteger() const
29		{
30	346454	unsigned size = d_size;
31	692908	Integer sign_bit = d_value.extractBitRange(1, size - 1);
32	692908	Integer val = d_value.extractBitRange(size - 1, 0);
33	346454	Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
34	692908	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	378	std::string zeroes;
43	1992	for (unsigned int i = 0; i < d_size - str.size(); ++i)
44		{
45	1803	zeroes.append("0");
46		}
47	189	return zeroes + str;
48		}
49		else
50		{
51	97	return str;
52		}
53		}
54
55	2986558	size_t BitVector::hash() const
56		{
57	2986558	return d_value.hash() + d_size;
58		}
59
60	1969	BitVector& BitVector::setBit(uint32_t i, bool value)
61		{
62	1969	CheckArgument(i < d_size, i);
63	1969	d_value.setBit(i, value);
64	1969	return *this;
65		}
66
67	59547	bool BitVector::isBitSet(uint32_t i) const
68		{
69	59547	CheckArgument(i < d_size, i);
70	59547	return d_value.isBitSet(i);
71		}
72
73	406759	unsigned BitVector::isPow2() const
74		{
75	406759	return d_value.isPow2();
76		}
77
78		/* -----------------------------------------------------------------------
79		* Operators
80		* ----------------------------------------------------------------------- */
81
82		/* String Operations ----------------------------------------------------- */
83
84	124618	BitVector BitVector::concat(const BitVector& other) const
85		{
86	124618	return BitVector(d_size + other.d_size,
87	249236	(d_value.multiplyByPow2(other.d_size)) + other.d_value);
88		}
89
90	362249	BitVector BitVector::extract(unsigned high, unsigned low) const
91		{
92	362249	CheckArgument(high < d_size, high);
93	362247	CheckArgument(low <= high, low);
94	362245	return BitVector(high - low + 1,
95	724490	d_value.extractBitRange(high - low + 1, low));
96		}
97
98		/* (Dis)Equality --------------------------------------------------------- */
99
100	16027861	bool BitVector::operator==(const BitVector& y) const
101		{
102	16027861	if (d_size != y.d_size) return false;
103	15457201	return d_value == y.d_value;
104		}
105
106	843927	bool BitVector::operator!=(const BitVector& y) const
107		{
108	843927	if (d_size != y.d_size) return true;
109	843927	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	8084	bool BitVector::unsignedLessThan(const BitVector& y) const
135		{
136	8084	CheckArgument(d_size == y.d_size, y);
137	8082	CheckArgument(d_value >= 0, this);
138	8082	CheckArgument(y.d_value >= 0, y);
139	8082	return d_value < y.d_value;
140		}
141
142	461	bool BitVector::unsignedLessThanEq(const BitVector& y) const
143		{
144	463	CheckArgument(d_size == y.d_size, this);
145	459	CheckArgument(d_value >= 0, this);
146	459	CheckArgument(y.d_value >= 0, y);
147	459	return d_value <= y.d_value;
148		}
149
150		/* Signed Inequality ----------------------------------------------------- */
151
152	8632	bool BitVector::signedLessThan(const BitVector& y) const
153		{
154	8632	CheckArgument(d_size == y.d_size, y);
155	8630	CheckArgument(d_value >= 0, this);
156	8630	CheckArgument(y.d_value >= 0, y);
157	17260	Integer a = (*this).toSignedInteger();
158	17260	Integer b = y.toSignedInteger();
159
160	17260	return a < b;
161		}
162
163	164586	bool BitVector::signedLessThanEq(const BitVector& y) const
164		{
165	164586	CheckArgument(d_size == y.d_size, y);
166	164584	CheckArgument(d_value >= 0, this);
167	164584	CheckArgument(y.d_value >= 0, y);
168	329168	Integer a = (*this).toSignedInteger();
169	329168	Integer b = y.toSignedInteger();
170
171	329168	return a <= b;
172		}
173
174		/* Bit-wise operations --------------------------------------------------- */
175
176	583	BitVector BitVector::operator^(const BitVector& y) const
177		{
178	583	CheckArgument(d_size == y.d_size, y);
179	583	return BitVector(d_size, d_value.bitwiseXor(y.d_value));
180		}
181
182	328503	BitVector BitVector::operator\|(const BitVector& y) const
183		{
184	328503	CheckArgument(d_size == y.d_size, y);
185	328503	return BitVector(d_size, d_value.bitwiseOr(y.d_value));
186		}
187
188	209879	BitVector BitVector::operator&(const BitVector& y) const
189		{
190	209879	CheckArgument(d_size == y.d_size, y);
191	209879	return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
192		}
193
194	1157781	BitVector BitVector::operator~() const
195		{
196	1157781	return BitVector(d_size, d_value.bitwiseNot());
197		}
198
199		/* Arithmetic operations ------------------------------------------------- */
200
201	1577354	BitVector BitVector::operator+(const BitVector& y) const
202		{
203	1577354	CheckArgument(d_size == y.d_size, y);
204	3154704	Integer sum = d_value + y.d_value;
205	3154704	return BitVector(d_size, sum);
206		}
207
208	316924	BitVector BitVector::operator-(const BitVector& y) const
209		{
210	316924	CheckArgument(d_size == y.d_size, y);
211		// to maintain the invariant that we are only adding BitVectors of the
212		// same size
213	633848	BitVector one(d_size, Integer(1));
214	633848	return *this + ~y + one;
215		}
216
217	717462	BitVector BitVector::operator-() const
218		{
219	1434924	BitVector one(d_size, Integer(1));
220	1434924	return ~(*this) + one;
221		}
222
223	328257	BitVector BitVector::operator*(const BitVector& y) const
224		{
225	328257	CheckArgument(d_size == y.d_size, y);
226	656510	Integer prod = d_value * y.d_value;
227	656510	return BitVector(d_size, prod);
228		}
229
230	30631	BitVector BitVector::unsignedDivTotal(const BitVector& y) const
231		{
232	30631	CheckArgument(d_size == y.d_size, y);
233		/* d_value / 0 = -1 = 2^d_size - 1 */
234	30629	if (y.d_value == 0)
235		{
236	4030	return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
237		}
238	26599	CheckArgument(d_value >= 0, this);
239	26599	CheckArgument(y.d_value > 0, y);
240	26599	return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
241		}
242
243	33107	BitVector BitVector::unsignedRemTotal(const BitVector& y) const
244		{
245	33107	CheckArgument(d_size == y.d_size, y);
246	33105	if (y.d_value == 0)
247		{
248	4265	return BitVector(d_size, d_value);
249		}
250	28840	CheckArgument(d_value >= 0, this);
251	28840	CheckArgument(y.d_value > 0, y);
252	28840	return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
253		}
254
255		/* Extend operations ----------------------------------------------------- */
256
257	52510	BitVector BitVector::zeroExtend(unsigned n) const
258		{
259	52510	return BitVector(d_size + n, d_value);
260		}
261
262	633685	BitVector BitVector::signExtend(unsigned n) const
263		{
264	1267370	Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
265	633685	if (sign_bit == Integer(0))
266		{
267	9853	return BitVector(d_size + n, d_value);
268		}
269	1247664	Integer val = d_value.oneExtend(d_size, n);
270	623832	return BitVector(d_size + n, val);
271		}
272
273		/* Shift operations ------------------------------------------------------ */
274
275	220026	BitVector BitVector::leftShift(const BitVector& y) const
276		{
277	220026	if (y.d_value > Integer(d_size))
278		{
279	957	return BitVector(d_size, Integer(0));
280		}
281	219069	if (y.d_value == 0)
282		{
283	19403	return *this;
284		}
285		// making sure we don't lose information casting
286	199666	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
287	199666	uint32_t amount = y.d_value.toUnsignedInt();
288	399332	Integer res = d_value.multiplyByPow2(amount);
289	199666	return BitVector(d_size, res);
290		}
291
292	5690	BitVector BitVector::logicalRightShift(const BitVector& y) const
293		{
294	5690	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	5688	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
300	5688	uint32_t amount = y.d_value.toUnsignedInt();
301	11376	Integer res = d_value.divByPow2(amount);
302	5688	return BitVector(d_size, res);
303		}
304
305	2131	BitVector BitVector::arithRightShift(const BitVector& y) const
306		{
307	4262	Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
308	2131	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	2102	if (y.d_value == 0)
321		{
322	354	return *this;
323		}
324
325		// making sure we don't lose information casting
326	1748	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
327
328	1748	uint32_t amount = y.d_value.toUnsignedInt();
329	3496	Integer rest = d_value.divByPow2(amount);
330
331	1748	if (sign_bit == Integer(0))
332		{
333	1416	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	615434	BitVector BitVector::mkOnes(unsigned size)
356		{
357	615434	CheckArgument(size > 0, size);
358	615434	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	29358	} // namespace cvc5