Merge pull request #5199 from peterschrammel/jbmc-accept-method-name

JBMC accepts method name directly

Author: peterschrammel

doc/cprover-manual/jbmc-user-manual.md

@@ -123,7 +123,7 @@ depends on an input):
 To limit the number of times the for-loop is unwound, we use the `--unwind N`
 options, in which case the following call to JBMC:
 ```
-$ jbmc tutorial.ExampleUnwind --function tutorial.ExampleUnwind.isPrime --unwind 10
+$ jbmc tutorial.ExampleUnwind.isPrime --unwind 10
 ```
 will terminate correctly. In this case, we will see `VERIFICATION SUCCESSFUL`,
 as no automatic assertions are violated.
@@ -139,7 +139,7 @@ JBMC will try to refute. On line 7, we check the assertion that all odd
 numbers greater than 1 are prime. To be sure that this always holds, we run
 JBMC on the example, with a reasonable `unwind` value:
 ```
-$ jbmc tutorial.ExampleUnwind --function tutorial.ExampleUnwind.doSomething --unwind 10
+$ jbmc tutorial.ExampleUnwind.doSomething --unwind 10
 ```
 Unsurprisingly JBMC doesn't agree, and prints an assertion failure
 (truncated here for readability):
@@ -223,7 +223,7 @@ Consider the following code:
 
 When given the `--throw-runtime-exceptions` options:
 ```
-$ jbmc tutorial.ExampleExceptions --tutorial.ExampleExceptions.strLength --throw-runtime-exceptions
+$ jbmc tutorial.ExampleExceptions.strLength --throw-runtime-exceptions
 ```
 JBMC will signal that the `str.length()` call may throw a runtime exception
 and that this exception is not caught.

jbmc/regression/jbmc/main-class-from-function/NoPackage$Nested$Deeper.class

@@ -0,0 +1,6 @@
+public class NoPackage {
+  public static class Nested {
+    public static class Deeper {
+    }
+  }
+}

jbmc/regression/jbmc/main-class-from-function/NoPackage$Nested.class

@@ -0,0 +1,6 @@
+package mypackage;
+
+public class Package {
+  public static class Inner {
+  }
+}

jbmc/regression/jbmc/main-class-from-function/NoPackage.class

@@ -0,0 +1,8 @@
+CORE
+
+'mypackage.Package$Inner.<init>'
+^EXIT=0$
+^SIGNAL=0$
+^Found Java main class: mypackage.Package\$Inner$
+--
+--

jbmc/regression/jbmc/main-class-from-function/NoPackage.java

@@ -0,0 +1,8 @@
+CORE
+
+'NoPackage$Nested$Deeper.<init>'
+^EXIT=0$
+^SIGNAL=0$
+^Found Java main class: NoPackage\$Nested\$Deeper$
+--
+--

jbmc/regression/jbmc/main-class-from-function/mypackage/Package$Inner.class

@@ -0,0 +1,8 @@
+CORE
+
+'NoPackage.<init>:()V'
+^EXIT=0$
+^SIGNAL=0$
+^Found Java main class: NoPackage$
+--
+--

jbmc/regression/jbmc/main-class-from-function/mypackage/Package.class

@@ -0,0 +1,8 @@
+CORE
+
+'mypackage.Package.<init>'
+^EXIT=0$
+^SIGNAL=0$
+^Found Java main class: mypackage.Package$
+--
+--

jbmc/regression/jbmc/main-class-from-function/mypackage/Package.java

@@ -0,0 +1,8 @@
+CORE
+
+'mypackage.Baggage'
+^EXIT=6$
+^SIGNAL=0$
+^Error: Could not find or load main class mypackage\.Baggage$
+--
+--

jbmc/regression/jbmc/main-class-from-function/test_inner.desc

@@ -0,0 +1,8 @@
+CORE
+
+mypackage.Baggage.do
+^EXIT=6$
+^SIGNAL=0$
+^Error: Could not find or load main class mypackage\.Baggage\.do$
+--
+--

jbmc/regression/jbmc/main-class-from-function/test_inner_inner.desc

@@ -0,0 +1,9 @@
+CORE
+
+'mypackage.Package.do:()V'
+^EXIT=6$
+^SIGNAL=0$
+^Found Java main class: mypackage.Package$
+^main symbol resolution failed: 'mypackage.Package.do:\(\)V' not found$
+--
+--

jbmc/regression/jbmc/main-class-from-function/test_nopackage.desc

@@ -751,6 +751,8 @@ void janalyzer_parse_optionst::help()
     "\n"
     " janalyzer [-?] [-h] [--help] show help\n"
     " janalyzer\n"
+    HELP_JAVA_METHOD_NAME
+    " janalyzer\n"
     HELP_JAVA_CLASS_NAME
     " janalyzer\n"
     HELP_JAVA_JAR

jbmc/regression/jbmc/main-class-from-function/test_package.desc

@@ -318,16 +318,46 @@ void java_bytecode_languaget::initialize_class_loader()
   }
 }
 
+static void throwMainClassLoadingError(const std::string &main_class)
+{
+  throw invalid_source_file_exceptiont(
+    "Error: Could not find or load main class " + main_class);
+}
+
 void java_bytecode_languaget::parse_from_main_class()
 {
   if(!main_class.empty())
   {
-    status() << "Java main class: " << main_class << eom;
+    // Try to load class
+    status() << "Trying to load Java main class: " << main_class << eom;
+    if(!java_class_loader.can_load_class(main_class))
+    {
+      // Try to extract class name and load class
+      const auto maybe_class_name =
+        class_name_from_method_name(id2string(main_class));
+      if(!maybe_class_name)
+      {
+        throwMainClassLoadingError(id2string(main_class));
+        return;
+      }
+      status() << "Trying to load Java main class: " << maybe_class_name.value()
+               << eom;
+      if(!java_class_loader.can_load_class(maybe_class_name.value()))
+      {
+        throwMainClassLoadingError(id2string(main_class));
+        return;
+      }
+      // Everything went well. We have a loadable main class.
+      // The entry point ('main') will be checked later.
+      config.main = id2string(main_class);
+      main_class = maybe_class_name.value();
+    }
+    status() << "Found Java main class: " << main_class << eom;
+    // Now really load it.
     const auto &parse_trees = java_class_loader(main_class);
     if(parse_trees.empty() || !parse_trees.front().loading_successful)
     {
-      throw invalid_source_file_exceptiont(
-        "Error: Could not find or load main class " + id2string(main_class));
+      throwMainClassLoadingError(id2string(main_class));
     }
   }
 }

jbmc/regression/jbmc/main-class-from-function/test_wrong_class.desc

@@ -140,12 +140,17 @@ Author: Daniel Kroening, [email protected]
   "                              jar files\n" \
   "                              A " JAVA_CLASSPATH_SEPARATOR \
   " separated list of directories and JAR\n" \
-  "                               archives to search for class files.\n" \
+  "                              archives to search for class files.\n" \
   " --main-class class-name      set the name of the main class\n"
 
+#define HELP_JAVA_METHOD_NAME /* NOLINT(*) */ \
+  "    method-name               fully qualified name of method\n" \
+  "                              used as entry point, e.g.\n" \
+  "                              mypackage.Myclass.foo:(I)Z\n"
+
 #define HELP_JAVA_CLASS_NAME /* NOLINT(*) */ \
   "    class-name                name of class\n" \
-  "                              The entry point is the method specified by\n" /* NOLINT(*) */ \
+  "                              The entry point is the method specified by\n" \
   "                              --function, or otherwise, the\n" \
   "                              public static void main(String[])\n" \
   "                              method of the given class.\n"
@@ -154,7 +159,7 @@ Author: Daniel Kroening, [email protected]
   "(jar):"
 
 #define HELP_JAVA_JAR /* NOLINT(*) */ \
-  "    -jar jarfile             JAR file to be checked\n" \
+  "    -jar jarfile              JAR file to be checked\n" \
   "                              The entry point is the method specified by\n" \
   "                              --function or otherwise, the\n" \
   "                              public static void main(String[]) method\n" \

jbmc/regression/jbmc/main-class-from-function/test_wrong_class_and_method.desc

@@ -103,6 +103,17 @@ static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
     .has_value();
 }
 
+bool java_class_loadert::can_load_class(const irep_idt &class_name)
+{
+  for(const auto &cp_entry : classpath_entries)
+  {
+    auto parse_tree = load_class(class_name, cp_entry);
+    if(parse_tree.has_value())
+      return true;
+  }
+  return false;
+}
+
 /// Check through all the places class parse trees can appear and returns the
 /// first implementation it finds plus any overlay class implementations.
 /// Uses \p class_loader_limit to limit the class files that it might (directly

jbmc/regression/jbmc/main-class-from-function/test_wrong_method.desc

@@ -43,6 +43,10 @@ class java_class_loadert : public java_class_loader_baset
 
   parse_tree_with_overlayst &operator()(const irep_idt &class_name);
 
+  /// Checks whether \p class_name is parseable from the classpath,
+  /// ignoring class loading limits.
+  bool can_load_class(const irep_idt &class_name);
+
   parse_tree_with_overlayst &get_parse_tree(
     java_class_loader_limitt &class_loader_limit,
     const irep_idt &class_name);

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -507,3 +507,13 @@ void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)
 {
   symbol.type.set(ID_C_class, declaring_class);
 }
+
+NODISCARD optionalt<std::string>
+class_name_from_method_name(const std::string &method_name)
+{
+  const auto signature_index = method_name.rfind(":");
+  const auto method_index = method_name.rfind(".", signature_index);
+  if(method_index == std::string::npos)
+    return {};
+  return method_name.substr(0, method_index);
+}

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_set>
 
 #include <util/message.h>
+#include <util/nodiscard.h>
 #include <util/optional.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
@@ -145,4 +146,10 @@ optionalt<irep_idt> declaring_class(const symbolt &symbol);
 /// declaring_class.
 void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class);
 
+/// Get JVM type name of the class in which \p method_name is defined.
+/// Returns an empty optional if the class name cannot be retrieved,
+/// e.g. method_name is an internal function.
+NODISCARD optionalt<std::string>
+class_name_from_method_name(const std::string &method_name);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -1051,6 +1051,8 @@ void jbmc_parse_optionst::help()
     "\n"
     " jbmc [-?] [-h] [--help]      show help\n"
     " jbmc\n"
+    HELP_JAVA_METHOD_NAME
+    " jbmc\n"
     HELP_JAVA_CLASS_NAME
     " jbmc\n"
     HELP_JAVA_JAR