Merge pull request #1431 from thk123/feature/java-load-class-utility

Created utility function for loading a class file

Author: Thomas Kiley

unit/Makefile

@@ -3,6 +3,7 @@
 # Source files for test utilities
 SRC = src/expr/require_expr.cpp \
       src/ansi-c/c_to_expr.cpp \
+      src/java_bytecode/load_java_class.cpp \
       unit_tests.cpp \
       catch_example.cpp \
       util/expr_iterator.cpp \

unit/java_bytecode/java_bytecode_convert_class/A.class

@@ -19,7 +19,7 @@ void concreteMethod() {
   }
 }
 
-class Extendor extends A {
+class Extender extends A {
   void method() {
 
   }

unit/java_bytecode/java_bytecode_convert_class/C.class

@@ -15,39 +15,18 @@
 #include <util/language.h>
 #include <util/message.h>
 #include <java_bytecode/java_bytecode_language.h>
+#include <src/java_bytecode/load_java_class.h>
 
 SCENARIO("java_bytecode_convert_abstract_class",
   "[core][java_bytecode][java_bytecode_convert_class]")
 {
-  std::unique_ptr<languaget>java_lang(new_java_bytecode_language());
-
-  // Configure the path loading
-  cmdlinet command_line;
-  command_line.set(
-    "java-cp-include-files",
-    "./java_bytecode/java_bytecode_convert_class");
-  config.java.classpath.push_back(
-    "./java_bytecode/java_bytecode_convert_class");
-
-  // Configure the language
-  null_message_handlert message_handler;
-  java_lang->get_language_options(command_line);
-  java_lang->set_message_handler(message_handler);
-
-  std::istringstream java_code_stream("ignored");
-
   GIVEN("Some class files in the class path")
   {
     WHEN("Parsing an interface")
     {
-      java_lang->parse(java_code_stream, "I.class");
-
-      symbol_tablet new_symbol_table;
-      java_lang->typecheck(new_symbol_table, "");
+      const symbol_tablet &new_symbol_table=
+        load_java_class("I", "./java_bytecode/java_bytecode_convert_class");
 
-      java_lang->final(new_symbol_table);
-
-      REQUIRE(new_symbol_table.has_symbol("java::I"));
       THEN("The symbol type should be abstract")
       {
         const symbolt &class_symbol=new_symbol_table.lookup("java::I");
@@ -61,14 +40,8 @@ SCENARIO("java_bytecode_convert_abstract_class",
     }
     WHEN("Parsing an abstract class")
     {
-      java_lang->parse(java_code_stream, "A.class");
-
-      symbol_tablet new_symbol_table;
-      java_lang->typecheck(new_symbol_table, "");
-
-      java_lang->final(new_symbol_table);
-
-      REQUIRE(new_symbol_table.has_symbol("java::A"));
+      const symbol_tablet &new_symbol_table=
+        load_java_class("A", "./java_bytecode/java_bytecode_convert_class");
       THEN("The symbol type should be abstract")
       {
         const symbolt &class_symbol=new_symbol_table.lookup("java::A");
@@ -82,14 +55,8 @@ SCENARIO("java_bytecode_convert_abstract_class",
     }
     WHEN("Passing a concrete class")
     {
-      java_lang->parse(java_code_stream, "C.class");
-
-      symbol_tablet new_symbol_table;
-      java_lang->typecheck(new_symbol_table, "");
-
-      java_lang->final(new_symbol_table);
-
-      REQUIRE(new_symbol_table.has_symbol("java::C"));
+      const symbol_tablet &new_symbol_table=
+        load_java_class("C", "./java_bytecode/java_bytecode_convert_class");
       THEN("The symbol type should not be abstract")
       {
         const symbolt &class_symbol=new_symbol_table.lookup("java::C");
@@ -103,14 +70,10 @@ SCENARIO("java_bytecode_convert_abstract_class",
     }
     WHEN("Passing a concrete class that implements an interface")
     {
-      java_lang->parse(java_code_stream, "Implementor.class");
-
-      symbol_tablet new_symbol_table;
-      java_lang->typecheck(new_symbol_table, "");
-
-      java_lang->final(new_symbol_table);
-
-      REQUIRE(new_symbol_table.has_symbol("java::Implementor"));
+      const symbol_tablet &new_symbol_table=
+        load_java_class(
+          "Implementor",
+          "./java_bytecode/java_bytecode_convert_class");
       THEN("The symbol type should not be abstract")
       {
         const symbolt &class_symbol=
@@ -125,18 +88,14 @@ SCENARIO("java_bytecode_convert_abstract_class",
     }
     WHEN("Passing a concrete class that extends an abstract class")
     {
-      java_lang->parse(java_code_stream, "Extendor.class");
-
-      symbol_tablet new_symbol_table;
-      java_lang->typecheck(new_symbol_table, "");
-
-      java_lang->final(new_symbol_table);
-
-      REQUIRE(new_symbol_table.has_symbol("java::Extendor"));
+      const symbol_tablet &new_symbol_table=
+        load_java_class(
+          "Extender",
+          "./java_bytecode/java_bytecode_convert_class");
       THEN("The symbol type should not be abstract")
       {
         const symbolt &class_symbol=
-          new_symbol_table.lookup("java::Extendor");
+          new_symbol_table.lookup("java::Extender");
         const typet &symbol_type=class_symbol.type;
 
         REQUIRE(symbol_type.id()==ID_struct);

unit/java_bytecode/java_bytecode_convert_class/ExampleClasses.java

@@ -0,0 +1,67 @@
+/*******************************************************************\
+
+ Module: Unit test utilities
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include "load_java_class.h"
+#include <catch.hpp>
+#include <iostream>
+
+#include <util/config.h>
+#include <util/language.h>
+#include <util/suffix.h>
+
+#include <java_bytecode/java_bytecode_language.h>
+
+/// Go through the process of loading, typechecking and finalising loading a
+/// specific class file to build the symbol table.
+/// \param java_class_name: The name of the class file to load. It should not
+///   include the .class extension.
+/// \param class_path: The path to load the class from. Should be relative to
+///   the unit directory.
+/// \return The symbol table that is generated by parsing this file.
+symbol_tablet load_java_class(
+  const std::string &java_class_name,
+  const std::string &class_path)
+{
+  // We don't expect the .class suffix to allow us to check the name of the
+  // class
+  PRECONDITION(!has_suffix(java_class_name, ".class"));
+
+  // Configure the path loading
+  cmdlinet command_line;
+  command_line.set("java-cp-include-files", class_path);
+  config.java.classpath.clear();
+  config.java.classpath.push_back(class_path);
+
+  symbol_tablet new_symbol_table;
+
+  std::unique_ptr<languaget>java_lang(new_java_bytecode_language());
+
+  std::istringstream java_code_stream("ignored");
+  null_message_handlert message_handler;
+
+  // Configure the language, load the class files
+  java_lang->get_language_options(command_line);
+  java_lang->set_message_handler(message_handler);
+  java_lang->parse(java_code_stream, java_class_name + ".class");
+  java_lang->typecheck(new_symbol_table, "");
+  java_lang->final(new_symbol_table);
+
+  // Verify that the class was loaded
+  const std::string class_symbol_name="java::"+java_class_name;
+  REQUIRE(new_symbol_table.has_symbol(class_symbol_name));
+  const symbolt &class_symbol=new_symbol_table.lookup(class_symbol_name);
+  REQUIRE(class_symbol.is_type);
+  const typet &class_type=class_symbol.type;
+  REQUIRE(class_type.id()==ID_struct);
+
+  // if this fails it indicates the class was not loaded
+  // Check your working directory and the class path is correctly configured
+  // as this often indicates that one of these is wrong.
+  REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class));
+  return new_symbol_table;
+}

unit/java_bytecode/java_bytecode_convert_class/Extender.class

@@ -0,0 +1,22 @@
+/*******************************************************************\
+
+ Module: Unit test utilities
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+/// \file
+/// Utility for loading and parsing a specified java class file, returning
+/// the symbol table generated by this.
+
+#ifndef CPROVER_SRC_JAVA_BYTECODE_LOAD_JAVA_CLASS_H
+#define CPROVER_SRC_JAVA_BYTECODE_LOAD_JAVA_CLASS_H
+
+#include <util/symbol_table.h>
+
+symbol_tablet load_java_class(
+  const std::string &java_class_name,
+  const std::string &class_path);
+
+#endif // CPROVER_SRC_JAVA_BYTECODE_LOAD_JAVA_CLASS_H