cprover
require_type.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Unit test utilities
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
9#include "require_type.h"
10
12
19 const typet &type,
20 const optionalt<typet> &subtype)
21{
22 REQUIRE(type.id() == ID_pointer);
23 const pointer_typet &pointer = to_pointer_type(type);
24
25 if(subtype)
26 REQUIRE(pointer.subtype() == subtype.value());
27
28 return pointer;
29}
30
36 const java_class_typet &java_class_type,
37 const irep_idt &component_name)
38{
39 const auto &component = std::find_if(
40 java_class_type.components().begin(),
41 java_class_type.components().end(),
42 [&component_name](const java_class_typet::componentt &component) {
43 return component.get_name() == component_name;
44 });
45
46 REQUIRE(component != java_class_type.components().end());
47 return *component;
48}
49
55 const struct_typet &struct_type,
56 const irep_idt &component_name)
57{
58 const auto &componet = std::find_if(
59 struct_type.components().begin(),
60 struct_type.components().end(),
61 [&component_name](const struct_union_typet::componentt &component) {
62 return component.get_name() == component_name;
63 });
64
65 REQUIRE(componet != struct_type.components().end());
66 return *componet;
67}
68
73{
74 REQUIRE(type.id() == ID_code);
75 return to_code_type(type);
76}
77
85require_type::require_code(const typet &type, const size_t num_params)
86{
87 code_typet code_type = require_code(type);
88 REQUIRE(code_type.parameters().size() == num_params);
89 return code_type;
90}
91
96{
98 return to_java_method_type(type);
99}
100
108require_type::require_java_method(const typet &type, const size_t num_params)
109{
110 java_method_typet method_type = require_java_method(type);
111 REQUIRE(method_type.parameters().size() == num_params);
112 return method_type;
113}
114
121 const code_typet &function_type,
122 const irep_idt &param_name)
123{
124 const auto param = std::find_if(
125 function_type.parameters().begin(),
126 function_type.parameters().end(),
127 [&param_name](const code_typet::parametert param) {
128 return param.get_base_name() == param_name;
129 });
130
131 REQUIRE(param != function_type.parameters().end());
132 return *param;
133}
134
141 const reference_typet &type_argument,
143{
144 switch(expected.kind)
145 {
147 {
148 REQUIRE(is_java_generic_parameter(type_argument));
149 java_generic_parametert parameter =
150 to_java_generic_parameter(type_argument);
151 REQUIRE(parameter.type_variable().get_identifier() == expected.description);
152 return true;
153 }
155 {
156 REQUIRE(!is_java_generic_parameter(type_argument));
157 REQUIRE(
158 to_struct_tag_type(type_argument.subtype()).get_identifier() ==
159 expected.description);
160 return true;
161 }
162 }
163 // Should be unreachable...
164 REQUIRE(false);
165 return false;
166}
167
172{
173 REQUIRE(is_java_generic_type(type));
174 return to_java_generic_type(type);
175}
176
190 const typet &type,
191 const require_type::expected_type_argumentst &type_expectations)
192{
193 const java_generic_typet &generic_type =
195
196 const java_generic_typet::generic_type_argumentst &generic_type_arguments =
197 generic_type.generic_type_arguments();
198 REQUIRE(generic_type_arguments.size() == type_expectations.size());
199 REQUIRE(
200 std::equal(
201 generic_type_arguments.begin(),
202 generic_type_arguments.end(),
203 type_expectations.begin(),
205
206 return generic_type;
207}
208
214{
215 REQUIRE(is_java_generic_parameter(type));
216 return to_java_generic_parameter(type);
217}
218
226 const typet &type,
227 const irep_idt &parameter)
228{
229 const java_generic_parametert &generic_param =
231
232 REQUIRE(
234 generic_param, {require_type::type_argument_kindt::Var, parameter}));
235
236 return generic_param;
237}
238
245 const typet &type,
246 const optionalt<struct_tag_typet> &expect_subtype)
247{
248 REQUIRE(!is_java_generic_parameter(type));
249 REQUIRE(!is_java_generic_type(type));
250 if(expect_subtype)
251 REQUIRE(type.subtype() == expect_subtype.value());
252 return type;
253}
254
259{
260 REQUIRE(class_type.id() == ID_struct);
261
262 const java_class_typet &java_class_type = to_java_class_type(class_type);
263 REQUIRE(java_class_type.is_class());
264 REQUIRE_FALSE(java_class_type.get_is_stub());
265
266 return java_class_type;
267}
268
273{
274 REQUIRE(class_type.id() == ID_struct);
275
276 const java_class_typet &java_class_type = to_java_class_type(class_type);
277 REQUIRE(java_class_type.is_class());
278 REQUIRE(java_class_type.get_is_stub());
279
280 return java_class_type;
281}
282
288{
289 REQUIRE(class_type.id() == ID_struct);
290
291 const class_typet &class_class_type = to_class_type(class_type);
292 const java_class_typet &java_class_type =
293 to_java_class_type(class_class_type);
294
295 REQUIRE(is_java_generic_class_type(java_class_type));
296 const java_generic_class_typet &java_generic_class_type =
297 to_java_generic_class_type(java_class_type);
298
299 return java_generic_class_type;
300}
301
308 const typet &class_type,
309 const std::initializer_list<irep_idt> &type_variables)
310{
311 const java_generic_class_typet java_generic_class_type =
312 require_java_generic_class(class_type);
313
314 const java_generic_class_typet::generic_typest &generic_type_vars =
315 java_generic_class_type.generic_types();
316 REQUIRE(generic_type_vars.size() == type_variables.size());
317 REQUIRE(
318 std::equal(
319 type_variables.begin(),
320 type_variables.end(),
321 generic_type_vars.begin(),
322 [](
323 const irep_idt &type_var_name,
324 const java_generic_parametert &param) { //NOLINT
325 REQUIRE(is_java_generic_parameter(param));
326 return param.type_variable().get_identifier() == type_var_name;
327 }));
328
329 return java_generic_class_type;
330}
331
337{
338 require_complete_class(class_type);
339 return require_java_generic_class(class_type);
340}
341
348 const typet &class_type,
349 const std::initializer_list<irep_idt> &type_variables)
350{
352 return require_java_generic_class(class_type, type_variables);
353}
354
360{
361 REQUIRE(class_type.id() == ID_struct);
362
363 const class_typet &class_class_type = to_class_type(class_type);
364 const java_class_typet &java_class_type =
365 to_java_class_type(class_class_type);
366
367 REQUIRE(is_java_implicitly_generic_class_type(java_class_type));
369 &java_implicitly_generic_class_type =
371
372 return java_implicitly_generic_class_type;
373}
374
382 const typet &class_type,
383 const std::initializer_list<irep_idt> &implicit_type_variables)
384{
386 &java_implicitly_generic_class_type =
388
390 &implicit_generic_type_vars =
391 java_implicitly_generic_class_type.implicit_generic_types();
392 REQUIRE(implicit_generic_type_vars.size() == implicit_type_variables.size());
393 auto param = implicit_generic_type_vars.begin();
394 auto type_var_name = implicit_type_variables.begin();
395 for(; param != implicit_generic_type_vars.end(); ++param, ++type_var_name)
396 {
397 REQUIRE(is_java_generic_parameter(*param));
398 REQUIRE(param->type_variable().get_identifier() == *type_var_name);
399 }
400 return java_implicitly_generic_class_type;
401}
402
408 const typet &class_type)
409{
410 require_complete_class(class_type);
411 return require_java_implicitly_generic_class(class_type);
412}
413
421 const typet &class_type,
422 const std::initializer_list<irep_idt> &implicit_type_variables)
423{
424 require_complete_class(class_type);
426 class_type, implicit_type_variables);
427}
428
434{
435 REQUIRE(class_type.id() == ID_struct);
436
437 const class_typet &class_class_type = to_class_type(class_type);
438 const java_class_typet &java_class_type =
439 to_java_class_type(class_class_type);
440
441 REQUIRE(!is_java_generic_class_type(java_class_type));
442 REQUIRE(!is_java_implicitly_generic_class_type(java_class_type));
443
444 return java_class_type;
445}
446
452{
453 require_complete_class(class_type);
454 return require_java_non_generic_class(class_type);
455}
456
461const struct_tag_typet &
462require_type::require_struct_tag(const typet &type, const irep_idt &identifier)
463{
464 REQUIRE(type.id() == ID_struct_tag);
465 const struct_tag_typet &result = to_struct_tag_type(type);
466 if(!identifier.empty())
467 {
468 REQUIRE(result.get_identifier() == identifier);
469 }
470 return result;
471}
472
475{
476 const auto pointer_type = require_type::require_pointer(type, {});
478 return pointer_type;
479}
480
487 const typet &type,
488 const std::string &identifier)
489{
490 struct_tag_typet struct_tag_type = require_struct_tag(type, identifier);
491 REQUIRE(is_java_generic_struct_tag_type(type));
493}
494
510 const typet &type,
511 const std::string &identifier,
512 const require_type::expected_type_argumentst &type_expectations)
513{
514 const java_generic_struct_tag_typet &generic_base_type =
515 require_java_generic_struct_tag_type(type, identifier);
516
517 const java_generic_typet::generic_type_argumentst &generic_type_arguments =
518 generic_base_type.generic_types();
519 REQUIRE(generic_type_arguments.size() == type_expectations.size());
520 REQUIRE(
521 std::equal(
522 generic_type_arguments.begin(),
523 generic_type_arguments.end(),
524 type_expectations.begin(),
526
527 return generic_base_type;
528}
529
538 const java_class_typet &class_type,
539 const std::vector<std::string> &expected_identifiers)
540{
541 const require_type::java_lambda_method_handlest &lambda_method_handles =
542 class_type.lambda_method_handles();
543 REQUIRE(lambda_method_handles.size() == expected_identifiers.size());
544
545 REQUIRE(std::equal(
546 lambda_method_handles.begin(),
547 lambda_method_handles.end(),
548 expected_identifiers.begin(),
549 [](
551 const std::string &expected_identifier) { //NOLINT
552 return lambda_method_handle.get_lambda_method_descriptor()
553 .get_identifier() == expected_identifier;
554 }));
555 return lambda_method_handles;
556}
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
Class type.
Definition: std_types.h:325
Base type of functions.
Definition: std_types.h:539
const parameterst & parameters() const
Definition: std_types.h:655
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
const irep_idt & id() const
Definition: irep.h:396
Represents a lambda call to a method.
Definition: java_types.h:482
bool get_is_stub() const
Definition: java_types.h:398
const componentst & components() const
Definition: java_types.h:224
const java_lambda_method_handlest & lambda_method_handles() const
Definition: java_types.h:517
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
std::vector< java_generic_parametert > generic_typest
Definition: java_types.h:975
const generic_typest & generic_types() const
Definition: java_types.h:982
Reference that points to a java_generic_parameter_tagt.
Definition: java_types.h:776
const type_variablet & type_variable() const
Definition: java_types.h:789
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:858
const generic_typest & generic_types() const
Definition: java_types.h:873
Reference that points to a java_generic_struct_tag_typet.
Definition: java_types.h:915
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:926
java_generic_struct_tag_typet::generic_typest generic_type_argumentst
Definition: java_types.h:917
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
const implicit_generic_typest & implicit_generic_types() const
Definition: java_types.h:1084
std::vector< java_generic_parametert > implicit_generic_typest
Definition: java_types.h:1070
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
The reference type.
Definition: pointer_expr.h:107
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
Structure type, corresponds to C style structs.
Definition: std_types.h:231
bool is_class() const
A struct may be a class, where members may have access restrictions.
Definition: std_types.h:245
const componentst & components() const
Definition: std_types.h:147
const irep_idt & get_identifier() const
Definition: std_types.h:410
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:184
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:954
const java_generic_struct_tag_typet & to_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:897
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:582
bool is_java_generic_type(const typet &type)
Definition: java_types.h:947
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:820
bool can_cast_type< java_method_typet >(const typet &type)
Definition: java_types.h:179
const java_implicitly_generic_class_typet & to_java_implicitly_generic_class_type(const java_class_typet &type)
Definition: java_types.h:1108
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:827
bool is_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:889
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:995
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:1100
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
Definition: java_types.h:1003
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)
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_incomplete_class(const typet &class_type)
Checks that the given type is an incomplete class.
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.
pointer_typet require_pointer_to_tag(const typet &type, const irep_idt &identifier=irep_idt())
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_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.
java_generic_typet require_java_generic_type(const typet &type)
Verify a given type is a java_generic_type.
pointer_typet require_pointer(const typet &type, const optionalt< typet > &subtype)
Checks a type is a pointer type optionally with a specific subtype.
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.
std::initializer_list< expected_type_argumentt > expected_type_argumentst
Definition: require_type.h:66
class_typet require_complete_class(const typet &class_type)
Checks that the given type is a complete class.
java_class_typet::java_lambda_method_handlest java_lambda_method_handlest
Definition: require_type.h:131
java_generic_parametert require_java_generic_parameter(const typet &type)
Verify a given type is a java_generic_parameter, e.g., T
java_class_typet require_complete_java_non_generic_class(const typet &class_type)
Verify that a class is a complete, valid nongeneric java class.
java_generic_class_typet require_java_generic_class(const typet &class_type)
Verify that a class is a valid 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.
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.
java_class_typet require_java_non_generic_class(const typet &class_type)
Verify that a class is a valid nongeneric java class.
code_typet require_code(const typet &type)
Checks a type is a code_type (i.e.
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.
java_method_typet require_java_method(const typet &type)
Checks a type is a java_method_typet (i.e.
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.
nonstd::optional< T > optionalt
Definition: optional.h:35
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
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.
Helper functions for requiring specific types If the type is of the wrong type, throw a CATCH excepti...
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:381