cprover
bv_arithmetic.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 "bv_arithmetic.h"
10 
11 #include <ostream>
12 
13 #include "string2int.h"
14 #include "arith_tools.h"
15 #include "std_types.h"
16 #include "std_expr.h"
17 
19 {
20  if(is_signed)
21  return signedbv_typet(width);
22  return unsignedbv_typet(width);
23 }
24 
26 {
27  return is_signed?power(2, width-1)-1:
28  power(2, width)-1;
29 }
30 
32 {
33  return is_signed?-power(2, width-1):
34  0;
35 }
36 
37 void bv_spect::from_type(const typet &type)
38 {
39  if(type.id()==ID_unsignedbv)
40  is_signed=false;
41  else if(type.id()==ID_signedbv)
42  is_signed=true;
43  else
45 
46  width=unsafe_string2unsigned(type.get_string(ID_width));
47 }
48 
49 void bv_arithmetict::print(std::ostream &out) const
50 {
51  out << to_ansi_c_string();
52 }
53 
54 std::string bv_arithmetict::format(const format_spect &) const
55 {
56  std::string result;
57 
58  result=integer2string(value);
59 
60  return result;
61 }
62 
64 {
65  value=i;
66  adjust();
67 }
68 
70 {
71  mp_integer p=power(2, spec.width);
72  value%=p;
73 
74  if(value>=p/2)
75  value-=p;
76 }
77 
79 {
80  if(value>=0)
81  return value;
82  return value+power(2, spec.width);
83 }
84 
86 {
88 }
89 
91 {
92  PRECONDITION(other.spec == spec);
93 
94  if(other.value==0)
95  value=0;
96  else
97  value/=other.value;
98 
99  return *this;
100 }
101 
103 {
104  PRECONDITION(other.spec == spec);
105 
106  value*=other.value;
107  adjust();
108 
109  return *this;
110 }
111 
113 {
114  PRECONDITION(other.spec == spec);
115 
116  value+=other.value;
117  adjust();
118 
119  return *this;
120 }
121 
123 {
124  PRECONDITION(other.spec == spec);
125 
126  value-=other.value;
127  adjust();
128 
129  return *this;
130 }
131 
133 {
134  PRECONDITION(other.spec == spec);
135 
136  value%=other.value;
137  adjust();
138 
139  return *this;
140 }
141 
143 {
144  return value<other.value;
145 }
146 
148 {
149  return value<=other.value;
150 }
151 
153 {
154  return value>other.value;
155 }
156 
158 {
159  return value>=other.value;
160 }
161 
163 {
164  return value==other.value;
165 }
166 
168 {
169  return value==i;
170 }
171 
173 {
174  return value!=other.value;
175 }
176 
177 void bv_arithmetict::change_spec(const bv_spect &dest_spec)
178 {
179  spec=dest_spec;
180  adjust();
181 }
182 
184 {
185  spec=bv_spect(expr.type());
187 }
The type of an expression, extends irept.
Definition: type.h:27
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
void from_integer(const mp_integer &i)
BigInt mp_integer
Definition: mp_arith.h:22
void change_spec(const bv_spect &dest_spec)
bool operator<=(const bv_arithmetict &other)
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
bool operator<(const bv_arithmetict &other)
void from_type(const typet &type)
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:69
const irep_idt & get_value() const
Definition: std_expr.h:4403
bv_arithmetict & operator-=(const bv_arithmetict &other)
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
typet & type()
Return the type of the expression.
Definition: expr.h:68
bv_arithmetict & operator*=(const bv_arithmetict &other)
bv_arithmetict & operator%=(const bv_arithmetict &other)
bool operator!=(const bv_arithmetict &other)
A constant literal expression.
Definition: std_expr.h:4384
void print(std::ostream &out) const
std::string to_ansi_c_string() const
Definition: bv_arithmetic.h:87
void from_expr(const constant_exprt &expr)
mp_integer pack() const
bool operator>(const bv_arithmetict &other)
const irep_idt & id() const
Definition: irep.h:259
bool operator>=(const bv_arithmetict &other)
bool is_signed
Definition: bv_arithmetic.h:26
bool operator==(const bv_arithmetict &other)
typet to_type() const
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1278
API to expression classes.
std::size_t width
Definition: bv_arithmetic.h:25
mp_integer max_value() const
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
constant_exprt to_expr() const
mp_integer value
Pre-defined types.
mp_integer min_value() const
bv_arithmetict & operator+=(const bv_arithmetict &other)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
bv_arithmetict & operator/=(const bv_arithmetict &other)
std::string format(const format_spect &format_spec) const
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.