cprover
replace_calls.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Replace calls
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
13 
14 #include "replace_calls.h"
15 
17 
18 #include <util/base_type.h>
19 #include <util/exception_utils.h>
20 #include <util/invariant.h>
21 #include <util/irep.h>
22 #include <util/string_utils.h>
23 #include <util/suffix.h>
24 
31  goto_modelt &goto_model,
32  const replacement_listt &replacement_list) const
33 {
34  replacement_mapt replacement_map = parse_replacement_list(replacement_list);
35  (*this)(goto_model, replacement_map);
36 }
37 
43  goto_modelt &goto_model,
44  const replacement_mapt &replacement_map) const
45 {
46  const namespacet ns(goto_model.symbol_table);
47  goto_functionst &goto_functions = goto_model.goto_functions;
48 
49  check_replacement_map(replacement_map, goto_functions, ns);
50 
51  for(auto &p : goto_functions.function_map)
52  {
53  goto_functionst::goto_functiont &goto_function = p.second;
54  goto_programt &goto_program = goto_function.body;
55 
56  (*this)(goto_program, goto_functions, ns, replacement_map);
57  }
58 }
59 
61  goto_programt &goto_program,
62  const goto_functionst &goto_functions,
63  const namespacet &ns,
64  const replacement_mapt &replacement_map) const
65 {
66  Forall_goto_program_instructions(it, goto_program)
67  {
68  goto_programt::instructiont &ins = *it;
69 
70  if(!ins.is_function_call())
71  continue;
72 
73  auto cfc = ins.get_function_call();
74  exprt &function = cfc.function();
75 
76  PRECONDITION(function.id() == ID_symbol);
77 
78  symbol_exprt &se = to_symbol_expr(function);
79  const irep_idt &id = se.get_identifier();
80 
81  auto f_it1 = goto_functions.function_map.find(id);
82 
84  f_it1 != goto_functions.function_map.end(),
85  "Called functions need to be present");
86 
87  replacement_mapt::const_iterator r_it = replacement_map.find(id);
88 
89  if(r_it == replacement_map.end())
90  continue;
91 
92  const irep_idt &new_id = r_it->second;
93 
94  auto f_it2 = goto_functions.function_map.find(new_id);
95  PRECONDITION(f_it2 != goto_functions.function_map.end());
96 
97  PRECONDITION(base_type_eq(f_it1->second.type, f_it2->second.type, ns));
98 
99  // check that returns have not been removed
100  if(to_code_type(f_it1->second.type).return_type().id() != ID_empty)
101  {
102  goto_programt::const_targett next_it = std::next(it);
103  if(next_it != goto_program.instructions.end() && next_it->is_assign())
104  {
105  const code_assignt &ca = next_it->get_assign();
106  const exprt &rhs = ca.rhs();
107 
108  INVARIANT(
109  rhs != return_value_symbol(id, ns),
110  "returns must not be removed before replacing calls");
111  }
112  }
113 
114  // Finally modify the call
115  function.type() = f_it2->second.type;
116  se.set_identifier(new_id);
117 
118  ins.set_function_call(cfc);
119  }
120 }
121 
123  const replacement_listt &replacement_list) const
124 {
125  replacement_mapt replacement_map;
126 
127  for(const std::string &s : replacement_list)
128  {
129  std::string original;
130  std::string replacement;
131 
132  split_string(s, ':', original, replacement, true);
133 
134  const auto r =
135  replacement_map.insert(std::make_pair(original, replacement));
136 
137  if(!r.second)
138  {
140  "conflicting replacement for function " + original, "--replace-calls");
141  }
142  }
143 
144  return replacement_map;
145 }
146 
148  const replacement_mapt &replacement_map,
149  const goto_functionst &goto_functions,
150  const namespacet &ns) const
151 {
152  for(const auto &p : replacement_map)
153  {
154  if(replacement_map.find(p.second) != replacement_map.end())
156  "function " + id2string(p.second) +
157  " cannot both be replaced and be a replacement",
158  "--replace-calls");
159 
160  auto it2 = goto_functions.function_map.find(p.second);
161 
162  if(it2 == goto_functions.function_map.end())
164  "replacement function " + id2string(p.second) + " needs to be present",
165  "--replace-calls");
166 
167  auto it1 = goto_functions.function_map.find(p.first);
168  if(it1 != goto_functions.function_map.end())
169  {
170  if(!base_type_eq(it1->second.type, it2->second.type, ns))
172  "functions " + id2string(p.first) + " and " + id2string(p.second) +
173  " are not type-compatible",
174  "--replace-calls");
175  }
176  }
177 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
replace_callst::replacement_listt
std::list< std::string > replacement_listt
Definition: replace_calls.h:21
string_utils.h
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
replace_calls.h
Replace calls to given functions with calls to other given functions.
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
replace_callst::check_replacement_map
void check_replacement_map(const replacement_mapt &replacement_map, const goto_functionst &goto_functions, const namespacet &ns) const
Definition: replace_calls.cpp:147
replace_callst::parse_replacement_list
replacement_mapt parse_replacement_list(const replacement_listt &replacement_list) const
Definition: replace_calls.cpp:122
goto_programt::instructiont::set_function_call
void set_function_call(code_function_callt c)
Set the function call for FUNCTION_CALL.
Definition: goto_program.h:248
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:40
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
base_type.h
Base Type Computation.
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
replace_callst::replacement_mapt
std::map< irep_idt, irep_idt > replacement_mapt
Definition: replace_calls.h:22
base_type_eq
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:290
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
goto_programt::instructiont::get_function_call
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
Definition: goto_program.h:241
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
remove_returns.h
Replace function returns by assignments to global variables.
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
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_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
replace_callst::operator()
void operator()(goto_modelt &goto_model, const replacement_listt &replacement_list) const
Replace function calls with calls to other functions.
Definition: replace_calls.cpp:30
suffix.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
return_value_symbol
symbol_exprt return_value_symbol(const irep_idt &identifier, const namespacet &ns)
produces the symbol that is used to store the return value of the function with the given identifier
Definition: remove_returns.cpp:415
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
r
static int8_t r
Definition: irep_hash.h:59
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:461
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:106
validation_modet::INVARIANT
@ INVARIANT
irep.h