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