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 
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  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 = to_code_assign(next_it->code);
104  const exprt &rhs = ca.rhs();
105 
106  if(rhs.id() == ID_symbol)
107  {
108  const symbol_exprt &se = to_symbol_expr(rhs);
109  INVARIANT(
111  "returns must not be removed before replacing calls");
112  }
113  }
114 
115  // Finally modify the call
116  function.type() = f_it2->second.type;
117  se.set_identifier(new_id);
118  }
119 }
120 
122  const replacement_listt &replacement_list) const
123 {
124  replacement_mapt replacement_map;
125 
126  for(const std::string &s : replacement_list)
127  {
128  std::string original;
129  std::string replacement;
130 
131  split_string(s, ':', original, replacement, true);
132 
133  const auto r =
134  replacement_map.insert(std::make_pair(original, replacement));
135 
136  if(!r.second)
137  {
139  "conflicting replacement for function " + original, "--replace-calls");
140  }
141  }
142 
143  return replacement_map;
144 }
145 
147  const replacement_mapt &replacement_map,
148  const goto_functionst &goto_functions,
149  const namespacet &ns) const
150 {
151  for(const auto &p : replacement_map)
152  {
153  if(replacement_map.find(p.second) != replacement_map.end())
155  "function " + id2string(p.second) +
156  " cannot both be replaced and be a replacement",
157  "--replace-calls");
158 
159  auto it2 = goto_functions.function_map.find(p.second);
160 
161  if(it2 == goto_functions.function_map.end())
163  "replacement function " + id2string(p.second) + " needs to be present",
164  "--replace-calls");
165 
166  auto it1 = goto_functions.function_map.find(p.first);
167  if(it1 != goto_functions.function_map.end())
168  {
169  if(!base_type_eq(it1->second.type, it2->second.type, ns))
171  "functions " + id2string(p.first) + " and " + id2string(p.second) +
172  " are not type-compatible",
173  "--replace-calls");
174  }
175  }
176 }
static int8_t r
Definition: irep_hash.h:59
void check_replacement_map(const replacement_mapt &replacement_map, const goto_functionst &goto_functions, const namespacet &ns) const
replacement_mapt parse_replacement_list(const replacement_listt &replacement_list) const
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:332
const irep_idt & get_identifier() const
Definition: std_expr.h:176
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
const irep_idt & id() const
Definition: irep.h:259
void operator()(goto_modelt &goto_model, const replacement_listt &replacement_list) const
Replace function calls with calls to other functions.
exprt & rhs()
Definition: std_code.h:274
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
instructionst::const_iterator const_targett
Definition: goto_program.h:415
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
codet representation of a function call statement.
Definition: std_code.h:1036
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Remove function returns.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Given a string s, split into a sequence of substrings when separated by specified delimiter.
Replace calls to given functions with calls to other given functions.
exprt & function()
Definition: std_code.h:1099
Base class for all expressions.
Definition: expr.h:54
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:171
std::list< std::string > replacement_listt
Definition: replace_calls.h:21
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
#define RETURN_VALUE_SUFFIX
Base Type Computation.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
std::map< irep_idt, irep_idt > replacement_mapt
Definition: replace_calls.h:22
A codet representing an assignment in the program.
Definition: std_code.h:256
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173