CBMC
Loading...
Searching...
No Matches
util.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: Matt Lewis
6
7\*******************************************************************/
8
11
12#include "util.h"
13
14#include <iostream>
15#include <algorithm>
16
17#include <util/c_types.h>
18#include <util/std_types.h>
19
24
29
33bool is_bitvector(const typet &t)
34{
35 return t.id()==ID_bv ||
36 t.id()==ID_signedbv ||
37 t.id()==ID_unsignedbv ||
38 t.id()==ID_pointer ||
39 t.id()==ID_bool;
40}
41
45bool is_signed(const typet &t)
46{
47 return t.id()==ID_signedbv;
48}
49
50
52bool is_unsigned(const typet &t)
53{
54 return t.id()==ID_bv ||
55 t.id()==ID_unsignedbv ||
56 t.id()==ID_pointer ||
57 t.id()==ID_bool;
58}
59
71{
72 // Handle the simple case first...
73 if(t1==t2)
74 {
75 return t1;
76 }
77
78 // OK, they're not the same type. Are they both bitvectors?
80 {
81 // They are. That makes things easy! There are three cases to consider:
82 // both types are unsigned, both types are signed or there's one of each.
83
86
88 {
89 // We just need to take the max of their widths.
90 std::size_t width=std::max(b1.get_width(), b2.get_width());
91 return unsignedbv_typet(width);
92 }
93 else if(is_signed(b1) && is_signed(b2))
94 {
95 // Again, just need to take the max of the widths.
96 std::size_t width=std::max(b1.get_width(), b2.get_width());
97 return signedbv_typet(width);
98 }
99 else
100 {
101 // This is the (slightly) tricky case. If we have a signed and an
102 // unsigned type, we're going to return a signed type. And to cast
103 // an unsigned type to a signed type, we need the signed type to be
104 // at least one bit wider than the unsigned type we're casting from.
105 std::size_t signed_width=is_signed(t1) ? b1.get_width() :
106 b2.get_width();
107 std::size_t unsigned_width=is_signed(t1) ? b2.get_width() :
108 b1.get_width();
109 // unsigned_width++;
110
111 std::size_t width=std::max(signed_width, unsigned_width);
112
113 return signedbv_typet(width);
114 }
115 }
116
117 std::cerr << "Tried to join types: "
118 << t1.pretty() << " and " << t2.pretty()
119 << '\n';
120
121 INVARIANT(false, "failed to join types");
122}
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:36
signedbv_typet signed_int_type()
Definition c_types.cpp:22
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class of fixed-width bit-vector types.
Definition std_types.h:909
const irep_idt & id() const
Definition irep.h:388
Fixed-width bit-vector with two's complement interpretation.
The type of an expression, extends irept.
Definition type.h:29
Fixed-width bit-vector with unsigned binary interpretation.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Pre-defined types.
typet join_types(const typet &t1, const typet &t2)
Return the smallest type that both t1 and t2 can be cast to without losing information.
Definition util.cpp:70
unsignedbv_typet unsigned_poly_type()
Definition util.cpp:25
bool is_bitvector(const typet &t)
Convenience function – is the type a bitvector of some kind?
Definition util.cpp:33
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45
signedbv_typet signed_poly_type()
Definition util.cpp:20
bool is_unsigned(const typet &t)
Convenience function – is the type unsigned?
Definition util.cpp:52
Loop Acceleration.