cprover
require_type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Unit test utilities
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #include "require_type.h"
10 
11 #include <testing-utils/catch.hpp>
12 #include <util/base_type.h>
13 #include <util/namespace.h>
14 #include <util/symbol_table.h>
15 
22  const typet &type,
23  const optionalt<typet> &subtype)
24 {
25  REQUIRE(type.id() == ID_pointer);
26  const pointer_typet &pointer = to_pointer_type(type);
27 
28  if(subtype)
29  {
31  base_type_eq(pointer.subtype(), subtype.value(), ns);
32  }
33  return pointer;
34 }
35 
41  const struct_typet &struct_type,
42  const irep_idt &component_name)
43 {
44  const auto &componet = std::find_if(
45  struct_type.components().begin(),
46  struct_type.components().end(),
47  [&component_name](const struct_union_typet::componentt &component) {
48  return component.get_name() == component_name;
49  });
50 
51  REQUIRE(componet != struct_type.components().end());
52  return *componet;
53 }
54 
59 {
60  REQUIRE(type.id() == ID_code);
61  return to_code_type(type);
62 }
63 
71 require_type::require_code(const typet &type, const size_t num_params)
72 {
73  code_typet code_type = require_code(type);
74  REQUIRE(code_type.parameters().size() == num_params);
75  return code_type;
76 }
77 
82 {
83  REQUIRE(can_cast_type<java_method_typet>(type));
84  return to_java_method_type(type);
85 }
86 
94 require_type::require_java_method(const typet &type, const size_t num_params)
95 {
96  java_method_typet method_type = require_java_method(type);
97  REQUIRE(method_type.parameters().size() == num_params);
98  return method_type;
99 }
100 
107  const code_typet &function_type,
108  const irep_idt &param_name)
109 {
110  const auto param = std::find_if(
111  function_type.parameters().begin(),
112  function_type.parameters().end(),
113  [&param_name](const code_typet::parametert param) {
114  return param.get_base_name() == param_name;
115  });
116 
117  REQUIRE(param != function_type.parameters().end());
118  return *param;
119 }
120 
127  const reference_typet &type_argument,
129 {
130  switch(expected.kind)
131  {
133  {
134  REQUIRE(is_java_generic_parameter((type_argument)));
135  java_generic_parametert parameter =
136  to_java_generic_parameter(type_argument);
137  REQUIRE(parameter.type_variable().get_identifier() == expected.description);
138  return true;
139  }
141  {
142  REQUIRE(!is_java_generic_parameter(type_argument));
143  REQUIRE(type_argument.subtype() == struct_tag_typet(expected.description));
144  return true;
145  }
146  }
147  // Should be unreachable...
148  REQUIRE(false);
149  return false;
150 }
151 
156 {
157  REQUIRE(is_java_generic_type(type));
158  return to_java_generic_type(type);
159 }
160 
174  const typet &type,
175  const require_type::expected_type_argumentst &type_expectations)
176 {
177  const java_generic_typet &generic_type =
179 
180  const java_generic_typet::generic_type_argumentst &generic_type_arguments =
181  generic_type.generic_type_arguments();
182  REQUIRE(generic_type_arguments.size() == type_expectations.size());
183  REQUIRE(
184  std::equal(
185  generic_type_arguments.begin(),
186  generic_type_arguments.end(),
187  type_expectations.begin(),
189 
190  return generic_type;
191 }
192 
198 {
199  REQUIRE(is_java_generic_parameter(type));
200  return to_java_generic_parameter(type);
201 }
202 
210  const typet &type,
211  const irep_idt &parameter)
212 {
213  const java_generic_parametert &generic_param =
215 
216  REQUIRE(
218  generic_param, {require_type::type_argument_kindt::Var, parameter}));
219 
220  return generic_param;
221 }
222 
229  const typet &type,
230  const optionalt<struct_tag_typet> &expect_subtype)
231 {
232  REQUIRE(!is_java_generic_parameter(type));
233  REQUIRE(!is_java_generic_type(type));
234  if(expect_subtype)
235  REQUIRE(type.subtype() == expect_subtype.value());
236  return type;
237 }
238 
243 {
244  REQUIRE(class_type.id() == ID_struct);
245 
246  const java_class_typet &java_class_type = to_java_class_type(class_type);
247  REQUIRE(java_class_type.is_class());
248  REQUIRE_FALSE(java_class_type.get_is_stub());
249 
250  return java_class_type;
251 }
252 
257 {
258  REQUIRE(class_type.id() == ID_struct);
259 
260  const java_class_typet &java_class_type = to_java_class_type(class_type);
261  REQUIRE(java_class_type.is_class());
262  REQUIRE(java_class_type.get_is_stub());
263 
264  return java_class_type;
265 }
266 
272 {
273  REQUIRE(class_type.id() == ID_struct);
274 
275  const class_typet &class_class_type = to_class_type(class_type);
276  const java_class_typet &java_class_type =
277  to_java_class_type(class_class_type);
278 
279  REQUIRE(is_java_generic_class_type(java_class_type));
280  const java_generic_class_typet &java_generic_class_type =
281  to_java_generic_class_type(java_class_type);
282 
283  return java_generic_class_type;
284 }
285 
292  const typet &class_type,
293  const std::initializer_list<irep_idt> &type_variables)
294 {
295  const java_generic_class_typet java_generic_class_type =
296  require_java_generic_class(class_type);
297 
298  const java_generic_class_typet::generic_typest &generic_type_vars =
299  java_generic_class_type.generic_types();
300  REQUIRE(generic_type_vars.size() == type_variables.size());
301  REQUIRE(
302  std::equal(
303  type_variables.begin(),
304  type_variables.end(),
305  generic_type_vars.begin(),
306  [](
307  const irep_idt &type_var_name,
308  const java_generic_parametert &param) { //NOLINT
309  REQUIRE(is_java_generic_parameter(param));
310  return param.type_variable().get_identifier() == type_var_name;
311  }));
312 
313  return java_generic_class_type;
314 }
315 
321 {
322  require_complete_class(class_type);
323  return require_java_generic_class(class_type);
324 }
325 
332  const typet &class_type,
333  const std::initializer_list<irep_idt> &type_variables)
334 {
336  return require_java_generic_class(class_type, type_variables);
337 }
338 
344 {
345  REQUIRE(class_type.id() == ID_struct);
346 
347  const class_typet &class_class_type = to_class_type(class_type);
348  const java_class_typet &java_class_type =
349  to_java_class_type(class_class_type);
350 
351  REQUIRE(is_java_implicitly_generic_class_type(java_class_type));
353  &java_implicitly_generic_class_type =
354  to_java_implicitly_generic_class_type(java_class_type);
355 
356  return java_implicitly_generic_class_type;
357 }
358 
366  const typet &class_type,
367  const std::initializer_list<irep_idt> &implicit_type_variables)
368 {
370  &java_implicitly_generic_class_type =
372 
374  &implicit_generic_type_vars =
375  java_implicitly_generic_class_type.implicit_generic_types();
376  REQUIRE(implicit_generic_type_vars.size() == implicit_type_variables.size());
377  REQUIRE(
378  std::equal(
379  implicit_type_variables.begin(),
380  implicit_type_variables.end(),
381  implicit_generic_type_vars.begin(),
382  [](
383  const irep_idt &type_var_name,
384  const java_generic_parametert &param) { //NOLINT
385  REQUIRE(is_java_generic_parameter(param));
386  return param.type_variable().get_identifier() == type_var_name;
387  }));
388 
389  return java_implicitly_generic_class_type;
390 }
391 
397  const typet &class_type)
398 {
399  require_complete_class(class_type);
400  return require_java_implicitly_generic_class(class_type);
401 }
402 
410  const typet &class_type,
411  const std::initializer_list<irep_idt> &implicit_type_variables)
412 {
413  require_complete_class(class_type);
415  class_type, implicit_type_variables);
416 }
417 
423 {
424  REQUIRE(class_type.id() == ID_struct);
425 
426  const class_typet &class_class_type = to_class_type(class_type);
427  const java_class_typet &java_class_type =
428  to_java_class_type(class_class_type);
429 
430  REQUIRE(!is_java_generic_class_type(java_class_type));
431  REQUIRE(!is_java_implicitly_generic_class_type(java_class_type));
432 
433  return java_class_type;
434 }
435 
441 {
442  require_complete_class(class_type);
443  return require_java_non_generic_class(class_type);
444 }
445 
450 const struct_tag_typet &
451 require_type::require_struct_tag(const typet &type, const irep_idt &identifier)
452 {
453  REQUIRE(type.id() == ID_struct_tag);
454  const struct_tag_typet &result = to_struct_tag_type(type);
455  if(identifier != "")
456  {
457  REQUIRE(result.get_identifier() == identifier);
458  }
459  return result;
460 }
461 
468  const typet &type,
469  const std::string &identifier)
470 {
471  struct_tag_typet struct_tag_type = require_struct_tag(type, identifier);
472  REQUIRE(is_java_generic_struct_tag_type(type));
473  return to_java_generic_struct_tag_type(type);
474 }
475 
491  const typet &type,
492  const std::string &identifier,
493  const require_type::expected_type_argumentst &type_expectations)
494 {
495  const java_generic_struct_tag_typet &generic_base_type =
496  require_java_generic_struct_tag_type(type, identifier);
497 
498  const java_generic_typet::generic_type_argumentst &generic_type_arguments =
499  generic_base_type.generic_types();
500  REQUIRE(generic_type_arguments.size() == type_expectations.size());
501  REQUIRE(
502  std::equal(
503  generic_type_arguments.begin(),
504  generic_type_arguments.end(),
505  type_expectations.begin(),
507 
508  return generic_base_type;
509 }
510 
519  const java_class_typet &class_type,
520  const std::vector<std::string> &expected_identifiers)
521 {
522  const require_type::java_lambda_method_handlest &lambda_method_handles =
523  class_type.lambda_method_handles();
524  REQUIRE(lambda_method_handles.size() == expected_identifiers.size());
525 
526  REQUIRE(std::equal(
527  lambda_method_handles.begin(),
528  lambda_method_handles.end(),
529  expected_identifiers.begin(),
530  [](
531  const irept &lambda_method_handle,
532  const std::string &expected_identifier) { //NOLINT
533  return lambda_method_handle.id() == expected_identifier;
534  }));
535  return lambda_method_handles;
536 }
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:479
is_java_generic_class_type
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:565
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
require_type::require_code
code_typet require_code(const typet &type)
Checks a type is a code_type (i.e.
Definition: require_type.cpp:58
require_type::expected_type_argumentt::description
irep_idt description
Definition: require_type.h:55
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
typet::subtype
const typet & subtype() const
Definition: type.h:38
class_typet
Class type.
Definition: std_types.h:365
java_generic_typet
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:483
require_type.h
java_generic_typet::generic_type_argumentst
std::vector< reference_typet > generic_type_argumentst
Definition: java_types.h:486
require_type::require_java_generic_struct_tag_type
java_generic_struct_tag_typet require_java_generic_struct_tag_type(const typet &type, const std::string &identifier)
Verify a given type is a java generic symbol type.
Definition: require_type.cpp:467
reference_typet
The reference type.
Definition: std_types.h:1565
java_implicitly_generic_class_typet::implicit_generic_types
const implicit_generic_typest & implicit_generic_types() const
Definition: java_types.h:654
java_generic_class_typet::generic_typest
std::vector< java_generic_parametert > generic_typest
Definition: java_types.h:545
typet
The type of an expression, extends irept.
Definition: type.h:27
require_type::expected_type_argumentst
std::initializer_list< expected_type_argumentt > expected_type_argumentst
Definition: require_type.h:58
require_type::require_complete_java_implicitly_generic_class
java_implicitly_generic_class_typet require_complete_java_implicitly_generic_class(const typet &class_type)
Verify that a class is a complete, valid java implicitly generic class.
Definition: require_type.cpp:396
to_class_type
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:409
require_type::java_lambda_method_handlest
java_class_typet::java_lambda_method_handlest java_lambda_method_handlest
Definition: require_type.h:123
java_generic_parametert
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>.
Definition: java_types.h:397
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
is_java_implicitly_generic_class_type
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:670
to_java_generic_class_type
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
Definition: java_types.h:573
namespace.h
java_generic_struct_tag_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:764
require_type::expected_type_argumentt
Definition: require_type.h:52
require_type::require_java_non_generic_type
const typet & require_java_non_generic_type(const typet &type, const optionalt< struct_tag_typet > &expect_subtype)
Test a type to ensure it is not a java generics type.
Definition: require_type.cpp:228
java_class_typet
Definition: java_types.h:101
java_generic_class_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:552
require_type::require_java_generic_type
java_generic_typet require_java_generic_type(const typet &type)
Verify a given type is a java_generic_type.
Definition: require_type.cpp:155
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
require_java_generic_type_argument_expectation
bool require_java_generic_type_argument_expectation(const reference_typet &type_argument, const require_type::expected_type_argumentt &expected)
Helper function for testing that java generic type arguments match a given expectation.
Definition: require_type.cpp:126
require_type::require_java_implicitly_generic_class
java_implicitly_generic_class_typet require_java_implicitly_generic_class(const typet &class_type)
Verify that a class is a valid java implicitly generic class.
Definition: require_type.cpp:343
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
require_type::require_lambda_method_handles
java_lambda_method_handlest require_lambda_method_handles(const java_class_typet &class_type, const std::vector< std::string > &expected_identifiers)
Verify that the lambda method handles of a class match the given expectation.
Definition: require_type.cpp:518
to_java_generic_struct_tag_type
const java_generic_struct_tag_typet & to_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:788
java_generic_typet::generic_type_arguments
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:495
base_type.h
require_type::require_complete_class
class_typet require_complete_class(const typet &class_type)
Checks that the given type is a complete class.
Definition: require_type.cpp:242
base_type_eq
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
require_type::type_argument_kindt::Var
@ Var
require_type::require_java_generic_parameter
java_generic_parametert require_java_generic_parameter(const typet &type)
Verify a given type is a java_generic_parameter, e.g., T
Definition: require_type.cpp:197
is_java_generic_parameter
bool is_java_generic_parameter(const typet &type)
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>.
Definition: java_types.h:446
require_type::require_java_method
java_method_typet require_java_method(const typet &type)
Checks a type is a java_method_typet (i.e.
Definition: require_type.cpp:81
is_java_generic_struct_tag_type
bool is_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:780
is_java_generic_type
bool is_java_generic_type(const typet &type)
Definition: java_types.h:517
struct_typet::is_class
bool is_class() const
A struct may be a class, where members may have access restrictions.
Definition: std_types.h:286
java_implicitly_generic_class_typet
Type to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class o...
Definition: java_types.h:637
require_type::require_complete_java_non_generic_class
java_class_typet require_complete_java_non_generic_class(const typet &class_type)
Verify that a class is a complete, valid nongeneric java class.
Definition: require_type.cpp:440
require_type::type_argument_kindt::Inst
@ Inst
code_typet
Base type of functions.
Definition: std_types.h:751
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
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
require_type::require_java_generic_class
java_generic_class_typet require_java_generic_class(const typet &class_type)
Verify that a class is a valid java generic class.
Definition: require_type.cpp:271
to_java_generic_type
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:524
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
struct_union_typet::componentt
Definition: std_types.h:121
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
require_type::require_incomplete_class
class_typet require_incomplete_class(const typet &class_type)
Checks that the given type is an incomplete class.
Definition: require_type.cpp:256
to_java_generic_parameter
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:453
require_type::require_parameter
code_typet::parametert require_parameter(const code_typet &function_type, const irep_idt &param_name)
Verify that a function has a parameter of a specific name.
Definition: require_type.cpp:106
java_implicitly_generic_class_typet::implicit_generic_typest
std::vector< java_generic_parametert > implicit_generic_typest
Definition: java_types.h:640
require_type::require_java_non_generic_class
java_class_typet require_java_non_generic_class(const typet &class_type)
Verify that a class is a valid nongeneric java class.
Definition: require_type.cpp:422
require_type::require_component
struct_typet::componentt require_component(const struct_typet &struct_type, const irep_idt &component_name)
Checks a struct like type has a component with a specific name.
Definition: require_type.cpp:40
require_type::expected_type_argumentt::kind
type_argument_kindt kind
Definition: require_type.h:54
code_typet::parametert
Definition: std_types.h:788
can_cast_type< java_method_typet >
bool can_cast_type< java_method_typet >(const typet &type)
Definition: java_types.h:333
to_java_implicitly_generic_class_type
const java_implicitly_generic_class_typet & to_java_implicitly_generic_class_type(const java_class_typet &type)
Definition: java_types.h:678
java_generic_struct_tag_typet
Type for a generic symbol, extends struct_tag_typet with a vector of java generic types.
Definition: java_types.h:754
require_type::require_pointer
pointer_typet require_pointer(const typet &type, const optionalt< typet > &subtype)
Checks a type is a pointer type optionally with a specific subtype.
Definition: require_type.cpp:21
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
java_generic_class_typet
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition: java_types.h:542
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:246
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:338
java_class_typet::get_is_stub
bool get_is_stub() const
Definition: java_types.h:179
symbol_table.h
Author: Diffblue Ltd.
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
require_type::require_struct_tag
const struct_tag_typet & require_struct_tag(const typet &type, const irep_idt &identifier="")
Verify a given type is a symbol type, optionally with a specific identifier.
Definition: require_type.cpp:451
java_class_typet::lambda_method_handles
const java_lambda_method_handlest & lambda_method_handles() const
Definition: java_types.h:198
java_method_typet
Definition: java_types.h:264
require_type::require_complete_java_generic_class
java_generic_class_typet require_complete_java_generic_class(const typet &class_type)
Verify that a class is a complete, valid java generic class.
Definition: require_type.cpp:320
java_generic_parametert::type_variable
const type_variablet & type_variable() const
Definition: java_types.h:412