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 #include <ansi-c/c_qualifiers.h>
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 
45  bool remove_function_pointers(goto_programt &goto_program);
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 
61  goto_programt &goto_program,
62  goto_programt::targett target);
63 
64  std::set<irep_idt> address_taken;
65 
66  typedef std::map<irep_idt, code_typet> type_mapt;
67  type_mapt type_map;
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 
84  std::set<irep_idt> &address_taken)
85  {
86  const symbol_tablet &symbol_table=ns.get_symbol_table();
87 
88  for(const auto &s : symbol_table.symbols)
89  compute_address_taken_functions(s.second.value, address_taken);
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(unsigned 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(unsigned 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  symbolt &tmp_symbol=
238  code_type.return_type(),
239  "remove_function_pointers",
240  "tmp_return_val",
241  function_call.source_location(),
242  irep_idt(),
243  symbol_table);
244 
245  symbol_exprt tmp_symbol_expr;
246  tmp_symbol_expr.type()=tmp_symbol.type;
247  tmp_symbol_expr.set_identifier(tmp_symbol.name);
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 
259  goto_programt &goto_program,
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  if(const_removal_check())
289  {
290  warning() << "Cast from const to non-const pointer found, only worst case"
291  << " function pointer removal will be done." << eom;
292  found_functions=false;
293  }
294  else
295  {
298 
299  found_functions=fpr(pointer, functions);
300 
301  // if found_functions is false, functions should be empty
302  // however, it is possible for found_functions to be true and functions
303  // to be empty (this happens if the pointer can only resolve to the null
304  // pointer)
305  CHECK_RETURN(found_functions || functions.empty());
306 
307  if(functions.size()==1)
308  {
309  to_code_function_call(target->code).function()=*functions.cbegin();
310  return;
311  }
312  }
313 
314  if(!found_functions)
315  {
317  {
318  // If this mode is enabled, we only remove function pointers
319  // that we can resolve either to an exact function, or an exact subset
320  // (e.g. a variable index in a constant array).
321  // Since we haven't found functions, we would now resort to
322  // replacing the function pointer with any function with a valid signature
323  // Since we don't want to do that, we abort.
324  return;
325  }
326 
327  bool return_value_used=code.lhs().is_not_nil();
328 
329  // get all type-compatible functions
330  // whose address is ever taken
331  for(const auto &t : type_map)
332  {
333  // address taken?
334  if(address_taken.find(t.first)==address_taken.end())
335  continue;
336 
337  // type-compatible?
338  if(!is_type_compatible(return_value_used, call_type, t.second))
339  continue;
340 
341  if(t.first=="pthread_mutex_cleanup")
342  continue;
343 
344  symbol_exprt expr;
345  expr.type()=t.second;
346  expr.set_identifier(t.first);
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 
436  goto_programt &goto_program)
437 {
438  bool did_something=false;
439 
440  Forall_goto_program_instructions(target, goto_program)
441  if(target->is_function_call())
442  {
443  const code_function_callt &code=
444  to_code_function_call(target->code);
445 
446  if(code.function().id()==ID_dereference)
447  {
448  remove_function_pointer(goto_program, target);
449  did_something=true;
450  }
451  }
452 
453  if(did_something)
454  {
455  remove_skip(goto_program);
456  goto_program.update();
457  }
458 
459  return did_something;
460 }
461 
463 {
464  bool did_something=false;
465 
466  for(goto_functionst::function_mapt::iterator f_it=
467  functions.function_map.begin();
468  f_it!=functions.function_map.end();
469  f_it++)
470  {
471  goto_programt &goto_program=f_it->second.body;
472 
473  if(remove_function_pointers(goto_program))
474  did_something=true;
475  }
476 
477  if(did_something)
478  functions.compute_location_numbers();
479 }
480 
483  const goto_functionst &goto_functions,
484  goto_programt &goto_program,
486  bool only_remove_const_fps)
487 {
489  rfp(
490  _message_handler,
491  symbol_table,
492  add_safety_assertion,
493  only_remove_const_fps,
494  goto_functions);
495 
496  return rfp.remove_function_pointers(goto_program);
497 }
498 
500  message_handlert &_message_handler,
502  goto_functionst &goto_functions,
504  bool only_remove_const_fps)
505 {
507  rfp(
508  _message_handler,
509  symbol_table,
510  add_safety_assertion,
511  only_remove_const_fps,
512  goto_functions);
513 
514  rfp(goto_functions);
515 }
516 
518  goto_modelt &goto_model,
520  bool only_remove_const_fps)
521 {
523  _message_handler,
524  goto_model.symbol_table,
525  goto_model.goto_functions,
526  add_safety_assertion,
527  only_remove_const_fps);
528 }
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: type_eq.cpp:20
The type of an expression.
Definition: type.h:20
mstreamt & warning()
Definition: message.h:228
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
void update()
Update all indices.
semantic type conversion
Definition: std_expr.h:1725
targett add_instruction()
Adds an instruction at the end.
Base type of functions.
Definition: std_types.h:734
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:103
bool is_not_nil() const
Definition: irep.h:104
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
void compute_address_taken_functions(const exprt &src, std::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, symbol_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
const symbol_tablet & get_symbol_table() const
Definition: namespace.h:91
Remove Indirect Function Calls.
exprt & op0()
Definition: expr.h:84
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:115
bool has_ellipsis() const
Definition: std_types.h:803
void fix_return_type(code_function_callt &function_call, goto_programt &dest)
#define forall_expr(it, expr)
Definition: expr.h:28
Fresh auxiliary symbol creation.
std::vector< parametert > parameterst
Definition: std_types.h:829
typet & type()
Definition: expr.h:60
exprt::operandst argumentst
Definition: std_code.h:687
symbol_tablet symbol_table
Definition: goto_model.h:25
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:240
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
An expression statement.
Definition: std_code.h:957
bool arg_is_type_compatible(const typet &call_type, const typet &function_type)
std::unordered_set< exprt, irep_hash > functionst
equality
Definition: std_expr.h:1082
void operator()(goto_functionst &goto_functions)
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:3742
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
void remove_ellipsis()
Definition: std_types.h:824
source_locationt source_location
Definition: message.h:175
The empty type.
Definition: std_types.h:53
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
std::map< irep_idt, code_typet > type_mapt
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:2593
The boolean constant false.
Definition: std_expr.h:3753
mstreamt & statistics()
Definition: message.h:243
Query Called Functions.
void fix_argument_types(code_function_callt &function_call)
bool remove_function_pointers(goto_programt &goto_program)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
typet type
Type of symbol.
Definition: symbol.h:37
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
message_handlert & get_message_handler()
Definition: message.h:127
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
const source_locationt & source_location() const
Definition: expr.h:142
void remove_function_pointer(goto_programt &goto_program, goto_programt::targett target)
const exprt & expression() const
Definition: std_code.h:970
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:115
void swap(irept &irep)
Definition: irep.h:231
source_locationt & add_source_location()
Definition: expr.h:147
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
void destructive_insert(const_targett target, goto_program_templatet< codeT, guardT > &p)
Inserts the given program at the given location.
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
dstringt irep_idt
Definition: irep.h:32
Base Type Computation.
Program Transformation.
#define forall_goto_functions(it, functions)
void compute_address_taken_in_symbols(std::set< irep_idt > &address_taken)
bool empty() const
Definition: dstring.h:61
void make_typecast(const typet &_type)
Definition: expr.cpp:90
goto_functionst goto_functions
Definition: goto_model.h:26
const typet & return_type() const
Definition: std_types.h:831
Assignment.
Definition: std_code.h:144
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700