Malloc should fail on too large allocations

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

Author: petr-bauch

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

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  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)) - 1;
+  int *p = malloc(cbmc_max_alloc_size); // try to allocate exactly the max
+
+  return 0;
+}

regression/cbmc/malloc-too-large-almost/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--malloc-size-check
+^EXIT=0$
+^SIGNAL=0$
+^\[malloc.max_allocation_check.\d+\] line \d+ malloc_size < 2 \^ \(pointer_width - object_size\) in ALLOCATE\(malloc_size, 0 != 0\): SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  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)) - 1;
+  // try to allocate the smallest violating amount
+  int *p = malloc(cbmc_max_alloc_size + 1);
+
+  return 0;
+}

regression/cbmc/malloc-too-large-just-about/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--malloc-size-check
+^EXIT=10$
+^SIGNAL=0$
+^\[malloc.max_allocation_check.\d+\] line \d+ malloc_size < 2 \^ \(pointer_width - object_size\) in ALLOCATE\(malloc_size, 0 != 0\): FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

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

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *p = malloc(SIZE_MAX);
+  assert(p);
+
+  return 0;
+}

regression/cbmc/malloc-too-large-max-size/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--malloc-size-check
+^EXIT=10$
+^SIGNAL=0$
+^\[malloc.max_allocation_check.\d+\] line \d+ malloc_size < 2 \^ \(pointer_width - object_size\) in ALLOCATE\(malloc_size, 0 != 0\): FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

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

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *p = malloc(SIZE_MAX);
+  assert(p);
+
+  return 0;
+}

src/analyses/goto_check.cpp

@@ -72,6 +72,7 @@ class goto_checkt
     enable_built_in_assertions=_options.get_bool_option("built-in-assertions");
     enable_assumptions=_options.get_bool_option("assumptions");
     error_labels=_options.get_list_option("error-label");
+    enable_malloc_size_check = _options.get_bool_option("malloc-size-check");
   }
 
   typedef goto_functionst::goto_functiont goto_functiont;
@@ -238,6 +239,7 @@ class goto_checkt
   bool enable_assertions;
   bool enable_built_in_assertions;
   bool enable_assumptions;
+  bool enable_malloc_size_check;
 
   typedef optionst::value_listt error_labelst;
   error_labelst error_labels;
@@ -1941,6 +1943,30 @@ void goto_checkt::goto_check(
         if(rw_ok_cond.has_value())
           rhs = *rw_ok_cond;
       }
+
+      if(enable_malloc_size_check && code_assign.rhs().id() == ID_side_effect)
+      {
+        const auto &rhs_side_effect = to_side_effect_expr(code_assign.rhs());
+        if(rhs_side_effect.get_statement() == ID_allocate)
+        {
+          const auto &alloc_size_type = rhs_side_effect.op0().type();
+          const auto pointer_bits =
+            from_integer(config.ansi_c.pointer_width, alloc_size_type);
+          const auto object_bits =
+            from_integer(config.bv_encoding.object_bits, alloc_size_type);
+          const auto max_alloc_size =
+            binary_exprt{from_integer(2, alloc_size_type),
+                         ID_power,
+                         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)",
+            "max allocation check",
+            i.code.source_location(),
+            code_assign.rhs(),
+            guardt{true_exprt{}, guard_manager});
+        }
+      }
     }
     else if(i.is_function_call())
     {

src/analyses/goto_check.h

@@ -38,7 +38,8 @@ void goto_check(
   "(div-by-zero-check)(enum-range-check)(signed-overflow-check)(unsigned-"     \
   "overflow-check)"                                                            \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
-  "(float-overflow-check)(nan-check)(no-built-in-assertions)"
+  "(float-overflow-check)(nan-check)(no-built-in-assertions)"                  \
+  "(malloc-size-check)"
 
 // clang-format off
 #define HELP_GOTO_CHECK \
@@ -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-size-check           check that CBMC can represent the allocated object of requested size" /* NOLINT(whitespace/line_length) */ \
 // clang-format on
 
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
@@ -70,6 +72,7 @@ void goto_check(
   options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("nan-check", cmdline.isset("nan-check")); \
-  options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")) /* NOLINT(whitespace/line_length) */
+  options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("malloc-size-check", cmdline.isset("malloc-size-check"))
 
 #endif // CPROVER_ANALYSES_GOTO_CHECK_H