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 {
53 set_width(width);
54 }
55
56 static void check(
57 const typet &type,
58 const validation_modet vm = validation_modet::INVARIANT)
59 {
61 vm, !type.get(ID_width).empty(), "bitvector type must have width");
62 }
63};
64
68template <>
69inline bool can_cast_type<bv_typet>(const typet &type)
70{
71 return type.id() == ID_bv;
72}
73
82inline 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
91{
93 bv_typet::check(type);
94 return static_cast<bv_typet &>(type);
95}
96
99{
100public:
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
122};
123
127template <>
129{
130 return type.id() == ID_signedbv || type.id() == ID_unsignedbv;
131}
132
141inline 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{
160public:
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,
168 const validation_modet vm = validation_modet::INVARIANT)
169 {
170 bitvector_typet::check(type, vm);
171 }
172};
173
177template <>
179{
180 return type.id() == ID_unsignedbv;
181}
182
191inline 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{
209public:
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,
217 const validation_modet vm = validation_modet::INVARIANT)
218 {
220 vm, !type.get(ID_width).empty(), "signed bitvector type must have width");
221 }
222};
223
227template <>
228inline bool can_cast_type<signedbv_typet>(const typet &type)
229{
230 return type.id() == ID_signedbv;
231}
232
241inline const signedbv_typet &to_signedbv_type(const typet &type)
242{
245 return static_cast<const signedbv_typet &>(type);
246}
247
250{
253 return static_cast<signedbv_typet &>(type);
254}
255
261{
262public:
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,
281 const validation_modet vm = validation_modet::INVARIANT)
282 {
284 vm, !type.get(ID_width).empty(), "fixed bitvector type must have width");
285 }
286};
287
291template <>
292inline bool can_cast_type<fixedbv_typet>(const typet &type)
293{
294 return type.id() == ID_fixedbv;
295}
296
305inline const fixedbv_typet &to_fixedbv_type(const typet &type)
306{
309 return static_cast<const fixedbv_typet &>(type);
310}
311
314{
317 return static_cast<fixedbv_typet &>(type);
318}
319
322{
323public:
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,
343 const validation_modet vm = validation_modet::INVARIANT)
344 {
346 vm, !type.get(ID_width).empty(), "float bitvector type must have width");
347 }
348};
349
353template <>
354inline bool can_cast_type<floatbv_typet>(const typet &type)
355{
356 return type.id() == ID_floatbv;
357}
358
367inline const floatbv_typet &to_floatbv_type(const typet &type)
368{
371 return static_cast<const floatbv_typet &>(type);
372}
373
376{
379 return static_cast<floatbv_typet &>(type);
380}
381
382#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:853
void set_width(std::size_t width)
Definition: std_types.h:869
std::size_t get_width() const
Definition: std_types.h:864
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:874
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:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
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:45
void set_size_t(const irep_idt &name, const std::size_t value)
Definition: irep.cpp:87
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:12
#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:887
#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