From acbde73f294a50fb5b4be3787d2870dcc271929c Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 19 Oct 2019 18:30:36 +0100 Subject: [PATCH 1/7] Make unsupported case notModelled instead of using assume Under-approximated models can lead to spurious UNSAT results in JBMC; however, we can mark over-approximated cases as notModelled and JBMC will detect them and give a warning that behaviour is over-approximating when reporting SAT. --- src/main/java/java/lang/String.java | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java index 390e734..c662869 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(); + } } /** From 695c8b545c355f0eb800ea7a7f0f9533bb7c4194 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 19 Oct 2019 18:31:27 +0100 Subject: [PATCH 2/7] Add missing cast Without the cast we get a spurious UNSAT. --- src/main/java/java/lang/String.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java index c662869..e43cb1f 100644 --- a/src/main/java/java/lang/String.java +++ b/src/main/java/java/lang/String.java @@ -4333,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); } From e36bb5d3b55879535458925504cfc78ed1b01d79 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 19 Oct 2019 18:31:52 +0100 Subject: [PATCH 3/7] Make unsupported case notModelled instead of using assume Under-approximated models can lead to spurious UNSAT results in JBMC; however, we can mark over-approximated cases as notModelled and JBMC will detect them and give a warning that behaviour is over-approximating when reporting SAT. --- src/main/java/java/util/regex/Pattern.java | 26 +++++++++++++++------- 1 file changed, 18 insertions(+), 8 deletions(-) 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; From 893ecd9eefd91697a450c010496216c9ef2b76c4 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 24 Nov 2019 12:34:37 +0000 Subject: [PATCH 4/7] Update to models-library@4d20c50 --- src/main/java/java/lang/Class.java | 66 +++++++++++++++++++++++++++++- 1 file changed, 64 insertions(+), 2 deletions(-) diff --git a/src/main/java/java/lang/Class.java b/src/main/java/java/lang/Class.java index 832ad57..2ff53ac 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: + *
    + *
  • TG-7636: IllegalAccessError error when attempting to set the java.lang.class via reflection
    • + *
  • TG-4727: When test-gen mocks java.lang.Class, it causes IllegalAccessError
    • + *
+ */ public final class Class { private Class() {} @@ -453,6 +505,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 +660,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 +675,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(); } } From f468b64f8b0bf63457347ab0e238e5e001c6e5b8 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 24 Nov 2019 12:35:09 +0000 Subject: [PATCH 5/7] Add java.util.Objects --- src/main/java/java/util/Objects.java | 298 +++++++++++++++++++++++++++ 1 file changed, 298 insertions(+) create mode 100644 src/main/java/java/util/Objects.java 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; + } +} From cfc3ce9dd0aee31e6be459b0baf4f792fbba3e07 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 24 Nov 2019 13:05:08 +0000 Subject: [PATCH 6/7] A partial solution for Class object singletons This is necessary to make comparisons such as o.getClass() == o.getClass() succeed. --- src/main/java/java/lang/Class.java | 25 ++++++++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) diff --git a/src/main/java/java/lang/Class.java b/src/main/java/java/lang/Class.java index 2ff53ac..763a129 100644 --- a/src/main/java/java/lang/Class.java +++ b/src/main/java/java/lang/Class.java @@ -107,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(); @@ -163,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, From 749e3388ad16eddab86d5e6f485fd0fe9da9e6c8 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 14 Nov 2020 18:11:45 +0000 Subject: [PATCH 7/7] Add java.net.URLDecoder --- src/main/java/java/net/URLDecoder.java | 207 +++++++++++++++++++++++++ 1 file changed, 207 insertions(+) create mode 100644 src/main/java/java/net/URLDecoder.java diff --git a/src/main/java/java/net/URLDecoder.java b/src/main/java/java/net/URLDecoder.java new file mode 100644 index 0000000..1e1138a --- /dev/null +++ b/src/main/java/java/net/URLDecoder.java @@ -0,0 +1,207 @@ +/* + * Copyright (c) 1998, 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.net; + +import java.io.*; + +/** + * Utility class for HTML form decoding. This class contains static methods + * for decoding a String from the application/x-www-form-urlencoded + * MIME format. + *

+ * The conversion process is the reverse of that used by the URLEncoder class. It is assumed + * that all characters in the encoded string are one of the following: + * "{@code a}" through "{@code z}", + * "{@code A}" through "{@code Z}", + * "{@code 0}" through "{@code 9}", and + * "{@code -}", "{@code _}", + * "{@code .}", and "{@code *}". The + * character "{@code %}" is allowed but is interpreted + * as the start of a special escaped sequence. + *

+ * The following rules are applied in the conversion: + * + *

    + *
  • The alphanumeric characters "{@code a}" through + * "{@code z}", "{@code A}" through + * "{@code Z}" and "{@code 0}" + * through "{@code 9}" remain the same. + *
  • The special characters "{@code .}", + * "{@code -}", "{@code *}", and + * "{@code _}" remain the same. + *
  • The plus sign "{@code +}" is converted into a + * space character "   " . + *
  • A sequence of the form "{@code %xy}" will be + * treated as representing a byte where xy is the two-digit + * hexadecimal representation of the 8 bits. Then, all substrings + * that contain one or more of these byte sequences consecutively + * will be replaced by the character(s) whose encoding would result + * in those consecutive bytes. + * The encoding scheme used to decode these characters may be specified, + * or if unspecified, the default encoding of the platform will be used. + *
+ *

+ * There are two possible ways in which this decoder could deal with + * illegal strings. It could either leave illegal characters alone or + * it could throw an {@link java.lang.IllegalArgumentException}. + * Which approach the decoder takes is left to the + * implementation. + * + * @author Mark Chamness + * @author Michael McCloskey + * @since 1.2 + */ + +public class URLDecoder { + + // The platform default encoding + static String dfltEncName = URLEncoder.dfltEncName; + + /** + * Decodes a {@code x-www-form-urlencoded} string. + * The platform's default encoding is used to determine what characters + * are represented by any consecutive sequences of the form + * "{@code %xy}". + * @param s the {@code String} to decode + * @deprecated The resulting string may vary depending on the platform's + * default encoding. Instead, use the decode(String,String) method + * to specify the encoding. + * @return the newly decoded {@code String} + */ + @Deprecated + public static String decode(String s) { + + String str = null; + + try { + str = decode(s, dfltEncName); + } catch (UnsupportedEncodingException e) { + // The system should always have the platform default + } + + return str; + } + + /** + * Decodes a {@code application/x-www-form-urlencoded} string using a specific + * encoding scheme. + * The supplied encoding is used to determine + * what characters are represented by any consecutive sequences of the + * form "{@code %xy}". + *

+ * Note: The + * World Wide Web Consortium Recommendation states that + * UTF-8 should be used. Not doing so may introduce + * incompatibilities. + * + * @param s the {@code String} to decode + * @param enc The name of a supported + * character + * encoding. + * @return the newly decoded {@code String} + * @exception UnsupportedEncodingException + * If character encoding needs to be consulted, but + * named character encoding is not supported + * @see URLEncoder#encode(java.lang.String, java.lang.String) + * @since 1.4 + */ + public static String decode(String s, String enc) + throws UnsupportedEncodingException{ + + boolean needToChange = false; + int numChars = s.length(); + StringBuffer sb = new StringBuffer(numChars > 500 ? numChars / 2 : numChars); + int i = 0; + + if (enc.length() == 0) { + throw new UnsupportedEncodingException ("URLDecoder: empty string enc parameter"); + } + + char c; + byte[] bytes = null; + while (i < numChars) { + c = s.charAt(i); + switch (c) { + case '+': + sb.append(' '); + i++; + needToChange = true; + break; + case '%': + /* + * Starting with this instance of %, process all + * consecutive substrings of the form %xy. Each + * substring %xy will yield a byte. Convert all + * consecutive bytes obtained this way to whatever + * character(s) they represent in the provided + * encoding. + */ + + try { + + // (numChars-i)/3 is an upper bound for the number + // of remaining bytes + if (bytes == null) + bytes = new byte[(numChars-i)/3]; + int pos = 0; + + while ( ((i+2) < numChars) && + (c=='%')) { + int v = Integer.parseInt(s.substring(i+1,i+3),16); + if (v < 0) + throw new IllegalArgumentException("URLDecoder: Illegal hex characters in escape (%) pattern - negative value"); + bytes[pos++] = (byte) v; + i+= 3; + if (i < numChars) + c = s.charAt(i); + } + + // A trailing, incomplete byte encoding such as + // "%x" will cause an exception to be thrown + + if ((i < numChars) && (c=='%')) + throw new IllegalArgumentException( + "URLDecoder: Incomplete trailing escape (%) pattern"); + + sb.append(new String(bytes, 0, pos, enc)); + } catch (NumberFormatException e) { + throw new IllegalArgumentException( + "URLDecoder: Illegal hex characters in escape (%) pattern - " + + e.getMessage()); + } + needToChange = true; + break; + default: + sb.append(c); + i++; + break; + } + } + + return (needToChange? sb.toString() : s); + } +}