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 "namespace.h"
17 #include "std_expr.h"
18 #include "string2int.h"
19 
21 {
22  const irep_idt integer_bits=get(ID_integer_bits);
23  DATA_INVARIANT(!integer_bits.empty(), "integer bits should be set");
24  return unsafe_string2unsigned(id2string(integer_bits));
25 }
26 
27 std::size_t floatbv_typet::get_f() const
28 {
29  const irep_idt &f=get(ID_f);
30  DATA_INVARIANT(!f.empty(), "the mantissa should be set");
32 }
33 
36  const irep_idt &component_name) const
37 {
38  std::size_t number=0;
39 
40  for(const auto &c : components())
41  {
42  if(c.get_name() == component_name)
43  return number;
44 
45  number++;
46  }
47 
49  return 0;
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 
83 struct_typet::baset::baset(const struct_tag_typet &base) : exprt(ID_base, base)
84 {
85 }
86 
88 {
89  bases().push_back(baset(base));
90 }
91 
93 {
94  for(const auto &b : bases())
95  {
96  if(to_struct_tag_type(b.type()).get_identifier() == id)
97  return b;
98  }
99  return {};
100 }
101 
106 bool struct_typet::is_prefix_of(const struct_typet &other) const
107 {
108  const componentst &ot_components=other.components();
109  const componentst &tt_components=components();
110 
111  if(ot_components.size()<
112  tt_components.size())
113  return false;
114 
115  componentst::const_iterator
116  ot_it=ot_components.begin();
117 
118  for(const auto &tt_c : tt_components)
119  {
120  if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name())
121  {
122  return false; // they just don't match
123  }
124 
125  ot_it++;
126  }
127 
128  return true; // ok, *this is a prefix of ot
129 }
130 
132 bool is_reference(const typet &type)
133 {
134  return type.id()==ID_pointer &&
135  type.get_bool(ID_C_reference);
136 }
137 
139 bool is_rvalue_reference(const typet &type)
140 {
141  return type.id()==ID_pointer &&
142  type.get_bool(ID_C_rvalue_reference);
143 }
144 
146 {
147  set(ID_from, integer2string(from));
148 }
149 
151 {
152  set(ID_to, integer2string(to));
153 }
154 
156 {
157  return string2integer(get_string(ID_from));
158 }
159 
161 {
162  return string2integer(get_string(ID_to));
163 }
164 
166 {
167  return -power(2, get_width()-1);
168 }
169 
171 {
172  return power(2, get_width()-1)-1;
173 }
174 
176 {
177  return from_integer(0, *this);
178 }
179 
181 {
182  return from_integer(smallest(), *this);
183 }
184 
186 {
187  return from_integer(largest(), *this);
188 }
189 
191 {
192  return 0;
193 }
194 
196 {
197  return power(2, get_width())-1;
198 }
199 
201 {
202  return from_integer(0, *this);
203 }
204 
206 {
207  return from_integer(smallest(), *this);
208 }
209 
211 {
212  return from_integer(largest(), *this);
213 }
214 
225  const typet &type,
226  const namespacet &ns)
227 {
228  // Helper function to avoid the code duplication in the branches
229  // below.
230  const auto has_constant_components = [&ns](const typet &subtype) -> bool {
231  if(subtype.id() == ID_struct || subtype.id() == ID_union)
232  {
233  const auto &struct_union_type = to_struct_union_type(subtype);
234  for(const auto &component : struct_union_type.components())
235  {
237  return true;
238  }
239  }
240  return false;
241  };
242 
243  // There are 4 possibilities the code below is handling.
244  // The possibilities are enumerated as comments, to show
245  // what each code is supposed to be handling. For more
246  // comprehensive test case for this, take a look at
247  // regression/cbmc/no_nondet_static/main.c
248 
249  // const int a;
250  if(type.get_bool(ID_C_constant))
251  return true;
252 
253  // This is a termination condition to break the recursion
254  // for recursive types such as the following:
255  // struct list { const int datum; struct list * next; };
256  // NOTE: the difference between this condition and the previous
257  // one is that this one always returns.
258  if(type.id() == ID_pointer)
259  return type.get_bool(ID_C_constant);
260 
261  // When we have a case like the following, we don't immediately
262  // see the struct t. Instead, we only get to see symbol t1, which
263  // we have to use the namespace to resolve to its definition:
264  // struct t { const int a; };
265  // struct t t1;
266  if(type.id() == ID_symbol_type ||
267  type.id() == ID_struct_tag ||
268  type.id() == ID_union_tag)
269  {
270  const auto &resolved_type = ns.follow(type);
271  return has_constant_components(resolved_type);
272  }
273 
274  // In a case like this, where we see an array (b[3] here), we know that
275  // the array contains subtypes. We get the first one, and
276  // then resolve it to its definition through the usage of the namespace.
277  // struct contains_constant_pointer { int x; int * const p; };
278  // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
279  if(type.has_subtype())
280  {
281  const auto &subtype = to_type_with_subtype(type).subtype();
283  }
284 
285  return false;
286 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:92
typet::subtype
const typet & subtype() const
Definition: type.h:38
signedbv_typet::largest_expr
constant_exprt largest_expr() const
Definition: std_types.cpp:185
signedbv_typet::smallest
mp_integer smallest() const
Definition: std_types.cpp:165
unsignedbv_typet::zero_expr
constant_exprt zero_expr() const
Definition: std_types.cpp:200
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
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
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:260
typet
The type of an expression, extends irept.
Definition: type.h:27
typet::has_subtype
bool has_subtype() const
Definition: type.h:56
floatbv_typet::get_f
std::size_t get_f() const
Definition: std_types.cpp:27
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
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:87
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:106
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:156
unsignedbv_typet::largest_expr
constant_exprt largest_expr() const
Definition: std_types.cpp:210
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:203
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
signedbv_typet::smallest_expr
constant_exprt smallest_expr() const
Definition: std_types.cpp:180
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:35
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
unsignedbv_typet::smallest
mp_integer smallest() const
Definition: std_types.cpp:190
struct_typet::baset::baset
baset(const struct_tag_typet &base)
Definition: std_types.cpp:83
range_typet::get_from
mp_integer get_from() const
Definition: std_types.cpp:155
std_types.h
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:303
range_typet::get_to
mp_integer get_to() const
Definition: std_types.cpp:160
irept::id
const irep_idt & id() const
Definition: irep.h:259
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:543
dstringt::empty
bool empty() const
Definition: dstring.h:75
unsignedbv_typet::largest
mp_integer largest() const
Definition: std_types.cpp:195
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
struct_typet::baset::type
struct_tag_typet & type()
Definition: std_types.cpp:73
unsignedbv_typet::smallest_expr
constant_exprt smallest_expr() const
Definition: std_types.cpp:205
struct_union_typet::componentt
Definition: std_types.h:121
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
range_typet::set_to
void set_to(const mp_integer &to)
Definition: std_types.cpp:150
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
signedbv_typet::zero_expr
constant_exprt zero_expr() const
Definition: std_types.cpp:175
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:132
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
fixedbv_typet::get_integer_bits
std::size_t get_integer_bits() const
Definition: std_types.cpp:20
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:224
unsafe_string2unsigned
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:69
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:218
signedbv_typet::largest
mp_integer largest() const
Definition: std_types.cpp:170
is_rvalue_reference
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:139
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:55
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
std_expr.h
struct_typet::baset
Base class or struct that a class or struct inherits from.
Definition: std_types.h:292
range_typet::set_from
void set_from(const mp_integer &_from)
Definition: std_types.cpp:145
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470