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,4 @@
+; Compile me with Jasmin 2.1+ (https://sourceforge.net/projects/jasmin/)
+
+.class public synthetic ExampleSynthetic
+.super java/lang/Object

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

@@ -0,0 +1,35 @@
+
+public class Test {
+
+  public static void main() {
+
+    assert ExampleAnnotation.class.isAnnotation();
+    assert ExampleInterface.class.isInterface();
+    assert ExampleEnum.class.isEnum();
+    assert ExampleSynthetic.class.isSynthetic();
+
+    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.java

@@ -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/ExampleSynthetic.class

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

jbmc/regression/jbmc/class-literals/ExampleSynthetic.j

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--lazy-methods
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+lazy-methods is incompatible with symex-driven lazy loading

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

@@ -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,31 @@ 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)
+{
+  static const 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()),
+         JAVA_CLASS_MODEL_SUFFIX))
+    {
+      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 +148,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 +176,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/Test.java

@@ -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.class

@@ -299,7 +299,7 @@ static symbol_exprt get_or_create_class_literal_symbol(
 {
   symbol_typet java_lang_Class("java::java.lang.Class");
   symbol_exprt symbol_expr(
-    id2string(class_id)+"@class_model",
+    id2string(class_id) + JAVA_CLASS_MODEL_SUFFIX,
     java_lang_Class);
   if(!symbol_table.has_symbol(symbol_expr.get_identifier()))
   {
@@ -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/java/lang/Class.java

@@ -68,6 +68,8 @@ enum lazy_methods_modet
   LAZY_METHODS_MODE_EXTERNAL_DRIVER
 };
 
+#define JAVA_CLASS_MODEL_SUFFIX "@class_model"
+
 class java_bytecode_languaget:public languaget
 {
 public:

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

@@ -209,6 +209,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);