From 19e6e86fde693d09023888f5ca746e30d135b2ea Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 10 Feb 2022 22:02:36 +0000
Subject: [PATCH] Warn when --malloc-may-fail has no effect

f7958df5d1 documented that malloc-may-fail needs to be used whenever the
library is added, but users might not actually have had a chance to read
updated documentation. Print a warning at runtime to make it more likely
that users become aware.
---
 regression/contracts/malloc-may-fail-warning/main.c  |  7 +++++++
 .../contracts/malloc-may-fail-warning/test.desc      | 11 +++++++++++
 .../contracts/malloc-may-fail-warning/with-malloc.c  | 10 ++++++++++
 .../malloc-may-fail-warning/with-malloc.desc         | 11 +++++++++++
 src/cbmc/cbmc_parse_options.cpp                      | 12 ++++++++++++
 .../goto_instrument_parse_options.cpp                | 12 ++++++++++++
 6 files changed, 63 insertions(+)
 create mode 100644 regression/contracts/malloc-may-fail-warning/main.c
 create mode 100644 regression/contracts/malloc-may-fail-warning/test.desc
 create mode 100644 regression/contracts/malloc-may-fail-warning/with-malloc.c
 create mode 100644 regression/contracts/malloc-may-fail-warning/with-malloc.desc

diff --git a/regression/contracts/malloc-may-fail-warning/main.c b/regression/contracts/malloc-may-fail-warning/main.c
new file mode 100644
index 00000000000..ad7c24ee5f0
--- /dev/null
+++ b/regression/contracts/malloc-may-fail-warning/main.c
@@ -0,0 +1,7 @@
+#include <stdlib.h>
+
+void main()
+{
+  int *p = malloc(sizeof(int));
+  __CPROVER_assert(p != NULL, "malloc-may-fail is not set");
+}
diff --git a/regression/contracts/malloc-may-fail-warning/test.desc b/regression/contracts/malloc-may-fail-warning/test.desc
new file mode 100644
index 00000000000..8970cd4fd4b
--- /dev/null
+++ b/regression/contracts/malloc-may-fail-warning/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--add-library _ --malloc-may-fail
+^malloc-may-fail has no effect when an implementation of malloc is already provided$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test is to confirm that ineffective use of malloc-may-fail yields a
+warning.
diff --git a/regression/contracts/malloc-may-fail-warning/with-malloc.c b/regression/contracts/malloc-may-fail-warning/with-malloc.c
new file mode 100644
index 00000000000..3c0d3ae34e7
--- /dev/null
+++ b/regression/contracts/malloc-may-fail-warning/with-malloc.c
@@ -0,0 +1,10 @@
+void *malloc(__CPROVER_size_t size)
+{
+  return __CPROVER_allocate(size, 0);
+}
+
+void main()
+{
+  int *p = malloc(sizeof(int));
+  __CPROVER_assert(p != NULL, "malloc-may-fail is not set");
+}
diff --git a/regression/contracts/malloc-may-fail-warning/with-malloc.desc b/regression/contracts/malloc-may-fail-warning/with-malloc.desc
new file mode 100644
index 00000000000..972dee2481f
--- /dev/null
+++ b/regression/contracts/malloc-may-fail-warning/with-malloc.desc
@@ -0,0 +1,11 @@
+CORE
+with-malloc.desc
+--malloc-may-fail
+^malloc-may-fail has no effect when an implementation of malloc is already provided$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test is to confirm that ineffective use of malloc-may-fail yields a
+warning.
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index ba9d672de8a..372199f5690 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -812,6 +812,18 @@ int cbmc_parse_optionst::get_goto_program(
     return CPROVER_EXIT_SUCCESS;
   }
 
+  if(cmdline.isset("malloc-may-fail"))
+  {
+    auto malloc_entry = goto_model.goto_functions.function_map.find("malloc");
+    if(
+      malloc_entry != goto_model.goto_functions.function_map.end() &&
+      malloc_entry->second.body_available())
+    {
+      log.warning() << "malloc-may-fail has no effect when an implementation "
+                    << "of malloc is already provided" << messaget::eom;
+    }
+  }
+
   if(cbmc_parse_optionst::process_goto_program(goto_model, options, log))
     return CPROVER_EXIT_INTERNAL_ERROR;
 
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index a99d5caa850..1574be969cf 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1066,6 +1066,18 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   // we add the library in some cases, as some analyses benefit
 
+  if(cmdline.isset("malloc-may-fail"))
+  {
+    auto malloc_entry = goto_model.goto_functions.function_map.find("malloc");
+    if(
+      malloc_entry != goto_model.goto_functions.function_map.end() &&
+      malloc_entry->second.body_available())
+    {
+      log.warning() << "malloc-may-fail has no effect when an implementation "
+                    << "of malloc is already provided" << messaget::eom;
+    }
+  }
+
   if(cmdline.isset("add-library") ||
      cmdline.isset("mm"))
   {