cprover
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  const typet &subtype() const
49  {
50  if(get_sub().empty())
51  return static_cast<const typet &>(get_nil_irep());
52  return static_cast<const typet &>(get_sub().front());
53  }
54 
56  {
57  subt &sub=get_sub();
58  if(sub.empty())
59  sub.resize(1);
60  return static_cast<typet &>(sub.front());
61  }
62 
63  bool has_subtypes() const
64  { return !get_sub().empty(); }
65 
66  bool has_subtype() const
67  {
68  return get_sub().size() == 1;
69  }
70 
72  { get_sub().clear(); }
73 
75  {
76  return (const source_locationt &)find(ID_C_source_location);
77  }
78 
80  {
81  return static_cast<source_locationt &>(add(ID_C_source_location));
82  }
83 
84  typet &add_type(const irep_idt &name)
85  {
86  return static_cast<typet &>(add(name));
87  }
88 
89  const typet &find_type(const irep_idt &name) const
90  {
91  return static_cast<const typet &>(find(name));
92  }
93 
102  static void
104  {
105  }
106 
115  static void validate(
116  const typet &type,
117  const namespacet &,
119  {
120  check_type(type, vm);
121  }
122 
131  static void validate_full(
132  const typet &type,
133  const namespacet &ns,
135  {
136  // check subtypes
137  for(const irept &sub : type.get_sub())
138  {
139  const typet &subtype = static_cast<const typet &>(sub);
140  validate_full_type(subtype, ns, vm);
141  }
142 
143  validate_type(type, ns, vm);
144  }
145 };
146 
149 {
150 public:
152  : typet(std::move(_id), std::move(_subtype))
153  {
154  }
155 
156  const typet &subtype() const
157  {
158  // the existence of get_sub().front() is established by check()
159  return static_cast<const typet &>(get_sub().front());
160  }
161 
163  {
164  // the existence of get_sub().front() is established by check()
165  return static_cast<typet &>(get_sub().front());
166  }
167 
168  static void check(
169  const typet &type,
171  {
172  DATA_CHECK(
173  vm, type.get_sub().size() == 1, "type must have one type parameter");
174  }
175 };
176 
178 {
180  return static_cast<const type_with_subtypet &>(type);
181 }
182 
184 {
186  return static_cast<type_with_subtypet &>(type);
187 }
188 
191 {
192 public:
193  typedef std::vector<typet> subtypest;
194 
195  type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
196  : typet(_id)
197  {
198  subtypes() = _subtypes;
199  }
200 
201  type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes) : typet(_id)
202  {
203  subtypes() = std::move(_subtypes);
204  }
205 
207  {
208  return (subtypest &)get_sub();
209  }
210 
211  const subtypest &subtypes() const
212  {
213  return (const subtypest &)get_sub();
214  }
215 
216  void move_to_subtypes(typet &type); // destroys type
217 
218  void copy_to_subtypes(const typet &type);
219 };
220 
222 {
223  return static_cast<const type_with_subtypest &>(type);
224 }
225 
227 {
228  return static_cast<type_with_subtypest &>(type);
229 }
230 
233 typet remove_const(typet type);
234 
235 #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:37
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:106
irept & add(const irep_idt &name)
Definition: irep.cpp:116
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:191
type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
Definition: type.h:195
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:206
std::vector< typet > subtypest
Definition: type.h:193
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)
Definition: type.h:201
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:211
Type with a single subtype.
Definition: type.h:149
const typet & subtype() const
Definition: type.h:156
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:168
typet & subtype()
Definition: type.h:162
type_with_subtypet(irep_idt _id, typet _subtype)
Definition: type.h:151
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:74
typet(irep_idt _id, typet _subtype)
Definition: type.h:37
const typet & subtype() const
Definition: type.h:48
typet(const irep_idt &_id)
Definition: type.h:33
typet & add_type(const irep_idt &name)
Definition: type.h:84
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:131
bool has_subtypes() const
Definition: type.h:63
const typet & find_type(const irep_idt &name) const
Definition: type.h:89
typet()
Definition: type.h:31
bool has_subtype() const
Definition: type.h:66
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:103
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:115
void remove_subtype()
Definition: type.h:71
typet & subtype()
Definition: type.h:55
source_locationt & add_source_location()
Definition: type.h:79
const irept & get_nil_irep()
Definition: irep.cpp:20
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:221
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177
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