Merge pull request #2237 from smowton/smowton/feature/initialize-class-literals

Java class literals: init using a library hook when possible

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);