CBMC
fixedbv.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 "fixedbv.h"
10 
11 #include "arith_tools.h"
12 #include "bitvector_types.h"
13 #include "std_expr.h"
14 
16 {
18  width=type.get_width();
19 }
20 
22 {
23  from_expr(expr);
24 }
25 
27 {
29  v = bvrep2integer(expr.get_value(), spec.width, true);
30 }
31 
33 {
34  v=i*power(2, spec.get_fraction_bits());
35 }
36 
38 {
39  // this rounds to zero, i.e., we just divide
40  return v/power(2, spec.get_fraction_bits());
41 }
42 
44 {
45  fixedbv_typet type;
46  type.set_width(spec.width);
48  PRECONDITION(spec.width != 0);
49  return constant_exprt(integer2bvrep(v, spec.width), type);
50 }
51 
52 void fixedbvt::round(const fixedbv_spect &dest_spec)
53 {
54  std::size_t old_fraction_bits=spec.width-spec.integer_bits;
55  std::size_t new_fraction_bits=dest_spec.width-dest_spec.integer_bits;
56 
57  mp_integer result;
58 
59  if(new_fraction_bits>old_fraction_bits)
60  result=v*power(2, new_fraction_bits-old_fraction_bits);
61  else if(new_fraction_bits<old_fraction_bits)
62  {
63  // may need to round
64  mp_integer p=power(2, old_fraction_bits-new_fraction_bits);
65  mp_integer div=v/p;
66  mp_integer rem=v%p;
67  if(rem<0)
68  rem=-rem;
69 
70  if(rem*2>=p)
71  {
72  if(v<0)
73  --div;
74  else
75  ++div;
76  }
77 
78  result=div;
79  }
80  else // new_faction_bits==old_fraction_vits
81  {
82  // no change!
83  result=v;
84  }
85 
86  v=result;
87  spec=dest_spec;
88 }
89 
91 {
92  v=-v;
93 }
94 
96 {
97  v*=o.v;
98 
99  fixedbv_spect old_spec=spec;
100 
101  spec.width+=o.spec.width;
103 
104  round(old_spec);
105 
106  return *this;
107 }
108 
110 {
111  v += o.v;
112  return *this;
113 }
114 
116 {
117  v -= o.v;
118  return *this;
119 }
120 
122 {
123  v*=power(2, o.spec.get_fraction_bits());
124  v/=o.v;
125 
126  return *this;
127 }
128 
129 bool fixedbvt::operator==(int i) const
130 {
131  return v==power(2, spec.get_fraction_bits())*i;
132 }
133 
134 std::string fixedbvt::format(
135  const format_spect &format_spec) const
136 {
137  std::string dest;
138  std::size_t fraction_bits=spec.get_fraction_bits();
139 
140  mp_integer int_value=v;
141  mp_integer factor=power(2, fraction_bits);
142 
143  if(int_value.is_negative())
144  {
145  dest+='-';
146  int_value.negate();
147  }
148 
149  std::string base_10_string=
150  integer2string(int_value*power(10, fraction_bits)/factor);
151 
152  while(base_10_string.size()<=fraction_bits)
153  base_10_string="0"+base_10_string;
154 
155  std::string integer_part=
156  std::string(base_10_string, 0, base_10_string.size()-fraction_bits);
157 
158  std::string fraction_part=
159  std::string(base_10_string, base_10_string.size()-fraction_bits);
160 
161  dest+=integer_part;
162 
163  // strip trailing zeros
164  while(!fraction_part.empty() &&
165  fraction_part[fraction_part.size()-1]=='0')
166  fraction_part.resize(fraction_part.size()-1);
167 
168  if(!fraction_part.empty())
169  dest+="."+fraction_part;
170 
171  while(dest.size()<format_spec.min_width)
172  dest=" "+dest;
173 
174  return dest;
175 }
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
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...
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Pre-defined bitvector types.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
void set_width(std::size_t width)
Definition: std_types.h:932
std::size_t get_width() const
Definition: std_types.h:925
A constant literal expression.
Definition: std_expr.h:2990
const irep_idt & get_value() const
Definition: std_expr.h:2998
typet & type()
Return the type of the expression.
Definition: expr.h:84
std::size_t integer_bits
Definition: fixedbv.h:22
std::size_t width
Definition: fixedbv.h:22
fixedbv_spect()
Definition: fixedbv.h:24
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
Fixed-width bit-vector with signed fixed-point interpretation.
void set_integer_bits(std::size_t b)
std::size_t get_integer_bits() const
fixedbv_spect spec
Definition: fixedbv.h:44
fixedbvt()
Definition: fixedbv.h:46
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
void from_expr(const constant_exprt &expr)
Definition: fixedbv.cpp:26
void negate()
Definition: fixedbv.cpp:90
bool operator==(int i) const
Definition: fixedbv.cpp:129
fixedbvt & operator+=(const fixedbvt &other)
Definition: fixedbv.cpp:109
mp_integer to_integer() const
Definition: fixedbv.cpp:37
fixedbvt & operator*=(const fixedbvt &other)
Definition: fixedbv.cpp:95
void round(const fixedbv_spect &dest_spec)
Definition: fixedbv.cpp:52
std::string format(const format_spect &format_spec) const
Definition: fixedbv.cpp:134
fixedbvt & operator/=(const fixedbvt &other)
Definition: fixedbv.cpp:121
fixedbvt & operator-=(const fixedbvt &other)
Definition: fixedbv.cpp:115
mp_integer v
Definition: fixedbv.h:100
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
unsigned min_width
Definition: format_spec.h:18
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
BigInt mp_integer
Definition: smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.