diff --git a/src/main/java/java/lang/Class.java b/src/main/java/java/lang/Class.java index 832ad57..763a129 100644 --- a/src/main/java/java/lang/Class.java +++ b/src/main/java/java/lang/Class.java @@ -39,6 +39,58 @@ import org.cprover.CProver; +/** + * Instances of the class {@code Class} represent classes and + * interfaces in a running Java application. An enum is a kind of + * class and an annotation is a kind of interface. Every array also + * belongs to a class that is reflected as a {@code Class} object + * that is shared by all arrays with the same element type and number + * of dimensions. The primitive Java types ({@code boolean}, + * {@code byte}, {@code char}, {@code short}, + * {@code int}, {@code long}, {@code float}, and + * {@code double}), and the keyword {@code void} are also + * represented as {@code Class} objects. + * + *

{@code Class} has no public constructor. Instead {@code Class} + * objects are constructed automatically by the Java Virtual Machine as classes + * are loaded and by calls to the {@code defineClass} method in the class + * loader. + * + *

The following example uses a {@code Class} object to print the + * class name of an object: + * + * 

+ *     void printClassName(Object obj) {
+ *         System.out.println("The class of " + obj +
+ *                            " is " + obj.getClass().getName());
+ *     }
+ *
+ * + *

It is also possible to get the {@code Class} object for a named + * type (or for void) using a class literal. See Section 15.8.2 of + * The Java™ Language Specification. + * For example: + * + *

+ * {@code System.out.println("The name of class Foo is: "+Foo.class.getName());} + *
+ * + * @param the type of the class modeled by this {@code Class} + * object. For example, the type of {@code String.class} is {@code + * Class}. Use {@code Class} if the class being modeled is + * unknown. + * + * @author unascribed + * @see java.lang.ClassLoader#defineClass(byte[], int, int) + * @since JDK1.0 + * + * @diffblue.limitedSupport + * Generated tests that create an instance of Class will be incorrect: + * + */ public final class Class { private Class() {} @@ -55,6 +107,13 @@ private Class() {} private boolean cproverIsMemberClass; private boolean cproverIsEnum; + // TODO: these fields are to enforce singleton semantics of + // Class objects as returned by Object.getClass() and Class.forName() + // The size is currently hard-coded which may lead to incorrect results. + // A map could be used here in future. + private static String[] cproverClassNames = new String[8]; + private static Class[] cproverClassInstances = new Class[8]; + public String toString() { return (isInterface() ? "interface " : (isPrimitive() ? "" : "class ")) + getName(); @@ -111,9 +170,21 @@ public String toGenericString() { // forName method. The goal is to correctly model combinations of forName // and getName, but precisely following the JDK behaviour is more involved. public static Class forName(String className) { - Class c=new Class(); - c.name=className; - return c; + String foundName = null; + for (int i = 0; i < cproverClassNames.length; ++i) { + String currentName = cproverClassNames[i]; + if (currentName == null) { + Class c = new Class(); + c.name = className; + cproverClassNames[i] = className; + cproverClassInstances[i] = c; + return c; + } + if (className.equals(currentName)) { + return cproverClassInstances[i]; + } + } + return CProver.nondetWithoutNullForNotModelled(); } public static Class forName(String name, boolean initialize, @@ -453,6 +524,7 @@ private static boolean desiredAssertionStatus0(Class clazz) { protected void cproverNondetInitialize() { CProver.assume(name != null); CProver.assume(enumConstantDirectory == null); + CProver.assume(classValueMap == null); } // DIFFBLUE MODEL LIBRARY @@ -607,6 +679,13 @@ public Method getMethod(String name, Class... parameterTypes) throws NoSuchMe return new Method(this, name, parameterTypes); } + // DIFFBLUE MODEL LIBRARY + // This field is never read in our model. We include them because ClassValue + // (in the java library, not our models) references it, so it is needed to + // make ClassValue compile. + // transient ClassValue.ClassValueMap classValueMap; + transient ClassValue.ClassValueMap classValueMap = null; + /** * Returns the {@code Class} representing the component type of an * array. If this class does not represent an array class this method @@ -615,10 +694,12 @@ public Method getMethod(String name, Class... parameterTypes) throws NoSuchMe * @return the {@code Class} representing the component type of this * class if this class is an array * @see java.lang.reflect.Array - * @since 1.1 + * @since JDK1.1 + * @diffblue.noSupport */ + // public native Class getComponentType(); public Class getComponentType() { CProver.notModelled(); - return CProver.nondetWithoutNullForNotModelled(); + return CProver.nondetWithNullForNotModelled(); } } diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java index 390e734..e43cb1f 100644 --- a/src/main/java/java/lang/String.java +++ b/src/main/java/java/lang/String.java @@ -2996,8 +2996,7 @@ public String replaceAll(String regex, String replacement) { // return Pattern.compile(regex).matcher(this).replaceAll(replacement); // DIFFBLUE MODELS LIBRARY: we assume the expression is just a string literal - CProver.assume( - regex.indexOf('[') == -1 && + if (regex.indexOf('[') == -1 && regex.indexOf(']') == -1 && regex.indexOf('.') == -1 && regex.indexOf('\\') == -1 && @@ -3010,8 +3009,12 @@ public String replaceAll(String regex, String replacement) regex.indexOf('}') == -1 && regex.indexOf('|') == -1 && regex.indexOf('(') == -1 && - regex.indexOf(')') == -1); - return replace(regex, replacement); + regex.indexOf(')') == -1) { + return replace(regex, replacement); + } else { + CProver.notModelled(); + return CProver.nondetWithNullForNotModelled(); + } } /** @@ -4330,7 +4333,7 @@ public static String valueOf(float f) { */ public static String valueOf(double d) { // string solver only knows how to convert floats to string - return CProverString.toString(d); + return CProverString.toString((float)d); // return Double.toString(d); } diff --git a/src/main/java/java/util/Objects.java b/src/main/java/java/util/Objects.java new file mode 100644 index 0000000..57c9c71 --- /dev/null +++ b/src/main/java/java/util/Objects.java @@ -0,0 +1,298 @@ +/* + * Copyright (c) 2009, 2013, Oracle and/or its affiliates. All rights reserved. + * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER. + * + * This code is free software; you can redistribute it and/or modify it + * under the terms of the GNU General Public License version 2 only, as + * published by the Free Software Foundation. Oracle designates this + * particular file as subject to the "Classpath" exception as provided + * by Oracle in the LICENSE file that accompanied this code. + * + * This code is distributed in the hope that it will be useful, but WITHOUT + * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or + * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License + * version 2 for more details (a copy is included in the LICENSE file that + * accompanied this code). + * + * You should have received a copy of the GNU General Public License version + * 2 along with this work; if not, write to the Free Software Foundation, + * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA. + * + * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA + * or visit www.oracle.com if you need additional information or have any + * questions. + */ + +package java.util; + +import java.util.function.Supplier; + +/** + * This class consists of {@code static} utility methods for operating + * on objects. These utilities include {@code null}-safe or {@code + * null}-tolerant methods for computing the hash code of an object, + * returning a string for an object, and comparing two objects. + * + * @since 1.7 + */ +public final class Objects { + private Objects() { + throw new AssertionError("No java.util.Objects instances for you!"); + } + + /** + * Returns {@code true} if the arguments are equal to each other + * and {@code false} otherwise. + * Consequently, if both arguments are {@code null}, {@code true} + * is returned and if exactly one argument is {@code null}, {@code + * false} is returned. Otherwise, equality is determined by using + * the {@link Object#equals equals} method of the first + * argument. + * + * @param a an object + * @param b an object to be compared with {@code a} for equality + * @return {@code true} if the arguments are equal to each other + * and {@code false} otherwise + * @see Object#equals(Object) + */ + public static boolean equals(Object a, Object b) { + return (a == b) || (a != null && a.equals(b)); + } + + /** + * Returns {@code true} if the arguments are deeply equal to each other + * and {@code false} otherwise. + * + * Two {@code null} values are deeply equal. If both arguments are + * arrays, the algorithm in {@link Arrays#deepEquals(Object[], + * Object[]) Arrays.deepEquals} is used to determine equality. + * Otherwise, equality is determined by using the {@link + * Object#equals equals} method of the first argument. + * + * @param a an object + * @param b an object to be compared with {@code a} for deep equality + * @return {@code true} if the arguments are deeply equal to each other + * and {@code false} otherwise + * @see Arrays#deepEquals(Object[], Object[]) + * @see Objects#equals(Object, Object) + */ + public static boolean deepEquals(Object a, Object b) { + if (a == b) + return true; + else if (a == null || b == null) + return false; + else + return Arrays.deepEquals0(a, b); + } + + /** + * Returns the hash code of a non-{@code null} argument and 0 for + * a {@code null} argument. + * + * @param o an object + * @return the hash code of a non-{@code null} argument and 0 for + * a {@code null} argument + * @see Object#hashCode + */ + public static int hashCode(Object o) { + return o != null ? o.hashCode() : 0; + } + + /** + * Generates a hash code for a sequence of input values. The hash + * code is generated as if all the input values were placed into an + * array, and that array were hashed by calling {@link + * Arrays#hashCode(Object[])}. + * + *

This method is useful for implementing {@link + * Object#hashCode()} on objects containing multiple fields. For + * example, if an object that has three fields, {@code x}, {@code + * y}, and {@code z}, one could write: + * + * 

+    * @Override public int hashCode() {
+    *     return Objects.hash(x, y, z);
+    * }
+    *
+ * + * Warning: When a single object reference is supplied, the returned + * value does not equal the hash code of that object reference. This + * value can be computed by calling {@link #hashCode(Object)}. + * + * @param values the values to be hashed + * @return a hash value of the sequence of input values + * @see Arrays#hashCode(Object[]) + * @see List#hashCode + */ + public static int hash(Object... values) { + return Arrays.hashCode(values); + } + + /** + * Returns the result of calling {@code toString} for a non-{@code + * null} argument and {@code "null"} for a {@code null} argument. + * + * @param o an object + * @return the result of calling {@code toString} for a non-{@code + * null} argument and {@code "null"} for a {@code null} argument + * @see Object#toString + * @see String#valueOf(Object) + */ + public static String toString(Object o) { + return String.valueOf(o); + } + + /** + * Returns the result of calling {@code toString} on the first + * argument if the first argument is not {@code null} and returns + * the second argument otherwise. + * + * @param o an object + * @param nullDefault string to return if the first argument is + * {@code null} + * @return the result of calling {@code toString} on the first + * argument if it is not {@code null} and the second argument + * otherwise. + * @see Objects#toString(Object) + */ + public static String toString(Object o, String nullDefault) { + return (o != null) ? o.toString() : nullDefault; + } + + /** + * Returns 0 if the arguments are identical and {@code + * c.compare(a, b)} otherwise. + * Consequently, if both arguments are {@code null} 0 + * is returned. + * + *

Note that if one of the arguments is {@code null}, a {@code + * NullPointerException} may or may not be thrown depending on + * what ordering policy, if any, the {@link Comparator Comparator} + * chooses to have for {@code null} values. + * + * @param the type of the objects being compared + * @param a an object + * @param b an object to be compared with {@code a} + * @param c the {@code Comparator} to compare the first two arguments + * @return 0 if the arguments are identical and {@code + * c.compare(a, b)} otherwise. + * @see Comparable + * @see Comparator + */ + public static int compare(T a, T b, Comparator c) { + return (a == b) ? 0 : c.compare(a, b); + } + + /** + * Checks that the specified object reference is not {@code null}. This + * method is designed primarily for doing parameter validation in methods + * and constructors, as demonstrated below: + * 

+     * public Foo(Bar bar) {
+     *     this.bar = Objects.requireNonNull(bar);
+     * }
+     *
+ * + * @param obj the object reference to check for nullity + * @param the type of the reference + * @return {@code obj} if not {@code null} + * @throws NullPointerException if {@code obj} is {@code null} + * + * @diffblue.fullSupport + * @diffblue.untested + * We do not have tests for this method, but it is called from some tested + * modelled methods. + */ + public static T requireNonNull(T obj) { + if (obj == null) + throw new NullPointerException(); + return obj; + } + + /** + * Checks that the specified object reference is not {@code null} and + * throws a customized {@link NullPointerException} if it is. This method + * is designed primarily for doing parameter validation in methods and + * constructors with multiple parameters, as demonstrated below: + * 
+     * public Foo(Bar bar, Baz baz) {
+     *     this.bar = Objects.requireNonNull(bar, "bar must not be null");
+     *     this.baz = Objects.requireNonNull(baz, "baz must not be null");
+     * }
+     *
+ * + * @param obj the object reference to check for nullity + * @param message detail message to be used in the event that a {@code + * NullPointerException} is thrown + * @param the type of the reference + * @return {@code obj} if not {@code null} + * @throws NullPointerException if {@code obj} is {@code null} + */ + public static T requireNonNull(T obj, String message) { + if (obj == null) + throw new NullPointerException(message); + return obj; + } + + /** + * Returns {@code true} if the provided reference is {@code null} otherwise + * returns {@code false}. + * + * @apiNote This method exists to be used as a + * {@link java.util.function.Predicate}, {@code filter(Objects::isNull)} + * + * @param obj a reference to be checked against {@code null} + * @return {@code true} if the provided reference is {@code null} otherwise + * {@code false} + * + * @see java.util.function.Predicate + * @since 1.8 + */ + public static boolean isNull(Object obj) { + return obj == null; + } + + /** + * Returns {@code true} if the provided reference is non-{@code null} + * otherwise returns {@code false}. + * + * @apiNote This method exists to be used as a + * {@link java.util.function.Predicate}, {@code filter(Objects::nonNull)} + * + * @param obj a reference to be checked against {@code null} + * @return {@code true} if the provided reference is non-{@code null} + * otherwise {@code false} + * + * @see java.util.function.Predicate + * @since 1.8 + */ + public static boolean nonNull(Object obj) { + return obj != null; + } + + /** + * Checks that the specified object reference is not {@code null} and + * throws a customized {@link NullPointerException} if it is. + * + *

Unlike the method {@link #requireNonNull(Object, String)}, + * this method allows creation of the message to be deferred until + * after the null check is made. While this may confer a + * performance advantage in the non-null case, when deciding to + * call this method care should be taken that the costs of + * creating the message supplier are less than the cost of just + * creating the string message directly. + * + * @param obj the object reference to check for nullity + * @param messageSupplier supplier of the detail message to be + * used in the event that a {@code NullPointerException} is thrown + * @param the type of the reference + * @return {@code obj} if not {@code null} + * @throws NullPointerException if {@code obj} is {@code null} + * @since 1.8 + */ + public static T requireNonNull(T obj, Supplier messageSupplier) { + if (obj == null) + throw new NullPointerException(messageSupplier.get()); + return obj; + } +} diff --git a/src/main/java/java/util/regex/Pattern.java b/src/main/java/java/util/regex/Pattern.java index ae980dd..ff12bfe 100644 --- a/src/main/java/java/util/regex/Pattern.java +++ b/src/main/java/java/util/regex/Pattern.java @@ -1157,9 +1157,9 @@ public int flags() { * no characters that has special meaning in regular expressions. * This way we can then match the regex using String.equals(). */ - private static void cproverAssumeIsPlainString(String regex) + private static boolean cproverIsPlainString(String regex) { - CProver.assume( + return regex.indexOf('[') == -1 && regex.indexOf(']') == -1 && regex.indexOf('{') == -1 && @@ -1173,7 +1173,11 @@ private static void cproverAssumeIsPlainString(String regex) regex.indexOf('*') == -1 && regex.indexOf('^') == -1 && regex.indexOf('$') == -1 && - regex.indexOf('|') == -1); + regex.indexOf('|') == -1; + } + private static void cproverAssumeIsPlainString(String regex) + { + CProver.assume(cproverIsPlainString(regex)); } /** @@ -1210,14 +1214,18 @@ public static boolean matches(String regex, CharSequence input) { // Matcher m = p.matcher(input); // return m.matches(); - // DIFFBLUE MODEL LIBRARY - // We disallow special characters so that we can do matching using equals. - cproverAssumeIsPlainString(regex); // if (input == null) { throw new NullPointerException(); // JDK throws NPE when the 2nd param is null } - return regex.equals(input); + // DIFFBLUE MODEL LIBRARY + // We disallow special characters so that we can do matching using equals. + if (cproverIsPlainString(regex)) { + return regex.equals(input); + } else { + CProver.notModelled(); + return CProver.nondetBoolean(); + } } /** @@ -1441,7 +1449,9 @@ public static String quote(String s) { private Pattern(String p, int f) { // DIFFBLUE MODEL LIBRARY // We disallow special characters so that we can use equals for matching. - cproverAssumeIsPlainString(p); + if (!cproverIsPlainString(p)) { + CProver.notModelled(); + } pattern = p; // pattern = p; // flags = f;