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 
16 #include <util/base_type.h>
17 #include <util/exception_utils.h>
18 #include <util/invariant.h>
19 #include <util/namespace.h>
20 #include <util/string_utils.h>
21 
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 exprt &rhs = next_it->assign_rhs();
104 
105  INVARIANT(
106  rhs != return_value_symbol(id, ns),
107  "returns must not be removed before replacing calls");
108  }
109  }
110 
111  // Finally modify the call
112  function.type() = ns.lookup(f_it2->first).type;
113  se.set_identifier(new_id);
114 
115  ins.set_function_call(cfc);
116  }
117 }
118 
120  const replacement_listt &replacement_list) const
121 {
122  replacement_mapt replacement_map;
123 
124  for(const std::string &s : replacement_list)
125  {
126  std::string original;
127  std::string replacement;
128 
129  split_string(s, ':', original, replacement, true);
130 
131  const auto r =
132  replacement_map.insert(std::make_pair(original, replacement));
133 
134  if(!r.second)
135  {
137  "conflicting replacement for function " + original, "--replace-calls");
138  }
139  }
140 
141  return replacement_map;
142 }
143 
145  const replacement_mapt &replacement_map,
146  const goto_functionst &goto_functions,
147  const namespacet &ns) const
148 {
149  for(const auto &p : replacement_map)
150  {
151  if(replacement_map.find(p.second) != replacement_map.end())
153  "function " + id2string(p.second) +
154  " cannot both be replaced and be a replacement",
155  "--replace-calls");
156 
157  auto it2 = goto_functions.function_map.find(p.second);
158 
159  if(it2 == goto_functions.function_map.end())
161  "replacement function " + id2string(p.second) + " needs to be present",
162  "--replace-calls");
163 
164  auto it1 = goto_functions.function_map.find(p.first);
165  if(it1 != goto_functions.function_map.end())
166  {
167  if(!base_type_eq(
168  ns.lookup(it1->first).type, ns.lookup(it2->first).type, ns))
170  "functions " + id2string(p.first) + " and " + id2string(p.second) +
171  " are not type-compatible",
172  "--replace-calls");
173  }
174  }
175 }
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.
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:178
void set_function_call(code_function_callt c)
Set the function call for FUNCTION_CALL.
Definition: goto_program.h:409
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
Definition: goto_program.h:353
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
instructionst::const_iterator const_targett
Definition: goto_program.h:647
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:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
std::list< std::string > replacement_listt
Definition: replace_calls.h:29
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:30
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:80
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:104
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Symbol Table + CFG.
#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:60
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:510
#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:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)