CBMC
bitvector_types.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pre-defined bitvector types
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_BITVECTOR_TYPES_H
13 #define CPROVER_UTIL_BITVECTOR_TYPES_H
14 
15 #include "std_types.h"
16 
19 inline bool is_signed_or_unsigned_bitvector(const typet &type)
20 {
21  return type.id() == ID_signedbv || type.id() == ID_unsignedbv;
22 }
23 
32 inline const bitvector_typet &to_bitvector_type(const typet &type)
33 {
35 
36  return static_cast<const bitvector_typet &>(type);
37 }
38 
41 {
43 
44  return static_cast<bitvector_typet &>(type);
45 }
46 
48 class bv_typet : public bitvector_typet
49 {
50 public:
51  explicit bv_typet(std::size_t width) : bitvector_typet(ID_bv)
52  {
53  set_width(width);
54  }
55 
56  static void check(
57  const typet &type,
59  {
60  DATA_CHECK(
61  vm, !type.get(ID_width).empty(), "bitvector type must have width");
62  }
63 };
64 
68 template <>
69 inline bool can_cast_type<bv_typet>(const typet &type)
70 {
71  return type.id() == ID_bv;
72 }
73 
82 inline const bv_typet &to_bv_type(const typet &type)
83 {
85  bv_typet::check(type);
86  return static_cast<const bv_typet &>(type);
87 }
88 
90 inline bv_typet &to_bv_type(typet &type)
91 {
93  bv_typet::check(type);
94  return static_cast<bv_typet &>(type);
95 }
96 
99 {
100 public:
101  integer_bitvector_typet(const irep_idt &id, std::size_t width)
102  : bitvector_typet(id, width)
103  {
104  }
105 
107  mp_integer smallest() const;
109  mp_integer largest() const;
110 
111  // If we ever need any of the following three methods in \ref fixedbv_typet or
112  // \ref floatbv_typet, we might want to move them to a new class
113  // numeric_bitvector_typet, which would be between integer_bitvector_typet and
114  // bitvector_typet in the hierarchy.
115 
119  constant_exprt zero_expr() const;
122 };
123 
127 template <>
129 {
130  return type.id() == ID_signedbv || type.id() == ID_unsignedbv;
131 }
132 
141 inline const integer_bitvector_typet &
143 {
145 
146  return static_cast<const integer_bitvector_typet &>(type);
147 }
148 
151 {
153 
154  return static_cast<integer_bitvector_typet &>(type);
155 }
156 
159 {
160 public:
161  explicit unsignedbv_typet(std::size_t width)
162  : integer_bitvector_typet(ID_unsignedbv, width)
163  {
164  }
165 
166  static void check(
167  const typet &type,
169  {
170  bitvector_typet::check(type, vm);
171  }
172 };
173 
177 template <>
178 inline bool can_cast_type<unsignedbv_typet>(const typet &type)
179 {
180  return type.id() == ID_unsignedbv;
181 }
182 
191 inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
192 {
195  return static_cast<const unsignedbv_typet &>(type);
196 }
197 
200 {
203  return static_cast<unsignedbv_typet &>(type);
204 }
205 
208 {
209 public:
210  explicit signedbv_typet(std::size_t width)
211  : integer_bitvector_typet(ID_signedbv, width)
212  {
213  }
214 
215  static void check(
216  const typet &type,
218  {
219  DATA_CHECK(
220  vm, !type.get(ID_width).empty(), "signed bitvector type must have width");
221  }
222 };
223 
227 template <>
228 inline bool can_cast_type<signedbv_typet>(const typet &type)
229 {
230  return type.id() == ID_signedbv;
231 }
232 
241 inline const signedbv_typet &to_signedbv_type(const typet &type)
242 {
244  signedbv_typet::check(type);
245  return static_cast<const signedbv_typet &>(type);
246 }
247 
250 {
252  signedbv_typet::check(type);
253  return static_cast<signedbv_typet &>(type);
254 }
255 
261 {
262 public:
264  {
265  }
266 
267  std::size_t get_fraction_bits() const
268  {
269  return get_width() - get_integer_bits();
270  }
271 
272  std::size_t get_integer_bits() const;
273 
274  void set_integer_bits(std::size_t b)
275  {
276  set_size_t(ID_integer_bits, b);
277  }
278 
279  static void check(
280  const typet &type,
282  {
283  DATA_CHECK(
284  vm, !type.get(ID_width).empty(), "fixed bitvector type must have width");
285  }
286 };
287 
291 template <>
292 inline bool can_cast_type<fixedbv_typet>(const typet &type)
293 {
294  return type.id() == ID_fixedbv;
295 }
296 
305 inline const fixedbv_typet &to_fixedbv_type(const typet &type)
306 {
308  fixedbv_typet::check(type);
309  return static_cast<const fixedbv_typet &>(type);
310 }
311 
314 {
316  fixedbv_typet::check(type);
317  return static_cast<fixedbv_typet &>(type);
318 }
319 
322 {
323 public:
325  {
326  }
327 
328  std::size_t get_e() const
329  {
330  // subtract one for sign bit
331  return get_width() - get_f() - 1;
332  }
333 
334  std::size_t get_f() const;
335 
336  void set_f(std::size_t b)
337  {
338  set_size_t(ID_f, b);
339  }
340 
341  static void check(
342  const typet &type,
344  {
345  DATA_CHECK(
346  vm, !type.get(ID_width).empty(), "float bitvector type must have width");
347  }
348 };
349 
353 template <>
354 inline bool can_cast_type<floatbv_typet>(const typet &type)
355 {
356  return type.id() == ID_floatbv;
357 }
358 
367 inline const floatbv_typet &to_floatbv_type(const typet &type)
368 {
370  floatbv_typet::check(type);
371  return static_cast<const floatbv_typet &>(type);
372 }
373 
376 {
378  floatbv_typet::check(type);
379  return static_cast<floatbv_typet &>(type);
380 }
381 
382 #endif // CPROVER_UTIL_BITVECTOR_TYPES_H
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
bool can_cast_type< integer_bitvector_typet >(const typet &type)
Check whether a reference to a typet is an integer_bitvector_typet.
bool can_cast_type< bv_typet >(const typet &type)
Check whether a reference to a typet is a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
bool can_cast_type< fixedbv_typet >(const typet &type)
Check whether a reference to a typet is a fixedbv_typet.
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_typet.
bool can_cast_type< floatbv_typet >(const typet &type)
Check whether a reference to a typet is a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Base class of fixed-width bit-vector types.
Definition: std_types.h:865
void set_width(std::size_t width)
Definition: std_types.h:881
std::size_t get_width() const
Definition: std_types.h:876
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:886
Fixed-width bit-vector without numerical interpretation.
bv_typet(std::size_t width)
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
A constant literal expression.
Definition: std_expr.h:2942
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:39
bool empty() const
Definition: dstring.h:90
Fixed-width bit-vector with signed fixed-point interpretation.
void set_integer_bits(std::size_t b)
std::size_t get_fraction_bits() const
std::size_t get_integer_bits() const
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Fixed-width bit-vector with IEEE floating-point interpretation.
void set_f(std::size_t b)
std::size_t get_f() const
std::size_t get_e() const
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Fixed-width bit-vector representing a signed or unsigned integer.
integer_bitvector_typet(const irep_idt &id, std::size_t width)
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
mp_integer largest() const
Return the largest value that can be represented using this type.
constant_exprt zero_expr() const
Return an expression representing the zero value of this type.
constant_exprt smallest_expr() const
Return an expression representing the smallest value of this type.
mp_integer smallest() const
Return the smallest value that can be represented using this type.
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void set_size_t(const irep_idt &name, const std::size_t value)
Definition: irep.cpp:86
const irep_idt & id() const
Definition: irep.h:396
Fixed-width bit-vector with two's complement interpretation.
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
signedbv_typet(std::size_t width)
The type of an expression, extends irept.
Definition: type.h:29
Fixed-width bit-vector with unsigned binary interpretation.
unsignedbv_typet(std::size_t width)
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
BigInt mp_integer
Definition: smt_terms.h:18
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Pre-defined types.
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:899
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
validation_modet