cprover
remove_function_pointers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: 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>
20 #include <util/source_location.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 {
34 public:
36  message_handlert &_message_handler,
37  symbol_tablet &_symbol_table,
38  bool _add_safety_assertion,
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 
48 protected:
50  const namespacet ns;
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,
71  goto_programt::targett target);
72 
73  std::unordered_set<irep_idt> address_taken;
74 
75  typedef std::map<irep_idt, code_typet> type_mapt;
77 };
78 
80  message_handlert &_message_handler,
81  symbol_tablet &_symbol_table,
82  bool _add_safety_assertion,
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 
132  bool return_value_used,
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'
139  if(!return_value_used)
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
154  const code_typet::parameterst &call_parameters=call_type.parameters();
155  const code_typet::parameterst &function_parameters=function_type.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 
182 static void fix_argument_types(code_function_callt &function_call)
183 {
184  const code_typet &code_type = to_code_type(function_call.function().type());
185 
186  const code_typet::parameterst &function_parameters=
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 
205 static void fix_return_type(
206  const irep_idt &in_function_id,
207  code_function_callt &function_call,
208  symbol_tablet &symbol_table,
209  goto_programt &dest)
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 
225  symbolt &tmp_symbol = get_fresh_aux_symbol(
226  code_type.return_type(),
227  id2string(in_function_id),
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 
239  code_assignt(old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()))));
240 }
241 
243  goto_programt &goto_program,
244  const irep_idt &function_id,
245  goto_programt::targett target)
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();
267  does_remove_constt const_removal_check(goto_program, ns);
268  const auto does_remove_const = const_removal_check();
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 
336  symbol_table,
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 
363  join_strings(
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,
381  goto_programt::targett target,
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
389  goto_programt final_skip;
390 
391  goto_programt::targett t_final = final_skip.add(goto_programt::make_skip());
392 
393  // build the calls and gotos
394 
395  goto_programt new_code_calls;
396  goto_programt new_code_gotos;
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
405  fix_argument_types(new_call);
406 
407  goto_programt tmp;
408  fix_return_type(function_id, new_call, symbol_table, tmp);
409 
410  auto call = new_code_calls.add(goto_programt::make_function_call(new_call));
411  new_code_calls.destructive_append(tmp);
412 
413  // goto final
414  new_code_calls.add(goto_programt::make_goto(t_final, true_exprt()));
415 
416  // goto to call
417  const address_of_exprt address_of(fun, pointer_type(fun.type()));
418 
419  const auto casted_address =
420  typecast_exprt::conditional_cast(address_of, pointer.type());
421 
422  new_code_gotos.add(
423  goto_programt::make_goto(call, equal_exprt(pointer, casted_address)));
424  }
425 
426  // fall-through
427  if(add_safety_assertion)
428  {
430  new_code_gotos.add(goto_programt::make_assertion(false_exprt()));
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
440  new_code.destructive_append(new_code_gotos);
441  new_code.destructive_append(new_code_calls);
442  new_code.destructive_append(final_skip);
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 
458  goto_programt::targett next_target=target;
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.
465  code_expressiont code_expression(function);
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 
537  message_handlert &_message_handler,
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,
543  bool only_remove_const_fps)
544 {
546  rfp(
547  _message_handler,
548  symbol_table,
549  add_safety_assertion,
550  only_remove_const_fps,
551  goto_functions);
552 
553  return rfp.remove_function_pointers(goto_program, function_id);
554 }
555 
557  message_handlert &_message_handler,
558  symbol_tablet &symbol_table,
559  goto_functionst &goto_functions,
560  bool add_safety_assertion,
561  bool only_remove_const_fps)
562 {
564  rfp(
565  _message_handler,
566  symbol_table,
567  add_safety_assertion,
568  only_remove_const_fps,
569  goto_functions);
570 
571  rfp(goto_functions);
572 }
573 
575  goto_modelt &goto_model,
576  bool add_safety_assertion,
577  bool only_remove_const_fps)
578 {
580  _message_handler,
581  goto_model.symbol_table,
582  goto_model.goto_functions,
583  add_safety_assertion,
584  only_remove_const_fps);
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.
Definition: pointer_expr.h:361
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.
exprt::operandst argumentst
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:541
const typet & return_type() const
Definition: std_types.h:645
void remove_ellipsis()
Definition: std_types.h:640
bool has_ellipsis() const
Definition: std_types.h:611
const parameterst & parameters() const
Definition: std_types.h:655
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
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
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.
Definition: goto_program.h:73
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:934
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:706
instructionst::iterator targett
Definition: goto_program.h:592
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:698
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())
Definition: goto_program.h:880
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
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())
Definition: goto_program.h:922
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:942
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().
Definition: namespace.cpp:138
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)
const irep_idt & get_comment() const
void set_property_class(const irep_idt &property_class)
const irep_idt & get_property_class() 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.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
irep_idt mode
Language mode.
Definition: symbol.h:49
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.
Definition: pointer_expr.h:704
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)
Definition: race_check.cpp:109
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
Definition: remove_skip.cpp:88
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.
Definition: string_utils.h:62