From 32f9b1384b5a0852ca23698b13ce7979e6275cf0 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 28 Sep 2018 19:57:14 +0100 Subject: [PATCH 1/5] java frontend: symbol_type -> struct_tag --- jbmc/src/java_bytecode/ci_lazy_methods.cpp | 2 +- .../java_bytecode/ci_lazy_methods_needed.cpp | 10 +- ...eric_parameter_specialization_map_keys.cpp | 12 +-- ...eneric_parameter_specialization_map_keys.h | 6 +- ...a_bytecode_concurrency_instrumentation.cpp | 2 +- .../java_bytecode_convert_class.cpp | 52 +++++----- .../java_bytecode_convert_method.cpp | 30 +++--- .../java_bytecode_instrument.cpp | 3 +- .../java_bytecode/java_bytecode_language.cpp | 2 +- .../java_bytecode_parse_tree.cpp | 4 +- .../java_bytecode/java_bytecode_parse_tree.h | 2 +- .../java_bytecode/java_bytecode_parser.cpp | 18 ++-- .../java_bytecode_typecheck_type.cpp | 4 +- jbmc/src/java_bytecode/java_entry_point.cpp | 6 +- .../src/java_bytecode/java_object_factory.cpp | 10 +- .../java_string_library_preprocess.cpp | 57 +++++------ .../java_bytecode/java_string_literals.cpp | 4 +- jbmc/src/java_bytecode/java_types.cpp | 96 ++++++++++--------- jbmc/src/java_bytecode/java_types.h | 39 ++++---- jbmc/src/java_bytecode/remove_exceptions.cpp | 2 +- jbmc/src/java_bytecode/remove_instanceof.cpp | 8 +- jbmc/src/java_bytecode/remove_java_new.cpp | 4 +- .../src/java_bytecode/select_pointer_type.cpp | 7 +- jbmc/src/java_bytecode/select_pointer_type.h | 4 +- .../require_goto_statements.cpp | 5 +- jbmc/unit/java-testing-utils/require_type.cpp | 34 +++---- jbmc/unit/java-testing-utils/require_type.h | 10 +- .../generic_parameters_test.cpp | 2 +- .../mutually_recursive_generics.cpp | 12 ++- .../convert_abstract_class.cpp | 30 +++--- .../convert_java_annotations.cpp | 4 +- .../convert_invoke_dynamic.cpp | 6 +- .../parse_bounded_generic_inner_classes.cpp | 2 +- .../parse_derived_generic_class.cpp | 76 +++++++-------- .../parse_functions_with_generics.cpp | 24 ++--- .../parse_generic_array_class.cpp | 24 ++--- .../parse_generic_class.cpp | 2 +- ...neric_class_with_generic_inner_classes.cpp | 71 +++++++------- ...parse_generic_class_with_inner_classes.cpp | 13 +-- .../parse_generic_fields.cpp | 20 ++-- .../parse_generic_functions.cpp | 72 +++++++------- .../parse_generic_superclasses.cpp | 12 +-- .../parse_nested_generics.cpp | 78 +++++++-------- ...ava_bytecode_parse_lambda_method_table.cpp | 14 +-- .../parse_java_annotations.cpp | 2 +- .../gen_nondet_string_init.cpp | 2 +- .../convert_exprt_to_string_exprt.cpp | 2 +- .../java_types/generic_type_index.cpp | 40 ++++---- .../java_types/java_generic_symbol_type.cpp | 12 +-- .../java_types/java_type_from_string.cpp | 4 +- jbmc/unit/util/has_subtype.cpp | 6 +- src/analyses/uncaught_exceptions_analysis.cpp | 4 +- src/goto-programs/class_identifier.cpp | 4 +- src/goto-programs/class_identifier.h | 6 +- .../remove_virtual_functions.cpp | 2 +- src/goto-programs/string_abstraction.h | 2 +- .../refinement/string_refinement_util.cpp | 4 +- 57 files changed, 506 insertions(+), 479 deletions(-) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 437919ac3fc..f6544b11b41 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -65,7 +65,7 @@ ci_lazy_methodst::ci_lazy_methodst( /// class static bool references_class_model(const exprt &expr) { - static const symbol_typet class_type("java::java.lang.Class"); + static const struct_tag_typet class_type("java::java.lang.Class"); for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it) { diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp index 706d0527f2c..a4f52febcd8 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp @@ -101,7 +101,7 @@ void ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer( const pointer_typet &pointer_type, const namespacet &ns) { - const symbol_typet &class_type = to_symbol_type(pointer_type.subtype()); + const auto &class_type = to_struct_tag_type(pointer_type.subtype()); const auto ¶m_classid = class_type.get_identifier(); // Note here: different arrays may have different element types, so we should @@ -139,10 +139,10 @@ void ci_lazy_methods_neededt::gather_field_types( { // If class_type is not a symbol this may be a reference array, // but we can't tell what type. - if(class_type.id() == ID_symbol_type) + if(class_type.id() == ID_struct_tag) { const typet &element_type = - java_array_element_type(to_symbol_type(class_type)); + java_array_element_type(to_struct_tag_type(class_type)); if(element_type.id() == ID_pointer) { // This is a reference array -- mark its element type available. @@ -154,11 +154,11 @@ void ci_lazy_methods_neededt::gather_field_types( { for(const auto &field : underlying_type.components()) { - if(field.type().id() == ID_struct || field.type().id() == ID_symbol_type) + if(field.type().id() == ID_struct || field.type().id() == ID_struct_tag) gather_field_types(field.type(), ns); else if(field.type().id() == ID_pointer) { - if(field.type().subtype().id() == ID_symbol_type) + if(field.type().subtype().id() == ID_struct_tag) { add_all_needed_classes(to_pointer_type(field.type())); } diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp index 7ecf957925b..f6f91cd0ca2 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp @@ -136,29 +136,29 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer( /// in the form of a symbol rather than a pointer (as opposed to the function /// insert_pairs_for_pointer). Own the keys and pop from their stack /// on destruction; otherwise do nothing. -/// \param symbol_type symbol type to get the specialized generic types from +/// \param struct_tag_type symbol type to get the specialized generic types from /// \param symbol_struct struct type of the symbol type, must be generic if /// the symbol is generic void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol( - const symbol_typet &symbol_type, + const struct_tag_typet &struct_tag_type, const typet &symbol_struct) { // If the struct is: // - an incomplete class or // - a class that is neither generic nor implicitly generic (this // may be due to unsupported class signature) - // then ignore the generic types in the symbol_type and do not add any pairs. + // then ignore the generic types in the struct_tag_type and do not add any pairs. // TODO TG-1996 should decide how mocking and generics should work // together. Currently an incomplete class is never marked as generic. If // this changes in TG-1996 then the condition below should be updated. if( - is_java_generic_symbol_type(symbol_type) && + is_java_generic_struct_tag_type(struct_tag_type) && !to_java_class_type(symbol_struct).get_is_stub() && (is_java_generic_class_type(symbol_struct) || is_java_implicitly_generic_class_type(symbol_struct))) { - const java_generic_symbol_typet &generic_symbol = - to_java_generic_symbol_type(symbol_type); + const java_generic_struct_tag_typet &generic_symbol = + to_java_generic_struct_tag_type(struct_tag_type); const std::vector &generic_parameters = get_all_generic_parameters(symbol_struct); diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h index 84a622b24c1..d518ab5db8a 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h @@ -1,3 +1,4 @@ + /// Author: Diffblue Ltd. #ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H @@ -50,9 +51,8 @@ class generic_parameter_specialization_map_keyst void insert_pairs_for_pointer( const pointer_typet &pointer_type, const typet &pointer_subtype_struct); - void insert_pairs_for_symbol( - const symbol_typet &symbol_type, - const typet &symbol_struct); + void + insert_pairs_for_symbol(const struct_tag_typet &, const typet &symbol_struct); private: /// Generic parameter specialization map to modify diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp index 27413c16309..89c6f6c0c09 100644 --- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp @@ -230,7 +230,7 @@ static void instrument_synchronized_code( // Create the finally block with the same label targeted in the catch-push const symbolt &tmp_symbol = get_fresh_aux_symbol( - java_reference_type(symbol_typet("java::java.lang.Throwable")), + java_reference_type(struct_tag_typet("java::java.lang.Throwable")), id2string(symbol.name), "caught-synchronized-exception", code.source_location(), diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 86bc7707ba9..6200190276f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -338,7 +338,7 @@ void java_bytecode_convert_classt::convert( if(!c.super_class.empty()) { - const symbol_typet base("java::" + id2string(c.super_class)); + const struct_tag_typet base("java::" + id2string(c.super_class)); // if the superclass is generic then the class has the superclass reference // including the generic info in its signature @@ -350,7 +350,7 @@ void java_bytecode_convert_classt::convert( { try { - const java_generic_symbol_typet generic_base( + const java_generic_struct_tag_typet generic_base( base, superclass_ref.value(), qualified_classname); class_type.add_base(generic_base); } @@ -378,7 +378,7 @@ void java_bytecode_convert_classt::convert( // interfaces are recorded as bases for(const auto &interface : c.implements) { - const symbol_typet base("java::" + id2string(interface)); + const struct_tag_typet base("java::" + id2string(interface)); // if the interface is generic then the class has the interface reference // including the generic info in its signature @@ -390,7 +390,7 @@ void java_bytecode_convert_classt::convert( { try { - const java_generic_symbol_typet generic_base( + const java_generic_struct_tag_typet generic_base( base, interface_ref.value(), qualified_classname); class_type.add_base(generic_base); } @@ -774,26 +774,27 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) for(const char l : letters) { - symbol_typet symbol_type= - to_symbol_type(java_array_type(l).subtype()); + struct_tag_typet struct_tag_type = + to_struct_tag_type(java_array_type(l).subtype()); - const irep_idt &symbol_type_identifier=symbol_type.get_identifier(); - if(symbol_table.has_symbol(symbol_type_identifier)) + const irep_idt &struct_tag_type_identifier = + struct_tag_type.get_identifier(); + if(symbol_table.has_symbol(struct_tag_type_identifier)) return; java_class_typet class_type; // we have the base class, java.lang.Object, length and data // of appropriate type - class_type.set_tag(symbol_type_identifier); + class_type.set_tag(struct_tag_type_identifier); // Note that non-array types don't have "java::" at the beginning of their // tag, and their name is "java::" + their tag. Since arrays do have // "java::" at the beginning of their tag we set the name to be the same as // the tag. - class_type.set_name(symbol_type_identifier); + class_type.set_name(struct_tag_type_identifier); class_type.components().reserve(3); class_typet::componentt base_class_component( - "@java.lang.Object", symbol_typet("java::java.lang.Object")); + "@java.lang.Object", struct_tag_typet("java::java.lang.Object")); base_class_component.set_pretty_name("@java.lang.Object"); base_class_component.set_base_name("@java.lang.Object"); class_type.components().push_back(base_class_component); @@ -809,7 +810,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) data_component.set_base_name("data"); class_type.components().push_back(data_component); - class_type.add_base(symbol_typet("java::java.lang.Object")); + class_type.add_base(struct_tag_typet("java::java.lang.Object")); INVARIANT( is_valid_java_array(class_type), @@ -817,8 +818,8 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) "object that doesn't match expectations"); symbolt symbol; - symbol.name=symbol_type_identifier; - symbol.base_name=symbol_type.get(ID_C_base_name); + symbol.name = struct_tag_type_identifier; + symbol.base_name = struct_tag_type.get(ID_C_base_name); symbol.is_type=true; symbol.type = class_type; symbol.mode = ID_java; @@ -827,13 +828,13 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) // Also provide a clone method: // ---------------------------- - const irep_idt clone_name= - id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;"; + const irep_idt clone_name = + id2string(struct_tag_type_identifier) + ".clone:()Ljava/lang/Object;"; 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); + this_param.type() = java_reference_type(struct_tag_type); const java_method_typet clone_type({this_param}, java_lang_object_type()); parameter_symbolt this_symbol; @@ -850,7 +851,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) local_symbol.name=local_name; local_symbol.base_name="cloned_array"; local_symbol.pretty_name=local_symbol.base_name; - local_symbol.type=java_reference_type(symbol_type); + local_symbol.type = java_reference_type(struct_tag_type); local_symbol.mode=ID_java; symbol_table.add(local_symbol); const auto &local_symexpr=local_symbol.symbol_expr(); @@ -860,9 +861,9 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) source_locationt location; location.set_function(local_name); side_effect_exprt java_new_array( - ID_java_new_array, java_reference_type(symbol_type), location); - dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type); - dereference_exprt new_array(local_symexpr, symbol_type); + ID_java_new_array, java_reference_type(struct_tag_type), location); + dereference_exprt old_array(this_symbol.symbol_expr(), struct_tag_type); + dereference_exprt new_array(local_symexpr, struct_tag_type); member_exprt old_length( old_array, length_component.get_name(), length_component.type()); java_new_array.copy_to_operands(old_length); @@ -923,8 +924,8 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) symbolt clone_symbol; clone_symbol.name=clone_name; - clone_symbol.pretty_name= - id2string(symbol_type_identifier)+".clone:()"; + clone_symbol.pretty_name = + id2string(struct_tag_type_identifier) + ".clone:()"; clone_symbol.base_name="clone"; clone_symbol.type=clone_type; clone_symbol.value=clone_body; @@ -1053,9 +1054,10 @@ static void find_and_replace_parameters( find_and_replace_parameters(argument, replacement_parameters); } } - else if(is_java_generic_symbol_type(type)) + else if(is_java_generic_struct_tag_type(type)) { - java_generic_symbol_typet &generic_base = to_java_generic_symbol_type(type); + java_generic_struct_tag_typet &generic_base = + to_java_generic_struct_tag_type(type); std::vector &gen_types = generic_base.generic_types(); for(auto &gen_type : gen_types) { diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 0f68c94e4f2..0393e41f1eb 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -380,8 +380,8 @@ void java_bytecode_convert_method_lazy( { 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)); + const reference_typet object_ref_type = + java_reference_type(struct_tag_typet(class_symbol.name)); this_p.type()=object_ref_type; this_p.set_this(); parameters.insert(parameters.begin(), this_p); @@ -655,7 +655,7 @@ static irep_idt get_if_cmp_operator(const irep_idt &stmt) static member_exprt to_member(const exprt &pointer, const exprt &fieldref) { - symbol_typet class_type(fieldref.get(ID_class)); + struct_tag_typet class_type(fieldref.get(ID_class)); const typecast_exprt pointer2(pointer, java_reference_type(class_type)); @@ -1181,9 +1181,11 @@ code_blockt java_bytecode_convert_methodt::convert_instructions( { if(cur_pc==it->handler_pc) { - if(catch_type != typet() || it->catch_type == symbol_typet(irep_idt())) + if( + catch_type != typet() || + it->catch_type == struct_tag_typet(irep_idt())) { - catch_type=symbol_typet("java::java.lang.Throwable"); + catch_type = struct_tag_typet("java::java.lang.Throwable"); break; } else @@ -1617,7 +1619,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions( const typecast_exprt pointer(op[0], java_array_type(statement[0])); dereference_exprt array(pointer, pointer.type().subtype()); - PRECONDITION(pointer.type().subtype().id() == ID_symbol_type); + PRECONDITION(pointer.type().subtype().id() == ID_struct_tag); array.set(ID_java_member_access, true); const member_exprt length(array, "length", java_int_type()); @@ -2088,7 +2090,7 @@ void java_bytecode_convert_methodt::convert_invoke( if(parameters.empty() || !parameters[0].get_this()) { irep_idt classname = arg0.get(ID_C_class); - typet thistype = symbol_typet(classname); + typet thistype = struct_tag_typet(classname); // Note invokespecial is used for super-method calls as well as // constructors. if(statement == "invokespecial") @@ -2504,7 +2506,7 @@ void java_bytecode_convert_methodt::convert_new( c = code_assignt(tmp, java_new_expr); c.add_source_location() = location; codet clinit_call = - get_clinit_call(to_symbol_type(arg0.type()).get_identifier()); + get_clinit_call(to_struct_tag_type(arg0.type()).get_identifier()); if(clinit_call.get_statement() != ID_skip) { c = code_blockt({clinit_call, c}); @@ -2518,10 +2520,10 @@ code_blockt java_bytecode_convert_methodt::convert_putstatic( const exprt::operandst &op, const symbol_exprt &symbol_expr) { - if(needed_lazy_methods && arg0.type().id() == ID_symbol_type) + if(needed_lazy_methods && arg0.type().id() == ID_struct_tag) { needed_lazy_methods->add_needed_class( - to_symbol_type(arg0.type()).get_identifier()); + to_struct_tag_type(arg0.type()).get_identifier()); } code_blockt block; @@ -2566,18 +2568,18 @@ void java_bytecode_convert_methodt::convert_getstatic( { if(needed_lazy_methods) { - if(arg0.type().id() == ID_symbol_type) + if(arg0.type().id() == ID_struct_tag) { needed_lazy_methods->add_needed_class( - to_symbol_type(arg0.type()).get_identifier()); + to_struct_tag_type(arg0.type()).get_identifier()); } else if(arg0.type().id() == ID_pointer) { const auto &pointer_type = to_pointer_type(arg0.type()); - if(pointer_type.subtype().id() == ID_symbol_type) + if(pointer_type.subtype().id() == ID_struct_tag) { needed_lazy_methods->add_needed_class( - to_symbol_type(pointer_type.subtype()).get_identifier()); + to_struct_tag_type(pointer_type.subtype()).get_identifier()); } } else if(is_assertions_disabled_field) diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp index 5af959797e9..085175ad806 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp @@ -108,8 +108,7 @@ code_ifthenelset java_bytecode_instrumentt::throw_exception( struct_union_typet::componentst{}); } - pointer_typet exc_ptr_type= - pointer_type(symbol_typet(exc_class_name)); + pointer_typet exc_ptr_type = pointer_type(struct_tag_typet(exc_class_name)); // Allocate and throw an instance of the exception class: diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 5f929f819f6..ae533e6b4f7 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -362,7 +362,7 @@ static void infer_opaque_type_fields( static symbol_exprt get_or_create_class_literal_symbol( const irep_idt &class_id, symbol_tablet &symbol_table) { - symbol_typet java_lang_Class("java::java.lang.Class"); + struct_tag_typet java_lang_Class("java::java.lang.Class"); symbol_exprt symbol_expr( id2string(class_id) + JAVA_CLASS_MODEL_SUFFIX, java_lang_Class); diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp index f44fe673a1c..c031d171547 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp @@ -105,8 +105,8 @@ java_bytecode_parse_treet::find_annotation( if(annotation.type.id() != ID_pointer) return false; const typet &type = annotation.type.subtype(); - return type.id() == ID_symbol_type && - to_symbol_type(type).get_identifier() == annotation_type_name; + return type.id() == ID_struct_tag && + to_struct_tag_type(type).get_identifier() == annotation_type_name; }); if(annotation_it == annotations.end()) return {}; diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index b58b6c8acd7..9a9fe8c0c20 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -117,7 +117,7 @@ struct java_bytecode_parse_treet std::size_t start_pc; std::size_t end_pc; std::size_t handler_pc; - symbol_typet catch_type; + struct_tag_typet catch_type; }; typedef std::vector exception_tablet; diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index ce9e534b14a..2c7f8f4eb2b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -629,7 +629,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src) for(const auto &p : ct.parameters()) get_class_refs_rec(p.type()); } - else if(src.id()==ID_symbol_type) + else if(src.id() == ID_struct_tag) { irep_idt name=src.get(ID_C_base_name); if(has_prefix(id2string(name), "array[")) @@ -797,11 +797,9 @@ void java_bytecode_parsert::rconstant_pool() const pool_entryt &class_name_entry=pool_entry(class_entry.ref1); typet type=type_entry(nameandtype_entry.ref2); - symbol_typet class_symbol= - java_classname(id2string(class_name_entry.s)); + auto class_tag = java_classname(id2string(class_name_entry.s)); - fieldref_exprt fieldref( - type, name_entry.s, class_symbol.get_identifier()); + fieldref_exprt fieldref(type, name_entry.s, class_tag.get_identifier()); it->expr=fieldref; } @@ -816,15 +814,13 @@ void java_bytecode_parsert::rconstant_pool() const pool_entryt &class_name_entry=pool_entry(class_entry.ref1); typet type=type_entry(nameandtype_entry.ref2); - symbol_typet class_symbol= - java_classname(id2string(class_name_entry.s)); + auto class_tag = java_classname(id2string(class_name_entry.s)); irep_idt component_name= id2string(name_entry.s)+ ":"+id2string(pool_entry(nameandtype_entry.ref2).s); - irep_idt class_name= - class_symbol.get_identifier(); + irep_idt class_name = class_tag.get_identifier(); irep_idt identifier= id2string(class_name)+"."+id2string(component_name); @@ -1252,8 +1248,8 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method) method.exception_table[e].end_pc=end_pc; method.exception_table[e].handler_pc=handler_pc; if(catch_type!=0) - method.exception_table[e].catch_type= - to_symbol_type(pool_entry(catch_type).expr.type()); + method.exception_table[e].catch_type = + to_struct_tag_type(pool_entry(catch_type).expr.type()); } u2 attributes_count=read_u2(); diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp index e3ddf9e6427..c85e2c12bd0 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp @@ -16,9 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com void java_bytecode_typecheckt::typecheck_type(typet &type) { - if(type.id() == ID_symbol_type) + if(type.id() == ID_struct_tag) { - irep_idt identifier=to_symbol_type(type).get_identifier(); + irep_idt identifier = to_struct_tag_type(type).get_identifier(); auto type_symbol = symbol_table.lookup(identifier); DATA_INVARIANT( diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 2626562568c..2bc0b7242e2 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -106,7 +106,7 @@ static const symbolt *get_class_literal_initializer( { if(symbol.value.is_not_nil()) return nullptr; - if(symbol.type != symbol_typet("java::java.lang.Class")) + if(symbol.type != struct_tag_typet("java::java.lang.Class")) return nullptr; if(!has_suffix(id2string(symbol.name), JAVA_CLASS_MODEL_SUFFIX)) return nullptr; @@ -202,7 +202,7 @@ static void java_static_lifetime_init( throw 0; } set_class_identifier( - to_struct_expr(*zero_object), ns, to_symbol_type(sym.type)); + to_struct_expr(*zero_object), ns, to_struct_tag_type(sym.type)); code_block.add( std::move(code_assignt(sym.symbol_expr(), *zero_object))); @@ -370,7 +370,7 @@ exprt::operandst java_build_arguments( main_arguments[param_number] = result_symbol.symbol_expr(); std::vector cases(alternatives.size()); - const auto initialize_parameter = [&](const symbol_typet &type) { + const auto initialize_parameter = [&](const struct_tag_typet &type) { code_blockt init_code_for_type; exprt init_expr_for_parameter = object_factory( java_reference_type(type), diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 98bf4839714..e01067e8e09 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -602,7 +602,7 @@ bool initialize_nondet_string_fields( if(struct_type.get_tag() == "java.lang.CharSequence") { set_class_identifier( - struct_expr, ns, symbol_typet("java::java.lang.String")); + struct_expr, ns, struct_tag_typet("java::java.lang.String")); } // OK, this is a String type with the expected fields -- add code to `code` @@ -1018,7 +1018,7 @@ void java_object_factoryt::gen_nondet_struct_init( CHECK_RETURN(initial_object.has_value()); irep_idt qualified_clsid = "java::" + id2string(class_identifier); set_class_identifier( - to_struct_expr(*initial_object), ns, symbol_typet(qualified_clsid)); + to_struct_expr(*initial_object), ns, struct_tag_typet(qualified_clsid)); // If the initialised type is a special-cased String type (one with length // and data fields introduced by string-library preprocessing), initialise @@ -1191,9 +1191,9 @@ void java_object_factoryt::gen_nondet_init( if(is_sub) { const typet &symbol = override_ ? override_type : expr.type(); - PRECONDITION(symbol.id() == ID_symbol_type); + PRECONDITION(symbol.id() == ID_struct_tag); generic_parameter_specialization_map_keys.insert_pairs_for_symbol( - to_symbol_type(symbol), struct_type); + to_struct_tag_type(symbol), struct_type); } gen_nondet_struct_init( @@ -1327,7 +1327,7 @@ void java_object_factoryt::gen_nondet_array_init( const source_locationt &location) { PRECONDITION(expr.type().id()==ID_pointer); - PRECONDITION(expr.type().subtype().id() == ID_symbol_type); + PRECONDITION(expr.type().subtype().id() == ID_struct_tag); PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE); const typet &type=ns.follow(expr.type().subtype()); diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index bd2691cbfda..666762b690b 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -36,8 +36,8 @@ Date: April 2017 static irep_idt get_tag(const typet &type) { /// \todo Use follow instead of assuming tag to symbol relationship. - if(type.id() == ID_symbol_type) - return to_symbol_type(type).get_identifier(); + if(type.id() == ID_struct_tag) + return to_struct_tag_type(type).get_identifier(); else if(type.id() == ID_struct) return irep_idt("java::" + id2string(to_struct_type(type).get_tag())); else @@ -214,7 +214,8 @@ void java_string_library_preprocesst::add_string_type( string_type.components().resize(3); string_type.components()[0].set_name("@java.lang.Object"); string_type.components()[0].set_pretty_name("@java.lang.Object"); - string_type.components()[0].type()=symbol_typet("java::java.lang.Object"); + string_type.components()[0].type() = + struct_tag_typet("java::java.lang.Object"); string_type.components()[1].set_name("length"); string_type.components()[1].set_pretty_name("length"); string_type.components()[1].type()=string_length_type(); @@ -222,11 +223,11 @@ void java_string_library_preprocesst::add_string_type( string_type.components()[2].set_pretty_name("data"); string_type.components()[2].type() = pointer_type(java_char_type()); string_type.set_access(ID_public); - string_type.add_base(symbol_typet("java::java.lang.Object")); + string_type.add_base(struct_tag_typet("java::java.lang.Object")); std::vector bases = get_string_type_base_classes(class_name); for(const irep_idt &base_name : bases) - string_type.add_base(symbol_typet("java::" + id2string(base_name))); + string_type.add_base(struct_tag_typet("java::" + id2string(base_name))); symbolt tmp_string_symbol; tmp_string_symbol.name="java::"+id2string(class_name); @@ -383,12 +384,12 @@ java_string_library_preprocesst::process_equals_function_operands( static const typet & get_data_type(const typet &type, const symbol_tablet &symbol_table) { - PRECONDITION(type.id() == ID_struct || type.id() == ID_symbol_type); - if(type.id() == ID_symbol_type) + PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag); + if(type.id() == ID_struct_tag) { const symbolt &sym = - symbol_table.lookup_ref(to_symbol_type(type).get_identifier()); - CHECK_RETURN(sym.type.id() != ID_symbol_type); + symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier()); + CHECK_RETURN(sym.type.id() != ID_struct_tag); return get_data_type(sym.type, symbol_table); } // else type id is ID_struct @@ -403,12 +404,12 @@ get_data_type(const typet &type, const symbol_tablet &symbol_table) static const typet & get_length_type(const typet &type, const symbol_tablet &symbol_table) { - PRECONDITION(type.id() == ID_struct || type.id() == ID_symbol_type); - if(type.id() == ID_symbol_type) + PRECONDITION(type.id() == ID_struct || type.id() == ID_struct_tag); + if(type.id() == ID_struct_tag) { const symbolt &sym = - symbol_table.lookup_ref(to_symbol_type(type).get_identifier()); - CHECK_RETURN(sym.type.id() != ID_symbol_type); + symbol_table.lookup_ref(to_struct_tag_type(type).get_identifier()); + CHECK_RETURN(sym.type.id() != ID_struct_tag); return get_length_type(sym.type, symbol_table); } // else type id is ID_struct @@ -881,9 +882,11 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr( PRECONDITION(implements_java_char_sequence_pointer(rhs.type())); typet deref_type; - if(rhs.type().subtype().id() == ID_symbol_type) - deref_type=symbol_table.lookup_ref( - to_symbol_type(rhs.type().subtype()).get_identifier()).type; + if(rhs.type().subtype().id() == ID_struct_tag) + deref_type = + symbol_table + .lookup_ref(to_struct_tag_type(rhs.type().subtype()).get_identifier()) + .type; else deref_type=rhs.type().subtype(); @@ -1180,48 +1183,48 @@ java_string_library_preprocesst::get_primitive_value_of_object( symbol_table_baset &symbol_table, code_blockt &code) { - optionalt object_type; + optionalt object_type; typet value_type; if(type_name==ID_boolean) { value_type=java_boolean_type(); - object_type=symbol_typet("java::java.lang.Boolean"); + object_type = struct_tag_typet("java::java.lang.Boolean"); } else if(type_name==ID_char) { value_type=java_char_type(); - object_type=symbol_typet("java::java.lang.Character"); + object_type = struct_tag_typet("java::java.lang.Character"); } else if(type_name==ID_byte) { value_type=java_byte_type(); - object_type=symbol_typet("java::java.lang.Byte"); + object_type = struct_tag_typet("java::java.lang.Byte"); } else if(type_name==ID_short) { value_type=java_short_type(); - object_type=symbol_typet("java::java.lang.Short"); + object_type = struct_tag_typet("java::java.lang.Short"); } else if(type_name==ID_int) { value_type=java_int_type(); - object_type=symbol_typet("java::java.lang.Integer"); + object_type = struct_tag_typet("java::java.lang.Integer"); } else if(type_name==ID_long) { value_type=java_long_type(); - object_type=symbol_typet("java::java.lang.Long"); + object_type = struct_tag_typet("java::java.lang.Long"); } else if(type_name==ID_float) { value_type=java_float_type(); - object_type=symbol_typet("java::java.lang.Float"); + object_type = struct_tag_typet("java::java.lang.Float"); } else if(type_name==ID_double) { value_type=java_double_type(); - object_type=symbol_typet("java::java.lang.Double"); + object_type = struct_tag_typet("java::java.lang.Double"); } else if(type_name==ID_void) return {}; @@ -1381,8 +1384,8 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format( if(name=="string_expr") { - pointer_typet string_pointer= - java_reference_type(symbol_typet("java::java.lang.String")); + pointer_typet string_pointer = + java_reference_type(struct_tag_typet("java::java.lang.String")); typecast_exprt arg_i_as_string(arg_i, string_pointer); code_assign_java_string_to_string_expr( to_string_expr(field_expr), diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp index f00025ec5bb..654f7058a9a 100644 --- a/jbmc/src/java_bytecode/java_string_literals.cpp +++ b/jbmc/src/java_bytecode/java_string_literals.cpp @@ -70,7 +70,7 @@ symbol_exprt get_or_create_string_literal_symbol( { PRECONDITION(string_expr.id() == ID_java_string_literal); const irep_idt value = string_expr.get(ID_value); - const symbol_typet string_type("java::java.lang.String"); + const struct_tag_typet string_type("java::java.lang.String"); const std::string escaped_symbol_name = escape_non_alnum(id2string(value)); const std::string escaped_symbol_name_with_prefix = @@ -96,7 +96,7 @@ symbol_exprt get_or_create_string_literal_symbol( // Regardless of string refinement setting, at least initialize // the literal with @clsid = String - symbol_typet jlo_symbol("java::java.lang.Object"); + struct_tag_typet jlo_symbol("java::java.lang.Object"); const auto &jlo_struct = to_struct_type(ns.follow(jlo_symbol)); struct_exprt jlo_init(jlo_symbol); const auto &jls_struct = to_struct_type(ns.follow(string_type)); diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index d4482012c36..cedd4189e08 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -84,7 +84,7 @@ reference_typet java_reference_type(const typet &subtype) reference_typet java_lang_object_type() { - return java_reference_type(symbol_typet("java::java.lang.Object")); + return java_reference_type(struct_tag_typet("java::java.lang.Object")); } /// Construct an array pointer type. It is a pointer to a symbol with identifier @@ -117,16 +117,16 @@ reference_typet java_array_type(const char subtype) irep_idt class_name="array["+subtype_str+"]"; - symbol_typet symbol_type("java::"+id2string(class_name)); - symbol_type.set(ID_C_base_name, class_name); - symbol_type.set(ID_element_type, java_type_from_char(subtype)); + struct_tag_typet struct_tag_type("java::" + id2string(class_name)); + struct_tag_type.set(ID_C_base_name, class_name); + struct_tag_type.set(ID_element_type, java_type_from_char(subtype)); - return java_reference_type(symbol_type); + return java_reference_type(struct_tag_type); } /// Return a const reference to the element type of a given java array type /// \param array_symbol The java array type -const typet &java_array_element_type(const symbol_typet &array_symbol) +const typet &java_array_element_type(const struct_tag_typet &array_symbol) { DATA_INVARIANT( is_java_array_tag(array_symbol.get_identifier()), @@ -136,7 +136,7 @@ const typet &java_array_element_type(const symbol_typet &array_symbol) /// Return a non-const reference to the element type of a given java array type /// \param array_symbol The java array type -typet &java_array_element_type(symbol_typet &array_symbol) +typet &java_array_element_type(struct_tag_typet &array_symbol) { DATA_INVARIANT( is_java_array_tag(array_symbol.get_identifier()), @@ -149,12 +149,12 @@ bool is_java_array_type(const typet &type) { if( !can_cast_type(type) || - !can_cast_type(type.subtype())) + !can_cast_type(type.subtype())) { return false; } - const auto &subtype_symbol = to_symbol_type(type.subtype()); - return is_java_array_tag(subtype_symbol.get_identifier()); + const auto &subtype_struct_tag = to_struct_tag_type(type.subtype()); + return is_java_array_tag(subtype_struct_tag.get_identifier()); } /// Checks whether the given type is a multi-dimensional array pointer type, @@ -162,9 +162,8 @@ bool is_java_array_type(const typet &type) /// array type. bool is_multidim_java_array_type(const typet &type) { - return is_java_array_type(type) && - is_java_array_type( - java_array_element_type(to_symbol_type(type.subtype()))); + return is_java_array_type(type) && is_java_array_type(java_array_element_type( + to_struct_tag_type(type.subtype()))); } /// See above @@ -417,13 +416,13 @@ build_class_name(const std::string &src, const std::string &class_name_prefix) std::string container_class = gather_full_class_name(src); std::string identifier = "java::" + container_class; - symbol_typet symbol_type(identifier); - symbol_type.set(ID_C_base_name, container_class); + struct_tag_typet struct_tag_type(identifier); + struct_tag_type.set(ID_C_base_name, container_class); std::size_t f_pos = src.find('<', 1); if(f_pos != std::string::npos) { - java_generic_typet result(symbol_type); + java_generic_typet result(struct_tag_type); // get generic type information do { @@ -441,7 +440,7 @@ build_class_name(const std::string &src, const std::string &class_name_prefix) return std::move(result); } - return java_reference_type(symbol_type); + return java_reference_type(struct_tag_type); } /// Finds the closing semi-colon ending a ClassTypeSignature that starts at @@ -611,7 +610,8 @@ typet java_type_from_string( irep_idt type_var_name(class_name_prefix+"::"+src.substr(1, src.size()-2)); return java_generic_parametert( type_var_name, - to_symbol_type(java_type_from_string("Ljava/lang/Object;").subtype())); + to_struct_tag_type( + java_type_from_string("Ljava/lang/Object;").subtype())); } case 'L': { @@ -711,7 +711,8 @@ std::vector java_generic_type_from_string( java_generic_parametert type_var_type( type_var_name, - to_symbol_type(java_type_from_string(bound_type, class_name).subtype())); + to_struct_tag_type( + java_type_from_string(bound_type, class_name).subtype())); types.push_back(type_var_type); signature=signature.substr(var_sep+1, std::string::npos); @@ -730,19 +731,19 @@ static std::string slash_to_dot(const std::string &src) return result; } -symbol_typet java_classname(const std::string &id) +struct_tag_typet java_classname(const std::string &id) { if(!id.empty() && id[0]=='[') - return to_symbol_type(java_type_from_string(id).subtype()); + return to_struct_tag_type(java_type_from_string(id).subtype()); std::string class_name=id; class_name=slash_to_dot(class_name); irep_idt identifier="java::"+class_name; - symbol_typet symbol_type(identifier); - symbol_type.set(ID_C_base_name, class_name); + struct_tag_typet struct_tag_type(identifier); + struct_tag_type.set(ID_C_base_name, class_name); - return symbol_type; + return struct_tag_type; } /// Programmatic documentation of the structure of a Java array (of either @@ -800,11 +801,11 @@ bool equal_java_types(const typet &type1, const typet &type2) bool arrays_with_same_element_type = true; if( type1.id() == ID_pointer && type2.id() == ID_pointer && - type1.subtype().id() == ID_symbol_type && - type2.subtype().id() == ID_symbol_type) + type1.subtype().id() == ID_struct_tag && + type2.subtype().id() == ID_struct_tag) { - const symbol_typet &subtype_symbol1 = to_symbol_type(type1.subtype()); - const symbol_typet &subtype_symbol2 = to_symbol_type(type2.subtype()); + const auto &subtype_symbol1 = to_struct_tag_type(type1.subtype()); + const auto &subtype_symbol2 = to_struct_tag_type(type2.subtype()); if( subtype_symbol1.get_identifier() == subtype_symbol2.get_identifier() && is_java_array_tag(subtype_symbol1.get_identifier())) @@ -847,15 +848,15 @@ void get_dependencies_from_generic_parameters_rec( get_dependencies_from_generic_parameters_rec(param.type(), refs); } - // symbol type - else if(t.id() == ID_symbol_type) + // struct tag + else if(t.id() == ID_struct_tag) { - const symbol_typet &symbol_type = to_symbol_type(t); - const irep_idt class_name(symbol_type.get_identifier()); + const auto &struct_tag_type = to_struct_tag_type(t); + const irep_idt class_name(struct_tag_type.get_identifier()); if(is_java_array_tag(class_name)) { get_dependencies_from_generic_parameters( - java_array_element_type(symbol_type), refs); + java_array_element_type(struct_tag_type), refs); } else refs.insert(strip_java_namespace_prefix(class_name)); @@ -916,25 +917,27 @@ void get_dependencies_from_generic_parameters( /// This assumes that the class named \p class_name_prefix extends or implements /// the class \p type, and that \p base_ref corresponds to a generic class. /// For instance since HashMap extends Map we would call -/// `java_generic_symbol_typet(symbol_typet("Map"), "Ljava/util/Map;", +/// `java_generic_struct_tag_typet(struct_tag_typet("Map"), "Ljava/util/Map;", /// "java.util.HashMap")` which generates a symbol type with identifier "Map", /// and two generic types with identifier "java.util.HashMap::K" and /// "java.util.HashMap::V" respectively. -java_generic_symbol_typet::java_generic_symbol_typet( - const symbol_typet &type, +java_generic_struct_tag_typet::java_generic_struct_tag_typet( + const struct_tag_typet &type, const std::string &base_ref, const std::string &class_name_prefix) - : symbol_typet(type) + : struct_tag_typet(type) { set(ID_C_java_generic_symbol, true); const typet &base_type = java_type_from_string(base_ref, class_name_prefix); PRECONDITION(is_java_generic_type(base_type)); const java_generic_typet &gen_base_type = to_java_generic_type(base_type); INVARIANT( - type.get_identifier() == to_symbol_type(gen_base_type.subtype()).get_identifier(), - "identifier of "+type.pretty()+"\n and identifier of type "+ - gen_base_type.subtype().pretty()+"\ncreated by java_type_from_string for "+ - base_ref+" should be equal"); + type.get_identifier() == + to_struct_tag_type(gen_base_type.subtype()).get_identifier(), + "identifier of " + type.pretty() + "\n and identifier of type " + + gen_base_type.subtype().pretty() + + "\ncreated by java_type_from_string for " + base_ref + + " should be equal"); generic_types().insert( generic_types().end(), gen_base_type.generic_type_arguments().begin(), @@ -945,7 +948,7 @@ java_generic_symbol_typet::java_generic_symbol_typet( /// in the vector of generic types. /// \param type The parameter type we are looking for. /// \return The index of the type in the vector of generic types. -optionalt java_generic_symbol_typet::generic_type_index( +optionalt java_generic_struct_tag_typet::generic_type_index( const java_generic_parametert &type) const { const auto &type_variable = type.get_name(); @@ -984,12 +987,13 @@ std::string pretty_java_type(const typet &type) return "byte"; else if(is_reference(type)) { - if(type.subtype().id() == ID_symbol_type) + if(type.subtype().id() == ID_struct_tag) { - const auto &symbol_type = to_symbol_type(type.subtype()); - const irep_idt &id = symbol_type.get_identifier(); + const auto &struct_tag_type = to_struct_tag_type(type.subtype()); + const irep_idt &id = struct_tag_type.get_identifier(); if(is_java_array_tag(id)) - return pretty_java_type(java_array_element_type(symbol_type)) + "[]"; + return pretty_java_type(java_array_element_type(struct_tag_type)) + + "[]"; else return id2string(strip_java_namespace_prefix(id)); } diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 3ce63a5ad42..0fa28f8cdf1 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -358,11 +358,11 @@ typet java_boolean_type(); typet java_void_type(); reference_typet java_reference_type(const typet &subtype); reference_typet java_lang_object_type(); -symbol_typet java_classname(const std::string &); +struct_tag_typet java_classname(const std::string &); reference_typet java_array_type(const char subtype); -const typet &java_array_element_type(const symbol_typet &array_symbol); -typet &java_array_element_type(symbol_typet &array_symbol); +const typet &java_array_element_type(const struct_tag_typet &array_symbol); +typet &java_array_element_type(struct_tag_typet &array_symbol); bool is_java_array_type(const typet &type); bool is_multidim_java_array_type(const typet &type); @@ -397,15 +397,15 @@ bool equal_java_types(const typet &type1, const typet &type2); class java_generic_parametert:public reference_typet { public: - typedef symbol_typet type_variablet; + typedef struct_tag_typet type_variablet; java_generic_parametert( const irep_idt &_type_var_name, - const symbol_typet &_bound): - reference_typet(java_reference_type(_bound)) + const struct_tag_typet &_bound) + : reference_typet(java_reference_type(_bound)) { set(ID_C_java_generic_parameter, true); - type_variables().push_back(symbol_typet(_type_var_name)); + type_variables().push_back(struct_tag_typet(_type_var_name)); } /// \return the type variable as symbol type @@ -748,16 +748,16 @@ void get_dependencies_from_generic_parameters( const typet &, std::set &); -/// Type for a generic symbol, extends symbol_typet with a +/// Type for a generic symbol, extends struct_tag_typet with a /// vector of java generic types. /// This is used to store the type of generic superclasses and interfaces. -class java_generic_symbol_typet : public symbol_typet +class java_generic_struct_tag_typet : public struct_tag_typet { public: typedef std::vector generic_typest; - java_generic_symbol_typet( - const symbol_typet &type, + java_generic_struct_tag_typet( + const struct_tag_typet &type, const std::string &base_ref, const std::string &class_name_prefix); @@ -777,26 +777,27 @@ class java_generic_symbol_typet : public symbol_typet /// \param type: the type to check /// \return true if the type is a symbol type with generics -inline bool is_java_generic_symbol_type(const typet &type) +inline bool is_java_generic_struct_tag_type(const typet &type) { return type.get_bool(ID_C_java_generic_symbol); } /// \param type: the type to convert /// \return the converted type -inline const java_generic_symbol_typet & -to_java_generic_symbol_type(const typet &type) +inline const java_generic_struct_tag_typet & +to_java_generic_struct_tag_type(const typet &type) { - PRECONDITION(is_java_generic_symbol_type(type)); - return static_cast(type); + PRECONDITION(is_java_generic_struct_tag_type(type)); + return static_cast(type); } /// \param type: the type to convert /// \return the converted type -inline java_generic_symbol_typet &to_java_generic_symbol_type(typet &type) +inline java_generic_struct_tag_typet & +to_java_generic_struct_tag_type(typet &type) { - PRECONDITION(is_java_generic_symbol_type(type)); - return static_cast(type); + PRECONDITION(is_java_generic_struct_tag_type(type)); + return static_cast(type); } /// Take a signature string and remove everything in angle brackets allowing for diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index d1a07643755..02876b34918 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -348,7 +348,7 @@ void remove_exceptionst::add_exception_dispatch_sequence( t_exc->function=instr_it->function; // use instanceof to check that this is the correct handler - symbol_typet type(stack_catch[i][j].first); + struct_tag_typet type(stack_catch[i][j].first); type_exprt expr(type); binary_predicate_exprt check(exc_thrown, ID_java_instanceof, expr); diff --git a/jbmc/src/java_bytecode/remove_instanceof.cpp b/jbmc/src/java_bytecode/remove_instanceof.cpp index 094886ce279..349d4d6fe2d 100644 --- a/jbmc/src/java_bytecode/remove_instanceof.cpp +++ b/jbmc/src/java_bytecode/remove_instanceof.cpp @@ -87,10 +87,10 @@ bool remove_instanceoft::lower_instanceof( // Find all types we know about that satisfy the given requirement: INVARIANT( - target_type.id() == ID_symbol_type, + target_type.id() == ID_struct_tag, "instanceof second operand should have a simple type"); - const irep_idt &target_name= - to_symbol_type(target_type).get_identifier(); + const irep_idt &target_name = + to_struct_tag_type(target_type).get_identifier(); std::vector children= class_hierarchy.get_children_trans(target_name); children.push_back(target_name); @@ -104,7 +104,7 @@ bool remove_instanceoft::lower_instanceof( // Make temporaries to store the class identifier (avoids repeated derefs) and // the instanceof result: - symbol_typet jlo=to_symbol_type(java_lang_object_type().subtype()); + auto jlo = to_struct_tag_type(java_lang_object_type().subtype()); exprt object_clsid = get_class_identifier_field(check_ptr, jlo, ns); symbolt &clsid_tmp_sym = get_fresh_aux_symbol( diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp index 24dedd44da4..633f703e9f3 100644 --- a/jbmc/src/java_bytecode/remove_java_new.cpp +++ b/jbmc/src/java_bytecode/remove_java_new.cpp @@ -96,7 +96,7 @@ goto_programt::targett remove_java_newt::lower_java_new( auto zero_object = zero_initializer(object_type, location, ns); CHECK_RETURN(zero_object.has_value()); set_class_identifier( - to_struct_expr(*zero_object), ns, to_symbol_type(object_type)); + to_struct_expr(*zero_object), ns, to_struct_tag_type(object_type)); goto_programt::targett t_i = dest.insert_after(target); t_i->make_assignment(code_assignt(deref, *zero_object)); t_i->source_location = location; @@ -156,7 +156,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array( auto zero_object = zero_initializer(object_type, location, ns); CHECK_RETURN(zero_object.has_value()); set_class_identifier( - to_struct_expr(*zero_object), ns, to_symbol_type(object_type)); + to_struct_expr(*zero_object), ns, to_struct_tag_type(object_type)); goto_programt::targett t_i = dest.insert_before(next); t_i->make_assignment(code_assignt(deref, *zero_object)); t_i->source_location = location; diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index 10cdbbe8449..7199ed196e8 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -82,10 +82,10 @@ pointer_typet select_pointer_typet::specialize_generics( visited_nodes.erase(parameter_name); return returned_type; } - else if(pointer_type.subtype().id() == ID_symbol_type) + else if(pointer_type.subtype().id() == ID_struct_tag) { // if the pointer is an array, recursively specialize its element type - const symbol_typet &array_subtype = to_symbol_type(pointer_type.subtype()); + const auto &array_subtype = to_struct_tag_type(pointer_type.subtype()); if(is_java_array_tag(array_subtype.get_identifier())) { const typet &array_element_type = java_array_element_type(array_subtype); @@ -208,7 +208,8 @@ select_pointer_typet::get_recursively_instantiated_type( return inst_val; } -std::set select_pointer_typet::get_parameter_alternative_types( +std::set +select_pointer_typet::get_parameter_alternative_types( const irep_idt &function_name, const irep_idt ¶meter_name, const namespacet &) const diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h index d8e508206c2..f0525c48b7c 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.h +++ b/jbmc/src/java_bytecode/select_pointer_type.h @@ -11,6 +11,8 @@ /// \file /// Handle selection of correct pointer type (for example changing abstract /// classes to concrete versions). +#include "java_types.h" + #include #include "java_types.h" @@ -56,7 +58,7 @@ class select_pointer_typet /// the function body. In the base class we just return an empty set. /// Derived classes can override this behaviour to provide more /// sophisticated alternative type identification. - virtual std::set get_parameter_alternative_types( + virtual std::set get_parameter_alternative_types( const irep_idt &function_name, const irep_idt ¶meter_name, const namespacet &ns) const; diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp index 3e948b63b72..bfac27c4155 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp +++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp @@ -340,7 +340,7 @@ const irep_idt &require_goto_statements::require_struct_component_assignment( { REQUIRE(component_assignment_rhs.type().id() == ID_pointer); REQUIRE( - to_symbol_type( + to_struct_tag_type( to_pointer_type(component_assignment_rhs.type()).subtype()) .get(ID_identifier) == typecast_name.value()); } @@ -423,7 +423,8 @@ require_goto_statements::require_struct_array_component_assignment( // Check the type we are casting to matches the array type REQUIRE(component_assignment_rhs.type().id() == ID_pointer); REQUIRE( - to_symbol_type(to_pointer_type(component_assignment_rhs.type()).subtype()) + to_struct_tag_type( + to_pointer_type(component_assignment_rhs.type()).subtype()) .get(ID_identifier) == array_type_name); // Get the tmp_object name and find assignments to it, there should be only diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 67bfa5aaf4d..24ac16ab35d 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -140,7 +140,7 @@ bool require_java_generic_type_argument_expectation( case require_type::type_argument_kindt::Inst: { REQUIRE(!is_java_generic_parameter(type_argument)); - REQUIRE(type_argument.subtype() == symbol_typet(expected.description)); + REQUIRE(type_argument.subtype() == struct_tag_typet(expected.description)); return true; } } @@ -227,7 +227,7 @@ java_generic_parametert require_type::require_java_generic_parameter( /// \return The value passed in the first argument const typet &require_type::require_java_non_generic_type( const typet &type, - const optionalt &expect_subtype) + const optionalt &expect_subtype) { REQUIRE(!is_java_generic_parameter(type)); REQUIRE(!is_java_generic_type(type)); @@ -447,11 +447,11 @@ require_type::require_complete_java_non_generic_class(const typet &class_type) /// \param type: The type to check /// \param identifier: The identifier the symbol type should have /// \return The cast version of the input type -const symbol_typet & -require_type::require_symbol(const typet &type, const irep_idt &identifier) +const struct_tag_typet & +require_type::require_struct_tag(const typet &type, const irep_idt &identifier) { - REQUIRE(type.id() == ID_symbol_type); - const symbol_typet &result = to_symbol_type(type); + REQUIRE(type.id() == ID_struct_tag); + const struct_tag_typet &result = to_struct_tag_type(type); if(identifier != "") { REQUIRE(result.get_identifier() == identifier); @@ -462,21 +462,22 @@ require_type::require_symbol(const typet &type, const irep_idt &identifier) /// Verify a given type is a java generic symbol type /// \param type: The type to check /// \param identifier: The identifier to match -/// \return The type, cast to a java_generic_symbol_typet -java_generic_symbol_typet require_type::require_java_generic_symbol_type( +/// \return The type, cast to a java_generic_struct_tag_typet +java_generic_struct_tag_typet +require_type::require_java_generic_struct_tag_type( const typet &type, const std::string &identifier) { - symbol_typet symbol_type = require_symbol(type, identifier); - REQUIRE(is_java_generic_symbol_type(type)); - return to_java_generic_symbol_type(type); + struct_tag_typet struct_tag_type = require_struct_tag(type, identifier); + REQUIRE(is_java_generic_struct_tag_type(type)); + return to_java_generic_struct_tag_type(type); } /// Verify a given type is a java generic symbol type, checking /// that it's associated type arguments match a given set of identifiers. /// Expected usage is something like this: /// -/// require_java_generic_symbol_type(type, "java::Generic", +/// require_java_generic_struct_tag_type(type, "java::Generic", /// {{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}, /// {require_type::type_argument_kindt::Var, "T"}}) /// @@ -484,14 +485,15 @@ java_generic_symbol_typet require_type::require_java_generic_symbol_type( /// \param identifier: The identifier to match /// \param type_expectations: A set of type argument kinds and identifiers /// which should be expected as the type arguments of the given generic type -/// \return The given type, cast to a java_generic_symbol_typet -java_generic_symbol_typet require_type::require_java_generic_symbol_type( +/// \return The given type, cast to a java_generic_struct_tag_typet +java_generic_struct_tag_typet +require_type::require_java_generic_struct_tag_type( const typet &type, const std::string &identifier, const require_type::expected_type_argumentst &type_expectations) { - const java_generic_symbol_typet &generic_base_type = - require_java_generic_symbol_type(type, identifier); + const java_generic_struct_tag_typet &generic_base_type = + require_java_generic_struct_tag_type(type, identifier); const java_generic_typet::generic_type_argumentst &generic_type_arguments = generic_base_type.generic_types(); diff --git a/jbmc/unit/java-testing-utils/require_type.h b/jbmc/unit/java-testing-utils/require_type.h index 168a781b863..6df0d4043d7 100644 --- a/jbmc/unit/java-testing-utils/require_type.h +++ b/jbmc/unit/java-testing-utils/require_type.h @@ -25,8 +25,8 @@ namespace require_type pointer_typet require_pointer(const typet &type, const optionalt &subtype); -const symbol_typet & -require_symbol(const typet &type, const irep_idt &identifier = ""); +const struct_tag_typet & +require_struct_tag(const typet &type, const irep_idt &identifier = ""); struct_typet::componentt require_component( const struct_typet &struct_type, @@ -71,7 +71,7 @@ java_generic_parametert require_java_generic_parameter( const typet &require_java_non_generic_type( const typet &type, - const optionalt &expect_subtype); + const optionalt &expect_subtype); class_typet require_complete_class(const typet &class_type); @@ -110,11 +110,11 @@ java_class_typet require_java_non_generic_class(const typet &class_type); java_class_typet require_complete_java_non_generic_class(const typet &class_type); -java_generic_symbol_typet require_java_generic_symbol_type( +java_generic_struct_tag_typet require_java_generic_struct_tag_type( const typet &type, const std::string &identifier); -java_generic_symbol_typet require_java_generic_symbol_type( +java_generic_struct_tag_typet require_java_generic_struct_tag_type( const typet &type, const std::string &identifier, const require_type::expected_type_argumentst &type_expectations); diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp index 907e9ca6059..7bc21581050 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp @@ -116,7 +116,7 @@ SCENARIO( const java_generic_typet &type = require_type::require_java_generic_type(component.type()); require_type::require_pointer( - type.generic_type_arguments()[0], symbol_typet{"java::BWrapper"}); + type.generic_type_arguments()[0], struct_tag_typet{"java::BWrapper"}); } THEN("Object 'this' has field 'field_input1' of type Wrapper") diff --git a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp index 6044b5596db..10d04b5f570 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp @@ -47,7 +47,7 @@ SCENARIO( // ... which is of type `KeyValue` ... const auto &subtype = gen_type.subtype(); const auto &key_value = - symbol_table.lookup_ref(to_symbol_type(subtype).get_identifier()); + symbol_table.lookup_ref(to_struct_tag_type(subtype).get_identifier()); REQUIRE(key_value.type.id() == ID_struct); REQUIRE(key_value.name == "java::KeyValue"); @@ -63,8 +63,9 @@ SCENARIO( next.type(), {{require_type::type_argument_kindt::Var, "java::KeyValue::K"}, {require_type::type_argument_kindt::Var, "java::KeyValue::V"}}); - REQUIRE(next_type.subtype().id() == ID_symbol_type); - const symbol_typet &next_symbol = to_symbol_type(next_type.subtype()); + REQUIRE(next_type.subtype().id() == ID_struct_tag); + const struct_tag_typet &next_symbol = + to_struct_tag_type(next_type.subtype()); REQUIRE( symbol_table.lookup_ref(next_symbol.get_identifier()).name == "java::KeyValue"); @@ -75,8 +76,9 @@ SCENARIO( reverse.type(), {{require_type::type_argument_kindt::Var, "java::KeyValue::V"}, {require_type::type_argument_kindt::Var, "java::KeyValue::K"}}); - REQUIRE(next_type.subtype().id() == ID_symbol_type); - const symbol_typet &reverse_symbol = to_symbol_type(reverse_type.subtype()); + REQUIRE(next_type.subtype().id() == ID_struct_tag); + const struct_tag_typet &reverse_symbol = + to_struct_tag_type(reverse_type.subtype()); REQUIRE( symbol_table.lookup_ref(next_symbol.get_identifier()).name == "java::KeyValue"); diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp index 59fe8de9e23..1a8db33cf34 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp @@ -31,10 +31,10 @@ SCENARIO("java_bytecode_convert_abstract_class", THEN("The symbol type should be abstract") { const symbolt &class_symbol=*new_symbol_table.lookup("java::I"); - const typet &symbol_type=class_symbol.type; + const typet &struct_tag_type = class_symbol.type; - REQUIRE(symbol_type.id()==ID_struct); - class_typet class_type=to_class_type(symbol_type); + REQUIRE(struct_tag_type.id() == ID_struct); + class_typet class_type = to_class_type(struct_tag_type); REQUIRE(class_type.is_class()); REQUIRE(class_type.is_abstract()); } @@ -46,10 +46,10 @@ SCENARIO("java_bytecode_convert_abstract_class", THEN("The symbol type should be abstract") { const symbolt &class_symbol=*new_symbol_table.lookup("java::A"); - const typet &symbol_type=class_symbol.type; + const typet &struct_tag_type = class_symbol.type; - REQUIRE(symbol_type.id()==ID_struct); - class_typet class_type=to_class_type(symbol_type); + REQUIRE(struct_tag_type.id() == ID_struct); + class_typet class_type = to_class_type(struct_tag_type); REQUIRE(class_type.is_class()); REQUIRE(class_type.is_abstract()); } @@ -61,10 +61,10 @@ SCENARIO("java_bytecode_convert_abstract_class", THEN("The symbol type should not be abstract") { const symbolt &class_symbol=*new_symbol_table.lookup("java::C"); - const typet &symbol_type=class_symbol.type; + const typet &struct_tag_type = class_symbol.type; - REQUIRE(symbol_type.id()==ID_struct); - class_typet class_type=to_class_type(symbol_type); + REQUIRE(struct_tag_type.id() == ID_struct); + class_typet class_type = to_class_type(struct_tag_type); REQUIRE(class_type.is_class()); REQUIRE_FALSE(class_type.is_abstract()); } @@ -79,10 +79,10 @@ SCENARIO("java_bytecode_convert_abstract_class", { const symbolt &class_symbol= *new_symbol_table.lookup("java::Implementor"); - const typet &symbol_type=class_symbol.type; + const typet &struct_tag_type = class_symbol.type; - REQUIRE(symbol_type.id()==ID_struct); - class_typet class_type=to_class_type(symbol_type); + REQUIRE(struct_tag_type.id() == ID_struct); + class_typet class_type = to_class_type(struct_tag_type); REQUIRE(class_type.is_class()); REQUIRE_FALSE(class_type.is_abstract()); } @@ -97,10 +97,10 @@ SCENARIO("java_bytecode_convert_abstract_class", { const symbolt &class_symbol= *new_symbol_table.lookup("java::Extender"); - const typet &symbol_type=class_symbol.type; + const typet &struct_tag_type = class_symbol.type; - REQUIRE(symbol_type.id()==ID_struct); - class_typet class_type=to_class_type(symbol_type); + REQUIRE(struct_tag_type.id() == ID_struct); + class_typet class_type = to_class_type(struct_tag_type); REQUIRE(class_type.is_class()); REQUIRE_FALSE(class_type.is_abstract()); } diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp index 6ecbe704bf2..ba5193b0e4d 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp @@ -35,7 +35,7 @@ SCENARIO( REQUIRE(annotations.size() == 1); const auto &annotation = annotations.front(); const auto &identifier = - to_symbol_type(annotation.type.subtype()).get_identifier(); + to_struct_tag_type(annotation.type.subtype()).get_identifier(); REQUIRE(id2string(identifier) == "java::MyClassAnnotation"); const auto &element_value_pair = annotation.element_value_pairs.front(); const auto &element_name = element_value_pair.element_name; @@ -62,7 +62,7 @@ SCENARIO( REQUIRE(annotations.size() == 1); const auto &annotation = annotations.front(); const auto &identifier = - to_symbol_type(annotation.type.subtype()).get_identifier(); + to_struct_tag_type(annotation.type.subtype()).get_identifier(); REQUIRE(id2string(identifier) == "java::MyMethodAnnotation"); const auto &element_value_pair = annotation.element_value_pairs.front(); const auto &element_name = element_value_pair.element_name; diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp index 3a5d42918d0..bca5d1f760e 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp @@ -72,8 +72,8 @@ void validate_lambda_assignment( const pointer_typet &lambda_temp_type = require_type::require_pointer(side_effect_expr.type(), {}); - const symbol_typet &lambda_implementor_type = - require_type::require_symbol(lambda_temp_type.subtype()); + const struct_tag_typet &lambda_implementor_type = + require_type::require_struct_tag(lambda_temp_type.subtype()); const irep_idt &tmp_class_identifier = lambda_implementor_type.get_identifier(); @@ -110,7 +110,7 @@ void validate_lambda_assignment( const java_class_typet::componentt super_class_component = require_type::require_component(tmp_lambda_class_type, "@java.lang.Object"); - const symbol_typet &super_class_type = require_type::require_symbol( + const struct_tag_typet &super_class_type = require_type::require_struct_tag( super_class_component.type(), "java::java.lang.Object"); THEN("The function in the class should call the lambda 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 c3718d0cabb..19fac0e8b1c 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 @@ -96,7 +96,7 @@ SCENARIO( require_type::require_component( to_struct_type(class_symbol.type), "belem"); require_type::require_pointer( - belem_type.type(), symbol_typet(class_prefix + "$BoundedInner")); + belem_type.type(), struct_tag_typet(class_prefix + "$BoundedInner")); require_type::require_java_generic_type( belem_type.type(), {{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}}); diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp index 4322a741845..46e3377f1a6 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp @@ -31,7 +31,7 @@ SCENARIO( { REQUIRE(derived_class_type.bases().size() == 1); const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::Generic", {{require_type::type_argument_kindt::Inst, @@ -54,7 +54,7 @@ SCENARIO( { REQUIRE(derived_class_type.bases().size() == 1); const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::GenericTwoParam", {{require_type::type_argument_kindt::Inst, @@ -77,7 +77,7 @@ SCENARIO( { REQUIRE(derived_class_type.bases().size() == 1); const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::Generic", {{require_type::type_argument_kindt::Var, @@ -99,7 +99,7 @@ SCENARIO( { REQUIRE(derived_class_type.bases().size() == 1); const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::Generic", {{require_type::type_argument_kindt::Inst, @@ -121,7 +121,7 @@ SCENARIO( { REQUIRE(derived_class_type.bases().size() == 1); const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::GenericTwoParam", {{require_type::type_argument_kindt::Var, @@ -145,7 +145,7 @@ SCENARIO( { REQUIRE(derived_class_type.bases().size() == 1); const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::Generic", {{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}}); @@ -168,7 +168,7 @@ SCENARIO( { REQUIRE(derived_class_type.bases().size() == 1); const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::Generic", {{require_type::type_argument_kindt::Var, @@ -193,7 +193,7 @@ SCENARIO( { REQUIRE(derived_class_type.bases().size() == 1); const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::Generic", {{require_type::type_argument_kindt::Var, @@ -216,7 +216,7 @@ SCENARIO( { REQUIRE(derived_class_type.bases().size() == 1); const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::DerivedGenericMixed2", {{require_type::type_argument_kindt::Inst, "java::java.lang.String"}}); @@ -243,12 +243,12 @@ SCENARIO( THEN("The superclass is correct") { const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_symbol(base_type, "java::java.lang.Object"); + require_type::require_struct_tag(base_type, "java::java.lang.Object"); } THEN("The second interface is correct") { const typet &base_type = derived_class_type.bases().at(1).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::InterfaceGeneric", {{require_type::type_argument_kindt::Inst, @@ -275,12 +275,12 @@ SCENARIO( THEN("The superclass is correct") { const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_symbol(base_type, "java::java.lang.Object"); + require_type::require_struct_tag(base_type, "java::java.lang.Object"); } THEN("The second interface is correct") { const typet &base_type = derived_class_type.bases().at(1).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::InterfaceGeneric", {{require_type::type_argument_kindt::Var, @@ -309,12 +309,12 @@ SCENARIO( THEN("The superclass is correct") { const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_symbol(base_type, "java::java.lang.Object"); + require_type::require_struct_tag(base_type, "java::java.lang.Object"); } THEN("The second interface is correct") { const typet &base_type = derived_class_type.bases().at(1).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::InterfaceGeneric", {{require_type::type_argument_kindt::Inst, @@ -323,7 +323,7 @@ SCENARIO( THEN("The first interface is correct") { const typet &base_type = derived_class_type.bases().at(2).type(); - require_type::require_symbol(base_type, "java::Interface"); + require_type::require_struct_tag(base_type, "java::Interface"); } } } @@ -348,7 +348,7 @@ SCENARIO( THEN("The superclass is correct") { const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::Generic", {{require_type::type_argument_kindt::Inst, @@ -357,12 +357,12 @@ SCENARIO( THEN("The first interface is correct") { const typet &base_type = derived_class_type.bases().at(1).type(); - require_type::require_symbol(base_type, "java::Interface"); + require_type::require_struct_tag(base_type, "java::Interface"); } THEN("The second interface is correct") { const typet &base_type = derived_class_type.bases().at(2).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::InterfaceGeneric", {{require_type::type_argument_kindt::Inst, @@ -390,7 +390,7 @@ SCENARIO( THEN("The superclass is correct") { const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::GenericTwoParam", {{require_type::type_argument_kindt::Var, @@ -401,12 +401,12 @@ SCENARIO( THEN("The first interface is correct") { const typet &base_type = derived_class_type.bases().at(1).type(); - require_type::require_symbol(base_type, "java::Interface"); + require_type::require_struct_tag(base_type, "java::Interface"); } THEN("The second interface is correct") { const typet &base_type = derived_class_type.bases().at(2).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::InterfaceGeneric", {{require_type::type_argument_kindt::Var, @@ -435,20 +435,20 @@ SCENARIO( THEN("The superclass is correct") { const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::Generic", {{require_type::type_argument_kindt::Inst, - "java::InterfaceGeneric"}}); + "java::InterfaceGeneric"}}); } THEN("The interface is correct") { const typet &base_type = derived_class_type.bases().at(1).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::InterfaceGeneric", {{require_type::type_argument_kindt::Inst, - "java::java.lang.Integer"}}); + "java::java.lang.Integer"}}); } } } @@ -473,12 +473,12 @@ SCENARIO( THEN("The superclass is correct") { const typet &base_type = derived_class_type.bases().at(0).type(); - const java_generic_symbol_typet &superclass_type = - require_type::require_java_generic_symbol_type( + const java_generic_struct_tag_typet &superclass_type = + require_type::require_java_generic_struct_tag_type( base_type, "java::Generic", {{require_type::type_argument_kindt::Inst, - "java::InterfaceGeneric"}}); + "java::InterfaceGeneric"}}); const typet &type_argument = superclass_type.generic_types().at(0); require_type::require_java_generic_type( @@ -489,11 +489,11 @@ SCENARIO( THEN("The interface is correct") { const typet &base_type = derived_class_type.bases().at(1).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::InterfaceGeneric", {{require_type::type_argument_kindt::Inst, - "java::java.lang.Integer"}}); + "java::java.lang.Integer"}}); } } } @@ -517,20 +517,20 @@ SCENARIO( THEN("The superclass is correct") { const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::Generic", {{require_type::type_argument_kindt::Inst, - "java::InterfaceGeneric"}}); + "java::InterfaceGeneric"}}); } THEN("The interface is correct") { const typet &base_type = derived_class_type.bases().at(1).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::InterfaceGeneric", {{require_type::type_argument_kindt::Var, - "java::ExtendsAndImplementsSameInterfaceGeneric::T"}}); + "java::ExtendsAndImplementsSameInterfaceGeneric::T"}}); } } } @@ -549,7 +549,7 @@ SCENARIO( { REQUIRE(derived_class_type.bases().size() == 1); const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::GenericBase$ImplicitGeneric", {{require_type::type_argument_kindt::Var, "java::GenericBase::T"}}); @@ -570,7 +570,7 @@ SCENARIO( { REQUIRE(derived_class_type.bases().size() == 1); const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::GenericBase$ImplicitAndExplicitGeneric", {{require_type::type_argument_kindt::Var, "java::GenericBase::T"}, @@ -593,7 +593,7 @@ SCENARIO( { REQUIRE(derived_class_type.bases().size() == 1); const typet &base_type = derived_class_type.bases().at(0).type(); - require_type::require_java_generic_symbol_type( + require_type::require_java_generic_struct_tag_type( base_type, "java::GenericBase2$ImplicitAndExplicitGeneric", {{require_type::type_argument_kindt::Var, "java::GenericBase2::T"}, 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 adf4c715165..c4eb67ad785 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 @@ -40,7 +40,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::Generic")); THEN("x is generic with parameter pointing to java.lang.Integer") { @@ -55,7 +55,7 @@ SCENARIO( { const typet return_type = func_code.return_type(); require_type::require_pointer( - return_type, symbol_typet("java::Generic")); + return_type, struct_tag_typet("java::Generic")); THEN("It is generic with parameter pointing to java.lang.Integer") { @@ -89,7 +89,7 @@ SCENARIO( 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")); + param_s.type(), struct_tag_typet("java::Generic")); THEN("s is generic with parameter pointing to java.lang.String") { @@ -104,7 +104,7 @@ SCENARIO( { const typet return_type = func_code.return_type(); require_type::require_pointer( - return_type, symbol_typet("java::Generic")); + return_type, struct_tag_typet("java::Generic")); THEN("It is generic with parameter pointing to java.lang.Integer") { @@ -138,7 +138,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::Generic")); THEN("x is generic with parameter pointing to java.lang.Integer") { @@ -154,7 +154,7 @@ SCENARIO( 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")); + param_y.type(), struct_tag_typet("java::Generic")); THEN("y is generic with parameter pointing to java.lang.Integer") { @@ -169,7 +169,7 @@ SCENARIO( { const typet return_type = func_code.return_type(); require_type::require_pointer( - return_type, symbol_typet("java::Generic")); + return_type, struct_tag_typet("java::Generic")); THEN("It is generic with parameter pointing to java.lang.Integer") { @@ -203,7 +203,7 @@ SCENARIO( 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")); + param_s.type(), struct_tag_typet("java::Generic")); THEN("s is generic with parameter pointing to java.lang.String") { @@ -219,7 +219,7 @@ SCENARIO( 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")); + param_b.type(), struct_tag_typet("java::Generic")); THEN("b is generic with parameter pointing to java.lang.Boolean") { @@ -234,7 +234,7 @@ SCENARIO( { const typet return_type = func_code.return_type(); require_type::require_pointer( - return_type, symbol_typet("java::Generic")); + return_type, struct_tag_typet("java::Generic")); THEN("It is generic with parameter pointing to java.lang.Integer") { @@ -269,14 +269,14 @@ SCENARIO( 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")); + param_inner.type(), struct_tag_typet(class_prefix + "$Inner")); } THEN("It has return type pointing to Generic") { const typet return_type = func_code.return_type(); require_type::require_pointer( - return_type, symbol_typet("java::Generic")); + return_type, struct_tag_typet("java::Generic")); THEN("It is generic with parameter pointing to java.lang.Integer") { diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp index fec2749f2e5..8fa1a7557f9 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp @@ -33,10 +33,10 @@ SCENARIO( THEN("It is an array") { const pointer_typet &field_t_pointer = require_type::require_pointer( - field_t.type(), symbol_typet("java::array[reference]")); + field_t.type(), struct_tag_typet("java::array[reference]")); - const symbol_typet &field_t_subtype = - to_symbol_type(field_t_pointer.subtype()); + const struct_tag_typet &field_t_subtype = + to_struct_tag_type(field_t_pointer.subtype()); const struct_typet &subtype_type = to_struct_type( new_symbol_table.lookup_ref(field_t_subtype.get_identifier()).type); REQUIRE(is_valid_java_array(subtype_type)); @@ -58,10 +58,10 @@ SCENARIO( THEN("It is an array") { const pointer_typet &field_t2_pointer = require_type::require_pointer( - field_t2.type(), symbol_typet("java::array[reference]")); + field_t2.type(), struct_tag_typet("java::array[reference]")); - const symbol_typet &field_t2_subtype = - to_symbol_type(field_t2_pointer.subtype()); + const struct_tag_typet &field_t2_subtype = + to_struct_tag_type(field_t2_pointer.subtype()); const struct_typet &subtype_struct = to_struct_type( new_symbol_table.lookup_ref(field_t2_subtype.get_identifier()).type); REQUIRE(is_valid_java_array(subtype_struct)); @@ -69,7 +69,8 @@ SCENARIO( THEN("The elements have type Generic") { const typet &element = java_array_element_type(field_t2_subtype); - require_type::require_pointer(element, symbol_typet("java::Generic")); + require_type::require_pointer( + element, struct_tag_typet("java::Generic")); require_type::require_java_generic_type( element, {{require_type::type_argument_kindt::Var, class_prefix + "::T"}}); @@ -85,10 +86,10 @@ SCENARIO( THEN("It is an array") { const pointer_typet &field_t3_pointer = require_type::require_pointer( - field_t3.type(), symbol_typet("java::array[reference]")); + field_t3.type(), struct_tag_typet("java::array[reference]")); - const symbol_typet &field_t3_subtype = - to_symbol_type(field_t3_pointer.subtype()); + const struct_tag_typet &field_t3_subtype = + to_struct_tag_type(field_t3_pointer.subtype()); const struct_typet &subtype_struct = to_struct_type( new_symbol_table.lookup_ref(field_t3_subtype.get_identifier()).type); REQUIRE(is_valid_java_array(subtype_struct)); @@ -96,7 +97,8 @@ SCENARIO( THEN("The elements have type Generic") { const typet &element = java_array_element_type(field_t3_subtype); - require_type::require_pointer(element, symbol_typet("java::Generic")); + require_type::require_pointer( + element, struct_tag_typet("java::Generic")); require_type::require_java_generic_type( element, {{require_type::type_argument_kindt::Inst, diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp index 9587507ebec..cb4c896879b 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp @@ -48,7 +48,7 @@ SCENARIO( const struct_union_typet::componentt &field_g = require_type::require_component(class_struct, "g"); require_type::require_pointer( - field_g.type(), symbol_typet("java::Generic")); + field_g.type(), struct_tag_typet("java::Generic")); THEN("It is generic with parameter pointing to java.lang.Integer") { 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 ca763c5e463..9edf5f90257 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 @@ -37,7 +37,7 @@ SCENARIO( require_type::require_component(java_generic_class, "field"); require_type::require_pointer( - field_component.type(), symbol_typet(class_prefix + "$InnerClass")); + field_component.type(), struct_tag_typet(class_prefix + "$InnerClass")); THEN("The pointer should be generic") { @@ -56,7 +56,7 @@ SCENARIO( require_type::require_pointer( field_component.type(), - symbol_typet(class_prefix + "$GenericInnerClass")); + struct_tag_typet(class_prefix + "$GenericInnerClass")); THEN("The pointer should be generic") { @@ -78,7 +78,7 @@ SCENARIO( require_type::require_pointer( field_component.type(), - symbol_typet(class_prefix + "$GenericInnerClass")); + struct_tag_typet(class_prefix + "$GenericInnerClass")); THEN("The pointer should be generic") { @@ -98,7 +98,7 @@ SCENARIO( require_type::require_pointer( field_component.type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerClass")); THEN("The pointer should be generic") @@ -121,7 +121,7 @@ SCENARIO( require_type::require_pointer( field_component.type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerClass")); THEN("The pointer should be generic") @@ -142,7 +142,7 @@ SCENARIO( require_type::require_pointer( field_component.type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass")); THEN("The pointer should be generic") @@ -167,7 +167,7 @@ SCENARIO( require_type::require_pointer( field_component.type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass")); THEN("The pointer should be generic") @@ -189,7 +189,7 @@ SCENARIO( require_type::require_pointer( field_component.type(), - symbol_typet(class_prefix + "$TwoParamInnerClass")); + struct_tag_typet(class_prefix + "$TwoParamInnerClass")); THEN("The pointer should be generic") { @@ -213,7 +213,7 @@ SCENARIO( require_type::require_pointer( field_component.type(), - symbol_typet(class_prefix + "$TwoParamInnerClass")); + struct_tag_typet(class_prefix + "$TwoParamInnerClass")); THEN("The pointer should be generic") { @@ -237,7 +237,7 @@ SCENARIO( require_type::require_pointer( field_component.type(), - symbol_typet(class_prefix + "$TwoParamInnerClass")); + struct_tag_typet(class_prefix + "$TwoParamInnerClass")); THEN("The pointer should be generic") { @@ -263,7 +263,7 @@ SCENARIO( require_type::require_pointer( field_component.type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass")); THEN("The pointer should be GenericClassWithGenericInnerClasses") @@ -324,7 +324,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet(class_prefix + "$InnerClass")); + param_type.type(), struct_tag_typet(class_prefix + "$InnerClass")); require_type::require_java_generic_type( param_type.type(), {{require_type::type_argument_kindt::Var, class_prefix + "::T"}}); @@ -353,7 +353,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet(class_prefix + "$InnerClass")); + param_type.type(), struct_tag_typet(class_prefix + "$InnerClass")); require_type::require_java_generic_type( param_type.type(), {{require_type::type_argument_kindt::Var, class_prefix + "::T"}}); @@ -361,7 +361,7 @@ SCENARIO( const auto ¶m_type2 = require_type::require_parameter(function_call, "input2"); require_type::require_pointer( - param_type2.type(), symbol_typet(class_prefix + "$InnerClass")); + param_type2.type(), struct_tag_typet(class_prefix + "$InnerClass")); require_type::require_java_generic_type( param_type2.type(), {{require_type::type_argument_kindt::Var, class_prefix + "::T"}}); @@ -389,7 +389,8 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet(class_prefix + "$GenericInnerClass")); + param_type.type(), + struct_tag_typet(class_prefix + "$GenericInnerClass")); require_type::require_java_generic_type( param_type.type(), {{require_type::type_argument_kindt::Var, @@ -420,7 +421,8 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet(class_prefix + "$GenericInnerClass")); + param_type.type(), + struct_tag_typet(class_prefix + "$GenericInnerClass")); require_type::require_java_generic_type( param_type.type(), {{require_type::type_argument_kindt::Var, class_prefix + "::T"}, @@ -451,7 +453,7 @@ SCENARIO( require_type::require_parameter(function_call, "input"); require_type::require_pointer( param_type.type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerClass")); require_type::require_java_generic_type( param_type.type(), @@ -485,7 +487,7 @@ SCENARIO( require_type::require_parameter(function_call, "input"); require_type::require_pointer( param_type.type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerClass")); require_type::require_java_generic_type( param_type.type(), @@ -517,7 +519,7 @@ SCENARIO( require_type::require_parameter(function_call, "input"); require_type::require_pointer( param_type.type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass")); require_type::require_java_generic_type( param_type.type(), @@ -553,7 +555,7 @@ SCENARIO( require_type::require_parameter(function_call, "input"); require_type::require_pointer( param_type.type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass")); require_type::require_java_generic_type( param_type.type(), @@ -584,7 +586,8 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet(class_prefix + "$TwoParamInnerClass")); + param_type.type(), + struct_tag_typet(class_prefix + "$TwoParamInnerClass")); require_type::require_java_generic_type( param_type.type(), {{require_type::type_argument_kindt::Var, @@ -617,7 +620,8 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet(class_prefix + "$TwoParamInnerClass")); + param_type.type(), + struct_tag_typet(class_prefix + "$TwoParamInnerClass")); require_type::require_java_generic_type( param_type.type(), {{require_type::type_argument_kindt::Var, @@ -650,7 +654,8 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet(class_prefix + "$TwoParamInnerClass")); + param_type.type(), + struct_tag_typet(class_prefix + "$TwoParamInnerClass")); require_type::require_java_generic_type( param_type.type(), {{require_type::type_argument_kindt::Var, class_prefix + "::T"}, @@ -679,7 +684,7 @@ SCENARIO( { require_type::require_pointer( function_call.return_type(), - symbol_typet(class_prefix + "$InnerClass")); + struct_tag_typet(class_prefix + "$InnerClass")); require_type::require_java_generic_type( function_call.return_type(), {{require_type::type_argument_kindt::Var, class_prefix + "::T"}}); @@ -706,7 +711,7 @@ SCENARIO( { require_type::require_pointer( function_call.return_type(), - symbol_typet(class_prefix + "$GenericInnerClass")); + struct_tag_typet(class_prefix + "$GenericInnerClass")); require_type::require_java_generic_type( function_call.return_type(), {{require_type::type_argument_kindt::Var, @@ -736,7 +741,7 @@ SCENARIO( { require_type::require_pointer( function_call.return_type(), - symbol_typet(class_prefix + "$GenericInnerClass")); + struct_tag_typet(class_prefix + "$GenericInnerClass")); require_type::require_java_generic_type( function_call.return_type(), {{require_type::type_argument_kindt::Var, class_prefix + "::T"}, @@ -765,7 +770,7 @@ SCENARIO( { require_type::require_pointer( function_call.return_type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerClass")); require_type::require_java_generic_type( function_call.return_type(), @@ -797,7 +802,7 @@ SCENARIO( { require_type::require_pointer( function_call.return_type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerClass")); require_type::require_java_generic_type( function_call.return_type(), @@ -827,7 +832,7 @@ SCENARIO( { require_type::require_pointer( function_call.return_type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass")); require_type::require_java_generic_type( function_call.return_type(), @@ -861,7 +866,7 @@ SCENARIO( { require_type::require_pointer( function_call.return_type(), - symbol_typet( + struct_tag_typet( class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass")); require_type::require_java_generic_type( function_call.return_type(), @@ -892,7 +897,7 @@ SCENARIO( { require_type::require_pointer( function_call.return_type(), - symbol_typet(class_prefix + "$TwoParamInnerClass")); + struct_tag_typet(class_prefix + "$TwoParamInnerClass")); require_type::require_java_generic_type( function_call.return_type(), {{require_type::type_argument_kindt::Var, @@ -924,7 +929,7 @@ SCENARIO( { require_type::require_pointer( function_call.return_type(), - symbol_typet(class_prefix + "$TwoParamInnerClass")); + struct_tag_typet(class_prefix + "$TwoParamInnerClass")); require_type::require_java_generic_type( function_call.return_type(), {{require_type::type_argument_kindt::Var, @@ -956,7 +961,7 @@ SCENARIO( { require_type::require_pointer( function_call.return_type(), - symbol_typet(class_prefix + "$TwoParamInnerClass")); + struct_tag_typet(class_prefix + "$TwoParamInnerClass")); require_type::require_java_generic_type( function_call.return_type(), {{require_type::type_argument_kindt::Var, class_prefix + "::T"}, diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp index 1c213fe788c..b2e73985df9 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp @@ -32,7 +32,7 @@ SCENARIO( { const auto &field = require_type::require_component(generic_class, "f1"); require_type::require_pointer( - field.type(), symbol_typet(outer_class_prefix + "$Inner")); + field.type(), struct_tag_typet(outer_class_prefix + "$Inner")); require_type::require_java_generic_type( field.type(), {{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"}}); @@ -41,7 +41,8 @@ SCENARIO( { const auto &field = require_type::require_component(generic_class, "f2"); require_type::require_pointer( - field.type(), symbol_typet(outer_class_prefix + "$Inner$InnerInner")); + field.type(), + struct_tag_typet(outer_class_prefix + "$Inner$InnerInner")); require_type::require_java_generic_type( field.type(), {{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"}}); @@ -50,7 +51,7 @@ SCENARIO( { const auto &field = require_type::require_component(generic_class, "f3"); require_type::require_pointer( - field.type(), symbol_typet(outer_class_prefix + "$GenericInner")); + field.type(), struct_tag_typet(outer_class_prefix + "$GenericInner")); require_type::require_java_generic_type( field.type(), {{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"}, @@ -85,7 +86,7 @@ SCENARIO( { const auto &field = require_type::require_component(java_class, "t2"); require_type::require_pointer( - field.type(), symbol_typet("java::Generic")); + field.type(), struct_tag_typet("java::Generic")); require_type::require_java_generic_type( field.type(), {{require_type::type_argument_kindt::Var, @@ -122,7 +123,7 @@ SCENARIO( { const auto &field = require_type::require_component(java_class, "tt2"); require_type::require_pointer( - field.type(), symbol_typet("java::Generic")); + field.type(), struct_tag_typet("java::Generic")); const java_generic_typet &generic_field = require_type::require_java_generic_type( field.type(), @@ -171,7 +172,7 @@ SCENARIO( const auto &field = require_type::require_component(generic_class, "gt2"); require_type::require_pointer( - field.type(), symbol_typet("java::GenericTwoParam")); + field.type(), struct_tag_typet("java::GenericTwoParam")); require_type::require_java_generic_type( field.type(), {{require_type::type_argument_kindt::Var, diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp index 817ebb40a07..88423dcaba8 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp @@ -45,7 +45,7 @@ SCENARIO( const struct_typet::componentt &field = require_type::require_component(class_struct, "f2"); require_type::require_pointer( - field.type(), symbol_typet("java::Generic")); + field.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { require_type::require_java_generic_type( @@ -59,7 +59,7 @@ SCENARIO( const struct_typet::componentt &field = require_type::require_component(class_struct, "f3"); require_type::require_pointer( - field.type(), symbol_typet("java::Generic")); + field.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { require_type::require_java_generic_type( @@ -74,7 +74,7 @@ SCENARIO( const struct_typet::componentt &field = require_type::require_component(class_struct, "f4"); require_type::require_pointer( - field.type(), symbol_typet("java::Generic")); + field.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { const java_generic_typet &generic_field = @@ -95,7 +95,7 @@ SCENARIO( const struct_typet::componentt &field = require_type::require_component(class_struct, "f5"); require_type::require_pointer( - field.type(), symbol_typet("java::Generic")); + field.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { const java_generic_typet &generic_field = @@ -124,7 +124,7 @@ SCENARIO( const struct_typet::componentt &field = require_type::require_component(class_struct, "f6"); require_type::require_pointer( - field.type(), symbol_typet("java::GenericTwoParam")); + field.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { require_type::require_java_generic_type( @@ -139,7 +139,7 @@ SCENARIO( const struct_typet::componentt &field = require_type::require_component(class_struct, "f7"); require_type::require_pointer( - field.type(), symbol_typet("java::GenericTwoParam")); + field.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { require_type::require_java_generic_type( @@ -154,7 +154,7 @@ SCENARIO( const struct_typet::componentt &field = require_type::require_component(class_struct, "f8"); require_type::require_pointer( - field.type(), symbol_typet("java::GenericTwoParam")); + field.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { require_type::require_java_generic_type( @@ -171,7 +171,7 @@ SCENARIO( const struct_typet::componentt &field = require_type::require_component(class_struct, "f9"); require_type::require_pointer( - field.type(), symbol_typet("java::GenericTwoParam")); + field.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { require_type::require_java_generic_type( @@ -188,7 +188,7 @@ SCENARIO( const struct_typet::componentt &field = require_type::require_component(class_struct, "f10"); require_type::require_pointer( - field.type(), symbol_typet("java::GenericTwoParam")); + field.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { require_type::require_java_generic_type( @@ -205,7 +205,7 @@ SCENARIO( const struct_typet::componentt &field = require_type::require_component(class_struct, "f11"); require_type::require_pointer( - field.type(), symbol_typet("java::GenericTwoParam")); + field.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { const java_generic_typet &generic_field = 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 b7dbdcdb1b0..c6a844bdafd 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 @@ -39,7 +39,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -66,7 +66,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -93,7 +93,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -120,7 +120,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::java.lang.Number")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -147,7 +147,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -174,7 +174,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -202,7 +202,7 @@ SCENARIO( 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")); + param_t.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -212,7 +212,7 @@ SCENARIO( 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")); + param_u.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -240,7 +240,7 @@ SCENARIO( 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")); + param_t.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -250,7 +250,7 @@ SCENARIO( 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")); + param_u.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -276,7 +276,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -302,7 +302,7 @@ SCENARIO( THEN("It has return type pointing to java.lang.Object") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::java.lang.Object")); + func_code.return_type(), struct_tag_typet("java::java.lang.Object")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -326,7 +326,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -351,7 +351,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -376,7 +376,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -401,7 +401,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -430,7 +430,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -439,7 +439,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -467,7 +467,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -476,7 +476,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -504,7 +504,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -513,7 +513,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -541,7 +541,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -550,7 +550,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -579,7 +579,7 @@ SCENARIO( 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")); + param_x.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -588,7 +588,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -616,7 +616,7 @@ SCENARIO( 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")); + param_u.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -625,7 +625,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -653,7 +653,7 @@ SCENARIO( 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")); + param_u.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -662,7 +662,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -690,7 +690,7 @@ SCENARIO( 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")); + param_u.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -701,7 +701,7 @@ SCENARIO( 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")); + param_v.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -710,7 +710,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -738,7 +738,7 @@ SCENARIO( 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")); + param_u.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -749,7 +749,7 @@ SCENARIO( 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")); + param_v.type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 @@ -758,7 +758,7 @@ SCENARIO( THEN("It has return type pointing to Generic") { require_type::require_pointer( - func_code.return_type(), symbol_typet("java::Generic")); + func_code.return_type(), struct_tag_typet("java::Generic")); // TODO: the bounds are not parsed yet; extend tests when fixed - // issue TG-1286 diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp index 9d9ac6a6068..8f2eb2421ce 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp @@ -36,9 +36,9 @@ SCENARIO( const java_class_typet &upper_type = to_java_class_type(upper_symbol.type); REQUIRE(upper_type.bases().size() == 1); - const symbol_typet base_type = require_type::require_symbol( + const struct_tag_typet base_type = require_type::require_struct_tag( upper_type.bases().at(0).type(), base_generic); - REQUIRE_FALSE(is_java_generic_symbol_type(base_type)); + REQUIRE_FALSE(is_java_generic_struct_tag_type(base_type)); } { const symbolt &lower_symbol = @@ -46,9 +46,9 @@ SCENARIO( const java_class_typet &lower_type = to_java_class_type(lower_symbol.type); REQUIRE(lower_type.bases().size() == 1); - const symbol_typet base_type = require_type::require_symbol( + const struct_tag_typet base_type = require_type::require_struct_tag( lower_type.bases().at(0).type(), base_generic); - REQUIRE_FALSE(is_java_generic_symbol_type(base_type)); + REQUIRE_FALSE(is_java_generic_struct_tag_type(base_type)); } { const symbolt &interface_symbol = @@ -56,9 +56,9 @@ SCENARIO( const java_class_typet &interface_type = to_java_class_type(interface_symbol.type); REQUIRE(interface_type.bases().size() == 2); - const symbol_typet base_type = require_type::require_symbol( + const struct_tag_typet base_type = require_type::require_struct_tag( interface_type.bases().at(1).type(), base_generic_interface); - REQUIRE_FALSE(is_java_generic_symbol_type(base_type)); + REQUIRE_FALSE(is_java_generic_struct_tag_type(base_type)); } } } 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 d7b03574414..c4a1bcc9bdd 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 @@ -31,7 +31,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field"); require_type::require_pointer( - field_component.type(), symbol_typet("java::Generic")); + field_component.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -54,7 +54,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field2"); require_type::require_pointer( - field_component.type(), symbol_typet("java::Generic")); + field_component.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -77,7 +77,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field3"); require_type::require_pointer( - field_component.type(), symbol_typet("java::Generic")); + field_component.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -107,7 +107,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field4"); require_type::require_pointer( - field_component.type(), symbol_typet("java::Generic")); + field_component.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -137,7 +137,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field5"); require_type::require_pointer( - field_component.type(), symbol_typet("java::Generic")); + field_component.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -163,7 +163,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field6"); require_type::require_pointer( - field_component.type(), symbol_typet("java::Generic")); + field_component.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -189,7 +189,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field7"); require_type::require_pointer( - field_component.type(), symbol_typet("java::Generic")); + field_component.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -215,7 +215,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field8"); require_type::require_pointer( - field_component.type(), symbol_typet("java::GenericTwoParam")); + field_component.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -246,7 +246,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field9"); require_type::require_pointer( - field_component.type(), symbol_typet("java::GenericTwoParam")); + field_component.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -277,7 +277,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field10"); require_type::require_pointer( - field_component.type(), symbol_typet("java::GenericTwoParam")); + field_component.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -308,7 +308,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field11"); require_type::require_pointer( - field_component.type(), symbol_typet("java::GenericTwoParam")); + field_component.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -334,7 +334,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field12"); require_type::require_pointer( - field_component.type(), symbol_typet("java::GenericTwoParam")); + field_component.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -367,7 +367,7 @@ SCENARIO( const struct_typet::componentt &field_component = require_type::require_component(class_type, "field13"); require_type::require_pointer( - field_component.type(), symbol_typet("java::GenericTwoParam")); + field_component.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -425,7 +425,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::Generic")); + param_type.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -463,7 +463,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::Generic")); + param_type.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -501,7 +501,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::Generic")); + param_type.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -546,7 +546,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::Generic")); + param_type.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -591,7 +591,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::Generic")); + param_type.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -632,7 +632,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::Generic")); + param_type.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -673,7 +673,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::Generic")); + param_type.type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -714,7 +714,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::GenericTwoParam")); + param_type.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -759,7 +759,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::GenericTwoParam")); + param_type.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -804,7 +804,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::GenericTwoParam")); + param_type.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -849,7 +849,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::GenericTwoParam")); + param_type.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -890,7 +890,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::GenericTwoParam")); + param_type.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -937,7 +937,7 @@ SCENARIO( const auto ¶m_type = require_type::require_parameter(function_call, "input"); require_type::require_pointer( - param_type.type(), symbol_typet("java::GenericTwoParam")); + param_type.type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -982,7 +982,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::Generic")); + function_call.return_type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -1018,7 +1018,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::Generic")); + function_call.return_type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -1054,7 +1054,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::Generic")); + function_call.return_type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -1096,7 +1096,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::Generic")); + function_call.return_type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -1138,7 +1138,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::Generic")); + function_call.return_type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -1177,7 +1177,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::Generic")); + function_call.return_type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -1216,7 +1216,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::Generic")); + function_call.return_type(), struct_tag_typet("java::Generic")); THEN("The pointer should be generic") { @@ -1255,7 +1255,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::GenericTwoParam")); + function_call.return_type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -1298,7 +1298,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::GenericTwoParam")); + function_call.return_type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -1341,7 +1341,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::GenericTwoParam")); + function_call.return_type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -1384,7 +1384,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::GenericTwoParam")); + function_call.return_type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -1423,7 +1423,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::GenericTwoParam")); + function_call.return_type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { @@ -1468,7 +1468,7 @@ SCENARIO( THEN("The return type is correct") { require_type::require_pointer( - function_call.return_type(), symbol_typet("java::GenericTwoParam")); + function_call.return_type(), struct_tag_typet("java::GenericTwoParam")); THEN("The pointer should be generic") { diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp index 8bbbdd3aba6..81c01a2b64b 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp @@ -285,7 +285,7 @@ SCENARIO( REQUIRE(id2string(lambda_method.descriptor) == method_type); const reference_typet dummy_generic_reference_type = - java_reference_type(symbol_typet{"java.lang.Object"}); + java_reference_type(struct_tag_typet{"java.lang.Object"}); // NOLINTNEXTLINE(whitespace/braces) fieldref_exprt fieldref{ @@ -318,7 +318,7 @@ SCENARIO( REQUIRE(id2string(lambda_method.descriptor) == method_type); const reference_typet dummy_generic_reference_type = - java_reference_type(symbol_typet{"DummyGeneric"}); + java_reference_type(struct_tag_typet{"DummyGeneric"}); fieldref_exprt fieldref{dummy_generic_reference_type, "staticSpecalisedGeneric", @@ -912,7 +912,7 @@ SCENARIO( REQUIRE_FALSE(lambda_method.is_static); const reference_typet dummy_generic_reference_type = - java_reference_type(symbol_typet{"java.lang.Object"}); + java_reference_type(struct_tag_typet{"java.lang.Object"}); // NOLINTNEXTLINE(whitespace/braces) const fieldref_exprt reference_fieldref{ @@ -951,7 +951,7 @@ SCENARIO( REQUIRE_FALSE(lambda_method.is_static); const reference_typet dummy_generic_reference_type = - java_reference_type(symbol_typet{"DummyGeneric"}); + java_reference_type(struct_tag_typet{"DummyGeneric"}); // NOLINTNEXTLINE(whitespace/braces) const fieldref_exprt generic_reference_fieldref{ @@ -999,7 +999,7 @@ SCENARIO( // Field ref for getting the outer class const reference_typet outer_class_reference_type = - java_reference_type(symbol_typet{"OuterMemberLambdas"}); + java_reference_type(struct_tag_typet{"OuterMemberLambdas"}); // NOLINTNEXTLINE(whitespace/braces) const fieldref_exprt outer_fieldref{ outer_class_reference_type, "this$0", "OuterMemberLambdas$Inner"}; @@ -1065,7 +1065,7 @@ SCENARIO( REQUIRE_FALSE(lambda_method.is_static); const reference_typet dummy_generic_reference_type = - java_reference_type(symbol_typet{"java.lang.Object"}); + java_reference_type(struct_tag_typet{"java.lang.Object"}); // NOLINTNEXTLINE(whitespace/braces) const fieldref_exprt reference_fieldref{ @@ -1107,7 +1107,7 @@ SCENARIO( REQUIRE_FALSE(lambda_method.is_static); const reference_typet dummy_generic_reference_type = - java_reference_type(symbol_typet{"DummyGeneric"}); + java_reference_type(struct_tag_typet{"DummyGeneric"}); // NOLINTNEXTLINE(whitespace/braces) const fieldref_exprt generic_reference_fieldref{ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp index cc8c5014fc2..73ac2a0ac19 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp @@ -93,7 +93,7 @@ SCENARIO( to_symbol_expr(element_value_pair.value).get_identifier(); const auto &java_type = java_type_from_string(id2string(id)); const std::string &class_name = - id2string(to_symbol_type(java_type.subtype()).get_identifier()); + id2string(to_struct_tag_type(java_type.subtype()).get_identifier()); REQUIRE(id2string(class_name) == "java::java.lang.String"); } } diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index 3c39c5a078e..3d2b388a965 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -43,7 +43,7 @@ SCENARIO( namespacet ns(symbol_table); // Declare a String named arg - symbol_typet java_string_type("java::java.lang.String"); + struct_tag_typet java_string_type("java::java.lang.String"); symbol_exprt expr("arg", java_string_type); java_object_factory_parameterst object_factory_parameters; diff --git a/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp index fb65105afbb..b61b57baad4 100644 --- a/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp +++ b/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp @@ -38,7 +38,7 @@ TEST_CASE("Convert exprt to string exprt") code_blockt code; java_string_library_preprocesst preprocess; preprocess.add_string_type("java.lang.String", symbol_table); - symbol_typet java_string_type("java::java.lang.String"); + struct_tag_typet java_string_type("java::java.lang.String"); symbol_exprt expr("a", pointer_type(java_string_type)); WHEN("String expression is converted to refined string expression") diff --git a/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp b/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp index 3dcadf430b1..18ac39cd497 100644 --- a/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp +++ b/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp @@ -14,21 +14,22 @@ SCENARIO("generic_type_index", "[core][java_types]") GIVEN("PrefixClassName extends GenericClass, " "and parameters X, value, Z") { - const auto symbol_type = symbol_typet("java::GenericClass"); - const auto generic_symbol_type = java_generic_symbol_typet( - symbol_type, "LGenericClass;", "PrefixClassName"); + const auto struct_tag_type = struct_tag_typet("java::GenericClass"); + const auto generic_struct_tag_type = java_generic_struct_tag_typet( + struct_tag_type, "LGenericClass;", "PrefixClassName"); java_generic_parametert paramX( - "PrefixClassName::X", symbol_typet(irep_idt())); + "PrefixClassName::X", struct_tag_typet(irep_idt())); java_generic_parametert value( - "PrefixClassName::value", symbol_typet(irep_idt())); + "PrefixClassName::value", struct_tag_typet(irep_idt())); java_generic_parametert paramZ( - "PrefixClassName::Z", symbol_typet(irep_idt())); + "PrefixClassName::Z", struct_tag_typet(irep_idt())); WHEN("Looking for parameter indexes") { - const auto indexX = generic_symbol_type.generic_type_index(paramX); - const auto index_value = generic_symbol_type.generic_type_index(value); - const auto indexZ = generic_symbol_type.generic_type_index(paramZ); + const auto indexX = generic_struct_tag_type.generic_type_index(paramX); + const auto index_value = + generic_struct_tag_type.generic_type_index(value); + const auto indexZ = generic_struct_tag_type.generic_type_index(paramZ); THEN("X has index 0, Y index 1 and Z is not found") { @@ -43,21 +44,24 @@ SCENARIO("generic_type_index", "[core][java_types]") GIVEN("HashMap extends Map, and parameters K, V, T") { - const auto symbol_type = symbol_typet("java::java.util.Map"); - const auto generic_symbol_type = java_generic_symbol_typet( - symbol_type, "Ljava/util/Map;", "java.util.HashMap"); + const auto struct_tag_type = struct_tag_typet("java::java.util.Map"); + const auto generic_struct_tag_type = java_generic_struct_tag_typet( + struct_tag_type, "Ljava/util/Map;", "java.util.HashMap"); java_generic_parametert param0( - "java.util.HashMap::K", symbol_typet(irep_idt())); + "java.util.HashMap::K", struct_tag_typet(irep_idt())); java_generic_parametert param1( - "java.util.HashMap::V", symbol_typet(irep_idt())); + "java.util.HashMap::V", struct_tag_typet(irep_idt())); java_generic_parametert param2( - "java.util.HashMap::T", symbol_typet(irep_idt())); + "java.util.HashMap::T", struct_tag_typet(irep_idt())); WHEN("Looking for parameter indexes") { - const auto index_param0 = generic_symbol_type.generic_type_index(param0); - const auto index_param1 = generic_symbol_type.generic_type_index(param1); - const auto index_param2 = generic_symbol_type.generic_type_index(param2); + const auto index_param0 = + generic_struct_tag_type.generic_type_index(param0); + const auto index_param1 = + generic_struct_tag_type.generic_type_index(param1); + const auto index_param2 = + generic_struct_tag_type.generic_type_index(param2); THEN("K has index 0, V index 1 and T is not found") { diff --git a/jbmc/unit/java_bytecode/java_types/java_generic_symbol_type.cpp b/jbmc/unit/java_bytecode/java_types/java_generic_symbol_type.cpp index d24e8bd2e54..86ff70500a3 100644 --- a/jbmc/unit/java_bytecode/java_types/java_generic_symbol_type.cpp +++ b/jbmc/unit/java_bytecode/java_types/java_generic_symbol_type.cpp @@ -9,17 +9,17 @@ #include #include -SCENARIO("java_generic_symbol_type", "[core][java_types]") +SCENARIO("java_generic_struct_tag_type", "[core][java_types]") { GIVEN("LGenericClass;") { - auto symbol_type = symbol_typet("java::GenericClass"); - const auto generic_symbol_type = java_generic_symbol_typet( - symbol_type, "LGenericClass;", "PrefixClassName"); + auto struct_tag_type = struct_tag_typet("java::GenericClass"); + const auto generic_struct_tag_type = java_generic_struct_tag_typet( + struct_tag_type, "LGenericClass;", "PrefixClassName"); - REQUIRE(generic_symbol_type.get_identifier() == "java::GenericClass"); + REQUIRE(generic_struct_tag_type.get_identifier() == "java::GenericClass"); - auto types = generic_symbol_type.generic_types(); + auto types = generic_struct_tag_type.generic_types(); REQUIRE(types.size() == 2); auto generic_var0 = to_java_generic_parameter(types[0]).type_variable(); diff --git a/jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp b/jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp index e6d7eac80ea..964e56165ea 100644 --- a/jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp +++ b/jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp @@ -41,8 +41,8 @@ SCENARIO("java_type_from_string", "[core][java_types]") GIVEN("Ljava/util/Map;") { - const auto generic_symbol_type = + const auto generic_struct_tag_type = java_type_from_string("Ljava/util/Map;", "java.util.Map"); - REQUIRE(generic_symbol_type != nil_typet()); + REQUIRE(generic_struct_tag_type != nil_typet()); } } diff --git a/jbmc/unit/util/has_subtype.cpp b/jbmc/unit/util/has_subtype.cpp index 93b2505e558..17614f530ab 100644 --- a/jbmc/unit/util/has_subtype.cpp +++ b/jbmc/unit/util/has_subtype.cpp @@ -66,8 +66,8 @@ SCENARIO("has_subtype", "[core][utils][has_subtype]") GIVEN("a recursive struct definition") { - symbol_typet symbol_type("A-struct"); - struct_typet::componentt comp("ptr", pointer_type(symbol_type)); + struct_tag_typet struct_tag("A-struct"); + struct_typet::componentt comp("ptr", pointer_type(struct_tag)); struct_typet struct_type; struct_type.components().push_back(comp); @@ -84,7 +84,7 @@ SCENARIO("has_subtype", "[core][utils][has_subtype]") } THEN("symbol type is a subtype") { - REQUIRE(has_subtype(struct_type, is_type(pointer_type(symbol_type)), ns)); + REQUIRE(has_subtype(struct_type, is_type(pointer_type(struct_tag)), ns)); } THEN("struct type is a subtype") { diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index 958660dee27..be9485fcbcb 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -19,8 +19,8 @@ irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type) { PRECONDITION(type.id()==ID_pointer); - if(type.subtype().id() == ID_symbol_type) - return to_symbol_type(type.subtype()).get_identifier(); + if(type.subtype().id() == ID_struct_tag) + return to_struct_tag_type(type.subtype()).get_identifier(); else return ID_empty; } diff --git a/src/goto-programs/class_identifier.cpp b/src/goto-programs/class_identifier.cpp index 23411c3b6e8..d247583af15 100644 --- a/src/goto-programs/class_identifier.cpp +++ b/src/goto-programs/class_identifier.cpp @@ -55,7 +55,7 @@ static exprt build_class_identifier( /// \return Member expression to access a class identifier, as above. exprt get_class_identifier_field( const exprt &this_expr_in, - const symbol_typet &suggested_type, + const struct_tag_typet &suggested_type, const namespacet &ns) { // Get a pointer from which we can extract a clsid. @@ -82,7 +82,7 @@ exprt get_class_identifier_field( void set_class_identifier( struct_exprt &expr, const namespacet &ns, - const symbol_typet &class_type) + const struct_tag_typet &class_type) { const struct_typet &struct_type=to_struct_type(ns.follow(expr.type())); const struct_typet::componentst &components=struct_type.components(); diff --git a/src/goto-programs/class_identifier.h b/src/goto-programs/class_identifier.h index 277c99895d2..73bb750ac7e 100644 --- a/src/goto-programs/class_identifier.h +++ b/src/goto-programs/class_identifier.h @@ -14,17 +14,17 @@ Author: Chris Smowton, chris.smowton@diffblue.com class exprt; class namespacet; -class symbol_typet; +class struct_tag_typet; class struct_exprt; exprt get_class_identifier_field( const exprt &this_expr, - const symbol_typet &suggested_type, + const struct_tag_typet &suggested_type, const namespacet &ns); void set_class_identifier( struct_exprt &expr, const namespacet &ns, - const symbol_typet &class_type); + const struct_tag_typet &class_type); #endif diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index e61c3ff830a..7e54bc32842 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -206,7 +206,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( // So long as `this` is already not `void*` typed, the second parameter // is ignored: exprt this_class_identifier = - get_class_identifier_field(this_expr, symbol_typet(irep_idt()), ns); + get_class_identifier_field(this_expr, struct_tag_typet(irep_idt()), ns); // If instructed, add an ASSUME(FALSE) to handle the case where we don't // match any expected type: diff --git a/src/goto-programs/string_abstraction.h b/src/goto-programs/string_abstraction.h index da78ecd3779..220e5465359 100644 --- a/src/goto-programs/string_abstraction.h +++ b/src/goto-programs/string_abstraction.h @@ -52,7 +52,7 @@ class string_abstractiont:public messaget bool is_char_type(const typet &type) const { - if(type.id() == ID_symbol_type) + if(type.id() == ID_struct_tag) return is_char_type(ns.follow(type)); if(type.id()!=ID_signedbv && diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 9cca8a0219f..9c94a6416d2 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -36,8 +36,8 @@ bool is_char_type(const typet &type) bool is_char_array_type(const typet &type, const namespacet &ns) { - if(type.id() == ID_symbol_type) - return is_char_array_type(ns.follow(type), ns); + if(type.id() == ID_struct_tag) + return is_char_array_type(ns.follow_tag(to_struct_tag_type(type)), ns); return type.id() == ID_array && is_char_type(type.subtype()); } From 84228a4b92c7183546beec4098347e51c57d3731 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 29 Sep 2018 10:55:09 +0100 Subject: [PATCH 2/5] use a struct_tag to identify base classes --- src/util/std_types.cpp | 29 +++++++++++++++++++++++++++++ src/util/std_types.h | 33 +++++++-------------------------- 2 files changed, 36 insertions(+), 26 deletions(-) diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index 98ba0dc2aa0..85f85303b56 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -70,6 +70,35 @@ struct_union_typet::component_type(const irep_idt &component_name) const return c.type(); } +struct_tag_typet &struct_typet::baset::type() +{ + return to_struct_tag_type(exprt::type()); +} + +const struct_tag_typet &struct_typet::baset::type() const +{ + return to_struct_tag_type(exprt::type()); +} + +struct_typet::baset::baset(const struct_tag_typet &base) : exprt(ID_base, base) +{ +} + +void struct_typet::add_base(const struct_tag_typet &base) +{ + bases().push_back(baset(base)); +} + +optionalt struct_typet::get_base(const irep_idt &id) const +{ + for(const auto &b : bases()) + { + if(to_struct_tag_type(b.type()).get_identifier() == id) + return b; + } + return {}; +} + /// Returns true if the struct is a prefix of \a other, i.e., if this struct /// has n components then the component types and names of this struct must /// match the first n components of \a other struct. diff --git a/src/util/std_types.h b/src/util/std_types.h index 3eaae96d01f..410fa2623fe 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -270,6 +270,8 @@ inline struct_union_typet &to_struct_union_type(typet &type) return static_cast(type); } +class struct_tag_typet; + /// Structure type, corresponds to C style structs class struct_typet:public struct_union_typet { @@ -290,19 +292,9 @@ class struct_typet:public struct_union_typet class baset : public exprt { public: - symbol_typet &type() - { - return to_symbol_type(exprt::type()); - } - - const symbol_typet &type() const - { - return to_symbol_type(exprt::type()); - } - - explicit baset(const symbol_typet &base) : exprt(ID_base, base) - { - } + struct_tag_typet &type(); + const struct_tag_typet &type() const; + explicit baset(const struct_tag_typet &base); }; typedef std::vector basest; @@ -321,23 +313,12 @@ class struct_typet:public struct_union_typet /// Add a base class/struct /// \param base: Type of case/class struct to be added. - void add_base(const symbol_typet &base) - { - bases().push_back(baset(base)); - } + void add_base(const struct_tag_typet &base); /// Return the base with the given name, if exists. /// \param id The name of the base we are looking for. /// \return The base if exists. - optionalt get_base(const irep_idt &id) const - { - for(const auto &b : bases()) - { - if(to_symbol_type(b.type()).get_identifier() == id) - return b; - } - return {}; - } + optionalt get_base(const irep_idt &id) const; /// Test whether `id` is a base class/struct. /// \param id: symbol type name From 2026b01d4862213f20b3ee6142cab69f31da388e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 5 Oct 2018 16:12:23 +0100 Subject: [PATCH 3/5] C++: bases are now struct tags --- src/cpp/cpp_typecheck_bases.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/cpp/cpp_typecheck_bases.cpp b/src/cpp/cpp_typecheck_bases.cpp index 703a49a5a76..68156d96c1c 100644 --- a/src/cpp/cpp_typecheck_bases.cpp +++ b/src/cpp/cpp_typecheck_bases.cpp @@ -43,10 +43,10 @@ void cpp_typecheckt::typecheck_compound_bases(struct_typet &type) // elaborate any class template instances given as bases elaborate_class_template(base_symbol_expr.type()); - if(base_symbol_expr.type().id() == ID_struct_tag) - base_symbol_expr.type().id(ID_symbol_type); + if(base_symbol_expr.type().id() == ID_symbol_type) + base_symbol_expr.type().id(ID_struct_tag); - if(base_symbol_expr.type().id() != ID_symbol_type) + if(base_symbol_expr.type().id() != ID_struct_tag) { error().source_location=name.source_location(); error() << "expected type symbol as struct/class base" << eom; @@ -54,7 +54,7 @@ void cpp_typecheckt::typecheck_compound_bases(struct_typet &type) } const symbolt &base_symbol = - lookup(to_symbol_type(base_symbol_expr.type())); + lookup(to_struct_tag_type(base_symbol_expr.type())); if(base_symbol.type.id()==ID_incomplete_struct) { From d1347f73179e6d809d592177781c3ae717995640 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Wed, 5 Dec 2018 15:13:22 +0000 Subject: [PATCH 4/5] Handle ID_struct_tag in interpreter get_size() --- src/goto-programs/interpreter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index df1c9fdafbe..75762b5fc9f 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -1031,7 +1031,7 @@ mp_integer interpretert::get_size(const typet &type) } return subtype_size; } - else if(type.id() == ID_symbol_type) + else if(type.id() == ID_symbol_type || type.id() == ID_struct_tag) { return get_size(ns.follow(type)); } From 0b2d3b164b6d7250b6f0d24c512ca2011d389767 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Wed, 5 Dec 2018 16:29:52 +0000 Subject: [PATCH 5/5] Doc linting --- .../generic_parameter_specialization_map_keys.cpp | 3 ++- jbmc/src/java_bytecode/java_types.cpp | 8 ++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp index f6f91cd0ca2..be9f02ebb32 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp @@ -147,7 +147,8 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol( // - an incomplete class or // - a class that is neither generic nor implicitly generic (this // may be due to unsupported class signature) - // then ignore the generic types in the struct_tag_type and do not add any pairs. + // then ignore the generic types in the struct_tag_type and do not add any + // pairs. // TODO TG-1996 should decide how mocking and generics should work // together. Currently an incomplete class is never marked as generic. If // this changes in TG-1996 then the condition below should be updated. diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index cedd4189e08..b4491b6cca8 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -917,10 +917,10 @@ void get_dependencies_from_generic_parameters( /// This assumes that the class named \p class_name_prefix extends or implements /// the class \p type, and that \p base_ref corresponds to a generic class. /// For instance since HashMap extends Map we would call -/// `java_generic_struct_tag_typet(struct_tag_typet("Map"), "Ljava/util/Map;", -/// "java.util.HashMap")` which generates a symbol type with identifier "Map", -/// and two generic types with identifier "java.util.HashMap::K" and -/// "java.util.HashMap::V" respectively. +/// `java_generic_struct_tag_typet(struct_tag_typet("Map"), +/// "Ljava/util/Map;", "java.util.HashMap")` which generates a symbol +/// type with identifier "Map", and two generic types with identifier +/// "java.util.HashMap::K" and "java.util.HashMap::V" respectively. java_generic_struct_tag_typet::java_generic_struct_tag_typet( const struct_tag_typet &type, const std::string &base_ref,