|
16 | 16 | #ifndef wasm_analysis_lattices_stack_h |
17 | 17 | #define wasm_analysis_lattices_stack_h |
18 | 18 |
|
19 | | -#include <deque> |
20 | | -#include <iostream> |
21 | 19 | #include <optional> |
| 20 | +#include <vector> |
22 | 21 |
|
23 | 22 | #include "../lattice.h" |
| 23 | +#include "bool.h" |
24 | 24 |
|
25 | 25 | namespace wasm::analysis { |
26 | 26 |
|
27 | 27 | // Note that in comments, bottom is left and top is right. |
28 | 28 |
|
29 | 29 | // This lattice models the behavior of a stack of values. The lattice is |
30 | 30 | // templated on L, which is a lattice which can model some abstract property of |
31 | | -// a value on the stack. The StackLattice itself can push or pop abstract values |
| 31 | +// a value on the stack. The Stack itself can push or pop abstract values |
32 | 32 | // and access the top of stack. |
33 | 33 | // |
34 | 34 | // The goal here is not to operate directly on the stacks. Rather, the |
35 | | -// StackLattice organizes the L elements in an efficient and natural way which |
36 | | -// reflects the behavior of the wasm value stack. Transfer functions will |
| 35 | +// Stack organizes the L elements in an efficient and natural way which |
| 36 | +// reflects the behavior of the Wasm value stack. Transfer functions will |
37 | 37 | // operate on stack elements individually. The stack itself is an intermediate |
38 | 38 | // structure. |
39 | 39 | // |
@@ -74,193 +74,115 @@ namespace wasm::analysis { |
74 | 74 | // instance, one could use this to analyze the maximum bit size of values on the |
75 | 75 | // Wasm value stack. When new actual values are pushed or popped off the Wasm |
76 | 76 | // value stack by instructions, the same is done to abstract lattice elements in |
77 | | -// the StackLattice. |
| 77 | +// the Stack. |
78 | 78 | // |
79 | 79 | // When two control flows are joined together, one with stack [b, a] and another |
80 | 80 | // with stack [b, a'], we can take the least upper bound to produce a stack [b, |
81 | 81 | // LUB(a, a')], where LUB(a, a') takes the maximum of the two maximum bit |
82 | 82 | // values. |
| 83 | +template<Lattice L> struct Stack { |
| 84 | + // The materialized stack of values. The infinite items underneath these |
| 85 | + // materialized values are bottom. The element at the base of the materialized |
| 86 | + // stack must not be bottom. |
| 87 | + using Element = std::vector<typename L::Element>; |
83 | 88 |
|
84 | | -template<Lattice L> class StackLattice { |
85 | | - L& lattice; |
| 89 | + L lattice; |
86 | 90 |
|
87 | | -public: |
88 | | - StackLattice(L& lattice) : lattice(lattice) {} |
| 91 | + Stack(L&& lattice) : lattice(std::move(lattice)) {} |
89 | 92 |
|
90 | | - class Element { |
91 | | - // The top lattice can be imagined as an infinitely high stack of top |
92 | | - // elements, which is unreachable in most cases. In practice, we make the |
93 | | - // stack an optional, and we represent top with the absence of a stack. |
94 | | - std::optional<std::deque<typename L::Element>> stackValue = |
95 | | - std::deque<typename L::Element>(); |
96 | | - |
97 | | - public: |
98 | | - bool isTop() const { return !stackValue.has_value(); } |
99 | | - bool isBottom() const { |
100 | | - return stackValue.has_value() && stackValue->empty(); |
101 | | - } |
102 | | - void setToTop() { stackValue.reset(); } |
103 | | - |
104 | | - typename L::Element& stackTop() { return stackValue->back(); } |
105 | | - |
106 | | - void push(typename L::Element&& element) { |
107 | | - // We can imagine each stack [b, a] as being implicitly an infinite stack |
108 | | - // of the form (bottom) [... BOTTOM, BOTTOM, b, a] (top). In that case, |
109 | | - // adding a bottom element to an empty stack changes nothing, so we don't |
110 | | - // actually add a bottom. |
111 | | - if (stackValue.has_value() && |
112 | | - (!stackValue->empty() || !element.isBottom())) { |
113 | | - stackValue->push_back(std::move(element)); |
114 | | - } |
115 | | - } |
116 | | - |
117 | | - void push(const typename L::Element& element) { |
118 | | - if (stackValue.has_value() && |
119 | | - (!stackValue->empty() || !element.isBottom())) { |
120 | | - stackValue->push_back(std::move(element)); |
121 | | - } |
| 93 | + void push(Element& elem, typename L::Element&& element) const noexcept { |
| 94 | + if (elem.empty() && element == lattice.getBottom()) { |
| 95 | + // no-op, the stack is already entirely made of bottoms. |
| 96 | + return; |
122 | 97 | } |
| 98 | + elem.emplace_back(std::move(element)); |
| 99 | + } |
123 | 100 |
|
124 | | - typename L::Element pop() { |
125 | | - typename L::Element value = stackValue->back(); |
126 | | - stackValue->pop_back(); |
127 | | - return value; |
128 | | - } |
129 | | - |
130 | | - void print(std::ostream& os) { |
131 | | - if (isTop()) { |
132 | | - os << "TOP STACK" << std::endl; |
133 | | - return; |
134 | | - } |
135 | | - |
136 | | - for (auto iter = stackValue->rbegin(); iter != stackValue->rend(); |
137 | | - ++iter) { |
138 | | - iter->print(os); |
139 | | - os << std::endl; |
140 | | - } |
| 101 | + typename L::Element pop(Element& elem) const noexcept { |
| 102 | + if (elem.empty()) { |
| 103 | + // "Pop" and return one of the infinite bottom elements. |
| 104 | + return lattice.getBottom(); |
141 | 105 | } |
142 | | - |
143 | | - friend StackLattice; |
144 | | - }; |
| 106 | + auto popped = elem.back(); |
| 107 | + elem.pop_back(); |
| 108 | + return popped; |
| 109 | + } |
145 | 110 |
|
146 | 111 | Element getBottom() const noexcept { return Element{}; } |
147 | 112 |
|
148 | | - // Like in computing the LUB, we compare the tops of the two stacks, as it |
149 | | - // handles the case of stacks of different scopes. Comparisons are done by |
150 | | - // element starting from the top. |
151 | | - // |
152 | | - // If the left stack is higher, and left top >= right top, then we say |
153 | | - // that left stack > right stack. If the left stack is lower and the left top |
154 | | - // >= right top or if the left stack is higher and the right top > left top or |
155 | | - // they are unrelated, then there is no relation. Same applies for the reverse |
156 | | - // relationship. |
157 | | - LatticeComparison compare(const Element& left, |
158 | | - const Element& right) const noexcept { |
159 | | - // Handle cases where there are top elements. |
160 | | - if (left.isTop()) { |
161 | | - if (right.isTop()) { |
162 | | - return LatticeComparison::EQUAL; |
163 | | - } else { |
164 | | - return LatticeComparison::GREATER; |
| 113 | + LatticeComparison compare(const Element& a, const Element& b) const noexcept { |
| 114 | + auto result = EQUAL; |
| 115 | + // Iterate starting from the end of the vectors to match up the tops of |
| 116 | + // stacks with different sizes. |
| 117 | + for (auto itA = a.rbegin(), itB = b.rbegin(); |
| 118 | + itA != a.rend() || itB != b.rend(); |
| 119 | + ++itA, ++itB) { |
| 120 | + if (itA == a.rend()) { |
| 121 | + // The rest of A's elements are bottom, but B has a non-bottom element |
| 122 | + // because of our invariant that the base of the materialized stack must |
| 123 | + // not be bottom. |
| 124 | + return LESS; |
165 | 125 | } |
166 | | - } else if (right.isTop()) { |
167 | | - return LatticeComparison::LESS; |
168 | | - } |
169 | | - |
170 | | - bool hasLess = false; |
171 | | - bool hasGreater = false; |
172 | | - |
173 | | - // Check the tops of both stacks which match (i.e. are within the heights |
174 | | - // of both stacks). If there is a pair which is not related, the stacks |
175 | | - // cannot be related. |
176 | | - for (auto leftIt = left.stackValue->crbegin(), |
177 | | - rightIt = right.stackValue->crbegin(); |
178 | | - leftIt != left.stackValue->crend() && |
179 | | - rightIt != right.stackValue->crend(); |
180 | | - ++leftIt, ++rightIt) { |
181 | | - LatticeComparison currComparison = lattice.compare(*leftIt, *rightIt); |
182 | | - switch (currComparison) { |
183 | | - case LatticeComparison::NO_RELATION: |
184 | | - return LatticeComparison::NO_RELATION; |
185 | | - case LatticeComparison::LESS: |
186 | | - hasLess = true; |
187 | | - break; |
188 | | - case LatticeComparison::GREATER: |
189 | | - hasGreater = true; |
190 | | - break; |
191 | | - default: |
192 | | - break; |
| 126 | + if (itB == b.rend()) { |
| 127 | + // The rest of B's elements are bottom, but A has a non-bottom element. |
| 128 | + return GREATER; |
| 129 | + } |
| 130 | + switch (lattice.compare(*itA, *itB)) { |
| 131 | + case NO_RELATION: |
| 132 | + return NO_RELATION; |
| 133 | + case EQUAL: |
| 134 | + continue; |
| 135 | + case LESS: |
| 136 | + if (result == GREATER) { |
| 137 | + // Cannot be both less and greater. |
| 138 | + return NO_RELATION; |
| 139 | + } |
| 140 | + result = LESS; |
| 141 | + continue; |
| 142 | + case GREATER: |
| 143 | + if (result == LESS) { |
| 144 | + // Cannot be both greater and less. |
| 145 | + return NO_RELATION; |
| 146 | + } |
| 147 | + result = GREATER; |
| 148 | + continue; |
193 | 149 | } |
194 | 150 | } |
195 | | - |
196 | | - // Check cases for when the stacks have unequal. As a rule, if a stack |
197 | | - // is higher, it is greater than the other stack, but if and only if |
198 | | - // when comparing their matching top portions the top portion of the |
199 | | - // higher stack is also >= the top portion of the shorter stack. |
200 | | - if (left.stackValue->size() > right.stackValue->size()) { |
201 | | - hasGreater = true; |
202 | | - } else if (right.stackValue->size() > left.stackValue->size()) { |
203 | | - hasLess = true; |
204 | | - } |
205 | | - |
206 | | - if (hasLess && !hasGreater) { |
207 | | - return LatticeComparison::LESS; |
208 | | - } else if (hasGreater && !hasLess) { |
209 | | - return LatticeComparison::GREATER; |
210 | | - } else if (hasLess && hasGreater) { |
211 | | - // Contradiction, and therefore must be unrelated. |
212 | | - return LatticeComparison::NO_RELATION; |
213 | | - } else { |
214 | | - return LatticeComparison::EQUAL; |
215 | | - } |
| 151 | + return result; |
216 | 152 | } |
217 | 153 |
|
218 | | - // When taking the join, we take the joins of the elements of each stack |
219 | | - // starting from the top of the stack. So, join([b, a], [b', a']) is [join(b, |
220 | | - // b'), join(a, a')]. If one stack is higher than the other, the bottom of the |
221 | | - // higher stack will be kept, while the join of the corresponding tops of each |
222 | | - // stack will be taken. For instance, join([d, c, b, a], [b', a']) is [d, c, |
223 | | - // join(b, b'), join(a, a')]. |
224 | | - // |
225 | | - // We start at the top because it makes taking the join of stacks with |
226 | | - // different scope easier, as mentioned at the top of the file. It also fits |
227 | | - // with the conception of the stack starting at the top and having an infinite |
228 | | - // bottom, which allows stacks of different height and scope to be easily |
229 | | - // joined. |
230 | 154 | bool join(Element& joinee, const Element& joiner) const noexcept { |
231 | | - // Top element cases, since top elements don't actually have the stack |
232 | | - // value. |
233 | | - if (joinee.isTop()) { |
234 | | - return false; |
235 | | - } else if (joiner.isTop()) { |
236 | | - joinee.stackValue.reset(); |
237 | | - return true; |
| 155 | + // If joiner is deeper than joinee, prepend those extra elements to joinee |
| 156 | + // first. They don't need to be explicitly joined with anything because they |
| 157 | + // would be joined with bottom, which wouldn't change them. |
| 158 | + bool result = false; |
| 159 | + size_t extraSize = 0; |
| 160 | + if (joiner.size() > joinee.size()) { |
| 161 | + extraSize = joiner.size() - joinee.size(); |
| 162 | + auto extraBegin = joiner.begin(); |
| 163 | + auto extraEnd = joiner.begin() + extraSize; |
| 164 | + joinee.insert(joinee.begin(), extraBegin, extraEnd); |
| 165 | + result = true; |
238 | 166 | } |
239 | | - |
240 | | - bool modified = false; |
241 | | - |
242 | | - // Merge the shorter height stack with the top of the longer height |
243 | | - // stack. We do this by taking the LUB of each pair of matching elements |
244 | | - // from both stacks. |
245 | | - auto joineeIt = joinee.stackValue->rbegin(); |
246 | | - auto joinerIt = joiner.stackValue->crbegin(); |
247 | | - for (; joineeIt != joinee.stackValue->rend() && |
248 | | - joinerIt != joiner.stackValue->crend(); |
| 167 | + // Join all the elements present in both materialized stacks, starting from |
| 168 | + // the end so the stack tops match up. Stop the iteration when we've |
| 169 | + // processed all of joinee, excluding any extra elements from joiner we just |
| 170 | + // prepended to it, or when we've processed all of joiner. |
| 171 | + auto joineeIt = joinee.rbegin(); |
| 172 | + auto joinerIt = joiner.rbegin(); |
| 173 | + auto joineeEnd = joinee.rend() - extraSize; |
| 174 | + for (; joineeIt != joineeEnd && joinerIt != joiner.rend(); |
249 | 175 | ++joineeIt, ++joinerIt) { |
250 | | - modified |= lattice.join(*joineeIt, *joinerIt); |
| 176 | + result |= lattice.join(*joineeIt, *joinerIt); |
251 | 177 | } |
252 | | - |
253 | | - // If the joiner stack is higher, append the bottom of it to our current |
254 | | - // stack. |
255 | | - for (; joinerIt != joiner.stackValue->crend(); ++joinerIt) { |
256 | | - joinee.stackValue->push_front(*joinerIt); |
257 | | - modified = true; |
258 | | - } |
259 | | - |
260 | | - return modified; |
| 178 | + return result; |
261 | 179 | } |
262 | 180 | }; |
263 | 181 |
|
| 182 | +#if __cplusplus >= 202002L |
| 183 | +static_assert(Lattice<Stack<Bool>>); |
| 184 | +#endif |
| 185 | + |
264 | 186 | } // namespace wasm::analysis |
265 | 187 |
|
266 | 188 | #endif // wasm_analysis_lattices_stack_h |
0 commit comments