From f1bd41ea4387c551d659810ca8df2de5d0150ced Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Wed, 1 Aug 2018 16:59:23 +0100 Subject: [PATCH 01/11] Change code_typet to java_method_typet in jbmc --- jbmc/src/java_bytecode/ci_lazy_methods.cpp | 2 +- jbmc/src/java_bytecode/expr2java.cpp | 18 ++-- .../java_bytecode_convert_class.cpp | 4 +- .../java_bytecode_convert_method.cpp | 54 ++++++------ .../java_bytecode_instrument.cpp | 4 +- .../java_bytecode/java_bytecode_language.cpp | 2 +- .../java_bytecode/java_bytecode_parser.cpp | 2 +- .../java_bytecode/java_bytecode_typecheck.h | 2 + .../java_bytecode_typecheck_type.cpp | 9 +- jbmc/src/java_bytecode/java_entry_point.cpp | 26 +++--- .../src/java_bytecode/java_object_factory.cpp | 2 +- .../java_static_initializers.cpp | 4 +- .../java_string_library_preprocess.cpp | 51 +++++------ .../java_string_library_preprocess.h | 32 +++---- jbmc/src/java_bytecode/java_types.cpp | 10 +-- jbmc/src/java_bytecode/java_types.h | 6 +- jbmc/src/java_bytecode/java_utils.cpp | 3 +- jbmc/src/java_bytecode/java_utils.h | 4 +- .../java_bytecode/simple_method_stubbing.cpp | 2 +- jbmc/unit/java-testing-utils/require_type.cpp | 20 ++--- jbmc/unit/java-testing-utils/require_type.h | 9 +- ...ove_virtual_functions_without_fallback.cpp | 5 +- .../convert_initalizers.cpp | 6 +- .../convert_method.cpp | 4 +- .../parse_bounded_generic_inner_classes.cpp | 4 +- .../parse_functions_with_generics.cpp | 28 +++--- ...neric_class_with_generic_inner_classes.cpp | 42 ++++----- .../parse_generic_functions.cpp | 88 +++++++++---------- .../parse_nested_generics.cpp | 52 +++++------ .../parse_signature_descriptor_mismatch.cpp | 16 ++-- .../java_bytecode/load_method_by_regex.cpp | 2 +- .../string_refinement/dependency_graph.cpp | 10 +-- .../string_symbol_resolution.cpp | 2 +- jbmc/unit/util/parameter_indices.cpp | 4 +- 34 files changed, 272 insertions(+), 257 deletions(-) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 18be0320498..dd7a161e303 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -376,7 +376,7 @@ void ci_lazy_methodst::initialize_instantiated_classes( for(const auto &mname : entry_points) { const auto &symbol=ns.lookup(mname); - const auto &mtype=to_code_type(symbol.type); + const auto &mtype = to_java_method_type(symbol.type); for(const auto ¶m : mtype.parameters()) { if(param.type().id()==ID_pointer) diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index 69518dd1c45..f6e8d87ebe3 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/jbmc/src/java_bytecode/expr2java.cpp @@ -56,11 +56,10 @@ std::string expr2javat::convert_code_function_call( dest+='='; } - const code_typet &code_type= - to_code_type(src.function().type()); + const java_method_typet &code_type = + to_java_method_type(src.function().type()); - bool has_this=code_type.has_this() && - !src.arguments().empty(); + bool has_this = code_type.has_this() && !src.arguments().empty(); if(has_this) { @@ -284,7 +283,7 @@ std::string expr2javat::convert_rec( return q+"byte"+d; else if(src.id()==ID_code) { - const code_typet &code_type=to_code_type(src); + const java_method_typet &code_type = to_java_method_type(src); // Java doesn't really have syntax for function types, // so we make one up, loosely inspired by the syntax @@ -293,11 +292,10 @@ std::string expr2javat::convert_rec( std::string dest=""; dest+='('; - const code_typet::parameterst ¶meters=code_type.parameters(); + const java_method_typet::parameterst ¶meters = code_type.parameters(); - for(code_typet::parameterst::const_iterator - it=parameters.begin(); - it!=parameters.end(); + for(java_method_typet::parameterst::const_iterator it = parameters.begin(); + it != parameters.end(); it++) { if(it!=parameters.begin()) @@ -315,7 +313,7 @@ std::string expr2javat::convert_rec( dest+=')'; - const typet &return_type=code_type.return_type(); + const typet &return_type = code_type.return_type(); dest+=" -> "+convert(return_type); return q + dest; diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 3c85b9c7401..e92d1906167 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -781,12 +781,12 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) const irep_idt clone_name= id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;"; - code_typet::parametert this_param; + java_method_typet::parametert this_param; this_param.set_identifier(id2string(clone_name)+"::this"); this_param.set_base_name("this"); this_param.set_this(); this_param.type()=java_reference_type(symbol_type); - const code_typet clone_type({this_param}, java_lang_object_type()); + const java_method_typet clone_type({this_param}, java_lang_object_type()); parameter_symbolt this_symbol; this_symbol.name=this_param.get_identifier(); diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 21cac212cd4..7841f503b0f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -87,11 +87,11 @@ class patternt /// parameters, which are initially nameless as method conversion hasn't /// happened. Also creates symbols in `symbol_table`. static void assign_parameter_names( - code_typet &ftype, + java_method_typet &ftype, const irep_idt &name_prefix, symbol_table_baset &symbol_table) { - code_typet::parameterst ¶meters=ftype.parameters(); + java_method_typet::parameterst ¶meters = ftype.parameters(); // Mostly borrowed from java_bytecode_convert.cpp; maybe factor this out. // assign names to parameters @@ -255,7 +255,7 @@ const exprt java_bytecode_convert_methodt::variable( /// message handler to collect warnings /// \return /// the constructed member type -code_typet member_type_lazy( +java_method_typet member_type_lazy( const std::string &descriptor, const optionalt &signature, const std::string &class_name, @@ -282,10 +282,11 @@ code_typet member_type_lazy( signature.value(), class_name); INVARIANT(member_type_from_signature.id()==ID_code, "Must be code type"); - if(to_code_type(member_type_from_signature).parameters().size()== - to_code_type(member_type_from_descriptor).parameters().size()) + if( + to_java_method_type(member_type_from_signature).parameters().size() == + to_java_method_type(member_type_from_descriptor).parameters().size()) { - return to_code_type(member_type_from_signature); + return to_java_method_type(member_type_from_signature); } else { @@ -306,7 +307,7 @@ code_typet member_type_lazy( << message.eom; } } - return to_code_type(member_type_from_descriptor); + return to_java_method_type(member_type_from_descriptor); } /// Retrieves the symbol of the lambda method associated with the given @@ -345,7 +346,7 @@ void java_bytecode_convert_method_lazy( { symbolt method_symbol; - code_typet member_type = member_type_lazy( + java_method_typet member_type = member_type_lazy( m.descriptor, m.signature, id2string(class_symbol.name), @@ -378,8 +379,8 @@ void java_bytecode_convert_method_lazy( // do we need to add 'this' as a parameter? if(!m.is_static) { - code_typet::parameterst ¶meters = member_type.parameters(); - code_typet::parametert this_p; + java_method_typet::parameterst ¶meters = member_type.parameters(); + java_method_typet::parametert this_p; const reference_typet object_ref_type= java_reference_type(symbol_typet(class_symbol.name)); this_p.type()=object_ref_type; @@ -442,12 +443,12 @@ void java_bytecode_convert_methodt::convert( symbolt &method_symbol=*symbol_table.get_writeable(method_identifier); - // Obtain a std::vector of code_typet::parametert objects from the + // Obtain a std::vector of java_method_typet::parametert objects from the // (function) type of the symbol java_method_typet method_type = to_java_method_type(method_symbol.type); method_type.set(ID_C_class, class_symbol.name); method_return_type = method_type.return_type(); - code_typet::parameterst ¶meters = method_type.parameters(); + java_method_typet::parameterst ¶meters = method_type.parameters(); // Determine the number of local variable slots used by the JVM to maintain // the formal parameters @@ -1250,9 +1251,10 @@ codet java_bytecode_convert_methodt::convert_instructions( id2string(arg0.get(ID_identifier))== "java::org.cprover.CProver.assume:(Z)V") { - const code_typet &code_type=to_code_type(arg0.type()); - INVARIANT(code_type.parameters().size()==1, - "function expected to have exactly one parameter"); + const java_method_typet &code_type = to_java_method_type(arg0.type()); + INVARIANT( + code_type.parameters().size() == 1, + "function expected to have exactly one parameter"); c = replace_call_to_cprover_assume(i_it->source_location, c); } // replace calls to CProver.atomicBegin @@ -1995,8 +1997,8 @@ codet java_bytecode_convert_methodt::convert_monitorenterexit( return code_skipt(); // becomes a function call - code_typet type( - {code_typet::parametert(java_reference_type(void_typet()))}, + java_method_typet type( + {java_method_typet::parametert(java_reference_type(void_typet()))}, void_typet()); code_function_callt call; call.function() = symbol_exprt(descriptor, type); @@ -2105,8 +2107,8 @@ void java_bytecode_convert_methodt::convert_invoke( const bool is_virtual( statement == "invokevirtual" || statement == "invokeinterface"); - code_typet &code_type = to_code_type(arg0.type()); - code_typet::parameterst ¶meters(code_type.parameters()); + java_method_typet &code_type = to_java_method_type(arg0.type()); + java_method_typet::parameterst ¶meters(code_type.parameters()); if(use_this) { @@ -2128,7 +2130,7 @@ void java_bytecode_convert_methodt::convert_invoke( code_type.set(ID_java_super_method_call, true); } reference_typet object_ref_type = java_reference_type(thistype); - code_typet::parametert this_p(object_ref_type); + java_method_typet::parametert this_p(object_ref_type); this_p.set_this(); this_p.set_base_name("this"); parameters.insert(parameters.begin(), this_p); @@ -2215,7 +2217,7 @@ void java_bytecode_convert_methodt::convert_invoke( symbol.value.make_nil(); symbol.mode = ID_java; assign_parameter_names( - to_code_type(symbol.type), symbol.name, symbol_table); + to_java_method_type(symbol.type), symbol.name, symbol_table); debug() << "Generating codet: new opaque symbol: method '" << symbol.name << "'" << eom; @@ -2945,7 +2947,7 @@ optionalt java_bytecode_convert_methodt::convert_invoke_dynamic( const source_locationt &location, const exprt &arg0) { - const code_typet &code_type = to_code_type(arg0.type()); + const java_method_typet &code_type = to_java_method_type(arg0.type()); const optionalt &lambda_method_symbol = get_lambda_method_symbol( lambda_method_handles, @@ -2958,7 +2960,7 @@ optionalt java_bytecode_convert_methodt::convert_invoke_dynamic( "type" << eom; - const code_typet::parameterst ¶meters(code_type.parameters()); + const java_method_typet::parameterst ¶meters(code_type.parameters()); pop(parameters.size()); @@ -3019,10 +3021,10 @@ void java_bytecode_initialize_parameter_names( &local_variable_table, symbol_table_baset &symbol_table) { - // Obtain a std::vector of code_typet::parametert objects from the + // Obtain a std::vector of java_method_typet::parametert objects from the // (function) type of the symbol - code_typet &code_type = to_code_type(method_symbol.type); - code_typet::parameterst ¶meters = code_type.parameters(); + java_method_typet &code_type = to_java_method_type(method_symbol.type); + java_method_typet::parameterst ¶meters = code_type.parameters(); // Find number of parameters unsigned slots_for_parameters = java_method_parameter_slots(code_type); diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp index 9eee6a4131d..ba6fcfd94ce 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp @@ -446,8 +446,8 @@ void java_bytecode_instrumentt::instrument_code(codet &code) add_expr_instrumentation(block, code_function_call.lhs()); add_expr_instrumentation(block, code_function_call.function()); - const code_typet &function_type= - to_code_type(code_function_call.function().type()); + const java_method_typet &function_type = + to_java_method_type(code_function_call.function().type()); // Check for a null this-argument of a virtual call: if(function_type.has_this()) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index a2cf076a131..8499e5913e6 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -1068,7 +1068,7 @@ bool java_bytecode_languaget::convert_single_method( // The return of an opaque function is a source of an otherwise invisible // instantiation, so here we ensure we've loaded the appropriate classes. - const code_typet function_type = to_code_type(symbol.type); + const java_method_typet function_type = to_java_method_type(symbol.type); if( const pointer_typet *pointer_return_type = type_try_dynamic_cast(function_type.return_type())) diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index ef41a7366f4..2f77e62492b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -610,7 +610,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src) { if(src.id()==ID_code) { - const code_typet &ct=to_code_type(src); + const java_method_typet &ct = to_java_method_type(src); const typet &rt=ct.return_type(); get_class_refs_rec(rt); for(const auto &p : ct.parameters()) diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck.h b/jbmc/src/java_bytecode/java_bytecode_typecheck.h index 9ac5611539e..4d56e105bf8 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck.h +++ b/jbmc/src/java_bytecode/java_bytecode_typecheck.h @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H +#include "java_types.h" + #include #include diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp index 2f26feb59bc..321a277bb73 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp @@ -38,13 +38,14 @@ void java_bytecode_typecheckt::typecheck_type(typet &type) } else if(type.id()==ID_code) { - code_typet &code_type=to_code_type(type); + java_method_typet &code_type = to_java_method_type(type); typecheck_type(code_type.return_type()); - code_typet::parameterst ¶meters=code_type.parameters(); + java_method_typet::parameterst ¶meters = code_type.parameters(); - for(code_typet::parameterst::iterator - it=parameters.begin(); it!=parameters.end(); it++) + for(java_method_typet::parameterst::iterator it = parameters.begin(); + it != parameters.end(); + it++) typecheck_type(it->type()); } } diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 5d14e771bb5..73fadb9b697 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -36,7 +36,7 @@ static void create_initialize(symbol_table_baset &symbol_table) initialize.base_name=INITIALIZE_FUNCTION; initialize.mode=ID_java; - initialize.type = code_typet({}, empty_typet()); + initialize.type = java_method_typet({}, empty_typet()); code_blockt init_code; @@ -251,12 +251,12 @@ static void java_static_lifetime_init( bool is_java_main(const symbolt &function) { bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD); - const code_typet &function_type = to_code_type(function.type); + const java_method_typet &function_type = to_java_method_type(function.type); const typet &string_array_type = java_type_from_string("[Ljava/lang/String;"); // checks whether the function is static and has a single String[] parameter bool is_static = !function_type.has_this(); // this should be implied by the signature - const code_typet::parameterst ¶meters = function_type.parameters(); + const java_method_typet::parameterst ¶meters = function_type.parameters(); bool has_correct_type = function_type.return_type().id() == ID_empty && parameters.size() == 1 && parameters[0].type().full_eq(string_array_type); @@ -281,8 +281,8 @@ exprt::operandst java_build_arguments( object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector) { - const code_typet::parameterst ¶meters= - to_code_type(function.type).parameters(); + const java_method_typet::parameterst ¶meters = + to_java_method_type(function.type).parameters(); exprt::operandst main_arguments; main_arguments.resize(parameters.size()); @@ -299,7 +299,7 @@ exprt::operandst java_build_arguments( param_numbertype); + const java_method_typet &type = to_java_method_type(func->type); code_function_callt fun_call; fun_call.function() = func->symbol_expr(); if(type.has_this()) diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index e486b38a9f3..b4daf706820 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -294,7 +294,7 @@ static void create_clinit_wrapper_symbols( // Create symbol for the "clinit_wrapper" symbolt wrapper_method_symbol; - const code_typet wrapper_method_type({}, void_typet()); + const java_method_typet wrapper_method_type({}, void_typet()); wrapper_method_symbol.name = clinit_wrapper_name(class_name); wrapper_method_symbol.pretty_name = wrapper_method_symbol.name; wrapper_method_symbol.base_name = "clinit_wrapper"; @@ -714,7 +714,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols( "a class cannot be both incomplete, and so have stub static fields, and " "also define a static initializer"); - const code_typet thunk_type({}, void_typet()); + const java_method_typet thunk_type({}, void_typet()); symbolt static_init_symbol; static_init_symbol.name = static_init_name; diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 21bc0451e7a..8a2b0f634f4 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -280,7 +280,7 @@ symbol_exprt java_string_library_preprocesst::fresh_array( /// added /// \return a list of expressions exprt::operandst java_string_library_preprocesst::process_parameters( - const code_typet::parameterst ¶ms, + const java_method_typet::parameterst ¶ms, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code) @@ -956,7 +956,7 @@ java_string_library_preprocesst::string_literal_to_string_expr( /// return false /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_equals_function_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) @@ -1011,13 +1011,13 @@ codet java_string_library_preprocesst::make_equals_function_code( /// \param symbol_table: symbol table /// \return Code corresponding to the Java conversion of floats to strings. codet java_string_library_preprocesst::make_float_to_string_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) { // Getting the argument - code_typet::parameterst params=type.parameters(); + java_method_typet::parameterst params = type.parameters(); PRECONDITION(params.size()==1); const symbol_exprt arg(params[0].get_identifier(), params[0].type()); @@ -1155,12 +1155,12 @@ codet java_string_library_preprocesst::make_float_to_string_code( /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_init_function_from_call( const irep_idt &function_name, - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool ignore_first_arg) { - code_typet::parameterst params=type.parameters(); + java_method_typet::parameterst params = type.parameters(); // The first parameter is the object to be initialized PRECONDITION(!params.empty()); @@ -1196,12 +1196,12 @@ codet java_string_library_preprocesst::make_init_function_from_call( codet java_string_library_preprocesst:: make_assign_and_return_function_from_call( const irep_idt &function_name, - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) { // This is similar to assign functions except we return a pointer to `this` - code_typet::parameterst params=type.parameters(); + java_method_typet::parameterst params = type.parameters(); PRECONDITION(!params.empty()); code_blockt code; code.add( @@ -1221,7 +1221,7 @@ codet java_string_library_preprocesst:: /// name. codet java_string_library_preprocesst::make_assign_function_from_call( const irep_idt &function_name, - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) { @@ -1503,7 +1503,7 @@ exprt java_string_library_preprocesst::make_argument_for_format( /// argument to the internal format function a structure containing /// the different possible types. codet java_string_library_preprocesst::make_string_format_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) @@ -1562,12 +1562,12 @@ codet java_string_library_preprocesst::make_string_format_code( /// return class1 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_object_get_class_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) { - code_typet::parameterst params=type.parameters(); + java_method_typet::parameterst params = type.parameters(); const symbol_exprt this_obj(params[0].get_identifier(), params[0].type()); // Code to be returned @@ -1620,7 +1620,8 @@ codet java_string_library_preprocesst::make_object_get_class_code( "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"); fun_call.lhs()=class1; fun_call.arguments().push_back(string1); - const code_typet fun_type({code_typet::parametert(string_ptr_type)}, class_type); + const java_method_typet fun_type( + {java_method_typet::parametert(string_ptr_type)}, class_type); fun_call.function().type()=fun_type; code.add(fun_call, loc); @@ -1641,7 +1642,7 @@ codet java_string_library_preprocesst::make_object_get_class_code( /// ~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_function_from_call( const irep_idt &function_name, - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) { @@ -1670,7 +1671,7 @@ codet java_string_library_preprocesst::make_function_from_call( /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_string_returning_function_from_call( const irep_idt &function_name, - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) { @@ -1711,7 +1712,7 @@ codet java_string_library_preprocesst::make_string_returning_function_from_call( /// return str /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_copy_string_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) @@ -1723,7 +1724,7 @@ codet java_string_library_preprocesst::make_copy_string_code( refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code); // Assign the argument to string_expr - code_typet::parametert op=type.parameters()[0]; + java_method_typet::parametert op = type.parameters()[0]; symbol_exprt arg0(op.get_identifier(), op.type()); code_assign_java_string_to_string_expr( string_expr, arg0, loc, symbol_table, code); @@ -1753,7 +1754,7 @@ codet java_string_library_preprocesst::make_copy_string_code( /// this = string_expr_to_java_string(string_expr) /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_copy_constructor_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) @@ -1767,7 +1768,7 @@ codet java_string_library_preprocesst::make_copy_constructor_code( refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code); // Assign argument to a string_expr - code_typet::parameterst params=type.parameters(); + java_method_typet::parameterst params = type.parameters(); symbol_exprt arg1(params[1].get_identifier(), params[1].type()); code_assign_java_string_to_string_expr( string_expr, arg1, loc, symbol_table, code); @@ -1791,7 +1792,7 @@ codet java_string_library_preprocesst::make_copy_constructor_code( /// \return code implementing String intitialization from a char array and /// arguments offset and end. codet java_string_library_preprocesst::make_init_from_array_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) @@ -1801,7 +1802,7 @@ codet java_string_library_preprocesst::make_init_from_array_code( // Code for the output code_blockt code; - code_typet::parameterst params = type.parameters(); + java_method_typet::parameterst params = type.parameters(); PRECONDITION(params.size() == 4); exprt::operandst args = process_parameters(type.parameters(), loc, symbol_table, code); @@ -1842,16 +1843,16 @@ codet java_string_library_preprocesst::make_init_from_array_code( /// return this->length /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_string_length_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) { (void)function_id; - code_typet::parameterst params=type.parameters(); + java_method_typet::parameterst params = type.parameters(); symbol_exprt arg_this(params[0].get_identifier(), params[0].type()); - dereference_exprt deref= + dereference_exprt deref = checked_dereference(arg_this, arg_this.type().subtype()); return code_returnt(get_length(deref, symbol_table)); } @@ -1902,7 +1903,7 @@ exprt java_string_library_preprocesst::code_for_function( symbol_table_baset &symbol_table) { const irep_idt &function_id = symbol.name; - const code_typet &type = to_code_type(symbol.type); + const java_method_typet &type = to_java_method_type(symbol.type); const source_locationt &loc = symbol.location; auto it_id=cprover_equivalent_to_java_function.find(function_id); if(it_id!=cprover_equivalent_to_java_function.end()) diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h index 382dc1b5d9d..78c3ae4667f 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.h +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h @@ -99,7 +99,7 @@ class java_string_library_preprocesst:public messaget const refined_string_typet refined_string_type; typedef std::function @@ -146,56 +146,56 @@ class java_string_library_preprocesst:public messaget std::unordered_set string_types; codet make_equals_function_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table); codet make_float_to_string_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table); codet make_string_to_char_array_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_tablet &symbol_table); codet make_string_format_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table); codet make_copy_string_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table); codet make_copy_constructor_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table); codet make_string_length_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table); codet make_object_get_class_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table); // Helper functions exprt::operandst process_parameters( - const code_typet::parameterst ¶ms, + const java_method_typet::parameterst ¶ms, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code); @@ -306,32 +306,32 @@ class java_string_library_preprocesst:public messaget codet make_function_from_call( const irep_idt &function_name, - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table); codet make_init_function_from_call( const irep_idt &function_name, - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool ignore_first_arg = true); codet make_assign_and_return_function_from_call( const irep_idt &function_name, - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table); codet make_assign_function_from_call( const irep_idt &function_name, - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table); codet make_string_returning_function_from_call( const irep_idt &function_name, - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table); @@ -354,7 +354,7 @@ class java_string_library_preprocesst:public messaget exprt get_object_at_index(const exprt &argv, std::size_t index); codet make_init_from_array_code( - const code_typet &type, + const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table); diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index 67e3a27e971..866ed2d8fcd 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -542,14 +542,14 @@ typet java_type_from_string( parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')'); // create parameters for each type - code_typet::parameterst parameters; + java_method_typet::parameterst parameters; std::transform( param_types.begin(), param_types.end(), std::back_inserter(parameters), - [](const typet &type) { return code_typet::parametert(type); }); + [](const typet &type) { return java_method_typet::parametert(type); }); - return code_typet(std::move(parameters), std::move(return_type)); + return java_method_typet(std::move(parameters), std::move(return_type)); } case '[': // array type @@ -817,7 +817,7 @@ void get_dependencies_from_generic_parameters_rec( // method type with parameters and return value else if(t.id() == ID_code) { - const code_typet &c = to_code_type(t); + const java_method_typet &c = to_java_method_type(t); get_dependencies_from_generic_parameters_rec(c.return_type(), refs); for(const auto ¶m : c.parameters()) get_dependencies_from_generic_parameters_rec(param.type(), refs); @@ -974,7 +974,7 @@ std::string pretty_java_type(const typet &type) return "?"; } -std::string pretty_signature(const code_typet &code_type) +std::string pretty_signature(const java_method_typet &code_type) { std::ostringstream result; result << '('; diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index cfd847eaa65..029b725c6f9 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -245,6 +245,10 @@ inline bool can_cast_type(const typet &type) class java_method_typet : public code_typet { public: + using code_typet::code_typet; + using code_typet::parameterst; + using code_typet::parametert; + const std::vector throws_exceptions() const { std::vector exceptions; @@ -732,6 +736,6 @@ std::string gather_full_class_name(const std::string &); std::string pretty_java_type(const typet &); // pretty signature for methods -std::string pretty_signature(const code_typet &); +std::string pretty_signature(const java_method_typet &); #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 9e9f4f499ab..7d57ef826e6 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_utils.h" #include "java_root_class.h" -#include "java_types.h" #include #include @@ -46,7 +45,7 @@ unsigned java_local_variable_slots(const typet &t) return bitwidth == 64 ? 2u : 1u; } -unsigned java_method_parameter_slots(const code_typet &t) +unsigned java_method_parameter_slots(const java_method_typet &t) { unsigned slots=0; diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index dea8f1bf412..e58db51594f 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_JAVA_BYTECODE_JAVA_UTILS_H #define CPROVER_JAVA_BYTECODE_JAVA_UTILS_H +#include "java_types.h" + #include #include @@ -31,7 +33,7 @@ unsigned java_local_variable_slots(const typet &t); /// Returns the the number of JVM local variables (slots) used by the JVM to /// pass, upon call, the arguments of a Java method whose type is \p t. -unsigned java_method_parameter_slots(const code_typet &t); +unsigned java_method_parameter_slots(const java_method_typet &t); const std::string java_class_to_package(const std::string &canonical_classname); diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp index 4fa38a5ea03..640f68196f7 100644 --- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp +++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp @@ -145,7 +145,7 @@ void java_simple_method_stubst::create_method_stub_at( void java_simple_method_stubst::create_method_stub(symbolt &symbol) { code_blockt new_instructions; - const code_typet &required_type = to_code_type(symbol.type); + const java_method_typet &required_type = to_java_method_type(symbol.type); // synthetic source location that contains the opaque function name only source_locationt synthesized_source_location; diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 77d09d02bc8..9a8669fc91b 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -55,22 +55,22 @@ struct_union_typet::componentt require_type::require_component( /// Checks a type is a code_type (i.e. a function) /// \param type: The type to check /// \return The cast version of the type code_type -code_typet require_type::require_code(const typet &type) +java_method_typet require_type::require_code(const typet &type) { REQUIRE(type.id() == ID_code); - return to_code_type(type); + return to_java_method_type(type); } -/// Verify a given type is an code_typet, and that the code it represents +/// Verify a given type is an java_method_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 +/// \param num_params check the the given java_method_typet expects this /// number of parameters -/// \return The type cast to a code_typet -code_typet +/// \return The type cast to a java_method_typet +java_method_typet require_type::require_code(const typet &type, const size_t num_params) { - code_typet code_type = require_code(type); + java_method_typet code_type = require_code(type); REQUIRE(code_type.parameters().size() == num_params); return code_type; } @@ -80,14 +80,14 @@ require_type::require_code(const typet &type, const size_t num_params) /// \param param_name: The name of the parameter /// \return: A reference to the parameter structure corresponding to this /// parameter name. -code_typet::parametert require_type::require_parameter( - const code_typet &function_type, +java_method_typet::parametert require_type::require_parameter( + const java_method_typet &function_type, const irep_idt ¶m_name) { const auto param = std::find_if( function_type.parameters().begin(), function_type.parameters().end(), - [¶m_name](const code_typet::parametert param) { + [¶m_name](const java_method_typet::parametert param) { return param.get_base_name() == param_name; }); diff --git a/jbmc/unit/java-testing-utils/require_type.h b/jbmc/unit/java-testing-utils/require_type.h index 3e59da59e72..e329fc0c866 100644 --- a/jbmc/unit/java-testing-utils/require_type.h +++ b/jbmc/unit/java-testing-utils/require_type.h @@ -32,12 +32,13 @@ struct_typet::componentt require_component( const struct_typet &struct_type, const irep_idt &component_name); -code_typet require_code(const typet &type); +java_method_typet require_code(const typet &type); -code_typet::parametert -require_parameter(const code_typet &function_type, const irep_idt ¶m_name); +java_method_typet::parametert require_parameter( + const java_method_typet &function_type, + const irep_idt ¶m_name); -code_typet require_code(const typet &type, const size_t num_params); +java_method_typet require_code(const typet &type, const size_t num_params); // A mini DSL for describing an expected set of type arguments for a // java_generic_typet diff --git a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp index fb294c1d148..cc11b383d2e 100644 --- a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp +++ b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp @@ -133,9 +133,8 @@ SCENARIO( call.function() = callee; // Specific argument doesn't matter, so just pass an appropriately typed // null pointer: - call.arguments().push_back( - null_pointer_exprt( - to_pointer_type(to_code_type(callee.type()).parameters()[0].type()))); + call.arguments().push_back(null_pointer_exprt(to_pointer_type( + to_java_method_type(callee.type()).parameters()[0].type()))); virtual_call_inst->code = call; test_program.add_instruction(END_FUNCTION); diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp index 8583977a748..ff497f1594b 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp @@ -33,7 +33,8 @@ void require_is_constructor(const test_datat &test_data) test_data.symbol_table.lookup_ref(test_data.constructor_descriptor); THEN("The constructor should be marked as a constructor") { - code_typet constructor_type = require_type::require_code(constructor.type); + java_method_typet constructor_type = + require_type::require_code(constructor.type); REQUIRE(constructor_type.get_is_constructor()); } } @@ -49,7 +50,8 @@ void require_is_static_initializer(const test_datat &test_data) test_data.symbol_table.lookup_ref(test_data.constructor_descriptor); THEN("The constructor should be marked as a constructor") { - code_typet constructor_type = require_type::require_code(constructor.type); + java_method_typet constructor_type = + require_type::require_code(constructor.type); REQUIRE_FALSE(constructor_type.get_is_constructor()); } } diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp index a925d8469f8..b3f1421b2c7 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp @@ -29,7 +29,7 @@ SCENARIO( const symbolt function_symbol = symbol_table.lookup_ref(method_name + ":(Ljava/lang/Object;)I"); - const code_typet &function_type = + const java_method_typet &function_type = require_type::require_code(function_symbol.type); THEN("The method should be marked as a bridge method") { @@ -43,7 +43,7 @@ SCENARIO( const symbolt function_symbol = symbol_table.lookup_ref(method_name + ":(LClassWithBridgeMethod;)I"); - const code_typet &function_type = + const java_method_typet &function_type = require_type::require_code(function_symbol.type); THEN("The method should be marked as a bridge method") { diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp index 5c3fe280632..9c21e55d3d3 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp @@ -76,9 +76,9 @@ SCENARIO( { const symbolt &method_symbol = new_symbol_table.lookup_ref(method_name); - const code_typet &method_type = + const java_method_typet &method_type = require_type::require_code(method_symbol.type); - const code_typet::parametert ¶m = + const java_method_typet::parametert ¶m = require_type::require_parameter(method_type, "x"); require_type::require_java_generic_parameter( param.type(), boundedinner_name + "::NUM"); diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp index 7a2845c648a..289bd642bde 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp @@ -32,12 +32,12 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &func_code = + const java_method_typet &func_code = require_type::require_code(func_symbol.type); THEN("It has parameter x pointing to Generic") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::Generic")); @@ -81,11 +81,12 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = require_type::require_code(func_symbol.type); + const java_method_typet func_code = + require_type::require_code(func_symbol.type); THEN("It has parameter s pointing to Generic") { - const code_typet::parametert ¶m_s = + const java_method_typet::parametert ¶m_s = require_type::require_parameter(func_code, "s"); require_type::require_pointer( param_s.type(), symbol_typet("java::Generic")); @@ -129,11 +130,12 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = require_type::require_code(func_symbol.type); + const java_method_typet func_code = + require_type::require_code(func_symbol.type); THEN("It has parameter x pointing to Generic") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::Generic")); @@ -149,7 +151,7 @@ SCENARIO( THEN("It has parameter y pointing to Generic") { - const code_typet::parametert ¶m_y = + const java_method_typet::parametert ¶m_y = require_type::require_parameter(func_code, "y"); require_type::require_pointer( param_y.type(), symbol_typet("java::Generic")); @@ -193,11 +195,12 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = require_type::require_code(func_symbol.type); + const java_method_typet func_code = + require_type::require_code(func_symbol.type); THEN("It has parameter s pointing to Generic") { - const code_typet::parametert ¶m_s = + const java_method_typet::parametert ¶m_s = require_type::require_parameter(func_code, "s"); require_type::require_pointer( param_s.type(), symbol_typet("java::Generic")); @@ -213,7 +216,7 @@ SCENARIO( THEN("It has parameter b pointing to Generic") { - const code_typet::parametert ¶m_b = + const java_method_typet::parametert ¶m_b = require_type::require_parameter(func_code, "b"); require_type::require_pointer( param_b.type(), symbol_typet("java::Generic")); @@ -258,11 +261,12 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = require_type::require_code(func_symbol.type); + const java_method_typet func_code = + require_type::require_code(func_symbol.type); THEN("It has parameter inner pointing to Inner") { - const code_typet::parametert ¶m_inner = + const java_method_typet::parametert ¶m_inner = require_type::require_parameter(func_code, "inner"); require_type::require_pointer( param_inner.type(), symbol_typet(class_prefix + "$Inner")); diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp index 47de0300e5b..a85a7c0e90c 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp @@ -316,7 +316,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of correct type") @@ -345,7 +345,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 3); THEN("The inputs are of correct type") @@ -381,7 +381,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of correct type") @@ -412,7 +412,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of correct type") @@ -442,7 +442,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of correct type") @@ -476,7 +476,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of correct type") @@ -508,7 +508,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of correct type") @@ -544,7 +544,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of correct type") @@ -576,7 +576,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of the correct type") @@ -609,7 +609,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of the correct type") @@ -642,7 +642,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs should be of the correct type") @@ -672,7 +672,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type should be correct") @@ -699,7 +699,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type should be correct") @@ -729,7 +729,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type should be correct") @@ -758,7 +758,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type should be correct") @@ -790,7 +790,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type should be correct") @@ -820,7 +820,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type should be correct") @@ -854,7 +854,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type should be correct") @@ -885,7 +885,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type should be correct") @@ -917,7 +917,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type should be correct") @@ -949,7 +949,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type should be correct") diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp index 41faa1bae19..3de8b022984 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp @@ -32,11 +32,11 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::Generic")); @@ -59,11 +59,11 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::Generic")); @@ -86,11 +86,11 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::Generic")); @@ -113,11 +113,11 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter x pointing to java.lang.Number") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::java.lang.Number")); @@ -140,11 +140,11 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::Generic")); @@ -167,11 +167,11 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::Generic")); @@ -194,12 +194,12 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 2); THEN("It contains parameter t pointing to Generic") { - const code_typet::parametert ¶m_t = + const java_method_typet::parametert ¶m_t = require_type::require_parameter(func_code, "t"); require_type::require_pointer( param_t.type(), symbol_typet("java::Generic")); @@ -209,7 +209,7 @@ SCENARIO( } THEN("It contains parameter u pointing to Generic") { - const code_typet::parametert ¶m_u = + const java_method_typet::parametert ¶m_u = require_type::require_parameter(func_code, "u"); require_type::require_pointer( param_u.type(), symbol_typet("java::Generic")); @@ -232,12 +232,12 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 2); THEN("It contains parameter t pointing to Generic") { - const code_typet::parametert ¶m_t = + const java_method_typet::parametert ¶m_t = require_type::require_parameter(func_code, "t"); require_type::require_pointer( param_t.type(), symbol_typet("java::Generic")); @@ -247,7 +247,7 @@ SCENARIO( } THEN("It contains parameter u pointing to Generic") { - const code_typet::parametert ¶m_u = + const java_method_typet::parametert ¶m_u = require_type::require_parameter(func_code, "u"); require_type::require_pointer( param_u.type(), symbol_typet("java::Generic")); @@ -271,7 +271,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 0); THEN("It has return type pointing to Generic") { @@ -297,7 +297,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 0); THEN("It has return type pointing to java.lang.Object") { @@ -322,7 +322,7 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = to_code_type(func_symbol.type); + const java_method_typet func_code = to_java_method_type(func_symbol.type); THEN("It has return type pointing to Generic") { require_type::require_pointer( @@ -346,7 +346,7 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 0); THEN("It has return type pointing to Generic") { @@ -371,7 +371,7 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 0); THEN("It has return type pointing to Generic") { @@ -396,7 +396,7 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 0); THEN("It has return type pointing to Generic") { @@ -422,12 +422,12 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::Generic")); @@ -459,12 +459,12 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::Generic")); @@ -496,12 +496,12 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::Generic")); @@ -533,12 +533,12 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::Generic")); @@ -571,12 +571,12 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { - const code_typet::parametert ¶m_x = + const java_method_typet::parametert ¶m_x = require_type::require_parameter(func_code, "x"); require_type::require_pointer( param_x.type(), symbol_typet("java::Generic")); @@ -608,12 +608,12 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter u pointing to Generic") { - const code_typet::parametert ¶m_u = + const java_method_typet::parametert ¶m_u = require_type::require_parameter(func_code, "u"); require_type::require_pointer( param_u.type(), symbol_typet("java::Generic")); @@ -645,12 +645,12 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 1); THEN("It contains parameter u pointing to Generic") { - const code_typet::parametert ¶m_u = + const java_method_typet::parametert ¶m_u = require_type::require_parameter(func_code, "u"); require_type::require_pointer( param_u.type(), symbol_typet("java::Generic")); @@ -682,12 +682,12 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 2); THEN("It contains parameter u pointing to Generic") { - const code_typet::parametert ¶m_u = + const java_method_typet::parametert ¶m_u = require_type::require_parameter(func_code, "u"); require_type::require_pointer( param_u.type(), symbol_typet("java::Generic")); @@ -698,7 +698,7 @@ SCENARIO( THEN("It contains parameter v pointing to Generic") { - const code_typet::parametert ¶m_v = + const java_method_typet::parametert ¶m_v = require_type::require_parameter(func_code, "v"); require_type::require_pointer( param_v.type(), symbol_typet("java::Generic")); @@ -730,12 +730,12 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(process_func_name)); const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet func_code = + const java_method_typet func_code = require_type::require_code(func_symbol.type, 2); THEN("It contains parameter u pointing to Generic") { - const code_typet::parametert ¶m_u = + const java_method_typet::parametert ¶m_u = require_type::require_parameter(func_code, "u"); require_type::require_pointer( param_u.type(), symbol_typet("java::Generic")); @@ -746,7 +746,7 @@ SCENARIO( THEN("It contains parameter v pointing to Generic") { - const code_typet::parametert ¶m_v = + const java_method_typet::parametert ¶m_v = require_type::require_parameter(func_code, "v"); require_type::require_pointer( param_v.type(), symbol_typet("java::Generic")); diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp index e3e5cf657ce..0bfef784b76 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp @@ -417,7 +417,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of correct type") @@ -455,7 +455,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of oorrect type") @@ -493,7 +493,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of correct type") @@ -538,7 +538,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of correct type") @@ -583,7 +583,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs are of correct type") @@ -624,7 +624,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs have correct type") @@ -665,7 +665,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs have correct type") @@ -706,7 +706,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs have correct type") @@ -751,7 +751,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs have correct type") @@ -796,7 +796,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs have correct type") @@ -841,7 +841,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs have correct type") @@ -882,7 +882,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs have correct type") @@ -929,7 +929,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 2); THEN("The inputs have correct type") @@ -976,7 +976,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") @@ -1012,7 +1012,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") @@ -1048,7 +1048,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") @@ -1090,7 +1090,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") @@ -1132,7 +1132,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") @@ -1171,7 +1171,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") @@ -1210,7 +1210,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") @@ -1249,7 +1249,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") @@ -1292,7 +1292,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") @@ -1335,7 +1335,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") @@ -1378,7 +1378,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") @@ -1417,7 +1417,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") @@ -1462,7 +1462,7 @@ SCENARIO( const symbolt &function_symbol = new_symbol_table.lookup_ref(process_func_name); - const code_typet &function_call = + const java_method_typet &function_call = require_type::require_code(function_symbol.type, 1); THEN("The return type is correct") diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp index 7cbdd2f55ac..fdae9d90a82 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp @@ -43,16 +43,16 @@ SCENARIO( inner_prefix + func_name + func_descriptor; REQUIRE(new_symbol_table.has_symbol(process_func_name)); - const code_typet func_code = - to_code_type(new_symbol_table.lookup_ref(process_func_name).type); + const java_method_typet func_code = + to_java_method_type(new_symbol_table.lookup_ref(process_func_name).type); REQUIRE(func_code.parameters().size() == 3); // TODO: for now, the parameters are not generic because we fall back to // descriptor due to mismatch; enable tests when fixed - issue TG-1309 - // code_typet::parametert param_parent= + // java_method_typet::parametert param_parent= // require_type::require_parameter(func_code,"arg1a"); // REQUIRE(is_java_generic_type(param_parent.type())); - // code_typet::parametert param_t= + // java_method_typet::parametert param_t= // require_type::require_parameter(func_code,"t"); // REQUIRE(is_java_generic_type(param_t.type())); } @@ -78,16 +78,16 @@ SCENARIO( inner_enum_prefix + func_name + func_descriptor; REQUIRE(new_symbol_table.has_symbol(process_func_name)); - const code_typet func_code = - to_code_type(new_symbol_table.lookup_ref(process_func_name).type); + const java_method_typet func_code = + to_java_method_type(new_symbol_table.lookup_ref(process_func_name).type); REQUIRE(func_code.parameters().size() == 3); // TODO: for now, the parameters are not generic because we fall back to // descriptor due to mismatch; enable tests when fixed - issue TG-1309 - // code_typet::parametert param_parent= + // java_method_typet::parametert param_parent= // require_type::require_parameter(func_code,"arg1a"); // REQUIRE(is_java_generic_type(param_parent.type())); - // code_typet::parametert param_t= + // java_method_typet::parametert param_t= // require_type::require_parameter(func_code,"arg2i"); // REQUIRE(is_java_generic_type(param_t.type())); } diff --git a/jbmc/unit/java_bytecode/load_method_by_regex.cpp b/jbmc/unit/java_bytecode/load_method_by_regex.cpp index 5b754996728..8b79894a1ca 100644 --- a/jbmc/unit/java_bytecode/load_method_by_regex.cpp +++ b/jbmc/unit/java_bytecode/load_method_by_regex.cpp @@ -92,7 +92,7 @@ static symbolt create_method_symbol(const std::string &method_name) { symbolt new_symbol; new_symbol.name = method_name; - new_symbol.type = code_typet{{}, nil_typet{}}; + new_symbol.type = java_method_typet{{}, nil_typet{}}; return new_symbol; } diff --git a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp b/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp index 1e7b9461e26..64856fddb96 100644 --- a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp +++ b/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp @@ -58,11 +58,11 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]") const symbol_exprt lhs("lhs", unsignedbv_typet(32)); const symbol_exprt lhs2("lhs2", unsignedbv_typet(32)); const symbol_exprt lhs3("lhs3", unsignedbv_typet(32)); - const code_typet fun_type( - {code_typet::parametert(length_type()), - code_typet::parametert(pointer_type(java_char_type())), - code_typet::parametert(string_type), - code_typet::parametert(string_type)}, + const java_method_typet fun_type( + {java_method_typet::parametert(length_type()), + java_method_typet::parametert(pointer_type(java_char_type())), + java_method_typet::parametert(string_type), + java_method_typet::parametert(string_type)}, unsignedbv_typet(32)); // fun1 is s3 = s1.concat(s2) diff --git a/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp b/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp index e7b6eb22478..587eb8d4812 100644 --- a/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp +++ b/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp @@ -64,7 +64,7 @@ SCENARIO("string_identifiers_resolution_from_equations", WHEN("There is a function call") { - symbol_exprt fun_sym("f", code_typet()); + symbol_exprt fun_sym("f", java_method_typet()); function_application_exprt fun(fun_sym, bool_typet()); fun.operands().push_back(c); symbol_exprt bool_sym("bool_b", bool_typet()); diff --git a/jbmc/unit/util/parameter_indices.cpp b/jbmc/unit/util/parameter_indices.cpp index f29f76f1c27..d7d4786163f 100644 --- a/jbmc/unit/util/parameter_indices.cpp +++ b/jbmc/unit/util/parameter_indices.cpp @@ -6,13 +6,13 @@ \*******************************************************************/ -#include #include +#include #include void check_consistency(const symbolt &symbol) { - const auto &code_type = to_code_type(symbol.type); + const auto &code_type = to_java_method_type(symbol.type); auto parameter_ids = code_type.parameter_identifiers(); auto parameter_indices = code_type.parameter_indices(); From da18c9f51c3baefc0d843b2ca0929446e67744c8 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Wed, 1 Aug 2018 17:05:16 +0100 Subject: [PATCH 02/11] Change variables named code_type to method_type This is for variables that have been changed to java_method_typet from code_typet --- jbmc/src/java_bytecode/expr2java.cpp | 12 ++++---- .../java_bytecode_convert_method.cpp | 28 +++++++++---------- .../java_bytecode_typecheck_type.cpp | 6 ++-- jbmc/src/java_bytecode/java_types.cpp | 4 +-- jbmc/unit/java-testing-utils/require_type.cpp | 8 +++--- jbmc/unit/util/parameter_indices.cpp | 6 ++-- 6 files changed, 32 insertions(+), 32 deletions(-) diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index f6e8d87ebe3..edd196ff53a 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/jbmc/src/java_bytecode/expr2java.cpp @@ -56,10 +56,10 @@ std::string expr2javat::convert_code_function_call( dest+='='; } - const java_method_typet &code_type = + const java_method_typet &method_type = to_java_method_type(src.function().type()); - bool has_this = code_type.has_this() && !src.arguments().empty(); + bool has_this = method_type.has_this() && !src.arguments().empty(); if(has_this) { @@ -283,7 +283,7 @@ std::string expr2javat::convert_rec( return q+"byte"+d; else if(src.id()==ID_code) { - const java_method_typet &code_type = to_java_method_type(src); + const java_method_typet &method_type = to_java_method_type(src); // Java doesn't really have syntax for function types, // so we make one up, loosely inspired by the syntax @@ -292,7 +292,7 @@ std::string expr2javat::convert_rec( std::string dest=""; dest+='('; - const java_method_typet::parameterst ¶meters = code_type.parameters(); + const java_method_typet::parameterst ¶meters = method_type.parameters(); for(java_method_typet::parameterst::const_iterator it = parameters.begin(); it != parameters.end(); @@ -304,7 +304,7 @@ std::string expr2javat::convert_rec( dest+=convert(it->type()); } - if(code_type.has_ellipsis()) + if(method_type.has_ellipsis()) { if(!parameters.empty()) dest+=", "; @@ -313,7 +313,7 @@ std::string expr2javat::convert_rec( dest+=')'; - const typet &return_type = code_type.return_type(); + const typet &return_type = method_type.return_type(); dest+=" -> "+convert(return_type); return q + dest; diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 7841f503b0f..69f30186d15 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1251,9 +1251,9 @@ codet java_bytecode_convert_methodt::convert_instructions( id2string(arg0.get(ID_identifier))== "java::org.cprover.CProver.assume:(Z)V") { - const java_method_typet &code_type = to_java_method_type(arg0.type()); + const java_method_typet &method_type = to_java_method_type(arg0.type()); INVARIANT( - code_type.parameters().size() == 1, + method_type.parameters().size() == 1, "function expected to have exactly one parameter"); c = replace_call_to_cprover_assume(i_it->source_location, c); } @@ -2107,8 +2107,8 @@ void java_bytecode_convert_methodt::convert_invoke( const bool is_virtual( statement == "invokevirtual" || statement == "invokeinterface"); - java_method_typet &code_type = to_java_method_type(arg0.type()); - java_method_typet::parameterst ¶meters(code_type.parameters()); + java_method_typet &method_type = to_java_method_type(arg0.type()); + java_method_typet::parameterst ¶meters(method_type.parameters()); if(use_this) { @@ -2124,10 +2124,10 @@ void java_bytecode_convert_methodt::convert_invoke( { if(needed_lazy_methods) needed_lazy_methods->add_needed_class(classname); - code_type.set_is_constructor(); + method_type.set_is_constructor(); } else - code_type.set(ID_java_super_method_call, true); + method_type.set(ID_java_super_method_call, true); } reference_typet object_ref_type = java_reference_type(thistype); java_method_typet::parametert this_p(object_ref_type); @@ -2172,7 +2172,7 @@ void java_bytecode_convert_methodt::convert_invoke( // do some type adjustment for return values - const typet &return_type = code_type.return_type(); + const typet &return_type = method_type.return_type(); if(return_type.id() != ID_empty) { @@ -2947,11 +2947,11 @@ optionalt java_bytecode_convert_methodt::convert_invoke_dynamic( const source_locationt &location, const exprt &arg0) { - const java_method_typet &code_type = to_java_method_type(arg0.type()); + const java_method_typet &method_type = to_java_method_type(arg0.type()); const optionalt &lambda_method_symbol = get_lambda_method_symbol( lambda_method_handles, - code_type.get_int(ID_java_lambda_method_handle_index)); + method_type.get_int(ID_java_lambda_method_handle_index)); if(lambda_method_symbol.has_value()) debug() << "Converting invokedynamic for lambda: " << lambda_method_symbol.value().name << eom; @@ -2960,11 +2960,11 @@ optionalt java_bytecode_convert_methodt::convert_invoke_dynamic( "type" << eom; - const java_method_typet::parameterst ¶meters(code_type.parameters()); + const java_method_typet::parameterst ¶meters(method_type.parameters()); pop(parameters.size()); - const typet &return_type = code_type.return_type(); + const typet &return_type = method_type.return_type(); if(return_type.id() == ID_empty) return {}; @@ -3023,11 +3023,11 @@ void java_bytecode_initialize_parameter_names( { // Obtain a std::vector of java_method_typet::parametert objects from the // (function) type of the symbol - java_method_typet &code_type = to_java_method_type(method_symbol.type); - java_method_typet::parameterst ¶meters = code_type.parameters(); + java_method_typet &method_type = to_java_method_type(method_symbol.type); + java_method_typet::parameterst ¶meters = method_type.parameters(); // Find number of parameters - unsigned slots_for_parameters = java_method_parameter_slots(code_type); + unsigned slots_for_parameters = java_method_parameter_slots(method_type); // Find parameter names in the local variable table: typedef std::pair base_name_and_identifiert; diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp index 321a277bb73..25f28713105 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp @@ -38,10 +38,10 @@ void java_bytecode_typecheckt::typecheck_type(typet &type) } else if(type.id()==ID_code) { - java_method_typet &code_type = to_java_method_type(type); - typecheck_type(code_type.return_type()); + java_method_typet &method_type = to_java_method_type(type); + typecheck_type(method_type.return_type()); - java_method_typet::parameterst ¶meters = code_type.parameters(); + java_method_typet::parameterst ¶meters = method_type.parameters(); for(java_method_typet::parameterst::iterator it = parameters.begin(); it != parameters.end(); diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index 866ed2d8fcd..2dd3c3f0178 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -974,13 +974,13 @@ std::string pretty_java_type(const typet &type) return "?"; } -std::string pretty_signature(const java_method_typet &code_type) +std::string pretty_signature(const java_method_typet &method_type) { std::ostringstream result; result << '('; bool first = true; - for(const auto p : code_type.parameters()) + for(const auto p : method_type.parameters()) { if(p.get_this()) continue; diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 9a8669fc91b..c2e9fbb67a4 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -54,7 +54,7 @@ struct_union_typet::componentt require_type::require_component( /// Checks a type is a code_type (i.e. a function) /// \param type: The type to check -/// \return The cast version of the type code_type +/// \return The cast version of the type method_type java_method_typet require_type::require_code(const typet &type) { REQUIRE(type.id() == ID_code); @@ -70,9 +70,9 @@ java_method_typet require_type::require_code(const typet &type) java_method_typet require_type::require_code(const typet &type, const size_t num_params) { - java_method_typet code_type = require_code(type); - REQUIRE(code_type.parameters().size() == num_params); - return code_type; + java_method_typet method_type = require_code(type); + REQUIRE(method_type.parameters().size() == num_params); + return method_type; } /// Verify that a function has a parameter of a specific name. diff --git a/jbmc/unit/util/parameter_indices.cpp b/jbmc/unit/util/parameter_indices.cpp index d7d4786163f..7dd6bee9277 100644 --- a/jbmc/unit/util/parameter_indices.cpp +++ b/jbmc/unit/util/parameter_indices.cpp @@ -12,9 +12,9 @@ void check_consistency(const symbolt &symbol) { - const auto &code_type = to_java_method_type(symbol.type); - auto parameter_ids = code_type.parameter_identifiers(); - auto parameter_indices = code_type.parameter_indices(); + const auto &method_type = to_java_method_type(symbol.type); + auto parameter_ids = method_type.parameter_identifiers(); + auto parameter_indices = method_type.parameter_indices(); REQUIRE(parameter_ids.size() == parameter_indices.size()); for(std::size_t i = 0; i < parameter_ids.size(); ++i) From 551df9cf1667f4784eb8e49dabe40d85e39b67f1 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Wed, 1 Aug 2018 17:15:35 +0100 Subject: [PATCH 03/11] Update unit tests to use java_method_typet --- .../remove_virtual_functions_without_fallback.cpp | 2 ++ jbmc/unit/util/parameter_indices.cpp | 5 +++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp index cc11b383d2e..7bba7e86cb8 100644 --- a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp +++ b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp @@ -7,6 +7,8 @@ \*******************************************************************/ +#include + #include #include diff --git a/jbmc/unit/util/parameter_indices.cpp b/jbmc/unit/util/parameter_indices.cpp index 7dd6bee9277..df41d773c77 100644 --- a/jbmc/unit/util/parameter_indices.cpp +++ b/jbmc/unit/util/parameter_indices.cpp @@ -6,9 +6,10 @@ \*******************************************************************/ -#include +#include + #include -#include +#include void check_consistency(const symbolt &symbol) { From 211931c06a00e2f010183452df0e8bb750a51ee2 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Wed, 1 Aug 2018 18:15:05 +0100 Subject: [PATCH 04/11] Add tag for java_method_type --- jbmc/src/java_bytecode/java_types.h | 28 +++++++++++++++++++++++++++- src/util/irep_ids.def | 1 + 2 files changed, 28 insertions(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 029b725c6f9..61d865f9f14 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -245,10 +245,36 @@ inline bool can_cast_type(const typet &type) class java_method_typet : public code_typet { public: - using code_typet::code_typet; using code_typet::parameterst; using code_typet::parametert; + /// Constructs a new code type, i.e. function type + /// \param _parameters: the vector of function parameters + /// \param _return_type: the return type + java_method_typet(parameterst &&_parameters, typet &&_return_type) + { + set(ID_C_java_method_type, true); + parameters().swap(_parameters); + return_type().swap(_return_type); + } + + /// Constructs a new code type, i.e. function type + /// \param _parameters: the vector of function parameters + /// \param _return_type: the return type + java_method_typet(parameterst &&_parameters, const typet &_return_type) + { + set(ID_C_java_method_type, true); + parameters().swap(_parameters); + return_type() = _return_type; + } + + /// \deprecated + DEPRECATED("Use the two argument constructor instead") + java_method_typet() + { + set(ID_C_java_method_type, true); + } + const std::vector throws_exceptions() const { std::vector exceptions; diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index d0066054482..7687299a1fb 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -697,6 +697,7 @@ IREP_ID_ONE(r_ok) IREP_ID_ONE(w_ok) IREP_ID_ONE(super_class) IREP_ID_ONE(exceptions_thrown_list) +IREP_ID_TWO(C_java_method_type, #java_method_type) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree From 972315affe1e66ab2bc13ab829040391587293e2 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Thu, 2 Aug 2018 12:25:35 +0100 Subject: [PATCH 05/11] Update docs on java_method_typet constructor --- jbmc/src/java_bytecode/java_types.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 61d865f9f14..c959fbd9c49 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -248,8 +248,8 @@ class java_method_typet : public code_typet using code_typet::parameterst; using code_typet::parametert; - /// Constructs a new code type, i.e. function type - /// \param _parameters: the vector of function parameters + /// Constructs a new code type, i.e. method type + /// \param _parameters: the vector of method parameters /// \param _return_type: the return type java_method_typet(parameterst &&_parameters, typet &&_return_type) { @@ -258,8 +258,8 @@ class java_method_typet : public code_typet return_type().swap(_return_type); } - /// Constructs a new code type, i.e. function type - /// \param _parameters: the vector of function parameters + /// Constructs a new code type, i.e. method type + /// \param _parameters: the vector of method parameters /// \param _return_type: the return type java_method_typet(parameterst &&_parameters, const typet &_return_type) { From c3b8b5abe652d2588faca7a1201eb4a2161d37f3 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Thu, 2 Aug 2018 12:26:04 +0100 Subject: [PATCH 06/11] Update tag in to_java_method_type --- jbmc/src/java_bytecode/java_types.h | 1 + 1 file changed, 1 insertion(+) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index c959fbd9c49..19e78df063a 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -298,6 +298,7 @@ inline const java_method_typet &to_java_method_type(const typet &type) inline java_method_typet &to_java_method_type(typet &type) { PRECONDITION(type.id() == ID_code); + type.set(ID_C_java_method_type, true); return static_cast(type); } From 6cefc6131a281a386623156e2898780f919b9793 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Thu, 2 Aug 2018 12:26:37 +0100 Subject: [PATCH 07/11] Unit tests conversion from code_typet to java_method_typet --- jbmc/unit/Makefile | 1 + .../java_types/java_method_type.cpp | 35 +++++++++++++++++++ 2 files changed, 36 insertions(+) create mode 100644 jbmc/unit/java_bytecode/java_types/java_method_type.cpp diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 6c491f75827..4da0d04fa0d 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -21,6 +21,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \ java_bytecode/java_types/erase_type_arguments.cpp \ java_bytecode/java_types/generic_type_index.cpp \ java_bytecode/java_types/java_generic_symbol_type.cpp \ + java_bytecode/java_types/java_method_type.cpp \ java_bytecode/java_types/java_type_from_string.cpp \ java_bytecode/java_utils_test.cpp \ java_bytecode/load_method_by_regex.cpp \ diff --git a/jbmc/unit/java_bytecode/java_types/java_method_type.cpp b/jbmc/unit/java_bytecode/java_types/java_method_type.cpp new file mode 100644 index 00000000000..c44206a6be0 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_types/java_method_type.cpp @@ -0,0 +1,35 @@ +/*******************************************************************\ + + Module: Unit tests for java_types + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include + +SCENARIO("java_method_type", "[core][java_types]") +{ + GIVEN("A code_typet") + { + code_typet::parameterst parameters; + typet return_type; + code_typet code_type = code_typet(); + THEN("It has id code_typet and not java_method_typet") + { + REQUIRE(code_type.id() == ID_code); + REQUIRE_FALSE(code_type.get_bool(ID_C_java_method_type)); + } + + WHEN("It is converted to a java_method_typet") + { + THEN("It should have id code_typet and java_method_typet") + { + java_method_typet method_type = to_java_method_type(code_type); + REQUIRE(method_type.id() == ID_code); + REQUIRE(method_type.get_bool(ID_C_java_method_type)); + } + } + } +} From 78f7cb798820f3b8dcf2e48c1f8e4d37987832ff Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Mon, 6 Aug 2018 15:37:20 +0100 Subject: [PATCH 08/11] Refactor constructors for java_method_typet --- jbmc/src/java_bytecode/java_types.h | 13 ++----------- .../string_refinement/string_symbol_resolution.cpp | 5 ++++- 2 files changed, 6 insertions(+), 12 deletions(-) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 19e78df063a..cb28bb4bb64 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -252,25 +252,16 @@ class java_method_typet : public code_typet /// \param _parameters: the vector of method parameters /// \param _return_type: the return type java_method_typet(parameterst &&_parameters, typet &&_return_type) + : code_typet(std::move(_parameters), std::move(_return_type)) { set(ID_C_java_method_type, true); - parameters().swap(_parameters); - return_type().swap(_return_type); } /// Constructs a new code type, i.e. method type /// \param _parameters: the vector of method parameters /// \param _return_type: the return type java_method_typet(parameterst &&_parameters, const typet &_return_type) - { - set(ID_C_java_method_type, true); - parameters().swap(_parameters); - return_type() = _return_type; - } - - /// \deprecated - DEPRECATED("Use the two argument constructor instead") - java_method_typet() + : code_typet(std::move(_parameters), _return_type) { set(ID_C_java_method_type, true); } diff --git a/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp b/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp index 587eb8d4812..443e9126a5f 100644 --- a/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp +++ b/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp @@ -64,7 +64,10 @@ SCENARIO("string_identifiers_resolution_from_equations", WHEN("There is a function call") { - symbol_exprt fun_sym("f", java_method_typet()); + java_method_typet::parameterst parameters; + typet return_type; + symbol_exprt fun_sym( + "f", java_method_typet(std::move(parameters), return_type)); function_application_exprt fun(fun_sym, bool_typet()); fun.operands().push_back(c); symbol_exprt bool_sym("bool_b", bool_typet()); From 6cb7e5d50f1c335c1428e2b87d79fa7567a409d7 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Mon, 6 Aug 2018 15:39:19 +0100 Subject: [PATCH 09/11] Reinstate require_code and add require_java_method --- jbmc/unit/java-testing-utils/require_type.cpp | 37 ++++++++++--- jbmc/unit/java-testing-utils/require_type.h | 12 +++-- .../convert_initalizers.cpp | 4 +- .../convert_method.cpp | 2 +- .../parse_bounded_generic_inner_classes.cpp | 2 +- .../parse_functions_with_generics.cpp | 10 ++-- ...neric_class_with_generic_inner_classes.cpp | 42 +++++++-------- .../parse_generic_functions.cpp | 44 ++++++++-------- .../parse_nested_generics.cpp | 52 +++++++++---------- 9 files changed, 115 insertions(+), 90 deletions(-) diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index c2e9fbb67a4..fb0d40e9470 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -54,10 +54,33 @@ struct_union_typet::componentt require_type::require_component( /// Checks a type is a code_type (i.e. a function) /// \param type: The type to check -/// \return The cast version of the type method_type -java_method_typet require_type::require_code(const typet &type) +/// \return The cast version of the type code_type +code_typet require_type::require_code(const typet &type) { REQUIRE(type.id() == ID_code); + 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; +} + +/// Checks a type is a java_method_typet (i.e. a function) +/// \param type: The type to check +/// \return The cast version of the type method_type +java_method_typet require_type::require_java_method(const typet &type) +{ + REQUIRE(can_cast_type(type)); return to_java_method_type(type); } @@ -68,9 +91,9 @@ java_method_typet require_type::require_code(const typet &type) /// number of parameters /// \return The type cast to a java_method_typet java_method_typet -require_type::require_code(const typet &type, const size_t num_params) +require_type::require_java_method(const typet &type, const size_t num_params) { - java_method_typet method_type = require_code(type); + java_method_typet method_type = require_java_method(type); REQUIRE(method_type.parameters().size() == num_params); return method_type; } @@ -80,14 +103,14 @@ require_type::require_code(const typet &type, const size_t num_params) /// \param param_name: The name of the parameter /// \return: A reference to the parameter structure corresponding to this /// parameter name. -java_method_typet::parametert require_type::require_parameter( - const java_method_typet &function_type, +code_typet::parametert require_type::require_parameter( + const code_typet &function_type, const irep_idt ¶m_name) { const auto param = std::find_if( function_type.parameters().begin(), function_type.parameters().end(), - [¶m_name](const java_method_typet::parametert param) { + [¶m_name](const code_typet::parametert param) { return param.get_base_name() == param_name; }); diff --git a/jbmc/unit/java-testing-utils/require_type.h b/jbmc/unit/java-testing-utils/require_type.h index e329fc0c866..168a781b863 100644 --- a/jbmc/unit/java-testing-utils/require_type.h +++ b/jbmc/unit/java-testing-utils/require_type.h @@ -32,13 +32,15 @@ struct_typet::componentt require_component( const struct_typet &struct_type, const irep_idt &component_name); -java_method_typet require_code(const typet &type); +code_typet require_code(const typet &type); +java_method_typet require_java_method(const typet &type); -java_method_typet::parametert require_parameter( - const java_method_typet &function_type, - const irep_idt ¶m_name); +code_typet::parametert +require_parameter(const code_typet &function_type, const irep_idt ¶m_name); -java_method_typet require_code(const typet &type, const size_t num_params); +code_typet require_code(const typet &type, const size_t num_params); +java_method_typet +require_java_method(const typet &type, const size_t num_params); // A mini DSL for describing an expected set of type arguments for a // java_generic_typet diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp index ff497f1594b..a314624c2ec 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp @@ -34,7 +34,7 @@ void require_is_constructor(const test_datat &test_data) THEN("The constructor should be marked as a constructor") { java_method_typet constructor_type = - require_type::require_code(constructor.type); + require_type::require_java_method(constructor.type); REQUIRE(constructor_type.get_is_constructor()); } } @@ -51,7 +51,7 @@ void require_is_static_initializer(const test_datat &test_data) THEN("The constructor should be marked as a constructor") { java_method_typet constructor_type = - require_type::require_code(constructor.type); + require_type::require_java_method(constructor.type); REQUIRE_FALSE(constructor_type.get_is_constructor()); } } diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp index b3f1421b2c7..15901f1c8b7 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp @@ -44,7 +44,7 @@ SCENARIO( symbol_table.lookup_ref(method_name + ":(LClassWithBridgeMethod;)I"); const java_method_typet &function_type = - require_type::require_code(function_symbol.type); + require_type::require_java_method(function_symbol.type); THEN("The method should be marked as a bridge method") { REQUIRE_FALSE(function_type.get_bool(ID_is_bridge_method)); diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp index 9c21e55d3d3..c3718d0cabb 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp @@ -77,7 +77,7 @@ SCENARIO( const symbolt &method_symbol = new_symbol_table.lookup_ref(method_name); const java_method_typet &method_type = - require_type::require_code(method_symbol.type); + require_type::require_java_method(method_symbol.type); const java_method_typet::parametert ¶m = require_type::require_parameter(method_type, "x"); require_type::require_java_generic_parameter( diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp index 289bd642bde..adf4c715165 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp @@ -33,7 +33,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet &func_code = - require_type::require_code(func_symbol.type); + require_type::require_java_method(func_symbol.type); THEN("It has parameter x pointing to Generic") { @@ -82,7 +82,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type); + require_type::require_java_method(func_symbol.type); THEN("It has parameter s pointing to Generic") { @@ -131,7 +131,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type); + require_type::require_java_method(func_symbol.type); THEN("It has parameter x pointing to Generic") { @@ -196,7 +196,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type); + require_type::require_java_method(func_symbol.type); THEN("It has parameter s pointing to Generic") { @@ -262,7 +262,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type); + require_type::require_java_method(func_symbol.type); THEN("It has parameter inner pointing to Inner") { diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp index a85a7c0e90c..ca763c5e463 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp @@ -317,7 +317,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of correct type") { @@ -346,7 +346,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 3); + require_type::require_java_method(function_symbol.type, 3); THEN("The inputs are of correct type") { @@ -382,7 +382,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of correct type") { @@ -413,7 +413,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of correct type") { @@ -443,7 +443,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of correct type") { @@ -477,7 +477,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of correct type") { @@ -509,7 +509,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of correct type") { @@ -545,7 +545,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of correct type") { @@ -577,7 +577,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of the correct type") { @@ -610,7 +610,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of the correct type") { @@ -643,7 +643,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs should be of the correct type") { @@ -673,7 +673,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type should be correct") { @@ -700,7 +700,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type should be correct") { @@ -730,7 +730,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type should be correct") { @@ -759,7 +759,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type should be correct") { @@ -791,7 +791,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type should be correct") { @@ -821,7 +821,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type should be correct") { @@ -855,7 +855,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type should be correct") { @@ -886,7 +886,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type should be correct") { @@ -918,7 +918,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type should be correct") { @@ -950,7 +950,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type should be correct") { diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp index 3de8b022984..b7dbdcdb1b0 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp @@ -33,7 +33,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { const java_method_typet::parametert ¶m_x = @@ -60,7 +60,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { const java_method_typet::parametert ¶m_x = @@ -87,7 +87,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { const java_method_typet::parametert ¶m_x = @@ -114,7 +114,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter x pointing to java.lang.Number") { const java_method_typet::parametert ¶m_x = @@ -141,7 +141,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { const java_method_typet::parametert ¶m_x = @@ -168,7 +168,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { const java_method_typet::parametert ¶m_x = @@ -195,7 +195,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 2); + require_type::require_java_method(func_symbol.type, 2); THEN("It contains parameter t pointing to Generic") { @@ -233,7 +233,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 2); + require_type::require_java_method(func_symbol.type, 2); THEN("It contains parameter t pointing to Generic") { @@ -272,7 +272,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 0); + require_type::require_java_method(func_symbol.type, 0); THEN("It has return type pointing to Generic") { require_type::require_pointer( @@ -298,7 +298,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 0); + require_type::require_java_method(func_symbol.type, 0); THEN("It has return type pointing to java.lang.Object") { require_type::require_pointer( @@ -347,7 +347,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 0); + require_type::require_java_method(func_symbol.type, 0); THEN("It has return type pointing to Generic") { require_type::require_pointer( @@ -372,7 +372,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 0); + require_type::require_java_method(func_symbol.type, 0); THEN("It has return type pointing to Generic") { require_type::require_pointer( @@ -397,7 +397,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 0); + require_type::require_java_method(func_symbol.type, 0); THEN("It has return type pointing to Generic") { require_type::require_pointer( @@ -423,7 +423,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { @@ -460,7 +460,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { @@ -497,7 +497,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { @@ -534,7 +534,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { @@ -572,7 +572,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter x pointing to Generic") { @@ -609,7 +609,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter u pointing to Generic") { @@ -646,7 +646,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 1); + require_type::require_java_method(func_symbol.type, 1); THEN("It contains parameter u pointing to Generic") { @@ -683,7 +683,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 2); + require_type::require_java_method(func_symbol.type, 2); THEN("It contains parameter u pointing to Generic") { @@ -731,7 +731,7 @@ SCENARIO( const symbolt func_symbol = new_symbol_table.lookup_ref(process_func_name); const java_method_typet func_code = - require_type::require_code(func_symbol.type, 2); + require_type::require_java_method(func_symbol.type, 2); THEN("It contains parameter u pointing to Generic") { diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp index 0bfef784b76..d7b03574414 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp @@ -418,7 +418,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of correct type") { @@ -456,7 +456,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of oorrect type") { @@ -494,7 +494,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of correct type") { @@ -539,7 +539,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of correct type") { @@ -584,7 +584,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs are of correct type") { @@ -625,7 +625,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs have correct type") { @@ -666,7 +666,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs have correct type") { @@ -707,7 +707,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs have correct type") { @@ -752,7 +752,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs have correct type") { @@ -797,7 +797,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs have correct type") { @@ -842,7 +842,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs have correct type") { @@ -883,7 +883,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs have correct type") { @@ -930,7 +930,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 2); + require_type::require_java_method(function_symbol.type, 2); THEN("The inputs have correct type") { @@ -977,7 +977,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { @@ -1013,7 +1013,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { @@ -1049,7 +1049,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { @@ -1091,7 +1091,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { @@ -1133,7 +1133,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { @@ -1172,7 +1172,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { @@ -1211,7 +1211,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { @@ -1250,7 +1250,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { @@ -1293,7 +1293,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { @@ -1336,7 +1336,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { @@ -1379,7 +1379,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { @@ -1418,7 +1418,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { @@ -1463,7 +1463,7 @@ SCENARIO( new_symbol_table.lookup_ref(process_func_name); const java_method_typet &function_call = - require_type::require_code(function_symbol.type, 1); + require_type::require_java_method(function_symbol.type, 1); THEN("The return type is correct") { From 273fff44b01c661b61ef2251d08424cd7388f65c Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Mon, 6 Aug 2018 15:40:36 +0100 Subject: [PATCH 10/11] Add can_cast_type and precondition. Also removes an irrelevant unit test due to this change. --- jbmc/src/java_bytecode/java_types.h | 11 ++++-- jbmc/unit/Makefile | 1 - .../convert_method.cpp | 8 +++-- .../java_types/java_method_type.cpp | 35 ------------------- 4 files changed, 14 insertions(+), 41 deletions(-) delete mode 100644 jbmc/unit/java_bytecode/java_types/java_method_type.cpp diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index cb28bb4bb64..0ca7538e95a 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -280,16 +280,21 @@ class java_method_typet : public code_typet } }; +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_code && type.get_bool(ID_C_java_method_type); +} + inline const java_method_typet &to_java_method_type(const typet &type) { - PRECONDITION(type.id() == ID_code); + PRECONDITION(can_cast_type(type)); return static_cast(type); } inline java_method_typet &to_java_method_type(typet &type) { - PRECONDITION(type.id() == ID_code); - type.set(ID_C_java_method_type, true); + PRECONDITION(can_cast_type(type)); return static_cast(type); } diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 4da0d04fa0d..6c491f75827 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -21,7 +21,6 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \ java_bytecode/java_types/erase_type_arguments.cpp \ java_bytecode/java_types/generic_type_index.cpp \ java_bytecode/java_types/java_generic_symbol_type.cpp \ - java_bytecode/java_types/java_method_type.cpp \ java_bytecode/java_types/java_type_from_string.cpp \ java_bytecode/java_utils_test.cpp \ java_bytecode/load_method_by_regex.cpp \ diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp index 15901f1c8b7..76aa4e0155e 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp @@ -30,8 +30,12 @@ SCENARIO( symbol_table.lookup_ref(method_name + ":(Ljava/lang/Object;)I"); const java_method_typet &function_type = - require_type::require_code(function_symbol.type); - THEN("The method should be marked as a bridge method") + require_type::require_java_method(function_symbol.type); + THEN("The method symbol should be of java_method_typet") + { + REQUIRE(function_type.get_bool(ID_C_java_method_type)); + } + THEN("And the method should be marked as a bridge method") { REQUIRE(function_type.get_bool(ID_is_bridge_method)); } diff --git a/jbmc/unit/java_bytecode/java_types/java_method_type.cpp b/jbmc/unit/java_bytecode/java_types/java_method_type.cpp deleted file mode 100644 index c44206a6be0..00000000000 --- a/jbmc/unit/java_bytecode/java_types/java_method_type.cpp +++ /dev/null @@ -1,35 +0,0 @@ -/*******************************************************************\ - - Module: Unit tests for java_types - - Author: Diffblue Ltd. - -\*******************************************************************/ - -#include -#include - -SCENARIO("java_method_type", "[core][java_types]") -{ - GIVEN("A code_typet") - { - code_typet::parameterst parameters; - typet return_type; - code_typet code_type = code_typet(); - THEN("It has id code_typet and not java_method_typet") - { - REQUIRE(code_type.id() == ID_code); - REQUIRE_FALSE(code_type.get_bool(ID_C_java_method_type)); - } - - WHEN("It is converted to a java_method_typet") - { - THEN("It should have id code_typet and java_method_typet") - { - java_method_typet method_type = to_java_method_type(code_type); - REQUIRE(method_type.id() == ID_code); - REQUIRE(method_type.get_bool(ID_C_java_method_type)); - } - } - } -} From 4dca215f5c9cacab29c3cb7e8845fcc7aa466190 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Wed, 8 Aug 2018 09:33:40 +0100 Subject: [PATCH 11/11] Goto program should not use java_method_typet --- .../remove_virtual_functions_without_fallback.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp index 7bba7e86cb8..fb294c1d148 100644 --- a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp +++ b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp @@ -7,8 +7,6 @@ \*******************************************************************/ -#include - #include #include @@ -135,8 +133,9 @@ SCENARIO( call.function() = callee; // Specific argument doesn't matter, so just pass an appropriately typed // null pointer: - call.arguments().push_back(null_pointer_exprt(to_pointer_type( - to_java_method_type(callee.type()).parameters()[0].type()))); + call.arguments().push_back( + null_pointer_exprt( + to_pointer_type(to_code_type(callee.type()).parameters()[0].type()))); virtual_call_inst->code = call; test_program.add_instruction(END_FUNCTION);