cprover
reaching_definitions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Range-based reaching definitions analysis (following Field-
4  Sensitive Program Dependence Analysis, Litvak et al., FSE 2010)
5 
6 Author: Michael Tautschnig
7 
8 Date: February 2013
9 
10 \*******************************************************************/
11 
15 
16 #include "reaching_definitions.h"
17 
19 #include <util/prefix.h>
20 
22 
23 #include "is_threaded.h"
24 #include "dirty.h"
25 
26 void rd_range_domaint::populate_cache(const irep_idt &identifier) const
27 {
28  assert(bv_container);
29 
30  valuest::const_iterator v_entry=values.find(identifier);
31  if(v_entry==values.end() ||
32  v_entry->second.empty())
33  return;
34 
35  ranges_at_loct &export_entry=export_cache[identifier];
36 
37  for(const auto &id : v_entry->second)
38  {
40 
41  export_entry[v.definition_at].insert(
42  std::make_pair(v.bit_begin, v.bit_end));
43  }
44 }
45 
47  locationt from,
48  locationt to,
49  ai_baset &ai,
50  const namespacet &ns)
51 {
53  dynamic_cast<reaching_definitions_analysist*>(&ai);
55  rd!=nullptr,
57  "ai has type reaching_definitions_analysist");
58 
59  assert(bv_container);
60 
61  // kill values
62  if(from->is_dead())
63  transform_dead(ns, from);
64  // kill thread-local values
65  else if(from->is_start_thread())
66  transform_start_thread(ns, *rd);
67  // do argument-to-parameter assignments
68  else if(from->is_function_call())
69  transform_function_call(ns, from, to, *rd);
70  // cleanup parameters
71  else if(from->is_end_function())
72  transform_end_function(ns, from, to, *rd);
73  // lhs assignments
74  else if(from->is_assign())
75  transform_assign(ns, from, from, *rd);
76  // initial (non-deterministic) value
77  else if(from->is_decl())
78  transform_assign(ns, from, from, *rd);
79 
80 #if 0
81  // handle return values
82  if(to->is_function_call())
83  {
84  const code_function_callt &code=to_code_function_call(to->code);
85 
86  if(code.lhs().is_not_nil())
87  {
88  rw_range_set_value_sett rw_set(ns, rd->get_value_sets());
89  goto_rw(to, rw_set);
90  const bool is_must_alias=rw_set.get_w_set().size()==1;
91 
93  {
94  const irep_idt &identifier=it->first;
95  // ignore symex::invalid_object
96  const symbolt *symbol_ptr;
97  if(ns.lookup(identifier, symbol_ptr))
98  continue;
99  assert(symbol_ptr!=0);
100 
101  const range_domaint &ranges=rw_set.get_ranges(it);
102 
103  if(is_must_alias &&
104  (!rd->get_is_threaded()(from) ||
105  (!symbol_ptr->is_shared() &&
106  !rd->get_is_dirty()(identifier))))
107  for(const auto &range : ranges)
108  kill(identifier, range.first, range.second);
109  }
110  }
111  }
112 #endif
113 }
114 
116  const namespacet &ns,
117  locationt from)
118 {
119  const irep_idt &identifier=
120  to_symbol_expr(to_code_dead(from->code).symbol()).get_identifier();
121 
122  valuest::iterator entry=values.find(identifier);
123 
124  if(entry!=values.end())
125  {
126  values.erase(entry);
127  export_cache.erase(identifier);
128  }
129 }
130 
132  const namespacet &ns,
134 {
135  for(valuest::iterator it=values.begin();
136  it!=values.end();
137  ) // no ++it
138  {
139  const irep_idt &identifier=it->first;
140 
141  if(!ns.lookup(identifier).is_shared() &&
142  !rd.get_is_dirty()(identifier))
143  {
144  export_cache.erase(identifier);
145 
146  valuest::iterator next=it;
147  ++next;
148  values.erase(it);
149  it=next;
150  }
151  else
152  ++it;
153  }
154 }
155 
157  const namespacet &ns,
158  locationt from,
159  locationt to,
161 {
162  const code_function_callt &code=to_code_function_call(from->code);
163 
165  ++next;
166 
167  // only if there is an actual call, i.e., we have a body
168  if(next!=to)
169  {
170  for(valuest::iterator it=values.begin();
171  it!=values.end();
172  ) // no ++it
173  {
174  const irep_idt &identifier=it->first;
175 
176  // dereferencing may introduce extra symbols
177  const symbolt *sym;
178  if((ns.lookup(identifier, sym) ||
179  !sym->is_shared()) &&
180  !rd.get_is_dirty()(identifier))
181  {
182  export_cache.erase(identifier);
183 
184  valuest::iterator next=it;
185  ++next;
186  values.erase(it);
187  it=next;
188  }
189  else
190  ++it;
191  }
192 
193  const symbol_exprt &fn_symbol_expr=to_symbol_expr(code.function());
194  const code_typet &code_type=
195  to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type);
196 
197  for(const auto &param : code_type.parameters())
198  {
199  const irep_idt &identifier=param.get_identifier();
200 
201  if(identifier.empty())
202  continue;
203 
204  range_spect size=
205  to_range_spect(pointer_offset_bits(param.type(), ns));
206  gen(from, identifier, 0, size);
207  }
208  }
209  else
210  {
211  // handle return values of undefined functions
212  const code_function_callt &code=to_code_function_call(from->code);
213 
214  if(code.lhs().is_not_nil())
215  transform_assign(ns, from, from, rd);
216  }
217 }
218 
220  const namespacet &ns,
221  locationt from,
222  locationt to,
224 {
226  --call;
227  const code_function_callt &code=to_code_function_call(call->code);
228 
229  valuest new_values;
230  new_values.swap(values);
231  values=rd[call].values;
232 
233  for(const auto &new_value : new_values)
234  {
235  const irep_idt &identifier=new_value.first;
236 
237  if(!rd.get_is_threaded()(call) ||
238  (!ns.lookup(identifier).is_shared() &&
239  !rd.get_is_dirty()(identifier)))
240  {
241  for(const auto &id : new_value.second)
242  {
243  const reaching_definitiont &v=bv_container->get(id);
244  kill(v.identifier, v.bit_begin, v.bit_end);
245  }
246  }
247 
248  for(const auto &id : new_value.second)
249  {
250  const reaching_definitiont &v=bv_container->get(id);
252  }
253  }
254 
255  const code_typet &code_type=
256  to_code_type(ns.lookup(from->function).type);
257 
258  for(const auto &param : code_type.parameters())
259  {
260  const irep_idt &identifier=param.get_identifier();
261 
262  if(identifier.empty())
263  continue;
264 
265  valuest::iterator entry=values.find(identifier);
266 
267  if(entry!=values.end())
268  {
269  values.erase(entry);
270  export_cache.erase(identifier);
271  }
272  }
273 
274  // handle return values
275  if(code.lhs().is_not_nil())
276  {
277 #if 0
278  rd_range_domaint *rd_state=
279  dynamic_cast<rd_range_domaint*>(&(rd.get_state(call)));
280  assert(rd_state!=0);
281  rd_state->
282 #endif
283  transform_assign(ns, from, call, rd);
284  }
285 }
286 
288  const namespacet &ns,
289  locationt from,
290  locationt to,
292 {
293  rw_range_set_value_sett rw_set(ns, rd.get_value_sets());
294  goto_rw(to, rw_set);
295  const bool is_must_alias=rw_set.get_w_set().size()==1;
296 
298  {
299  const irep_idt &identifier=it->first;
300  // ignore symex::invalid_object
301  const symbolt *symbol_ptr;
302  if(ns.lookup(identifier, symbol_ptr))
303  continue;
305  symbol_ptr!=nullptr,
307  "Symbol is in symbol table");
308 
309  const range_domaint &ranges=rw_set.get_ranges(it);
310 
311  if(is_must_alias &&
312  (!rd.get_is_threaded()(from) ||
313  (!symbol_ptr->is_shared() &&
314  !rd.get_is_dirty()(identifier))))
315  for(const auto &range : ranges)
316  kill(identifier, range.first, range.second);
317 
318  for(const auto &range : ranges)
319  gen(from, identifier, range.first, range.second);
320  }
321 }
322 
324  const irep_idt &identifier,
325  const range_spect &range_start,
326  const range_spect &range_end)
327 {
328  assert(range_start>=0);
329  // -1 for objects of infinite/unknown size
330  if(range_end==-1)
331  {
332  kill_inf(identifier, range_start);
333  return;
334  }
335 
336  assert(range_end>range_start);
337 
338  valuest::iterator entry=values.find(identifier);
339  if(entry==values.end())
340  return;
341 
342  bool clear_export_cache=false;
343  values_innert new_values;
344 
345  for(values_innert::iterator
346  it=entry->second.begin();
347  it!=entry->second.end();
348  ) // no ++it
349  {
350  const reaching_definitiont &v=bv_container->get(*it);
351 
352  if(v.bit_begin >= range_end)
353  ++it;
354  else if(v.bit_end!=-1 &&
355  v.bit_end <= range_start)
356  ++it;
357  else if(v.bit_begin >= range_start &&
358  v.bit_end!=-1 &&
359  v.bit_end <= range_end) // rs <= a < b <= re
360  {
361  clear_export_cache=true;
362 
363  entry->second.erase(it++);
364  }
365  else if(v.bit_begin >= range_start) // rs <= a <= re < b
366  {
367  clear_export_cache=true;
368 
369  reaching_definitiont v_new=v;
370  v_new.bit_begin=range_end;
371  new_values.insert(bv_container->add(v_new));
372 
373  entry->second.erase(it++);
374  }
375  else if(v.bit_end==-1 ||
376  v.bit_end > range_end) // a <= rs < re < b
377  {
378  clear_export_cache=true;
379 
380  reaching_definitiont v_new=v;
381  v_new.bit_end=range_start;
382 
383  reaching_definitiont v_new2=v;
384  v_new2.bit_begin=range_end;
385 
386  new_values.insert(bv_container->add(v_new));
387  new_values.insert(bv_container->add(v_new2));
388 
389  entry->second.erase(it++);
390  }
391  else // a <= rs < b <= re
392  {
393  clear_export_cache=true;
394 
395  reaching_definitiont v_new=v;
396  v_new.bit_end=range_start;
397  new_values.insert(bv_container->add(v_new));
398 
399  entry->second.erase(it++);
400  }
401  }
402 
403  if(clear_export_cache)
404  export_cache.erase(identifier);
405 
406  values_innert::iterator it=entry->second.begin();
407  for(const auto &id : new_values)
408  {
409  while(it!=entry->second.end() && *it<id)
410  ++it;
411  if(it==entry->second.end() || id<*it)
412  {
413  entry->second.insert(it, id);
414  }
415  else if(it!=entry->second.end())
416  {
417  assert(*it==id);
418  ++it;
419  }
420  }
421 }
422 
424  const irep_idt &identifier,
425  const range_spect &range_start)
426 {
427  assert(range_start>=0);
428 
429 #if 0
430  valuest::iterator entry=values.find(identifier);
431  if(entry==values.end())
432  return;
433 
434  XXX export_cache_available=false;
435 
436  // makes the analysis underapproximating
437  rangest &ranges=entry->second;
438 
439  for(rangest::iterator it=ranges.begin();
440  it!=ranges.end();
441  ) // no ++it
442  if(it->second.first!=-1 &&
443  it->second.first <= range_start)
444  ++it;
445  else if(it->first >= range_start) // rs <= a < b <= re
446  {
447  ranges.erase(it++);
448  }
449  else // a <= rs < b < re
450  {
451  it->second.first=range_start;
452  ++it;
453  }
454 #endif
455 }
456 
458  locationt from,
459  const irep_idt &identifier,
460  const range_spect &range_start,
461  const range_spect &range_end)
462 {
463  // objects of size 0 like union U { signed : 0; };
464  if(range_start==0 && range_end==0)
465  return false;
466 
467  assert(range_start>=0);
468 
469  // -1 for objects of infinite/unknown size
470  assert(range_end>range_start || range_end==-1);
471 
473  v.identifier=identifier;
474  v.definition_at=from;
475  v.bit_begin=range_start;
476  v.bit_end=range_end;
477 
478  if(!values[identifier].insert(bv_container->add(v)).second)
479  return false;
480 
481  export_cache.erase(identifier);
482 
483 #if 0
484  range_spect merged_range_end=range_end;
485 
486  std::pair<valuest::iterator, bool> entry=
487  values.insert(std::make_pair(identifier, rangest()));
488  rangest &ranges=entry.first->second;
489 
490  if(!entry.second)
491  {
492  for(rangest::iterator it=ranges.begin();
493  it!=ranges.end();
494  ) // no ++it
495  {
496  if(it->second.second!=from ||
497  (it->second.first!=-1 && it->second.first <= range_start) ||
498  (range_end!=-1 && it->first >= range_end))
499  ++it;
500  else if(it->first > range_start) // rs < a < b,re
501  {
502  if(range_end!=-1)
503  merged_range_end=std::max(range_end, it->second.first);
504  ranges.erase(it++);
505  }
506  else if(it->second.first==-1 ||
507  (range_end!=-1 &&
508  it->second.first >= range_end)) // a <= rs < re <= b
509  {
510  // nothing to do
511  return false;
512  }
513  else // a <= rs < b < re
514  {
515  it->second.first=range_end;
516  return true;
517  }
518  }
519  }
520 
521  ranges.insert(std::make_pair(
522  range_start,
523  std::make_pair(merged_range_end, from)));
524 #endif
525 
526  return true;
527 }
528 
529 void rd_range_domaint::output(std::ostream &out) const
530 {
531  out << "Reaching definitions:\n";
532 
533  if(has_values.is_known())
534  {
535  out << has_values.to_string() << '\n';
536  return;
537  }
538 
539  for(const auto &value : values)
540  {
541  const irep_idt &identifier=value.first;
542 
543  const ranges_at_loct &ranges=get(identifier);
544 
545  out << " " << identifier << "[";
546 
547  for(ranges_at_loct::const_iterator itl=ranges.begin();
548  itl!=ranges.end();
549  ++itl)
550  for(rangest::const_iterator itr=itl->second.begin();
551  itr!=itl->second.end();
552  ++itr)
553  {
554  if(itr!=itl->second.begin() ||
555  itl!=ranges.begin())
556  out << ";";
557 
558  out << itr->first << ":" << itr->second;
559  out << "@" << itl->first->location_number;
560  }
561 
562  out << "]\n";
563 
564  clear_cache(identifier);
565  }
566 }
567 
570  values_innert &dest,
571  const values_innert &other)
572 {
573  bool more=false;
574 
575 #if 0
576  ranges_at_loct::iterator itr=it->second.begin();
577  for(const auto &o : ito->second)
578  {
579  while(itr!=it->second.end() && itr->first<o.first)
580  ++itr;
581  if(itr==it->second.end() || o.first<itr->first)
582  {
583  it->second.insert(o);
584  more=true;
585  }
586  else if(itr!=it->second.end())
587  {
588  assert(itr->first==o.first);
589 
590  for(const auto &o_range : o.second)
591  more=gen(itr->second, o_range.first, o_range.second) ||
592  more;
593 
594  ++itr;
595  }
596  }
597 #else
598  values_innert::iterator itr=dest.begin();
599  for(const auto &id : other)
600  {
601  while(itr!=dest.end() && *itr<id)
602  ++itr;
603  if(itr==dest.end() || id<*itr)
604  {
605  dest.insert(itr, id);
606  more=true;
607  }
608  else if(itr!=dest.end())
609  {
610  assert(*itr==id);
611  ++itr;
612  }
613  }
614 #endif
615 
616  return more;
617 }
618 
621  const rd_range_domaint &other,
622  locationt from,
623  locationt to)
624 {
625  bool changed=has_values.is_false();
627 
628  valuest::iterator it=values.begin();
629  for(const auto &value : other.values)
630  {
631  while(it!=values.end() && it->first<value.first)
632  ++it;
633  if(it==values.end() || value.first<it->first)
634  {
635  values.insert(value);
636  changed=true;
637  }
638  else if(it!=values.end())
639  {
640  assert(it->first==value.first);
641 
642  if(merge_inner(it->second, value.second))
643  {
644  changed=true;
645  export_cache.erase(it->first);
646  }
647 
648  ++it;
649  }
650  }
651 
652  return changed;
653 }
654 
657  const rd_range_domaint &other,
660  const namespacet &ns)
661 {
662  // TODO: dirty vars
663 #if 0
665  dynamic_cast<reaching_definitions_analysist*>(&ai);
666  assert(rd!=0);
667 #endif
668 
669  bool changed=has_values.is_false();
671 
672  valuest::iterator it=values.begin();
673  for(const auto &value : other.values)
674  {
675  const irep_idt &identifier=value.first;
676 
677  if(!ns.lookup(identifier).is_shared()
678  /*&& !rd.get_is_dirty()(identifier)*/)
679  continue;
680 
681  while(it!=values.end() && it->first<value.first)
682  ++it;
683  if(it==values.end() || value.first<it->first)
684  {
685  values.insert(value);
686  changed=true;
687  }
688  else if(it!=values.end())
689  {
690  assert(it->first==value.first);
691 
692  if(merge_inner(it->second, value.second))
693  {
694  changed=true;
695  export_cache.erase(it->first);
696  }
697 
698  ++it;
699  }
700  }
701 
702  return changed;
703 }
704 
706  const irep_idt &identifier) const
707 {
708  populate_cache(identifier);
709 
710  static ranges_at_loct empty;
711 
712  export_cachet::const_iterator entry=export_cache.find(identifier);
713 
714  if(entry==export_cache.end())
715  return empty;
716  else
717  return entry->second;
718 }
719 
721 {
722  if(is_dirty)
723  delete is_dirty;
724  if(is_threaded)
725  delete is_threaded;
726  if(value_sets)
727  delete value_sets;
728 }
729 
731  const goto_functionst &goto_functions)
732 {
734  (*value_sets_)(goto_functions);
735  value_sets=value_sets_;
736 
737  is_threaded=new is_threadedt(goto_functions);
738 
739  is_dirty=new dirtyt(goto_functions);
740 
742 }
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
bool is_false() const
Definition: threeval.h:26
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:209
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
Over-approximate Concurrency for Threaded Goto Programs.
bool is_shared() const
Definition: symbol.h:103
Base type of functions.
Definition: std_types.h:734
bool is_not_nil() const
Definition: irep.h:104
#define forall_rw_range_set_w_objects(it, rw_set)
Definition: goto_rw.h:27
void clear_cache(const irep_idt &identifier) const
void transform_function_call(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
ai_domain_baset::locationt definition_at
Variables whose address is taken.
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:260
std::unordered_map< irep_idt, values_innert, irep_id_hash > valuest
const irep_idt & get_identifier() const
Definition: std_expr.h:120
range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:54
static tvt unknown()
Definition: threeval.h:33
int range_spect
Definition: goto_rw.h:52
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
const dirtyt & get_is_dirty() const
bool merge_inner(values_innert &dest, const values_innert &other)
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
sparse_bitvector_analysist< reaching_definitiont > * bv_container
const char * to_string() const
Definition: threeval.cpp:13
instructionst::const_iterator const_targett
bool is_known() const
Definition: threeval.h:28
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
void populate_cache(const irep_idt &identifier) const
bool gen(locationt from, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void goto_rw(goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
Definition: goto_rw.cpp:678
value_setst & get_value_sets() const
void transform_start_thread(const namespacet &ns, reaching_definitions_analysist &rd)
A function call.
Definition: std_code.h:657
void transform_dead(const namespacet &ns, locationt from)
exprt & symbol()
Definition: std_code.h:247
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
Pointer Logic.
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
virtual void initialize(const goto_functionst &goto_functions)
std::vector< typename inner_mapt::const_iterator > values
const V & get(const std::size_t value_index) const
bool merge(const rd_range_domaint &other, locationt from, locationt to)
virtual statet & get_state(goto_programt::const_targett l)
exprt & function()
Definition: std_code.h:677
Definition: ai.h:108
const parameterst & parameters() const
Definition: std_types.h:841
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
Definition: dirty.h:22
export_cachet export_cache
virtual void initialize(const goto_programt &)
Definition: ai.cpp:269
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
std::size_t add(const V &value)
goto_programt::const_targett locationt
Definition: ai.h:42
std::multimap< range_spect, range_spect > rangest
void transform_assign(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
Expression to hold a symbol (variable)
Definition: std_expr.h:82
Value Set Propagation (flow insensitive)
void transform_end_function(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
std::map< locationt, rangest > ranges_at_loct
bool empty() const
Definition: dstring.h:61
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
std::set< std::size_t > values_innert
const is_threadedt & get_is_threaded() const
const ranges_at_loct & get(const irep_idt &identifier) const
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700