Merge pull request #5156 from thomasspriggs/tas/lazy_initialize

Support for an external lazy methods driver to control when the `INITIALIZE_FUNCTION` is generated

Author: thomasspriggs

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <string>
 
+#include <linking/static_lifetime_init.h>
+
 #include <util/cmdline.h>
 #include <util/config.h>
 #include <util/expr_iterator.h>
@@ -757,6 +759,7 @@ bool java_bytecode_languaget::typecheck(
     "the Java front-end should only be used with an empty symbol table");
 
   java_internal_additions(symbol_table);
+  create_java_initialize(symbol_table);
 
   if(language_options->string_refinement_enabled)
     string_preprocess.initialize_conversion_table();
@@ -942,6 +945,8 @@ bool java_bytecode_languaget::typecheck(
       convert_single_method(
         method_sig.first, journalling_symbol_table, class_to_declared_symbols);
     }
+    convert_single_method(
+      INITIALIZE_FUNCTION, journalling_symbol_table, class_to_declared_symbols);
     // Now convert all newly added string methods
     for(const auto &fn_name : journalling_symbol_table.get_inserted())
     {
@@ -1095,6 +1100,7 @@ void java_bytecode_languaget::methods_provided(
   // Add all synthetic methods to map
   for(const auto &kv : synthetic_methods)
     methods.insert(kv.first);
+  methods.insert(INITIALIZE_FUNCTION);
 }
 
 /// \brief Promote a lazy-converted method (one whose type is known but whose
@@ -1119,8 +1125,9 @@ void java_bytecode_languaget::convert_lazy_method(
   lazy_class_to_declared_symbols_mapt class_to_declared_symbols;
   convert_single_method(function_id, symbol_table, class_to_declared_symbols);
 
-  // Instrument runtime exceptions (unless symbol is a stub)
-  if(symbol.value.is_not_nil())
+  // Instrument runtime exceptions (unless symbol is a stub or is the
+  // INITIALISE_FUNCTION).
+  if(symbol.value.is_not_nil() && function_id != INITIALIZE_FUNCTION)
   {
     java_bytecode_instrument_symbol(
       symbol_table,
@@ -1201,6 +1208,20 @@ bool java_bytecode_languaget::convert_single_method(
   // Nothing to do if body is already loaded
   if(symbol.value.is_not_nil())
     return false;
+
+  if(function_id == INITIALIZE_FUNCTION)
+  {
+    java_static_lifetime_init(
+      symbol_table,
+      symbol.location,
+      language_options->assume_inputs_non_null,
+      object_factory_parameters,
+      *pointer_type_selector,
+      language_options->string_refinement_enabled,
+      get_message_handler());
+    return false;
+  }
+
   INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
 
   bool ret = convert_single_method_code(

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -53,7 +53,6 @@ void create_java_initialize(symbol_table_baset &symbol_table)
   initialize.mode=ID_java;
 
   initialize.type = java_method_typet({}, java_void_type());
-
   symbol_table.add(initialize);
 }
 
@@ -104,7 +103,7 @@ static constant_exprt constant_bool(bool val)
   return from_integer(val ? 1 : 0, java_boolean_type());
 }
 
-static void java_static_lifetime_init(
+void java_static_lifetime_init(
   symbol_table_baset &symbol_table,
   const source_locationt &source_location,
   bool assume_init_pointers_not_null,
@@ -115,6 +114,7 @@ static void java_static_lifetime_init(
 {
   symbolt &initialize_symbol =
     symbol_table.get_writeable_ref(INITIALIZE_FUNCTION);
+  PRECONDITION(initialize_symbol.value.is_nil());
   code_blockt code_block;
 
   const symbol_exprt rounding_mode =
@@ -590,17 +590,6 @@ bool java_entry_point(
 
   assert(symbol.type.id()==ID_code);
 
-  create_java_initialize(symbol_table);
-
-  java_static_lifetime_init(
-    symbol_table,
-    symbol.location,
-    assume_init_pointers_not_null,
-    object_factory_parameters,
-    pointer_type_selector,
-    string_refinement_enabled,
-    message_handler);
-
   return generate_java_start_function(
     symbol,
     symbol_table,

jbmc/src/java_bytecode/java_entry_point.h

@@ -190,4 +190,14 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
 /// code for it yet.
 void create_java_initialize(symbol_table_baset &symbol_table);
 
+/// Adds the body to __CPROVER_initialize
+void java_static_lifetime_init(
+  symbol_table_baset &symbol_table,
+  const source_locationt &source_location,
+  bool assume_init_pointers_not_null,
+  java_object_factory_parameterst object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector,
+  bool string_refinement_enabled,
+  message_handlert &message_handler);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H

jbmc/unit/java_bytecode/java_bytecode_language/language.cpp

@@ -12,6 +12,9 @@ Author: Diffblue Limited.
 
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <java_bytecode/java_bytecode_language.h>
+#include <linking/static_lifetime_init.h>
+#include <util/options.h>
 
 SCENARIO(
   "java_bytecode_language_opaque_field",
@@ -45,3 +48,68 @@ SCENARIO(
     }
   }
 }
+
+static void use_external_driver(java_bytecode_languaget &language)
+{
+  optionst options;
+  options.set_option("symex-driven-lazy-loading", true);
+  language.set_language_options(options);
+}
+
+SCENARIO(
+  "LAZY_METHODS_MODE_EXTERNAL_DRIVER based generation of cprover_initialise",
+  "[core][java_bytecode_language]")
+{
+  java_bytecode_languaget language;
+  null_message_handlert null_message_handler;
+  language.set_message_handler(null_message_handler);
+  use_external_driver(language);
+  symbol_tablet symbol_table;
+  GIVEN("java_bytecode_languaget::typecheck is run.")
+  {
+    language.typecheck(symbol_table, "");
+    THEN("The " INITIALIZE_FUNCTION " is in the symbol table without code.")
+    {
+      const symbolt *const initialise =
+        symbol_table.lookup(INITIALIZE_FUNCTION);
+      REQUIRE(initialise);
+      REQUIRE(initialise->value.is_nil());
+    }
+    GIVEN(
+      "java_bytecode_languaget::convert_lazy_method is used to "
+      "generate " INITIALIZE_FUNCTION)
+    {
+      language.convert_lazy_method(INITIALIZE_FUNCTION, symbol_table);
+      THEN("The " INITIALIZE_FUNCTION " is in the symbol table with code.")
+      {
+        const symbolt *const initialise =
+          symbol_table.lookup(INITIALIZE_FUNCTION);
+        REQUIRE(initialise);
+        REQUIRE(can_cast_expr<codet>(initialise->value));
+      }
+    }
+  }
+}
+
+TEST_CASE(
+  "Standard generation of cprover_initialise",
+  "[core][java_bytecode_language]")
+{
+  java_bytecode_languaget language;
+  null_message_handlert null_message_handler;
+  language.set_message_handler(null_message_handler);
+  language.set_language_options(optionst{});
+  symbol_tablet symbol_table;
+  GIVEN("java_bytecode_languaget::typecheck is run.")
+  {
+    language.typecheck(symbol_table, "");
+    THEN("The " INITIALIZE_FUNCTION
+         " function is in the symbol table with code.")
+    {
+      const symbolt *const initialise =
+        symbol_table.lookup(INITIALIZE_FUNCTION);
+      REQUIRE(initialise);
+      REQUIRE(can_cast_expr<codet>(initialise->value));
+    }
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_language/module_dependencies.txt

@@ -1,3 +1,5 @@
+java_bytecode
 java-testing-utils
+linking
 testing-utils
 util