Merge pull request #5127 from smowton/smowton/feature/lift-clinit-calls

Optionally lift clinit calls after Java method conversion

Author: smowton

jbmc/regression/jbmc/clinit-lifting1/Other.class

@@ -0,0 +1,20 @@
+public class Test {
+
+  public static void main(boolean unknown) {
+
+    int total = 0;
+
+    for(int i = 0; i < 10; ++i) {
+      if(unknown)
+        total += Other.x;
+    }
+
+  }
+
+}
+
+class Other {
+
+  static int x = 1;
+
+}

jbmc/regression/jbmc/clinit-lifting1/Test.class

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.main --java-lift-clinit-calls
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+Unwinding recursion java::Other\.<clinit_wrapper> iteration 1\nUnwinding loop java::Test\.main:\(Z\)V\.0 iteration 1
+--
+Unwinding recursion java::Other\.<clinit_wrapper> iteration 1\nUnwinding loop java::Test\.main:\(Z\)V\.0 iteration 2
+--
+This checks that the clinit-wrapper function is called prior to iteration 1 of the loop, but not iteration 2.
+

jbmc/regression/jbmc/clinit-lifting1/Test.java

@@ -0,0 +1,22 @@
+public class Test {
+
+  public static void main(boolean unknown, boolean other_unknown) {
+
+    int total = 0;
+
+    for(int i = 0; i < 10; ++i) {
+      if(unknown)
+        total += Other.x;
+      else if(other_unknown)
+        total -= Other.x;
+    }
+
+  }
+
+}
+
+class Other {
+
+  static int x = 1;
+
+}

jbmc/regression/jbmc/clinit-lifting1/test.desc

@@ -0,0 +1,11 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.main --java-lift-clinit-calls --show-goto-functions
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+\s*// 0 no location\n\s*Other\.<clinit_wrapper>\(\);\s*// 1 no location\s*int total;
+--
+--
+This checks that the clinit-wrapper function is called once, even though there are two calls in the source
+With symex-driven loading there's an exception check after the clinit_wrapper function finishes.

jbmc/regression/jbmc/clinit-lifting2/Other.class

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.main --java-lift-clinit-calls
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+Unwinding recursion java::Other\.<clinit_wrapper> iteration 1\nUnwinding loop java::Test\.main:\(ZZ\)V\.0 iteration 1
+--
+Unwinding recursion java::Other\.<clinit_wrapper> iteration 1\nUnwinding loop java::Test\.main:\(ZZ\)V\.0 iteration 2
+--
+This checks that the clinit-wrapper function is called prior to iteration 1 of the loop, but not iteration 2.
+

jbmc/regression/jbmc/clinit-lifting2/Test.class

@@ -0,0 +1,28 @@
+public class Test {
+
+  public static void main(boolean unknown, boolean other_unknown) {
+
+    int total = 0;
+
+    for(int i = 0; i < 10; ++i) {
+      if(unknown)
+        total += Other.x;
+      else if(other_unknown)
+        total -= Third.x;
+    }
+
+  }
+
+}
+
+class Other {
+
+  static int x = 1;
+
+}
+
+class Third {
+
+  static int x = 1;
+
+}

jbmc/regression/jbmc/clinit-lifting2/Test.java

@@ -0,0 +1,11 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.main --java-lift-clinit-calls --show-goto-functions
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+\s*// 0 no location\n\s*Other\.<clinit_wrapper>\(\);\s*// 1 no location\s*Third\.<clinit_wrapper>\(\);\s*// 2 no location\s*int total;
+--
+--
+This checks that the clinit-wrapper function is called once, even though there are two calls in the source
+With symex-driven loading there's an exception check after the clinit_wrapper function

jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.main --java-lift-clinit-calls
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+Unwinding recursion java::Other\.<clinit_wrapper> iteration 1\nUnwinding recursion java::Third\.<clinit_wrapper> iteration 1\nUnwinding loop java::Test\.main:\(ZZ\)V\.0 iteration 1
+--
+Unwinding recursion java::Other\.<clinit_wrapper> iteration 1\nUnwinding recursion java::Third\.<clinit_wrapper> iteration 1\nUnwinding loop java::Test\.main:\(ZZ\)V\.0 iteration 2
+--
+This checks that the clinit-wrapper functions are called prior to iteration 1 of the loop, but not iteration 2.
+

jbmc/regression/jbmc/clinit-lifting2/test.desc

@@ -43,6 +43,7 @@ SRC = assignments_from_json.cpp \
       java_trace_validation.cpp \
       java_types.cpp \
       java_utils.cpp \
+      lift_clinit_calls.cpp \
       lambda_synthesis.cpp \
       load_method_by_regex.cpp \
       mz_zip_archive.cpp \

jbmc/regression/jbmc/clinit-lifting3/Other.class

@@ -42,6 +42,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_string_literals.h"
 #include "java_utils.h"
 #include "lambda_synthesis.h"
+#include "lift_clinit_calls.h"
 
 #include "expr2java.h"
 #include "load_method_by_regex.h"
@@ -104,6 +105,8 @@ void parse_java_language_options(const cmdlinet &cmd, optionst &options)
   {
     options.set_option("static-values", cmd.get_value("static-values"));
   }
+  options.set_option(
+    "java-lift-clinit-calls", cmd.isset("java-lift-clinit-calls"));
 }
 
 prefix_filtert get_context(const optionst &options)
@@ -247,6 +250,8 @@ java_bytecode_language_optionst::java_bytecode_language_optionst(
 
   if(options.is_set("context-include") || options.is_set("context-exclude"))
     method_context = get_context(options);
+
+  should_lift_clinit_calls = options.get_bool_option("java-lift-clinit-calls");
 }
 
 /// Consume options that are java bytecode specific.
@@ -1174,7 +1179,8 @@ static void notify_static_method_calls(
 }
 
 /// \brief Convert a method (one whose type is known but whose body hasn't
-///   been converted) but don't run typecheck, etc
+///   been converted) if it doesn't already have a body, and lift clinit calls
+///   if requested by the user.
 /// \remarks Amends the symbol table entry for function `function_id`, which
 ///   should be a method provided by this instance of `java_bytecode_languaget`
 ///   to have a value representing the method body.
@@ -1197,6 +1203,41 @@ bool java_bytecode_languaget::convert_single_method(
     return false;
   INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
 
+  bool ret = convert_single_method_code(
+    function_id, symbol_table, needed_lazy_methods, class_to_declared_symbols);
+
+  if(symbol.value.is_not_nil() && language_options->should_lift_clinit_calls)
+  {
+    auto &writable_symbol = symbol_table.get_writeable_ref(function_id);
+    writable_symbol.value =
+      lift_clinit_calls(std::move(to_code(writable_symbol.value)));
+  }
+
+  INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
+
+  return ret;
+}
+
+/// \brief Convert a method (one whose type is known but whose body hasn't
+///   been converted) but don't run typecheck, etc
+/// \remarks Amends the symbol table entry for function `function_id`, which
+///   should be a method provided by this instance of `java_bytecode_languaget`
+///   to have a value representing the method body.
+/// \param function_id: method ID to convert
+/// \param symbol_table: global symbol table
+/// \param needed_lazy_methods: optionally a collection of needed methods to
+///   update with any methods touched during the conversion
+/// \param class_to_declared_symbols: maps classes to the symbols that
+///   they declare.
+bool java_bytecode_languaget::convert_single_method_code(
+  const irep_idt &function_id,
+  symbol_table_baset &symbol_table,
+  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
+  lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
+{
+  const auto &symbol = symbol_table.lookup_ref(function_id);
+  PRECONDITION(symbol.value.is_nil());
+
   // Get bytecode for specified function if we have it
   method_bytecodet::opt_reft cmb = method_bytecode.get(function_id);
 
@@ -1219,8 +1260,6 @@ bool java_bytecode_languaget::convert_single_method(
     // Add these to the needed_lazy_methods collection
     notify_static_method_calls(generated_code, needed_lazy_methods);
     writable_symbol.value = std::move(generated_code);
-    INVARIANT(
-      declaring_class(writable_symbol), "Method must have a declaring class.");
     return false;
   }
   else if(
@@ -1305,8 +1344,6 @@ bool java_bytecode_languaget::convert_single_method(
     // function:
     notify_static_method_calls(
       to_code(writable_symbol.value), needed_lazy_methods);
-    INVARIANT(
-      declaring_class(writable_symbol), "Method must have a declaring class.");
     return false;
   }
 
@@ -1327,7 +1364,6 @@ bool java_bytecode_languaget::convert_single_method(
       language_options->threading_support,
       language_options->method_context,
       language_options->assert_no_exceptions_thrown);
-    INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
     return false;
   }
 
@@ -1354,7 +1390,6 @@ bool java_bytecode_languaget::convert_single_method(
     }
   }
 
-  INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
   return true;
 }
 

jbmc/regression/jbmc/clinit-lifting3/Test.class

@@ -49,7 +49,8 @@ Author: Daniel Kroening, [email protected]
   "(lazy-methods-extra-entry-point):" \
   "(java-load-class):" \
   "(java-no-load-class):" \
-  "(static-values):"
+  "(static-values):" \
+  "(java-lift-clinit-calls)"
 
 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \
   " --disable-uncaught-exception-check\n" \
@@ -117,7 +118,12 @@ Author: Daniel Kroening, [email protected]
   "                              instead of calling the normal static initializer\n"/* NOLINT(*) */ \
   "                              (clinit) method.\n" \
   "                              The argument can be a relative or absolute path to\n"/* NOLINT(*) */ \
-  "                              the file.\n"
+  "                              the file.\n" \
+  " --java-lift-clinit-calls     Lifts clinit calls in function bodies to the top of the\n" /* NOLINT(*) */ \
+  "                              function. This may reduce the overall cost of static\n" /* NOLINT(*) */ \
+  "                              initialisation, but may be unsound if there are\n" /* NOLINT(*) */ \
+  "                              cyclic dependencies between static initializers due\n" /* NOLINT(*) */ \
+  "                              to potentially changing their order of execution." /* NOLINT(*) */
 // clang-format on
 
 class symbolt;
@@ -200,6 +206,11 @@ struct java_bytecode_language_optionst
   /// same kind of "return nondet null or instance of return type" body that we
   /// use for stubbed methods. The original method body will never be loaded.
   optionalt<prefix_filtert> method_context;
+
+  /// Should we lift clinit calls in function bodies to the top? For example,
+  /// turning `if(x) A.clinit() else B.clinit()` into
+  /// `A.clinit(); B.clinit(); if(x) ...`
+  bool should_lift_clinit_calls;
 };
 
 #define JAVA_CLASS_MODEL_SUFFIX "@class_model"
@@ -290,6 +301,11 @@ class java_bytecode_languaget:public languaget
     symbol_table_baset &symbol_table,
     optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
     lazy_class_to_declared_symbols_mapt &class_to_declared_symbols);
+  bool convert_single_method_code(
+    const irep_idt &function_id,
+    symbol_table_baset &symbol_table,
+    optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
+    lazy_class_to_declared_symbols_mapt &class_to_declared_symbols);
 
   bool do_ci_lazy_method_conversion(symbol_tablet &);
   const select_pointer_typet &get_pointer_type_selector() const;
@@ -302,7 +318,6 @@ class java_bytecode_languaget:public languaget
   method_bytecodet method_bytecode;
   java_string_library_preprocesst string_preprocess;
 
-
 private:
   virtual std::vector<load_extra_methodst>
   build_extra_entry_points(const optionst &) const;

jbmc/regression/jbmc/clinit-lifting3/Test.java

@@ -0,0 +1,69 @@
+/*******************************************************************\
+
+Module: Static initializer call lifting
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// file Static initializer call lifting
+
+#include "lift_clinit_calls.h"
+
+#include <java_bytecode/java_static_initializers.h>
+
+#include <util/expr_iterator.h>
+
+#include <algorithm>
+
+codet lift_clinit_calls(codet input)
+{
+  // 1. Gather any clinit calls present in `input`:
+  std::vector<symbol_exprt> clinit_wrappers_called;
+
+  for(auto it = input.depth_begin(), itend = input.depth_end(); it != itend;
+      ++it)
+  {
+    if(const auto code = expr_try_dynamic_cast<codet>(*it))
+    {
+      if(code->get_statement() == ID_function_call)
+      {
+        if(
+          const auto callee = expr_try_dynamic_cast<symbol_exprt>(
+            to_code_function_call(*code).function()))
+        {
+          if(is_clinit_wrapper_function(callee->get_identifier()))
+          {
+            clinit_wrappers_called.push_back(*callee);
+            // Replace call with skip:
+            it.mutate() = code_skipt();
+          }
+        }
+      }
+    }
+  }
+
+  if(clinit_wrappers_called.empty())
+    return input;
+
+  // 2. Unique, such that each clinit method is only called once:
+  std::sort(clinit_wrappers_called.begin(), clinit_wrappers_called.end());
+  auto delete_after =
+    std::unique(clinit_wrappers_called.begin(), clinit_wrappers_called.end());
+  clinit_wrappers_called.erase(delete_after, clinit_wrappers_called.end());
+
+  // 3. Lift static init calls to top of function:
+  code_blockt result;
+  for(const auto &callee : clinit_wrappers_called)
+  {
+    code_function_callt new_call(callee);
+    // Nuke the source location, now that the call doesn't really relate to any
+    // one particular line:
+    new_call.function().drop_source_location();
+    result.add(new_call);
+  }
+
+  result.add(std::move(input));
+
+  return std::move(result);
+}