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/simplify_expr.h>
15 #include <util/base_type.h>
16 #include <util/std_code.h>
17 #include <util/symbol_table.h>
18 #include <util/guard.h>
19 #include <util/options.h>
20 
22  const exprt &expr,
23  const symbolt *&symbol)
24 {
25  if(expr.id()==ID_symbol)
26  {
27  if(expr.get_bool("#invalid_object"))
28  return false;
29 
30  const symbolt &ptr_symbol=ns.lookup(expr);
31 
32  const irep_idt &failed_symbol=
33  ptr_symbol.type.get("#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  if(valid_local_variables->find(symbol.name)!=
57  valid_local_variables->end())
58  return true; // valid local
59  #else
60  return true;
61  #endif
62 
63  return false;
64 }
65 
67  const std::string &property,
68  const std::string &msg,
69  const guardt &guard)
70 {
71  exprt guard_expr=guard.as_expr();
72 
73  if(assertions.insert(guard_expr).second)
74  {
75  guard_expr.make_not();
76 
77  // first try simplifier on it
78  if(options.get_bool_option("simplify"))
79  simplify(guard_expr, ns);
80 
81  if(!guard_expr.is_true())
82  {
84  options.get_bool_option("assert-to-assume")?ASSUME:ASSERT;
85 
87  t->guard.swap(guard_expr);
88  t->source_location=dereference_location;
89  t->source_location.set_property_class(property);
90  t->source_location.set_comment("dereference failure: "+msg);
91  }
92  }
93 }
94 
96  exprt &expr,
97  guardt &guard,
99 {
100  if(!dereference.has_dereference(expr))
101  return;
102 
103  if(expr.id()==ID_and || expr.id()==ID_or)
104  {
105  if(!expr.is_boolean())
106  throw expr.id_string()+" must be Boolean, but got "+
107  expr.pretty();
108 
109  guardt old_guard=guard;
110 
111  for(unsigned i=0; i<expr.operands().size(); i++)
112  {
113  exprt &op=expr.operands()[i];
114 
115  if(!op.is_boolean())
116  throw expr.id_string()+" takes Boolean operands only, but got "+
117  op.pretty();
118 
121 
122  if(expr.id()==ID_or)
123  {
124  exprt tmp(op);
125  tmp.make_not();
126  guard.add(tmp);
127  }
128  else
129  guard.add(op);
130  }
131 
132  guard.swap(old_guard);
133 
134  return;
135  }
136  else if(expr.id()==ID_if)
137  {
138  if(expr.operands().size()!=3)
139  throw "if takes three arguments";
140 
141  if(!expr.op0().is_boolean())
142  {
143  std::string msg=
144  "first argument of if must be boolean, but got "
145  +expr.op0().pretty();
146  throw msg;
147  }
148 
150 
151  bool o1=dereference.has_dereference(expr.op1());
152  bool o2=dereference.has_dereference(expr.op2());
153 
154  if(o1)
155  {
156  guardt old_guard=guard;
157  guard.add(expr.op0());
158  dereference_rec(expr.op1(), guard, mode);
159  guard.swap(old_guard);
160  }
161 
162  if(o2)
163  {
164  guardt old_guard=guard;
165  exprt tmp(expr.op0());
166  tmp.make_not();
167  guard.add(tmp);
168  dereference_rec(expr.op2(), guard, mode);
169  guard.swap(old_guard);
170  }
171 
172  return;
173  }
174 
175  if(expr.id()==ID_address_of ||
176  expr.id()=="reference_to")
177  {
178  // turn &*p to p
179  // this has *no* side effect!
180 
181  assert(expr.operands().size()==1);
182 
183  if(expr.op0().id()==ID_dereference)
184  {
185  assert(expr.op0().operands().size()==1);
186 
187  exprt tmp;
188  tmp.swap(expr.op0().op0());
189 
190  if(tmp.type()!=expr.type())
191  tmp.make_typecast(expr.type());
192 
193  expr.swap(tmp);
194  }
195  }
196 
197  Forall_operands(it, expr)
198  dereference_rec(*it, guard, mode);
199 
200  if(expr.id()==ID_dereference)
201  {
202  if(expr.operands().size()!=1)
203  throw "dereference expects one operand";
204 
206 
208  expr.op0(), guard, mode);
209 
210  expr.swap(tmp);
211  }
212  else if(expr.id()==ID_index)
213  {
214  // this is old stuff and will go away
215 
216  if(expr.operands().size()!=2)
217  throw "index expects two operands";
218 
219  if(expr.op0().type().id()==ID_pointer)
220  {
222 
223  exprt tmp1(ID_plus, expr.op0().type());
224  tmp1.operands().swap(expr.operands());
225 
226  exprt tmp2=dereference.dereference(tmp1, guard, mode);
227  tmp2.swap(expr);
228  }
229  }
230 }
231 
233  const exprt &expr,
234  value_setst::valuest &dest)
235 {
236  value_sets.get_values(current_target, expr, dest);
237 }
238 
240  exprt &expr,
241  const bool checks_only,
243 {
244  guardt guard;
245 
246  if(checks_only)
247  {
248  exprt tmp(expr);
249  dereference_rec(tmp, guard, mode);
250  }
251  else
252  dereference_rec(expr, guard, mode);
253 }
254 
256  goto_programt &goto_program,
257  bool checks_only)
258 {
259  for(goto_programt::instructionst::iterator
260  it=goto_program.instructions.begin();
261  it!=goto_program.instructions.end();
262  it++)
263  {
264  new_code.clear();
265  assertions.clear();
266 
267  dereference_instruction(it, checks_only);
268 
269  // insert new instructions
270  while(!new_code.instructions.empty())
271  {
272  goto_program.insert_before_swap(it, new_code.instructions.front());
273  new_code.instructions.pop_front();
274  it++;
275  }
276  }
277 }
278 
280  goto_functionst &goto_functions,
281  bool checks_only)
282 {
283  for(goto_functionst::function_mapt::iterator
284  it=goto_functions.function_map.begin();
285  it!=goto_functions.function_map.end();
286  it++)
287  dereference_program(it->second.body, checks_only);
288 }
289 
291  goto_programt::targett target,
292  bool checks_only)
293 {
294  current_target=target;
295  #if 0
296  valid_local_variables=&target->local_variables;
297  #endif
298  goto_programt::instructiont &i=*target;
299 
301 
302  if(i.is_assign())
303  {
304  if(i.code.operands().size()!=2)
305  throw "assignment expects two operands";
306 
308  i.code.op0(), checks_only, value_set_dereferencet::modet::WRITE);
310  i.code.op1(), checks_only, value_set_dereferencet::modet::READ);
311  }
312  else if(i.is_function_call())
313  {
314  code_function_callt &function_call=to_code_function_call(to_code(i.code));
315 
316  if(function_call.lhs().is_not_nil())
318  function_call.lhs(),
319  checks_only,
321 
323  function_call.function(),
324  checks_only,
327  function_call.op2(), checks_only, value_set_dereferencet::modet::READ);
328  }
329  else if(i.is_return())
330  {
331  Forall_operands(it, i.code)
333  }
334  else if(i.is_other())
335  {
336  const irep_idt &statement=i.code.get(ID_statement);
337 
338  if(statement==ID_expression)
339  {
340  if(i.code.operands().size()!=1)
341  throw "expression expects one operand";
342 
344  i.code.op0(), checks_only, value_set_dereferencet::modet::READ);
345  }
346  else if(statement==ID_printf)
347  {
348  Forall_operands(it, i.code)
350  *it, checks_only, value_set_dereferencet::modet::READ);
351  }
352  }
353 }
354 
357  exprt &expr)
358 {
359  current_target=target;
360  #if 0
361  valid_local_variables=&target->local_variables;
362  #endif
363 
365 }
366 
368  goto_programt &goto_program)
369 {
370  dereference_program(goto_program, true);
371 }
372 
374  goto_functionst &goto_functions)
375 {
376  dereference_program(goto_functions, true);
377 }
378 
380  goto_programt &goto_program,
381  symbol_tablet &symbol_table,
382  value_setst &value_sets)
383 {
384  namespacet ns(symbol_table);
385 
386  optionst options;
387 
389  goto_program_dereference(ns, symbol_table, options, value_sets);
390 
391  goto_program_dereference.dereference_program(goto_program);
392 }
393 
395  goto_functionst &goto_functions,
396  symbol_tablet &symbol_table,
397  value_setst &value_sets)
398 {
399  namespacet ns(symbol_table);
400 
401  optionst options;
402 
404  goto_program_dereference(ns, symbol_table, options, value_sets);
405 
406  Forall_goto_functions(it, goto_functions)
407  goto_program_dereference.dereference_program(it->second.body);
408 }
409 
411  goto_programt &goto_program,
412  symbol_tablet &symbol_table,
413  const optionst &options,
414  value_setst &value_sets)
415 {
416  namespacet ns(symbol_table);
418  goto_program_dereference(ns, symbol_table, options, value_sets);
419  goto_program_dereference.pointer_checks(goto_program);
420 }
421 
423  goto_functionst &goto_functions,
424  symbol_tablet &symbol_table,
425  const optionst &options,
426  value_setst &value_sets)
427 {
428  namespacet ns(symbol_table);
430  goto_program_dereference(ns, symbol_table, options, value_sets);
431  goto_program_dereference.pointer_checks(goto_functions);
432 }
433 
436  exprt &expr,
437  const namespacet &ns,
438  value_setst &value_sets)
439 {
440  optionst options;
441  symbol_tablet new_symbol_table;
443  goto_program_dereference(ns, new_symbol_table, options, value_sets);
444  goto_program_dereference.dereference_expression(target, expr);
445 }
irep_idt name
The unique identifier.
Definition: symbol.h:46
exprt as_expr() const
Definition: guard.h:43
goto_program_instruction_typet
The type of an instruction in a GOTO program.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
targett add_instruction()
Adds an instruction at the end.
bool is_boolean() const
Definition: expr.cpp:231
bool is_not_nil() const
Definition: irep.h:104
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:84
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 clear()
Clear the goto program.
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)
instructionst instructions
The list of instructions in the goto program.
goto_programt::const_targett current_target
bool is_true() const
Definition: expr.cpp:133
Definition: guard.h:19
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
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:70
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:189
instructionst::const_iterator const_targett
void pointer_checks(goto_programt &goto_program, symbol_tablet &symbol_table, const optionst &options, value_setst &value_sets)
const std::set< irep_idt > * valid_local_variables
const source_locationt & find_source_location() const
Definition: expr.cpp:466
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
Guard Data Structure.
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)
Symbol table.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
typet type
Type of symbol.
Definition: symbol.h:37
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:100
value_set_dereferencet dereference
void dereference_program(goto_programt &goto_program, bool checks_only=false)
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)
#define Forall_goto_functions(it, functions)
static bool has_dereference(const exprt &expr)
Returns &#39;true&#39; iff the given expression contains unary &#39;*&#39;.
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const std::string & id_string() const
Definition: irep.h:192
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
exprt & op2()
Definition: expr.h:90
Options.
Base Type Computation.
operandst & operands()
Definition: expr.h:70
std::list< exprt > valuest
Definition: value_sets.h:28
bool empty() const
Definition: dstring.h:61
void add(const exprt &expr)
Definition: guard.cpp:64
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
bool simplify(exprt &expr, const namespacet &ns)