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