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:
140  ai_domain_baset(),
141  has_values(false),
142  bv_container(nullptr)
143  {
144  }
145 
148  {
149  bv_container=&_bv_container;
150  }
151 
164  void transform(
165  const irep_idt &function_from,
166  locationt from,
167  const irep_idt &function_to,
168  locationt to,
169  ai_baset &ai,
170  const namespacet &ns) final override;
171 
172  void output(
173  std::ostream &out,
174  const ai_baset &,
175  const namespacet &) const final override
176  {
177  output(out);
178  }
179 
180  void make_top() final override
181  {
182  values.clear();
183  if(bv_container)
184  bv_container->clear();
185  has_values=tvt(true);
186  }
187 
188  void make_bottom() final override
189  {
190  values.clear();
191  if(bv_container)
192  bv_container->clear();
193  has_values=tvt(false);
194  }
195 
196  void make_entry() final override
197  {
198  make_top();
199  }
200 
201  bool is_top() const override final
202  {
203  DATA_INVARIANT(!has_values.is_true() || values.empty(),
204  "If domain is top, the value map must be empty");
205  return has_values.is_true();
206  }
207 
208  bool is_bottom() const override final
209  {
211  "If domain is bottom, the value map must be empty");
212  return has_values.is_false();
213  }
214 
227  bool merge(
228  const rd_range_domaint &other,
229  locationt from,
230  locationt to);
231 
232  bool merge_shared(
233  const rd_range_domaint &other,
234  locationt from,
235  locationt to,
236  const namespacet &ns);
237 
238  // each element x represents a range of bits [x.first, x.second)
239  typedef std::multimap<range_spect, range_spect> rangest;
240  typedef std::map<locationt, rangest> ranges_at_loct;
241 
242  const ranges_at_loct &get(const irep_idt &identifier) const;
243  void clear_cache(const irep_idt &identifier) const
244  {
245  export_cache[identifier].clear();
246  }
247 
248 private:
253 
262 
263  typedef std::set<std::size_t> values_innert;
264  #ifdef USE_DSTRING
265  typedef std::map<irep_idt, values_innert> valuest;
266  #else
267  typedef std::unordered_map<irep_idt, values_innert> valuest;
268  #endif
269  valuest values;
275 
276  #ifdef USE_DSTRING
277  typedef std::map<irep_idt, ranges_at_loct> export_cachet;
278  #else
279  typedef std::unordered_map<irep_idt, ranges_at_loct> export_cachet;
280  #endif
281  mutable export_cachet export_cache;
293 
294  void populate_cache(const irep_idt &identifier) const;
295 
296  void transform_dead(
297  const namespacet &ns,
298  locationt from);
300  const namespacet &ns,
303  const namespacet &ns,
304  const irep_idt &function_from,
305  locationt from,
306  const irep_idt &function_to,
309  const namespacet &ns,
310  const irep_idt &function_from,
311  locationt from,
312  locationt to,
314  void transform_assign(
315  const namespacet &ns,
316  locationt from,
317  locationt to,
319 
320  void kill(
321  const irep_idt &identifier,
322  const range_spect &range_start,
323  const range_spect &range_end);
324  void kill_inf(
325  const irep_idt &identifier,
326  const range_spect &range_start);
327  bool gen(
328  locationt from,
329  const irep_idt &identifier,
330  const range_spect &range_start,
331  const range_spect &range_end);
332 
333  void output(std::ostream &out) const;
334 
335  bool merge_inner(
336  values_innert &dest,
337  const values_innert &other);
338 };
339 
341  public concurrency_aware_ait<rd_range_domaint>,
342  public sparse_bitvector_analysist<reaching_definitiont>
343 {
344 public:
345  // constructor
346  explicit reaching_definitions_analysist(const namespacet &_ns);
347 
349 
350  void initialize(const goto_functionst &goto_functions) override;
351 
353  {
355 
356  rd_range_domaint *rd_state=dynamic_cast<rd_range_domaint*>(&s);
358  rd_state!=nullptr,
360  "rd_state has type rd_range_domaint");
361 
362  rd_state->set_bitvector_container(*this);
363 
364  return s;
365  }
366 
368  {
369  assert(value_sets);
370  return *value_sets;
371  }
372 
374  {
375  assert(is_threaded);
376  return *is_threaded;
377  }
378 
379  const dirtyt &get_is_dirty() const
380  {
381  assert(is_dirty);
382  return *is_dirty;
383  }
384 
385 protected:
386  const namespacet &ns;
387  std::unique_ptr<value_setst> value_sets;
388  std::unique_ptr<is_threadedt> is_threaded;
389  std::unique_ptr<dirtyt> is_dirty;
390 };
391 
392 #endif // CPROVER_ANALYSES_REACHING_DEFINITIONS_H
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
bool is_false() const
Definition: threeval.h:26
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:382
void initialize(const goto_functionst &goto_functions) override
Initialize all the abstract states for a whole program.
void transform_end_function(const namespacet &ns, const irep_idt &function_from, locationt from, locationt to, reaching_definitions_analysist &rd)
virtual 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: ai.h:419
void clear_cache(const irep_idt &identifier) const
goto_programt::const_targett locationt
Definition: ai.h:36
ai_domain_baset::locationt definition_at
The iterator to the GOTO instruction where the variable has been written to.
std::unordered_map< irep_idt, ranges_at_loct > export_cachet
int range_spect
Definition: goto_rw.h:61
std::unique_ptr< dirtyt > is_dirty
const dirtyt & get_is_dirty() const
bool merge_inner(values_innert &dest, const values_innert &other)
Identifies a GOTO instruction where a given variable is defined (i.e.
range_spect bit_begin
The two integers below define a range of bits (i.e.
sparse_bitvector_analysist< reaching_definitiont > * bv_container
It points to the actual reaching definitions data of individual program variables.
statet & get_state(locationt l) override
Get the state for the given location, creating it in a default way if it doesn't exist.
An instance of this class provides an assignment of unique numeric ID to each inserted reaching_defin...
void transform_function_call(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, reaching_definitions_analysist &rd)
bool is_top() const override final
irep_idt identifier
The name of the variable which was defined.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
void make_bottom() final override
no states
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
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...
std::unordered_map< irep_idt, values_innert > valuest
void set_bitvector_container(sparse_bitvector_analysist< reaching_definitiont > &_bv_container)
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: threeval.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
std::unique_ptr< value_setst > value_sets
value_setst & get_value_sets() const
void transform_start_thread(const namespacet &ns, reaching_definitions_analysist &rd)
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
A collection of goto functions.
Because the class is inherited from ai_domain_baset, its instance represents an element of a domain o...
void transform_dead(const namespacet &ns, locationt from)
Computes an instance obtained from a *this by transformation over DEAD v GOTO instruction.
std::map< reaching_definitiont, std::size_t > inner_mapt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
tvt has_values
This (three value logic) flag determines, whether the instance represents top, bottom,...
bool is_true() const
Definition: threeval.h:25
valuest values
It is an ordered map from program variable names to IDs of reaching_definitiont instances stored in m...
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,...
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.
bool is_bottom() const override final
const V & get(const std::size_t value_index) const
bool merge(const rd_range_domaint &other, locationt from, locationt to)
Implements the join operation of two instances *this and other.
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
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: dirty.h:23
export_cachet export_cache
It is a helper data structure.
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
reaching_definitions_analysist(const namespacet &_ns)
std::size_t add(const V &value)
goto_programt::const_targett locationt
Definition: ai_domain.h:40
std::multimap< range_spect, range_spect > rangest
void transform_assign(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
std::unordered_map< irep_idt, inner_mapt > value_map
A map from names of program variables to a set of pairs (reaching_definitiont, ID).
std::unique_ptr< is_threadedt > is_threaded
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
void make_entry() final override
Make this domain a reasonable entry-point state.
std::map< locationt, rangest > ranges_at_loct
Generic exception types primarily designed for use with invariants.
std::set< std::size_t > values_innert
const is_threadedt & get_is_threaded() const
const ranges_at_loct & get(const irep_idt &identifier) const