cprover
Loading...
Searching...
No Matches
reaching_definitions.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Range-based reaching definitions analysis (following Field-
4 Sensitive Program Dependence Analysis, Litvak et al., FSE 2010)
5
6Author: Michael Tautschnig
7
8Date: 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
33class value_setst;
34class is_threadedt;
35class dirtyt;
37
41template<typename V>
43{
44public:
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
70protected:
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
103inline 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{
137public:
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)
178 has_values=tvt(true);
179 }
180
181 void make_bottom() final override
182 {
183 values.clear();
184 if(bv_container)
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 {
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
238private:
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{
336public:
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
362protected:
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
std::unique_ptr< is_threadedt > is_threaded
const is_threadedt & get_is_threaded() const
std::unique_ptr< dirtyt > is_dirty
std::unique_ptr< value_setst > value_sets
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.