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