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  locationt from,
161  const irep_idt &function_to,
162  locationt 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(
222  const rd_range_domaint &other,
223  locationt from,
224  locationt to);
225 
226  bool merge_shared(
227  const rd_range_domaint &other,
228  locationt from,
229  locationt to,
230  const namespacet &ns);
231 
232  // each element x represents a range of bits [x.first, x.second)
233  typedef std::multimap<range_spect, range_spect> rangest;
234  typedef std::map<locationt, rangest> ranges_at_loct;
235 
236  const ranges_at_loct &get(const irep_idt &identifier) const;
237  void clear_cache(const irep_idt &identifier) const
238  {
239  export_cache[identifier].clear();
240  }
241 
242 private:
247 
256 
257  typedef std::set<std::size_t> values_innert;
258  #ifdef USE_DSTRING
259  typedef std::map<irep_idt, values_innert> valuest;
260  #else
261  typedef std::unordered_map<irep_idt, values_innert> valuest;
262  #endif
263  valuest values;
269 
270  #ifdef USE_DSTRING
271  typedef std::map<irep_idt, ranges_at_loct> export_cachet;
272  #else
273  typedef std::unordered_map<irep_idt, ranges_at_loct> export_cachet;
274  #endif
275  mutable export_cachet export_cache;
287 
288  void populate_cache(const irep_idt &identifier) const;
289 
290  void transform_dead(
291  const namespacet &ns,
292  locationt from);
294  const namespacet &ns,
297  const namespacet &ns,
298  const irep_idt &function_from,
299  locationt from,
300  const irep_idt &function_to,
303  const namespacet &ns,
304  const irep_idt &function_from,
305  locationt from,
306  const irep_idt &function_to,
307  locationt to,
309  void transform_assign(
310  const namespacet &ns,
311  locationt from,
312  const irep_idt &function_to,
313  locationt to,
315 
316  void kill(
317  const irep_idt &identifier,
318  const range_spect &range_start,
319  const range_spect &range_end);
320  void kill_inf(
321  const irep_idt &identifier,
322  const range_spect &range_start);
323  bool gen(
324  locationt from,
325  const irep_idt &identifier,
326  const range_spect &range_start,
327  const range_spect &range_end);
328 
329  void output(std::ostream &out) const;
330 
331  bool merge_inner(
332  values_innert &dest,
333  const values_innert &other);
334 };
335 
337  public concurrency_aware_ait<rd_range_domaint>,
338  public sparse_bitvector_analysist<reaching_definitiont>
339 {
340 public:
341  // constructor
342  explicit reaching_definitions_analysist(const namespacet &_ns);
343 
345 
346  void initialize(const goto_functionst &goto_functions) override;
347 
349  {
350  assert(value_sets);
351  return *value_sets;
352  }
353 
355  {
356  assert(is_threaded);
357  return *is_threaded;
358  }
359 
360  const dirtyt &get_is_dirty() const
361  {
362  assert(is_dirty);
363  return *is_dirty;
364  }
365 
366 protected:
367  const namespacet &ns;
368  std::unique_ptr<value_setst> value_sets;
369  std::unique_ptr<is_threadedt> is_threaded;
370  std::unique_ptr<dirtyt> is_dirty;
371 };
372 
373 #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:268
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
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:348
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:334
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:234
reaching_definitions_analysist::get_is_threaded
const is_threadedt & get_is_threaded() const
Definition: reaching_definitions.h:354
sparse_bitvector_analysist::values
std::vector< typename inner_mapt::const_iterator > values
It is a map from an ID to the corresponding reaching_definitiont instance inside the map value_map.
Definition: reaching_definitions.h:77
rd_range_domaint::values_innert
std::set< std::size_t > values_innert
Definition: reaching_definitions.h:257
rd_range_domaint::has_values
tvt has_values
This (three value logic) flag determines, whether the instance represents top, bottom,...
Definition: reaching_definitions.h:246
rd_range_domaint::merge
bool merge(const rd_range_domaint &other, locationt from, locationt to)
Implements the join operation of two instances *this and other.
Definition: reaching_definitions.cpp:672
rd_range_domaint::bv_container
sparse_bitvector_analysist< reaching_definitiont > *const bv_container
It points to the actual reaching definitions data of individual program variables.
Definition: reaching_definitions.h:255
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:757
reaching_definitions_analysist
Definition: reaching_definitions.h:339
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:204
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:369
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
rd_range_domaint::transform
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
Computes an instance obtained from the instance *this by transformation over a GOTO instruction refer...
Definition: reaching_definitions.cpp:91
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::gen
bool gen(locationt from, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
A utility function which updates internal data structures by inserting a new reaching definition reco...
Definition: reaching_definitions.cpp:509
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:271
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:233
tvt
Definition: threeval.h:20
rd_range_domaint::merge_inner
bool merge_inner(values_innert &dest, const values_innert &other)
Definition: reaching_definitions.cpp:621
rd_range_domaint::transform_dead
void transform_dead(const namespacet &ns, locationt from)
Computes an instance obtained from a *this by transformation over DEAD v GOTO instruction.
Definition: reaching_definitions.cpp:164
range_spect
int range_spect
Definition: goto_rw.h:65
reaching_definitions_analysist::~reaching_definitions_analysist
virtual ~reaching_definitions_analysist()
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
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:179
reaching_definitions_analysist::get_is_dirty
const dirtyt & get_is_dirty() const
Definition: reaching_definitions.h:360
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:708
concurrency_aware_ait
Base class for concurrency-aware abstract interpretation.
Definition: ai.h:642
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
reaching_definitions_analysist::initialize
void initialize(const goto_functionst &goto_functions) override
Initialize all the abstract states for a whole program.
Definition: reaching_definitions.cpp:772
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:286
rd_range_domaint::kill_inf
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
Definition: reaching_definitions.cpp:471
reaching_definitiont
Identifies a GOTO instruction where a given variable is defined (i.e.
Definition: reaching_definitions.h:87
reaching_definitions_analysist::ns
const namespacet & ns
Definition: reaching_definitions.h:367
rd_range_domaint::kill
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: reaching_definitions.cpp:371
rd_range_domaint::output
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
Definition: reaching_definitions.h:166
rd_range_domaint::transform_end_function
void transform_end_function(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, reaching_definitions_analysist &rd)
Definition: reaching_definitions.cpp:265
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
reaching_definitions_analysist::is_dirty
std::unique_ptr< dirtyt > is_dirty
Definition: reaching_definitions.h:370
rd_range_domaint::clear_cache
void clear_cache(const irep_idt &identifier) const
Definition: reaching_definitions.h:237
rd_range_domaint::valuest
std::map< irep_idt, values_innert > valuest
Definition: reaching_definitions.h:259
sparse_bitvector_analysist::get
const V & get(const std::size_t value_index) const
Definition: reaching_definitions.h:46
reaching_definitions_analysist::value_sets
std::unique_ptr< value_setst > value_sets
Definition: reaching_definitions.h:368
tvt::is_true
bool is_true() const
Definition: threeval.h:25