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 
85  {
86  if(location.is_not_nil())
87  add_source_location() = std::move(location);
88  return std::move(*this);
89  }
90 
93  {
94  if(location.is_not_nil())
95  add_source_location() = std::move(location);
96  return *this;
97  }
98 
101  typet &&with_source_location(const typet &type) &&
102  {
103  return std::move(*this).with_source_location(type.source_location());
104  }
105 
108  {
109  auto &location = type.source_location();
110  if(location.is_not_nil())
111  add_source_location() = location;
112  return *this;
113  }
114 
115  typet &add_type(const irep_idt &name)
116  {
117  return static_cast<typet &>(add(name));
118  }
119 
120  const typet &find_type(const irep_idt &name) const
121  {
122  return static_cast<const typet &>(find(name));
123  }
124 
133  static void
135  {
136  }
137 
146  static void validate(
147  const typet &type,
148  const namespacet &,
150  {
151  check_type(type, vm);
152  }
153 
162  static void validate_full(
163  const typet &type,
164  const namespacet &ns,
166  {
167  // check subtypes
168  for(const irept &sub : type.get_sub())
169  {
170  const typet &subtype = static_cast<const typet &>(sub);
171  validate_full_type(subtype, ns, vm);
172  }
173 
174  validate_type(type, ns, vm);
175  }
176 };
177 
180 {
181 public:
183  : typet(std::move(_id), std::move(_subtype))
184  {
185  }
186 
187  const typet &subtype() const
188  {
189  // the existence of get_sub().front() is established by check()
190  return static_cast<const typet &>(get_sub().front());
191  }
192 
194  {
195  // the existence of get_sub().front() is established by check()
196  return static_cast<typet &>(get_sub().front());
197  }
198 
199  static void check(
200  const typet &type,
202  {
203  DATA_CHECK(
204  vm, type.get_sub().size() == 1, "type must have one type parameter");
205  }
206 };
207 
209 {
211  return static_cast<const type_with_subtypet &>(type);
212 }
213 
215 {
217  return static_cast<type_with_subtypet &>(type);
218 }
219 
222 {
223 public:
224  typedef std::vector<typet> subtypest;
225 
226  type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
227  : typet(_id)
228  {
229  subtypes() = _subtypes;
230  }
231 
232  type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes) : typet(_id)
233  {
234  subtypes() = std::move(_subtypes);
235  }
236 
238  {
239  return (subtypest &)get_sub();
240  }
241 
242  const subtypest &subtypes() const
243  {
244  return (const subtypest &)get_sub();
245  }
246 
247  void move_to_subtypes(typet &type); // destroys type
248 
249  void copy_to_subtypes(const typet &type);
250 };
251 
253 {
254  return static_cast<const type_with_subtypest &>(type);
255 }
256 
258 {
259  return static_cast<type_with_subtypest &>(type);
260 }
261 
264 typet remove_const(typet type);
265 
266 #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:38
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:360
subt & get_sub()
Definition: irep.h:444
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
irept & add(const irep_idt &name)
Definition: irep.cpp:103
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Type with multiple subtypes.
Definition: type.h:222
type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
Definition: type.h:226
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:237
std::vector< typet > subtypest
Definition: type.h:224
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)
Definition: type.h:232
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:242
Type with a single subtype.
Definition: type.h:180
const typet & subtype() const
Definition: type.h:187
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:199
typet & subtype()
Definition: type.h:193
type_with_subtypet(irep_idt _id, typet _subtype)
Definition: type.h:182
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:72
typet & with_source_location(const typet &type) &
This is a 'fluent style' method for adding a source location.
Definition: type.h:107
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:115
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:162
bool has_subtypes() const
Definition: type.h:61
const typet & find_type(const irep_idt &name) const
Definition: type.h:120
typet()
Definition: type.h:31
typet && with_source_location(source_locationt location) &&
This is a 'fluent style' method for creating a new type with an added-on source location.
Definition: type.h:84
typet && with_source_location(const typet &type) &&
This is a 'fluent style' method for creating a new type with an added-on source location.
Definition: type.h:101
bool has_subtype() const
Definition: type.h:64
typet & with_source_location(source_locationt location) &
This is a 'fluent style' method for adding a source location.
Definition: type.h:92
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:134
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:146
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:252
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:208
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