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 <cassert>
15 
16 #include <util/fresh_symbol.h>
17 #include <util/replace_expr.h>
18 #include <util/source_location.h>
19 #include <util/std_expr.h>
20 #include <util/type_eq.h>
21 #include <util/message.h>
22 #include <util/base_type.h>
23 
25 #include <util/invariant.h>
26 
27 #include <util/c_types.h>
28 
29 #include "remove_skip.h"
32 
34 {
35 public:
37  message_handlert &_message_handler,
38  symbol_tablet &_symbol_table,
39  bool _add_safety_assertion,
41  const goto_functionst &goto_functions);
42 
43  void operator()(goto_functionst &goto_functions);
44 
46 
47 protected:
48  const namespacet ns;
51 
52  // We can optionally halt the FP removal if we aren't able to use
53  // remove_const_function_pointerst to successfully narrow to a small
54  // subset of possible functions and just leave the function pointer
55  // as it is.
56  // This can be activated in goto-instrument using
57  // --remove-const-function-pointers instead of --remove-function-pointers
59 
62  goto_programt::targett target);
63 
64  std::unordered_set<irep_idt> address_taken;
65 
66  typedef std::map<irep_idt, code_typet> type_mapt;
68 
69  bool is_type_compatible(
70  bool return_value_used,
71  const code_typet &call_type,
72  const code_typet &function_type);
73 
75  const typet &call_type,
76  const typet &function_type);
77 
78  void fix_argument_types(code_function_callt &function_call);
79  void fix_return_type(
80  code_function_callt &function_call,
81  goto_programt &dest);
82 
83  void
84  compute_address_taken_in_symbols(std::unordered_set<irep_idt> &address_taken)
85  {
87 
88  for(const auto &s : symbol_table.symbols)
90  }
91 };
92 
94  message_handlert &_message_handler,
95  symbol_tablet &_symbol_table,
96  bool _add_safety_assertion, bool only_resolve_const_fps,
97  const goto_functionst &goto_functions):
98  messaget(_message_handler),
99  ns(_symbol_table),
100  symbol_table(_symbol_table),
101  add_safety_assertion(_add_safety_assertion),
102  only_resolve_const_fps(only_resolve_const_fps)
103 {
106 
107  // build type map
108  forall_goto_functions(f_it, goto_functions)
109  type_map[f_it->first]=f_it->second.type;
110 }
111 
113  const typet &call_type,
114  const typet &function_type)
115 {
116  if(type_eq(call_type, function_type, ns))
117  return true;
118 
119  // any integer-vs-enum-vs-pointer is ok
120  if(call_type.id()==ID_signedbv ||
121  call_type.id()==ID_unsigned ||
122  call_type.id()==ID_bool ||
123  call_type.id()==ID_pointer ||
124  call_type.id()==ID_c_enum ||
125  call_type.id()==ID_c_enum_tag)
126  {
127  if(function_type.id()==ID_signedbv ||
128  function_type.id()==ID_unsigned ||
129  function_type.id()==ID_bool ||
130  function_type.id()==ID_pointer ||
131  function_type.id()==ID_c_enum ||
132  function_type.id()==ID_c_enum_tag)
133  return true;
134 
135  return false;
136  }
137 
138  // structs/unions need to match,
139  // which could be made more generous
140 
141  return false;
142 }
143 
145  bool return_value_used,
146  const code_typet &call_type,
147  const code_typet &function_type)
148 {
149  // we are willing to ignore anything that's returned
150  // if we call with 'void'
151  if(!return_value_used)
152  {
153  }
154  else if(type_eq(call_type.return_type(), empty_typet(), ns))
155  {
156  // ok
157  }
158  else
159  {
160  if(!arg_is_type_compatible(call_type.return_type(),
161  function_type.return_type()))
162  return false;
163  }
164 
165  // let's look at the parameters
166  const code_typet::parameterst &call_parameters=call_type.parameters();
167  const code_typet::parameterst &function_parameters=function_type.parameters();
168 
169  if(function_type.has_ellipsis() &&
170  function_parameters.empty())
171  {
172  // always ok
173  }
174  else if(call_type.has_ellipsis() &&
175  call_parameters.empty())
176  {
177  // always ok
178  }
179  else
180  {
181  // we are quite strict here, could be much more generous
182  if(call_parameters.size()!=function_parameters.size())
183  return false;
184 
185  for(std::size_t i=0; i<call_parameters.size(); i++)
186  if(!arg_is_type_compatible(call_parameters[i].type(),
187  function_parameters[i].type()))
188  return false;
189  }
190 
191  return true;
192 }
193 
195  code_function_callt &function_call)
196 {
197  const code_typet &code_type=
198  to_code_type(ns.follow(function_call.function().type()));
199 
200  const code_typet::parameterst &function_parameters=
201  code_type.parameters();
202 
203  code_function_callt::argumentst &call_arguments=
204  function_call.arguments();
205 
206  for(std::size_t i=0; i<function_parameters.size(); i++)
207  {
208  if(i<call_arguments.size())
209  {
210  if(!type_eq(call_arguments[i].type(),
211  function_parameters[i].type(), ns))
212  {
213  call_arguments[i].make_typecast(function_parameters[i].type());
214  }
215  }
216  }
217 }
218 
220  code_function_callt &function_call,
221  goto_programt &dest)
222 {
223  // are we returning anything at all?
224  if(function_call.lhs().is_nil())
225  return;
226 
227  const code_typet &code_type=
228  to_code_type(ns.follow(function_call.function().type()));
229 
230  // type already ok?
231  if(type_eq(
232  function_call.lhs().type(),
233  code_type.return_type(), ns))
234  return;
235 
236  const symbolt &function_symbol =
237  ns.lookup(to_symbol_expr(function_call.function()).get_identifier());
238 
239  symbolt &tmp_symbol = get_fresh_aux_symbol(
240  code_type.return_type(),
241  id2string(function_call.source_location().get_function()),
242  "tmp_return_val_" + id2string(function_symbol.base_name),
243  function_call.source_location(),
244  function_symbol.mode,
245  symbol_table);
246 
247  const symbol_exprt tmp_symbol_expr = tmp_symbol.symbol_expr();
248 
249  exprt old_lhs=function_call.lhs();
250  function_call.lhs()=tmp_symbol_expr;
251 
252  goto_programt::targett t_assign=dest.add_instruction();
253  t_assign->make_assignment();
254  t_assign->code=code_assignt(
255  old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()));
256 }
257 
260  goto_programt::targett target)
261 {
262  const code_function_callt &code=
263  to_code_function_call(target->code);
264 
265  const exprt &function=code.function();
266 
267  // this better have the right type
268  code_typet call_type=to_code_type(function.type());
269 
270  // refine the type in case the forward declaration was incomplete
271  if(call_type.has_ellipsis() &&
272  call_type.parameters().empty())
273  {
274  call_type.remove_ellipsis();
275  forall_expr(it, code.arguments())
276  call_type.parameters().push_back(
277  code_typet::parametert(it->type()));
278  }
279 
280  assert(function.id()==ID_dereference);
281  assert(function.operands().size()==1);
282 
283  bool found_functions;
284 
285  const exprt &pointer=function.op0();
287  does_remove_constt const_removal_check(goto_program, ns);
288  const auto does_remove_const = const_removal_check();
289  if(does_remove_const.first)
290  {
291  warning().source_location = does_remove_const.second;
292  warning() << "cast from const to non-const pointer found, only worst case"
293  << " function pointer removal will be done." << eom;
294  found_functions=false;
295  }
296  else
297  {
300 
301  found_functions=fpr(pointer, functions);
302 
303  // if found_functions is false, functions should be empty
304  // however, it is possible for found_functions to be true and functions
305  // to be empty (this happens if the pointer can only resolve to the null
306  // pointer)
307  CHECK_RETURN(found_functions || functions.empty());
308 
309  if(functions.size()==1)
310  {
311  to_code_function_call(target->code).function()=*functions.cbegin();
312  return;
313  }
314  }
315 
316  if(!found_functions)
317  {
319  {
320  // If this mode is enabled, we only remove function pointers
321  // that we can resolve either to an exact function, or an exact subset
322  // (e.g. a variable index in a constant array).
323  // Since we haven't found functions, we would now resort to
324  // replacing the function pointer with any function with a valid signature
325  // Since we don't want to do that, we abort.
326  return;
327  }
328 
329  bool return_value_used=code.lhs().is_not_nil();
330 
331  // get all type-compatible functions
332  // whose address is ever taken
333  for(const auto &t : type_map)
334  {
335  // address taken?
336  if(address_taken.find(t.first)==address_taken.end())
337  continue;
338 
339  // type-compatible?
340  if(!is_type_compatible(return_value_used, call_type, t.second))
341  continue;
342 
343  if(t.first=="pthread_mutex_cleanup")
344  continue;
345 
346  symbol_exprt expr(t.first, t.second);
347  functions.insert(expr);
348  }
349  }
350 
351  // the final target is a skip
352  goto_programt final_skip;
353 
354  goto_programt::targett t_final=final_skip.add_instruction();
355  t_final->make_skip();
356 
357  // build the calls and gotos
358 
359  goto_programt new_code_calls;
360  goto_programt new_code_gotos;
361 
362  for(const auto &fun : functions)
363  {
364  // call function
365  goto_programt::targett t1=new_code_calls.add_instruction();
366  t1->make_function_call(code);
367  to_code_function_call(t1->code).function()=fun;
368 
369  // the signature of the function might not match precisely
371 
372  fix_return_type(to_code_function_call(t1->code), new_code_calls);
373  // goto final
374  goto_programt::targett t3=new_code_calls.add_instruction();
375  t3->make_goto(t_final, true_exprt());
376 
377  // goto to call
378  address_of_exprt address_of(fun, pointer_type(fun.type()));
379 
380  if(address_of.type()!=pointer.type())
381  address_of.make_typecast(pointer.type());
382 
383  goto_programt::targett t4=new_code_gotos.add_instruction();
384  t4->make_goto(t1, equal_exprt(pointer, address_of));
385  }
386 
387  // fall-through
389  {
390  goto_programt::targett t=new_code_gotos.add_instruction();
391  t->make_assertion(false_exprt());
392  t->source_location.set_property_class("pointer dereference");
393  t->source_location.set_comment("invalid function pointer");
394  }
395 
396  goto_programt new_code;
397 
398  // patch them all together
399  new_code.destructive_append(new_code_gotos);
400  new_code.destructive_append(new_code_calls);
401  new_code.destructive_append(final_skip);
402 
403  // set locations
405  {
406  irep_idt property_class=it->source_location.get_property_class();
407  irep_idt comment=it->source_location.get_comment();
408  it->source_location=target->source_location;
409  it->function=target->function;
410  if(!property_class.empty())
411  it->source_location.set_property_class(property_class);
412  if(!comment.empty())
413  it->source_location.set_comment(comment);
414  }
415 
416  goto_programt::targett next_target=target;
417  next_target++;
418 
419  goto_program.destructive_insert(next_target, new_code);
420 
421  // We preserve the original dereferencing to possibly catch
422  // further pointer-related errors.
423  code_expressiont code_expression;
424  code_expression.add_source_location()=function.source_location();
425  code_expression.expression()=function;
426  target->code.swap(code_expression);
427  target->type=OTHER;
428 
429  // report statistics
430  statistics().source_location=target->source_location;
431  statistics() << "replacing function pointer by "
432  << functions.size() << " possible targets" << eom;
433 
434  // list the names of functions when verbosity is at debug level
436  debug(),
437  [&functions](mstreamt &mstream) {
438  mstream << "targets: ";
439 
440  bool first = true;
441  for(const auto &function : functions)
442  {
443  if(!first)
444  mstream << ", ";
445 
446  mstream << function.get_identifier();
447  first = false;
448  }
449 
450  mstream << eom;
451  });
452 }
453 
456 {
457  bool did_something=false;
458 
460  if(target->is_function_call())
461  {
462  const code_function_callt &code=
463  to_code_function_call(target->code);
464 
465  if(code.function().id()==ID_dereference)
466  {
468  did_something=true;
469  }
470  }
471 
472  if(did_something)
474 
475  return did_something;
476 }
477 
479 {
480  bool did_something=false;
481 
482  for(goto_functionst::function_mapt::iterator f_it=
483  functions.function_map.begin();
484  f_it!=functions.function_map.end();
485  f_it++)
486  {
487  goto_programt &goto_program=f_it->second.body;
488 
490  did_something=true;
491  }
492 
493  if(did_something)
494  functions.compute_location_numbers();
495 }
496 
498  symbol_tablet &symbol_table,
499  const goto_functionst &goto_functions,
501  bool add_safety_assertion,
502  bool only_remove_const_fps)
503 {
505  rfp(
506  _message_handler,
507  symbol_table,
508  add_safety_assertion,
509  only_remove_const_fps,
510  goto_functions);
511 
513 }
514 
516  message_handlert &_message_handler,
517  symbol_tablet &symbol_table,
518  goto_functionst &goto_functions,
519  bool add_safety_assertion,
520  bool only_remove_const_fps)
521 {
523  rfp(
524  _message_handler,
525  symbol_table,
526  add_safety_assertion,
527  only_remove_const_fps,
528  goto_functions);
529 
530  rfp(goto_functions);
531 }
532 
534  goto_modelt &goto_model,
535  bool add_safety_assertion,
536  bool only_remove_const_fps)
537 {
539  _message_handler,
540  goto_model.symbol_table,
541  goto_model.goto_functions,
542  add_safety_assertion,
543  only_remove_const_fps);
544 }
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: type_eq.cpp:18
The type of an expression.
Definition: type.h:22
semantic type conversion
Definition: std_expr.h:2111
Base type of functions.
Definition: std_types.h:764
bool is_type_compatible(bool return_value_used, const code_typet &call_type, const code_typet &function_type)
bool is_nil() const
Definition: irep.h:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
const symbol_tablet & get_symbol_table() const
Definition: namespace.h:106
Remove Indirect Function Calls.
exprt & op0()
Definition: expr.h:72
irep_idt mode
Language mode.
Definition: symbol.h:52
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
bool has_ellipsis() const
Definition: std_types.h:861
void fix_return_type(code_function_callt &function_call, goto_programt &dest)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
void compute_address_taken_functions(const exprt &src, std::unordered_set< irep_idt > &address_taken)
get all functions whose address is taken
const irep_idt & get_function() const
#define forall_expr(it, expr)
Definition: expr.h:28
Fresh auxiliary symbol creation.
std::vector< parametert > parameterst
Definition: std_types.h:767
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Definition: goto_program.h:486
function_mapt function_map
typet & type()
Definition: expr.h:56
exprt::operandst argumentst
Definition: std_code.h:858
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
An expression statement.
Definition: std_code.h:1188
bool arg_is_type_compatible(const typet &call_type, const typet &function_type)
mstreamt & warning() const
Definition: message.h:307
equality
Definition: std_expr.h:1354
void operator()(goto_functionst &goto_functions)
std::unordered_set< irep_idt > address_taken
const irep_idt & id() const
Definition: irep.h:189
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
void compute_location_numbers()
The boolean constant true.
Definition: std_expr.h:4488
argumentst & arguments()
Definition: std_code.h:860
void remove_ellipsis()
Definition: std_types.h:890
instructionst::iterator targett
Definition: goto_program.h:397
void compute_address_taken_in_symbols(std::unordered_set< irep_idt > &address_taken)
source_locationt source_location
Definition: message.h:214
The empty type.
Definition: std_types.h:54
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
Definition: goto_program.h:495
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
A function call.
Definition: std_code.h:828
std::map< irep_idt, code_typet > type_mapt
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
const typet & follow(const typet &) const
Definition: namespace.cpp:55
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)
Operator to return the address of an object.
Definition: std_expr.h:3170
const symbolst & symbols
The boolean constant false.
Definition: std_expr.h:4499
Query Called Functions.
void fix_argument_types(code_function_callt &function_call)
bool remove_function_pointers(goto_programt &goto_program)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
message_handlert & get_message_handler()
Definition: message.h:153
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, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
exprt & function()
Definition: std_code.h:848
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
const source_locationt & source_location() const
Definition: expr.h:125
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to mstream using output_generator if the configured verbosity is at least as high as ...
Definition: message.cpp:113
void remove_function_pointer(goto_programt &goto_program, goto_programt::targett target)
const exprt & expression() const
Definition: std_code.h:1201
std::unordered_set< symbol_exprt, irep_hash > functionst
void swap(irept &irep)
Definition: irep.h:231
goto_programt & goto_program
Definition: cover.cpp:63
source_locationt & add_source_location()
Definition: expr.h:130
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
mstreamt & debug() const
Definition: message.h:332
Base Type Computation.
Program Transformation.
#define forall_goto_functions(it, functions)
mstreamt mstream
Definition: message.h:343
bool empty() const
Definition: dstring.h:61
void make_typecast(const typet &_type)
Definition: expr.cpp:84
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
mstreamt & statistics() const
Definition: message.h:322
const typet & return_type() const
Definition: std_types.h:895
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Assignment.
Definition: std_code.h:195
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879