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())
     {