Java frontend: create String an Class literals earlier

This creates String and Class literals ahead of running java_bytecode_convert_method
instead of creating them in an after-the-fact fixup in typecheck_expr as previously.
These now exist before method conversion begins and __CPROVER_initialize is created,
which means the String literals are correctly initialised even when using incremental
method conversion.

This can be a little wasteful if they are only referred to from methods that would never
truly be invoked, but preliminary experiments suggest that creating ~10000 Strings takes
under a second, and that Java lazy loading can quickly delete ones that are not in fact
used.

Java CI lazy methods is augmented a little to notice that if we need global A, and global
A is initialised with a reference to global B, then we need global B as well. We appear to
have got away wtih this before because the inter-global references were introduced after
CI lazy methods finished loading methods.

Author: smowton

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1712,41 +1712,12 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       assert(op.empty() && results.size()==1);
 
-      // 1) Pushing a String causes a reference to a java.lang.String object
-      // to be constructed and pushed onto the operand stack.
+      INVARIANT(
+        arg0.id() != ID_java_string_literal && arg0.id() != ID_type,
+        "String and Class literals should have been lowered in "
+        "generate_constant_global_variables");
 
-      // 2) Pushing an int or a float causes a primitive value to be pushed
-      // onto the stack.
-
-      // 3) Pushing a Class constant causes a reference to a java.lang.Class
-      // to be pushed onto the operand stack
-
-      if(arg0.id()==ID_java_string_literal)
-      {
-        // these need to be references to java.lang.String
-        results[0]=arg0;
-        symbol_typet string_type("java::java.lang.String");
-        results[0].type()=java_reference_type(string_type);
-      }
-      else if(arg0.id()==ID_type)
-      {
-        irep_idt class_id=arg0.type().get(ID_identifier);
-        symbol_typet java_lang_Class("java::java.lang.Class");
-        symbol_exprt symbol_expr(
-          id2string(class_id)+"@class_model",
-          java_lang_Class);
-        address_of_exprt address_of_expr(symbol_expr);
-        results[0]=address_of_expr;
-      }
-      else if(arg0.id()==ID_constant)
-      {
-        results[0]=arg0;
-      }
-      else
-      {
-        error() << "unexpected ldc argument" << eom;
-        throw 0;
-      }
+      results[0] = arg0;
     }
     else if(statement=="goto" || statement=="goto_w")
     {

src/java_bytecode/java_bytecode_language.cpp

@@ -30,6 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_entry_point.h"
 #include "java_bytecode_parser.h"
 #include "java_class_loader.h"
+#include "java_string_literals.h"
 #include "java_utils.h"
 #include <java_bytecode/ci_lazy_methods.h>
 #include <java_bytecode/generate_java_generic_type.h>
@@ -256,6 +257,118 @@ static void infer_opaque_type_fields(
   }
 }
 
+/// Create if necessary, then return the constant global java.lang.Class symbol
+/// for a given class id
+/// \param class_id: class identifier
+/// \param symbol_table: global symbol table; a symbol may be added
+/// \return java.lang.Class typed symbol expression
+static symbol_exprt get_or_create_class_literal_symbol(
+  const irep_idt &class_id, symbol_tablet &symbol_table)
+{
+  symbol_typet java_lang_Class("java::java.lang.Class");
+  symbol_exprt symbol_expr(
+    id2string(class_id)+"@class_model",
+    java_lang_Class);
+  if(!symbol_table.has_symbol(symbol_expr.get_identifier()))
+  {
+    symbolt new_class_symbol;
+    new_class_symbol.name = symbol_expr.get_identifier();
+    new_class_symbol.type = symbol_expr.type();
+    INVARIANT(
+      has_prefix(id2string(new_class_symbol.name), "java::"),
+      "class identifier should have 'java::' prefix");
+    new_class_symbol.base_name =
+      id2string(new_class_symbol.name).substr(6);
+    new_class_symbol.mode = ID_java;
+    new_class_symbol.is_lvalue = true;
+    new_class_symbol.is_state_var = true;
+    new_class_symbol.is_static_lifetime = true;
+    symbol_table.add(new_class_symbol);
+  }
+
+  return symbol_expr;
+}
+
+/// Get result of a Java load-constant (ldc) instruction.
+/// Possible cases:
+/// 1) Pushing a String causes a reference to a java.lang.String object
+/// to be constructed and pushed onto the operand stack.
+/// 2) Pushing an int or a float causes a primitive value to be pushed
+/// onto the stack.
+/// 3) Pushing a Class constant causes a reference to a java.lang.Class
+/// to be pushed onto the operand stack
+/// \param ldc_arg0: raw operand to the ldc opcode
+/// \param symbol_table: global symbol table. If the argument `ldc_arg0` is a
+///   String or Class constant then a new constant global may be added.
+/// \param string_refinement_enabled: true if --refine-strings is enabled, which
+///   influences how String literals are structured.
+/// \return ldc result
+static exprt get_ldc_result(
+  const exprt &ldc_arg0,
+  symbol_tablet &symbol_table,
+  bool string_refinement_enabled)
+{
+  if(ldc_arg0.id() == ID_type)
+  {
+    const irep_idt &class_id = ldc_arg0.type().get(ID_identifier);
+    return
+      address_of_exprt(
+        get_or_create_class_literal_symbol(class_id, symbol_table));
+  }
+  else if(ldc_arg0.id() == ID_java_string_literal)
+  {
+    return
+      address_of_exprt(
+        get_or_create_string_literal_symbol(
+          ldc_arg0, symbol_table, string_refinement_enabled));
+  }
+  else
+  {
+    INVARIANT(
+      ldc_arg0.id() == ID_constant,
+      "ldc argument should be constant, string literal or class literal");
+    return ldc_arg0;
+  }
+}
+
+/// Creates global variables for constants mentioned in a given method. These
+/// are either string literals, or class literals (the java.lang.Class instance
+/// returned by `(some_reference_typed_expression).class`). The method parse
+/// tree is rewritten to directly reference these globals.
+/// \param parse_tree: parse tree to search for constant global references
+/// \param symbol_table: global symbol table, to which constant globals will be
+///   added.
+/// \param string_refinement_enabled: true if `--refine-stings` is active,
+///   which changes how string literals are structured.
+static void generate_constant_global_variables(
+  java_bytecode_parse_treet &parse_tree,
+  symbol_tablet &symbol_table,
+  bool string_refinement_enabled)
+{
+  for(auto &method : parse_tree.parsed_class.methods)
+  {
+    for(auto &instruction : method.instructions)
+    {
+      // ldc* instructions are Java bytecode "load constant" ops, which can
+      // retrieve a numeric constant, String literal, or Class literal.
+      if(instruction.statement == "ldc" ||
+         instruction.statement == "ldc2" ||
+         instruction.statement == "ldc_w" ||
+         instruction.statement == "ldc2_w")
+      {
+        INVARIANT(
+          instruction.args.size() != 0,
+          "ldc instructions should have an argument");
+        instruction.args[0] =
+          get_ldc_result(
+            instruction.args[0],
+            symbol_table,
+            string_refinement_enabled);
+      }
+    }
+  }
+}
+
 bool java_bytecode_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
@@ -317,6 +430,23 @@ bool java_bytecode_languaget::typecheck(
     infer_opaque_type_fields(c.second, symbol_table);
   }
 
+  // Create global variables for constants (String and Class literals) up front.
+  // This means that when running with lazy loading, we will be aware of these
+  // literal globals' existence when __CPROVER_initialize is generated in
+  // `generate_support_functions`.
+  const std::size_t before_constant_globals_size = symbol_table.symbols.size();
+  for(auto &c : java_class_loader.class_map)
+  {
+    generate_constant_global_variables(
+      c.second,
+      symbol_table,
+      string_refinement_enabled);
+  }
+  status() << "Java: added "
+           << (symbol_table.symbols.size() - before_constant_globals_size)
+           << " String or Class constant symbols"
+           << messaget::eom;
+
   // Now incrementally elaborate methods
   // that are reachable from this entry point.
   if(lazy_methods_mode==LAZY_METHODS_MODE_CONTEXT_INSENSITIVE)

src/java_bytecode/java_bytecode_typecheck.h

@@ -67,7 +67,6 @@ class java_bytecode_typecheckt:public typecheckt
   void typecheck_code(codet &);
   void typecheck_type(typet &);
   void typecheck_expr_symbol(symbol_exprt &);
-  void typecheck_expr_java_string_literal(exprt &);
   void typecheck_expr_member(member_exprt &);
   void typecheck_expr_java_new(side_effect_exprt &);
   void typecheck_expr_java_new_array(side_effect_exprt &);

src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -21,7 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_utils.h"
 #include "java_root_class.h"
 #include "java_string_library_preprocess.h"
-#include "java_string_literals.h"
 
 void java_bytecode_typecheckt::typecheck_expr(exprt &expr)
 {
@@ -39,6 +38,11 @@ void java_bytecode_typecheckt::typecheck_expr(exprt &expr)
   Forall_operands(it, expr)
     typecheck_expr(*it);
 
+  INVARIANT(
+    expr.id() != ID_java_string_literal,
+    "String literals should have been converted to constant globals "
+    "before typecheck_expr");
+
   if(expr.id()==ID_symbol)
     typecheck_expr_symbol(to_symbol_expr(expr));
   else if(expr.id()==ID_side_effect)
@@ -49,8 +53,6 @@ void java_bytecode_typecheckt::typecheck_expr(exprt &expr)
     else if(statement==ID_java_new_array)
       typecheck_expr_java_new_array(to_side_effect_expr(expr));
   }
-  else if(expr.id()==ID_java_string_literal)
-    typecheck_expr_java_string_literal(expr);
   else if(expr.id()==ID_member)
     typecheck_expr_member(to_member_expr(expr));
 }
@@ -70,13 +72,6 @@ void java_bytecode_typecheckt::typecheck_expr_java_new_array(
   typecheck_type(type);
 }
 
-void java_bytecode_typecheckt::typecheck_expr_java_string_literal(exprt &expr)
-{
-  expr = address_of_exprt(
-    get_or_create_string_literal_symbol(
-      expr, symbol_table, string_refinement_enabled));
-}
-
 void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt &expr)
 {
   irep_idt identifier=expr.get_identifier();

src/java_bytecode/java_string_literals.cpp

@@ -162,7 +162,16 @@ symbol_exprt get_or_create_string_literal_symbol(
     return_symbol.type = return_symbol.value.type();
     if(symbol_table.add(return_symbol))
       throw "failed to add return symbol to symbol table";
-    new_symbol.value = literal_init;
+
+    // Initialise the literal structure with
+    // (ABC_return_value, { ..., .length = N, .data = &ABC_constarray }),
+    // using a C-style comma expression to indicate that we need the
+    // _return_value global for its side-effects.
+    exprt init_comma_expr(ID_comma);
+    init_comma_expr.type() = literal_init.type();
+    init_comma_expr.copy_to_operands(return_symbol.symbol_expr());
+    init_comma_expr.move_to_operands(literal_init);
+    new_symbol.value = init_comma_expr;
   }
   else if(jls_struct.components().size()>=1 &&
           jls_struct.components()[0].get_name()=="@java.lang.Object")