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("#invalid_object"))
29  return false;
30 
31  const symbolt &ptr_symbol = ns.lookup(to_symbol_expr(expr));
32 
33  const irep_idt &failed_symbol=
34  ptr_symbol.type.get("#failed_symbol");
35 
36  if(failed_symbol.empty())
37  return false;
38 
39  return !ns.lookup(failed_symbol, symbol);
40  }
41 
42  return false;
43 }
44 
46  const irep_idt &identifier)
47 {
48  const symbolt &symbol=ns.lookup(identifier);
49 
50  if(symbol.type.id()==ID_code)
51  return true;
52 
53  if(symbol.is_static_lifetime)
54  return true; // global/static
55 
56  #if 0
57  if(valid_local_variables->find(symbol.name)!=
58  valid_local_variables->end())
59  return true; // valid local
60  #else
61  return true;
62  #endif
63 
64  return false;
65 }
66 
68  const std::string &property,
69  const std::string &msg,
70  const guardt &guard)
71 {
72  exprt guard_expr=guard.as_expr();
73 
74  if(assertions.insert(guard_expr).second)
75  {
76  guard_expr.make_not();
77 
78  // first try simplifier on it
79  if(options.get_bool_option("simplify"))
80  simplify(guard_expr, ns);
81 
82  if(!guard_expr.is_true())
83  {
85  options.get_bool_option("assert-to-assume")?ASSUME:ASSERT;
86 
88  t->guard.swap(guard_expr);
89  t->source_location=dereference_location;
90  t->source_location.set_property_class(property);
91  t->source_location.set_comment("dereference failure: "+msg);
92  }
93  }
94 }
95 
97  exprt &expr,
98  guardt &guard,
100 {
101  if(!has_subexpr(expr, ID_dereference))
102  return;
103 
104  if(expr.id()==ID_and || expr.id()==ID_or)
105  {
106  if(!expr.is_boolean())
107  throw expr.id_string()+" must be Boolean, but got "+
108  expr.pretty();
109 
110  guardt old_guard=guard;
111 
112  for(auto &op : expr.operands())
113  {
114  if(!op.is_boolean())
115  throw expr.id_string()+" takes Boolean operands only, but got "+
116  op.pretty();
117 
118  if(has_subexpr(op, ID_dereference))
120 
121  if(expr.id()==ID_or)
122  {
123  exprt tmp(op);
124  tmp.make_not();
125  guard.add(tmp);
126  }
127  else
128  guard.add(op);
129  }
130 
131  guard.swap(old_guard);
132 
133  return;
134  }
135  else if(expr.id()==ID_if)
136  {
137  if(expr.operands().size()!=3)
138  throw "if takes three arguments";
139 
140  if(!expr.op0().is_boolean())
141  {
142  std::string msg=
143  "first argument of if must be boolean, but got "
144  +expr.op0().pretty();
145  throw msg;
146  }
147 
149 
150  bool o1 = has_subexpr(expr.op1(), ID_dereference);
151  bool o2 = has_subexpr(expr.op2(), ID_dereference);
152 
153  if(o1)
154  {
155  guardt old_guard=guard;
156  guard.add(expr.op0());
157  dereference_rec(expr.op1(), guard, mode);
158  guard.swap(old_guard);
159  }
160 
161  if(o2)
162  {
163  guardt old_guard=guard;
164  exprt tmp(expr.op0());
165  tmp.make_not();
166  guard.add(tmp);
167  dereference_rec(expr.op2(), guard, mode);
168  guard.swap(old_guard);
169  }
170 
171  return;
172  }
173 
174  if(expr.id()==ID_address_of ||
175  expr.id()=="reference_to")
176  {
177  // turn &*p to p
178  // this has *no* side effect!
179 
180  assert(expr.operands().size()==1);
181 
182  if(expr.op0().id()==ID_dereference)
183  {
184  assert(expr.op0().operands().size()==1);
185 
186  exprt tmp;
187  tmp.swap(expr.op0().op0());
188 
189  if(tmp.type()!=expr.type())
190  tmp.make_typecast(expr.type());
191 
192  expr.swap(tmp);
193  }
194  }
195 
196  Forall_operands(it, expr)
197  dereference_rec(*it, guard, mode);
198 
199  if(expr.id()==ID_dereference)
200  {
201  if(expr.operands().size()!=1)
202  throw "dereference expects one operand";
203 
205 
207  expr.op0(), guard, mode);
208 
209  expr.swap(tmp);
210  }
211  else if(expr.id()==ID_index)
212  {
213  // this is old stuff and will go away
214 
215  if(expr.operands().size()!=2)
216  throw "index expects two operands";
217 
218  if(expr.op0().type().id()==ID_pointer)
219  {
221 
222  exprt tmp1(ID_plus, expr.op0().type());
223  tmp1.operands().swap(expr.operands());
224 
225  exprt tmp2=dereference.dereference(tmp1, guard, mode);
226  tmp2.swap(expr);
227  }
228  }
229 }
230 
232  const exprt &expr,
233  value_setst::valuest &dest)
234 {
235  value_sets.get_values(current_target, expr, dest);
236 }
237 
239  exprt &expr,
240  const bool checks_only,
242 {
243  guardt guard;
244 
245  if(checks_only)
246  {
247  exprt tmp(expr);
248  dereference_rec(tmp, guard, mode);
249  }
250  else
251  dereference_rec(expr, guard, mode);
252 }
253 
256  bool checks_only)
257 {
258  for(goto_programt::instructionst::iterator
259  it=goto_program.instructions.begin();
260  it!=goto_program.instructions.end();
261  it++)
262  {
263  new_code.clear();
264  assertions.clear();
265 
266  dereference_instruction(it, checks_only);
267 
268  // insert new instructions
269  while(!new_code.instructions.empty())
270  {
272  new_code.instructions.pop_front();
273  it++;
274  }
275  }
276 }
277 
279  goto_functionst &goto_functions,
280  bool checks_only)
281 {
282  for(goto_functionst::function_mapt::iterator
283  it=goto_functions.function_map.begin();
284  it!=goto_functions.function_map.end();
285  it++)
286  dereference_program(it->second.body, checks_only);
287 }
288 
290  goto_programt::targett target,
291  bool checks_only)
292 {
293  current_target=target;
294  #if 0
295  valid_local_variables=&target->local_variables;
296  #endif
297  goto_programt::instructiont &i=*target;
298 
300 
301  if(i.is_assign())
302  {
303  if(i.code.operands().size()!=2)
304  throw "assignment expects two operands";
305 
307  i.code.op0(), checks_only, value_set_dereferencet::modet::WRITE);
309  i.code.op1(), checks_only, value_set_dereferencet::modet::READ);
310  }
311  else if(i.is_function_call())
312  {
314 
315  if(function_call.lhs().is_not_nil())
317  function_call.lhs(),
318  checks_only,
320 
322  function_call.function(),
323  checks_only,
326  function_call.op2(), checks_only, value_set_dereferencet::modet::READ);
327  }
328  else if(i.is_return())
329  {
330  Forall_operands(it, i.code)
332  }
333  else if(i.is_other())
334  {
335  const irep_idt &statement=i.code.get(ID_statement);
336 
337  if(statement==ID_expression)
338  {
339  if(i.code.operands().size()!=1)
340  throw "expression expects one operand";
341 
343  i.code.op0(), checks_only, value_set_dereferencet::modet::READ);
344  }
345  else if(statement==ID_printf)
346  {
347  Forall_operands(it, i.code)
349  *it, checks_only, value_set_dereferencet::modet::READ);
350  }
351  }
352 }
353 
356  exprt &expr)
357 {
358  current_target=target;
359  #if 0
360  valid_local_variables=&target->local_variables;
361  #endif
362 
364 }
365 
368 {
370 }
371 
373  goto_functionst &goto_functions)
374 {
375  dereference_program(goto_functions, true);
376 }
377 
380  symbol_tablet &symbol_table,
381  value_setst &value_sets)
382 {
383  namespacet ns(symbol_table);
384 
385  optionst options;
386 
388  goto_program_dereference(ns, symbol_table, options, value_sets);
389 
390  goto_program_dereference.dereference_program(goto_program);
391 }
392 
394  goto_modelt &goto_model,
395  value_setst &value_sets)
396 {
397  namespacet ns(goto_model.symbol_table);
398 
399  optionst options;
400 
402  goto_program_dereference(
403  ns, goto_model.symbol_table, options, value_sets);
404 
405  Forall_goto_functions(it, goto_model.goto_functions)
406  goto_program_dereference.dereference_program(it->second.body);
407 }
408 
411  symbol_tablet &symbol_table,
412  const optionst &options,
413  value_setst &value_sets)
414 {
415  namespacet ns(symbol_table);
417  goto_program_dereference(ns, symbol_table, options, value_sets);
418  goto_program_dereference.pointer_checks(goto_program);
419 }
420 
422  goto_functionst &goto_functions,
423  symbol_tablet &symbol_table,
424  const optionst &options,
425  value_setst &value_sets)
426 {
427  namespacet ns(symbol_table);
429  goto_program_dereference(ns, symbol_table, options, value_sets);
430  goto_program_dereference.pointer_checks(goto_functions);
431 }
432 
435  exprt &expr,
436  const namespacet &ns,
437  value_setst &value_sets)
438 {
439  optionst options;
440  symbol_tablet new_symbol_table;
442  goto_program_dereference(ns, new_symbol_table, options, value_sets);
443  goto_program_dereference.dereference_expression(target, expr);
444 }
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:103
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:189
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:125
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:828
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)
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:848
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:192
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
goto_programt & goto_program
Definition: cover.cpp:63
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
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:61
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:130
void add(const exprt &expr)
Definition: guard.cpp:64
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
bool simplify(exprt &expr, const namespacet &ns)