diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/Bar.class b/jbmc/regression/jbmc/deterministic_assignments_json/Bar.class new file mode 100644 index 00000000000..5227989a8fa Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/Bar.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/Bar.java b/jbmc/regression/jbmc/deterministic_assignments_json/Bar.java new file mode 100644 index 00000000000..f17871f7c4e --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/Bar.java @@ -0,0 +1,12 @@ +public class Bar { + private static int c = Util.setTo(10); + private int x; + + public Bar(int x) { + this.x = Util.setTo(x); + } + + public int get() { + return x + c; + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/Color.class b/jbmc/regression/jbmc/deterministic_assignments_json/Color.class new file mode 100644 index 00000000000..ca4f20ac1bf Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/Color.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/Color.java b/jbmc/regression/jbmc/deterministic_assignments_json/Color.java new file mode 100644 index 00000000000..bd365306a56 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/Color.java @@ -0,0 +1,29 @@ +public enum Color { + RED(false), + BLUE(false), + GREEN(false), + WHITE(true), + GREY(true), + BLACK(true); + + private boolean grayscale; + + Color(boolean grayscale) { + this.grayscale = grayscale; + } + + public boolean isGrayscale() { + return grayscale; + } + + public static Color enumField = Color.WHITE; + public static void testEnumInOwnTypePass() { + assert enumField == Color.WHITE && enumField.name().equals("WHITE") && + enumField.ordinal() == 3 && enumField.isGrayscale(); + } + public static void testEnumInOwnTypeFail() { + assert enumField != Color.WHITE || !enumField.name().equals("WHITE") || + enumField.ordinal() != 3 || !enumField.isGrayscale(); + } + +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/Foo.class b/jbmc/regression/jbmc/deterministic_assignments_json/Foo.class new file mode 100644 index 00000000000..19da52a769c Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/Foo.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/Foo.java b/jbmc/regression/jbmc/deterministic_assignments_json/Foo.java new file mode 100644 index 00000000000..5ea07c7f506 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/Foo.java @@ -0,0 +1,14 @@ +public class Foo { + private int i; + private Bar b; + + public Foo(int i, int x) + { + this.i = Util.setTo(i); + this.b = new Bar(x); + } + + public int get() { + return i + b.get(); + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementation.class b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementation.class new file mode 100644 index 00000000000..d672a271e03 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementation.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementation.java b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementation.java new file mode 100644 index 00000000000..8d65a17bdba --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementation.java @@ -0,0 +1,20 @@ +public class GenericImplementation implements GenericInterface { + + T[] elements; + + public GenericImplementation(T[] array) { + elements = array; + } + + public int size() { + return elements.length; + } + + public T first() { + return elements[0]; + } + + public int num() { + return 5; + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationLess.class b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationLess.class new file mode 100644 index 00000000000..93ae27db4fb Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationLess.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationLess.java b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationLess.java new file mode 100644 index 00000000000..b9557f0e741 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationLess.java @@ -0,0 +1,21 @@ +public class GenericImplementationLess implements GenericInterface { + + Foo[] elements; + + public GenericImplementationLess(Foo[] array) { + elements = array; + } + + public int size() { + return elements.length; + } + + public Foo first() { + return elements[0]; + } + + public int num() { + return first().get(); + } + +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationMore.class b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationMore.class new file mode 100644 index 00000000000..62009b5efb3 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationMore.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationMore.java b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationMore.java new file mode 100644 index 00000000000..5825fd5a248 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationMore.java @@ -0,0 +1,25 @@ +public class GenericImplementationMore implements GenericInterface { + + T[] elementsT; + U[] elementsU; + + public GenericImplementationMore(T[] arrayT, U[] arrayU) { + elementsT = arrayT; + elementsU = arrayU; + } + + public int size() { + return elementsT.length + elementsU.length; + } + + public T first() { + return elementsT[0]; + } + + public int num() { + if (elementsU[0] instanceof Bar) { + return ((Bar) elementsU[0]).get(); + } + return elementsU.length; + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationSimpleMore.class b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationSimpleMore.class new file mode 100644 index 00000000000..29804cce167 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationSimpleMore.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationSimpleMore.java b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationSimpleMore.java new file mode 100644 index 00000000000..2ba6b19b8d4 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationSimpleMore.java @@ -0,0 +1,22 @@ +public class GenericImplementationSimpleMore implements GenericInterface { + T t; + U u; + + public GenericImplementationSimpleMore(T t, U u) { + this.t = t; + this.u = u; + } + + public int size() { + return 2; + } + public T first() { + return t; + } + public int num() { + if (u instanceof Bar) { + return ((Bar) u).get(); + } + return 1; + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericInterface.class b/jbmc/regression/jbmc/deterministic_assignments_json/GenericInterface.class new file mode 100644 index 00000000000..3cab9c26421 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/GenericInterface.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericInterface.java b/jbmc/regression/jbmc/deterministic_assignments_json/GenericInterface.java new file mode 100644 index 00000000000..73166ff3fc6 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/GenericInterface.java @@ -0,0 +1,8 @@ +public interface GenericInterface { + + int size(); + + T first(); + + int num(); +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericMultiDim.class b/jbmc/regression/jbmc/deterministic_assignments_json/GenericMultiDim.class new file mode 100644 index 00000000000..4f005374763 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/GenericMultiDim.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericMultiDim.java b/jbmc/regression/jbmc/deterministic_assignments_json/GenericMultiDim.java new file mode 100644 index 00000000000..a43017e6fe1 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/GenericMultiDim.java @@ -0,0 +1,11 @@ +public class GenericMultiDim { + + public K key; + public V value; + + public GenericMultiDim(K k, V v) { + key = k; + value = v; + } + +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericType.class b/jbmc/regression/jbmc/deterministic_assignments_json/GenericType.class new file mode 100644 index 00000000000..4ad4b3e68fd Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/GenericType.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/GenericType.java b/jbmc/regression/jbmc/deterministic_assignments_json/GenericType.java new file mode 100644 index 00000000000..974026b7007 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/GenericType.java @@ -0,0 +1,8 @@ +public class GenericType { + public T field; + + public GenericType(T f) { + field = f; + } + +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractClass.class b/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractClass.class new file mode 100644 index 00000000000..4603265861b Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractClass.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractClass.java b/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractClass.java new file mode 100644 index 00000000000..355838eb729 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractClass.java @@ -0,0 +1,8 @@ +public abstract class MyAbstractClass { + + abstract public int num(); + + public int concreteNum() { + return 11; + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationA.class b/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationA.class new file mode 100644 index 00000000000..314d4567148 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationA.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationA.java b/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationA.java new file mode 100644 index 00000000000..ec1b54ac866 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationA.java @@ -0,0 +1,5 @@ +public class MyAbstractImplementationA extends MyAbstractClass { + public int num() { + return concreteNum(); + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationB.class b/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationB.class new file mode 100644 index 00000000000..facaa221d5a Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationB.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationB.java b/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationB.java new file mode 100644 index 00000000000..9f73fb87cc9 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationB.java @@ -0,0 +1,5 @@ +public class MyAbstractImplementationB extends MyAbstractClass { + public int num() { + return 2 * concreteNum(); + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyClassWithInheritedFields.class b/jbmc/regression/jbmc/deterministic_assignments_json/MyClassWithInheritedFields.class new file mode 100644 index 00000000000..e45dd02699b Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MyClassWithInheritedFields.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyClassWithInheritedFields.java b/jbmc/regression/jbmc/deterministic_assignments_json/MyClassWithInheritedFields.java new file mode 100644 index 00000000000..0f1f6e420cd --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MyClassWithInheritedFields.java @@ -0,0 +1,10 @@ +public class MyClassWithInheritedFields extends MyParent { + int childField = Util.setTo(4); + + public static int sum(MyClassWithInheritedFields myTemp) { + int sum = myTemp.childField + myTemp.parentField; + if (sum == 10) + return sum; + return sum; + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyConcreteClass.class b/jbmc/regression/jbmc/deterministic_assignments_json/MyConcreteClass.class new file mode 100644 index 00000000000..2d15c1c0b09 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MyConcreteClass.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyConcreteClass.java b/jbmc/regression/jbmc/deterministic_assignments_json/MyConcreteClass.java new file mode 100644 index 00000000000..2122509f9f1 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MyConcreteClass.java @@ -0,0 +1,8 @@ +public class MyConcreteClass { + + public static int numField = Util.setTo(10); + + public int num() { + return numField; + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationA.class b/jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationA.class new file mode 100644 index 00000000000..08f8557fc4e Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationA.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationA.java b/jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationA.java new file mode 100644 index 00000000000..588528c91b7 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationA.java @@ -0,0 +1,6 @@ +public class MyImplementationA implements MyInterface { + int field = Util.setTo(11); + public int num() { + return field; + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationB.class b/jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationB.class new file mode 100644 index 00000000000..7eff86ac5fb Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationB.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationB.java b/jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationB.java new file mode 100644 index 00000000000..11f33bab45f --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationB.java @@ -0,0 +1,6 @@ +public class MyImplementationB implements MyInterface { + int field = Util.setTo(22); + public int num() { + return field; + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyInterface.class b/jbmc/regression/jbmc/deterministic_assignments_json/MyInterface.class new file mode 100644 index 00000000000..7c3c8051c24 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MyInterface.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyInterface.java b/jbmc/regression/jbmc/deterministic_assignments_json/MyInterface.java new file mode 100644 index 00000000000..632d57c2be8 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MyInterface.java @@ -0,0 +1,5 @@ +public interface MyInterface { + + int num(); + +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerA.class b/jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerA.class new file mode 100644 index 00000000000..fbfc1e9b332 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerA.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerA.java b/jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerA.java new file mode 100644 index 00000000000..ddc0d3484ae --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerA.java @@ -0,0 +1,6 @@ +public class MyInterfaceContainerA { + MyImplementationA field = new MyImplementationA(); + public MyInterface getField() { + return field; + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerB.class b/jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerB.class new file mode 100644 index 00000000000..07ed62805f2 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerB.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerB.java b/jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerB.java new file mode 100644 index 00000000000..fc750a96a00 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerB.java @@ -0,0 +1,6 @@ +public class MyInterfaceContainerB { + MyInterface field = new MyImplementationB(); + public MyInterface getField() { + return field; + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyParent.class b/jbmc/regression/jbmc/deterministic_assignments_json/MyParent.class new file mode 100644 index 00000000000..0f99712c26b Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MyParent.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MyParent.java b/jbmc/regression/jbmc/deterministic_assignments_json/MyParent.java new file mode 100644 index 00000000000..0cbff7db744 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MyParent.java @@ -0,0 +1,4 @@ +public class MyParent { + int parentField = Util.setTo(3); + String parentString = "parent"; +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MySubclassA.class b/jbmc/regression/jbmc/deterministic_assignments_json/MySubclassA.class new file mode 100644 index 00000000000..1a81e1117d4 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MySubclassA.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MySubclassA.java b/jbmc/regression/jbmc/deterministic_assignments_json/MySubclassA.java new file mode 100644 index 00000000000..88cbfe8bac5 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MySubclassA.java @@ -0,0 +1,6 @@ +public class MySubclassA extends MyConcreteClass { + @Override + public int num() { + return 2 * super.num(); + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MySubclassB.class b/jbmc/regression/jbmc/deterministic_assignments_json/MySubclassB.class new file mode 100644 index 00000000000..ec9f1e73f24 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/MySubclassB.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/MySubclassB.java b/jbmc/regression/jbmc/deterministic_assignments_json/MySubclassB.java new file mode 100644 index 00000000000..0ddbcec475b --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/MySubclassB.java @@ -0,0 +1,6 @@ +public class MySubclassB extends MyConcreteClass { + @Override + public int num() { + return 3 * super.num(); + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/OtherClass.class b/jbmc/regression/jbmc/deterministic_assignments_json/OtherClass.class new file mode 100644 index 00000000000..7fdd170471a Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/OtherClass.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/OtherClass.java b/jbmc/regression/jbmc/deterministic_assignments_json/OtherClass.java new file mode 100644 index 00000000000..04032e4b79e --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/OtherClass.java @@ -0,0 +1,4 @@ +public class OtherClass { + + public static Foo otherField = new Foo(12, 24); +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/README b/jbmc/regression/jbmc/deterministic_assignments_json/README new file mode 100644 index 00000000000..6137a049fa2 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/README @@ -0,0 +1,10 @@ +This directory contains tests for the --static-values feature: reading initial +values of static fields from a JSON file. +Most of the tests are in StaticValues.java, some more tests are included in +Color.java, and all other classes are used to create instances of various kinds +of objects to use in the tests. +The initial static field values are read from the file clinit-state.json. +The script generate-json.sh (which calls org.cprover.JsonGenerator in the Maven +project) can be used to generate output similar to the contents of +clinit-state.json (with slightly less pretty-printing/newlines, which are not +supported in the custom writers and were manually added to clinit-state.json). diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/StaticParent.class b/jbmc/regression/jbmc/deterministic_assignments_json/StaticParent.class new file mode 100644 index 00000000000..0bf39dbc35b Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/StaticParent.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/StaticParent.java b/jbmc/regression/jbmc/deterministic_assignments_json/StaticParent.java new file mode 100644 index 00000000000..5db1c0fb9e9 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/StaticParent.java @@ -0,0 +1,3 @@ +public class StaticParent { + protected static int inheritedStatic = Util.setTo(10); +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.class b/jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.class new file mode 100644 index 00000000000..c3f257dfd4d Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.java b/jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.java new file mode 100644 index 00000000000..753fb1db4c0 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.java @@ -0,0 +1,419 @@ +public class StaticValues extends StaticParent { + + // primitive types + public static int intField = Util.fib(15); + public static void testIntPass() { + assert intField == 610; + } + public static void testIntFail() { + assert intField != 610; + } + + public static char asciiCharField = 'a'; + public static char hexCharField = '\u0001'; + public static char chineseCharField = '字'; + public static char specialCharField = '\n'; + public static char fibCharField = (char) Util.fib(15); + public static void testAsciiCharPass() { + assert asciiCharField == 'a'; + } + public static void testAsciiCharFail() { + assert asciiCharField != 'a'; + } + public static void testHexCharPass() { + assert hexCharField == '\u0001'; + } + public static void testHexCharFail() { + assert hexCharField != '\u0001'; + } + public static void testChineseCharPass() { + assert chineseCharField == '字'; + } + public static void testChineseCharFail() { + assert chineseCharField != '字'; + } + public static void testSpecialCharPass() { + assert specialCharField == '\n'; + } + public static void testSpecialCharFail() { + assert specialCharField != '\n'; + } + public static void testFibCharPass() { + assert fibCharField == 'ɢ'; + } + public static void testFibCharFail() { + assert fibCharField != 'ɢ'; + } + + public static byte byteField = (byte) Util.fib(15); + public static void testBytePass() { + assert byteField == 98; + } + public static void testByteFail() { + assert byteField != 98; + } + + public static boolean booleanField = Util.fib(15) == 610; + public static void testBooleanPass() { + assert booleanField; + } + public static void testBooleanFail() { + assert !booleanField; + } + + public static long longField = Util.fib(15) + 9223372036854775197L; + public static void testLongPass() { + assert longField == 9223372036854775807L; + } + public static void testLongFail() { + assert longField != 9223372036854775807L; + } + + public static short shortField = (short) Util.fib(6); + public static void testShortPass() { + assert shortField == 8; + } + public static void testShortFail() { + assert shortField != 8; + } + + public static double doubleField = Util.fib(6) + 65.23; + public static void testDoublePass() { + assert doubleField == 73.23; + } + public static void testDoubleFail() { + assert doubleField != 73.23; + } + + public static float floatField = Util.fib(6) + 45.12f; + public static void testFloatPass() { + assert floatField == 53.12f; + } + public static void testFloatFail() { + assert floatField != 53.12f; + } + + // null reference types + public static Foo nullField = null; + public static void testNullPass() { + assert nullField == null; + } + public static void testNullFail() { + assert nullField != null; + } + + // non-null reference types + public static final Foo foo = new Foo(3,4); + public static void testReferencePass() { + assert intField - foo.get() == 593; + } + public static void testReferenceFail() { + assert intField - foo.get() != 593; + } + + // reference-equal reference types + public static Foo referenceToOther = foo; + public static void testReferenceToOtherPass() { + assert intField - referenceToOther.get() == 593 && referenceToOther == foo; + } + public static void testReferenceToOtherFail() { + assert intField - referenceToOther.get() != 593 || referenceToOther != foo; + } + + // reference-equal reference types in different classes + public static Foo referenceToOtherClass = OtherClass.otherField; + // #KNOWNBUG + public static void testReferenceToOtherClassPass() { + assert referenceToOtherClass.get() == 46 && referenceToOtherClass == OtherClass.otherField; + } + // #KNOWNBUG + public static void testReferenceToOtherClassFail() { + assert referenceToOtherClass.get() != 46 || referenceToOtherClass != OtherClass.otherField; + } + + // arrays + public static int[] primitiveArrayField = {Util.fib(5), Util.fib(10), Util.fib(15)}; + public static void testPrimitiveArrayPass() { + assert primitiveArrayField.length == 3 && primitiveArrayField[0] == 5 && + primitiveArrayField[1] == 55 && primitiveArrayField[2] == 610; + } + public static void testPrimitiveArrayFail() { + assert primitiveArrayField.length != 3 || primitiveArrayField[0] != 5 || + primitiveArrayField[1] != 55 || primitiveArrayField[2] != 610; + } + public static void testPrimitiveArraySumPass() { + int sum = 0; + for (int i : primitiveArrayField) { + sum += i; + } + assert sum == 670; + } + public static void testPrimitiveArraySumFail() { + int sum = 0; + for (int i : primitiveArrayField) { + sum += i; + } + assert sum != 670; + } + + public static int[] referenceToPrimitiveArray = primitiveArrayField; + public static void testReferenceToPrimitiveArrayPass() { + assert referenceToPrimitiveArray == primitiveArrayField; + } + public static void testReferenceToPrimitiveArrayFail() { + assert referenceToPrimitiveArray != primitiveArrayField; + } + + public static char[] charArrayField = { + '\u0000', '\u0001', '\u0041', 'B', '?', ';', '\u2FC3' + }; + public static void testCharArrayPass() { + assert charArrayField.length == 7 && charArrayField[0] == '\u0000' && + charArrayField[1] == '\u0001' && charArrayField[2] == '\u0041' && + charArrayField[3] == 'B' && charArrayField[4] == '?' && charArrayField[5] == ';' && + charArrayField[6] == '\u2FC3'; + } + public static void testCharArrayFail() { + assert charArrayField.length != 7 || charArrayField[0] != '\u0000' || + charArrayField[1] != '\u0001' || charArrayField[2] != '\u0041' || + charArrayField[3] != 'B' || charArrayField[4] != '?' || charArrayField[5] != ';' || + charArrayField[6] != '\u2FC3'; + } + + + public static Foo[] referenceArrayField = {new Foo(5, -1), new Foo(6, 7)}; + public static void testReferenceArrayPass() { + assert referenceArrayField.length == 2 && referenceArrayField[0].get() == 14 && + referenceArrayField[1].get() == 23; + } + public static void testReferenceArrayFail() { + assert referenceArrayField.length != 2 || referenceArrayField[0].get() != 14 || + referenceArrayField[1].get() != 23; + } + + public static Foo[] referenceToReferenceArray = referenceArrayField; + public static void testReferenceToReferenceArrayPass() { + assert referenceToReferenceArray == referenceArrayField; + } + public static void testReferenceToReferenceArrayFail() { + assert referenceToReferenceArray != referenceArrayField; + } + + // Strings + public static String stringField = Util.repeat("hello! ", 6); + public static void testStringPass() { + assert stringField.equals("hello! hello! hello! hello! hello! hello! "); + } + public static void testStringFail() { + assert !stringField.equals("hello! hello! hello! hello! hello! hello! "); + } + + public static String referenceToString = stringField; + public static void testReferenceToStringPass1() { + assert referenceToString.equals("hello! hello! hello! hello! hello! hello! "); + } + // #KNOWNBUG + public static void testReferenceToStringPass2() { + assert referenceToString == stringField; + } + public static void testReferenceToStringFail1() { + assert !referenceToString.equals("hello! hello! hello! hello! hello! hello! "); + } + // #KNOWNBUG + public static void testReferenceToStringFail2() { + assert referenceToString != stringField; + } + + public static StringContainer stringContainerField = new StringContainer(); + public static void testStringContainerPass() { + assert stringContainerField.contained.equals("abcabcabcabcabc"); + } + public static void testStringContainerFail() { + assert !stringContainerField.contained.equals("abcabcabcabcabc"); + } + + // StringBuilder, StringBuffer + public static StringBuilder stringBuilderField = new StringBuilder(Util.repeat("a", 8)); + public static void testStringBuilderPass() { + assert stringBuilderField.toString().equals("aaaaaaaa"); + } + public static void testStringBuilderFail() { + assert !stringBuilderField.toString().equals("aaaaaaaa"); + } + + public static StringBuffer stringBufferField = new StringBuffer(Util.repeat("b", 6)); + public static void testStringBufferPass() { + assert stringBufferField.toString().equals("bbbbbb"); + } + public static void testStringBufferFail() { + assert !stringBufferField.toString().equals("bbbbbb"); + } + + // generics + public static GenericType genericField = new GenericType<>(new Foo(3, 4)); + public static void testGenericPass() { + assert genericField.field.get() == 17; + } + public static void testGenericFail() { + assert genericField.field.get() != 17; + } + + public static GenericMultiDim genericMultiDimField = + new GenericMultiDim<>(new Foo(2, 8), new Bar(4)); + public static void testGenericMultiDimPass() { + assert genericMultiDimField.key.get() == 20 && genericMultiDimField.value.get() == 14; + } + public static void testGenericMultiDimFail() { + assert genericMultiDimField.key.get() != 20 || genericMultiDimField.value.get() != 14; + } + + // enums + public static Color enumField = Color.WHITE; + public static void testEnumPass() { + assert enumField == Color.WHITE && enumField.name().equals("WHITE") && + enumField.ordinal() == 3 && enumField.isGrayscale(); + } + public static void testEnumFail() { + assert enumField != Color.WHITE || !enumField.name().equals("WHITE") || + enumField.ordinal() != 3 || !enumField.isGrayscale(); + } + + // inheritance - static field with inherited fields + public static MyClassWithInheritedFields myInheriting = new MyClassWithInheritedFields(); + public static void testSubclassFieldPass() { + assert myInheriting.childField + myInheriting.parentField + myInheriting.parentString.length() == 13; + } + public static void testSubclassFieldFail() { + assert myInheriting.childField + myInheriting.parentField + myInheriting.parentString.length() != 13; + } + + // inheritance - static field inherited from parent + public static void testInheritedFieldPass() { + assert inheritedStatic == 10; + } + public static void testInheritedFieldFail() { + assert inheritedStatic != 10; + } + + // inheritance - different implementing classes of an interface + public static MyInterface interfaceFirst = new MyImplementationA(); + public static void testInterfaceFirstPass() { + assert interfaceFirst.num() == 11; + } + public static void testInterfaceFirstFail() { + assert interfaceFirst.num() != 11; + } + + public static MyInterface interfaceSecond = new MyImplementationB(); + public static void testInterfaceSecondPass() { + assert interfaceSecond.num() == 22; + } + public static void testInterfaceSecondFail() { + assert interfaceSecond.num() != 22; + } + + public static MyInterfaceContainerA interfaceContainerFirst = new MyInterfaceContainerA(); + public static void testInterfaceContainerFirstPass() { + assert interfaceContainerFirst.getField().num() == 11; + } + public static void testInterfaceContainerFirstFail() { + assert interfaceContainerFirst.getField().num() != 11; + } + + public static MyInterfaceContainerB interfaceContainerSecond = new MyInterfaceContainerB(); + public static void testInterfaceContainerSecondPass() { + assert interfaceContainerSecond.getField().num() == 22; + } + public static void testInterfaceContainerSecondFail() { + assert interfaceContainerSecond.getField().num() != 22; + } + + // inheritance - different implementing classes of an abstract class + public static MyAbstractClass abstractClassFirst = new MyAbstractImplementationA(); + public static void testAbstractClassFirstPass() { + assert abstractClassFirst.num() == 11; + } + public static void testAbstractClassFirstFail() { + assert abstractClassFirst.num() != 11; + } + + public static MyAbstractClass abstractClassSecond = new MyAbstractImplementationB(); + public static void testAbstractClassSecondPass() { + assert abstractClassSecond.num() == 22; + } + public static void testAbstractClassSecondFail() { + assert abstractClassSecond.num() != 22; + } + + // inheritance - different subclasses of a concrete class + public static MyConcreteClass concreteClassFirst = new MySubclassA(); + public static void testConcreteClassFirstPass() { + assert concreteClassFirst.num() == 20; + } + public static void testConcreteClassFirstFail() { + assert concreteClassFirst.num() != 20; + } + + public static MyConcreteClass concreteClassSecond = new MySubclassB(); + public static void testConcreteClassSecondPass() { + assert concreteClassSecond.num() == 30; + } + public static void testConcreteClassSecondFail() { + assert concreteClassSecond.num() != 30; + } + + // inheritance with generics + public static GenericInterface genericInterfaceSame = + new GenericImplementation<>(new Foo[]{new Foo(4, 6), new Foo(12, 14)}); + public static void testGenericInterfaceSamePass() { + assert genericInterfaceSame.size() == 2 && genericInterfaceSame.first().get() == 20 && + genericInterfaceSame.num() == 5; + } + public static void testGenericInterfaceSameFail() { + assert genericInterfaceSame.size() != 2 || genericInterfaceSame.first().get() != 20 || + genericInterfaceSame.num() != 5; + } + + public static GenericInterface genericInterfaceSimpleMore = + new GenericImplementationSimpleMore(new Foo(2, 6), new Bar(11)); + public static void testGenericInterfaceSimpleMorePass() { + assert genericInterfaceSimpleMore.size() == 2 && genericInterfaceSimpleMore.first().get() == 18 + && genericInterfaceSimpleMore.num() == 21; + } + public static void testGenericInterfaceSimpleMoreFail() { + assert genericInterfaceSimpleMore.size() != 2 || genericInterfaceSimpleMore.first().get() != 18 + || genericInterfaceSimpleMore.num() != 21; + } + + public static GenericInterface genericInterfaceMore = + new GenericImplementationMore(new Foo[]{new Foo(1, 5)}, new Bar[]{new Bar(15), new Bar(12)}); + public static void testGenericInterfaceMorePass() { + assert genericInterfaceMore.size() == 3 && genericInterfaceMore.first().get() == 16 && + genericInterfaceMore.num() == 25; + } + public static void testGenericInterfaceMoreFail() { + assert genericInterfaceMore.size() != 3 || genericInterfaceMore.first().get() != 16 || + genericInterfaceMore.num() != 25; + } + + public static GenericInterface genericInterfaceLess = + new GenericImplementationLess(new Foo[]{new Foo(1, 5)}); + public static void testGenericInterfaceLessPass() { + assert genericInterfaceLess.size() == 1 && genericInterfaceLess.first().get() == 16 && + genericInterfaceLess.num() == 16; + } + public static void testGenericInterfaceLessFail() { + assert genericInterfaceLess.size() != 1 || genericInterfaceLess.first().get() != 16 || + genericInterfaceLess.num() != 16; + } + + public static GenericType genericWithInterfaceField = + new GenericType(new MyImplementationA()); + public static void testGenericWithInterfaceFieldPass() { + assert genericWithInterfaceField.field.num() == 11; + } + public static void testGenericWithInterfaceFieldFail() { + assert genericWithInterfaceField.field.num() != 11; + } + +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/StringContainer.class b/jbmc/regression/jbmc/deterministic_assignments_json/StringContainer.class new file mode 100644 index 00000000000..29627c47f46 Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/StringContainer.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/StringContainer.java b/jbmc/regression/jbmc/deterministic_assignments_json/StringContainer.java new file mode 100644 index 00000000000..def0b5aff8f --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/StringContainer.java @@ -0,0 +1,3 @@ +public class StringContainer { + String contained = Util.repeat("abc", 5); +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/Util.class b/jbmc/regression/jbmc/deterministic_assignments_json/Util.class new file mode 100644 index 00000000000..b1499e7021d Binary files /dev/null and b/jbmc/regression/jbmc/deterministic_assignments_json/Util.class differ diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/Util.java b/jbmc/regression/jbmc/deterministic_assignments_json/Util.java new file mode 100644 index 00000000000..9b398ea754b --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/Util.java @@ -0,0 +1,38 @@ +/** + * Utility methods for tests related to retrieving (deterministic) initial + * values of static fields from a JSON file. + * These methods are generally used to initialize static fields using a loop, so + * without the --static-values option, JBMC would need a very high unwind limit. + * With the initial values given in a JSON file, lower unwind values can be + * used. + */ +public class Util { + + public static int fib(int num) { + int zeroFib = 0; + int oneFib = 1; + for (int i = 0; i < num; i++) { + int temp = oneFib; + oneFib = temp + zeroFib; + zeroFib = temp; + } + return zeroFib; + } + + public static int setTo(int value) { + int sign = value >= 0 ? 1 : -1; + int i = 0; + for (; i < sign * value; i++) { + } + return sign * i; + } + + public static String repeat(String part, int copies) { + StringBuilder builder = new StringBuilder(); + for (int i = 0; i < copies; i++) { + builder.append(part); + } + return builder.toString(); + } + +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/clinit-state.json b/jbmc/regression/jbmc/deterministic_assignments_json/clinit-state.json new file mode 100644 index 00000000000..8d341195fa4 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/clinit-state.json @@ -0,0 +1,424 @@ +{ + "Bar":{ + "c":{ + "@type":"java.lang.Integer", + "value":10 + } + }, + "MySubclassB":{ + "numField":{ + "@type":"java.lang.Integer", + "value":10 + } + }, + "MySubclassA":{ + "numField":{ + "@type":"java.lang.Integer", + "value":10 + } + }, + "Color":{ + "RED":{ + "@type":"Color", + "name":"RED", + "ordinal":0, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":false + } + }, + "WHITE":{ + "@type":"Color", + "name":"WHITE", + "ordinal":3, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":true + } + }, + "BLUE":{ + "@type":"Color", + "name":"BLUE", + "ordinal":1, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":false + } + }, + "BLACK":{ + "@type":"Color", + "name":"BLACK", + "ordinal":5, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":true + } + }, + "GREEN":{ + "@type":"Color", + "name":"GREEN", + "ordinal":2, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":false + } + }, + "GREY":{ + "@type":"Color", + "name":"GREY", + "ordinal":4, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":true + } + }, + "$VALUES":{ + "@type":"[LColor;", + "@items":[ + { + "name":"RED", + "ordinal":0, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":false + } + }, + { + "name":"BLUE", + "ordinal":1, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":false + } + }, + { + "name":"GREEN", + "ordinal":2, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":false + } + }, + { + "name":"WHITE", + "ordinal":3, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":true + } + }, + { + "name":"GREY", + "ordinal":4, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":true + } + }, + { + "name":"BLACK", + "ordinal":5, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":true + } + } + ] + }, + "enumField":{ + "@type":"Color", + "name":"WHITE", + "ordinal":3, + "grayscale":{ + "@type":"java.lang.Boolean", + "value":true + } + } + }, + "MyConcreteClass":{ + "numField":{ + "@type":"java.lang.Integer", + "value":10 + } + }, + "StaticParent":{ + "inheritedStatic":{ + "@type":"java.lang.Integer", + "value":10 + } + }, + "StaticValues":{ + "floatField":{ + "@type":"java.lang.Float", + "value":53.12 + }, + "interfaceFirst":{ + "@type":"MyImplementationA", + "field":11 + }, + "doubleField":{ + "@type":"java.lang.Double", + "value":73.23 + }, + "genericInterfaceLess":{ + "@type":"GenericImplementationLess", + "elements":[ + { + "i":1, + "b":{ + "x":5 + } + } + ] + }, + "referenceToOther":{ + "@id":4, + "@type":"Foo", + "i":3, + "b":{ + "x":4 + } + }, + "abstractClassFirst":{ + "@type":"MyAbstractImplementationA" + }, + "chineseCharField":{ + "@type":"java.lang.Character", + "value":"字" + }, + "booleanField":{ + "@type":"java.lang.Boolean", + "value":true + }, + "foo":{"@ref":4}, + "genericInterfaceMore":{ + "@type":"GenericImplementationMore", + "elementsT":{ + "@type":"[LFoo;", + "@items":[ + { + "i":1, + "b":{ + "x":5 + } + } + ] + }, + "elementsU":{ + "@type":"[LBar;", + "@items":[ + { + "x":15 + }, + { + "x":12 + } + ] + } + }, + "byteField":{ + "@type":"java.lang.Byte", + "value":98 + }, + "genericInterfaceSame":{ + "@type":"GenericImplementation", + "elements":{ + "@type":"[LFoo;", + "@items":[ + { + "i":4, + "b":{ + "x":6 + } + }, + { + "i":12, + "b":{ + "x":14 + } + } + ] + } + }, + "asciiCharField":{ + "@type":"java.lang.Character", + "value":"a" + }, + "stringContainerField":{ + "@type":"StringContainer", + "contained":"abcabcabcabcabc" + }, + "referenceArrayField":{ + "@id":3, + "@type":"[LFoo;", + "@items":[ + { + "i":5, + "b":{ + "x":-1 + } + }, + { + "i":6, + "b":{ + "x":7 + } + } + ] + }, + "intField":{ + "@type":"java.lang.Integer", + "value":610 + }, + "stringBufferField":{ + "@type":"java.lang.StringBuffer", + "value":"bbbbbb" + }, + "genericField":{ + "@type":"GenericType", + "field":{ + "@type":"Foo", + "i":3, + "b":{ + "x":4 + } + } + }, + "concreteClassFirst":{ + "@type":"MySubclassA" + }, + "referenceToPrimitiveArray":{ + "@id":2, + "@type":"[I", + "@items":[ + 5,55,610 + ] + }, + "interfaceSecond":{ + "@type":"MyImplementationB", + "field":22 + }, + "primitiveArrayField":{"@ref":2}, + "charArrayField":{ + "@type":"[C", + "@items":[ + "\u0000\u0001AB?;⿃" + ] + }, + "fibCharField":{ + "@type":"java.lang.Character", + "value":"ɢ" + }, + "longField":{ + "@type":"java.lang.Long", + "value":"9223372036854775807" + }, + "inheritedStatic":{ + "@type":"java.lang.Integer", + "value":10 + }, + "interfaceContainerFirst":{ + "@type":"MyInterfaceContainerA", + "field":{ + "field":11 + } + }, + "genericWithInterfaceField":{ + "@type":"GenericType", + "field":{ + "@type":"MyImplementationA", + "field":11 + } + }, + "concreteClassSecond":{ + "@type":"MySubclassB" + }, + "genericMultiDimField":{ + "@type":"GenericMultiDim", + "key":{ + "@type":"Foo", + "i":2, + "b":{ + "x":8 + } + }, + "value":{ + "@type":"Bar", + "x":4 + } + }, + "specialCharField":{ + "@type":"java.lang.Character", + "value":"\n" + }, + "hexCharField":{ + "@type":"java.lang.Character", + "value":"\u0001" + }, + "shortField":{ + "@type":"java.lang.Short", + "value":8 + }, + "genericInterfaceSimpleMore":{ + "@type":"GenericImplementationSimpleMore", + "t":{ + "@type":"Foo", + "i":2, + "b":{ + "x":6 + } + }, + "u":{ + "@type":"Bar", + "x":11 + } + }, + "interfaceContainerSecond":{ + "@type":"MyInterfaceContainerB", + "field":{ + "@type":"MyImplementationB", + "field":22 + } + }, + "referenceToReferenceArray":{"@ref":3}, + "stringBuilderField":{ + "@type":"java.lang.StringBuilder", + "value":"aaaaaaaa" + }, + "myInheriting":{ + "@type":"MyClassWithInheritedFields", + "childField":4, + "parentField":3, + "parentString":"parent" + }, + "nullField":null,"abstractClassSecond":{ + "@type":"MyAbstractImplementationB" + }, + "referenceToOtherClass":{ + "@id":1, + "@type":"Foo", + "i":12, + "b":{ + "x":24 + } + }, + "stringField":{ + "@type":"java.lang.String", + "value":"hello! hello! hello! hello! hello! hello! " + }, + "referenceToString":{ + "@type":"java.lang.String", + "value":"hello! hello! hello! hello! hello! hello! " + }, + "enumField":{ + "@type":"Color", + "name":"WHITE","ordinal":3,"grayscale":{ + "@type":"java.lang.Boolean", + "value":true + } + } + }, + "OtherClass":{ + "otherField":{"@ref":1} + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/generate-json.sh b/jbmc/regression/jbmc/deterministic_assignments_json/generate-json.sh new file mode 100755 index 00000000000..8d0c355bfe3 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/generate-json.sh @@ -0,0 +1,7 @@ +#!/bin/bash + +mvn package +java -cp target/jsonGenerator-1.0-SNAPSHOT-jar-with-dependencies.jar:. org.cprover.JsonGenerator +# The following command only works using GNU sed. +# (Remove all lines containing the string "StaticFieldMap" as they are not needed.) +sed -i '/StaticFieldMap/d' clinit-state.json diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/pom.xml b/jbmc/regression/jbmc/deterministic_assignments_json/pom.xml new file mode 100644 index 00000000000..376191f2ff7 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/pom.xml @@ -0,0 +1,63 @@ + + + 4.0.0 + jsonGenerator + jsonGenerator + 1.0-SNAPSHOT + + + + com.cedarsoftware + json-io + 4.10.1 + + + + + + + org.apache.maven.plugins + maven-assembly-plugin + + + package + + single + + + + + + com.diffblue.prototype.StaticInitState + + + + + jar-with-dependencies + + + + + + + org.apache.maven.plugins + maven-jar-plugin + + + + com.diffblue.prototype.StaticInitState + + + + + + + + + 1.8 + 1.8 + + + diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/EnumWriter.java b/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/EnumWriter.java new file mode 100644 index 00000000000..c37449755f6 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/EnumWriter.java @@ -0,0 +1,41 @@ +package org.cprover; + +import com.cedarsoftware.util.io.JsonWriter; + +import java.io.IOException; +import java.io.Writer; +import java.lang.reflect.Field; +import java.lang.reflect.Modifier; +import java.util.Map; + +import static com.cedarsoftware.util.io.JsonWriter.JsonClassWriterEx.Support.getWriter; + +public class EnumWriter implements JsonWriter.JsonClassWriterEx { + + /** + * Writes enums just like regular class types: by writing a key-value pair for all of its fields. + * The difference to the standard way of writing enums in json-io is that the latter ignores the + * ordinal field. + */ + public void write(Object obj, boolean showType, Writer output, Map args) + throws IOException { + JsonWriter outerWriter = getWriter(args); + Enum enumm = (Enum) obj; + output.write("\"name\":\"" + enumm.name() + "\""); + output.write(','); + output.write("\"ordinal\":" + enumm.ordinal()); + for (Field field : enumm.getDeclaringClass().getDeclaredFields()) { + if ((field.getModifiers() & Modifier.STATIC) != Modifier.STATIC) { + output.write(",\"" + field.getName() + "\":"); + try { + field.setAccessible(true); + outerWriter.writeImpl(field.get(enumm), true, true, true); + } + catch (IllegalAccessException ex) { + System.err.println("Could not access field " + field.getName() + " in class " + + enumm.getDeclaringClass() + "."); + } + } + } + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/JsonGenerator.java b/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/JsonGenerator.java new file mode 100644 index 00000000000..88ce6c71669 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/JsonGenerator.java @@ -0,0 +1,107 @@ +package org.cprover; + +import java.io.File; +import java.io.FileWriter; +import java.io.IOException; +import java.lang.reflect.Field; +import java.lang.reflect.Modifier; +import java.util.*; + +import com.cedarsoftware.util.io.JsonWriter; + +public class JsonGenerator { + + /** + * For all *.class files in the current directory, assuming one Java file per class file, write + * the initial values of their static fields to the file clinit-state.json. + */ + public static void main(String[] args) throws ClassNotFoundException, IOException { + File here = new File(System.getProperty("user.dir")); + File jsonFile = new File("clinit-state.json"); + StaticFieldMap> classMap = new StaticFieldMap<>(); + for (File file : here.listFiles()) { + if (file.getName().endsWith(".class")) { + String className = classNameFromFile(file); + StaticFieldMap staticFieldMap = staticFieldMap(Class.forName(className)); + if (!staticFieldMap.isEmpty()) { + classMap.put(className, staticFieldMap); + } + } + } + Map jsonArgs = jsonWriterArgs(); + String json = JsonWriter.objectToJson(classMap, jsonArgs); + FileWriter writer = new FileWriter(jsonFile); + writer.write(json); + writer.close(); + } + + public static Map jsonWriterArgs() { + Map args = new HashMap<>(); + args.put(JsonWriter.WRITE_LONGS_AS_STRINGS, true); + args.put(JsonWriter.PRETTY_PRINT, true); + + // We do not use json-io's shorthands for these types. + Map typeNameMap = new HashMap<>(); + typeNameMap.put("java.lang.Boolean", "java.lang.Boolean"); + typeNameMap.put("java.lang.Byte", "java.lang.Byte"); + typeNameMap.put("java.lang.Character", "java.lang.Character"); + typeNameMap.put("java.lang.Class", "java.lang.Class"); + typeNameMap.put("java.lang.Double", "java.lang.Double"); + typeNameMap.put("java.lang.Float", "java.lang.Float"); + typeNameMap.put("java.lang.Integer", "java.lang.Integer"); + typeNameMap.put("java.lang.Long", "java.lang.Long"); + typeNameMap.put("java.lang.Short", "java.lang.Short"); + typeNameMap.put("java.lang.String", "java.lang.String"); + typeNameMap.put("java.util.Date", "java.util.Date"); + args.put(JsonWriter.TYPE_NAME_MAP, typeNameMap); + + Map customWriters = new HashMap<>(); + customWriters.put(Enum.class, new EnumWriter()); + customWriters.put(String.class, new StringModelWriter()); + customWriters.put(StaticFieldMap.class, new StaticFieldMapWriter()); + args.put(JsonWriter.CUSTOM_WRITER_MAP, customWriters); + return args; + } + + /** + * Assumes that a file MyClass.class contains exactly one Java class called MyClass. + */ + public static String classNameFromFile(File file) { + String fileName = file.getName(); + return fileName.substring(0, fileName.length() - 6); + } + + public static StaticFieldMap staticFieldMap(Class clazz) { + StaticFieldMap staticFields = new StaticFieldMap<>(); + for (Field field : getAllStaticFields(clazz)) { + field.setAccessible(true); + try { + if (!field.getName().equals("$assertionsDisabled")) { + staticFields.put(field.getName(), field.get(null)); + } + } + catch (IllegalAccessException e) { + System.err.println("Could not access field " + field.getName() + " in class " + + clazz.getName() + "."); + } + } + return staticFields; + } + + public static List getAllStaticFields(Class clazz) { + List fields = new ArrayList<>(); + if (clazz == null) { + return fields; + } + for (Field field : clazz.getDeclaredFields()) { + if ((field.getModifiers() & Modifier.STATIC) == Modifier.STATIC) { + fields.add(field); + } + } + fields.addAll(getAllStaticFields(clazz.getSuperclass())); + for (Class interfaze : clazz.getInterfaces()) { + fields.addAll(getAllStaticFields(interfaze)); + } + return fields; + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/StaticFieldMap.java b/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/StaticFieldMap.java new file mode 100644 index 00000000000..dcb557520f4 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/StaticFieldMap.java @@ -0,0 +1,13 @@ +package org.cprover; + +import java.util.HashMap; + +/** + * A map whose keys are of type String. + * We use this instead of e.g. HashMap and define a custom writer for it because + * json-io prints Maps in a special way that would ignore our custom String + * writer for both the keys and values of the Map. We want to use the custom + * String writer for values but not for keys. + */ +public class StaticFieldMap extends HashMap { +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/StaticFieldMapWriter.java b/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/StaticFieldMapWriter.java new file mode 100644 index 00000000000..4b73bff386f --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/StaticFieldMapWriter.java @@ -0,0 +1,39 @@ +package org.cprover; + +import com.cedarsoftware.util.io.JsonWriter; + +import java.io.IOException; +import java.io.Writer; +import java.util.Iterator; +import java.util.Map; + +import static com.cedarsoftware.util.io.JsonWriter.JsonClassWriterEx.Support.getWriter; + +public class StaticFieldMapWriter implements JsonWriter.JsonClassWriterEx { + + public void write(Object obj, boolean showType, Writer output, Map args) + throws IOException { + StaticFieldMap map = (StaticFieldMap) obj; + writeHelper(map, output, args); + } + + private void writeHelper(StaticFieldMap map, Writer output, Map args) + throws IOException { + JsonWriter outerWriter = getWriter(args); + // Make sure the output is still valid JSON if we (accidentally) try to write an empty map. + if (map.isEmpty()) { + output.write("\"@noFields\": true"); + return; + } + Iterator> it = map.entrySet().iterator(); + Map.Entry entry = it.next(); + output.write('"' + entry.getKey() + "\":"); + outerWriter.writeImpl(entry.getValue(), true, true, true); + while (it.hasNext()) { + output.write(','); + entry = it.next(); + output.write('"' + entry.getKey() + "\":"); + outerWriter.writeImpl(entry.getValue(), true, true, true); + } + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/StringModelWriter.java b/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/StringModelWriter.java new file mode 100644 index 00000000000..3f5165a0378 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/StringModelWriter.java @@ -0,0 +1,27 @@ +package org.cprover; + +import com.cedarsoftware.util.io.JsonWriter; + +import java.io.IOException; +import java.io.Writer; + +import static com.cedarsoftware.util.io.JsonWriter.writeJsonUtf8String; + +/** + * This duplicates JsonStringWriter from json-io. + * json-io has a check for JsonStringWriter which results in never printing its type. + * We avoid this check by having our own custom writer for strings. + */ +public class StringModelWriter implements JsonWriter.JsonClassWriter { + + public void write(Object obj, boolean showType, Writer output) throws IOException { + output.write("\"value\":"); + writeJsonUtf8String((String) obj, output); + } + + public boolean hasPrimitiveForm() { return true; } + + public void writePrimitiveForm(Object o, Writer output) throws IOException { + writeJsonUtf8String((String) o, output); + } +} diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_abstract_class_first_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_abstract_class_first_fail.desc new file mode 100644 index 00000000000..092d5878b49 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_abstract_class_first_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testAbstractClassFirstFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_abstract_class_first_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_abstract_class_first_pass.desc new file mode 100644 index 00000000000..0e5e27e1c1d --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_abstract_class_first_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testAbstractClassFirstPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_abstract_class_second_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_abstract_class_second_fail.desc new file mode 100644 index 00000000000..9c2c0037d21 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_abstract_class_second_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testAbstractClassSecondFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_abstract_class_second_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_abstract_class_second_pass.desc new file mode 100644 index 00000000000..f6baa7c3112 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_abstract_class_second_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testAbstractClassSecondPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_ascii_char_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_ascii_char_fail.desc new file mode 100644 index 00000000000..da88ffe070b --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_ascii_char_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testAsciiCharFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_ascii_char_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_ascii_char_pass.desc new file mode 100644 index 00000000000..dffd11247da --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_ascii_char_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testAsciiCharPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_boolean_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_boolean_fail.desc new file mode 100644 index 00000000000..d25c447743b --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_boolean_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testBooleanFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_boolean_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_boolean_pass.desc new file mode 100644 index 00000000000..30aa04b809b --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_boolean_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testBooleanPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_byte_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_byte_fail.desc new file mode 100644 index 00000000000..b9e258d088f --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_byte_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testByteFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_byte_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_byte_pass.desc new file mode 100644 index 00000000000..871672ea3e3 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_byte_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testBytePass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_char_array_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_char_array_fail.desc new file mode 100644 index 00000000000..23b73de8707 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_char_array_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 8 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testCharArrayFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_char_array_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_char_array_pass.desc new file mode 100644 index 00000000000..2bf0e7ac143 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_char_array_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 8 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testCharArrayPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_chinese_char_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_chinese_char_fail.desc new file mode 100644 index 00000000000..9fe1f36f592 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_chinese_char_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testChineseCharFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_chinese_char_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_chinese_char_pass.desc new file mode 100644 index 00000000000..93f2003cdca --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_chinese_char_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testChineseCharPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_concrete_class_first_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_concrete_class_first_fail.desc new file mode 100644 index 00000000000..d4762237b07 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_concrete_class_first_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testConcreteClassFirstFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_concrete_class_first_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_concrete_class_first_pass.desc new file mode 100644 index 00000000000..1dd90c73c75 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_concrete_class_first_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testConcreteClassFirstPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_concrete_class_second_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_concrete_class_second_fail.desc new file mode 100644 index 00000000000..6bb6f4042e8 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_concrete_class_second_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testConcreteClassSecondFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_concrete_class_second_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_concrete_class_second_pass.desc new file mode 100644 index 00000000000..273a89a1d97 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_concrete_class_second_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testConcreteClassSecondPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_double_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_double_fail.desc new file mode 100644 index 00000000000..4afd8470a46 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_double_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testDoubleFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_double_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_double_pass.desc new file mode 100644 index 00000000000..283610e6d91 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_double_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testDoublePass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_enum_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_enum_fail.desc new file mode 100644 index 00000000000..764934e95fb --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_enum_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testEnumFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_enum_in_own_type_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_enum_in_own_type_fail.desc new file mode 100644 index 00000000000..72b520ab417 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_enum_in_own_type_fail.desc @@ -0,0 +1,8 @@ +CORE +Color.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function Color.testEnumInOwnTypeFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_enum_in_own_type_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_enum_in_own_type_pass.desc new file mode 100644 index 00000000000..1d57540a4ec --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_enum_in_own_type_pass.desc @@ -0,0 +1,8 @@ +CORE +Color.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function Color.testEnumInOwnTypePass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_enum_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_enum_pass.desc new file mode 100644 index 00000000000..ce5f1038b2b --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_enum_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testEnumPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_fib_char_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_fib_char_fail.desc new file mode 100644 index 00000000000..3a67a27a09f --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_fib_char_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testFibCharFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_fib_char_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_fib_char_pass.desc new file mode 100644 index 00000000000..6b1bcce2f85 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_fib_char_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testFibCharPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_float_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_float_fail.desc new file mode 100644 index 00000000000..f607e897c8c --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_float_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testFloatFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_float_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_float_pass.desc new file mode 100644 index 00000000000..c84a3248157 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_float_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testFloatPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_fail.desc new file mode 100644 index 00000000000..8ad372415f6 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_less_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_less_fail.desc new file mode 100644 index 00000000000..5ae508d8ee3 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_less_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericInterfaceLessFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_less_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_less_pass.desc new file mode 100644 index 00000000000..263e662986b --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_less_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericInterfaceLessPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_more_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_more_fail.desc new file mode 100644 index 00000000000..d8924246781 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_more_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericInterfaceMoreFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_more_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_more_pass.desc new file mode 100644 index 00000000000..de5a9a5ed51 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_more_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericInterfaceMorePass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_same_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_same_fail.desc new file mode 100644 index 00000000000..1a8de99540e --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_same_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericInterfaceSameFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_same_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_same_pass.desc new file mode 100644 index 00000000000..4bd90c7a24d --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_same_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericInterfaceSamePass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_simple_more_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_simple_more_fail.desc new file mode 100644 index 00000000000..fed476ee57d --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_simple_more_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericInterfaceSimpleMoreFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_simple_more_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_simple_more_pass.desc new file mode 100644 index 00000000000..1c5a7a2a3e8 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_interface_simple_more_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericInterfaceSimpleMorePass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_multi_dim_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_multi_dim_fail.desc new file mode 100644 index 00000000000..3c35c1ea23c --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_multi_dim_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericMultiDimFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_multi_dim_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_multi_dim_pass.desc new file mode 100644 index 00000000000..1bd1e387546 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_multi_dim_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericMultiDimPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_pass.desc new file mode 100644 index 00000000000..de1025a7bd0 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_with_interface_field_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_with_interface_field_fail.desc new file mode 100644 index 00000000000..0e8851e5bd4 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_with_interface_field_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericWithInterfaceFieldFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_with_interface_field_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_with_interface_field_pass.desc new file mode 100644 index 00000000000..fd7c2303538 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_generic_with_interface_field_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testGenericWithInterfaceFieldPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_hex_char_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_hex_char_fail.desc new file mode 100644 index 00000000000..6fe768cc91d --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_hex_char_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testHexCharFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_hex_char_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_hex_char_pass.desc new file mode 100644 index 00000000000..3cc1ea9de94 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_hex_char_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testHexCharPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_inherited_field_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_inherited_field_fail.desc new file mode 100644 index 00000000000..35a77ac1a78 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_inherited_field_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testInheritedFieldFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_inherited_field_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_inherited_field_pass.desc new file mode 100644 index 00000000000..a4dd51ed1f8 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_inherited_field_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testInheritedFieldPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_int_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_int_fail.desc new file mode 100644 index 00000000000..8be3b78f0e7 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_int_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testIntFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_int_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_int_pass.desc new file mode 100644 index 00000000000..d35b2e84686 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_int_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testIntPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_container_first_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_container_first_fail.desc new file mode 100644 index 00000000000..dea30237c8e --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_container_first_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testInterfaceContainerFirstFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_container_first_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_container_first_pass.desc new file mode 100644 index 00000000000..d0a80c2bfe6 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_container_first_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testInterfaceContainerFirstPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_container_second_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_container_second_fail.desc new file mode 100644 index 00000000000..7ebfb74900b --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_container_second_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testInterfaceContainerSecondFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_container_second_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_container_second_pass.desc new file mode 100644 index 00000000000..dc18560e90a --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_container_second_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testInterfaceContainerSecondPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_first_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_first_fail.desc new file mode 100644 index 00000000000..bb792e55e71 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_first_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testInterfaceFirstFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_first_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_first_pass.desc new file mode 100644 index 00000000000..8a0b9bed8cf --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_first_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testInterfaceFirstPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_second_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_second_fail.desc new file mode 100644 index 00000000000..12d5e7c9dc7 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_second_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testInterfaceSecondFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_second_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_second_pass.desc new file mode 100644 index 00000000000..9ae3f0ec342 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_interface_second_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testInterfaceSecondPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_long_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_long_fail.desc new file mode 100644 index 00000000000..2f274ae656f --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_long_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testLongFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_long_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_long_pass.desc new file mode 100644 index 00000000000..fa56a871912 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_long_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testLongPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_null_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_null_fail.desc new file mode 100644 index 00000000000..54fc719b53e --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_null_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testNullFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_null_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_null_pass.desc new file mode 100644 index 00000000000..e4da3ca49a4 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_null_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testNullPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_primitive_array_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_primitive_array_fail.desc new file mode 100644 index 00000000000..85f0fc7bca5 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_primitive_array_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testPrimitiveArrayFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_primitive_array_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_primitive_array_pass.desc new file mode 100644 index 00000000000..38496fbbeeb --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_primitive_array_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testPrimitiveArrayPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_primitive_array_sum_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_primitive_array_sum_fail.desc new file mode 100644 index 00000000000..10bdb15c473 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_primitive_array_sum_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 4 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testPrimitiveArraySumFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_primitive_array_sum_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_primitive_array_sum_pass.desc new file mode 100644 index 00000000000..78211f2fa5e --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_primitive_array_sum_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 4 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testPrimitiveArraySumPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_array_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_array_fail.desc new file mode 100644 index 00000000000..178242de16c --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_array_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceArrayFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_array_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_array_pass.desc new file mode 100644 index 00000000000..0b949db0c35 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_array_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceArrayPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_fail.desc new file mode 100644 index 00000000000..698e68b56c6 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_pass.desc new file mode 100644 index 00000000000..8ffd65c610b --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferencePass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_class_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_class_fail.desc new file mode 100644 index 00000000000..cbc02f55073 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_class_fail.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceToOtherClassFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_class_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_class_pass.desc new file mode 100644 index 00000000000..abb0cadd035 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_class_pass.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceToOtherClassPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_fail.desc new file mode 100644 index 00000000000..bd6c2ccbcd8 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceToOtherFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_pass.desc new file mode 100644 index 00000000000..78a20c3a969 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceToOtherPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_primitive_array_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_primitive_array_fail.desc new file mode 100644 index 00000000000..5951c8c5e1b --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_primitive_array_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceToPrimitiveArrayFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_primitive_array_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_primitive_array_pass.desc new file mode 100644 index 00000000000..de673ff20d0 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_primitive_array_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceToPrimitiveArrayPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_reference_array_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_reference_array_fail.desc new file mode 100644 index 00000000000..4e4b91d533f --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_reference_array_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceToReferenceArrayFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_reference_array_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_reference_array_pass.desc new file mode 100644 index 00000000000..97aaa59814a --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_reference_array_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceToReferenceArrayPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_string_fail1.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_string_fail1.desc new file mode 100644 index 00000000000..bd55fa86ff9 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_string_fail1.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceToStringFail1 +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_string_fail2.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_string_fail2.desc new file mode 100644 index 00000000000..7d67268eb2e --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_string_fail2.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceToStringFail2 +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_string_pass1.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_string_pass1.desc new file mode 100644 index 00000000000..46ff32e959c --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_string_pass1.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceToStringPass1 +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_string_pass2.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_string_pass2.desc new file mode 100644 index 00000000000..a4d5de17bcc --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_string_pass2.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testReferenceToStringPass2 +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_short_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_short_fail.desc new file mode 100644 index 00000000000..4acdf327fb0 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_short_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testShortFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_short_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_short_pass.desc new file mode 100644 index 00000000000..baf78d807d1 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_short_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testShortPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_special_char_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_special_char_fail.desc new file mode 100644 index 00000000000..83032d3c862 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_special_char_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testSpecialCharFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_special_char_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_special_char_pass.desc new file mode 100644 index 00000000000..54368f2f0e0 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_special_char_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testSpecialCharPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_string_buffer_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_buffer_fail.desc new file mode 100644 index 00000000000..02e1b935a19 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_buffer_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testStringBufferFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_string_buffer_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_buffer_pass.desc new file mode 100644 index 00000000000..4d93db3def9 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_buffer_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testStringBufferPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_string_builder_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_builder_fail.desc new file mode 100644 index 00000000000..6243b151d8d --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_builder_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testStringBuilderFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_string_builder_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_builder_pass.desc new file mode 100644 index 00000000000..1f15ddf3d42 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_builder_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testStringBuilderPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_string_container_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_container_fail.desc new file mode 100644 index 00000000000..f234a2d9d10 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_container_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testStringContainerFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_string_container_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_container_pass.desc new file mode 100644 index 00000000000..c68a4b3e115 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_container_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testStringContainerPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_string_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_fail.desc new file mode 100644 index 00000000000..0d8d246784b --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testStringFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_string_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_pass.desc new file mode 100644 index 00000000000..8b3754d8538 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_string_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testStringPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_subclass_field_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_subclass_field_fail.desc new file mode 100644 index 00000000000..8097342af41 --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_subclass_field_fail.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testSubclassFieldFail +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_subclass_field_pass.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_subclass_field_pass.desc new file mode 100644 index 00000000000..ed319b2822f --- /dev/null +++ b/jbmc/regression/jbmc/deterministic_assignments_json/test_subclass_field_pass.desc @@ -0,0 +1,8 @@ +CORE +StaticValues.class +--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testSubclassFieldPass +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index 066a67240da..f1b404433cd 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/jbmc/src/java_bytecode/Makefile @@ -1,4 +1,5 @@ -SRC = bytecode_info.cpp \ +SRC = assignments_from_json.cpp \ + bytecode_info.cpp \ character_refine_preprocess.cpp \ ci_lazy_methods.cpp \ ci_lazy_methods_needed.cpp \ diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp new file mode 100644 index 00000000000..b84d4d76fe8 --- /dev/null +++ b/jbmc/src/java_bytecode/assignments_from_json.cpp @@ -0,0 +1,844 @@ +/*******************************************************************\ + +Module: Assignments to values specified in JSON files + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include "assignments_from_json.h" + +#include "ci_lazy_methods_needed.h" +#include "java_static_initializers.h" +#include "java_string_library_preprocess.h" +#include "java_string_literals.h" +#include "java_utils.h" + +#include +#include +#include +#include +#include +#include + +/// Values passed around between most functions of the recursive deterministic +/// assignment algorithm entered from \ref assign_from_json. +/// The values in a given `object_creation_infot` are never reassigned, but the +/// ones that are not marked `const` may be mutated. +struct object_creation_infot +{ + /// Code block to append all new code to for the deterministic assignments. + code_blockt █ + + /// Handles allocation of new symbols, adds them to its symbol table (which + /// will usually be the same as the `symbol_table` of this struct) and keeps + /// track of them so declarations for them can be added by the caller before + /// `block`. + allocate_objectst &allocate_objects; + + /// Used for looking up symbols corresponding to Java classes and methods. + symbol_table_baset &symbol_table; + + /// Where runtime types differ from compile-time types, we need to mark the + /// runtime types as needed by lazy methods. + optionalt &needed_lazy_methods; + + /// Map to keep track of reference-equal objects. Each entry has an ID (such + /// that any two reference-equal objects have the same ID) and the expression + /// for the symbol that all these references point to. + std::unordered_map &references; + + /// Source location associated with the newly added codet. + const source_locationt &loc; + + /// Maximum value allowed for any (constant or variable length) arrays in user + /// code. + size_t max_user_array_length; + + /// Used for the workaround for enums only. + /// See assign_enum_from_json. + const java_class_typet &declaring_class_type; +}; + +static java_class_typet +followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table) +{ + const pointer_typet &pointer_type = to_pointer_type(expr.type()); + const java_class_typet &java_class_type = + to_java_class_type(namespacet{symbol_table}.follow(pointer_type.subtype())); + return java_class_type; +} + +static bool +has_enum_type(const exprt &expr, const symbol_table_baset &symbol_table) +{ + return followed_class_type(expr, symbol_table).get_is_enumeration(); +} + +/// This function is used as a workaround until reference-equal objects defined +/// across several classes are tracked correctly. Once reference-equality works +/// in all cases, this function can be removed. +/// Until then, in the case of an enum expression that needs to be assigned a +/// value, we distinguish between two cases: +/// 1) the declaring class of the enum expression is the same as the type of the +/// enum expression. For example, for an enum Pet {DOG, CAT}, the declaring +/// class of the expression Pet.DOG is Pet, and the type of the expression is +/// also Pet. The same is true for the expressions that represent the +/// elements of the $VALUES array of Pet, and for any user-defined Pet-typed +/// fields in Pet.java. In this case, initialize the expression just as a +/// regular object that has known reference-equal objects. (Corresponds to +/// creating the enum constant in Java or referencing it directly.) +/// See assign_reference_from_json. +/// 2) otherwise, initialize it by indexing the $VALUES array with the given +/// ordinal. An example of this case would be the field `pet` in +/// `class MyClass { Pet pet; }` (its declaring class is `MyClass` and its +/// own type is `Pet`). +/// See assign_enum_from_json. +/// \param expr: an expression representing a Java object. +/// \param symbol_table: used for looking up the type of \p expr. +/// \param declaring_class_type: type of the class where \p expr is declared. +/// \return `true` if \p expr has an enum type and is declared within the +/// definition of that same type, `false` otherwise. +bool is_enum_with_type_equal_to_declaring_type( + const exprt &expr, + const symbol_table_baset &symbol_table, + const java_class_typet &declaring_class_type) +{ + PRECONDITION(can_cast_type(expr.type())); + return followed_class_type(expr, symbol_table) == declaring_class_type && + declaring_class_type.get_is_enumeration(); +} + +/// If the argument has a "@type" key, return the corresponding value, else +/// return an empty optional. +/// A runtime type that is different from the objects compile-time type should +/// be specified in `json` in this way. +/// Type values are of the format "my.package.name.ClassName". +static optionalt get_type(const jsont &json) +{ + if(!json.is_object()) + return {}; + const auto &json_object = to_json_object(json); + if(json_object.find("@type") == json_object.end()) + return {}; + return json_object["@type"].value; +} + +/// Return true iff the argument has a "@id" key. +/// The presence of such a key means that there exist objects that are +/// reference-equal to this object. +/// The corresponding value is the unique ID of all objects that are reference- +/// equal to this one. +/// All other key-value pairs of `json` should be as usual. +static bool has_id(const jsont &json) +{ + if(!json.is_object()) + return false; + const auto &json_object = to_json_object(json); + return json_object.find("@id") != json_object.end(); +} + +/// Return true iff the argument has a "@ref" key. +/// The corresponding value is the unique ID of all objects that are reference- +/// equal to this one. +/// Any other key-value pairs of `json` will be ignored. +static bool is_reference(const jsont &json) +{ + if(!json.is_object()) + return false; + const auto &json_object = to_json_object(json); + return json_object.find("@ref") != json_object.end(); +} + +/// Return the unique ID of all objects that are reference-equal to this one. +/// This is the value corresponding to a "@id" or "@ref" key. +/// See \ref has_id and \ref is_reference. +static std::string get_id_or_reference_value(const jsont &json) +{ + PRECONDITION(has_id(json) || is_reference(json)); + if(has_id(json)) + return json["@id"].value; + return json["@ref"].value; +} + +/// Return a unique ID for an enum, based on its type and `name` field. +/// This is needed for the enum workaround until reference-equality across +/// different classes is supported. +/// See \ref is_enum_with_type_equal_to_declaring_type. +static std::string get_enum_id( + const exprt &expr, + const jsont &json, + const symbol_table_baset &symbol_table) +{ + PRECONDITION(json.is_object()); + const auto &json_object = to_json_object(json); + INVARIANT( + json_object.find("name") != json_object.end(), + "JSON representation of enums should include name field"); + return id2string(followed_class_type(expr, symbol_table).get_tag()) + '.' + + (json["name"].value); +} + +/// Return true iff the argument has a `"@nondetLength": true` entry. +/// If such an entry is present on a JSON representation of an array, it means +/// that the array should be assigned a nondeterministic length, constrained to +/// be at least the number of elements specified for this array. +static bool has_nondet_length(const jsont &json) +{ + if(!json.is_object()) + return false; + const auto &json_object = to_json_object(json); + if(json_object.find("@nondetLength") != json_object.end()) + return (json["@nondetLength"].is_true()); + return false; +} + +/// For typed versions of primitive, string or array types, looks up their +/// untyped contents with the key specific to their type. +/// See the examples on \ref assign_from_json for the terminology used here +/// (typed vs. untyped). +static jsont get_untyped(const jsont &json, const std::string &object_key) +{ + if(get_type(json) || has_nondet_length(json)) + return json[object_key]; + return json; +} + +/// \ref get_untyped for primitive types. +static jsont get_untyped_primitive(const jsont &json) +{ + return get_untyped(json, "value"); +} + +/// \ref get_untyped for array types. +/// char arrays are treated as a special case as they are represented as an +/// array of a single String element by json-io, rather than an array of one or +/// more char elements. +static json_arrayt +get_untyped_array(const jsont &json, const typet &element_type) +{ + const jsont untyped = get_untyped(json, "@items"); + PRECONDITION(untyped.is_array()); + const auto &json_array = to_json_array(untyped); + if(element_type == java_char_type()) + { + PRECONDITION(json_array.size() == 1); + const auto &first = *json_array.begin(); + PRECONDITION(first.is_string()); + const auto &json_string = to_json_string(first); + + const auto wide_string = utf8_to_utf16_native_endian(json_string.value); + auto string_range = make_range(wide_string.begin(), wide_string.end()); + const auto json_range = string_range.map([](const wchar_t &c) { + const std::u16string u16(1, c); + return json_stringt{utf16_native_endian_to_utf8(u16)}; + }); + return json_arrayt{json_range.begin(), json_range.end()}; + } + return json_array; +} + +/// \ref get_untyped for string types. +/// Note that this differs from the standard serialization of java.lang.String +/// in json-io, but is consistent with the serialization of StringBuilder and +/// StringBuffer. +static jsont get_untyped_string(const jsont &json) +{ + return get_untyped(json, "value"); +} + +/// Given a JSON representation of a (non-array) reference-typed object and a +/// type inferred from the type of a containing array, get the runtime type of +/// the corresponding pointer expression. +/// \param json: JSON representation of a non-array object. If it contains a +/// `@type` field, this takes priority over \p type_from_array. Types for non- +/// array objects are stored in the JSON in the format +/// "my.package.name.ClassName". +/// \param type_from_array: may contain an element type name given by a +/// containing array. Such types are stored in the form +/// "Lmy.package.name.ClassName;". +/// \param symbol_table: used to look up the type given its name. +/// \return runtime type of the object, if specified by at least one of the +/// parameters. +static optionalt runtime_type( + const jsont &json, + const optionalt &type_from_array, + const symbol_table_baset &symbol_table) +{ + const auto type_from_json = get_type(json); + if(!type_from_json && !type_from_array) + return {}; // no runtime type specified, use compile-time type + const auto runtime_type = [&]() -> std::string { + if(type_from_json) + return "java::" + *type_from_json; + INVARIANT( + type_from_array->find('L') == 0 && + type_from_array->rfind(';') == type_from_array->length() - 1, + "Types inferred from the type of a containing array should be of the " + "form Lmy.package.name.ClassName;"); + return "java::" + type_from_array->substr(1, type_from_array->length() - 2); + }(); + if(!symbol_table.has_symbol(runtime_type)) + return {}; // Fall back to compile-time type if runtime type was not found + const auto &replacement_class_type = + to_java_class_type(symbol_table.lookup_ref(runtime_type).type); + return replacement_class_type; +} + +/// Given a JSON representation of an array and a type inferred from the type of +/// a containing array, get the element type by removing the leading '['. +/// Types for arrays are stored in the format "[Lmy.package.name.ClassName;". +/// In this case, the returned value would be "Lmy.package.name.ClassName;". +/// \p type_from_array would only have a value if this array is stored within +/// another array, i.e.\ within a ClassName[][]. +/// Keeping track of array types in this way is necessary to assign generic +/// arrays with no compile-time types. +/// \param json: JSON representation of an array. If it contains a `@type` +/// field, this takes priority over \p type_from_array. +/// \param type_from_array: may contain a type name from a containing array. +/// \return if the type of an array was given, the type of its elements. +static optionalt element_type_from_array_type( + const jsont &json, + const optionalt &type_from_array) +{ + if(const auto json_array_type = get_type(json)) + { + INVARIANT( + json_array_type->find('[') == 0, + "Array types in the JSON input should be of the form " + "[[...[Lmy.package.name.ClassName; (with n occurrences of [ for an " + "n-dimensional array)"); + return json_array_type->substr(1); + } + else if(type_from_array) + { + INVARIANT( + type_from_array->find('[') == 0, + "For arrays that are themselves contained by an array from which a type " + "is inferred, such a type should be of the form " + "[[...[Lmy.package.name.ClassName;"); + return type_from_array->substr(1); + } + return {}; +} + +void assign_from_json_rec( + const exprt &expr, + const jsont &json, + const optionalt &type_from_array, + object_creation_infot &info); + +/// One of the base cases (primitive case) of the recursion. +/// For characters, the encoding in \p json is assumed to be UTF-8. +/// See \ref assign_from_json_rec. +static void assign_primitive_from_json( + const exprt &expr, + const jsont &json, + code_blockt &block) +{ + if(json.is_null()) // field is not mentioned in json, leave as default value + return; + if(expr.type() == java_boolean_type()) + { + if(json.is_true()) + block.add(code_assignt{expr, true_exprt{}}); + else + block.add(code_assignt{expr, false_exprt{}}); + } + else if( + expr.type() == java_int_type() || expr.type() == java_byte_type() || + expr.type() == java_short_type() || expr.type() == java_long_type()) + { + block.add( + code_assignt{expr, from_integer(std::stoll(json.value), expr.type())}); + } + else if(expr.type() == java_double_type()) + { + ieee_floatt ieee_float(to_floatbv_type(expr.type())); + ieee_float.from_double(std::stod(json.value)); + block.add(code_assignt{expr, ieee_float.to_expr()}); + } + else if(expr.type() == java_float_type()) + { + ieee_floatt ieee_float(to_floatbv_type(expr.type())); + ieee_float.from_float(std::stof(json.value)); + block.add(code_assignt{expr, ieee_float.to_expr()}); + } + else if(expr.type() == java_char_type()) + { + const std::wstring wide_value = utf8_to_utf16_native_endian(json.value); + PRECONDITION(wide_value.length() == 1); + block.add( + code_assignt{expr, from_integer(wide_value.front(), expr.type())}); + } +} + +/// One of the base cases of the recursive algorithm. See +/// \ref assign_from_json_rec. +static void assign_null(const exprt &expr, code_blockt &block) +{ + block.add( + code_assignt{expr, null_pointer_exprt{to_pointer_type(expr.type())}}); +} + +/// In the case of an assignment of an array given a JSON representation, this +/// function assigns the data component of the array, which contains the array +/// elements. \p expr is a pointer to the array containing the component. +static void assign_array_data_component_from_json( + const exprt &expr, + const jsont &json, + const optionalt &type_from_array, + object_creation_infot &info) +{ + const auto &java_class_type = followed_class_type(expr, info.symbol_table); + const auto &data_component = java_class_type.components()[2]; + const auto &element_type = + java_array_element_type(to_struct_tag_type(expr.type().subtype())); + const exprt data_member_expr = typecast_exprt::conditional_cast( + member_exprt{dereference_exprt{expr}, "data", data_component.type()}, + pointer_type(element_type)); + + const symbol_exprt &array_init_data = + info.allocate_objects.allocate_automatic_local_object( + data_member_expr.type(), "user_specified_array_data_init"); + const code_assignt data_assign{array_init_data, data_member_expr, info.loc}; + info.block.add(data_assign); + + size_t index = 0; + const optionalt inferred_element_type = + element_type_from_array_type(json, type_from_array); + const json_arrayt json_array = get_untyped_array(json, element_type); + for(auto it = json_array.begin(); it < json_array.end(); it++, index++) + { + const dereference_exprt element_at_index = array_element_from_pointer( + array_init_data, from_integer(index, java_int_type())); + assign_from_json_rec(element_at_index, *it, inferred_element_type, info); + } +} + +/// Allocate a fresh array of length \p array_length_expr and assigns \p expr +/// to it. +static void allocate_array( + const exprt &expr, + const exprt &array_length_expr, + object_creation_infot &info) +{ + const pointer_typet &pointer_type = to_pointer_type(expr.type()); + const auto &element_type = + java_array_element_type(to_struct_tag_type(pointer_type.subtype())); + side_effect_exprt java_new_array{ID_java_new_array, pointer_type}; + java_new_array.copy_to_operands(array_length_expr); + java_new_array.type().subtype().set(ID_element_type, element_type); + code_assignt assign{expr, java_new_array, info.loc}; + info.block.add(assign); +} + +/// One of the cases in the recursive algorithm: the case where \p expr +/// represents an array. +/// The length of the array is given by a symbol: \p given_length_expr if it is +/// specified (this will be the case when there are two or more reference-equal +/// arrays), or a fresh symbol otherwise. +/// If \p given_length_expr is specified, we assume that an array with this +/// symbol as its length has already been allocated and that \p expr has been +/// assigned to it. +/// Either way, the length symbol stores a nondet integer, and we add +/// constraints on this: if "nondetLength" is specified in \p json, then the +/// number of elements specified in \p json should be the minimum length of the +/// array. Otherwise the number of elements should be the exact length of the +/// array. +/// For the assignment of the array elements, see +/// \ref assign_array_data_component_from_json. +/// For the overall algorithm, see \ref assign_from_json_rec. +static void assign_array_from_json( + const exprt &expr, + const jsont &json, + const optionalt &given_length_expr, + const optionalt &type_from_array, + object_creation_infot &info) +{ + PRECONDITION(is_java_array_type(expr.type())); + const auto &element_type = + java_array_element_type(to_struct_tag_type(expr.type().subtype())); + + exprt length_expr; + if(given_length_expr) + length_expr = *given_length_expr; + else + { + length_expr = info.allocate_objects.allocate_automatic_local_object( + java_int_type(), "user_specified_array_length"); + info.block.add(code_assignt{ + length_expr, side_effect_expr_nondett{java_int_type(), info.loc}}); + info.block.add(code_assumet{binary_predicate_exprt{ + length_expr, ID_ge, from_integer(0, java_int_type())}}); + allocate_array(expr, length_expr, info); + } + const json_arrayt json_array = get_untyped_array(json, element_type); + const auto number_of_elements = + from_integer(json_array.size(), java_int_type()); + info.block.add(code_assumet{ + binary_predicate_exprt{length_expr, ID_ge, number_of_elements}}); + if(has_nondet_length(json)) + { + info.block.add(code_assumet{binary_predicate_exprt{ + length_expr, + ID_le, + from_integer(info.max_user_array_length, java_int_type())}}); + } + else + { + info.block.add(code_assumet{ + binary_predicate_exprt{length_expr, ID_le, number_of_elements}}); + } + assign_array_data_component_from_json(expr, json, type_from_array, info); +} + +/// One of the cases in the recursive algorithm: the case where \p expr +/// represents a string. +/// See \ref assign_from_json_rec. +static void assign_string_from_json( + const jsont &json, + const exprt &expr, + object_creation_infot &info) +{ + const auto json_string = get_untyped_string(json); + PRECONDITION(json_string.is_string()); + info.block.add(code_assignt{expr, + get_or_create_string_literal_symbol( + json_string.value, info.symbol_table, true)}); +} + +/// Helper function for \ref assign_struct_from_json which recursively assigns +/// values to all of the fields of the Java object represented by \p expr (the +/// components of its type and all of its parent types). +static void assign_struct_components_from_json( + const exprt &expr, + const jsont &json, + object_creation_infot &info) +{ + const java_class_typet &java_class_type = + to_java_class_type(namespacet{info.symbol_table}.follow(expr.type())); + for(const auto &component : java_class_type.components()) + { + const irep_idt &component_name = component.get_name(); + if( + component_name == "@class_identifier" || + component_name == "cproverMonitorCount") + { + continue; + } + member_exprt member_expr{expr, component_name, component.type()}; + if(component_name[0] == '@') // component is parent struct type + assign_struct_components_from_json(member_expr, json, info); + else // component is class field (pointer to struct) + { + const jsont member_json = json[id2string(component_name)]; + assign_from_json_rec(member_expr, member_json, {}, info); + } + } +} + +/// One of the cases in the recursive algorithm: the case where \p expr is a +/// struct, which is the result of dereferencing a pointer that corresponds to +/// the Java object described in \p json. +/// See \ref assign_from_json_rec. +static void assign_struct_from_json( + const exprt &expr, + const jsont &json, + object_creation_infot &info) +{ + const namespacet ns{info.symbol_table}; + const java_class_typet &java_class_type = + to_java_class_type(ns.follow(expr.type())); + if(is_java_string_type(java_class_type)) + assign_string_from_json(json, expr, info); + else + { + auto initial_object = zero_initializer(expr.type(), info.loc, ns); + CHECK_RETURN(initial_object.has_value()); + set_class_identifier( + to_struct_expr(*initial_object), + ns, + struct_tag_typet("java::" + id2string(java_class_type.get_tag()))); + info.block.add(code_assignt{expr, *initial_object}); + assign_struct_components_from_json(expr, json, info); + } +} + +/// Same as \ref assign_pointer_from_json without special cases (enums). +static void assign_non_enum_pointer_from_json( + const exprt &expr, + const jsont &json, + object_creation_infot &info) +{ + exprt dereferenced_symbol_expr = + info.allocate_objects.allocate_dynamic_object( + info.block, expr, to_pointer_type(expr.type()).subtype()); + assign_struct_from_json(dereferenced_symbol_expr, json, info); +} + +/// One of the cases in the recursive algorithm: the case where the expression +/// to be assigned a value is an enum constant that is referenced outside of the +/// definition of its type. (See \ref is_enum_with_type_equal_to_declaring_type +/// for this temporary distinction. See \ref assign_from_json for details about +/// the recursion.) +/// Once reference-equality of fields in different classes is supported, this +/// function can be removed. +static void assign_enum_from_json( + const exprt &expr, + const jsont &json, + object_creation_infot &info) +{ + const auto &java_class_type = followed_class_type(expr, info.symbol_table); + const std::string &enum_name = id2string(java_class_type.get_name()); + if(const auto func = info.symbol_table.lookup(clinit_wrapper_name(enum_name))) + info.block.add(code_function_callt{func->symbol_expr()}); + + const irep_idt values_name = enum_name + ".$VALUES"; + if(!info.symbol_table.has_symbol(values_name)) + { + // Fallback: generate a new enum instance instead of getting it from $VALUES + assign_non_enum_pointer_from_json(expr, json, info); + return; + } + + dereference_exprt values_struct{ + info.symbol_table.lookup_ref(values_name).symbol_expr()}; + const auto &values_struct_type = + to_struct_type(namespacet{info.symbol_table}.follow(values_struct.type())); + PRECONDITION(is_valid_java_array(values_struct_type)); + const member_exprt values_data = member_exprt{ + values_struct, "data", values_struct_type.components()[2].type()}; + + const exprt ordinal_expr = + from_integer(std::stoi(json["ordinal"].value), java_int_type()); + + info.block.add(code_assignt{ + expr, + typecast_exprt::conditional_cast( + array_element_from_pointer(values_data, ordinal_expr), expr.type())}); +} + +/// One of the cases in the recursive algorithm: the case where \p expr is a +/// pointer to a struct, whose type is the same as the runtime-type of the +/// corresponding Java object. +/// See \ref assign_from_json_rec. +static void assign_pointer_from_json( + const exprt &expr, + const jsont &json, + object_creation_infot &info) +{ + // This check can be removed when tracking reference-equal objects across + // different classes has been implemented. + if(has_enum_type(expr, info.symbol_table)) + assign_enum_from_json(expr, json, info); + else + assign_non_enum_pointer_from_json(expr, json, info); +} + +/// One of the cases in the recursive algorithm: the case where \p expr is a +/// pointer to a struct, and \p runtime_type is the runtime type of the +/// corresponding Java object, which may be more specific than the type pointed +/// to by `expr.type()` (the compile-time type of the object). +/// See \ref assign_from_json_rec. +static void assign_pointer_with_given_type_from_json( + const exprt &expr, + const jsont &json, + const java_class_typet &runtime_type, + object_creation_infot &info) +{ + const auto &pointer_type = to_pointer_type(expr.type()); + pointer_typet replacement_pointer_type = + pointer_to_replacement_type(pointer_type, runtime_type); + if(!equal_java_types(pointer_type, replacement_pointer_type)) + { + const auto &new_symbol = + info.allocate_objects.allocate_automatic_local_object( + replacement_pointer_type, "user_specified_subtype_symbol"); + if(info.needed_lazy_methods) + { + info.needed_lazy_methods->add_all_needed_classes( + replacement_pointer_type); + } + + assign_pointer_from_json(new_symbol, json, info); + info.block.add( + code_assignt{expr, typecast_exprt{new_symbol, pointer_type}}); + } + else + assign_pointer_from_json(expr, json, info); +} + +/// Helper function for \ref assign_reference_from_json. +/// Look up the given \p id in the reference map and gets or creates the symbol +/// for it. +/// In the case of arrays, if the first time we see an ID is in a `@ref` object +/// (rather than `@id`), we do not know what the length of the array will be, so +/// we need to allocate an array of nondeterministic length. The length will +/// be constrained (in \ref assign_array_from_json) once we find the +/// corresponding `@id` object. +/// \param expr: expression representing the Java object for which a symbol is +/// retrieved or allocated. +/// \param id: key in the reference map for this object +/// \param info: references used throughout the recursive algorithm. +/// \return a pair: the first element is true if a new symbol was allocated for +/// the given ID and false if the ID was found in the reference map. The +/// second element has the symbol expression(s) for this ID. +static std::pair get_or_create_reference( + const exprt &expr, + const std::string &id, + object_creation_infot &info) +{ + const auto &pointer_type = to_pointer_type(expr.type()); + const auto id_it = info.references.find(id); + if(id_it == info.references.end()) + { + object_creation_referencet reference; + if(is_java_array_type(expr.type())) + { + reference.expr = info.allocate_objects.allocate_automatic_local_object( + pointer_type, "user_specified_array_ref"); + reference.array_length = + info.allocate_objects.allocate_automatic_local_object( + java_int_type(), "user_specified_array_length"); + info.block.add(code_assignt{*reference.array_length, + side_effect_expr_nondett{java_int_type()}}); + info.block.add(code_assumet{binary_predicate_exprt{ + *reference.array_length, ID_ge, from_integer(0, java_int_type())}}); + allocate_array(reference.expr, *reference.array_length, info); + info.references.insert({id, reference}); + } + else + { + reference.expr = info.allocate_objects.allocate_dynamic_object_symbol( + info.block, expr, pointer_type.subtype()); + info.references.insert({id, reference}); + } + return {true, reference}; + } + return {false, id_it->second}; +} + +/// One of the cases in the recursive algorithm: the case where \p expr +/// corresponds to a Java object that is reference-equal to one or more other +/// Java objects represented in the initial JSON file. +/// See \ref assign_from_json_rec. +/// Such an object will either have the key-value pair `@id: some_key` in +/// \p json, together with a full representation of the object, or it will only +/// have one key-value pair, `@ref: some_key`. For each key, there is only one +/// `@id` field in the JSON file. +/// A special case is enums, which are always represented as a full object +/// without any `@id` or `@ref` keys. This is mostly the same as the output from +/// json-io for enums, except that in our representation, we need to include the +/// ordinal field so that e.g. switch statements on enums will work. +/// We keep track of object IDs using a map from IDs to symbol expressions. +/// Usually the ID is the `some_key` from the example above, except for enums, +/// where the ID is of the form `my.package.name.EnumName.CONSTANT`. +/// The first time we see an ID (`@id`, `@ref` or enum constant), we allocate a +/// symbol for it. The first time we see the full representation of the object +/// (`@id` or enum constant) we initialize the allocated memory. This strategy +/// may need to be changed to support reference-equality of fields across +/// several different classes (e.g.\ as soon as we find a `@ref` for the first +/// time we might want to search the whole initial JSON file for the +/// corresponding `@id`). +static void assign_reference_from_json( + const exprt &expr, + const jsont &json, + const optionalt &type_from_array, + object_creation_infot &info) +{ + const std::string &id = has_enum_type(expr, info.symbol_table) + ? get_enum_id(expr, json, info.symbol_table) + : get_id_or_reference_value(json); + const auto bool_reference_pair = get_or_create_reference(expr, id, info); + const bool is_new_id = bool_reference_pair.first; + const object_creation_referencet &reference = bool_reference_pair.second; + if(has_id(json) || (is_new_id && has_enum_type(expr, info.symbol_table))) + { + if(is_java_array_type(expr.type())) + { + assign_array_from_json( + reference.expr, json, reference.array_length, type_from_array, info); + } + else + assign_struct_from_json(dereference_exprt(reference.expr), json, info); + } + info.block.add(code_assignt{ + expr, typecast_exprt::conditional_cast(reference.expr, expr.type())}); +} + +/// Entry point of the recursive deterministic assignment algorithm. +/// \param expr: expression to assign a deterministic value to. In the case of +/// the entry point, this is either a pointer to a struct, or an expression +/// corresponding to a Java primitive. +/// \param json: a JSON representation of the deterministic value to assign. +/// \param type_from_array: if `expr` was found as an element of an array, +/// the element type of this array. +/// \param info: references used throughout the recursive algorithm. +void assign_from_json_rec( + const exprt &expr, + const jsont &json, + const optionalt &type_from_array, + object_creation_infot &info) +{ + if(can_cast_type(expr.type())) + { + if(json.is_null()) + assign_null(expr, info.block); + else if( + is_reference(json) || has_id(json) || + is_enum_with_type_equal_to_declaring_type( + expr, info.symbol_table, info.declaring_class_type)) + // The last condition can be replaced with + // has_enum_type(expr, info.symbol_table) once tracking reference-equality + // across different classes has been implemented. + { + assign_reference_from_json(expr, json, type_from_array, info); + } + else if(is_java_array_type(expr.type())) + assign_array_from_json(expr, json, {}, type_from_array, info); + else if( + const auto runtime_type = + ::runtime_type(json, type_from_array, info.symbol_table)) + { + assign_pointer_with_given_type_from_json(expr, json, *runtime_type, info); + } + else + assign_pointer_from_json(expr, json, info); + } + else + assign_primitive_from_json(expr, get_untyped_primitive(json), info.block); +} + +void assign_from_json( + const exprt &expr, + const jsont &json, + const irep_idt &function_id, + code_blockt &assignments, + symbol_table_baset &symbol_table, + optionalt &needed_lazy_methods, + size_t max_user_array_length, + std::unordered_map &references) +{ + source_locationt location{}; + location.set_function(function_id); + allocate_objectst allocate(ID_java, location, function_id, symbol_table); + code_blockt body_rec; + const auto class_name = declaring_class(symbol_table.lookup_ref(function_id)); + INVARIANT( + class_name, + "Function " + id2string(function_id) + " must be declared by a class."); + const auto &class_type = + to_java_class_type(symbol_table.lookup_ref(*class_name).type); + object_creation_infot info{body_rec, + allocate, + symbol_table, + needed_lazy_methods, + references, + location, + max_user_array_length, + class_type}; + assign_from_json_rec(expr, json, {}, info); + allocate.declare_created_symbols(assignments); + assignments.append(body_rec); +} diff --git a/jbmc/src/java_bytecode/assignments_from_json.h b/jbmc/src/java_bytecode/assignments_from_json.h new file mode 100644 index 00000000000..65976a135e3 --- /dev/null +++ b/jbmc/src/java_bytecode/assignments_from_json.h @@ -0,0 +1,119 @@ +/*******************************************************************\ + +Module: Assignments to values specified in JSON files + +Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file + +#ifndef CPROVER_JAVA_BYTECODE_ASSIGNMENTS_FROM_JSON_H +#define CPROVER_JAVA_BYTECODE_ASSIGNMENTS_FROM_JSON_H + +#include + +class jsont; +class symbol_table_baset; +class ci_lazy_methods_neededt; + +/// Information to store when several references point to the same Java object. +struct object_creation_referencet +{ + /// Expression for the symbol that stores the value that may be reference + /// equal to other values. + exprt expr; + + /// If `symbol` is an array, this expression stores its length. + optionalt array_length; +}; + +/// Given an expression \p expr representing a Java object or primitive and a +/// JSON representation \p json of the value of a Java object or primitive of a +/// compatible type, adds statements to \p block to assign \p expr to the +/// deterministic value specified by \p json. +/// The expected format of the JSON representation is mostly the same as that +/// of the json-io serialization library (https://github.com/jdereg/json-io) if +/// run with the following options, as of version 4.10.1: +/// - A type name map with identity mappings such as +/// `("java.lang.Boolean", "java.lang.Boolean")` for all primitive wrapper +/// types, java.lang.Class, java.lang.String and java.util.Date. That is, we +/// are not using the json-io default shorthands for those types. +/// - `WRITE_LONGS_AS_STRINGS` should be set to `true` to avoid a loss of +/// precision when representing longs. +/// +/// Some examples of json-io representations that may not be obvious include: +/// - The representation of a Java object generally may or may not contain a +/// `"@type"` key. The value corresponding to such a key specifies the runtime +/// type of the object (or the boxed type if the object is primitive). If no +/// `"@type"` key is present, it is assumed that the runtime type is the same +/// as the compile-time type. Most reference-typed objects are represented as +/// JSON objects (i.e. key-value maps) either way, so the `"@type"` key is +/// just an additional key in the map. However, primitive types, arrays and +/// string types without a `"@type"` key are not represented as JSON objects. +/// For example, "untyped" ints are just represented as e.g. 1234, i.e. a JSON +/// number. The "typed" version of this int then becomes +/// `{"@type":"java.lang.Integer","value":1234}`, i.e. a JSON object, with the +/// original ("untyped") JSON number stored in the "value" entry. For arrays, +/// the corresponding key is called "@items", not "value". Typed versions of +/// primitive types are probably not necessary, but json-io will sometimes +/// produce such values, which is why we support both typed and untyped +/// versions. +/// - The way we deal with reference-equal objects is that they all get assigned +/// the same ID, and exactly one of them will have an `{"@id": some_ID}` +/// entry, in addition to its usual representation. All the other objects with +/// this ID are represented simply as `{"@ref": some_ID}`, with no further +/// entries. +/// +/// The above rule has the following exceptions: +/// - It seems that strings are always printed in "primitive" representation by +/// json-io, i.e.\ they are always JSON strings, and never JSON objects with +/// a `@type` key. For cases where we don't know that an expression has a +/// string type (e.g.\ if its type is generic and specialized to +/// java.lang.String), we need to sometimes represent strings as JSON objects +/// with a `@type` key. In this case, the content of the string will be the +/// value associated with a `value` key (similarly to StringBuilder in +/// json-io). See \ref get_untyped_string. +/// - json-io does not include the `ordinal` field of enums in its +/// representation, but our algorithm depends on it being present. It may be +/// possible to rewrite parts of it to set the ordinal depending on the order +/// of elements seen in the `$VALUES` array, but it would generally make +/// things more complicated. +/// +/// For examples of JSON representations of objects, see the regression tests +/// for this feature in +/// jbmc/regression/jbmc/deterministic_assignments_json. +/// +/// Known limitations: +/// - If two reference-equal objects are defined in the same function, they are +/// correctly assigned the same value. +/// However, the case where they are defined in two different functions is not +/// supported. The object that is stored as a `{"@ref":1}` or similar will +/// generally either point to a freshly allocated symbol or an out-of-scope +/// symbol. The `{"@id":1}` (or similar) object may be assigned correctly, or +/// it may point to an out-of-scope symbol. This is because the symbol for the +/// shared value is currently allocated dynamically. To fix this limitation, +/// static allocation would have to be used instead, together with a static +/// boolean to keep track of whether or not the symbol has been allocated +/// already. +/// - The special floating-point values NaN and positive/negative infinity are +/// not supported. Note that in json-io 4.10.1, these are printed as "null". +/// Future versions of json-io will support these values, and this function +/// should be consistent with that if possible. +/// - json-io prints \\uFFFF as a single character, which is not read correctly +/// by the JSON parser. +/// - Not all assignments have source locations, and those that do only link to +/// a function, not a line number. +/// +/// For parameter documentation, see \ref object_creation_infot. +void assign_from_json( + const exprt &expr, + const jsont &json, + const irep_idt &function_id, + code_blockt &block, + symbol_table_baset &symbol_table, + optionalt &needed_lazy_methods, + size_t max_user_array_length, + std::unordered_map &references); + +#endif // CPROVER_JAVA_BYTECODE_ASSIGNMENTS_FROM_JSON_H diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index fb0e8a7f043..2506bc3cb8c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -87,6 +87,10 @@ void parse_java_language_options(const cmdlinet &cmd, optionst &options) options.set_option( "java-cp-include-files", cmd.get_value("java-cp-include-files")); } + if(cmd.isset("static-values")) + { + options.set_option("static-values", cmd.get_value("static-values")); + } } /// Consume options that are java bytecode specific. @@ -177,6 +181,7 @@ void java_bytecode_languaget::set_language_options(const optionst &options) java_cp_include_files=".*"; nondet_static = options.get_bool_option("nondet-static"); + static_values_file = options.get_option("static-values"); language_options_initialized=true; } @@ -784,11 +789,11 @@ bool java_bytecode_languaget::typecheck( symbol_table, symbol_table_journal.get_inserted(), synthetic_methods); } - // For each class that will require a static initializer wrapper, create a - // function named package.classname::clinit_wrapper, and a corresponding - // global tracking whether it has run or not: - create_static_initializer_wrappers( - symbol_table, synthetic_methods, threading_support); + create_static_initializer_symbols( + symbol_table, + synthetic_methods, + threading_support, + !static_values_file.empty()); // Now incrementally elaborate methods // that are reachable from this entry point. @@ -1086,6 +1091,7 @@ bool java_bytecode_languaget::convert_single_method( function_id, symbol_table, nondet_static, + !static_values_file.empty(), object_factory_parameters, get_pointer_type_selector(), get_message_handler()); @@ -1094,10 +1100,27 @@ bool java_bytecode_languaget::convert_single_method( function_id, symbol_table, nondet_static, + !static_values_file.empty(), object_factory_parameters, get_pointer_type_selector(), get_message_handler()); break; + case synthetic_method_typet::USER_SPECIFIED_STATIC_INITIALIZER: + { + const auto class_name = + declaring_class(symbol_table.lookup_ref(function_id)); + INVARIANT( + class_name, "user_specified_clinit must be declared by a class."); + writable_symbol.value = get_user_specified_clinit_body( + *class_name, + static_values_file, + symbol_table, + get_message_handler(), + needed_lazy_methods, + max_user_array_length, + references); + break; + } case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER: writable_symbol.value = stub_global_initializer_factory.get_stub_initializer_body( diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 64ef639061c..7f745981a3c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H +#include "assignments_from_json.h" #include "ci_lazy_methods.h" #include "ci_lazy_methods_needed.h" #include "java_class_loader.h" @@ -39,7 +40,8 @@ Author: Daniel Kroening, kroening@kroening.com "(no-lazy-methods)" \ "(lazy-methods-extra-entry-point):" \ "(java-load-class):" \ - "(java-no-load-class):" + "(java-no-load-class):" \ + "(static-values):" #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \ " --disable-uncaught-exception-check\n" \ @@ -71,7 +73,13 @@ Author: Daniel Kroening, kroening@kroening.com " METHODNAME can be a regex that will be matched\n" /* NOLINT(*) */ \ " against all symbols. If missing a java:: prefix\n" /* NOLINT(*) */ \ " will be added. If no descriptor is found, all\n"/* NOLINT(*) */ \ - " overloads of a method will also be added.\n" + " overloads of a method will also be added.\n" \ + " --static-values f Load initial values of static fields from the given\n"/* NOLINT(*) */ \ + " JSON file. We assign static fields to these values\n"/* NOLINT(*) */ \ + " instead of calling the normal static initializer\n"/* NOLINT(*) */ \ + " (clinit) method.\n" \ + " The argument can be a relative or absolute path to\n"/* NOLINT(*) */ \ + " the file.\n" // clang-format on class symbolt; @@ -197,6 +205,10 @@ class java_bytecode_languaget:public languaget java_string_library_preprocesst string_preprocess; std::string java_cp_include_files; bool nondet_static; + /// Path to a JSON file which contains initial values of static fields (right + /// after the static initializer of the class was run). This is read from the + /// --static-values command-line option. + std::string static_values_file; // list of classes to force load even without reference from the entry point std::vector java_load_classes; @@ -216,6 +228,12 @@ class java_bytecode_languaget:public languaget std::unordered_set no_load_classes; std::vector extra_methods; + + /// Map used in all calls to functions that deterministically create objects + /// (currently only \ref assign_from_json). + /// It tracks objects that should be reference-equal to each other by mapping + /// IDs of such objects to symbols that store their values. + std::unordered_map references; }; std::unique_ptr new_java_bytecode_language(); diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 0c8c8221901..9bb4ee4c0db 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -10,11 +10,12 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "java_object_factory.h" #include "java_utils.h" #include -#include -#include +#include +#include #include +#include +#include #include -#include /// The three states in which a `` method for a class can be before, /// after, and during static class initialization. These states are only used @@ -52,6 +53,7 @@ static typet clinit_states_type() // Disable linter here to allow a std::string constant, since that holds // a length, whereas a cstr would require strlen every time. const std::string clinit_wrapper_suffix = "::clinit_wrapper"; // NOLINT(*) +const std::string user_specified_clinit_suffix = "::user_specified_clinit"; // NOLINT(*) const std::string clinit_function_suffix = ".:()V"; // NOLINT(*) /// Get the Java static initializer wrapper name for a given class (the wrapper @@ -65,6 +67,11 @@ irep_idt clinit_wrapper_name(const irep_idt &class_name) return id2string(class_name) + clinit_wrapper_suffix; } +irep_idt user_specified_clinit_name(const irep_idt &class_name) +{ + return id2string(class_name) + user_specified_clinit_suffix; +} + /// Check if function_id is a clinit wrapper /// \param function_id: some function identifier /// \return true if the passed identifier is a clinit wrapper @@ -190,6 +197,8 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state) /// \param class_name: name of the class to generate clinit wrapper calls for /// \param [out] init_body: appended with calls to clinit wrapper /// \param nondet_static: true if nondet-static option was given +/// \param replace_clinit: true iff calls to clinit are replaced with calls to +/// user_specified_clinit. /// \param object_factory_parameters: object factory parameters used to populate /// nondet-initialized globals and objects reachable from them (only needed /// if nondet-static is true) @@ -201,6 +210,7 @@ static void clinit_wrapper_do_recursive_calls( const irep_idt &class_name, code_blockt &init_body, const bool nondet_static, + const bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler) @@ -214,8 +224,10 @@ static void clinit_wrapper_do_recursive_calls( init_body.add(code_function_callt{base_init_func->symbol_expr()}); } - const irep_idt &real_clinit_name = clinit_function_name(class_name); - if(const auto clinit_func = symbol_table.lookup(real_clinit_name)) + const irep_idt &clinit_name = replace_clinit + ? user_specified_clinit_name(class_name) + : clinit_function_name(class_name); + if(const auto clinit_func = symbol_table.lookup(clinit_name)) init_body.add(code_function_callt{clinit_func->symbol_expr()}); // If nondet-static option is given, add a standard nondet initialization for @@ -291,6 +303,65 @@ static bool needs_clinit_wrapper( return false; } +static void create_function_symbol( + const irep_idt &class_name, + const irep_idt &function_name, + const irep_idt &function_base_name, + const synthetic_method_typet &synthetic_method_type, + symbol_tablet &symbol_table, + synthetic_methods_mapt &synthetic_methods) +{ + symbolt function_symbol; + const java_method_typet function_type({}, java_void_type()); + function_symbol.name = function_name; + function_symbol.pretty_name = function_symbol.name; + function_symbol.base_name = function_base_name; + function_symbol.type = function_type; + // This provides a back-link from a method to its associated class, as is done + // for java_bytecode_convert_methodt::convert. + set_declaring_class(function_symbol, class_name); + function_symbol.mode = ID_java; + bool failed = symbol_table.add(function_symbol); + INVARIANT(!failed, id2string(function_base_name) + " symbol should be fresh"); + + auto insert_result = + synthetic_methods.emplace(function_symbol.name, synthetic_method_type); + INVARIANT( + insert_result.second, + "synthetic methods map should not already contain entry for " + + id2string(function_base_name)); +} + +// Create symbol for the "clinit_wrapper" +static void create_clinit_wrapper_function_symbol( + const irep_idt &class_name, + symbol_tablet &symbol_table, + synthetic_methods_mapt &synthetic_methods) +{ + create_function_symbol( + class_name, + clinit_wrapper_name(class_name), + "clinit_wrapper", + synthetic_method_typet::STATIC_INITIALIZER_WRAPPER, + symbol_table, + synthetic_methods); +} + +// Create symbol for the "user_specified_clinit" +static void create_user_specified_clinit_function_symbol( + const irep_idt &class_name, + symbol_tablet &symbol_table, + synthetic_methods_mapt &synthetic_methods) +{ + create_function_symbol( + class_name, + user_specified_clinit_name(class_name), + "user_specified_clinit", + synthetic_method_typet::USER_SPECIFIED_STATIC_INITIALIZER, + symbol_table, + synthetic_methods); +} + /// Creates a static initializer wrapper symbol for the given class, along with /// a global boolean that tracks if it has been run already. /// \param class_name: class symbol name @@ -345,27 +416,8 @@ static void create_clinit_wrapper_symbols( true); } - // Create symbol for the "clinit_wrapper" - symbolt wrapper_method_symbol; - const java_method_typet wrapper_method_type({}, java_void_type()); - wrapper_method_symbol.name = clinit_wrapper_name(class_name); - wrapper_method_symbol.pretty_name = wrapper_method_symbol.name; - wrapper_method_symbol.base_name = "clinit_wrapper"; - wrapper_method_symbol.type = wrapper_method_type; - // This provides a back-link from a method to its associated class, as is done - // for java_bytecode_convert_methodt::convert. - set_declaring_class(wrapper_method_symbol, class_name); - wrapper_method_symbol.mode = ID_java; - bool failed = symbol_table.add(wrapper_method_symbol); - INVARIANT(!failed, "clinit-wrapper symbol should be fresh"); - - auto insert_result = synthetic_methods.emplace( - wrapper_method_symbol.name, - synthetic_method_typet::STATIC_INITIALIZER_WRAPPER); - INVARIANT( - insert_result.second, - "synthetic methods map should not already contain entry for " - "clinit wrapper"); + create_clinit_wrapper_function_symbol( + class_name, symbol_table, synthetic_methods); } /// Thread safe version of the static initializer. @@ -436,6 +488,8 @@ static void create_clinit_wrapper_symbols( /// name created by `create_clinit_wrapper_symbols`) /// \param symbol_table: global symbol table /// \param nondet_static: true if nondet-static option was given +/// \param replace_clinit: true iff calls to clinit are replaced with calls to +/// user_specified_clinit. /// \param object_factory_parameters: object factory parameters used to populate /// nondet-initialized globals and objects reachable from them (only needed /// if nondet-static is true) @@ -447,6 +501,7 @@ code_blockt get_thread_safe_clinit_wrapper_body( const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, + const bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler) @@ -599,6 +654,7 @@ code_blockt get_thread_safe_clinit_wrapper_body( *class_name, init_body, nondet_static, + replace_clinit, object_factory_parameters, pointer_type_selector, message_handler); @@ -628,6 +684,8 @@ code_blockt get_thread_safe_clinit_wrapper_body( /// name created by `create_clinit_wrapper_symbols`) /// \param symbol_table: global symbol table /// \param nondet_static: true if nondet-static option was given +/// \param replace_clinit: true iff calls to clinit are replaced with calls to +/// user_specified_clinit. /// \param object_factory_parameters: object factory parameters used to populate /// nondet-initialized globals and objects reachable from them (only needed /// if nondet-static is true) @@ -639,6 +697,7 @@ code_ifthenelset get_clinit_wrapper_body( const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, + const bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler) @@ -683,6 +742,7 @@ code_ifthenelset get_clinit_wrapper_body( *class_name, init_body, nondet_static, + replace_clinit, object_factory_parameters, pointer_type_selector, message_handler); @@ -691,17 +751,91 @@ code_ifthenelset get_clinit_wrapper_body( return code_ifthenelset(std::move(check_already_run), std::move(init_body)); } -/// Create static initializer wrappers for all classes that need them. +code_blockt get_user_specified_clinit_body( + const irep_idt &class_id, + const std::string &static_values_file, + symbol_table_baset &symbol_table, + message_handlert &message_handler, + optionalt needed_lazy_methods, + size_t max_user_array_length, + std::unordered_map &references) +{ + jsont json; + if( + !static_values_file.empty() && + !parse_json(static_values_file, message_handler, json) && json.is_object()) + { + const auto &json_object = to_json_object(json); + const auto class_entry = + json_object.find(id2string(strip_java_namespace_prefix(class_id))); + if(class_entry != json_object.end()) + { + const auto &class_json_value = class_entry->second; + if(class_json_value.is_object()) + { + const auto &class_json_object = to_json_object(class_json_value); + std::map static_field_values; + for(const auto &symbol_pair : symbol_table) + { + const symbolt &symbol = symbol_pair.second; + if( + declaring_class(symbol) && *declaring_class(symbol) == class_id && + symbol.is_static_lifetime) + { + const symbol_exprt &static_field_expr = symbol.symbol_expr(); + const auto &static_field_entry = + class_json_object.find(id2string(symbol.base_name)); + if(static_field_entry != class_json_object.end()) + { + static_field_values.insert( + {static_field_expr, static_field_entry->second}); + } + } + } + code_blockt body; + for(const auto &value_pair : static_field_values) + { + assign_from_json( + value_pair.first, + value_pair.second, + clinit_function_name(class_id), + body, + symbol_table, + needed_lazy_methods, + max_user_array_length, + references); + } + return body; + } + } + } + const irep_idt &real_clinit_name = clinit_function_name(class_id); + if(const auto clinit_func = symbol_table.lookup(real_clinit_name)) + return code_blockt{{code_function_callt{clinit_func->symbol_expr()}}}; + return code_blockt{}; +} + +/// Create static initializer wrappers and possibly user-specified functions for +/// initial static field value assignments for all classes that need them. +/// For each class that will require a static initializer wrapper, create a +/// function named package.classname::clinit_wrapper, and a corresponding +/// global tracking whether it has run or not. If a file containing initial +/// static values is given, also create a function named +/// package.classname::user_specified_clinit. /// \param symbol_table: global symbol table /// \param synthetic_methods: synthetic methods map. Will be extended noting /// that any wrapper belongs to this code, and so `get_clinit_wrapper_body` /// should be used to produce the method body when required. /// \param thread_safe: if true state variables required to make the /// clinit_wrapper thread safe will be created. -void create_static_initializer_wrappers( +/// \param is_user_clinit_needed: determines whether or not a symbol for the +/// synthetic user_specified_clinit function should be created. This is true +/// if a file was given with the --static-values option and false otherwise. +void create_static_initializer_symbols( symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, - const bool thread_safe) + const bool thread_safe, + const bool is_user_clinit_needed) { // Top-sort the class hierarchy, such that we visit parents before children, // and can so identify parents that need static initialisation by whether we @@ -718,6 +852,11 @@ void create_static_initializer_wrappers( { create_clinit_wrapper_symbols( class_identifier, symbol_table, synthetic_methods, thread_safe); + if(is_user_clinit_needed) + { + create_user_specified_clinit_function_symbol( + class_identifier, symbol_table, synthetic_methods); + } } } } diff --git a/jbmc/src/java_bytecode/java_static_initializers.h b/jbmc/src/java_bytecode/java_static_initializers.h index b4963d3c07a..70736244110 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.h +++ b/jbmc/src/java_bytecode/java_static_initializers.h @@ -9,6 +9,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com #ifndef CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H #define CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H +#include "assignments_from_json.h" +#include "ci_lazy_methods_needed.h" #include "java_object_factory_parameters.h" #include "select_pointer_type.h" #include "synthetic_methods_map.h" @@ -20,18 +22,21 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include irep_idt clinit_wrapper_name(const irep_idt &class_name); +irep_idt user_specified_clinit_name(const irep_idt &class_name); bool is_clinit_wrapper_function(const irep_idt &function_id); -void create_static_initializer_wrappers( +void create_static_initializer_symbols( symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, - const bool thread_safe); + const bool thread_safe, + const bool is_user_clinit_needed); code_blockt get_thread_safe_clinit_wrapper_body( const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, + const bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler); @@ -40,10 +45,43 @@ code_ifthenelset get_clinit_wrapper_body( const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, + const bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler); +/// Create the body of a user_specified_clinit function for a given class, which +/// includes assignments for all static fields of the class to values read from +/// an input file. If the file could not be parsed or an entry for this class +/// could not be found in it, the user_specified_clinit function will only +/// contain a call to the "real" clinit function, and not include any +/// assignments itself. If an entry for this class is found but some of its +/// static fields are not mentioned in the input file, those fields will be +/// assigned default values (zero or null). +/// \param class_id: the id of the class to create a user_specified_clinit +/// function body for. +/// \param static_values_file: input file containing values of static fields. +/// The format is expected to be a map whose keys are class names, and whose +/// values are maps from static field names to values. Currently only JSON +/// is supported as a file format. +/// \param symbol_table: used to look up and create new symbols +/// \param message_handler: used to log any errors with parsing the input file +/// \param needed_lazy_methods: used to mark any runtime types given in the +/// input file as needed +/// \param max_user_array_length: maximum value for constant or variable length +/// arrays. Any arrays that were specified to be of nondeterministic length in +/// the input file will be limited by this value. +/// \param references: map to keep track of reference-equal objets. +/// \return the body of the user_specified_clinit function as a code block. +code_blockt get_user_specified_clinit_body( + const irep_idt &class_id, + const std::string &static_values_file, + symbol_table_baset &symbol_table, + message_handlert &message_handler, + optionalt needed_lazy_methods, + size_t max_user_array_length, + std::unordered_map &references); + class stub_global_initializer_factoryt { /// Maps class symbols onto the stub globals that belong to them diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index a8b92121f17..6ee494e8e47 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -183,6 +183,18 @@ irep_idt resolve_friendly_method_name( } } +pointer_typet pointer_to_replacement_type( + const pointer_typet &given_pointer_type, + const java_class_typet &replacement_class_type) +{ + if(can_cast_type(given_pointer_type.subtype())) + { + struct_tag_typet struct_tag_subtype{replacement_class_type.get_name()}; + return pointer_type(struct_tag_subtype); + } + return pointer_type(replacement_class_type); +} + dereference_exprt checked_dereference(const exprt &expr) { dereference_exprt result(expr); diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index f2759395148..f0fe1e29f2d 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -77,6 +77,13 @@ irep_idt resolve_friendly_method_name( const symbol_table_baset &symbol_table, std::string &error); +/// Given a pointer type to a Java class and a type representing a more specific +/// Java class, return a pointer type to the more specific class with the same +/// structure as the original pointer type. +pointer_typet pointer_to_replacement_type( + const pointer_typet &given_pointer_type, + const java_class_typet &replacement_class_type); + /// Dereference an expression and flag it for a null-pointer check /// \param expr: expression to dereference and check dereference_exprt checked_dereference(const exprt &expr); diff --git a/jbmc/src/java_bytecode/synthetic_methods_map.h b/jbmc/src/java_bytecode/synthetic_methods_map.h index e7773da3612..26645c67e00 100644 --- a/jbmc/src/java_bytecode/synthetic_methods_map.h +++ b/jbmc/src/java_bytecode/synthetic_methods_map.h @@ -27,6 +27,12 @@ enum class synthetic_method_typet /// These are generated for both user and stub types, to ensure the actual /// static initializer is only run once on any given path. STATIC_INITIALIZER_WRAPPER, + /// Only exists if the `--static-values` option was used. + /// If a given type has an entry in the file given by this option, the "user + /// specified static initializer" contains a sequence of assignments from + /// static field expressions to values read from the file. + /// Otherwise, this function simply calls the regular clinit. + USER_SPECIFIED_STATIC_INITIALIZER, /// A generated (synthetic) static initializer function for a stub type. /// Because we don't have the bytecode for a stub type (by definition), we /// generate a static initializer function to initialize its static fields. diff --git a/src/util/Makefile b/src/util/Makefile index 0113f6bfed4..dd3b6cc43ad 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -1,5 +1,6 @@ SRC = allocate_objects.cpp \ arith_tools.cpp \ + array_element_from_pointer.cpp \ array_name.cpp \ base_type.cpp \ bv_arithmetic.cpp \ diff --git a/src/util/allocate_objects.cpp b/src/util/allocate_objects.cpp index 4d06024d428..684dc33d8ba 100644 --- a/src/util/allocate_objects.cpp +++ b/src/util/allocate_objects.cpp @@ -121,25 +121,7 @@ symbol_exprt allocate_objectst::allocate_automatic_local_object( return aux_symbol.symbol_expr(); } -/// Generates code for allocating a dynamic object. A new variable with basename -/// prefix `alloc_site` is introduced to which the allocated memory is assigned. -/// Then, the variable is assigned to `target_expr`. For example, with -/// `target_expr` being `*p` the following code is generated: -/// -/// `alloc_site$1 = ALLOCATE(object_size, FALSE);` -/// `*p = alloc_site$1;` -/// -/// The function returns a dereference expressiont that dereferences the -/// allocation site variable (e.g., `*alloc_site$1`) and which can be used to -/// initialize the allocated memory. -/// -/// \param output_code: Code block to which the necessary code is added -/// \param target_expr: A pointer to the allocated memory will be assigned to -/// this (lvalue) expression -/// \param allocate_type: Type of the object allocated -/// \return A dereference_exprt that dereferences the pointer to the allocated -/// memory, or an empty expression when `allocate_type` is void -exprt allocate_objectst::allocate_dynamic_object( +exprt allocate_objectst::allocate_dynamic_object_symbol( code_blockt &output_code, const exprt &target_expr, const typet &allocate_type) @@ -183,7 +165,16 @@ exprt allocate_objectst::allocate_dynamic_object( code.add_source_location() = source_location; output_code.add(code); - return dereference_exprt(malloc_sym.symbol_expr()); + return malloc_sym.symbol_expr(); +} + +exprt allocate_objectst::allocate_dynamic_object( + code_blockt &output_code, + const exprt &target_expr, + const typet &allocate_type) +{ + return dereference_exprt( + allocate_dynamic_object_symbol(output_code, target_expr, allocate_type)); } exprt allocate_objectst::allocate_non_dynamic_object( diff --git a/src/util/allocate_objects.h b/src/util/allocate_objects.h index 40a518a88dc..9e917e37c13 100644 --- a/src/util/allocate_objects.h +++ b/src/util/allocate_objects.h @@ -62,6 +62,29 @@ class allocate_objectst const typet &allocate_type, const irep_idt &basename_prefix = "tmp"); + /// Generates code for allocating a dynamic object. A new variable with + /// basename prefix `alloc_site` is introduced to which the allocated memory + /// is assigned. + /// Then, the variable is assigned to `target_expr`. For example, with + /// `target_expr` being `*p` the following code is generated: + /// + /// `alloc_site$1 = ALLOCATE(object_size, FALSE);` + /// `*p = alloc_site$1;` + /// + /// \param output_code: Code block to which the necessary code is added + /// \param target_expr: A pointer to the allocated memory will be assigned to + /// this (lvalue) expression + /// \param allocate_type: Type of the object allocated + /// \return The pointer to the allocated memory, or an empty expression + /// when `allocate_type` is void + exprt allocate_dynamic_object_symbol( + code_blockt &output_code, + const exprt &target_expr, + const typet &allocate_type); + + /// Generate the same code as \ref allocate_dynamic_object_symbol, but + /// return a dereference_exprt that dereferences the newly created pointer + /// to the allocated memory. exprt allocate_dynamic_object( code_blockt &output_code, const exprt &target_expr, diff --git a/src/util/array_element_from_pointer.cpp b/src/util/array_element_from_pointer.cpp new file mode 100644 index 00000000000..1639c772a5e --- /dev/null +++ b/src/util/array_element_from_pointer.cpp @@ -0,0 +1,18 @@ +/*******************************************************************\ + +Module: Element access in a pointer array + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include "array_element_from_pointer.h" + +dereference_exprt +array_element_from_pointer(const exprt &pointer, const exprt &index) +{ + PRECONDITION(can_cast_type(pointer.type())); + PRECONDITION( + index.type().id() == ID_signedbv || index.type().id() == ID_unsignedbv); + return dereference_exprt{plus_exprt{pointer, index}}; +} diff --git a/src/util/array_element_from_pointer.h b/src/util/array_element_from_pointer.h index a1315ddbbfe..fb7bf84bf7b 100644 --- a/src/util/array_element_from_pointer.h +++ b/src/util/array_element_from_pointer.h @@ -22,12 +22,6 @@ Author: Diffblue Ltd. /// \param index: index of the element to access /// \return expression representing the (\p index)'th element of the array dereference_exprt -array_element_from_pointer(const exprt &pointer, const exprt &index) -{ - PRECONDITION(can_cast_type(pointer.type())); - PRECONDITION( - index.type().id() == ID_signedbv || index.type().id() == ID_unsignedbv); - return dereference_exprt{plus_exprt{pointer, index}}; -} +array_element_from_pointer(const exprt &pointer, const exprt &index); #endif // CPROVER_UTIL_ARRAY_ELEMENT_FROM_POINTER_H diff --git a/src/util/json.h b/src/util/json.h index 55f59d6b62c..2f9db3b888a 100644 --- a/src/util/json.h +++ b/src/util/json.h @@ -446,4 +446,16 @@ inline const json_objectt &to_json_object(const jsont &json) return static_cast(json); } +inline json_stringt &to_json_string(jsont &json) +{ + PRECONDITION(json.kind == jsont::kindt::J_STRING); + return static_cast(json); +} + +inline const json_stringt &to_json_string(const jsont &json) +{ + PRECONDITION(json.kind == jsont::kindt::J_STRING); + return static_cast(json); +} + #endif // CPROVER_UTIL_JSON_H