CBMC
std_types.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pre-defined types
4 
5 Author: 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 
19 void 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  {
26  DATA_CHECK(
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 
75 const typet &
76 struct_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 
84 {
86 }
87 
89 {
91 }
92 
94  : exprt(ID_base, std::move(base))
95 {
96 }
97 
99 {
100  bases().push_back(baset(base));
101 }
102 
104 {
105  for(const auto &b : bases())
106  {
107  if(to_struct_tag_type(b.type()).get_identifier() == id)
108  return b;
109  }
110  return {};
111 }
112 
117 bool struct_typet::is_prefix_of(const struct_typet &other) const
118 {
119  const componentst &ot_components=other.components();
120  const componentst &tt_components=components();
121 
122  if(ot_components.size()<
123  tt_components.size())
124  return false;
125 
126  componentst::const_iterator
127  ot_it=ot_components.begin();
128 
129  for(const auto &tt_c : tt_components)
130  {
131  if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name())
132  {
133  return false; // they just don't match
134  }
135 
136  ot_it++;
137  }
138 
139  return true; // ok, *this is a prefix of ot
140 }
141 
143 bool is_reference(const typet &type)
144 {
145  return type.id()==ID_pointer &&
146  type.get_bool(ID_C_reference);
147 }
148 
150 bool is_rvalue_reference(const typet &type)
151 {
152  return type.id()==ID_pointer &&
153  type.get_bool(ID_C_rvalue_reference);
154 }
155 
157 {
158  set(ID_from, integer2string(from));
159 }
160 
162 {
163  set(ID_to, integer2string(to));
164 }
165 
167 {
168  return string2integer(get_string(ID_from));
169 }
170 
172 {
173  return string2integer(get_string(ID_to));
174 }
175 
186  const typet &type,
187  const namespacet &ns)
188 {
189  // Helper function to avoid the code duplication in the branches
190  // below.
191  const auto has_constant_components = [&ns](const typet &subtype) -> bool {
192  if(subtype.id() == ID_struct || subtype.id() == ID_union)
193  {
194  const auto &struct_union_type = to_struct_union_type(subtype);
195  for(const auto &component : struct_union_type.components())
196  {
198  return true;
199  }
200  }
201  return false;
202  };
203 
204  // There are 4 possibilities the code below is handling.
205  // The possibilities are enumerated as comments, to show
206  // what each code is supposed to be handling. For more
207  // comprehensive test case for this, take a look at
208  // regression/cbmc/no_nondet_static/main.c
209 
210  // const int a;
211  if(type.get_bool(ID_C_constant))
212  return true;
213 
214  // This is a termination condition to break the recursion
215  // for recursive types such as the following:
216  // struct list { const int datum; struct list * next; };
217  // NOTE: the difference between this condition and the previous
218  // one is that this one always returns.
219  if(type.id() == ID_pointer)
220  return type.get_bool(ID_C_constant);
221 
222  // When we have a case like the following, we don't immediately
223  // see the struct t. Instead, we only get to see symbol t1, which
224  // we have to use the namespace to resolve to its definition:
225  // struct t { const int a; };
226  // struct t t1;
227  if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
228  {
229  const auto &resolved_type = ns.follow(type);
230  return has_constant_components(resolved_type);
231  }
232 
233  // In a case like this, where we see an array (b[3] here), we know that
234  // the array contains subtypes. We get the first one, and
235  // then resolve it to its definition through the usage of the namespace.
236  // struct contains_constant_pointer { int x; int * const p; };
237  // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
238  if(type.has_subtype())
239  {
240  const auto &subtype = to_type_with_subtype(type).subtype();
242  }
243 
244  return false;
245 }
246 
248  typet _index_type,
249  typet _element_type,
250  constant_exprt _size)
251  : type_with_subtypet(ID_vector, std::move(_element_type))
252 {
253  index_type_nonconst() = std::move(_index_type);
254  size() = std::move(_size);
255 }
256 
258 {
259  // For backwards compatibility, allow the case that the array type is
260  // not annotated with an index type.
261  const auto &annotated_type =
262  static_cast<const typet &>(find(ID_C_index_type));
263  if(annotated_type.is_nil())
264  return c_index_type();
265  else
266  return annotated_type;
267 }
268 
270 {
271  return static_cast<const constant_exprt &>(find(ID_size));
272 }
273 
275 {
276  return static_cast<constant_exprt &>(add(ID_size));
277 }
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:800
A constant literal expression.
Definition: std_expr.h:2942
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:39
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:105
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
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:409
irept & add(const irep_idt &name)
Definition: irep.cpp:115
bool is_nil() const
Definition: irep.h:376
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:3026
void set_to(const mp_integer &to)
Definition: std_types.cpp:161
void set_from(const mp_integer &_from)
Definition: std_types.cpp:156
mp_integer get_to() const
Definition: std_types.cpp:171
mp_integer get_from() const
Definition: std_types.cpp:166
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
struct_tag_typet & type()
Definition: std_types.cpp:83
Structure type, corresponds to C style structs.
Definition: std_types.h:231
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:117
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:98
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:262
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
Definition: std_types.cpp:103
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:76
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:63
const componentst & components() const
Definition: std_types.h:147
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
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:165
const typet & subtype() const
Definition: type.h:172
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:184
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:50
bool has_subtype() const
Definition: type.h:82
vector_typet(typet index_type, typet element_type, constant_exprt size)
Definition: std_types.cpp:247
typet & index_type_nonconst()
The type of any index expression into an instance of this type.
Definition: std_types.h:1018
const constant_exprt & size() const
Definition: std_types.cpp:269
typet index_type() const
The type of any index expression into an instance of this type.
Definition: std_types.cpp:257
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
nonstd::optional< T > optionalt
Definition: optional.h:35
BigInt mp_integer
Definition: smt_terms.h:18
#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:77
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:185
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:143
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:150
Pre-defined types.
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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:193
#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