diff --git a/unit/testing-utils/require_type.cpp b/unit/testing-utils/require_type.cpp index 882f39005c4..9d8233a52d8 100644 --- a/unit/testing-utils/require_type.cpp +++ b/unit/testing-utils/require_type.cpp @@ -59,11 +59,26 @@ code_typet require_type::require_code(const typet &type) return to_code_type(type); } +/// Verify a given type is an code_typet, and that the code it represents +/// accepts a given number of parameters +/// \param type The type to check +/// \param num_params check the the given code_typet expects this +/// number of parameters +/// \return The type cast to a code_typet +code_typet require_type::require_code( + const typet &type, + const size_t num_params) +{ + code_typet code_type=require_code(type); + REQUIRE(code_type.parameters().size()==num_params); + return code_type; +} + /// Verify that a function has a parameter of a specific name. /// \param function_type: The type of the function /// \param param_name: The name of the parameter /// \return: A reference to the parameter structure corresponding to this -/// parameter name. +/// parameter name. code_typet::parametert require_type::require_parameter( const code_typet &function_type, const irep_idt ¶m_name) @@ -78,3 +93,111 @@ code_typet::parametert require_type::require_parameter( REQUIRE(param != function_type.parameters().end()); return *param; } + +/// Helper function for testing that java_generic_parametert types match +/// a given expectation. +/// \param param The generic parameter to test +/// \param expected The expected value of the parameter +/// \return true if the generic parameter type meets the expectations +bool require_java_generic_parametert_expectation( + const java_generic_parametert ¶m, + const require_type::expected_type_parametert &expected) +{ + switch(expected.kind) + { + case require_type::type_parameter_kindt::Var: + REQUIRE(!is_java_generic_inst_parameter((param))); + REQUIRE(param.type_variable().get_identifier()==expected.description); + return true; + case require_type::type_parameter_kindt::Inst: + REQUIRE(is_java_generic_inst_parameter((param))); + REQUIRE(param.subtype()==symbol_typet(expected.description)); + return true; + } + // Should be unreachable... + REQUIRE(false); + return false; +} + + +/// Verify a given type is a java_generic_type, optionally checking +/// that it's associated type variables match a given set of identifiers. +/// Expected usage is something like this: +/// +/// require_java_generic_type(type, +/// {{Inst,"java::java.lang.Integer"},{Var,"T"}}) +/// +/// \param type The type to check +/// \param type_expectations An optional set of type variable kinds +/// and identifiers which should be expected as the type parameters of the +/// given generic type. +/// \return The given type, cast to a java_generic_typet +java_generic_typet require_type::require_java_generic_type( + const typet &type, + const optionalt &type_expectations) +{ + REQUIRE(is_java_generic_type(type)); + const java_generic_typet &generic_type=to_java_generic_type(type); + if(type_expectations) + { + const java_generic_typet::generic_type_variablest &generic_type_vars= + generic_type.generic_type_variables(); + REQUIRE(generic_type_vars.size()==type_expectations->size()); + REQUIRE( + std::equal( + generic_type_vars.begin(), + generic_type_vars.end(), + type_expectations->begin(), + require_java_generic_parametert_expectation)); + } + + return generic_type; +} + +/// Verify a given type is a java_generic_parameter, optionally checking +/// that it's associated type variables match a given set of expectations. +/// Expected usage is something like this: +/// +/// require_java_generic_parameter(parameter, {Inst,"java::java.lang.Integer"}) +/// +/// or +/// +/// require_java_generic_parameter(parameter, {Var,"T"}) +/// +/// \param type The type to check +/// \param type_expectation An optional description of the identifiers/kinds +/// which / should be expected as the type parameter of the generic parameter. +/// \return The given type, cast to a java_generic_parametert +java_generic_parametert require_type::require_java_generic_parameter( + const typet &type, + const optionalt &type_expectation) +{ + REQUIRE(is_java_generic_parameter(type)); + const java_generic_parametert &generic_param=to_java_generic_parameter(type); + if(type_expectation) + { + REQUIRE( + require_java_generic_parametert_expectation( + generic_param, + type_expectation.value())); + } + + return generic_param; +} + +/// Test a type to ensure it is not a java generics type. +/// \param type The type to test +/// \param expect_subtype Optionally, also test that the subtype of the given +/// type matches this parameter +/// \return The value passed in the first argument +const typet &require_type::require_java_non_generic_type( + const typet &type, + const optionalt &expect_subtype) +{ + REQUIRE(!is_java_generic_parameter(type)); + REQUIRE(!is_java_generic_type(type)); + REQUIRE(!is_java_generic_inst_parameter(type)); + if(expect_subtype) + REQUIRE(type.subtype()==expect_subtype.value()); + return type; +} diff --git a/unit/testing-utils/require_type.h b/unit/testing-utils/require_type.h index 488abb5da44..215f5335cf0 100644 --- a/unit/testing-utils/require_type.h +++ b/unit/testing-utils/require_type.h @@ -17,6 +17,8 @@ #include #include +#include + // NOLINTNEXTLINE(readability/namespace) namespace require_type @@ -29,8 +31,37 @@ struct_typet::componentt require_component( const irep_idt &component_name); code_typet require_code(const typet &type); + code_typet::parametert require_parameter(const code_typet &function_type, const irep_idt ¶m_name); + +code_typet require_code( + const typet &type, + const size_t num_params); + +// A mini DSL for describing an expected set of type parameters for a +// java_generic_typet +enum class type_parameter_kindt { Inst, Var }; +struct expected_type_parametert +{ + type_parameter_kindt kind; + irep_idt description; +}; +typedef std::initializer_list + expected_type_parameterst; + +java_generic_typet require_java_generic_type( + const typet &type, + const optionalt &type_expectations); + + +java_generic_parametert require_java_generic_parameter( + const typet &type, + const optionalt &type_expectation); + +const typet &require_java_non_generic_type( + const typet &type, + const optionalt &expect_subtype); } -#endif +#endif // CPROVER_TESTING_UTILS_REQUIRE_TYPE_H