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 
36 {
37  const irep_idt integer_bits=get(ID_integer_bits);
38  DATA_INVARIANT(!integer_bits.empty(), "integer bits should be set");
39  return unsafe_string2unsigned(id2string(integer_bits));
40 }
41 
42 std::size_t floatbv_typet::get_f() const
43 {
44  const irep_idt &f=get(ID_f);
45  DATA_INVARIANT(!f.empty(), "the mantissa should be set");
47 }
48 
51  const irep_idt &component_name) const
52 {
53  std::size_t number=0;
54 
55  for(const auto &c : components())
56  {
57  if(c.get_name() == component_name)
58  return number;
59 
60  number++;
61  }
62 
64 }
65 
68  const irep_idt &component_name) const
69 {
70  for(const auto &c : components())
71  {
72  if(c.get_name() == component_name)
73  return c;
74  }
75 
76  return static_cast<const componentt &>(get_nil_irep());
77 }
78 
79 const typet &
80 struct_union_typet::component_type(const irep_idt &component_name) const
81 {
82  const auto &c = get_component(component_name);
83  CHECK_RETURN(c.is_not_nil());
84  return c.type();
85 }
86 
88 {
90 }
91 
93 {
95 }
96 
98  : exprt(ID_base, std::move(base))
99 {
100 }
101 
103 {
104  bases().push_back(baset(base));
105 }
106 
108 {
109  for(const auto &b : bases())
110  {
111  if(to_struct_tag_type(b.type()).get_identifier() == id)
112  return b;
113  }
114  return {};
115 }
116 
121 bool struct_typet::is_prefix_of(const struct_typet &other) const
122 {
123  const componentst &ot_components=other.components();
124  const componentst &tt_components=components();
125 
126  if(ot_components.size()<
127  tt_components.size())
128  return false;
129 
130  componentst::const_iterator
131  ot_it=ot_components.begin();
132 
133  for(const auto &tt_c : tt_components)
134  {
135  if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name())
136  {
137  return false; // they just don't match
138  }
139 
140  ot_it++;
141  }
142 
143  return true; // ok, *this is a prefix of ot
144 }
145 
147 bool is_reference(const typet &type)
148 {
149  return type.id()==ID_pointer &&
150  type.get_bool(ID_C_reference);
151 }
152 
154 bool is_rvalue_reference(const typet &type)
155 {
156  return type.id()==ID_pointer &&
157  type.get_bool(ID_C_rvalue_reference);
158 }
159 
161 {
162  set(ID_from, integer2string(from));
163 }
164 
166 {
167  set(ID_to, integer2string(to));
168 }
169 
171 {
172  return string2integer(get_string(ID_from));
173 }
174 
176 {
177  return string2integer(get_string(ID_to));
178 }
179 
181 {
182  return bv_spect(*this).min_value();
183 }
184 
186 {
187  return bv_spect(*this).max_value();
188 }
189 
191 {
192  return from_integer(0, *this);
193 }
194 
196 {
197  return from_integer(smallest(), *this);
198 }
199 
201 {
202  return from_integer(largest(), *this);
203 }
204 
215  const typet &type,
216  const namespacet &ns)
217 {
218  // Helper function to avoid the code duplication in the branches
219  // below.
220  const auto has_constant_components = [&ns](const typet &subtype) -> bool {
221  if(subtype.id() == ID_struct || subtype.id() == ID_union)
222  {
223  const auto &struct_union_type = to_struct_union_type(subtype);
224  for(const auto &component : struct_union_type.components())
225  {
227  return true;
228  }
229  }
230  return false;
231  };
232 
233  // There are 4 possibilities the code below is handling.
234  // The possibilities are enumerated as comments, to show
235  // what each code is supposed to be handling. For more
236  // comprehensive test case for this, take a look at
237  // regression/cbmc/no_nondet_static/main.c
238 
239  // const int a;
240  if(type.get_bool(ID_C_constant))
241  return true;
242 
243  // This is a termination condition to break the recursion
244  // for recursive types such as the following:
245  // struct list { const int datum; struct list * next; };
246  // NOTE: the difference between this condition and the previous
247  // one is that this one always returns.
248  if(type.id() == ID_pointer)
249  return type.get_bool(ID_C_constant);
250 
251  // When we have a case like the following, we don't immediately
252  // see the struct t. Instead, we only get to see symbol t1, which
253  // we have to use the namespace to resolve to its definition:
254  // struct t { const int a; };
255  // struct t t1;
256  if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
257  {
258  const auto &resolved_type = ns.follow(type);
259  return has_constant_components(resolved_type);
260  }
261 
262  // In a case like this, where we see an array (b[3] here), we know that
263  // the array contains subtypes. We get the first one, and
264  // then resolve it to its definition through the usage of the namespace.
265  // struct contains_constant_pointer { int x; int * const p; };
266  // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
267  if(type.has_subtype())
268  {
269  const auto &subtype = to_type_with_subtype(type).subtype();
271  }
272 
273  return false;
274 }
275 
276 vector_typet::vector_typet(const typet &_subtype, const constant_exprt &_size)
277  : type_with_subtypet(ID_vector, _subtype)
278 {
279  size() = _size;
280 }
281 
283 {
284  return static_cast<const constant_exprt &>(find(ID_size));
285 }
286 
288 {
289  return static_cast<constant_exprt &>(add(ID_size));
290 }
291 
294 {
295  const union_typet::componentst &comps = components();
296 
297  optionalt<mp_integer> max_width;
298  typet max_comp_type;
299  irep_idt max_comp_name;
300 
301  for(const auto &comp : comps)
302  {
303  auto element_width = pointer_offset_bits(comp.type(), ns);
304 
305  if(!element_width.has_value())
306  return {};
307 
308  if(max_width.has_value() && *element_width <= *max_width)
309  continue;
310 
311  max_width = *element_width;
312  max_comp_type = comp.type();
313  max_comp_name = comp.get_name();
314  }
315 
316  if(!max_width.has_value())
317  return {};
318  else
319  return std::make_pair(
320  struct_union_typet::componentt{max_comp_name, max_comp_type}, *max_width);
321 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Arrays with given size.
Definition: std_types.h:968
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.cpp:22
const exprt & size() const
Definition: std_types.h:976
mp_integer min_value() const
mp_integer max_value() const
A constant literal expression.
Definition: std_expr.h:2668
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
std::size_t get_integer_bits() const
Definition: std_types.cpp:35
std::size_t get_f() const
Definition: std_types.cpp:42
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
Definition: std_types.cpp:200
mp_integer largest() const
Return the largest value that can be represented using this type.
Definition: std_types.cpp:185
constant_exprt zero_expr() const
Return an expression representing the zero value of this type.
Definition: std_types.cpp:190
constant_exprt smallest_expr() const
Return an expression representing the smallest value of this type.
Definition: std_types.cpp:195
mp_integer smallest() const
Return the smallest value that can be represented using this type.
Definition: std_types.cpp:180
irept & add(const irep_namet &name)
Definition: irep.cpp:113
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
tree_implementationt baset
Definition: irep.h:385
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
bool is_nil() const
Definition: irep.h:387
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The NIL expression.
Definition: std_expr.h:2735
void set_to(const mp_integer &to)
Definition: std_types.cpp:165
void set_from(const mp_integer &_from)
Definition: std_types.cpp:160
mp_integer get_to() const
Definition: std_types.cpp:175
mp_integer get_from() const
Definition: std_types.cpp:170
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:498
struct_tag_typet & type()
Definition: std_types.cpp:87
Structure type, corresponds to C style structs.
Definition: std_types.h:226
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:121
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:102
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:257
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
Definition: std_types.cpp:107
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:80
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:67
const componentst & components() const
Definition: std_types.h:142
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:50
std::vector< componentt > componentst
Definition: std_types.h:135
const irep_idt & get_identifier() const
Definition: std_types.h:459
Type with a single subtype.
Definition: type.h:146
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
bool has_subtype() const
Definition: type.h:65
optionalt< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
Definition: std_types.cpp:293
vector_typet(const typet &_subtype, const constant_exprt &_size)
Definition: std_types.cpp:276
const constant_exprt & size() const
Definition: std_types.cpp:282
const irept & get_nil_irep()
Definition: irep.cpp:26
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
BigInt mp_integer
Definition: mp_arith.h:19
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
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:214
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:147
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:154
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:209
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:523
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:38
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:154
#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