cprover
reaching_definitions.h
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 
24 
25 #ifndef CPROVER_ANALYSES_REACHING_DEFINITIONS_H
26 #define CPROVER_ANALYSES_REACHING_DEFINITIONS_H
27 
28 #include <util/base_exceptions.h>
29 #include <util/threeval.h>
30 
31 #include "ai.h"
32 #include "goto_rw.h"
33 
34 class value_setst;
35 class is_threadedt;
36 class dirtyt;
38 
42 template<typename V>
44 {
45 public:
46  const V &get(const std::size_t value_index) const
47  {
48  assert(value_index<values.size());
49  return values[value_index]->first;
50  }
51 
52  std::size_t add(const V &value)
53  {
54  inner_mapt &m=value_map[value.identifier];
55 
56  std::pair<typename inner_mapt::iterator, bool> entry=
57  m.insert(std::make_pair(value, values.size()));
58 
59  if(entry.second)
60  values.push_back(entry.first);
61 
62  return entry.first->second;
63  }
64 
65  void clear()
66  {
67  value_map.clear();
68  values.clear();
69  }
70 
71 protected:
72  typedef typename std::map<V, std::size_t> inner_mapt;
77  std::vector<typename inner_mapt::const_iterator> values;
81  std::unordered_map<irep_idt, inner_mapt> value_map;
82 };
83 
87 {
100 };
101 
104 inline bool operator<(
105  const reaching_definitiont &a,
106  const reaching_definitiont &b)
107 {
109  return true;
111  return false;
112 
113  if(a.bit_begin<b.bit_begin)
114  return true;
115  if(b.bit_begin<a.bit_begin)
116  return false;
117 
118  if(a.bit_end<b.bit_end)
119  return true;
120  if(b.bit_end<a.bit_end)
121  return false;
122 
123  // we do not expect comparison of unrelated definitions
124  // as this operator< is only used in sparse_bitvector_analysist
125  assert(a.identifier==b.identifier);
126 
127  return false;
128 }
129 
137 {
138 public:
141  : ai_domain_baset(), has_values(false), bv_container(_bv_container)
142  {
143  PRECONDITION(bv_container != nullptr);
144  }
145 
158  void transform(
159  const irep_idt &function_from,
160  trace_ptrt trace_from,
161  const irep_idt &function_to,
162  trace_ptrt trace_to,
163  ai_baset &ai,
164  const namespacet &ns) final override;
165 
166  void output(
167  std::ostream &out,
168  const ai_baset &,
169  const namespacet &) const final override
170  {
171  output(out);
172  }
173 
174  void make_top() final override
175  {
176  values.clear();
177  if(bv_container)
178  bv_container->clear();
179  has_values=tvt(true);
180  }
181 
182  void make_bottom() final override
183  {
184  values.clear();
185  if(bv_container)
186  bv_container->clear();
187  has_values=tvt(false);
188  }
189 
190  void make_entry() final override
191  {
192  make_top();
193  }
194 
195  bool is_top() const override final
196  {
197  DATA_INVARIANT(!has_values.is_true() || values.empty(),
198  "If domain is top, the value map must be empty");
199  return has_values.is_true();
200  }
201 
202  bool is_bottom() const override final
203  {
205  "If domain is bottom, the value map must be empty");
206  return has_values.is_false();
207  }
208 
221  bool merge(const rd_range_domaint &other, trace_ptrt from, trace_ptrt to);
222 
223  bool merge_shared(
224  const rd_range_domaint &other,
225  locationt from,
226  locationt to,
227  const namespacet &ns);
228 
229  // each element x represents a range of bits [x.first, x.second)
230  typedef std::multimap<range_spect, range_spect> rangest;
231  typedef std::map<locationt, rangest> ranges_at_loct;
232 
233  const ranges_at_loct &get(const irep_idt &identifier) const;
234  void clear_cache(const irep_idt &identifier) const
235  {
236  export_cache[identifier].clear();
237  }
238 
239 private:
244 
253 
254  typedef std::set<std::size_t> values_innert;
255  #ifdef USE_DSTRING
256  typedef std::map<irep_idt, values_innert> valuest;
257  #else
258  typedef std::unordered_map<irep_idt, values_innert> valuest;
259  #endif
260  valuest values;
266 
267  #ifdef USE_DSTRING
268  typedef std::map<irep_idt, ranges_at_loct> export_cachet;
269  #else
270  typedef std::unordered_map<irep_idt, ranges_at_loct> export_cachet;
271  #endif
272  mutable export_cachet export_cache;
284 
285  void populate_cache(const irep_idt &identifier) const;
286 
287  void transform_dead(
288  const namespacet &ns,
289  locationt from);
291  const namespacet &ns,
294  const namespacet &ns,
295  const irep_idt &function_from,
296  locationt from,
297  const irep_idt &function_to,
300  const namespacet &ns,
301  const irep_idt &function_from,
302  locationt from,
303  const irep_idt &function_to,
304  locationt to,
306  void transform_assign(
307  const namespacet &ns,
308  locationt from,
309  const irep_idt &function_to,
310  locationt to,
312 
313  void kill(
314  const irep_idt &identifier,
315  const range_spect &range_start,
316  const range_spect &range_end);
317  void kill_inf(
318  const irep_idt &identifier,
319  const range_spect &range_start);
320  bool gen(
321  locationt from,
322  const irep_idt &identifier,
323  const range_spect &range_start,
324  const range_spect &range_end);
325 
326  void output(std::ostream &out) const;
327 
328  bool merge_inner(
329  values_innert &dest,
330  const values_innert &other);
331 };
332 
334  public concurrency_aware_ait<rd_range_domaint>,
335  public sparse_bitvector_analysist<reaching_definitiont>
336 {
337 public:
338  // constructor
339  explicit reaching_definitions_analysist(const namespacet &_ns);
340 
342 
343  void initialize(const goto_functionst &goto_functions) override;
344 
346  {
347  assert(value_sets);
348  return *value_sets;
349  }
350 
352  {
353  assert(is_threaded);
354  return *is_threaded;
355  }
356 
357  const dirtyt &get_is_dirty() const
358  {
359  assert(is_dirty);
360  return *is_dirty;
361  }
362 
363 protected:
364  const namespacet &ns;
365  std::unique_ptr<value_setst> value_sets;
366  std::unique_ptr<is_threadedt> is_threaded;
367  std::unique_ptr<dirtyt> is_dirty;
368 };
369 
370 #endif // CPROVER_ANALYSES_REACHING_DEFINITIONS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
rd_range_domaint::is_top
bool is_top() const override final
Definition: reaching_definitions.h:195
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:265
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:676
sparse_bitvector_analysist< reaching_definitiont >::inner_mapt
std::map< reaching_definitiont, std::size_t > inner_mapt
Definition: reaching_definitions.h:72
reaching_definitions_analysist::reaching_definitions_analysist
reaching_definitions_analysist(const namespacet &_ns)
Definition: reaching_definitions.cpp:53
dirtyt
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:27
reaching_definitions_analysist::get_value_sets
value_setst & get_value_sets() const
Definition: reaching_definitions.h:345
threeval.h
sparse_bitvector_analysist
An instance of this class provides an assignment of unique numeric ID to each inserted reaching_defin...
Definition: reaching_definitions.h:44
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:338
sparse_bitvector_analysist::value_map
std::unordered_map< irep_idt, inner_mapt > value_map
A map from names of program variables to a set of pairs (reaching_definitiont, ID).
Definition: reaching_definitions.h:81
rd_range_domaint::ranges_at_loct
std::map< locationt, rangest > ranges_at_loct
Definition: reaching_definitions.h:231
reaching_definitions_analysist::get_is_threaded
const is_threadedt & get_is_threaded() const
Definition: reaching_definitions.h:351
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:254
rd_range_domaint::has_values
tvt has_values
This (three value logic) flag determines, whether the instance represents top, bottom,...
Definition: reaching_definitions.h:243
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:252
rd_range_domaint::make_bottom
void make_bottom() final override
no states
Definition: reaching_definitions.h:182
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:761
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
reaching_definitions_analysist
Definition: reaching_definitions.h:336
goto_rw.h
is_threadedt
Definition: is_threaded.h:22
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:208
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
base_exceptions.h
Generic exception types primarily designed for use with invariants.
reaching_definitions_analysist::is_threaded
std::unique_ptr< is_threadedt > is_threaded
Definition: reaching_definitions.h:366
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
reaching_definitiont::identifier
irep_idt identifier
The name of the variable which was defined.
Definition: reaching_definitions.h:89
rd_range_domaint::is_bottom
bool is_bottom() const override final
Definition: reaching_definitions.h:202
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
sparse_bitvector_analysist::clear
void clear()
Definition: reaching_definitions.h:65
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
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:514
operator<
bool operator<(const reaching_definitiont &a, const reaching_definitiont &b)
In order to use instances of this structure as keys in ordered containers, such as std::map,...
Definition: reaching_definitions.h:104
rd_range_domaint::export_cachet
std::map< irep_idt, ranges_at_loct > export_cachet
Definition: reaching_definitions.h:268
ai.h
Abstract Interpretation.
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:230
tvt
Definition: threeval.h:20
rd_range_domaint::merge_inner
bool merge_inner(values_innert &dest, const values_innert &other)
Definition: reaching_definitions.cpp:626
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()
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:77
value_setst
Definition: value_sets.h:22
rd_range_domaint::make_entry
void make_entry() final override
Make this domain a reasonable entry-point state.
Definition: reaching_definitions.h:190
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:357
rd_range_domaint::make_top
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
Definition: reaching_definitions.h:174
rd_range_domaint::merge_shared
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
Definition: reaching_definitions.cpp:712
concurrency_aware_ait
Base class for concurrency-aware abstract interpretation.
Definition: ai.h:643
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
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:776
rd_range_domaint::rd_range_domaint
rd_range_domaint(sparse_bitvector_analysist< reaching_definitiont > *_bv_container)
Definition: reaching_definitions.h:139
reaching_definitiont::bit_end
range_spect bit_end
Definition: reaching_definitions.h:99
rd_range_domaint::export_cache
export_cachet export_cache
It is a helper data structure.
Definition: reaching_definitions.h:283
rd_range_domaint::kill_inf
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
Definition: reaching_definitions.cpp:476
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:364
rd_range_domaint::kill
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: reaching_definitions.cpp:376
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:269
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
reaching_definitions_analysist::is_dirty
std::unique_ptr< dirtyt > is_dirty
Definition: reaching_definitions.h:367
rd_range_domaint::clear_cache
void clear_cache(const irep_idt &identifier) const
Definition: reaching_definitions.h:234
rd_range_domaint::valuest
std::map< irep_idt, values_innert > valuest
Definition: reaching_definitions.h:256
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:365
tvt::is_true
bool is_true() const
Definition: threeval.h:25