CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
mp_arith.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "mp_arith.h"
10
11#include <algorithm>
12#include <cctype>
13#include <climits>
14#include <vector>
15
16#include "arith_tools.h"
17#include "invariant.h"
18
19typedef BigInt::ullong_t ullong_t; // NOLINT(readability/identifiers)
20typedef BigInt::llong_t llong_t; // NOLINT(readability/identifiers)
21
23{
25
26 if(a>=0)
27 return a/power;
28 else
29 {
30 // arithmetic shift right isn't division for negative numbers!
31 // http://en.wikipedia.org/wiki/Arithmetic_shift
32
33 if((a%power)==0)
34 return a/power;
35 else
36 return a/power-1;
37 }
38}
39
41{
42 return a*power(2, b);
43}
44
45std::ostream &operator<<(std::ostream &out, const mp_integer &n)
46{
47 out << integer2string(n);
48 return out;
49}
50
54const mp_integer string2integer(const std::string &n, unsigned base)
55{
56 for(std::size_t i=0; i<n.size(); i++)
57 if(!(isalnum(n[i]) || (n[i]=='-' && i==0)))
58 return 0;
59
60 return mp_integer(n.c_str(), base);
61}
62
64const std::string integer2binary(const mp_integer &n, std::size_t width)
65{
66 mp_integer a(n);
67
68 if(width==0)
69 return "";
70
71 bool neg=a.is_negative();
72
73 if(neg)
74 {
75 a.negate();
76 a=a-1;
77 }
78
79 std::size_t len = a.digits(2) + 2;
80 std::vector<char> buffer(len);
81 char *s = a.as_string(buffer.data(), len, 2);
82
83 std::string result(s);
84
85 if(result.size()<width)
86 {
87 std::string fill;
88 fill.resize(width-result.size(), '0');
89 result=fill+result;
90 }
91 else if(result.size()>width)
92 result=result.substr(result.size()-width, width);
93
94 if(neg)
95 {
96 for(std::size_t i=0; i<result.size(); i++)
97 result[i]=(result[i]=='0')?'1':'0';
98 }
99
100 return result;
101}
102
103const std::string integer2string(const mp_integer &n, unsigned base)
104{
105 unsigned len = n.digits(base) + 2;
106 std::vector<char> buffer(len);
107 char *s = n.as_string(buffer.data(), len, base);
108
109 std::string result(s);
110
111 return result;
112}
113
117const mp_integer binary2integer(const std::string &n, bool is_signed)
118{
119 if(n.empty())
120 return 0;
121
122 if(n.size() <= (sizeof(unsigned long) * CHAR_BIT))
123 {
124 // this is a tuned implementation for short integers
125
126 unsigned long mask=1;
127 mask=mask << (n.size()-1);
128 mp_integer top_bit=(n[0]=='1') ? mask : 0;
129 if(is_signed)
130 top_bit.negate();
131 mask>>=1;
132 unsigned long other_bits=0;
133
134 for(std::string::const_iterator it=++n.begin();
135 it!=n.end();
136 ++it)
137 {
138 if(*it=='1')
139 other_bits+=mask;
140 else if(*it!='0')
141 return 0;
142
143 mask>>=1;
144 }
145
146 return top_bit+other_bits;
147 }
148
149 #if 0
150
151 mp_integer mask=1;
152 mask=mask << (n.size()-1);
153 mp_integer result=(n[0]=='1') ? mask : 0;
154 if(is_signed)
155 result.negate();
156 mask=mask>>1;
157
158 for(std::string::const_iterator it=++n.begin();
159 it!=n.end();
160 ++it)
161 {
162 if(*it=='1')
163 result+=mask;
164
165 mask=mask>>1;
166 }
167
168 return result;
169
170 #else
171 if(n.find_first_not_of("01")!=std::string::npos)
172 return 0;
173
174 if(is_signed && n[0]=='1')
175 {
176 mp_integer result(n.c_str()+1, 2);
177 result-=mp_integer(1)<<(n.size()-1);
178 return result;
179 }
180 else
181 return BigInt(n.c_str(), 2);
182
183 #endif
184}
185
191 const mp_integer &a,
192 const mp_integer &b,
193 std::function<bool(bool, bool)> f)
194{
195 const auto digits = std::max(a.digits(2), b.digits(2));
196
197 mp_integer result = 0;
198 mp_integer tmp_a = a, tmp_b = b;
199
200 for(std::size_t i = 0; i < digits; i++)
201 {
202 const bool bit_a = tmp_a.is_odd();
203 const bool bit_b = tmp_b.is_odd();
204 const bool bit_result = f(bit_a, bit_b);
205 if(bit_result)
206 result += power(2, i);
207 tmp_a /= 2;
208 tmp_b /= 2;
209 }
210
211 return result;
212}
213
216{
217 PRECONDITION(!a.is_negative() && !b.is_negative());
218
219 // fast path for small numbers
220 if(a.is_ulong() && b.is_ulong())
221 return a.to_ulong() | b.to_ulong();
222
223 return bitwise(a, b, [](bool a, bool b) { return a || b; });
224}
225
228{
229 PRECONDITION(!a.is_negative() && !b.is_negative());
230
231 // fast path for small numbers
232 if(a.is_ulong() && b.is_ulong())
233 return a.to_ulong() & b.to_ulong();
234
235 return bitwise(a, b, [](bool a, bool b) { return a && b; });
236}
237
240{
241 PRECONDITION(!a.is_negative() && !b.is_negative());
242
243 // fast path for small numbers
244 if(a.is_ulong() && b.is_ulong())
245 return a.to_ulong() ^ b.to_ulong();
246
247 return bitwise(a, b, [](bool a, bool b) { return a != b; });
248}
249
254 const mp_integer &a,
255 const mp_integer &b,
256 std::size_t true_size)
257{
258 PRECONDITION(a.is_long() && b.is_ulong());
259 PRECONDITION(b <= true_size || a == 0);
260
261 ullong_t shift=b.to_ulong();
262
263 llong_t result=a.to_long()<<shift;
264 llong_t mask =
265 true_size < (sizeof(llong_t) * CHAR_BIT) ? (1LL << true_size) - 1 : -1;
266 return result&mask;
267}
268
273 const mp_integer &a,
274 const mp_integer &b,
275 std::size_t true_size)
276{
277 PRECONDITION(a.is_long() && b.is_ulong());
278 llong_t number=a.to_long();
279 ullong_t shift=b.to_ulong();
280 PRECONDITION(shift <= true_size);
281
282 const llong_t sign = (1LL << (true_size - 1)) & number;
283 const llong_t pad = (sign == 0) ? 0 : ~((1LL << (true_size - shift)) - 1);
284 llong_t result=(number >> shift)|pad;
285 return result;
286}
287
292 const mp_integer &a,
293 const mp_integer &b,
294 std::size_t true_size)
295{
296 PRECONDITION(a.is_long() && b.is_ulong());
297 PRECONDITION(b <= true_size || a == 0);
298
299 ullong_t shift=b.to_ulong();
300 llong_t result=a.to_long()<<shift;
301 if(true_size < (sizeof(llong_t) * CHAR_BIT))
302 {
303 const llong_t sign = (1LL << (true_size - 1)) & result;
304 const llong_t mask = (1LL << true_size) - 1;
305 // Sign-fill out-of-range bits:
306 if(sign==0)
307 result&=mask;
308 else
309 result|=~mask;
310 }
311 return result;
312}
313
318 const mp_integer &a,
319 const mp_integer &b,
320 std::size_t true_size)
321{
322 PRECONDITION(a.is_long() && b.is_ulong());
324
325 ullong_t shift = b.to_ulong();
326 ullong_t result=((ullong_t)a.to_long()) >> shift;
327 return result;
328}
329
334 const mp_integer &a,
335 const mp_integer &b,
336 std::size_t true_size)
337{
338 PRECONDITION(a.is_ulong() && b.is_ulong());
340
341 ullong_t number=a.to_ulong();
342 ullong_t shift=b.to_ulong();
343
345 const ullong_t filter = 1ULL << (true_size - 1);
346 ullong_t result=(number >> shift)|((number<<revShift)&filter);
347 return result;
348}
349
354 const mp_integer &a,
355 const mp_integer &b,
356 std::size_t true_size)
357{
358 PRECONDITION(a.is_ulong() && b.is_ulong());
360
361 ullong_t number=a.to_ulong();
362 ullong_t shift=b.to_ulong();
363
365 const ullong_t filter = 1ULL << (true_size - 1);
366 ullong_t result=((number<<shift)&filter)|((number&filter) >> revShift);
367 return result;
368}
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
int isalnum(int c)
Definition ctype.c:4
literalt neg(literalt a)
Definition literal.h:193
BigInt::llong_t llong_t
Definition mp_arith.cpp:20
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition mp_arith.cpp:117
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
BigInt::ullong_t ullong_t
Definition mp_arith.cpp:19
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:317
mp_integer operator>>(const mp_integer &a, const mp_integer &b)
Definition mp_arith.cpp:22
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:253
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:272
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:291
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:333
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
mp_integer bitwise_and(const mp_integer &a, const mp_integer &b)
bitwise 'and' of two nonnegative integers
Definition mp_arith.cpp:227
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
Definition mp_arith.cpp:215
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise 'xor' of two nonnegative integers
Definition mp_arith.cpp:239
mp_integer operator<<(const mp_integer &a, const mp_integer &b)
Definition mp_arith.cpp:40
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:190
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:353
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition mp_arith.cpp:64
static struct_typet::componentst::iterator pad(struct_typet::componentst &components, struct_typet::componentst::iterator where, std::size_t pad_bits)
Definition padding.cpp:154
BigInt mp_integer
Definition smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition invariant.h:463
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45