Add --java-load-containing-class-only option

Add option to only load the class (and inner classes) that contain the
method under test.

Author: Joel Allred

jbmc/regression/jbmc/load-containing-class-only/External.class

@@ -0,0 +1,8 @@
+class External {
+
+  public static int get() {
+    assert(false);
+    return 40;
+  }
+
+}

jbmc/regression/jbmc/load-containing-class-only/External.java

@@ -0,0 +1,7 @@
+class Test {
+
+  public static int test() {
+    return External.get();
+  }
+
+}

jbmc/regression/jbmc/load-containing-class-only/Test.class

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.test --load-containing-class-only
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that External.class is not loaded when using --load-containing-class-only

jbmc/regression/jbmc/load-containing-class-only/Test.java

@@ -10,15 +10,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <string>
 
-#include <util/symbol_table.h>
-#include <util/suffix.h>
-#include <util/config.h>
+#include <json/json_parser.h>
 #include <util/cmdline.h>
+#include <util/config.h>
 #include <util/expr_iterator.h>
+#include <util/invariant.h>
 #include <util/journalling_symbol_table.h>
 #include <util/string2int.h>
-#include <util/invariant.h>
-#include <json/json_parser.h>
+#include <util/string_utils.h>
+#include <util/suffix.h>
+#include <util/symbol_table.h>
 
 #include <goto-programs/class_hierarchy.h>
 
@@ -124,7 +125,32 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
     std::back_inserter(extra_methods),
     build_load_method_by_regex);
 
-  if(cmd.isset("java-cp-include-files"))
+  if(cmd.isset("load-containing-class-only"))
+  {
+    const std::string function_to_analyse = cmd.get_value("function");
+    const std::size_t first_dollar_index =
+      function_to_analyse.find_first_of('$');
+    const std::size_t last_dot_index = function_to_analyse.find_last_of('.');
+    std::string class_name = function_to_analyse;
+    if(first_dollar_index != std::string::npos)
+      class_name = class_name.substr(0, first_dollar_index);
+    else
+      class_name = class_name.substr(0, last_dot_index);
+    replace_all(class_name, ".", "\\/");
+    java_cp_include_files = class_name +
+                            "(\\$.*)?\\.class|"
+                            "java\\/.*|"
+                            "javax\\/.*|"
+                            "sun\\/.*|"
+                            "org\\/cprover\\/.*|"
+                            "com\\/diffblue\\/annotation\\/.*";
+
+    if(cmd.isset("java-cp-include-files"))
+      warning() << "--java-cp-include-files ignored due to "
+                   "--load-containing-class-only"
+                << eom;
+  }
+  else if(cmd.isset("java-cp-include-files"))
   {
     java_cp_include_files=cmd.get_value("java-cp-include-files");
     // load file list from JSON file

jbmc/regression/jbmc/load-containing-class-only/test.desc

@@ -38,7 +38,8 @@ Author: Daniel Kroening, kroening@kroening.com
   "(java-max-input-tree-depth):" /* will go away */ \
   "(max-nondet-tree-depth):" \
   "(java-max-vla-length):" \
-  "(java-cp-include-files):" \
+  "(load-containing-class-only)" \
+  "(java-cp-include-files)" \
   "(lazy-methods)" /* will go away */ \
   "(no-lazy-methods)" \
   "(lazy-methods-extra-entry-point):" \
@@ -59,6 +60,8 @@ Author: Daniel Kroening, kroening@kroening.com
   "                              never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \
   "                              entry point with null\n" /* NOLINT(*) */ \
   " --java-max-vla-length N      limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
+  " --load-containing-class-only only load the class containing the " \
+  "                              method under test and the library classes" \
   " --java-cp-include-files r    regexp or JSON list of files to load\n" \
   "                              (with '@' prefix)\n" \
   " --no-lazy-methods            load and translate all methods given on\n" \

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -24,7 +24,11 @@ void java_class_loader_limitt::setup_class_load_limit(
   // '@' signals file reading with list of class files to load
   use_regex_match = java_cp_include_files[0] != '@';
   if(use_regex_match)
+  {
     regex_matcher=std::regex(java_cp_include_files);
+    debug() << "Limit loading to classes matching : " << java_cp_include_files
+            << eom;
+  }
   else
   {
     assert(java_cp_include_files.length()>1);
@@ -54,7 +58,10 @@ bool java_class_loader_limitt::load_class_file(const std::string &file_name)
   if(use_regex_match)
   {
     std::smatch string_matches;
-    return std::regex_match(file_name, string_matches, regex_matcher);
+    if(std::regex_match(file_name, string_matches, regex_matcher))
+      return true;
+    debug() << file_name + " discarded since not matching loader regexp" << eom;
+    return false;
   }
   else
     // load .class file only if it is in the match set

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -54,6 +54,7 @@ class optionst;
   "(string-max-input-length):" \
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
+  "(load-containing-class-only)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
   "(show-symbol-table)(show-parse-tree)" \