Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/bitvector.cpp	Lines:	171	171	100.0 %
Date:	2021-09-29	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	432636	unsigned BitVector::getSize() const { return d_size; }
23
24	116175	const Integer& BitVector::getValue() const { return d_value; }
25
26	31175	Integer BitVector::toInteger() const { return d_value; }
27
28	325620	Integer BitVector::toSignedInteger() const
29		{
30	325620	unsigned size = d_size;
31	651240	Integer sign_bit = d_value.extractBitRange(1, size - 1);
32	651240	Integer val = d_value.extractBitRange(size - 1, 0);
33	325620	Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
34	651240	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	406	std::string zeroes;
43	2040	for (unsigned int i = 0; i < d_size - str.size(); ++i)
44		{
45	1837	zeroes.append("0");
46		}
47	203	return zeroes + str;
48		}
49		else
50		{
51	83	return str;
52		}
53		}
54
55	2501426	size_t BitVector::hash() const
56		{
57	2501426	return d_value.hash() + d_size;
58		}
59
60	885	BitVector& BitVector::setBit(uint32_t i, bool value)
61		{
62	885	CheckArgument(i < d_size, i);
63	885	d_value.setBit(i, value);
64	885	return *this;
65		}
66
67	48933	bool BitVector::isBitSet(uint32_t i) const
68		{
69	48933	CheckArgument(i < d_size, i);
70	48933	return d_value.isBitSet(i);
71		}
72
73	405959	unsigned BitVector::isPow2() const
74		{
75	405959	return d_value.isPow2();
76		}
77
78		/* -----------------------------------------------------------------------
79		* Operators
80		* ----------------------------------------------------------------------- */
81
82		/* String Operations ----------------------------------------------------- */
83
84	113641	BitVector BitVector::concat(const BitVector& other) const
85		{
86	113641	return BitVector(d_size + other.d_size,
87	227282	(d_value.multiplyByPow2(other.d_size)) + other.d_value);
88		}
89
90	264387	BitVector BitVector::extract(unsigned high, unsigned low) const
91		{
92	264387	CheckArgument(high < d_size, high);
93	264385	CheckArgument(low <= high, low);
94	264383	return BitVector(high - low + 1,
95	528766	d_value.extractBitRange(high - low + 1, low));
96		}
97
98		/* (Dis)Equality --------------------------------------------------------- */
99
100	15949140	bool BitVector::operator==(const BitVector& y) const
101		{
102	15949140	if (d_size != y.d_size) return false;
103	15633923	return d_value == y.d_value;
104		}
105
106	735287	bool BitVector::operator!=(const BitVector& y) const
107		{
108	735287	if (d_size != y.d_size) return true;
109	735287	return d_value != y.d_value;
110		}
111
112		/* Unsigned Inequality --------------------------------------------------- */
113
114	389	bool BitVector::operator<(const BitVector& y) const
115		{
116	389	return d_value < y.d_value;
117		}
118
119	716	bool BitVector::operator<=(const BitVector& y) const
120		{
121	716	return d_value <= y.d_value;
122		}
123
124	1186	bool BitVector::operator>(const BitVector& y) const
125		{
126	1186	return d_value > y.d_value;
127		}
128
129	287	bool BitVector::operator>=(const BitVector& y) const
130		{
131	287	return d_value >= y.d_value;
132		}
133
134	8624	bool BitVector::unsignedLessThan(const BitVector& y) const
135		{
136	8624	CheckArgument(d_size == y.d_size, y);
137	8622	CheckArgument(d_value >= 0, this);
138	8622	CheckArgument(y.d_value >= 0, y);
139	8622	return d_value < y.d_value;
140		}
141
142	457	bool BitVector::unsignedLessThanEq(const BitVector& y) const
143		{
144	459	CheckArgument(d_size == y.d_size, this);
145	455	CheckArgument(d_value >= 0, this);
146	455	CheckArgument(y.d_value >= 0, y);
147	455	return d_value <= y.d_value;
148		}
149
150		/* Signed Inequality ----------------------------------------------------- */
151
152	8024	bool BitVector::signedLessThan(const BitVector& y) const
153		{
154	8024	CheckArgument(d_size == y.d_size, y);
155	8022	CheckArgument(d_value >= 0, this);
156	8022	CheckArgument(y.d_value >= 0, y);
157	16044	Integer a = (*this).toSignedInteger();
158	16044	Integer b = y.toSignedInteger();
159
160	16044	return a < b;
161		}
162
163	154760	bool BitVector::signedLessThanEq(const BitVector& y) const
164		{
165	154760	CheckArgument(d_size == y.d_size, y);
166	154758	CheckArgument(d_value >= 0, this);
167	154758	CheckArgument(y.d_value >= 0, y);
168	309516	Integer a = (*this).toSignedInteger();
169	309516	Integer b = y.toSignedInteger();
170
171	309516	return a <= b;
172		}
173
174		/* Bit-wise operations --------------------------------------------------- */
175
176	523	BitVector BitVector::operator^(const BitVector& y) const
177		{
178	523	CheckArgument(d_size == y.d_size, y);
179	523	return BitVector(d_size, d_value.bitwiseXor(y.d_value));
180		}
181
182	287236	BitVector BitVector::operator\|(const BitVector& y) const
183		{
184	287236	CheckArgument(d_size == y.d_size, y);
185	287236	return BitVector(d_size, d_value.bitwiseOr(y.d_value));
186		}
187
188	202095	BitVector BitVector::operator&(const BitVector& y) const
189		{
190	202095	CheckArgument(d_size == y.d_size, y);
191	202095	return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
192		}
193
194	1109079	BitVector BitVector::operator~() const
195		{
196	1109079	return BitVector(d_size, d_value.bitwiseNot());
197		}
198
199		/* Arithmetic operations ------------------------------------------------- */
200
201	1496997	BitVector BitVector::operator+(const BitVector& y) const
202		{
203	1496997	CheckArgument(d_size == y.d_size, y);
204	2993990	Integer sum = d_value + y.d_value;
205	2993990	return BitVector(d_size, sum);
206		}
207
208	295188	BitVector BitVector::operator-(const BitVector& y) const
209		{
210	295188	CheckArgument(d_size == y.d_size, y);
211		// to maintain the invariant that we are only adding BitVectors of the
212		// same size
213	590376	BitVector one(d_size, Integer(1));
214	590376	return *this + ~y + one;
215		}
216
217	702046	BitVector BitVector::operator-() const
218		{
219	1404092	BitVector one(d_size, Integer(1));
220	1404092	return ~(*this) + one;
221		}
222
223	326855	BitVector BitVector::operator*(const BitVector& y) const
224		{
225	326855	CheckArgument(d_size == y.d_size, y);
226	653706	Integer prod = d_value * y.d_value;
227	653706	return BitVector(d_size, prod);
228		}
229
230	30677	BitVector BitVector::unsignedDivTotal(const BitVector& y) const
231		{
232	30677	CheckArgument(d_size == y.d_size, y);
233		/* d_value / 0 = -1 = 2^d_size - 1 */
234	30675	if (y.d_value == 0)
235		{
236	4028	return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
237		}
238	26647	CheckArgument(d_value >= 0, this);
239	26647	CheckArgument(y.d_value > 0, y);
240	26647	return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
241		}
242
243	33146	BitVector BitVector::unsignedRemTotal(const BitVector& y) const
244		{
245	33146	CheckArgument(d_size == y.d_size, y);
246	33144	if (y.d_value == 0)
247		{
248	4253	return BitVector(d_size, d_value);
249		}
250	28891	CheckArgument(d_value >= 0, this);
251	28891	CheckArgument(y.d_value > 0, y);
252	28891	return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
253		}
254
255		/* Extend operations ----------------------------------------------------- */
256
257	49245	BitVector BitVector::zeroExtend(unsigned n) const
258		{
259	49245	return BitVector(d_size + n, d_value);
260		}
261
262	579813	BitVector BitVector::signExtend(unsigned n) const
263		{
264	1159626	Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
265	579813	if (sign_bit == Integer(0))
266		{
267	9349	return BitVector(d_size + n, d_value);
268		}
269	1140928	Integer val = d_value.oneExtend(d_size, n);
270	570464	return BitVector(d_size + n, val);
271		}
272
273		/* Shift operations ------------------------------------------------------ */
274
275	206778	BitVector BitVector::leftShift(const BitVector& y) const
276		{
277	206778	if (y.d_value > Integer(d_size))
278		{
279	960	return BitVector(d_size, Integer(0));
280		}
281	205818	if (y.d_value == 0)
282		{
283	17835	return *this;
284		}
285		// making sure we don't lose information casting
286	187983	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
287	187983	uint32_t amount = y.d_value.toUnsignedInt();
288	375966	Integer res = d_value.multiplyByPow2(amount);
289	187983	return BitVector(d_size, res);
290		}
291
292	5222	BitVector BitVector::logicalRightShift(const BitVector& y) const
293		{
294	5222	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	5220	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
300	5220	uint32_t amount = y.d_value.toUnsignedInt();
301	10440	Integer res = d_value.divByPow2(amount);
302	5220	return BitVector(d_size, res);
303		}
304
305	2117	BitVector BitVector::arithRightShift(const BitVector& y) const
306		{
307	4234	Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
308	2117	if (y.d_value > Integer(d_size))
309		{
310	26	if (sign_bit == Integer(0))
311		{
312	10	return BitVector(d_size, Integer(0));
313		}
314		else
315		{
316	16	return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) - 1);
317		}
318		}
319
320	2091	if (y.d_value == 0)
321		{
322	351	return *this;
323		}
324
325		// making sure we don't lose information casting
326	1740	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
327
328	1740	uint32_t amount = y.d_value.toUnsignedInt();
329	3480	Integer rest = d_value.divByPow2(amount);
330
331	1740	if (sign_bit == Integer(0))
332		{
333	1422	return BitVector(d_size, rest);
334		}
335	636	Integer res = rest.oneExtend(d_size - amount, amount);
336	318	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	562474	BitVector BitVector::mkOnes(unsigned size)
356		{
357	562474	CheckArgument(size > 0, size);
358	562474	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	22746	} // namespace cvc5