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_expr.h>
22 
24 
26 #include "goto_model.h"
28 #include "remove_skip.h"
29 
31 {
32 public:
34  message_handlert &_message_handler,
35  symbol_tablet &_symbol_table,
36  bool _add_safety_assertion,
38  const goto_functionst &goto_functions);
39 
40  void operator()(goto_functionst &goto_functions);
41 
43  goto_programt &goto_program,
44  const irep_idt &function_id);
45 
46  // a set of function symbols
48 
57  goto_programt &goto_program,
58  const irep_idt &function_id,
60  const functionst &functions);
61 
62 protected:
64  const namespacet ns;
67 
68  // We can optionally halt the FP removal if we aren't able to use
69  // remove_const_function_pointerst to successfully narrow to a small
70  // subset of possible functions and just leave the function pointer
71  // as it is.
72  // This can be activated in goto-instrument using
73  // --remove-const-function-pointers instead of --remove-function-pointers
75 
83  goto_programt &goto_program,
84  const irep_idt &function_id,
85  goto_programt::targett target);
86 
87  std::unordered_set<irep_idt> address_taken;
88 
89  typedef std::map<irep_idt, code_typet> type_mapt;
91 
92  bool is_type_compatible(
93  bool return_value_used,
94  const code_typet &call_type,
95  const code_typet &function_type);
96 
98  const typet &call_type,
99  const typet &function_type);
100 
101  void fix_argument_types(code_function_callt &function_call);
102  void fix_return_type(
103  const irep_idt &in_function_id,
104  code_function_callt &function_call,
105  goto_programt &dest);
106 };
107 
109  message_handlert &_message_handler,
110  symbol_tablet &_symbol_table,
111  bool _add_safety_assertion,
112  bool only_resolve_const_fps,
113  const goto_functionst &goto_functions)
114  : log(_message_handler),
115  ns(_symbol_table),
116  symbol_table(_symbol_table),
117  add_safety_assertion(_add_safety_assertion),
118  only_resolve_const_fps(only_resolve_const_fps)
119 {
120  for(const auto &s : symbol_table.symbols)
122 
124 
125  // build type map
126  for(const auto &gf_entry : goto_functions.function_map)
127  {
128  type_map.emplace(
129  gf_entry.first, to_code_type(ns.lookup(gf_entry.first).type));
130  }
131 }
132 
134  const typet &call_type,
135  const typet &function_type)
136 {
137  if(call_type == function_type)
138  return true;
139 
140  // any integer-vs-enum-vs-pointer is ok
141  if(
142  call_type.id() == ID_signedbv || call_type.id() == ID_unsigned ||
143  call_type.id() == ID_bool || call_type.id() == ID_c_bool ||
144  call_type.id() == ID_c_enum_tag || call_type.id() == ID_c_enum ||
145  call_type.id() == ID_pointer)
146  {
147  return function_type.id() == ID_signedbv ||
148  function_type.id() == ID_unsigned || function_type.id() == ID_bool ||
149  function_type.id() == ID_c_bool ||
150  function_type.id() == ID_pointer ||
151  function_type.id() == ID_c_enum ||
152  function_type.id() == ID_c_enum_tag;
153  }
154 
155  return pointer_offset_bits(call_type, ns) ==
156  pointer_offset_bits(function_type, ns);
157 }
158 
160  bool return_value_used,
161  const code_typet &call_type,
162  const code_typet &function_type)
163 {
164  // we are willing to ignore anything that's returned
165  // if we call with 'void'
166  if(!return_value_used)
167  {
168  }
169  else if(call_type.return_type() == empty_typet())
170  {
171  // ok
172  }
173  else
174  {
175  if(!arg_is_type_compatible(call_type.return_type(),
176  function_type.return_type()))
177  return false;
178  }
179 
180  // let's look at the parameters
181  const code_typet::parameterst &call_parameters=call_type.parameters();
182  const code_typet::parameterst &function_parameters=function_type.parameters();
183 
184  if(function_type.has_ellipsis() &&
185  function_parameters.empty())
186  {
187  // always ok
188  }
189  else if(call_type.has_ellipsis() &&
190  call_parameters.empty())
191  {
192  // always ok
193  }
194  else
195  {
196  // we are quite strict here, could be much more generous
197  if(call_parameters.size()!=function_parameters.size())
198  return false;
199 
200  for(std::size_t i=0; i<call_parameters.size(); i++)
201  if(!arg_is_type_compatible(call_parameters[i].type(),
202  function_parameters[i].type()))
203  return false;
204  }
205 
206  return true;
207 }
208 
210  code_function_callt &function_call)
211 {
212  const code_typet &code_type = to_code_type(function_call.function().type());
213 
214  const code_typet::parameterst &function_parameters=
215  code_type.parameters();
216 
217  code_function_callt::argumentst &call_arguments=
218  function_call.arguments();
219 
220  for(std::size_t i=0; i<function_parameters.size(); i++)
221  {
222  if(i<call_arguments.size())
223  {
224  if(call_arguments[i].type() != function_parameters[i].type())
225  {
226  call_arguments[i] =
227  typecast_exprt(call_arguments[i], function_parameters[i].type());
228  }
229  }
230  }
231 }
232 
234  const irep_idt &in_function_id,
235  code_function_callt &function_call,
236  goto_programt &dest)
237 {
238  // are we returning anything at all?
239  if(function_call.lhs().is_nil())
240  return;
241 
242  const code_typet &code_type = to_code_type(function_call.function().type());
243 
244  // type already ok?
245  if(function_call.lhs().type() == code_type.return_type())
246  return;
247 
248  const symbolt &function_symbol =
249  ns.lookup(to_symbol_expr(function_call.function()).get_identifier());
250 
251  symbolt &tmp_symbol = get_fresh_aux_symbol(
252  code_type.return_type(),
253  id2string(in_function_id),
254  "tmp_return_val_" + id2string(function_symbol.base_name),
255  function_call.source_location(),
256  function_symbol.mode,
257  symbol_table);
258 
259  const symbol_exprt tmp_symbol_expr = tmp_symbol.symbol_expr();
260 
261  exprt old_lhs=function_call.lhs();
262  function_call.lhs()=tmp_symbol_expr;
263 
265  code_assignt(old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()))));
266 }
267 
269  goto_programt &goto_program,
270  const irep_idt &function_id,
271  goto_programt::targett target)
272 {
273  const auto &function = to_dereference_expr(as_const(*target).call_function());
274 
275  // this better have the right type
276  code_typet call_type=to_code_type(function.type());
277 
278  // refine the type in case the forward declaration was incomplete
279  if(call_type.has_ellipsis() &&
280  call_type.parameters().empty())
281  {
282  call_type.remove_ellipsis();
283  for(const auto &argument : as_const(*target).call_arguments())
284  {
285  call_type.parameters().push_back(code_typet::parametert(argument.type()));
286  }
287  }
288 
289  bool found_functions;
290 
291  const exprt &pointer = function.pointer();
293  does_remove_constt const_removal_check(goto_program, ns);
294  const auto does_remove_const = const_removal_check();
295  if(does_remove_const.first)
296  {
297  log.warning().source_location = does_remove_const.second;
298  log.warning() << "cast from const to non-const pointer found, "
299  << "only worst case function pointer removal will be done."
300  << messaget::eom;
301  found_functions=false;
302  }
303  else
304  {
307 
308  found_functions=fpr(pointer, functions);
309 
310  // if found_functions is false, functions should be empty
311  // however, it is possible for found_functions to be true and functions
312  // to be empty (this happens if the pointer can only resolve to the null
313  // pointer)
314  CHECK_RETURN(found_functions || functions.empty());
315 
316  if(functions.size()==1)
317  {
318  target->call_function() = *functions.cbegin();
319  return;
320  }
321  }
322 
323  if(!found_functions)
324  {
326  {
327  // If this mode is enabled, we only remove function pointers
328  // that we can resolve either to an exact function, or an exact subset
329  // (e.g. a variable index in a constant array).
330  // Since we haven't found functions, we would now resort to
331  // replacing the function pointer with any function with a valid signature
332  // Since we don't want to do that, we abort.
333  return;
334  }
335 
336  bool return_value_used = as_const(*target).call_lhs().is_not_nil();
337 
338  // get all type-compatible functions
339  // whose address is ever taken
340  for(const auto &t : type_map)
341  {
342  // address taken?
343  if(address_taken.find(t.first)==address_taken.end())
344  continue;
345 
346  // type-compatible?
347  if(!is_type_compatible(return_value_used, call_type, t.second))
348  continue;
349 
350  if(t.first=="pthread_mutex_cleanup")
351  continue;
352 
353  symbol_exprt expr(t.first, t.second);
354  functions.insert(expr);
355  }
356  }
357 
358  remove_function_pointer(goto_program, function_id, target, functions);
359 }
360 
362  goto_programt &goto_program,
363  const irep_idt &function_id,
364  goto_programt::targett target,
365  const functionst &functions)
366 {
367  const exprt &function = target->call_function();
368  const exprt &pointer = to_dereference_expr(function).pointer();
369 
370  // the final target is a skip
371  goto_programt final_skip;
372 
373  goto_programt::targett t_final = final_skip.add(goto_programt::make_skip());
374 
375  // build the calls and gotos
376 
377  goto_programt new_code_calls;
378  goto_programt new_code_gotos;
379 
380  for(const auto &fun : functions)
381  {
382  // call function
383  auto new_call =
384  code_function_callt(target->call_lhs(), fun, target->call_arguments());
385 
386  // the signature of the function might not match precisely
387  fix_argument_types(new_call);
388 
389  goto_programt tmp;
390  fix_return_type(function_id, new_call, tmp);
391 
392  auto call = new_code_calls.add(goto_programt::make_function_call(new_call));
393  new_code_calls.destructive_append(tmp);
394 
395  // goto final
396  new_code_calls.add(goto_programt::make_goto(t_final, true_exprt()));
397 
398  // goto to call
399  const address_of_exprt address_of(fun, pointer_type(fun.type()));
400 
401  const auto casted_address =
402  typecast_exprt::conditional_cast(address_of, pointer.type());
403 
404  new_code_gotos.add(
405  goto_programt::make_goto(call, equal_exprt(pointer, casted_address)));
406  }
407 
408  // fall-through
410  {
412  new_code_gotos.add(goto_programt::make_assertion(false_exprt()));
413  t->source_location.set_property_class("pointer dereference");
414  t->source_location.set_comment("invalid function pointer");
415  }
417 
418  goto_programt new_code;
419 
420  // patch them all together
421  new_code.destructive_append(new_code_gotos);
422  new_code.destructive_append(new_code_calls);
423  new_code.destructive_append(final_skip);
424 
425  // set locations
426  for(auto &instruction : new_code.instructions)
427  {
428  source_locationt &source_location = instruction.source_location;
429 
430  irep_idt property_class = source_location.get_property_class();
431  irep_idt comment = source_location.get_comment();
432  source_location = target->source_location;
433  if(!property_class.empty())
434  source_location.set_property_class(property_class);
435  if(!comment.empty())
436  source_location.set_comment(comment);
437  }
438 
439  goto_programt::targett next_target=target;
440  next_target++;
441 
442  goto_program.destructive_insert(next_target, new_code);
443 
444  // We preserve the original dereferencing to possibly catch
445  // further pointer-related errors.
446  code_expressiont code_expression(function);
447  code_expression.add_source_location()=function.source_location();
448  target->code_nonconst().swap(code_expression);
449  target->type=OTHER;
450 
451  // report statistics
452  log.statistics().source_location = target->source_location;
453  log.statistics() << "replacing function pointer by " << functions.size()
454  << " possible targets" << messaget::eom;
455 
456  // list the names of functions when verbosity is at debug level
458  log.debug(), [&functions](messaget::mstreamt &mstream) {
459  mstream << "targets: ";
460 
461  bool first = true;
462  for(const auto &function : functions)
463  {
464  if(!first)
465  mstream << ", ";
466 
467  mstream << function.get_identifier();
468  first = false;
469  }
470 
471  mstream << messaget::eom;
472  });
473 }
474 
476  goto_programt &goto_program,
477  const irep_idt &function_id)
478 {
479  bool did_something=false;
480 
481  Forall_goto_program_instructions(target, goto_program)
482  if(target->is_function_call())
483  {
484  if(target->call_function().id() == ID_dereference)
485  {
486  remove_function_pointer(goto_program, function_id, target);
487  did_something=true;
488  }
489  }
490 
491  if(did_something)
492  remove_skip(goto_program);
493 
494  return did_something;
495 }
496 
498 {
499  bool did_something=false;
500 
501  for(goto_functionst::function_mapt::iterator f_it=
502  functions.function_map.begin();
503  f_it!=functions.function_map.end();
504  f_it++)
505  {
506  goto_programt &goto_program=f_it->second.body;
507 
508  if(remove_function_pointers(goto_program, f_it->first))
509  did_something=true;
510  }
511 
512  if(did_something)
513  functions.compute_location_numbers();
514 }
515 
517  message_handlert &_message_handler,
518  symbol_tablet &symbol_table,
519  const goto_functionst &goto_functions,
520  goto_programt &goto_program,
521  const irep_idt &function_id,
522  bool add_safety_assertion,
523  bool only_remove_const_fps)
524 {
526  rfp(
527  _message_handler,
528  symbol_table,
529  add_safety_assertion,
530  only_remove_const_fps,
531  goto_functions);
532 
533  return rfp.remove_function_pointers(goto_program, function_id);
534 }
535 
537  message_handlert &_message_handler,
538  symbol_tablet &symbol_table,
539  goto_functionst &goto_functions,
540  bool add_safety_assertion,
541  bool only_remove_const_fps)
542 {
544  rfp(
545  _message_handler,
546  symbol_table,
547  add_safety_assertion,
548  only_remove_const_fps,
549  goto_functions);
550 
551  rfp(goto_functions);
552 }
553 
555  goto_modelt &goto_model,
556  bool add_safety_assertion,
557  bool only_remove_const_fps)
558 {
560  _message_handler,
561  goto_model.symbol_table,
562  goto_model.goto_functions,
563  add_safety_assertion,
564  only_remove_const_fps);
565 }
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:243
Operator to return the address of an object.
Definition: pointer_expr.h:341
A codet representing an assignment in the program.
Definition: std_code.h:293
codet representation of an expression statement.
Definition: std_code.h:1840
codet representation of a function call statement.
Definition: std_code.h:1213
exprt & function()
Definition: std_code.h:1248
argumentst & arguments()
Definition: std_code.h:1258
exprt::operandst argumentst
Definition: std_code.h:1222
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:2811
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:71
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:963
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:744
instructionst::iterator targett
Definition: goto_program.h:646
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:736
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:909
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:753
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:951
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:453
bool is_nil() const
Definition: irep.h:387
source_locationt source_location
Definition: message.h:247
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & statistics() const
Definition: message.h:419
mstreamt & warning() const
Definition: message.h:404
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition: message.cpp:139
mstreamt & debug() const
Definition: message.h:429
message_handlert & get_message_handler()
Definition: message.h:184
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)
bool is_type_compatible(bool return_value_used, const code_typet &call_type, const code_typet &function_type)
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)
void fix_return_type(const irep_idt &in_function_id, code_function_callt &function_call, goto_programt &dest)
bool arg_is_type_compatible(const typet &call_type, const typet &function_type)
std::unordered_set< irep_idt > address_taken
void remove_function_pointer(goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target, const functionst &functions)
Replace a call to a dynamic function at location target in the given goto-program by a case-split ove...
remove_const_function_pointerst::functionst functionst
void fix_argument_types(code_function_callt &function_call)
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:2802
Semantic type conversion.
Definition: std_expr.h:1866
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
The type of an expression, extends irept.
Definition: type.h:28
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)
@ OTHER
Definition: goto_program.h:35
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:684
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
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 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:86
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