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 
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 }
bv_arithmetict::operator-=
bv_arithmetict & operator-=(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:122
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
bv_arithmetict::format
std::string format(const format_spect &format_spec) const
Definition: bv_arithmetic.cpp:54
arith_tools.h
bv_arithmetict::operator%=
bv_arithmetict & operator%=(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:132
bv_arithmetict::pack
mp_integer pack() const
Definition: bv_arithmetic.cpp:78
bv_spect::is_signed
bool is_signed
Definition: bv_arithmetic.h:26
format_spect
Definition: format_spec.h:16
typet
The type of an expression, extends irept.
Definition: type.h:29
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
bv_arithmetict::operator!=
bool operator!=(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:172
bv_arithmetic.h
bv_arithmetict::operator<=
bool operator<=(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:147
bv_arithmetict::from_expr
void from_expr(const constant_exprt &expr)
Definition: bv_arithmetic.cpp:183
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
bv_arithmetict::operator==
bool operator==(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:162
integer2bvrep
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...
Definition: arith_tools.cpp:379
bv_arithmetict::operator+=
bv_arithmetict & operator+=(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:112
bv_spect
Definition: bv_arithmetic.h:23
bv_arithmetict::print
void print(std::ostream &out) const
Definition: bv_arithmetic.cpp:49
bv_spect::from_type
void from_type(const typet &type)
Definition: bv_arithmetic.cpp:37
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
std_types.h
Pre-defined types.
bv_arithmetict::from_integer
void from_integer(const mp_integer &i)
Definition: bv_arithmetic.cpp:63
bv_spect::to_type
typet to_type() const
Definition: bv_arithmetic.cpp:18
irept::id
const irep_idt & id() const
Definition: irep.h:418
bv_arithmetict::operator/=
bv_arithmetict & operator/=(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:90
bv_arithmetict::change_spec
void change_spec(const bv_spect &dest_spec)
Definition: bv_arithmetic.cpp:177
bv_spect::width
std::size_t width
Definition: bv_arithmetic.h:25
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
bv_arithmetict::adjust
void adjust()
Definition: bv_arithmetic.cpp:69
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:401
bv_arithmetict::value
mp_integer value
Definition: bv_arithmetic.h:123
bv_arithmetict::to_expr
constant_exprt to_expr() const
Definition: bv_arithmetic.cpp:85
bv_arithmetict::operator>=
bool operator>=(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:157
bv_arithmetict::to_ansi_c_string
std::string to_ansi_c_string() const
Definition: bv_arithmetic.h:87
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
bv_spect::min_value
mp_integer min_value() const
Definition: bv_arithmetic.cpp:31
bv_arithmetict::operator<
bool operator<(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:142
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
bv_arithmetict
Definition: bv_arithmetic.h:51
std_expr.h
API to expression classes.
bv_spect::max_value
mp_integer max_value() const
Definition: bv_arithmetic.cpp:25
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
bv_arithmetict::operator*=
bv_arithmetict & operator*=(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:102
bv_arithmetict::operator>
bool operator>(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:152
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
bv_arithmetict::spec
bv_spect spec
Definition: bv_arithmetic.h:53