-
Notifications
You must be signed in to change notification settings - Fork 300
Expand file tree
/
Copy pathfixedbv.cpp
More file actions
175 lines (135 loc) · 3.44 KB
/
Copy pathfixedbv.cpp
File metadata and controls
175 lines (135 loc) · 3.44 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
/*******************************************************************\
Module:
Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
#include "fixedbv.h"
#include "arith_tools.h"
#include "bitvector_types.h"
#include "std_expr.h"
fixedbv_spect::fixedbv_spect(const fixedbv_typet &type)
{
integer_bits=type.get_integer_bits();
width=type.get_width();
}
fixedbvt::fixedbvt(const constant_exprt &expr)
{
from_expr(expr);
}
void fixedbvt::from_expr(const constant_exprt &expr)
{
spec=fixedbv_spect(to_fixedbv_type(expr.type()));
v = bvrep2integer(expr.get_value(), spec.width, true);
}
void fixedbvt::from_integer(const mp_integer &i)
{
v=i*power(2, spec.get_fraction_bits());
}
mp_integer fixedbvt::to_integer() const
{
// this rounds to zero, i.e., we just divide
return v/power(2, spec.get_fraction_bits());
}
constant_exprt fixedbvt::to_expr() const
{
fixedbv_typet type;
type.set_width(spec.width);
type.set_integer_bits(spec.integer_bits);
PRECONDITION(spec.width != 0);
return constant_exprt(integer2bvrep(v, spec.width), type);
}
void fixedbvt::round(const fixedbv_spect &dest_spec)
{
std::size_t old_fraction_bits=spec.width-spec.integer_bits;
std::size_t new_fraction_bits=dest_spec.width-dest_spec.integer_bits;
mp_integer result;
if(new_fraction_bits>old_fraction_bits)
result=v*power(2, new_fraction_bits-old_fraction_bits);
else if(new_fraction_bits<old_fraction_bits)
{
// may need to round
mp_integer p=power(2, old_fraction_bits-new_fraction_bits);
mp_integer div=v/p;
mp_integer rem=v%p;
if(rem<0)
rem=-rem;
if(rem*2>=p)
{
if(v<0)
--div;
else
++div;
}
result=div;
}
else // new_faction_bits==old_fraction_vits
{
// no change!
result=v;
}
v=result;
spec=dest_spec;
}
void fixedbvt::negate()
{
v=-v;
}
fixedbvt &fixedbvt::operator*=(const fixedbvt &o)
{
v*=o.v;
fixedbv_spect old_spec=spec;
spec.width+=o.spec.width;
spec.integer_bits+=o.spec.integer_bits;
round(old_spec);
return *this;
}
fixedbvt &fixedbvt::operator+=(const fixedbvt &o)
{
v += o.v;
return *this;
}
fixedbvt &fixedbvt::operator-=(const fixedbvt &o)
{
v -= o.v;
return *this;
}
fixedbvt &fixedbvt::operator/=(const fixedbvt &o)
{
v*=power(2, o.spec.get_fraction_bits());
v/=o.v;
return *this;
}
bool fixedbvt::operator==(int i) const
{
return v==power(2, spec.get_fraction_bits())*i;
}
std::string fixedbvt::format(
const format_spect &format_spec) const
{
std::string dest;
std::size_t fraction_bits=spec.get_fraction_bits();
mp_integer int_value=v;
mp_integer factor=power(2, fraction_bits);
if(int_value.is_negative())
{
dest+='-';
int_value.negate();
}
std::string base_10_string=
integer2string(int_value*power(10, fraction_bits)/factor);
while(base_10_string.size()<=fraction_bits)
base_10_string="0"+base_10_string;
std::string integer_part=
std::string(base_10_string, 0, base_10_string.size()-fraction_bits);
std::string fraction_part=
std::string(base_10_string, base_10_string.size()-fraction_bits);
dest+=integer_part;
// strip trailing zeros
while(!fraction_part.empty() &&
fraction_part[fraction_part.size()-1]=='0')
fraction_part.resize(fraction_part.size()-1);
if(!fraction_part.empty())
dest+="."+fraction_part;
while(dest.size()<format_spec.min_width)
dest=" "+dest;
return dest;
}