diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 5580caa8862..b87fc9c2280 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -375,7 +375,7 @@ void java_bytecode_convert_classt::convert( { class_type.add_base(base); } - class_typet::componentt base_class_field; + java_class_typet::componentt base_class_field; base_class_field.type() = class_type.bases().at(0).type(); base_class_field.set_name("@" + id2string(c.super_class)); base_class_field.set_base_name("@" + id2string(c.super_class)); @@ -740,10 +740,10 @@ void java_bytecode_convert_classt::convert( } else { - class_typet &class_type=to_class_type(class_symbol.type); + auto &class_type = to_java_class_type(class_symbol.type); class_type.components().emplace_back(); - class_typet::componentt &component=class_type.components().back(); + auto &component = class_type.components().back(); component.set_name(f.name); component.set_base_name(f.name); @@ -798,18 +798,18 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) class_type.set_name(struct_tag_type_identifier); class_type.components().reserve(3); - class_typet::componentt base_class_component( + java_class_typet::componentt base_class_component( "@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); - class_typet::componentt length_component("length", java_int_type()); + java_class_typet::componentt length_component("length", java_int_type()); length_component.set_pretty_name("length"); length_component.set_base_name("length"); class_type.components().push_back(length_component); - class_typet::componentt data_component( + java_class_typet::componentt data_component( "data", java_reference_type(java_type_from_char(l))); data_component.set_pretty_name("data"); data_component.set_base_name("data"); diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index da84fe35975..31f286026f6 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -332,7 +332,7 @@ static void infer_opaque_type_fields( symbolt &writable_class_symbol = symbol_table.get_writeable_ref(class_symbol_id); auto &components = - to_struct_type(writable_class_symbol.type).components(); + to_java_class_type(writable_class_symbol.type).components(); components.emplace_back(component_name, fieldref.type()); components.back().set_base_name(component_name); components.back().set_pretty_name(component_name); diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 7b39f917c3b..b738f9fdd16 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -101,7 +101,60 @@ inline bool can_cast_type(const typet &) class java_class_typet:public class_typet { - public: +public: + class componentt : public class_typet::componentt + { + public: + componentt() = default; + + componentt(const irep_idt &_name, typet _type) + : class_typet::componentt(_name, std::move(_type)) + { + } + + /// is a method or field 'final'? + bool get_is_final() const + { + return get_bool(ID_final); + } + + /// is a method or field 'final'? + void set_is_final(const bool is_final) + { + set(ID_final, is_final); + } + + /// is a method 'native'? + bool get_is_native() const + { + return get_bool(ID_is_native_method); + } + + /// marks a method as 'native' + void set_is_native(const bool is_native) + { + set(ID_is_native_method, is_native); + } + }; + + using componentst = std::vector; + + const componentst &components() const + { + return (const componentst &)(find(ID_components).get_sub()); + } + + componentst &components() + { + return (componentst &)(add(ID_components).get_sub()); + } + + const componentt &get_component(const irep_idt &component_name) const + { + return static_cast( + class_typet::get_component(component_name)); + } + const irep_idt &get_access() const { return get(ID_access); diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 893cfb8dc7b..9c8e682fa8b 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -30,11 +30,30 @@ pointer_typet require_type::require_pointer( return pointer; } +/// Checks that a class has a component with a specific name +/// \param java_class_type: The class that should have the component +/// \param component_name: The name of the component +/// \return The component with the specified name +java_class_typet::componentt require_type::require_component( + const java_class_typet &java_class_type, + const irep_idt &component_name) +{ + const auto &component = std::find_if( + java_class_type.components().begin(), + java_class_type.components().end(), + [&component_name](const java_class_typet::componentt &component) { + return component.get_name() == component_name; + }); + + REQUIRE(component != java_class_type.components().end()); + return *component; +} + /// Checks a struct like type has a component with a specific name /// \param struct_type: The structure that should have the component /// \param component_name: The name of the component /// \return The component with the specified name -struct_union_typet::componentt require_type::require_component( +struct_typet::componentt require_type::require_component( const struct_typet &struct_type, const irep_idt &component_name) { diff --git a/jbmc/unit/java-testing-utils/require_type.h b/jbmc/unit/java-testing-utils/require_type.h index 14ae5c47f7b..d0d8912453f 100644 --- a/jbmc/unit/java-testing-utils/require_type.h +++ b/jbmc/unit/java-testing-utils/require_type.h @@ -32,6 +32,10 @@ const pointer_typet require_pointer_to_tag( const typet &type, const irep_idt &identifier = irep_idt()); +java_class_typet::componentt require_component( + const java_class_typet &java_class_type, + const irep_idt &component_name); + struct_typet::componentt require_component( const struct_typet &struct_type, const irep_idt &component_name); diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp index 1b9f7d8c9b6..ada4c440109 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp @@ -36,9 +36,9 @@ SCENARIO( { const symbolt &opaque_class_symbol = symbol_table.lookup_ref(opaque_class_prefix); - const struct_typet &opaque_class_struct = - to_struct_type(opaque_class_symbol.type); - const struct_union_typet::componentt &field = + const auto &opaque_class_struct = + to_java_class_type(opaque_class_symbol.type); + const auto &field = require_type::require_component(opaque_class_struct, "field2"); REQUIRE(field.get_is_final()); } diff --git a/src/util/std_types.h b/src/util/std_types.h index 85390988cc3..93210340ed5 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -123,16 +123,6 @@ class struct_union_typet:public typet { return set(ID_C_is_padding, is_padding); } - - bool get_is_final() const - { - return get_bool(ID_final); - } - - void set_is_final(const bool is_final) - { - set(ID_final, is_final); - } }; typedef std::vector componentst;