Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/bitvector.cpp	Lines:	171	171	100.0 %
Date:	2021-11-07	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	584479	unsigned BitVector::getSize() const { return d_size; }
23
24	178924	const Integer& BitVector::getValue() const { return d_value; }
25
26	40734	Integer BitVector::toInteger() const { return d_value; }
27
28	445670	Integer BitVector::toSignedInteger() const
29		{
30	445670	unsigned size = d_size;
31	891340	Integer sign_bit = d_value.extractBitRange(1, size - 1);
32	891340	Integer val = d_value.extractBitRange(size - 1, 0);
33	445670	Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
34	891340	return res;
35		}
36
37	29370	std::string BitVector::toString(unsigned int base) const
38		{
39	58740	std::string str = d_value.toString(base);
40	29370	if (base == 2 && d_size > str.size())
41		{
42	32418	std::string zeroes;
43	378273	for (unsigned int i = 0; i < d_size - str.size(); ++i)
44		{
45	362064	zeroes.append("0");
46		}
47	16209	return zeroes + str;
48		}
49		else
50		{
51	13161	return str;
52		}
53		}
54
55	3615781	size_t BitVector::hash() const
56		{
57	3615781	return d_value.hash() + d_size;
58		}
59
60	2715	BitVector& BitVector::setBit(uint32_t i, bool value)
61		{
62	2715	CheckArgument(i < d_size, i);
63	2715	d_value.setBit(i, value);
64	2715	return *this;
65		}
66
67	92144	bool BitVector::isBitSet(uint32_t i) const
68		{
69	92144	CheckArgument(i < d_size, i);
70	92144	return d_value.isBitSet(i);
71		}
72
73	536442	unsigned BitVector::isPow2() const
74		{
75	536442	return d_value.isPow2();
76		}
77
78		/* -----------------------------------------------------------------------
79		* Operators
80		* ----------------------------------------------------------------------- */
81
82		/* String Operations ----------------------------------------------------- */
83
84	159831	BitVector BitVector::concat(const BitVector& other) const
85		{
86	159831	return BitVector(d_size + other.d_size,
87	319662	(d_value.multiplyByPow2(other.d_size)) + other.d_value);
88		}
89
90	374639	BitVector BitVector::extract(unsigned high, unsigned low) const
91		{
92	374639	CheckArgument(high < d_size, high);
93	374637	CheckArgument(low <= high, low);
94	374635	return BitVector(high - low + 1,
95	749270	d_value.extractBitRange(high - low + 1, low));
96		}
97
98		/* (Dis)Equality --------------------------------------------------------- */
99
100	24008142	bool BitVector::operator==(const BitVector& y) const
101		{
102	24008142	if (d_size != y.d_size) return false;
103	23502812	return d_value == y.d_value;
104		}
105
106	1063552	bool BitVector::operator!=(const BitVector& y) const
107		{
108	1063552	if (d_size != y.d_size) return true;
109	1063552	return d_value != y.d_value;
110		}
111
112		/* Unsigned Inequality --------------------------------------------------- */
113
114	1569	bool BitVector::operator<(const BitVector& y) const
115		{
116	1569	return d_value < y.d_value;
117		}
118
119	2354	bool BitVector::operator<=(const BitVector& y) const
120		{
121	2354	return d_value <= y.d_value;
122		}
123
124	2720	bool BitVector::operator>(const BitVector& y) const
125		{
126	2720	return d_value > y.d_value;
127		}
128
129	1011	bool BitVector::operator>=(const BitVector& y) const
130		{
131	1011	return d_value >= y.d_value;
132		}
133
134	10142	bool BitVector::unsignedLessThan(const BitVector& y) const
135		{
136	10142	CheckArgument(d_size == y.d_size, y);
137	10140	CheckArgument(d_value >= 0, this);
138	10140	CheckArgument(y.d_value >= 0, y);
139	10140	return d_value < y.d_value;
140		}
141
142	555	bool BitVector::unsignedLessThanEq(const BitVector& y) const
143		{
144	557	CheckArgument(d_size == y.d_size, this);
145	553	CheckArgument(d_value >= 0, this);
146	553	CheckArgument(y.d_value >= 0, y);
147	553	return d_value <= y.d_value;
148		}
149
150		/* Signed Inequality ----------------------------------------------------- */
151
152	11207	bool BitVector::signedLessThan(const BitVector& y) const
153		{
154	11207	CheckArgument(d_size == y.d_size, y);
155	11205	CheckArgument(d_value >= 0, this);
156	11205	CheckArgument(y.d_value >= 0, y);
157	22410	Integer a = (*this).toSignedInteger();
158	22410	Integer b = y.toSignedInteger();
159
160	22410	return a < b;
161		}
162
163	211602	bool BitVector::signedLessThanEq(const BitVector& y) const
164		{
165	211602	CheckArgument(d_size == y.d_size, y);
166	211600	CheckArgument(d_value >= 0, this);
167	211600	CheckArgument(y.d_value >= 0, y);
168	423200	Integer a = (*this).toSignedInteger();
169	423200	Integer b = y.toSignedInteger();
170
171	423200	return a <= b;
172		}
173
174		/* Bit-wise operations --------------------------------------------------- */
175
176	801	BitVector BitVector::operator^(const BitVector& y) const
177		{
178	801	CheckArgument(d_size == y.d_size, y);
179	801	return BitVector(d_size, d_value.bitwiseXor(y.d_value));
180		}
181
182	417481	BitVector BitVector::operator\|(const BitVector& y) const
183		{
184	417481	CheckArgument(d_size == y.d_size, y);
185	417481	return BitVector(d_size, d_value.bitwiseOr(y.d_value));
186		}
187
188	284169	BitVector BitVector::operator&(const BitVector& y) const
189		{
190	284169	CheckArgument(d_size == y.d_size, y);
191	284169	return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
192		}
193
194	1388232	BitVector BitVector::operator~() const
195		{
196	1388232	return BitVector(d_size, d_value.bitwiseNot());
197		}
198
199		/* Arithmetic operations ------------------------------------------------- */
200
201	1905214	BitVector BitVector::operator+(const BitVector& y) const
202		{
203	1905214	CheckArgument(d_size == y.d_size, y);
204	3810424	Integer sum = d_value + y.d_value;
205	3810424	return BitVector(d_size, sum);
206		}
207
208	407710	BitVector BitVector::operator-(const BitVector& y) const
209		{
210	407710	CheckArgument(d_size == y.d_size, y);
211		// to maintain the invariant that we are only adding BitVectors of the
212		// same size
213	815420	BitVector one(d_size, Integer(1));
214	815420	return *this + ~y + one;
215		}
216
217	815488	BitVector BitVector::operator-() const
218		{
219	1630976	BitVector one(d_size, Integer(1));
220	1630976	return ~(*this) + one;
221		}
222
223	447477	BitVector BitVector::operator*(const BitVector& y) const
224		{
225	447477	CheckArgument(d_size == y.d_size, y);
226	894950	Integer prod = d_value * y.d_value;
227	894950	return BitVector(d_size, prod);
228		}
229
230	61013	BitVector BitVector::unsignedDivTotal(const BitVector& y) const
231		{
232	61013	CheckArgument(d_size == y.d_size, y);
233		/* d_value / 0 = -1 = 2^d_size - 1 */
234	61011	if (y.d_value == 0)
235		{
236	8009	return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
237		}
238	53002	CheckArgument(d_value >= 0, this);
239	53002	CheckArgument(y.d_value > 0, y);
240	53002	return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
241		}
242
243	65921	BitVector BitVector::unsignedRemTotal(const BitVector& y) const
244		{
245	65921	CheckArgument(d_size == y.d_size, y);
246	65919	if (y.d_value == 0)
247		{
248	8478	return BitVector(d_size, d_value);
249		}
250	57441	CheckArgument(d_value >= 0, this);
251	57441	CheckArgument(y.d_value > 0, y);
252	57441	return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
253		}
254
255		/* Extend operations ----------------------------------------------------- */
256
257	66819	BitVector BitVector::zeroExtend(unsigned n) const
258		{
259	66819	return BitVector(d_size + n, d_value);
260		}
261
262	840337	BitVector BitVector::signExtend(unsigned n) const
263		{
264	1680674	Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
265	840337	if (sign_bit == Integer(0))
266		{
267	11695	return BitVector(d_size + n, d_value);
268		}
269	1657284	Integer val = d_value.oneExtend(d_size, n);
270	828642	return BitVector(d_size + n, val);
271		}
272
273		/* Shift operations ------------------------------------------------------ */
274
275	281939	BitVector BitVector::leftShift(const BitVector& y) const
276		{
277	281939	if (y.d_value > Integer(d_size))
278		{
279	1163	return BitVector(d_size, Integer(0));
280		}
281	280776	if (y.d_value == 0)
282		{
283	25175	return *this;
284		}
285		// making sure we don't lose information casting
286	255601	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
287	255601	uint32_t amount = y.d_value.toUnsignedInt();
288	511202	Integer res = d_value.multiplyByPow2(amount);
289	255601	return BitVector(d_size, res);
290		}
291
292	7120	BitVector BitVector::logicalRightShift(const BitVector& y) const
293		{
294	7120	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	7118	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
300	7118	uint32_t amount = y.d_value.toUnsignedInt();
301	14236	Integer res = d_value.divByPow2(amount);
302	7118	return BitVector(d_size, res);
303		}
304
305	2526	BitVector BitVector::arithRightShift(const BitVector& y) const
306		{
307	5052	Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
308	2526	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	2497	if (y.d_value == 0)
321		{
322	429	return *this;
323		}
324
325		// making sure we don't lose information casting
326	2068	CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
327
328	2068	uint32_t amount = y.d_value.toUnsignedInt();
329	4136	Integer rest = d_value.divByPow2(amount);
330
331	2068	if (sign_bit == Integer(0))
332		{
333	1640	return BitVector(d_size, rest);
334		}
335	856	Integer res = rest.oneExtend(d_size - amount, amount);
336	428	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	818317	BitVector BitVector::mkOnes(unsigned size)
356		{
357	818317	CheckArgument(size > 0, size);
358	818317	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	31137	} // namespace cvc5