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 
12 #include <util/namespace.h>
13 #include <util/symbol_table.h>
14 
21  const typet &type,
22  const optionalt<typet> &subtype)
23 {
24  REQUIRE(type.id() == ID_pointer);
25  const pointer_typet &pointer = to_pointer_type(type);
26 
27  if(subtype)
28  REQUIRE(pointer.subtype() == subtype.value());
29 
30  return pointer;
31 }
32 
38  const java_class_typet &java_class_type,
39  const irep_idt &component_name)
40 {
41  const auto &component = std::find_if(
42  java_class_type.components().begin(),
43  java_class_type.components().end(),
44  [&component_name](const java_class_typet::componentt &component) {
45  return component.get_name() == component_name;
46  });
47 
48  REQUIRE(component != java_class_type.components().end());
49  return *component;
50 }
51 
57  const struct_typet &struct_type,
58  const irep_idt &component_name)
59 {
60  const auto &componet = std::find_if(
61  struct_type.components().begin(),
62  struct_type.components().end(),
63  [&component_name](const struct_union_typet::componentt &component) {
64  return component.get_name() == component_name;
65  });
66 
67  REQUIRE(componet != struct_type.components().end());
68  return *componet;
69 }
70 
75 {
76  REQUIRE(type.id() == ID_code);
77  return to_code_type(type);
78 }
79 
87 require_type::require_code(const typet &type, const size_t num_params)
88 {
89  code_typet code_type = require_code(type);
90  REQUIRE(code_type.parameters().size() == num_params);
91  return code_type;
92 }
93 
98 {
99  REQUIRE(can_cast_type<java_method_typet>(type));
100  return to_java_method_type(type);
101 }
102 
110 require_type::require_java_method(const typet &type, const size_t num_params)
111 {
112  java_method_typet method_type = require_java_method(type);
113  REQUIRE(method_type.parameters().size() == num_params);
114  return method_type;
115 }
116 
123  const code_typet &function_type,
124  const irep_idt &param_name)
125 {
126  const auto param = std::find_if(
127  function_type.parameters().begin(),
128  function_type.parameters().end(),
129  [&param_name](const code_typet::parametert param) {
130  return param.get_base_name() == param_name;
131  });
132 
133  REQUIRE(param != function_type.parameters().end());
134  return *param;
135 }
136 
143  const reference_typet &type_argument,
145 {
146  switch(expected.kind)
147  {
149  {
150  REQUIRE(is_java_generic_parameter(type_argument));
151  java_generic_parametert parameter =
152  to_java_generic_parameter(type_argument);
153  REQUIRE(parameter.type_variable().get_identifier() == expected.description);
154  return true;
155  }
157  {
158  REQUIRE(!is_java_generic_parameter(type_argument));
159  REQUIRE(
160  to_struct_tag_type(type_argument.subtype()).get_identifier() ==
161  expected.description);
162  return true;
163  }
164  }
165  // Should be unreachable...
166  REQUIRE(false);
167  return false;
168 }
169 
174 {
175  REQUIRE(is_java_generic_type(type));
176  return to_java_generic_type(type);
177 }
178 
192  const typet &type,
193  const require_type::expected_type_argumentst &type_expectations)
194 {
195  const java_generic_typet &generic_type =
197 
198  const java_generic_typet::generic_type_argumentst &generic_type_arguments =
199  generic_type.generic_type_arguments();
200  REQUIRE(generic_type_arguments.size() == type_expectations.size());
201  REQUIRE(
202  std::equal(
203  generic_type_arguments.begin(),
204  generic_type_arguments.end(),
205  type_expectations.begin(),
207 
208  return generic_type;
209 }
210 
216 {
217  REQUIRE(is_java_generic_parameter(type));
218  return to_java_generic_parameter(type);
219 }
220 
228  const typet &type,
229  const irep_idt &parameter)
230 {
231  const java_generic_parametert &generic_param =
233 
234  REQUIRE(
236  generic_param, {require_type::type_argument_kindt::Var, parameter}));
237 
238  return generic_param;
239 }
240 
247  const typet &type,
248  const optionalt<struct_tag_typet> &expect_subtype)
249 {
250  REQUIRE(!is_java_generic_parameter(type));
251  REQUIRE(!is_java_generic_type(type));
252  if(expect_subtype)
253  REQUIRE(type.subtype() == expect_subtype.value());
254  return type;
255 }
256 
261 {
262  REQUIRE(class_type.id() == ID_struct);
263 
264  const java_class_typet &java_class_type = to_java_class_type(class_type);
265  REQUIRE(java_class_type.is_class());
266  REQUIRE_FALSE(java_class_type.get_is_stub());
267 
268  return java_class_type;
269 }
270 
275 {
276  REQUIRE(class_type.id() == ID_struct);
277 
278  const java_class_typet &java_class_type = to_java_class_type(class_type);
279  REQUIRE(java_class_type.is_class());
280  REQUIRE(java_class_type.get_is_stub());
281 
282  return java_class_type;
283 }
284 
290 {
291  REQUIRE(class_type.id() == ID_struct);
292 
293  const class_typet &class_class_type = to_class_type(class_type);
294  const java_class_typet &java_class_type =
295  to_java_class_type(class_class_type);
296 
297  REQUIRE(is_java_generic_class_type(java_class_type));
298  const java_generic_class_typet &java_generic_class_type =
299  to_java_generic_class_type(java_class_type);
300 
301  return java_generic_class_type;
302 }
303 
310  const typet &class_type,
311  const std::initializer_list<irep_idt> &type_variables)
312 {
313  const java_generic_class_typet java_generic_class_type =
314  require_java_generic_class(class_type);
315 
316  const java_generic_class_typet::generic_typest &generic_type_vars =
317  java_generic_class_type.generic_types();
318  REQUIRE(generic_type_vars.size() == type_variables.size());
319  REQUIRE(
320  std::equal(
321  type_variables.begin(),
322  type_variables.end(),
323  generic_type_vars.begin(),
324  [](
325  const irep_idt &type_var_name,
326  const java_generic_parametert &param) { //NOLINT
327  REQUIRE(is_java_generic_parameter(param));
328  return param.type_variable().get_identifier() == type_var_name;
329  }));
330 
331  return java_generic_class_type;
332 }
333 
339 {
340  require_complete_class(class_type);
341  return require_java_generic_class(class_type);
342 }
343 
350  const typet &class_type,
351  const std::initializer_list<irep_idt> &type_variables)
352 {
354  return require_java_generic_class(class_type, type_variables);
355 }
356 
362 {
363  REQUIRE(class_type.id() == ID_struct);
364 
365  const class_typet &class_class_type = to_class_type(class_type);
366  const java_class_typet &java_class_type =
367  to_java_class_type(class_class_type);
368 
369  REQUIRE(is_java_implicitly_generic_class_type(java_class_type));
371  &java_implicitly_generic_class_type =
372  to_java_implicitly_generic_class_type(java_class_type);
373 
374  return java_implicitly_generic_class_type;
375 }
376 
384  const typet &class_type,
385  const std::initializer_list<irep_idt> &implicit_type_variables)
386 {
388  &java_implicitly_generic_class_type =
390 
392  &implicit_generic_type_vars =
393  java_implicitly_generic_class_type.implicit_generic_types();
394  REQUIRE(implicit_generic_type_vars.size() == implicit_type_variables.size());
395  auto param = implicit_generic_type_vars.begin();
396  auto type_var_name = implicit_type_variables.begin();
397  for(; param != implicit_generic_type_vars.end(); ++param, ++type_var_name)
398  {
399  REQUIRE(is_java_generic_parameter(*param));
400  REQUIRE(param->type_variable().get_identifier() == *type_var_name);
401  }
402  return java_implicitly_generic_class_type;
403 }
404 
410  const typet &class_type)
411 {
412  require_complete_class(class_type);
413  return require_java_implicitly_generic_class(class_type);
414 }
415 
423  const typet &class_type,
424  const std::initializer_list<irep_idt> &implicit_type_variables)
425 {
426  require_complete_class(class_type);
428  class_type, implicit_type_variables);
429 }
430 
436 {
437  REQUIRE(class_type.id() == ID_struct);
438 
439  const class_typet &class_class_type = to_class_type(class_type);
440  const java_class_typet &java_class_type =
441  to_java_class_type(class_class_type);
442 
443  REQUIRE(!is_java_generic_class_type(java_class_type));
444  REQUIRE(!is_java_implicitly_generic_class_type(java_class_type));
445 
446  return java_class_type;
447 }
448 
454 {
455  require_complete_class(class_type);
456  return require_java_non_generic_class(class_type);
457 }
458 
463 const struct_tag_typet &
464 require_type::require_struct_tag(const typet &type, const irep_idt &identifier)
465 {
466  REQUIRE(type.id() == ID_struct_tag);
467  const struct_tag_typet &result = to_struct_tag_type(type);
468  if(!identifier.empty())
469  {
470  REQUIRE(result.get_identifier() == identifier);
471  }
472  return result;
473 }
474 
477 {
478  const auto pointer_type = require_type::require_pointer(type, {});
480  return pointer_type;
481 }
482 
489  const typet &type,
490  const std::string &identifier)
491 {
492  struct_tag_typet struct_tag_type = require_struct_tag(type, identifier);
493  REQUIRE(is_java_generic_struct_tag_type(type));
494  return to_java_generic_struct_tag_type(type);
495 }
496 
512  const typet &type,
513  const std::string &identifier,
514  const require_type::expected_type_argumentst &type_expectations)
515 {
516  const java_generic_struct_tag_typet &generic_base_type =
517  require_java_generic_struct_tag_type(type, identifier);
518 
519  const java_generic_typet::generic_type_argumentst &generic_type_arguments =
520  generic_base_type.generic_types();
521  REQUIRE(generic_type_arguments.size() == type_expectations.size());
522  REQUIRE(
523  std::equal(
524  generic_type_arguments.begin(),
525  generic_type_arguments.end(),
526  type_expectations.begin(),
528 
529  return generic_base_type;
530 }
531 
540  const java_class_typet &class_type,
541  const std::vector<std::string> &expected_identifiers)
542 {
543  const require_type::java_lambda_method_handlest &lambda_method_handles =
544  class_type.lambda_method_handles();
545  REQUIRE(lambda_method_handles.size() == expected_identifiers.size());
546 
547  REQUIRE(std::equal(
548  lambda_method_handles.begin(),
549  lambda_method_handles.end(),
550  expected_identifiers.begin(),
551  [](
553  const std::string &expected_identifier) { //NOLINT
554  return lambda_method_handle.get_lambda_method_descriptor()
555  .get_identifier() == expected_identifier;
556  }));
557  return lambda_method_handles;
558 }
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
is_java_generic_class_type
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:995
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
require_type::require_code
code_typet require_code(const typet &type)
Checks a type is a code_type (i.e.
Definition: require_type.cpp:74
require_type::expected_type_argumentt::description
irep_idt description
Definition: require_type.h:63
java_class_typet::componentt
Definition: java_types.h:202
typet::subtype
const typet & subtype() const
Definition: type.h:47
class_typet
Class type.
Definition: std_types.h:320
java_generic_typet
Reference that points to a java_generic_struct_tag_typet.
Definition: java_types.h:916
require_type.h
Helper functions for requiring specific types If the type is of the wrong type, throw a CATCH excepti...
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:488
reference_typet
The reference type.
Definition: std_types.h:1553
java_implicitly_generic_class_typet::implicit_generic_types
const implicit_generic_typest & implicit_generic_types() const
Definition: java_types.h:1084
java_generic_class_typet::generic_typest
std::vector< java_generic_parametert > generic_typest
Definition: java_types.h:975
typet
The type of an expression, extends irept.
Definition: type.h:29
require_type::expected_type_argumentst
std::initializer_list< expected_type_argumentt > expected_type_argumentst
Definition: require_type.h:66
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:409
to_class_type
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:376
lambda_method_handle
static optionalt< java_class_typet::java_lambda_method_handlet > lambda_method_handle(const symbol_tablet &symbol_table, const irep_idt &method_identifier, const java_method_typet &dynamic_method_type)
Definition: lambda_synthesis.cpp:77
require_type::java_lambda_method_handlest
java_class_typet::java_lambda_method_handlest java_lambda_method_handlest
Definition: require_type.h:131
java_generic_parametert
Reference that points to a java_generic_parameter_tagt.
Definition: java_types.h:778
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
is_java_implicitly_generic_class_type
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:1100
to_java_generic_class_type
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
Definition: java_types.h:1003
java_generic_typet::generic_type_argumentst
java_generic_struct_tag_typet::generic_typest generic_type_argumentst
Definition: java_types.h:918
namespace.h
java_generic_struct_tag_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:874
require_type::expected_type_argumentt
Definition: require_type.h:61
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:246
java_class_typet
Definition: java_types.h:199
java_generic_class_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:982
java_class_typet::java_lambda_method_handlet
Represents a lambda call to a method.
Definition: java_types.h:484
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:173
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:142
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:361
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
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:539
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:898
java_generic_typet::generic_type_arguments
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:927
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:260
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:215
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:821
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:97
is_java_generic_struct_tag_type
bool is_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:890
is_java_generic_type
bool is_java_generic_type(const typet &type)
Definition: java_types.h:947
struct_typet::is_class
bool is_class() const
A struct may be a class, where members may have access restrictions.
Definition: std_types.h:240
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:1068
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:453
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
require_type::type_argument_kindt::Inst
@ Inst
code_typet
Base type of functions.
Definition: std_types.h:736
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:515
dstringt::empty
bool empty() const
Definition: dstring.h:88
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
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:289
to_java_generic_type
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:954
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
struct_union_typet::componentt
Definition: std_types.h:64
java_class_typet::components
const componentst & components() const
Definition: java_types.h:226
require_type::require_pointer_to_tag
pointer_typet require_pointer_to_tag(const typet &type, const irep_idt &identifier=irep_idt())
Definition: require_type.cpp:476
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
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:274
to_java_generic_parameter
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:828
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:122
java_implicitly_generic_class_typet::implicit_generic_typest
std::vector< java_generic_parametert > implicit_generic_typest
Definition: java_types.h:1070
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:435
require_type::expected_type_argumentt::kind
type_argument_kindt kind
Definition: require_type.h:62
use_catch.h
code_typet::parametert
Definition: std_types.h:753
can_cast_type< java_method_typet >
bool can_cast_type< java_method_typet >(const typet &type)
Definition: java_types.h:181
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:1108
java_generic_struct_tag_typet
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:859
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:20
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:973
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
java_class_typet::get_is_stub
bool get_is_stub() const
Definition: java_types.h:400
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:1488
require_type::require_component
java_class_typet::componentt require_component(const java_class_typet &java_class_type, const irep_idt &component_name)
Checks that a class has a component with a specific name.
Definition: require_type.cpp:37
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:464
java_class_typet::lambda_method_handles
const java_lambda_method_handlest & lambda_method_handles() const
Definition: java_types.h:519
java_method_typet
Definition: java_types.h:103
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:338
java_generic_parametert::type_variable
const type_variablet & type_variable() const
Definition: java_types.h:791