CBMC
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 #include <util/message.h>
16 #include <util/std_code.h>
17 
18 #include "goto_functions.h"
19 
26  goto_programt &goto_program,
28  const exprt &lhs,
29  const exprt::operandst &arguments)
30 {
31  PRECONDITION(target->is_function_call());
32  PRECONDITION(!goto_program.empty());
33 
34  goto_programt tmp;
35 
36  // evaluate function arguments -- they might have
37  // pointer dereferencing or the like
38  for(const exprt &argument : arguments)
39  {
41  code_expressiont(argument), target->source_location()));
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 
53  }
54 
55  // kill call
56  *target = goto_programt::make_location(target->source_location());
57  target++;
58 
59  goto_program.destructive_insert(target, tmp);
60 }
61 
67  const goto_programt::const_targett target,
68  const goto_functionst &goto_functions)
69 {
70  if(!target->is_function_call())
71  return false;
72 
73  const exprt &f = target->call_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 
100  goto_programt &goto_program,
101  const goto_functionst &goto_functions,
102  message_handlert &message_handler)
103 {
104  for(goto_programt::targett it = goto_program.instructions.begin();
105  it != goto_program.instructions.end();) // no it++
106  {
107  if(is_opaque_function_call(it, goto_functions))
108  {
109  messaget log{message_handler};
110  log.status() << "Removing call to "
111  << to_symbol_expr(it->call_function()).get_identifier()
112  << ", which has no body" << messaget::eom;
114  goto_program, it, it->call_lhs(), it->call_arguments());
115  }
116  else
117  {
118  it++;
119  }
120  }
121 }
122 
129  goto_functionst &goto_functions,
130  message_handlert &message_handler)
131 {
132  for(auto &gf_entry : goto_functions.function_map)
133  {
134  (*this)(gf_entry.second.body, goto_functions, message_handler);
135  }
136 }
A goto_instruction_codet representing an assignment in the program.
codet representation of an expression statement.
Definition: std_code.h:1394
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
source_locationt & add_source_location()
Definition: expr.h:236
const source_locationt & source_location() const
Definition: expr.h:231
typet & type()
Return the type of the expression.
Definition: expr.h:84
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:730
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:901
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
bool empty() const
Is the program empty?
Definition: goto_program.h:799
bool is_not_nil() const
Definition: irep.h:368
const irep_idt & id() const
Definition: irep.h:384
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
static eomt eom
Definition: message.h:297
void remove_call_no_body(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Remove a single 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.
void operator()(goto_programt &goto_program, const goto_functionst &goto_functions, message_handlert &)
Remove calls to functions without a body and replace them with evaluations of the arguments of the ca...
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
const source_locationt & source_location() const
Definition: type.h:72
Goto Programs with Functions.
double log(double x)
Definition: math.c:2776
Remove calls to functions without a body.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272