Extend lazy-methods-extra-entry-point to support regex methods

This will allow for loading for example, all constructors or all methods
called getSomething.

Tests using this require minor modifications when they have specified
the descriptor as the brackets must be escaped for the regex. However,
the new code handles the case where no descriptor is provided (in which
case it will match all overloads) and the case where no java:: prefix
has been provided, leaving similar behaviour.

Correcting documentation for the extra entry points

Author: thk123

jbmc/regression/jbmc/lazyloading10/test.desc

@@ -1,11 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.sety
-^EXIT=6$
 ^SIGNAL=0$
-entry point 'test\.sety' is ambiguous between:
-test\.sety:\(I\)V
-test\.sety:\(F\)V
+CI lazy methods: elaborate java::test\.sety:\(I\)V
+CI lazy methods: elaborate java::test\.sety:\(F\)V
 --
 --
 This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

jbmc/regression/jbmc/lazyloading11/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(I)V' --lazy-methods-extra-entry-point 'test.sety:(F)V'
+--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:\(I\)V' --lazy-methods-extra-entry-point 'test.sety:\(F\)V'
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

jbmc/regression/jbmc/lazyloading7/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(I)V'
+--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:\(I\)V'
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

jbmc/regression/jbmc/lazyloading8/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(F)V'
+--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:\(F\)V'
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

jbmc/src/java_bytecode/Makefile

@@ -32,6 +32,7 @@ SRC = bytecode_info.cpp \
       java_string_literals.cpp \
       java_types.cpp \
       java_utils.cpp \
+      load_method_by_regex.cpp \
       mz_zip_archive.cpp \
       remove_exceptions.cpp \
       remove_instanceof.cpp \

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -37,6 +37,7 @@ Author: Daniel Kroening, [email protected]
 #include "ci_lazy_methods.h"
 
 #include "expr2java.h"
+#include "load_method_by_regex.h"
 
 /// Consume options that are java bytecode specific.
 /// \param Command:line options
@@ -94,10 +95,11 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
 
   const std::list<std::string> &extra_entry_points=
     cmd.get_values("lazy-methods-extra-entry-point");
-  lazy_methods_extra_entry_points.insert(
-    lazy_methods_extra_entry_points.end(),
+  std::transform(
     extra_entry_points.begin(),
-    extra_entry_points.end());
+    extra_entry_points.end(),
+    std::back_inserter(extra_methods),
+    build_load_method_by_regex);
 
   if(cmd.isset("java-cp-include-files"))
   {
@@ -815,7 +817,7 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
     symbol_table,
     main_class,
     main_jar_classes,
-    lazy_methods_extra_entry_points,
+    extra_methods,
     java_class_loader,
     java_load_classes,
     get_pointer_type_selector(),

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -62,7 +62,10 @@ Author: Daniel Kroening, [email protected]
   " --lazy-methods-extra-entry-point METHODNAME\n"                                               /* NOLINT(*) */ \
   "                                  treat METHODNAME as a possible program entry point for\n"   /* NOLINT(*) */ \
   "                                  the purpose of lazy method loading\n"                       /* NOLINT(*) */ \
-  "                                  A '.*' wildcard is allowed to specify all class members\n"
+  "                                  METHODNAME can be a regex that will be matched against\n"   /* NOLINT(*) */ \
+  "                                  all symbols. If missing a java:: prefix will be added\n"    /* NOLINT(*) */ \
+  "                                  If no descriptor is found, all overloads of a method will\n"/* NOLINT(*) */ \
+  "                                  also be added."                                             /* NOLINT(*) */
 // clang-format on
 
 class symbolt;
@@ -173,7 +176,6 @@ class java_bytecode_languaget:public languaget
   size_t max_user_array_length;     // max size for user code created arrays
   method_bytecodet method_bytecode;
   lazy_methods_modet lazy_methods_mode;
-  std::vector<irep_idt> lazy_methods_extra_entry_points;
   bool string_refinement_enabled;
   bool throw_runtime_exceptions;
   bool assert_uncaught_exceptions;
@@ -195,6 +197,8 @@ class java_bytecode_languaget:public languaget
   class_hierarchyt class_hierarchy;
   // List of classes to never load
   std::unordered_set<std::string> no_load_classes;
+
+  std::vector<load_extra_methodst> extra_methods;
 };
 
 std::unique_ptr<languaget> new_java_bytecode_language();

jbmc/src/java_bytecode/load_method_by_regex.cpp

@@ -0,0 +1,74 @@
+
+/*******************************************************************\
+
+Module: Java Bytecode
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include "load_method_by_regex.h"
+
+#include <regex>
+
+#include <util/symbol_table.h>
+
+/// For a given user provided pattern, return a regex, having dealt with the
+/// cases where the user has not prefixed with java:: or suffixed with the
+/// descriptor
+/// \param pattern: The user provided pattern
+/// \return The regex to match with
+static std::regex build_regex_from_pattern(const std::string &pattern)
+{
+  std::string modified_pattern = pattern;
+  if(does_pattern_miss_descriptor(pattern))
+    modified_pattern += R"(:\(.*\).*)";
+
+  if(!has_prefix(pattern, "java::"))
+    modified_pattern = "java::" + modified_pattern;
+
+  return std::regex{modified_pattern};
+}
+
+/// Identify if a parameter includes a part that will match a descriptor. That
+/// is, does it have a colon separtor.
+/// \param pattern: The user provided pattern
+/// \return True if no descriptor is found (that is, the only : relates to the
+/// java:: prefix.
+bool does_pattern_miss_descriptor(const std::string &pattern)
+{
+  const size_t descriptor_index = pattern.rfind(':');
+  if(descriptor_index == std::string::npos)
+    return true;
+
+  static const std::string java_prefix = "java::";
+  return descriptor_index == java_prefix.length() - 1 &&
+         has_prefix(pattern, java_prefix);
+}
+
+/// Create a lambda that returns the symbols that the given pattern should be
+/// loaded.If the pattern doesn't include a colon for matching the descriptor,
+/// append a `:\(.*\).*` to the regex. Note this will mean all overloaded
+/// methods will be marked as extra entry points for CI lazy loading.
+/// If the pattern doesn't include the java:: prefix, prefix that
+/// \param pattern: The user provided pattern
+/// \return The lambda to execute.
+std::function<std::vector<irep_idt>(const symbol_tablet &symbol_table)>
+build_load_method_by_regex(const std::string &pattern)
+{
+  std::regex regex = build_regex_from_pattern(pattern);
+
+  return [=](const symbol_tablet &symbol_table) {
+    std::vector<irep_idt> matched_methods;
+    for(const auto &symbol : symbol_table.symbols)
+    {
+      if(
+        symbol.second.is_function() &&
+        std::regex_match(id2string(symbol.first), regex))
+      {
+        matched_methods.push_back(symbol.first);
+      }
+    }
+    return matched_methods;
+  };
+}

jbmc/src/java_bytecode/load_method_by_regex.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: Java Bytecode
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// \file
+/// Process a pattern to use as a regex for selecting extra entry points for
+/// ci_lazy_methodst
+
+#ifndef CPROVER_JAVA_BYTECODE_LOAD_METHOD_BY_REGEX_H
+#define CPROVER_JAVA_BYTECODE_LOAD_METHOD_BY_REGEX_H
+
+#include <java_bytecode/ci_lazy_methods.h>
+
+class symbol_tablet;
+
+std::function<std::vector<irep_idt>(const symbol_tablet &symbol_table)>
+build_load_method_by_regex(const std::string &pattern);
+
+bool does_pattern_miss_descriptor(const std::string &pattern);
+
+#endif // CPROVER_JAVA_BYTECODE_LOAD_METHOD_BY_REGEX_H

jbmc/unit/Makefile

@@ -21,6 +21,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
        java_bytecode/java_types/java_generic_symbol_type.cpp \
        java_bytecode/java_types/java_type_from_string.cpp \
        java_bytecode/java_utils_test.cpp \
+       java_bytecode/load_method_by_regex.cpp \
        java_bytecode/inherited_static_fields/inherited_static_fields.cpp \
        pointer-analysis/custom_value_set_analysis.cpp \
        solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \