Merge pull request #1913 from thk123/refactor/lazy-load-java-class-unit-tests

Refactor load java class to allow lazy loading of methods

Author: Thomas Kiley

unit/testing-utils/Makefile

@@ -1,5 +1,6 @@
 SRC = \
   c_to_expr.cpp \
+  free_form_cmdline.cpp \
   load_java_class.cpp \
   require_expr.cpp \
   require_goto_statements.cpp \

unit/testing-utils/free_form_cmdline.cpp

@@ -0,0 +1,35 @@
+/*******************************************************************\
+
+ Module: Unit test utilities
+
+ Author: DiffBlue Limited.
+
+\*******************************************************************/
+
+#include "free_form_cmdline.h"
+
+/// Create a command line option that can be set
+/// \param flag_name: The name of the command line option to support
+void free_form_cmdlinet::create_flag(const std::string &flag_name)
+{
+  optiont option;
+  option.optstring = flag_name;
+  options.push_back(option);
+}
+
+/// Equivalent to specifying --flag for the command line
+/// \param flag: The name of the flag to specify
+void free_form_cmdlinet::add_flag(std::string flag)
+{
+  create_flag(flag);
+  set(flag);
+}
+
+/// Equivalent to specifying --flag value
+/// \param flag: The name of the flag to specify
+/// \param value: The value to the set the command line option to
+void free_form_cmdlinet::add_option(std::string flag, std::string value)
+{
+  create_flag(flag);
+  set(flag, value);
+}

unit/testing-utils/free_form_cmdline.h

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+ Module: Unit test utilities
+
+ Author: DiffBlue Limited.
+
+\*******************************************************************/
+
+#ifndef CPROVER_TESTING_UTILS_FREE_FORM_CMDLINE_H
+#define CPROVER_TESTING_UTILS_FREE_FORM_CMDLINE_H
+
+#include <util/cmdline.h>
+
+/// An implementation of cmdlinet to be used in tests. It does not require
+/// specifying exactly what flags are supported and instead allows setting any
+/// flag
+class free_form_cmdlinet : public cmdlinet
+{
+public:
+  void add_flag(std::string flag);
+  void add_option(std::string flag, std::string value);
+
+private:
+  void create_flag(const std::string &flag_name);
+};
+
+#endif // CPROVER_TESTING_UTILS_FREE_FORM_CMDLINE_H

unit/testing-utils/load_java_class.cpp

@@ -7,17 +7,43 @@
 \*******************************************************************/
 
 #include "load_java_class.h"
+#include "free_form_cmdline.h"
 #include <testing-utils/catch.hpp>
 #include <iostream>
 
 #include <util/config.h>
-#include <util/options.h>
 #include <util/suffix.h>
 
 #include <goto-programs/lazy_goto_model.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 
+/// Go through the process of loading, type-checking and finalising loading a
+/// specific class file to build the symbol table. The functions are converted
+/// using ci_lazy_methods (equivalent to passing --lazy-methods to JBMC)
+/// \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.
+/// \param main: The name of the main function or "" to use the default
+///   behaviour to find a main function.
+/// \return The symbol table that is generated by parsing this file.
+symbol_tablet load_java_class_lazy(
+  const std::string &java_class_name,
+  const std::string &class_path,
+  const std::string &main)
+{
+  free_form_cmdlinet lazy_command_line;
+  lazy_command_line.add_flag("lazy-methods");
+
+  return load_java_class(
+    java_class_name,
+    class_path,
+    main,
+    new_java_bytecode_language(),
+    lazy_command_line);
+}
+
 /// Go through the process of loading, type-checking 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
@@ -51,7 +77,8 @@ symbol_tablet load_java_class(
   const std::string &java_class_name,
   const std::string &class_path,
   const std::string &main,
-  std::unique_ptr<languaget> &&java_lang)
+  std::unique_ptr<languaget> &&java_lang,
+  const cmdlinet &command_line)
 {
   // We expect the name of the class without the .class suffix to allow us to
   // check it
@@ -66,8 +93,6 @@ symbol_tablet load_java_class(
     message_handler);
 
   // 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);
   config.main = main;
@@ -109,3 +134,19 @@ symbol_tablet load_java_class(
   REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class));
   return std::move(maybe_goto_model->symbol_table);
 }
+
+symbol_tablet load_java_class(
+  const std::string &java_class_name,
+  const std::string &class_path,
+  const std::string &main,
+  std::unique_ptr<languaget> &&java_lang)
+{
+  cmdlinet command_line;
+  // TODO(tkiley): This doesn't do anything as "java-cp-include-files" is an
+  // TODO(tkiley): unknown argument. This could be changed by using the
+  // TODO(tkiley): free_form_cmdlinet however this causes some tests to fail.
+  // TODO(tkiley): TG-2708 to investigate and fix
+  command_line.set("java-cp-include-files", class_path);
+  return load_java_class(
+    java_class_name, class_path, main, std::move(java_lang), command_line);
+}

unit/testing-utils/load_java_class.h

@@ -18,6 +18,7 @@
 #include <goto-programs/goto_model.h>
 
 #include <langapi/language.h>
+#include <util/cmdline.h>
 
 symbol_tablet load_java_class(
   const std::string &java_class_name,
@@ -30,4 +31,16 @@ symbol_tablet load_java_class(
   const std::string &main,
   std::unique_ptr<languaget> &&java_lang);
 
+symbol_tablet load_java_class(
+  const std::string &java_class_name,
+  const std::string &class_path,
+  const std::string &main,
+  std::unique_ptr<languaget> &&java_lang,
+  const cmdlinet &command_line);
+
+symbol_tablet load_java_class_lazy(
+  const std::string &java_class_name,
+  const std::string &class_path,
+  const std::string &main);
+
 #endif // CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H