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 <cassert>
12 #include <ostream>
13 
14 #include "string2int.h"
15 #include "arith_tools.h"
16 #include "std_types.h"
17 #include "std_expr.h"
18 
20 {
21  if(is_signed)
22  return signedbv_typet(width);
23  return unsignedbv_typet(width);
24 }
25 
27 {
28  return is_signed?power(2, width-1)-1:
29  power(2, width)-1;
30 }
31 
33 {
34  return is_signed?-power(2, width-1):
35  0;
36 }
37 
38 void bv_spect::from_type(const typet &type)
39 {
40  if(type.id()==ID_unsignedbv)
41  is_signed=false;
42  else if(type.id()==ID_signedbv)
43  is_signed=true;
44  else
45  assert(0);
46 
47  width=unsafe_string2unsigned(type.get_string(ID_width));
48 }
49 
50 void bv_arithmetict::print(std::ostream &out) const
51 {
52  out << to_ansi_c_string();
53 }
54 
55 std::string bv_arithmetict::format(const format_spect &format_spec) const
56 {
57  std::string result;
58 
59  result=integer2string(value);
60 
61  return result;
62 }
63 
65 {
66  value=i;
67  adjust();
68 }
69 
71 {
72  mp_integer p=power(2, spec.width);
73  value%=p;
74 
75  if(value>=p/2)
76  value-=p;
77 }
78 
80 {
81  if(value>=0)
82  return value;
83  return value+power(2, spec.width);
84 }
85 
87 {
88  constant_exprt result(spec.to_type());
90  return result;
91 }
92 
94 {
95  assert(other.spec==spec);
96 
97  if(other.value==0)
98  value=0;
99  else
100  value/=other.value;
101 
102  return *this;
103 }
104 
106 {
107  assert(other.spec==spec);
108 
109  value*=other.value;
110  adjust();
111 
112  return *this;
113 }
114 
116 {
117  assert(other.spec==spec);
118 
119  value+=other.value;
120  adjust();
121 
122  return *this;
123 }
124 
126 {
127  assert(other.spec==spec);
128 
129  value-=other.value;
130  adjust();
131 
132  return *this;
133 }
134 
136 {
137  assert(other.spec==spec);
138 
139  value%=other.value;
140  adjust();
141 
142  return *this;
143 }
144 
146 {
147  return value<other.value;
148 }
149 
151 {
152  return value<=other.value;
153 }
154 
156 {
157  return value>other.value;
158 }
159 
161 {
162  return value>=other.value;
163 }
164 
166 {
167  return value==other.value;
168 }
169 
171 {
172  return value==i;
173 }
174 
176 {
177  return value!=other.value;
178 }
179 
180 void bv_arithmetict::change_spec(const bv_spect &dest_spec)
181 {
182  spec=dest_spec;
183  adjust();
184 }
185 
187 {
188  assert(expr.is_constant());
189  spec=bv_spect(expr.type());
190  value=binary2integer(expr.get_string(ID_value), spec.is_signed);
191 }
The type of an expression.
Definition: type.h:20
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1125
void from_integer(const mp_integer &i)
BigInt mp_integer
Definition: mp_arith.h:19
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:104
bool operator<(const bv_arithmetict &other)
void from_type(const typet &type)
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
bv_arithmetict & operator-=(const bv_arithmetict &other)
typet & type()
Definition: expr.h:60
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:3685
void from_expr(const exprt &expr)
void print(std::ostream &out) const
std::string to_ansi_c_string() const
Definition: bv_arithmetic.h:86
mp_integer pack() const
bool operator>(const bv_arithmetict &other)
const irep_idt & id() const
Definition: irep.h:189
void set_value(const irep_idt &value)
Definition: std_expr.h:3707
bool operator>=(const bv_arithmetict &other)
bool is_signed
Definition: bv_arithmetic.h:25
bool operator==(const bv_arithmetict &other)
typet to_type() const
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1171
API to expression classes.
std::size_t width
Definition: bv_arithmetic.h:24
mp_integer max_value() const
mp_integer value
bool is_constant() const
Definition: expr.cpp:128
API to type classes.
mp_integer min_value() const
Base class for all expressions.
Definition: expr.h:46
bv_arithmetict & operator+=(const bv_arithmetict &other)
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:63
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
bv_arithmetict & operator/=(const bv_arithmetict &other)
std::string format(const format_spect &format_spec) const
exprt to_expr() const
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.