Skip to content

Detect use of free() with alloca-allocated objects #4270

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 25, 2019
Merged

Detect use of free() with alloca-allocated objects #4270

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions regression/cbmc/alloca1/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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);
}
10 changes: 10 additions & 0 deletions regression/cbmc/alloca1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
4 changes: 2 additions & 2 deletions regression/cbmc/function-return-no-body1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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">
--
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the step_nr really important? Perhaps make .*?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed, now using \d+.

^warning: ignoring
2 changes: 1 addition & 1 deletion regression/goto-analyzer/constant_propagation_01/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion regression/goto-analyzer/constant_propagation_02/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion regression/goto-analyzer/constant_propagation_03/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion regression/goto-analyzer/constant_propagation_04/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion regression/goto-analyzer/constant_propagation_07/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion regression/goto-analyzer/constant_propagation_12/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
1 change: 1 addition & 0 deletions src/ansi-c/ansi_c_internal_additions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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__["
Expand Down
11 changes: 11 additions & 0 deletions src/ansi-c/library/stdlib.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand All @@ -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;
}

Expand All @@ -164,6 +169,7 @@ __CPROVER_HIDE:;
#undef free

__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
extern void *__CPROVER_alloca_object;

inline void free(void *ptr)
{
Expand All @@ -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
Expand Down
1 change: 1 addition & 0 deletions src/cpp/cpp_internal_additions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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';
Expand Down