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

romainbrenguier · 2019-04-01T10:39:22Z

The way String.format is implemented in the string preprocessing is hacky and buggy.
By adding a CProverString.format function as interface, the preprocessing becomes very simple, the complexity is then transfered to the java models, for which it is much easier to write clean code (than goto-program for java).
This should go together with an update of the models: diffblue/java-models-library#20

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.
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).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

smowton

Seems sensible

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: e74d753).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106699730
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 660b193).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106716601
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

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

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 06e7e9f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106916333
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 7a920a1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106919141
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

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

peterschrammel · 2019-04-03T15:54:43Z

src/solvers/strings/string_constraint_generator_format.cpp

+    const exprt as_int = format_arg_from_string(string, ID_int);
+    return typecast_exprt{as_int, floatbv_typet{}};
+  }
+  UNHANDLED_CASE;


byte, short, double and long are not handled yet?

They are all handled by being cast to a long within the model. So ID_int does not need to make a distinction between byte, short, int and long.

Drive-by comment: so what about double?

It's also cast to a long. ID_float handles both the cases where the formatting string except a float and a double (this was the same before my PR).

diffblue/java-models-library#20

This makes the link between the CProverString.format signature from java and the ID_cprover_string_format_func from the solver.

This makes it accept a function as argument, which gives for possible types the corresponding value of the argument. This will allow us to adapt more easily to a change in the way the arguments of format are given: they are now given as a struct but we want to have the possibility to give them as a string.

Add the possibility to pass argument to the builtin format function as strings instead of structs with fields.

add_axioms_from_int_hex is deprecated, we use add_axioms_for_string_of_int_with_radix instead.

This should now be in the model, and the implementation of models can use CProverString.format.

This tests the new implementation of String.format using the java models.

To use the builtin format function, the java entry point is now CProverString.format, so we can remove the legacy code which was handling String.format directly.

Reflects the new way the argument are passed to the format builtin function.

romainbrenguier · 2019-04-03T16:05:08Z

The java-models-library update is now pointing to master

allredj

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

romainbrenguier added do not merge In progress do not review labels Apr 1, 2019

romainbrenguier requested review from cesaro, chrisr-diffblue, cristina-david, kroening, martin-cs, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners April 1, 2019 10:39

smowton approved these changes Apr 1, 2019

View reviewed changes

romainbrenguier force-pushed the feature/cprover-string-format branch 3 times, most recently from fad62ee to e74d753 Compare April 2, 2019 07:49

romainbrenguier added do not merge and removed do not merge In progress do not review labels Apr 2, 2019

romainbrenguier force-pushed the feature/cprover-string-format branch 2 times, most recently from 801c355 to 147a223 Compare April 2, 2019 09:29

allredj reviewed Apr 2, 2019

View reviewed changes

romainbrenguier force-pushed the feature/cprover-string-format branch 2 times, most recently from 660b193 to 1acddc7 Compare April 2, 2019 11:19

allredj reviewed Apr 2, 2019

View reviewed changes

romainbrenguier force-pushed the feature/cprover-string-format branch 2 times, most recently from 06785cc to fe27d99 Compare April 2, 2019 12:51

allredj approved these changes Apr 3, 2019

View reviewed changes

allredj reviewed Apr 3, 2019

View reviewed changes

tautschnig assigned peterschrammel and martin-cs and unassigned allredj Apr 3, 2019

romainbrenguier force-pushed the feature/cprover-string-format branch 3 times, most recently from 7a920a1 to e45a2d0 Compare April 3, 2019 12:40

allredj reviewed Apr 3, 2019

View reviewed changes

peterschrammel approved these changes Apr 3, 2019

View reviewed changes

peterschrammel removed their assignment Apr 3, 2019

romainbrenguier added 10 commits April 3, 2019 17:00

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

69528ad

diffblue/java-models-library#20

Add preprocessing for CProverString.format

9899d25

This makes the link between the CProverString.format signature from java and the ID_cprover_string_format_func from the solver.

Make add_axioms_for_format accept string arguments

8cd312c

Add the possibility to pass argument to the builtin format function as strings instead of structs with fields.

Use non-deprecated function for hex printing

526746d

add_axioms_from_int_hex is deprecated, we use add_axioms_for_string_of_int_with_radix instead.

Remove preprocessing for String.format

5a3772b

This should now be in the model, and the implementation of models can use CProverString.format.

Add tests for String.format

10924e1

This tests the new implementation of String.format using the java models.

Remove code that is now unreachable

c24de41

To use the builtin format function, the java entry point is now CProverString.format, so we can remove the legacy code which was handling String.format directly.

Update add_axioms_for_format_specifier documentation

8fc7988

Reflects the new way the argument are passed to the format builtin function.

Handle the case of null arguments for format

7c34ea4

romainbrenguier force-pushed the feature/cprover-string-format branch from e45a2d0 to 7c34ea4 Compare April 3, 2019 16:00

romainbrenguier removed the do not merge label Apr 3, 2019

tautschnig unassigned martin-cs Apr 3, 2019

allredj reviewed Apr 3, 2019

View reviewed changes

romainbrenguier merged commit b2d0d2c into diffblue:develop Apr 4, 2019

romainbrenguier deleted the feature/cprover-string-format branch April 4, 2019 09:08

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

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

Uh oh!

romainbrenguier commented Apr 1, 2019

Uh oh!

smowton left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

peterschrammel Apr 3, 2019

Uh oh!

romainbrenguier Apr 3, 2019

Uh oh!

tautschnig Apr 3, 2019

Uh oh!

romainbrenguier Apr 3, 2019

Uh oh!

romainbrenguier commented Apr 3, 2019

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

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

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

Uh oh!

Conversation

romainbrenguier commented Apr 1, 2019

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

peterschrammel Apr 3, 2019

Choose a reason for hiding this comment

Uh oh!

romainbrenguier Apr 3, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Apr 3, 2019

Choose a reason for hiding this comment

Uh oh!

romainbrenguier Apr 3, 2019

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Apr 3, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!