cprover
remove_virtual_functions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove Virtual Function (Method) Calls
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 #include "class_hierarchy.h"
14 #include "class_identifier.h"
15 
16 #include <util/c_types.h>
17 #include <util/prefix.h>
18 #include <util/type_eq.h>
19 
21 {
22 public:
24  const symbol_tablet &_symbol_table,
25  const goto_functionst &goto_functions);
26 
27  void operator()(goto_functionst &goto_functions);
28 
29  bool remove_virtual_functions(goto_programt &goto_program);
30 
31 protected:
32  const namespacet ns;
34 
36 
38  goto_programt &goto_program,
39  goto_programt::targett target);
40 
41  class functiont
42  {
43  public:
44  functiont() {}
45  explicit functiont(const irep_idt &_class_id) :
46  class_id(_class_id)
47  {}
48 
51  };
52 
53  typedef std::vector<functiont> functionst;
54  void get_functions(const exprt &, functionst &);
56  const irep_idt &,
57  const symbol_exprt &,
58  const irep_idt &,
59  functionst &,
60  std::set<irep_idt> &visited) const;
62  const irep_idt &class_id,
63  const irep_idt &component_name) const;
64 };
65 
67  const symbol_tablet &_symbol_table,
68  const goto_functionst &goto_functions):
69  ns(_symbol_table),
70  symbol_table(_symbol_table)
71 {
73 }
74 
76  goto_programt &goto_program,
78 {
79  const code_function_callt &code=
80  to_code_function_call(target->code);
81 
82  const auto &vcall_source_loc=target->source_location;
83 
84  const exprt &function=code.function();
85  assert(function.id()==ID_virtual_function);
86  assert(!code.arguments().empty());
87 
88  functionst functions;
89  get_functions(function, functions);
90 
91  if(functions.empty())
92  {
93  target->make_skip();
94  return; // give up
95  }
96 
97  // only one option?
98  if(functions.size()==1)
99  {
100  assert(target->is_function_call());
101  if(functions.begin()->symbol_expr==symbol_exprt())
102  target->make_skip();
103  else
104  to_code_function_call(target->code).function()=
105  functions.begin()->symbol_expr;
106  return;
107  }
108 
109  // the final target is a skip
110  goto_programt final_skip;
111 
112  goto_programt::targett t_final=final_skip.add_instruction();
113  t_final->source_location=vcall_source_loc;
114 
115  t_final->make_skip();
116 
117  // build the calls and gotos
118 
119  goto_programt new_code_calls;
120  goto_programt new_code_gotos;
121 
122  exprt this_expr=code.arguments()[0];
123  // If necessary, cast to the last candidate function to
124  // get the object's clsid. By the structure of get_functions,
125  // this is the parent of all other classes under consideration.
126  const auto &base_classid=functions.back().class_id;
127  const auto &base_function_symbol=functions.back().symbol_expr;
128  symbol_typet suggested_type(base_classid);
129  exprt c_id2=get_class_identifier_field(this_expr, suggested_type, ns);
130 
131  std::map<irep_idt, goto_programt::targett> calls;
132  // Note backwards iteration, to get the least-derived candidate first.
133  for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
134  {
135  const auto &fun=*it;
136  auto insertit=calls.insert(
137  {fun.symbol_expr.get_identifier(), goto_programt::targett()});
138 
139  // Only create one call sequence per possible target:
140  if(insertit.second)
141  {
142  goto_programt::targett t1=new_code_calls.add_instruction();
143  t1->source_location=vcall_source_loc;
144  if(!fun.symbol_expr.get_identifier().empty())
145  {
146  // call function
147  t1->make_function_call(code);
148  auto &newcall=to_code_function_call(t1->code);
149  newcall.function()=fun.symbol_expr;
150  typet need_type=
151  pointer_type(symbol_typet(fun.symbol_expr.get(ID_C_class)));
152  if(!type_eq(newcall.arguments()[0].type(), need_type, ns))
153  newcall.arguments()[0].make_typecast(need_type);
154  }
155  else
156  {
157  // No definition for this type; shouldn't be possible...
158  t1->make_assertion(false_exprt());
159  }
160  insertit.first->second=t1;
161  // goto final
162  goto_programt::targett t3=new_code_calls.add_instruction();
163  t3->source_location=vcall_source_loc;
164  t3->make_goto(t_final, true_exprt());
165  }
166 
167  // If this calls the base function we just fall through.
168  // Otherwise branch to the right call:
169  if(fun.symbol_expr!=base_function_symbol)
170  {
171  exprt c_id1=constant_exprt(fun.class_id, string_typet());
172  goto_programt::targett t4=new_code_gotos.add_instruction();
173  t4->source_location=vcall_source_loc;
174  t4->make_goto(insertit.first->second, equal_exprt(c_id1, c_id2));
175  }
176  }
177 
178  goto_programt new_code;
179 
180  // patch them all together
181  new_code.destructive_append(new_code_gotos);
182  new_code.destructive_append(new_code_calls);
183  new_code.destructive_append(final_skip);
184 
185  // set locations
187  {
188  const irep_idt property_class=it->source_location.get_property_class();
189  const irep_idt comment=it->source_location.get_comment();
190  it->source_location=target->source_location;
191  it->function=target->function;
192  if(!property_class.empty())
193  it->source_location.set_property_class(property_class);
194  if(!comment.empty())
195  it->source_location.set_comment(comment);
196  }
197 
198  goto_programt::targett next_target=target;
199  next_target++;
200 
201  goto_program.destructive_insert(next_target, new_code);
202 
203  // finally, kill original invocation
204  target->make_skip();
205 }
206 
219  const irep_idt &this_id,
220  const symbol_exprt &last_method_defn,
221  const irep_idt &component_name,
222  functionst &functions,
223  std::set<irep_idt> &visited) const
224 {
225  auto findit=class_hierarchy.class_map.find(this_id);
226  if(findit==class_hierarchy.class_map.end())
227  return;
228 
229  for(const auto &child : findit->second.children)
230  {
231  if(!visited.insert(child).second)
232  continue;
233  exprt method=get_method(child, component_name);
234  functiont function(child);
235  if(method.is_not_nil())
236  {
237  function.symbol_expr=to_symbol_expr(method);
238  function.symbol_expr.set(ID_C_class, child);
239  }
240  else
241  {
242  function.symbol_expr=last_method_defn;
243  }
244  functions.push_back(function);
245 
247  child,
248  function.symbol_expr,
249  component_name,
250  functions,
251  visited);
252  }
253 }
254 
256  const exprt &function,
257  functionst &functions)
258 {
259  const irep_idt class_id=function.get(ID_C_class);
260  const irep_idt component_name=function.get(ID_component_name);
261  assert(!class_id.empty());
262  functiont root_function;
263 
264  // Start from current class, go to parents until something
265  // is found.
266  irep_idt c=class_id;
267  while(!c.empty())
268  {
269  exprt method=get_method(c, component_name);
270  if(method.is_not_nil())
271  {
272  root_function.class_id=c;
273  root_function.symbol_expr=to_symbol_expr(method);
274  root_function.symbol_expr.set(ID_C_class, c);
275  break; // abort
276  }
277 
278  const class_hierarchyt::idst &parents=
279  class_hierarchy.class_map[c].parents;
280 
281  if(parents.empty())
282  break;
283  c=parents.front();
284  }
285 
286  if(root_function.class_id.empty())
287  {
288  // No definition here; this is an abstract function.
289  root_function.class_id=class_id;
290  }
291 
292  // iterate over all children, transitively
293  std::set<irep_idt> visited;
295  class_id,
296  root_function.symbol_expr,
297  component_name,
298  functions,
299  visited);
300 
301  if(root_function.symbol_expr!=symbol_exprt())
302  functions.push_back(root_function);
303 }
304 
306  const irep_idt &class_id,
307  const irep_idt &component_name) const
308 {
309  irep_idt id=id2string(class_id)+"."+
310  id2string(component_name);
311 
312  const symbolt *symbol;
313  if(ns.lookup(id, symbol))
314  return nil_exprt();
315 
316  return symbol->symbol_expr();
317 }
318 
320  goto_programt &goto_program)
321 {
322  bool did_something=false;
323 
324  Forall_goto_program_instructions(target, goto_program)
325  if(target->is_function_call())
326  {
327  const code_function_callt &code=
328  to_code_function_call(target->code);
329 
330  if(code.function().id()==ID_virtual_function)
331  {
332  remove_virtual_function(goto_program, target);
333  did_something=true;
334  }
335  }
336 
337  if(did_something)
338  {
339  goto_program.update();
340  }
341 
342  return did_something;
343 }
344 
346 {
347  bool did_something=false;
348 
349  for(goto_functionst::function_mapt::iterator f_it=
350  functions.function_map.begin();
351  f_it!=functions.function_map.end();
352  f_it++)
353  {
354  goto_programt &goto_program=f_it->second.body;
355 
356  if(remove_virtual_functions(goto_program))
357  did_something=true;
358  }
359 
360  if(did_something)
361  functions.compute_location_numbers();
362 }
363 
365  const symbol_tablet &symbol_table,
366  goto_functionst &goto_functions)
367 {
369  rvf(symbol_table, goto_functions);
370 
371  rvf(goto_functions);
372 }
373 
375 {
377  goto_model.symbol_table, goto_model.goto_functions);
378 }
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
void operator()(goto_functionst &goto_functions)
void update()
Update all indices.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
targett add_instruction()
Adds an instruction at the end.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
remove_virtual_functionst(const symbol_tablet &_symbol_table, const goto_functionst &goto_functions)
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
bool remove_virtual_functions(goto_programt &goto_program)
Remove Virtual Function (Method) Calls.
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:115
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
A constant literal expression.
Definition: std_expr.h:3685
void remove_virtual_functions(const symbol_tablet &symbol_table, goto_functionst &goto_functions)
TO_BE_DOCUMENTED.
Definition: std_types.h:1490
equality
Definition: std_expr.h:1082
Class Hierarchy.
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:191
The boolean constant true.
Definition: std_expr.h:3742
argumentst & arguments()
Definition: std_code.h:689
A reference into the symbol table.
Definition: std_types.h:109
exprt get_method(const irep_idt &class_id, const irep_idt &component_name) const
The NIL expression.
Definition: std_expr.h:3764
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
class_mapt class_map
A function call.
Definition: std_code.h:657
std::vector< functiont > functionst
exprt get_class_identifier_field(const exprt &this_expr_in, const symbol_typet &suggested_type, const namespacet &ns)
The boolean constant false.
Definition: std_expr.h:3753
void get_functions(const exprt &, functionst &)
std::vector< irep_idt > idst
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void get_child_functions_rec(const irep_idt &, const symbol_exprt &, const irep_idt &, functionst &, std::set< irep_idt > &visited) const
Used by get_functions to track the most-derived parent that provides an override of a given function...
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#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.
Extract class identifier.
bool empty() const
Definition: dstring.h:61
goto_functionst goto_functions
Definition: goto_model.h:26
void remove_virtual_function(goto_programt &goto_program, goto_programt::targett target)
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700