[TG-1523] fix removed required virtual calls

regression/cbmc-java/removed_virtual_functions/AbstractList.java

@@ -0,0 +1,42 @@
+public abstract class AbstractList<E>
+    implements List<E>
+{
+    public Iterator<E> iterator() {
+        return new Itr();
+    }
+
+    public ListIterator<E> listIterator() {
+        return listIterator(0);
+    }
+
+    public boolean equals(Object o) {
+        if (o == this)
+            return true;
+        if (!(o instanceof List))
+            return false;
+
+        ListIterator<E> e1 = listIterator();
+        ListIterator<?> e2 = ((List<?>) o).listIterator();
+        while (e1.hasNext() && e2.hasNext()) {
+            E o1 = e1.next();
+            Object o2 = e2.next();
+            if (!(o1==null ? o2==null : o1.equals(o2)))
+                return false;
+        }
+        return !(e1.hasNext() || e2.hasNext());
+    }
+
+    private class Itr implements Iterator<E> {
+        Itr() {
+        }
+
+        public boolean hasNext() {
+            return false;
+        }
+
+        public E next() {
+            return null;
+        }
+
+    }
+}

regression/cbmc-java/removed_virtual_functions/ArrayList.java

@@ -0,0 +1,31 @@
+public class ArrayList<E> extends AbstractList<E>
+    implements List<E>
+{
+    public ListIterator<E> listIterator() {
+        return new ListItr(0);
+    }
+    public ListIterator<E> listIterator(int index) {
+        return new ListItr(index);
+    }
+    private class ListItr extends Itr implements ListIterator<E> {
+        ListItr(int index) {
+            super();
+        }
+
+        public boolean hasPrevious() {
+            return false;
+        }
+    }
+
+    private class Itr implements Iterator<E> {
+        Itr() {
+        }
+
+        public boolean hasNext() {
+            return false;
+        }
+        public E next() {
+            return null;
+        }
+    }
+}

regression/cbmc-java/removed_virtual_functions/ArrayListEquals.java

@@ -0,0 +1,11 @@
+public class ArrayListEquals {
+
+    public int check2(ArrayList<Integer> l1) {
+        ArrayList<Integer> al = new ArrayList<Integer>();
+        if(l1.equals(al))
+            return 1;
+        else
+            return 0;
+    }
+
+}

regression/cbmc-java/removed_virtual_functions/Iterator.java

@@ -0,0 +1,4 @@
+public interface Iterator<E> {
+    boolean hasNext();
+    E next();
+}

regression/cbmc-java/removed_virtual_functions/List.java

@@ -0,0 +1,4 @@
+public interface List<E> {
+    ListIterator<E> listIterator();
+    ListIterator<E> listIterator(int index);
+}

regression/cbmc-java/removed_virtual_functions/ListIterator.java

@@ -0,0 +1,5 @@
+public interface ListIterator<E> extends Iterator<E> {
+    boolean hasNext();
+    boolean hasPrevious();
+    E next();
+}

regression/cbmc-java/removed_virtual_functions/test.desc

@@ -0,0 +1,6 @@
+CORE
+ArrayListEquals.class
+--lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function ArrayListEquals.check2 --show-goto-functions
+e2 . ArrayList\$Itr.hasNext:\(\)Z\(\);
+--
+e2 . ListIterator.hasNext:\(\)Z\(\);

src/goto-programs/remove_virtual_functions.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 /// \file
 /// Remove Virtual Function (Method) Calls
+#include <algorithm>
 
 #include "remove_virtual_functions.h"
 #include "class_hierarchy.h"
@@ -47,15 +48,20 @@ class remove_virtual_functionst
     goto_programt::targett target);
 
   void get_functions(const exprt &, dispatch_table_entriest &);
+  typedef std::function<
+    resolve_concrete_function_callt::concrete_function_callt(
+      const irep_idt &,
+      const irep_idt &)>
+    function_call_resolvert;
   void get_child_functions_rec(
     const irep_idt &,
     const symbol_exprt &,
     const irep_idt &,
     dispatch_table_entriest &,
-    std::set<irep_idt> &visited) const;
-  exprt get_method(
-    const irep_idt &class_id,
-    const irep_idt &component_name) const;
+    std::set<irep_idt> &visited,
+    const function_call_resolvert &) const;
+  exprt
+  get_method(const irep_idt &class_id, const irep_idt &component_name) const;
 };
 
 remove_virtual_functionst::remove_virtual_functionst(
@@ -192,6 +198,10 @@ void remove_virtual_functionst::remove_virtual_function(
       {
         // No definition for this type; shouldn't be possible...
         t1->make_assertion(false_exprt());
+        t1->source_location.set_comment(
+          ("cannot find calls for " +
+           id2string(code.function().get(ID_identifier)) + " dispatching " +
+           id2string(fun.class_id)));
       }
       insertit.first->second=t1;
       // goto final
@@ -247,6 +257,7 @@ void remove_virtual_functionst::remove_virtual_function(
 /// `last_method_defn`: the most-derived parent of `this_id` to define the
 ///   requested function
 /// `component_name`: name of the function searched for
+/// `resolve_function_call`: function to resolve abstract method call
 /// \return `functions` is assigned a list of {class name, function symbol}
 ///   pairs indicating that if `this` is of the given class, then the call will
 ///   target the given function. Thus if A <: B <: C and A and C provide
@@ -257,7 +268,8 @@ void remove_virtual_functionst::get_child_functions_rec(
   const symbol_exprt &last_method_defn,
   const irep_idt &component_name,
   dispatch_table_entriest &functions,
-  std::set<irep_idt> &visited) const
+  std::set<irep_idt> &visited,
+  const function_call_resolvert &resolve_function_call) const
 {
   auto findit=class_hierarchy.class_map.find(this_id);
   if(findit==class_hierarchy.class_map.end())
@@ -278,14 +290,30 @@ void remove_virtual_functionst::get_child_functions_rec(
     {
       function.symbol_expr=last_method_defn;
     }
+    if(function.symbol_expr == symbol_exprt())
+    {
+      const resolve_concrete_function_callt::concrete_function_callt
+        &resolved_call = resolve_function_call(child, component_name);
+      if(resolved_call.is_valid())
+      {
+        function.class_id = resolved_call.get_class_identifier();
+        const symbolt &called_symbol =
+          symbol_table.lookup_ref(resolved_call.get_virtual_method_name());
+
+        function.symbol_expr = called_symbol.symbol_expr();
+        function.symbol_expr.set(
+          ID_C_class, resolved_call.get_class_identifier());
+      }
+    }
     functions.push_back(function);
 
     get_child_functions_rec(
       child,
       function.symbol_expr,
       component_name,
       functions,
-      visited);
+      visited,
+      resolve_function_call);
   }
 }
 
@@ -294,21 +322,30 @@ void remove_virtual_functionst::get_functions(
   dispatch_table_entriest &functions)
 {
   const irep_idt class_id=function.get(ID_C_class);
+  const std::string class_id_string(id2string(class_id));
   const irep_idt component_name=function.get(ID_component_name);
+  const std::string component_name_string(id2string(component_name));
   INVARIANT(!class_id.empty(), "All virtual functions must have a class");
 
   resolve_concrete_function_callt get_virtual_call_target(
     symbol_table, class_hierarchy);
-  const resolve_concrete_function_callt::concrete_function_callt &
-    resolved_call=get_virtual_call_target(class_id, component_name);
+  const function_call_resolvert resolve_function_call =
+    [&get_virtual_call_target](
+      const irep_idt &class_id, const irep_idt &component_name) {
+      return get_virtual_call_target(class_id, component_name);
+    };
+
+  const resolve_concrete_function_callt::concrete_function_callt
+    &resolved_call = get_virtual_call_target(class_id, component_name);
+
   dispatch_table_entryt root_function;
 
   if(resolved_call.is_valid())
   {
     root_function.class_id=resolved_call.get_class_identifier();
 
-    const symbolt &called_symbol=
-      *symbol_table.lookup(resolved_call.get_virtual_method_name());
+    const symbolt &called_symbol =
+      symbol_table.lookup_ref(resolved_call.get_virtual_method_name());
 
     root_function.symbol_expr=called_symbol.symbol_expr();
     root_function.symbol_expr.set(
@@ -327,7 +364,8 @@ void remove_virtual_functionst::get_functions(
     root_function.symbol_expr,
     component_name,
     functions,
-    visited);
+    visited,
+    resolve_function_call);
 
   if(root_function.symbol_expr!=symbol_exprt())
     functions.push_back(root_function);