From 74cfc8b19b7b5f371cbcb0052000c8b8d9f7bbf9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 19 Feb 2024 15:23:39 +0000 Subject: [PATCH] JBMC: Replace uses of namespacet::follow This is deprecated. Use suitable variants of `follow_tag` instead. --- .../java_bytecode/assignments_from_json.cpp | 15 ++++--- jbmc/src/java_bytecode/expr2java.cpp | 4 +- ...a_bytecode_concurrency_instrumentation.cpp | 5 +-- .../java_bytecode_convert_method.cpp | 2 +- .../java_bytecode/java_bytecode_language.cpp | 7 ++-- .../src/java_bytecode/java_object_factory.cpp | 42 +++++++++---------- jbmc/src/java_bytecode/java_pointer_casts.cpp | 21 ++++++---- .../java_string_library_preprocess.cpp | 3 +- .../java_bytecode/java_string_literals.cpp | 4 +- jbmc/src/java_bytecode/remove_java_new.cpp | 3 +- .../java_bytecode/simple_method_stubbing.cpp | 7 +--- 11 files changed, 57 insertions(+), 56 deletions(-) diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp index f9e7a075807..bc461979943 100644 --- a/jbmc/src/java_bytecode/assignments_from_json.cpp +++ b/jbmc/src/java_bytecode/assignments_from_json.cpp @@ -67,9 +67,8 @@ static java_class_typet followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table) { const pointer_typet &pointer_type = to_pointer_type(expr.type()); - const java_class_typet &java_class_type = to_java_class_type( - namespacet{symbol_table}.follow(pointer_type.base_type())); - return java_class_type; + return to_java_class_type(namespacet{symbol_table}.follow_tag( + to_struct_tag_type(pointer_type.base_type()))); } static bool @@ -530,8 +529,8 @@ static code_with_references_listt assign_struct_components_from_json( const jsont &json, object_creation_infot &info) { - const java_class_typet &java_class_type = - to_java_class_type(namespacet{info.symbol_table}.follow(expr.type())); + const java_class_typet &java_class_type = to_java_class_type( + namespacet{info.symbol_table}.follow_tag(to_struct_tag_type(expr.type()))); code_with_references_listt result; for(const auto &component : java_class_type.components()) { @@ -576,7 +575,7 @@ static code_with_references_listt assign_struct_from_json( { const namespacet ns{info.symbol_table}; const java_class_typet &java_class_type = - to_java_class_type(ns.follow(expr.type())); + to_java_class_type(ns.follow_tag(to_struct_tag_type(expr.type()))); code_with_references_listt result; if(is_java_string_type(java_class_type)) { @@ -641,8 +640,8 @@ static code_with_references_listt assign_enum_from_json( dereference_exprt values_struct{ info.symbol_table.lookup_ref(values_name).symbol_expr()}; - const auto &values_struct_type = - to_struct_type(namespacet{info.symbol_table}.follow(values_struct.type())); + const auto &values_struct_type = namespacet{info.symbol_table}.follow_tag( + to_struct_tag_type(values_struct.type())); PRECONDITION(is_valid_java_array(values_struct_type)); const member_exprt values_data = member_exprt{ values_struct, "data", values_struct_type.components()[2].type()}; diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index c5c69145449..223988d10f6 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/jbmc/src/java_bytecode/expr2java.cpp @@ -105,7 +105,9 @@ std::string expr2javat::convert_struct( const exprt &src, unsigned &precedence) { - const typet &full_type=ns.follow(src.type()); + const typet &full_type = src.type().id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(src.type())) + : src.type(); if(full_type.id()!=ID_struct) return convert_norep(src, precedence); diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp index d90414ac368..0ae89521cdf 100644 --- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp @@ -409,9 +409,8 @@ static void instrument_get_monitor_count( PRECONDITION(f_code.arguments().size() == 1); const namespacet ns(symbol_table); - const auto &followed_type = - ns.follow(to_pointer_type(f_code.arguments()[0].type()).base_type()); - const auto &object_type = to_struct_type(followed_type); + const auto &object_type = ns.follow_tag(to_struct_tag_type( + to_pointer_type(f_code.arguments()[0].type()).base_type())); code_assignt code_assign( f_code.lhs(), member_exprt( diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 758bcdf6ec8..1bae680fa5d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -667,7 +667,7 @@ static member_exprt to_member( exprt accessed_object = checked_dereference(typed_pointer); const auto type_of = [&ns](const exprt &object) { - return to_struct_type(ns.follow(object.type())); + return ns.follow_tag(to_struct_tag_type(object.type())); }; // The field access is described as being against a particular type, but it diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index c01b67e100a..7d9e8262da6 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -507,7 +507,8 @@ static void infer_opaque_type_fields( "') should have an opaque superclass"); const auto &superclass_type = class_type->bases().front().type(); class_symbol_id = superclass_type.get_identifier(); - class_type = &to_java_class_type(ns.follow(superclass_type)); + class_type = &to_java_class_type( + ns.follow_tag(to_struct_tag_type(superclass_type))); } } } @@ -1502,8 +1503,8 @@ bool java_bytecode_languaget::convert_single_method_code( // TODO(tkiley): ci_lazy_methods_neededt, but this needs further // TODO(tkiley): investigation namespacet ns{symbol_table}; - const java_class_typet &underlying_type = - to_java_class_type(ns.follow(pointer_return_type->base_type())); + const java_class_typet &underlying_type = to_java_class_type( + ns.follow_tag(to_struct_tag_type(pointer_return_type->base_type()))); if(!underlying_type.is_abstract()) needed_lazy_methods->add_all_needed_classes(*pointer_return_type); diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 9236637d0f8..9675e9a9c31 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -199,10 +199,8 @@ void java_object_factoryt::gen_pointer_target_init( PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE); const namespacet ns(symbol_table); - const typet &followed_target_type = ns.follow(target_type); - PRECONDITION(followed_target_type.id() == ID_struct); - - const auto &target_class_type = to_java_class_type(followed_target_type); + const auto &target_class_type = + to_java_class_type(ns.follow_tag(to_struct_tag_type(target_type))); if(target_class_type.get_tag().starts_with("java::array[")) { assignments.append(gen_nondet_array_init( @@ -374,7 +372,7 @@ void initialize_nondet_string_fields( { namespacet ns(symbol_table); const struct_typet &struct_type = - to_struct_type(ns.follow(struct_expr.type())); + ns.follow_tag(to_struct_tag_type(struct_expr.type())); PRECONDITION(is_java_string_type(struct_type)); // We allow type StringBuffer and StringBuilder to be initialized @@ -481,9 +479,6 @@ void java_object_factoryt::gen_nondet_pointer_init( { PRECONDITION(expr.type().id()==ID_pointer); const namespacet ns(symbol_table); - const typet &subtype = pointer_type.base_type(); - const typet &followed_subtype = ns.follow(subtype); - PRECONDITION(followed_subtype.id() == ID_struct); const pointer_typet &replacement_pointer_type = pointer_type_selector.convert_pointer_type( pointer_type, generic_parameter_specialization_map, ns); @@ -501,7 +496,7 @@ void java_object_factoryt::gen_nondet_pointer_init( generic_parameter_specialization_map); generic_parameter_specialization_map_keys.insert( replacement_pointer_type, - ns.follow(replacement_pointer_type.base_type())); + ns.follow_tag(to_struct_tag_type(replacement_pointer_type.base_type()))); const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init( assignments, lifetime, replacement_pointer_type, depth, location); @@ -529,7 +524,9 @@ void java_object_factoryt::gen_nondet_pointer_init( // When we visit for 2nd time a type AND the maximum depth is exceeded, we set // the pointer to NULL instead of recursively initializing the struct to which // it points. - const struct_typet &struct_type = to_struct_type(followed_subtype); + const struct_tag_typet &tag_type = + to_struct_tag_type(pointer_type.base_type()); + const struct_typet &struct_type = ns.follow_tag(tag_type); const irep_idt &struct_tag = struct_type.get_tag(); // If this is a recursive type of some kind AND the depth is exceeded, set @@ -564,7 +561,7 @@ void java_object_factoryt::gen_nondet_pointer_init( // ci_lazy_methodst::initialize_instantiated_classes. if( const auto class_type = - type_try_dynamic_cast(followed_subtype)) + type_try_dynamic_cast(struct_type)) { if(class_type->get_base("java::java.lang.Enum")) { @@ -581,13 +578,13 @@ void java_object_factoryt::gen_nondet_pointer_init( // if the initialization mode is MAY_UPDATE or MUST_UPDATE in place, then we // emit to `update_in_place_assignments` code for in-place initialization of // the object pointed by `expr`, assuming that such object is of type - // `subtype` + // `tag_type` if(update_in_place!=update_in_placet::NO_UPDATE_IN_PLACE) { gen_pointer_target_init( update_in_place_assignments, expr, - subtype, + tag_type, lifetime, depth, update_in_placet::MUST_UPDATE_IN_PLACE, @@ -610,7 +607,7 @@ void java_object_factoryt::gen_nondet_pointer_init( gen_pointer_target_init( non_null_inst, expr, - subtype, + tag_type, lifetime, depth, update_in_placet::NO_UPDATE_IN_PLACE, @@ -773,7 +770,7 @@ void java_object_factoryt::gen_nondet_struct_init( const source_locationt &location) { const namespacet ns(symbol_table); - PRECONDITION(ns.follow(expr.type()).id()==ID_struct); + PRECONDITION(expr.type().id() == ID_struct_tag); typedef struct_typet::componentst componentst; const irep_idt &struct_tag=struct_type.get_tag(); @@ -1008,7 +1005,6 @@ void java_object_factoryt::gen_nondet_init( { const typet &type = override_type.has_value() ? *override_type : expr.type(); const namespacet ns(symbol_table); - const typet &followed_type = ns.follow(type); if(type.id()==ID_pointer) { @@ -1021,7 +1017,8 @@ void java_object_factoryt::gen_nondet_init( generic_parameter_specialization_map_keys( generic_parameter_specialization_map); generic_parameter_specialization_map_keys.insert( - pointer_type, ns.follow(pointer_type.base_type())); + pointer_type, + ns.follow_tag(to_struct_tag_type(pointer_type.base_type()))); gen_nondet_pointer_init( assignments, @@ -1032,9 +1029,9 @@ void java_object_factoryt::gen_nondet_init( update_in_place, location); } - else if(followed_type.id() == ID_struct) + else if(type.id() == ID_struct_tag) { - const struct_typet struct_type = to_struct_type(followed_type); + const struct_typet struct_type = ns.follow_tag(to_struct_tag_type(type)); // If we are about to initialize a generic class (as a superclass object // for a different object), add its concrete types to the map and delete @@ -1388,8 +1385,8 @@ code_blockt gen_nondet_array_init( code_blockt statements; const namespacet ns(symbol_table); - const typet &type = ns.follow(to_pointer_type(expr.type()).base_type()); - const struct_typet &struct_type = to_struct_type(type); + const struct_typet &struct_type = + ns.follow_tag(to_struct_tag_type(to_pointer_type(expr.type()).base_type())); const typet &element_type = static_cast( to_pointer_type(expr.type()).base_type().find(ID_element_type)); @@ -1492,7 +1489,8 @@ bool java_object_factoryt::gen_nondet_enum_init( // Access members (length and data) of $VALUES array dereference_exprt deref_expr(values.symbol_expr()); - const auto &deref_struct_type = to_struct_type(ns.follow(deref_expr.type())); + const auto &deref_struct_type = + ns.follow_tag(to_struct_tag_type(deref_expr.type())); PRECONDITION(is_valid_java_array(deref_struct_type)); const auto &comps = deref_struct_type.components(); const member_exprt length_expr(deref_expr, "length", comps[1].type()); diff --git a/jbmc/src/java_bytecode/java_pointer_casts.cpp b/jbmc/src/java_bytecode/java_pointer_casts.cpp index e5fd1d399cf..63a439959e6 100644 --- a/jbmc/src/java_bytecode/java_pointer_casts.cpp +++ b/jbmc/src/java_bytecode/java_pointer_casts.cpp @@ -37,12 +37,11 @@ bool find_superclass_with_type( PRECONDITION(ptr.type().id() == ID_pointer); while(true) { - const typet ptr_base = ns.follow(to_pointer_type(ptr.type()).base_type()); - - if(ptr_base.id()!=ID_struct) + const typet &ptr_base = to_pointer_type(ptr.type()).base_type(); + if(ptr_base.id() != ID_struct_tag) return false; - - const struct_typet &base_struct=to_struct_type(ptr_base); + const struct_typet &base_struct = + ns.follow_tag(to_struct_tag_type(ptr_base)); if(base_struct.components().empty()) return false; @@ -60,7 +59,11 @@ bool find_superclass_with_type( // Compare the real (underlying) type, as target_type is already a non- // symbolic type. - if(ns.follow(first_field_type)==target_type) + const typet &underlying_type = + first_field_type.id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(first_field_type)) + : first_field_type; + if(underlying_type == target_type) return true; } } @@ -88,8 +91,6 @@ exprt make_clean_pointer_cast( return typecast_exprt(ptr, target_type); } - const typet &target_base = ns.follow(target_type.base_type()); - exprt bare_ptr=ptr; while(bare_ptr.id()==ID_typecast) { @@ -112,6 +113,10 @@ exprt make_clean_pointer_cast( // recorded on the pointer, not the pointee), so it may still be necessary // to use a cast to reintroduce the qualifier (for example, the base might // be recorded as a List, when we're looking for a List) + const typet &target_base = + target_type.base_type().id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(target_type.base_type())) + : target_type.base_type(); if(find_superclass_with_type(superclass_ptr, target_base, ns)) return typecast_exprt::conditional_cast(superclass_ptr, target_type); diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 3fed7144ed6..02aade88b5b 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -807,7 +807,8 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string( { // Initialise the supertype with the appropriate classid: namespacet ns(symbol_table); - const struct_typet &lhs_type = to_struct_type(ns.follow(deref.type())); + const struct_typet &lhs_type = + ns.follow_tag(to_struct_tag_type(deref.type())); auto zero_base_object = *zero_initializer( lhs_type.components().front().type(), source_locationt{}, ns); set_class_identifier( diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp index d22899f77e3..d63681580b9 100644 --- a/jbmc/src/java_bytecode/java_string_literals.cpp +++ b/jbmc/src/java_bytecode/java_string_literals.cpp @@ -70,9 +70,9 @@ symbol_exprt get_or_create_string_literal_symbol( // Regardless of string refinement setting, at least initialize // the literal with @clsid = String struct_tag_typet jlo_symbol("java::java.lang.Object"); - const auto &jlo_struct = to_struct_type(ns.follow(jlo_symbol)); + const auto &jlo_struct = ns.follow_tag(jlo_symbol); struct_exprt jlo_init({}, jlo_symbol); - const auto &jls_struct = to_struct_type(ns.follow(string_type)); + const auto &jls_struct = ns.follow_tag(string_type); java_root_class_init(jlo_init, jlo_struct, "java::java.lang.String"); // If string refinement *is* around, populate the actual diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp index 09bb31e5c47..cf50669e28d 100644 --- a/jbmc/src/java_bytecode/remove_java_new.cpp +++ b/jbmc/src/java_bytecode/remove_java_new.cpp @@ -144,7 +144,6 @@ goto_programt::targett remove_java_newt::lower_java_new_array( source_locationt location = rhs.source_location(); struct_tag_typet object_type = to_struct_tag_type(to_pointer_type(rhs.type()).base_type()); - PRECONDITION(ns.follow(object_type).id() == ID_struct); // build size expression const auto object_size = size_of_expr(object_type, ns); @@ -160,7 +159,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array( goto_programt::make_assignment(code_assignt(lhs, malloc_expr), location); goto_programt::targett next = std::next(target); - const struct_typet &struct_type = to_struct_type(ns.follow(object_type)); + const struct_typet &struct_type = ns.follow_tag(object_type); PRECONDITION(is_valid_java_array(struct_type)); diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp index 301bd8cd639..bdcc51908f8 100644 --- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp +++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp @@ -97,13 +97,10 @@ void java_simple_method_stubst::create_method_stub_at( "Nondet initializer result type: expected a pointer", expected_type); - namespacet ns(symbol_table); - - const auto &expected_base = - ns.follow(to_pointer_type(expected_type).base_type()); - if(expected_base.id() != ID_struct) + if(to_pointer_type(expected_type).base_type().id() != ID_struct_tag) return; + namespacet ns(symbol_table); const exprt cast_ptr = make_clean_pointer_cast(ptr, to_pointer_type(expected_type), ns);