Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Apr 3, 2019

Conversation

romainbrenguier
Copy link
Contributor

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.


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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

JDK version ? It's still Java.

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

formatString is arg0

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

formatString is arg0

@@ -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
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What about when the input is nondet?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

@antlechner antlechner left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link

@antlechner antlechner left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

❓ 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?

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

@romainbrenguier romainbrenguier Apr 2, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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").

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.
@romainbrenguier romainbrenguier force-pushed the feature/string-format branch 2 times, most recently from 7d23b60 to 9f561d9 Compare April 2, 2019 12:31
@romainbrenguier romainbrenguier force-pushed the feature/string-format branch from 9f561d9 to d23a1dd Compare April 2, 2019 12:52
*/
static String cproverFormatArgument(Object obj) {
if (obj == null) return "null";
if (obj instanceof String) return (String) obj;
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ 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.

* <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.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@@ -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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 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.

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.
@romainbrenguier romainbrenguier force-pushed the feature/string-format branch from d88266e to 4940fbd Compare April 3, 2019 05:51
The null case is a bit special.
@romainbrenguier romainbrenguier force-pushed the feature/string-format branch from 4940fbd to 077484f Compare April 3, 2019 06:02
@romainbrenguier romainbrenguier merged commit 287f0b7 into master Apr 3, 2019
@romainbrenguier romainbrenguier deleted the feature/string-format branch April 3, 2019 15:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants