Reimplement 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/test.desc

@@ -1,9 +1,9 @@
 CORE
 main.c
-
+--malloc-max-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$
+^\[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

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_max_check = _options.get_bool_option("malloc-max-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_max_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_max_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-max-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-max-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-max-check", cmdline.isset("malloc-max-check"))
 
 #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 ${converter_input_path}
+    DEPENDS converter
 )
 
 add_executable(file_converter file_converter.cpp)

src/ansi-c/library/stdlib.c

@@ -115,9 +115,6 @@ inline void *malloc(__CPROVER_size_t malloc_size)
   // realistically, malloc may return NULL,
   // and __CPROVER_allocate doesn't, but no one cares
   __CPROVER_HIDE:;
-  // 8 is the default object bits for ANSI-C and C++
-  if (malloc_size >= ((__CPROVER_size_t)1<<(64-8)))
-    return (void*)0;
   void *malloc_res;
   malloc_res = __CPROVER_allocate(malloc_size, 0);