Merge pull request diffblue#334 from diffblue/pull-support-20180216

Merge from master, 20180216

Author: smowton

.gitignore

@@ -10,6 +10,7 @@ src/goto-analyzer/taint_driver_scripts/.idea/*
 /*.creator
 /*.creator.user
 /*.files
+/*.idea
 /*.includes
 # Eclipse
 src/.cproject
@@ -45,6 +46,7 @@ src/ansi-c/gcc_builtin_headers_tm.inc
 src/ansi-c/gcc_builtin_headers_mips.inc
 src/ansi-c/gcc_builtin_headers_power.inc
 src/ansi-c/gcc_builtin_headers_ubsan.inc
+src/java_bytecode/java_core_models.inc
 
 # regression/test files
 *.out
@@ -116,8 +118,11 @@ src/ansi-c/file_converter
 src/ansi-c/file_converter.exe
 src/ansi-c/library/converter
 src/ansi-c/library/converter.exe
+src/java_bytecode/converter
+src/java_bytecode/converter.exe
 src/util/irep_ids_convert
 src/util/irep_ids_convert.exe
+build/
 
 *.pyc
 

regression/cbmc-java/ArithmeticException6/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--java-throw-runtime-exceptions --function ArithmeticExceptionTest.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$

regression/cbmc-java/LocalVarTable5/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---show-goto-functions
+--show-goto-functions --function test.main
 dead anonlocal::1i
 dead anonlocal::2i
 dead anonlocal::3a

regression/cbmc-java/NondetInitValidate/Test.class renamed to regression/cbmc-java/NondetInit/Test.class

@@ -0,0 +1,16 @@
+import org.cprover.CProver;
+
+class Test {
+
+    int[] arr;
+
+    void cproverNondetInitialize() {
+        CProver.assume(arr != null && arr.length == 1);
+        // The following access should now be legal:
+        arr[0] = 100;
+    }
+
+    public static void main(Test nondetInput) {
+    }
+
+}

regression/cbmc-java/NondetInitValidate/Test.java renamed to regression/cbmc-java/NondetInit/Test.java

@@ -0,0 +1,4 @@
+CORE
+Test.class
+--function Test.main
+^VERIFICATION SUCCESSFUL$

regression/cbmc-java/NondetInitValidate/test.desc renamed to regression/cbmc-java/NondetInit/test.desc

@@ -0,0 +1,23 @@
+import org.cprover.CProver;
+
+class Test {
+
+    int[] arr;
+
+    void cproverNondetInitialize() {
+        CProver.assume(arr != null && arr.length == 1);
+        // The following access should now be legal:
+        arr[0] = 100;
+    }
+
+    public static void main(Subclass nondetInput) {
+        // The condition enforced by cproverNondetInitialize should hold
+        // even though the parameter is a subtype of Test, not directly an
+        // instance of Test itself.
+        if(nondetInput != null)
+            assert nondetInput.arr.length == 1;
+    }
+
+}
+
+class Subclass extends Test { }

regression/cbmc-java/NondetInitValidate/test_lazy.desc renamed to regression/cbmc-java/NondetInit/test_lazy.desc

@@ -0,0 +1,4 @@
+CORE
+Test.class
+--function Test.main
+^VERIFICATION SUCCESSFUL$

regression/cbmc-java/NondetInit2/Test.class

@@ -1,6 +1,6 @@
 CORE
 VarLengthArrayTrace1.class
---trace
+--trace --function VarLengthArrayTrace1.main
 ^EXIT=10$
 ^SIGNAL=0$
 dynamic_3_array\[1.*\]=10

regression/cbmc-java/NondetInit2/Test.java

@@ -1,6 +1,6 @@
 CORE
 arrayread1.class
---unwind 3 --no-propagation
+--unwind 3 --no-propagation --function arrayread1.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-java/NondetInit2/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-java/NondetInit3/Subclass.class

@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions
+--java-throw-runtime-exceptions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-java/NondetInit3/Test.class

@@ -0,0 +1,9 @@
+CORE
+test.class
+--show-symbol-table
+^EXIT=0$
+^SIGNAL=0$
+^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<clinit\>\:\(\)V$
+--
+--
+tests that the core models are  being loaded by checking if the static initializer for the CProver class was

regression/cbmc-java/NondetInit3/Test.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+class test
+{
+  public static void main(String[] args)
+  {
+    int i=CProver.nondetInt();
+    assert(i!=0);
+  }
+}
+

regression/cbmc-java/NondetInit3/test.desc

@@ -1,6 +1,6 @@
 CORE
 Break.class
---show-goto-functions
+--show-goto-functions --function Break.main
 ^EXIT=0$
 ^SIGNAL=0$
 dead i;

regression/cbmc-java/VarLengthArrayTrace1/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

regression/cbmc-java/arrayread1/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.class
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test verifies that catches are executed in the correct order
+

regression/cbmc-java/cast_null1/test.desc

@@ -0,0 +1,31 @@
+class A extends RuntimeException {}
+class B extends A {}
+
+// This test verifies that catches are executed in the correct order
+public class test {
+  public static void main (String args[]) {
+    int i = 0;
+    try {
+      try {
+        throw new A();
+      }
+      catch(A exc) {
+        i++;
+        throw new B();
+      }
+      finally
+      {
+        // Make sure A threw into the catch
+        assert(i==1);
+        i++;
+      }
+    }
+    catch(B exc) {
+      // Make sure finally was executed
+      assert(i==2);
+      i++;
+    }
+    // Make sure B was rethrown by finally
+    assert(i==3);
+  }
+}

regression/cbmc-java/cast_null2/test.desc

@@ -0,0 +1,7 @@
+CORE
+test.class
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
+--
+Tests embedded try-catch-finally to ensure the catching order is correct

regression/cbmc-java/coreModels/test.class

@@ -0,0 +1,54 @@
+import org.cprover.CProver;
+class A extends RuntimeException {}
+class B extends A {}
+
+// This test verifies that catches are executed in the correct order
+public class test {
+  public static void main (String args[]) {
+    int i = 0;
+    int j = 0;
+    try {
+      try {
+        try {
+          if (CProver.nondetBoolean()) throw new A();
+          else throw new B();
+        }
+        catch(B exc) {
+          i++;
+        }
+        catch(A exc) {
+          i++;
+          throw new B();
+        }
+        finally
+        {
+          // Make sure A threw into the catch
+          assert(i==1);
+          i++;
+        }
+        assert(i==2);
+        // Account for the rethrow in finally
+        j++;
+      }
+      catch(B exc) {
+        // Make sure finally was executed
+        assert(i==2);
+        i++;
+        throw new B();
+      }
+      finally 
+      {
+        assert ((i+j) == 3);
+      }
+      // Account for the rethrow in finally
+      j++;
+    }
+    catch(B exc)
+    {
+      i++;
+    }
+    // Make sure B was rethrown by finally when A was thrown
+    // or if B was thrown there was no rethrow
+    assert(i+j == 4);
+  }
+}

regression/cbmc-java/coreModels/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-java/coreModels/test.java

@@ -7,5 +7,5 @@ Gn.class
 .*file Gn.java line 9 function java::Gn.foo1:\(LGn;\)V bytecode-index 1 block 1: FAILED
 .*file Gn.java line 10 function java::Gn.foo1:\(LGn;\)V bytecode-index 4 block 2: FAILED
 .*file Gn.java line 11 function java::Gn.foo1:\(LGn;\)V bytecode-index 5 block 3: FAILED
-.*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block 1: SATISFIED
+.*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block 2: SATISFIED
 --

regression/cbmc-java/destructor1/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---show-symbol-table
+--show-symbol-table --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^pc7:

regression/cbmc-java/exceptions22/test.desc

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

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--function Test.main
+^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/exceptions26/B.class

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

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

regression/cbmc-java/exceptions26/test.desc

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

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.main
+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/exceptions27/A.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/exceptions27/B.class

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

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