From 3c3348a98e82fbcb6b10e2c74ade47cb3c1fbf13 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 26 Nov 2018 14:37:41 +0000
Subject: [PATCH] Detect use of free() with alloca-allocated objects

As we internally use dynamic allocation, we previously did not distinguish
alloca-allocated from malloc/calloc-allocated ones.
---
 regression/cbmc/alloca1/main.c                       | 12 ++++++++++++
 regression/cbmc/alloca1/test.desc                    | 10 ++++++++++
 regression/cbmc/function-return-no-body1/test.desc   |  4 ++--
 .../goto-analyzer/constant_propagation_01/test.desc  |  2 +-
 .../goto-analyzer/constant_propagation_02/test.desc  |  2 +-
 .../goto-analyzer/constant_propagation_03/test.desc  |  2 +-
 .../goto-analyzer/constant_propagation_04/test.desc  |  2 +-
 .../goto-analyzer/constant_propagation_07/test.desc  |  2 +-
 .../goto-analyzer/constant_propagation_12/test.desc  |  2 +-
 src/ansi-c/ansi_c_internal_additions.cpp             |  1 +
 src/ansi-c/library/stdlib.c                          | 11 +++++++++++
 src/cpp/cpp_internal_additions.cpp                   |  1 +
 12 files changed, 43 insertions(+), 8 deletions(-)
 create mode 100644 regression/cbmc/alloca1/main.c
 create mode 100644 regression/cbmc/alloca1/test.desc

diff --git a/regression/cbmc/alloca1/main.c b/regression/cbmc/alloca1/main.c
new file mode 100644
index 00000000000..014bf955d14
--- /dev/null
+++ b/regression/cbmc/alloca1/main.c
@@ -0,0 +1,12 @@
+#include <stdlib.h>
+
+#ifdef _WIN32
+void *alloca(size_t alloca_size);
+#endif
+
+int main()
+{
+  int *p = alloca(sizeof(int));
+  *p = 42;
+  free(p);
+}
diff --git a/regression/cbmc/alloca1/test.desc b/regression/cbmc/alloca1/test.desc
new file mode 100644
index 00000000000..66fa40a9537
--- /dev/null
+++ b/regression/cbmc/alloca1/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+free called for stack-allocated object: FAILURE$
+^\*\* 1 of 12 failed
+--
+^warning: ignoring
diff --git a/regression/cbmc/function-return-no-body1/test.desc b/regression/cbmc/function-return-no-body1/test.desc
index a7f228211dc..17f1370937f 100644
--- a/regression/cbmc/function-return-no-body1/test.desc
+++ b/regression/cbmc/function-return-no-body1/test.desc
@@ -5,7 +5,7 @@ activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-<function_call hidden="false" step_nr="18" thread="0">\n\s*<function display_name="no_body" identifier="no_body">
-<function_return hidden="false" step_nr="19" thread="0">\n\s*<function display_name="no_body" identifier="no_body">
+<function_call hidden="false" step_nr="\d+" thread="0">\n\s*<function display_name="no_body" identifier="no_body">
+<function_return hidden="false" step_nr="\d+" thread="0">\n\s*<function display_name="no_body" identifier="no_body">
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc
index a4a79f28ab1..e219da8cbc2 100644
--- a/regression/goto-analyzer/constant_propagation_01/test.desc
+++ b/regression/goto-analyzer/constant_propagation_01/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, 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
index 6a28820a4b0..8de026212bf 100644
--- a/regression/goto-analyzer/constant_propagation_02/test.desc
+++ b/regression/goto-analyzer/constant_propagation_02/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 12, 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
index 6a28820a4b0..8de026212bf 100644
--- a/regression/goto-analyzer/constant_propagation_03/test.desc
+++ b/regression/goto-analyzer/constant_propagation_03/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 12, 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
index 6a28820a4b0..8de026212bf 100644
--- a/regression/goto-analyzer/constant_propagation_04/test.desc
+++ b/regression/goto-analyzer/constant_propagation_04/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 12, 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
index 291f5339049..834532f9fa3 100644
--- a/regression/goto-analyzer/constant_propagation_07/test.desc
+++ b/regression/goto-analyzer/constant_propagation_07/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 11, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 10, 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
index df5dd997788..60a7a7e0891 100644
--- a/regression/goto-analyzer/constant_propagation_12/test.desc
+++ b/regression/goto-analyzer/constant_propagation_12/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index b22dafa554e..9c8de954b65 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -148,6 +148,7 @@ void ansi_c_internal_additions(std::string &code)
     "const void *" CPROVER_PREFIX "memory_leak=0;\n"
     "void *" CPROVER_PREFIX "allocate("
       CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
+    "const void *" CPROVER_PREFIX "alloca_object = 0;\n"
 
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index b96b12a2239..15d47b7784b 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -128,6 +128,7 @@ inline void *malloc(__CPROVER_size_t malloc_size)
 /* FUNCTION: __builtin_alloca */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+extern void *__CPROVER_alloca_object;
 
 inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
 {
@@ -144,6 +145,10 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
   __CPROVER_malloc_size=record_malloc?alloca_size:__CPROVER_malloc_size;
   __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
 
+  // record alloca to detect invalid free
+  __CPROVER_bool record_alloca = __VERIFIER_nondet___CPROVER_bool();
+  __CPROVER_alloca_object = record_alloca ? res : __CPROVER_alloca_object;
+
   return res;
 }
 
@@ -164,6 +169,7 @@ __CPROVER_HIDE:;
 #undef free
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+extern void *__CPROVER_alloca_object;
 
 inline void free(void *ptr)
 {
@@ -185,6 +191,11 @@ inline void free(void *ptr)
                          !__CPROVER_malloc_is_new_array,
                          "free called for new[] object");
 
+  // catch people who try to use free(...) with alloca
+  __CPROVER_precondition(
+    ptr == 0 || __CPROVER_alloca_object != ptr,
+    "free called for stack-allocated object");
+
   if(ptr!=0)
   {
     // non-deterministically record as deallocated
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
index f62f0880a25..3a11eb1be04 100644
--- a/src/cpp/cpp_internal_additions.cpp
+++ b/src/cpp/cpp_internal_additions.cpp
@@ -85,6 +85,7 @@ void cpp_internal_additions(std::ostream &out)
   out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n';
   out << "void *" CPROVER_PREFIX "allocate("
       << CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);" << '\n';
+  out << "const void *" CPROVER_PREFIX "alloca_object = 0;" << '\n';
 
   // auxiliaries for new/delete
   out << "void *__new(__CPROVER::size_t);" << '\n';