cprover
Loading...
Searching...
No Matches
goto_program_dereference.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dereferencing Operations on GOTO Programs
4
5Author: 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
24const symbolt *
26{
27 if(expr.id()==ID_symbol)
28 {
30 return nullptr;
31
33
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
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
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
125 tmp2.swap(expr);
126 }
127 }
128}
129
134std::vector<exprt>
139
146 exprt &expr,
147 const bool checks_only)
148{
149 if(checks_only)
150 {
151 exprt tmp(expr);
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();
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
197 bool checks_only)
198{
199 current_target=target;
201
202 if(i.has_condition())
203 {
204 exprt c = i.get_condition();
206 i.set_condition(c);
207 }
208
209 if(i.is_assign())
210 {
211 dereference_expr(i.assign_lhs_nonconst(), checks_only);
212 dereference_expr(i.assign_rhs_nonconst(), checks_only);
213 }
214 else if(i.is_function_call())
215 {
216 if(as_const(i).call_lhs().is_not_nil())
217 dereference_expr(i.call_lhs(), checks_only);
218
219 dereference_expr(i.call_function(), checks_only);
220
221 for(auto &arg : i.call_arguments())
223 }
224 else if(i.is_set_return_value())
225 {
226 dereference_expr(i.return_value(), checks_only);
227 }
228 else if(i.is_other())
229 {
230 auto code = i.get_other();
231 const irep_idt &statement = code.get_statement();
232
233 if(statement==ID_expression)
234 {
235 if(code.operands().size() != 1)
236 throw "expression expects one operand";
237
239 }
240 else if(statement==ID_printf)
241 {
242 for(auto &op : code.operands())
244 }
245
246 i.set_other(code);
247 }
248}
249
252 const irep_idt &function_id,
254 exprt &expr)
255{
256 current_function = function_id;
257 current_target=target;
258 dereference_expr(expr, false);
259}
260
265 goto_modelt &goto_model,
266 value_setst &value_sets)
267{
268 namespacet ns(goto_model.symbol_table);
269
270 optionst options;
271
274 ns, goto_model.symbol_table, options, value_sets);
275
276 for(auto &gf_entry : goto_model.goto_functions.function_map)
277 goto_program_dereference.dereference_program(gf_entry.second.body);
278}
279
283 const irep_idt &function_id,
285 exprt &expr,
286 const namespacet &ns,
287 value_setst &value_sets)
288{
289 optionst options;
290 symbol_tablet new_symbol_table;
292 goto_program_dereference(ns, new_symbol_table, options, value_sets);
293 goto_program_dereference.dereference_expression(function_id, target, expr);
294}
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.cpp:51
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
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.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void clear()
Clear the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
instructionst::const_iterator const_targett
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:495
const std::string & id_string() const
Definition irep.h:399
const irep_idt & id() const
Definition irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The symbol table.
Symbol table entry.
Definition symbol.h:28
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
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
Deprecated expression utility functions.
Symbol Table + CFG.
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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
code_expressiont & to_code_expression(codet &code)
Definition std_code.h:1428
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
Author: Diffblue Ltd.