|
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