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, irep_id_hash> 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 transform(
117  locationt from,
118  locationt to,
119  ai_baset &ai,
120  const namespacet &ns) final;
121 
122  void output(
123  std::ostream &out,
124  const ai_baset &ai,
125  const namespacet &ns) const final
126  {
127  output(out);
128  }
129 
130  void make_top() final
131  {
132  values.clear();
133  if(bv_container)
134  bv_container->clear();
135  has_values=tvt(true);
136  }
137 
138  void make_bottom() final
139  {
140  values.clear();
141  if(bv_container)
142  bv_container->clear();
143  has_values=tvt(false);
144  }
145 
146  void make_entry() final
147  {
148  make_top();
149  }
150 
151  // returns true iff there is something new
152  bool merge(
153  const rd_range_domaint &other,
154  locationt from,
155  locationt to);
156 
157  bool merge_shared(
158  const rd_range_domaint &other,
159  locationt from,
160  locationt to,
161  const namespacet &ns);
162 
163  // each element x represents a range of bits [x.first, x.second)
164  typedef std::multimap<range_spect, range_spect> rangest;
165  typedef std::map<locationt, rangest> ranges_at_loct;
166 
167  const ranges_at_loct &get(const irep_idt &identifier) const;
168  void clear_cache(const irep_idt &identifier) const
169  {
170  export_cache[identifier].clear();
171  }
172 
173 private:
175 
177 
178  typedef std::set<std::size_t> values_innert;
179  #ifdef USE_DSTRING
180  typedef std::map<irep_idt, values_innert> valuest;
181  #else
182  typedef std::unordered_map<irep_idt, values_innert, irep_id_hash> valuest;
183  #endif
184  valuest values;
185 
186  #ifdef USE_DSTRING
187  typedef std::map<irep_idt, ranges_at_loct> export_cachet;
188  #else
189  typedef std::unordered_map<irep_idt, ranges_at_loct, irep_id_hash>
191  #endif
192  mutable export_cachet export_cache;
193 
194  void populate_cache(const irep_idt &identifier) const;
195 
196  void transform_dead(
197  const namespacet &ns,
198  locationt from);
199  void transform_start_thread(
200  const namespacet &ns,
202  void transform_function_call(
203  const namespacet &ns,
204  locationt from,
205  locationt to,
207  void transform_end_function(
208  const namespacet &ns,
209  locationt from,
210  locationt to,
212  void transform_assign(
213  const namespacet &ns,
214  locationt from,
215  locationt to,
217 
218  void kill(
219  const irep_idt &identifier,
220  const range_spect &range_start,
221  const range_spect &range_end);
222  void kill_inf(
223  const irep_idt &identifier,
224  const range_spect &range_start);
225  bool gen(
226  locationt from,
227  const irep_idt &identifier,
228  const range_spect &range_start,
229  const range_spect &range_end);
230 
231  void output(std::ostream &out) const;
232 
233  bool merge_inner(
234  values_innert &dest,
235  const values_innert &other);
236 };
237 
239  public concurrency_aware_ait<rd_range_domaint>,
240  public sparse_bitvector_analysist<reaching_definitiont>
241 {
242 public:
243  // constructor
246  ns(_ns),
247  value_sets(nullptr),
248  is_threaded(nullptr),
249  is_dirty(nullptr)
250  {
251  }
252 
254 
255  virtual void initialize(
256  const goto_functionst &goto_functions);
257 
259  {
261 
262  rd_range_domaint *rd_state=dynamic_cast<rd_range_domaint*>(&s);
264  rd_state!=nullptr,
266  "rd_state has type rd_range_domaint");
267 
268  rd_state->set_bitvector_container(*this);
269 
270  return s;
271  }
272 
274  {
275  assert(value_sets);
276  return *value_sets;
277  }
278 
280  {
281  assert(is_threaded);
282  return *is_threaded;
283  }
284 
285  const dirtyt &get_is_dirty() const
286  {
287  assert(is_dirty);
288  return *is_dirty;
289  }
290 
291 protected:
292  const namespacet &ns;
296 };
297 
298 #endif // CPROVER_ANALYSES_REACHING_DEFINITIONS_H
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:209
virtual statet & get_state(locationt l) override
Definition: ai.h:381
void clear_cache(const irep_idt &identifier) const
ai_domain_baset::locationt definition_at
std::unordered_map< irep_idt, values_innert, irep_id_hash > valuest
int range_spect
Definition: goto_rw.h:52
const dirtyt & get_is_dirty() const
sparse_bitvector_analysist< reaching_definitiont > * bv_container
std::unordered_map< irep_idt, inner_mapt, irep_id_hash > value_map
instructionst::const_iterator const_targett
void set_bitvector_container(sparse_bitvector_analysist< reaching_definitiont > &_bv_container)
Definition: threeval.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:62
value_setst & get_value_sets() const
std::map< reaching_definitiont, std::size_t > inner_mapt
bool operator<(const reaching_definitiont &a, const reaching_definitiont &b)
std::unordered_map< irep_idt, ranges_at_loct, irep_id_hash > export_cachet
std::vector< typename inner_mapt::const_iterator > values
virtual statet & get_state(goto_programt::const_targett l)
Abstract Interpretation.
Definition: ai.h:108
Definition: dirty.h:22
export_cachet export_cache
reaching_definitions_analysist(const namespacet &_ns)
std::size_t add(const V &value)
goto_programt::const_targett locationt
Definition: ai.h:42
std::multimap< range_spect, range_spect > rangest
std::map< locationt, rangest > ranges_at_loct
Generic exception types primarily designed for use with invariants.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
std::set< std::size_t > values_innert
const is_threadedt & get_is_threaded() const