CBMC
type.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Defines typet, type_with_subtypet and type_with_subtypest
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  Maria Svorenova, maria.svorenova@diffblue.com
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_UTIL_TYPE_H
14 #define CPROVER_UTIL_TYPE_H
15 
16 class namespacet;
17 
18 #include "source_location.h"
19 #include "validate.h"
20 #include "validate_types.h"
21 #include "validation_mode.h"
22 
28 class typet:public irept
29 {
30 public:
31  typet() { }
32 
33  explicit typet(const irep_idt &_id):irept(_id) { }
34 
35  // the STL implementation shipped with GCC 5 is broken
36 #if !defined(__GLIBCXX__) || __GLIBCXX__ >= 20181026
37  typet(irep_idt _id, typet _subtype)
38  : irept(std::move(_id), {}, {std::move(_subtype)})
39  {
40  }
41 #else
42  typet(irep_idt _id, typet _subtype) : irept(std::move(_id))
43  {
44  add_subtype() = std::move(_subtype);
45  }
46 #endif
47 
48  // This method allows the construction of a type with a subtype by
49  // starting from a type without subtype. It avoids copying the contents
50  // of the type. The primary use-case are parsers, where a copy could be
51  // too expensive. Consider type_with_subtypet(id, subtype) for other
52  // use-cases.
54  {
55  subt &sub = get_sub();
56  if(sub.empty())
57  sub.resize(1);
58  return static_cast<typet &>(sub.front());
59  }
60 
61  bool has_subtypes() const
62  { return !get_sub().empty(); }
63 
64  bool has_subtype() const
65  {
66  return get_sub().size() == 1;
67  }
68 
70  { get_sub().clear(); }
71 
73  {
74  return (const source_locationt &)find(ID_C_source_location);
75  }
76 
78  {
79  return static_cast<source_locationt &>(add(ID_C_source_location));
80  }
81 
82  typet &add_type(const irep_idt &name)
83  {
84  return static_cast<typet &>(add(name));
85  }
86 
87  const typet &find_type(const irep_idt &name) const
88  {
89  return static_cast<const typet &>(find(name));
90  }
91 
100  static void
102  {
103  }
104 
113  static void validate(
114  const typet &type,
115  const namespacet &,
117  {
118  check_type(type, vm);
119  }
120 
129  static void validate_full(
130  const typet &type,
131  const namespacet &ns,
133  {
134  // check subtypes
135  for(const irept &sub : type.get_sub())
136  {
137  const typet &subtype = static_cast<const typet &>(sub);
138  validate_full_type(subtype, ns, vm);
139  }
140 
141  validate_type(type, ns, vm);
142  }
143 };
144 
147 {
148 public:
150  : typet(std::move(_id), std::move(_subtype))
151  {
152  }
153 
154  const typet &subtype() const
155  {
156  // the existence of get_sub().front() is established by check()
157  return static_cast<const typet &>(get_sub().front());
158  }
159 
161  {
162  // the existence of get_sub().front() is established by check()
163  return static_cast<typet &>(get_sub().front());
164  }
165 
166  static void check(
167  const typet &type,
169  {
170  DATA_CHECK(
171  vm, type.get_sub().size() == 1, "type must have one type parameter");
172  }
173 };
174 
176 {
178  return static_cast<const type_with_subtypet &>(type);
179 }
180 
182 {
184  return static_cast<type_with_subtypet &>(type);
185 }
186 
189 {
190 public:
191  typedef std::vector<typet> subtypest;
192 
193  type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
194  : typet(_id)
195  {
196  subtypes() = _subtypes;
197  }
198 
199  type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes) : typet(_id)
200  {
201  subtypes() = std::move(_subtypes);
202  }
203 
205  {
206  return (subtypest &)get_sub();
207  }
208 
209  const subtypest &subtypes() const
210  {
211  return (const subtypest &)get_sub();
212  }
213 
214  void move_to_subtypes(typet &type); // destroys type
215 
216  void copy_to_subtypes(const typet &type);
217 };
218 
220 {
221  return static_cast<const type_with_subtypest &>(type);
222 }
223 
225 {
226  return static_cast<type_with_subtypest &>(type);
227 }
228 
231 typet remove_const(typet type);
232 
233 #endif // CPROVER_UTIL_TYPE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:39
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
subt & get_sub()
Definition: irep.h:456
const irept & find(const irep_idt &name) const
Definition: irep.cpp:101
irept & add(const irep_idt &name)
Definition: irep.cpp:111
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Type with multiple subtypes.
Definition: type.h:189
type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
Definition: type.h:193
void move_to_subtypes(typet &type)
Move the provided type to the subtypes of this type.
Definition: type.cpp:25
subtypest & subtypes()
Definition: type.h:204
std::vector< typet > subtypest
Definition: type.h:191
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)
Definition: type.h:199
void copy_to_subtypes(const typet &type)
Copy the provided type to the subtypes of this type.
Definition: type.cpp:17
const subtypest & subtypes() const
Definition: type.h:209
Type with a single subtype.
Definition: type.h:147
const typet & subtype() const
Definition: type.h:154
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:166
typet & subtype()
Definition: type.h:160
type_with_subtypet(irep_idt _id, typet _subtype)
Definition: type.h:149
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:72
typet(irep_idt _id, typet _subtype)
Definition: type.h:37
typet & add_subtype()
Definition: type.h:53
typet(const irep_idt &_id)
Definition: type.h:33
typet & add_type(const irep_idt &name)
Definition: type.h:82
static void validate_full(const typet &type, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the type is well-formed (full check, including checks of subtypes)
Definition: type.h:129
bool has_subtypes() const
Definition: type.h:61
const typet & find_type(const irep_idt &name) const
Definition: type.h:87
typet()
Definition: type.h:31
bool has_subtype() const
Definition: type.h:64
static void check(const typet &, const validation_modet=validation_modet::INVARIANT)
Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked)
Definition: type.h:101
static void validate(const typet &type, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Check that the type is well-formed, assuming that its subtypes have already been checked for well-for...
Definition: type.h:113
void remove_subtype()
Definition: type.h:69
source_locationt & add_source_location()
Definition: type.h:77
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:219
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:175
typet remove_const(typet type)
Remove const qualifier from type (if any).
Definition: type.cpp:32
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
void check_type(const typet &type, const validation_modet vm)
Check that the given type is well-formed (shallow checks only, i.e., subtypes are not checked)
void validate_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed, assuming that its subtypes have already been checked for we...
void validate_full_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed (full check, including checks of subtypes)
validation_modet