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_mapt::const_iterator it=locals.locals_map.find(identifier);
64  if(it==locals.locals_map.end() ||
65  it->second.type().id()!=ID_pointer ||
66  dirty(identifier))
67  return false;
68 
69  return true;
70 }
71 
73  const exprt &lhs,
74  const exprt &rhs,
75  points_tot &loc_info_src,
76  points_tot &loc_info_dest)
77 {
78  if(lhs.id()==ID_symbol)
79  {
80  const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
81 
82  if(is_tracked(identifier))
83  {
84  unsigned dest_pointer=pointers.number(identifier);
85  flagst rhs_flags=get_rec(rhs, loc_info_src);
86  loc_info_dest[dest_pointer]=rhs_flags;
87  }
88  }
89  else if(lhs.id()==ID_dereference)
90  {
91  }
92  else if(lhs.id()==ID_index)
93  {
94  assign_lhs(to_index_expr(lhs).array(), rhs, loc_info_src, loc_info_dest);
95  }
96  else if(lhs.id()==ID_member)
97  {
98  assign_lhs(
99  to_member_expr(lhs).struct_op(), rhs, loc_info_src, loc_info_dest);
100  }
101  else if(lhs.id()==ID_typecast)
102  {
103  assign_lhs(to_typecast_expr(lhs).op(), rhs, loc_info_src, loc_info_dest);
104  }
105  else if(lhs.id()==ID_if)
106  {
107  assign_lhs(to_if_expr(lhs).true_case(), rhs, loc_info_src, loc_info_dest);
108  assign_lhs(to_if_expr(lhs).false_case(), rhs, loc_info_src, loc_info_dest);
109  }
110 }
111 
114  const exprt &rhs)
115 {
116  local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
117 
118  assert(loc_it!=cfg.loc_map.end());
119 
120  return get_rec(rhs, loc_infos[loc_it->second]);
121 }
122 
124  const exprt &rhs,
125  points_tot &loc_info_src)
126 {
127  if(rhs.id()==ID_constant)
128  {
129  if(rhs.is_zero())
130  return flagst::mk_null();
131  else
133  }
134  else if(rhs.id()==ID_symbol)
135  {
136  const irep_idt &identifier=to_symbol_expr(rhs).get_identifier();
137  if(is_tracked(identifier))
138  {
139  unsigned src_pointer=pointers.number(identifier);
140  return loc_info_src[src_pointer];
141  }
142  else
143  return flagst::mk_unknown();
144  }
145  else if(rhs.id()==ID_address_of)
146  {
147  const exprt &object=to_address_of_expr(rhs).object();
148 
149  if(object.id()==ID_symbol)
150  {
151  if(locals.is_local(to_symbol_expr(object).get_identifier()))
152  return flagst::mk_dynamic_local();
153  else
155  }
156  else if(object.id()==ID_index)
157  {
158  const index_exprt &index_expr=to_index_expr(object);
159  if(index_expr.array().id()==ID_symbol)
160  {
161  if(locals.is_local(
162  to_symbol_expr(index_expr.array()).get_identifier()))
164  else
166  }
167  else
168  return flagst::mk_unknown();
169  }
170  else
171  return flagst::mk_unknown();
172  }
173  else if(rhs.id()==ID_typecast)
174  {
175  return get_rec(to_typecast_expr(rhs).op(), loc_info_src);
176  }
177  else if(rhs.id()==ID_uninitialized)
178  {
179  return flagst::mk_uninitialized();
180  }
181  else if(rhs.id()==ID_plus)
182  {
183  if(rhs.operands().size()>=3)
184  {
185  assert(rhs.op0().type().id()==ID_pointer);
186  return get_rec(rhs.op0(), loc_info_src) |
188  }
189  else if(rhs.operands().size()==2)
190  {
191  // one must be pointer, one an integer
192  if(rhs.op0().type().id()==ID_pointer)
193  {
194  return get_rec(rhs.op0(), loc_info_src) |
196  }
197  else if(rhs.op1().type().id()==ID_pointer)
198  {
199  return get_rec(rhs.op1(), loc_info_src) |
201  }
202  else
203  return flagst::mk_unknown();
204  }
205  else
206  return flagst::mk_unknown();
207  }
208  else if(rhs.id()==ID_minus)
209  {
210  if(rhs.op0().type().id()==ID_pointer)
211  {
212  return get_rec(rhs.op0(), loc_info_src) |
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_map)
258  if(is_tracked(local.first))
259  loc_infos[0][pointers.number(local.first)]=flagst::mk_unknown();
260 
261  while(!work_queue.empty())
262  {
263  unsigned loc_nr=work_queue.top();
264  const local_cfgt::nodet &node=cfg.nodes[loc_nr];
265  const goto_programt::instructiont &instruction=*node.t;
266  work_queue.pop();
267 
268  auto &loc_info_src=loc_infos[loc_nr];
269  auto loc_info_dest=loc_infos[loc_nr];
270 
271  switch(instruction.type)
272  {
273  case ASSIGN:
274  {
275  const code_assignt &code_assign=to_code_assign(instruction.code);
276  assign_lhs(
277  code_assign.lhs(), code_assign.rhs(), loc_info_src, loc_info_dest);
278  }
279  break;
280 
281  case DECL:
282  {
283  const code_declt &code_decl=to_code_decl(instruction.code);
284  assign_lhs(
285  code_decl.symbol(),
286  exprt(ID_uninitialized),
287  loc_info_src,
288  loc_info_dest);
289  }
290  break;
291 
292  case DEAD:
293  {
294  const code_deadt &code_dead=to_code_dead(instruction.code);
295  assign_lhs(
296  code_dead.symbol(),
297  exprt(ID_uninitialized),
298  loc_info_src,
299  loc_info_dest);
300  }
301  break;
302 
303  case FUNCTION_CALL:
304  {
305  const code_function_callt &code_function_call=
306  to_code_function_call(instruction.code);
307  if(code_function_call.lhs().is_not_nil())
308  assign_lhs(
309  code_function_call.lhs(), nil_exprt(), loc_info_src, loc_info_dest);
310  }
311  break;
312 
313  default:
314  {
315  }
316  }
317 
318  for(const auto &succ : node.successors)
319  {
320  assert(succ<loc_infos.size());
321  if(merge(loc_infos[succ], (loc_info_dest)))
322  work_queue.push(succ);
323  }
324  }
325 }
326 
328  std::ostream &out,
329  const goto_functiont &goto_function,
330  const namespacet &ns) const
331 {
332  unsigned l=0;
333 
334  forall_goto_program_instructions(i_it, goto_function.body)
335  {
336  out << "**** " << i_it->source_location << "\n";
337 
338  const auto &loc_info=loc_infos[l];
339 
341  p_it=loc_info.begin();
342  p_it!=loc_info.end();
343  p_it++)
344  {
345  out << " " << pointers[p_it-loc_info.begin()]
346  << ": "
347  << *p_it
348  << "\n";
349  }
350 
351  out << "\n";
352  goto_function.body.output_instruction(ns, "", out, *i_it);
353  out << "\n";
354 
355  l++;
356  }
357 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:291
bool is_not_nil() const
Definition: irep.h:173
loc_mapt loc_map
Definition: local_cfg.h:33
exprt & object()
Definition: std_expr.h:3178
exprt & op0()
Definition: expr.h:72
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:344
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
exprt & symbol()
Definition: std_code.h:268
locals_mapt locals_map
Definition: locals.h:38
bool is_tracked(const irep_idt &identifier)
Deprecated expression utility functions.
const irep_idt & get_identifier() const
Definition: std_expr.h:128
goto_programt body
Definition: goto_function.h:23
flagst get_rec(const exprt &rhs, points_tot &loc_info_src)
typet & type()
Definition: expr.h:56
Field-insensitive, location-sensitive bitvector analysis.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3199
size_type size() const
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1326
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
nodest nodes
Definition: local_cfg.h:36
bool is_local(const irep_idt &identifier) const
Definition: locals.h:32
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:209
A declaration of a local variable.
Definition: std_code.h:254
The NIL expression.
Definition: std_expr.h:4508
exprt & rhs()
Definition: std_code.h:214
API to expression classes.
exprt & op1()
Definition: expr.h:75
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
A function call.
Definition: std_code.h:858
data_typet::const_iterator const_iterator
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
static bool merge(points_tot &a, points_tot &b)
exprt & symbol()
Definition: std_code.h:321
goto_programt::const_targett t
Definition: local_cfg.h:28
void assign_lhs(const exprt &lhs, const exprt &rhs, points_tot &loc_info_src, points_tot &loc_info_dest)
flagst get(const goto_programt::const_targett t, const exprt &src)
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
Base class for all expressions.
Definition: expr.h:42
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
A removal of a local variable.
Definition: std_code.h:307
bool is_zero() const
Definition: expr.cpp:161
An expression containing a side effect.
Definition: std_code.h:1271
operandst & operands()
Definition: expr.h:66
std::stack< unsigned > work_queuet
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
exprt & array()
Definition: std_expr.h:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
Assignment.
Definition: std_code.h:196
const irep_idt & get_statement() const
Definition: std_code.h:1292
successorst successors
Definition: local_cfg.h:29
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909
array index operator
Definition: std_expr.h:1462