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 {
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 {
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
110
113inline bool operator<(
114 const reaching_definitiont &a,
115 const reaching_definitiont &b)
116{
117 if(goto_programt::target_less_than()(a.definition_at, b.definition_at))
118 return true;
119 if(goto_programt::target_less_than()(b.definition_at, a.definition_at))
120 return false;
121
122 if(a.bit_begin.is_unknown() != b.bit_begin.is_unknown())
123 return a.bit_begin.is_unknown();
124
125 if(!a.bit_begin.is_unknown())
126 {
127 if(a.bit_begin < b.bit_begin)
128 return true;
129 if(b.bit_begin < a.bit_begin)
130 return false;
131 }
132
133 if(a.bit_end.is_unknown() != b.bit_end.is_unknown())
134 return a.bit_end.is_unknown();
135
136 if(!a.bit_end.is_unknown())
137 {
138 if(a.bit_end < b.bit_end)
139 return true;
140 if(b.bit_end < a.bit_end)
141 return false;
142 }
143
144 // we do not expect comparison of unrelated definitions
145 // as this operator< is only used in sparse_bitvector_analysist
146 INVARIANT(
147 a.identifier == b.identifier, "comparison of unrelated definitions");
148
149 return false;
150}
151
159{
160public:
167
180 void transform(
181 const irep_idt &function_from,
183 const irep_idt &function_to,
185 ai_baset &ai,
186 const namespacet &ns) final override;
187
188 void output(
189 std::ostream &out,
190 const ai_baset &,
191 const namespacet &) const final override
192 {
193 output(out);
194 }
195
196 void make_top() final override
197 {
198 values.clear();
199 if(bv_container)
201 has_values=tvt(true);
202 }
203
204 void make_bottom() final override
205 {
206 values.clear();
207 if(bv_container)
209 has_values=tvt(false);
210 }
211
212 bool is_top() const override final
213 {
215 "If domain is top, the value map must be empty");
216 return has_values.is_true();
217 }
218
220 {
222 "If domain is bottom, the value map must be empty");
223 return has_values.is_false();
224 }
225
238 bool merge(const rd_range_domaint &other, trace_ptrt from, trace_ptrt to);
239
240 bool merge_shared(
241 const rd_range_domaint &other,
244 const namespacet &ns);
245
246 // each element x represents a range of bits [x.first, x.second)
247 typedef std::multimap<range_spect, range_spect> rangest;
248 typedef std::map<locationt, rangest, goto_programt::target_less_than>
250
251 const ranges_at_loct &get(const irep_idt &identifier) const;
252 void clear_cache(const irep_idt &identifier) const
253 {
254 export_cache[identifier].clear();
255 }
256
257private:
262
271
272 typedef std::set<std::size_t> values_innert;
273 #ifdef USE_DSTRING
274 typedef std::map<irep_idt, values_innert> valuest;
275 #else
276 typedef std::unordered_map<irep_idt, values_innert> valuest;
277 #endif
284
285 #ifdef USE_DSTRING
286 typedef std::map<irep_idt, ranges_at_loct> export_cachet;
287 #else
288 typedef std::unordered_map<irep_idt, ranges_at_loct> export_cachet;
289 #endif
302
303 void populate_cache(const irep_idt &identifier) const;
304
305 void transform_dead(
306 const namespacet &ns,
309 const namespacet &ns,
312 const namespacet &ns,
313 const irep_idt &function_from,
315 const irep_idt &function_to,
318 const namespacet &ns,
319 const irep_idt &function_from,
321 const irep_idt &function_to,
324 void transform_assign(
325 const namespacet &ns,
327 const irep_idt &function_to,
330
331 void kill(
332 const irep_idt &identifier,
334 const range_spect &range_end);
335 void kill_inf(
336 const irep_idt &identifier,
337 const range_spect &range_start);
338 bool gen(
340 const irep_idt &identifier,
342 const range_spect &range_end);
343
344 void output(std::ostream &out) const;
345
346 bool merge_inner(
347 values_innert &dest,
348 const values_innert &other);
349};
350
352 public concurrency_aware_ait<rd_range_domaint>,
353 public sparse_bitvector_analysist<reaching_definitiont>
354{
355public:
356 // constructor
358
360
361 void initialize(const goto_functionst &goto_functions) override;
362
364 {
366 return *value_sets;
367 }
368
370 {
372 return *is_threaded;
373 }
374
375 const dirtyt &get_is_dirty() const
376 {
378 return *is_dirty;
379 }
380
381protected:
383 std::unique_ptr<value_setst> value_sets;
384 std::unique_ptr<is_threadedt> is_threaded;
385 std::unique_ptr<dirtyt> is_dirty;
386};
387
388#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:118
virtual void clear()
Reset the abstract state.
Definition ai.h:266
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Base class for concurrency-aware abstract interpretation.
Definition ai.h:652
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition dirty.h:28
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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
Data type to describe upper and lower bounds of the range of bits that a read or write access may aff...
Definition goto_rw.h:61
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 directly (see make_entry) and domains may refuse to implem...
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)
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)
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)
std::map< locationt, rangest, goto_programt::target_less_than > ranges_at_loct
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
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:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
A total order over targett and const_targett.
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.
reaching_definitiont(const irep_idt &identifier, const ai_domain_baset::locationt &definition_at, const range_spect &bit_begin, const range_spect &bit_end)
irep_idt identifier
The name of the variable which was defined.