Fix max malloc size #5298

thk123 · 2020-04-16T14:03:03Z

Previously, to work out the max allocation size, we we working out how many bits there were for the offset (pointer_width - object_bits - 1) and then raising 2 to that power. However, we were doing this with int literals, and so the calculation was done in 32bits.

Therefore, for the default object bits (8) gives you:

1 << (64 - 8 - 1)

Which depends on your compiler / OS might give you zero, or 8388608 (since overflow on signed integral types is undefined behavior, both are valid). The correct number is 36028797018963968

This PR changes to use a 64 bit type on all platforms, and invariant if the result is not going to fit.

Also adds unit tests showing this, and documentation explaining the calculations.

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).
[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.

danpoe · 2020-04-16T14:20:13Z

src/ansi-c/ansi_c_internal_additions.cpp

+max_malloc_size(std::size_t pointer_width, std::size_t object_bits)
+{
+  PRECONDITION(pointer_width >= 1);
+  PRECONDITION(object_bits < pointer_width - 1);


I think this should be object_bits < pointer_width. Just one bit for the offset would still be ok.

I think not: you need one bit for the sign?
Pointer width = 8
Object bits = 7
1-1 = 0 bits for the offset?

Just saw second comment - OK I misunderstood what you said - I thought the signed bit was used for something else, rather than the offset?

The offset is signed. So with just one bit, 0 (in binary) would be 0 (in decimal), and 1 (in binary) would be -1 (in decimal).

danpoe · 2020-04-16T14:22:30Z

src/ansi-c/ansi_c_internal_additions.cpp

+  PRECONDITION(pointer_width >= 1);
+  PRECONDITION(object_bits < pointer_width - 1);
+  PRECONDITION(object_bits >= 1);
+  const auto bits_for_offset = pointer_width - object_bits - 1;


The naming is not quite right as the bits for the offset is pointer_width - object_bits. The offset is signed and the sign bit is considered to be part of the offset.

danpoe · 2020-04-16T14:24:40Z

src/ansi-c/ansi_c_internal_additions.cpp

@@ -120,6 +122,25 @@ static std::string architecture_string(T value, const char *s)
         std::string(s) + "=" + std::to_string(value) + ";\n";
 }

+using max_alloc_sizet = uint64_t;


Shouldn't this be size_t? That's the type with which __CPROVER_max_malloc_size is declared.

Yes this makes sense!

Though the advantage of using a platform agnostic width is writing the unit tests is easier

@danpoe The problem is that cbmcs size_t that we analyze with isn't necessarily the same as that which we get when compiling cbmc itself.

As pointed out by @thk123 in private communication, when using size_t instead of uint64_t, the computation would overflow when running on a 32-bit machine and using e.g. --LLP64.

Could we please use mp_integer here instead of any architecturally limited type? We do not want to run into limitations of the host or compiler with this computation.

danpoe · 2020-04-16T14:27:32Z

src/ansi-c/ansi_c_internal_additions.cpp

+  PRECONDITION(object_bits >= 1);
+  const auto bits_for_offset = pointer_width - object_bits - 1;
+  PRECONDITION(bits_for_offset < std::numeric_limits<max_alloc_sizet>::digits);
+  return ((max_alloc_sizet)1) << (max_alloc_sizet)bits_for_offset;


I think casting bits_for_offset would be unnecessary.

I'd prefer to be explicit here, since the specific rules of what type gets promoted are fiddly.

size_t issue

danpoe · 2020-04-20T10:40:37Z

src/ansi-c/ansi_c_internal_additions.cpp

+/// are left in the pointer of width \p pointer_width.
+///
+/// The offset needs to be able to represent up to the allocation_size, and
+/// down to -allocation_size, hence 2^(pointer_width - object_bits - 1)


I think the description has it backwards. The allocation size is a result of how we represent the offset, and not the other way round.

In my head - they are simply intertwined via the following relationship

max_alloc_size = 2^(bits_for_offset - 1)

That said I didn't like how the function returns max_alloc_size, but the description implies you input the max allocation size. I just found this a clearer way to think about the relationship - I'll have another go.

Yes that makes sense. The current description looks good to me. My reasoning for why I preferred offset -> allocation size was that this is the direction of the computation in the method.

danpoe · 2020-04-20T10:42:51Z

src/ansi-c/ansi_c_internal_additions.cpp

+  PRECONDITION(object_bits >= 1);
+  const auto offset_bits = pointer_width - object_bits;
+  // We require the offset to be able to express upto allocation_size - 1,
+  // but also down to -allocation_size + 1, therefore the size is allowable


Should this be just -allocation_size? Since we can represent one more negative value than positive values.

Yes you're right - a pointer to the end of the memory would be valid, and you'd need to subtract the full allocation size to get back to the start.

Pulled out into a fnuction and assert that the max allocation size does not exceed 64 bits. Do not attempt to do the left shift in a 32 bit int, instead cast to 64 bits before doing the shift.

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

@danpoe I've made the suggestde changes: https://github.com/diffblue/cbmc/compare/566b57ce6f60f8c5d80499e9113bb1dc8473a470..8789d7eb42391db0e8a1e4a645256320b93cb5e4#diff-1975841ce4287c4605974098716678fc

tautschnig

Thank you for fixing the overflow bug, but as said in my comment I believe that the arithmetic should be done on mp_integer.

tautschnig · 2020-04-22T13:46:08Z

src/ansi-c/ansi_c_internal_additions.cpp

@@ -120,6 +122,25 @@ static std::string architecture_string(T value, const char *s)
         std::string(s) + "=" + std::to_string(value) + ";\n";
 }

+using max_alloc_sizet = uint64_t;


Could we please use mp_integer here instead of any architecturally limited type? We do not want to run into limitations of the host or compiler with this computation.

tautschnig · 2020-04-22T13:46:59Z

unit/ansi-c/max_malloc_size.cpp

+\*******************************************************************/
+
+#include <ansi-c/ansi_c_internal_additions.cpp>
+#include <iostream>


Is this include actually needed?

Ensure that invalid numbers of bits for object id throws, as well as any overflow if the max allocation size is too big.

This ensures the other preconditions don't pass spuriously with a zero width pointer

This is valid - the offset can be 0 for a pointer pointing at the start of a single byte allocation.

This removes the possibility for the calculation itself to overflow

thk123 · 2020-04-22T17:41:04Z

@tautschnig done (which of course removes the possibility of any overflow). Will merge when passes CI / tomorrow

unit/ansi-c/max_malloc_size.cpp

thk123 requested review from peterschrammel and danpoe April 16, 2020 14:03

thk123 requested review from chrisr-diffblue, kroening and tautschnig as code owners April 16, 2020 14:03

thk123 force-pushed the fix-max-alloc-size branch 3 times, most recently from 68adf73 to 86e4944 Compare April 16, 2020 14:13

thk123 changed the title ~~Fix max alloc size~~ Fix max malloc size Apr 16, 2020

thk123 force-pushed the fix-max-alloc-size branch from 86e4944 to 9a4c18e Compare April 16, 2020 14:15

danpoe reviewed Apr 16, 2020

View reviewed changes

thk123 force-pushed the fix-max-alloc-size branch from bfc4e00 to 566b57c Compare April 17, 2020 17:39

danpoe previously approved these changes Apr 20, 2020

View reviewed changes

danpoe reviewed Apr 20, 2020

View reviewed changes

Fix overflow error for objects whose offset is >32

3f86b3e

Pulled out into a fnuction and assert that the max allocation size does not exceed 64 bits. Do not attempt to do the left shift in a 32 bit int, instead cast to 64 bits before doing the shift.

thk123 force-pushed the fix-max-alloc-size branch 2 times, most recently from 8789d7e to 9438b49 Compare April 22, 2020 09:48

danpoe approved these changes Apr 22, 2020

View reviewed changes

tautschnig approved these changes Apr 22, 2020

View reviewed changes

Thomas Kiley added 5 commits April 22, 2020 18:39

Add unit test for checking the max malloc size

48497ff

Ensure that invalid numbers of bits for object id throws, as well as any overflow if the max allocation size is too big.

Also check for pointers whose width is too small

5a2e85e

This ensures the other preconditions don't pass spuriously with a zero width pointer

Clarify the calculation for working out the max allocation size

4fe6842

Allow offset of a single bit

12d94f1

This is valid - the offset can be 0 for a pointer pointing at the start of a single byte allocation.

Use mp_integer for calculation

448ff24

This removes the possibility for the calculation itself to overflow

thk123 force-pushed the fix-max-alloc-size branch from 9438b49 to 448ff24 Compare April 22, 2020 17:39

tautschnig merged commit 51b5618 into diffblue:develop Apr 23, 2020

thk123 deleted the fix-max-alloc-size branch April 23, 2020 09:11

thk123 commented Apr 23, 2020

View reviewed changes

unit/ansi-c/max_malloc_size.cpp Show resolved Hide resolved

thk123 mentioned this pull request Apr 23, 2020

Remove empty section from unit test #5317

Merged

Fix max malloc size #5298

Fix max malloc size #5298

Uh oh!

Conversation

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

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!

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!

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!

thk123 commented Apr 22, 2020

Uh oh!

tautschnig 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!

thk123 commented Apr 22, 2020

Uh oh!

Uh oh!

Uh oh!

thk123 commented Apr 16, 2020 •

edited

Loading