Skip to content

Commit 2987406

Browse files
dcattaruzzapeterschrammel
dcattaruzza
authored and
peterschrammel
committed
Bitwise operators for mpinteger
1 parent 27153d1 commit 2987406

File tree

2 files changed

+287
-0
lines changed

2 files changed

+287
-0
lines changed

‎src/util/mp_arith.cpp

+264
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,9 @@ Author: Daniel Kroening, [email protected]
1717
#include "mp_arith.h"
1818
#include "arith_tools.h"
1919

20+
21+
typedef BigInt::ullong_t ullong_t;
22+
2023
/*******************************************************************\
2124
2225
Function: >>
@@ -320,3 +323,264 @@ unsigned integer2unsigned(const mp_integer &n)
320323
assert(ull <= std::numeric_limits<unsigned>::max());
321324
return (unsigned)ull;
322325
}
326+
327+
/*******************************************************************\
328+
329+
Function: bitwise_or
330+
331+
Inputs:
332+
333+
Outputs:
334+
335+
Purpose: bitwise or
336+
bitwise operations only make sense on native objects, hence the
337+
largest object size should be the largest available c++ integer
338+
size (currently long long)
339+
340+
\*******************************************************************/
341+
342+
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
343+
{
344+
ullong_t result=a.to_ulong()|b.to_ulong();
345+
return result;
346+
}
347+
348+
/*******************************************************************\
349+
350+
Function: bitwise_and
351+
352+
Inputs:
353+
354+
Outputs:
355+
356+
Purpose: bitwise and
357+
bitwise operations only make sense on native objects, hence the
358+
largest object size should be the largest available c++ integer
359+
size (currently long long)
360+
361+
\*******************************************************************/
362+
363+
mp_integer bitwise_and(const mp_integer &a, const mp_integer &b)
364+
{
365+
ullong_t result=a.to_ulong()&b.to_ulong();
366+
return result;
367+
}
368+
369+
/*******************************************************************\
370+
371+
Function: bitwise_xor
372+
373+
Inputs:
374+
375+
Outputs:
376+
377+
Purpose: bitwise xor
378+
bitwise operations only make sense on native objects, hence the
379+
largest object size should be the largest available c++ integer
380+
size (currently long long)
381+
382+
\*******************************************************************/
383+
384+
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
385+
{
386+
ullong_t result=a.to_ulong()^b.to_ulong();
387+
return result;
388+
}
389+
390+
/*******************************************************************\
391+
392+
Function: bitwise_neg
393+
394+
Inputs:
395+
396+
Outputs:
397+
398+
Purpose: bitwise negation
399+
bitwise operations only make sense on native objects, hence the
400+
largest object size should be the largest available c++ integer
401+
size (currently long long)
402+
403+
\*******************************************************************/
404+
405+
mp_integer bitwise_neg(const mp_integer &a)
406+
{
407+
ullong_t result=~a.to_ulong();
408+
return result;
409+
}
410+
411+
/*******************************************************************\
412+
413+
Function: arith_left_shift
414+
415+
Inputs:
416+
417+
Outputs:
418+
419+
Purpose: arithmetic left shift
420+
bitwise operations only make sense on native objects, hence the
421+
largest object size should be the largest available c++ integer
422+
size (currently long long)
423+
424+
\*******************************************************************/
425+
426+
mp_integer arith_left_shift(
427+
const mp_integer &a,
428+
const mp_integer &b,
429+
std::size_t true_size)
430+
{
431+
ullong_t shift=b.to_ulong();
432+
if(shift>true_size && a!=mp_integer(0))
433+
throw "shift value out of range";
434+
435+
ullong_t result=a.to_ulong()<<shift;
436+
return result;
437+
}
438+
439+
/*******************************************************************\
440+
441+
Function: arith_right_shift
442+
443+
Inputs:
444+
445+
Outputs:
446+
447+
Purpose: arithmetic right shift (loads sign on MSB)
448+
bitwise operations only make sense on native objects, hence the
449+
largest object size should be the largest available c++ integer
450+
size (currently long long)
451+
452+
\*******************************************************************/
453+
454+
mp_integer arith_right_shift(
455+
const mp_integer &a,
456+
const mp_integer &b,
457+
std::size_t true_size)
458+
{
459+
ullong_t number=a.to_ulong();
460+
ullong_t shift=b.to_ulong();
461+
if(shift>true_size)
462+
throw "shift value out of range";
463+
464+
ullong_t sign=(1<<(true_size-1))&number;
465+
ullong_t pad=(sign==0) ? 0 : ~((1<<(true_size-shift))-1);
466+
ullong_t result=(number>>shift)|pad;
467+
return result;
468+
}
469+
470+
/*******************************************************************\
471+
472+
Function: logic_left_shift
473+
474+
Inputs:
475+
476+
Outputs:
477+
478+
Purpose: logic left shift
479+
bitwise operations only make sense on native objects, hence the
480+
largest object size should be the largest available c++ integer
481+
size (currently long long)
482+
483+
\*******************************************************************/
484+
485+
mp_integer logic_left_shift(
486+
const mp_integer &a,
487+
const mp_integer &b,
488+
std::size_t true_size)
489+
{
490+
ullong_t shift=b.to_ulong();
491+
if(shift>true_size && a!=mp_integer(0))
492+
throw "shift value out of range";
493+
494+
ullong_t result=a.to_ulong()<<shift;
495+
return result;
496+
}
497+
498+
/*******************************************************************\
499+
500+
Function: logic_right_shift
501+
502+
Inputs:
503+
504+
Outputs:
505+
506+
Purpose: logic right shift (loads 0 on MSB)
507+
bitwise operations only make sense on native objects, hence the
508+
largest object size should be the largest available c++ integer
509+
size (currently long long)
510+
511+
\*******************************************************************/
512+
513+
mp_integer logic_right_shift(
514+
const mp_integer &a,
515+
const mp_integer &b,
516+
std::size_t true_size)
517+
{
518+
ullong_t shift=b.to_ulong();
519+
if(shift>true_size)
520+
throw "shift value out of range";
521+
522+
ullong_t result=a.to_ulong()>>shift;
523+
return result;
524+
}
525+
526+
/*******************************************************************\
527+
528+
Function: rotate_right
529+
530+
Inputs:
531+
532+
Outputs:
533+
534+
Purpose: rotates right (MSB=LSB)
535+
bitwise operations only make sense on native objects, hence the
536+
largest object size should be the largest available c++ integer
537+
size (currently long long)
538+
539+
\*******************************************************************/
540+
541+
mp_integer rotate_right(
542+
const mp_integer &a,
543+
const mp_integer &b,
544+
std::size_t true_size)
545+
{
546+
ullong_t number=a.to_ulong();
547+
ullong_t shift=b.to_ulong();
548+
if(shift>true_size)
549+
throw "shift value out of range";
550+
551+
ullong_t revShift=true_size-shift;
552+
ullong_t filter=1<<(true_size-1);
553+
ullong_t result=(number>>shift)|((number<<revShift)&filter);
554+
return result;
555+
}
556+
557+
/*******************************************************************\
558+
559+
Function: rotate_left
560+
561+
Inputs:
562+
563+
Outputs:
564+
565+
Purpose: rotate left (LSB=MSB)
566+
bitwise operations only make sense on native objects, hence the
567+
largest object size should be the largest available c++ integer
568+
size (currently long long)
569+
570+
\*******************************************************************/
571+
572+
mp_integer rotate_left(
573+
const mp_integer &a,
574+
const mp_integer &b,
575+
std::size_t true_size)
576+
{
577+
ullong_t number=a.to_ulong();
578+
ullong_t shift=b.to_ulong();
579+
if(shift>true_size)
580+
throw "shift value out of range";
581+
582+
ullong_t revShift=true_size-shift;
583+
ullong_t filter=1<<(true_size-1);
584+
ullong_t result=((number<<shift)&filter)|((number&filter)>>revShift);
585+
return result;
586+
}

‎src/util/mp_arith.h

+23
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,28 @@ typedef BigInt mp_integer;
2020
std::ostream &operator<<(std::ostream &, const mp_integer &);
2121
mp_integer operator>>(const mp_integer &, const mp_integer &);
2222
mp_integer operator<<(const mp_integer &, const mp_integer &);
23+
mp_integer bitwise_or(const mp_integer &, const mp_integer &);
24+
mp_integer bitwise_and(const mp_integer &, const mp_integer &);
25+
mp_integer bitwise_xor(const mp_integer &, const mp_integer &);
26+
mp_integer bitwise_neg(const mp_integer &);
27+
28+
mp_integer arith_left_shift(
29+
const mp_integer &, const mp_integer &, std::size_t true_size);
30+
31+
mp_integer arith_right_shift(
32+
const mp_integer &, const mp_integer &, std::size_t true_size);
33+
34+
mp_integer logic_left_shift(
35+
const mp_integer &, const mp_integer &, std::size_t true_size);
36+
37+
mp_integer logic_right_shift(
38+
const mp_integer &, const mp_integer &, std::size_t true_size);
39+
40+
mp_integer rotate_right(
41+
const mp_integer &, const mp_integer &, std::size_t true_size);
42+
43+
mp_integer rotate_left(
44+
const mp_integer &, const mp_integer &, std::size_t true_size);
2345

2446
const std::string integer2string(const mp_integer &, unsigned base=10);
2547
const mp_integer string2integer(const std::string &, unsigned base=10);
@@ -28,5 +50,6 @@ const mp_integer binary2integer(const std::string &, bool is_signed);
2850
mp_integer::ullong_t integer2ulong(const mp_integer &);
2951
std::size_t integer2size_t(const mp_integer &);
3052
unsigned integer2unsigned(const mp_integer &);
53+
const mp_integer mp_zero=string2integer("0");
3154

3255
#endif // CPROVER_UTIL_MP_ARITH_H

0 commit comments

Comments
 (0)