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