cprover
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 // we may wish to make the index type part of the array type
36 return c_index_type();
37}
38
41 const irep_idt &component_name) const
42{
43 std::size_t number=0;
44
45 for(const auto &c : components())
46 {
47 if(c.get_name() == component_name)
48 return number;
49
50 number++;
51 }
52
54}
55
58 const irep_idt &component_name) const
59{
60 for(const auto &c : components())
61 {
62 if(c.get_name() == component_name)
63 return c;
64 }
65
66 return static_cast<const componentt &>(get_nil_irep());
67}
68
69const typet &
70struct_union_typet::component_type(const irep_idt &component_name) const
71{
72 const auto &c = get_component(component_name);
73 CHECK_RETURN(c.is_not_nil());
74 return c.type();
75}
76
78{
80}
81
83{
85}
86
88 : exprt(ID_base, std::move(base))
89{
90}
91
93{
94 bases().push_back(baset(base));
95}
96
98{
99 for(const auto &b : bases())
100 {
101 if(to_struct_tag_type(b.type()).get_identifier() == id)
102 return b;
103 }
104 return {};
105}
106
112{
113 const componentst &ot_components=other.components();
114 const componentst &tt_components=components();
115
116 if(ot_components.size()<
117 tt_components.size())
118 return false;
119
120 componentst::const_iterator
121 ot_it=ot_components.begin();
122
123 for(const auto &tt_c : tt_components)
124 {
125 if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name())
126 {
127 return false; // they just don't match
128 }
129
130 ot_it++;
131 }
132
133 return true; // ok, *this is a prefix of ot
134}
135
137bool is_reference(const typet &type)
138{
139 return type.id()==ID_pointer &&
140 type.get_bool(ID_C_reference);
141}
142
144bool is_rvalue_reference(const typet &type)
145{
146 return type.id()==ID_pointer &&
147 type.get_bool(ID_C_rvalue_reference);
148}
149
151{
152 set(ID_from, integer2string(from));
153}
154
156{
157 set(ID_to, integer2string(to));
158}
159
161{
162 return string2integer(get_string(ID_from));
163}
164
166{
167 return string2integer(get_string(ID_to));
168}
169
180 const typet &type,
181 const namespacet &ns)
182{
183 // Helper function to avoid the code duplication in the branches
184 // below.
185 const auto has_constant_components = [&ns](const typet &subtype) -> bool {
186 if(subtype.id() == ID_struct || subtype.id() == ID_union)
187 {
188 const auto &struct_union_type = to_struct_union_type(subtype);
189 for(const auto &component : struct_union_type.components())
190 {
192 return true;
193 }
194 }
195 return false;
196 };
197
198 // There are 4 possibilities the code below is handling.
199 // The possibilities are enumerated as comments, to show
200 // what each code is supposed to be handling. For more
201 // comprehensive test case for this, take a look at
202 // regression/cbmc/no_nondet_static/main.c
203
204 // const int a;
205 if(type.get_bool(ID_C_constant))
206 return true;
207
208 // This is a termination condition to break the recursion
209 // for recursive types such as the following:
210 // struct list { const int datum; struct list * next; };
211 // NOTE: the difference between this condition and the previous
212 // one is that this one always returns.
213 if(type.id() == ID_pointer)
214 return type.get_bool(ID_C_constant);
215
216 // When we have a case like the following, we don't immediately
217 // see the struct t. Instead, we only get to see symbol t1, which
218 // we have to use the namespace to resolve to its definition:
219 // struct t { const int a; };
220 // struct t t1;
221 if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
222 {
223 const auto &resolved_type = ns.follow(type);
224 return has_constant_components(resolved_type);
225 }
226
227 // In a case like this, where we see an array (b[3] here), we know that
228 // the array contains subtypes. We get the first one, and
229 // then resolve it to its definition through the usage of the namespace.
230 // struct contains_constant_pointer { int x; int * const p; };
231 // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
232 if(type.has_subtype())
233 {
234 const auto &subtype = to_type_with_subtype(type).subtype();
236 }
237
238 return false;
239}
240
241vector_typet::vector_typet(const typet &_subtype, const constant_exprt &_size)
242 : type_with_subtypet(ID_vector, _subtype)
243{
244 size() = _size;
245}
246
248{
249 // we may wish to make the index type part of the vector type
250 return c_index_type();
251}
252
254{
255 return static_cast<const constant_exprt &>(find(ID_size));
256}
257
259{
260 return static_cast<constant_exprt &>(add(ID_size));
261}
bitvector_typet c_index_type()
Definition: c_types.cpp:16
Arrays with given size.
Definition: std_types.h:763
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:790
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
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
tree_implementationt baset
Definition: irep.h:374
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool is_nil() const
Definition: irep.h:376
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:409
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
void set_to(const mp_integer &to)
Definition: std_types.cpp:155
void set_from(const mp_integer &_from)
Definition: std_types.cpp:150
mp_integer get_to() const
Definition: std_types.cpp:165
mp_integer get_from() const
Definition: std_types.cpp:160
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
struct_tag_typet & type()
Definition: std_types.cpp:77
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
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...
Definition: std_types.cpp:111
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:92
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
Definition: std_types.cpp:97
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:70
const componentst & components() const
Definition: std_types.h:147
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:57
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:40
std::vector< componentt > componentst
Definition: std_types.h:140
const irep_idt & get_identifier() const
Definition: std_types.h:410
Type with a single subtype.
Definition: type.h:149
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:168
const typet & subtype() const
Definition: type.h:156
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
bool has_subtype() const
Definition: type.h:66
vector_typet(const typet &_subtype, const constant_exprt &_size)
Definition: std_types.cpp:241
const constant_exprt & size() const
Definition: std_types.cpp:253
typet index_type() const
The type of any index expression into an instance of this type.
Definition: std_types.cpp:247
const irept & get_nil_irep()
Definition: irep.cpp:20
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.
nonstd::optional< T > optionalt
Definition: optional.h:35
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#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:48
API to expression classes.
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.
Definition: std_types.cpp:179
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:137
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:144
Pre-defined types.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
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:177
#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