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/invariant.h>
20 #include <util/irep.h>
21 #include <util/string_utils.h>
22 #include <util/suffix.h>
23 
30  goto_modelt &goto_model,
31  const replacement_listt &replacement_list) const
32 {
33  replacement_mapt replacement_map = parse_replacement_list(replacement_list);
34  (*this)(goto_model, replacement_map);
35 }
36 
42  goto_modelt &goto_model,
43  const replacement_mapt &replacement_map) const
44 {
45  const namespacet ns(goto_model.symbol_table);
46  goto_functionst &goto_functions = goto_model.goto_functions;
47 
48  check_replacement_map(replacement_map, goto_functions, ns);
49 
50  for(auto &p : goto_functions.function_map)
51  {
52  goto_functionst::goto_functiont &goto_function = p.second;
53  goto_programt &goto_program = goto_function.body;
54 
55  (*this)(goto_program, goto_functions, ns, replacement_map);
56  }
57 }
58 
61  const goto_functionst &goto_functions,
62  const namespacet &ns,
63  const replacement_mapt &replacement_map) const
64 {
66  {
67  goto_programt::instructiont &ins = *it;
68 
69  if(!ins.is_function_call())
70  continue;
71 
73  exprt &function = cfc.function();
74 
75  PRECONDITION(function.id() == ID_symbol);
76 
77  symbol_exprt &se = to_symbol_expr(function);
78  const irep_idt &id = se.get_identifier();
79 
80  auto f_it1 = goto_functions.function_map.find(id);
81 
83  f_it1 != goto_functions.function_map.end(),
84  "Called functions need to be present");
85 
86  replacement_mapt::const_iterator r_it = replacement_map.find(id);
87 
88  if(r_it == replacement_map.end())
89  continue;
90 
91  const irep_idt &new_id = r_it->second;
92 
93  auto f_it2 = goto_functions.function_map.find(new_id);
94  PRECONDITION(f_it2 != goto_functions.function_map.end());
95 
96  PRECONDITION(base_type_eq(f_it1->second.type, f_it2->second.type, ns));
97 
98  // check that returns have not been removed
99  goto_programt::const_targett next_it = std::next(it);
100  if(next_it != goto_program.instructions.end() && next_it->is_assign())
101  {
102  const code_assignt &ca = to_code_assign(next_it->code);
103  const exprt &rhs = ca.rhs();
104 
105  if(rhs.id() == ID_symbol)
106  {
107  const symbol_exprt &se = to_symbol_expr(rhs);
109  throw "Returns must not be removed before replacing calls";
110  }
111  }
112 
113  // Finally modify the call
114  function.type() = f_it2->second.type;
115  se.set_identifier(new_id);
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  throw "Conflicting replacement for function " + original;
136  }
137 
138  return replacement_map;
139 }
140 
142  const replacement_mapt &replacement_map,
143  const goto_functionst &goto_functions,
144  const namespacet &ns) const
145 {
146  for(const auto &p : replacement_map)
147  {
148  if(replacement_map.find(p.second) != replacement_map.end())
149  throw "Function " + id2string(p.second) +
150  " cannot both be replaced and "
151  "be a replacement";
152 
153  auto it2 = goto_functions.function_map.find(p.second);
154 
155  if(it2 == goto_functions.function_map.end())
156  throw "Replacement function " + id2string(p.second) +
157  " needs to be present";
158 
159  auto it1 = goto_functions.function_map.find(p.first);
160  if(it1 != goto_functions.function_map.end())
161  {
162  if(!base_type_eq(it1->second.type, it2->second.type, ns))
163  throw "Functions " + id2string(p.first) + " and " +
164  id2string(p.second) + " are not type-compatible";
165  }
166  }
167 }
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)
Definition: base_type.cpp:326
const irep_idt & get_identifier() const
Definition: std_expr.h:128
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:173
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
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:214
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
A function call.
Definition: std_code.h:858
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
Remove function returns.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
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:878
Base class for all expressions.
Definition: expr.h:42
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:123
goto_programt & goto_program
Definition: cover.cpp:63
std::list< std::string > replacement_listt
Definition: replace_calls.h:21
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
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)
Definition: invariant.h:278
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
std::map< irep_idt, irep_idt > replacement_mapt
Definition: replace_calls.h:22
Assignment.
Definition: std_code.h:196
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909