cprover
Loading...
Searching...
No Matches
replace_calls.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Replace calls
4
5Author: Daniel Poetzl
6
7\*******************************************************************/
8
13
14#include "replace_calls.h"
15
16#include <util/base_type.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 {
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.
const typet & return_type() const
Definition: std_types.h:645
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 ...
const irep_idt & id() const
Definition: irep.h:396
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
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)