Simplify malloc models for allocation failures

Author: danpoe

src/ansi-c/ansi_c_internal_additions.cpp

@@ -186,17 +186,13 @@ void ansi_c_internal_additions(std::string &code)
       CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
     "const void *" CPROVER_PREFIX "alloca_object = 0;\n"
 
-    "int " CPROVER_PREFIX "malloc_failure_mode="+
-      std::to_string(config.ansi_c.malloc_failure_mode)+";\n"
-    "int " CPROVER_PREFIX "malloc_failure_mode_return_null="+
-    std::to_string(config.ansi_c.malloc_failure_mode_return_null)+";\n"
-    "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="+
     integer2string(max_malloc_size(config.ansi_c.pointer_width, config
     .bv_encoding.object_bits))+";\n"
-    CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_may_fail = " +
-    std::to_string(config.ansi_c.malloc_may_fail) + ";\n"
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "allocate_may_fail = " +
+    std::to_string(config.ansi_c.allocate_may_fail) + ";\n"
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "allocate_size_null = " +
+    std::to_string(config.ansi_c.allocate_size_null) + ";\n"
 
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["

src/ansi-c/library/stdlib.c

@@ -75,29 +75,14 @@ __CPROVER_HIDE:;
   __CPROVER_size_t alloc_size = nmemb * size;
 #pragma CPROVER check pop
 
-  if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null)
+  if(__CPROVER_allocate_size_null && alloc_size > __CPROVER_max_malloc_size)
   {
-    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
-    if(
-      alloc_size > __CPROVER_max_malloc_size ||
-      (__CPROVER_malloc_may_fail && should_malloc_fail))
-    {
-      return (void *)0;
-    }
+    return (void *)0;
   }
-  else if(
-    __CPROVER_malloc_failure_mode ==
-    __CPROVER_malloc_failure_mode_assert_then_assume)
+
+  if(__CPROVER_allocate_may_fail && __VERIFIER_nondet___CPROVER_bool())
   {
-    __CPROVER_assert(
-      alloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
-    __CPROVER_assume(alloc_size <= __CPROVER_max_malloc_size);
-
-    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
-    __CPROVER_assert(
-      !__CPROVER_malloc_may_fail || !should_malloc_fail,
-      "max allocation may fail");
-    __CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail);
+    return (void *)0;
   }
 
   void *malloc_res;
@@ -141,29 +126,14 @@ inline void *malloc(__CPROVER_size_t malloc_size)
 // but we only do so if `--malloc-may-fail` is set
 __CPROVER_HIDE:;
 
-  if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null)
+  if(__CPROVER_allocate_size_null && malloc_size > __CPROVER_max_malloc_size)
   {
-    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
-    if(
-      malloc_size > __CPROVER_max_malloc_size ||
-      (__CPROVER_malloc_may_fail && should_malloc_fail))
-    {
-      return (void *)0;
-    }
+    return (void *)0;
   }
-  else if(
-    __CPROVER_malloc_failure_mode ==
-    __CPROVER_malloc_failure_mode_assert_then_assume)
+
+  if(__CPROVER_allocate_may_fail && __VERIFIER_nondet___CPROVER_bool())
   {
-    __CPROVER_assert(
-      malloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
-    __CPROVER_assume(malloc_size <= __CPROVER_max_malloc_size);
-
-    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
-    __CPROVER_assert(
-      !__CPROVER_malloc_may_fail || !should_malloc_fail,
-      "max allocation may fail");
-    __CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail);
+    return (void *)0;
   }
 
   void *malloc_res;

src/cbmc/cbmc_parse_options.cpp

@@ -1073,11 +1073,12 @@ void cbmc_parse_optionst::help()
     " --error-label label          check that label is unreachable\n"
     " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --malloc-fail-assert         set malloc failure mode to assert-then-assume\n"
-    " --malloc-fail-null           set malloc failure mode to return null\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --malloc-may-fail            allow malloc calls to return a null pointer\n"
+    << help_entry(
+      "--allocate-size-null",
+      "allocation functions return null when more memory is allocated than can be addressed by cbmc") // NOLINT(*)
+    << help_entry(
+      "--allocate-may-fail",
+      "allow allocation functions to return null") <<
     HELP_REACHABILITY_SLICER
     HELP_REACHABILITY_SLICER_FB
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -51,8 +51,8 @@ class optionst;
   "(object-bits):" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
-  "(malloc-fail-assert)(malloc-fail-null)" \
-  "(malloc-may-fail)" \
+  "(allocate-size-null)" \
+  "(allocate-may-fail)" \
   OPT_XML_INTERFACE \
   OPT_JSON_INTERFACE \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \

src/util/config.cpp

@@ -1093,17 +1093,17 @@ bool configt::set(const cmdlinet &cmdline)
     bv_encoding.is_object_bits_default = false;
   }
 
-  if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null"))
+  if(
+    cmdline.isset("allocate-size-check") && cmdline.isset("allocate-size-null"))
   {
     throw invalid_command_line_argument_exceptiont{
-      "at most one malloc failure mode is acceptable", "--malloc-fail-null"};
+      "only one of --allocate-size-check/--allocate-size-null can be given at "
+      "a time",
+      "--allocate-size-check/--allocate-size-null"};
   }
-  if(cmdline.isset("malloc-fail-null"))
-    ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_return_null;
-  if(cmdline.isset("malloc-fail-assert"))
-    ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume;
 
-  ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");
+  ansi_c.allocate_may_fail = cmdline.isset("allocate-may-fail");
+  ansi_c.allocate_size_null = cmdline.isset("allocate-size-null");
 
   return false;
 }

src/util/config.h

@@ -129,16 +129,9 @@ class configt
     libt lib;
 
     bool string_abstraction;
-    bool malloc_may_fail = false;
 
-    enum malloc_failure_modet
-    {
-      malloc_failure_mode_none = 0,
-      malloc_failure_mode_return_null = 1,
-      malloc_failure_mode_assert_then_assume = 2
-    };
-
-    malloc_failure_modet malloc_failure_mode = malloc_failure_mode_none;
+    bool allocate_may_fail = false;
+    bool allocate_size_null = false;
 
     static const std::size_t default_object_bits=8;
   } ansi_c;