Conversion functions from primitive types to strings #5048

danpoe · 2019-08-22T15:14:07Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/s My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

In the initialization of the conversion table, CProverString operations are grouped together for better readability.

romainbrenguier · 2019-08-22T15:35:48Z

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -1548,6 +1548,21 @@ void java_string_library_preprocesst::initialize_conversion_table()
  cprover_equivalent_to_java_string_returning_function
    ["java::org.cprover.CProverString.substring:(Ljava/Lang/"
     "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
+  cprover_equivalent_to_java_string_returning_function
+    ["java::org.cprover.CProverString.toString:(Z)Ljava/lang/String;"] =
+      ID_cprover_string_of_bool_func;


⛏️ actually this could be implemented directly as a model, there is not complicated logic involved, so I don't know if this is needed 🍭

Yes, I think in that case we can remove both ID_cprover_string_of_bool_func as well as CProverString.toString(char) and use b ? "true" : "false" directly.

romainbrenguier · 2019-08-22T15:36:03Z

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

+      ID_cprover_string_of_bool_func;
+  cprover_equivalent_to_java_string_returning_function
+    ["java::org.cprover.CProverString.toString:(C)Ljava/lang/String;"] =
+      ID_cprover_string_of_char_func;


We could use

char arr[] = {c}; return new String(arr);

which calls ofCharArray() which creates a StringBuilder and uses append() to insert the char and then returns StringBuilder.toString(). Any idea if this might have performance implications?

romainbrenguier · 2019-08-22T15:36:50Z

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

+      ID_cprover_string_of_long_func;
+  cprover_equivalent_to_java_string_returning_function
+    ["java::org.cprover.CProverString.toString:(F)Ljava/lang/String;"] =
+      ID_cprover_string_of_float_func;


why is there no string_of_double entry?

Double to string is handled by a model via CProverString.toString(CProver.doubleToFloat(d)) as double to string conversion is not implemented AFAIK.

romainbrenguier · 2019-08-22T15:38:26Z

jbmc/regression/jbmc-strings/CProverStringToString/Main.java

+    /*case 5:
+      c = Character.MAX_VALUE;
+      r = "\uFFFF";
+      break;*/


why is this commented out? ☕

This case does not work. I have to investigate why.

romainbrenguier · 2019-08-22T15:39:41Z

jbmc/regression/jbmc-strings/CProverStringToString/Main.java

+    case 8:
+      f = Float.NaN;
+      r = "NaN";
+      break;*/


Does not work yet.

martin-cs

A passing thought

martin-cs · 2019-08-23T09:00:58Z

jbmc/regression/jbmc-strings/CProverStringToString/Main.java

+      break;
+    case 5:
+      f = Float.MIN_VALUE;
+      r = "1.4E-45";


Where did this number come from?

That's the result of String.valueOf(f) (same as Float.toString(f)) 🍞

martin-cs · 2019-08-23T09:01:33Z

jbmc/regression/jbmc-strings/CProverStringToString/Main.java

+      break;
+    /*case 4:
+      f = Float.MAX_VALUE;
+      r = "3.4028235E38";


This is kind of a weird way of formatting this.

smowton

No further comments except what @romainbrenguier already raised

…able New CProverString.toString() operations are added which are now handled internally by cbmc. These operations can be used to model other Java methods such as Integer.toString().

These models can be compiled and run and have the same semantics as implemented by the string solver. They can thus be used to check that the string solver gives the correct result by comparing the result of a concrete run with the result obtained by cbmc.

After converting '\uFFFF' to string the result differs from "\uFFFF" for a check with `equals()`.

danpoe · 2019-08-23T17:53:11Z

Ok, I'll merge this once CI passes. The behavior of the string operations does not change, but a new test has revealed some issues in the float to string conversion. I've marked the test as KNOWNBUG for now.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: ba12215).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/124413147

Group CProverString operations in initialize_conversion_table()

c1894ab

In the initialization of the conversion table, CProverString operations are grouped together for better readability.

danpoe requested review from cesaro, cristina-david, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners August 22, 2019 15:14

danpoe added the do not merge label Aug 22, 2019

danpoe requested a review from romainbrenguier August 22, 2019 15:25

romainbrenguier approved these changes Aug 22, 2019

View reviewed changes

martin-cs reviewed Aug 23, 2019

View reviewed changes

smowton approved these changes Aug 23, 2019

View reviewed changes

danpoe force-pushed the refactor/primitive-types-to-string branch 3 times, most recently from 874f2ff to 3cf74b0 Compare August 23, 2019 16:42

danpoe added 2 commits August 23, 2019 17:42

Add CProver.toString() functions to string preprocessing conversion t…

1a9435a

…able New CProverString.toString() operations are added which are now handled internally by cbmc. These operations can be used to model other Java methods such as Integer.toString().

danpoe force-pushed the refactor/primitive-types-to-string branch from 3cf74b0 to ba12215 Compare August 23, 2019 16:57

danpoe added 2 commits August 23, 2019 17:57

Add regression tests for CProverString.toString() operations

754ebdb

Add regression test for bug of char to string conversion

ba12215

After converting '\uFFFF' to string the result differs from "\uFFFF" for a check with `equals()`.

danpoe removed the do not merge label Aug 23, 2019

danpoe merged commit cbec723 into diffblue:develop Aug 23, 2019

allredj reviewed Aug 23, 2019

View reviewed changes

danpoe deleted the refactor/primitive-types-to-string branch June 2, 2020 17:17

Conversion functions from primitive types to strings #5048

Conversion functions from primitive types to strings #5048

Uh oh!

Conversation

danpoe commented Aug 22, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

danpoe commented Aug 23, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

danpoe commented Aug 22, 2019 •

edited

Loading