cprover
remove_calls_no_body.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove calls to functions without a body
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
11 
12 #include "remove_calls_no_body.h"
13 
14 #include <util/invariant.h>
15 
16 #include "goto_functions.h"
17 
26  const exprt &lhs,
27  const exprt::operandst &arguments)
28 {
29  PRECONDITION(target->is_function_call());
31 
32  goto_programt tmp;
33 
34  // evaluate function arguments -- they might have
35  // pointer dereferencing or the like
36  for(const exprt &argument : arguments)
37  {
39  t->make_other(code_expressiont(argument));
40  t->source_location = target->source_location;
41  t->function = target->function;
42  }
43 
44  // return value
45  if(lhs.is_not_nil())
46  {
47  side_effect_expr_nondett rhs(lhs.type(), target->source_location);
48 
49  code_assignt code(lhs, rhs);
50  code.add_source_location() = target->source_location;
51 
52  goto_programt::targett t = tmp.add_instruction(ASSIGN);
53  t->source_location = target->source_location;
54  t->function = target->function;
55  t->code.swap(code);
56  }
57 
58  // kill call
59  target->type = LOCATION;
60  target->code.clear();
61  target++;
62 
63  goto_program.destructive_insert(target, tmp);
64 }
65 
71  const goto_programt::const_targett target,
72  const goto_functionst &goto_functions)
73 {
74  if(!target->is_function_call())
75  return false;
76 
77  const code_function_callt &cfc = to_code_function_call(target->code);
78  const exprt &f = cfc.function();
79 
80  if(f.id() != ID_symbol)
81  return false;
82 
83  const symbol_exprt &se = to_symbol_expr(f);
84  const irep_idt id = se.get_identifier();
85 
86  goto_functionst::function_mapt::const_iterator f_it =
87  goto_functions.function_map.find(id);
88 
89  if(f_it != goto_functions.function_map.end())
90  {
91  return !f_it->second.body_available();
92  }
93 
94  return false;
95 }
96 
105 {
107  it != goto_program.instructions.end();) // no it++
108  {
109  if(is_opaque_function_call(it, goto_functions))
110  {
111  const code_function_callt &cfc = to_code_function_call(it->code);
112  remove_call_no_body(goto_program, it, cfc.lhs(), cfc.arguments());
113  }
114  else
115  {
116  it++;
117  }
118  }
119 }
120 
126 {
127  Forall_goto_functions(f_it, goto_functions)
128  {
129  (*this)(f_it->second.body, goto_functions);
130  }
131 }
bool is_not_nil() const
Definition: irep.h:173
const irep_idt & get_identifier() const
Definition: std_expr.h:128
Goto Programs with Functions.
Remove calls to functions without a body.
function_mapt function_map
typet & type()
Definition: expr.h:56
void operator()(goto_programt &goto_program, const goto_functionst &goto_functions)
Remove calls to functions without a body and replace them with evaluations of the arguments of the ca...
An expression statement.
Definition: std_code.h:1220
bool is_opaque_function_call(const goto_programt::const_targett target, const goto_functionst &goto_functions)
Check if instruction is a call to an opaque function through an ordinary (non-function pointer) call...
const irep_idt & id() const
Definition: irep.h:259
argumentst & arguments()
Definition: std_code.h:890
instructionst::iterator targett
Definition: goto_program.h:397
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
instructionst::const_iterator const_targett
Definition: goto_program.h:398
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
Definition: goto_program.h:495
A function call.
Definition: std_code.h:858
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::vector< exprt > operandst
Definition: expr.h:45
const source_locationt & source_location() const
Definition: type.h:97
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
exprt & function()
Definition: std_code.h:878
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
void remove_call_no_body(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Remove a single call.
#define Forall_goto_functions(it, functions)
bool empty() const
Is the program empty?
Definition: goto_program.h:590
goto_programt & goto_program
Definition: cover.cpp:63
Expression to hold a symbol (variable)
Definition: std_expr.h:90
Assignment.
Definition: std_code.h:196
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909