cprover
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 "arith_tools.h"
16 #include "bv_arithmetic.h"
17 #include "namespace.h"
18 #include "pointer_offset_size.h"
19 #include "std_expr.h"
20 #include "string2int.h"
21 
22 void array_typet::check(const typet &type, const validation_modet vm)
23 {
24  PRECONDITION(type.id() == ID_array);
25  const array_typet &array_type = static_cast<const array_typet &>(type);
26  if(array_type.size().is_nil())
27  {
28  DATA_CHECK(
29  vm,
30  array_type.size() == nil_exprt{},
31  "nil array size must be exactly nil");
32  }
33 }
34 
37  const irep_idt &component_name) const
38 {
39  std::size_t number=0;
40 
41  for(const auto &c : components())
42  {
43  if(c.get_name() == component_name)
44  return number;
45 
46  number++;
47  }
48 
50 }
51 
54  const irep_idt &component_name) const
55 {
56  for(const auto &c : components())
57  {
58  if(c.get_name() == component_name)
59  return c;
60  }
61 
62  return static_cast<const componentt &>(get_nil_irep());
63 }
64 
65 const typet &
66 struct_union_typet::component_type(const irep_idt &component_name) const
67 {
68  const auto &c = get_component(component_name);
69  CHECK_RETURN(c.is_not_nil());
70  return c.type();
71 }
72 
74 {
76 }
77 
79 {
81 }
82 
84  : exprt(ID_base, std::move(base))
85 {
86 }
87 
89 {
90  bases().push_back(baset(base));
91 }
92 
94 {
95  for(const auto &b : bases())
96  {
97  if(to_struct_tag_type(b.type()).get_identifier() == id)
98  return b;
99  }
100  return {};
101 }
102 
107 bool struct_typet::is_prefix_of(const struct_typet &other) const
108 {
109  const componentst &ot_components=other.components();
110  const componentst &tt_components=components();
111 
112  if(ot_components.size()<
113  tt_components.size())
114  return false;
115 
116  componentst::const_iterator
117  ot_it=ot_components.begin();
118 
119  for(const auto &tt_c : tt_components)
120  {
121  if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name())
122  {
123  return false; // they just don't match
124  }
125 
126  ot_it++;
127  }
128 
129  return true; // ok, *this is a prefix of ot
130 }
131 
133 bool is_reference(const typet &type)
134 {
135  return type.id()==ID_pointer &&
136  type.get_bool(ID_C_reference);
137 }
138 
140 bool is_rvalue_reference(const typet &type)
141 {
142  return type.id()==ID_pointer &&
143  type.get_bool(ID_C_rvalue_reference);
144 }
145 
147 {
148  set(ID_from, integer2string(from));
149 }
150 
152 {
153  set(ID_to, integer2string(to));
154 }
155 
157 {
158  return string2integer(get_string(ID_from));
159 }
160 
162 {
163  return string2integer(get_string(ID_to));
164 }
165 
176  const typet &type,
177  const namespacet &ns)
178 {
179  // Helper function to avoid the code duplication in the branches
180  // below.
181  const auto has_constant_components = [&ns](const typet &subtype) -> bool {
182  if(subtype.id() == ID_struct || subtype.id() == ID_union)
183  {
184  const auto &struct_union_type = to_struct_union_type(subtype);
185  for(const auto &component : struct_union_type.components())
186  {
188  return true;
189  }
190  }
191  return false;
192  };
193 
194  // There are 4 possibilities the code below is handling.
195  // The possibilities are enumerated as comments, to show
196  // what each code is supposed to be handling. For more
197  // comprehensive test case for this, take a look at
198  // regression/cbmc/no_nondet_static/main.c
199 
200  // const int a;
201  if(type.get_bool(ID_C_constant))
202  return true;
203 
204  // This is a termination condition to break the recursion
205  // for recursive types such as the following:
206  // struct list { const int datum; struct list * next; };
207  // NOTE: the difference between this condition and the previous
208  // one is that this one always returns.
209  if(type.id() == ID_pointer)
210  return type.get_bool(ID_C_constant);
211 
212  // When we have a case like the following, we don't immediately
213  // see the struct t. Instead, we only get to see symbol t1, which
214  // we have to use the namespace to resolve to its definition:
215  // struct t { const int a; };
216  // struct t t1;
217  if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
218  {
219  const auto &resolved_type = ns.follow(type);
220  return has_constant_components(resolved_type);
221  }
222 
223  // In a case like this, where we see an array (b[3] here), we know that
224  // the array contains subtypes. We get the first one, and
225  // then resolve it to its definition through the usage of the namespace.
226  // struct contains_constant_pointer { int x; int * const p; };
227  // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
228  if(type.has_subtype())
229  {
230  const auto &subtype = to_type_with_subtype(type).subtype();
232  }
233 
234  return false;
235 }
236 
237 vector_typet::vector_typet(const typet &_subtype, const constant_exprt &_size)
238  : type_with_subtypet(ID_vector, _subtype)
239 {
240  size() = _size;
241 }
242 
244 {
245  return static_cast<const constant_exprt &>(find(ID_size));
246 }
247 
249 {
250  return static_cast<constant_exprt &>(add(ID_size));
251 }
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:404
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
array_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.cpp:22
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
struct_typet::get_base
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
Definition: std_types.cpp:93
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:208
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
typet::has_subtype
bool has_subtype() const
Definition: type.h:65
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:122
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
struct_typet::add_base
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:88
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
struct_typet::is_prefix_of
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:107
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:154
struct_union_typet::component_type
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:66
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
bv_arithmetic.h
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:443
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
type_with_subtypet
Type with a single subtype.
Definition: type.h:146
namespace.h
struct_union_typet::component_number
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:36
array_typet::size
const exprt & size() const
Definition: std_types.h:765
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
range_typet::get_from
mp_integer get_from() const
Definition: std_types.cpp:156
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
std_types.h
Pre-defined types.
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:256
range_typet::get_to
mp_integer get_to() const
Definition: std_types.cpp:161
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:468
irept::baset
tree_implementationt baset
Definition: irep.h:385
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:243
struct_typet::baset::type
struct_tag_typet & type()
Definition: std_types.cpp:73
struct_union_typet::componentt
Definition: std_types.h:63
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
vector_typet::vector_typet
vector_typet(const typet &_subtype, const constant_exprt &_size)
Definition: std_types.cpp:237
range_typet::set_to
void set_to(const mp_integer &to)
Definition: std_types.cpp:151
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
array_typet
Arrays with given size.
Definition: std_types.h:757
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:133
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
is_constant_or_has_constant_components
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:175
is_rvalue_reference
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:140
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
std_expr.h
API to expression classes.
range_typet::set_from
void set_from(const mp_integer &_from)
Definition: std_types.cpp:146
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106