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