Skip to content

Fix max malloc size #5298

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Apr 23, 2020
+85 −2
Merged

Fix max malloc size #5298

Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
3f86b3e
Fix overflow error for objects whose offset is >32
Apr 16, 2020
48497ff
Add unit test for checking the max malloc size
Apr 16, 2020
5a2e85e
Also check for pointers whose width is too small
Apr 16, 2020
4fe6842
Clarify the calculation for working out the max allocation size
Apr 17, 2020
12d94f1
Allow offset of a single bit
Apr 17, 2020
448ff24
Use mp_integer for calculation
Apr 22, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 22 additions & 2 deletions src/ansi-c/ansi_c_internal_additions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@ Author: Daniel Kroening, [email protected]

#include "ansi_c_internal_additions.h"

#include <limits>

#include <util/c_types.h>
#include <util/config.h>

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

using max_alloc_sizet = uint64_t;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes this makes sense!

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

/// The maximum allocation size is determined by the number of bits that
/// are left in the pointer of width \p pointer_width after allowing for the
/// signed bit, and the bits used for the objects ID (determined by
/// \p object_bits).
/// \param pointer_width: The width of the pointer
/// \param object_bits : The number of bits used to represent the ID
/// \return The size in bytes of the maximum allocation supported.
static max_alloc_sizet
max_malloc_size(std::size_t pointer_width, std::size_t object_bits)
{
PRECONDITION(object_bits < pointer_width - 1);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

PRECONDITION(object_bits >= 1);
const auto bits_for_offset = pointer_width - object_bits - 1;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

PRECONDITION(bits_for_offset < std::numeric_limits<max_alloc_sizet>::digits);
return ((max_alloc_sizet)1) << (max_alloc_sizet)bits_for_offset;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think casting bits_for_offset would be unnecessary.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

}

void ansi_c_internal_additions(std::string &code)
{
// clang-format off
Expand Down Expand Up @@ -162,8 +182,8 @@ void ansi_c_internal_additions(std::string &code)
"int " CPROVER_PREFIX "malloc_failure_mode_assert_then_assume="+
std::to_string(config.ansi_c.malloc_failure_mode_assert_then_assume)+";\n"
CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+
std::to_string(1 << (config.ansi_c.pointer_width -
config.bv_encoding.object_bits - 1))+";\n"
std::to_string(max_malloc_size(config.ansi_c.pointer_width, config
.bv_encoding.object_bits))+";\n"

// this is ANSI-C
"extern " CPROVER_PREFIX "thread_local const char __func__["
Expand Down