cprover
mp_arith.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "mp_arith.h"
10 
11 #include <algorithm>
12 #include <cctype>
13 #include <cstdlib>
14 #include <limits>
15 #include <ostream>
16 #include <sstream>
17 #include <vector>
18 
19 #include "arith_tools.h"
20 #include "invariant.h"
21 
22 typedef BigInt::ullong_t ullong_t; // NOLINT(readability/identifiers)
23 typedef BigInt::llong_t llong_t; // NOLINT(readability/identifiers)
24 
26 {
27  mp_integer power=::power(2, b);
28 
29  if(a>=0)
30  return a/power;
31  else
32  {
33  // arithmetic shift right isn't division for negative numbers!
34  // http://en.wikipedia.org/wiki/Arithmetic_shift
35 
36  if((a%power)==0)
37  return a/power;
38  else
39  return a/power-1;
40  }
41 }
42 
44 {
45  return a*power(2, b);
46 }
47 
48 std::ostream &operator<<(std::ostream &out, const mp_integer &n)
49 {
50  out << integer2string(n);
51  return out;
52 }
53 
57 const mp_integer string2integer(const std::string &n, unsigned base)
58 {
59  for(std::size_t i=0; i<n.size(); i++)
60  if(!(isalnum(n[i]) || (n[i]=='-' && i==0)))
61  return 0;
62 
63  return mp_integer(n.c_str(), base);
64 }
65 
67 const std::string integer2binary(const mp_integer &n, std::size_t width)
68 {
69  mp_integer a(n);
70 
71  if(width==0)
72  return "";
73 
74  bool neg=a.is_negative();
75 
76  if(neg)
77  {
78  a.negate();
79  a=a-1;
80  }
81 
82  std::size_t len = a.digits(2) + 2;
83  std::vector<char> buffer(len);
84  char *s = a.as_string(buffer.data(), len, 2);
85 
86  std::string result(s);
87 
88  if(result.size()<width)
89  {
90  std::string fill;
91  fill.resize(width-result.size(), '0');
92  result=fill+result;
93  }
94  else if(result.size()>width)
95  result=result.substr(result.size()-width, width);
96 
97  if(neg)
98  {
99  for(std::size_t i=0; i<result.size(); i++)
100  result[i]=(result[i]=='0')?'1':'0';
101  }
102 
103  return result;
104 }
105 
106 const std::string integer2string(const mp_integer &n, unsigned base)
107 {
108  unsigned len = n.digits(base) + 2;
109  std::vector<char> buffer(len);
110  char *s = n.as_string(buffer.data(), len, base);
111 
112  std::string result(s);
113 
114  return result;
115 }
116 
120 const mp_integer binary2integer(const std::string &n, bool is_signed)
121 {
122  if(n.empty())
123  return 0;
124 
125  if(n.size()<=(sizeof(unsigned long)*8))
126  {
127  // this is a tuned implementation for short integers
128 
129  unsigned long mask=1;
130  mask=mask << (n.size()-1);
131  mp_integer top_bit=(n[0]=='1') ? mask : 0;
132  if(is_signed)
133  top_bit.negate();
134  mask>>=1;
135  unsigned long other_bits=0;
136 
137  for(std::string::const_iterator it=++n.begin();
138  it!=n.end();
139  ++it)
140  {
141  if(*it=='1')
142  other_bits+=mask;
143  else if(*it!='0')
144  return 0;
145 
146  mask>>=1;
147  }
148 
149  return top_bit+other_bits;
150  }
151 
152  #if 0
153 
154  mp_integer mask=1;
155  mask=mask << (n.size()-1);
156  mp_integer result=(n[0]=='1') ? mask : 0;
157  if(is_signed)
158  result.negate();
159  mask=mask>>1;
160 
161  for(std::string::const_iterator it=++n.begin();
162  it!=n.end();
163  ++it)
164  {
165  if(*it=='1')
166  result+=mask;
167 
168  mask=mask>>1;
169  }
170 
171  return result;
172 
173  #else
174  if(n.find_first_not_of("01")!=std::string::npos)
175  return 0;
176 
177  if(is_signed && n[0]=='1')
178  {
179  mp_integer result(n.c_str()+1, 2);
180  result-=mp_integer(1)<<(n.size()-1);
181  return result;
182  }
183  else
184  return BigInt(n.c_str(), 2);
185 
186  #endif
187 }
188 
190 {
191  PRECONDITION(n.is_ulong());
192  return n.to_ulong();
193 }
194 
195 std::size_t integer2size_t(const mp_integer &n)
196 {
197  PRECONDITION(n>=0 && n<=std::numeric_limits<std::size_t>::max());
198  PRECONDITION(n.is_ulong());
199  mp_integer::ullong_t ull = n.to_ulong();
200  return (std::size_t) ull;
201 }
202 
203 unsigned integer2unsigned(const mp_integer &n)
204 {
205  PRECONDITION(n>=0 && n<=std::numeric_limits<unsigned>::max());
206  PRECONDITION(n.is_ulong());
207  mp_integer::ullong_t ull = n.to_ulong();
208  return (unsigned)ull;
209 }
210 
216  const mp_integer &a,
217  const mp_integer &b,
218  std::function<bool(bool, bool)> f)
219 {
220  const auto digits = std::max(a.digits(2), b.digits(2));
221 
222  mp_integer result = 0;
223  mp_integer tmp_a = a, tmp_b = b;
224 
225  for(std::size_t i = 0; i < digits; i++)
226  {
227  const bool bit_a = tmp_a.is_odd();
228  const bool bit_b = tmp_b.is_odd();
229  const bool bit_result = f(bit_a, bit_b);
230  if(bit_result)
231  result += power(2, i);
232  tmp_a /= 2;
233  tmp_b /= 2;
234  }
235 
236  return result;
237 }
238 
241 {
242  PRECONDITION(!a.is_negative() && !b.is_negative());
243 
244  // fast path for small numbers
245  if(a.is_ulong() && b.is_ulong())
246  return a.to_ulong() | b.to_ulong();
247 
248  return bitwise(a, b, [](bool a, bool b) { return a || b; });
249 }
250 
253 {
254  PRECONDITION(!a.is_negative() && !b.is_negative());
255 
256  // fast path for small numbers
257  if(a.is_ulong() && b.is_ulong())
258  return a.to_ulong() & b.to_ulong();
259 
260  return bitwise(a, b, [](bool a, bool b) { return a && b; });
261 }
262 
265 {
266  PRECONDITION(!a.is_negative() && !b.is_negative());
267 
268  // fast path for small numbers
269  if(a.is_ulong() && b.is_ulong())
270  return a.to_ulong() ^ b.to_ulong();
271 
272  return bitwise(a, b, [](bool a, bool b) { return a != b; });
273 }
274 
279  const mp_integer &a,
280  const mp_integer &b,
281  std::size_t true_size)
282 {
283  PRECONDITION(a.is_long() && b.is_ulong());
284  PRECONDITION(b <= true_size || a == 0);
285 
286  ullong_t shift=b.to_ulong();
287 
288  llong_t result=a.to_long()<<shift;
289  llong_t mask=
290  true_size<(sizeof(llong_t)*8) ?
291  (1LL << true_size) - 1 :
292  -1;
293  return result&mask;
294 }
295 
300  const mp_integer &a,
301  const mp_integer &b,
302  std::size_t true_size)
303 {
304  PRECONDITION(a.is_long() && b.is_ulong());
305  llong_t number=a.to_long();
306  ullong_t shift=b.to_ulong();
307  PRECONDITION(shift <= true_size);
308 
309  const llong_t sign = (1LL << (true_size - 1)) & number;
310  const llong_t pad = (sign == 0) ? 0 : ~((1LL << (true_size - shift)) - 1);
311  llong_t result=(number >> shift)|pad;
312  return result;
313 }
314 
319  const mp_integer &a,
320  const mp_integer &b,
321  std::size_t true_size)
322 {
323  PRECONDITION(a.is_long() && b.is_ulong());
324  PRECONDITION(b <= true_size || a == 0);
325 
326  ullong_t shift=b.to_ulong();
327  llong_t result=a.to_long()<<shift;
328  if(true_size<(sizeof(llong_t)*8))
329  {
330  const llong_t sign = (1LL << (true_size - 1)) & result;
331  const llong_t mask = (1LL << true_size) - 1;
332  // Sign-fill out-of-range bits:
333  if(sign==0)
334  result&=mask;
335  else
336  result|=~mask;
337  }
338  return result;
339 }
340 
345  const mp_integer &a,
346  const mp_integer &b,
347  std::size_t true_size)
348 {
349  PRECONDITION(a.is_long() && b.is_ulong());
350  PRECONDITION(b <= true_size);
351 
352  ullong_t shift = b.to_ulong();
353  ullong_t result=((ullong_t)a.to_long()) >> shift;
354  return result;
355 }
356 
361  const mp_integer &a,
362  const mp_integer &b,
363  std::size_t true_size)
364 {
365  PRECONDITION(a.is_ulong() && b.is_ulong());
366  PRECONDITION(b <= true_size);
367 
368  ullong_t number=a.to_ulong();
369  ullong_t shift=b.to_ulong();
370 
371  ullong_t revShift=true_size-shift;
372  const ullong_t filter = 1ULL << (true_size - 1);
373  ullong_t result=(number >> shift)|((number<<revShift)&filter);
374  return result;
375 }
376 
381  const mp_integer &a,
382  const mp_integer &b,
383  std::size_t true_size)
384 {
385  PRECONDITION(a.is_ulong() && b.is_ulong());
386  PRECONDITION(b <= true_size);
387 
388  ullong_t number=a.to_ulong();
389  ullong_t shift=b.to_ulong();
390 
391  ullong_t revShift=true_size-shift;
392  const ullong_t filter = 1ULL << (true_size - 1);
393  ullong_t result=((number<<shift)&filter)|((number&filter) >> revShift);
394  return result;
395 }
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
BigInt mp_integer
Definition: mp_arith.h:22
mp_integer rotate_left(const mp_integer &a, const mp_integer &b, std::size_t true_size)
rotate left (LSB=MSB) bitwise operations only make sense on native objects, hence the largest object ...
Definition: mp_arith.cpp:380
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
mp_integer::ullong_t integer2ulong(const mp_integer &n)
Definition: mp_arith.cpp:189
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise 'xor' of two nonnegative integers
Definition: mp_arith.cpp:264
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
mp_integer arith_left_shift(const mp_integer &a, const mp_integer &b, std::size_t true_size)
arithmetic left shift bitwise operations only make sense on native objects, hence the largest object ...
Definition: mp_arith.cpp:278
mp_integer logic_left_shift(const mp_integer &a, const mp_integer &b, std::size_t true_size)
logic left shift bitwise operations only make sense on native objects, hence the largest object size ...
Definition: mp_arith.cpp:318
static struct_typet::componentst::iterator pad(struct_typet::componentst &components, struct_typet::componentst::iterator where, std::size_t pad_bits)
Definition: padding.cpp:151
mp_integer operator<<(const mp_integer &a, const mp_integer &b)
Definition: mp_arith.cpp:43
mp_integer logic_right_shift(const mp_integer &a, const mp_integer &b, std::size_t true_size)
logic right shift (loads 0 on MSB) bitwise operations only make sense on native objects,...
Definition: mp_arith.cpp:344
mp_integer bitwise_and(const mp_integer &a, const mp_integer &b)
bitwise 'and' of two nonnegative integers
Definition: mp_arith.cpp:252
mp_integer arith_right_shift(const mp_integer &a, const mp_integer &b, std::size_t true_size)
arithmetic right shift (loads sign on MSB) bitwise operations only make sense on native objects,...
Definition: mp_arith.cpp:299
mp_integer operator>>(const mp_integer &a, const mp_integer &b)
Definition: mp_arith.cpp:25
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
mp_integer rotate_right(const mp_integer &a, const mp_integer &b, std::size_t true_size)
rotates right (MSB=LSB) bitwise operations only make sense on native objects, hence the largest objec...
Definition: mp_arith.cpp:360
BigInt::llong_t llong_t
Definition: mp_arith.cpp:23
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
Definition: mp_arith.cpp:240
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
BigInt::ullong_t ullong_t
Definition: mp_arith.cpp:22
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
literalt neg(literalt a)
Definition: literal.h:192
mp_integer bitwise(const mp_integer &a, const mp_integer &b, std::function< bool(bool, bool)> f)
bitwise binary operation over two integers, given as a functor
Definition: mp_arith.cpp:215
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.