cprover
Loading...
Searching...
No Matches
std_types.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Pre-defined types
4
5Author: Daniel Kroening, kroening@kroening.com
6 Maria Svorenova, maria.svorenova@diffblue.com
7
8\*******************************************************************/
9
12
13#include "std_types.h"
14
15#include "c_types.h"
16#include "namespace.h"
17#include "std_expr.h"
18
19void array_typet::check(const typet &type, const validation_modet vm)
20{
21 PRECONDITION(type.id() == ID_array);
23 const array_typet &array_type = static_cast<const array_typet &>(type);
24 if(array_type.size().is_nil())
25 {
27 vm,
28 array_type.size() == nil_exprt{},
29 "nil array size must be exactly nil");
30 }
31}
32
34{
35 // For backwards compatibility, allow the case that the array type is
36 // not annotated with an index type.
37 const auto &annotated_type =
38 static_cast<const typet &>(find(ID_C_index_type));
39 if(annotated_type.is_nil())
40 return c_index_type();
41 else
42 return annotated_type;
43}
44
47 const irep_idt &component_name) const
48{
49 std::size_t number=0;
50
51 for(const auto &c : components())
52 {
53 if(c.get_name() == component_name)
54 return number;
55
56 number++;
57 }
58
60}
61
64 const irep_idt &component_name) const
65{
66 for(const auto &c : components())
67 {
68 if(c.get_name() == component_name)
69 return c;
70 }
71
72 return static_cast<const componentt &>(get_nil_irep());
73}
74
75const typet &
76struct_union_typet::component_type(const irep_idt &component_name) const
77{
78 const auto &c = get_component(component_name);
79 CHECK_RETURN(c.is_not_nil());
80 return c.type();
81}
82
87
92
94 : exprt(ID_base, std::move(base))
95{
96}
97
99{
100 bases().push_back(baset(base));
101}
102
103std::optional<struct_typet::baset>
105{
106 for(const auto &b : bases())
107 {
108 if(to_struct_tag_type(b.type()).get_identifier() == id)
109 return b;
110 }
111 return {};
112}
113
119{
120 const componentst &ot_components=other.components();
121 const componentst &tt_components=components();
122
123 if(ot_components.size()<
124 tt_components.size())
125 return false;
126
127 componentst::const_iterator
128 ot_it=ot_components.begin();
129
130 for(const auto &tt_c : tt_components)
131 {
132 if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name())
133 {
134 return false; // they just don't match
135 }
136
137 ot_it++;
138 }
139
140 return true; // ok, *this is a prefix of ot
141}
142
144bool is_reference(const typet &type)
145{
146 return type.id()==ID_pointer &&
147 type.get_bool(ID_C_reference);
148}
149
151bool is_rvalue_reference(const typet &type)
152{
153 return type.id()==ID_pointer &&
154 type.get_bool(ID_C_rvalue_reference);
155}
156
158{
159 set(ID_from, integer2string(from));
160}
161
163{
164 set(ID_to, integer2string(to));
165}
166
168{
169 return string2integer(get_string(ID_from));
170}
171
173{
174 return string2integer(get_string(ID_to));
175}
176
187 const typet &type,
188 const namespacet &ns)
189{
190 // Helper function to avoid the code duplication in the branches
191 // below.
192 const auto has_constant_components = [&ns](const typet &subtype) -> bool {
193 if(subtype.id() == ID_struct || subtype.id() == ID_union)
194 {
195 const auto &struct_union_type = to_struct_union_type(subtype);
196 for(const auto &component : struct_union_type.components())
197 {
199 return true;
200 }
201 }
202 return false;
203 };
204
205 // There are 4 possibilities the code below is handling.
206 // The possibilities are enumerated as comments, to show
207 // what each code is supposed to be handling. For more
208 // comprehensive test case for this, take a look at
209 // regression/cbmc/no_nondet_static/main.c
210
211 // const int a;
212 if(type.get_bool(ID_C_constant))
213 return true;
214
215 // This is a termination condition to break the recursion
216 // for recursive types such as the following:
217 // struct list { const int datum; struct list * next; };
218 // NOTE: the difference between this condition and the previous
219 // one is that this one always returns.
220 if(type.id() == ID_pointer)
221 return type.get_bool(ID_C_constant);
222
223 // When we have a case like the following, we don't immediately
224 // see the struct t. Instead, we only get to see symbol t1, which
225 // we have to use the namespace to resolve to its definition:
226 // struct t { const int a; };
227 // struct t t1;
228 if(type.id() == ID_struct_tag)
229 {
230 const auto &resolved_type = ns.follow_tag(to_struct_tag_type(type));
231 return has_constant_components(resolved_type);
232 }
233 else if(type.id() == ID_union_tag)
234 {
235 const auto &resolved_type = ns.follow_tag(to_union_tag_type(type));
236 return has_constant_components(resolved_type);
237 }
238
239 // In a case like this, where we see an array (b[3] here), we know that
240 // the array contains subtypes. We get the first one, and
241 // then resolve it to its definition through the usage of the namespace.
242 // struct contains_constant_pointer { int x; int * const p; };
243 // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
244 if(type.has_subtype())
245 {
246 const auto &subtype = to_type_with_subtype(type).subtype();
247 return is_constant_or_has_constant_components(subtype, ns);
248 }
249
250 return false;
251}
252
254 typet _index_type,
255 typet _element_type,
256 constant_exprt _size)
257 : type_with_subtypet(ID_vector, std::move(_element_type))
258{
259 index_type_nonconst() = std::move(_index_type);
260 size() = std::move(_size);
261}
262
264{
265 // For backwards compatibility, allow the case that the array type is
266 // not annotated with an index type.
267 const auto &annotated_type =
268 static_cast<const typet &>(find(ID_C_index_type));
269 if(annotated_type.is_nil())
270 return c_index_type();
271 else
272 return annotated_type;
273}
274
276{
277 return static_cast<const constant_exprt &>(find(ID_size));
278}
279
281{
282 return static_cast<constant_exprt &>(add(ID_size));
283}
bitvector_typet c_index_type()
Definition c_types.cpp:16
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
Arrays with given size.
Definition std_types.h:807
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition std_types.cpp:19
typet index_type() const
The type of the index expressions into any instance of this type.
Definition std_types.cpp:33
const exprt & size() const
Definition std_types.h:840
A constant literal expression.
Definition std_expr.h:2987
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
tree_implementationt baset
Definition irep.h:366
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
const irep_idt & id() const
Definition irep.h:388
irept & add(const irep_idt &name)
Definition irep.cpp:103
bool is_nil() const
Definition irep.h:368
const std::string & get_string(const irep_idt &name) const
Definition irep.h:401
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
The NIL expression.
Definition std_expr.h:3073
void set_to(const mp_integer &to)
void set_from(const mp_integer &_from)
mp_integer get_to() const
mp_integer get_from() const
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:493
baset(struct_tag_typet base)
Definition std_types.cpp:93
struct_tag_typet & type()
Definition std_types.cpp:83
Structure type, corresponds to C style structs.
Definition std_types.h:231
const basest & bases() const
Get the collection of base classes/structs.
Definition std_types.h:262
std::optional< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
bool is_prefix_of(const struct_typet &other) const
Returns true if the struct is a prefix of other, i.e., if this struct has n components then the compo...
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition std_types.cpp:98
const typet & component_type(const irep_idt &component_name) const
Definition std_types.cpp:76
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition std_types.cpp:63
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition std_types.cpp:46
const irep_idt & get_identifier() const
Definition std_types.h:410
Type with a single subtype.
Definition type.h:180
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition type.h:199
const typet & subtype() const
Definition type.h:187
The type of an expression, extends irept.
Definition type.h:29
bool has_subtype() const
Definition type.h:64
vector_typet(typet index_type, typet element_type, constant_exprt size)
const constant_exprt & size() const
typet & index_type_nonconst()
The type of any index expression into an instance of this type.
Definition std_types.h:1062
typet index_type() const
The type of any index expression into an instance of this type.
const irept & get_nil_irep()
Definition irep.cpp:19
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
STL namespace.
bool is_reference(const typet &type)
Returns true if the type is a reference.
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:80
API to expression classes.
Pre-defined types.
bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)
Identify whether a given type is constant itself or contains constant components.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208
#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