- Fixed vtables in Java.

- Removed UB in Java bytecode module.
- Recompiled virtual1-virtual4 with JDK 8.

Author: pkesseli

regression/cbmc-java/virtual1/A.class

@@ -16,6 +16,7 @@ class virtual1
   public static void main(String[] args)
   {
     A a=new A();
+    B b=new B();
     a.f();
   }
 }

regression/cbmc-java/virtual1/B.class

@@ -15,8 +15,9 @@ class virtual2
 {
   public static void main(String[] args)
   {
-    A a=new B();
-    a.f();
+    A a=new A();
+    A b=new B();
+    b.f();
   }
 }
 

regression/cbmc-java/virtual1/virtual1.class

@@ -1,22 +1,28 @@
 interface A
 {
   public void f();
-};
+}
 
 class B implements A
 {
   public void f()
   {
     assert false;
   }
-};
+}
+
+class C implements A
+{
+  public void f(){}
+}
 
 class virtual3
 {
   public static void main(String[] args)
   {
-    A a = new B();
-    a.f();
+    A b = new B();
+    A c = new C();
+    b.f();
   }
 }
 

regression/cbmc-java/virtual1/virtual1.java

@@ -20,8 +20,9 @@ class virtual4
 {
   public static void main(String[] args)
   {
-    A a = new C();
-    a.f();
+    A b = new B();
+    A c = new C();
+    c.f();
   }
 }
 

regression/cbmc-java/virtual2/virtual2.class

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_predicates.h>
 #include <util/pointer_offset_size.h>
 #include <util/vtable.h>
+#include <util/namespace_utils.h>
 
 #include <linking/zero_initializer.h>
 
@@ -545,61 +546,33 @@ symbol_exprt get_vt(const irep_idt &class_name) {
   return symbol_exprt(vt_name, vttype);
 }
 
-const dereference_exprt cast_if_necessary(const exprt &lhs,
-    const irep_idt &ptr_class, const irep_idt &vt_class) {
-  const symbol_typet class_type(vt_class);
-  if (ptr_class == vt_class) return dereference_exprt(lhs, class_type);
-  const symbol_typet target_type(ptr_class);
-  const typecast_exprt cast(lhs, pointer_typet(target_type));
-  return dereference_exprt(cast, target_type);
-}
-
-void assign_vtpointer(goto_programt &dest, const namespacet &ns,
-    const exprt &lhs, const irep_idt &ptr_class, const irep_idt &vt_class,
-    const source_locationt &location) {
-  const symbol_exprt ptr_vt(get_vt(ptr_class));
-  const symbol_exprt vt(get_vt(vt_class));
-  const dereference_exprt lhs_ref(cast_if_necessary(lhs, ptr_class, vt_class));
-  const std::string memb_name(vtnamest::get_pointer(id2string(ptr_class)));
-  const pointer_typet ptr_vt_type(ptr_vt.type());
-  const member_exprt vtmember(lhs_ref, memb_name, ptr_vt_type);
-  const address_of_exprt vtable_ptr(vt);
-  const goto_programt::targett instr(dest.add_instruction(ASSIGN));
-  instr->source_location = location;
-  if (ptr_class == vt_class) {
-    instr->code = code_assignt(vtmember, vtable_ptr);
-  } else {
-    const typecast_exprt cast(vtable_ptr, ptr_vt_type);
-    instr->code = code_assignt(vtmember, cast);
-  }
-}
-
 bool is_type_missing(const namespacet &ns, const symbol_typet &type)
 {
   return !ns.get_symbol_table().has_symbol(type.get_identifier());
 }
 
-void assign_vtpointers(goto_programt &dest, const namespacet &ns,
-    const exprt &lhs, const symbol_typet &class_type,
-    const source_locationt &location)
+exprt &get_vt_pointer_member(struct_exprt &expr)
+{
+  // We assume the first member is vt_pointer or super class object.
+  assert(expr.has_operands());
+  exprt &op0=expr.op0();
+  if (ID_struct != op0.id()) return op0;
+  return get_vt_pointer_member(to_struct_expr(op0));
+}
+
+void set_vt_pointer(struct_exprt &expr, const namespacet &ns,
+    const symbol_typet &class_type)
 {
   if (is_type_missing(ns, class_type)) return;
   const irep_idt &class_name(class_type.get_identifier());
-  const irep_idt vtname(vtnamest::get_table(id2string(class_name)));
-  if (ns.get_symbol_table().has_symbol(vtname)) {
-    const class_typet &full_class_type(to_class_type(ns.follow(class_type)));
-    const irept::subt &bases(full_class_type.bases());
-    for (irept::subt::const_iterator it=bases.begin(); it != bases.end(); ++it) {
-      const typet &type(static_cast<const typet &>(it->find(ID_type)));
-      const symbol_typet &parent_type(to_symbol_type(type));
-      if (is_type_missing(ns, parent_type)) continue;
-      const irep_idt &parent_name(parent_type.get_identifier());
-      const irep_idt parent_vtname(vtnamest::get_table(id2string(parent_name)));
-      if(!ns.get_symbol_table().has_symbol(parent_vtname)) continue;
-      assign_vtpointer(dest, ns, lhs, parent_name, class_name, location);
-    }
-    assign_vtpointer(dest, ns, lhs, class_name, class_name, location);
-  }
+  const symbol_exprt vt(get_vt(class_name));
+  exprt &vt_pointer_member=get_vt_pointer_member(expr);
+  const typet &member_type=vt_pointer_member.type();
+  const address_of_exprt vt_pointer(vt);
+  if (type_eq(member_type, vt_pointer.type(), ns))
+    vt_pointer_member=vt_pointer;
+  else
+    vt_pointer_member=typecast_exprt(vt_pointer, member_type);
 }
 }
 
@@ -647,11 +620,10 @@ void goto_convertt::do_java_new(
   // zero-initialize the object
   dereference_exprt deref(lhs, object_type);
   exprt zero_object=zero_initializer(object_type, location, ns, get_message_handler());
+  set_vt_pointer(to_struct_expr(zero_object), ns, to_symbol_type(object_type));
   goto_programt::targett t_i=dest.add_instruction(ASSIGN);
   t_i->code=code_assignt(deref, zero_object);
   t_i->source_location=location;
-
-  assign_vtpointers(dest, ns, lhs, to_symbol_type(object_type), location);
 }
 
 /*******************************************************************\

regression/cbmc-java/virtual2/virtual2.java

@@ -747,12 +747,8 @@ codet java_bytecode_convertt::convert_instructions(
 
       if(is_virtual)
       {
-#if 0
         const exprt &this_arg=call.arguments().front();
         call.function() = make_vtable_function(arg0, this_arg);
-#else
-        call.function() = arg0;
-#endif
       }
       else
         call.function() = arg0;

regression/cbmc-java/virtual3/C.class

@@ -160,6 +160,10 @@ bool java_bytecode_languaget::typecheck(
       return true;
   }
 
+  // Construct vtable symbols before typecheck
+  if (java_bytecode_vtable(symbol_table, module))
+    return true;
+
   // now typecheck all
   if(java_bytecode_typecheck(
        symbol_table, get_message_handler()))

regression/cbmc-java/virtual3/virtual3.class

@@ -591,7 +591,7 @@ void java_bytecode_parsert::rinterfaces(classt &parsed_class)
   u2 interfaces_count=read_u2();
 
   for(unsigned i=0; i<interfaces_count; i++)
-    parsed_class.implements.push_back(pool_entry(read_u2()).s);
+    parsed_class.implements.push_back(constant(read_u2()).type().get(ID_C_base_name));
 }
 
 /*******************************************************************\

regression/cbmc-java/virtual3/virtual3.java

@@ -162,8 +162,8 @@ class java_bytecode_vtable_factoryt
     std::vector<class_typet> bases;
     extract_types(bases, class_type.bases(), method);
     //extract_types(bases, class_type.find(ID_interfaces).get_sub(), method);
-    for(std::vector<class_typet>::const_iterator b=bases.begin(); b != bases.end(); ++b)
-      add_vtable_entry(vtable_value, *b, class_type, method);
+    for(const std::vector<class_typet>::value_type &b : bases)
+      add_vtable_entry(vtable_value, b, class_type, method);
   }
 
   void create_vtable_entry(struct_exprt &vtable_value,
@@ -189,21 +189,21 @@ class java_bytecode_vtable_factoryt
     return symbol_table.has_symbol(vtnamest::get_type(class_name));
   }
 
-  void operator()(const std::pair<const irep_idt, symbolt> &named_symbol)
+  void operator()(const irep_idt &symbol_name)
   {
-    const symbolt &symbol(named_symbol.second);
+    const symbolt &symbol = symbol_table.lookup(symbol_name);
     if (!is_class_with_vt(symbol)) return;
     const class_typet &class_type(to_class_type(symbol.type));
-    const std::string &class_name(id2string(named_symbol.first));
+    const std::string &class_name(id2string(symbol_name));
     if (symbol_table.has_symbol(vtnamest::get_table(class_name))) return;
     symbolt vtable_symbol;
     create_vtable_symbol(vtable_symbol, class_type);
     const class_typet::methodst &methods(class_type.methods());
     struct_exprt vtable_value;
-    for (class_typet::methodst::const_iterator m=methods.begin(); m != methods.end(); ++m)
-      create_base_vtable_entries(vtable_value, class_type, *m);
-    for (class_typet::methodst::const_iterator m=methods.begin(); m != methods.end(); ++m)
-      create_vtable_entry(vtable_value, class_type, *m);
+    for (const class_typet::methodst::value_type &m : methods)
+      create_base_vtable_entries(vtable_value, class_type, m);
+    for (const class_typet::methodst::value_type &m : methods)
+      create_vtable_entry(vtable_value, class_type, m);
     set_vtable_value(vtable_symbol, class_type, vtable_value);
     assert(!symbol_table.add(vtable_symbol));
   }
@@ -228,12 +228,18 @@ bool java_bytecode_vtable(
   const std::string &module)
 {
   const symbol_tablet::symbolst &symbols(symbol_table.symbols);
+  std::vector<irep_idt> names;
+  names.reserve(symbols.size());
+  std::transform(symbols.begin(), symbols.end(), std::back_inserter(names),
+      [](const std::pair<irep_idt, symbolt> &entry)
+      { return entry.first;});
   java_bytecode_vtable_factoryt factory(symbol_table, module);
-  std::for_each(symbols.begin(), symbols.end(), factory);
+  std::for_each(names.begin(), names.end(), factory);
   return factory.has_error;
 }
 
-namespace {
+namespace
+{
 
 void create_vtable_type(const irep_idt &vt_name, symbol_tablet &symbol_table,
     const symbolt &class_symbol) {
@@ -252,6 +258,7 @@ void create_vtable_type(const irep_idt &vt_name, symbol_tablet &symbol_table,
 }
 
 const char ID_isvtptr[] = "is_vtptr";
+const char ID_vtable_pointer[] = "@vtable_pointer";
 
 void add_vtable_pointer_member(
   const irep_idt &vt_name,
@@ -260,9 +267,9 @@ void add_vtable_pointer_member(
   struct_typet::componentt comp;
 
   comp.type()=pointer_typet(symbol_typet(vt_name));
-  comp.set_name("@vtable_pointer");
-  comp.set_base_name("@vtable_pointer");
-  comp.set_pretty_name("@vtable_pointer");
+  comp.set_name(ID_vtable_pointer);
+  comp.set_base_name(ID_vtable_pointer);
+  comp.set_pretty_name(ID_vtable_pointer);
   comp.set(ID_isvtptr, true);
 
   struct_typet &class_type=to_struct_type(class_symbol.type);
@@ -386,17 +393,22 @@ exprt make_vtable_function(
   const irep_idt &func_name(func.get(ID_identifier));
   const std::string class_id(get_full_class_name(id2string(func_name)));
 
-  //if (class_id.find("java.lang.") != std::string::npos) {
-    // TODO: Handle unavailable models!
-    //return func;
-  //}
+  // TODO: Handle unavailable models!
+  if (class_id.find("java.") != std::string::npos) {
+    // When translating a single java_bytecode_parse_treet, we don't know
+    // which classes will eventually be available yet. If we could provide
+    // access to the class loader here, we know which classes have been
+    // loaded successfully. For classes which have not been loaded, returning
+    // "func" is equivalent to an unimplemented function.
+    return func;
+  }
 
   const symbol_typet vtable_type(vtnamest::get_type(class_id));
-  const pointer_typet vtable_pointer_type(vtable_type);
+  const pointer_typet vt_ptr_type(vtable_type);
   const symbol_typet target_type(class_id);
   const exprt this_ref(get_ref(this_obj, target_type));
   const typet ref_type(this_ref.type());
-  const member_exprt vtable_member(this_ref, "@vtable_pointer", vtable_pointer_type);
+  const member_exprt vtable_member(this_ref, ID_vtable_pointer, vt_ptr_type);
   const dereference_exprt vtable(vtable_member, vtable_type); // TODO: cast?
   const pointer_typet func_ptr_type(func.type());
   const member_exprt func_ptr(vtable, func_name, func_ptr_type);

regression/cbmc-java/virtual4/virtual4.class

@@ -18,15 +18,15 @@ void create_vtable_symbol(
   symbol_tablet &symbol_table,
   const class symbolt &class_symbol);
 
-code_assignt make_vtable_assignment(
-  const symbol_tablet &symbol_table,
-  const exprt &func);
-
 exprt make_vtable_function(
   const exprt &function,
   const exprt &this_obj);
 
 void set_virtual_name(
   class_typet::methodt &method);
 
+bool java_bytecode_vtable(
+  symbol_tablet &symbol_table,
+  const std::string &module);
+
 #endif /* CPROVER_JAVA_BYTECODE_VTABLE_H */