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 <iterator>
15 #include <algorithm>
16 
17 #include <util/std_expr.h>
18 #include <util/std_code.h>
19 #include <util/expr_util.h>
20 
21 #include <util/c_types.h>
22 #include <langapi/language_util.h>
23 
24 void local_bitvector_analysist::flagst::print(std::ostream &out) const
25 {
26  if(is_unknown())
27  out << "+unknown";
28  if(is_uninitialized())
29  out << "+uninitialized";
30  if(is_uses_offset())
31  out << "+uses_offset";
32  if(is_dynamic_local())
33  out << "+dynamic_local";
34  if(is_dynamic_heap())
35  out << "+dynamic_heap";
36  if(is_null())
37  out << "+null";
38  if(is_static_lifetime())
39  out << "+static_lifetime";
40  if(is_integer_address())
41  out << "+integer_address";
42 }
43 
45 {
46  bool result=false;
47 
48  std::size_t max_index=
49  std::max(a.size(), b.size());
50 
51  for(std::size_t i=0; i<max_index; i++)
52  {
53  if(a[i].merge(b[i]))
54  result=true;
55  }
56 
57  return result;
58 }
59 
62 {
63  localst::locals_sett::const_iterator it = locals.locals.find(identifier);
64  return it != locals.locals.end() && ns.lookup(*it).type.id() == ID_pointer &&
65  !dirty(identifier);
66 }
67 
69  const exprt &lhs,
70  const exprt &rhs,
71  points_tot &loc_info_src,
72  points_tot &loc_info_dest)
73 {
74  if(lhs.id()==ID_symbol)
75  {
76  const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
77 
78  if(is_tracked(identifier))
79  {
80  unsigned dest_pointer=pointers.number(identifier);
81  flagst rhs_flags=get_rec(rhs, loc_info_src);
82  loc_info_dest[dest_pointer]=rhs_flags;
83  }
84  }
85  else if(lhs.id()==ID_dereference)
86  {
87  }
88  else if(lhs.id()==ID_index)
89  {
90  assign_lhs(to_index_expr(lhs).array(), rhs, loc_info_src, loc_info_dest);
91  }
92  else if(lhs.id()==ID_member)
93  {
94  assign_lhs(
95  to_member_expr(lhs).struct_op(), rhs, loc_info_src, loc_info_dest);
96  }
97  else if(lhs.id()==ID_typecast)
98  {
99  assign_lhs(to_typecast_expr(lhs).op(), rhs, loc_info_src, loc_info_dest);
100  }
101  else if(lhs.id()==ID_if)
102  {
103  assign_lhs(to_if_expr(lhs).true_case(), rhs, loc_info_src, loc_info_dest);
104  assign_lhs(to_if_expr(lhs).false_case(), rhs, loc_info_src, loc_info_dest);
105  }
106 }
107 
110  const exprt &rhs)
111 {
112  local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
113 
114  assert(loc_it!=cfg.loc_map.end());
115 
116  return get_rec(rhs, loc_infos[loc_it->second]);
117 }
118 
120  const exprt &rhs,
121  points_tot &loc_info_src)
122 {
123  if(rhs.id()==ID_constant)
124  {
125  if(rhs.is_zero())
126  return flagst::mk_null();
127  else
129  }
130  else if(rhs.id()==ID_symbol)
131  {
132  const irep_idt &identifier=to_symbol_expr(rhs).get_identifier();
133  if(is_tracked(identifier))
134  {
135  unsigned src_pointer=pointers.number(identifier);
136  return loc_info_src[src_pointer];
137  }
138  else
139  return flagst::mk_unknown();
140  }
141  else if(rhs.id()==ID_address_of)
142  {
143  const exprt &object=to_address_of_expr(rhs).object();
144 
145  if(object.id()==ID_symbol)
146  {
147  if(locals.is_local(to_symbol_expr(object).get_identifier()))
148  return flagst::mk_dynamic_local();
149  else
151  }
152  else if(object.id()==ID_index)
153  {
154  const index_exprt &index_expr=to_index_expr(object);
155  if(index_expr.array().id()==ID_symbol)
156  {
157  if(locals.is_local(
158  to_symbol_expr(index_expr.array()).get_identifier()))
160  else
162  }
163  else
164  return flagst::mk_unknown();
165  }
166  else
167  return flagst::mk_unknown();
168  }
169  else if(rhs.id()==ID_typecast)
170  {
171  return get_rec(to_typecast_expr(rhs).op(), loc_info_src);
172  }
173  else if(rhs.id()==ID_uninitialized)
174  {
175  return flagst::mk_uninitialized();
176  }
177  else if(rhs.id()==ID_plus)
178  {
179  const auto &plus_expr = to_plus_expr(rhs);
180 
181  if(plus_expr.operands().size() >= 3)
182  {
184  plus_expr.op0().type().id() == ID_pointer,
185  "pointer in pointer-typed sum must be op0");
186  return get_rec(plus_expr.op0(), loc_info_src) | flagst::mk_uses_offset();
187  }
188  else if(plus_expr.operands().size() == 2)
189  {
190  // one must be pointer, one an integer
191  if(plus_expr.op0().type().id() == ID_pointer)
192  {
193  return get_rec(plus_expr.op0(), loc_info_src) |
195  }
196  else if(plus_expr.op1().type().id() == ID_pointer)
197  {
198  return get_rec(plus_expr.op1(), loc_info_src) |
200  }
201  else
202  return flagst::mk_unknown();
203  }
204  else
205  return flagst::mk_unknown();
206  }
207  else if(rhs.id()==ID_minus)
208  {
209  const auto &op0 = to_minus_expr(rhs).op0();
210 
211  if(op0.type().id() == ID_pointer)
212  {
213  return get_rec(op0, loc_info_src) | flagst::mk_uses_offset();
214  }
215  else
216  return flagst::mk_unknown();
217  }
218  else if(rhs.id()==ID_member)
219  {
220  return flagst::mk_unknown();
221  }
222  else if(rhs.id()==ID_index)
223  {
224  return flagst::mk_unknown();
225  }
226  else if(rhs.id()==ID_dereference)
227  {
228  return flagst::mk_unknown();
229  }
230  else if(rhs.id()==ID_side_effect)
231  {
232  const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
233  const irep_idt &statement=side_effect_expr.get_statement();
234 
235  if(statement==ID_allocate)
236  return flagst::mk_dynamic_heap();
237  else
238  return flagst::mk_unknown();
239  }
240  else
241  return flagst::mk_unknown();
242 }
243 
245 {
246  if(cfg.nodes.empty())
247  return;
248 
249  work_queuet work_queue;
250  work_queue.push(0);
251 
252  loc_infos.resize(cfg.nodes.size());
253 
254  // Gather the objects we track, and
255  // feed in sufficiently bad defaults for their value
256  // in the entry location.
257  for(const auto &local : locals.locals)
258  {
259  if(is_tracked(local))
260  loc_infos[0][pointers.number(local)] = flagst::mk_unknown();
261  }
262 
263  while(!work_queue.empty())
264  {
265  unsigned loc_nr=work_queue.top();
266  const local_cfgt::nodet &node=cfg.nodes[loc_nr];
267  const goto_programt::instructiont &instruction=*node.t;
268  work_queue.pop();
269 
270  auto &loc_info_src=loc_infos[loc_nr];
271  auto loc_info_dest=loc_infos[loc_nr];
272 
273  switch(instruction.type)
274  {
275  case ASSIGN:
276  {
277  const code_assignt &code_assign = to_code_assign(instruction.code);
278  assign_lhs(
279  code_assign.lhs(), code_assign.rhs(), loc_info_src, loc_info_dest);
280  break;
281  }
282 
283  case DECL:
284  {
285  const code_declt &code_decl = to_code_decl(instruction.code);
286  assign_lhs(
287  code_decl.symbol(),
288  exprt(ID_uninitialized),
289  loc_info_src,
290  loc_info_dest);
291  break;
292  }
293 
294  case DEAD:
295  {
296  const code_deadt &code_dead = to_code_dead(instruction.code);
297  assign_lhs(
298  code_dead.symbol(),
299  exprt(ID_uninitialized),
300  loc_info_src,
301  loc_info_dest);
302  break;
303  }
304 
305  case FUNCTION_CALL:
306  {
307  const code_function_callt &code_function_call =
308  to_code_function_call(instruction.code);
309  if(code_function_call.lhs().is_not_nil())
310  assign_lhs(
311  code_function_call.lhs(), nil_exprt(), loc_info_src, loc_info_dest);
312  break;
313  }
314 
315  case CATCH:
316  case THROW:
317 #if 0
318  DATA_INVARIANT(false, "Exceptions must be removed before analysis");
319  break;
320 #endif
321  case RETURN:
322 #if 0
323  DATA_INVARIANT(false, "Returns must be removed before analysis");
324  break;
325 #endif
326  case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
327  case ATOMIC_END: // Ignoring is a valid over-approximation
328  case LOCATION: // No action required
329  case START_THREAD: // Require a concurrent analysis at higher level
330  case END_THREAD: // Require a concurrent analysis at higher level
331  case SKIP: // No action required
332  case ASSERT: // No action required
333  case ASSUME: // Ignoring is a valid over-approximation
334  case GOTO: // Ignoring the guard is a valid over-approximation
335  case END_FUNCTION: // No action required
336  break;
337  case OTHER:
338 #if 0
340  false, "Unclear what is a safe over-approximation of OTHER");
341 #endif
342  break;
343  case INCOMPLETE_GOTO:
344  case NO_INSTRUCTION_TYPE:
345  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
346  break;
347  }
348 
349  for(const auto &succ : node.successors)
350  {
351  assert(succ<loc_infos.size());
352  if(merge(loc_infos[succ], (loc_info_dest)))
353  work_queue.push(succ);
354  }
355  }
356 }
357 
359  std::ostream &out,
360  const goto_functiont &goto_function,
361  const namespacet &ns) const
362 {
363  unsigned l=0;
364 
365  forall_goto_program_instructions(i_it, goto_function.body)
366  {
367  out << "**** " << i_it->source_location << "\n";
368 
369  const auto &loc_info=loc_infos[l];
370 
372  p_it=loc_info.begin();
373  p_it!=loc_info.end();
374  p_it++)
375  {
376  out << " " << pointers[p_it-loc_info.begin()]
377  << ": "
378  << *p_it
379  << "\n";
380  }
381 
382  out << "\n";
383  goto_function.body.output_instruction(ns, irep_idt(), out, *i_it);
384  out << "\n";
385 
386  l++;
387  }
388 }
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:30
local_bitvector_analysist::ns
const namespacet & ns
Definition: local_bitvector_analysis.h:181
local_bitvector_analysis.h
Field-insensitive, location-sensitive bitvector analysis.
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:450
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
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:136
local_bitvector_analysist::flagst::mk_dynamic_local
static flagst mk_dynamic_local()
Definition: local_bitvector_analysis.h:116
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
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
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:68
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:131
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:272
local_bitvector_analysist::build
void build()
Definition: local_bitvector_analysis.cpp:244
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
exprt
Base class for all expressions.
Definition: expr.h:53
localst::locals
locals_sett locals
Definition: locals.h:38
irep_idt
dstringt irep_idt
Definition: irep.h:32
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1931
local_bitvector_analysist::flagst::mk_unknown
static flagst mk_unknown()
Definition: local_bitvector_analysis.h:86
local_bitvector_analysist::is_tracked
bool is_tracked(const irep_idt &identifier)
Definition: local_bitvector_analysis.cpp:61
expanding_vectort
Definition: expanding_vector.h:17
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:965
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
local_bitvector_analysist::loc_infos
loc_infost loc_infos
Definition: local_bitvector_analysis.h:195
local_bitvector_analysist::cfg
local_cfgt cfg
Definition: local_bitvector_analysis.h:46
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
THROW
@ THROW
Definition: goto_program.h:50
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::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
coverage_criteriont::LOCATION
@ LOCATION
GOTO
@ GOTO
Definition: goto_program.h:34
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:511
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_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:41
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
language_util.h
local_bitvector_analysist::get_rec
flagst get_rec(const exprt &rhs, points_tot &loc_info_src)
Definition: local_bitvector_analysis.cpp:119
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:519
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
local_bitvector_analysist::locals
localst locals
Definition: local_bitvector_analysis.h:45
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
local_bitvector_analysist::flagst::mk_integer_address
static flagst mk_integer_address()
Definition: local_bitvector_analysis.h:156
local_bitvector_analysist::flagst::is_integer_address
bool is_integer_address() const
Definition: local_bitvector_analysis.h:161
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:920
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
local_cfgt::nodes
nodest nodes
Definition: local_cfg.h:36
localst::is_local
bool is_local(const irep_idt &identifier) const
Definition: locals.h:32
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
local_bitvector_analysist::flagst::is_null
bool is_null() const
Definition: local_bitvector_analysis.h:141
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
OTHER
@ OTHER
Definition: goto_program.h:37
code_deadt::symbol
symbol_exprt & symbol()
Definition: std_code.h:473
local_bitvector_analysist::flagst::is_static_lifetime
bool is_static_lifetime() const
Definition: local_bitvector_analysis.h:151
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
local_cfgt::nodet
Definition: local_cfg.h:26
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:42
SKIP
@ SKIP
Definition: goto_program.h:38
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:467
local_bitvector_analysist::flagst::mk_dynamic_heap
static flagst mk_dynamic_heap()
Definition: local_bitvector_analysis.h:126
local_bitvector_analysist::output
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
Definition: local_bitvector_analysis.cpp:358
local_bitvector_analysist::flagst::is_dynamic_local
bool is_dynamic_local() const
Definition: local_bitvector_analysis.h:121
local_bitvector_analysist::work_queuet
std::stack< unsigned > work_queuet
Definition: local_bitvector_analysis.h:184
std_code.h
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:408
local_bitvector_analysist::pointers
numbering< irep_idt > pointers
Definition: local_bitvector_analysis.h:186
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1897
local_bitvector_analysist::flagst::mk_uninitialized
static flagst mk_uninitialized()
Definition: local_bitvector_analysis.h:96
local_bitvector_analysist::flagst::is_uses_offset
bool is_uses_offset() const
Definition: local_bitvector_analysis.h:111
RETURN
@ RETURN
Definition: goto_program.h:45
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
local_bitvector_analysist::flagst::is_unknown
bool is_unknown() const
Definition: local_bitvector_analysis.h:91
local_bitvector_analysist::dirty
dirtyt dirty
Definition: local_bitvector_analysis.h:44
expr_util.h
Deprecated expression utility functions.
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
local_bitvector_analysist::flagst::mk_uses_offset
static flagst mk_uses_offset()
Definition: local_bitvector_analysis.h:106
CATCH
@ CATCH
Definition: goto_program.h:51
DECL
@ DECL
Definition: goto_program.h:47
expanding_vectort::size
size_type size() const
Definition: expanding_vector.h:46
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
local_bitvector_analysist::flagst
Definition: local_bitvector_analysis.h:50
ASSUME
@ ASSUME
Definition: goto_program.h:35
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
local_bitvector_analysist::flagst::print
void print(std::ostream &) const
Definition: local_bitvector_analysis.cpp:24
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:101
START_THREAD
@ START_THREAD
Definition: goto_program.h:39
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
local_bitvector_analysist::get
flagst get(const goto_programt::const_targett t, const exprt &src)
Definition: local_bitvector_analysis.cpp:108
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:44
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
DEAD
@ DEAD
Definition: goto_program.h:48
local_cfgt::nodet::t
goto_programt::const_targett t
Definition: local_cfg.h:28
index_exprt
Array index operator.
Definition: std_expr.h:1293
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:43
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
ASSERT
@ ASSERT
Definition: goto_program.h:36
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
std_expr.h
API to expression classes.
c_types.h
local_bitvector_analysist::merge
static bool merge(points_tot &a, points_tot &b)
Definition: local_bitvector_analysis.cpp:44
END_THREAD
@ END_THREAD
Definition: goto_program.h:40
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
local_bitvector_analysist::flagst::mk_static_lifetime
static flagst mk_static_lifetime()
Definition: local_bitvector_analysis.h:146