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 
20  const typet &type,
21  const optionalt<typet> &subtype)
22 {
23  REQUIRE(type.id() == ID_pointer);
24  const pointer_typet &pointer = to_pointer_type(type);
25 
26  if(subtype)
27  {
28  // TODO: use base_type_eq
29  REQUIRE(pointer.subtype() == subtype.value());
30  }
31  return pointer;
32 }
33 
39  const struct_typet &struct_type,
40  const irep_idt &component_name)
41 {
42  const auto &componet = std::find_if(
43  struct_type.components().begin(),
44  struct_type.components().end(),
45  [&component_name](const struct_union_typet::componentt &component) {
46  return component.get_name() == component_name;
47  });
48 
49  REQUIRE(componet != struct_type.components().end());
50  return *componet;
51 }
52 
57 {
58  REQUIRE(type.id() == ID_code);
59  return to_code_type(type);
60 }
61 
69 require_type::require_code(const typet &type, const size_t num_params)
70 {
71  code_typet code_type = require_code(type);
72  REQUIRE(code_type.parameters().size() == num_params);
73  return code_type;
74 }
75 
82  const code_typet &function_type,
83  const irep_idt &param_name)
84 {
85  const auto param = std::find_if(
86  function_type.parameters().begin(),
87  function_type.parameters().end(),
88  [&param_name](const code_typet::parametert param) {
89  return param.get_base_name() == param_name;
90  });
91 
92  REQUIRE(param != function_type.parameters().end());
93  return *param;
94 }
95 
102  const reference_typet &type_argument,
104 {
105  switch(expected.kind)
106  {
108  {
109  REQUIRE(is_java_generic_parameter((type_argument)));
110  java_generic_parametert parameter =
111  to_java_generic_parameter(type_argument);
112  REQUIRE(parameter.type_variable().get_identifier() == expected.description);
113  return true;
114  }
116  {
117  REQUIRE(!is_java_generic_parameter(type_argument));
118  REQUIRE(type_argument.subtype() == symbol_typet(expected.description));
119  return true;
120  }
121  }
122  // Should be unreachable...
123  REQUIRE(false);
124  return false;
125 }
126 
131 {
132  REQUIRE(is_java_generic_type(type));
133  return to_java_generic_type(type);
134 }
135 
149  const typet &type,
150  const require_type::expected_type_argumentst &type_expectations)
151 {
152  const java_generic_typet &generic_type =
154 
155  const java_generic_typet::generic_type_argumentst &generic_type_arguments =
156  generic_type.generic_type_arguments();
157  REQUIRE(generic_type_arguments.size() == type_expectations.size());
158  REQUIRE(
159  std::equal(
160  generic_type_arguments.begin(),
161  generic_type_arguments.end(),
162  type_expectations.begin(),
164 
165  return generic_type;
166 }
167 
173 {
174  REQUIRE(is_java_generic_parameter(type));
175  return to_java_generic_parameter(type);
176 }
177 
185  const typet &type,
186  const irep_idt &parameter)
187 {
188  const java_generic_parametert &generic_param =
190 
191  REQUIRE(
193  generic_param, {require_type::type_argument_kindt::Var, parameter}));
194 
195  return generic_param;
196 }
197 
204  const typet &type,
205  const optionalt<symbol_typet> &expect_subtype)
206 {
207  REQUIRE(!is_java_generic_parameter(type));
208  REQUIRE(!is_java_generic_type(type));
209  if(expect_subtype)
210  REQUIRE(type.subtype() == expect_subtype.value());
211  return type;
212 }
213 
218 {
219  REQUIRE(class_type.id() == ID_struct);
220 
221  const class_typet &class_class_type = to_class_type(class_type);
222  REQUIRE(class_class_type.is_class());
223  REQUIRE_FALSE(class_class_type.get_bool(ID_incomplete_class));
224 
225  return class_class_type;
226 }
227 
232 {
233  REQUIRE(class_type.id() == ID_struct);
234 
235  const class_typet &class_class_type = to_class_type(class_type);
236  REQUIRE(class_class_type.is_class());
237  REQUIRE(class_class_type.get_bool(ID_incomplete_class));
238 
239  return class_class_type;
240 }
241 
247 {
248  REQUIRE(class_type.id() == ID_struct);
249 
250  const class_typet &class_class_type = to_class_type(class_type);
251  const java_class_typet &java_class_type =
252  to_java_class_type(class_class_type);
253 
254  REQUIRE(is_java_generic_class_type(java_class_type));
255  const java_generic_class_typet &java_generic_class_type =
256  to_java_generic_class_type(java_class_type);
257 
258  return java_generic_class_type;
259 }
260 
267  const typet &class_type,
268  const std::initializer_list<irep_idt> &type_variables)
269 {
270  const java_generic_class_typet java_generic_class_type =
271  require_java_generic_class(class_type);
272 
273  const java_generic_class_typet::generic_typest &generic_type_vars =
274  java_generic_class_type.generic_types();
275  REQUIRE(generic_type_vars.size() == type_variables.size());
276  REQUIRE(
277  std::equal(
278  type_variables.begin(),
279  type_variables.end(),
280  generic_type_vars.begin(),
281  [](
282  const irep_idt &type_var_name,
283  const java_generic_parametert &param) { //NOLINT
284  REQUIRE(is_java_generic_parameter(param));
285  return param.type_variable().get_identifier() == type_var_name;
286  }));
287 
288  return java_generic_class_type;
289 }
290 
296 {
297  require_complete_class(class_type);
298  return require_java_generic_class(class_type);
299 }
300 
307  const typet &class_type,
308  const std::initializer_list<irep_idt> &type_variables)
309 {
311  return require_java_generic_class(class_type, type_variables);
312 }
313 
319 {
320  REQUIRE(class_type.id() == ID_struct);
321 
322  const class_typet &class_class_type = to_class_type(class_type);
323  const java_class_typet &java_class_type =
324  to_java_class_type(class_class_type);
325 
326  REQUIRE(is_java_implicitly_generic_class_type(java_class_type));
328  &java_implicitly_generic_class_type =
329  to_java_implicitly_generic_class_type(java_class_type);
330 
331  return java_implicitly_generic_class_type;
332 }
333 
341  const typet &class_type,
342  const std::initializer_list<irep_idt> &implicit_type_variables)
343 {
345  &java_implicitly_generic_class_type =
347 
349  &implicit_generic_type_vars =
350  java_implicitly_generic_class_type.implicit_generic_types();
351  REQUIRE(implicit_generic_type_vars.size() == implicit_type_variables.size());
352  REQUIRE(
353  std::equal(
354  implicit_type_variables.begin(),
355  implicit_type_variables.end(),
356  implicit_generic_type_vars.begin(),
357  [](
358  const irep_idt &type_var_name,
359  const java_generic_parametert &param) { //NOLINT
360  REQUIRE(is_java_generic_parameter(param));
361  return param.type_variable().get_identifier() == type_var_name;
362  }));
363 
364  return java_implicitly_generic_class_type;
365 }
366 
372  const typet &class_type)
373 {
374  require_complete_class(class_type);
375  return require_java_implicitly_generic_class(class_type);
376 }
377 
385  const typet &class_type,
386  const std::initializer_list<irep_idt> &implicit_type_variables)
387 {
388  require_complete_class(class_type);
390  class_type, implicit_type_variables);
391 }
392 
398 {
399  REQUIRE(class_type.id() == ID_struct);
400 
401  const class_typet &class_class_type = to_class_type(class_type);
402  const java_class_typet &java_class_type =
403  to_java_class_type(class_class_type);
404 
405  REQUIRE(!is_java_generic_class_type(java_class_type));
406  REQUIRE(!is_java_implicitly_generic_class_type(java_class_type));
407 
408  return java_class_type;
409 }
410 
416 {
417  require_complete_class(class_type);
418  return require_java_non_generic_class(class_type);
419 }
420 
425 const symbol_typet &
426 require_type::require_symbol(const typet &type, const irep_idt &identifier)
427 {
428  REQUIRE(type.id() == ID_symbol);
429  const symbol_typet &result = to_symbol_type(type);
430  if(identifier != "")
431  {
432  REQUIRE(result.get_identifier() == identifier);
433  }
434  return result;
435 }
436 
442  const typet &type,
443  const std::string &identifier)
444 {
445  symbol_typet symbol_type = require_symbol(type, identifier);
446  REQUIRE(is_java_generic_symbol_type(type));
447  return to_java_generic_symbol_type(type);
448 }
449 
464  const typet &type,
465  const std::string &identifier,
466  const require_type::expected_type_argumentst &type_expectations)
467 {
468  const java_generic_symbol_typet &generic_base_type =
469  require_java_generic_symbol_type(type, identifier);
470 
471  const java_generic_typet::generic_type_argumentst &generic_type_arguments =
472  generic_base_type.generic_types();
473  REQUIRE(generic_type_arguments.size() == type_expectations.size());
474  REQUIRE(
475  std::equal(
476  generic_type_arguments.begin(),
477  generic_type_arguments.end(),
478  type_expectations.begin(),
480 
481  return generic_base_type;
482 }
483 
492  const java_class_typet &class_type,
493  const std::vector<std::string> &expected_identifiers)
494 {
495  const require_type::java_lambda_method_handlest &lambda_method_handles =
496  class_type.lambda_method_handles();
497  REQUIRE(lambda_method_handles.size() == expected_identifiers.size());
498 
499  REQUIRE(
500  std::equal(
501  lambda_method_handles.begin(),
502  lambda_method_handles.end(),
503  expected_identifiers.begin(),
504  [](
505  const symbol_exprt &lambda_method_handle,
506  const std::string &expected_identifier) { //NOLINT
507  return lambda_method_handle.get_identifier() == expected_identifier;
508  }));
509  return lambda_method_handles;
510 }
The type of an expression.
Definition: type.h:22
java_generic_class_typet require_complete_java_generic_class(const typet &class_type)
Verify that a class is a complete, valid java generic class.
std::vector< java_generic_parametert > implicit_generic_typest
Definition: java_types.h:473
Base type of functions.
Definition: std_types.h:764
const java_lambda_method_handlest & lambda_method_handles() const
Definition: java_types.h:126
bool is_java_generic_symbol_type(const typet &type)
Definition: java_types.h:613
java_generic_symbol_typet require_java_generic_symbol_type(const typet &type, const std::string &identifier)
Verify a given type is a java generic symbol type.
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
Definition: java_types.h:406
const typet & require_java_non_generic_type(const typet &type, const optionalt< symbol_typet > &expect_subtype)
Test a type to ensure it is not a java generics type.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
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:281
const irep_idt & get_identifier() const
Definition: std_expr.h:128
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:288
const componentst & components() const
Definition: std_types.h:245
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.
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
Definition: std_types.h:435
Structure type.
Definition: std_types.h:297
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.
std::initializer_list< expected_type_argumentt > expected_type_argumentst
Definition: require_type.h:55
java_class_typet::java_lambda_method_handlest java_lambda_method_handlest
Definition: require_type.h:120
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:330
const irep_idt & id() const
Definition: irep.h:189
const java_generic_symbol_typet & to_java_generic_symbol_type(const typet &type)
Definition: java_types.h:621
const type_variablet & type_variable() const
Definition: java_types.h:247
std::vector< reference_typet > generic_type_argumentst
Definition: java_types.h:321
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition: java_types.h:375
A reference into the symbol table.
Definition: std_types.h:110
java_generic_parametert require_java_generic_parameter(const typet &type)
Verify a given type is a java_generic_parameter, e.g., T
The pointer type.
Definition: std_types.h:1426
nonstd::optional< T > optionalt
Definition: optional.h:35
const java_implicitly_generic_class_typet & to_java_implicitly_generic_class_type(const java_class_typet &type)
Definition: java_types.h:511
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.
class_typet require_complete_class(const typet &class_type)
Checks that the given type is a complete class.
const symbol_typet & require_symbol(const typet &type, const irep_idt &identifier="")
Verify a given type is a symbol type, optionally with a specific identifier.
java_generic_typet require_java_generic_type(const typet &type)
Verify a given type is a java_generic_type.
java_class_typet require_complete_java_non_generic_class(const typet &class_type)
Verify that a class is a complete, valid nongeneric java class.
const generic_typest & generic_types() const
Definition: java_types.h:597
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:398
symbol_exprt require_symbol(const exprt &expr, const irep_idt &symbol_name)
Verify a given exprt is an symbol_exprt with a identifier name equal to the symbol_name.
Type for a generic symbol, extends symbol_typet with a vector of java generic types.
Definition: java_types.h:587
java_generic_class_typet require_java_generic_class(const typet &class_type)
Verify that a class is a valid java generic class.
const implicit_generic_typest & implicit_generic_types() const
Definition: java_types.h:487
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.
java_class_typet require_java_non_generic_class(const typet &class_type)
Verify that a class is a valid nongeneric java class.
The reference type.
Definition: std_types.h:1483
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:318
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:353
const parameterst & parameters() const
Definition: std_types.h:905
pointer_typet require_pointer(const typet &type, const optionalt< typet > &subtype)
Checks a type is a pointer type optionally with a specific subtype.
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>...
Definition: java_types.h:232
code_typet require_code(const typet &type)
Checks a type is a code_type (i.e.
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool is_java_generic_type(const typet &type)
Definition: java_types.h:346
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
class_typet require_incomplete_class(const typet &class_type)
Checks that the given type is an incomplete class.
Base Type Computation.
const typet & subtype() const
Definition: type.h:33
C++ class type.
Definition: std_types.h:341
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.
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:503
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:470
Helper functions for requiring specific types If the type is of the wrong type, throw a CATCH excepti...
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:163
const irep_idt & get_identifier() const
Definition: std_types.h:123
const generic_typest & generic_types() const
Definition: java_types.h:385
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.
std::vector< java_generic_parametert > generic_typest
Definition: java_types.h:378