JCI: don't load method instructions

This speeds loading 40000 classes up by around 3x.

Author: smowton

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -32,9 +32,11 @@ Author: Daniel Kroening, kroening@kroening.com
 class java_bytecode_parsert:public parsert
 {
 public:
-  java_bytecode_parsert()
+  explicit java_bytecode_parsert(bool skip_instructions)
+    : skip_instructions(skip_instructions)
   {
-    get_bytecodes();
+    if(!skip_instructions)
+      get_bytecodes();
   }
 
   virtual bool parse();
@@ -78,6 +80,7 @@ class java_bytecode_parsert:public parsert
   };
 
   std::vector<bytecodet> bytecodes;
+  bool skip_instructions = false;
 
   pool_entryt &pool_entry(u2 index)
   {
@@ -1215,7 +1218,7 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
 
   irep_idt attribute_name=pool_entry(attribute_name_index).s;
 
-  if(attribute_name=="Code")
+  if(attribute_name=="Code" && !skip_instructions)
   {
     UNUSED_u2(max_stack);
     UNUSED_u2(max_locals);
@@ -1861,9 +1864,12 @@ void java_bytecode_parsert::rmethod(classt &parsed_class)
 }
 
 optionalt<java_bytecode_parse_treet>
-java_bytecode_parse(std::istream &istream, message_handlert &message_handler)
+java_bytecode_parse(
+  std::istream &istream,
+  message_handlert &message_handler,
+  bool skip_instructions)
 {
-  java_bytecode_parsert java_bytecode_parser;
+  java_bytecode_parsert java_bytecode_parser(skip_instructions);
   java_bytecode_parser.in=&istream;
   java_bytecode_parser.set_message_handler(message_handler);
 
@@ -1878,7 +1884,10 @@ java_bytecode_parse(std::istream &istream, message_handlert &message_handler)
 }
 
 optionalt<java_bytecode_parse_treet>
-java_bytecode_parse(const std::string &file, message_handlert &message_handler)
+java_bytecode_parse(
+  const std::string &file,
+  message_handlert &message_handler,
+  bool skip_instructions)
 {
   std::ifstream in(file, std::ios::binary);
 
@@ -1890,7 +1899,7 @@ java_bytecode_parse(const std::string &file, message_handlert &message_handler)
     return {};
   }
 
-  return java_bytecode_parse(in, message_handler);
+  return java_bytecode_parse(in, message_handler, skip_instructions);
 }
 
 /// Parses the local variable type table of a method. The LVTT holds generic

jbmc/src/java_bytecode/java_bytecode_parser.h

@@ -16,10 +16,28 @@ Author: Daniel Kroening, kroening@kroening.com
 
 struct java_bytecode_parse_treet;
 
+/// Attempt to parse a Java class from the given file.
+/// \param file: file to load from
+/// \param msg: gets log messages
+/// \param skip_instructions: if true, the loaded class's methods will all be
+///   empty. Saves time and memory for consumers that only want signature info.
+/// \return parse tree, or Empty on failure
 optionalt<java_bytecode_parse_treet>
-java_bytecode_parse(const std::string &file, class message_handlert &);
-
+java_bytecode_parse(
+  const std::string &file,
+  class message_handlert &msg,
+  bool skip_instructions = false);
+
+/// Attempt to parse a Java class from the given stream
+/// \param stream: stream to load from
+/// \param msg: gets log messages
+/// \param skip_instructions: if true, the loaded class's methods will all be
+///   empty. Saves time and memory for consumers that only want signature info.
+/// \return parse tree, or Empty on failure
 optionalt<java_bytecode_parse_treet>
-java_bytecode_parse(std::istream &, class message_handlert &);
+java_bytecode_parse(
+  std::istream &stream,
+  class message_handlert &msg,
+  bool skip_instructions = false);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSER_H

jbmc/unit/Makefile

@@ -36,6 +36,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_lvtt_generic_local_vars.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
+       java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp \
        java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \
        java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \
        java_bytecode/java_bytecode_parser/parse_java_class.cpp \

jbmc/unit/java_bytecode/java_bytecode_parser/Trivial.class

@@ -0,0 +1,7 @@
+public class Trivial {
+
+  int x;
+  public Trivial() { x = 1; }
+  public void f() { x++; };
+
+}

jbmc/unit/java_bytecode/java_bytecode_parser/Trivial.java

@@ -0,0 +1,75 @@
+/*******************************************************************\
+
+ Module: Unit tests to parse a class without its methods' instructions
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <java-testing-utils/load_java_class.h>
+#include <java_bytecode/java_bytecode_parse_tree.h>
+#include <java_bytecode/java_bytecode_parser.h>
+#include <util/message.h>
+
+#include <testing-utils/catch.hpp>
+
+SCENARIO(
+  "java_bytecode_parse_class_without_instructions",
+  "[core][java_bytecode][java_bytecode_parser]")
+{
+  null_message_handlert null_out;
+
+  WHEN("Loading a class without instructions")
+  {
+    auto loaded =
+      java_bytecode_parse(
+        "./java_bytecode/java_bytecode_parser/Trivial.class", null_out, true);
+    THEN("Loading should succeed")
+    {
+      REQUIRE(loaded);
+      const auto &loaded_class = *loaded;
+
+      THEN("It should have two methods")
+      {
+        REQUIRE(loaded_class.parsed_class.methods.size() == 2);
+
+        const auto &methodone = *loaded_class.parsed_class.methods.begin();
+        const auto &methodtwo =
+          *std::next(loaded_class.parsed_class.methods.begin());
+
+        THEN("Neither method should have instructions")
+        {
+          REQUIRE(methodone.instructions.size() == 0);
+          REQUIRE(methodtwo.instructions.size() == 0);
+        }
+      }
+    }
+  }
+
+  WHEN("Loading the same class normally")
+  {
+    auto loaded =
+      java_bytecode_parse(
+        "./java_bytecode/java_bytecode_parser/Trivial.class", null_out, false);
+    THEN("Loading should succeed")
+    {
+      REQUIRE(loaded);
+      const auto &loaded_class = *loaded;
+
+      THEN("It should have two methods")
+      {
+        REQUIRE(loaded_class.parsed_class.methods.size() == 2);
+
+        const auto &methodone = *loaded_class.parsed_class.methods.begin();
+        const auto &methodtwo =
+          *std::next(loaded_class.parsed_class.methods.begin());
+
+        THEN("Both methods should have instructions")
+        {
+          REQUIRE(methodone.instructions.size() != 0);
+          REQUIRE(methodtwo.instructions.size() != 0);
+        }
+      }
+    }
+  }
+}