82 bool only_resolve_const_fps,
84 : message_handler(_message_handler),
86 symbol_table(_symbol_table),
87 only_resolve_const_fps(only_resolve_const_fps)
103 const typet &call_type,
104 const typet &function_type,
107 if(call_type == function_type)
112 call_type.
id() == ID_signedbv || call_type.
id() == ID_unsignedbv ||
113 call_type.
id() == ID_bool || call_type.
id() == ID_c_bool ||
114 call_type.
id() == ID_c_enum_tag || call_type.
id() == ID_c_enum ||
115 call_type.
id() == ID_pointer)
117 return function_type.
id() == ID_signedbv ||
118 function_type.
id() == ID_unsignedbv ||
119 function_type.
id() == ID_bool || function_type.
id() == ID_c_bool ||
120 function_type.
id() == ID_pointer ||
121 function_type.
id() == ID_c_enum ||
122 function_type.
id() == ID_c_enum_tag;
130 bool return_value_used,
137 if(!return_value_used)
156 function_parameters.empty())
161 call_parameters.empty())
168 if(call_parameters.size()!=function_parameters.size())
171 for(std::size_t i=0; i<call_parameters.size(); i++)
173 call_parameters[i].type(), function_parameters[i].type(), ns))
190 for(std::size_t i=0; i<function_parameters.size(); i++)
192 if(i<call_arguments.size())
194 if(call_arguments[i].type() != function_parameters[i].type())
199 function_parameters[i].type());
223 const symbolt &function_symbol =
231 function_symbol.
mode,
237 function_call.
lhs()=tmp_symbol_expr;
261 for(
const auto &argument :
as_const(*target).call_arguments())
267 bool found_functions;
269 const exprt &pointer =
function.pointer();
272 const auto does_remove_const = const_removal_check();
274 if(does_remove_const.first)
276 log.warning().source_location = does_remove_const.second;
277 log.warning() <<
"cast from const to non-const pointer found, "
278 <<
"only worst case function pointer removal will be done."
280 found_functions=
false;
287 found_functions=fpr(pointer, functions);
295 if(functions.size()==1)
297 target->call_function() = *functions.cbegin();
315 bool return_value_used =
as_const(*target).call_lhs().is_not_nil();
327 return_value_used, call_type, t.second,
ns))
330 if(t.first==
"pthread_mutex_cleanup")
334 functions.insert(expr);
348 const std::unordered_set<symbol_exprt, irep_hash> &candidates)
352 comment <<
"dereferenced function pointer must be ";
354 if(candidates.size() == 1)
356 comment << candidates.begin()->get_identifier();
358 else if(candidates.empty())
360 comment.str(
"no candidates for dereferenced function pointer");
371 [](
const symbol_exprt &s) { return s.get_identifier(); });
385 const std::unordered_set<symbol_exprt, irep_hash> &functions)
387 const exprt &
function = target->call_function();
401 for(
const auto &fun : functions)
412 function_id, new_call, target->source_location(), symbol_table, tmp);
414 auto call = new_code_calls.
add(
425 const auto casted_address =
462 log.statistics().source_location = target->source_location();
463 log.statistics() <<
"replacing function pointer by " << functions.size()
467 log.conditional_output(
469 mstream <<
"targets: ";
472 for(const auto &function : functions)
477 mstream << function.get_identifier();
489 bool did_something=
false;
492 if(target->is_function_call())
494 if(target->call_function().id() == ID_dereference)
504 return did_something;
509 bool did_something=
false;
511 for(goto_functionst::function_mapt::iterator f_it=
529 bool only_remove_const_fps)
534 only_remove_const_fps,
544 instruction.is_function_call() &&
545 instruction.call_function().id() == ID_dereference)
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
pointer_typet pointer_type(const typet &subtype)
bitvector_typet c_index_type()
Operator to return the address of an object.
codet representation of an expression statement.
goto_instruction_codet representation of a function call statement.
exprt::operandst argumentst
std::vector< parametert > parameterst
const typet & return_type() const
bool has_ellipsis() const
const parameterst & parameters() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
The Boolean constant false.
A collection of goto functions.
function_mapt function_map
void compute_location_numbers()
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
std::unordered_set< symbol_exprt, irep_hash > functionst
remove_function_pointerst(message_handlert &_message_handler, symbol_tablet &_symbol_table, bool only_resolve_const_fps, const goto_functionst &goto_functions)
std::map< irep_idt, code_typet > type_mapt
void operator()(goto_functionst &goto_functions)
message_handlert & message_handler
void remove_function_pointer(goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target)
Replace a call to a dynamic function at location target in the given goto-program by determining func...
symbol_tablet & symbol_table
std::unordered_set< irep_idt > address_taken
bool only_resolve_const_fps
bool remove_function_pointers(goto_programt &goto_program, const irep_idt &function_id)
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
irep_idt base_name
Base (non-scoped) name.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
irep_idt mode
Language mode.
The Boolean constant true.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
void compute_address_taken_functions(const exprt &src, std::unordered_set< irep_idt > &address_taken)
get all functions whose address is taken
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
static bool arg_is_type_compatible(const typet &call_type, const typet &function_type, const namespacet &ns)
void remove_function_pointer(message_handlert &message_handler, symbol_tablet &symbol_table, goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target, const std::unordered_set< symbol_exprt, irep_hash > &functions)
Replace a call to a dynamic function at location target in the given goto-program by a case-split ove...
bool function_is_type_compatible(bool return_value_used, const code_typet &call_type, const code_typet &function_type, const namespacet &ns)
Returns true iff call_type can be converted to produce a function call of the same type as function_t...
static std::string function_pointer_assertion_comment(const std::unordered_set< symbol_exprt, irep_hash > &candidates)
static void fix_argument_types(code_function_callt &function_call)
void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, bool only_remove_const_fps)
bool has_function_pointers(const goto_programt &goto_program)
static void fix_return_type(const irep_idt &in_function_id, code_function_callt &function_call, const source_locationt &source_location, symbol_tablet &symbol_table, goto_programt &dest)
Remove Indirect Function Calls.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define CHECK_RETURN(CONDITION)
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.