From d397f587c4959d648a289cdba743969a86d2396d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Nov 2022 08:48:54 +0000 Subject: [PATCH] Memory allocations produced via alloca have function scope We must not mark the allocation as dead when leaving the block, but instead need to defer that until the end of the function. --- regression/cbmc-library/alloca-03/main.c | 32 +++++ regression/cbmc-library/alloca-03/test.desc | 10 ++ src/goto-programs/builtin_functions.cpp | 132 +++++++++++++------ src/goto-programs/goto_convert_class.h | 9 ++ src/goto-programs/goto_convert_functions.cpp | 5 + 5 files changed, 150 insertions(+), 38 deletions(-) create mode 100644 regression/cbmc-library/alloca-03/main.c create mode 100644 regression/cbmc-library/alloca-03/test.desc diff --git a/regression/cbmc-library/alloca-03/main.c b/regression/cbmc-library/alloca-03/main.c new file mode 100644 index 00000000000..e201c937ec9 --- /dev/null +++ b/regression/cbmc-library/alloca-03/main.c @@ -0,0 +1,32 @@ +#include + +#ifdef _WIN32 +void *alloca(size_t alloca_size); +#endif + +typedef int *int_ptr; + +int_ptr global; + +void foo() +{ + int_ptr ptr[2]; + for(int i = 0; i < 2; ++i) + { + ptr[i] = alloca(sizeof(int)); + } + *(ptr[0]) = 42; + *(ptr[1]) = 42; + + _Bool nondet; + if(nondet) + global = ptr[0]; + else + global = ptr[1]; +} + +int main() +{ + foo(); + *global = 42; +} diff --git a/regression/cbmc-library/alloca-03/test.desc b/regression/cbmc-library/alloca-03/test.desc new file mode 100644 index 00000000000..0ce80143c07 --- /dev/null +++ b/regression/cbmc-library/alloca-03/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--pointer-check +^\[main.pointer_dereference.\d+\] line 31 dereference failure: dead object in \*global: FAILURE$ +^\*\* 1 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 68fefbc2900..6d97ef14ad0 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -721,6 +722,97 @@ void goto_convertt::do_havoc_slice( dest.add(goto_programt::make_other(array_replace, source_location)); } +/// alloca allocates memory that is freed when leaving the function (and not the +/// block, as regular destructors would do). +void goto_convertt::do_alloca( + const exprt &lhs, + const symbol_exprt &function, + const exprt::operandst &arguments, + goto_programt &dest, + const irep_idt &mode) +{ + const source_locationt &source_location = function.source_location(); + exprt new_lhs = lhs; + + // make sure we have a left-hand side to track the allocation even when the + // original program did not + if(lhs.is_nil()) + { + new_lhs = new_tmp_symbol( + to_code_type(function.type()).return_type(), + "alloca", + dest, + source_location, + mode) + .symbol_expr(); + } + + // do the actual function call + code_function_callt function_call(new_lhs, function, arguments); + function_call.add_source_location() = source_location; + copy(function_call, FUNCTION_CALL, dest); + + // Don't add instrumentation when we're in alloca (which might in turn call + // __builtin_alloca) -- the instrumentation will be done for the call of + // alloca. Also, we can only add instrumentation when we're in a function + // context. + if( + function.source_location().get_function() == "alloca" || !targets.prefix || + !targets.suffix) + { + return; + } + + // create a symbol to eventually (and non-deterministically) mark the + // allocation as dead; this symbol has function scope and is initialised to + // NULL + symbol_exprt this_alloca_ptr = + get_fresh_aux_symbol( + to_code_type(function.type()).return_type(), + id2string(function.source_location().get_function()), + "tmp_alloca", + source_location, + mode, + symbol_table) + .symbol_expr(); + goto_programt decl_prg; + decl_prg.add(goto_programt::make_decl(this_alloca_ptr, source_location)); + decl_prg.add(goto_programt::make_assignment( + this_alloca_ptr, + null_pointer_exprt{to_pointer_type(this_alloca_ptr.type())}, + source_location)); + targets.prefix->destructive_insert( + targets.prefix->instructions.begin(), decl_prg); + + // non-deterministically update this_alloca_ptr + if_exprt rhs{ + side_effect_expr_nondett{bool_typet(), source_location}, + new_lhs, + this_alloca_ptr}; + dest.add(goto_programt::make_assignment( + this_alloca_ptr, std::move(rhs), source_location)); + + // mark pointer to alloca result as dead, unless the alloca result (in + // this_alloca_ptr) is still NULL + symbol_exprt dead_object_sym = + ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); + exprt alloca_result = + typecast_exprt::conditional_cast(this_alloca_ptr, dead_object_sym.type()); + if_exprt not_null{ + equal_exprt{ + this_alloca_ptr, + null_pointer_exprt{to_pointer_type(this_alloca_ptr.type())}}, + dead_object_sym, + std::move(alloca_result)}; + auto assign = goto_programt::make_assignment( + std::move(dead_object_sym), std::move(not_null), source_location); + targets.suffix->insert_before_swap( + targets.suffix->instructions.begin(), assign); + targets.suffix->insert_after( + targets.suffix->instructions.begin(), + goto_programt::make_dead(this_alloca_ptr, source_location)); +} + /// add function calls to function queue for later processing void goto_convertt::do_function_call_symbol( const exprt &lhs, @@ -1398,45 +1490,9 @@ void goto_convertt::do_function_call_symbol( copy(function_call, FUNCTION_CALL, dest); } - else if( - (identifier == "alloca" || identifier == "__builtin_alloca") && - function.source_location().get_function() != "alloca") + else if(identifier == "alloca" || identifier == "__builtin_alloca") { - const source_locationt &source_location = function.source_location(); - exprt new_lhs = lhs; - - if(lhs.is_nil()) - { - new_lhs = new_tmp_symbol( - to_code_type(function.type()).return_type(), - "alloca", - dest, - source_location, - mode) - .symbol_expr(); - } - - code_function_callt function_call(new_lhs, function, arguments); - function_call.add_source_location() = source_location; - copy(function_call, FUNCTION_CALL, dest); - - // create a backup copy to ensure that no assignments to the pointer affect - // the destructor code that will execute eventually - if(!lhs.is_nil()) - make_temp_symbol(new_lhs, "alloca", dest, mode); - - // mark pointer to alloca result as dead - symbol_exprt dead_object_sym = - ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); - exprt alloca_result = - typecast_exprt::conditional_cast(new_lhs, dead_object_sym.type()); - if_exprt rhs{ - side_effect_expr_nondett{bool_typet(), source_location}, - std::move(alloca_result), - dead_object_sym}; - code_assignt assign{ - std::move(dead_object_sym), std::move(rhs), source_location}; - targets.destructor_stack.add(assign); + do_alloca(lhs, function, arguments, dest, mode); } else { diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 103baa005b8..b0c869bd300 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -382,6 +382,9 @@ class goto_convertt:public messaget struct targetst { + goto_programt *prefix = nullptr; + goto_programt *suffix = nullptr; + bool return_set, has_return_value, break_set, continue_set, default_set, throw_set, leave_set; @@ -688,6 +691,12 @@ class goto_convertt:public messaget const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode); + void do_alloca( + const exprt &lhs, + const symbol_exprt &function, + const exprt::operandst &arguments, + goto_programt &dest, + const irep_idt &mode); exprt get_array_argument(const exprt &src); }; diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 55d0bfe0aad..2401c7046bb 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -196,6 +196,8 @@ void goto_convert_functionst::convert_function( tmp_end_function.add(goto_programt::make_end_function(end_location)); targets = targetst(); + targets.prefix = &f.body; + targets.suffix = &tmp_end_function; targets.set_return(end_function); targets.has_return_value = code_type.return_type().id() != ID_empty && code_type.return_type().id() != ID_constructor && @@ -235,6 +237,9 @@ void goto_convert_functionst::convert_function( f.make_hidden(); lifetime = parent_lifetime; + + targets.prefix = nullptr; + targets.suffix = nullptr; } void goto_convert(goto_modelt &goto_model, message_handlert &message_handler)