Bugfix/char array in string solver #3248

romainbrenguier · 2018-10-29T16:21:28Z

Each commit message has a non-empty body, explaining why the change was made.
[na] Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
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.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig

Looks ok to me.

smowton · 2018-10-29T17:10:28Z

A fix suggests a regression test?

martin-cs

I agree with @smowton . It is not obvious what the effect of the bug fix is. It would be nice to have at least one test that is wrong before and right afterwards just to make clear one of the higher-level effects of this.

romainbrenguier · 2018-10-30T08:02:06Z

@smowton @martin-cs I agree that this PR should have tests, and I tried adding some but couldn't manage to do it in two days of work. The issue appears on another of our tool and I couldn't reproduce with JBMC, (the example uses --cover location which no longer exists in JBMC). Unit tests will be good but I encounter lot of bugs in the different layers of the solvers when the formulas don't come from a goto-program but are hand-written for the unit test. I have a PR that add tests for this fix in another of our repository https://github.com/diffblue/test-gen/pull/2428
I want look a bit more in depth at the bugs I encounter while writing unit testing, and write tests for each layers but this will require more time.

tautschnig · 2018-10-30T08:24:00Z

To keep effort reasonable I'd say it's ok if there are regression tests elsewhere.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 3129270).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89619587
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 1dc3227).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89626120
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

thk123

I agree it would be better to see a regression added as part of this PR too

thk123 · 2018-10-30T12:16:54Z

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -36,7 +36,7 @@ class tt
  }


⛏️ typo in commit message:

We The way it was used was inconsistent.

First sentence also has some problems.

thk123 · 2018-10-30T12:18:36Z

src/util/refined_string_type.cpp

@@ -21,10 +21,10 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include "std_expr.h"

 refined_string_typet::refined_string_typet(
-  const typet &index_type, const typet &char_type)
+  const typet &index_type,
+  const typet &content_type)


Does content_type need to be a pointer_typet? If so, perhaps make this only except a pointer_typet

allredj

I think this makes sense though I'm worried about maintainability. Somehow it should be clear why we have to do the array replacement there and I find the inline comment a bit vague. I suggest extracting that into a separate function.

src/solvers/refinement/string_refinement.cpp

allredj · 2018-10-30T17:40:23Z

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -36,7 +36,7 @@ class tt
  }


First sentence also has some problems.

allredj

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

allredj

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

allredj · 2018-11-01T09:24:58Z

src/solvers/refinement/string_refinement.cpp

+/// Similar to `symbol_resolve.replace_expr` but doesn't mutate the expression
+/// and return the transformed expression instead.
+static exprt
+transform_expr(const union_find_replacet &symbol_resolve, exprt expr)


exprt-> equal_exprt (in the doc you mention equations)

That's more or less what I had in mind. However transform_expr sounds like do_something_to_expr. 😄
How about substitute_with_repr?

I would keep transform as it is used in the standard library for operations without side-effects https://en.cppreference.com/w/cpp/algorithm/transform

Yeah but in std::transform you give the operation as argument, so the generic name makes sense there. Not here, because the caller doesn't know what the operation is.

Yes you are right, but instead of having a "substitute" and a "replace" function name (difficult to see which one is which from the name), I suggest to name this one replace_expr_copy (following the _copy pattern of the stl), making it clear that this one creates a new copy of the expression.

allredj · 2018-11-01T09:26:17Z

src/solvers/refinement/string_refinement.cpp

+/// Substitute sub-expressions in equation by representative elements of
+/// `symbol_resolve` whenever possible.
+/// Similar to `symbol_resolve.replace_expr` but doesn't mutate the expression
+/// and return the transformed expression instead.


⛏️ return -> returns

allredj · 2018-11-01T09:34:34Z

src/solvers/refinement/string_refinement.cpp

+      dependencies,
+      eq_with_char_array_replaced_with_representative_elements,
+      generator.array_pool);
+    if(!node_added)


That's much clearer to me. Thanks!

src/solvers/refinement/string_refinement.cpp

No functional changes

The data should be kept between calls to dec_solve because the set of equations from the last call are not recorded.

In the string refinement we replace symbols corresponding to arrays of characters by cannonical element to ensure that symbols resolving to the same expression are associated the same node. We should not replace char array in equations that are passed to supert, since the underlying solver should handle pointers and arrays, and string_refinementt should not interfer with it.

We make the second argument be the content type. This is more compatible, and is how it is used at least once in the code base. The way it was used was inconsistent.

allredj

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

romainbrenguier requested review from kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners October 29, 2018 16:21

tautschnig approved these changes Oct 29, 2018

View reviewed changes

tautschnig assigned romainbrenguier Oct 29, 2018

martin-cs reviewed Oct 29, 2018

View reviewed changes

romainbrenguier force-pushed the bugfix/char-array-in-string-solver branch from 14268da to 3129270 Compare October 30, 2018 07:59

tautschnig assigned peterschrammel and martin-cs and unassigned romainbrenguier Oct 30, 2018

romainbrenguier force-pushed the bugfix/char-array-in-string-solver branch from 3129270 to 1dc3227 Compare October 30, 2018 09:06

allredj reviewed Oct 30, 2018

View reviewed changes

thk123 reviewed Oct 30, 2018

View reviewed changes

allredj reviewed Oct 30, 2018

View reviewed changes

romainbrenguier force-pushed the bugfix/char-array-in-string-solver branch from 1dc3227 to cc6e0f9 Compare October 31, 2018 09:59

romainbrenguier requested review from cesaro, cristina-david and NathanJPhillips as code owners October 31, 2018 09:59

romainbrenguier force-pushed the bugfix/char-array-in-string-solver branch from cc6e0f9 to 959d680 Compare October 31, 2018 10:22

allredj reviewed Oct 31, 2018

View reviewed changes

peterschrammel approved these changes Oct 31, 2018

View reviewed changes

romainbrenguier force-pushed the bugfix/char-array-in-string-solver branch from 959d680 to 58e6339 Compare November 1, 2018 07:13

allredj reviewed Nov 1, 2018

View reviewed changes

allredj approved these changes Nov 1, 2018

View reviewed changes

romainbrenguier added 6 commits November 2, 2018 06:46

Make type more precise

64379dd

No functional changes

Correct the way symbol_resolve is computed

ab537ef

The data should be kept between calls to dec_solve because the set of equations from the last call are not recorded.

Correct refined_string_typet constructor

00aaa6d

We make the second argument be the content type. This is more compatible, and is how it is used at least once in the code base. The way it was used was inconsistent.

Use replace_expr_copy to clarify loop in dec_solve

cf0f085

Make content type an pointer_typet in refined_string_type

33b005c

romainbrenguier force-pushed the bugfix/char-array-in-string-solver branch from 58e6339 to 33b005c Compare November 2, 2018 07:21

allredj reviewed Nov 2, 2018

View reviewed changes

romainbrenguier merged commit 64ec195 into diffblue:develop Nov 5, 2018

romainbrenguier deleted the bugfix/char-array-in-string-solver branch November 5, 2018 09:25

Bugfix/char array in string solver #3248

Bugfix/char array in string solver #3248

Uh oh!

Conversation

romainbrenguier commented Oct 29, 2018

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Oct 29, 2018

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Oct 30, 2018

Uh oh!

tautschnig commented Oct 30, 2018

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!

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

Uh oh!

Uh oh!

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!

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!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!