Merge pull request #4270 from tautschnig/alloca-free

Detect use of free() with alloca-allocated objects

Author: tautschnig

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);
+}

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

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

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

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

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

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

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

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

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__["

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

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';