Tests to check inconsistent assumptions involving __CPROVER_r_ok #5321

danpoe · 2020-04-24T15:14:30Z

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.
n/a 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.

thk123

Looks good - some general comments, also I note these are only for r_ok, we presumably need them for the other primitives.

Overall comments:

Do we need to test the local and global pointer every time? Produces a lot of duplication, do they end up looking very different in the formulas?
Should we be testing pointers to memory mallocd with > size of the object (e.g. arrays)
Should we be testing pointers to statically allocated arrays
Should we best testing pointers that are passed in from another function

Also, this is a lot of quite specific tests. I'd be tempted to move them out of regression/cbmc (perhaps into a folder called cprover-primitives, or perhaps tag them as THROUGH when they are enabled

thk123 · 2020-04-24T15:18:29Z

regression/cbmc/r_w_ok_inconsistent_dead/test-global-no-cp.desc

+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer to an out of scope


💚 Thanks

Though an explanation of why FUTURE (and link to relevant ticket) would be good

I think the test and the test description already provide this explanation. The FUTURE just indicates that the test does not currently pass.

regression/cbmc/r_w_ok_inconsistent_dead/test-global-no-cp.desc

thk123 · 2020-04-24T15:20:37Z

regression/cbmc/r_w_ok_inconsistent_dead/test-global-no-cp.desc

@@ -0,0 +1,10 @@
+FUTURE
+main.c
+--function test_global_pointer --pointer-check --no-simplify --no-propagation


❓ Could we include somewhere an explanation why the no-propagation flag is needed to be tested separately?

Do you think I should add an explanation to every .desc file? Basically we want to test with --no-simplify --no-propagation (which turns off expression simplification and constant propagation) and without those two, so as to check that both the constraint encoding and the simplification/constant propagation work correctly.

regression/cbmc/r_w_ok_inconsistent_integer/main.c

regression/cbmc/r_w_ok_inconsistent_integer/test-global.desc

regression/cbmc/r_w_ok_inconsistent_nondet/main.c

regression/cbmc/r_w_ok_inconsistent_valid/main.c

thk123 · 2020-04-24T15:33:58Z

regression/cbmc/r_w_ok_inconsistent_valid/test-global-no-cp.desc

@@ -0,0 +1,11 @@
+KNOWNBUG


Why is this knownbug rather than future?

This particular test made cbmc crash. I'll add a comment to say that, and will add a simpler test too that shows the same bug.

regression/cbmc/r_w_ok_inconsistent_valid/test-global-no-cp.desc

thk123 · 2020-04-24T15:35:41Z

regression/cbmc/r_w_ok_inconsistent_valid_negated/main.c

+  __CPROVER_assume(p1 != NULL);
+
+  __CPROVER_assume(
+    !__CPROVER_r_ok(p1, 1) ||


I'd highlight the negation here with a comment explaining the purpose

Ehh only if you think worth it - it is of course also explained in the description

danielsn · 2020-04-28T15:58:20Z

regression/cbmc/r_w_ok_inconsistent_dead/main.c

+  }
+
+  __CPROVER_assume(__CPROVER_r_ok(p, 1));
+  assert(0); // fails


What does "fails" mean. Do you really mean unreachable?

It means that the assertion fails, i.e. is reachable.

danielsn · 2020-04-28T15:59:57Z

regression/cbmc/r_w_ok_inconsistent_dead/test-global-no-cp.desc

@@ -0,0 +1,10 @@
+FUTURE


What does FUTURE mean?

Tests that currently don't pass but are not bugs are marked as FUTURE. This is typically used for tests for unimplemented features. Here the test doesn't pass due to the overapproximate behaviour of __CPROVER_r_ok(). If it will be made more pecise in the future it should pass.

danpoe · 2020-04-28T16:19:36Z

@thk123 Indeed the separate tests for global and local pointers were unnecessary. The intention was to account for differences in the result of the local bitvector analysis but it gives the same result for both cases.

danpoe · 2020-04-30T10:28:13Z

@thk123 I've now put the tests in a new directory cbmc-primitives. The tests are very quick so don't need to be tagged as THOROUGH.

Regarding your points (2) and (3) above, we don't necessarily need to separately test these cases as the behaviour is exactly the same for malloced objects of size 1 or > 1 and for static objects of size 1 or size > 1 (i.e. statically allocated arrays). Also the behaviour will be the same for pointers passed into functions.

thk123

Probably what CI is telling you, but your new folder will need a Makefile and CMakeLists.txt to tell it how to behave. (A short README.md explaining the purpose of the folder would be appreciated, but not required).

Do you think I should add an explanation to every .desc file? Basically we want to test with --no-simplify --no-propagation (which turns off expression simplification and constant propagation) and without those two, so as to check that both the constraint encoding and the simplification/constant propagation work correctly.

Frankly yes - since no way to know what test will be opened, best to put it in all of them. Should of course just be the same sentence copy-pasted!

Anyways, thanks for the tweaks, blocking comments addressed - though would appreciate raising and referencing bugs for the crashes to be sure we turn the tests back on when they're fixed. Just need to add the Make stuff to the folder and we should be good.

thk123 · 2020-04-29T09:22:49Z

regression/cbmc/r_w_ok_bug/test.desc

+--
+^warning: ignoring
+--
+Crashes during the flattening


This is pretty bad! I guess we should raise a bug?

We should raise a bug/cbmc issue for this and mention it in the .desc

Issue recorded as #5328, and added the number to the .desc file.

thk123 · 2020-04-30T11:21:53Z

regression/cbmc-primitives/r_w_ok_inconsistent_integer/main.c

+
+void main()
+{
+  // pointer with object bits = 123 and offset = 123


Thanks for the improvement - as the reader, I'm still left with the question of why you're constructing such a pointer. I think this would still be improved with a comment as to why this is an interesting pointer. Is it because it tricks cbmc into thinking it is valid?

Yes, it's a pointer that doesn't point to valid memory but isn't special in any other way. Added a description.

thk123 · 2020-04-30T11:22:58Z

regression/cbmc-primitives/r_w_ok_valid_negated/main.c

+  char *p1 = &c1;
+
+  assert(!__CPROVER_r_ok(p1, 2));
+  assert(!__CPROVER_r_ok(p1 - 1, 1));
+  assert(!__CPROVER_r_ok(p1 + 1, 1));
+
+  char *p2 = &c2;
+
+  assert(!__CPROVER_r_ok(p2, 2));
+  assert(!__CPROVER_r_ok(p2 - 1, 1));
+  assert(!__CPROVER_r_ok(p2 + 1, 1));
+
+  char *p3 = malloc(1);
+
+  assert(!__CPROVER_r_ok(p3, 2));
+  assert(!__CPROVER_r_ok(p3 - 1, 1));
+  assert(!__CPROVER_r_ok(p3 + 1, 1));


This is much better imo 💚

…VER_r_ok() Adds tests to check that inconsistent assumptions involving __CPROVER_r_ok() can be detected by checking if a subsequent assert(0) fails.

danpoe force-pushed the tests/pointer-primitives branch from 85de939 to fa60778 Compare April 24, 2020 15:16

danpoe added the aws Bugs or features of importance to AWS CBMC users label Apr 24, 2020

thk123 reviewed Apr 24, 2020

View reviewed changes

danpoe mentioned this pull request Apr 27, 2020

__CPROVER_w_ok has weird behaviour #5194

Closed

danielsn reviewed Apr 28, 2020

View reviewed changes

danpoe force-pushed the tests/pointer-primitives branch from fa60778 to f514175 Compare April 28, 2020 16:04

danpoe force-pushed the tests/pointer-primitives branch 3 times, most recently from f0527ae to b34b155 Compare April 29, 2020 17:06

danpoe force-pushed the tests/pointer-primitives branch from b34b155 to e9b5146 Compare April 30, 2020 10:29

danpoe marked this pull request as ready for review April 30, 2020 10:35

thk123 approved these changes Apr 30, 2020

View reviewed changes

danpoe force-pushed the tests/pointer-primitives branch 2 times, most recently from 09be997 to f6a0800 Compare May 1, 2020 08:55

danpoe added 2 commits May 6, 2020 14:06

Add regression tests to for inconsistent assumptions involving __CPRO…

62880cd

…VER_r_ok() Adds tests to check that inconsistent assumptions involving __CPROVER_r_ok() can be detected by checking if a subsequent assert(0) fails.

Add regression test for cbmc crash in flattening

b1be232

danpoe force-pushed the tests/pointer-primitives branch from f6a0800 to b1be232 Compare May 6, 2020 13:07

danpoe merged commit 873daa9 into diffblue:develop May 6, 2020

danpoe deleted the tests/pointer-primitives branch June 2, 2020 17:05

Tests to check inconsistent assumptions involving __CPROVER_r_ok #5321

Tests to check inconsistent assumptions involving __CPROVER_r_ok #5321

Uh oh!

Conversation

danpoe commented Apr 24, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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!

danpoe commented Apr 28, 2020

Uh oh!

danpoe commented Apr 30, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

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!

danpoe commented Apr 24, 2020 •

edited

Loading

danpoe commented Apr 30, 2020 •

edited

Loading