Allow extra entry-points to be specified for CI lazy loading

This allows driver programs that want more symbols elaborated
than are strictly accessible from the input arguments to request them.

This makes java-frontend documentation uniform rather than duplicate the
docs as usual, and also makes get_values non-fatal for parameters a
particular frontend did not supply, in common with other getters, in
order to avoid breaking unit tests that don't use lazy-methods.

Author: smowton

regression/cbmc-java/lazyloading10/test.class

@@ -0,0 +1,8 @@
+CORE
+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

regression/cbmc-java/lazyloading10/test.desc

@@ -0,0 +1,14 @@
+public class test {
+
+    int x;
+    int y;
+    
+    public test() { x = 1; y = 2; }
+    public void setx(int _x) { x = _x; }
+    public void sety(int _y) { y = _y; }
+    public void sety(float _y) { y = (int)_y; }
+    public void f() { }
+    
+}
+
+

regression/cbmc-java/lazyloading10/test.java

@@ -0,0 +1,10 @@
+CORE
+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"
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+CI lazy methods: elaborate java::test\.sety:\(I\)V
+CI lazy methods: elaborate java::test\.sety:\(F\)V
+--
+CI lazy methods: elaborate java::test\.setx:\(I\)V

regression/cbmc-java/lazyloading11/test.class

@@ -0,0 +1,14 @@
+public class test {
+
+    int x;
+    int y;
+    
+    public test() { x = 1; y = 2; }
+    public void setx(int _x) { x = _x; }
+    public void sety(int _y) { y = _y; }
+    public void sety(float _y) { y = (int)_y; }
+    public void f() { }
+    
+}
+
+

regression/cbmc-java/lazyloading11/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.setx
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+CI lazy methods: elaborate java::test\.setx:\(I\)V
+--
+CI lazy methods: elaborate java::test\.sety:\(I\)V
+CI lazy methods: elaborate java::test\.sety:\(F\)V

regression/cbmc-java/lazyloading11/test.java

@@ -0,0 +1,14 @@
+public class test {
+
+    int x;
+    int y;
+    
+    public test() { x = 1; y = 2; }
+    public void setx(int _x) { x = _x; }
+    public void sety(int _y) { y = _y; }
+    public void sety(float _y) { y = (int)_y; }
+    public void f() { }
+    
+}
+
+

regression/cbmc-java/lazyloading6/test.class

@@ -0,0 +1,10 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point "test.sety:(I)V"
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+CI lazy methods: elaborate java::test\.sety:\(I\)V
+--
+CI lazy methods: elaborate java::test\.setx:\(I\)V
+CI lazy methods: elaborate java::test\.sety:\(F\)V

regression/cbmc-java/lazyloading6/test.desc

@@ -0,0 +1,14 @@
+public class test {
+
+    int x;
+    int y;
+    
+    public test() { x = 1; y = 2; }
+    public void setx(int _x) { x = _x; }
+    public void sety(int _y) { y = _y; }
+    public void sety(float _y) { y = (int)_y; }
+    public void f() { }
+    
+}
+
+

regression/cbmc-java/lazyloading6/test.java

@@ -0,0 +1,10 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point "test.sety:(F)V"
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+CI lazy methods: elaborate java::test\.sety:\(F\)V
+--
+CI lazy methods: elaborate java::test\.sety:\(I\)V
+CI lazy methods: elaborate java::test\.setx:\(I\)V

regression/cbmc-java/lazyloading7/test.class

@@ -0,0 +1,14 @@
+public class test {
+
+    int x;
+    int y;
+    
+    public test() { x = 1; y = 2; }
+    public void setx(int _x) { x = _x; }
+    public void sety(int _y) { y = _y; }
+    public void sety(float _y) { y = (int)_y; }
+    public void f() { }
+    
+}
+
+

regression/cbmc-java/lazyloading7/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point "test.*"
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+CI lazy methods: elaborate java::test\.setx:\(I\)V
+CI lazy methods: elaborate java::test\.sety:\(I\)V
+CI lazy methods: elaborate java::test\.sety:\(F\)V

regression/cbmc-java/lazyloading7/test.java

@@ -0,0 +1,14 @@
+public class test {
+
+    int x;
+    int y;
+    
+    public test() { x = 1; y = 2; }
+    public void setx(int _x) { x = _x; }
+    public void sety(int _y) { y = _y; }
+    public void sety(float _y) { y = (int)_y; }
+    public void f() { }
+    
+}
+
+

regression/cbmc-java/lazyloading8/test.class

@@ -1073,22 +1073,9 @@ void cbmc_parse_optionst::help()
     "Java Bytecode frontend options:\n"
     " --classpath dir/jar          set the classpath\n"
     " --main-class class-name      set the name of the main class\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --java-assume-inputs-non-null test harness makes input arguments not null\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --java-max-input-array-length N maximum allowed length for an array passed as input\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --java-max-input-tree-depth N   object references are (deterministically) set to null in the object\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    "                                 hierarchy of input parameters when their depth is >= N and the object\n"
-    "                                 type happens twice in the tree branch\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --java-max-vla-length        limit the length of user-code-created arrays\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --java-cp-include-files      regexp or JSON list of files to load (with '@' prefix)\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
+    JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
+    // This one is handled by cbmc_parse_options not by the Java frontend,
+    // hence its presence here:
     " --java-unwind-enum-static    try to unwind loops in static initialization of enums\n"
     "\n"
     "Semantic transformations:\n"

regression/cbmc-java/lazyloading8/test.desc

@@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/goto_check.h>
 
+#include <java_bytecode/java_bytecode_language.h>
+
 #include "xml_interface.h"
 
 class bmct;
@@ -64,14 +66,9 @@ class optionst;
   "(string-abstraction)(no-arch)(arch):" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(graphml-witness):" \
-  "(java-max-vla-length):" \
+  JAVA_BYTECODE_LANGUAGE_OPTIONS \
   "(java-unwind-enum-static)" \
-  "(java-cp-include-files):" \
-  "(java-throw-runtime-exceptions)" \
-  "(java-max-input-array-length):" \
-  "(java-max-input-tree-depth):" \
   "(localize-faults)(localize-faults-method):" \
-  "(lazy-methods)" \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 
 class cbmc_parse_optionst:

regression/cbmc-java/lazyloading8/test.java

@@ -536,6 +536,8 @@ void clobber_parse_optionst::help()
     " --round-to-minus-inf         IEEE floating point rounding mode\n"
     " --round-to-zero              IEEE floating point rounding mode\n"
     "\n"
+    JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
+    "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
     " --show-properties            show the properties\n"

regression/cbmc-java/lazyloading9/test.class

@@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <analyses/goto_check.h>
 #include <goto-programs/show_goto_functions.h>
 
+#include <java_bytecode/java_bytecode_language.h>
+
 class goto_functionst;
 class optionst;
 
@@ -32,7 +34,8 @@ class optionst;
   "(version)" \
   "(string-abstraction)" \
   "(show-locs)(show-vcc)(show-properties)(show-trace)" \
-  "(property):"
+  "(property):" \
+  JAVA_BYTECODE_LANGUAGE_OPTIONS
 
 class clobber_parse_optionst:
   public parse_options_baset,

regression/cbmc-java/lazyloading9/test.desc

@@ -493,6 +493,7 @@ void goto_analyzer_parse_optionst::help()
     "Java Bytecode frontend options:\n"
     " --classpath dir/jar          set the classpath\n"
     " --main-class class-name      set the name of the main class\n"
+    JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
     "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"

regression/cbmc-java/lazyloading9/test.java

@@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/goto_check.h>
 
+#include <java_bytecode/java_bytecode_language.h>
+
 class bmct;
 class goto_functionst;
 class optionst;
@@ -45,7 +47,8 @@ class optionst;
   "(unreachable-instructions)(unreachable-functions)" \
   "(reachable-functions)" \
   "(intervals)(show-intervals)" \
-  "(non-null)(show-non-null)"
+  "(non-null)(show-non-null)" \
+  JAVA_BYTECODE_LANGUAGE_OPTIONS
 
 class goto_analyzer_parse_optionst:
   public parse_options_baset,

src/cbmc/cbmc_parse_options.cpp

@@ -28,6 +28,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_entry_point.h"
 #include "java_bytecode_parser.h"
 #include "java_class_loader.h"
+#include "java_utils.h"
 
 #include "expr2java.h"
 
@@ -54,6 +55,13 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   else
     lazy_methods_mode=LAZY_METHODS_MODE_EAGER;
 
+  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(),
+    extra_entry_points.begin(),
+    extra_entry_points.end());
+
   if(cmd.isset("java-cp-include-files"))
   {
     java_cp_include_files=cmd.get_value("java-cp-include-files");
@@ -463,6 +471,54 @@ bool java_bytecode_languaget::typecheck(
   return false;
 }
 
+/// Translates the given list of method names from human-readable to
+/// internal syntax.
+/// Expands any wildcards (entries ending in '.*') in the given method
+/// list to include all non-static methods defined on the given class.
+/// \param [in, out] methods: List of methods to expand. Any wildcard entries
+///   will be deleted and the expanded entries appended to the end.
+/// \param symbol_table: global symbol table
+static void resolve_method_names(
+  std::vector<irep_idt> &methods,
+  const symbol_tablet &symbol_table)
+{
+  std::vector<irep_idt> new_methods;
+  for(const irep_idt &method : methods)
+  {
+    const std::string &method_str=id2string(method);
+    if(!has_suffix(method_str, ".*"))
+    {
+      std::string error_message;
+      irep_idt internal_name=
+        resolve_friendly_method_name(
+          method_str,
+          symbol_table,
+          error_message);
+      if(internal_name==irep_idt())
+        throw "entry point "+error_message;
+      new_methods.push_back(internal_name);
+    }
+    else
+    {
+      irep_idt classname="java::"+method_str.substr(0, method_str.length()-2);
+      if(!symbol_table.has_symbol(classname))
+        throw "wildcard entry point '"+method_str+"': unknown class";
+
+      for(const auto &name_symbol : symbol_table.symbols)
+      {
+        if(name_symbol.second.type.id()!=ID_code)
+          continue;
+        if(!to_code_type(name_symbol.second.type).has_this())
+          continue;
+        if(has_prefix(id2string(name_symbol.first), id2string(classname)))
+          new_methods.push_back(name_symbol.first);
+      }
+    }
+  }
+
+  methods=std::move(new_methods);
+}
+
 /// Uses a simple context-insensitive ('ci') analysis to determine which methods
 /// may be reachable from the main entry point. In brief, static methods are
 /// reachable if we find a callsite in another reachable site, while virtual
@@ -512,6 +568,15 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
   else
     method_worklist2.push_back(main_function.main_function.name);
 
+  // Add any extra entry points specified; we should elaborate these in the
+  // same way as the main function.
+  std::vector<irep_idt> extra_entry_points=lazy_methods_extra_entry_points;
+  resolve_method_names(extra_entry_points, symbol_table);
+  method_worklist2.insert(
+    method_worklist2.begin(),
+    extra_entry_points.begin(),
+    extra_entry_points.end());
+
   std::set<irep_idt> needed_classes;
 
   {

src/cbmc/cbmc_parse_options.h

@@ -16,6 +16,32 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_class_loader.h"
 #include "java_string_library_preprocess.h"
 
+#define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \
+  "(java-assume-inputs-non-null)"                 \
+  "(java-throw-runtime-exceptions)"               \
+  "(java-max-input-array-length):"                \
+  "(java-max-input-tree-depth):"                  \
+  "(java-max-vla-length):"                        \
+  "(java-cp-include-files):"                      \
+  "(lazy-methods)"                                \
+  "(lazy-methods-extra-entry-point):"
+
+#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/                                          \
+  " --java-assume-inputs-non-null    never initialize reference-typed parameter to the\n"       \
+  "                                  entry point with null\n"                                   \
+  " --java-throw-runtime-exceptions  make implicit runtime exceptions explicit\n"               \
+  " --java-max-input-array-length N  limit input array size to <= N\n"                          \
+  " --java-max-input-tree-depth N    object references are (deterministically) set to null in\n"\
+  "                                  the object\n"                                              \
+  " --java-max-vla-length            limit the length of user-code-created arrays\n"            \
+  " --java-cp-include-files          regexp or JSON list of files to load (with '@' prefix)\n"  \
+  " --lazy-methods                   only translate methods that appear to be reachable from\n" \
+  "                                  the --function entry point or main class\n"                \
+  " --lazy-methods-extra-entry-point METHODNAME\n"                                              \
+  "                                  treat METHODNAME as a possible program entry point for\n"  \
+  "                                  the purpose of lazy method loading\n"                      \
+  "                                  A '.*' wildcard is allowed to specify all class members\n"
+
 #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
 #define MAX_NONDET_TREE_DEPTH 5
 
@@ -107,6 +133,7 @@ class java_bytecode_languaget:public languaget
   size_t max_user_array_length;     // max size for user code created arrays
   lazy_methodst lazy_methods;
   lazy_methods_modet lazy_methods_mode;
+  std::vector<irep_idt> lazy_methods_extra_entry_points;
   bool string_refinement_enabled;
   bool throw_runtime_exceptions;
   java_string_library_preprocesst string_preprocess;