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, kroening@kroening.com
 #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, kroening@kroening.com
   " --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/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 \