String refinement must not rely on input equations to be simplified #4069
Conversation
tautschnig
requested review from
chrisr-diffblue,
kroening,
peterschrammel and
smowton
as code owners
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: c098207).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99641918
tautschnig
force-pushed
the
string-solver-simplify
branch
from
c098207 to
e47155b
Compare
tautschnig
requested review from
martin-cs and
romainbrenguier
as code owners
| @@ -645,7 +645,10 @@ decision_proceduret::resultt string_refinementt::dec_solve() | |||
| for(equal_exprt &eq : equations) | |||
| { | |||
| if(can_cast_expr<function_application_exprt>(eq.rhs())) | |||
| { | |||
| simplify(eq.rhs(), ns); | |||
There was a problem hiding this comment.
I was a bit confused by the distinction between simplify and simplify_expr; the second one should probably be called simplify_copy, but that's outside the scope of this PR, and they probably need some rework.
| ^\[.*assertion.1\].* line 8.* SUCCESS$ | ||
| ^\[.*assertion.2\].* line 9.* FAILURE$ | ||
| -- | ||
| non equal types |
There was a problem hiding this comment.
maybe add a comment on what this test is checking
tautschnig
force-pushed
the
string-solver-simplify
branch
from
e47155b to
b737ba2
Compare
|
I have expanded the commit message and added a comment to the newly added test. |
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: e47155b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99661188
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.
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: b737ba2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99664907
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.
JBMC would produce wrong results when running the newly added test. Various methods in string solver either assume a canonical representation of objects in table lookups or only deal with a limited set of expressions, which is reasonable so as not to duplicate abilities that the simplifier already has.
tautschnig
force-pushed
the
string-solver-simplify
branch
from
b737ba2 to
03025a1
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 03025a1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99691293
JBMC would produce wrong results when running the newly added test.