Merge pull request #1228 from thk123/bugfix/lazy-method-params

Lazy Methods not loading base classes of params

Author: thk123

regression/cbmc-java/lazyloading_inheritance_field/Base.class

@@ -0,0 +1,7 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.test
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::Base\.f:\(\)V
+--

regression/cbmc-java/lazyloading_inheritance_field/Derived.class

@@ -0,0 +1,27 @@
+class Base
+{
+  void f() { }
+}
+
+class Middle extends Base
+{
+}
+
+class Derived extends Middle
+{
+  void f() { }
+}
+
+class Foo
+{
+  public Middle m;
+}
+
+public class test {
+
+  public static void test(Foo foo) {
+    if(foo != null && foo.m != null) {
+      foo.m.f();
+    }
+  }
+}

regression/cbmc-java/lazyloading_inheritance_field/Foo.class

@@ -49,6 +49,7 @@ SRC = basic_blocks.cpp \
       remove_vector.cpp \
       remove_virtual_functions.cpp \
       replace_java_nondet.cpp \
+      resolve_concrete_function_call.cpp \
       safety_checker.cpp \
       set_properties.cpp \
       show_goto_functions.cpp \

regression/cbmc-java/lazyloading_inheritance_field/Middle.class

@@ -64,6 +64,11 @@ void class_hierarchyt::get_children_trans_rec(
     get_children_trans_rec(child, dest);
 }
 
+/// Get all the classes that inherit (directly or indirectly) from class c. The
+/// first element(s) will be the immediate parents of c, followed by their
+/// immedatiate parents and so on.
+/// \param c: The class to consider
+/// \param [out] dest: A list of class ids that c eventually inherits from.
 void class_hierarchyt::get_parents_trans_rec(
   const irep_idt &c,
   idst &dest) const

regression/cbmc-java/lazyloading_inheritance_field/test.class

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 #include "class_hierarchy.h"
 #include "class_identifier.h"
 
+#include <goto-programs/resolve_concrete_function_call.h>
+
 #include <util/c_types.h>
 #include <util/prefix.h>
 #include <util/type_eq.h>
@@ -258,32 +260,26 @@ void remove_virtual_functionst::get_functions(
 {
   const irep_idt class_id=function.get(ID_C_class);
   const irep_idt component_name=function.get(ID_component_name);
-  assert(!class_id.empty());
+  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);
   functiont root_function;
 
-  // Start from current class, go to parents until something
-  // is found.
-  irep_idt c=class_id;
-  while(!c.empty())
+  if(resolved_call.is_valid())
   {
-    exprt method=get_method(c, component_name);
-    if(method.is_not_nil())
-    {
-      root_function.class_id=c;
-      root_function.symbol_expr=to_symbol_expr(method);
-      root_function.symbol_expr.set(ID_C_class, c);
-      break; // abort
-    }
+    root_function.class_id=resolved_call.get_class_identifier();
 
-    const class_hierarchyt::idst &parents=
-      class_hierarchy.class_map[c].parents;
+    const symbolt &called_symbol=
+      symbol_table.lookup(resolved_call.get_virtual_method_name());
 
-    if(parents.empty())
-      break;
-    c=parents.front();
+    root_function.symbol_expr=called_symbol.symbol_expr();
+    root_function.symbol_expr.set(
+      ID_C_class, resolved_call.get_class_identifier());
   }
-
-  if(root_function.class_id.empty())
+  else
   {
     // No definition here; this is an abstract function.
     root_function.class_id=class_id;
@@ -306,8 +302,9 @@ exprt remove_virtual_functionst::get_method(
   const irep_idt &class_id,
   const irep_idt &component_name) const
 {
-  irep_idt id=id2string(class_id)+"."+
-              id2string(component_name);
+  const irep_idt &id=
+    resolve_concrete_function_callt::build_virtual_method_name(
+      class_id, component_name);
 
   const symbolt *symbol;
   if(ns.lookup(id, symbol))