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/options.h>
16 #include <util/pointer_expr.h>
17 #include <util/simplify_expr.h>
18 #include <util/std_code.h>
19 #include <util/symbol_table.h>
20 
23 const symbolt *
25 {
26  if(expr.id()==ID_symbol)
27  {
28  if(expr.get_bool(ID_C_invalid_object))
29  return nullptr;
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 nullptr;
37 
38  const symbolt *symbol = nullptr;
39  ns.lookup(failed_symbol, symbol);
40  return symbol;
41  }
42 
43  return nullptr;
44 }
45 
50 {
51  if(!has_subexpr(expr, ID_dereference))
52  return;
53 
54  if(expr.id()==ID_and || expr.id()==ID_or)
55  {
56  if(!expr.is_boolean())
57  throw expr.id_string()+" must be Boolean, but got "+
58  expr.pretty();
59 
60  for(auto &op : expr.operands())
61  {
62  if(!op.is_boolean())
63  throw expr.id_string()+" takes Boolean operands only, but got "+
64  op.pretty();
65 
66  if(has_subexpr(op, ID_dereference))
67  dereference_rec(op);
68  }
69  return;
70  }
71  else if(expr.id()==ID_if)
72  {
73  auto &if_expr = to_if_expr(expr);
74 
75  if(!if_expr.cond().is_boolean())
76  {
77  std::string msg = "first argument of if must be boolean, but got " +
78  if_expr.cond().pretty();
79  throw msg;
80  }
81 
82  dereference_rec(if_expr.cond());
83 
84  bool o1 = has_subexpr(if_expr.true_case(), ID_dereference);
85  bool o2 = has_subexpr(if_expr.false_case(), ID_dereference);
86 
87  if(o1)
88  dereference_rec(if_expr.true_case());
89 
90  if(o2)
91  dereference_rec(if_expr.false_case());
92 
93  return;
94  }
95 
96  if(expr.id() == ID_address_of)
97  {
98  // turn &*p to p
99  // this has *no* side effect!
100 
101  if(to_address_of_expr(expr).object().id() == ID_dereference)
103  to_dereference_expr(to_address_of_expr(expr).object()).pointer(),
104  expr.type());
105  }
106 
107  Forall_operands(it, expr)
108  dereference_rec(*it);
109 
110  if(expr.id()==ID_dereference)
111  {
112  expr = dereference.dereference(to_dereference_expr(expr).pointer());
113  }
114  else if(expr.id()==ID_index)
115  {
116  // this is old stuff and will go away
117 
118  if(to_index_expr(expr).array().type().id() == ID_pointer)
119  {
120  exprt tmp1(ID_plus, to_index_expr(expr).array().type());
121  tmp1.operands().swap(expr.operands());
122 
123  exprt tmp2 = dereference.dereference(tmp1);
124  tmp2.swap(expr);
125  }
126  }
127 }
128 
133 std::vector<exprt>
135 {
137 }
138 
145  exprt &expr,
146  const bool checks_only)
147 {
148  if(checks_only)
149  {
150  exprt tmp(expr);
151  dereference_rec(tmp);
152  }
153  else
154  dereference_rec(expr);
155 }
156 
158  goto_programt &goto_program,
159  bool checks_only)
160 {
161  for(goto_programt::instructionst::iterator
162  it=goto_program.instructions.begin();
163  it!=goto_program.instructions.end();
164  it++)
165  {
166  new_code.clear();
167  dereference_instruction(it, checks_only);
168 
169  // insert new instructions
170  while(!new_code.instructions.empty())
171  {
172  goto_program.insert_before_swap(it, new_code.instructions.front());
173  new_code.instructions.pop_front();
174  it++;
175  }
176  }
177 }
178 
180  goto_functionst &goto_functions,
181  bool checks_only)
182 {
183  for(goto_functionst::function_mapt::iterator
184  it=goto_functions.function_map.begin();
185  it!=goto_functions.function_map.end();
186  it++)
187  dereference_program(it->second.body, checks_only);
188 }
189 
195  goto_programt::targett target,
196  bool checks_only)
197 {
198  current_target=target;
199  goto_programt::instructiont &i=*target;
200 
201  if(i.has_condition())
202  {
203  exprt c = i.get_condition();
204  dereference_expr(c, checks_only);
205  i.set_condition(c);
206  }
207 
208  if(i.is_assign())
209  {
210  auto assignment = i.get_assign();
211  dereference_expr(assignment.lhs(), checks_only);
212  dereference_expr(assignment.rhs(), checks_only);
213  i.set_assign(assignment);
214  }
215  else if(i.is_function_call())
216  {
217  code_function_callt function_call = i.get_function_call();
218 
219  if(function_call.lhs().is_not_nil())
220  dereference_expr(function_call.lhs(), checks_only);
221 
222  dereference_expr(function_call.function(), checks_only);
223 
224  for(auto &arg : function_call.arguments())
225  dereference_expr(arg, checks_only);
226 
227  i.set_function_call(function_call);
228  }
229  else if(i.is_return())
230  {
231  dereference_expr(i.return_value(), checks_only);
232  }
233  else if(i.is_other())
234  {
235  auto code = i.get_other();
236  const irep_idt &statement = code.get_statement();
237 
238  if(statement==ID_expression)
239  {
240  if(code.operands().size() != 1)
241  throw "expression expects one operand";
242 
243  dereference_expr(to_code_expression(code).expression(), checks_only);
244  }
245  else if(statement==ID_printf)
246  {
247  for(auto &op : code.operands())
248  dereference_expr(op, checks_only);
249  }
250 
251  i.set_other(code);
252  }
253 }
254 
257  const irep_idt &function_id,
259  exprt &expr)
260 {
261  current_function = function_id;
262  current_target=target;
263  dereference_expr(expr, false);
264 }
265 
270  goto_modelt &goto_model,
271  value_setst &value_sets)
272 {
273  namespacet ns(goto_model.symbol_table);
274 
275  optionst options;
276 
278  goto_program_dereference(
279  ns, goto_model.symbol_table, options, value_sets);
280 
281  for(auto &gf_entry : goto_model.goto_functions.function_map)
282  goto_program_dereference.dereference_program(gf_entry.second.body);
283 }
284 
288  const irep_idt &function_id,
290  exprt &expr,
291  const namespacet &ns,
292  value_setst &value_sets)
293 {
294  optionst options;
295  symbol_tablet new_symbol_table;
297  goto_program_dereference(ns, new_symbol_table, options, value_sets);
298  goto_program_dereference.dereference_expression(function_id, target, expr);
299 }
codet representation of a function call statement.
Definition: std_code.h:1215
exprt & function()
Definition: std_code.h:1250
argumentst & arguments()
Definition: std_code.h:1260
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:65
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
Wrapper for functions removing dereferences in expressions contained in a goto program.
void dereference_program(goto_programt &goto_program, bool checks_only=false)
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
void dereference_expr(exprt &expr, const bool checks_only)
Remove dereference expressions contained in expr.
value_set_dereferencet dereference
std::vector< exprt > get_value_set(const exprt &expr) const override
Gets the value set corresponding to the current target and expression expr.
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
Remove dereference from expressions contained in the instruction at target.
void dereference_rec(exprt &expr)
Turn subexpression of expr of the form &*p into p and use dereference on subexpressions of the form *...
goto_programt::const_targett current_target
void dereference_expression(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr)
Set the current target to target and remove derefence from expr.
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
void set_function_call(code_function_callt c)
Set the function call for FUNCTION_CALL.
Definition: goto_program.h:313
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:320
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:344
const exprt & return_value() const
Get the return value of a RETURN instruction.
Definition: goto_program.h:284
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
Definition: goto_program.h:306
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:350
void set_assign(code_assignt c)
Set the assignment for ASSIGN.
Definition: goto_program.h:193
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:357
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:186
void set_other(codet &c)
Set the statement for OTHER.
Definition: goto_program.h:327
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
void clear()
Clear the goto program.
Definition: goto_program.h:754
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:577
instructionst::iterator targett
Definition: goto_program.h:550
instructionst::const_iterator const_targett
Definition: goto_program.h:551
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:492
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
const std::string & id_string() const
Definition: irep.h:410
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:452
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
The symbol table.
Definition: symbol_table.h:20
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
exprt dereference(const exprt &pointer, bool display_points_to_sets=false)
Dereference the given pointer-expression.
virtual std::vector< exprt > get_values(const irep_idt &function_id, goto_programt::const_targett l, const exprt &expr)=0
#define Forall_operands(it, expr)
Definition: expr.h:25
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:140
Deprecated expression utility functions.
void remove_pointers(goto_modelt &goto_model, value_setst &value_sets)
Remove dereferences in all expressions contained in the program goto_model.
void dereference(const irep_idt &function_id, 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...
Options.
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1876
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
Author: Diffblue Ltd.