Merge pull request #8101 from thomasspriggs/tas/default-malloc-failure

Use malloc-fail-null by default

Author: Enrico Steffinlongo

Diff for: doc/man/cbmc.1

@@ -105,9 +105,6 @@ disable signed arithmetic over\- and underflow checks
 \fB\-\-no\-malloc\-may\-fail\fR
 do not allow malloc calls to fail by default
 .TP
-\fB\-\-no\-malloc\-fail\-null\fR
-do not set malloc failure mode to return null pointer
-.TP
 \fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
 do not generate unwinding assertions (cannot be
 used with \fB\-\-cover\fR)

Diff for: doc/man/goto-analyzer.1

@@ -637,9 +637,6 @@ disable signed arithmetic over\- and underflow checks
 \fB\-\-no\-malloc\-may\-fail\fR
 do not allow malloc calls to fail by default
 .TP
-\fB\-\-no\-malloc\-fail\-null\fR
-do not set malloc failure mode to return null pointer
-.TP
 \fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
 do not generate unwinding assertions (cannot be
 used with \fB\-\-cover\fR)

Diff for: doc/man/goto-instrument.1

@@ -697,6 +697,9 @@ set malloc failure mode to assert\-then\-assume
 \fB\-\-malloc\-fail\-null\fR
 set malloc failure mode to return null
 .TP
+\fB\-\-no\-malloc\-may\-fail\fR
+do not allow malloc calls to fail by default
+.TP
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
 .TP

Diff for: regression/contracts-dfcc/chain.sh

@@ -43,6 +43,10 @@ else
   $goto_cc -o "${name}${dfcc_suffix}.gb" "${name}.c"
 fi
 
+if [[ "${args_inst}" != *"malloc"* ]]; then
+  args_inst="--no-malloc-may-fail $args_inst"
+fi
+
 rm -f "${name}${dfcc_suffix}-mod.gb"
 $goto_instrument ${args_inst} "${name}${dfcc_suffix}.gb" "${name}${dfcc_suffix}-mod.gb"
 if [ ! -e "${name}${dfcc_suffix}-mod.gb" ] ; then

Diff for: regression/goto-instrument/chain.sh

@@ -21,7 +21,7 @@ else
 fi
 
 rm -f "${target}-mod.gb"
-$goto_instrument ${args} "${target}.gb" "${target}-mod.gb"
+$goto_instrument --no-malloc-may-fail ${args} "${target}.gb" "${target}-mod.gb"
 if [ ! -e "${target}-mod.gb" ] ; then
   cp "${target}.gb" "${target}-mod.gb"
 elif echo $args | grep -q -- "--dump-c-type-header" ; then
@@ -39,5 +39,5 @@ elif echo $args | grep -q -- "--dump-c" ; then
 
   rm "${target}-mod.c"
 fi
-$goto_instrument --show-goto-functions "${target}-mod.gb"
+$goto_instrument --no-malloc-may-fail --show-goto-functions "${target}-mod.gb"
 $cbmc --no-standard-checks "${target}-mod.gb"

Diff for: regression/goto-synthesizer/chain.sh

@@ -37,7 +37,7 @@ fi
 rm -f "${name}-mod.gb"
 rm -f "${name}-mod-2.gb"
 echo "Running goto-instrument: "
-$goto_instrument ${args_inst} "${name}.gb" "${name}-mod.gb"
+$goto_instrument --no-malloc-may-fail ${args_inst} "${name}.gb" "${name}-mod.gb"
 if [ ! -e "${name}-mod.gb" ] ; then
   cp "$name.gb" "${name}-mod.gb"
 elif echo $args_inst | grep -q -- "--dump-c" ; then
@@ -53,9 +53,9 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
 fi
 echo "Running goto-synthesizer: "
 if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then
-  $goto_synthesizer ${args_synthesizer} "${name}-mod.gb"
+  $goto_synthesizer ${args_synthesizer} --no-malloc-may-fail "${name}-mod.gb"
 else
-  $goto_synthesizer ${args_synthesizer} "${name}-mod.gb" "${name}-mod-2.gb"
+  $goto_synthesizer ${args_synthesizer} --no-malloc-may-fail "${name}-mod.gb" "${name}-mod-2.gb"
   echo "Running CBMC: "
   $cbmc --no-standard-checks ${args_cbmc} "${name}-mod-2.gb"
 fi

Diff for: src/cbmc/cbmc_parse_options.cpp

@@ -126,10 +126,28 @@ void cbmc_parse_optionst::set_default_analysis_flags(
   {
     options.set_option("unwinding-assertions", enabled);
   }
+
+  if(enabled)
+  {
+    config.ansi_c.malloc_may_fail = true;
+    config.ansi_c.malloc_failure_mode =
+      configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null;
+  }
+  else
+  {
+    config.ansi_c.malloc_may_fail = false;
+    config.ansi_c.malloc_failure_mode =
+      configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_none;
+  }
 }
 
 void cbmc_parse_optionst::get_command_line_options(optionst &options)
 {
+  // Enable flags that in combination provide analysis with no surprises
+  // (expected checks and no unsoundness by missing checks).
+  cbmc_parse_optionst::set_default_analysis_flags(
+    options, !cmdline.isset("no-standard-checks"));
+
   if(config.set(cmdline))
   {
     usage_error();
@@ -366,11 +384,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     "self-loops-to-assumptions",
     !cmdline.isset("no-self-loops-to-assumptions"));
 
-  // Enable flags that in combination provide analysis with no surprises
-  // (expected checks and no unsoundness by missing checks).
-  cbmc_parse_optionst::set_default_analysis_flags(
-    options, !cmdline.isset("no-standard-checks"));
-
   // all (other) checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 

Diff for: src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -68,13 +68,29 @@ void goto_analyzer_parse_optionst::set_default_analysis_flags(
   options.set_option("signed-overflow-check", enabled);
   options.set_option("undefined-shift-check", enabled);
 
+  if(enabled)
+  {
+    config.ansi_c.malloc_may_fail = true;
+    config.ansi_c.malloc_failure_mode =
+      configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null;
+  }
+  else
+  {
+    config.ansi_c.malloc_may_fail = false;
+    config.ansi_c.malloc_failure_mode =
+      configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_none;
+  }
+
   // This is in-line with the options we set for CBMC in cbmc_parse_optionst
   // with the exception of unwinding-assertions, which don't make sense in
   // the context of abstract interpretation.
 }
 
 void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
 {
+  goto_analyzer_parse_optionst::set_default_analysis_flags(
+    options, !cmdline.isset("no-standard-checks"));
+
   if(config.set(cmdline))
   {
     usage_error();
@@ -84,9 +100,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("function"))
     options.set_option("function", cmdline.get_value("function"));
 
-  goto_analyzer_parse_optionst::set_default_analysis_flags(
-    options, !cmdline.isset("no-standard-checks"));
-
   // all (other) checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 

Diff for: src/goto-analyzer/goto_analyzer_parse_options.h

@@ -89,6 +89,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 
+#include <util/config.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
 #include <util/ui_message.h>
@@ -152,6 +153,7 @@ class optionst;
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
   OPT_GOTO_CHECK \
+  OPT_CONFIG_LIBRARY \
   "(show-symbol-table)(show-parse-tree)" \
   "(property):" \
   "(verbosity):(version)" \

Diff for: src/util/config.cpp

@@ -1126,7 +1126,15 @@ bool configt::set(const cmdlinet &cmdline)
   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");
+  if(cmdline.isset("malloc-may-fail"))
+  {
+    ansi_c.malloc_may_fail = true;
+  }
+  if(cmdline.isset("no-malloc-may-fail"))
+  {
+    ansi_c.malloc_may_fail = false;
+    ansi_c.malloc_failure_mode = ansi_ct::malloc_failure_mode_none;
+  }
 
   if(cmdline.isset("c89"))
     ansi_c.set_c89();

Diff for: src/util/config.h

@@ -71,10 +71,12 @@ class symbol_table_baset;
 
 #define OPT_CONFIG_LIBRARY                                                     \
   "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)"                    \
+  "(no-malloc-may-fail)"                                                       \
   "(string-abstraction)"
 
 #define HELP_CONFIG_LIBRARY                                                    \
   " {y--malloc-may-fail} \t allow malloc calls to return a null pointer\n"     \
+  " {y--no-malloc-may-fail} \t disable potential malloc failure\n"             \
   " {y--malloc-fail-assert} \t "                                               \
   "set malloc failure mode to assert-then-assume\n"                            \
   " {y--malloc-fail-null} \t set malloc failure mode to return null\n"         \
@@ -272,7 +274,7 @@ class configt
     libt lib;
 
     bool string_abstraction;
-    bool malloc_may_fail = false;
+    bool malloc_may_fail = true;
 
     enum malloc_failure_modet
     {
@@ -281,7 +283,7 @@ class configt
       malloc_failure_mode_assert_then_assume = 2
     };
 
-    malloc_failure_modet malloc_failure_mode = malloc_failure_mode_none;
+    malloc_failure_modet malloc_failure_mode = malloc_failure_mode_return_null;
 
     static const std::size_t default_object_bits = 8;