Fix max malloc size

src/ansi-c/ansi_c_internal_additions.cpp

@@ -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>
 
@@ -120,6 +122,34 @@ static std::string architecture_string(T value, const char *s)
          std::string(s) + "=" + std::to_string(value) + ";\n";
 }
 
+/// The maximum allocation size is determined by the number of bits that
+/// 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.
+static mp_integer
+max_malloc_size(std::size_t pointer_width, std::size_t object_bits)
+{
+  PRECONDITION(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,
+  // 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;
+  return ((mp_integer)1) << (mp_integer)bits_for_positive_offset;
+}
+
 void ansi_c_internal_additions(std::string &code)
 {
   // clang-format off
@@ -162,8 +192,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"
+      integer2string(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__["

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 \

unit/ansi-c/max_malloc_size.cpp

@@ -0,0 +1,50 @@
+/*******************************************************************\
+
+Module: Unit test for max_malloc_size
+
+Author: Thomas Kiley
+
+\*******************************************************************/
+
+#include <ansi-c/ansi_c_internal_additions.cpp>
+#include <testing-utils/use_catch.h>
+
+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, 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("Not enough bits in the pointer")
+  {
+    REQUIRE_THROWS_AS(max_malloc_size(0, 0), invariant_failedt);
+  }
+
+  SECTION("Max allocation size overflow")
+  {
+  }
+
+  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*/);
+    REQUIRE(
+      max_malloc_size(128, 63) == string2integer("18446744073709551616"
+                                                 /*2^64*/));
+  }
+}

unit/ansi-c/module_dependencies.txt

@@ -0,0 +1,2 @@
+testing-utils
+ansi-c