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 
24  goto_programt &goto_program,
26  const exprt &lhs,
27  const exprt::operandst &arguments)
28 {
29  PRECONDITION(target->is_function_call());
30  PRECONDITION(!goto_program.empty());
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  code_expressiont(argument), target->source_location));
40  }
41 
42  // return value
43  if(lhs.is_not_nil())
44  {
45  side_effect_expr_nondett rhs(lhs.type(), target->source_location);
46 
47  code_assignt code(lhs, rhs);
48  code.add_source_location() = target->source_location;
49 
51  }
52 
53  // kill call
54  target->type = LOCATION;
55  target->code.clear();
56  target++;
57 
58  goto_program.destructive_insert(target, tmp);
59 }
60 
66  const goto_programt::const_targett target,
67  const goto_functionst &goto_functions)
68 {
69  if(!target->is_function_call())
70  return false;
71 
72  const code_function_callt &cfc = target->get_function_call();
73  const exprt &f = cfc.function();
74 
75  if(f.id() != ID_symbol)
76  return false;
77 
78  const symbol_exprt &se = to_symbol_expr(f);
79  const irep_idt id = se.get_identifier();
80 
81  goto_functionst::function_mapt::const_iterator f_it =
82  goto_functions.function_map.find(id);
83 
84  if(f_it != goto_functions.function_map.end())
85  {
86  return !f_it->second.body_available();
87  }
88 
89  return false;
90 }
91 
99 operator()(goto_programt &goto_program, const goto_functionst &goto_functions)
100 {
101  for(goto_programt::targett it = goto_program.instructions.begin();
102  it != goto_program.instructions.end();) // no it++
103  {
104  if(is_opaque_function_call(it, goto_functions))
105  {
106  const code_function_callt &cfc = it->get_function_call();
107  remove_call_no_body(goto_program, it, cfc.lhs(), cfc.arguments());
108  }
109  else
110  {
111  it++;
112  }
113  }
114 }
115 
121 {
122  Forall_goto_functions(f_it, goto_functions)
123  {
124  (*this)(f_it->second.body, goto_functions);
125  }
126 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
invariant.h
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:762
exprt
Base class for all expressions.
Definition: expr.h:53
remove_calls_no_body.h
Remove calls to functions without a body.
remove_calls_no_bodyt::remove_call_no_body
void remove_call_no_body(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Remove a single call.
Definition: remove_calls_no_body.cpp:23
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
remove_calls_no_bodyt::operator()
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...
Definition: remove_calls_no_body.cpp:99
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
coverage_criteriont::LOCATION
@ LOCATION
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:677
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_programt::make_other
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:913
remove_calls_no_bodyt::is_opaque_function_call
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.
Definition: remove_calls_no_body.cpp:65
goto_functions.h
Goto Programs with Functions.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1810