cprover
goto_program_dereference.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dereferencing Operations on GOTO Programs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/expr_util.h>
15 #include <util/simplify_expr.h>
16 #include <util/base_type.h>
17 #include <util/std_code.h>
18 #include <util/symbol_table.h>
19 #include <util/guard.h>
20 #include <util/options.h>
21 
28  const exprt &expr,
29  const symbolt *&symbol)
30 {
31  if(expr.id()==ID_symbol)
32  {
33  if(expr.get_bool(ID_C_invalid_object))
34  return false;
35 
36  const symbolt &ptr_symbol = ns.lookup(to_symbol_expr(expr));
37 
38  const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
39 
40  if(failed_symbol.empty())
41  return false;
42 
43  return !ns.lookup(failed_symbol, symbol);
44  }
45 
46  return false;
47 }
48 
51  const irep_idt &identifier)
52 {
53  const symbolt &symbol=ns.lookup(identifier);
54 
55  if(symbol.type.id()==ID_code)
56  return true;
57 
58  if(symbol.is_static_lifetime)
59  return true; // global/static
60 
61  #if 0
62  return valid_local_variables->find(symbol.name)!=
63  valid_local_variables->end(); // valid local
64  #else
65  return true;
66  #endif
67 }
68 
71  const std::string &property,
72  const std::string &msg,
73  const guardt &guard)
74 {
75  exprt guard_expr=guard.as_expr();
76 
77  if(assertions.insert(guard_expr).second)
78  {
79  guard_expr = boolean_negate(guard_expr);
80 
81  // first try simplifier on it
82  if(options.get_bool_option("simplify"))
83  simplify(guard_expr, ns);
84 
85  if(!guard_expr.is_true())
86  {
88  options.get_bool_option("assert-to-assume")?ASSUME:ASSERT;
89 
91  t->guard.swap(guard_expr);
92  t->source_location=dereference_location;
93  t->source_location.set_property_class(property);
94  t->source_location.set_comment("dereference failure: "+msg);
95  }
96  }
97 }
98 
105  exprt &expr,
106  guardt &guard,
108 {
109  if(!has_subexpr(expr, ID_dereference))
110  return;
111 
112  if(expr.id()==ID_and || expr.id()==ID_or)
113  {
114  if(!expr.is_boolean())
115  throw expr.id_string()+" must be Boolean, but got "+
116  expr.pretty();
117 
118  guardt old_guard=guard;
119 
120  for(auto &op : expr.operands())
121  {
122  if(!op.is_boolean())
123  throw expr.id_string()+" takes Boolean operands only, but got "+
124  op.pretty();
125 
126  if(has_subexpr(op, ID_dereference))
128 
129  if(expr.id()==ID_or)
130  guard.add(boolean_negate(op));
131  else
132  guard.add(op);
133  }
134 
135  guard.swap(old_guard);
136 
137  return;
138  }
139  else if(expr.id()==ID_if)
140  {
141  if(expr.operands().size()!=3)
142  throw "if takes three arguments";
143 
144  if(!expr.op0().is_boolean())
145  {
146  std::string msg=
147  "first argument of if must be boolean, but got "
148  +expr.op0().pretty();
149  throw msg;
150  }
151 
153 
154  bool o1 = has_subexpr(expr.op1(), ID_dereference);
155  bool o2 = has_subexpr(expr.op2(), ID_dereference);
156 
157  if(o1)
158  {
159  guardt old_guard=guard;
160  guard.add(expr.op0());
161  dereference_rec(expr.op1(), guard, mode);
162  guard.swap(old_guard);
163  }
164 
165  if(o2)
166  {
167  guardt old_guard=guard;
168  guard.add(boolean_negate(expr.op0()));
169  dereference_rec(expr.op2(), guard, mode);
170  guard.swap(old_guard);
171  }
172 
173  return;
174  }
175 
176  if(expr.id()==ID_address_of ||
177  expr.id()=="reference_to")
178  {
179  // turn &*p to p
180  // this has *no* side effect!
181 
182  assert(expr.operands().size()==1);
183 
184  if(expr.op0().id()==ID_dereference)
185  {
186  assert(expr.op0().operands().size()==1);
187 
188  exprt tmp;
189  tmp.swap(expr.op0().op0());
190 
191  if(tmp.type()!=expr.type())
192  tmp.make_typecast(expr.type());
193 
194  expr.swap(tmp);
195  }
196  }
197 
198  Forall_operands(it, expr)
199  dereference_rec(*it, guard, mode);
200 
201  if(expr.id()==ID_dereference)
202  {
203  if(expr.operands().size()!=1)
204  throw "dereference expects one operand";
205 
207 
209  expr.op0(), guard, mode);
210 
211  expr.swap(tmp);
212  }
213  else if(expr.id()==ID_index)
214  {
215  // this is old stuff and will go away
216 
217  if(expr.operands().size()!=2)
218  throw "index expects two operands";
219 
220  if(expr.op0().type().id()==ID_pointer)
221  {
223 
224  exprt tmp1(ID_plus, expr.op0().type());
225  tmp1.operands().swap(expr.operands());
226 
227  exprt tmp2=dereference.dereference(tmp1, guard, mode);
228  tmp2.swap(expr);
229  }
230  }
231 }
232 
238  const exprt &expr,
239  value_setst::valuest &dest)
240 {
241  value_sets.get_values(current_target, expr, dest);
242 }
243 
251  exprt &expr,
252  const bool checks_only,
254 {
255  guardt guard;
256 
257  if(checks_only)
258  {
259  exprt tmp(expr);
260  dereference_rec(tmp, guard, mode);
261  }
262  else
263  dereference_rec(expr, guard, mode);
264 }
265 
267  goto_programt &goto_program,
268  bool checks_only)
269 {
270  for(goto_programt::instructionst::iterator
271  it=goto_program.instructions.begin();
272  it!=goto_program.instructions.end();
273  it++)
274  {
275  new_code.clear();
276  assertions.clear();
277 
278  dereference_instruction(it, checks_only);
279 
280  // insert new instructions
281  while(!new_code.instructions.empty())
282  {
283  goto_program.insert_before_swap(it, new_code.instructions.front());
284  new_code.instructions.pop_front();
285  it++;
286  }
287  }
288 }
289 
291  goto_functionst &goto_functions,
292  bool checks_only)
293 {
294  for(goto_functionst::function_mapt::iterator
295  it=goto_functions.function_map.begin();
296  it!=goto_functions.function_map.end();
297  it++)
298  dereference_program(it->second.body, checks_only);
299 }
300 
306  goto_programt::targett target,
307  bool checks_only)
308 {
309  current_target=target;
310  #if 0
311  valid_local_variables=&target->local_variables;
312  #endif
313  goto_programt::instructiont &i=*target;
314 
316 
317  if(i.is_assign())
318  {
319  if(i.code.operands().size()!=2)
320  throw "assignment expects two operands";
321 
323  i.code.op0(), checks_only, value_set_dereferencet::modet::WRITE);
325  i.code.op1(), checks_only, value_set_dereferencet::modet::READ);
326  }
327  else if(i.is_function_call())
328  {
329  code_function_callt &function_call = to_code_function_call(i.code);
330 
331  if(function_call.lhs().is_not_nil())
333  function_call.lhs(),
334  checks_only,
336 
338  function_call.function(),
339  checks_only,
342  function_call.op2(), checks_only, value_set_dereferencet::modet::READ);
343  }
344  else if(i.is_return())
345  {
346  Forall_operands(it, i.code)
348  }
349  else if(i.is_other())
350  {
351  const irep_idt &statement=i.code.get(ID_statement);
352 
353  if(statement==ID_expression)
354  {
355  if(i.code.operands().size()!=1)
356  throw "expression expects one operand";
357 
359  i.code.op0(), checks_only, value_set_dereferencet::modet::READ);
360  }
361  else if(statement==ID_printf)
362  {
363  Forall_operands(it, i.code)
365  *it, checks_only, value_set_dereferencet::modet::READ);
366  }
367  }
368 }
369 
373  exprt &expr)
374 {
375  current_target=target;
376  #if 0
377  valid_local_variables=&target->local_variables;
378  #endif
379 
381 }
382 
386  goto_programt &goto_program)
387 {
388  dereference_program(goto_program, true);
389 }
390 
394  goto_functionst &goto_functions)
395 {
396  dereference_program(goto_functions, true);
397 }
398 
401  goto_programt &goto_program,
402  symbol_tablet &symbol_table,
403  value_setst &value_sets)
404 {
405  namespacet ns(symbol_table);
406 
407  optionst options;
408 
410  goto_program_dereference(ns, symbol_table, options, value_sets);
411 
412  goto_program_dereference.dereference_program(goto_program);
413 }
414 
419  goto_modelt &goto_model,
420  value_setst &value_sets)
421 {
422  namespacet ns(goto_model.symbol_table);
423 
424  optionst options;
425 
427  goto_program_dereference(
428  ns, goto_model.symbol_table, options, value_sets);
429 
430  Forall_goto_functions(it, goto_model.goto_functions)
431  goto_program_dereference.dereference_program(it->second.body);
432 }
433 
436  goto_programt &goto_program,
437  symbol_tablet &symbol_table,
438  const optionst &options,
439  value_setst &value_sets)
440 {
441  namespacet ns(symbol_table);
443  goto_program_dereference(ns, symbol_table, options, value_sets);
444  goto_program_dereference.pointer_checks(goto_program);
445 }
446 
449  goto_functionst &goto_functions,
450  symbol_tablet &symbol_table,
451  const optionst &options,
452  value_setst &value_sets)
453 {
454  namespacet ns(symbol_table);
456  goto_program_dereference(ns, symbol_table, options, value_sets);
457  goto_program_dereference.pointer_checks(goto_functions);
458 }
459 
464  exprt &expr,
465  const namespacet &ns,
466  value_setst &value_sets)
467 {
468  optionst options;
469  symbol_tablet new_symbol_table;
471  goto_program_dereference(ns, new_symbol_table, options, value_sets);
472  goto_program_dereference.dereference_expression(target, expr);
473 }
exprt::op2
exprt & op2()
Definition: expr.h:90
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
has_subexpr
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:139
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
goto_program_dereferencet::assertions
std::set< exprt > assertions
Unused.
Definition: goto_program_dereference.h:102
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:313
optionst
Definition: options.h:22
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
guardt::add
void add(const exprt &expr)
Definition: guard.cpp:43
goto_program_dereferencet::is_valid_object
virtual bool is_valid_object(const irep_idt &identifier)
Definition: goto_program_dereference.cpp:50
goto_program_dereferencet::options
const optionst & options
Definition: goto_program_dereference.h:63
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:24
value_set_dereferencet::dereference
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
Dereference the given pointer-expression.
Definition: value_set_dereference.cpp:35
exprt::op0
exprt & op0()
Definition: expr.h:84
options.h
value_setst::get_values
virtual void get_values(goto_programt::const_targett l, const exprt &expr, valuest &dest)=0
goto_program_dereferencet::value_sets
value_setst & value_sets
Definition: goto_program_dereference.h:65
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
value_set_dereferencet::modet::READ
@ READ
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1089
value_set_dereferencet::modet::WRITE
@ WRITE
goto_program_dereferencet::has_failed_symbol
bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override
Definition: goto_program_dereference.cpp:27
pointer_checks
void pointer_checks(goto_programt &goto_program, symbol_tablet &symbol_table, const optionst &options, value_setst &value_sets)
Definition: goto_program_dereference.cpp:435
goto_program_dereferencet::dereference
value_set_dereferencet dereference
Definition: goto_program_dereference.h:66
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
guard.h
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
goto_program_dereferencet::dereference_expression
void dereference_expression(goto_programt::const_targett target, exprt &expr)
Set the current target to target and remove derefence from expr.
Definition: goto_program_dereference.cpp:371
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
guardt
Definition: guard.h:19
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
base_type.h
value_setst::valuest
std::list< exprt > valuest
Definition: value_sets.h:28
dereference
void dereference(goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
Definition: goto_program_dereference.cpp:462
goto_programt::instructiont::code
codet code
Definition: goto_program.h:181
goto_program_dereferencet::dereference_location
source_locationt dereference_location
Unused.
Definition: goto_program_dereference.h:99
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:229
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:127
goto_program_dereferencet
Wrapper for functions removing dereferences in expressions contained in a goto program.
Definition: goto_program_dereference.h:24
irept::id_string
const std::string & id_string() const
Definition: irep.h:262
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2320
exprt::op1
exprt & op1()
Definition: expr.h:87
irept::swap
void swap(irept &irep)
Definition: irep.h:303
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
dstringt::empty
bool empty() const
Definition: dstring.h:75
std_code.h
goto_program_dereferencet::pointer_checks
void pointer_checks(goto_programt &goto_program)
Throw an exception in case removing dereferences from the program would throw an exception.
Definition: goto_program_dereference.cpp:385
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:144
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:647
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:31
goto_program_dereferencet::get_value_set
void get_value_set(const exprt &expr, value_setst::valuest &dest) override
Gets the value set corresponding to the current target and expression expr.
Definition: goto_program_dereference.cpp:237
simplify_expr.h
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
expr_util.h
Deprecated expression utility functions.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
value_setst
Definition: value_sets.h:21
goto_program_dereferencet::dereference_instruction
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
Remove dereference from expressions contained in the instruction at target.
Definition: goto_program_dereference.cpp:305
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
goto_program_dereferencet::dereference_expr
void dereference_expr(exprt &expr, const bool checks_only, const value_set_dereferencet::modet mode)
Remove dereference expressions contained in expr.
Definition: goto_program_dereference.cpp:250
symbolt
Symbol table entry.
Definition: symbol.h:27
ASSUME
@ ASSUME
Definition: goto_program.h:35
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
goto_program_dereference.h
goto_programt::instructiont::guard
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:307
goto_program_dereferencet::dereference_program
void dereference_program(goto_programt &goto_program, bool checks_only=false)
Definition: goto_program_dereference.cpp:266
goto_program_dereferencet::new_code
goto_programt new_code
Unused.
Definition: goto_program_dereference.h:105
guardt::as_expr
exprt as_expr() const
Definition: guard.h:41
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
value_set_dereferencet::modet
modet
Definition: value_set_dereference.h:53
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
goto_program_dereferencet::current_target
goto_programt::const_targett current_target
Definition: goto_program_dereference.h:96
exprt::operands
operandst & operands()
Definition: expr.h:78
goto_program_dereferencet::dereference_failure
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)
Definition: goto_program_dereference.cpp:70
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
symbol_table.h
Author: Diffblue Ltd.
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
remove_pointers
void remove_pointers(goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)
Definition: goto_program_dereference.cpp:400
goto_program_dereferencet::dereference_rec
void dereference_rec(exprt &expr, guardt &guard, const value_set_dereferencet::modet mode)
Turn subexpression of expr of the form &*p or reference_to(*p) to p and use dereference on subexpress...
Definition: goto_program_dereference.cpp:104
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:308
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:117
ASSERT
@ ASSERT
Definition: goto_program.h:36
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
goto_program_dereferencet::ns
const namespacet & ns
Definition: goto_program_dereference.h:64
goto_programt::instructiont::is_return
bool is_return() const
Definition: goto_program.h:306
source_locationt::set_property_class
void set_property_class(const irep_idt &property_class)
Definition: source_location.h:132