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