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,9 @@
+CORE
+test.c
+--malloc-may-fail --malloc-fail-null
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line 6 assertion array != NULL: FAILURE
+--
+--
+Compiling a file with goto-cc should not affect how --malloc-may-fail behaves

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

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #include <memory>
 
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/exit_codes.h>
@@ -778,6 +779,47 @@ bool cbmc_parse_optionst::set_properties()
   return false;
 }
 
+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())};
+}
+
+/// 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
+static void
+add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
+{
+  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,
+      CPROVER_PREFIX "malloc_may_fail",
+      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,
+      CPROVER_PREFIX "malloc_failure_mode",
+      config.ansi_c.malloc_failure_mode)));
+}
+
 int cbmc_parse_optionst::get_goto_program(
   goto_modelt &goto_model,
   const optionst &options,
@@ -879,6 +921,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());