Fixing inheritance issue for java programs.

CBMC was incorrectly stubbing inherited methods. This leads to such methods
being treated as non-det. The fix simply prevents CBMC from stubbing methods
that are inherited.

Author: Degiorgio

regression/Makefile

@@ -3,6 +3,7 @@ DIRS = ansi-c \
        cbmc \
        cpp \
        cbmc-java \
+       cbmc-java-inheritance \
        goto-analyzer \
        goto-instrument \
        goto-instrument-typedef \

regression/cbmc-java-inheritance/Makefile

@@ -0,0 +1,38 @@
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
+
+%.class: %.java ../../src/org.cprover.jar
+	javac -g -cp ../../src/org.cprover.jar:. $<
+
+nondet_java_files := $(shell find . -name "Nondet*.java")
+nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files))
+
+.PHONY: nondet-class-files
+nondet-class-files: $(nondet_class_files)
+
+.PHONY: clean-nondet-class-files
+clean-nondet-class-files:
+	-rm $(nondet_class_files)

regression/cbmc-java-inheritance/inheritance01/A.class

@@ -0,0 +1,5 @@
+CORE
+test.class
+--function test.check
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java-inheritance/inheritance01/B.class

@@ -0,0 +1,20 @@
+class A
+{
+  public int toInt()
+  {
+    return 12345;
+  }
+}
+
+class B extends A
+{
+}
+
+class test
+{
+  void check()
+  {
+    B b=new B();
+    assert(b.toInt()==12345);
+  }
+}

regression/cbmc-java-inheritance/inheritance01/test.class

@@ -0,0 +1,5 @@
+CORE
+test.class
+--function test.check
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java-inheritance/inheritance01/test.desc

@@ -0,0 +1,24 @@
+class A
+{
+  protected int toInt()
+  {
+    return 12345;
+  }
+}
+
+class B extends A
+{
+  public void secondary()
+  {
+    assert(toInt()==12345);
+  }
+}
+
+class test
+{
+  void check()
+  {
+    B b=new B();
+    b.secondary();
+  }
+}

regression/cbmc-java-inheritance/inheritance01/test.java

@@ -0,0 +1,5 @@
+CORE
+test.class
+--function test.check
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java-inheritance/inheritance02/A.class

@@ -0,0 +1,24 @@
+class Z 
+{
+  public int toInt()
+  {
+    return 12345;
+  }
+}
+
+class A extends Z
+{
+}
+
+class B extends A
+{
+}
+
+class test
+{
+  void check()
+  {
+    B b=new B();
+    assert(b.toInt()==12345);
+  }
+}

regression/cbmc-java-inheritance/inheritance02/B.class

@@ -0,0 +1,5 @@
+CORE
+test.class
+--function test.check
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java-inheritance/inheritance02/test.class

@@ -0,0 +1,28 @@
+class A
+{
+  public int toInt()
+  {
+    return 12345;
+  }
+}
+
+class B extends A
+{
+  public int toInt()
+  {
+    return 9999;
+  }
+}
+
+class Z extends B
+{
+}
+
+class test
+{
+  void check()
+  {
+    Z z=new Z();
+    assert(z.toInt()==9999);
+  }
+}

regression/cbmc-java-inheritance/inheritance02/test.desc

@@ -0,0 +1,5 @@
+CORE
+test.class
+--function test.check
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java-inheritance/inheritance02/test.java

@@ -0,0 +1,21 @@
+interface A
+{
+  public int toInt();
+}
+
+class B implements A
+{
+  public int toInt()
+  {
+    return 12345;
+  }
+}
+
+class test
+{
+  void check()
+  {
+    B b=new B();
+    assert(b.toInt()==12345);
+  }
+}

regression/cbmc-java-inheritance/inheritance03/A.class

@@ -0,0 +1,10 @@
+package temp;
+
+class A
+{
+  int toint()
+  {
+    return 123456;
+  }
+}
+

regression/cbmc-java-inheritance/inheritance03/B.class

@@ -0,0 +1,9 @@
+package temp;
+
+public class B extends A
+{
+  public int check()
+  {
+    return toint();
+  }
+}

regression/cbmc-java-inheritance/inheritance03/Z.class

@@ -0,0 +1,5 @@
+CORE
+test.class
+--function test.check
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java-inheritance/inheritance03/test.class

@@ -0,0 +1,11 @@
+import temp.B;
+
+public class test
+{
+  public void check()
+  {
+     B myObject = new B();
+     assert(myObject.check()==123456);
+  }
+}
+

regression/cbmc-java-inheritance/inheritance03/test.desc

@@ -19,11 +19,13 @@ Author: Daniel Kroening, [email protected]
 #include <util/prefix.h>
 #include <util/arith_tools.h>
 #include <util/ieee_float.h>
+#include <util/invariant.h>
 
 #include <linking/zero_initializer.h>
 
 #include <goto-programs/cfg.h>
 #include <goto-programs/remove_exceptions.h>
+#include <goto-programs/class_hierarchy.h>
 #include <analyses/cfg_dominators.h>
 
 #include "java_bytecode_convert_method.h"
@@ -32,6 +34,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_types.h"
 #include "java_utils.h"
 #include "java_string_library_preprocess.h"
+#include "java_utils.h"
 
 #include <limits>
 #include <algorithm>
@@ -1428,12 +1431,12 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       assert(arg0.id()==ID_virtual_function);
 
-      // does the function symbol exist?
+      // if we don't have a definition for the called symbol, and we won't
+      // inherit a definition from a super-class, create a stub.
       irep_idt id=arg0.get(ID_identifier);
-
-      if(symbol_table.symbols.find(id)==symbol_table.symbols.end())
+      if(symbol_table.symbols.find(id)==symbol_table.symbols.end() &&
+         !(is_virtual && is_method_inherited(arg0.get(ID_C_class), id)))
       {
-        // no, create stub
         symbolt symbol;
         symbol.name=id;
         symbol.base_name=arg0.get(ID_C_base_name);
@@ -2687,3 +2690,40 @@ void java_bytecode_convert_method(
 
   java_bytecode_convert_method(class_symbol, method);
 }
+
+const bool java_bytecode_convert_methodt::is_method_inherited(
+  const irep_idt &classname, const irep_idt &methodid) const
+{
+  class_hierarchyt ch;
+  namespacet ns(symbol_table);
+  ch(symbol_table);
+
+  std::string stripped_methodid(id2string(methodid));
+  stripped_methodid.erase(0, classname.size());
+
+  const std::string &classpackage=java_class_to_package(id2string(classname));
+  const auto &parents=ch.get_parents_trans(classname);
+  for(const auto &parent : parents)
+  {
+    const irep_idt id=id2string(parent)+stripped_methodid;
+    const symbolt *symbol;
+    if(!ns.lookup(id, symbol) &&
+       symbol->type.id()==ID_code)
+    {
+      const auto &access=symbol->type.get(ID_access);
+      if(access==ID_public || access==ID_protected)
+        return true;
+      // methods with the default access modifier are only
+      // accessible within the same package.
+      else if(access==ID_default &&
+              java_class_to_package(id2string(parent))==classpackage)
+        return true;
+      else if(access==ID_private)
+        continue;
+      else
+        INVARIANT(false, "Unexpected access modifier.");
+    }
+  }
+  return false;
+}
+

regression/cbmc-java-inheritance/inheritance03/test.java

@@ -258,6 +258,10 @@ class java_bytecode_convert_methodt:public messaget
   bool class_needs_clinit(const irep_idt &classname);
   exprt get_or_create_clinit_wrapper(const irep_idt &classname);
   codet get_clinit_call(const irep_idt &classname);
+
+  const bool is_method_inherited(
+    const irep_idt &classname,
+    const irep_idt &methodid) const;
 };
 
 #endif

regression/cbmc-java-inheritance/inheritance04/A.class

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/prefix.h>
 #include <util/std_types.h>
 #include <util/invariant.h>
+#include <util/string_utils.h>
 
 #include "java_utils.h"
 #include "java_types.h"
@@ -52,3 +53,8 @@ unsigned java_method_parameter_slots(const code_typet &t)
 
   return slots;
 }
+
+const std::string java_class_to_package(const std::string &canonical_classname)
+{
+  return trim_from_last_delimiter(canonical_classname, '.');
+}

regression/cbmc-java-inheritance/inheritance04/B.class

@@ -24,4 +24,6 @@ unsigned java_local_variable_slots(const typet &t);
 /// pass, upon call, the arguments of a Java method whose type is \p t.
 unsigned java_method_parameter_slots(const code_typet &t);
 
+const std::string java_class_to_package(const std::string &canonical_classname);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H

regression/cbmc-java-inheritance/inheritance04/Z.class

@@ -99,3 +99,14 @@ void split_string(
   left=result[0];
   right=result[1];
 }
+
+std::string trim_from_last_delimiter(
+  const std::string &s,
+  const char delim)
+{
+  std::string result="";
+  const size_t index=s.find_last_of(delim);
+  if(index!=std::string::npos)
+    result=s.substr(0, index);
+  return result;
+}

regression/cbmc-java-inheritance/inheritance04/test.class

@@ -29,4 +29,8 @@ void split_string(
   std::string &right,
   bool strip=false);
 
+std::string trim_from_last_delimiter(
+  const std::string &s,
+  const char delim);
+
 #endif