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  // check that returns have not been removed
98  if(to_code_type(function.type()).return_type().id() != ID_empty)
99  {
100  goto_programt::const_targett next_it = std::next(it);
101  if(next_it != goto_program.instructions.end() && next_it->is_assign())
102  {
103  const code_assignt &ca = next_it->get_assign();
104  const exprt &rhs = ca.rhs();
105 
106  INVARIANT(
107  rhs != return_value_symbol(id, ns),
108  "returns must not be removed before replacing calls");
109  }
110  }
111 
112  // Finally modify the call
113  function.type() = ns.lookup(f_it2->first).type;
114  se.set_identifier(new_id);
115 
116  ins.set_function_call(cfc);
117  }
118 }
119 
121  const replacement_listt &replacement_list) const
122 {
123  replacement_mapt replacement_map;
124 
125  for(const std::string &s : replacement_list)
126  {
127  std::string original;
128  std::string replacement;
129 
130  split_string(s, ':', original, replacement, true);
131 
132  const auto r =
133  replacement_map.insert(std::make_pair(original, replacement));
134 
135  if(!r.second)
136  {
138  "conflicting replacement for function " + original, "--replace-calls");
139  }
140  }
141 
142  return replacement_map;
143 }
144 
146  const replacement_mapt &replacement_map,
147  const goto_functionst &goto_functions,
148  const namespacet &ns) const
149 {
150  for(const auto &p : replacement_map)
151  {
152  if(replacement_map.find(p.second) != replacement_map.end())
154  "function " + id2string(p.second) +
155  " cannot both be replaced and be a replacement",
156  "--replace-calls");
157 
158  auto it2 = goto_functions.function_map.find(p.second);
159 
160  if(it2 == goto_functions.function_map.end())
162  "replacement function " + id2string(p.second) + " needs to be present",
163  "--replace-calls");
164 
165  auto it1 = goto_functions.function_map.find(p.first);
166  if(it1 != goto_functions.function_map.end())
167  {
168  if(!base_type_eq(
169  ns.lookup(it1->first).type, ns.lookup(it2->first).type, ns))
171  "functions " + id2string(p.first) + " and " + id2string(p.second) +
172  " are not type-compatible",
173  "--replace-calls");
174  }
175  }
176 }
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
Base Type Computation.
A codet representing an assignment in the program.
Definition: std_code.h:295
exprt & rhs()
Definition: std_code.h:317
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
void set_function_call(code_function_callt c)
Set the function call for FUNCTION_CALL.
Definition: goto_program.h:313
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
Definition: goto_program.h:306
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
instructionst::const_iterator const_targett
Definition: goto_program.h:551
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
std::list< std::string > replacement_listt
Definition: replace_calls.h:21
replacement_mapt parse_replacement_list(const replacement_listt &replacement_list) const
void check_replacement_map(const replacement_mapt &replacement_map, const goto_functionst &goto_functions, const namespacet &ns) const
std::map< irep_idt, irep_idt > replacement_mapt
Definition: replace_calls.h:22
void operator()(goto_modelt &goto_model, const replacement_listt &replacement_list) const
Replace function calls with calls to other functions.
Expression to hold a symbol (variable)
Definition: std_expr.h:81
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:105
const irep_idt & get_identifier() const
Definition: std_expr.h:110
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
static int8_t r
Definition: irep_hash.h:59
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
Replace function returns by assignments to global variables.
Replace calls to given functions with calls to other given functions.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)