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  const exprt &function = ins.call_function();
74 
75  PRECONDITION(function.id() == ID_symbol);
76 
77  const 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  // check that returns have not been removed
97  if(to_code_type(function.type()).return_type().id() != ID_empty)
98  {
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 exprt &rhs = next_it->assign_rhs();
103 
104  INVARIANT(
105  rhs != return_value_symbol(id, ns),
106  "returns must not be removed before replacing calls");
107  }
108  }
109 
110  // Finally modify the call
111  ins.call_function().type() = ns.lookup(f_it2->first).type;
113  }
114 }
115 
117  const replacement_listt &replacement_list) const
118 {
119  replacement_mapt replacement_map;
120 
121  for(const std::string &s : replacement_list)
122  {
123  std::string original;
124  std::string replacement;
125 
126  split_string(s, ':', original, replacement, true);
127 
128  const auto r =
129  replacement_map.insert(std::make_pair(original, replacement));
130 
131  if(!r.second)
132  {
134  "conflicting replacement for function " + original, "--replace-calls");
135  }
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())
150  "function " + id2string(p.second) +
151  " cannot both be replaced and be a replacement",
152  "--replace-calls");
153 
154  auto it2 = goto_functions.function_map.find(p.second);
155 
156  if(it2 == goto_functions.function_map.end())
158  "replacement function " + id2string(p.second) + " needs to be present",
159  "--replace-calls");
160 
161  auto it1 = goto_functions.function_map.find(p.first);
162  if(it1 != goto_functions.function_map.end())
163  {
164  if(!base_type_eq(
165  ns.lookup(it1->first).type, ns.lookup(it2->first).type, ns))
167  "functions " + id2string(p.first) + " and " + id2string(p.second) +
168  " are not type-compatible",
169  "--replace-calls");
170  }
171  }
172 }
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:291
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
typet & type()
Return the type of the expression.
Definition: expr.h:82
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
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:271
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
instructionst::const_iterator const_targett
Definition: goto_program.h:593
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:47
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)