cprover
local_bitvector_analysis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-insensitive, location-sensitive may-alias analysis
4 
5 Author: 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 
20 void local_bitvector_analysist::flagst::print(std::ostream &out) const
21 {
22  if(is_unknown())
23  out << "+unknown";
24  if(is_uninitialized())
25  out << "+uninitialized";
26  if(is_uses_offset())
27  out << "+uses_offset";
28  if(is_dynamic_local())
29  out << "+dynamic_local";
30  if(is_dynamic_heap())
31  out << "+dynamic_heap";
32  if(is_null())
33  out << "+null";
34  if(is_static_lifetime())
35  out << "+static_lifetime";
36  if(is_integer_address())
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  {
49  if(a[i].merge(b[i]))
50  result=true;
51  }
52 
53  return result;
54 }
55 
58 {
59  localst::locals_sett::const_iterator it = locals.locals.find(identifier);
60  return it != locals.locals.end() && ns.lookup(*it).type.id() == ID_pointer &&
61  !dirty(identifier);
62 }
63 
65  const exprt &lhs,
66  const exprt &rhs,
67  points_tot &loc_info_src,
68  points_tot &loc_info_dest)
69 {
70  if(lhs.id()==ID_symbol)
71  {
72  const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
73 
74  if(is_tracked(identifier))
75  {
76  unsigned dest_pointer=pointers.number(identifier);
77  flagst rhs_flags=get_rec(rhs, loc_info_src);
78  loc_info_dest[dest_pointer]=rhs_flags;
79  }
80  }
81  else if(lhs.id()==ID_dereference)
82  {
83  }
84  else if(lhs.id()==ID_index)
85  {
86  assign_lhs(to_index_expr(lhs).array(), rhs, loc_info_src, loc_info_dest);
87  }
88  else if(lhs.id()==ID_member)
89  {
90  assign_lhs(
91  to_member_expr(lhs).struct_op(), rhs, loc_info_src, loc_info_dest);
92  }
93  else if(lhs.id()==ID_typecast)
94  {
95  assign_lhs(to_typecast_expr(lhs).op(), rhs, loc_info_src, loc_info_dest);
96  }
97  else if(lhs.id()==ID_if)
98  {
99  assign_lhs(to_if_expr(lhs).true_case(), rhs, loc_info_src, loc_info_dest);
100  assign_lhs(to_if_expr(lhs).false_case(), rhs, loc_info_src, loc_info_dest);
101  }
102 }
103 
106  const exprt &rhs)
107 {
108  local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
109 
110  assert(loc_it!=cfg.loc_map.end());
111 
112  return get_rec(rhs, loc_infos[loc_it->second]);
113 }
114 
116  const exprt &rhs,
117  points_tot &loc_info_src)
118 {
119  if(rhs.id()==ID_constant)
120  {
121  if(rhs.is_zero())
122  return flagst::mk_null();
123  else
125  }
126  else if(rhs.id()==ID_symbol)
127  {
128  const irep_idt &identifier=to_symbol_expr(rhs).get_identifier();
129  if(is_tracked(identifier))
130  {
131  unsigned src_pointer=pointers.number(identifier);
132  return loc_info_src[src_pointer];
133  }
134  else
135  return flagst::mk_unknown();
136  }
137  else if(rhs.id()==ID_address_of)
138  {
139  const exprt &object=to_address_of_expr(rhs).object();
140 
141  if(object.id()==ID_symbol)
142  {
143  if(locals.is_local(to_symbol_expr(object).get_identifier()))
144  return flagst::mk_dynamic_local();
145  else
147  }
148  else if(object.id()==ID_index)
149  {
150  const index_exprt &index_expr=to_index_expr(object);
151  if(index_expr.array().id()==ID_symbol)
152  {
153  if(locals.is_local(
154  to_symbol_expr(index_expr.array()).get_identifier()))
156  else
158  }
159  else
160  return flagst::mk_unknown();
161  }
162  else
163  return flagst::mk_unknown();
164  }
165  else if(rhs.id()==ID_typecast)
166  {
167  return get_rec(to_typecast_expr(rhs).op(), loc_info_src);
168  }
169  else if(rhs.id()==ID_uninitialized)
170  {
171  return flagst::mk_uninitialized();
172  }
173  else if(rhs.id()==ID_plus)
174  {
175  const auto &plus_expr = to_plus_expr(rhs);
176 
177  if(plus_expr.operands().size() >= 3)
178  {
180  plus_expr.op0().type().id() == ID_pointer,
181  "pointer in pointer-typed sum must be op0");
182  return get_rec(plus_expr.op0(), loc_info_src) | flagst::mk_uses_offset();
183  }
184  else if(plus_expr.operands().size() == 2)
185  {
186  // one must be pointer, one an integer
187  if(plus_expr.op0().type().id() == ID_pointer)
188  {
189  return get_rec(plus_expr.op0(), loc_info_src) |
191  }
192  else if(plus_expr.op1().type().id() == ID_pointer)
193  {
194  return get_rec(plus_expr.op1(), loc_info_src) |
196  }
197  else
198  return flagst::mk_unknown();
199  }
200  else
201  return flagst::mk_unknown();
202  }
203  else if(rhs.id()==ID_minus)
204  {
205  const auto &op0 = to_minus_expr(rhs).op0();
206 
207  if(op0.type().id() == ID_pointer)
208  {
209  return get_rec(op0, loc_info_src) | flagst::mk_uses_offset();
210  }
211  else
212  return flagst::mk_unknown();
213  }
214  else if(rhs.id()==ID_member)
215  {
216  return flagst::mk_unknown();
217  }
218  else if(rhs.id()==ID_index)
219  {
220  return flagst::mk_unknown();
221  }
222  else if(rhs.id()==ID_dereference)
223  {
224  return flagst::mk_unknown();
225  }
226  else if(rhs.id()==ID_side_effect)
227  {
228  const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
229  const irep_idt &statement=side_effect_expr.get_statement();
230 
231  if(statement==ID_allocate)
232  return flagst::mk_dynamic_heap();
233  else
234  return flagst::mk_unknown();
235  }
236  else
237  return flagst::mk_unknown();
238 }
239 
241 {
242  if(cfg.nodes.empty())
243  return;
244 
245  work_queuet work_queue;
246  work_queue.push(0);
247 
248  loc_infos.resize(cfg.nodes.size());
249 
250  // Gather the objects we track, and
251  // feed in sufficiently bad defaults for their value
252  // in the entry location.
253  for(const auto &local : locals.locals)
254  {
255  if(is_tracked(local))
257  }
258 
259  while(!work_queue.empty())
260  {
261  unsigned loc_nr=work_queue.top();
262  const local_cfgt::nodet &node=cfg.nodes[loc_nr];
263  const goto_programt::instructiont &instruction=*node.t;
264  work_queue.pop();
265 
266  auto &loc_info_src=loc_infos[loc_nr];
267  auto loc_info_dest=loc_infos[loc_nr];
268 
269  switch(instruction.type)
270  {
271  case ASSIGN:
272  {
273  const code_assignt &code_assign = instruction.get_assign();
274  assign_lhs(
275  code_assign.lhs(), code_assign.rhs(), loc_info_src, loc_info_dest);
276  break;
277  }
278 
279  case DECL:
280  assign_lhs(
281  instruction.decl_symbol(),
282  exprt(ID_uninitialized),
283  loc_info_src,
284  loc_info_dest);
285  break;
286 
287  case DEAD:
288  assign_lhs(
289  instruction.dead_symbol(),
290  exprt(ID_uninitialized),
291  loc_info_src,
292  loc_info_dest);
293  break;
294 
295  case FUNCTION_CALL:
296  {
297  const auto &lhs = instruction.call_lhs();
298  if(lhs.is_not_nil())
299  assign_lhs(lhs, nil_exprt(), loc_info_src, loc_info_dest);
300  break;
301  }
302 
303  case CATCH:
304  case THROW:
305 #if 0
306  DATA_INVARIANT(false, "Exceptions must be removed before analysis");
307  break;
308 #endif
309  case SET_RETURN_VALUE:
310 #if 0
311  DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
312  break;
313 #endif
314  case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
315  case ATOMIC_END: // Ignoring is a valid over-approximation
316  case LOCATION: // No action required
317  case START_THREAD: // Require a concurrent analysis at higher level
318  case END_THREAD: // Require a concurrent analysis at higher level
319  case SKIP: // No action required
320  case ASSERT: // No action required
321  case ASSUME: // Ignoring is a valid over-approximation
322  case GOTO: // Ignoring the guard is a valid over-approximation
323  case END_FUNCTION: // No action required
324  break;
325  case OTHER:
326 #if 0
328  false, "Unclear what is a safe over-approximation of OTHER");
329 #endif
330  break;
331  case INCOMPLETE_GOTO:
332  case NO_INSTRUCTION_TYPE:
333  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
334  break;
335  }
336 
337  for(const auto &succ : node.successors)
338  {
339  assert(succ<loc_infos.size());
340  if(merge(loc_infos[succ], (loc_info_dest)))
341  work_queue.push(succ);
342  }
343  }
344 }
345 
347  std::ostream &out,
348  const goto_functiont &goto_function,
349  const namespacet &ns) const
350 {
351  unsigned l=0;
352 
353  for(const auto &instruction : goto_function.body.instructions)
354  {
355  out << "**** " << instruction.source_location << "\n";
356 
357  const auto &loc_info=loc_infos[l];
358 
360  p_it=loc_info.begin();
361  p_it!=loc_info.end();
362  p_it++)
363  {
364  out << " " << pointers[p_it-loc_info.begin()]
365  << ": "
366  << *p_it
367  << "\n";
368  }
369 
370  out << "\n";
371  goto_function.body.output_instruction(ns, irep_idt(), out, instruction);
372  out << "\n";
373 
374  l++;
375  }
376 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_functiont::body
goto_programt body
Definition: goto_function.h:26
local_bitvector_analysist::ns
const namespacet & ns
Definition: local_bitvector_analysis.h:182
SET_RETURN_VALUE
@ SET_RETURN_VALUE
Definition: goto_program.h:43
local_bitvector_analysis.h
Field-insensitive, location-sensitive bitvector analysis.
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:350
local_cfgt::loc_map
loc_mapt loc_map
Definition: local_cfg.h:33
local_bitvector_analysist::flagst::mk_null
static flagst mk_null()
Definition: local_bitvector_analysis.h:137
local_bitvector_analysist::flagst::mk_dynamic_local
static flagst mk_dynamic_local()
Definition: local_bitvector_analysis.h:117
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:315
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
local_bitvector_analysist::assign_lhs
void assign_lhs(const exprt &lhs, const exprt &rhs, points_tot &loc_info_src, points_tot &loc_info_dest)
Definition: local_bitvector_analysis.cpp:64
expanding_vectort::const_iterator
data_typet::const_iterator const_iterator
Definition: expanding_vector.h:27
local_bitvector_analysist::flagst::is_dynamic_heap
bool is_dynamic_heap() const
Definition: local_bitvector_analysis.h:132
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:434
local_bitvector_analysist::build
void build()
Definition: local_bitvector_analysis.cpp:240
exprt
Base class for all expressions.
Definition: expr.h:54
localst::locals
locals_sett locals
Definition: locals.h:43
irep_idt
dstringt irep_idt
Definition: irep.h:37
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1952
local_bitvector_analysist::flagst::mk_unknown
static flagst mk_unknown()
Definition: local_bitvector_analysis.h:87
local_bitvector_analysist::is_tracked
bool is_tracked(const irep_idt &identifier)
Definition: local_bitvector_analysis.cpp:57
goto_programt::instructiont::decl_symbol
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:253
expanding_vectort
Definition: expanding_vector.h:17
local_bitvector_analysist::pointers
numberingt< irep_idt > pointers
Definition: local_bitvector_analysis.h:187
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
goto_programt::instructiont::get_assign
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:198
local_bitvector_analysist::loc_infos
loc_infost loc_infos
Definition: local_bitvector_analysis.h:196
local_bitvector_analysist::cfg
local_cfgt cfg
Definition: local_bitvector_analysis.h:47
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
THROW
@ THROW
Definition: goto_program.h:48
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
GOTO
@ GOTO
Definition: goto_program.h:32
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
goto_programt::instructiont::dead_symbol
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:295
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:47
local_bitvector_analysist::get_rec
flagst get_rec(const exprt &rhs, points_tot &loc_info_src)
Definition: local_bitvector_analysis.cpp:115
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
local_bitvector_analysist::locals
localst locals
Definition: local_bitvector_analysis.h:46
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
local_bitvector_analysist::flagst::mk_integer_address
static flagst mk_integer_address()
Definition: local_bitvector_analysis.h:157
local_bitvector_analysist::flagst::is_integer_address
bool is_integer_address() const
Definition: local_bitvector_analysis.h:162
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:310
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:31
local_cfgt::nodes
nodest nodes
Definition: local_cfg.h:36
localst::is_local
bool is_local(const irep_idt &identifier) const
Definition: locals.h:37
index_exprt::array
exprt & array()
Definition: std_expr.h:1344
local_bitvector_analysist::flagst::is_null
bool is_null() const
Definition: local_bitvector_analysis.h:142
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
OTHER
@ OTHER
Definition: goto_program.h:35
local_bitvector_analysist::flagst::is_static_lifetime
bool is_static_lifetime() const
Definition: local_bitvector_analysis.h:152
irept::id
const irep_idt & id() const
Definition: irep.h:407
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
local_cfgt::nodet
Definition: local_cfg.h:26
goto_programt::instructiont::call_lhs
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:375
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:40
SKIP
@ SKIP
Definition: goto_program.h:36
local_bitvector_analysist::flagst::mk_dynamic_heap
static flagst mk_dynamic_heap()
Definition: local_bitvector_analysis.h:127
local_bitvector_analysist::output
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
Definition: local_bitvector_analysis.cpp:346
local_bitvector_analysist::flagst::is_dynamic_local
bool is_dynamic_local() const
Definition: local_bitvector_analysis.h:122
local_bitvector_analysist::work_queuet
std::stack< unsigned > work_queuet
Definition: local_bitvector_analysis.h:185
std_code.h
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1918
local_bitvector_analysist::flagst::mk_uninitialized
static flagst mk_uninitialized()
Definition: local_bitvector_analysis.h:97
local_bitvector_analysist::flagst::is_uses_offset
bool is_uses_offset() const
Definition: local_bitvector_analysis.h:112
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
local_bitvector_analysist::flagst::is_unknown
bool is_unknown() const
Definition: local_bitvector_analysis.h:92
local_bitvector_analysist::dirty
dirtyt dirty
Definition: local_bitvector_analysis.h:45
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
ASSIGN
@ ASSIGN
Definition: goto_program.h:44
local_bitvector_analysist::flagst::mk_uses_offset
static flagst mk_uses_offset()
Definition: local_bitvector_analysis.h:107
CATCH
@ CATCH
Definition: goto_program.h:49
DECL
@ DECL
Definition: goto_program.h:45
expanding_vectort::size
size_type size() const
Definition: expanding_vector.h:46
local_bitvector_analysist::flagst
Definition: local_bitvector_analysis.h:51
numberingt::number
number_type number(const key_type &a)
Definition: numbering.h:37
ASSUME
@ ASSUME
Definition: goto_program.h:33
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
local_bitvector_analysist::flagst::print
void print(std::ostream &) const
Definition: local_bitvector_analysis.cpp:20
local_cfgt::nodet::successors
successorst successors
Definition: local_cfg.h:29
local_bitvector_analysist::flagst::is_uninitialized
bool is_uninitialized() const
Definition: local_bitvector_analysis.h:102
START_THREAD
@ START_THREAD
Definition: goto_program.h:37
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:47
local_bitvector_analysist::get
flagst get(const goto_programt::const_targett t, const exprt &src)
Definition: local_bitvector_analysis.cpp:104
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:42
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
DEAD
@ DEAD
Definition: goto_program.h:46
local_cfgt::nodet::t
goto_programt::const_targett t
Definition: local_cfg.h:28
index_exprt
Array index operator.
Definition: std_expr.h:1328
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:41
symbol_table.h
Author: Diffblue Ltd.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
LOCATION
@ LOCATION
Definition: goto_program.h:39
ASSERT
@ ASSERT
Definition: goto_program.h:34
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
local_bitvector_analysist::merge
static bool merge(points_tot &a, points_tot &b)
Definition: local_bitvector_analysis.cpp:40
END_THREAD
@ END_THREAD
Definition: goto_program.h:38
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:50
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1896
binary_exprt::op0
exprt & op0()
Definition: expr.h:99
local_bitvector_analysist::flagst::mk_static_lifetime
static flagst mk_static_lifetime()
Definition: local_bitvector_analysis.h:147