Add --load-containing-class-only option

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

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

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

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

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

@@ -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/src/java_bytecode/java_bytecode_language.cpp

@@ -10,15 +10,16 @@ Author: Daniel Kroening, [email protected]
 
 #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/src/java_bytecode/java_bytecode_language.h

@@ -38,6 +38,7 @@ Author: Daniel Kroening, [email protected]
   "(java-max-input-tree-depth):" /* will go away */ \
   "(max-nondet-tree-depth):" \
   "(java-max-vla-length):" \
+  "(load-containing-class-only)" \
   "(java-cp-include-files):" \
   "(lazy-methods)" /* will go away */ \
   "(no-lazy-methods)" \
@@ -59,6 +60,8 @@ Author: Daniel Kroening, [email protected]
   "                              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_class_loader_limit.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

src/util/string_utils.cpp

@@ -148,3 +148,16 @@ std::string escape(const std::string &s)
 
   return result;
 }
+
+void replace_all(
+  std::string &str,
+  const std::string &from,
+  const std::string &to)
+{
+  size_t start_pos = 0;
+  while((start_pos = str.find(from, start_pos)) != std::string::npos)
+  {
+    str.replace(start_pos, from.length(), to);
+    start_pos += to.length();
+  }
+}

src/util/string_utils.h

@@ -67,4 +67,6 @@ Stream &join_strings(
 /// programming language.
 std::string escape(const std::string &);
 
+void replace_all(std::string &, const std::string &, const std::string &);
+
 #endif