diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp index 08eebadcb8e..673ed6d22d2 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp @@ -18,28 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr2java.h" -void java_bytecode_parse_treet::classt::swap( - classt &other) -{ - other.name.swap(name); - other.extends.swap(extends); - std::swap(other.is_enum, is_enum); - std::swap(other.enum_elements, enum_elements); - std::swap(other.is_abstract, is_abstract); - std::swap(other.is_public, is_public); - std::swap(other.is_protected, is_protected); - std::swap(other.is_private, is_private); - std::swap(other.is_final, is_final); - std::swap(other.signature, signature); - other.implements.swap(implements); - other.fields.swap(fields); - other.methods.swap(methods); - other.annotations.swap(annotations); - std::swap( - other.attribute_bootstrapmethods_read, attribute_bootstrapmethods_read); - std::swap(other.lambda_method_handle_map, lambda_method_handle_map); -} - void java_bytecode_parse_treet::output(std::ostream &out) const { parsed_class.output(out); diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index 829856c5b0b..2086989c920 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -261,17 +261,10 @@ class java_bytecode_parse_treet void output(std::ostream &out) const; - void swap(classt &other); }; classt parsed_class; - void swap(java_bytecode_parse_treet &other) - { - other.parsed_class.swap(parsed_class); - other.class_refs.swap(class_refs); - std::swap(loading_successful, other.loading_successful); - } void output(std::ostream &out) const; diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index db44f7c5b74..618b8727e4c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1688,10 +1688,8 @@ void java_bytecode_parsert::rmethod(classt &parsed_class) rmethod_attribute(method); } -bool java_bytecode_parse( - std::istream &istream, - java_bytecode_parse_treet &parse_tree, - message_handlert &message_handler) +optionalt +java_bytecode_parse(std::istream &istream, message_handlert &message_handler) { java_bytecode_parsert java_bytecode_parser; java_bytecode_parser.in=&istream; @@ -1699,15 +1697,16 @@ bool java_bytecode_parse( bool parser_result=java_bytecode_parser.parse(); - parse_tree.swap(java_bytecode_parser.parse_tree); + if(parser_result) + { + return {}; + } - return parser_result; + return java_bytecode_parser.parse_tree; } -bool java_bytecode_parse( - const std::string &file, - java_bytecode_parse_treet &parse_tree, - message_handlert &message_handler) +optionalt +java_bytecode_parse(const std::string &file, message_handlert &message_handler) { std::ifstream in(file, std::ios::binary); @@ -1716,10 +1715,10 @@ bool java_bytecode_parse( messaget message(message_handler); message.error() << "failed to open input file `" << file << '\'' << messaget::eom; - return true; + return {}; } - return java_bytecode_parse(in, parse_tree, message_handler); + return java_bytecode_parse(in, message_handler); } /// Parses the local variable type table of a method. The LVTT holds generic diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.h b/jbmc/src/java_bytecode/java_bytecode_parser.h index e0f19ef2d60..f723f8bf197 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.h +++ b/jbmc/src/java_bytecode/java_bytecode_parser.h @@ -12,15 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include -bool java_bytecode_parse( - const std::string &file, - class java_bytecode_parse_treet &, - class message_handlert &); +optionalt +java_bytecode_parse(const std::string &file, class message_handlert &); -bool java_bytecode_parse( - std::istream &, - class java_bytecode_parse_treet &, - class message_handlert &); +optionalt +java_bytecode_parse(std::istream &, class message_handlert &); #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSER_H diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index ca9c14f8062..39e83c6e663 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -97,11 +97,8 @@ optionalt java_class_loadert::get_class_from_jar( if(!data.has_value()) return {}; - java_bytecode_parse_treet parse_tree; std::istringstream istream(*data); - if(java_bytecode_parse(istream, parse_tree, get_message_handler())) - return {}; - return parse_tree; + return java_bytecode_parse(istream, get_message_handler()); } static bool is_overlay_class(const java_bytecode_parse_treet::classt &c) @@ -192,9 +189,10 @@ java_class_loadert::get_parse_tree( debug() << "Getting class `" << class_name << "' from file " << full_path << eom; - java_bytecode_parse_treet parse_tree; - if(!java_bytecode_parse(full_path, parse_tree, get_message_handler())) - parse_trees.push_back(std::move(parse_tree)); + optionalt parse_tree = + java_bytecode_parse(full_path, get_message_handler()); + if(parse_tree) + parse_trees.push_back(std::move(*parse_tree)); } } } 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 c738dfdf6b5..dae1e5362f4 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 @@ -33,17 +33,16 @@ SCENARIO( GIVEN( "A class with a static lambda variables from " + compiler + " compiler.") { - java_bytecode_parse_treet parse_tree; - java_bytecode_parse( + optionalt parse_tree = java_bytecode_parse( "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + compiler + "_classes/StaticLambdas.class", - parse_tree, message_handler); WHEN("Parsing that class") { - REQUIRE(parse_tree.loading_successful); + REQUIRE(parse_tree); + REQUIRE(parse_tree->loading_successful); const java_bytecode_parse_treet::classt parsed_class = - parse_tree.parsed_class; + parse_tree->parsed_class; REQUIRE(parsed_class.attribute_bootstrapmethods_read); REQUIRE(parsed_class.lambda_method_handle_map.size() == 12); @@ -345,17 +344,16 @@ SCENARIO( null_message_handlert message_handler; GIVEN("A method with local lambdas from " + compiler + " compiler.") { - java_bytecode_parse_treet parse_tree; - java_bytecode_parse( + optionalt parse_tree = java_bytecode_parse( "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + compiler + "_classes/LocalLambdas.class", - parse_tree, message_handler); WHEN("Parsing that class") { - REQUIRE(parse_tree.loading_successful); + REQUIRE(parse_tree); + REQUIRE(parse_tree->loading_successful); const java_bytecode_parse_treet::classt parsed_class = - parse_tree.parsed_class; + parse_tree->parsed_class; REQUIRE(parsed_class.attribute_bootstrapmethods_read); REQUIRE(parsed_class.lambda_method_handle_map.size() == 12); @@ -655,17 +653,16 @@ SCENARIO( "A class that has lambdas as member variables from " + compiler + " compiler.") { - java_bytecode_parse_treet parse_tree; - java_bytecode_parse( + optionalt parse_tree = java_bytecode_parse( "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + compiler + "_classes/MemberLambdas.class", - parse_tree, message_handler); WHEN("Parsing that class") { - REQUIRE(parse_tree.loading_successful); + REQUIRE(parse_tree); + REQUIRE(parse_tree->loading_successful); const java_bytecode_parse_treet::classt parsed_class = - parse_tree.parsed_class; + parse_tree->parsed_class; REQUIRE(parsed_class.attribute_bootstrapmethods_read); REQUIRE(parsed_class.lambda_method_handle_map.size() == 12); @@ -991,17 +988,16 @@ SCENARIO( "variables from " + compiler + " compiler.") { - java_bytecode_parse_treet parse_tree; - java_bytecode_parse( + optionalt parse_tree = java_bytecode_parse( "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + compiler + "_classes/OuterMemberLambdas$Inner.class", - parse_tree, message_handler); WHEN("Parsing that class") { - REQUIRE(parse_tree.loading_successful); + REQUIRE(parse_tree); + REQUIRE(parse_tree->loading_successful); const java_bytecode_parse_treet::classt parsed_class = - parse_tree.parsed_class; + parse_tree->parsed_class; REQUIRE(parsed_class.attribute_bootstrapmethods_read); REQUIRE(parsed_class.lambda_method_handle_map.size() == 3);