CProverString.format definition and String.format model using it #20

romainbrenguier · 2019-04-01T10:33:25Z

This is a proposal for a CProverString.format which will act as an interface to the a builtin function of Jbmc.
String.format is an example of how it can be used in the models.
The way we deserialize the arguments in the solver will have to be synchronized with how we serialize them in `formatArgument.

peterschrammel · 2019-04-01T10:44:44Z

src/main/java/org/cprover/CProverString.java

+
+    /**
+     * Format a string according to the given {@code format}.
+     * Unlike the java version, all arguments are given by strings, there is


JDK version ? It's still Java.

allredj · 2019-04-01T14:13:26Z

src/main/java/org/cprover/CProverString.java

+     * a fixed number of them and they should not be null.
+     */
+    public static String format(
+            String formatString, String arg1, String arg2, String arg3,


formatString is arg0

allredj · 2019-04-01T14:13:26Z

src/main/java/org/cprover/CProverString.java

+     * a fixed number of them and they should not be null.
+     */
+    public static String format(
+            String formatString, String arg1, String arg2, String arg3,


formatString is arg0

allredj · 2019-04-01T14:17:34Z

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

@@ -3812,9 +3840,20 @@ public String toString() {
     * @diffblue.untested
     */
    public static String format(String format, Object... args) {
-        // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC
-        return CProver.nondetWithoutNullForNotModelled();
+        // DIFFBLUE MODEL LIBRARY


I suppose we need to constrain the size of args to be <= 10, otherwise we might generated incorrect tests using arguments that are ignored in cbmc, but not by the JVM.

I made format return a nondet value in the case of more than 10 arguments, which is correct for the point of view of verification. I think it will be very rare to get a list of non-deterministic size here as arguments are normally passed explicitly and not through a list.

What about when the input is nondet?

OK, I now understand your comment about verification (although you allow false positives). I'll transfer my complaint to the "other" models-library :-).

diffblue/java-models-library#20

antlechner

I haven't looked at the cbmc implementation of String.format yet so I can't comment on the details of the serialisation of Object arguments.

src/main/java/org/cprover/CProverString.java

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

antlechner

Found something that I think should be documented or fixed before this can be merged.

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

antlechner · 2019-04-02T12:21:14Z

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

+    static String cproverFormatArgument(Object obj)
+    {
+        if(obj == null)
+            return "";


❓ In the JDK implementation of String.format, null is not generally formatted as an empty string. For example,

String f = String.format("%s %s", null, "hello"); System.out.println(f);

prints null hello. Why does this method return an empty string in this case?

https://docs.oracle.com/javase/7/docs/api/java/util/Formatter.html has a "Conversions" section that explains some of the null cases. For %s and %h, null is formatted as null, but for %b, it is formatted as false. It looks like for the character and number cases, null is not an expected input, but with %c and null I also got it to print null.

@antlechner Fixed that to give "null" for null objects

I think the special cases will have to be handled in the solver because at this point we don't know which format specifier is used for the corresponding argument. And for %b %c we will be able to distinguish "null" from valid inputs (which will begin with "000").

That makes sense. But I think there is still a problem because sometimes null and "null" can give different results. For example,

String.format("%b", null);

is false but

String.format("%b", "null");

is true. Is there an easy way to fix this? If not then the limitation should be documented.

This could be fixed but I'm afraid the solution I have in mind would make handling the string case a bit more complicated, so the whole would be slower, so I prefer to document the limitation (and I hope giving a String to match a "%b" is rare).

@antlechner done

I agree it's better for now to document the limitation of an edge case than to slow down the general case.

This directly translates to a builtin function of CBMC string solver.

diffblue/java-models-library#20

allredj · 2019-04-02T14:45:56Z

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

+     */
+    static String cproverFormatArgument(Object obj) {
+        if (obj == null) return "null";
+        if (obj instanceof String) return (String) obj;


⛏️ I realise I didn't review this PR properly. Why do you use that one line notation here? Does it come from OpenJDK? We usually use braces for conditionals.

allredj · 2019-04-02T14:51:18Z

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

+     * <li>
+     *   the string "null" is interpreted the same way {@code null} would be by
+     *   the JDK format, which is correct for the %s format specifier but not
+     *   %b for instance.


I don't understand this comment. What is the the JDK format?

antlechner · 2019-04-02T16:31:23Z

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

@@ -3988,12 +4042,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


💡 It's worth documenting that date/time related format specifiers are not supported. The example from the Javadoc of Formatter.java, String.format("Duke's Birthday: %1$tm %1$te,%1$tY", c);, gives an invariant violation.

antlechner · 2019-04-02T16:33:42Z

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

+    static String cproverFormatArgument(Object obj)
+    {
+        if(obj == null)
+            return "";


I agree it's better for now to document the limitation of an edge case than to slow down the general case.

This uses CProverString.format which is builtin in the string solver.

The null case is a bit special.

diffblue/java-models-library#20

romainbrenguier force-pushed the feature/string-format branch from e773eff to fcb68b9 Compare April 1, 2019 10:34

romainbrenguier mentioned this pull request Apr 1, 2019

Use CProverString.format as interface to the solver builtin function diffblue/cbmc#4477

Merged

7 tasks

peterschrammel approved these changes Apr 1, 2019

View reviewed changes

peterschrammel assigned romainbrenguier Apr 1, 2019

diffblue deleted a comment from peterschrammel Apr 1, 2019

allredj reviewed Apr 1, 2019

View reviewed changes

romainbrenguier force-pushed the feature/string-format branch 2 times, most recently from e2cd3ed to cda1e9c Compare April 1, 2019 15:47

romainbrenguier added a commit to romainbrenguier/cbmc that referenced this pull request Apr 1, 2019

Update java-models-library for diffblue/java-models-library#20

e07634f

diffblue/java-models-library#20

romainbrenguier added a commit to romainbrenguier/cbmc that referenced this pull request Apr 1, 2019

Update java-models-library for diffblue/java-models-library#20

96bf88d

diffblue/java-models-library#20

romainbrenguier force-pushed the feature/string-format branch from cda1e9c to 4f94868 Compare April 2, 2019 07:44

romainbrenguier added a commit to romainbrenguier/cbmc that referenced this pull request Apr 2, 2019

Update java-models-library for diffblue/java-models-library#20

d8e80b5

diffblue/java-models-library#20

romainbrenguier force-pushed the feature/string-format branch from 4f94868 to 8e1a387 Compare April 2, 2019 08:51

romainbrenguier added a commit to romainbrenguier/cbmc that referenced this pull request Apr 2, 2019

Update java-models-library for diffblue/java-models-library#20

b57022c

diffblue/java-models-library#20

allredj approved these changes Apr 2, 2019

View reviewed changes

antlechner approved these changes Apr 2, 2019

View reviewed changes

antlechner suggested changes Apr 2, 2019

View reviewed changes

Add CProverString.format function

59cfa41

This directly translates to a builtin function of CBMC string solver.

romainbrenguier force-pushed the feature/string-format branch 2 times, most recently from 7d23b60 to 9f561d9 Compare April 2, 2019 12:31

romainbrenguier added a commit to romainbrenguier/cbmc that referenced this pull request Apr 2, 2019

Update java-models-library for diffblue/java-models-library#20

e7461a2

diffblue/java-models-library#20

romainbrenguier force-pushed the feature/string-format branch from 9f561d9 to d23a1dd Compare April 2, 2019 12:52

romainbrenguier added a commit to romainbrenguier/cbmc that referenced this pull request Apr 2, 2019

Update java-models-library for diffblue/java-models-library#20

e79d49d

diffblue/java-models-library#20

romainbrenguier added a commit to romainbrenguier/cbmc that referenced this pull request Apr 2, 2019

Update java-models-library for diffblue/java-models-library#20

5863373

diffblue/java-models-library#20

allredj reviewed Apr 2, 2019

View reviewed changes

antlechner reviewed Apr 2, 2019

View reviewed changes

antlechner approved these changes Apr 2, 2019

View reviewed changes

Add a model of String.format

4392850

This uses CProverString.format which is builtin in the string solver.

romainbrenguier force-pushed the feature/string-format branch from d88266e to 4940fbd Compare April 3, 2019 05:51

Document limitation of String.format

077484f

The null case is a bit special.

romainbrenguier force-pushed the feature/string-format branch from 4940fbd to 077484f Compare April 3, 2019 06:02

romainbrenguier added a commit to romainbrenguier/cbmc that referenced this pull request Apr 3, 2019

Update java-models-library for diffblue/java-models-library#20

c19cca9

diffblue/java-models-library#20

romainbrenguier added a commit to romainbrenguier/cbmc that referenced this pull request Apr 3, 2019

Update java-models-library for diffblue/java-models-library#20

9329020

diffblue/java-models-library#20

romainbrenguier merged commit 287f0b7 into master Apr 3, 2019

romainbrenguier deleted the feature/string-format branch April 3, 2019 15:57

romainbrenguier added a commit to romainbrenguier/cbmc that referenced this pull request Apr 3, 2019

Update java-models-library for diffblue/java-models-library#20

69528ad

diffblue/java-models-library#20

CProverString.format definition and String.format model using it #20

CProverString.format definition and String.format model using it #20

Conversation

romainbrenguier commented Apr 1, 2019

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!

antlechner left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

antlechner left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

romainbrenguier Apr 2, 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!

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!

Uh oh!

romainbrenguier Apr 2, 2019 •

edited

Loading