Set malloc_may_fail through symbol table

Do not fix up the value by tweaking __CPROVER_initialize. This
simplifies the code and allows us to regenerate __CPROVER_initialize at
any time (at least as far as __CPROVER_malloc_may_fail and
__CPROVER_malloc_failure_mode are concerned).

Author: peterschrammel

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -721,10 +721,6 @@ int jbmc_parse_optionst::get_goto_program(
 
     goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
 
-    // if we added the ansi-c library models here this should also call
-    // add_malloc_may_fail_variable_initializations(goto_model);
-    // here
-
     if(cmdline.isset("validate-goto-model"))
     {
       goto_model.validate();

src/ansi-c/ansi_c_internal_additions.cpp

@@ -188,15 +188,21 @@ 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"
 
-    "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"
+    "int " CPROVER_PREFIX "thread_local "
+      CPROVER_PREFIX "malloc_failure_mode=" +
+      std::to_string(config.ansi_c.malloc_may_fail) + ";\n"
+    "int " CPROVER_PREFIX "thread_local "
+      CPROVER_PREFIX "malloc_failure_mode_return_null="+
+      std::to_string(config.ansi_c.malloc_failure_mode_return_null)+";\n"
+    "int " CPROVER_PREFIX "thread_local "
+      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"
-    "extern " CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_may_fail;\n"
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "thread_local "
+      CPROVER_PREFIX "malloc_may_fail=" +
+      std::to_string(config.ansi_c.malloc_may_fail) + ";\n"
 
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["

src/cbmc/cbmc_parse_options.cpp

@@ -50,7 +50,6 @@ 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/initialize_goto_model.h>
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/loop_ids.h>
@@ -893,8 +892,6 @@ 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);
-
   // Common removal of types and complex constructs
   if(::process_goto_program(goto_model, options, log))
     return true;

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -22,7 +22,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <cpp/cprover_library.h>
 
-#include <goto-programs/add_malloc_may_fail_variable_initializations.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/process_goto_program.h>
@@ -667,8 +666,6 @@ bool goto_analyzer_parse_optionst::process_goto_program(
   link_to_library(goto_model, ui_message_handler, cprover_cpp_library_factory);
   link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
 
-  add_malloc_may_fail_variable_initializations(goto_model);
-
   // Common removal of types and complex constructs
   if(::process_goto_program(goto_model, options, log))
     return true;

src/goto-diff/goto_diff_parse_options.cpp

@@ -20,7 +20,6 @@ Author: Peter Schrammel
 #include <util/options.h>
 #include <util/version.h>
 
-#include <goto-programs/add_malloc_may_fail_variable_initializations.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/loop_ids.h>
@@ -175,8 +174,6 @@ bool goto_diff_parse_optionst::process_goto_program(
   link_to_library(goto_model, ui_message_handler, cprover_cpp_library_factory);
   link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
 
-  add_malloc_may_fail_variable_initializations(goto_model);
-
   // Common removal of types and complex constructs
   if(::process_goto_program(goto_model, options, log))
     return true;

src/goto-programs/Makefile

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

src/goto-programs/add_malloc_may_fail_variable_initializations.cpp

@@ -1228,6 +1228,48 @@ static unsigned unsigned_from_ns(
   return numeric_cast_v<unsigned>(int_value);
 }
 
+/// Set the values of malloc_may_fail and malloc_failure_mode based on
+/// their entries found in the symbol table, if such entries exist.
+void configt::set_malloc_failure_mode_from_symbol_table(
+  const symbol_tablet &symbol_table)
+{
+  const auto malloc_may_fail_id = irep_idt{CPROVER_PREFIX "malloc_may_fail"};
+  if(!symbol_table.has_symbol(malloc_may_fail_id))
+    return;
+
+  const namespacet ns(symbol_table);
+
+  const symbolt &malloc_may_fail_sym = ns.lookup(malloc_may_fail_id);
+  config.ansi_c.malloc_may_fail =
+    numeric_cast_v<int>(to_constant_expr(malloc_may_fail_sym.value)) != 0;
+
+  const auto malloc_failure_mode_id =
+    irep_idt{CPROVER_PREFIX "malloc_failure_mode"};
+  const symbolt &malloc_failure_mode_sym = ns.lookup(malloc_failure_mode_id);
+  const int parsed_failure_mode =
+    numeric_cast_v<int>(to_constant_expr(malloc_failure_mode_sym.value));
+  INVARIANT(
+    parsed_failure_mode >= 0 && parsed_failure_mode <= 2,
+    "unexpected value found for " + id2string(malloc_failure_mode_id));
+  // the following is perhaps more verbose than necessary, but compiler
+  // warnings will make sure we keep handling all enum values
+  switch(parsed_failure_mode)
+  {
+  case ansi_ct::malloc_failure_modet::malloc_failure_mode_none:
+    config.ansi_c.malloc_failure_mode =
+      ansi_ct::malloc_failure_modet::malloc_failure_mode_none;
+    break;
+  case ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null:
+    config.ansi_c.malloc_failure_mode =
+      ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null;
+    break;
+  case ansi_ct::malloc_failure_modet::malloc_failure_mode_assert_then_assume:
+    config.ansi_c.malloc_failure_mode =
+      ansi_ct::malloc_failure_modet::malloc_failure_mode_assert_then_assume;
+    break;
+  }
+}
+
 void configt::set_from_symbol_table(
   const symbol_tablet &symbol_table)
 {
@@ -1284,6 +1326,8 @@ void configt::set_from_symbol_table(
   // lib, string_abstraction not stored in namespace
 
   set_object_bits_from_symbol_table(symbol_table);
+
+  set_malloc_failure_mode_from_symbol_table(symbol_table);
 }
 
 /// Sets the number of bits used for object addresses

src/goto-programs/add_malloc_may_fail_variable_initializations.h

@@ -334,6 +334,8 @@ class configt
 
 private:
   void set_classpath(const std::string &cp);
+
+  void set_malloc_failure_mode_from_symbol_table(const symbol_tablet &);
 };
 
 extern configt config;