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 
23  const exprt &expr,
24  const symbolt *&symbol)
25 {
26  if(expr.id()==ID_symbol)
27  {
28  if(expr.get_bool(ID_C_invalid_object))
29  return false;
30 
31  const symbolt &ptr_symbol = ns.lookup(to_symbol_expr(expr));
32 
33  const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
34 
35  if(failed_symbol.empty())
36  return false;
37 
38  return !ns.lookup(failed_symbol, symbol);
39  }
40 
41  return false;
42 }
43 
45  const irep_idt &identifier)
46 {
47  const symbolt &symbol=ns.lookup(identifier);
48 
49  if(symbol.type.id()==ID_code)
50  return true;
51 
52  if(symbol.is_static_lifetime)
53  return true; // global/static
54 
55  #if 0
56  return valid_local_variables->find(symbol.name)!=
57  valid_local_variables->end(); // valid local
58  #else
59  return true;
60  #endif
61 }
62 
64  const std::string &property,
65  const std::string &msg,
66  const guardt &guard)
67 {
68  exprt guard_expr=guard.as_expr();
69 
70  if(assertions.insert(guard_expr).second)
71  {
72  guard_expr.make_not();
73 
74  // first try simplifier on it
75  if(options.get_bool_option("simplify"))
76  simplify(guard_expr, ns);
77 
78  if(!guard_expr.is_true())
79  {
81  options.get_bool_option("assert-to-assume")?ASSUME:ASSERT;
82 
84  t->guard.swap(guard_expr);
85  t->source_location=dereference_location;
86  t->source_location.set_property_class(property);
87  t->source_location.set_comment("dereference failure: "+msg);
88  }
89  }
90 }
91 
93  exprt &expr,
94  guardt &guard,
96 {
97  if(!has_subexpr(expr, ID_dereference))
98  return;
99 
100  if(expr.id()==ID_and || expr.id()==ID_or)
101  {
102  if(!expr.is_boolean())
103  throw expr.id_string()+" must be Boolean, but got "+
104  expr.pretty();
105 
106  guardt old_guard=guard;
107 
108  for(auto &op : expr.operands())
109  {
110  if(!op.is_boolean())
111  throw expr.id_string()+" takes Boolean operands only, but got "+
112  op.pretty();
113 
114  if(has_subexpr(op, ID_dereference))
116 
117  if(expr.id()==ID_or)
118  {
119  exprt tmp(op);
120  tmp.make_not();
121  guard.add(tmp);
122  }
123  else
124  guard.add(op);
125  }
126 
127  guard.swap(old_guard);
128 
129  return;
130  }
131  else if(expr.id()==ID_if)
132  {
133  if(expr.operands().size()!=3)
134  throw "if takes three arguments";
135 
136  if(!expr.op0().is_boolean())
137  {
138  std::string msg=
139  "first argument of if must be boolean, but got "
140  +expr.op0().pretty();
141  throw msg;
142  }
143 
145 
146  bool o1 = has_subexpr(expr.op1(), ID_dereference);
147  bool o2 = has_subexpr(expr.op2(), ID_dereference);
148 
149  if(o1)
150  {
151  guardt old_guard=guard;
152  guard.add(expr.op0());
153  dereference_rec(expr.op1(), guard, mode);
154  guard.swap(old_guard);
155  }
156 
157  if(o2)
158  {
159  guardt old_guard=guard;
160  exprt tmp(expr.op0());
161  tmp.make_not();
162  guard.add(tmp);
163  dereference_rec(expr.op2(), guard, mode);
164  guard.swap(old_guard);
165  }
166 
167  return;
168  }
169 
170  if(expr.id()==ID_address_of ||
171  expr.id()=="reference_to")
172  {
173  // turn &*p to p
174  // this has *no* side effect!
175 
176  assert(expr.operands().size()==1);
177 
178  if(expr.op0().id()==ID_dereference)
179  {
180  assert(expr.op0().operands().size()==1);
181 
182  exprt tmp;
183  tmp.swap(expr.op0().op0());
184 
185  if(tmp.type()!=expr.type())
186  tmp.make_typecast(expr.type());
187 
188  expr.swap(tmp);
189  }
190  }
191 
192  Forall_operands(it, expr)
193  dereference_rec(*it, guard, mode);
194 
195  if(expr.id()==ID_dereference)
196  {
197  if(expr.operands().size()!=1)
198  throw "dereference expects one operand";
199 
201 
203  expr.op0(), guard, mode);
204 
205  expr.swap(tmp);
206  }
207  else if(expr.id()==ID_index)
208  {
209  // this is old stuff and will go away
210 
211  if(expr.operands().size()!=2)
212  throw "index expects two operands";
213 
214  if(expr.op0().type().id()==ID_pointer)
215  {
217 
218  exprt tmp1(ID_plus, expr.op0().type());
219  tmp1.operands().swap(expr.operands());
220 
221  exprt tmp2=dereference.dereference(tmp1, guard, mode);
222  tmp2.swap(expr);
223  }
224  }
225 }
226 
228  const exprt &expr,
229  value_setst::valuest &dest)
230 {
231  value_sets.get_values(current_target, expr, dest);
232 }
233 
235  exprt &expr,
236  const bool checks_only,
238 {
239  guardt guard;
240 
241  if(checks_only)
242  {
243  exprt tmp(expr);
244  dereference_rec(tmp, guard, mode);
245  }
246  else
247  dereference_rec(expr, guard, mode);
248 }
249 
252  bool checks_only)
253 {
254  for(goto_programt::instructionst::iterator
255  it=goto_program.instructions.begin();
256  it!=goto_program.instructions.end();
257  it++)
258  {
259  new_code.clear();
260  assertions.clear();
261 
262  dereference_instruction(it, checks_only);
263 
264  // insert new instructions
265  while(!new_code.instructions.empty())
266  {
268  new_code.instructions.pop_front();
269  it++;
270  }
271  }
272 }
273 
275  goto_functionst &goto_functions,
276  bool checks_only)
277 {
278  for(goto_functionst::function_mapt::iterator
279  it=goto_functions.function_map.begin();
280  it!=goto_functions.function_map.end();
281  it++)
282  dereference_program(it->second.body, checks_only);
283 }
284 
286  goto_programt::targett target,
287  bool checks_only)
288 {
289  current_target=target;
290  #if 0
291  valid_local_variables=&target->local_variables;
292  #endif
293  goto_programt::instructiont &i=*target;
294 
296 
297  if(i.is_assign())
298  {
299  if(i.code.operands().size()!=2)
300  throw "assignment expects two operands";
301 
303  i.code.op0(), checks_only, value_set_dereferencet::modet::WRITE);
305  i.code.op1(), checks_only, value_set_dereferencet::modet::READ);
306  }
307  else if(i.is_function_call())
308  {
309  code_function_callt &function_call = to_code_function_call(i.code);
310 
311  if(function_call.lhs().is_not_nil())
313  function_call.lhs(),
314  checks_only,
316 
318  function_call.function(),
319  checks_only,
322  function_call.op2(), checks_only, value_set_dereferencet::modet::READ);
323  }
324  else if(i.is_return())
325  {
326  Forall_operands(it, i.code)
328  }
329  else if(i.is_other())
330  {
331  const irep_idt &statement=i.code.get(ID_statement);
332 
333  if(statement==ID_expression)
334  {
335  if(i.code.operands().size()!=1)
336  throw "expression expects one operand";
337 
339  i.code.op0(), checks_only, value_set_dereferencet::modet::READ);
340  }
341  else if(statement==ID_printf)
342  {
343  Forall_operands(it, i.code)
345  *it, checks_only, value_set_dereferencet::modet::READ);
346  }
347  }
348 }
349 
352  exprt &expr)
353 {
354  current_target=target;
355  #if 0
356  valid_local_variables=&target->local_variables;
357  #endif
358 
360 }
361 
364 {
366 }
367 
369  goto_functionst &goto_functions)
370 {
371  dereference_program(goto_functions, true);
372 }
373 
376  symbol_tablet &symbol_table,
377  value_setst &value_sets)
378 {
379  namespacet ns(symbol_table);
380 
381  optionst options;
382 
384  goto_program_dereference(ns, symbol_table, options, value_sets);
385 
386  goto_program_dereference.dereference_program(goto_program);
387 }
388 
390  goto_modelt &goto_model,
391  value_setst &value_sets)
392 {
393  namespacet ns(goto_model.symbol_table);
394 
395  optionst options;
396 
398  goto_program_dereference(
399  ns, goto_model.symbol_table, options, value_sets);
400 
401  Forall_goto_functions(it, goto_model.goto_functions)
402  goto_program_dereference.dereference_program(it->second.body);
403 }
404 
407  symbol_tablet &symbol_table,
408  const optionst &options,
409  value_setst &value_sets)
410 {
411  namespacet ns(symbol_table);
413  goto_program_dereference(ns, symbol_table, options, value_sets);
414  goto_program_dereference.pointer_checks(goto_program);
415 }
416 
418  goto_functionst &goto_functions,
419  symbol_tablet &symbol_table,
420  const optionst &options,
421  value_setst &value_sets)
422 {
423  namespacet ns(symbol_table);
425  goto_program_dereference(ns, symbol_table, options, value_sets);
426  goto_program_dereference.pointer_checks(goto_functions);
427 }
428 
431  exprt &expr,
432  const namespacet &ns,
433  value_setst &value_sets)
434 {
435  optionst options;
436  symbol_tablet new_symbol_table;
438  goto_program_dereference(ns, new_symbol_table, options, value_sets);
439  goto_program_dereference.dereference_expression(target, expr);
440 }
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
irep_idt name
The unique identifier.
Definition: symbol.h:43
exprt as_expr() const
Definition: guard.h:43
bool is_boolean() const
Definition: expr.cpp:156
bool is_not_nil() const
Definition: irep.h:173
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
virtual void get_values(goto_programt::const_targett l, const exprt &expr, valuest &dest)=0
void dereference(goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
exprt & op0()
Definition: expr.h:72
void set_property_class(const irep_idt &property_class)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
void remove_pointers(goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)
virtual bool is_valid_object(const irep_idt &identifier)
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
Deprecated expression utility functions.
goto_programt::const_targett current_target
bool is_true() const
Definition: expr.cpp:124
Definition: guard.h:19
function_mapt function_map
typet & type()
Definition: expr.h:56
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void dereference_rec(exprt &expr, guardt &guard, const value_set_dereferencet::modet mode)
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
bool is_static_lifetime
Definition: symbol.h:67
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
void clear()
Clear the goto program.
Definition: goto_program.h:611
virtual void get_value_set(const exprt &expr, value_setst::valuest &dest)
void pointer_checks(goto_programt &goto_program)
const irep_idt & id() const
Definition: irep.h:259
void pointer_checks(goto_programt &goto_program, symbol_tablet &symbol_table, const optionst &options, value_setst &value_sets)
instructionst::iterator targett
Definition: goto_program.h:397
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:138
const source_locationt & find_source_location() const
Definition: expr.cpp:246
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
exprt & op1()
Definition: expr.h:75
The symbol table.
Definition: symbol_table.h:19
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:29
A function call.
Definition: std_code.h:858
Guard Data Structure.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
typet type
Type of symbol.
Definition: symbol.h:34
void dereference_expr(exprt &expr, const bool checks_only, const value_set_dereferencet::modet mode)
void dereference_expression(goto_programt::const_targett target, exprt &expr)
void make_not()
Definition: expr.cpp:91
value_set_dereferencet dereference
void dereference_program(goto_programt &goto_program, bool checks_only=false)
exprt & function()
Definition: std_code.h:878
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)
#define Forall_goto_functions(it, functions)
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
const std::string & id_string() const
Definition: irep.h:262
void swap(irept &irep)
Definition: irep.h:303
#define Forall_operands(it, expr)
Definition: expr.h:23
goto_programt & goto_program
Definition: cover.cpp:63
exprt & op2()
Definition: expr.h:78
Options.
Base Type Computation.
operandst & operands()
Definition: expr.h:66
std::list< exprt > valuest
Definition: value_sets.h:28
bool empty() const
Definition: dstring.h:73
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
void add(const exprt &expr)
Definition: guard.cpp:64
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909
bool simplify(exprt &expr, const namespacet &ns)