Use OBJECT_SIZE(p) for dynamic memory bounds checking #5247

danpoe · 2020-02-26T14:59:09Z

This changes the dynamic memory bounds checking predicate in address_check().
It now uses OBJECT_SIZE() instead of the variables __CPROVER_malloc_size and
__CPROVER_malloc_object that are set in the malloc() model. This also means that
the predicates __CPROVER_r_ok()/__CPROVER_w_ok() will be more precise. In the
previous approach, the following assertion could not be proven for example:

void main() { char *c = malloc(1); assert(!__CPROVER_r_ok(c, 2)); }

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.

codecov-io · 2020-02-26T17:13:05Z

Codecov Report

Merging #5247 into develop will decrease coverage by 0.01%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #5247      +/-   ##
===========================================
- Coverage    67.42%   67.41%   -0.02%     
===========================================
  Files         1162     1162              
  Lines        95637    95637              
===========================================
- Hits         64484    64473      -11     
- Misses       31153    31164      +11

Flag	Coverage Δ
#cproversmt2	`42.56% <100%> (-0.02%)`	⬇️
#regression	`63.94% <100%> (-0.02%)`	⬇️
#unit	`31.9% <0%> (ø)`	⬆️

Impacted Files	Coverage Δ
src/analyses/goto_check.cpp	`79.45% <100%> (ø)`	⬆️
src/util/pointer_predicates.cpp	`55% <0%> (-13.75%)`	⬇️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update cd2c65b...8f0f289. Read the comment docs.

thk123

I can't say I really understand much about the code change, but the tests look robust. I assume it is already tested, but it is worth having a test using --pointer-check and so some dynamically allocated memory?

regression/cbmc/r_w_ok5/main.c

regression/cbmc/r_w_ok7/main.c

regression/cbmc/r_w_ok7/test.desc

regression/cbmc/r_w_ok7/main.c

thk123 · 2020-02-28T10:36:03Z

regression/cbmc/r_w_ok8/main.c

+{
+  int *x = malloc(2);
+  int *y = malloc(2);
+  assert(__CPROVER_r_ok(x, 3) == __CPROVER_r_ok(y, 3));


❓ Not sure I understand the purpose of the test

This was reported in issue #5194. It checks that two uses of __CPROVER_r_ok() can return false simultaneously. Previously only one call could return false at a time.

👍 Please add to the desc file 🙂

regression/cbmc/r_w_ok8/test.desc

thk123 · 2020-02-28T10:36:50Z

regression/cbmc/r_w_ok6/main.c

+  assert(__CPROVER_r_ok(p, 2));
+  assert(!__CPROVER_r_ok(p, 2));
+
+  assert(__CPROVER_r_ok(p, 3));


Nice - not obvious so good to check it works

danpoe · 2020-02-28T14:03:36Z

@thk123 Ok, addressed all the comments.

thk123

Thanks - looks great.

thk123 · 2020-02-28T14:08:52Z

regression/cbmc/r_w_ok8/test.desc

+simultaneously in the encoding of the program. Previously, at most one call
+could be false at a time. This was imprecise, however, it was sufficient to
+guarantee soundness when the __CPROVER_r_ok() primitive was used directly in an
+assertion (i.e., as assert(__CPROVER_r_ok(p, size)).


You could link to the relevant issue so people can find more context

thk123 · 2020-02-28T14:09:17Z

regression/cbmc/r_w_ok5/test.desc

+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring


⛏️ Still missing an explanation

I think this one is simple enough to not need an explanation

This changes the dynamic memory bounds checking predicate in address_check(). It now uses OBJECT_SIZE() instead of the variables __CPROVER_malloc_size and __CPROVER_malloc_object that are set in the malloc() model. This also means that the predicates __CPROVER_r_ok()/__CPROVER_w_ok() will be more precise. In the previous approach, the following assertion could not be proven for example: void main() { char *c = malloc(1); assert(!__CPROVER_r_ok(c, 2)); }

danpoe requested review from chrisr-diffblue, martin-cs, peterschrammel, smowton and thk123 as code owners February 26, 2020 14:59

danpoe force-pushed the feature/memory-bounds-check branch 3 times, most recently from cbddb64 to 2129b2f Compare February 26, 2020 16:58

danpoe force-pushed the feature/memory-bounds-check branch 3 times, most recently from 0d509c9 to 8f0f289 Compare February 27, 2020 11:21

thk123 reviewed Feb 28, 2020

View reviewed changes

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

danpoe force-pushed the feature/memory-bounds-check branch from 8f0f289 to f1fa849 Compare February 28, 2020 14:02

thk123 approved these changes Feb 28, 2020

View reviewed changes

danpoe force-pushed the feature/memory-bounds-check branch from f1fa849 to e05d813 Compare February 28, 2020 15:47

danpoe merged commit 8a24f79 into diffblue:develop Feb 28, 2020

tautschnig mentioned this pull request Mar 2, 2020

__CPROVER_w_ok has weird behaviour #5194

Closed

danpoe deleted the feature/memory-bounds-check branch June 2, 2020 17:06

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Use OBJECT_SIZE(p) for dynamic memory bounds checking #5247

Use OBJECT_SIZE(p) for dynamic memory bounds checking #5247

Uh oh!

danpoe commented Feb 26, 2020 •

edited

Loading

Uh oh!

codecov-io commented Feb 26, 2020 •

edited

Loading

Uh oh!

thk123 left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thk123 Feb 28, 2020

Uh oh!

danpoe Feb 28, 2020 •

edited

Loading

Uh oh!

thk123 Feb 28, 2020

Uh oh!

Uh oh!

thk123 Feb 28, 2020

Uh oh!

danpoe commented Feb 28, 2020

Uh oh!

thk123 left a comment

Uh oh!

thk123 Feb 28, 2020

Uh oh!

thk123 Feb 28, 2020

Uh oh!

danpoe Feb 28, 2020

Uh oh!

Uh oh!

Use OBJECT_SIZE(p) for dynamic memory bounds checking #5247

Use OBJECT_SIZE(p) for dynamic memory bounds checking #5247

Uh oh!

Conversation

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

Uh oh!

Uh oh!

codecov-io commented Feb 26, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thk123 Feb 28, 2020

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thk123 Feb 28, 2020

Choose a reason for hiding this comment

Uh oh!

Uh oh!

thk123 Feb 28, 2020

Choose a reason for hiding this comment

Uh oh!

danpoe commented Feb 28, 2020

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 Feb 28, 2020

Choose a reason for hiding this comment

Uh oh!

thk123 Feb 28, 2020

Choose a reason for hiding this comment

Uh oh!

danpoe Feb 28, 2020

Choose a reason for hiding this comment

Uh oh!

Uh oh!

danpoe commented Feb 26, 2020 •

edited

Loading

codecov-io commented Feb 26, 2020 •

edited

Loading

danpoe Feb 28, 2020 •

edited

Loading