diff --git a/regression/cbmc/Function_Pointer18/test.desc b/regression/cbmc/Function_Pointer18/test.desc index e255c4accf31..a06375958f38 100644 --- a/regression/cbmc/Function_Pointer18/test.desc +++ b/regression/cbmc/Function_Pointer18/test.desc @@ -1,11 +1,13 @@ CORE main.c -^EXIT=0$ -^SIGNAL=0$ -\[f2.assertion.1\] line [0-9]+ assertion 0: SUCCESS -\[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS +^\*\*\*\* WARNING: no body for function main::fptr_call +^\*\*\*\* WARNING: no body for function main::fptr_call\$0 +\[f2.assertion.1\] line [0-9]+ assertion 0: FAILURE +\[main.assertion.1\] line [0-9]+ assertion x == 1: FAILURE \[main.assertion.2\] line [0-9]+ assertion x == 2: SUCCESS -^VERIFICATION SUCCESSFUL$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc/Function_Pointer20/main.c b/regression/cbmc/Function_Pointer20/main.c new file mode 100644 index 000000000000..bfa3e4028423 --- /dev/null +++ b/regression/cbmc/Function_Pointer20/main.c @@ -0,0 +1,26 @@ +#include + +struct PtrWrapper +{ + char *value_c; +}; + +void fn(struct PtrWrapper wrapper) +{ + assert(wrapper.value_c == 'B'); +} + +void indirect(int (*fn_ptr)(char *), char *data) +{ + fn_ptr(data); + assert(0); +} + +int main() +{ + struct PtrWrapper wrapper; + wrapper.value_c = 'A'; + + int (*alias)(char *) = (int (*)(char *))fn; + indirect(alias, &wrapper.value_c); +} diff --git a/regression/cbmc/Function_Pointer20/test.desc b/regression/cbmc/Function_Pointer20/test.desc new file mode 100644 index 000000000000..5921de71cc71 --- /dev/null +++ b/regression/cbmc/Function_Pointer20/test.desc @@ -0,0 +1,10 @@ +CORE +main.c + +^\*\*\*\* WARNING: no body for function indirect::fptr_call +^\[indirect.assertion.1\] line 16 assertion 0: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc/Function_Pointer_Init_No_Candidate/main.c b/regression/cbmc/Function_Pointer_Init_No_Candidate/main.c index c19c7f2dee98..dc783a6502b1 100644 --- a/regression/cbmc/Function_Pointer_Init_No_Candidate/main.c +++ b/regression/cbmc/Function_Pointer_Init_No_Candidate/main.c @@ -4,9 +4,7 @@ typedef int (*other_function_type)(int n); void foo(other_function_type other_function) { - // returning from the function call is unreachable -> the following assertion - // should succeed - // requesting `pointer-check` will then catch the fact that there is no valid + // requesting `pointer-check` will catch the fact that there is no valid // candidate function to call resulting in an invalid function pointer // failure assert(other_function(4) > 5); diff --git a/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc b/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc index 01bd38d3647e..1de45e098875 100644 --- a/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc +++ b/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc @@ -1,7 +1,7 @@ CORE main.c --function foo --pointer-check -^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) > 5: SUCCESS$ +^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) > 5: FAILURE$ ^\[foo.pointer_dereference.\d+\] line \d+ no candidates for dereferenced function pointer: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/value-set-function-pointers-simple/test.desc b/regression/goto-analyzer/value-set-function-pointers-simple/test.desc index 604658c3d808..bee4fb417c43 100644 --- a/regression/goto-analyzer/value-set-function-pointers-simple/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-simple/test.desc @@ -10,7 +10,7 @@ main.c ^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\) :value-set-end ^main::1::fun2_show \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end ^main::1::fun3_show \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end -^fun_global_show \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end +^fun_global_show \(\) -> value-set-begin: TOP :value-set-end ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/value-set-fi-fp-removal5/test.desc b/regression/goto-instrument/value-set-fi-fp-removal5/test.desc index 637e25cc8354..9a92fcae4d3e 100644 --- a/regression/goto-instrument/value-set-fi-fp-removal5/test.desc +++ b/regression/goto-instrument/value-set-fi-fp-removal5/test.desc @@ -5,6 +5,7 @@ test.c ^SIGNAL=0$ ^file test.c line 19 function main: replacing function pointer by 0 possible targets$ -- +-- This test checks that the value-set-fi-based function pointer removal precisely identifies the function to call for a particular function pointer call. diff --git a/src/goto-instrument/value_set_fi_fp_removal.cpp b/src/goto-instrument/value_set_fi_fp_removal.cpp index 80e7c10d6f5e..b4f763eda98b 100644 --- a/src/goto-instrument/value_set_fi_fp_removal.cpp +++ b/src/goto-instrument/value_set_fi_fp_removal.cpp @@ -31,6 +31,7 @@ void value_set_fi_fp_removal( message.status() << "Instrumenting" << messaget::eom; // now replace aliases by addresses + std::list fall_back_fns; for(auto &f : goto_model.goto_functions.function_map) { for(auto target = f.second.body.instructions.begin(); @@ -69,18 +70,26 @@ void value_set_fi_fp_removal( if(functions.size() > 0) { - remove_function_pointer( + fall_back_fns.push_back(remove_function_pointer( message_handler, goto_model.symbol_table, f.second.body, f.first, target, functions, - true); + true)); } } } } } - goto_model.goto_functions.update(); + + for(const auto &id : fall_back_fns) + { + goto_model.goto_functions.function_map[id].set_parameter_identifiers( + to_code_type(ns.lookup(id).type)); + } + + if(!fall_back_fns.empty()) + goto_model.goto_functions.update(); } diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 5d1f373ec57f..6fc3c9f69143 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -36,21 +36,21 @@ class remove_function_pointerst public: remove_function_pointerst( message_handlert &_message_handler, - symbol_tablet &_symbol_table, + goto_modelt &goto_model, bool _add_safety_assertion, - bool only_resolve_const_fps, - const goto_functionst &goto_functions); + bool only_resolve_const_fps); - void operator()(goto_functionst &goto_functions); + void operator()(); - bool remove_function_pointers( + NODISCARD + std::list remove_function_pointers( goto_programt &goto_program, const irep_idt &function_id); protected: message_handlert &message_handler; + goto_modelt &goto_model; const namespacet ns; - symbol_tablet &symbol_table; bool add_safety_assertion; // We can optionally halt the FP removal if we aren't able to use @@ -67,7 +67,9 @@ class remove_function_pointerst /// \param goto_program: The goto program that contains target /// \param function_id: Name of function containing the target /// \param target: location with function call with function pointer - void remove_function_pointer( + /// \return Name of fall back function symbol, if any; this function must be + /// added to GOTO functions by the caller. + optionalt remove_function_pointer( goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target); @@ -80,23 +82,22 @@ class remove_function_pointerst remove_function_pointerst::remove_function_pointerst( message_handlert &_message_handler, - symbol_tablet &_symbol_table, + goto_modelt &goto_model, bool _add_safety_assertion, - bool only_resolve_const_fps, - const goto_functionst &goto_functions) + bool only_resolve_const_fps) : message_handler(_message_handler), - ns(_symbol_table), - symbol_table(_symbol_table), + goto_model(goto_model), + ns(goto_model.symbol_table), add_safety_assertion(_add_safety_assertion), only_resolve_const_fps(only_resolve_const_fps) { - for(const auto &s : symbol_table.symbols) + for(const auto &s : goto_model.symbol_table.symbols) compute_address_taken_functions(s.second.value, address_taken); - compute_address_taken_functions(goto_functions, address_taken); + compute_address_taken_functions(goto_model.goto_functions, address_taken); // build type map - for(const auto &gf_entry : goto_functions.function_map) + for(const auto &gf_entry : goto_model.goto_functions.function_map) { type_map.emplace( gf_entry.first, to_code_type(ns.lookup(gf_entry.first).type)); @@ -208,6 +209,7 @@ static void fix_argument_types(code_function_callt &function_call) static void fix_return_type( const irep_idt &in_function_id, + const source_locationt &source_location, code_function_callt &function_call, symbol_tablet &symbol_table, goto_programt &dest) @@ -230,7 +232,7 @@ static void fix_return_type( code_type.return_type(), id2string(in_function_id), "tmp_return_val_" + id2string(function_symbol.base_name), - function_call.source_location(), + source_location, function_symbol.mode, symbol_table); @@ -239,13 +241,14 @@ static void fix_return_type( exprt old_lhs=function_call.lhs(); function_call.lhs()=tmp_symbol_expr; - dest.add(goto_programt::make_assignment(code_assignt( + dest.add(goto_programt::make_assignment( old_lhs, make_byte_extract( - tmp_symbol_expr, from_integer(0, c_index_type()), old_lhs.type())))); + tmp_symbol_expr, from_integer(0, c_index_type()), old_lhs.type()), + source_location)); } -void remove_function_pointerst::remove_function_pointer( +optionalt remove_function_pointerst::remove_function_pointer( goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target) @@ -284,7 +287,7 @@ void remove_function_pointerst::remove_function_pointer( else { remove_const_function_pointerst fpr( - log.get_message_handler(), ns, symbol_table); + log.get_message_handler(), ns, goto_model.symbol_table); found_functions=fpr(pointer, functions); @@ -297,7 +300,7 @@ void remove_function_pointerst::remove_function_pointer( if(functions.size()==1) { target->call_function() = *functions.cbegin(); - return; + return {}; } } @@ -311,7 +314,7 @@ void remove_function_pointerst::remove_function_pointer( // Since we haven't found functions, we would now resort to // replacing the function pointer with any function with a valid signature // Since we don't want to do that, we abort. - return; + return {}; } bool return_value_used = as_const(*target).call_lhs().is_not_nil(); @@ -337,9 +340,9 @@ void remove_function_pointerst::remove_function_pointer( } } - ::remove_function_pointer( + return ::remove_function_pointer( message_handler, - symbol_table, + goto_model.symbol_table, goto_program, function_id, target, @@ -379,7 +382,7 @@ static std::string function_pointer_assertion_comment( return comment.str(); } -void remove_function_pointer( +irep_idt remove_function_pointer( message_handlert &message_handler, symbol_tablet &symbol_table, goto_programt &goto_program, @@ -388,13 +391,15 @@ void remove_function_pointer( const std::unordered_set &functions, const bool add_safety_assertion) { + const auto &source_location = target->source_location(); const exprt &function = target->call_function(); const exprt &pointer = to_dereference_expr(function).pointer(); // the final target is a skip goto_programt final_skip; - goto_programt::targett t_final = final_skip.add(goto_programt::make_skip()); + goto_programt::targett t_final = + final_skip.add(goto_programt::make_skip(source_location)); // build the calls and gotos @@ -411,13 +416,15 @@ void remove_function_pointer( fix_argument_types(new_call); goto_programt tmp; - fix_return_type(function_id, new_call, symbol_table, tmp); + fix_return_type(function_id, source_location, new_call, symbol_table, tmp); - auto call = new_code_calls.add(goto_programt::make_function_call(new_call)); + auto call = new_code_calls.add( + goto_programt::make_function_call(new_call, source_location)); new_code_calls.destructive_append(tmp); // goto final - new_code_calls.add(goto_programt::make_goto(t_final, true_exprt())); + new_code_calls.add( + goto_programt::make_goto(t_final, true_exprt(), source_location)); // goto to call const address_of_exprt address_of(fun, pointer_type(fun.type())); @@ -425,20 +432,34 @@ void remove_function_pointer( const auto casted_address = typecast_exprt::conditional_cast(address_of, pointer.type()); - new_code_gotos.add( - goto_programt::make_goto(call, equal_exprt(pointer, casted_address))); + new_code_gotos.add(goto_programt::make_goto( + call, equal_exprt(pointer, casted_address), source_location)); } - // fall-through + // fall-through -- create a fresh function (without body) that will be called; + // generate-function-body can be used to decide the behavior of this new + // function if(add_safety_assertion) { - goto_programt::targett t = - new_code_gotos.add(goto_programt::make_assertion(false_exprt())); + goto_programt::targett t = new_code_gotos.add( + goto_programt::make_assertion(false_exprt(), source_location)); t->source_location_nonconst().set_property_class("pointer dereference"); t->source_location_nonconst().set_comment( function_pointer_assertion_comment(functions)); } - new_code_gotos.add(goto_programt::make_assumption(false_exprt())); + symbolt &fall_back_fn_symbol = get_fresh_aux_symbol( + function.type(), + id2string(function_id), + "fptr_call", + source_location, + symbol_table.lookup_ref(function_id).mode, + symbol_table); + fall_back_fn_symbol.is_file_local = true; + new_code_gotos.add(goto_programt::make_function_call( + target->call_lhs(), + fall_back_fn_symbol.symbol_expr(), + target->call_arguments(), + source_location)); goto_programt new_code; @@ -447,35 +468,17 @@ void remove_function_pointer( new_code.destructive_append(new_code_calls); new_code.destructive_append(final_skip); - // set locations - for(auto &instruction : new_code.instructions) - { - source_locationt &source_location = instruction.source_location_nonconst(); - - irep_idt property_class = source_location.get_property_class(); - irep_idt comment = source_location.get_comment(); - source_location = target->source_location(); - if(!property_class.empty()) - source_location.set_property_class(property_class); - if(!comment.empty()) - source_location.set_comment(comment); - } - - goto_programt::targett next_target=target; - next_target++; - - goto_program.destructive_insert(next_target, new_code); + goto_program.destructive_insert(std::next(target), new_code); // We preserve the original dereferencing to possibly catch // further pointer-related errors. code_expressiont code_expression(function); code_expression.add_source_location()=function.source_location(); - *target = - goto_programt::make_other(code_expression, target->source_location()); + *target = goto_programt::make_other(code_expression, source_location); // report statistics messaget log{message_handler}; - log.statistics().source_location = target->source_location(); + log.statistics().source_location = source_location; log.statistics() << "replacing function pointer by " << functions.size() << " possible targets" << messaget::eom; @@ -496,96 +499,65 @@ void remove_function_pointer( mstream << messaget::eom; }); + + return fall_back_fn_symbol.name; } -bool remove_function_pointerst::remove_function_pointers( +std::list remove_function_pointerst::remove_function_pointers( goto_programt &goto_program, const irep_idt &function_id) { - bool did_something=false; + std::list fall_back_fns; Forall_goto_program_instructions(target, goto_program) if(target->is_function_call()) { if(target->call_function().id() == ID_dereference) { - remove_function_pointer(goto_program, function_id, target); - did_something=true; + auto fall_back = + remove_function_pointer(goto_program, function_id, target); + if(fall_back.has_value()) + fall_back_fns.push_back(*fall_back); } } - if(did_something) + if(!fall_back_fns.empty()) remove_skip(goto_program); - return did_something; + return fall_back_fns; } -void remove_function_pointerst::operator()(goto_functionst &functions) +void remove_function_pointerst::operator()() { - bool did_something=false; + std::list fall_back_fns; - for(goto_functionst::function_mapt::iterator f_it= - functions.function_map.begin(); - f_it!=functions.function_map.end(); - f_it++) + for(auto &f_entry : goto_model.goto_functions.function_map) { - goto_programt &goto_program=f_it->second.body; + goto_programt &goto_program = f_entry.second.body; - if(remove_function_pointers(goto_program, f_it->first)) - did_something=true; + fall_back_fns.splice( + fall_back_fns.end(), + remove_function_pointers(goto_program, f_entry.first)); } - if(did_something) - functions.compute_location_numbers(); -} + for(const auto &id : fall_back_fns) + { + goto_model.goto_functions.function_map[id].set_parameter_identifiers( + to_code_type(goto_model.symbol_table.lookup_ref(id).type)); + } -bool remove_function_pointers( - message_handlert &_message_handler, - symbol_tablet &symbol_table, - const goto_functionst &goto_functions, - goto_programt &goto_program, - const irep_idt &function_id, - bool add_safety_assertion, - bool only_remove_const_fps) -{ - remove_function_pointerst - rfp( - _message_handler, - symbol_table, - add_safety_assertion, - only_remove_const_fps, - goto_functions); - - return rfp.remove_function_pointers(goto_program, function_id); + if(!fall_back_fns.empty()) + goto_model.goto_functions.update(); } void remove_function_pointers( message_handlert &_message_handler, - symbol_tablet &symbol_table, - goto_functionst &goto_functions, - bool add_safety_assertion, - bool only_remove_const_fps) -{ - remove_function_pointerst - rfp( - _message_handler, - symbol_table, - add_safety_assertion, - only_remove_const_fps, - goto_functions); - - rfp(goto_functions); -} - -void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, bool add_safety_assertion, bool only_remove_const_fps) { - remove_function_pointers( - _message_handler, - goto_model.symbol_table, - goto_model.goto_functions, - add_safety_assertion, - only_remove_const_fps); + remove_function_pointerst rfp{ + _message_handler, goto_model, add_safety_assertion, only_remove_const_fps}; + + rfp(); } diff --git a/src/goto-programs/remove_function_pointers.h b/src/goto-programs/remove_function_pointers.h index ccbfd308847d..0d24f5b1a200 100644 --- a/src/goto-programs/remove_function_pointers.h +++ b/src/goto-programs/remove_function_pointers.h @@ -14,6 +14,8 @@ Date: June 2003 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H #define CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H +#include + #include "goto_program.h" #include @@ -31,22 +33,6 @@ void remove_function_pointers( bool add_safety_assertion, bool only_remove_const_fps=false); -void remove_function_pointers( - message_handlert &_message_handler, - symbol_tablet &symbol_table, - goto_functionst &goto_functions, - bool add_safety_assertion, - bool only_remove_const_fps=false); - -bool remove_function_pointers( - message_handlert &_message_handler, - symbol_tablet &symbol_table, - const goto_functionst &goto_functions, - goto_programt &goto_program, - const irep_idt &function_id, - bool add_safety_assertion, - bool only_remove_const_fps = false); - /// Replace a call to a dynamic function at location /// target in the given goto-program by a case-split /// over a given set of functions @@ -57,8 +43,10 @@ bool remove_function_pointers( /// \param target: location with function call with function pointer /// \param functions: The set of functions to consider /// \param add_safety_assertion: Iff true, include an assertion that the -// pointer matches one of the candidate functions -void remove_function_pointer( +/// pointer matches one of the candidate functions +/// \return Name of fall back function symbol; this function must be added to +/// GOTO functions by the caller. +NODISCARD irep_idt remove_function_pointer( message_handlert &message_handler, symbol_tablet &symbol_table, goto_programt &goto_program, diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index 56b29c333656..3555a4e5ea90 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -35,7 +35,8 @@ void for_each_function_call(GotoFunctionT &&goto_function, Handler handler) handler); } -static void restrict_function_pointer( +NODISCARD +static optionalt restrict_function_pointer( message_handlert &message_handler, symbol_tablet &symbol_table, goto_programt &goto_program, @@ -54,7 +55,7 @@ static void restrict_function_pointer( const auto &original_function = location->call_function(); if(!can_cast_expr(original_function)) - return; + return {}; // because we run the label function pointer calls transformation pass before // this stage a dereference can only dereference a symbol expression @@ -66,14 +67,14 @@ static void restrict_function_pointer( restrictions.restrictions.find(pointer_symbol.get_identifier()); if(restriction_iterator == restrictions.restrictions.end()) - return; + return {}; const namespacet ns(symbol_table); std::unordered_set candidates; for(const auto &candidate : restriction_iterator->second) candidates.insert(ns.lookup(candidate).symbol_expr()); - remove_function_pointer( + return remove_function_pointer( message_handler, symbol_table, goto_program, @@ -177,20 +178,32 @@ void restrict_function_pointers( if(restrictions.restrictions.empty()) return; + std::list fall_back_fns; for(auto &function_item : goto_model.goto_functions.function_map) { goto_functiont &goto_function = function_item.second; for_each_function_call(goto_function, [&](const goto_programt::targett it) { - restrict_function_pointer( + auto fall_back_fn_opt = restrict_function_pointer( message_handler, goto_model.symbol_table, goto_function.body, function_item.first, restrictions, it); + if(fall_back_fn_opt.has_value()) + fall_back_fns.push_back(*fall_back_fn_opt); }); } + + for(const auto &id : fall_back_fns) + { + goto_model.goto_functions.function_map[id].set_parameter_identifiers( + to_code_type(goto_model.symbol_table.lookup_ref(id).type)); + } + + if(!fall_back_fns.empty()) + goto_model.goto_functions.update(); } void parse_function_pointer_restriction_options_from_cmdline(