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 
46 void rd_range_domaint::populate_cache(const irep_idt &identifier) const
47 {
48  assert(bv_container);
49 
50  valuest::const_iterator v_entry=values.find(identifier);
51  if(v_entry==values.end() ||
52  v_entry->second.empty())
53  return;
54 
55  ranges_at_loct &export_entry=export_cache[identifier];
56 
57  for(const auto &id : v_entry->second)
58  {
60 
61  export_entry[v.definition_at].insert(
62  std::make_pair(v.bit_begin, v.bit_end));
63  }
64 }
65 
67  const irep_idt &function_from,
68  locationt from,
69  const irep_idt &function_to,
70  locationt to,
71  ai_baset &ai,
72  const namespacet &ns)
73 {
75  dynamic_cast<reaching_definitions_analysist*>(&ai);
77  rd!=nullptr,
79  "ai has type reaching_definitions_analysist");
80 
81  assert(bv_container);
82 
83  // kill values
84  if(from->is_dead())
85  transform_dead(ns, from);
86  // kill thread-local values
87  else if(from->is_start_thread())
88  transform_start_thread(ns, *rd);
89  // do argument-to-parameter assignments
90  else if(from->is_function_call())
91  transform_function_call(ns, function_from, from, function_to, *rd);
92  // cleanup parameters
93  else if(from->is_end_function())
94  transform_end_function(ns, function_from, from, to, *rd);
95  // lhs assignments
96  else if(from->is_assign())
97  transform_assign(ns, from, from, *rd);
98  // initial (non-deterministic) value
99  else if(from->is_decl())
100  transform_assign(ns, from, from, *rd);
101 
102 #if 0
103  // handle return values
104  if(to->is_function_call())
105  {
106  const code_function_callt &code=to_code_function_call(to->code);
107 
108  if(code.lhs().is_not_nil())
109  {
110  rw_range_set_value_sett rw_set(ns, rd->get_value_sets());
111  goto_rw(to, rw_set);
112  const bool is_must_alias=rw_set.get_w_set().size()==1;
113 
115  {
116  const irep_idt &identifier=it->first;
117  // ignore symex::invalid_object
118  const symbolt *symbol_ptr;
119  if(ns.lookup(identifier, symbol_ptr))
120  continue;
121  assert(symbol_ptr!=0);
122 
123  const range_domaint &ranges=rw_set.get_ranges(it);
124 
125  if(is_must_alias &&
126  (!rd->get_is_threaded()(from) ||
127  (!symbol_ptr->is_shared() &&
128  !rd->get_is_dirty()(identifier))))
129  for(const auto &range : ranges)
130  kill(identifier, range.first, range.second);
131  }
132  }
133  }
134 #endif
135 }
136 
140  const namespacet &,
141  locationt from)
142 {
143  const irep_idt &identifier = to_code_dead(from->code).get_identifier();
144 
145  valuest::iterator entry=values.find(identifier);
146 
147  if(entry!=values.end())
148  {
149  values.erase(entry);
150  export_cache.erase(identifier);
151  }
152 }
153 
155  const namespacet &ns,
157 {
158  for(valuest::iterator it=values.begin();
159  it!=values.end();
160  ) // no ++it
161  {
162  const irep_idt &identifier=it->first;
163 
164  if(!ns.lookup(identifier).is_shared() &&
165  !rd.get_is_dirty()(identifier))
166  {
167  export_cache.erase(identifier);
168 
169  valuest::iterator next=it;
170  ++next;
171  values.erase(it);
172  it=next;
173  }
174  else
175  ++it;
176  }
177 }
178 
180  const namespacet &ns,
181  const irep_idt &function_from,
182  locationt from,
183  const irep_idt &function_to,
185 {
186  const code_function_callt &code=to_code_function_call(from->code);
187 
188  // only if there is an actual call, i.e., we have a body
189  if(function_from != function_to)
190  {
191  for(valuest::iterator it=values.begin();
192  it!=values.end();
193  ) // no ++it
194  {
195  const irep_idt &identifier=it->first;
196 
197  // dereferencing may introduce extra symbols
198  const symbolt *sym;
199  if((ns.lookup(identifier, sym) ||
200  !sym->is_shared()) &&
201  !rd.get_is_dirty()(identifier))
202  {
203  export_cache.erase(identifier);
204 
205  valuest::iterator next=it;
206  ++next;
207  values.erase(it);
208  it=next;
209  }
210  else
211  ++it;
212  }
213 
214  const symbol_exprt &fn_symbol_expr=to_symbol_expr(code.function());
215  const code_typet &code_type=
216  to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type);
217 
218  for(const auto &param : code_type.parameters())
219  {
220  const irep_idt &identifier=param.get_identifier();
221 
222  if(identifier.empty())
223  continue;
224 
225  auto param_bits = pointer_offset_bits(param.type(), ns);
226  if(param_bits.has_value())
227  gen(from, identifier, 0, to_range_spect(*param_bits));
228  else
229  gen(from, identifier, 0, -1);
230  }
231  }
232  else
233  {
234  // handle return values of undefined functions
235  if(to_code_function_call(from->code).lhs().is_not_nil())
236  transform_assign(ns, from, from, rd);
237  }
238 }
239 
241  const namespacet &ns,
242  const irep_idt &function_from,
243  locationt from,
244  locationt to,
246 {
247  locationt call = to;
248  --call;
249  const code_function_callt &code=to_code_function_call(call->code);
250 
251  valuest new_values;
252  new_values.swap(values);
253  values=rd[call].values;
254 
255  for(const auto &new_value : new_values)
256  {
257  const irep_idt &identifier=new_value.first;
258 
259  if(!rd.get_is_threaded()(call) ||
260  (!ns.lookup(identifier).is_shared() &&
261  !rd.get_is_dirty()(identifier)))
262  {
263  for(const auto &id : new_value.second)
264  {
265  const reaching_definitiont &v=bv_container->get(id);
266  kill(v.identifier, v.bit_begin, v.bit_end);
267  }
268  }
269 
270  for(const auto &id : new_value.second)
271  {
272  const reaching_definitiont &v=bv_container->get(id);
274  }
275  }
276 
277  const code_typet &code_type = to_code_type(ns.lookup(function_from).type);
278 
279  for(const auto &param : code_type.parameters())
280  {
281  const irep_idt &identifier=param.get_identifier();
282 
283  if(identifier.empty())
284  continue;
285 
286  valuest::iterator entry=values.find(identifier);
287 
288  if(entry!=values.end())
289  {
290  values.erase(entry);
291  export_cache.erase(identifier);
292  }
293  }
294 
295  // handle return values
296  if(code.lhs().is_not_nil())
297  {
298 #if 0
299  rd_range_domaint *rd_state=
300  dynamic_cast<rd_range_domaint*>(&(rd.get_state(call)));
301  assert(rd_state!=0);
302  rd_state->
303 #endif
304  transform_assign(ns, from, call, rd);
305  }
306 }
307 
309  const namespacet &ns,
310  locationt from,
311  locationt to,
313 {
314  rw_range_set_value_sett rw_set(ns, rd.get_value_sets());
315  goto_rw(to, rw_set);
316  const bool is_must_alias=rw_set.get_w_set().size()==1;
317 
319  {
320  const irep_idt &identifier=it->first;
321  // ignore symex::invalid_object
322  const symbolt *symbol_ptr;
323  if(ns.lookup(identifier, symbol_ptr))
324  continue;
326  symbol_ptr!=nullptr,
328  "Symbol is in symbol table");
329 
330  const range_domaint &ranges=rw_set.get_ranges(it);
331 
332  if(is_must_alias &&
333  (!rd.get_is_threaded()(from) ||
334  (!symbol_ptr->is_shared() &&
335  !rd.get_is_dirty()(identifier))))
336  for(const auto &range : ranges)
337  kill(identifier, range.first, range.second);
338 
339  for(const auto &range : ranges)
340  gen(from, identifier, range.first, range.second);
341  }
342 }
343 
345  const irep_idt &identifier,
346  const range_spect &range_start,
347  const range_spect &range_end)
348 {
349  assert(range_start>=0);
350  // -1 for objects of infinite/unknown size
351  if(range_end==-1)
352  {
353  kill_inf(identifier, range_start);
354  return;
355  }
356 
357  assert(range_end>range_start);
358 
359  valuest::iterator entry=values.find(identifier);
360  if(entry==values.end())
361  return;
362 
363  bool clear_export_cache=false;
364  values_innert new_values;
365 
366  for(values_innert::iterator
367  it=entry->second.begin();
368  it!=entry->second.end();
369  ) // no ++it
370  {
371  const reaching_definitiont &v=bv_container->get(*it);
372 
373  if(v.bit_begin >= range_end)
374  ++it;
375  else if(v.bit_end!=-1 &&
376  v.bit_end <= range_start)
377  ++it;
378  else if(v.bit_begin >= range_start &&
379  v.bit_end!=-1 &&
380  v.bit_end <= range_end) // rs <= a < b <= re
381  {
382  clear_export_cache=true;
383 
384  entry->second.erase(it++);
385  }
386  else if(v.bit_begin >= range_start) // rs <= a <= re < b
387  {
388  clear_export_cache=true;
389 
390  reaching_definitiont v_new=v;
391  v_new.bit_begin=range_end;
392  new_values.insert(bv_container->add(v_new));
393 
394  entry->second.erase(it++);
395  }
396  else if(v.bit_end==-1 ||
397  v.bit_end > range_end) // a <= rs < re < b
398  {
399  clear_export_cache=true;
400 
401  reaching_definitiont v_new=v;
402  v_new.bit_end=range_start;
403 
404  reaching_definitiont v_new2=v;
405  v_new2.bit_begin=range_end;
406 
407  new_values.insert(bv_container->add(v_new));
408  new_values.insert(bv_container->add(v_new2));
409 
410  entry->second.erase(it++);
411  }
412  else // a <= rs < b <= re
413  {
414  clear_export_cache=true;
415 
416  reaching_definitiont v_new=v;
417  v_new.bit_end=range_start;
418  new_values.insert(bv_container->add(v_new));
419 
420  entry->second.erase(it++);
421  }
422  }
423 
424  if(clear_export_cache)
425  export_cache.erase(identifier);
426 
427  values_innert::iterator it=entry->second.begin();
428  for(const auto &id : new_values)
429  {
430  while(it!=entry->second.end() && *it<id)
431  ++it;
432  if(it==entry->second.end() || id<*it)
433  {
434  entry->second.insert(it, id);
435  }
436  else if(it!=entry->second.end())
437  {
438  assert(*it==id);
439  ++it;
440  }
441  }
442 }
443 
445  const irep_idt &,
446  const range_spect &range_start)
447 {
448  assert(range_start>=0);
449 
450 #if 0
451  valuest::iterator entry=values.find(identifier);
452  if(entry==values.end())
453  return;
454 
455  XXX export_cache_available=false;
456 
457  // makes the analysis underapproximating
458  rangest &ranges=entry->second;
459 
460  for(rangest::iterator it=ranges.begin();
461  it!=ranges.end();
462  ) // no ++it
463  if(it->second.first!=-1 &&
464  it->second.first <= range_start)
465  ++it;
466  else if(it->first >= range_start) // rs <= a < b <= re
467  {
468  ranges.erase(it++);
469  }
470  else // a <= rs < b < re
471  {
472  it->second.first=range_start;
473  ++it;
474  }
475 #endif
476 }
477 
483  locationt from,
484  const irep_idt &identifier,
485  const range_spect &range_start,
486  const range_spect &range_end)
487 {
488  // objects of size 0 like union U { signed : 0; };
489  if(range_start==0 && range_end==0)
490  return false;
491 
492  assert(range_start>=0);
493 
494  // -1 for objects of infinite/unknown size
495  assert(range_end>range_start || range_end==-1);
496 
498  v.identifier=identifier;
499  v.definition_at=from;
500  v.bit_begin=range_start;
501  v.bit_end=range_end;
502 
503  if(!values[identifier].insert(bv_container->add(v)).second)
504  return false;
505 
506  export_cache.erase(identifier);
507 
508 #if 0
509  range_spect merged_range_end=range_end;
510 
511  std::pair<valuest::iterator, bool> entry=
512  values.insert(std::make_pair(identifier, rangest()));
513  rangest &ranges=entry.first->second;
514 
515  if(!entry.second)
516  {
517  for(rangest::iterator it=ranges.begin();
518  it!=ranges.end();
519  ) // no ++it
520  {
521  if(it->second.second!=from ||
522  (it->second.first!=-1 && it->second.first <= range_start) ||
523  (range_end!=-1 && it->first >= range_end))
524  ++it;
525  else if(it->first > range_start) // rs < a < b,re
526  {
527  if(range_end!=-1)
528  merged_range_end=std::max(range_end, it->second.first);
529  ranges.erase(it++);
530  }
531  else if(it->second.first==-1 ||
532  (range_end!=-1 &&
533  it->second.first >= range_end)) // a <= rs < re <= b
534  {
535  // nothing to do
536  return false;
537  }
538  else // a <= rs < b < re
539  {
540  it->second.first=range_end;
541  return true;
542  }
543  }
544  }
545 
546  ranges.insert(std::make_pair(
547  range_start,
548  std::make_pair(merged_range_end, from)));
549 #endif
550 
551  return true;
552 }
553 
554 void rd_range_domaint::output(std::ostream &out) const
555 {
556  out << "Reaching definitions:\n";
557 
558  if(has_values.is_known())
559  {
560  out << has_values.to_string() << '\n';
561  return;
562  }
563 
564  for(const auto &value : values)
565  {
566  const irep_idt &identifier=value.first;
567 
568  const ranges_at_loct &ranges=get(identifier);
569 
570  out << " " << identifier << "[";
571 
572  for(ranges_at_loct::const_iterator itl=ranges.begin();
573  itl!=ranges.end();
574  ++itl)
575  for(rangest::const_iterator itr=itl->second.begin();
576  itr!=itl->second.end();
577  ++itr)
578  {
579  if(itr!=itl->second.begin() ||
580  itl!=ranges.begin())
581  out << ";";
582 
583  out << itr->first << ":" << itr->second;
584  out << "@" << itl->first->location_number;
585  }
586 
587  out << "]\n";
588 
589  clear_cache(identifier);
590  }
591 }
592 
595  values_innert &dest,
596  const values_innert &other)
597 {
598  bool more=false;
599 
600 #if 0
601  ranges_at_loct::iterator itr=it->second.begin();
602  for(const auto &o : ito->second)
603  {
604  while(itr!=it->second.end() && itr->first<o.first)
605  ++itr;
606  if(itr==it->second.end() || o.first<itr->first)
607  {
608  it->second.insert(o);
609  more=true;
610  }
611  else if(itr!=it->second.end())
612  {
613  assert(itr->first==o.first);
614 
615  for(const auto &o_range : o.second)
616  more=gen(itr->second, o_range.first, o_range.second) ||
617  more;
618 
619  ++itr;
620  }
621  }
622 #else
623  values_innert::iterator itr=dest.begin();
624  for(const auto &id : other)
625  {
626  while(itr!=dest.end() && *itr<id)
627  ++itr;
628  if(itr==dest.end() || id<*itr)
629  {
630  dest.insert(itr, id);
631  more=true;
632  }
633  else if(itr!=dest.end())
634  {
635  assert(*itr==id);
636  ++itr;
637  }
638  }
639 #endif
640 
641  return more;
642 }
643 
646  const rd_range_domaint &other,
647  locationt,
648  locationt)
649 {
650  bool changed=has_values.is_false();
652 
653  valuest::iterator it=values.begin();
654  for(const auto &value : other.values)
655  {
656  while(it!=values.end() && it->first<value.first)
657  ++it;
658  if(it==values.end() || value.first<it->first)
659  {
660  values.insert(value);
661  changed=true;
662  }
663  else if(it!=values.end())
664  {
665  assert(it->first==value.first);
666 
667  if(merge_inner(it->second, value.second))
668  {
669  changed=true;
670  export_cache.erase(it->first);
671  }
672 
673  ++it;
674  }
675  }
676 
677  return changed;
678 }
679 
682  const rd_range_domaint &other,
683  locationt,
684  locationt,
685  const namespacet &ns)
686 {
687  // TODO: dirty vars
688 #if 0
690  dynamic_cast<reaching_definitions_analysist*>(&ai);
691  assert(rd!=0);
692 #endif
693 
694  bool changed=has_values.is_false();
696 
697  valuest::iterator it=values.begin();
698  for(const auto &value : other.values)
699  {
700  const irep_idt &identifier=value.first;
701 
702  if(!ns.lookup(identifier).is_shared()
703  /*&& !rd.get_is_dirty()(identifier)*/)
704  continue;
705 
706  while(it!=values.end() && it->first<value.first)
707  ++it;
708  if(it==values.end() || value.first<it->first)
709  {
710  values.insert(value);
711  changed=true;
712  }
713  else if(it!=values.end())
714  {
715  assert(it->first==value.first);
716 
717  if(merge_inner(it->second, value.second))
718  {
719  changed=true;
720  export_cache.erase(it->first);
721  }
722 
723  ++it;
724  }
725  }
726 
727  return changed;
728 }
729 
731  const irep_idt &identifier) const
732 {
733  populate_cache(identifier);
734 
735  static ranges_at_loct empty;
736 
737  export_cachet::const_iterator entry=export_cache.find(identifier);
738 
739  if(entry==export_cache.end())
740  return empty;
741  else
742  return entry->second;
743 }
744 
746  const goto_functionst &goto_functions)
747 {
748  auto value_sets_=util_make_unique<value_set_analysis_fit>(ns);
749  (*value_sets_)(goto_functions);
750  value_sets=std::move(value_sets_);
751 
752  is_threaded=util_make_unique<is_threadedt>(goto_functions);
753 
754  is_dirty=util_make_unique<dirtyt>(goto_functions);
755 
757 }
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:382
void initialize(const goto_functionst &goto_functions) override
Initialize all the abstract states for a whole program.
void transform_end_function(const namespacet &ns, const irep_idt &function_from, locationt from, locationt to, reaching_definitions_analysist &rd)
Over-approximate Concurrency for Threaded Goto Programs.
bool is_shared() const
Definition: symbol.h:95
Base type of functions.
Definition: std_types.h:751
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
ai_domain_baset::locationt definition_at
The iterator to the GOTO instruction where the variable has been written to.
Variables whose address is taken.
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:473
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
const irep_idt & get_identifier() const
Definition: std_expr.h:176
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
bool merge_inner(values_innert &dest, const values_innert &other)
Identifies a GOTO instruction where a given variable is defined (i.e.
range_spect bit_begin
The two integers below define a range of bits (i.e.
Symbol table entry.
Definition: symbol.h:27
sparse_bitvector_analysist< reaching_definitiont > * bv_container
It points to the actual reaching definitions data of individual program variables.
statet & get_state(locationt l) override
Get the state for the given location, creating it in a default way if it doesn&#39;t exist.
const char * to_string() const
Definition: threeval.cpp:13
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: ai.cpp:202
void transform_function_call(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, reaching_definitions_analysist &rd)
irep_idt identifier
The name of the variable which was defined.
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
Given the passed variable name identifier it collects data from bv_container for each ID in values[id...
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)
A utility function which updates internal data structures by inserting a new reaching definition reco...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void goto_rw(goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
Definition: goto_rw.cpp:722
std::unique_ptr< value_setst > value_sets
value_setst & get_value_sets() const
void transform_start_thread(const namespacet &ns, reaching_definitions_analysist &rd)
codet representation of a function call statement.
Definition: std_code.h:1036
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
Because the class is inherited from ai_domain_baset, its instance represents an element of a domain o...
void transform_dead(const namespacet &ns, locationt from)
Computes an instance obtained from a *this by transformation over DEAD v GOTO instruction.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
tvt has_values
This (three value logic) flag determines, whether the instance represents top, bottom, or any other element of the lattice, by values TRUE, FALSE, and UNKNOWN respectively.
valuest values
It is an ordered map from program variable names to IDs of reaching_definitiont instances stored in m...
Pointer Logic.
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
std::vector< typename inner_mapt::const_iterator > values
It is a map from an ID to the corresponding reaching_definitiont instance inside the map value_map...
const V & get(const std::size_t value_index) const
bool merge(const rd_range_domaint &other, locationt from, locationt to)
Implements the join operation of two instances *this and other`.
exprt & function()
Definition: std_code.h:1099
The basic interface of an abstract interpreter.
Definition: ai.h:32
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
Computes an instance obtained from the instance *this by transformation over a GOTO instruction refer...
const parameterst & parameters() const
Definition: std_types.h:893
export_cachet export_cache
It is a helper data structure.
reaching_definitions_analysist(const namespacet &_ns)
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:143
Value Set Propagation (flow insensitive)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::unique_ptr< is_threadedt > is_threaded
std::map< locationt, rangest > ranges_at_loct
bool empty() const
Definition: dstring.h:75
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
const irep_idt & get_identifier() const
Definition: std_code.h:442
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:1173