Remove java_bytecode_parse_treet::classt::swap and return using optionalt instead.

jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -18,28 +18,6 @@ Author: Daniel Kroening, [email protected]
 
 #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);

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -22,6 +22,16 @@ Author: Daniel Kroening, [email protected]
 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;
 

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1688,26 +1688,25 @@ 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<class java_bytecode_parse_treet>
+java_bytecode_parse(std::istream &istream, message_handlert &message_handler)
 {
   java_bytecode_parsert java_bytecode_parser;
   java_bytecode_parser.in=&istream;
   java_bytecode_parser.set_message_handler(message_handler);
 
   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<class java_bytecode_parse_treet>
+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

jbmc/src/java_bytecode/java_bytecode_parser.h

@@ -12,15 +12,12 @@ Author: Daniel Kroening, [email protected]
 
 #include <iosfwd>
 #include <string>
+#include <util/optional.h>
 
-bool java_bytecode_parse(
-  const std::string &file,
-  class java_bytecode_parse_treet &,
-  class message_handlert &);
+optionalt<class java_bytecode_parse_treet>
+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<class java_bytecode_parse_treet>
+java_bytecode_parse(std::istream &, class message_handlert &);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSER_H

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -97,11 +97,8 @@ optionalt<java_bytecode_parse_treet> 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<java_bytecode_parse_treet> 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<java_bytecode_parse_treet> 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<java_bytecode_parse_treet> 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<java_bytecode_parse_treet> parse_tree =
+          java_bytecode_parse(full_path, get_message_handler());
+        if(parse_tree)
+          parse_trees.emplace_back(std::move(*parse_tree));
       }
     }
   }

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<java_bytecode_parse_treet> 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<java_bytecode_parse_treet> 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<java_bytecode_parse_treet> 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<java_bytecode_parse_treet> 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);