Optionally lift clinit calls after Java method conversion

This lifts all clinit calls in Java function bodies to the top, thereby
reducing the chances that a clinit method is repeatedly maybe-called (e.g.
due to `if(x) { A.staticfield.set(1); }`, which will only run A.<clinit> if
the branch is taken). If code like this occurs in a loop, for example, the
static initializer could be run by symex on every iteration, creating large
alias sets to account for all the possible initializer calls and sometimes
producing much larger formulas than are necessary.

On the other hand, with this option set, if `x` is definitely false we will
nontheless needlessly run the initializer, so in some circumstances the
option can increase costs.

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.
@@ -1200,6 +1206,13 @@ bool java_bytecode_languaget::convert_single_method(
   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;

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"
@@ -307,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);
+}

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

@@ -0,0 +1,18 @@
+/*******************************************************************\
+
+Module: Static initializer call lifting
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// file Static initializer call lifting
+
+#ifndef CPROVER_JAVA_BYTECODE_LIFT_CLINIT_CALLS_H
+#define CPROVER_JAVA_BYTECODE_LIFT_CLINIT_CALLS_H
+
+#include <util/std_code.h>
+
+codet lift_clinit_calls(codet input);
+
+#endif // CPROVER_JAVA_BYTECODE_LIFT_CLINIT_CALLS_H