Merge pull request #5500 from hannes-steffenhagen-diffblue/fix/malloc-checks

hannes-steffenhagen-diffblue · web-flow · commit 2c7decc99f81 · 2020-09-23T17:44:23.000+01:00
Fix bug that prevented --malloc-may-fail from working
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -726,6 +726,10 @@ 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();
diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 18, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 14, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 13, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 16, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.c b/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;
+}
diff --git a/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc b/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.
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/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__["
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -48,6 +48,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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>
@@ -890,6 +891,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());
 
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <jsil/jsil_language.h>
 
+#include <goto-programs/add_malloc_may_fail_variable_initializations.h>
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
@@ -814,7 +815,12 @@ 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);
-    #endif
+
+    // these are commented out as well because without the library
+    // this initialization code doesn’t make any sense
+    add_malloc_may_fail_variable_initializations(goto_model);
+
+#endif
 
     // remove function pointers
     log.status() << "Removing function pointers and virtual functions"
diff --git a/src/goto-programs/Makefile b/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 \
diff --git a/src/goto-programs/add_malloc_may_fail_variable_initializations.cpp b/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)));
+}
diff --git a/src/goto-programs/add_malloc_may_fail_variable_initializations.h b/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

Original file line number	Diff line number	Diff line change
`@@ -726,6 +726,10 @@ int jbmc_parse_optionst::get_goto_program(`
`726`	`726`
`727`	`727`	`goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);`
`728`	`728`
	`729`	`+ // if we added the ansi-c library models here this should also call`
	`730`	`+ // add_malloc_may_fail_variable_initializations(goto_model);`
	`731`	`+ // here`
	`732`	`+`
`729`	`733`	`if(cmdline.isset("validate-goto-model"))`
`730`	`734`	`{`
`731`	`735`	`goto_model.validate();`