CBMC
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/std_code.h>
18 #include <util/symbol_table.h>
19 
21 
24 const symbolt *
26 {
27  if(expr.id()==ID_symbol)
28  {
29  if(expr.get_bool(ID_C_invalid_object))
30  return nullptr;
31 
32  const symbolt &ptr_symbol = ns.lookup(to_symbol_expr(expr));
33 
34  const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
35 
36  if(failed_symbol.empty())
37  return nullptr;
38 
39  const symbolt *symbol = nullptr;
40  ns.lookup(failed_symbol, symbol);
41  return symbol;
42  }
43 
44  return nullptr;
45 }
46 
51 {
52  if(!has_subexpr(expr, ID_dereference))
53  return;
54 
55  if(expr.id()==ID_and || expr.id()==ID_or)
56  {
57  if(!expr.is_boolean())
58  throw expr.id_string()+" must be Boolean, but got "+
59  expr.pretty();
60 
61  for(auto &op : expr.operands())
62  {
63  if(!op.is_boolean())
64  throw expr.id_string()+" takes Boolean operands only, but got "+
65  op.pretty();
66 
67  if(has_subexpr(op, ID_dereference))
68  dereference_rec(op);
69  }
70  return;
71  }
72  else if(expr.id()==ID_if)
73  {
74  auto &if_expr = to_if_expr(expr);
75 
76  if(!if_expr.cond().is_boolean())
77  {
78  std::string msg = "first argument of if must be boolean, but got " +
79  if_expr.cond().pretty();
80  throw msg;
81  }
82 
83  dereference_rec(if_expr.cond());
84 
85  bool o1 = has_subexpr(if_expr.true_case(), ID_dereference);
86  bool o2 = has_subexpr(if_expr.false_case(), ID_dereference);
87 
88  if(o1)
89  dereference_rec(if_expr.true_case());
90 
91  if(o2)
92  dereference_rec(if_expr.false_case());
93 
94  return;
95  }
96 
97  if(expr.id() == ID_address_of)
98  {
99  // turn &*p to p
100  // this has *no* side effect!
101 
102  if(to_address_of_expr(expr).object().id() == ID_dereference)
104  to_dereference_expr(to_address_of_expr(expr).object()).pointer(),
105  expr.type());
106  }
107 
108  Forall_operands(it, expr)
109  dereference_rec(*it);
110 
111  if(expr.id()==ID_dereference)
112  {
113  expr = dereference.dereference(to_dereference_expr(expr).pointer());
114  }
115  else if(expr.id()==ID_index)
116  {
117  // this is old stuff and will go away
118 
119  if(to_index_expr(expr).array().type().id() == ID_pointer)
120  {
121  exprt tmp1(ID_plus, to_index_expr(expr).array().type());
122  tmp1.operands().swap(expr.operands());
123 
124  exprt tmp2 = dereference.dereference(tmp1);
125  tmp2.swap(expr);
126  }
127  }
128 }
129 
134 std::vector<exprt>
136 {
138 }
139 
146  exprt &expr,
147  const bool checks_only)
148 {
149  if(checks_only)
150  {
151  exprt tmp(expr);
152  dereference_rec(tmp);
153  }
154  else
155  dereference_rec(expr);
156 }
157 
159  goto_programt &goto_program,
160  bool checks_only)
161 {
162  for(goto_programt::instructionst::iterator
163  it=goto_program.instructions.begin();
164  it!=goto_program.instructions.end();
165  it++)
166  {
167  new_code.clear();
168  dereference_instruction(it, checks_only);
169 
170  // insert new instructions
171  while(!new_code.instructions.empty())
172  {
173  goto_program.insert_before_swap(it, new_code.instructions.front());
174  new_code.instructions.pop_front();
175  it++;
176  }
177  }
178 }
179 
181  goto_functionst &goto_functions,
182  bool checks_only)
183 {
184  for(goto_functionst::function_mapt::iterator
185  it=goto_functions.function_map.begin();
186  it!=goto_functions.function_map.end();
187  it++)
188  dereference_program(it->second.body, checks_only);
189 }
190 
196  goto_programt::targett target,
197  bool checks_only)
198 {
199  current_target=target;
200  goto_programt::instructiont &i=*target;
201 
202  if(i.has_condition())
203  dereference_expr(i.condition_nonconst(), checks_only);
204 
205  if(i.is_assign())
206  {
207  dereference_expr(i.assign_lhs_nonconst(), checks_only);
208  dereference_expr(i.assign_rhs_nonconst(), checks_only);
209  }
210  else if(i.is_function_call())
211  {
212  if(as_const(i).call_lhs().is_not_nil())
213  dereference_expr(i.call_lhs(), checks_only);
214 
215  dereference_expr(i.call_function(), checks_only);
216 
217  for(auto &arg : i.call_arguments())
218  dereference_expr(arg, checks_only);
219  }
220  else if(i.is_set_return_value())
221  {
222  dereference_expr(i.return_value(), checks_only);
223  }
224  else if(i.is_other())
225  {
226  auto code = i.get_other();
227  const irep_idt &statement = code.get_statement();
228 
229  if(statement==ID_expression)
230  {
231  if(code.operands().size() != 1)
232  throw "expression expects one operand";
233 
234  dereference_expr(to_code_expression(code).expression(), checks_only);
235  }
236  else if(statement==ID_printf)
237  {
238  for(auto &op : code.operands())
239  dereference_expr(op, checks_only);
240  }
241 
242  i.set_other(code);
243  }
244 }
245 
248  const irep_idt &function_id,
250  exprt &expr)
251 {
252  current_function = function_id;
253  current_target=target;
254  dereference_expr(expr, false);
255 }
256 
261  goto_modelt &goto_model,
262  value_setst &value_sets,
263  message_handlert &message_handler)
264 {
265  namespacet ns(goto_model.symbol_table);
266 
267  optionst options;
268 
269  goto_program_dereferencet goto_program_dereference(
270  ns, goto_model.symbol_table, options, value_sets, message_handler);
271 
272  for(auto &gf_entry : goto_model.goto_functions.function_map)
273  goto_program_dereference.dereference_program(gf_entry.second.body);
274 }
275 
279  const irep_idt &function_id,
281  exprt &expr,
282  const namespacet &ns,
283  value_setst &value_sets,
284  message_handlert &message_handler)
285 {
286  optionst options;
287  symbol_tablet new_symbol_table;
288  goto_program_dereferencet goto_program_dereference(
289  ns, new_symbol_table, options, value_sets, message_handler);
290  goto_program_dereference.dereference_expression(function_id, target, expr);
291 }
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Base class for all expressions.
Definition: expr.h:56
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.h:224
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
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:181
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:286
bool is_set_return_value() const
Definition: goto_program.h:492
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:272
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:360
exprt & assign_rhs_nonconst()
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:221
exprt & condition_nonconst()
Get the condition of gotos, assume, assert.
Definition: goto_program.h:373
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:258
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:314
void set_other(goto_instruction_codet &c)
Set the statement for OTHER.
Definition: goto_program.h:321
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:300
exprt & assign_lhs_nonconst()
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:207
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
void clear()
Clear the goto program.
Definition: goto_program.h:820
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:643
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
const std::string & id_string() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:388
void swap(irept &irep)
Definition: irep.h:434
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
The symbol table.
Definition: symbol_table.h:14
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:2081
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:27
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:115
Deprecated expression utility functions.
Symbol Table + CFG.
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets, message_handlert &message_handler)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
void remove_pointers(goto_modelt &goto_model, value_setst &value_sets, message_handlert &message_handler)
Remove dereferences in all expressions contained in the program goto_model.
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:890
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1428
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2455
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1538
Author: Diffblue Ltd.