Extend and cleanup usability of __CPROVER_{r,w}_ok #4485

tautschnig · 2019-04-04T18:39:04Z

__CPROVER_r_ok and __CPROVER_w_ok had surprising behaviour that wasn't documented. Make the behaviour less surprising and document it.

Each commit message has a non-empty body, explaining why the change was made.
n/a 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).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

danielsn · 2019-04-04T18:43:50Z

You might want to add a test where "r_ok" should pass, but "w_ok" should fail. Something like

void test() {
  const char* str = "foobar";
  assert(!__CPROVER_w_ok(str, 6));
  assert(__CPROVER_r_ok(str, 6));
}

tautschnig · 2019-04-04T18:55:09Z

You might want to add a test where "r_ok" should pass, but "w_ok" should fail.

Thank you very much for the suggestion - I have added such a test, but marked it as KNOWNBUG as we do not currently have a way do distinguish lvalues at this point.

allredj

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

danielsn · 2019-04-04T19:42:41Z

regression/cbmc/r_w_ok1/main.c

+  assert(__CPROVER_r_ok(arbitrary_size, n));
+  assert(__CPROVER_w_ok(arbitrary_size, n));
+
+  assert(__CPROVER_r_ok(arbitrary_size, n + 1));


Why does this succeed?

Without --pointer-check any use of __CPROVER_{r,w}_ok is now a no-op (and is now also documented as such), but with --pointer-check this fails as expected (there are two regression tests using the same main.c file included).

Is this what we want? I would find it more intuitive if these were independent.

It does make the implementation a lot easier, and also removes a need for documentation, so that seems much better. The only cost is that we will unconditionally need to run the local alias analysis.

Ok, this will require #4471 to be merged first. And another bug left to be debugged.

Hmm, actually there is more to it than just #4471, we also seem to be messing up ID_this elsewhere.

If the cost of the local alias analysis is a concern, there could be a quick scan for the predicate in the function; but so far, that analysis has not been cause for concern.

Agreed, I just need to fix bugs in the C++ and Java front-ends first as the local alias analysis needs to succeed in doing symbol-table lookups...

Ensure Java stubbing names parameters [blocks: #4485]

We did not have an explicit test of __CPROVER_{r,w}_ok, only implicit ones as we use these predicates in our model of the C library. While preparing a test it became apparent that the predicates are only evaluated when --pointer-check is set. This caused surprising behaviour as a negated predicate would result in failing assertions. Instead, make sure the expression is always evaluated, independent of --pointer-check. This requires always performing a local alias analysis, even when no pointer checks are enabled.

smowton · 2019-04-10T10:35:47Z

src/analyses/goto_check.cpp

@@ -1765,6 +1773,15 @@ void goto_checkt::goto_check(

      // the LHS might invalidate any assertion
      invalidate(code_assign.lhs());
+
+      if(has_subexpr(i.code.op1(), [](const exprt &expr) {


i.code.op1 -> code_assign.rhs

smowton · 2019-04-10T10:37:03Z

src/analyses/goto_check.cpp

+      {
+        auto rw_ok_cond = rw_ok_check(i.code.op1());
+        if(rw_ok_cond.has_value())
+          i.code.op1() = *rw_ok_cond;


Hang on, so if any subexpr was an r_ok or w_ok then you overwrite the whole RHS? That seems surprising, what's the rationale for blowing away arbitrary AST nodes here?

No, rw_ok_check will take care of only replacing parts of the RHS.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 1a8b834).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107785716
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 · 2019-04-10T12:51:55Z

src/analyses/goto_check.cpp

+             return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
+           }))
+        {
+          auto rw_ok_cond = rw_ok_check(i.code.op0());


to_code_return(code).return_value()

Oops, thank you for keeping me from being lazy.

We previously only evaluated __CPROVER_{r,w}_ok in assertions (without telling anyone that was the case). Instead, evaluate it in all contexts where it might reasonably appear.

We do not currently have a good way of distinguishing lvalues from rvalues, and thus actually treat __CPROVER_w_ok and __CPROVER_r_ok the same. The test shows that this shouldn't always be done.

allredj

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

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

tautschnig added the bugfix label Apr 4, 2019

tautschnig requested review from chrisr-diffblue, danpoe, martin-cs, owen-mc-diffblue, peterschrammel, smowton and thk123 as code owners April 4, 2019 18:39

tautschnig force-pushed the cprover-rw-ok branch from c4b19af to b44e86a Compare April 4, 2019 18:39

tautschnig requested a review from kroening as a code owner April 4, 2019 18:53

tautschnig force-pushed the cprover-rw-ok branch from fceca1f to 7f8f20e Compare April 4, 2019 18:57

tautschnig assigned kroening Apr 4, 2019

allredj reviewed Apr 4, 2019

View reviewed changes

danielsn reviewed Apr 4, 2019

View reviewed changes

tautschnig assigned tautschnig and unassigned kroening Apr 5, 2019

tautschnig added the dependent - do not merge label Apr 8, 2019

tautschnig changed the title ~~Extend and cleanup usability of __CPROVER_{r,w}_ok~~ Extend and cleanup usability of __CPROVER_{r,w}_ok [depends-on: #4471] Apr 8, 2019

tautschnig changed the title ~~Extend and cleanup usability of __CPROVER_{r,w}_ok [depends-on: #4471]~~ Extend and cleanup usability of __CPROVER_{r,w}_ok [depends-on: #4502] Apr 9, 2019

tautschnig force-pushed the cprover-rw-ok branch from 7f8f20e to 369495c Compare April 9, 2019 11:11

danielsn mentioned this pull request Apr 9, 2019

Faster CBMC stubs for memset and memcpy awslabs/aws-c-common#300

Merged

tautschnig added a commit that referenced this pull request Apr 10, 2019

Merge pull request #4502 from tautschnig/parameter-names

7dd720b

Ensure Java stubbing names parameters [blocks: #4485]

tautschnig changed the title ~~Extend and cleanup usability of __CPROVER_{r,w}_ok [depends-on: #4502]~~ Extend and cleanup usability of __CPROVER_{r,w}_ok Apr 10, 2019

tautschnig force-pushed the cprover-rw-ok branch from 369495c to 1a8b834 Compare April 10, 2019 10:25

tautschnig requested review from cesaro, cristina-david and NathanJPhillips as code owners April 10, 2019 10:25

tautschnig requested a review from pkesseli as a code owner April 10, 2019 10:25

tautschnig removed the dependent - do not merge label Apr 10, 2019

tautschnig assigned smowton, peterschrammel, martin-cs and chrisr-diffblue and unassigned tautschnig Apr 10, 2019

smowton reviewed Apr 10, 2019

View reviewed changes

tautschnig force-pushed the cprover-rw-ok branch from 1a8b834 to d7dc902 Compare April 10, 2019 11:55

allredj reviewed Apr 10, 2019

View reviewed changes

smowton approved these changes Apr 10, 2019

View reviewed changes

tautschnig added 2 commits April 10, 2019 12:57

Support __CPROVER_{r,w}_ok in assignments, assumptions, gotos, returns

5226466

We previously only evaluated __CPROVER_{r,w}_ok in assertions (without telling anyone that was the case). Instead, evaluate it in all contexts where it might reasonably appear.

Add test showing limitations of __CPROVER_w_ok

7ecf1f6

We do not currently have a good way of distinguishing lvalues from rvalues, and thus actually treat __CPROVER_w_ok and __CPROVER_r_ok the same. The test shows that this shouldn't always be done.

tautschnig force-pushed the cprover-rw-ok branch from d7dc902 to 7ecf1f6 Compare April 10, 2019 12:58

allredj reviewed Apr 10, 2019

View reviewed changes

tautschnig merged commit ebecdd8 into diffblue:develop Apr 10, 2019

tautschnig deleted the cprover-rw-ok branch April 10, 2019 19:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Extend and cleanup usability of __CPROVER_{r,w}_ok #4485

Extend and cleanup usability of __CPROVER_{r,w}_ok #4485

tautschnig commented Apr 4, 2019

danielsn commented Apr 4, 2019 •

edited

Loading

tautschnig commented Apr 4, 2019

allredj left a comment

danielsn Apr 4, 2019

tautschnig Apr 4, 2019

kroening Apr 5, 2019

tautschnig Apr 5, 2019

tautschnig Apr 5, 2019

tautschnig Apr 5, 2019

kroening Apr 6, 2019

tautschnig Apr 6, 2019

smowton Apr 10, 2019

tautschnig Apr 10, 2019

smowton Apr 10, 2019

tautschnig Apr 10, 2019 •

edited

Loading

allredj left a comment

smowton Apr 10, 2019

tautschnig Apr 10, 2019

allredj left a comment

allredj left a comment

Extend and cleanup usability of __CPROVER_{r,w}_ok #4485

Extend and cleanup usability of __CPROVER_{r,w}_ok #4485

Conversation

tautschnig commented Apr 4, 2019

danielsn commented Apr 4, 2019 • edited Loading

tautschnig commented Apr 4, 2019

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig Apr 10, 2019 • edited Loading

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

danielsn commented Apr 4, 2019 •

edited

Loading

tautschnig Apr 10, 2019 •

edited

Loading