Add tests for inherited static fields

These cover various permutations of static fields defined on parents, on interfaces,
and those parents and/or interfaces being opaque (stubs). They check both that
jbmc doesn't outright crash, and in some cases that jbmc correctly determines that
two static fields must be the same one, and therefore cannot differ.

Author: smowton

regression/cbmc-java/inherited_static_field1/Parent.class

@@ -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.class

@@ -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_field1/Test.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_field1/test.desc

@@ -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/Parent.class

@@ -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/Parent.java

@@ -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_field10/Test.class

@@ -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_field10/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_field10/compile_against/Parent.class

@@ -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_field10/compile_against/Parent.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_field10/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_field2/InterfaceWithStatic.class

@@ -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_field2/InterfaceWithStatic.java

@@ -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_field2/Parent.class

@@ -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.class

@@ -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_field2/Test.java

@@ -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_field2/test.desc

@@ -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_field3/Test.class

@@ -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_field3/Test.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_field3/test.desc

@@ -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_field4/Grandparent.class

@@ -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_field4/Parent.class

@@ -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_field4/Test.class

@@ -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_field4/Test.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_field4/test.desc

@@ -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_field5/InterfaceWithStatic.class

@@ -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_field5/InterfaceWithStatic.java

@@ -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.

regression/cbmc-java/inherited_static_field5/Test.class

@@ -25,6 +25,7 @@ SRC += unit_tests.cpp \
        miniBDD_new.cpp \
        java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
        java_bytecode/java_utils_test.cpp \
+       java_bytecode/inherited_static_fields/inherited_static_fields.cpp \
        pointer-analysis/custom_value_set_analysis.cpp \
        sharing_node.cpp \
        solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \

regression/cbmc-java/inherited_static_field5/Test.java

@@ -0,0 +1,12 @@
+
+public class Test1 extends Parent1 {
+
+  public static int main() {
+    return x;
+  }
+
+}
+
+class Parent1 {
+  public static int x;
+}

regression/cbmc-java/inherited_static_field5/test.desc

@@ -0,0 +1,18 @@
+
+import java.util.ArrayList;
+
+public class Test2 implements StaticInterface2 {
+
+  public static int main() {
+    return x;
+  }
+
+}
+
+interface StaticInterface2 {
+  // 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();
+}