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)