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..7d5adcff2d0 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -22,6 +22,16 @@ Author: Daniel Kroening, kroening@kroening.com class java_bytecode_parse_treet { public: + // Disallow copy construction and copy assignment, but allow move construction + // and move assignment. + #ifndef _MSC_VER // Ommit this on MS VC2013 as move is not supported. + java_bytecode_parse_treet(const java_bytecode_parse_treet &) = delete; + java_bytecode_parse_treet & + operator=(const java_bytecode_parse_treet &) = delete; + java_bytecode_parse_treet(java_bytecode_parse_treet &&) = default; + java_bytecode_parse_treet &operator=(java_bytecode_parse_treet &&) = default; + #endif + virtual ~java_bytecode_parse_treet() = default; class annotationt { @@ -178,6 +188,17 @@ class java_bytecode_parse_treet class classt { public: + classt() = default; + + // Disallow copy construction and copy assignment, but allow move + // construction and move assignment. + #ifndef _MSC_VER // Ommit this on MS VC2013 as move is not supported. + classt(const classt &) = delete; + classt &operator=(const classt &) = delete; + classt(classt &&) = default; + classt &operator=(classt &&) = default; + #endif + irep_idt name, extends; bool is_abstract=false; bool is_enum=false; @@ -261,17 +282,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..18fb937234a 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 std::move(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..2541e4eeb76 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) @@ -136,7 +133,7 @@ java_class_loadert::get_parse_tree( optionalt parse_tree = get_class_from_jar(class_name, jar_file, *index, class_loader_limit); if(parse_tree) - parse_trees.push_back(*parse_tree); + parse_trees.emplace_back(std::move(*parse_tree)); } // Then add core models @@ -156,7 +153,7 @@ java_class_loadert::get_parse_tree( optionalt parse_tree = get_class_from_jar(class_name, core_models, *index, class_loader_limit); if(parse_tree) - parse_trees.push_back(*parse_tree); + parse_trees.emplace_back(std::move(*parse_tree)); } } @@ -171,7 +168,7 @@ java_class_loadert::get_parse_tree( optionalt parse_tree = get_class_from_jar(class_name, cp_entry, *index, class_loader_limit); if(parse_tree) - parse_trees.push_back(*parse_tree); + parse_trees.emplace_back(std::move(*parse_tree)); } else { @@ -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.emplace_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..ad4fd25a9c8 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); - const java_bytecode_parse_treet::classt parsed_class = - parse_tree.parsed_class; + REQUIRE(parse_tree); + REQUIRE(parse_tree->loading_successful); + const java_bytecode_parse_treet::classt &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); - const java_bytecode_parse_treet::classt parsed_class = - parse_tree.parsed_class; + REQUIRE(parse_tree); + REQUIRE(parse_tree->loading_successful); + const java_bytecode_parse_treet::classt &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); - const java_bytecode_parse_treet::classt parsed_class = - parse_tree.parsed_class; + REQUIRE(parse_tree); + REQUIRE(parse_tree->loading_successful); + const java_bytecode_parse_treet::classt &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); - const java_bytecode_parse_treet::classt parsed_class = - parse_tree.parsed_class; + REQUIRE(parse_tree); + REQUIRE(parse_tree->loading_successful); + const java_bytecode_parse_treet::classt &parsed_class = + parse_tree->parsed_class; REQUIRE(parsed_class.attribute_bootstrapmethods_read); REQUIRE(parsed_class.lambda_method_handle_map.size() == 3);