Prevent potential string solver failures by romainbrenguier · Pull Request #4489 · diffblue/cbmc

romainbrenguier · 2019-04-05T13:07:40Z

Two small corrections which prevent a bug which I observed while testing the field-sensitivity branch (#2574)

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.
[na] 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.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

Some nitpicks, but LGTM even if considered independently of field-sensitive symex branch.

allredj · 2019-04-05T13:14:24Z

src/solvers/strings/string_refinement.cpp

    }
    const auto array = supert::get(current.get());
    const auto index = get(index_expr->index());
+    if(array.is_nil())


⛏️ A comment explaining why we do that would be useful (the commit message is good in that sense).

allredj · 2019-04-05T13:15:36Z

src/solvers/strings/string_refinement.cpp

+  {
+    add_lemma(binary_relation_exprt{
+      string.length(), ID_ge, from_integer(0, string.length().type())});
+  }


Commit message should be changed to Constrain all generated strings to have non-negative length. I was initially confused because I thought you were excluding 0.

I'm massively surprised we didn't already have that constraint somewhere though...

A similar constraint exists in the goto-program for all non-deterministic strings generated there. But we didn't have it for new strings generated by the solver itself.

peterschrammel · 2019-04-05T13:44:36Z

jbmc/regression/jbmc-strings/StringConcat/test_string_nondet_array.desc

+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED
+line 318 no uncaught exception: FAILURE


Can you check that the right exception is thrown?

We could do that, if we didn't use --throw-runtime-exceptions but the failure I observed happened specifically when the option was used so I prefer to keep it. We could look for a particular exception in the trace, but here both NullPointerException and ArrayOutOfBoundsException could be valid counterexample traces.

Those two exceptions could still be matched by a single regular expression?

If the underlying solver does not know about the existence of an array, it can return nil, which shouldn't be returned inside an index_expression as in particular the type will be broken.

Generated strings should have positive length, not adding these lemmas could potentially lead to overflow errors in check_axioms which means the solver will end with an error because the index set is empty.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: a2273f1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107230480
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: f2fa572).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107233242
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.

smowton

Looks good

smowton · 2019-04-05T14:34:38Z

jbmc/regression/jbmc-strings/StringConcat/test_string_nondet_array.desc

+^SIGNAL=0$
+^VERIFICATION FAILED
+line 318 no uncaught exception: FAILURE
+--


No need for these

This is an example for which a branch with changes to symex (field-sensitivity) caused failure in the string solver because a nil expression got into the model.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 2c2c5ed).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107250045
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.

romainbrenguier added bugfix String solver labels Apr 5, 2019

romainbrenguier requested review from martin-cs and peterschrammel as code owners April 5, 2019 13:07

romainbrenguier force-pushed the bugfix/string-solver-nil-array branch 2 times, most recently from 3d387d0 to a2273f1 Compare April 5, 2019 13:12

allredj approved these changes Apr 5, 2019

View reviewed changes

tautschnig assigned peterschrammel and martin-cs Apr 5, 2019

romainbrenguier force-pushed the bugfix/string-solver-nil-array branch from a2273f1 to f2fa572 Compare April 5, 2019 13:32

peterschrammel approved these changes Apr 5, 2019

View reviewed changes

tautschnig assigned romainbrenguier and unassigned peterschrammel and martin-cs Apr 5, 2019

romainbrenguier added 2 commits April 5, 2019 14:48

Handle nil case in string_refinementt::get

36e579c

If the underlying solver does not know about the existence of an array, it can return nil, which shouldn't be returned inside an index_expression as in particular the type will be broken.

Constrain all generated strings to have non-negative length

9962b7c

Generated strings should have positive length, not adding these lemmas could potentially lead to overflow errors in check_axioms which means the solver will end with an error because the index set is empty.

allredj reviewed Apr 5, 2019

View reviewed changes

smowton approved these changes Apr 5, 2019

View reviewed changes

Add a test for the string solver

2c2c5ed

This is an example for which a branch with changes to symex (field-sensitivity) caused failure in the string solver because a nil expression got into the model.

romainbrenguier force-pushed the bugfix/string-solver-nil-array branch from f2fa572 to 2c2c5ed Compare April 5, 2019 15:18

allredj reviewed Apr 5, 2019

View reviewed changes

tautschnig merged commit 14f618c into diffblue:develop Apr 6, 2019

Conversation

romainbrenguier commented Apr 5, 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!

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!

smowton left a comment

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

romainbrenguier commented Apr 5, 2019 •

edited

Loading