Handle more formulas than just equations in string solver #5016

romainbrenguier · 2019-08-14T07:41:30Z

Previously the string-solver was restricting builtin-functions to be the left-hand-side of an equations, so formulas like g1 => c = char_at(string, 10) would be forbidden.
This removes this restriction by replacing these function applications by symbols.
The array_to_length and pointer_to_array associations should still only appear on lhs of an equations. Char array equalities should also only appear as an equation.

The changes are tested with unit tests as the current symex is not producing the kind of formulas which were not handled.
The motivation for this feature is that I have seen this kind of equations appear while experimenting with BDD guards #4765

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

codecov-io · 2019-08-16T09:41:33Z

Codecov Report

Merging #5016 into develop will increase coverage by 0.04%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #5016      +/-   ##
===========================================
+ Coverage    69.48%   69.52%   +0.04%     
===========================================
  Files         1310     1311       +1     
  Lines       108813   108955     +142     
===========================================
+ Hits         75609    75755     +146     
+ Misses       33204    33200       -4

Impacted Files	Coverage Δ
src/solvers/strings/string_dependencies.h	`100% <ø> (ø)`	⬆️
src/solvers/strings/string_refinement.h	`100% <ø> (ø)`	⬆️
src/solvers/strings/string_refinement.cpp	`88.52% <100%> (+0.24%)`	⬆️
...ers/strings/string_refinement/dependency_graph.cpp	`100% <100%> (ø)`	⬆️
src/solvers/strings/string_dependencies.cpp	`82.75% <100%> (+0.14%)`	⬆️
...rs/strings/string_refinement/string_refinement.cpp	`100% <100%> (ø)`
src/solvers/strings/string_refinement_util.cpp	`94.66% <0%> (-4%)`	⬇️
unit/catch/catch.hpp	`41.35% <0%> (+0.08%)`	⬆️
... and 1 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 744671a...10418f6. Read the comment docs.

allredj

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

allredj

A change requested in the documentation, otherwise looks good.

allredj · 2019-08-19T09:06:05Z

src/solvers/strings/string_dependencies.h

@@ -188,16 +188,20 @@ class string_dependenciest
 /// If the string builtin_function is not a supported one, mark all the string
 /// arguments as depending on an unknown builtin_function.
 /// \param dependencies: graph to which we add the node
-/// \param equation: an equation whose right hand side is possibly a call to a


The function description needs updating. It still mentions the rhs.

allredj · 2019-08-19T09:26:51Z

src/solvers/strings/string_dependencies.h

+///   builtin functions
+/// \return an expression in which function applications have been replaced
+///   by symbols corresponding to the `return_value` field of the associated
+///   builtin function.


🚫 Missing: Document that the function returns empty when there is no substitution.

allredj · 2019-08-19T11:56:06Z

src/solvers/strings/string_refinement.cpp

+        for(const auto &eq : equations)
+        {
+          if(auto equal_expr = expr_try_dynamic_cast<equal_exprt>(eq))
+            equalities.push_back(*equal_expr);


Not sure I understand. Why do equalities that don't appear as top-level equal_exprts not need to be added to the vector of equalities? 🐎

If they don't appear at the top then we can't be sure they always hold, for instance if we have g1 => (s1 == s2), we cannot be sure s1 and s2 will be equal in the end and we have to keep them as separate symbols (instead of replacing occurences of s1 by s2).

allredj · 2019-08-19T11:57:20Z

src/solvers/strings/string_refinement.cpp

-    equations.push_back(eq_expr);
-  }
+  if(!value)
+    equations.push_back(not_exprt{expr});


Is that to compensate for 🐎 ?

not really, it's more like the opposite: because we introduce things that may not be equal_exprt in equations they need to be filtered out in the previous commit

Since the argument is a unique_ptr, it cannot be copied so having the function take the argument by copy means that it has to be moved at the function call, which makes clear from there that the argument is moved and shouldn't be used afterwards.

The add_node function was only handling expressions of the form: `lhs = builtin_function(args)` We make it handle more general expressions and look recursively for functions to replace, for instance `(lhs == a) && (builtin_function(b) == builtin_function(c))` would be replaced by `(lhs == a) && (string_builtin_return1 == string_builtin_return2)`.

This makes the function more generic

This make it handle the cases where the function application is not directly the right hand side of the equation but may be deeper inside the expression.

EXplicit that it is not modified by the function.

Accept formulas that are not equations as input. This is to make the solver more robust to different kind of formulas. In particular, formulas of the form `guard1 => result = some_string_builin_function(s)` should be accepted.

Even if they are not equations, they may contain formulas talking about char arrays and other expressions which require special handling by the solver.

This tests the solver directly on a set of desired formula instead of through symex as would a regression test. This can be easier to debug when trying to track a bug or add an new feature, as the correspondence with the string solver code would be easier to see.

allredj

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

romainbrenguier requested review from martin-cs and peterschrammel as code owners August 14, 2019 07:41

romainbrenguier added enhancement String solver labels Aug 14, 2019

romainbrenguier force-pushed the enhance/solver-equations branch 8 times, most recently from e8e3a4e to 10418f6 Compare August 16, 2019 08:45

allredj reviewed Aug 16, 2019

View reviewed changes

romainbrenguier assigned peterschrammel and allredj Aug 16, 2019

peterschrammel approved these changes Aug 17, 2019

View reviewed changes

peterschrammel assigned romainbrenguier and unassigned peterschrammel Aug 17, 2019

allredj suggested changes Aug 19, 2019

View reviewed changes

romainbrenguier added 8 commits August 19, 2019 13:04

make_char_array_pointer_associations take exprt argument

2fc646c

This makes the function more generic

Make the string ids replacement look for function_application

ba7578d

This make it handle the cases where the function application is not directly the right hand side of the equation but may be deeper inside the expression.

Mark argument const for identifiers resolution

95f599e

EXplicit that it is not modified by the function.

Make equations of type exprt instead of equal_exprt

f07cbb1

Accept formulas that are not equations as input. This is to make the solver more robust to different kind of formulas. In particular, formulas of the form `guard1 => result = some_string_builin_function(s)` should be accepted.

Give all formulas to the solver

445a880

Even if they are not equations, they may contain formulas talking about char arrays and other expressions which require special handling by the solver.

romainbrenguier force-pushed the enhance/solver-equations branch from 10418f6 to 462d355 Compare August 19, 2019 12:14

romainbrenguier removed their assignment Aug 19, 2019

allredj approved these changes Aug 19, 2019

View reviewed changes

allredj reviewed Aug 20, 2019

View reviewed changes

romainbrenguier merged commit 440ad9c into diffblue:develop Aug 20, 2019

romainbrenguier deleted the enhance/solver-equations branch August 20, 2019 09:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Handle more formulas than just equations in string solver #5016

Handle more formulas than just equations in string solver #5016

Uh oh!

romainbrenguier commented Aug 14, 2019

Uh oh!

codecov-io commented Aug 16, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj Aug 19, 2019

Uh oh!

allredj Aug 19, 2019

Uh oh!

allredj Aug 19, 2019

Uh oh!

romainbrenguier Aug 19, 2019

Uh oh!

allredj Aug 19, 2019

Uh oh!

romainbrenguier Aug 19, 2019

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

Handle more formulas than just equations in string solver #5016

Handle more formulas than just equations in string solver #5016

Uh oh!

Conversation

romainbrenguier commented Aug 14, 2019

Uh oh!

codecov-io commented Aug 16, 2019

Codecov Report

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 Aug 19, 2019

Choose a reason for hiding this comment

Uh oh!

allredj Aug 19, 2019

Choose a reason for hiding this comment

Uh oh!

allredj Aug 19, 2019

Choose a reason for hiding this comment

Uh oh!

romainbrenguier Aug 19, 2019

Choose a reason for hiding this comment

Uh oh!

allredj Aug 19, 2019

Choose a reason for hiding this comment

Uh oh!

romainbrenguier Aug 19, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!