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 
15 
16 #ifndef CPROVER_ANALYSES_REACHING_DEFINITIONS_H
17 #define CPROVER_ANALYSES_REACHING_DEFINITIONS_H
18 
19 #include <util/base_exceptions.h>
20 #include <util/threeval.h>
21 
22 #include "ai.h"
23 #include "goto_rw.h"
24 
25 class value_setst;
26 class is_threadedt;
27 class dirtyt;
29 
30 // requirement: V has a member "identifier" of type irep_idt
31 template<typename V>
33 {
34 public:
35  const V &get(const std::size_t value_index) const
36  {
37  assert(value_index<values.size());
38  return values[value_index]->first;
39  }
40 
41  std::size_t add(const V &value)
42  {
43  inner_mapt &m=value_map[value.identifier];
44 
45  std::pair<typename inner_mapt::iterator, bool> entry=
46  m.insert(std::make_pair(value, values.size()));
47 
48  if(entry.second)
49  values.push_back(entry.first);
50 
51  return entry.first->second;
52  }
53 
54  void clear()
55  {
56  value_map.clear();
57  values.clear();
58  }
59 
60 protected:
61  typedef typename std::map<V, std::size_t> inner_mapt;
62  std::vector<typename inner_mapt::const_iterator> values;
63  std::unordered_map<irep_idt, inner_mapt> value_map;
64 };
65 
67 {
72 };
73 
74 inline bool operator<(
75  const reaching_definitiont &a,
76  const reaching_definitiont &b)
77 {
79  return true;
81  return false;
82 
83  if(a.bit_begin<b.bit_begin)
84  return true;
85  if(b.bit_begin<a.bit_begin)
86  return false;
87 
88  if(a.bit_end<b.bit_end)
89  return true;
90  if(b.bit_end<a.bit_end)
91  return false;
92 
93  // we do not expect comparison of unrelated definitions
94  // as this operator< is only used in sparse_bitvector_analysist
95  assert(a.identifier==b.identifier);
96 
97  return false;
98 }
99 
101 {
102 public:
104  ai_domain_baset(),
105  has_values(false),
106  bv_container(nullptr)
107  {
108  }
109 
112  {
113  bv_container=&_bv_container;
114  }
115 
116  void
117  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
118  final override;
119 
120  void output(
121  std::ostream &out,
122  const ai_baset &ai,
123  const namespacet &ns) const final override
124  {
125  output(out);
126  }
127 
128  void make_top() final override
129  {
130  values.clear();
131  if(bv_container)
132  bv_container->clear();
133  has_values=tvt(true);
134  }
135 
136  void make_bottom() final override
137  {
138  values.clear();
139  if(bv_container)
140  bv_container->clear();
141  has_values=tvt(false);
142  }
143 
144  void make_entry() final override
145  {
146  make_top();
147  }
148 
149  bool is_top() const override final
150  {
151  DATA_INVARIANT(!has_values.is_true() || values.empty(),
152  "If domain is top, the value map must be empty");
153  return has_values.is_true();
154  }
155 
156  bool is_bottom() const override final
157  {
159  "If domain is bottom, the value map must be empty");
160  return has_values.is_false();
161  }
162 
163  // returns true iff there is something new
164  bool merge(
165  const rd_range_domaint &other,
166  locationt from,
167  locationt to);
168 
169  bool merge_shared(
170  const rd_range_domaint &other,
171  locationt from,
172  locationt to,
173  const namespacet &ns);
174 
175  // each element x represents a range of bits [x.first, x.second)
176  typedef std::multimap<range_spect, range_spect> rangest;
177  typedef std::map<locationt, rangest> ranges_at_loct;
178 
179  const ranges_at_loct &get(const irep_idt &identifier) const;
180  void clear_cache(const irep_idt &identifier) const
181  {
182  export_cache[identifier].clear();
183  }
184 
185 private:
187 
189 
190  typedef std::set<std::size_t> values_innert;
191  #ifdef USE_DSTRING
192  typedef std::map<irep_idt, values_innert> valuest;
193  #else
194  typedef std::unordered_map<irep_idt, values_innert> valuest;
195  #endif
197 
198  #ifdef USE_DSTRING
199  typedef std::map<irep_idt, ranges_at_loct> export_cachet;
200  #else
201  typedef std::unordered_map<irep_idt, ranges_at_loct> export_cachet;
202  #endif
204 
205  void populate_cache(const irep_idt &identifier) const;
206 
207  void transform_dead(
208  const namespacet &ns,
209  locationt from);
211  const namespacet &ns,
214  const namespacet &ns,
215  locationt from,
216  locationt to,
219  const namespacet &ns,
220  locationt from,
221  locationt to,
223  void transform_assign(
224  const namespacet &ns,
225  locationt from,
226  locationt to,
228 
229  void kill(
230  const irep_idt &identifier,
231  const range_spect &range_start,
232  const range_spect &range_end);
233  void kill_inf(
234  const irep_idt &identifier,
235  const range_spect &range_start);
236  bool gen(
237  locationt from,
238  const irep_idt &identifier,
239  const range_spect &range_start,
240  const range_spect &range_end);
241 
242  void output(std::ostream &out) const;
243 
244  bool merge_inner(
245  values_innert &dest,
246  const values_innert &other);
247 };
248 
250  public concurrency_aware_ait<rd_range_domaint>,
251  public sparse_bitvector_analysist<reaching_definitiont>
252 {
253 public:
254  // constructor
255  explicit reaching_definitions_analysist(const namespacet &_ns);
256 
258 
259  virtual void initialize(
260  const goto_functionst &goto_functions) override;
261 
263  {
265 
266  rd_range_domaint *rd_state=dynamic_cast<rd_range_domaint*>(&s);
268  rd_state!=nullptr,
270  "rd_state has type rd_range_domaint");
271 
272  rd_state->set_bitvector_container(*this);
273 
274  return s;
275  }
276 
278  {
279  assert(value_sets);
280  return *value_sets;
281  }
282 
284  {
285  assert(is_threaded);
286  return *is_threaded;
287  }
288 
289  const dirtyt &get_is_dirty() const
290  {
291  assert(is_dirty);
292  return *is_dirty;
293  }
294 
295 protected:
296  const namespacet &ns;
297  std::unique_ptr<value_setst> value_sets;
298  std::unique_ptr<is_threadedt> is_threaded;
299  std::unique_ptr<dirtyt> is_dirty;
300 };
301 
302 #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:213
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final override
virtual void initialize(const goto_functionst &goto_functions) override
virtual statet & get_state(locationt l) override
Definition: ai.h:424
void clear_cache(const irep_idt &identifier) const
void transform_function_call(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
ai_domain_baset::locationt definition_at
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
virtual statet & get_state(goto_programt::const_targett l) override
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
bool merge_inner(values_innert &dest, const values_innert &other)
sparse_bitvector_analysist< reaching_definitiont > * bv_container
bool is_top() const override final
void make_bottom() final override
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
void populate_cache(const irep_idt &identifier) const
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)
Definition: threeval.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
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 transform_dead(const namespacet &ns, locationt from)
std::map< reaching_definitiont, std::size_t > inner_mapt
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
bool is_true() const
Definition: threeval.h:25
bool operator<(const reaching_definitiont &a, const reaching_definitiont &b)
std::vector< typename inner_mapt::const_iterator > values
bool is_bottom() const override final
bool merge(const rd_range_domaint &other, locationt from, locationt to)
Abstract Interpretation.
Definition: ai.h:128
Definition: dirty.h:23
export_cachet export_cache
void make_top() final override
reaching_definitions_analysist(const namespacet &_ns)
std::size_t add(const V &value)
goto_programt::const_targett locationt
Definition: ai.h:44
std::multimap< range_spect, range_spect > rangest
void transform_assign(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
void transform_end_function(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
std::unordered_map< irep_idt, inner_mapt > value_map
std::unique_ptr< is_threadedt > is_threaded
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
void make_entry() final override
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