-
Notifications
You must be signed in to change notification settings - Fork 4
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
Conversation
e773eff
to
fcb68b9
Compare
|
||
/** | ||
* Format a string according to the given {@code format}. | ||
* Unlike the java version, all arguments are given by strings, there is |
There was a problem hiding this comment.
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, |
There was a problem hiding this comment.
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, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
formatString
is arg0
src/main/java/java/lang/String.java
Outdated
@@ -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 |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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 :-).
e2cd3ed
to
cda1e9c
Compare
cda1e9c
to
4f94868
Compare
4f94868
to
8e1a387
Compare
There was a problem hiding this 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.
There was a problem hiding this 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.
src/main/java/java/lang/String.java
Outdated
static String cproverFormatArgument(Object obj) | ||
{ | ||
if(obj == null) | ||
return ""; |
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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
.
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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").
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@antlechner done
There was a problem hiding this comment.
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.
7d23b60
to
9f561d9
Compare
9f561d9
to
d23a1dd
Compare
src/main/java/java/lang/String.java
Outdated
*/ | ||
static String cproverFormatArgument(Object obj) { | ||
if (obj == null) return "null"; | ||
if (obj instanceof String) return (String) obj; |
There was a problem hiding this comment.
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.
src/main/java/java/lang/String.java
Outdated
* <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. |
There was a problem hiding this comment.
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
?
src/main/java/java/lang/String.java
Outdated
@@ -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 |
There was a problem hiding this comment.
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.
src/main/java/java/lang/String.java
Outdated
static String cproverFormatArgument(Object obj) | ||
{ | ||
if(obj == null) | ||
return ""; |
There was a problem hiding this comment.
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.
d88266e
to
4940fbd
Compare
The null case is a bit special.
4940fbd
to
077484f
Compare
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.