Handle common floats to string operations in the model and not in the string solver

Author: Vojtech Forejt

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);
     }
 

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));
     }
 
     /**

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;
+  }
 }