From 3f86b3e820579e8bf76774d258cd1f771f1baad6 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 16 Apr 2020 14:51:56 +0100 Subject: [PATCH 1/6] Fix overflow error for objects whose offset is >32 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. --- src/ansi-c/ansi_c_internal_additions.cpp | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 5be02100d99..c6fe3b6fc21 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_internal_additions.h" +#include + #include #include @@ -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; +/// 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); + PRECONDITION(object_bits >= 1); + const auto bits_for_offset = pointer_width - object_bits - 1; + PRECONDITION(bits_for_offset < std::numeric_limits::digits); + return ((max_alloc_sizet)1) << (max_alloc_sizet)bits_for_offset; +} + void ansi_c_internal_additions(std::string &code) { // clang-format off @@ -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__[" From 48497ff0493a6797f6bbd17c35de3282abda4e3c Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 16 Apr 2020 14:53:17 +0100 Subject: [PATCH 2/6] Add unit test for checking the max malloc size Ensure that invalid numbers of bits for object id throws, as well as any overflow if the max allocation size is too big. --- unit/Makefile | 1 + unit/ansi-c/max_malloc_size.cpp | 41 +++++++++++++++++++++++++++++ unit/ansi-c/module_dependencies.txt | 2 ++ 3 files changed, 44 insertions(+) create mode 100644 unit/ansi-c/max_malloc_size.cpp create mode 100644 unit/ansi-c/module_dependencies.txt diff --git a/unit/Makefile b/unit/Makefile index 5974c05e6b6..5ba0727175f 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -14,6 +14,7 @@ SRC += analyses/ai/ai.cpp \ analyses/does_remove_const/does_expr_lose_const.cpp \ analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ + ansi-c/max_malloc_size.cpp \ big-int/big-int.cpp \ compound_block_locations.cpp \ get_goto_model_from_c_test.cpp \ diff --git a/unit/ansi-c/max_malloc_size.cpp b/unit/ansi-c/max_malloc_size.cpp new file mode 100644 index 00000000000..72f1bf3ce2d --- /dev/null +++ b/unit/ansi-c/max_malloc_size.cpp @@ -0,0 +1,41 @@ +/*******************************************************************\ + +Module: Unit test for max_malloc_size + +Author: Thomas Kiley + +\*******************************************************************/ + +#include +#include + +TEST_CASE( + "max_malloc_size", + "[core][ansi-c][ansi_c_internal_additions][max_malloc_size]") +{ + cbmc_invariants_should_throwt throw_invariants; + + SECTION("Too many bits for pointer ID") + { + REQUIRE_THROWS_AS(max_malloc_size(4, 3), invariant_failedt); + REQUIRE_THROWS_AS(max_malloc_size(4, 4), invariant_failedt); + REQUIRE_THROWS_AS(max_malloc_size(4, 5), invariant_failedt); + } + + SECTION("Not enough bits for pointer ID") + { + REQUIRE_THROWS_AS(max_malloc_size(4, 0), invariant_failedt); + } + + SECTION("Max allocation size overflow") + { + REQUIRE_THROWS_AS(max_malloc_size(128, 63), invariant_failedt); + } + + SECTION("Valid allocation size configurations") + { + // Here we use 4 bits for the object ID, leaving 3 for the offset + REQUIRE(max_malloc_size(8, 4) == 8); + REQUIRE(max_malloc_size(128, 64) == 9223372036854775808ull /*2^63*/); + } +} diff --git a/unit/ansi-c/module_dependencies.txt b/unit/ansi-c/module_dependencies.txt new file mode 100644 index 00000000000..2a77c3a0403 --- /dev/null +++ b/unit/ansi-c/module_dependencies.txt @@ -0,0 +1,2 @@ +testing-utils +ansi-c From 5a2e85e134977afabb3423810c6a2d54ef85b762 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 16 Apr 2020 15:12:46 +0100 Subject: [PATCH 3/6] Also check for pointers whose width is too small This ensures the other preconditions don't pass spuriously with a zero width pointer --- src/ansi-c/ansi_c_internal_additions.cpp | 1 + unit/ansi-c/max_malloc_size.cpp | 5 +++++ 2 files changed, 6 insertions(+) diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index c6fe3b6fc21..a0af7f6fade 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -133,6 +133,7 @@ using max_alloc_sizet = uint64_t; static max_alloc_sizet max_malloc_size(std::size_t pointer_width, std::size_t object_bits) { + PRECONDITION(pointer_width >= 1); PRECONDITION(object_bits < pointer_width - 1); PRECONDITION(object_bits >= 1); const auto bits_for_offset = pointer_width - object_bits - 1; diff --git a/unit/ansi-c/max_malloc_size.cpp b/unit/ansi-c/max_malloc_size.cpp index 72f1bf3ce2d..ff0c7a99531 100644 --- a/unit/ansi-c/max_malloc_size.cpp +++ b/unit/ansi-c/max_malloc_size.cpp @@ -27,6 +27,11 @@ TEST_CASE( REQUIRE_THROWS_AS(max_malloc_size(4, 0), invariant_failedt); } + SECTION("Not enough bits in the pointer") + { + REQUIRE_THROWS_AS(max_malloc_size(0, 0), invariant_failedt); + } + SECTION("Max allocation size overflow") { REQUIRE_THROWS_AS(max_malloc_size(128, 63), invariant_failedt); From 4fe6842b087eb9d81ab7f4dac079e03be8ff4f37 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 17 Apr 2020 17:40:44 +0100 Subject: [PATCH 4/6] Clarify the calculation for working out the max allocation size --- src/ansi-c/ansi_c_internal_additions.cpp | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index a0af7f6fade..f00b5d4feea 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -124,9 +124,16 @@ static std::string architecture_string(T value, const char *s) using max_alloc_sizet = uint64_t; /// 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). +/// are left in the pointer of width \p pointer_width. +/// +/// The allocation size cannot exceed the number represented by the (signed) +/// offset, otherwise it would not be possible to store a pointer into a +/// valid bit of memory. Therefore, the max allocation size is +/// 2^(offset_bits - 1), where the offset bits is the number of bits left in the +/// pointer after the object bits. +/// +/// The offset must be signed, as a pointer can point to the end of the memory +/// block, and needs to be able to point back to the start. /// \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. @@ -136,9 +143,14 @@ max_malloc_size(std::size_t pointer_width, std::size_t object_bits) PRECONDITION(pointer_width >= 1); PRECONDITION(object_bits < pointer_width - 1); PRECONDITION(object_bits >= 1); - const auto bits_for_offset = pointer_width - object_bits - 1; - PRECONDITION(bits_for_offset < std::numeric_limits::digits); - return ((max_alloc_sizet)1) << (max_alloc_sizet)bits_for_offset; + 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, therefore the size is allowable + // is number of bits, less the signed bit. + const auto bits_for_positive_offset = offset_bits - 1; + PRECONDITION( + bits_for_positive_offset < std::numeric_limits::digits); + return ((max_alloc_sizet)1) << (max_alloc_sizet)bits_for_positive_offset; } void ansi_c_internal_additions(std::string &code) From 12d94f1b4d4c69b1018e0895dce6df8d6b41cbd9 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 17 Apr 2020 17:58:52 +0100 Subject: [PATCH 5/6] Allow offset of a single bit This is valid - the offset can be 0 for a pointer pointing at the start of a single byte allocation. --- src/ansi-c/ansi_c_internal_additions.cpp | 2 +- unit/ansi-c/max_malloc_size.cpp | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index f00b5d4feea..881f36a2b62 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -141,7 +141,7 @@ static max_alloc_sizet max_malloc_size(std::size_t pointer_width, std::size_t object_bits) { PRECONDITION(pointer_width >= 1); - PRECONDITION(object_bits < pointer_width - 1); + PRECONDITION(object_bits < pointer_width); 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, diff --git a/unit/ansi-c/max_malloc_size.cpp b/unit/ansi-c/max_malloc_size.cpp index ff0c7a99531..785c4f6a02a 100644 --- a/unit/ansi-c/max_malloc_size.cpp +++ b/unit/ansi-c/max_malloc_size.cpp @@ -17,7 +17,6 @@ TEST_CASE( SECTION("Too many bits for pointer ID") { - REQUIRE_THROWS_AS(max_malloc_size(4, 3), invariant_failedt); REQUIRE_THROWS_AS(max_malloc_size(4, 4), invariant_failedt); REQUIRE_THROWS_AS(max_malloc_size(4, 5), invariant_failedt); } @@ -39,6 +38,9 @@ TEST_CASE( SECTION("Valid allocation size configurations") { + // The one bit offset can be used to store 0, or -1, so we can allocate + // a single bit + REQUIRE(max_malloc_size(4, 3) == 1); // Here we use 4 bits for the object ID, leaving 3 for the offset REQUIRE(max_malloc_size(8, 4) == 8); REQUIRE(max_malloc_size(128, 64) == 9223372036854775808ull /*2^63*/); From 448ff241254524a209e8b7d4ebb4fb5906d95131 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Wed, 22 Apr 2020 18:39:15 +0100 Subject: [PATCH 6/6] Use mp_integer for calculation This removes the possibility for the calculation itself to overflow --- src/ansi-c/ansi_c_internal_additions.cpp | 9 +++------ unit/ansi-c/max_malloc_size.cpp | 4 +++- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 881f36a2b62..68486e49a23 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -122,7 +122,6 @@ static std::string architecture_string(T value, const char *s) std::string(s) + "=" + std::to_string(value) + ";\n"; } -using max_alloc_sizet = uint64_t; /// The maximum allocation size is determined by the number of bits that /// are left in the pointer of width \p pointer_width. /// @@ -137,7 +136,7 @@ using max_alloc_sizet = uint64_t; /// \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 +static mp_integer max_malloc_size(std::size_t pointer_width, std::size_t object_bits) { PRECONDITION(pointer_width >= 1); @@ -148,9 +147,7 @@ max_malloc_size(std::size_t pointer_width, std::size_t object_bits) // but also down to -allocation_size, therefore the size is allowable // is number of bits, less the signed bit. const auto bits_for_positive_offset = offset_bits - 1; - PRECONDITION( - bits_for_positive_offset < std::numeric_limits::digits); - return ((max_alloc_sizet)1) << (max_alloc_sizet)bits_for_positive_offset; + return ((mp_integer)1) << (mp_integer)bits_for_positive_offset; } void ansi_c_internal_additions(std::string &code) @@ -195,7 +192,7 @@ 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(max_malloc_size(config.ansi_c.pointer_width, config + integer2string(max_malloc_size(config.ansi_c.pointer_width, config .bv_encoding.object_bits))+";\n" // this is ANSI-C diff --git a/unit/ansi-c/max_malloc_size.cpp b/unit/ansi-c/max_malloc_size.cpp index 785c4f6a02a..acbb7c30218 100644 --- a/unit/ansi-c/max_malloc_size.cpp +++ b/unit/ansi-c/max_malloc_size.cpp @@ -33,7 +33,6 @@ TEST_CASE( SECTION("Max allocation size overflow") { - REQUIRE_THROWS_AS(max_malloc_size(128, 63), invariant_failedt); } SECTION("Valid allocation size configurations") @@ -44,5 +43,8 @@ TEST_CASE( // Here we use 4 bits for the object ID, leaving 3 for the offset REQUIRE(max_malloc_size(8, 4) == 8); REQUIRE(max_malloc_size(128, 64) == 9223372036854775808ull /*2^63*/); + REQUIRE( + max_malloc_size(128, 63) == string2integer("18446744073709551616" + /*2^64*/)); } }