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 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:274
reaching_definitions_analysist::get_state
statet & get_state(locationt l) override
Get the state for the given location, creating it in a default way if it doesn't exist.
Definition: reaching_definitions.h:352
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:46
reaching_definitions_analysist::reaching_definitions_analysist
reaching_definitions_analysist(const namespacet &_ns)
Definition: reaching_definitions.cpp:29
reaching_definitions_analysist::get_value_sets
value_setst & get_value_sets() const
Definition: reaching_definitions.h:367
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
prefix.h
rd_range_domaint::ranges_at_loct
std::map< locationt, rangest > ranges_at_loct
Definition: reaching_definitions.h:240
goto_rw
void goto_rw(goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
Definition: goto_rw.cpp:722
nullptr_exceptiont
Definition: base_exceptions.h:29
rd_range_domaint::transform_end_function
void transform_end_function(const namespacet &ns, const irep_idt &function_from, locationt from, locationt to, reaching_definitions_analysist &rd)
Definition: reaching_definitions.cpp:240
reaching_definitions_analysist::get_is_threaded
const is_threadedt & get_is_threaded() const
Definition: reaching_definitions.h:373
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:263
rd_range_domaint::has_values
tvt has_values
This (three value logic) flag determines, whether the instance represents top, bottom,...
Definition: reaching_definitions.h:252
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:645
rw_range_set_value_sett
Definition: goto_rw.h:257
rd_range_domaint::bv_container
sparse_bitvector_analysist< reaching_definitiont > * bv_container
It points to the actual reaching definitions data of individual program variables.
Definition: reaching_definitions.h:261
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
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:730
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1089
reaching_definitions_analysist
Definition: reaching_definitions.h:340
to_range_spect
range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:63
tvt::is_known
bool is_known() const
Definition: threeval.h:28
INVARIANT_STRUCTURED
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:382
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:179
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
make_unique.h
reaching_definitions_analysist::is_threaded
std::unique_ptr< is_threadedt > is_threaded
Definition: reaching_definitions.h:388
reaching_definitiont::identifier
irep_idt identifier
The name of the variable which was defined.
Definition: reaching_definitions.h:89
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:66
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:473
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
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:136
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
code_typet
Base type of functions.
Definition: std_types.h:751
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:482
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:1173
dstringt::empty
bool empty() const
Definition: dstring.h:75
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:893
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:239
rd_range_domaint::merge_inner
bool merge_inner(values_innert &dest, const values_innert &other)
Definition: reaching_definitions.cpp:594
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:139
range_spect
int range_spect
Definition: goto_rw.h:61
reaching_definitions_analysist::~reaching_definitions_analysist
virtual ~reaching_definitions_analysist()
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:40
rd_range_domaint::transform_start_thread
void transform_start_thread(const namespacet &ns, reaching_definitions_analysist &rd)
Definition: reaching_definitions.cpp:154
reaching_definitions_analysist::get_is_dirty
const dirtyt & get_is_dirty() const
Definition: reaching_definitions.h:379
rd_range_domaint::merge_shared
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
Definition: reaching_definitions.cpp:681
symbolt
Symbol table entry.
Definition: symbol.h:27
concurrency_aware_ait
Definition: ai.h:467
ai_baset
The basic interface of an abstract interpreter.
Definition: ai.h:32
rd_range_domaint::valuest
std::unordered_map< irep_idt, values_innert > valuest
Definition: reaching_definitions.h:267
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:745
reaching_definitiont::bit_end
range_spect bit_end
Definition: reaching_definitions.h:99
rd_range_domaint::transform_assign
void transform_assign(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
Definition: reaching_definitions.cpp:308
rd_range_domaint::export_cache
export_cachet export_cache
It is a helper data structure.
Definition: reaching_definitions.h:292
rd_range_domaint::kill_inf
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
Definition: reaching_definitions.cpp:444
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:386
code_deadt::get_identifier
const irep_idt & get_identifier() const
Definition: std_code.h:442
rd_range_domaint::kill
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: reaching_definitions.cpp:344
rd_range_domaint::output
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
Definition: reaching_definitions.h:172
ai_baset::initialize
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: ai.cpp:202
reaching_definitions_analysist::is_dirty
std::unique_ptr< dirtyt > is_dirty
Definition: reaching_definitions.h:389
rd_range_domaint::clear_cache
void clear_cache(const irep_idt &identifier) const
Definition: reaching_definitions.h:243
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:387
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
range_domaint
Definition: goto_rw.h:73