cprover
Loading...
Searching...
No Matches
remove_function_pointers.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include <util/c_types.h>
15#include <util/fresh_symbol.h>
16#include <util/invariant.h>
17#include <util/message.h>
18#include <util/pointer_expr.h>
21#include <util/std_code.h>
22#include <util/std_expr.h>
23#include <util/string_utils.h>
24
26
28#include "goto_model.h"
30#include "remove_skip.h"
31
33{
34public:
40 const goto_functionst &goto_functions);
41
42 void operator()(goto_functionst &goto_functions);
43
45 goto_programt &goto_program,
46 const irep_idt &function_id);
47
48protected:
53
54 // We can optionally halt the FP removal if we aren't able to use
55 // remove_const_function_pointerst to successfully narrow to a small
56 // subset of possible functions and just leave the function pointer
57 // as it is.
58 // This can be activated in goto-instrument using
59 // --remove-const-function-pointers instead of --remove-function-pointers
61
69 goto_programt &goto_program,
70 const irep_idt &function_id,
72
73 std::unordered_set<irep_idt> address_taken;
74
75 typedef std::map<irep_idt, code_typet> type_mapt;
77};
78
83 bool only_resolve_const_fps,
84 const goto_functionst &goto_functions)
85 : message_handler(_message_handler),
86 ns(_symbol_table),
87 symbol_table(_symbol_table),
88 add_safety_assertion(_add_safety_assertion),
89 only_resolve_const_fps(only_resolve_const_fps)
90{
91 for(const auto &s : symbol_table.symbols)
93
95
96 // build type map
97 for(const auto &gf_entry : goto_functions.function_map)
98 {
99 type_map.emplace(
100 gf_entry.first, to_code_type(ns.lookup(gf_entry.first).type));
101 }
102}
103
105 const typet &call_type,
106 const typet &function_type,
107 const namespacet &ns)
108{
109 if(call_type == function_type)
110 return true;
111
112 // any integer-vs-enum-vs-pointer is ok
113 if(
114 call_type.id() == ID_signedbv || call_type.id() == ID_unsigned ||
115 call_type.id() == ID_bool || call_type.id() == ID_c_bool ||
116 call_type.id() == ID_c_enum_tag || call_type.id() == ID_c_enum ||
117 call_type.id() == ID_pointer)
118 {
119 return function_type.id() == ID_signedbv ||
120 function_type.id() == ID_unsigned || function_type.id() == ID_bool ||
121 function_type.id() == ID_c_bool ||
122 function_type.id() == ID_pointer ||
123 function_type.id() == ID_c_enum ||
124 function_type.id() == ID_c_enum_tag;
125 }
126
127 return pointer_offset_bits(call_type, ns) ==
128 pointer_offset_bits(function_type, ns);
129}
130
133 const code_typet &call_type,
134 const code_typet &function_type,
135 const namespacet &ns)
136{
137 // we are willing to ignore anything that's returned
138 // if we call with 'void'
140 {
141 }
142 else if(call_type.return_type() == empty_typet())
143 {
144 // ok
145 }
146 else
147 {
149 call_type.return_type(), function_type.return_type(), ns))
150 return false;
151 }
152
153 // let's look at the parameters
156
157 if(function_type.has_ellipsis() &&
158 function_parameters.empty())
159 {
160 // always ok
161 }
162 else if(call_type.has_ellipsis() &&
163 call_parameters.empty())
164 {
165 // always ok
166 }
167 else
168 {
169 // we are quite strict here, could be much more generous
170 if(call_parameters.size()!=function_parameters.size())
171 return false;
172
173 for(std::size_t i=0; i<call_parameters.size(); i++)
175 call_parameters[i].type(), function_parameters[i].type(), ns))
176 return false;
177 }
178
179 return true;
180}
181
182static void fix_argument_types(code_function_callt &function_call)
183{
184 const code_typet &code_type = to_code_type(function_call.function().type());
185
187 code_type.parameters();
188
189 code_function_callt::argumentst &call_arguments=
190 function_call.arguments();
191
192 for(std::size_t i=0; i<function_parameters.size(); i++)
193 {
194 if(i<call_arguments.size())
195 {
196 if(call_arguments[i].type() != function_parameters[i].type())
197 {
198 call_arguments[i] =
199 typecast_exprt(call_arguments[i], function_parameters[i].type());
200 }
201 }
202 }
203}
204
205static void fix_return_type(
207 code_function_callt &function_call,
208 symbol_tablet &symbol_table,
210{
211 // are we returning anything at all?
212 if(function_call.lhs().is_nil())
213 return;
214
215 const code_typet &code_type = to_code_type(function_call.function().type());
216
217 // type already ok?
218 if(function_call.lhs().type() == code_type.return_type())
219 return;
220
221 const namespacet ns(symbol_table);
222 const symbolt &function_symbol =
223 ns.lookup(to_symbol_expr(function_call.function()).get_identifier());
224
226 code_type.return_type(),
228 "tmp_return_val_" + id2string(function_symbol.base_name),
229 function_call.source_location(),
230 function_symbol.mode,
231 symbol_table);
232
233 const symbol_exprt tmp_symbol_expr = tmp_symbol.symbol_expr();
234
235 exprt old_lhs=function_call.lhs();
236 function_call.lhs()=tmp_symbol_expr;
237
240}
241
243 goto_programt &goto_program,
244 const irep_idt &function_id,
246{
247 const auto &function = to_dereference_expr(as_const(*target).call_function());
248
249 // this better have the right type
250 code_typet call_type=to_code_type(function.type());
251
252 // refine the type in case the forward declaration was incomplete
253 if(call_type.has_ellipsis() &&
254 call_type.parameters().empty())
255 {
256 call_type.remove_ellipsis();
257 for(const auto &argument : as_const(*target).call_arguments())
258 {
259 call_type.parameters().push_back(code_typet::parametert(argument.type()));
260 }
261 }
262
263 bool found_functions;
264
265 const exprt &pointer = function.pointer();
270 if(does_remove_const.first)
271 {
272 log.warning().source_location = does_remove_const.second;
273 log.warning() << "cast from const to non-const pointer found, "
274 << "only worst case function pointer removal will be done."
275 << messaget::eom;
276 found_functions=false;
277 }
278 else
279 {
281 log.get_message_handler(), ns, symbol_table);
282
283 found_functions=fpr(pointer, functions);
284
285 // if found_functions is false, functions should be empty
286 // however, it is possible for found_functions to be true and functions
287 // to be empty (this happens if the pointer can only resolve to the null
288 // pointer)
289 CHECK_RETURN(found_functions || functions.empty());
290
291 if(functions.size()==1)
292 {
293 target->call_function() = *functions.cbegin();
294 return;
295 }
296 }
297
298 if(!found_functions)
299 {
301 {
302 // If this mode is enabled, we only remove function pointers
303 // that we can resolve either to an exact function, or an exact subset
304 // (e.g. a variable index in a constant array).
305 // Since we haven't found functions, we would now resort to
306 // replacing the function pointer with any function with a valid signature
307 // Since we don't want to do that, we abort.
308 return;
309 }
310
311 bool return_value_used = as_const(*target).call_lhs().is_not_nil();
312
313 // get all type-compatible functions
314 // whose address is ever taken
315 for(const auto &t : type_map)
316 {
317 // address taken?
318 if(address_taken.find(t.first)==address_taken.end())
319 continue;
320
321 // type-compatible?
323 return_value_used, call_type, t.second, ns))
324 continue;
325
326 if(t.first=="pthread_mutex_cleanup")
327 continue;
328
329 symbol_exprt expr(t.first, t.second);
330 functions.insert(expr);
331 }
332 }
333
337 goto_program,
338 function_id,
339 target,
340 functions,
342}
343
345 const std::unordered_set<symbol_exprt, irep_hash> &candidates)
346{
347 std::stringstream comment;
348
349 comment << "dereferenced function pointer must be ";
350
351 if(candidates.size() == 1)
352 {
353 comment << candidates.begin()->get_identifier();
354 }
355 else if(candidates.empty())
356 {
357 comment.str("no candidates for dereferenced function pointer");
358 }
359 else
360 {
361 comment << "one of [";
362
364 comment,
365 candidates.begin(),
366 candidates.end(),
367 ", ",
368 [](const symbol_exprt &s) { return s.get_identifier(); });
369
370 comment << ']';
371 }
372
373 return comment.str();
374}
375
377 message_handlert &message_handler,
378 symbol_tablet &symbol_table,
379 goto_programt &goto_program,
380 const irep_idt &function_id,
382 const std::unordered_set<symbol_exprt, irep_hash> &functions,
383 const bool add_safety_assertion)
384{
385 const exprt &function = target->call_function();
386 const exprt &pointer = to_dereference_expr(function).pointer();
387
388 // the final target is a skip
390
392
393 // build the calls and gotos
394
397
398 for(const auto &fun : functions)
399 {
400 // call function
401 auto new_call =
402 code_function_callt(target->call_lhs(), fun, target->call_arguments());
403
404 // the signature of the function might not match precisely
406
408 fix_return_type(function_id, new_call, symbol_table, tmp);
409
411 new_code_calls.destructive_append(tmp);
412
413 // goto final
415
416 // goto to call
418
419 const auto casted_address =
421
422 new_code_gotos.add(
424 }
425
426 // fall-through
427 if(add_safety_assertion)
428 {
431 t->source_location_nonconst().set_property_class("pointer dereference");
432 t->source_location_nonconst().set_comment(
434 }
436
437 goto_programt new_code;
438
439 // patch them all together
443
444 // set locations
445 for(auto &instruction : new_code.instructions)
446 {
447 source_locationt &source_location = instruction.source_location_nonconst();
448
449 irep_idt property_class = source_location.get_property_class();
450 irep_idt comment = source_location.get_comment();
451 source_location = target->source_location();
452 if(!property_class.empty())
453 source_location.set_property_class(property_class);
454 if(!comment.empty())
455 source_location.set_comment(comment);
456 }
457
459 next_target++;
460
461 goto_program.destructive_insert(next_target, new_code);
462
463 // We preserve the original dereferencing to possibly catch
464 // further pointer-related errors.
466 code_expression.add_source_location()=function.source_location();
467 *target =
468 goto_programt::make_other(code_expression, target->source_location());
469
470 // report statistics
471 messaget log{message_handler};
472 log.statistics().source_location = target->source_location();
473 log.statistics() << "replacing function pointer by " << functions.size()
474 << " possible targets" << messaget::eom;
475
476 // list the names of functions when verbosity is at debug level
477 log.conditional_output(
478 log.debug(), [&functions](messaget::mstreamt &mstream) {
479 mstream << "targets: ";
480
481 bool first = true;
482 for(const auto &function : functions)
483 {
484 if(!first)
485 mstream << ", ";
486
487 mstream << function.get_identifier();
488 first = false;
489 }
490
491 mstream << messaget::eom;
492 });
493}
494
496 goto_programt &goto_program,
497 const irep_idt &function_id)
498{
499 bool did_something=false;
500
501 Forall_goto_program_instructions(target, goto_program)
502 if(target->is_function_call())
503 {
504 if(target->call_function().id() == ID_dereference)
505 {
506 remove_function_pointer(goto_program, function_id, target);
507 did_something=true;
508 }
509 }
510
511 if(did_something)
512 remove_skip(goto_program);
513
514 return did_something;
515}
516
518{
519 bool did_something=false;
520
521 for(goto_functionst::function_mapt::iterator f_it=
522 functions.function_map.begin();
523 f_it!=functions.function_map.end();
524 f_it++)
525 {
526 goto_programt &goto_program=f_it->second.body;
527
528 if(remove_function_pointers(goto_program, f_it->first))
529 did_something=true;
530 }
531
532 if(did_something)
533 functions.compute_location_numbers();
534}
535
538 symbol_tablet &symbol_table,
539 const goto_functionst &goto_functions,
540 goto_programt &goto_program,
541 const irep_idt &function_id,
542 bool add_safety_assertion,
544{
546 rfp(
548 symbol_table,
549 add_safety_assertion,
551 goto_functions);
552
553 return rfp.remove_function_pointers(goto_program, function_id);
554}
555
558 symbol_tablet &symbol_table,
559 goto_functionst &goto_functions,
560 bool add_safety_assertion,
562{
564 rfp(
566 symbol_table,
567 add_safety_assertion,
569 goto_functions);
570
571 rfp(goto_functions);
572}
573
575 goto_modelt &goto_model,
576 bool add_safety_assertion,
578{
581 goto_model.symbol_table,
582 goto_model.goto_functions,
583 add_safety_assertion,
585}
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
A codet representing an assignment in the program.
codet representation of an expression statement.
Definition std_code.h:1394
codet representation of a function call statement.
Base type of functions.
Definition std_types.h:539
std::vector< parametert > parameterst
Definition std_types.h:542
const parameterst & parameters() const
Definition std_types.h:655
const typet & return_type() const
Definition std_types.h:645
bool has_ellipsis() const
Definition std_types.h:611
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
The empty type.
Definition std_types.h:51
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
const source_locationt & source_location() const
Definition expr.h:230
The Boolean constant false.
Definition std_expr.h:2865
A collection of goto functions.
function_mapt function_map
void compute_location_numbers()
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
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_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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
std::map< irep_idt, code_typet > type_mapt
void operator()(goto_functionst &goto_functions)
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...
remove_function_pointerst(message_handlert &_message_handler, symbol_tablet &_symbol_table, bool _add_safety_assertion, bool only_resolve_const_fps, const goto_functionst &goto_functions)
std::unordered_set< irep_idt > address_taken
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)
const irep_idt & get_property_class() const
const irep_idt & get_comment() const
Expression to hold a symbol (variable)
Definition std_expr.h:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Symbol table entry.
Definition symbol.h:28
The Boolean constant true.
Definition std_expr.h:2856
Semantic type conversion.
Definition std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
void compute_address_taken_functions(const exprt &src, std::unordered_set< irep_idt > &address_taken)
get all functions whose address is taken
Query Called Functions.
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.
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
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, const bool add_safety_assertion)
Replace a call to a dynamic function at location target in the given goto-program by a case-split ove...
static void fix_return_type(const irep_idt &in_function_id, code_function_callt &function_call, symbol_tablet &symbol_table, goto_programt &dest)
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...
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)
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)
Remove Indirect Function Calls.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
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.