From 08276ebd9ada0be45a9d3f99b4c02021329572ee Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 25 Jan 2019 12:13:05 +0000 Subject: [PATCH 1/3] Replace use of deprecated nil_typet in java_type_from_string Use optionalt as recommended in the deprecation note. --- .../java_bytecode_convert_class.cpp | 8 ++- .../java_bytecode_convert_method.cpp | 41 ++++++-------- .../java_bytecode/java_bytecode_parser.cpp | 49 ++++++++--------- jbmc/src/java_bytecode/java_entry_point.cpp | 4 +- .../java_local_variable_table.cpp | 4 +- jbmc/src/java_bytecode/java_types.cpp | 53 +++++++++---------- jbmc/src/java_bytecode/java_types.h | 6 +-- .../convert_invoke_dynamic.cpp | 30 +++++------ .../parse_java_annotations.cpp | 6 +-- .../java_types/java_type_from_string.cpp | 10 ++-- 10 files changed, 98 insertions(+), 113 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 6f65546eca1..1c1751e9a01 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -637,10 +637,8 @@ void java_bytecode_convert_classt::convert( typet field_type; if(f.signature.has_value()) { - field_type=java_type_from_string_with_exception( - f.descriptor, - f.signature, - id2string(class_symbol.name)); + field_type = *java_type_from_string_with_exception( + f.descriptor, f.signature, id2string(class_symbol.name)); /// this is for a free type variable, e.g., a field of the form `T f;` if(is_java_generic_parameter(field_type)) @@ -670,7 +668,7 @@ void java_bytecode_convert_classt::convert( } } else - field_type=java_type_from_string(f.descriptor); + field_type = *java_type_from_string(f.descriptor); // is this a static field? if(f.is_static) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 671c702dafc..320ef2c90aa 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -259,21 +259,26 @@ java_method_typet member_type_lazy( messaget message(message_handler); - typet member_type_from_descriptor=java_type_from_string(descriptor); - INVARIANT(member_type_from_descriptor.id()==ID_code, "Must be code type"); + auto member_type_from_descriptor = java_type_from_string(descriptor); + INVARIANT( + member_type_from_descriptor.has_value() && + member_type_from_descriptor->id() == ID_code, + "Must be code type"); if(signature.has_value()) { try { - typet member_type_from_signature=java_type_from_string( - signature.value(), - class_name); - INVARIANT(member_type_from_signature.id()==ID_code, "Must be code type"); + auto member_type_from_signature = + java_type_from_string(signature.value(), class_name); + INVARIANT( + member_type_from_signature.has_value() && + member_type_from_signature->id() == ID_code, + "Must be code type"); if( - to_java_method_type(member_type_from_signature).parameters().size() == - to_java_method_type(member_type_from_descriptor).parameters().size()) + to_java_method_type(*member_type_from_signature).parameters().size() == + to_java_method_type(*member_type_from_descriptor).parameters().size()) { - return to_java_method_type(member_type_from_signature); + return to_java_method_type(*member_type_from_signature); } else { @@ -294,7 +299,7 @@ java_method_typet member_type_lazy( << message.eom; } } - return to_java_method_type(member_type_from_descriptor); + return to_java_method_type(*member_type_from_descriptor); } /// Retrieves the symbol of the lambda method associated with the given @@ -460,24 +465,10 @@ void java_bytecode_convert_methodt::convert( if(!is_parameter(v)) continue; - // Construct a fully qualified name for the parameter v, - // e.g. my.package.ClassName.myMethodName:(II)I::anIntParam, and then a - // symbol_exprt with the parameter and its type - typet t; - if(v.signature.has_value()) - { - t=java_type_from_string_with_exception( - v.descriptor, - v.signature, - id2string(class_symbol.name)); - } - else - t=java_type_from_string(v.descriptor); - std::ostringstream id_oss; id_oss << method_id << "::" << v.name; irep_idt identifier(id_oss.str()); - symbol_exprt result(identifier, t); + symbol_exprt result = symbol_exprt::typeless(identifier); result.set(ID_C_base_name, v.name); // Create a new variablet in the variables vector; in fact this entry will diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index d79e9f43b27..c5ffcd2833f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -100,7 +100,7 @@ class java_bytecode_parsert:public parsert const typet type_entry(u2 index) { - return java_type_from_string(id2string(pool_entry(index).s)); + return *java_type_from_string(id2string(pool_entry(index).s)); } void populate_bytecode_mnemonics_table() @@ -547,10 +547,8 @@ void java_bytecode_parsert::get_class_refs() break; case CONSTANT_NameAndType: - { - typet t=java_type_from_string(id2string(pool_entry(c.ref2).s)); - get_class_refs_rec(t); - } + get_class_refs_rec( + *java_type_from_string(id2string(pool_entry(c.ref2).s))); break; default: {} @@ -562,23 +560,22 @@ void java_bytecode_parsert::get_class_refs() for(const auto &field : parse_tree.parsed_class.fields) { get_annotation_class_refs(field.annotations); - typet field_type; + if(field.signature.has_value()) { - field_type=java_type_from_string_with_exception( + typet field_type = *java_type_from_string_with_exception( field.descriptor, field.signature, - "java::"+id2string(parse_tree.parsed_class.name)); + "java::" + id2string(parse_tree.parsed_class.name)); // add generic type args to class refs as dependencies, same below for // method types and entries from the local variable type table get_dependencies_from_generic_parameters( field_type, parse_tree.class_refs); + get_class_refs_rec(field_type); } - else - field_type=java_type_from_string(field.descriptor); - - get_class_refs_rec(field_type); + else if(const auto field_type = java_type_from_string(field.descriptor)) + get_class_refs_rec(*field_type); } for(const auto &method : parse_tree.parsed_class.methods) @@ -586,35 +583,34 @@ void java_bytecode_parsert::get_class_refs() get_annotation_class_refs(method.annotations); for(const auto ¶meter_annotations : method.parameter_annotations) get_annotation_class_refs(parameter_annotations); - typet method_type; + if(method.signature.has_value()) { - method_type=java_type_from_string_with_exception( + typet method_type = *java_type_from_string_with_exception( method.descriptor, method.signature, - "java::"+id2string(parse_tree.parsed_class.name)); + "java::" + id2string(parse_tree.parsed_class.name)); get_dependencies_from_generic_parameters( method_type, parse_tree.class_refs); + get_class_refs_rec(method_type); } - else - method_type=java_type_from_string(method.descriptor); + else if(const auto method_type = java_type_from_string(method.descriptor)) + get_class_refs_rec(*method_type); - get_class_refs_rec(method_type); for(const auto &var : method.local_variable_table) { - typet var_type; if(var.signature.has_value()) { - var_type=java_type_from_string_with_exception( + typet var_type = *java_type_from_string_with_exception( var.descriptor, var.signature, - "java::"+id2string(parse_tree.parsed_class.name)); + "java::" + id2string(parse_tree.parsed_class.name)); get_dependencies_from_generic_parameters( var_type, parse_tree.class_refs); + get_class_refs_rec(var_type); } - else - var_type=java_type_from_string(var.descriptor); - get_class_refs_rec(var_type); + else if(const auto var_type = java_type_from_string(var.descriptor)) + get_class_refs_rec(*var_type); } } } @@ -672,8 +668,9 @@ void java_bytecode_parsert::get_annotation_value_class_refs(const exprt &value) if(const auto &symbol_expr = expr_try_dynamic_cast(value)) { const irep_idt &value_id = symbol_expr->get_identifier(); - const typet value_type = java_type_from_string(id2string(value_id)); - get_class_refs_rec(value_type); + const auto value_type = java_type_from_string(id2string(value_id)); + if(value_type.has_value()) + get_class_refs_rec(*value_type); } else if(const auto &array_expr = expr_try_dynamic_cast(value)) { diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 6c24b213723..32985f4a0de 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -267,14 +267,14 @@ bool is_java_main(const symbolt &function) { bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD); const java_method_typet &function_type = to_java_method_type(function.type); - const typet &string_array_type = java_type_from_string("[Ljava/lang/String;"); + const auto string_array_type = java_type_from_string("[Ljava/lang/String;"); // checks whether the function is static and has a single String[] parameter bool is_static = !function_type.has_this(); // this should be implied by the signature const java_method_typet::parameterst ¶meters = function_type.parameters(); bool has_correct_type = function_type.return_type().id() == ID_empty && parameters.size() == 1 && - parameters[0].type().full_eq(string_array_type); + parameters[0].type().full_eq(*string_array_type); bool public_access = function_type.get(ID_access) == ID_public; return named_main && is_static && has_correct_type && public_access; } diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp index 406171f13f2..7049c711e25 100644 --- a/jbmc/src/java_bytecode/java_local_variable_table.cpp +++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp @@ -794,9 +794,9 @@ void java_bytecode_convert_methodt::setup_local_variables( const std::string class_name = method_name.substr(0, class_name_end); const typet t = v.var.signature.has_value() - ? java_type_from_string_with_exception( + ? *java_type_from_string_with_exception( v.var.descriptor, v.var.signature, class_name) - : java_type_from_string(v.var.descriptor); + : *java_type_from_string(v.var.descriptor); std::ostringstream id_oss; id_oss << method_id << "::" << v.var.start_pc << "::" << v.var.name; diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index f8d13d84c06..e02142283e2 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -351,9 +351,9 @@ std::vector parse_list_types( for(const std::string &raw_type : parse_raw_list_types(src, opening_bracket, closing_bracket)) { - const typet new_type = java_type_from_string(raw_type, class_name_prefix); - INVARIANT(new_type != nil_typet(), "Failed to parse type"); - type_list.push_back(new_type); + auto new_type = java_type_from_string(raw_type, class_name_prefix); + INVARIANT(new_type.has_value(), "Failed to parse type"); + type_list.push_back(std::move(*new_type)); } return type_list; } @@ -501,12 +501,12 @@ size_t find_closing_semi_colon_for_reference_type( /// \param class_name_prefix: name of class to append to generic type /// variables/parameters /// \return internal type representation for GOTO programs -typet java_type_from_string( +optionalt java_type_from_string( const std::string &src, const std::string &class_name_prefix) { if(src.empty()) - return nil_typet(); + return {}; // a java type is encoded in different ways // - a method type is encoded as '(...)R' where the parenthesis include the @@ -550,15 +550,15 @@ typet java_type_from_string( "Cannot currently parse bounds on generic types"); } - const typet &method_type=java_type_from_string( - src.substr(closing_generic+1, std::string::npos), class_name_prefix); + auto method_type = java_type_from_string( + src.substr(closing_generic + 1, std::string::npos), class_name_prefix); // This invariant being violated means that tkiley has not understood // part of the signature spec. // Only class and method signatures can start with a '<' and classes are // handled separately. INVARIANT( - method_type.id()==ID_code, + method_type.has_value() && method_type->id() == ID_code, "This should correspond to method signatures only"); return method_type; @@ -567,9 +567,9 @@ typet java_type_from_string( { std::size_t e_pos=src.rfind(')'); if(e_pos==std::string::npos) - return nil_typet(); + return {}; - typet return_type = java_type_from_string( + auto return_type = java_type_from_string( std::string(src, e_pos + 1, std::string::npos), class_name_prefix); std::vector param_types = @@ -583,7 +583,7 @@ typet java_type_from_string( std::back_inserter(parameters), [](const typet &type) { return java_method_typet::parametert(type); }); - return java_method_typet(std::move(parameters), std::move(return_type)); + return java_method_typet(std::move(parameters), std::move(*return_type)); } case '[': // array type @@ -591,18 +591,17 @@ typet java_type_from_string( // If this is a reference array, we generate a plain array[reference] // with void* members, but note the real type in ID_element_type. if(src.size()<=1) - return nil_typet(); + return {}; char subtype_letter=src[1]; - const typet subtype= - java_type_from_string(src.substr(1, std::string::npos), - class_name_prefix); + auto subtype = java_type_from_string( + src.substr(1, std::string::npos), class_name_prefix); if(subtype_letter=='L' || // [L denotes a reference array of some sort. subtype_letter=='[' || // Array-of-arrays subtype_letter=='T') // Array of generic types subtype_letter='A'; typet tmp=java_array_type(std::tolower(subtype_letter)); - tmp.subtype().set(ID_element_type, subtype); - return tmp; + tmp.subtype().set(ID_element_type, std::move(*subtype)); + return std::move(tmp); } case 'B': return java_byte_type(); @@ -623,7 +622,7 @@ typet java_type_from_string( return java_generic_parametert( type_var_name, to_struct_tag_type( - java_type_from_string("Ljava/lang/Object;").subtype())); + java_type_from_string("Ljava/lang/Object;")->subtype())); } case 'L': { @@ -639,7 +638,7 @@ typet java_type_from_string( throw unsupported_java_class_signature_exceptiont("wild card generic"); } default: - return nil_typet(); + return {}; } } @@ -724,7 +723,7 @@ std::vector java_generic_type_from_string( java_generic_parametert type_var_type( type_var_name, to_struct_tag_type( - java_type_from_string(bound_type, class_name).subtype())); + java_type_from_string(bound_type, class_name)->subtype())); types.push_back(type_var_type); signature=signature.substr(var_sep+1, std::string::npos); @@ -746,7 +745,7 @@ static std::string slash_to_dot(const std::string &src) struct_tag_typet java_classname(const std::string &id) { if(!id.empty() && id[0]=='[') - return to_struct_tag_type(java_type_from_string(id).subtype()); + return to_struct_tag_type(java_type_from_string(id)->subtype()); std::string class_name=id; @@ -900,9 +899,9 @@ void get_dependencies_from_generic_parameters( // class signature without bounds and without wildcards else if(signature.find('*') == std::string::npos) { - get_dependencies_from_generic_parameters_rec( - java_type_from_string(signature, erase_type_arguments(signature)), - refs); + auto type_from_string = + java_type_from_string(signature, erase_type_arguments(signature)); + get_dependencies_from_generic_parameters_rec(*type_from_string, refs); } } catch(unsupported_java_class_signature_exceptiont &) @@ -940,9 +939,9 @@ java_generic_struct_tag_typet::java_generic_struct_tag_typet( : 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); + const auto 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_struct_tag_type(gen_base_type.subtype()).get_identifier(), diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index c192ff7ce2f..252ad568561 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -380,9 +380,9 @@ bool is_java_array_type(const typet &type); bool is_multidim_java_array_type(const typet &type); typet java_type_from_char(char t); -typet java_type_from_string( +optionalt java_type_from_string( const std::string &, - const std::string &class_name_prefix=""); + const std::string &class_name_prefix = ""); char java_char_from_type(const typet &type); std::vector java_generic_type_from_string( const std::string &, @@ -715,7 +715,7 @@ class unsupported_java_class_signature_exceptiont:public std::logic_error } }; -inline typet java_type_from_string_with_exception( +inline optionalt java_type_from_string_with_exception( const std::string &descriptor, const optionalt &signature, const std::string &class_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 6dbc812870f..bc0846681f2 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 @@ -240,11 +240,11 @@ SCENARIO( symbol_exprt integer_param{"primitive", java_int_type()}; symbol_exprt ref_param{"reference", - java_type_from_string("Ljava/lang/Object;")}; + *java_type_from_string("Ljava/lang/Object;")}; // NOLINTNEXTLINE(whitespace/braces) symbol_exprt generic_param{ "specalisedGeneric", - java_type_from_string("LDummyGeneric;")}; + *java_type_from_string("LDummyGeneric;")}; test_data.expected_params = {integer_param, ref_param, generic_param}; test_data.should_return_value = false; @@ -266,14 +266,14 @@ SCENARIO( "java::LocalLambdas.lambda$test$2:" "[I[Ljava/lang/Object;[LDummyGeneric;)V"; - symbol_exprt integer_param{"primitive", java_type_from_string("[I")}; + symbol_exprt integer_param{"primitive", *java_type_from_string("[I")}; symbol_exprt ref_param{"reference", - java_type_from_string("[Ljava/lang/Object;")}; + *java_type_from_string("[Ljava/lang/Object;")}; // NOLINTNEXTLINE(whitespace/braces) symbol_exprt generic_param{ "specalisedGeneric", - java_type_from_string("[LDummyGeneric;")}; + *java_type_from_string("[LDummyGeneric;")}; test_data.expected_params = {integer_param, ref_param, generic_param}; test_data.should_return_value = false; @@ -428,11 +428,11 @@ SCENARIO( symbol_exprt integer_param{"primitive", java_int_type()}; symbol_exprt ref_param{"reference", // NOLINT(whitespace/braces) - java_type_from_string("Ljava/lang/Object;")}; + *java_type_from_string("Ljava/lang/Object;")}; // NOLINTNEXTLINE(whitespace/braces) symbol_exprt generic_param{ "specalisedGeneric", - java_type_from_string("LDummyGeneric;")}; + *java_type_from_string("LDummyGeneric;")}; test_data.expected_params = {integer_param, ref_param, generic_param}; test_data.should_return_value = false; @@ -451,13 +451,13 @@ SCENARIO( "java::MemberLambdas.lambda$new$2:" "([I[Ljava/lang/Object;[LDummyGeneric;)V"; - symbol_exprt integer_param{"primitive", java_type_from_string("[I")}; + symbol_exprt integer_param{"primitive", *java_type_from_string("[I")}; symbol_exprt ref_param{"reference", // NOLINT(whitespace/braces) - java_type_from_string("[Ljava/lang/Object;")}; + *java_type_from_string("[Ljava/lang/Object;")}; // NOLINTNEXTLINE(whitespace/braces) symbol_exprt generic_param{ "specalisedGeneric", - java_type_from_string("[LDummyGeneric;")}; + *java_type_from_string("[LDummyGeneric;")}; test_data.expected_params = {integer_param, ref_param, generic_param}; test_data.should_return_value = false; @@ -600,11 +600,11 @@ SCENARIO( symbol_exprt integer_param{"primitive", java_int_type()}; symbol_exprt ref_param{"reference", - java_type_from_string("Ljava/lang/Object;")}; + *java_type_from_string("Ljava/lang/Object;")}; // NOLINTNEXTLINE(whitespace/braces) symbol_exprt generic_param{ "specalisedGeneric", - java_type_from_string("LDummyGeneric;")}; + *java_type_from_string("LDummyGeneric;")}; test_data.expected_params = {integer_param, ref_param, generic_param}; test_data.should_return_value = false; @@ -623,13 +623,13 @@ SCENARIO( "java::StaticLambdas.lambda$static$2:" "([I[Ljava/lang/Object;[LDummyGeneric;)V"; - symbol_exprt integer_param{"primitive", java_type_from_string("[I")}; + symbol_exprt integer_param{"primitive", *java_type_from_string("[I")}; symbol_exprt ref_param{"reference", - java_type_from_string("[Ljava/lang/Object;")}; + *java_type_from_string("[Ljava/lang/Object;")}; // NOLINTNEXTLINE(whitespace/braces) symbol_exprt generic_param{ "specalisedGeneric", - java_type_from_string("[LDummyGeneric;")}; + *java_type_from_string("[LDummyGeneric;")}; test_data.expected_params = {integer_param, ref_param, generic_param}; test_data.should_return_value = false; 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 d1ddc46c754..d3a8f56444b 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_struct_tag_type(java_type.subtype()).get_identifier()); + id2string(to_struct_tag_type(java_type->subtype()).get_identifier()); REQUIRE(id2string(class_name) == "java::java.lang.String"); } } @@ -117,7 +117,7 @@ SCENARIO( const auto &id = to_symbol_expr(element_value_pair.value).get_identifier(); const auto &java_type = java_type_from_string(id2string(id)); - REQUIRE(java_type == java_byte_type()); + REQUIRE(*java_type == java_byte_type()); } } WHEN("Parsing an annotation with Class value specified to void") @@ -139,7 +139,7 @@ SCENARIO( const auto &id = to_symbol_expr(element_value_pair.value).get_identifier(); const auto &java_type = java_type_from_string(id2string(id)); - REQUIRE(java_type == void_type()); + REQUIRE(*java_type == void_type()); } } WHEN("Parsing an annotation with an array field.") 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 0ee79226a39..aaf4dc6fb6f 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 @@ -16,33 +16,33 @@ SCENARIO("java_type_from_string", "[core][java_types]") GIVEN("Ljava/lang/Integer;") { const auto integer_type = java_type_from_string("Ljava/lang/Integer;", ""); - REQUIRE(integer_type != nil_typet()); + REQUIRE(integer_type.has_value()); } GIVEN("TE;") { const auto generic_type_E = java_type_from_string("TE;", "MyClass"); - REQUIRE(generic_type_E != nil_typet()); + REQUIRE(generic_type_E.has_value()); } GIVEN("Ljava/util/List;") { const auto generic_list_type = java_type_from_string("Ljava/util/List;", "java.util.List"); - REQUIRE(generic_list_type != nil_typet()); + REQUIRE(generic_list_type.has_value()); } GIVEN("Ljava/util/List;") { const auto integer_list_type = java_type_from_string("Ljava/util/List;", ""); - REQUIRE(integer_list_type != nil_typet()); + REQUIRE(integer_list_type.has_value()); } GIVEN("Ljava/util/Map;") { const auto generic_struct_tag_type = java_type_from_string("Ljava/util/Map;", "java.util.Map"); - REQUIRE(generic_struct_tag_type != nil_typet()); + REQUIRE(generic_struct_tag_type.has_value()); } } From 6f1084e736579cf6968fa9750a57bc9ab49dbe9a Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 31 Jan 2019 13:42:58 +0000 Subject: [PATCH 2/3] Address errors in handcrafted bytecode The jasmin contained two errors: calling base class constructor with invokevirtual rather than invokespecial the descriptor of the type for the local variable was not a valid descriptor. --- .../jbmc/stack_var12/stack_typecast.class | Bin 367 -> 386 bytes .../jbmc/stack_var12/stack_typecast.j | 4 ++-- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/jbmc/regression/jbmc/stack_var12/stack_typecast.class b/jbmc/regression/jbmc/stack_var12/stack_typecast.class index 0d88a2fa4c97f7a4771a8337e3f5e3746f4a3851..47b0d0bcdf0bbcb3efb8ec2280747e97a6d8c578 100644 GIT binary patch delta 219 zcmaFQ)Wpnn>ff$?3=9l<3{n%h92`X$1Q{8aH8jH*8Cab2Q&Jfj1bm815|gvzODYRe zlM{ff$?3=9l<43ZPM9Q1@41Q;2ZH8jH*8Cab2Q&Kq@_!xK?8MuP;ON)|I z-7<4hc^D)Zco`WOJ=qyVCwA*H@=e@nWyinC+oIsu+ zkY)tZtXkU`1UCX1AcbNK{F4nC#jHiNBDXMbMX@AoW#BTdTLYA1Vh{q7Y+x-64B|jG S511{&z|0^D*2@i6#RdRj92iLe diff --git a/jbmc/regression/jbmc/stack_var12/stack_typecast.j b/jbmc/regression/jbmc/stack_var12/stack_typecast.j index 011f8a018e8..fb773bfd89b 100644 --- a/jbmc/regression/jbmc/stack_var12/stack_typecast.j +++ b/jbmc/regression/jbmc/stack_var12/stack_typecast.j @@ -6,14 +6,14 @@ .method public ()V aload_0 - invokevirtual java/lang/Object/()V + invokespecial java/lang/Object/()V return .end method .method public f()I .limit stack 6 .limit locals 1 - .var 0 is this stack_typecast from begin to end + .var 0 is this Lstack_typecast; from begin to end .line 0 begin: From 8f71a23c0ba06cedd82e49bcd84a9925352e4ac8 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 31 Jan 2019 13:44:44 +0000 Subject: [PATCH 3/3] Do not allow getting type from descriptor to fail There should be no unsupported cases here. --- .../java_bytecode/java_bytecode_parser.cpp | 22 +++++++++++-------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index c5ffcd2833f..13b3623a52c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -574,8 +574,10 @@ void java_bytecode_parsert::get_class_refs() field_type, parse_tree.class_refs); get_class_refs_rec(field_type); } - else if(const auto field_type = java_type_from_string(field.descriptor)) - get_class_refs_rec(*field_type); + else + { + get_class_refs_rec(*java_type_from_string(field.descriptor)); + } } for(const auto &method : parse_tree.parsed_class.methods) @@ -594,8 +596,10 @@ void java_bytecode_parsert::get_class_refs() method_type, parse_tree.class_refs); get_class_refs_rec(method_type); } - else if(const auto method_type = java_type_from_string(method.descriptor)) - get_class_refs_rec(*method_type); + else + { + get_class_refs_rec(*java_type_from_string(method.descriptor)); + } for(const auto &var : method.local_variable_table) { @@ -609,8 +613,10 @@ void java_bytecode_parsert::get_class_refs() var_type, parse_tree.class_refs); get_class_refs_rec(var_type); } - else if(const auto var_type = java_type_from_string(var.descriptor)) - get_class_refs_rec(*var_type); + else + { + get_class_refs_rec(*java_type_from_string(var.descriptor)); + } } } } @@ -668,9 +674,7 @@ void java_bytecode_parsert::get_annotation_value_class_refs(const exprt &value) if(const auto &symbol_expr = expr_try_dynamic_cast(value)) { const irep_idt &value_id = symbol_expr->get_identifier(); - const auto value_type = java_type_from_string(id2string(value_id)); - if(value_type.has_value()) - get_class_refs_rec(*value_type); + get_class_refs_rec(*java_type_from_string(id2string(value_id))); } else if(const auto &array_expr = expr_try_dynamic_cast(value)) {