cprover
bv_arithmetic.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_BV_ARITHMETIC_H
11 #define CPROVER_UTIL_BV_ARITHMETIC_H
12 
13 #include <iosfwd>
14 
15 #include "mp_arith.h"
16 #include "format_spec.h"
17 
18 class constant_exprt;
19 class exprt;
20 class typet;
21 
22 class bv_spect
23 {
24 public:
25  std::size_t width;
26  bool is_signed;
27 
28  explicit bv_spect(const typet &type)
29  {
30  from_type(type);
31  }
32 
33  void from_type(const typet &type);
34 
35  bv_spect():width(0), is_signed(false)
36  {
37  }
38 
39  mp_integer max_value() const;
40  mp_integer min_value() const;
41 
42  typet to_type() const;
43 
44  bool operator==(const bv_spect &other) const
45  {
46  return width==other.width && is_signed==other.is_signed;
47  }
48 };
49 
51 {
52 public:
54 
55  explicit bv_arithmetict(const bv_spect &_spec):
56  spec(_spec), value(0)
57  {
58  }
59 
61  {
62  }
63 
64  explicit bv_arithmetict(const constant_exprt &expr)
65  {
66  from_expr(expr);
67  }
68 
69  void negate();
70 
71  void make_zero()
72  {
73  value=0;
74  }
75 
76  bool is_zero() const { return value==0; }
77 
78  // performs conversion to bit-vector format
79  void from_integer(const mp_integer &i);
80 
81  // performs conversion from ieee floating point format
82  void change_spec(const bv_spect &dest_spec);
83  mp_integer to_integer() const { return value; }
84 
85  void print(std::ostream &out) const;
86 
87  std::string to_ansi_c_string() const
88  {
89  return format(format_spect());
90  }
91 
92  std::string format(const format_spect &format_spec) const;
93 
94  // expressions
95  constant_exprt to_expr() const;
96  void from_expr(const constant_exprt &expr);
97 
103 
104  bool operator<(const bv_arithmetict &other);
105  bool operator<=(const bv_arithmetict &other);
106  bool operator>(const bv_arithmetict &other);
107  bool operator>=(const bv_arithmetict &other);
108  bool operator==(const bv_arithmetict &other);
109  bool operator!=(const bv_arithmetict &other);
110  bool operator==(int i);
111 
112  std::ostream &operator<<(std::ostream &out)
113  {
114  return out << to_ansi_c_string();
115  }
116 
117  // turn into natural number representation
118  void unpack(const mp_integer &i) { value=i; adjust(); }
119  mp_integer pack() const;
120 
121 protected:
122  // we store negative numbers as such
124 
125  // puts the value back into its range
126  void adjust();
127 };
128 
129 #endif // CPROVER_UTIL_BV_ARITHMETIC_H
bv_arithmetict::operator-=
bv_arithmetict & operator-=(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:122
bv_arithmetict::bv_arithmetict
bv_arithmetict(const bv_spect &_spec)
Definition: bv_arithmetic.h:55
bv_arithmetict::format
std::string format(const format_spect &format_spec) const
Definition: bv_arithmetic.cpp:54
mp_arith.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_arithmetict::to_integer
mp_integer to_integer() const
Definition: bv_arithmetic.h:83
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
bv_arithmetict::is_zero
bool is_zero() const
Definition: bv_arithmetic.h:76
bv_arithmetict::unpack
void unpack(const mp_integer &i)
Definition: bv_arithmetic.h:118
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
bv_spect::bv_spect
bv_spect(const typet &type)
Definition: bv_arithmetic.h:28
bv_arithmetict::operator!=
bool operator!=(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:172
exprt
Base class for all expressions.
Definition: expr.h:53
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
bv_arithmetict::operator==
bool operator==(const bv_arithmetict &other)
Definition: bv_arithmetic.cpp:162
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_arithmetict::make_zero
void make_zero()
Definition: bv_arithmetic.h:71
bv_spect::from_type
void from_type(const typet &type)
Definition: bv_arithmetic.cpp:37
bv_spect::operator==
bool operator==(const bv_spect &other) const
Definition: bv_arithmetic.h:44
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
bv_arithmetict::bv_arithmetict
bv_arithmetict(const constant_exprt &expr)
Definition: bv_arithmetic.h:64
bv_arithmetict::bv_arithmetict
bv_arithmetict()
Definition: bv_arithmetic.h:60
format_spec.h
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
bv_arithmetict::adjust
void adjust()
Definition: bv_arithmetic.cpp:69
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::operator<<
std::ostream & operator<<(std::ostream &out)
Definition: bv_arithmetic.h:112
bv_arithmetict::to_ansi_c_string
std::string to_ansi_c_string() const
Definition: bv_arithmetic.h:87
bv_spect::bv_spect
bv_spect()
Definition: bv_arithmetic.h:35
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
bv_arithmetict::negate
void negate()
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
bv_arithmetict
Definition: bv_arithmetic.h:51
bv_spect::max_value
mp_integer max_value() const
Definition: bv_arithmetic.cpp:25
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
bv_arithmetict::spec
bv_spect spec
Definition: bv_arithmetic.h:53