From 9ea5cedcfb9822800ba1f0a3b6935325e609e7e7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 21 Oct 2021 12:47:58 +0100 Subject: [PATCH] goto symex now handles function pointers --- src/goto-programs/process_goto_program.cpp | 9 ++- src/goto-symex/goto_symex.h | 17 +++--- src/goto-symex/symex_function_call.cpp | 67 +++++++++++++--------- 3 files changed, 56 insertions(+), 37 deletions(-) diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp index 57cbdd6115b..045606d23f4 100644 --- a/src/goto-programs/process_goto_program.cpp +++ b/src/goto-programs/process_goto_program.cpp @@ -40,9 +40,12 @@ bool process_goto_program( string_instrumentation(goto_model); // remove function pointers - log.status() << "Removal of function pointers and virtual functions" - << messaget::eom; - remove_function_pointers(log.get_message_handler(), goto_model, false); + if(options.get_bool_option("remove-function-pointers")) + { + log.status() << "Removal of function pointers and virtual functions" + << messaget::eom; + remove_function_pointers(log.get_message_handler(), goto_model, false); + } mm_io(goto_model); diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index c7fb2d37abe..cc2670eb1bb 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com class address_of_exprt; class code_function_callt; +class dereference_exprt; class function_application_exprt; class goto_symex_statet; class path_storaget; @@ -445,19 +446,19 @@ class goto_symext /// \param state: Symbolic execution state for current instruction virtual void symex_end_of_function(statet &); - /// Symbolic execution of a call to a function call. + /// Symbolic execution of a call to a function given via a pointer. /// \param get_goto_function: The delegate to retrieve function bodies (see /// \ref get_goto_functiont) /// \param state: Symbolic execution state for current instruction - /// \param lhs: nil or the lhs of the function call instruction - /// \param function: the symbol of the function to call - /// \param arguments: the arguments of the function call - virtual void symex_function_call_symbol( + /// \param lhs: nil or the lhs of the function call instruction, cleaned + /// \param function: the dereference expression for the function to call, cleaned + /// \param arguments: the arguments of the function call, cleaned + void symex_function_call_post_clean_rec( const get_goto_functiont &get_goto_function, statet &state, - const exprt &lhs, - const symbol_exprt &function, - const exprt::operandst &arguments); + const exprt &cleaned_lhs, + const exprt &cleaned_function, + const exprt::operandst &cleaned_arguments); /// Symbolic execution of a function call by inlining. /// Records the call in \p target by appending a function call step and: diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 096fe555ee4..577af4568e4 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -178,44 +178,59 @@ void goto_symext::symex_function_call( { const exprt &function = instruction.call_function(); - // If at some point symex_function_call can support more - // expression ids(), like ID_Dereference, please expand the - // precondition appropriately. - PRECONDITION(function.id() == ID_symbol); - - symex_function_call_symbol( - get_goto_function, - state, - instruction.call_lhs(), - to_symbol_expr(instruction.call_function()), - instruction.call_arguments()); -} + PRECONDITION(function.id() == ID_symbol || function.id() == ID_dereference); -void goto_symext::symex_function_call_symbol( - const get_goto_functiont &get_goto_function, - statet &state, - const exprt &lhs, - const symbol_exprt &function, - const exprt::operandst &arguments) -{ + // clean lhs exprt cleaned_lhs; - if(lhs.is_nil()) - cleaned_lhs = lhs; + if(instruction.call_lhs().is_nil()) + cleaned_lhs = nil_exprt(); else - cleaned_lhs = clean_expr(lhs, state, true); + cleaned_lhs = clean_expr(instruction.call_lhs(), state, true); - // no need to clean the function, which is a symbol only + // need to clean the function expression in case it's a dereference + auto cleaned_function = clean_expr(function, state, false); + // clean the arguments exprt::operandst cleaned_arguments; - for(auto &argument : arguments) + for(auto &argument : instruction.call_arguments()) cleaned_arguments.push_back(clean_expr(argument, state, false)); target.location(state.guard.as_expr(), state.source); - symex_function_call_post_clean( - get_goto_function, state, cleaned_lhs, function, cleaned_arguments); + // We get an if-then-else nest that contains symbols + // in the case of function pointers, and we traverse that recursively. + symex_function_call_post_clean_rec( + get_goto_function, state, cleaned_lhs, cleaned_function, cleaned_arguments); +} + +void goto_symext::symex_function_call_post_clean_rec( + const get_goto_functiont &get_goto_function, + statet &state, + const exprt &cleaned_lhs, + const exprt &cleaned_function, + const exprt::operandst &cleaned_arguments) +{ + if(cleaned_function.id() == ID_symbol) + { + symex_function_call_post_clean( + get_goto_function, + state, + cleaned_lhs, + to_symbol_expr(cleaned_function), + cleaned_arguments); + } + else if(cleaned_function.id() == ID_if) + { + DATA_INVARIANT_WITH_DIAGNOSTICS( + false, "todo", irep_pretty_diagnosticst(cleaned_function)); + } + else + DATA_INVARIANT_WITH_DIAGNOSTICS( + false, + "cleaned function is expected to consist of if and symbol", + irep_pretty_diagnosticst(cleaned_function)); } void goto_symext::symex_function_call_post_clean(