Re-implement inside stdlib.c

will be squashed.

Note: this also introduces some new overflow checks. Also the pre-structhack in
test `cbmc/Pointer_byte_extract5` no longer works with `--no-simplify`. But as
the issue #5213 shows, CBMC has a much bigger problem with that. So we propose
the rewrite the test to use the standard, flexible-array, approach.

Author: petr-bauch

regression/cbmc/Pointer_byte_extract5/main.i

@@ -11,13 +11,13 @@ typedef union
 typedef struct
 {
   int Count;
-  Union List[1];
+  Union List[0];
 } Struct3;
 #pragma pack(pop)
 
 int main()
 {
-  Struct3 *p = malloc(sizeof(Struct3) + sizeof(Union));
+  Struct3 *p = malloc(sizeof(Struct3) + 2 * sizeof(Union));
   p->Count = 3;
   int po=0;
 

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -4,7 +4,7 @@ main.i
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE
-\*\* 1 of 11 failed 
+\*\* 1 of 12 failed
 --
 ^warning: ignoring
 --

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

@@ -8,6 +8,7 @@ int main()
   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
+  assert(p);
 
   return 0;
 }

regression/cbmc/malloc-too-large/largest_representable.desc

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

regression/cbmc/malloc-too-large/max_size.desc

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

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

@@ -9,6 +9,7 @@ int main()
   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);
+  assert(p);
 
   return 0;
 }

regression/cbmc/malloc-too-large/one_byte_too_large.desc

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

regression/cbmc/pointer-overflow1/test.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : SUCCESS
 ^VERIFICATION FAILED$
-^\*\* 8 of 11 failed
+^\*\* 8 of 12 failed
 --
 ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
 ^warning: ignoring

regression/cbmc/r_w_ok1/main.c

@@ -16,6 +16,13 @@ int main()
   assert(__CPROVER_w_ok(p, sizeof(int)));
 
   size_t n;
+
+  // n is arbitrary but no larger than what CBMC can represent
+  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;
+  __CPROVER_assume(n<=cbmc_max_alloc_size);
+
   char *arbitrary_size = malloc(n);
 
   assert(__CPROVER_r_ok(arbitrary_size, n));

src/analyses/goto_check.cpp

@@ -72,7 +72,6 @@ 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;
@@ -239,7 +238,6 @@ 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;
@@ -1943,30 +1941,6 @@ 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_id_width)",
-            "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,8 +38,7 @@ 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)"                  \
-  "(malloc-size-check)"
+  "(float-overflow-check)(nan-check)(no-built-in-assertions)"
 
 // clang-format off
 #define HELP_GOTO_CHECK \
@@ -56,7 +55,6 @@ 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) \
@@ -72,7 +70,6 @@ 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("malloc-size-check", cmdline.isset("malloc-size-check"))
+  options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */
 
 #endif // CPROVER_ANALYSES_GOTO_CHECK_H

src/ansi-c/CMakeLists.txt

@@ -13,7 +13,7 @@ endforeach()
 
 add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
     COMMAND converter < ${converter_input_path} > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
-    DEPENDS converter
+    DEPENDS converter ${converter_input_path}
 )
 
 add_executable(file_converter file_converter.cpp)

src/ansi-c/ansi_c_internal_additions.cpp

@@ -155,6 +155,10 @@ void ansi_c_internal_additions(std::string &code)
     "void *" CPROVER_PREFIX "allocate("
       CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
     "const void *" CPROVER_PREFIX "alloca_object = 0;\n"
+    CPROVER_PREFIX "size_t " CPROVER_PREFIX "pointer_width="+
+      std::to_string(config.ansi_c.pointer_width)+";\n"
+    CPROVER_PREFIX "size_t " CPROVER_PREFIX "object_bits="+
+      std::to_string(config.bv_encoding.object_bits)+";\n"
 
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["

src/ansi-c/library/cprover.h

@@ -16,6 +16,8 @@ extern const void *__CPROVER_malloc_object;
 extern __CPROVER_size_t __CPROVER_malloc_size;
 extern _Bool __CPROVER_malloc_is_new_array;
 extern const void *__CPROVER_memory_leak;
+extern __CPROVER_size_t __CPROVER_pointer_width;
+extern __CPROVER_size_t __CPROVER_object_bits;
 
 void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);

src/ansi-c/library/stdlib.c

@@ -115,6 +115,12 @@ inline void *malloc(__CPROVER_size_t malloc_size)
   // realistically, malloc may return NULL,
   // and __CPROVER_allocate doesn't, but no one cares
   __CPROVER_HIDE:;
+
+  if(
+    malloc_size >= ((__CPROVER_size_t)1
+                    << (__CPROVER_pointer_width - __CPROVER_object_bits)))
+    return (void *)0;
+
   void *malloc_res;
   malloc_res = __CPROVER_allocate(malloc_size, 0);