diff --git a/jbmc/regression/jbmc/class-literals-static-state/pom.xml b/jbmc/regression/jbmc/class-literals-static-state/pom.xml new file mode 100644 index 000000000000..2986c14740c7 --- /dev/null +++ b/jbmc/regression/jbmc/class-literals-static-state/pom.xml @@ -0,0 +1,37 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.class-literals-static-state + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/class-literals-static-state/src/main/java/Test.java b/jbmc/regression/jbmc/class-literals-static-state/src/main/java/Test.java new file mode 100644 index 000000000000..d62037dca9b2 --- /dev/null +++ b/jbmc/regression/jbmc/class-literals-static-state/src/main/java/Test.java @@ -0,0 +1,13 @@ +public class Test { + static class A {} + + static class B {} + + public static void main() { + Class a = A.class; + Class b = B.class; + assert a != b; + // at least the class literals of A and B have been initialised + assert org.cprover.regression.ClassLiteralCounter.count[0] >= 2; + } +} diff --git a/jbmc/regression/jbmc/class-literals-static-state/src/main/java/java/lang/Class.java b/jbmc/regression/jbmc/class-literals-static-state/src/main/java/java/lang/Class.java new file mode 100644 index 000000000000..b5d5120a81eb --- /dev/null +++ b/jbmc/regression/jbmc/class-literals-static-state/src/main/java/java/lang/Class.java @@ -0,0 +1,25 @@ +package java.lang; + +public class Class { + + private String name; + + @org.cprover.MustNotThrow + public void cproverInitializeClassLiteral( + String name, + boolean isAnnotation, + boolean isArray, + boolean isInterface, + boolean isSynthetic, + boolean isLocalClass, + boolean isMemberClass, + boolean isEnum) { + this.name = name; + // a static field of another class, which must not be reset afterwards + org.cprover.regression.ClassLiteralCounter.count[0]++; + } + + public String getName() { return name; } + + public boolean desiredAssertionStatus() { return true; } +} diff --git a/jbmc/regression/jbmc/class-literals-static-state/src/main/java/org/cprover/regression/ClassLiteralCounter.java b/jbmc/regression/jbmc/class-literals-static-state/src/main/java/org/cprover/regression/ClassLiteralCounter.java new file mode 100644 index 000000000000..d81f2af34fc8 --- /dev/null +++ b/jbmc/regression/jbmc/class-literals-static-state/src/main/java/org/cprover/regression/ClassLiteralCounter.java @@ -0,0 +1,6 @@ +package org.cprover.regression; + +public class ClassLiteralCounter { + // Number of class literals that have been initialised + public static final int[] count = new int[1]; +} diff --git a/jbmc/regression/jbmc/class-literals-static-state/test.desc b/jbmc/regression/jbmc/class-literals-static-state/test.desc new file mode 100644 index 000000000000..3cc69197acbb --- /dev/null +++ b/jbmc/regression/jbmc/class-literals-static-state/test.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.main -cp target/classes +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +JBMC initialises class literals by calling cproverInitializeClassLiteral of the +model of java.lang.Class. Its effects on static fields must persist: class +literals must thus only be initialised once all other static symbols +(including the static fields of java.lang.Class and the flag recording whether +its static initializer has run) have been initialised. diff --git a/jbmc/regression/jbmc/get-class-for-name/classLiteral.desc b/jbmc/regression/jbmc/get-class-for-name/classLiteral.desc new file mode 100644 index 000000000000..02c3223b3990 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/classLiteral.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.classLiteral -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the same java.lang.Class object as +Class.forName, also for classes whose class literal the program does not +refer to, irrespective of which of the two is called first. JBMC obtains the +Class object of such a class from cproverGetClassObject of the model of +java.lang.Class on the first call of getClass for that class. diff --git a/jbmc/regression/jbmc/get-class-for-name/enumFlag.desc b/jbmc/regression/jbmc/get-class-for-name/enumFlag.desc new file mode 100644 index 000000000000..f27df42beda2 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/enumFlag.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.enumFlag -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the same java.lang.Class object as +Class.forName, also for classes whose class literal the program does not +refer to, irrespective of which of the two is called first. JBMC obtains the +Class object of such a class from cproverGetClassObject of the model of +java.lang.Class on the first call of getClass for that class. diff --git a/jbmc/regression/jbmc/get-class-for-name/firstCallOnBranch.desc b/jbmc/regression/jbmc/get-class-for-name/firstCallOnBranch.desc new file mode 100644 index 000000000000..3c3acc296ff6 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/firstCallOnBranch.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.firstCallOnBranch -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the same java.lang.Class object as +Class.forName, also for classes whose class literal the program does not +refer to, irrespective of which of the two is called first. JBMC obtains the +Class object of such a class from cproverGetClassObject of the model of +java.lang.Class on the first call of getClass for that class. diff --git a/jbmc/regression/jbmc/get-class-for-name/forNameThenGetClass.desc b/jbmc/regression/jbmc/get-class-for-name/forNameThenGetClass.desc new file mode 100644 index 000000000000..03e7c8bd3765 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/forNameThenGetClass.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.forNameThenGetClass -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the same java.lang.Class object as +Class.forName, also for classes whose class literal the program does not +refer to, irrespective of which of the two is called first. JBMC obtains the +Class object of such a class from cproverGetClassObject of the model of +java.lang.Class on the first call of getClass for that class. diff --git a/jbmc/regression/jbmc/get-class-for-name/getClassThenForName.desc b/jbmc/regression/jbmc/get-class-for-name/getClassThenForName.desc new file mode 100644 index 000000000000..83df332a74b7 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/getClassThenForName.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.getClassThenForName -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the same java.lang.Class object as +Class.forName, also for classes whose class literal the program does not +refer to, irrespective of which of the two is called first. JBMC obtains the +Class object of such a class from cproverGetClassObject of the model of +java.lang.Class on the first call of getClass for that class. diff --git a/jbmc/regression/jbmc/get-class-for-name/mustFail.desc b/jbmc/regression/jbmc/get-class-for-name/mustFail.desc new file mode 100644 index 000000000000..bfe980189104 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/mustFail.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.mustFail -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=10$ +^SIGNAL=0$ +^\[java::Test\.mustFail:\(\)V\.assertion\.1\] line 54 .*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +The Class objects of different classes must be distinct. diff --git a/jbmc/regression/jbmc/get-class-for-name/objectReceiver.desc b/jbmc/regression/jbmc/get-class-for-name/objectReceiver.desc new file mode 100644 index 000000000000..a17c99453cc9 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/objectReceiver.desc @@ -0,0 +1,12 @@ +CORE +Test +--function Test.objectReceiver -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Objects whose runtime type is java.lang.Object use the model of +Object.getClass, which calls Class.forName; their Class object must be the +class literal of java.lang.Object, and differ from those of other classes. diff --git a/jbmc/regression/jbmc/get-class-for-name/pom.xml b/jbmc/regression/jbmc/get-class-for-name/pom.xml new file mode 100644 index 000000000000..438b42ada37f --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/pom.xml @@ -0,0 +1,37 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.get-class-for-name + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/get-class-for-name/src/main/java/Test.java b/jbmc/regression/jbmc/get-class-for-name/src/main/java/Test.java new file mode 100644 index 000000000000..ac807b139cad --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/src/main/java/Test.java @@ -0,0 +1,56 @@ +public class Test { + static class A {} + static class B {} + static class C {} + enum E { X } + + public static void forNameThenGetClass() { + Class c = Class.forName("Test$A"); + assert new A().getClass() == c; + assert Class.forName("Test$A") == c; + } + + public static void getClassThenForName() { + Class c = new A().getClass(); + assert Class.forName("Test$A") == c; + } + + public static void classLiteral() { + assert Class.forName("Test$C") == C.class; + assert new C().getClass() == C.class; + } + + public static void twoClasses() { + Class a = Class.forName("Test$A"); + Class b = Class.forName("Test$B"); + assert new B().getClass() == b; + assert new A().getClass() == a; + assert a != b; + } + + public static void firstCallOnBranch(boolean nondet) { + if (nondet) + new A().getClass(); + Class c = new A().getClass(); + assert Class.forName("Test$A") == c; + } + + public static void enumFlag() { + Class c = Class.forName("Test$E"); + assert E.X.getClass() == c; + assert c.isEnum(); + } + + public static void objectReceiver() { + Object o = new Object(); + assert o.getClass() == Object.class; + assert new Object().getClass() == o.getClass(); + Object a = new A(); + assert a.getClass() != o.getClass(); + } + + public static void mustFail() { + Class c = Class.forName("Test$A"); + assert new B().getClass() == c; + } +} diff --git a/jbmc/regression/jbmc/get-class-for-name/src/main/java/java/lang/Class.java b/jbmc/regression/jbmc/get-class-for-name/src/main/java/java/lang/Class.java new file mode 100644 index 000000000000..7bc5a9cf95c8 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/src/main/java/java/lang/Class.java @@ -0,0 +1,74 @@ +package java.lang; + +// A minimal model of java.lang.Class with unique Class objects per name, which +// provides cproverGetClassObject for JBMC's implementation of getClass. +public class Class { + private String name; + private boolean cproverIsEnum; + private Class cproverNextClass; + + // Class literals that JBMC initialises in __CPROVER_initialize + private static final Class[] literals = new Class[1]; + // Class objects created by forName or cproverGetClassObject + private static final Class[] others = new Class[1]; + + public String getName() { return name; } + public boolean isEnum() { return cproverIsEnum; } + public boolean desiredAssertionStatus() { return true; } + + private static Class findOther(String name) { + for (Class c = others[0]; c != null; c = c.cproverNextClass) + if (name.equals(c.name)) + return c; + return null; + } + + private static Class newOther(String name) { + Class c = new Class<>(); + c.name = name; + c.cproverNextClass = others[0]; + others[0] = c; + return c; + } + + public static Class forName(String name) { + for (Class c = literals[0]; c != null; c = c.cproverNextClass) + if (name.equals(c.name)) + return c; + Class c = findOther(name); + return c != null ? c : newOther(name); + } + + @org.cprover.MustNotThrow + public void cproverInitializeClassLiteral( + String name, + boolean isAnnotation, + boolean isArray, + boolean isInterface, + boolean isSynthetic, + boolean isLocalClass, + boolean isMemberClass, + boolean isEnum) { + this.name = name; + this.cproverIsEnum = isEnum; + cproverNextClass = literals[0]; + literals[0] = this; + } + + @org.cprover.MustNotThrow + private static Class cproverGetClassObject( + String name, + boolean isAnnotation, + boolean isArray, + boolean isInterface, + boolean isSynthetic, + boolean isLocalClass, + boolean isMemberClass, + boolean isEnum) { + Class c = findOther(name); + if (c == null) + c = newOther(name); + c.cproverIsEnum = isEnum; + return c; + } +} diff --git a/jbmc/regression/jbmc/get-class-for-name/threading.desc b/jbmc/regression/jbmc/get-class-for-name/threading.desc new file mode 100644 index 000000000000..447cc55507ea --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/threading.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.forNameThenGetClass --java-threading -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +With --java-threading, getClass obtains the Class object using the same +protocol as the thread-safe static initializer wrappers. diff --git a/jbmc/regression/jbmc/get-class-for-name/twoClasses.desc b/jbmc/regression/jbmc/get-class-for-name/twoClasses.desc new file mode 100644 index 000000000000..cb0305aabf50 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/twoClasses.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.twoClasses -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the same java.lang.Class object as +Class.forName, also for classes whose class literal the program does not +refer to, irrespective of which of the two is called first. JBMC obtains the +Class object of such a class from cproverGetClassObject of the model of +java.lang.Class on the first call of getClass for that class. diff --git a/jbmc/regression/jbmc/get-class-invokespecial/pom.xml b/jbmc/regression/jbmc/get-class-invokespecial/pom.xml new file mode 100644 index 000000000000..ee9cfaad48cc --- /dev/null +++ b/jbmc/regression/jbmc/get-class-invokespecial/pom.xml @@ -0,0 +1,34 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.get-class-invokespecial + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + com.github.abextm + jasmin-maven-plugin + + + + + diff --git a/jbmc/regression/jbmc/get-class-invokespecial/src/main/java/A.j b/jbmc/regression/jbmc/get-class-invokespecial/src/main/java/A.j new file mode 100644 index 000000000000..ba3dc5596fbe --- /dev/null +++ b/jbmc/regression/jbmc/get-class-invokespecial/src/main/java/A.j @@ -0,0 +1,8 @@ +.class public A +.super java/lang/Object + +.method public ()V + aload_0 + invokespecial java/lang/Object/()V + return +.end method diff --git a/jbmc/regression/jbmc/get-class-invokespecial/src/main/java/B.j b/jbmc/regression/jbmc/get-class-invokespecial/src/main/java/B.j new file mode 100644 index 000000000000..c979f3836cb5 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-invokespecial/src/main/java/B.j @@ -0,0 +1,47 @@ +.class public B +.super A + +.method public ()V + aload_0 + invokespecial A/()V + return +.end method + +.method public viaSuper()Ljava/lang/Class; + .limit stack 1 + .limit locals 1 + aload_0 + invokespecial A/getClass()Ljava/lang/Class; + areturn +.end method + +; assert new B().viaSuper() == new B().getClass(); +; assert new B().viaSuper() != new A().getClass(); +.method public static test()V + .limit stack 3 + .limit locals 0 + new B + dup + invokespecial B/()V + invokevirtual B/viaSuper()Ljava/lang/Class; + new B + dup + invokespecial B/()V + invokevirtual java/lang/Object/getClass()Ljava/lang/Class; + if_acmpne fail + new B + dup + invokespecial B/()V + invokevirtual B/viaSuper()Ljava/lang/Class; + new A + dup + invokespecial A/()V + invokevirtual java/lang/Object/getClass()Ljava/lang/Class; + if_acmpeq fail + return +fail: + new java/lang/AssertionError + dup + invokespecial java/lang/AssertionError/()V + athrow +.end method diff --git a/jbmc/regression/jbmc/get-class-invokespecial/test.desc b/jbmc/regression/jbmc/get-class-invokespecial/test.desc new file mode 100644 index 000000000000..cd8a40477083 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-invokespecial/test.desc @@ -0,0 +1,13 @@ +CORE +B +--function B.test -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +super.getClass() must return the Class object of the runtime type of the +receiver, as Object.getClass is final. javac emits invokespecial +java/lang/Object/getClass for super.getClass(), but other compilers may name +the superclass (here: A) instead, which must not bind to A's getClass override. diff --git a/jbmc/regression/jbmc/get-class/classLiteral.desc b/jbmc/regression/jbmc/get-class/classLiteral.desc new file mode 100644 index 000000000000..a2e67e7d5cb9 --- /dev/null +++ b/jbmc/regression/jbmc/get-class/classLiteral.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.classLiteral -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the unique java.lang.Class object of the runtime +type of the receiver, which is also the class literal of that type. diff --git a/jbmc/regression/jbmc/get-class/differentClass.desc b/jbmc/regression/jbmc/get-class/differentClass.desc new file mode 100644 index 000000000000..28826e0bf159 --- /dev/null +++ b/jbmc/regression/jbmc/get-class/differentClass.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.differentClass -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the unique java.lang.Class object of the runtime +type of the receiver, which is also the class literal of that type. diff --git a/jbmc/regression/jbmc/get-class/mustFail.desc b/jbmc/regression/jbmc/get-class/mustFail.desc new file mode 100644 index 000000000000..0b8e1d907e7a --- /dev/null +++ b/jbmc/regression/jbmc/get-class/mustFail.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.mustFail -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 58 .*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +Objects of different runtime types have different Class objects. diff --git a/jbmc/regression/jbmc/get-class/noClassLiteral.desc b/jbmc/regression/jbmc/get-class/noClassLiteral.desc new file mode 100644 index 000000000000..ee1426260e14 --- /dev/null +++ b/jbmc/regression/jbmc/get-class/noClassLiteral.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.noClassLiteral -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the unique java.lang.Class object of the runtime +type of the receiver, which is also the class literal of that type. diff --git a/jbmc/regression/jbmc/get-class/pom.xml b/jbmc/regression/jbmc/get-class/pom.xml new file mode 100644 index 000000000000..ebf9a029ee4d --- /dev/null +++ b/jbmc/regression/jbmc/get-class/pom.xml @@ -0,0 +1,37 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.get-class + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/get-class/sameClass.desc b/jbmc/regression/jbmc/get-class/sameClass.desc new file mode 100644 index 000000000000..be50905e6ef0 --- /dev/null +++ b/jbmc/regression/jbmc/get-class/sameClass.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.sameClass -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the unique java.lang.Class object of the runtime +type of the receiver, which is also the class literal of that type. diff --git a/jbmc/regression/jbmc/get-class/src/main/java/Test.java b/jbmc/regression/jbmc/get-class/src/main/java/Test.java new file mode 100644 index 000000000000..d844f80d7eab --- /dev/null +++ b/jbmc/regression/jbmc/get-class/src/main/java/Test.java @@ -0,0 +1,60 @@ +public class Test { + static class A { + int x; + + A(int x) { + this.x = x; + } + + @Override + public boolean equals(Object o) { + // a common idiom, which requires Class objects to be unique + if(o == null || getClass() != o.getClass()) + return false; + return x == ((A)o).x; + } + } + + static class B extends A { + B(int x) { + super(x); + } + } + + // no class literal of C appears in this program + static class C { + } + + public static void sameClass(int i) { + A a1 = new A(i); + A a2 = new A(i); + assert a1.getClass() == a2.getClass(); + assert a1.equals(a2); + } + + public static void classLiteral() { + A a = new A(1); + assert a.getClass() == A.class; + assert a.getClass() != B.class; + } + + public static void differentClass(int i) { + A a = new A(i); + B b = new B(i); + assert a.getClass() != b.getClass(); + assert !a.equals(b); + } + + public static void noClassLiteral() { + Object c1 = new C(); + Object c2 = new C(); + assert c1.getClass() == c2.getClass(); + assert c1.getClass().getName().equals("Test$C"); + } + + public static void mustFail(int i) { + A a = new A(i); + B b = new B(i); + assert a.getClass() == b.getClass(); + } +} diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 0dff8aa4ddb2..bca53c21d261 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -69,6 +69,7 @@ char1 class-fields class-literals + class-literals-static-state class-loading-annotations class_hierarchy Class_method1 @@ -163,6 +164,9 @@ function3 function4 generic_base_type + get-class + get-class-for-name + get-class-invokespecial generic_class_bound1 generic_function_parameter generic_static_field diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index a6e650389dc0..66e75806f614 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2236,8 +2236,19 @@ void java_bytecode_convert_methodt::convert_invoke( exprt::operandst &results) { const bool use_this(statement != "invokestatic"); + // Object.getClass is final, so that getClass always returns the Class object + // of the runtime type of the receiver, also when called via invokespecial + // (super.getClass()). Bind such calls dynamically, so that they reach the + // override of the runtime type that java_bytecode_languaget creates, rather + // than that of the class that invokespecial names (javac names + // java.lang.Object, other compilers may name the superclass). + const bool is_get_class_call = + statement == "invokespecial" && + class_method_descriptor.mangled_method_name() == + "getClass:()Ljava/lang/Class;"; const bool is_virtual( - statement == "invokevirtual" || statement == "invokeinterface"); + statement == "invokevirtual" || statement == "invokeinterface" || + is_get_class_call); const irep_idt &invoked_method_id = class_method_descriptor.get_identifier(); INVARIANT( @@ -2292,7 +2303,7 @@ void java_bytecode_convert_methodt::convert_invoke( needed_lazy_methods->add_needed_class(class_id); method_type.set_is_constructor(); } - else + else if(!is_get_class_call) method_type.set(ID_java_super_method_call, true); } } diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index b982ff625b00..22efba9e67cb 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -18,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -791,6 +793,395 @@ static void create_stub_global_symbols( } } +/// Name of the global that \ref get_class_method_body uses to store the +/// java.lang.Class object of \p class_id if the program does not refer to +/// its class literal. It is null until getClass is first called on an object +/// of that class. +static irep_idt lazy_class_object_name(const irep_idt &class_id) +{ + return id2string(class_id) + "@class_object"; +} + +/// Name of the global that, with --java-threading, records whether a thread +/// has started (1) or completed (2) obtaining the Class object stored in +/// \ref lazy_class_object_name. +static irep_idt lazy_class_object_state_name(const irep_idt &class_id) +{ + return id2string(class_id) + "@class_object_state"; +} + +/// Signature of the method of the model of java.lang.Class that returns the +/// Class object of a class whose class literal the program does not refer +/// to. It takes the same arguments as cproverInitializeClassLiteral, and +/// returns the Class object that Class.forName created for this class, if +/// any, and a new one otherwise. +static const irep_idt &class_object_factory_signature() +{ + static const irep_idt signature = + "java::java.lang.Class.cproverGetClassObject:" + "(Ljava/lang/String;ZZZZZZZ)Ljava/lang/Class;"; + return signature; +} + +static const irep_idt &object_get_class_name() +{ + static const irep_idt name = + "java::java.lang.Object.getClass:()Ljava/lang/Class;"; + return name; +} + +/// For each class that can have instances, add a method `getClass` that +/// overrides java.lang.Object.getClass and returns the class's Class object +/// (see \ref get_class_method_body). Only the symbols are created here, the +/// bodies are generated when the methods are converted, so that this is +/// compatible with lazy loading: context-insensitive lazy loading only converts +/// the overrides of classes that are instantiated, and symex-driven lazy +/// loading converts those of the runtime types that symbolic execution +/// encounters. Any symbols that the bodies use are created up front, as all +/// globals must exist before __CPROVER_initialize is generated. +/// \param symbol_table: global symbol table +/// \param synthetic_methods: synthetic method map, to which the methods are +/// added +/// \param threading_support: true if --java-threading was given +static void create_get_class_methods( + symbol_table_baset &symbol_table, + synthetic_methods_mapt &synthetic_methods, + bool threading_support) +{ + const symbolt *object_get_class = + symbol_table.lookup(object_get_class_name()); + if(object_get_class == nullptr || object_get_class->value.is_not_nil()) + return; + + const bool have_class_object_factory = + symbol_table.has_symbol(class_object_factory_signature()); + const bool have_class_literal_initializer = + symbol_table.has_symbol(get_java_class_literal_initializer_signature()); + + // Careful not to add to the symbol table while iterating over it + std::vector class_ids; + for(const auto &entry : symbol_table) + { + const symbolt &symbol = entry.second; + if( + !symbol.is_type || symbol.mode != ID_java || + !can_cast_type(symbol.type) || + symbol.name == "java::java.lang.Object" || is_java_array_tag(symbol.name)) + { + continue; + } + const java_class_typet &class_type = to_java_class_type(symbol.type); + if(class_type.get_interface() || class_type.get_abstract()) + continue; + class_ids.push_back(symbol.name); + } + + const java_method_typet &object_get_class_type = + to_java_method_type(object_get_class->type); + for(const irep_idt &class_id : class_ids) + { + const irep_idt method_id = + id2string(class_id) + ".getClass:()Ljava/lang/Class;"; + if(symbol_table.has_symbol(method_id)) + continue; + + // If the program does not refer to the class literal, the Class object + // is only created or initialised once getClass is first called for this + // class (see get_class_method_body): initialising the class literals of + // all classes in __CPROVER_initialize would be expensive with + // symex-driven lazy loading, which does not remove unused globals. + const irep_idt literal_id = id2string(class_id) + JAVA_CLASS_MODEL_SUFFIX; + if( + !symbol_table.has_symbol(literal_id) && + (have_class_object_factory || have_class_literal_initializer)) + { + if(!have_class_object_factory) + { + get_or_create_class_literal_symbol(class_id, symbol_table); + symbol_table.get_writeable_ref(literal_id) + .type.set(ID_C_no_initialization_required, true); + } + + const typet &class_reference_type = object_get_class_type.return_type(); + symbolt class_object_symbol{ + lazy_class_object_name(class_id), class_reference_type, ID_java}; + class_object_symbol.base_name = + id2string(class_object_symbol.name).substr(6); + class_object_symbol.is_lvalue = true; + class_object_symbol.is_state_var = true; + class_object_symbol.is_static_lifetime = true; + class_object_symbol.value = + null_pointer_exprt{to_pointer_type(class_reference_type)}; + symbol_table.add(class_object_symbol); + + if(threading_support) + { + symbolt state_symbol{ + lazy_class_object_state_name(class_id), java_int_type(), ID_java}; + state_symbol.base_name = id2string(state_symbol.name).substr(6); + state_symbol.is_lvalue = true; + state_symbol.is_state_var = true; + state_symbol.is_static_lifetime = true; + state_symbol.value = from_integer(0, java_int_type()); + symbol_table.add(state_symbol); + } + } + else + get_or_create_class_literal_symbol(class_id, symbol_table); + + java_method_typet method_type = object_get_class_type; + method_type.set_is_final(true); + auto &this_param = method_type.parameters().front(); + this_param.type() = java_reference_type(struct_tag_typet{class_id}); + this_param.set_base_name("this"); + this_param.set_identifier(id2string(method_id) + "::this"); + + symbolt method_symbol{method_id, method_type, ID_java}; + method_symbol.base_name = "getClass"; + method_symbol.pretty_name = id2string(class_id).substr(6) + ".getClass()"; + set_declaring_class(method_symbol, class_id); + symbol_table.add(method_symbol); + synthetic_methods[method_id] = synthetic_method_typet::GET_CLASS; + } +} + +/// Body of an override of java.lang.Object.getClass created by +/// \ref create_get_class_methods for class C. If the program refers to the +/// class literal of C, which __CPROVER_initialize then initialises, or the +/// model of java.lang.Class has neither cproverGetClassObject nor +/// cproverInitializeClassLiteral: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// return &C@class_model; +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// Otherwise, the Class object is obtained on the first call from the model +/// of java.lang.Class, which returns the object that Class.forName created +/// for C, if any. The name is obtained via CProver.classIdentifier, as no new +/// String literals can be created at this point: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// if(C@class_object == null) +/// C@class_object = Class.cproverGetClassObject( +/// CProver.classIdentifier(this), ...); +/// return C@class_object; +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// With --java-threading, only one thread obtains the Class object, and other +/// threads wait for it to complete, as in the thread-safe static initializer +/// wrappers (see get_thread_safe_clinit_wrapper_body): +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// ATOMIC_BEGIN +/// assume(C@class_object_state != 1); +/// must_init = C@class_object_state == 0; +/// if(must_init) +/// C@class_object_state = 1; +/// ATOMIC_END +/// if(must_init) +/// { +/// C@class_object = Class.cproverGetClassObject(...); +/// ATOMIC_BEGIN +/// C@class_object_state = 2; +/// ATOMIC_END +/// } +/// return C@class_object; +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// Obtaining the Class object does not call getClass for C, so that this does +/// not need to handle recursive initialisation as the static initializer +/// wrappers do. +/// With a model of java.lang.Class that does not have cproverGetClassObject, +/// the class literal is initialised instead, in the same way as +/// java_static_lifetime_init does: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// if(C@class_object == null) +/// { +/// C@class_model = { zero-initialised object of type java.lang.Class }; +/// C@class_model.cproverInitializeClassLiteral( +/// CProver.classIdentifier(this), ...); +/// C@class_object = &C@class_model; +/// } +/// return C@class_object; +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// \param function_id: name of the method +/// \param symbol_table: global symbol table +/// \param threading_support: true if --java-threading was given +/// \param message_handler: message handler +/// \return code of the method +static codet get_class_method_body( + const irep_idt &function_id, + symbol_table_baset &symbol_table, + bool threading_support, + message_handlert &message_handler) +{ + const symbolt &symbol = symbol_table.lookup_ref(function_id); + const java_method_typet &method_type = to_java_method_type(symbol.type); + for(const auto ¶meter : method_type.parameters()) + { + parameter_symbolt parameter_symbol; + parameter_symbol.name = parameter.get_identifier(); + parameter_symbol.base_name = parameter.get_base_name(); + parameter_symbol.mode = ID_java; + parameter_symbol.type = parameter.type(); + symbol_table.add(parameter_symbol); + } + + const auto class_id = declaring_class(symbol); + INVARIANT(class_id.has_value(), "getClass override must have a class"); + const source_locationt &loc = symbol.location; + const irep_idt literal_id = id2string(*class_id) + JAVA_CLASS_MODEL_SUFFIX; + + code_blockt code; + + const symbolt *class_object = + symbol_table.lookup(lazy_class_object_name(*class_id)); + if(class_object == nullptr) + { + code.add(code_frontend_returnt{typecast_exprt::conditional_cast( + address_of_exprt{symbol_table.lookup_ref(literal_id).symbol_expr()}, + method_type.return_type())}); + return std::move(code); + } + + const symbolt *factory = + symbol_table.lookup(class_object_factory_signature()); + const symbolt *initializer = + symbol_table.lookup(get_java_class_literal_initializer_signature()); + INVARIANT( + factory != nullptr || initializer != nullptr, + "create_get_class_methods only creates " + id2string(class_object->name) + + " if the model of java.lang.Class can initialise it"); + const java_method_typet &callee_type = + to_java_method_type((factory != nullptr ? factory : initializer)->type); + // cproverGetClassObject is static, cproverInitializeClassLiteral takes the + // class literal as its first argument + const typet &string_type = + callee_type.parameters()[factory != nullptr ? 0 : 1].type(); + + code_blockt init; + + exprt name = null_pointer_exprt{to_pointer_type(string_type)}; + const symbolt *class_identifier = symbol_table.lookup( + "java::org.cprover.CProver.classIdentifier:" + "(Ljava/lang/Object;)Ljava/lang/String;"); + if(class_identifier != nullptr) + { + const symbolt &name_symbol = fresh_java_symbol( + string_type, "class_name", loc, function_id, symbol_table); + init.add(code_frontend_declt{name_symbol.symbol_expr()}); + const java_method_typet &class_identifier_type = + to_java_method_type(class_identifier->type); + init.add(code_function_callt{ + name_symbol.symbol_expr(), + class_identifier->symbol_expr(), + {typecast_exprt::conditional_cast( + symbol_exprt{ + method_type.parameters()[0].get_identifier(), + method_type.parameters()[0].type()}, + class_identifier_type.parameters()[0].type())}}); + name = name_symbol.symbol_expr(); + } + + const java_class_typet &class_type = + to_java_class_type(symbol_table.lookup_ref(*class_id).type); + auto constant_bool = [](bool b) + { return from_integer(b ? 1 : 0, java_boolean_type()); }; + const side_effect_expr_nondett nondet_bool{java_boolean_type(), loc}; + // Argument order is: name, isAnnotation, isArray, isInterface, + // isSynthetic, isLocalClass, isMemberClass, isEnum + exprt::operandst arguments{ + name, + constant_bool(class_type.get_is_annotation()), + constant_bool(false), + constant_bool(class_type.get_interface()), + constant_bool(class_type.get_synthetic()), + nondet_bool, + nondet_bool, + constant_bool(class_type.get_is_enumeration())}; + + const symbol_exprt class_object_expr = class_object->symbol_expr(); + if(factory != nullptr) + { + const symbolt &result_symbol = fresh_java_symbol( + callee_type.return_type(), + "class_object", + loc, + function_id, + symbol_table); + init.add(code_frontend_declt{result_symbol.symbol_expr()}); + init.add(code_function_callt{ + result_symbol.symbol_expr(), + factory->symbol_expr(), + std::move(arguments)}); + init.add(code_frontend_assignt{ + class_object_expr, + typecast_exprt::conditional_cast( + result_symbol.symbol_expr(), class_object_expr.type())}); + } + else + { + const symbol_exprt class_literal = + symbol_table.lookup_ref(literal_id).symbol_expr(); + const namespacet ns{symbol_table}; + auto zero_object = zero_initializer(class_literal.type(), loc, ns); + if(!zero_object.has_value()) + { + messaget log{message_handler}; + log.error() << "failed to zero-initialize " << class_literal.identifier() + << messaget::eom; + throw 0; + } + set_class_identifier( + to_struct_expr(*zero_object), + ns, + to_struct_tag_type(class_literal.type())); + init.add(code_frontend_assignt{class_literal, *zero_object}); + + arguments.insert(arguments.begin(), address_of_exprt{class_literal}); + init.add( + code_function_callt{initializer->symbol_expr(), std::move(arguments)}); + init.add(code_frontend_assignt{ + class_object_expr, + typecast_exprt::conditional_cast( + address_of_exprt{class_literal}, class_object_expr.type())}); + } + + const symbolt *state = + symbol_table.lookup(lazy_class_object_state_name(*class_id)); + if(threading_support && state != nullptr) + { + const symbol_exprt state_expr = state->symbol_expr(); + auto state_value = [](int value) + { return from_integer(value, java_int_type()); }; + const symbolt &must_init = fresh_java_symbol( + java_boolean_type(), "must_init", loc, function_id, symbol_table); + const symbol_exprt must_init_expr = must_init.symbol_expr(); + code.add(code_frontend_declt{must_init_expr}); + code.add(codet{ID_atomic_begin}); + code.add(code_assumet{notequal_exprt{state_expr, state_value(1)}}); + code.add(code_frontend_assignt{ + must_init_expr, + typecast_exprt{ + equal_exprt{state_expr, state_value(0)}, java_boolean_type()}}); + code.add(code_ifthenelset{ + equal_exprt{state_expr, state_value(0)}, + code_frontend_assignt{state_expr, state_value(1)}}); + code.add(codet{ID_atomic_end}); + init.add(codet{ID_atomic_begin}); + init.add(code_frontend_assignt{state_expr, state_value(2)}); + init.add(codet{ID_atomic_end}); + code.add(code_ifthenelset{ + notequal_exprt{must_init_expr, from_integer(0, java_boolean_type())}, + std::move(init)}); + } + else + { + code.add(code_ifthenelset{ + equal_exprt{ + class_object_expr, + null_pointer_exprt{to_pointer_type(class_object_expr.type())}}, + std::move(init)}); + } + code.add(code_frontend_returnt{typecast_exprt::conditional_cast( + class_object_expr, method_type.return_type())}); + return std::move(code); +} + bool java_bytecode_languaget::typecheck( symbol_table_baset &symbol_table, const std::string &, @@ -936,6 +1327,9 @@ bool java_bytecode_languaget::typecheck( } } + create_get_class_methods( + symbol_table, synthetic_methods, language_options->threading_support); + messaget log(message_handler); log.status() << "Java: added " << (symbol_table.symbols.size() - before_constant_globals_size) @@ -1437,6 +1831,13 @@ bool java_bytecode_languaget::convert_single_method_code( writable_symbol.value = invokedynamic_synthetic_method( function_id, symbol_table, message_handler); break; + case synthetic_method_typet::GET_CLASS: + writable_symbol.value = get_class_method_body( + function_id, + symbol_table, + language_options->threading_support, + message_handler); + break; case synthetic_method_typet::CREATE_ARRAY_WITH_TYPE: { INVARIANT( diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index fa074554c8e5..8ac95439cca4 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -265,17 +265,39 @@ void java_static_lifetime_init( for(const auto &entry : symbol_table.symbols) symbol_names.insert(id2string(entry.first)); + // Class literals are initialised by calling a method of the model of + // java.lang.Class, which may access static fields and thus run static + // initializers. Initialise class literals only once all other static symbols + // have been initialised: otherwise, zero-initialising a static field, or the + // flag that records whether a static initializer has run, may undo the + // effects of that method. + std::set class_literals; + bool class_literal_phase = false; std::set additional_symbols; - while(!symbol_names.empty() || !additional_symbols.empty()) + while(true) { if(!additional_symbols.empty()) symbol_names.swap(additional_symbols); + else if(symbol_names.empty()) + { + if(class_literal_phase || class_literals.empty()) + break; + class_literal_phase = true; + symbol_names.swap(class_literals); + } for(const auto &symbol_name : symbol_names) { const symbolt &sym = symbol_table.lookup_ref(symbol_name); if(should_init_symbol(sym)) { + if( + !class_literal_phase && + get_class_literal_initializer(sym, symbol_table) != nullptr) + { + class_literals.insert(symbol_name); + continue; + } auto new_symbols = init_symbol( sym, code_block, diff --git a/jbmc/src/java_bytecode/synthetic_methods_map.h b/jbmc/src/java_bytecode/synthetic_methods_map.h index bfe203cfadee..27d430f190b5 100644 --- a/jbmc/src/java_bytecode/synthetic_methods_map.h +++ b/jbmc/src/java_bytecode/synthetic_methods_map.h @@ -49,7 +49,11 @@ enum class synthetic_method_typet INVOKEDYNAMIC_METHOD, /// Our internal implementation of CProver.createArrayWithType, which needs to /// access internal type-id fields - CREATE_ARRAY_WITH_TYPE + CREATE_ARRAY_WITH_TYPE, + /// An override of java.lang.Object.getClass in a class C, which returns the + /// class literal of C. Virtual method dispatch then makes getClass return + /// the unique java.lang.Class object of the runtime type of the receiver. + GET_CLASS }; /// Maps method names on to a synthetic method kind.