cprover
Loading...
Searching...
No Matches
local_bitvector_analysis.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-insensitive, location-sensitive may-alias analysis
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include <algorithm>
15
16#include <util/pointer_expr.h>
17#include <util/std_code.h>
18#include <util/symbol_table.h>
19
20void local_bitvector_analysist::flagst::print(std::ostream &out) const
21{
22 if(is_unknown())
23 out << "+unknown";
25 out << "+uninitialized";
26 if(is_uses_offset())
27 out << "+uses_offset";
29 out << "+dynamic_local";
30 if(is_dynamic_heap())
31 out << "+dynamic_heap";
32 if(is_null())
33 out << "+null";
35 out << "+static_lifetime";
37 out << "+integer_address";
38}
39
41{
42 bool result=false;
43
44 std::size_t max_index=
45 std::max(a.size(), b.size());
46
47 for(std::size_t i=0; i<max_index; i++)
48 result |= a[i].merge(b[i]);
49
50 return result;
51}
52
55{
56 localst::locals_sett::const_iterator it = locals.locals.find(identifier);
57 return it != locals.locals.end() && ns.lookup(*it).type.id() == ID_pointer &&
58 !dirty(identifier);
59}
60
62 const exprt &lhs,
63 const exprt &rhs,
66{
67 if(lhs.id()==ID_symbol)
68 {
69 const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
70
71 if(is_tracked(identifier))
72 {
73 const auto dest_pointer = pointers.number(identifier);
76 }
77 }
78 else if(lhs.id()==ID_dereference)
79 {
80 }
81 else if(lhs.id()==ID_index)
82 {
84 }
85 else if(lhs.id()==ID_member)
86 {
88 to_member_expr(lhs).struct_op(), rhs, loc_info_src, loc_info_dest);
89 }
90 else if(lhs.id()==ID_typecast)
91 {
93 }
94 else if(lhs.id()==ID_if)
95 {
96 assign_lhs(to_if_expr(lhs).true_case(), rhs, loc_info_src, loc_info_dest);
97 assign_lhs(to_if_expr(lhs).false_case(), rhs, loc_info_src, loc_info_dest);
98 }
99}
100
103 const exprt &rhs)
104{
105 local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
106
107 assert(loc_it!=cfg.loc_map.end());
108
109 return get_rec(rhs, loc_infos[loc_it->second]);
110}
111
113 const exprt &rhs,
115{
116 if(rhs.id()==ID_constant)
117 {
118 if(rhs.is_zero())
119 return flagst::mk_null();
120 else
122 }
123 else if(rhs.id()==ID_symbol)
124 {
125 const irep_idt &identifier=to_symbol_expr(rhs).get_identifier();
126 if(is_tracked(identifier))
127 {
128 const auto src_pointer = pointers.number(identifier);
130 }
131 else
132 return flagst::mk_unknown();
133 }
134 else if(rhs.id()==ID_address_of)
135 {
136 const exprt &object=to_address_of_expr(rhs).object();
137
138 if(object.id()==ID_symbol)
139 {
142 else
144 }
145 else if(object.id()==ID_index)
146 {
147 const index_exprt &index_expr=to_index_expr(object);
148 if(index_expr.array().id()==ID_symbol)
149 {
150 if(locals.is_local(
153 else
155 }
156 else
157 return flagst::mk_unknown();
158 }
159 else
160 return flagst::mk_unknown();
161 }
162 else if(rhs.id()==ID_typecast)
163 {
164 return get_rec(to_typecast_expr(rhs).op(), loc_info_src);
165 }
166 else if(rhs.id()==ID_uninitialized)
167 {
169 }
170 else if(rhs.id()==ID_plus)
171 {
172 const auto &plus_expr = to_plus_expr(rhs);
173
174 if(plus_expr.operands().size() >= 3)
175 {
177 plus_expr.op0().type().id() == ID_pointer,
178 "pointer in pointer-typed sum must be op0");
180 }
181 else if(plus_expr.operands().size() == 2)
182 {
183 // one must be pointer, one an integer
184 if(plus_expr.op0().type().id() == ID_pointer)
185 {
186 return get_rec(plus_expr.op0(), loc_info_src) |
188 }
189 else if(plus_expr.op1().type().id() == ID_pointer)
190 {
191 return get_rec(plus_expr.op1(), loc_info_src) |
193 }
194 else
195 return flagst::mk_unknown();
196 }
197 else
198 return flagst::mk_unknown();
199 }
200 else if(rhs.id()==ID_minus)
201 {
202 const auto &op0 = to_minus_expr(rhs).op0();
203
204 if(op0.type().id() == ID_pointer)
205 {
207 }
208 else
209 return flagst::mk_unknown();
210 }
211 else if(rhs.id()==ID_member)
212 {
213 return flagst::mk_unknown();
214 }
215 else if(rhs.id()==ID_index)
216 {
217 return flagst::mk_unknown();
218 }
219 else if(rhs.id()==ID_dereference)
220 {
221 return flagst::mk_unknown();
222 }
223 else if(rhs.id()==ID_side_effect)
224 {
226 const irep_idt &statement=side_effect_expr.get_statement();
227
228 if(statement==ID_allocate)
230 else
231 return flagst::mk_unknown();
232 }
233 else
234 return flagst::mk_unknown();
235}
236
238{
239 if(cfg.nodes.empty())
240 return;
241
242 std::set<local_cfgt::node_nrt> work_queue;
243 work_queue.insert(0);
244
245 loc_infos.resize(cfg.nodes.size());
246
247 // Gather the objects we track, and
248 // feed in sufficiently bad defaults for their value
249 // in the entry location.
250 for(const auto &local : locals.locals)
251 {
252 if(is_tracked(local))
254 }
255
256 while(!work_queue.empty())
257 {
258 const auto loc_nr = *work_queue.begin();
259 const local_cfgt::nodet &node=cfg.nodes[loc_nr];
260 const goto_programt::instructiont &instruction=*node.t;
261 work_queue.erase(work_queue.begin());
262
265
266 switch(instruction.type())
267 {
268 case ASSIGN:
270 instruction.assign_lhs(),
271 instruction.assign_rhs(),
274 break;
275
276 case DECL:
278 instruction.decl_symbol(),
282 break;
283
284 case DEAD:
286 instruction.dead_symbol(),
290 break;
291
292 case FUNCTION_CALL:
293 {
294 const auto &lhs = instruction.call_lhs();
295 if(lhs.is_not_nil())
297 break;
298 }
299
300 case CATCH:
301 case THROW:
302#if 0
303 DATA_INVARIANT(false, "Exceptions must be removed before analysis");
304 break;
305#endif
306 case SET_RETURN_VALUE:
307#if 0
308 DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
309 break;
310#endif
311 case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
312 case ATOMIC_END: // Ignoring is a valid over-approximation
313 case LOCATION: // No action required
314 case START_THREAD: // Require a concurrent analysis at higher level
315 case END_THREAD: // Require a concurrent analysis at higher level
316 case SKIP: // No action required
317 case ASSERT: // No action required
318 case ASSUME: // Ignoring is a valid over-approximation
319 case GOTO: // Ignoring the guard is a valid over-approximation
320 case END_FUNCTION: // No action required
321 break;
322 case OTHER:
323#if 0
325 false, "Unclear what is a safe over-approximation of OTHER");
326#endif
327 break;
328 case INCOMPLETE_GOTO:
330 DATA_INVARIANT(false, "Only complete instructions can be analyzed");
331 break;
332 }
333
334 for(const auto &succ : node.successors)
335 {
336 assert(succ<loc_infos.size());
337 if(merge(loc_infos[succ], (loc_info_dest)))
338 work_queue.insert(succ);
339 }
340 }
341}
342
344 std::ostream &out,
345 const goto_functiont &goto_function,
346 const namespacet &ns) const
347{
348 std::size_t l = 0;
349
350 for(const auto &instruction : goto_function.body.instructions)
351 {
352 out << "**** " << instruction.source_location() << "\n";
353
354 const auto &loc_info=loc_infos[l];
355
357 p_it=loc_info.begin();
358 p_it!=loc_info.end();
359 p_it++)
360 {
361 out << " " << pointers[p_it-loc_info.begin()]
362 << ": "
363 << *p_it
364 << "\n";
365 }
366
367 out << "\n";
368 goto_function.body.output_instruction(ns, irep_idt(), out, instruction);
369 out << "\n";
370
371 l++;
372 }
373}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
exprt & op0()
Definition expr.h:99
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
data_typet::const_iterator const_iterator
Base class for all expressions.
Definition expr.h:54
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:64
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
goto_program_instruction_typet type() const
What kind of instruction?
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Array index operator.
Definition std_expr.h:1328
const irep_idt & id() const
Definition irep.h:396
static bool merge(points_tot &a, points_tot &b)
flagst get(const goto_programt::const_targett t, const exprt &src)
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
flagst get_rec(const exprt &rhs, points_tot &loc_info_src)
void assign_lhs(const exprt &lhs, const exprt &rhs, points_tot &loc_info_src, points_tot &loc_info_dest)
bool is_tracked(const irep_idt &identifier)
goto_programt::const_targett t
Definition local_cfg.h:28
successorst successors
Definition local_cfg.h:29
nodest nodes
Definition local_cfg.h:36
loc_mapt loc_map
Definition local_cfg.h:33
bool is_local(const irep_idt &identifier) const
Definition locals.h:37
locals_sett locals
Definition locals.h:43
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 NIL expression.
Definition std_expr.h:2874
number_type number(const key_type &a)
Definition numbering.h:37
An expression containing a side effect.
Definition std_code.h:1450
const irep_idt & get_identifier() const
Definition std_expr.h:109
@ FUNCTION_CALL
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
dstringt irep_idt
Definition irep.h:37
Field-insensitive, location-sensitive bitvector analysis.
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.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:953
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:998
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
Author: Diffblue Ltd.