Fix bug that prevented --malloc-may-fail from working

We have code in our stdlib models that depends on two global variables,
__CPROVER_malloc_may_fail and __CPROVER_malloc_failure_mode. Previously
these were set based on the ansi-c config in builtin_additions by
generating C code containing definitions for these variables.

The problem with that is that if you compile an executable using goto-cc
we also load the builtin_additions, so this executable already contains
definitions for these variables which can't be overridden.

This works around this issue by instead declaring these variables as
extern in builtin_additions, and setting their values dynamically as
last-minute instrumentation at the end of __CPROVER_initialize.  Giving
these no/nondet initial values is important because otherwise
preprocessing like constant folding on goto-binaries before cbmc
actually runs could remove branches we can, in fact, take with different
values set by --malloc-fail-* flags.

An alternative would be to instead dynamically change the code for the
models functions as instrumentation, but this has a couple of problems;
For instance this means we might change the behaviour of custom stdlib
models (which we allow via --no-library) or custom goto instrumentation
in unexpected ways. I believe this way is the least likely to cause any
friction like that.

Author: hannes-steffenhagen-diffblue

regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main(void)
+{
+  int *array = calloc(10, sizeof(int));
+  assert(array != NULL);
+  free(array);
+  return 0;
+}

regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--malloc-may-fail --malloc-fail-null
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line 7 assertion array != .*: FAILURE
+--
+--
+Compiling a file with goto-cc should not affect how --malloc-may-fail behaves
+Regex in the assertion because on travis for some reason the preprocessor seems to run
+before cbmc.

src/ansi-c/ansi_c_internal_additions.cpp

@@ -186,17 +186,15 @@ 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"
+    "extern int " CPROVER_PREFIX "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"
+    "extern " CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_may_fail;\n"
 
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["

src/cbmc/cbmc_parse_options.cpp

@@ -48,6 +48,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/stop_on_fail_verifier.h>
 #include <goto-checker/stop_on_fail_verifier_with_fault_localization.h>
 
+#include <goto-programs/add_malloc_may_fail_variable_initializations.h>
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
@@ -879,6 +880,8 @@ bool cbmc_parse_optionst::process_goto_program(
   link_to_library(
     goto_model, log.get_message_handler(), cprover_c_library_factory);
 
+  add_malloc_may_fail_variable_initializations(goto_model);
+
   if(options.get_bool_option("string-abstraction"))
     string_instrumentation(goto_model, log.get_message_handler());
 

src/goto-programs/Makefile

@@ -1,4 +1,5 @@
-SRC = adjust_float_expressions.cpp \
+SRC = add_malloc_may_fail_variable_initializations.cpp \
+      adjust_float_expressions.cpp \
       builtin_functions.cpp \
       class_hierarchy.cpp \
       class_identifier.cpp \

src/goto-programs/add_malloc_may_fail_variable_initializations.cpp

@@ -0,0 +1,62 @@
+/// \file
+/// \author Diffblue Ltd.
+
+#include "add_malloc_may_fail_variable_initializations.h"
+
+#include "goto_model.h"
+
+#include <util/arith_tools.h>
+#include <util/config.h>
+#include <util/irep.h>
+
+template <typename T>
+code_assignt make_integer_assignment(
+  const symbol_table_baset &symbol_table,
+  const irep_idt &symbol_name,
+  T &&value)
+{
+  const auto &symbol = symbol_table.lookup_ref(symbol_name).symbol_expr();
+  return code_assignt{symbol, from_integer(value, symbol.type())};
+}
+
+void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
+{
+  const auto malloc_may_fail_id = irep_idt{CPROVER_PREFIX "malloc_may_fail"};
+  const auto malloc_failure_mode_id =
+    irep_idt{CPROVER_PREFIX "malloc_failure_mode"};
+  if(!goto_model.symbol_table.has_symbol(malloc_may_fail_id))
+  {
+    // if malloc_may_fail isn't in the symbol table (i.e. builtin library not
+    // loaded) then we don't generate initialisation code for it.
+    return;
+  }
+
+  INVARIANT(
+    goto_model.symbol_table.has_symbol(malloc_failure_mode_id),
+    "if malloc_may_fail is in the symbol table then so should "
+    "malloc_failure_mode");
+
+  auto const initialize_function_name = CPROVER_PREFIX "initialize";
+  PRECONDITION(
+    goto_model.get_goto_functions().function_map.count(
+      initialize_function_name) == 1);
+  auto &initialize_function =
+    goto_model.goto_functions.function_map.find(initialize_function_name)
+      ->second;
+  const auto initialize_function_end =
+    --initialize_function.body.instructions.end();
+
+  initialize_function.body.insert_before(
+    initialize_function_end,
+    goto_programt::make_assignment(make_integer_assignment(
+      goto_model.symbol_table,
+      malloc_may_fail_id,
+      config.ansi_c.malloc_may_fail)));
+
+  initialize_function.body.insert_before(
+    initialize_function_end,
+    goto_programt::make_assignment(make_integer_assignment(
+      goto_model.symbol_table,
+      malloc_failure_mode_id,
+      config.ansi_c.malloc_failure_mode)));
+}

src/goto-programs/add_malloc_may_fail_variable_initializations.h

@@ -0,0 +1,20 @@
+/// \file
+/// \author Diffblue Ltd.
+/// Adds an instrumentation to add initialisations for variables
+/// used by the --malloc-may-fail and related flags in cbmc
+
+// NOLINT(whitespace/line_length)
+#ifndef CPROVER_GOTO_PROGRAMS_ADD_MALLOC_MAY_FAIL_VARIABLE_INITIALIZATIONS_H
+// NOLINT(whitespace/line_length)
+#define CPROVER_GOTO_PROGRAMS_ADD_MALLOC_MAY_FAIL_VARIABLE_INITIALIZATIONS_H
+
+class goto_modelt;
+
+/// Some variables have different initial values based on what flags are being
+/// passed to cbmc; since the _start function might've been generated by goto-cc
+/// before getting passed over here we need to add the initialisation of these
+/// variables here as a post-processing step
+void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model);
+
+// NOLINT(whitespace/line_length)
+#endif // CPROVER_GOTO_PROGRAMS_ADD_MALLOC_MAY_FAIL_VARIABLE_INITIALIZATIONS_H