JBMC: use simple method stubbing pass

This uses lazy_goto_modelt's support for driver programs supplying method replacements
to provide stub implementations of methods whose code is unavailable.

Author: smowton

src/jbmc/jbmc_parse_options.cpp

@@ -58,6 +58,7 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/remove_java_new.h>
 #include <java_bytecode/replace_java_nondet.h>
+#include <java_bytecode/simple_method_stubbing.h>
 
 #include <cbmc/version.h>
 
@@ -522,6 +523,21 @@ int jbmc_parse_optionst::doit()
     };
   }
 
+  object_factory_params.max_nondet_array_length =
+    cmdline.isset("java-max-input-array-length")
+      ? std::stoul(cmdline.get_value("java-max-input-array-length"))
+      : MAX_NONDET_ARRAY_LENGTH_DEFAULT;
+  object_factory_params.max_nondet_string_length =
+    cmdline.isset("string-max-input-length")
+      ? std::stoul(cmdline.get_value("string-max-input-length"))
+      : MAX_NONDET_STRING_LENGTH;
+  object_factory_params.max_nondet_tree_depth =
+    cmdline.isset("java-max-input-tree-depth")
+      ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
+      : MAX_NONDET_TREE_DEPTH;
+
+  stub_objects_are_not_null = cmdline.isset("java-assume-inputs-non-null");
+
   if(!cmdline.isset("symex-driven-lazy-loading"))
   {
     std::unique_ptr<goto_modelt> goto_model_ptr;
@@ -757,23 +773,11 @@ void jbmc_parse_optionst::process_goto_function(
     replace_java_nondet(function);
 
     // Similar removal of java nondet statements:
-    // TODO Should really get this from java_bytecode_language somehow, but we
-    // don't have an instance of that here.
-    object_factory_parameterst factory_params;
-    factory_params.max_nondet_array_length=
-      cmdline.isset("java-max-input-array-length")
-        ? std::stoul(cmdline.get_value("java-max-input-array-length"))
-        : MAX_NONDET_ARRAY_LENGTH_DEFAULT;
-    factory_params.max_nondet_string_length=
-      cmdline.isset("string-max-input-length")
-        ? std::stoul(cmdline.get_value("string-max-input-length"))
-        : MAX_NONDET_STRING_LENGTH;
-    factory_params.max_nondet_tree_depth=
-      cmdline.isset("java-max-input-tree-depth")
-        ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
-        : MAX_NONDET_TREE_DEPTH;
-
-    convert_nondet(function, get_message_handler(), factory_params, ID_java);
+    convert_nondet(
+      function,
+      get_message_handler(),
+      object_factory_params,
+      ID_java);
 
     // add generic checks
     goto_check(ns, options, ID_java, function.get_goto_function());
@@ -1014,7 +1018,7 @@ bool jbmc_parse_optionst::process_goto_functions(
 
 bool jbmc_parse_optionst::can_generate_function_body(const irep_idt &name)
 {
-  return false;
+  return true;
 }
 
 bool jbmc_parse_optionst::generate_function_body(
@@ -1023,7 +1027,27 @@ bool jbmc_parse_optionst::generate_function_body(
   goto_functiont &function,
   bool body_available)
 {
-  return false;
+  // Provide a simple stub implementation for any function we don't have a
+  // bytecode implementation for:
+
+  if(!body_available && symbol_table.lookup_ref(function_name).mode == ID_java)
+  {
+    java_generate_simple_method_stub(
+      function_name,
+      symbol_table,
+      stub_objects_are_not_null,
+      object_factory_params,
+      get_message_handler());
+
+    goto_convert_functionst converter(symbol_table, get_message_handler());
+    converter.convert_function(function_name, function);
+
+    return true;
+  }
+  else
+  {
+    return false;
+  }
 }
 
 /// display command line help

src/jbmc/jbmc_parse_options.h

@@ -114,6 +114,8 @@ class jbmc_parse_optionst:
   ui_message_handlert ui_message_handler;
   std::unique_ptr<cover_configt> cover_config;
   path_strategy_choosert path_strategy_chooser;
+  object_factory_parameterst object_factory_params;
+  bool stub_objects_are_not_null;
 
   void eval_verbosity();
   void get_command_line_options(optionst &);