@@ -31,19 +31,20 @@ in a basic block is taken into consideration when performing the analysis.
31
31
4 . ** Intra-procedural:** The analysis is done on one function at a time.
32
32
33
33
## Dataflow Analysis Details
34
- For every basic block we compute the following sets: ` In ` and ` Kill ` . The ` In `
34
+ For every basic block, we compute the following sets: ` In ` and ` Kill ` . The ` In `
35
35
set for basic block ` B ` is denoted as ` In[B] ` and the ` Kill ` set is denoted as
36
36
` Kill[B] ` .
37
37
38
- For every edge we compute the following sets: ` Out ` and ` Gen ` . The ` Out ` set on
39
- edge ` Bi->Bj ` is denoted as ` Out[Bi][Bj] ` and the Gen set is denoted as
38
+ For every edge, we compute the following sets: ` Out ` and ` Gen ` . The ` Out ` set on
39
+ edge ` Bi->Bj ` is denoted as ` Out[Bi][Bj] ` and the ` Gen ` set is denoted as
40
40
` Gen[Bi][Bj] ` .
41
41
42
42
### In[ B]
43
43
` In[B] ` stores the mapping between an ` _Nt_array_ptr ` and its widened bounds
44
44
inside block ` B ` . For example, given ` _Nt_array_ptr V ` with declared bounds
45
- ` (low, high) ` , ` In[B] ` would store the mapping ` {V:i} ` , where ` i ` is an unsigned
46
- integer and the bounds of ` V ` should be widened to ` (low, high + i) ` .
45
+ ` (V + low, V + high) ` , ` In[B] ` would store the mapping ` {V:i} ` , where ` i ` is an
46
+ unsigned integer implying that the bounds of ` V ` should be widened to
47
+ ` (V + low, V + high + i) ` .
47
48
48
49
Dataflow equation:
49
50
` In[B] = ∩ Out[B*][B], where B* ∈ pred(B) ` .
@@ -57,43 +58,43 @@ Thus, `Kill[B]` stores the mapping between a statement `S` and `_Nt_array_ptr's`
57
58
whose bounds are killed in ` S ` .
58
59
59
60
### Gen[ Bi] [ Bj ]
60
- Given ` _Nt_array_ptr V ` with declared bounds ` (low, high) ` , the bounds of ` V `
61
- can be widened by 1 if ` V ` is dereferenced at the upper bound. This means that
62
- if there is an edge ` Bi->Bj ` whose edge condition is of the form `if ( * (V +
63
- high + i))` , where ` i` is an unsigned integer offset, the widened bounds
64
- ` {V:i+1} ` can be added to ` Gen[Bi][Bj] ` , provided we have already tested for
65
- pointer access of the form ` if (*(V + high + i - 1)) ` .
61
+ Given ` _Nt_array_ptr V ` with declared bounds ` (V + low, V + high) ` , the bounds
62
+ of ` V ` can be widened by 1 if ` V ` is dereferenced at its current upper bound.
63
+ This means that if there is an edge ` Bi->Bj ` whose edge condition is of the
64
+ form ` if (*(V + high + i))` , where ` i ` is an unsigned integer offset, the
65
+ widened bounds ` {V:i+1} ` can be added to ` Gen[Bi][Bj] ` , provided we have
66
+ already tested for pointer access of the form ` if (*(V + high + ( i - 1) )) ` .
66
67
67
68
For example:
68
69
```
69
- _Nt_array_ptr<T> V : bounds (low, high);
70
+ _Nt_array_ptr<T> V : bounds (V + low, V + high);
70
71
if (*V) { // Ptr dereference is NOT at the current upper bound. No bounds widening.
71
- if (*(V + high)) { // Ptr dereference is at the current upper bound. Widen bounds by 1. New bounds for V are (low, high + 1).
72
- if (*(V + high + 1)) { // Ptr dereference is at the current upper bound. Widen bounds by 1. New bounds for V are (low, high + 2).
73
- if (*(V + high + 3)) { // Ptr dereference is *not* at the current upper bound. No bounds widening. Flag an error!.
72
+ if (*(V + high)) { // Ptr dereference is at the current upper bound. Widen bounds by 1. New bounds for V are (V + low, V + high + 1).
73
+ if (*(V + high + 1)) { // Ptr dereference is at the current upper bound. Widen bounds by 1. New bounds for V are (V + low, V + high + 2).
74
+ if (*(V + high + 3)) { // Ptr dereference is NOT at the current upper bound. No bounds widening. Flag an error!
74
75
```
75
76
76
77
### Out[ Bi] [ Bj ]
77
78
` Out[Bi][Bj] ` denotes the bounds widened by block ` Bi ` on edge ` Bi->Bj ` .
78
79
79
80
Dataflow equation:
80
- ` Out[Bi][Bj] = (In[Bi] - Kill[Bi]) ∪ Gen[Bi][Bj] `
81
+ ` Out[Bi][Bj] = (In[Bi] - Kill[Bi]) ∪ Gen[Bi][Bj], where Bj ∈ succ(Bi) ` .
81
82
82
83
### Initial values of In and Out sets
83
84
84
85
To compute ` In[B] ` , we compute the intersection of ` Out[B*][B] ` , where ` B* ` are
85
86
all preds of block ` B ` . When there is a back edge from block ` B' ` to ` B ` (for
86
- example in the case of loops), the Out set for block ` B' ` will be empty. As a
87
+ example in the case of loops), the ` Out ` set for block ` B' ` will be empty. As a
87
88
result, the intersection operation would always result in an empty set ` In[B] ` .
88
89
89
- So to handle this, we initialize the In and Out sets for all blocks to ` Top ` .
90
- ` Top ` represents the union of the Gen sets of all edges. We have chosen the
91
- offsets of ptr variables in ` Top ` to be the max unsigned int . The reason behind
92
- this is that in order to compute the actual In sets for blocks we are going to
93
- intersect the Out sets on all the incoming edges of the block. And in that case
94
- we would always pick the ptr with the smaller offset. Choosing max unsigned int
95
- also makes handling ` Top ` much easier as we do not need to explicitly store edge
96
- info.
90
+ So to handle this, we initialize the ` In ` and ` Out ` sets for all blocks to
91
+ ` Top ` . ` Top ` represents the union of the ` Gen ` sets of all edges. We have
92
+ chosen the offsets of ptr variables in ` Top ` to be ` UINT_MAX ` . The reason
93
+ behind this is that in order to compute the actual ` In ` sets for blocks we are
94
+ going to intersect the ` Out ` sets on all the incoming edges of the block. And
95
+ in that case we would always pick the ptr with the smaller offset. Choosing
96
+ ` UINT_MAX ` also makes handling ` Top ` much easier as we do not need to
97
+ explicitly store edge info.
97
98
98
99
Thus, we have the following two equations for ` Top ` :
99
100
```
@@ -107,16 +108,16 @@ In[B] = Top
107
108
Out[Bi][Bj] = Top, where Bj ∈ succ(Bi)
108
109
```
109
110
110
- Now, we also need to handle the case where there is an unconditional jump into a
111
- block (for example, as a result of a ` goto ` ). In this case, we cannot widen the
112
- bounds because we would not have tested the ptr dereference on the
113
- unconditional edge. So in this case we want the intersection (and hence the In
114
- set) to result in an empty set.
111
+ Now, we also need to handle the case where there is an unconditional jump into
112
+ a block (for example, as a result of a ` goto ` ). In this case, we cannot widen
113
+ the bounds because we would not have tested the ptr dereference on the
114
+ unconditional edge. So in this case we want the intersection (and hence the
115
+ ` In ` set) to result in an empty set.
115
116
116
- So we initialize the In and Out sets of all blocks to ` Top ` , except the Entry
117
- block.
117
+ So we initialize the ` In ` and ` Out ` sets of all blocks to ` Top ` , except the
118
+ ` Entry ` block.
118
119
119
- Thus, we have the following initial value for the Entry block:
120
+ Thus, we have the following initial values for the ` Entry ` block:
120
121
```
121
122
In[Entry] = ∅
122
123
Out[Entry][B*] = ∅, where B* ∈ succ(Entry)
@@ -128,12 +129,12 @@ The main class that implements the analysis is
128
129
and the main function is ` BoundsAnalysis::WidenBounds() ` .
129
130
130
131
` WidenBounds ` will perform the bounds widening for the entire function. We can
131
- then we can call ` BoundsAnalysis::GetWidenedBounds ` to retrieve the
132
- widened bounds for the current basic block.
132
+ then call ` BoundsAnalysis::GetWidenedBounds ` to retrieve the widened bounds for
133
+ the current basic block.
133
134
134
135
The approach used for implementing the analysis is the iterative worklist
135
136
algorithm in which we keep adding blocks to a worklist as long as we do not
136
- reach a fixed point i.e.: as long as the Out sets for the blocks keep changing.
137
+ reach a fixed point i.e.: as long as the ` Out ` sets for the blocks keep changing.
137
138
138
139
### Algorithm
139
140
```
0 commit comments