cprover
value_set_fi_fp_removal.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: value_set_fi_Fp_removal
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
10
12
14
15#include <util/c_types.h>
16#include <util/fresh_symbol.h>
17#include <util/message.h>
18#include <util/namespace.h>
19#include <util/pointer_expr.h>
20#include <util/std_code.h>
21
22#ifdef USE_STD_STRING
23# include <util/dstring.h>
24#endif
25
27 code_function_callt &function_call,
28 const namespacet &ns)
29{
30 const code_typet &code_type =
31 to_code_type(ns.follow(function_call.function().type()));
32
33 const code_typet::parameterst &function_parameters = code_type.parameters();
34
35 code_function_callt::argumentst &call_arguments = function_call.arguments();
36
37 for(std::size_t i = 0; i < function_parameters.size(); i++)
38 {
39 // casting pointers might result in more arguments than function parameters
40 if(i < call_arguments.size())
41 {
42 call_arguments[i] = typecast_exprt::conditional_cast(
43 call_arguments[i], function_parameters[i].type());
44 }
45 }
46}
47
49 code_function_callt &function_call,
50 goto_programt &dest,
51 goto_modelt &goto_model)
52{
53 // are we returning anything at all?
54 if(function_call.lhs().is_nil())
55 return;
56
57 const namespacet ns(goto_model.symbol_table);
58
59 const code_typet &code_type =
60 to_code_type(ns.follow(function_call.function().type()));
61
62 // type already ok?
63 if(function_call.lhs().type() == code_type.return_type())
64 return;
65
66 const symbolt &function_symbol =
67 ns.lookup(to_symbol_expr(function_call.function()).get_identifier());
68
69 symbolt &tmp_symbol = get_fresh_aux_symbol(
70 code_type.return_type(),
71 id2string(function_call.source_location().get_function()),
72 "tmp_return_val_" + id2string(function_symbol.base_name),
73 function_call.source_location(),
74 function_symbol.mode,
75 goto_model.symbol_table);
76
77 const symbol_exprt tmp_symbol_expr = tmp_symbol.symbol_expr();
78
79 exprt old_lhs = function_call.lhs();
80 function_call.lhs() = tmp_symbol_expr;
81
83 code_assignt(old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()))));
84}
85
87 goto_programt &goto_program,
89 const std::set<symbol_exprt> &functions,
90 goto_modelt &goto_model)
91{
92 const exprt &function = as_const(*target).call_function();
93 PRECONDITION(function.id() == ID_dereference);
94
95 // this better have the right type
96 code_typet call_type = to_code_type(function.type());
97
98 // refine the type in case the forward declaration was incomplete
99 if(call_type.has_ellipsis() && call_type.parameters().empty())
100 {
101 call_type.remove_ellipsis();
102 for(const auto &argument : as_const(*target).call_arguments())
103 call_type.parameters().push_back(code_typet::parametert(argument.type()));
104 }
105
106 const exprt &pointer = to_dereference_expr(function).pointer();
107
108 // the final target is a skip
109 goto_programt final_skip;
111
112 // build the calls and gotos
113
114 goto_programt new_code_calls;
115 goto_programt new_code_gotos;
116
117 for(const auto &fun : functions)
118 {
119 // call function
122 as_const(*target).call_lhs(),
123 fun,
124 as_const(*target).call_arguments(),
125 target->source_location()));
126
127 // the signature of the function might not match precisely
128 const namespacet ns(goto_model.symbol_table);
129 fix_argument_types(to_code_function_call(t1->code_nonconst()), ns);
131 to_code_function_call(t1->code_nonconst()), new_code_calls, goto_model);
132
133 // goto final
134 new_code_calls.add(goto_programt::make_goto(t_final, true_exprt()));
135
136 // goto to call
137 address_of_exprt address_of(fun, pointer_type(fun.type()));
138
139 new_code_gotos.add(goto_programt::make_goto(
140 t1,
142 pointer,
143 typecast_exprt::conditional_cast(address_of, pointer.type()))));
144 }
145
148 t->source_location_nonconst().set_property_class("pointer dereference");
149 t->source_location_nonconst().set_comment("invalid function pointer");
150
151 goto_programt new_code;
152
153 // patch them all together
154 new_code.destructive_append(new_code_gotos);
155 new_code.destructive_append(new_code_calls);
156 new_code.destructive_append(final_skip);
157
158 // set locations
159 for(auto &instruction : new_code.instructions)
160 {
161 irep_idt property_class =
162 instruction.source_location().get_property_class();
163 irep_idt comment = instruction.source_location().get_comment();
164 instruction.source_location_nonconst() = target->source_location();
165 if(!property_class.empty())
166 instruction.source_location_nonconst().set_property_class(property_class);
167 if(!comment.empty())
168 instruction.source_location_nonconst().set_comment(comment);
169 }
170
171 goto_programt::targett next_target = target;
172 next_target++;
173
174 goto_program.destructive_insert(next_target, new_code);
175
176 // We preserve the original dereferencing to possibly catch
177 // further pointer-related errors.
179 code_expressiont(function), function.source_location());
180}
181
183 goto_modelt &goto_model,
184 message_handlert &message_handler)
185{
186 messaget message(message_handler);
187 message.status() << "Doing FI value set analysis" << messaget::eom;
188
189 const namespacet ns(goto_model.symbol_table);
190 value_set_analysis_fit value_sets(ns);
191 value_sets(goto_model.goto_functions);
192
193 message.status() << "Instrumenting" << messaget::eom;
194
195 // now replace aliases by addresses
196 for(auto &f : goto_model.goto_functions.function_map)
197 {
198 for(auto target = f.second.body.instructions.begin();
199 target != f.second.body.instructions.end();
200 target++)
201 {
202 if(target->is_function_call())
203 {
204 const auto &function = as_const(*target).call_function();
205 if(function.id() == ID_dereference)
206 {
207 message.status() << "CALL at " << target->source_location() << ":"
208 << messaget::eom;
209
210 const auto &pointer = to_dereference_expr(function).pointer();
211 auto addresses = value_sets.get_values(f.first, target, pointer);
212
213 std::set<symbol_exprt> functions;
214
215 for(const auto &address : addresses)
216 {
217 // is this a plain function address?
218 // strip leading '&'
219 if(address.id() == ID_object_descriptor)
220 {
221 const auto &od = to_object_descriptor_expr(address);
222 const auto &object = od.object();
223 if(object.type().id() == ID_code && object.id() == ID_symbol)
224 functions.insert(to_symbol_expr(object));
225 }
226 }
227
228 for(const auto &f : functions)
229 message.status()
230 << " function: " << f.get_identifier() << messaget::eom;
231
232 if(functions.size() > 0)
234 f.second.body, target, functions, goto_model);
235 }
236 }
237 }
238 }
239 goto_model.goto_functions.update();
240}
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
Operator to return the address of an object.
Definition: pointer_expr.h:361
A codet representing an assignment in the program.
codet representation of an expression statement.
Definition: std_code.h:1394
codet representation of a function call statement.
exprt::operandst argumentst
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:542
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
void remove_ellipsis()
Definition: std_types.h:640
bool has_ellipsis() const
Definition: std_types.h:611
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
const source_locationt & source_location() const
Definition: expr.h:230
The Boolean constant false.
Definition: std_expr.h:2865
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
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
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:706
instructionst::iterator targett
Definition: goto_program.h:592
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:698
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:880
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:942
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
source_locationt source_location
Definition: message.h:247
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
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
const irep_idt & get_function() const
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2856
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
std::vector< exprt > get_values(const irep_idt &function_id, locationt l, const exprt &expr) override
Container for C-Strings.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
const code_function_callt & to_code_function_call(const codet &code)
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
API to expression classes for Pointers.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: pointer_expr.h:238
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
#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
Value Set Propagation (flow insensitive)
void value_set_fi_fp_removal(goto_modelt &goto_model, message_handlert &message_handler)
Builds the flow-insensitive value set for all function pointers and replaces function pointers with a...
void remove_function_pointer(goto_programt &goto_program, goto_programt::targett target, const std::set< symbol_exprt > &functions, goto_modelt &goto_model)
void fix_return_type(code_function_callt &function_call, goto_programt &dest, goto_modelt &goto_model)
void fix_argument_types(code_function_callt &function_call, const namespacet &ns)
flow insensitive value set function pointer removal