cprover
Loading...
Searching...
No Matches
bitvector_types.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Pre-defined bitvector types
4
5Author: 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
19inline bool is_signed_or_unsigned_bitvector(const typet &type)
20{
21 return type.id() == ID_signedbv || type.id() == ID_unsignedbv;
22}
23
32inline 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
49{
50public:
51 explicit bv_typet(std::size_t width) : bitvector_typet(ID_bv)
52 {
54 }
55
56 static void check(
57 const typet &type,
59 {
61 vm, !type.get(ID_width).empty(), "bitvector type must have width");
62 }
63
64 // helpers to create common constants
67};
68
72template <>
73inline bool can_cast_type<bv_typet>(const typet &type)
74{
75 return type.id() == ID_bv;
76}
77
86inline const bv_typet &to_bv_type(const typet &type)
87{
89 bv_typet::check(type);
90 return static_cast<const bv_typet &>(type);
91}
92
95{
97 bv_typet::check(type);
98 return static_cast<bv_typet &>(type);
99}
100
103{
104public:
105 integer_bitvector_typet(const irep_idt &id, std::size_t width)
107 {
108 }
109
111 mp_integer smallest() const;
113 mp_integer largest() const;
114
115 // If we ever need any of the following three methods in \ref fixedbv_typet or
116 // \ref floatbv_typet, we might want to move them to a new class
117 // numeric_bitvector_typet, which would be between integer_bitvector_typet and
118 // bitvector_typet in the hierarchy.
119
126};
127
131template <>
133{
134 return type.id() == ID_signedbv || type.id() == ID_unsignedbv;
135}
136
145inline const integer_bitvector_typet &
147{
149
150 return static_cast<const integer_bitvector_typet &>(type);
151}
152
160
163{
164public:
165 explicit unsignedbv_typet(std::size_t width)
166 : integer_bitvector_typet(ID_unsignedbv, width)
167 {
168 }
169
170 static void check(
171 const typet &type,
173 {
174 bitvector_typet::check(type, vm);
175 }
176};
177
181template <>
183{
184 return type.id() == ID_unsignedbv;
185}
186
195inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
196{
199 return static_cast<const unsignedbv_typet &>(type);
200}
201
204{
207 return static_cast<unsignedbv_typet &>(type);
208}
209
212{
213public:
214 explicit signedbv_typet(std::size_t width)
215 : integer_bitvector_typet(ID_signedbv, width)
216 {
217 }
218
219 static void check(
220 const typet &type,
222 {
224 vm, !type.get(ID_width).empty(), "signed bitvector type must have width");
225 }
226};
227
231template <>
232inline bool can_cast_type<signedbv_typet>(const typet &type)
233{
234 return type.id() == ID_signedbv;
235}
236
245inline const signedbv_typet &to_signedbv_type(const typet &type)
246{
249 return static_cast<const signedbv_typet &>(type);
250}
251
254{
257 return static_cast<signedbv_typet &>(type);
258}
259
265{
266public:
268 {
269 }
270
271 std::size_t get_fraction_bits() const
272 {
273 return get_width() - get_integer_bits();
274 }
275
276 std::size_t get_integer_bits() const;
277
278 void set_integer_bits(std::size_t b)
279 {
280 set_size_t(ID_integer_bits, b);
281 }
282
283 static void check(
284 const typet &type,
286 {
288 vm, !type.get(ID_width).empty(), "fixed bitvector type must have width");
289 }
290};
291
295template <>
296inline bool can_cast_type<fixedbv_typet>(const typet &type)
297{
298 return type.id() == ID_fixedbv;
299}
300
309inline const fixedbv_typet &to_fixedbv_type(const typet &type)
310{
313 return static_cast<const fixedbv_typet &>(type);
314}
315
318{
321 return static_cast<fixedbv_typet &>(type);
322}
323
326{
327public:
329 {
330 }
331
332 std::size_t get_e() const
333 {
334 // subtract one for sign bit
335 return get_width() - get_f() - 1;
336 }
337
338 std::size_t get_f() const;
339
340 void set_f(std::size_t b)
341 {
342 set_size_t(ID_f, b);
343 }
344
345 static void check(
346 const typet &type,
348 {
350 vm, !type.get(ID_width).empty(), "float bitvector type must have width");
351 }
352};
353
357template <>
358inline bool can_cast_type<floatbv_typet>(const typet &type)
359{
360 return type.id() == ID_floatbv;
361}
362
371inline const floatbv_typet &to_floatbv_type(const typet &type)
372{
375 return static_cast<const floatbv_typet &>(type);
376}
377
380{
383 return static_cast<floatbv_typet &>(type);
384}
385
386#endif // CPROVER_UTIL_BITVECTOR_TYPES_H
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_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 bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a 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 integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Base class of fixed-width bit-vector types.
Definition std_types.h:909
void set_width(std::size_t width)
Definition std_types.h:932
std::size_t get_width() const
Definition std_types.h:925
std::size_t width() const
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition std_types.h:939
bitvector_typet(const irep_idt &_id)
Definition std_types.h:911
Fixed-width bit-vector without numerical interpretation.
constant_exprt all_ones_expr() const
bv_typet(std::size_t width)
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
constant_exprt all_zeros_expr() const
A constant literal expression.
Definition std_expr.h:2995
bool empty() const
Definition dstring.h:89
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:82
const irep_idt & id() const
Definition irep.h:388
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
typet()
Definition type.h:31
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)
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
BigInt mp_integer
Definition smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Pre-defined types.
#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
dstringt irep_idt