From 59cfa41c9f49751e418601735e3c9171c7b4fd5f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 1 Apr 2019 09:24:21 +0100 Subject: [PATCH 1/3] Add CProverString.format function This directly translates to a builtin function of CBMC string solver. --- src/main/java/org/cprover/CProverString.java | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/main/java/org/cprover/CProverString.java b/src/main/java/org/cprover/CProverString.java index 344459c..f26624b 100644 --- a/src/main/java/org/cprover/CProverString.java +++ b/src/main/java/org/cprover/CProverString.java @@ -410,4 +410,17 @@ public static String ofCharArray(char value[], int offset, int count) { } return builder.toString(); } + + /** + * Format a string according to the given {@param formatString}. + * Unlike the JDK version, all arguments are given by strings, there is + * a fixed number of them and they should not be null. + * This fixed number corresponds to the constant {@code MAX_FORMAT_ARGS} defined in + * {@code java_string_library_preprocess.h} from JBMC. + */ + public static String format( + String formatString, String arg0, String arg1, String arg2, String arg3, + String arg4, String arg5, String arg6, String arg7, String arg8, String arg9) { + return CProver.nondetWithoutNullForNotModelled(); + } } From 43928500c46fa261f42ea7b9af283c4199e4ca0f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 1 Apr 2019 09:25:06 +0100 Subject: [PATCH 2/3] Add a model of String.format This uses CProverString.format which is builtin in the string solver. --- src/main/java/java/lang/String.java | 67 ++++++++++++++++++++++++++--- 1 file changed, 62 insertions(+), 5 deletions(-) diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java index c9d2bcd..6351a50 100644 --- a/src/main/java/java/lang/String.java +++ b/src/main/java/java/lang/String.java @@ -3884,6 +3884,50 @@ public char[] toCharArray() { return result; } + /** + * Helper function for the {@code format} function. + * Serialize potential String.format argument to a String. + * The returned String is never null. + */ + static String cproverFormatArgument(Object obj) { + if (obj == null) { + return "null"; + } + if (obj instanceof String) { + return (String) obj; + } + + // All primitive types are cast to a long + long longValue = 0; + if (obj instanceof Integer) { + longValue = (Integer) obj; + } else if (obj instanceof Long) { + longValue = (Long) obj; + } else if (obj instanceof Float) { + longValue = (long) ((Float) obj).doubleValue(); + } else if (obj instanceof Double) { + longValue = (long) ((Double) obj).doubleValue(); + } else if (obj instanceof Character) { + char charValue = (Character) obj; + longValue = (long) charValue; + } else if (obj instanceof Byte) { + byte byteValue = ((Byte) obj); + longValue = (long) byteValue; + } else if (obj instanceof Boolean) { + longValue = ((Boolean) obj) ? 1 : 0; + } else { + return CProver.nondetWithoutNull(""); + } + + // The long value is encoded using a string of 4 characters + StringBuilder builder = new StringBuilder(); + builder.append((char) (longValue >> 48 & 0xFFFF)); + builder.append((char) (longValue >> 32 & 0xFFFF)); + builder.append((char) (longValue >> 16 & 0xFFFF)); + builder.append((char) (longValue & 0xFFFF)); + return builder.toString(); + } + /** * Returns a formatted string using the specified format string and * arguments. @@ -3946,9 +3990,23 @@ public char[] toCharArray() { * @diffblue.untested */ public static String format(String format, Object... args) { - // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC - return CProver.nondetWithoutNullForNotModelled(); // return new Formatter().format(format, args).toString(); + // DIFFBLUE MODEL LIBRARY + if (args.length > 10) { + return CProver.nondetWithoutNull(""); + } + String arg0 = args.length > 0 ? cproverFormatArgument(args[0]) : ""; + String arg1 = args.length > 1 ? cproverFormatArgument(args[1]) : ""; + String arg2 = args.length > 2 ? cproverFormatArgument(args[2]) : ""; + String arg3 = args.length > 3 ? cproverFormatArgument(args[3]) : ""; + String arg4 = args.length > 4 ? cproverFormatArgument(args[4]) : ""; + String arg5 = args.length > 5 ? cproverFormatArgument(args[5]) : ""; + String arg6 = args.length > 6 ? cproverFormatArgument(args[6]) : ""; + String arg7 = args.length > 7 ? cproverFormatArgument(args[7]) : ""; + String arg8 = args.length > 8 ? cproverFormatArgument(args[8]) : ""; + String arg9 = args.length > 9 ? cproverFormatArgument(args[9]) : ""; + return CProverString.format(format, arg0, arg1, arg2, arg3, arg4, arg5, + arg6, arg7, arg8, arg9); } /** @@ -3988,12 +4046,11 @@ public static String format(String format, Object... args) { * @see java.util.Formatter * @since 1.5 * - * @diffblue.noSupport + * @diffblue.limitedSupport The locale argument is ignored */ public static String format(Locale l, String format, Object... args) { // return new Formatter(l).format(format, args).toString(); - CProver.notModelled(); - return CProver.nondetWithoutNullForNotModelled(); + return format(format, args); } /** From 077484fa992576df7d99d9f44ff90609ff10a3ac Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 2 Apr 2019 14:55:02 +0100 Subject: [PATCH 3/3] Document limitation of String.format The null case is a bit special. --- src/main/java/java/lang/String.java | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java index 6351a50..e16dd1d 100644 --- a/src/main/java/java/lang/String.java +++ b/src/main/java/java/lang/String.java @@ -3986,6 +3986,11 @@ static String cproverFormatArgument(Object obj) { *
  • * having 5 arguments or more makes the solver slow *
    • + *
  • + * the string "null" is interpreted the same way {@code null} would be by + * the JDK String.format function, which is correct for the %s format + * specifier but not %b for instance. + *
    • * * @diffblue.untested */ @@ -4046,7 +4051,8 @@ public static String format(String format, Object... args) { * @see java.util.Formatter * @since 1.5 * - * @diffblue.limitedSupport The locale argument is ignored + * @diffblue.limitedSupport The locale argument is ignored and it has the + * same limitations as {@link #format(String, Object...)}. */ public static String format(Locale l, String format, Object... args) { // return new Formatter(l).format(format, args).toString();