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  subtype() = std::move(_subtype);
45  }
46 #endif
47 
48  // Deliberately protected -- use type-specific accessor methods instead.
49 protected:
50  const typet &subtype() const
51  {
52  if(get_sub().empty())
53  return static_cast<const typet &>(get_nil_irep());
54  return static_cast<const typet &>(get_sub().front());
55  }
56 
58  {
59  subt &sub=get_sub();
60  if(sub.empty())
61  sub.resize(1);
62  return static_cast<typet &>(sub.front());
63  }
64 
65 public:
66  // This method allows the construction of a type with a subtype by
67  // starting from a type without subtype. It avoids copying the contents
68  // of the type. The primary use-case are parsers, where a copy could be
69  // too expensive. Consider type_with_subtypet(id, subtype) for other
70  // use-cases.
72  {
73  subt &sub = get_sub();
74  if(sub.empty())
75  sub.resize(1);
76  return static_cast<typet &>(sub.front());
77  }
78 
79  bool has_subtypes() const
80  { return !get_sub().empty(); }
81 
82  bool has_subtype() const
83  {
84  return get_sub().size() == 1;
85  }
86 
88  { get_sub().clear(); }
89 
91  {
92  return (const source_locationt &)find(ID_C_source_location);
93  }
94 
96  {
97  return static_cast<source_locationt &>(add(ID_C_source_location));
98  }
99 
100  typet &add_type(const irep_idt &name)
101  {
102  return static_cast<typet &>(add(name));
103  }
104 
105  const typet &find_type(const irep_idt &name) const
106  {
107  return static_cast<const typet &>(find(name));
108  }
109 
118  static void
120  {
121  }
122 
131  static void validate(
132  const typet &type,
133  const namespacet &,
135  {
136  check_type(type, vm);
137  }
138 
147  static void validate_full(
148  const typet &type,
149  const namespacet &ns,
151  {
152  // check subtypes
153  for(const irept &sub : type.get_sub())
154  {
155  const typet &subtype = static_cast<const typet &>(sub);
156  validate_full_type(subtype, ns, vm);
157  }
158 
159  validate_type(type, ns, vm);
160  }
161 };
162 
165 {
166 public:
168  : typet(std::move(_id), std::move(_subtype))
169  {
170  }
171 
172  const typet &subtype() const
173  {
174  // the existence of get_sub().front() is established by check()
175  return static_cast<const typet &>(get_sub().front());
176  }
177 
179  {
180  // the existence of get_sub().front() is established by check()
181  return static_cast<typet &>(get_sub().front());
182  }
183 
184  static void check(
185  const typet &type,
187  {
188  DATA_CHECK(
189  vm, type.get_sub().size() == 1, "type must have one type parameter");
190  }
191 };
192 
194 {
196  return static_cast<const type_with_subtypet &>(type);
197 }
198 
200 {
202  return static_cast<type_with_subtypet &>(type);
203 }
204 
207 {
208 public:
209  typedef std::vector<typet> subtypest;
210 
211  type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
212  : typet(_id)
213  {
214  subtypes() = _subtypes;
215  }
216 
217  type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes) : typet(_id)
218  {
219  subtypes() = std::move(_subtypes);
220  }
221 
223  {
224  return (subtypest &)get_sub();
225  }
226 
227  const subtypest &subtypes() const
228  {
229  return (const subtypest &)get_sub();
230  }
231 
232  void move_to_subtypes(typet &type); // destroys type
233 
234  void copy_to_subtypes(const typet &type);
235 };
236 
238 {
239  return static_cast<const type_with_subtypest &>(type);
240 }
241 
243 {
244  return static_cast<type_with_subtypest &>(type);
245 }
246 
249 typet remove_const(typet type);
250 
251 #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:105
irept & add(const irep_idt &name)
Definition: irep.cpp:115
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:207
type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
Definition: type.h:211
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:222
std::vector< typet > subtypest
Definition: type.h:209
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)
Definition: type.h:217
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:227
Type with a single subtype.
Definition: type.h:165
const typet & subtype() const
Definition: type.h:172
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:184
typet & subtype()
Definition: type.h:178
type_with_subtypet(irep_idt _id, typet _subtype)
Definition: type.h:167
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:90
typet(irep_idt _id, typet _subtype)
Definition: type.h:37
const typet & subtype() const
Definition: type.h:50
typet & add_subtype()
Definition: type.h:71
typet(const irep_idt &_id)
Definition: type.h:33
typet & add_type(const irep_idt &name)
Definition: type.h:100
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:147
bool has_subtypes() const
Definition: type.h:79
const typet & find_type(const irep_idt &name) const
Definition: type.h:105
typet()
Definition: type.h:31
bool has_subtype() const
Definition: type.h:82
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:119
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:131
void remove_subtype()
Definition: type.h:87
typet & subtype()
Definition: type.h:57
source_locationt & add_source_location()
Definition: type.h:95
const irept & get_nil_irep()
Definition: irep.cpp:19
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:237
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:193
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