From 32d0f608d8276d42d253aed687633f2ea46d0ca7 Mon Sep 17 00:00:00 2001 From: Vojtech Forejt Date: Fri, 10 May 2019 15:21:43 +0100 Subject: [PATCH 1/2] Handle common floats to string operations in the model and not in the string solver --- src/main/java/java/lang/String.java | 5 +++-- src/main/java/java/lang/StringBuffer.java | 4 ++-- src/main/java/org/cprover/CProver.java | 23 +++++++++++++++++++++++ 3 files changed, 28 insertions(+), 4 deletions(-) diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java index f38b3f8..2139ca1 100644 --- a/src/main/java/java/lang/String.java +++ b/src/main/java/java/lang/String.java @@ -4266,8 +4266,9 @@ public static String valueOf(float f) { * actual program. */ public static String valueOf(double d) { - // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC - return CProver.nondetWithoutNullForNotModelled(); + // DIFFBLUE MODEL LIBRARY we cast the number down to float because + // the string solver only knows how to convert floats to string + return valueOf(CProver.doubleToFloat(d)); // return Double.toString(d); } diff --git a/src/main/java/java/lang/StringBuffer.java b/src/main/java/java/lang/StringBuffer.java index b89d4e4..8ec1f82 100644 --- a/src/main/java/java/lang/StringBuffer.java +++ b/src/main/java/java/lang/StringBuffer.java @@ -576,7 +576,7 @@ public synchronized StringBuffer append(float f) { // toStringCache = null; // super.append(f); // return this; - return CProver.nondetWithoutNullForNotModelled(); + return append(String.valueOf(f)); } /** @@ -589,7 +589,7 @@ public synchronized StringBuffer append(double d) { // toStringCache = null; // super.append(d); // return this; - return CProver.nondetWithoutNullForNotModelled(); + return append(String.valueOf(d)); } /** diff --git a/src/main/java/org/cprover/CProver.java b/src/main/java/org/cprover/CProver.java index 1508f0f..619be30 100644 --- a/src/main/java/org/cprover/CProver.java +++ b/src/main/java/org/cprover/CProver.java @@ -322,4 +322,27 @@ public static String classIdentifier(Object object) { return object.getClass().getCanonicalName(); } + + /** + * This method converts a double to a float and adds assumes that the conversion + * did not result any loss of precision. Calling this method is useful when we + * need to call a certain complicated operation on double, but we only have it + * implemented for floats. + * + * The method is a workaround for the current limitations of the string solver, + * which is able to convert float to String but not double to String. Once this + * limitation goes away, the method and its usages can be removed. + * + * The method itself has limitations: + * * There are doubles that can't be converted to float and back without loss + * of precision, so the assertion will sometimes be violated + * * Even if the assertion is satisfied for numbers d and converted, these + * might not have the same String representation. + */ + public static float doubleToFloat(double d) + { + float converted = nondetFloat(); + assert(d == (double) converted); + return converted; + } } From 24afc75a73bde0225468f87d5a6f6a47d7fd4c6d Mon Sep 17 00:00:00 2001 From: Vojtech Forejt Date: Mon, 13 May 2019 13:38:37 +0100 Subject: [PATCH 2/2] Handle StringBuffer.append(int) in the model Complements this PR on cbmc: https://github.com/diffblue/cbmc/pull/4633 --- src/main/java/java/lang/StringBuffer.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/main/java/java/lang/StringBuffer.java b/src/main/java/java/lang/StringBuffer.java index 8ec1f82..35c56dd 100644 --- a/src/main/java/java/lang/StringBuffer.java +++ b/src/main/java/java/lang/StringBuffer.java @@ -531,11 +531,10 @@ public synchronized StringBuffer append(char c) { */ @Override public synchronized StringBuffer append(int i) { - // DIFFBLUE MODEL LIBRARY this is replaced internally // toStringCache = null; // super.append(i); // return this; - return CProver.nondetWithoutNullForNotModelled(); + return append(String.valueOf(i)); } /**