Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/bitvector.cpp	Lines:	171	171	100.0 %
Date:	2021-05-22	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	462464	unsigned BitVector::getSize() const { return d_size; }
23
24	122086	const Integer& BitVector::getValue() const { return d_value; }
25
26	29105	Integer BitVector::toInteger() const { return d_value; }
27
28	331058	Integer BitVector::toSignedInteger() const
29		{
30	331058	unsigned size = d_size;
31	662116	Integer sign_bit = d_value.extractBitRange(1, size - 1);
32	662116	Integer val = d_value.extractBitRange(size - 1, 0);
33	331058	Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
34	662116	return res;
35		}
36
37	405860	std::string BitVector::toString(unsigned int base) const
38		{
39	811720	std::string str = d_value.toString(base);
40	405860	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	405671	return str;
52		}
53		}
54
55	3199668	size_t BitVector::hash() const
56		{
57	3199668	return d_value.hash() + d_size;
58		}
59
60	2071	BitVector& BitVector::setBit(uint32_t i, bool value)
61		{
62	2071	CheckArgument(i < d_size, i);
63	2071	d_value.setBit(i, value);
64	2071	return *this;
65		}
66
67	52581	bool BitVector::isBitSet(uint32_t i) const
68		{
69	52581	CheckArgument(i < d_size, i);
70	52581	return d_value.isBitSet(i);
71		}
72
73	396459	unsigned BitVector::isPow2() const
74		{
75	396459	return d_value.isPow2();
76		}
77
78		/* -----------------------------------------------------------------------
79		* Operators
80		* ----------------------------------------------------------------------- */
81
82		/* String Operations ----------------------------------------------------- */
83
84	124715	BitVector BitVector::concat(const BitVector& other) const
85		{
86	124715	return BitVector(d_size + other.d_size,
87	249430	(d_value.multiplyByPow2(other.d_size)) + other.d_value);
88		}
89
90	316742	BitVector BitVector::extract(unsigned high, unsigned low) const
91		{
92	316742	CheckArgument(high < d_size, high);
93	316740	CheckArgument(low <= high, low);
94	316738	return BitVector(high - low + 1,
95	633476	d_value.extractBitRange(high - low + 1, low));
96		}
97
98		/* (Dis)Equality --------------------------------------------------------- */
99
100	16776920	bool BitVector::operator==(const BitVector& y) const
101		{
102	16776920	if (d_size != y.d_size) return false;
103	16195795	return d_value == y.d_value;
104		}
105
106	883251	bool BitVector::operator!=(const BitVector& y) const
107		{
108	883251	if (d_size != y.d_size) return true;
109	883251	return d_value != y.d_value;
110		}
111
112		/* Unsigned Inequality --------------------------------------------------- */
113
114	9784568	bool BitVector::operator<(const BitVector& y) const
115		{
116	9784568	return d_value < y.d_value;
117		}
118
119	1160684	bool BitVector::operator<=(const BitVector& y) const
120		{
121	1160684	return d_value <= y.d_value;
122		}
123
124	3393	bool BitVector::operator>(const BitVector& y) const
125		{
126	3393	return d_value > y.d_value;
127		}
128
129	816	bool BitVector::operator>=(const BitVector& y) const
130		{
131	816	return d_value >= y.d_value;
132		}
133
134	7610	bool BitVector::unsignedLessThan(const BitVector& y) const
135		{
136	7610	CheckArgument(d_size == y.d_size, y);
137	7608	CheckArgument(d_value >= 0, this);
138	7608	CheckArgument(y.d_value >= 0, y);
139	7608	return d_value < y.d_value;
140		}
141
142	432	bool BitVector::unsignedLessThanEq(const BitVector& y) const
143		{
144	434	CheckArgument(d_size == y.d_size, this);
145	430	CheckArgument(d_value >= 0, this);
146	430	CheckArgument(y.d_value >= 0, y);
147	430	return d_value <= y.d_value;
148		}
149
150		/* Signed Inequality ----------------------------------------------------- */
151
152	8129	bool BitVector::signedLessThan(const BitVector& y) const
153		{
154	8129	CheckArgument(d_size == y.d_size, y);
155	8127	CheckArgument(d_value >= 0, this);
156	8127	CheckArgument(y.d_value >= 0, y);
157	16254	Integer a = (*this).toSignedInteger();
158	16254	Integer b = y.toSignedInteger();
159
160	16254	return a < b;
161		}
162
163	157397	bool BitVector::signedLessThanEq(const BitVector& y) const
164		{
165	157397	CheckArgument(d_size == y.d_size, y);
166	157395	CheckArgument(d_value >= 0, this);
167	157395	CheckArgument(y.d_value >= 0, y);
168	314790	Integer a = (*this).toSignedInteger();
169	314790	Integer b = y.toSignedInteger();
170
171	314790	return a <= b;
172		}
173
174		/* Bit-wise operations --------------------------------------------------- */
175
176	588	BitVector BitVector::operator^(const BitVector& y) const
177		{
178	588	CheckArgument(d_size == y.d_size, y);
179	588	return BitVector(d_size, d_value.bitwiseXor(y.d_value));
180		}
181
182	322114	BitVector BitVector::operator\|(const BitVector& y) const
183		{
184	322114	CheckArgument(d_size == y.d_size, y);
185	322114	return BitVector(d_size, d_value.bitwiseOr(y.d_value));
186		}
187
188	207975	BitVector BitVector::operator&(const BitVector& y) const
189		{
190	207975	CheckArgument(d_size == y.d_size, y);
191	207975	return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
192		}
193
194	1179766	BitVector BitVector::operator~() const
195		{
196	1179766	return BitVector(d_size, d_value.bitwiseNot());
197		}
198
199		/* Arithmetic operations ------------------------------------------------- */
200
201	8230834	BitVector BitVector::operator+(const BitVector& y) const
202		{
203	8230834	CheckArgument(d_size == y.d_size, y);
204	16461664	Integer sum = d_value + y.d_value;
205	16461664	return BitVector(d_size, sum);
206		}
207
208	307372	BitVector BitVector::operator-(const BitVector& y) const
209		{
210	307372	CheckArgument(d_size == y.d_size, y);
211		// to maintain the invariant that we are only adding BitVectors of the
212		// same size
213	614744	BitVector one(d_size, Integer(1));
214	614744	return *this + ~y + one;
215		}
216
217	749459	BitVector BitVector::operator-() const
218		{
219	1498918	BitVector one(d_size, Integer(1));
220	1498918	return ~(*this) + one;
221		}
222
223	328290	BitVector BitVector::operator*(const BitVector& y) const
224		{
225	328290	CheckArgument(d_size == y.d_size, y);
226	656576	Integer prod = d_value * y.d_value;
227	656576	return BitVector(d_size, prod);
228		}
229
230	29968	BitVector BitVector::unsignedDivTotal(const BitVector& y) const
231		{
232	29968	CheckArgument(d_size == y.d_size, y);
233		/* d_value / 0 = -1 = 2^d_size - 1 */
234	29966	if (y.d_value == 0)
235		{
236	3997	return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
237		}
238	25969	CheckArgument(d_value >= 0, this);
239	25969	CheckArgument(y.d_value > 0, y);
240	25969	return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
241		}
242
243	32494	BitVector BitVector::unsignedRemTotal(const BitVector& y) const
244		{
245	32494	CheckArgument(d_size == y.d_size, y);
246	32492	if (y.d_value == 0)
247		{
248	3981	return BitVector(d_size, d_value);
249		}
250	28511	CheckArgument(d_value >= 0, this);
251	28511	CheckArgument(y.d_value > 0, y);
252	28511	return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
253		}
254
255		/* Extend operations ----------------------------------------------------- */
256
257	50069	BitVector BitVector::zeroExtend(unsigned n) const
258		{
259	50069	return BitVector(d_size + n, d_value);
260		}
261
262	632705	BitVector BitVector::signExtend(unsigned n) const
263		{
264	1265410	Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
265	632705	if (sign_bit == Integer(0))
266		{
267	9157	return BitVector(d_size + n, d_value);
268		}
269	1247096	Integer val = d_value.oneExtend(d_size, n);
270	623548	return BitVector(d_size + n, val);
271		}
272
273		/* Shift operations ------------------------------------------------------ */
274
275	210368	BitVector BitVector::leftShift(const BitVector& y) const
276		{
277	210368	if (y.d_value > Integer(d_size))
278		{
279	913	return BitVector(d_size, Integer(0));
280		}
281	209455	if (y.d_value == 0)
282		{
283	19068	return *this;
284		}
285		// making sure we don't lose information casting
286	190387	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
287	190387	uint32_t amount = y.d_value.toUnsignedInt();
288	380774	Integer res = d_value.multiplyByPow2(amount);
289	190387	return BitVector(d_size, res);
290		}
291
292	5103	BitVector BitVector::logicalRightShift(const BitVector& y) const
293		{
294	5103	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	5101	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
300	5101	uint32_t amount = y.d_value.toUnsignedInt();
301	10202	Integer res = d_value.divByPow2(amount);
302	5101	return BitVector(d_size, res);
303		}
304
305	1647	BitVector BitVector::arithRightShift(const BitVector& y) const
306		{
307	3294	Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
308	1647	if (y.d_value > Integer(d_size))
309		{
310	5	if (sign_bit == Integer(0))
311		{
312	3	return BitVector(d_size, Integer(0));
313		}
314		else
315		{
316	2	return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) - 1);
317		}
318		}
319
320	1642	if (y.d_value == 0)
321		{
322	332	return *this;
323		}
324
325		// making sure we don't lose information casting
326	1310	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
327
328	1310	uint32_t amount = y.d_value.toUnsignedInt();
329	2620	Integer rest = d_value.divByPow2(amount);
330
331	1310	if (sign_bit == Integer(0))
332		{
333	1109	return BitVector(d_size, rest);
334		}
335	402	Integer res = rest.oneExtend(d_size - amount, amount);
336	201	return BitVector(d_size, res);
337		}
338
339		/* -----------------------------------------------------------------------
340		* Static helpers.
341		* ----------------------------------------------------------------------- */
342
343	86	BitVector BitVector::mkZero(unsigned size)
344		{
345	86	CheckArgument(size > 0, size);
346	86	return BitVector(size);
347		}
348
349	314	BitVector BitVector::mkOne(unsigned size)
350		{
351	314	CheckArgument(size > 0, size);
352	314	return BitVector(size, 1u);
353		}
354
355	615358	BitVector BitVector::mkOnes(unsigned size)
356		{
357	615358	CheckArgument(size > 0, size);
358	615358	return BitVector(1, Integer(1)).signExtend(size - 1);
359		}
360
361	126	BitVector BitVector::mkMinSigned(unsigned size)
362		{
363	126	CheckArgument(size > 0, size);
364	126	BitVector res(size);
365	126	res.setBit(size - 1, true);
366	126	return res;
367		}
368
369	68	BitVector BitVector::mkMaxSigned(unsigned size)
370		{
371	68	CheckArgument(size > 0, size);
372	68	return ~BitVector::mkMinSigned(size);
373		}
374
375	28194	} // namespace cvc5