Shorten virtual dispatch tables

regression/cbmc-java/NullPointer2/test.desc

@@ -3,7 +3,7 @@ NullPointer2.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V$
+^  file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/virtual6/test.desc

@@ -5,4 +5,3 @@ A.class
 ^SIGNAL=0$
 IF "java::C".*THEN GOTO
 IF "java::B".*THEN GOTO
-IF "java::A".*THEN GOTO

regression/cbmc-java/virtual7/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.class
+--show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+IF "java::E".*THEN GOTO [12]
+IF "java::B".*THEN GOTO [12]
+IF "java::D".*THEN GOTO [12]
+IF "java::C".*THEN GOTO [12]
+--
+IF "java::A".*THEN GOTO
+GOTO 4

regression/cbmc-java/virtual7/test.java

@@ -0,0 +1,25 @@
+public class test {
+  public static void main() {
+    A[] as = { new A(), new B(), new C(), new D(), new E() };
+    as[2].f();
+  }
+}
+
+class A {
+  void f() { }
+}
+
+
+class B extends A {
+  void f() { }
+}
+
+class C extends A {
+  void f() { }
+}
+
+class D extends C {
+}
+
+class E extends B {
+}

src/goto-programs/remove_virtual_functions.cpp

@@ -104,6 +104,8 @@ void remove_virtual_functionst::remove_virtual_function(
   const code_function_callt &code=
     to_code_function_call(target->code);
 
+  const auto &vcall_source_loc=target->source_location;
+
   const exprt &function=code.function();
   assert(function.id()==ID_virtual_function);
   assert(!code.arguments().empty());
@@ -121,16 +123,20 @@ void remove_virtual_functionst::remove_virtual_function(
   if(functions.size()==1)
   {
     assert(target->is_function_call());
-    to_code_function_call(target->code).function()=
-      functions.begin()->symbol_expr;
-
+    if(functions.begin()->symbol_expr==symbol_exprt())
+      target->make_skip();
+    else
+      to_code_function_call(target->code).function()=
+        functions.begin()->symbol_expr;
     return;
   }
 
   // the final target is a skip
   goto_programt final_skip;
 
   goto_programt::targett t_final=final_skip.add_instruction();
+  t_final->source_location=vcall_source_loc;
+
   t_final->make_skip();
 
   // build the calls and gotos
@@ -142,46 +148,57 @@ void remove_virtual_functionst::remove_virtual_function(
   // If necessary, cast to the last candidate function to
   // get the object's clsid. By the structure of get_functions,
   // this is the parent of all other classes under consideration.
-  symbol_typet suggested_type(functions.back().class_id);
+  const auto &base_classid=functions.back().class_id;
+  const auto &base_function_symbol=functions.back().symbol_expr;
+  symbol_typet suggested_type(base_classid);
   exprt c_id2=get_class_identifier_field(this_expr, suggested_type, ns);
 
-  goto_programt::targett last_function;
-  for(const auto &fun : functions)
+  std::map<irep_idt, goto_programt::targett> calls;
+  // Note backwards iteration, to get the least-derived candidate first.
+  for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
   {
-    goto_programt::targett t1=new_code_calls.add_instruction();
-    if(!fun.symbol_expr.get_identifier().empty())
+    const auto &fun=*it;
+    auto insertit=calls.insert(
+      {fun.symbol_expr.get_identifier(), goto_programt::targett()});
+
+    // Only create one call sequence per possible target:
+    if(insertit.second)
     {
+      goto_programt::targett t1=new_code_calls.add_instruction();
+      t1->source_location=vcall_source_loc;
+      if(!fun.symbol_expr.get_identifier().empty())
+      {
       // call function
-      t1->make_function_call(code);
-      auto &newcall=to_code_function_call(t1->code);
-      newcall.function()=fun.symbol_expr;
-      pointer_typet need_type(symbol_typet(fun.symbol_expr.get(ID_C_class)));
-      if(!type_eq(newcall.arguments()[0].type(), need_type, ns))
-        newcall.arguments()[0].make_typecast(need_type);
+        t1->make_function_call(code);
+        auto &newcall=to_code_function_call(t1->code);
+        newcall.function()=fun.symbol_expr;
+        pointer_typet need_type(symbol_typet(fun.symbol_expr.get(ID_C_class)));
+        if(!type_eq(newcall.arguments()[0].type(), need_type, ns))
+          newcall.arguments()[0].make_typecast(need_type);
+      }
+      else
+      {
+        // No definition for this type; shouldn't be possible...
+        t1->make_assertion(false_exprt());
+      }
+      insertit.first->second=t1;
+      // goto final
+      goto_programt::targett t3=new_code_calls.add_instruction();
+      t3->source_location=vcall_source_loc;
+      t3->make_goto(t_final, true_exprt());
     }
-    else
+
+    // If this calls the base function we just fall through.
+    // Otherwise branch to the right call:
+    if(fun.symbol_expr!=base_function_symbol)
     {
-      // No definition for this type; shouldn't be possible...
-      t1->make_assertion(false_exprt());
+      exprt c_id1=constant_exprt(fun.class_id, string_typet());
+      goto_programt::targett t4=new_code_gotos.add_instruction();
+      t4->source_location=vcall_source_loc;
+      t4->make_goto(insertit.first->second, equal_exprt(c_id1, c_id2));
     }
-
-    last_function=t1;
-
-    // goto final
-    goto_programt::targett t3=new_code_calls.add_instruction();
-    t3->make_goto(t_final, true_exprt());
-
-    exprt c_id1=constant_exprt(fun.class_id, string_typet());
-
-    goto_programt::targett t4=new_code_gotos.add_instruction();
-    t4->make_goto(t1, equal_exprt(c_id1, c_id2));
   }
 
-  // In any other case (most likely a stub class) call the most basic
-  // version of the method we know to exist:
-  goto_programt::targett fallthrough=new_code_gotos.add_instruction();
-  fallthrough->make_goto(last_function);
-
   goto_programt new_code;
 
   // patch them all together