From 52a669f0e05e3775a716f8627a044764ab5d863b Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 10 May 2018 16:18:28 +0100 Subject: [PATCH 1/4] Remove `java_bytecode::swap` and return using `optionalt` instead. This removes the `swap` method as suggested in https://github.com/diffblue/cbmc/pull/2011 Avoiding having a `swap`method, makes updates less error prone. --- .../java_bytecode_parse_tree.cpp | 22 ------------ .../java_bytecode/java_bytecode_parse_tree.h | 7 ---- .../java_bytecode/java_bytecode_parser.cpp | 23 ++++++------ jbmc/src/java_bytecode/java_bytecode_parser.h | 13 +++---- jbmc/src/java_bytecode/java_class_loader.cpp | 12 +++---- ...ava_bytecode_parse_lambda_method_table.cpp | 36 +++++++++---------- 6 files changed, 37 insertions(+), 76 deletions(-) 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); From c5cbcecd19cff8e8c43f401e0a92a73a0902dda4 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 24 May 2018 19:03:10 +0100 Subject: [PATCH 2/4] Fix instances where copying was being used instead of moving. --- jbmc/src/java_bytecode/java_bytecode_parser.cpp | 2 +- jbmc/src/java_bytecode/java_class_loader.cpp | 6 +++--- .../java_bytecode_parse_lambda_method_table.cpp | 8 ++++---- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 618b8727e4c..18fb937234a 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1702,7 +1702,7 @@ java_bytecode_parse(std::istream &istream, message_handlert &message_handler) return {}; } - return java_bytecode_parser.parse_tree; + return std::move(java_bytecode_parser.parse_tree); } optionalt diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 39e83c6e663..bf775331bd5 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -133,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.push_back(std::move(*parse_tree)); } // Then add core models @@ -153,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.push_back(std::move(*parse_tree)); } } @@ -168,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.push_back(std::move(*parse_tree)); } else { 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 dae1e5362f4..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 @@ -41,7 +41,7 @@ SCENARIO( { REQUIRE(parse_tree); REQUIRE(parse_tree->loading_successful); - const java_bytecode_parse_treet::classt parsed_class = + 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); @@ -352,7 +352,7 @@ SCENARIO( { REQUIRE(parse_tree); REQUIRE(parse_tree->loading_successful); - const java_bytecode_parse_treet::classt parsed_class = + 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); @@ -661,7 +661,7 @@ SCENARIO( { REQUIRE(parse_tree); REQUIRE(parse_tree->loading_successful); - const java_bytecode_parse_treet::classt parsed_class = + 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); @@ -996,7 +996,7 @@ SCENARIO( { REQUIRE(parse_tree); REQUIRE(parse_tree->loading_successful); - const java_bytecode_parse_treet::classt parsed_class = + 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); From f154840d3a95ec13ec9f37053a6e10856b28ad79 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 24 May 2018 19:00:21 +0100 Subject: [PATCH 3/4] Delete copy constructor of `class java_bytecode_parse_treet`. This deletes the default copy constructor of `java_bytecode_parse_treet`, but allows move construction. This enforces allowing move semantics only and prevents accidental copying. --- .../java_bytecode/java_bytecode_parse_tree.h | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index 2086989c920..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; From eeb732f667e9044e3bdda86fedf077f5c165bacb Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 24 May 2018 19:09:26 +0100 Subject: [PATCH 4/4] Switch `push_back` to `emplace_back` when constructing `parse_trees`. --- jbmc/src/java_bytecode/java_class_loader.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index bf775331bd5..2541e4eeb76 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -133,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(std::move(*parse_tree)); + parse_trees.emplace_back(std::move(*parse_tree)); } // Then add core models @@ -153,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(std::move(*parse_tree)); + parse_trees.emplace_back(std::move(*parse_tree)); } } @@ -168,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(std::move(*parse_tree)); + parse_trees.emplace_back(std::move(*parse_tree)); } else { @@ -192,7 +192,7 @@ java_class_loadert::get_parse_tree( optionalt parse_tree = java_bytecode_parse(full_path, get_message_handler()); if(parse_tree) - parse_trees.push_back(std::move(*parse_tree)); + parse_trees.emplace_back(std::move(*parse_tree)); } } }