Java class literals: init using a library hook when possible

The Java library definition of java.lang.Class, when nondet initialized, can be quite time
consuming due to the enumeration constant dictionary's internal array. Instead, let's give
the library a chance to set Class constants (literals like MyClass.class) itself.

While we're at it we might as well gain the ability to prove some properties of the literals.
We currently supply those class attributes that are easy to come by in the parse tree; with a
little more effort in the parser IsLocalClass and IsMemberClass could be determined.

Author: smowton

jbmc/regression/jbmc/class-literals/ExampleAnnotation.class

@@ -0,0 +1,4 @@
+
+public @interface ExampleAnnotation {
+
+}

jbmc/regression/jbmc/class-literals/ExampleAnnotation.java

@@ -0,0 +1,5 @@
+
+public enum ExampleEnum {
+
+}
+

jbmc/regression/jbmc/class-literals/ExampleEnum.class

@@ -0,0 +1,4 @@
+
+interface ExampleInterface {
+
+}

jbmc/regression/jbmc/class-literals/ExampleEnum.java

@@ -0,0 +1,34 @@
+
+public class Test {
+
+  public static void main() {
+
+    assert ExampleAnnotation.class.isAnnotation();
+    assert ExampleInterface.class.isInterface();
+    assert ExampleEnum.class.isEnum();
+
+    assert char[].class.isArray();
+    assert short[].class.isArray();
+    assert int[].class.isArray();
+    assert long[].class.isArray();
+    assert float[].class.isArray();
+    assert double[].class.isArray();
+    assert boolean[].class.isArray();
+    assert Object[].class.isArray();
+    assert Object[][].class.isArray();
+
+    // Note use of '==' not '.equals', as we expect the same exact literal,
+    // which in jbmc always have the same address.
+    // Note names of array classes are not tested yet, as arrays' types are
+    // printed as their raw signature, to be addressed separately.
+    // Note also primitive types (e.g. int.class) are not addresses here, as
+    // they are created through box types' static initializers (e.g. Integer
+    // has a static member TYPE that holds the Class for `int.class`)
+
+    assert ExampleAnnotation.class.getName() == "ExampleAnnotation";
+    assert ExampleInterface.class.getName() == "ExampleInterface";
+    assert ExampleEnum.class.getName() == "ExampleEnum";
+
+  }
+
+}

jbmc/regression/jbmc/class-literals/ExampleInterface.class

@@ -0,0 +1,45 @@
+package java.lang;
+
+public class Class {
+
+  private String name;
+
+  private boolean isAnnotation;
+  private boolean isArray;
+  private boolean isInterface;
+  private boolean isSynthetic;
+  private boolean isLocalClass;
+  private boolean isMemberClass;
+  private boolean isEnum;
+
+  public void cproverInitializeClassLiteral(
+    String name,
+    boolean isAnnotation,
+    boolean isArray,
+    boolean isInterface,
+    boolean isSynthetic,
+    boolean isLocalClass,
+    boolean isMemberClass,
+    boolean isEnum) {
+
+    this.name = name;
+    this.isAnnotation = isAnnotation;
+    this.isArray = isArray;
+    this.isInterface = isInterface;
+    this.isSynthetic = isSynthetic;
+    this.isLocalClass = isLocalClass;
+    this.isMemberClass = isMemberClass;
+    this.isEnum = isEnum;
+
+  }
+
+  public String getName() { return name; }
+
+  public boolean isAnnotation() { return isAnnotation; }
+  public boolean isArray() { return isArray; }
+  public boolean isInterface() { return isInterface; }
+  public boolean isSynthetic() { return isSynthetic; }
+  public boolean isLocalClass() { return isLocalClass; }
+  public boolean isMemberClass() { return isMemberClass; }
+  public boolean isEnum() { return isEnum; }
+}

jbmc/regression/jbmc/class-literals/ExampleInterface.java

@@ -0,0 +1,8 @@
+CORE
+Test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/class-literals/Test.class

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--lazy-methods
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/class-literals/Test.java

@@ -13,6 +13,7 @@
 #include "java_string_library_preprocess.h"
 #include "remove_exceptions.h"
 
+#include <util/expr_iterator.h>
 #include <util/suffix.h>
 
 #include <goto-programs/resolve_inherited_component.h>
@@ -52,6 +53,30 @@ ci_lazy_methodst::ci_lazy_methodst(
   class_hierarchy(symbol_table);
 }
 
+/// Checks if an expression refers to any class literals (e.g. MyType.class)
+/// These are expressed as ldc instructions in Java bytecode, and as symbols
+/// of the form MyType@class_model in GOTO programs.
+/// \param expr: expression to check
+/// \return true if the expression or any of its subexpressions refer to a
+///   class
+static bool references_class_model(const exprt &expr)
+{
+  symbol_typet class_type("java::java.lang.Class");
+
+  for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it)
+  {
+    if(can_cast_expr<symbol_exprt>(*it) &&
+       it->type() == class_type &&
+       has_suffix(
+         id2string(to_symbol_expr(*it).get_identifier()), "@class_model"))
+    {
+      return true;
+    }
+  }
+
+  return false;
+}
+
 /// Uses a simple context-insensitive ('ci') analysis to determine which methods
 /// may be reachable from the main entry point. In brief, static methods are
 /// reachable if we find a callsite in another reachable site, while virtual
@@ -122,6 +147,7 @@ bool ci_lazy_methodst::operator()(
 
   std::unordered_set<irep_idt> methods_already_populated;
   std::unordered_set<exprt, irep_hash> virtual_function_calls;
+  bool class_initializer_seen = false;
 
   bool any_new_classes = true;
   while(any_new_classes)
@@ -149,8 +175,19 @@ bool ci_lazy_methodst::operator()(
           // Couldn't convert this function
           continue;
         }
-        gather_virtual_callsites(
-          symbol_table.lookup_ref(mname).value, virtual_function_calls);
+        const exprt &method_body = symbol_table.lookup_ref(mname).value;
+
+        gather_virtual_callsites(method_body, virtual_function_calls);
+
+        if(!class_initializer_seen && references_class_model(method_body))
+        {
+          class_initializer_seen = true;
+          irep_idt initializer_signature =
+            get_java_class_literal_initializer_signature();
+          if(symbol_table.has_symbol(initializer_signature))
+            methods_to_convert_later.insert(initializer_signature);
+        }
+
         any_new_methods=true;
       }
     }

jbmc/regression/jbmc/class-literals/java/lang/Class.class

@@ -265,6 +265,9 @@ void java_bytecode_convert_classt::convert(
   class_type.set_tag(c.name);
   class_type.set(ID_base_name, c.name);
   class_type.set(ID_abstract, c.is_abstract);
+  class_type.set(ID_is_annotation, c.is_annotation);
+  class_type.set(ID_interface, c.is_interface);
+  class_type.set(ID_synthetic, c.is_synthetic);
   class_type.set_final(c.is_final);
   if(c.is_enum)
   {

jbmc/regression/jbmc/class-literals/java/lang/Class.java

@@ -785,7 +785,8 @@ bool java_bytecode_languaget::generate_support_functions(
       get_message_handler(),
       assume_inputs_non_null,
       object_factory_parameters,
-      get_pointer_type_selector());
+      get_pointer_type_selector(),
+      string_refinement_enabled);
 }
 
 /// Uses a simple context-insensitive ('ci') analysis to determine which methods

jbmc/regression/jbmc/class-literals/test.desc

@@ -204,6 +204,9 @@ class java_bytecode_parse_treet
     bool is_enum=false;
     bool is_public=false, is_protected=false, is_private=false;
     bool is_final = false;
+    bool is_interface = false;
+    bool is_synthetic = false;
+    bool is_annotation = false;
     bool attribute_bootstrapmethods_read = false;
     size_t enum_elements=0;
 

jbmc/regression/jbmc/class-literals/test_lazy.desc

@@ -451,9 +451,11 @@ bool java_bytecode_parsert::parse()
 #define ACC_BRIDGE       0x0040
 #define ACC_VARARGS      0x0080
 #define ACC_NATIVE       0x0100
+#define ACC_INTERFACE    0x0200
 #define ACC_ABSTRACT     0x0400
 #define ACC_STRICT       0x0800
 #define ACC_SYNTHETIC    0x1000
+#define ACC_ANNOTATION   0x2000
 #define ACC_ENUM         0x4000
 
 #ifdef _MSC_VER
@@ -496,6 +498,9 @@ void java_bytecode_parsert::rClassFile()
   parsed_class.is_protected=(access_flags&ACC_PROTECTED)!=0;
   parsed_class.is_private=(access_flags&ACC_PRIVATE)!=0;
   parsed_class.is_final = (access_flags & ACC_FINAL) != 0;
+  parsed_class.is_interface = (access_flags & ACC_INTERFACE) != 0;
+  parsed_class.is_synthetic = (access_flags & ACC_SYNTHETIC) != 0;
+  parsed_class.is_annotation = (access_flags & ACC_ANNOTATION) != 0;
   parsed_class.name=
     constant(this_class).type().get(ID_C_base_name);
 

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <linking/static_lifetime_init.h>
 
 #include "java_object_factory.h"
+#include "java_string_literals.h"
 #include "java_utils.h"
 
 static void create_initialize(symbol_table_baset &symbol_table)
@@ -65,12 +66,50 @@ static bool should_init_symbol(const symbolt &sym)
   return is_java_string_literal_id(sym.name);
 }
 
+/// Get the symbol name of java.lang.Class' initializer method. This method
+/// should initialize a Class instance with known properties of the type it
+/// represents, such as its name, whether it is abstract, or an enumeration,
+/// etc. The method may or may not exist in any particular symbol table; it is
+/// up to the caller to check.
+/// \return Class initializer method's symbol name.
+irep_idt get_java_class_literal_initializer_signature()
+{
+  static irep_idt signature =
+    "java::java.lang.Class.cproverInitializeClassLiteral:"
+    "(Ljava/lang/String;ZZZZZZZ)V";
+  return signature;
+}
+
+/// If symbol is a class literal, and an appropriate initializer method exists,
+/// return a pointer to its symbol. If not, return null.
+/// \param symbol: possible class literal symbol
+/// \param symbol_table: table to search
+/// \return pointer to the initializer method symbol or null
+static const symbolt *get_class_literal_initializer(
+  const symbolt &symbol,
+  const symbol_table_baset &symbol_table)
+{
+  if(symbol.value.is_not_nil())
+    return nullptr;
+  if(symbol.type != symbol_typet("java::java.lang.Class"))
+    return nullptr;
+  if(!has_suffix(id2string(symbol.name), "@class_model"))
+    return nullptr;
+  return symbol_table.lookup(get_java_class_literal_initializer_signature());
+}
+
+static constant_exprt constant_bool(bool val)
+{
+  return from_integer(val ? 1 : 0, java_boolean_type());
+}
+
 static void java_static_lifetime_init(
   symbol_table_baset &symbol_table,
   const source_locationt &source_location,
   bool assume_init_pointers_not_null,
   const object_factory_parameterst &object_factory_parameters,
-  const select_pointer_typet &pointer_type_selector)
+  const select_pointer_typet &pointer_type_selector,
+  bool string_refinement_enabled)
 {
   symbolt &initialize_symbol=*symbol_table.get_writeable(INITIALIZE_FUNCTION);
   code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
@@ -88,7 +127,53 @@ static void java_static_lifetime_init(
     const symbolt &sym=*symbol_table.lookup(symname);
     if(should_init_symbol(sym))
     {
-      if(sym.value.is_nil() && sym.type!=empty_typet())
+      if(const symbolt *class_literal_init_method =
+         get_class_literal_initializer(sym, symbol_table))
+      {
+        const std::string &name_str = id2string(sym.name);
+        irep_idt class_name =
+          name_str.substr(0, name_str.size() - strlen("@class_model"));
+        const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
+
+        bool class_is_array = is_java_array_tag(sym.name);
+
+        exprt name_literal(ID_java_string_literal);
+        name_literal.set(ID_value, to_class_type(class_symbol.type).get_tag());
+
+        symbol_exprt class_name_literal =
+          get_or_create_string_literal_symbol(
+            name_literal, symbol_table, string_refinement_enabled);
+
+        // Call the literal initializer method instead of a nondet initializer:
+
+        // For arguments we can't parse yet:
+        side_effect_expr_nondett nondet_bool(java_boolean_type());
+
+        // Argument order is: name, isAnnotation, isArray, isInterface,
+        // isSynthetic, isLocalClass, isMemberClass, isEnum
+
+        code_function_callt initializer_call;
+        initializer_call.function() = class_literal_init_method->symbol_expr();
+
+        code_function_callt::argumentst &args = initializer_call.arguments();
+
+        args.push_back(address_of_exprt(sym.symbol_expr())); /* this */
+        args.push_back(address_of_exprt(class_name_literal));
+        args.push_back(
+          constant_bool(class_symbol.type.get_bool(ID_is_annotation)));
+        args.push_back(constant_bool(class_is_array));
+        args.push_back(
+          constant_bool(class_symbol.type.get_bool(ID_interface)));
+        args.push_back(
+          constant_bool(class_symbol.type.get_bool(ID_synthetic)));
+        args.push_back(nondet_bool);
+        args.push_back(nondet_bool);
+        args.push_back(
+          constant_bool(class_symbol.type.get_bool(ID_enumeration)));
+
+        code_block.move_to_operands(initializer_call);
+      }
+      else if(sym.value.is_nil() && sym.type!=empty_typet())
       {
         bool allow_null=!assume_init_pointers_not_null;
         if(allow_null)
@@ -403,7 +488,8 @@ bool java_entry_point(
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   const object_factory_parameterst &object_factory_parameters,
-  const select_pointer_typet &pointer_type_selector)
+  const select_pointer_typet &pointer_type_selector,
+  bool string_refinement_enabled)
 {
   // check if the entry point is already there
   if(symbol_table.symbols.find(goto_functionst::entry_point())!=
@@ -426,7 +512,8 @@ bool java_entry_point(
     symbol.location,
     assume_init_pointers_not_null,
     object_factory_parameters,
-    pointer_type_selector);
+    pointer_type_selector,
+    string_refinement_enabled);
 
   return generate_java_start_function(
     symbol,

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -25,7 +25,8 @@ bool java_entry_point(
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   const object_factory_parameterst &object_factory_parameters,
-  const select_pointer_typet &pointer_type_selector);
+  const select_pointer_typet &pointer_type_selector,
+  bool string_refinement_enabled);
 
 struct main_function_resultt
 {
@@ -60,6 +61,8 @@ struct main_function_resultt
   }
 };
 
+irep_idt get_java_class_literal_initializer_signature();
+
 /// Figures out the entry point of the code to verify
 main_function_resultt get_main_symbol(
   const symbol_table_baset &symbol_table,