Simplify when combining string-refinement result constraints #4957

JohnDumbell · 2019-07-29T12:43:16Z

Due to the improvements in constant prop we increasingly have constraints that are trivially simplified, like:

if 5 >= 2 do x else y

Also because of the way these conditions are combined - the resulting merged if gets added to all subsequent conditions and values - we end up with expressions like this:

if 5 >= 2 then (if 5 >= 2 do x ... else y ...) else (if 5 >= 2 do x ... else y ...)

Where the size of the expression increases exponentially to the complexity of the original if statement even if the entire conditional is trivial to prove right/wrong. This could likely be worked out by the SAT solver happily enough but due to the size of the resulting expressions (I've seen ones 1.34 billion nodes deep) it never gets there within a reasonable time-frame.

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.

codecov-io · 2019-07-31T11:00:12Z

Codecov Report

Merging #4957 into develop will decrease coverage by 0.03%.
The diff coverage is 76.56%.

@@             Coverage Diff             @@
##           develop    #4957      +/-   ##
===========================================
- Coverage    69.47%   69.44%   -0.04%     
===========================================
  Files         1310     1310              
  Lines       108763   108747      -16     
===========================================
- Hits         75566    75520      -46     
- Misses       33197    33227      +30

Impacted Files	Coverage Δ
src/solvers/strings/string_builtin_function.h	`77.41% <ø> (ø)`	⬆️
src/solvers/strings/string_constraint_generator.h	`100% <ø> (ø)`	⬆️
...rs/strings/string_constraint_generator_testing.cpp	`100% <100%> (ø)`	⬆️
...ngs/string_constraint_generator_transformation.cpp	`95.03% <100%> (-0.77%)`	⬇️
...rs/strings/string_constraint_generator_indexof.cpp	`100% <100%> (ø)`	⬆️
...trings/string_constraint_generator_code_points.cpp	`100% <100%> (ø)`	⬆️
.../strings/string_concatenation_builtin_function.cpp	`83.9% <100%> (-0.19%)`	⬇️
src/solvers/strings/string_builtin_function.cpp	`66.66% <100%> (ø)`	⬆️
...ers/strings/string_constraint_generator_insert.cpp	`59.25% <36.84%> (+1.42%)`	⬆️
.../strings/string_constraint_generator_constants.cpp	`65.51% <62.5%> (+2.18%)`	⬆️
... and 16 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update bb6baff...8868378. Read the comment docs.

allredj

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

tautschnig · 2019-08-05T07:30:49Z

src/solvers/strings/string_constraint_generator_main.cpp

  merge(result2.second, std::move(result1.second));
+  simplify(return_code, ns);
+
  return {return_code, std::move(result2.second)};


May I suggest to use return {simplify_expr(return_code, ns), std::move(result2.second)}; at which point the return_code can be made const exprt.

romainbrenguier · 2019-08-05T09:03:11Z

src/solvers/strings/string_constraint_generator_main.cpp

  merge(result2.second, std::move(result1.second));
+  simplify(return_code, ns);


the change should be documented

Anywhere specific?

in the documentation of combine_results

src/solvers/strings/string_constraint_generator_constants.cpp

allredj

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

romainbrenguier · 2019-08-07T06:52:56Z

src/solvers/strings/string_constraint_generator_constants.cpp

@@ -78,6 +78,7 @@ add_axioms_for_empty_string(const function_application_exprt &f)
 /// \param arg: expression of type string typet
 /// \param guard: condition under which `res` should be equal to arg
 /// \param array_pool: pool of arrays representing strings
+/// \param ns: the namespace


💡 Maybe it will be good to say that this argument is so that we can simplify some expressions. We could pass a function simplify_expr as argument instead to make that obvious (just an idea)

Or maybe we could have a class and have some const members (such as a namespacet)? The architecture of the string solver code makes it really painful to add new capabilities.

We could basically use the string_constraint_generatort class for that (either pass it as an argument of the function or make the function a member), but we should clean-up the members of the class first: the string_constraintst field should just be an output of the methods and not a field and I think the messaget field does not belong there.

I don't know what exactly the right solution looks like, but I get the impression that making everything free functions has been taken a little too far here. It severely hampers maintainability. The PR we are looking at could have been a one-line change, but instead it's currently +87/-48. We need to make sure we find a good balance between perfectly clean code and maintainability.

Here is the clean-up I suggest #4995, you could then replace the fresh_symbol, array_pool, and ns arguments in these functions by just a string_constraint_generatort object and then further changes like this one could be small.

I'll happily do that. I was tempted to do it originally while doing this, but the changes were just under the acceptable threshold for me.

smowton · 2019-08-13T08:16:00Z

Is this good to go?

JohnDumbell · 2019-08-13T09:25:40Z

Not yet, I'll make the required changes now to help clean it up then should be good.

JohnDumbell · 2019-08-14T12:49:16Z

I've made the changes which results in the original change being one line. Right now the clean-up commits are all in separate blocks of work to make things a little easier to see what's been done, but I'll squash them together before merging.

allredj

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

romainbrenguier · 2019-08-14T13:34:29Z

src/solvers/strings/string_constraint_generator.h

+
+  /// \todo The specification may not be correct for the case where the
+  /// string is shorter than end. An actual java program should throw an
+  /// exception in that case.


💡 this looks outdated compared to the add_axioms_for_substring(const function_application_exprt) (but not related to this PR)

romainbrenguier · 2019-08-14T13:36:52Z

src/solvers/strings/string_constraint_generator.h

-  const function_application_exprt &f,
-  array_poolt &array_pool);
+public:
+  std::pair<exprt, string_constraintst> add_axioms_for_concat(


💡 at some point we should remove the add_ from these method names, since it doesn't add them but return them (doesn't need to be in this PR)

romainbrenguier · 2019-08-14T13:38:37Z

src/solvers/strings/string_builtin_function.cpp

-    auto pair = add_axioms_for_insert(
-      generator.fresh_symbol, result, input1, input2, args[0], array_pool);
+    auto pair = generator.add_axioms_for_insert(
+      result, input1, input2, args[0]);


this commit should be squashed in the previous one if it doesn't compile without it

allredj

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

Also removed all arguments that can now be accessed directly via their fields.

Due to the improvements in constant prop we increasingly have constraints that are trivially simplified, like: if 5 >= 2 do x else y Also because of the way these conditions are combined - the resulting merged if gets added to all subsequent conditions and values - we end up with expressions like this: if 5 >= 2 then (if 5 >= 2 do x ... else y ...) else (if 5 >= 2 do x ... else y ...) Where the size of the expression increases exponentially to the complexity of the original if statement even if the entire conditional is trivial to prove right/wrong. This could likely be worked out by the SAT solver happily enough but due to the size of the resulting expressions (I've seen ones 1.34 billion nodes deep) it never gets there within a reasonable time-frame.

allredj

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

JohnDumbell requested review from martin-cs, peterschrammel and romainbrenguier as code owners July 29, 2019 12:43

JohnDumbell self-assigned this Jul 29, 2019

JohnDumbell force-pushed the jd/feature/string_refine_combine_simplify branch 4 times, most recently from 0976b08 to 40a3138 Compare July 30, 2019 09:30

JohnDumbell requested review from chrisr-diffblue, kroening, smowton and tautschnig as code owners July 30, 2019 09:30

JohnDumbell force-pushed the jd/feature/string_refine_combine_simplify branch from 40a3138 to c70f7ef Compare July 31, 2019 10:07

allredj reviewed Jul 31, 2019

View reviewed changes

tautschnig approved these changes Aug 5, 2019

View reviewed changes

tautschnig assigned peterschrammel, martin-cs and romainbrenguier Aug 5, 2019

romainbrenguier reviewed Aug 5, 2019

View reviewed changes

JohnDumbell force-pushed the jd/feature/string_refine_combine_simplify branch from c70f7ef to 46cf072 Compare August 5, 2019 16:57

allredj reviewed Aug 5, 2019

View reviewed changes

romainbrenguier approved these changes Aug 6, 2019

View reviewed changes

romainbrenguier removed their assignment Aug 6, 2019

romainbrenguier reviewed Aug 7, 2019

View reviewed changes

romainbrenguier mentioned this pull request Aug 8, 2019

Clean up string constraint generator class #4995

Merged

6 tasks

JohnDumbell force-pushed the jd/feature/string_refine_combine_simplify branch 2 times, most recently from 902389c to 326d02c Compare August 13, 2019 14:28

JohnDumbell force-pushed the jd/feature/string_refine_combine_simplify branch 3 times, most recently from e1c7a85 to dad8579 Compare August 14, 2019 11:16

allredj reviewed Aug 14, 2019

View reviewed changes

romainbrenguier approved these changes Aug 14, 2019

View reviewed changes

JohnDumbell force-pushed the jd/feature/string_refine_combine_simplify branch from dad8579 to 8868378 Compare August 14, 2019 13:54

allredj reviewed Aug 14, 2019

View reviewed changes

JohnDumbell added 2 commits August 29, 2019 10:57

Move add_axiom methods to string_constraint_generator

4c48218

Also removed all arguments that can now be accessed directly via their fields.

JohnDumbell force-pushed the jd/feature/string_refine_combine_simplify branch from 8868378 to 303ec4d Compare August 29, 2019 10:47

allredj reviewed Aug 29, 2019

View reviewed changes

JohnDumbell merged commit 73e410a into diffblue:develop Sep 3, 2019

JohnDumbell deleted the jd/feature/string_refine_combine_simplify branch September 3, 2019 11:03

		merge(result2.second, std::move(result1.second));
		simplify(return_code, ns);

Simplify when combining string-refinement result constraints #4957

Simplify when combining string-refinement result constraints #4957

Uh oh!

Conversation

JohnDumbell commented Jul 29, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov-io commented Jul 31, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

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

Uh oh!

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

smowton commented Aug 13, 2019

Uh oh!

JohnDumbell commented Aug 13, 2019

Uh oh!

JohnDumbell commented Aug 14, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

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!

Uh oh!

JohnDumbell commented Jul 29, 2019 •

edited

Loading

codecov-io commented Jul 31, 2019 •

edited

Loading

JohnDumbell commented Aug 14, 2019 •

edited

Loading