CBMC
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  // array_set, array_copy, array_replace have side effects
130  else if(from->is_other())
131  transform_assign(ns, from, function_from, from, *rd);
132 }
133 
137  const namespacet &,
138  locationt from)
139 {
140  const irep_idt &identifier = from->dead_symbol().get_identifier();
141 
142  valuest::iterator entry=values.find(identifier);
143 
144  if(entry!=values.end())
145  {
146  values.erase(entry);
147  export_cache.erase(identifier);
148  }
149 }
150 
152  const namespacet &ns,
154 {
155  for(valuest::iterator it=values.begin();
156  it!=values.end();
157  ) // no ++it
158  {
159  const irep_idt &identifier=it->first;
160 
161  if(!ns.lookup(identifier).is_shared() &&
162  !rd.get_is_dirty()(identifier))
163  {
164  export_cache.erase(identifier);
165 
166  valuest::iterator next=it;
167  ++next;
168  values.erase(it);
169  it=next;
170  }
171  else
172  ++it;
173  }
174 }
175 
177  const namespacet &ns,
178  const irep_idt &function_from,
179  locationt from,
180  const irep_idt &function_to,
182 {
183  // only if there is an actual call, i.e., we have a body
184  const symbol_exprt &fn_symbol_expr = to_symbol_expr(from->call_function());
185  if(function_to == fn_symbol_expr.get_identifier())
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  // dereferencing may introduce extra symbols
194  const symbolt *sym;
195  if((ns.lookup(identifier, sym) ||
196  !sym->is_shared()) &&
197  !rd.get_is_dirty()(identifier))
198  {
199  export_cache.erase(identifier);
200 
201  valuest::iterator next=it;
202  ++next;
203  values.erase(it);
204  it=next;
205  }
206  else
207  ++it;
208  }
209 
210  const code_typet &code_type=
211  to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type);
212 
213  for(const auto &param : code_type.parameters())
214  {
215  const irep_idt &identifier=param.get_identifier();
216 
217  if(identifier.empty())
218  continue;
219 
220  auto param_bits = pointer_offset_bits(param.type(), ns);
221  if(param_bits.has_value())
222  {
223  gen(
224  from,
225  identifier,
226  range_spect{0},
227  range_spect::to_range_spect(*param_bits));
228  }
229  else
230  gen(from, identifier, range_spect{0}, range_spect::unknown());
231  }
232  }
233  else
234  {
235  // handle return values of undefined functions
236  if(from->call_lhs().is_not_nil())
237  transform_assign(ns, from, function_from, from, rd);
238  }
239 }
240 
242  const namespacet &ns,
243  const irep_idt &function_from,
244  locationt from,
245  const irep_idt &function_to,
246  locationt to,
248 {
249  locationt call = to;
250  --call;
251 
252  valuest new_values;
253  new_values.swap(values);
254  values=rd[call].values;
255 
256  for(const auto &new_value : new_values)
257  {
258  const irep_idt &identifier=new_value.first;
259 
260  if(!rd.get_is_threaded()(call) ||
261  (!ns.lookup(identifier).is_shared() &&
262  !rd.get_is_dirty()(identifier)))
263  {
264  for(const auto &id : new_value.second)
265  {
266  const reaching_definitiont &v=bv_container->get(id);
267  kill(v.identifier, v.bit_begin, v.bit_end);
268  }
269  }
270 
271  for(const auto &id : new_value.second)
272  {
273  const reaching_definitiont &v=bv_container->get(id);
275  }
276  }
277 
278  const code_typet &code_type = to_code_type(ns.lookup(function_from).type);
279 
280  for(const auto &param : code_type.parameters())
281  {
282  const irep_idt &identifier=param.get_identifier();
283 
284  if(identifier.empty())
285  continue;
286 
287  valuest::iterator entry=values.find(identifier);
288 
289  if(entry!=values.end())
290  {
291  values.erase(entry);
292  export_cache.erase(identifier);
293  }
294  }
295 
296  // handle return values
297  if(call->call_lhs().is_not_nil())
298  {
299  transform_assign(ns, from, function_to, call, rd);
300  }
301 }
302 
304  const namespacet &ns,
305  locationt from,
306  const irep_idt &function_to,
307  locationt to,
309 {
310  rw_range_set_value_sett rw_set(ns, rd.get_value_sets());
311  goto_rw(function_to, to, rw_set);
312  const bool is_must_alias=rw_set.get_w_set().size()==1;
313 
314  for(const auto &written_object_entry : rw_set.get_w_set())
315  {
316  const irep_idt &identifier = written_object_entry.first;
317  // ignore symex::invalid_object
318  const symbolt *symbol_ptr;
319  if(ns.lookup(identifier, symbol_ptr))
320  continue;
322  symbol_ptr!=nullptr,
324  "Symbol is in symbol table");
325 
326  const range_domaint &ranges =
327  rw_set.get_ranges(written_object_entry.second);
328 
329  if(is_must_alias &&
330  (!rd.get_is_threaded()(from) ||
331  (!symbol_ptr->is_shared() &&
332  !rd.get_is_dirty()(identifier))))
333  for(const auto &range : ranges)
334  kill(identifier, range.first, range.second);
335 
336  for(const auto &range : ranges)
337  gen(from, identifier, range.first, range.second);
338  }
339 }
340 
342  const irep_idt &identifier,
343  const range_spect &range_start,
344  const range_spect &range_end)
345 {
346  PRECONDITION(range_start >= range_spect{0});
347 
348  if(range_end.is_unknown())
349  {
350  kill_inf(identifier, range_start);
351  return;
352  }
353 
354  assert(range_end>range_start);
355 
356  valuest::iterator entry=values.find(identifier);
357  if(entry==values.end())
358  return;
359 
360  bool clear_export_cache=false;
361  values_innert new_values;
362 
363  for(values_innert::iterator
364  it=entry->second.begin();
365  it!=entry->second.end();
366  ) // no ++it
367  {
368  const reaching_definitiont &v=bv_container->get(*it);
369 
370  if(v.bit_begin >= range_end)
371  ++it;
372  else if(!v.bit_end.is_unknown() && v.bit_end <= range_start)
373  {
374  ++it;
375  }
376  else if(
377  v.bit_begin >= range_start && !v.bit_end.is_unknown() &&
378  v.bit_end <= range_end) // rs <= a < b <= re
379  {
380  clear_export_cache=true;
381 
382  entry->second.erase(it++);
383  }
384  else if(v.bit_begin >= range_start) // rs <= a <= re < b
385  {
386  clear_export_cache=true;
387 
388  reaching_definitiont v_new=v;
389  v_new.bit_begin=range_end;
390  new_values.insert(bv_container->add(v_new));
391 
392  entry->second.erase(it++);
393  }
394  else if(v.bit_end.is_unknown() || v.bit_end > range_end) // a <= rs < re < b
395  {
396  clear_export_cache=true;
397 
398  reaching_definitiont v_new=v;
399  v_new.bit_end=range_start;
400 
401  reaching_definitiont v_new2=v;
402  v_new2.bit_begin=range_end;
403 
404  new_values.insert(bv_container->add(v_new));
405  new_values.insert(bv_container->add(v_new2));
406 
407  entry->second.erase(it++);
408  }
409  else // a <= rs < b <= re
410  {
411  clear_export_cache=true;
412 
413  reaching_definitiont v_new=v;
414  v_new.bit_end=range_start;
415  new_values.insert(bv_container->add(v_new));
416 
417  entry->second.erase(it++);
418  }
419  }
420 
421  if(clear_export_cache)
422  export_cache.erase(identifier);
423 
424  values_innert::iterator it=entry->second.begin();
425  for(const auto &id : new_values)
426  {
427  while(it!=entry->second.end() && *it<id)
428  ++it;
429  if(it==entry->second.end() || id<*it)
430  {
431  entry->second.insert(it, id);
432  }
433  else if(it!=entry->second.end())
434  {
435  assert(*it==id);
436  ++it;
437  }
438  }
439 }
440 
442  const irep_idt &,
443  const range_spect &range_start)
444 {
445  PRECONDITION(range_start >= range_spect{0});
446 
447 #if 0
448  valuest::iterator entry=values.find(identifier);
449  if(entry==values.end())
450  return;
451 
452  XXX export_cache_available=false;
453 
454  // makes the analysis underapproximating
455  rangest &ranges=entry->second;
456 
457  for(rangest::iterator it=ranges.begin();
458  it!=ranges.end();
459  ) // no ++it
460  if(it->second.first!=-1 &&
461  it->second.first <= range_start)
462  ++it;
463  else if(it->first >= range_start) // rs <= a < b <= re
464  {
465  ranges.erase(it++);
466  }
467  else // a <= rs < b < re
468  {
469  it->second.first=range_start;
470  ++it;
471  }
472 #endif
473 }
474 
480  locationt from,
481  const irep_idt &identifier,
482  const range_spect &range_start,
483  const range_spect &range_end)
484 {
485  // objects of size 0 like union U { signed : 0; };
486  if(range_start == range_spect{0} && range_end == range_spect{0})
487  return false;
488 
489  PRECONDITION(range_start >= range_spect{0});
490  PRECONDITION(range_end == range_spect::unknown() || range_end > range_start);
491 
492  reaching_definitiont v{identifier, from, range_start, range_end};
493  if(!values[identifier].insert(bv_container->add(v)).second)
494  return false;
495 
496  export_cache.erase(identifier);
497 
498 #if 0
499  range_spect merged_range_end=range_end;
500 
501  std::pair<valuest::iterator, bool> entry=
502  values.insert(std::make_pair(identifier, rangest()));
503  rangest &ranges=entry.first->second;
504 
505  if(!entry.second)
506  {
507  for(rangest::iterator it=ranges.begin();
508  it!=ranges.end();
509  ) // no ++it
510  {
511  if(it->second.second!=from ||
512  (it->second.first!=-1 && it->second.first <= range_start) ||
513  (range_end!=-1 && it->first >= range_end))
514  ++it;
515  else if(it->first > range_start) // rs < a < b,re
516  {
517  if(range_end!=-1)
518  merged_range_end=std::max(range_end, it->second.first);
519  ranges.erase(it++);
520  }
521  else if(it->second.first==-1 ||
522  (range_end!=-1 &&
523  it->second.first >= range_end)) // a <= rs < re <= b
524  {
525  // nothing to do
526  return false;
527  }
528  else // a <= rs < b < re
529  {
530  it->second.first=range_end;
531  return true;
532  }
533  }
534  }
535 
536  ranges.insert(std::make_pair(
537  range_start,
538  std::make_pair(merged_range_end, from)));
539 #endif
540 
541  return true;
542 }
543 
544 void rd_range_domaint::output(std::ostream &out) const
545 {
546  out << "Reaching definitions:\n";
547 
548  if(has_values.is_known())
549  {
550  out << has_values.to_string() << '\n';
551  return;
552  }
553 
554  for(const auto &value : values)
555  {
556  const irep_idt &identifier=value.first;
557 
558  const ranges_at_loct &ranges=get(identifier);
559 
560  out << " " << identifier << "[";
561 
562  for(ranges_at_loct::const_iterator itl=ranges.begin();
563  itl!=ranges.end();
564  ++itl)
565  for(rangest::const_iterator itr=itl->second.begin();
566  itr!=itl->second.end();
567  ++itr)
568  {
569  if(itr!=itl->second.begin() ||
570  itl!=ranges.begin())
571  out << ";";
572 
573  out << itr->first << ":" << itr->second;
574  out << "@" << itl->first->location_number;
575  }
576 
577  out << "]\n";
578 
579  clear_cache(identifier);
580  }
581 }
582 
585  values_innert &dest,
586  const values_innert &other)
587 {
588  bool more=false;
589 
590 #if 0
591  ranges_at_loct::iterator itr=it->second.begin();
592  for(const auto &o : ito->second)
593  {
594  while(itr!=it->second.end() && itr->first<o.first)
595  ++itr;
596  if(itr==it->second.end() || o.first<itr->first)
597  {
598  it->second.insert(o);
599  more=true;
600  }
601  else if(itr!=it->second.end())
602  {
603  assert(itr->first==o.first);
604 
605  for(const auto &o_range : o.second)
606  more=gen(itr->second, o_range.first, o_range.second) ||
607  more;
608 
609  ++itr;
610  }
611  }
612 #else
613  values_innert::iterator itr=dest.begin();
614  for(const auto &id : other)
615  {
616  while(itr!=dest.end() && *itr<id)
617  ++itr;
618  if(itr==dest.end() || id<*itr)
619  {
620  dest.insert(itr, id);
621  more=true;
622  }
623  else if(itr!=dest.end())
624  {
625  assert(*itr==id);
626  ++itr;
627  }
628  }
629 #endif
630 
631  return more;
632 }
633 
635  const rd_range_domaint &other,
636  trace_ptrt,
637  trace_ptrt)
638 {
639  bool changed=has_values.is_false();
641 
642  valuest::iterator it=values.begin();
643  for(const auto &value : other.values)
644  {
645  while(it!=values.end() && it->first<value.first)
646  ++it;
647  if(it==values.end() || value.first<it->first)
648  {
649  values.insert(value);
650  changed=true;
651  }
652  else if(it!=values.end())
653  {
654  assert(it->first==value.first);
655 
656  if(merge_inner(it->second, value.second))
657  {
658  changed=true;
659  export_cache.erase(it->first);
660  }
661 
662  ++it;
663  }
664  }
665 
666  return changed;
667 }
668 
671  const rd_range_domaint &other,
672  locationt,
673  locationt,
674  const namespacet &ns)
675 {
676  // TODO: dirty vars
677 #if 0
679  dynamic_cast<reaching_definitions_analysist*>(&ai);
680  assert(rd!=0);
681 #endif
682 
683  bool changed=has_values.is_false();
685 
686  valuest::iterator it=values.begin();
687  for(const auto &value : other.values)
688  {
689  const irep_idt &identifier=value.first;
690 
691  if(!ns.lookup(identifier).is_shared()
692  /*&& !rd.get_is_dirty()(identifier)*/)
693  continue;
694 
695  while(it!=values.end() && it->first<value.first)
696  ++it;
697  if(it==values.end() || value.first<it->first)
698  {
699  values.insert(value);
700  changed=true;
701  }
702  else if(it!=values.end())
703  {
704  assert(it->first==value.first);
705 
706  if(merge_inner(it->second, value.second))
707  {
708  changed=true;
709  export_cache.erase(it->first);
710  }
711 
712  ++it;
713  }
714  }
715 
716  return changed;
717 }
718 
720  const irep_idt &identifier) const
721 {
722  populate_cache(identifier);
723 
724  static ranges_at_loct empty;
725 
726  export_cachet::const_iterator entry=export_cache.find(identifier);
727 
728  if(entry==export_cache.end())
729  return empty;
730  else
731  return entry->second;
732 }
733 
735  const goto_functionst &goto_functions)
736 {
737  auto value_sets_=util_make_unique<value_set_analysis_fit>(ns);
738  (*value_sets_)(goto_functions);
739  value_sets=std::move(value_sets_);
740 
741  is_threaded=util_make_unique<is_threadedt>(goto_functions);
742 
743  is_dirty=util_make_unique<dirtyt>(goto_functions);
744 
746 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
pointer_offset_size.h
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:286
bad_cast_exceptiont
Definition: base_exceptions.h:17
dirty.h
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:634
range_spect::is_unknown
bool is_unknown() const
Definition: goto_rw.h:74
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:366
rw_range_sett::get_ranges
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition: goto_rw.h:231
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:303
range_spect
Data type to describe upper and lower bounds of the range of bits that a read or write access may aff...
Definition: goto_rw.h:60
rd_range_domaint::ranges_at_loct
std::map< locationt, rangest > ranges_at_loct
Definition: reaching_definitions.h:252
nullptr_exceptiont
Definition: base_exceptions.h:29
reaching_definitions_analysist::get_is_threaded
const is_threadedt & get_is_threaded() const
Definition: reaching_definitions.h:372
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:275
rd_range_domaint::has_values
tvt has_values
This (three value logic) flag determines, whether the instance represents top, bottom,...
Definition: reaching_definitions.h:264
rw_range_set_value_sett
Definition: goto_rw.h:368
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:273
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:112
reaching_definitiont::bit_begin
range_spect bit_begin
The two integers below define a range of bits (i.e.
Definition: reaching_definitions.h:95
rd_range_domaint::get
const ranges_at_loct & get(const irep_idt &identifier) const
Definition: reaching_definitions.cpp:719
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:74
reaching_definitions_analysist
Definition: reaching_definitions.h:354
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:176
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
base_exceptions.h
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
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:387
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:142
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:101
is_threaded.h
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:157
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:222
code_typet
Base type of functions.
Definition: std_types.h:538
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:479
symbolt::is_shared
bool is_shared() const
Definition: symbol.h:95
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
dstringt::empty
bool empty() const
Definition: dstring.h:88
tvt::to_string
const char * to_string() const
Definition: threeval.cpp:13
reaching_definitions.h
value_set_analysis_fi.h
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:251
rd_range_domaint::merge_inner
bool merge_inner(values_innert &dest, const values_innert &other)
Definition: reaching_definitions.cpp:584
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:136
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:195
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:24
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:196
rd_range_domaint::transform_start_thread
void transform_start_thread(const namespacet &ns, reaching_definitions_analysist &rd)
Definition: reaching_definitions.cpp:151
reaching_definitions_analysist::get_is_dirty
const dirtyt & get_is_dirty() const
Definition: reaching_definitions.h:378
rd_range_domaint::merge_shared
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
Definition: reaching_definitions.cpp:670
symbolt
Symbol table entry.
Definition: symbol.h:27
concurrency_aware_ait
Base class for concurrency-aware abstract interpretation.
Definition: ai.h:652
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:118
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:734
reaching_definitiont::bit_end
range_spect bit_end
Definition: reaching_definitions.h:96
ai_domain_factory_baset::locationt
ai_domain_baset::locationt locationt
Definition: ai_domain.h:171
range_spect::unknown
static range_spect unknown()
Definition: goto_rw.h:69
goto_rw
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
Definition: goto_rw.cpp:843
rd_range_domaint::export_cache
export_cachet export_cache
It is a helper data structure.
Definition: reaching_definitions.h:304
rd_range_domaint::kill_inf
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
Definition: reaching_definitions.cpp:441
reaching_definitiont
Identifies a GOTO instruction where a given variable is defined (i.e.
Definition: reaching_definitions.h:85
reaching_definitions_analysist::ns
const namespacet & ns
Definition: reaching_definitions.h:385
rd_range_domaint::kill
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: reaching_definitions.cpp:341
rd_range_domaint::output
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
Definition: reaching_definitions.h:187
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:241
reaching_definitions_analysist::is_dirty
std::unique_ptr< dirtyt > is_dirty
Definition: reaching_definitions.h:388
rd_range_domain_factoryt
This ensures that all domains are constructed with the appropriate pointer back to the analysis engin...
Definition: reaching_definitions.cpp:32
rd_range_domaint::clear_cache
void clear_cache(const irep_idt &identifier) const
Definition: reaching_definitions.h:255
rd_range_domaint::valuest
std::map< irep_idt, values_innert > valuest
Definition: reaching_definitions.h:277
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:386
rw_range_sett::get_w_set
const objectst & get_w_set() const
Definition: goto_rw.h:225
range_domaint
Definition: goto_rw.h:174
range_spect::to_range_spect
static range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:79