Malloc should fail on too large allocations #5210

xbauch · 2020-01-06T12:02:25Z

via goto-checker with a dedicated cmdl option and a property that acknowledges pointer-width and object-size.

Each commit message has a non-empty body, explaining why the change was made.
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).
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.

xbauch · 2020-01-06T12:03:35Z

This may fix #4604.

xbauch · 2020-01-06T14:07:47Z

It seems that we have a few regression tests that call malloc with nondeterministic value (of type size_t) without assuming reasonable upper bound.

chrisr-diffblue · 2020-01-07T09:57:32Z

src/ansi-c/library/stdlib.c

@@ -115,6 +115,9 @@ inline void *malloc(__CPROVER_size_t malloc_size)
  // realistically, malloc may return NULL,
  // and __CPROVER_allocate doesn't, but no one cares
  __CPROVER_HIDE:;
+  // 8 is the default object bits for ANSI-C and C++
+  if (malloc_size >= ((__CPROVER_size_t)1<<(64-8)))


Can't the object bits size be changed on the command line with --object-bits ? and if so, this probably needs to accommodate that. Ditto for the hardcoded 64, which would probably be wrong if --32 is specified to cbmc :-)

I moved the check into goto-checker, i.e. the stdlib.c implemetation is unchanged, we can use the pointer-width and object-bits from config, and the whole thing is behind an option, so it won't affect the existing tests.

chrisr-diffblue · 2020-01-07T10:02:43Z

regression/cbmc/malloc-too-large/main.c

+
+int main()
+{
+  int *p = malloc(SIZE_MAX);


It would also be nice to have a test for a size that is 1 byte larger than the maximum CBMC can support, and also for a size that is exactly the same as the largest CBMC can support - just to test the boundary condition.

allredj

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

codecov-io · 2020-01-07T13:40:13Z

Codecov Report

Merging #5210 into develop will decrease coverage by 35.53%.
The diff coverage is 25%.

@@             Coverage Diff              @@
##           develop    #5210       +/-   ##
============================================
- Coverage    67.42%   31.89%   -35.54%     
============================================
  Files         1162      910      -252     
  Lines        95620    79452    -16168     
============================================
- Hits         64476    25338    -39138     
- Misses       31144    54114    +22970

Flag	Coverage Δ
#cproversmt2	`?`
#regression	`?`
#unit	`31.89% <25%> (-0.01%)`	⬇️

Impacted Files	Coverage Δ
src/cbmc/cbmc_parse_options.cpp	`13.23% <ø> (-62.42%)`	⬇️
src/cbmc/cbmc_parse_options.h	`0% <ø> (-100%)`	⬇️
src/util/config.h	`40% <ø> (-32.73%)`	⬇️
src/ansi-c/cprover_library.cpp	`0% <0%> (-92.86%)`	⬇️
src/cpp/cprover_library.cpp	`0% <0%> (-90%)`	⬇️
src/ansi-c/ansi_c_internal_additions.cpp	`85.71% <100%> (-6.74%)`	⬇️
src/util/config.cpp	`29.64% <50%> (-26.56%)`	⬇️
src/cpp/cpp_typecheck_virtual_table.cpp	`0% <0%> (-100%)`	⬇️
src/cpp/cpp_name.cpp	`0% <0%> (-100%)`	⬇️
src/cpp/cpp_enum_type.h	`0% <0%> (-100%)`	⬇️
... and 887 more

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 1f2f1fa...195da86. Read the comment docs.

chrisr-diffblue · 2020-01-07T14:33:24Z

regression/cbmc/malloc-too-large-almost/main.c

+{
+  size_t pointer_width = sizeof(void *) * 8;
+  size_t object_bits = 8; // by default
+  size_t cbmc_max_alloc_size = (size_t)1 << (pointer_width - object_bits);


A really tiny nit pick, so feel free to ignore me :-) But I'd personally write this as:

size_t cbmc_max_alloc_size = ((size_t)1 << (pointer_width - object_bits))-1; int *p2 = malloc(cbmc_max_alloc_size); // try to allocate exactly the max

just so that the variable names really do mean what they say. Ditto for the other test case - but like I say, it's a really minor nit for me to pick...

chrisr-diffblue · 2020-01-07T14:36:30Z

src/analyses/goto_check.h

@@ -55,6 +56,7 @@ void goto_check(
  " --nan-check                  check floating-point for NaN\n" \
  " --no-built-in-assertions     ignore assertions in built-in library\n" \
  " --enum-range-check           checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \
+  " --malloc-max-check           check that CBMC can represent the allocated object of requested size" /* NOLINT(whitespace/line_length) */ \


Is a better name for this option "malloc-size-check" ? Don't have a strong opinion.

chrisr-diffblue

Generally looks good to me, and I like that it's moved into goto-check. Apologies for the niggle comments - take them as suggestions, and not absolute requirements.

allredj

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

smowton · 2020-01-08T09:54:54Z

src/analyses/goto_check.cpp

+                         minus_exprt{pointer_bits, object_bits}};
+          add_guarded_property(
+            binary_relation_exprt{rhs_side_effect.op0(), ID_lt, max_alloc_size},
+            "malloc_size < 2 ^ (pointer_width - object_size)",


object_size -> object_id_width?

allredj

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

martin-cs · 2020-01-13T15:39:39Z

On Tue, 2020-01-07 at 06:40 -0800, Chris Ryder wrote: Generally looks good to me, and I like that it's moved into goto- check.

I'm not sure I do. Keeping the modelling of malloc in one place, in the library models seems, to me, to be important. Setting CPROVER globals to control max limits, if malloc can fail, etc. seems a more flexible option and keeps all the modelling together.

danielsn · 2020-01-23T20:07:47Z

It seems that we have a few regression tests that call malloc with nondeterministic value (of type size_t) without assuming reasonable upper bound.

I see two ways to handle malloc(size) where size is too large:

assert(size <= MAX_MALLOC_SIZE)
if(size > MAX_MALLOC_SIZE) return NULL

xbauch · 2020-02-24T15:44:11Z

test group	before	after	slowdown
cbmc-CORE	127.9	146.88	1.14839718530102
cbmc-paths-lifo-CORE	159.87	182.46	1.14130230812535
cbmc-library-CORE	19.11	22.46	1.1753008895866
goto-analyzer-CORE	15.89	17.75	1.11705475141598
ansi-c-CORE	70.67	72.89	1.03141361256545
cbmc-cprover-smt2-CORE	143.8	159.32	1.10792767732962
goto-instrument-CORE	67.93	69.95	1.02973649344914
jbmc-CORE	179.93	196.51	1.09214694603457
strings-smoke-tests-CORE	68.95	69.65	1.01015228426396
strings-smoke-tests-symex-driven-lazy-loading-CORE	260.05	300.16	1.15423956931359
jbmc-symex-driven-lazy-loading-CORE	725.48	802.43	1.1060677068975
jbmc-strings-CORE	317.44	327.24	1.03087197580645
jbmc-strings-symex-driven-lazy-loading-CORE	950.72	1018.15	1.07092519353753
total	2053.73	2233.66	1.0876113218388

There is some time regression but the CI is suddenly takes >1800s to compile (before it was ~50s).

smowton · 2020-02-24T16:00:47Z

That's ccache.

xbauch · 2020-02-24T16:07:08Z

That's ccache.

Do you mean that it's ccache that's timing out or that the difference between build times is caused by ccache?

chrisr-diffblue · 2020-02-24T16:13:16Z

Difference in build times, I suspect. Because you've touched a few header files that are reasonably widely included, ccache is going to end up thinking it does actually need to rebuild a lot of things, rather than just pulling them from the cache.

chrisr-diffblue · 2020-02-24T16:22:37Z

Since the failing Travis job did actually get as far as saving it's ccache, there's a reasonably high (by Travis standards...) that simply re-running the failed job will make it pass.

xbauch · 2020-02-24T16:24:00Z

Since the failing Travis job did actually get as far as saving it's ccache, there's a reasonably high (by Travis standards...) that simply re-running the failed job will make it pass.

This was my 4th attempt.

chrisr-diffblue · 2020-02-24T16:25:45Z

:-s Well that sucks...

chrisr-diffblue · 2020-02-24T16:34:43Z

Looking a little deeper... the previous Travis run had two of the OSX configs timeout... one of those configs got as far as saving its cache, the other didnt. This most recent Travis run has only a single Travis failure - the config that previously timed out before saving it's cache - while the config that did manage to save it's cache has now passed. So I think it is worth one more attempt to re-run the Travis jobs since I think all the configs have now saved updated caches.

1: two new options to choose between fail by assert-then-assume and return null 2: `__CPROVER_max_malloc_size` is introduced 3: some tests for boundary conditions 4: user-level documentation

More assignments due to the `__CPROVER_malloc_max_size` and `__CPROVER_malloc_failure_mode` instantiations.

and test them to any number.

specifically the C90-style struct hack with non-flexible member.

xbauch · 2020-02-25T11:07:51Z

The changes in this PR cause ~7% slow down (the CORE test suite from 1560s to 1674s). It might be avoided if we figured out how to introduce #ifdefs in the library models based on user options. Any ideas @peterschrammel? Is it worth the trouble?

before we were extracting the value for the symbol to be used as array size, but the initialization to the extracted value is not guaranteed to happen before the initialization of the array. So we avoid extracting this value from the snapshot altogether.

chrisr-diffblue reviewed Jan 7, 2020

View reviewed changes

allredj reviewed Jan 7, 2020

View reviewed changes

chrisr-diffblue reviewed Jan 7, 2020

View reviewed changes

chrisr-diffblue approved these changes Jan 7, 2020

View reviewed changes

xbauch force-pushed the fix/malloc-size-too-large branch from b32032f to b73f968 Compare January 7, 2020 16:06

allredj reviewed Jan 7, 2020

View reviewed changes

xbauch marked this pull request as ready for review January 8, 2020 09:52

xbauch requested review from danpoe, martin-cs, peterschrammel, smowton and thk123 as code owners January 8, 2020 09:52

smowton approved these changes Jan 8, 2020

View reviewed changes

xbauch force-pushed the fix/malloc-size-too-large branch from b73f968 to 0c2c362 Compare January 8, 2020 10:08

allredj reviewed Jan 8, 2020

View reviewed changes

xbauch requested review from kroening and tautschnig as code owners January 15, 2020 13:17

xbauch force-pushed the fix/malloc-size-too-large branch from 9c704e8 to c7a0d53 Compare January 17, 2020 12:55

xbauch force-pushed the fix/malloc-size-too-large branch 5 times, most recently from cce4e8e to b31422a Compare January 24, 2020 14:35

xbauch force-pushed the fix/malloc-size-too-large branch 2 times, most recently from e517347 to 277f2d0 Compare February 24, 2020 13:29

xbauch force-pushed the fix/malloc-size-too-large branch from 277f2d0 to b7bfd6b Compare February 24, 2020 16:37

petr-bauch added 4 commits February 25, 2020 09:40

Malloc should fail on too large allocations

531b856

1: two new options to choose between fail by assert-then-assume and return null 2: `__CPROVER_max_malloc_size` is introduced 3: some tests for boundary conditions 4: user-level documentation

Update the constant propagation tests

2ad3503

More assignments due to the `__CPROVER_malloc_max_size` and `__CPROVER_malloc_failure_mode` instantiations.

Update the expected number of assertions

de0bc8b

and test them to any number.

Remove undefined behaviour from pointer-byte-extract5

14682de

specifically the C90-style struct hack with non-flexible member.

xbauch force-pushed the fix/malloc-size-too-large branch from b7bfd6b to 6fa1464 Compare February 25, 2020 09:42

xbauch added the do not merge label Feb 25, 2020

xbauch force-pushed the fix/malloc-size-too-large branch from 5a38ecf to 6fa1464 Compare February 25, 2020 12:50

Snapshot harness test fix

195da86

before we were extracting the value for the symbol to be used as array size, but the initialization to the extracted value is not guaranteed to happen before the initialization of the array. So we avoid extracting this value from the snapshot altogether.

xbauch force-pushed the fix/malloc-size-too-large branch from 6fa1464 to 195da86 Compare February 25, 2020 12:51

xbauch removed the do not merge label Feb 25, 2020

xbauch force-pushed the fix/malloc-size-too-large branch from e73e6aa to 195da86 Compare February 27, 2020 11:04

xbauch merged commit cd2c65b into diffblue:develop Feb 27, 2020

xbauch mentioned this pull request Feb 27, 2020

CBMC malloc should fail if called for a size CBMC cannot represent #4604

Closed

karkhaz mentioned this pull request Mar 16, 2020

goto-cc isn't aware of cbmc's --object-bits setting #5272

Closed

martin-cs mentioned this pull request May 28, 2020

Update/cbmc submodule may 2020 diffblue/gnat2goto#350

Merged

martin-cs mentioned this pull request Jul 1, 2020

Rework memory allocation failure checks and options #5401

Open

5 tasks

tautschnig mentioned this pull request Nov 13, 2020

Synchronise goto-cc command-line options to re-enable Windows regression tests #5572

Closed

3 tasks

SaswatPadhi mentioned this pull request May 19, 2021

Spurious malloc behavior for large allocations #6130

Closed

Malloc should fail on too large allocations #5210

Malloc should fail on too large allocations #5210

Uh oh!

Conversation

xbauch commented Jan 6, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

xbauch commented Jan 6, 2020

Uh oh!

xbauch commented Jan 6, 2020

Uh oh!

chrisr-diffblue Jan 7, 2020

Choose a reason for hiding this comment

Uh oh!

xbauch Jan 7, 2020

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue Jan 7, 2020

Choose a reason for hiding this comment

Uh oh!

xbauch Jan 7, 2020

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

chrisr-diffblue Jan 7, 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!

chrisr-diffblue Jan 7, 2020

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue 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 Jan 8, 2020

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Jan 13, 2020 via email

Uh oh!

danielsn commented Jan 23, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

xbauch commented Feb 24, 2020

Uh oh!

smowton commented Feb 24, 2020

Uh oh!

xbauch commented Feb 24, 2020

Uh oh!

chrisr-diffblue commented Feb 24, 2020

Uh oh!

chrisr-diffblue commented Feb 24, 2020

Uh oh!

xbauch commented Feb 24, 2020

Uh oh!

chrisr-diffblue commented Feb 24, 2020

Uh oh!

chrisr-diffblue commented Feb 24, 2020

Uh oh!

xbauch commented Feb 25, 2020

Uh oh!

Uh oh!

xbauch commented Jan 6, 2020 •

edited

Loading

codecov-io commented Jan 7, 2020 •

edited

Loading

chrisr-diffblue Jan 7, 2020 •

edited

Loading

danielsn commented Jan 23, 2020 •

edited

Loading