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

forejtv · 2019-05-10T14:56:06Z

No description provided.

romainbrenguier · 2019-05-13T08:36:07Z

src/main/java/org/cprover/CProver.java

+  public static float doubleToFloat(double d)
+  {
+    float converted = nondetFloat();
+    CProver.assume(d < Float.MAX_VALUE && d > -Float.MAX_VALUE && d == (double) converted);


This makes sense for test generation but not really for verification. Could we change this assume for an assert?

Hmmm. I am not sure what if you suggest is better than the current approach, but I see where you're coming from, at least the user will explicitly see the violated assertion in the output. I've changed this.

romainbrenguier · 2019-05-13T08:36:56Z

src/main/java/org/cprover/CProver.java

+  public static float doubleToFloat(double d)
+  {
+    float converted = nondetFloat();
+    CProver.assume(d < Float.MAX_VALUE && d > -Float.MAX_VALUE && d == (double) converted);


Isn't the last condition enough to ensure the two first ones?

forejtv · 2019-05-13T08:47:37Z

Thanks @romainbrenguier for your comments, this is now ready for re-reviews.

antlechner

Could you explain why you're making these changes? Do they improve performance, or was something changed in the string solver that requires this?

antlechner · 2019-05-13T10:54:20Z

src/main/java/java/lang/String.java

-        // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC
-        return CProver.nondetWithoutNullForNotModelled();
+        // DIFFBLUE MODEL LIBRARY we cast the number down to float because string solver only knows how to convert floats to string
+        return valueOf(CProver.doubleToFloat(d));


❓ How is the result of this method call different from just casting d to type float?

In doubleToFloat we're ensuring that there's no loss of precision in the conversion, so that we convert the correct number to string. Say we had double x, then converted it to double y, and then we converted that to String z. z is a string representation of y, but not necessarily of x. After a discussion with @romainbrenguier I went for the doubleToFloat implementation in order to make it more likely that the string representation of x equals the string representation of y.

I understand the precision problem but I don't understand how doubleToFloat avoids this problem. As float has fewer bits than double, wouldn't there always be a loss of precision? And can we be sure that for every double d, there is actually a float f such that d == (double) f;? Since there are strictly fewer floats than doubles this doesn't look right... and would mean that we sometimes can't get past the assume in doubleToFloat.
Maybe we could briefly discuss this in person? It's possible that I'm just missing something.
In any case, some tests in another repository would be great to see what this actually does/fixes.

antlechner · 2019-05-13T10:55:03Z

src/main/java/java/lang/String.java

    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 string solver only knows how to convert floats to string


⚒️ Could you wrap this line at 80 characters please?
❓ Also, is it a new thing that the string solver only converts floats and not doubles? If not, how did this work before?

It's not a new thing, before we'd either crash completely or not crash and then return a conversion which was likely to be incorrect.

antlechner · 2019-05-13T10:57:56Z

src/main/java/java/lang/StringBuffer.java

        // super.append(i);
        // return this;
-        return CProver.nondetWithoutNullForNotModelled();
+        return append(String.valueOf(i));


⛏️ This isn't related to floats so should probably be in a separate commit.
❔ Why is this done for int but not long, char etc.?

Good point. It's a follow-up from diffblue/cbmc#4633. I've split this into a separate commit.

Other types should be coming later too, but at the moment I concentrated on the bugs that I've seen in our benchmarks, and am handling them one by one.

forejtv · 2019-05-13T22:20:23Z

@antlechner The reason for the changes is that there are a lot of toString or similar methods in the string solver, and some of them are buggy. To make maintenance easier we decided to use models for most, and along the way fix some of the bug. This is the cbmc PR that removes the string solver hanglind of the methods: diffblue/cbmc#4648

antlechner

Thanks for explaining these changes in person, this makes a lot more sense now I know it's a workaround that will be improved in the future.
It would be great if you could add some documentation about this. Tests in at least one repository would be good too to check if this workaround works for most common values of double or if it's very easy to hit the limitations.

romainbrenguier

Can you squash the last commit into the relevant one? Otherwise looks good.

romainbrenguier · 2019-05-13T09:03:22Z

src/main/java/java/lang/String.java

    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 string solver only knows how to convert floats to string


⛏️ this line is long

romainbrenguier · 2019-05-14T08:15:03Z

src/main/java/org/cprover/CProver.java

+  public static float doubleToFloat(double d)
+  {
+    float converted = nondetFloat();
+    CProver.assume(d == (double) converted);


I would say this makes sense in the models-library but in the core models this assumption shouldn't be there because it constrain the behavior too much and for verification we always want an over-approximation of the behavior.

… string solver

Complements this PR on cbmc: diffblue/cbmc#4633

forejtv requested review from allredj and romainbrenguier May 10, 2019 14:56

forejtv mentioned this pull request May 10, 2019

Do not handle float and double to string operations in the string solver diffblue/cbmc#4648

Merged

7 tasks

forejtv requested a review from antlechner May 12, 2019 00:17

romainbrenguier reviewed May 13, 2019

View reviewed changes

antlechner reviewed May 13, 2019

View reviewed changes

forejtv force-pushed the forejtv/floats-to-string branch from 4ee1992 to c842964 Compare May 13, 2019 12:40

antlechner approved these changes May 14, 2019

View reviewed changes

romainbrenguier approved these changes May 14, 2019

View reviewed changes

Vojtech Forejt added 2 commits May 14, 2019 16:27

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

32d0f60

… string solver

Handle StringBuffer.append(int) in the model

24afc75

Complements this PR on cbmc: diffblue/cbmc#4633

forejtv force-pushed the forejtv/floats-to-string branch from aefa206 to 24afc75 Compare May 14, 2019 15:28

forejtv merged commit 79d3380 into master May 14, 2019

rjmunro deleted the forejtv/floats-to-string branch September 11, 2019 09:24

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

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

Uh oh!

Conversation

forejtv commented May 10, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

forejtv May 13, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

forejtv commented May 13, 2019

Uh oh!

antlechner 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!

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!

forejtv commented May 13, 2019

Uh oh!

antlechner left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier 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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

forejtv May 13, 2019 •

edited

Loading