Rework memory allocation failure checks and options

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

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

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 14 failed
+\*\* 1 of 12 failed
 --
 ^warning: ignoring
 --

regression/cbmc/array_constraints1/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\*\* 2 of 16
+^\*\* 2 of 14
 --
 ^warning: ignoring

regression/cbmc/malloc-may-fail/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---malloc-may-fail --malloc-fail-null
+--allocation-may-fail
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$

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

@@ -1,9 +1,9 @@
 CORE
 largest_representable.c
---malloc-fail-assert
+--overly-large-allocation-check
 ^EXIT=0$
 ^SIGNAL=0$
-^\[malloc.assertion.\d+\] line \d+ max allocation size exceeded: SUCCESS$
+^\[malloc.allocate.\d+\] line \d+ .*: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

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

@@ -1,9 +1,9 @@
 CORE
 max_size.c
---malloc-fail-assert
+--overly-large-allocation-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[malloc.assertion.\d+\] line \d+ max allocation size exceeded: FAILURE$
+^\[malloc.allocate.\d+\] line \d+ .*: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

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

@@ -1,6 +1,6 @@
 CORE
 one_byte_too_large.c
---malloc-fail-null
+--overly-large-allocation-returns-null
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$

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 13 failed
+^\*\* 8 of 11 failed
 --
 ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
 ^warning: ignoring

regression/cbmc/r_w_ok1/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 
 __CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$
-^\*\* 2 of 12 failed
+^\*\* 2 of 10 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

src/analyses/goto_check.cpp

@@ -75,6 +75,8 @@ class goto_checkt
     error_labels=_options.get_list_option("error-label");
     enable_pointer_primitive_check =
       _options.get_bool_option("pointer-primitive-check");
+    enable_overly_large_allocation_check =
+      _options.get_bool_option("overly-large-allocation-check");
   }
 
   typedef goto_functionst::goto_functiont goto_functiont;
@@ -195,6 +197,10 @@ class goto_checkt
   /// \param guard: the condition under which the operation happens
   void pointer_primitive_check(const exprt &expr, const guardt &guard);
 
+  void overly_large_allocation_check(
+    const side_effect_exprt &expr,
+    const guardt &guard);
+
   /// Returns true if the given expression is a pointer primitive such as
   /// __CPROVER_r_ok()
   ///
@@ -256,6 +262,7 @@ class goto_checkt
   bool enable_built_in_assertions;
   bool enable_assumptions;
   bool enable_pointer_primitive_check;
+  bool enable_overly_large_allocation_check;
 
   typedef optionst::value_listt error_labelst;
   error_labelst error_labels;
@@ -1229,6 +1236,29 @@ void goto_checkt::pointer_primitive_check(
     guard);
 }
 
+void goto_checkt::overly_large_allocation_check(
+  const side_effect_exprt &expr,
+  const guardt &guard)
+{
+  if(!enable_overly_large_allocation_check)
+    return;
+
+  const exprt size_expr = expr.operands().front();
+
+  binary_relation_exprt bre(
+    size_expr,
+    ID_le,
+    ns.lookup(CPROVER_PREFIX "max_malloc_size").symbol_expr());
+
+  add_guarded_property(
+    bre,
+    "more memory allocated than can be addressed by cbmc",
+    "allocate",
+    expr.source_location(),
+    expr,
+    guard);
+}
+
 bool goto_checkt::is_pointer_primitive(const exprt &expr)
 {
   // we don't need to include the __CPROVER_same_object primitive here as it
@@ -1812,6 +1842,15 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
   {
     pointer_primitive_check(expr, guard);
   }
+  else if(expr.id() == ID_side_effect)
+  {
+    const auto &side_effect_expr = to_side_effect_expr(expr);
+
+    if(side_effect_expr.get_statement() == ID_allocate)
+    {
+      overly_large_allocation_check(side_effect_expr, guard);
+    }
+  }
 }
 
 void goto_checkt::check(const exprt &expr)
@@ -1934,6 +1973,8 @@ void goto_checkt::goto_check(
         flag_resetter.set_flag(enable_nan_check, false);
       else if(d.first == "disable:pointer-primitive-check")
         flag_resetter.set_flag(enable_pointer_primitive_check, false);
+      else if(d.first == "disable:overly-large-allocation-check")
+        flag_resetter.set_flag(enable_overly_large_allocation_check, false);
     }
 
     new_code.clear();

src/analyses/goto_check.h

@@ -39,7 +39,8 @@ void goto_check(
   "overflow-check)"                                                            \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
   "(float-overflow-check)(nan-check)(no-built-in-assertions)"                  \
-  "(pointer-primitive-check)"
+  "(pointer-primitive-check)"                                                  \
+  "(overly-large-allocation-check)"
 
 // clang-format off
 #define HELP_GOTO_CHECK \
@@ -56,7 +57,10 @@ 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) */ \
-  " --pointer-primitive-check    checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */
+  " --pointer-primitive-check    checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */ \
+  << help_entry( \
+    "--overly-large-allocation-check", \
+    "checks that no individual allocation exceeds CBMC's address space limit")
 
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
   options.set_option("bounds-check", cmdline.isset("bounds-check")); \
@@ -72,7 +76,8 @@ void goto_check(
   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("pointer-primitive-check", cmdline.isset("pointer-primitive-check")) /* NOLINT(whitespace/line_length) */
+  options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("overly-large-allocation-check", cmdline.isset("overly-large-allocation-check")) /* NOLINT(whitespace/line_length) */
 // clang-format on
 
 #endif // CPROVER_ANALYSES_GOTO_CHECK_H

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

@@ -1067,17 +1067,18 @@ void cbmc_parse_optionst::help()
     HELP_SHOW_GOTO_FUNCTIONS
     "\n"
     "Program instrumentation options:\n"
-    HELP_GOTO_CHECK
+    << HELP_GOTO_CHECK <<
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     " --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(
+      "--overly-large-allocation-returns-null",
+      "memory allocation functions return null when more memory is allocated than can be addressed by cbmc") // NOLINT(*)
+    << help_entry(
+      "--allocation-may-fail",
+      "allow memory 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)" \
+  "(overly-large-allocation-returns-null)" \
+  "(allocation-may-fail)" \
   OPT_XML_INTERFACE \
   OPT_JSON_INTERFACE \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -916,7 +916,7 @@ void goto_analyzer_parse_optionst::help()
     HELP_SHOW_PROPERTIES
     "\n"
     "Program instrumentation options:\n"
-    HELP_GOTO_CHECK
+    << HELP_GOTO_CHECK <<
     "\n"
     "Other options:\n"
     HELP_VALIDATE

src/goto-diff/goto_diff_parse_options.cpp

@@ -407,7 +407,7 @@ void goto_diff_parse_optionst::help()
     " --compact-output             output dependencies in compact mode\n"
     "\n"
     "Program instrumentation options:\n"
-    HELP_GOTO_CHECK
+    << HELP_GOTO_CHECK <<
     " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
     "Other options:\n"
     " --version                    show version and exit\n"

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1792,7 +1792,7 @@ void goto_instrument_parse_optionst::help()
     "\n"
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"
-    HELP_GOTO_CHECK
+    << HELP_GOTO_CHECK <<
     " --uninitialized-check        add checks for uninitialized locals (experimental)\n" // NOLINT(*)
     " --error-label label          check that label is unreachable\n"
     " --stack-depth n              add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)

src/util/config.cpp

@@ -1093,17 +1093,20 @@ 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("overly-large-allocation-check") &&
+    cmdline.isset("overly-large-allocation-returns-null"))
   {
     throw invalid_command_line_argument_exceptiont{
-      "at most one malloc failure mode is acceptable", "--malloc-fail-null"};
+      "only one of "
+      "--overly-large-allocation-check/--overly-large-allocation-returns-null "
+      "can be given at a time",
+      "--overly-large-allocation-check/--overly-large-allocation-returns-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("allocation-may-fail");
+  ansi_c.allocate_size_null =
+    cmdline.isset("overly-large-allocation-returns-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;