JCI: don't load method instructions

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -32,9 +32,10 @@ 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();
+    populate_bytecode_mnemonics_table();
   }
 
   virtual bool parse();
@@ -78,6 +79,7 @@ class java_bytecode_parsert:public parsert
   };
 
   std::vector<bytecodet> bytecodes;
+  const bool skip_instructions = false;
 
   pool_entryt &pool_entry(u2 index)
   {
@@ -101,8 +103,13 @@ class java_bytecode_parsert:public parsert
     return java_type_from_string(id2string(pool_entry(index).s));
   }
 
-  void get_bytecodes()
+  void populate_bytecode_mnemonics_table()
   {
+    // This is only useful for rbytecodes, which in turn is only useful to
+    // parse method instructions.
+    if(skip_instructions)
+      return;
+
     // pre-hash the mnemonics, so we do this only once
     bytecodes.resize(256);
     for(const bytecode_infot *p=bytecode_info; p->mnemonic!=nullptr; p++)
@@ -951,6 +958,9 @@ void java_bytecode_parsert::rfields(classt &parsed_class)
 void java_bytecode_parsert::rbytecode(
   methodt::instructionst &instructions)
 {
+  INVARIANT(
+    bytecodes.size() == 256, "bytecode mnemonics should have been populated");
+
   u4 code_length=read_u4();
 
   u4 address;
@@ -1215,7 +1225,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 +1871,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 +1891,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 +1906,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: handles 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 optionalt 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: handles 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 optionalt 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/Annotation.java

@@ -0,0 +1 @@
+public @interface Annotation { }

jbmc/unit/java_bytecode/java_bytecode_parser/Trivial.java

@@ -0,0 +1,10 @@
+public class Trivial {
+  @Annotation
+  public class Inner {
+    @Annotation
+    private int x;
+    public Inner() { x = 1; }
+    @Annotation
+    public void f() { x++; };
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp

@@ -0,0 +1,105 @@
+/*******************************************************************\
+
+ 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 <testing-utils/message.h>
+#include <util/message.h>
+
+#include <testing-utils/catch.hpp>
+
+static void check_class_structure(
+  const java_bytecode_parse_treet::classt &loaded_class)
+{
+  REQUIRE(loaded_class.methods.size() == 2);
+  REQUIRE(loaded_class.is_public);
+  REQUIRE(loaded_class.annotations.size() == 1);
+  REQUIRE(loaded_class.fields.size() == 2);
+  REQUIRE(loaded_class.super_class == "java.lang.Object");
+  REQUIRE(loaded_class.is_inner_class);
+  REQUIRE(loaded_class.outer_class == "Trivial");
+
+  const auto &fieldone = *loaded_class.fields.begin();
+  const auto &fieldtwo = *std::next(loaded_class.fields.begin());
+  const auto &field_x = fieldone.name == "x" ? fieldone : fieldtwo;
+  REQUIRE(field_x.name == "x");
+  REQUIRE(field_x.is_private);
+  REQUIRE(field_x.annotations.size() == 1);
+
+  const auto &methodone = *loaded_class.methods.begin();
+  const auto &methodtwo = *std::next(loaded_class.methods.begin());
+  const auto &method_f =
+    methodone.name == "f" ? methodone : methodtwo;
+  const auto &method_constructor =
+    methodone.name == "f" ? methodtwo : methodone;
+
+  REQUIRE(method_f.is_public);
+  REQUIRE(method_f.annotations.size() == 1);
+  REQUIRE(method_constructor.is_public);
+  REQUIRE(method_constructor.annotations.size() == 0);
+}
+
+SCENARIO(
+  "java_bytecode_parse_class_without_instructions",
+  "[core][java_bytecode][java_bytecode_parser]")
+{
+  WHEN("Loading a class without instructions")
+  {
+    auto loaded =
+      java_bytecode_parse(
+        "./java_bytecode/java_bytecode_parser/Trivial$Inner.class",
+        null_message_handler,
+        true);
+    THEN("Loading should succeed")
+    {
+      REQUIRE(loaded);
+      const auto &loaded_class = loaded->parsed_class;
+
+      THEN("It should have the expected structure")
+      {
+        check_class_structure(loaded_class);
+        const auto &methodone = *loaded_class.methods.begin();
+        const auto &methodtwo = *std::next(loaded_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$Inner.class",
+        null_message_handler,
+        false);
+    THEN("Loading should succeed")
+    {
+      REQUIRE(loaded);
+      const auto &loaded_class = loaded->parsed_class;
+
+      THEN("It should have the expected structure")
+      {
+        check_class_structure(loaded_class);
+        const auto &methodone = *loaded_class.methods.begin();
+        const auto &methodtwo = *std::next(loaded_class.methods.begin());
+
+        THEN("Both methods should have instructions")
+        {
+          REQUIRE(methodone.instructions.size() != 0);
+          REQUIRE(methodtwo.instructions.size() != 0);
+        }
+      }
+    }
+  }
+}