Add support for inheritence of Java static fields. Fixes TG-2457

regression/cbmc-java/inherited_static_field1/Test.java

@@ -0,0 +1,16 @@
+public class Test extends Parent {
+
+  public static void main(int nondet) {
+
+    x = nondet;
+    assert x == Parent.x;
+
+  }
+
+}
+
+class Parent {
+
+  public static int x;
+
+}

regression/cbmc-java/inherited_static_field1/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+
+^VERIFICATION SUCCESSFUL$
+--
+--
+This checks that jbmc knows that test.x and parent.x refer to the same field.
+Both test and parent are concrete (available) classes.

regression/cbmc-java/inherited_static_field10/Parent.java

@@ -0,0 +1,9 @@
+
+public class Parent {
+
+  // This is the version of Parent we will run jbmc against, which has
+  // a static field 'x', but that field is private and cannot correspond
+  // to the reference 'Test.x'.
+  private static int x;
+
+}

regression/cbmc-java/inherited_static_field10/Test.java

@@ -0,0 +1,10 @@
+public class Test extends Parent {
+
+  public static void main(int nondet) {
+
+    x = nondet;
+    assert x == Parent.x;
+
+  }
+
+}

regression/cbmc-java/inherited_static_field10/compile_against/Parent.java

@@ -0,0 +1,8 @@
+
+public class Parent {
+
+  // This is the version of Parent we compile Test.java against, which does
+  // have a static field 'x'.
+  public static int x;
+
+}

regression/cbmc-java/inherited_static_field10/test.desc

@@ -0,0 +1,11 @@
+CORE
+Test.class
+
+Stub static field x found for non-stub type java::Test\. In future this will be a fatal error\.
+assertion at file Test\.java line 6 .* FAILURE
+^VERIFICATION FAILED$
+--
+Stub static field x found for non-stub type java::Parent\. In future this will be a fatal error\.
+--
+This test is the same as inherited_static_field9, except that the version of Parent we run against
+has a private static field that Test's 'x' cannot be referring to.

regression/cbmc-java/inherited_static_field2/InterfaceWithStatic.java

@@ -0,0 +1,12 @@
+import java.util.ArrayList;
+
+interface InterfaceWithStatic {
+
+  // The ArrayList is only here to define a constant x that
+  // is complicated enough for javac to generate a static init
+  // rather than just propagate the constant to all users.
+  static ArrayList<Integer> al = new ArrayList<Integer>();
+  static int x = al.size();
+
+}
+

regression/cbmc-java/inherited_static_field2/Test.java

@@ -0,0 +1,16 @@
+public class Test extends Parent implements InterfaceWithStatic {
+
+  public static void main() {
+
+    int val1 = InterfaceWithStatic.x;
+    int val2 = x;
+    assert val1 == val2;
+
+  }
+
+}
+
+class Parent {
+
+}
+

regression/cbmc-java/inherited_static_field2/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+
+^VERIFICATION SUCCESSFUL$
+--
+--
+This checks that jbmc knows that Test.x and InterfaceWithStatic.x are the same field.
+All types are concrete (not stubs).

regression/cbmc-java/inherited_static_field3/Test.java

@@ -0,0 +1,15 @@
+public class Test extends OpaqueParent {
+
+  public static void main() {
+
+    assert x == OpaqueParent.x;
+
+  }
+
+}
+
+class OpaqueParent {
+
+  public static int x;
+
+}

regression/cbmc-java/inherited_static_field3/test.desc

@@ -0,0 +1,7 @@
+CORE
+Test.class
+
+^VERIFICATION SUCCESSFUL$
+--
+--
+This is the same as test inherited_static_field1, except Test's parent is opaque.

regression/cbmc-java/inherited_static_field4/Test.java

@@ -0,0 +1,22 @@
+public class Test extends Parent {
+
+  public static void main(int nondet) {
+
+    x = nondet;
+    assert x == Grandparent.x;
+
+  }
+
+}
+
+class Parent extends Grandparent {
+
+  public static int x;
+
+}
+
+class Grandparent {
+
+  public static int x;
+
+}

regression/cbmc-java/inherited_static_field4/test.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+
+assertion at file Test\.java line 6 .* FAILURE
+^VERIFICATION FAILED$
+--
+--
+This checks that jbmc knows that the hidden field Grandparent.x is not the same
+as Test.x, which resolves to Parent.x.

regression/cbmc-java/inherited_static_field5/InterfaceWithStatic.java

@@ -0,0 +1,12 @@
+import java.util.ArrayList;
+
+interface InterfaceWithStatic {
+
+  // The ArrayList is only here to define a constant x that
+  // is complicated enough for javac to generate a static init
+  // rather than just propagate the constant to all users.
+  static ArrayList<Integer> al = new ArrayList<Integer>();
+  static int x = al.size();
+
+}
+

regression/cbmc-java/inherited_static_field5/Test.java

@@ -0,0 +1,16 @@
+public class Test extends OpaqueParent implements InterfaceWithStatic {
+
+  public static void main() {
+
+    int val1 = x;
+    int val2 = InterfaceWithStatic.x;
+    assert val1 == val2;
+
+  }
+
+}
+
+class OpaqueParent {
+
+}
+

regression/cbmc-java/inherited_static_field5/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+
+^VERIFICATION SUCCESSFUL$
+--
+--
+This is the same as inherited_static_field2, except that Test's parent is opaque. It must pass because
+the field 'x' should be found on InterfaceWithStatic, and so not created as a stub on OpaqueParent.

regression/cbmc-java/inherited_static_field6/Test.java

@@ -0,0 +1,22 @@
+public class Test extends OpaqueParent {
+
+  public static void main(int nondet) {
+
+    x = nondet;
+    assert x == Grandparent.x;
+
+  }
+
+}
+
+class OpaqueParent extends Grandparent {
+
+  public static int x;
+
+}
+
+class Grandparent {
+
+  public static int x;
+
+}

regression/cbmc-java/inherited_static_field6/test.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+
+assertion at file Test\.java line 6 .* FAILURE
+^VERIFICATION FAILED$
+--
+--
+This test is the same as inherited_static_field4, except that Test's parent is opaque.
+This checks that jbmc guesses that the hidden field Grandparent.x is not the same
+as Test.x, which may resolve to the (unseen) Parent.x.

regression/cbmc-java/inherited_static_field7/OpaqueInterfaceWithStatic.java

@@ -0,0 +1,12 @@
+import java.util.ArrayList;
+
+interface OpaqueInterfaceWithStatic {
+
+  // The ArrayList is only here to define a constant x that
+  // is complicated enough for javac to generate a static init
+  // rather than just propagate the constant to all users.
+  static ArrayList<Integer> al = new ArrayList<Integer>();
+  static int x = al.size();
+
+}
+

regression/cbmc-java/inherited_static_field7/Test.java

@@ -0,0 +1,12 @@
+public class Test implements OpaqueInterfaceWithStatic {
+
+  public static void main() {
+
+    int val1 = x;
+    int val2 = OpaqueInterfaceWithStatic.x;
+    assert val1 == val2;
+
+  }
+
+}
+

regression/cbmc-java/inherited_static_field7/test.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test must pass, as there is only one opaque parent (interface_with_static).
+In particular this one makes sure we don't identify Object as opaque and guess that
+java.lang.Object.x exists (since we know Object doesn't have static fields).

regression/cbmc-java/inherited_static_field8/Test.java

@@ -0,0 +1,23 @@
+public class Test extends Parent {
+
+  public static void main(int nondet) {
+
+    x = nondet;
+    assert x == Parent.x;
+    assert x == OpaqueGrandparent.x;
+
+  }
+
+}
+
+class Parent extends OpaqueGrandparent {
+
+  public static int x;
+
+}
+
+class OpaqueGrandparent {
+
+  public static int x;
+
+}

regression/cbmc-java/inherited_static_field8/test.desc

@@ -0,0 +1,11 @@
+CORE
+Test.class
+
+assertion at file Test\.java line 6 .* SUCCESS
+assertion at file Test\.java line 7 .* FAILURE
+^VERIFICATION FAILED$
+--
+--
+This test is the same as inherited_static_field4, except that Test's grandparent is opaque.
+This checks that jbmc infers that the hidden field Grandparent.x is not the same
+as Test.x, which is known to resolve to Parent.x.

regression/cbmc-java/inherited_static_field9/Parent.java

@@ -0,0 +1,7 @@
+
+public class Parent {
+
+  // This is the version of Parent we will run jbmc against, which does
+  // not have a static field 'x'.
+
+}

regression/cbmc-java/inherited_static_field9/Test.java

@@ -0,0 +1,10 @@
+public class Test extends Parent {
+
+  public static void main(int nondet) {
+
+    x = nondet;
+    assert x == Parent.x;
+
+  }
+
+}

regression/cbmc-java/inherited_static_field9/compile_against/Parent.java

@@ -0,0 +1,8 @@
+
+public class Parent {
+
+  // This is the version of Parent we compile Test.java against, which does
+  // have a static field 'x'.
+  public static int x;
+
+}

regression/cbmc-java/inherited_static_field9/test.desc

@@ -0,0 +1,13 @@
+CORE
+Test.class
+
+Stub static field x found for non-stub type java::Test\. In future this will be a fatal error\.
+Stub static field x found for non-stub type java::Parent\. In future this will be a fatal error\.
+assertion at file Test\.java line 6 .* FAILURE
+^VERIFICATION FAILED$
+--
+--
+This tests the corner case where static fields are found on non-stub types, here caused
+by compiling Test.class against a version of Parent.class (in directory compile_against)
+that has a static field but then analysing it with one that doesn't have that field.
+In future, as the warning messages we check for note, this will be a fatal error.

src/goto-programs/Makefile

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