Skip to content

Commit 30fe835

Browse files
tlivelyradekdoulik
authored andcommitted
[analysis] Add a FullLattice concept and Inverted lattice (WebAssembly#6038)
The FullLattice concept extends the base Lattice with `getTop` and `meet` operations. The `Inverted` lattice uses these operations to reverse the order of an arbitrary full lattice, for example to create a lattice of integers ordered by `>` rather than by `<`.
1 parent e661836 commit 30fe835

File tree

5 files changed

+202
-7
lines changed

5 files changed

+202
-7
lines changed

src/analysis/lattice.h

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,9 +59,29 @@ concept Lattice = requires(const L& lattice,
5959
{ lattice.join(elem, constElem) } noexcept -> std::same_as<bool>;
6060
};
6161

62+
// The analysis framework only uses bottom elements and least upper bounds (i.e.
63+
// joins) directly, so lattices do not necessarily need to implement top
64+
// elements and greatest lower bounds (i.e. meets) to be useable, even though
65+
// they are required for mathematical lattices. Implementing top elements and
66+
// meets does have the benefit of making a lattice generically invertable,
67+
// though. See lattices/inverted.h.
68+
template<typename L>
69+
concept FullLattice =
70+
Lattice<L> && requires(const L& lattice,
71+
const typename L::Element& constElem,
72+
typename L::Element& elem) {
73+
// Get the top element of this lattice.
74+
{ lattice.getTop() } noexcept -> std::same_as<typename L::Element>;
75+
// Modify `elem` in-place to be the meet (aka greatest lower bound) of
76+
// `elem` and `constEleme`, returning true iff `elem` was modified, i.e. if
77+
// it was not already a lower bound of `constElem`.
78+
{ lattice.meet(elem, constElem) } noexcept -> std::same_as<bool>;
79+
};
80+
6281
#else // __cplusplus >= 202002L
6382

6483
#define Lattice typename
84+
#define FullLattice typename
6585

6686
#endif // __cplusplus >= 202002L
6787

src/analysis/lattices/bool.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ namespace wasm::analysis {
2626
struct Bool {
2727
using Element = bool;
2828
Element getBottom() const noexcept { return false; }
29+
Element getTop() const noexcept { return true; }
2930
LatticeComparison compare(Element a, Element b) const noexcept {
3031
return a > b ? GREATER : a == b ? EQUAL : LESS;
3132
}
@@ -36,6 +37,13 @@ struct Bool {
3637
}
3738
return false;
3839
}
40+
bool meet(Element& self, Element other) const noexcept {
41+
if (self && !other) {
42+
self = other;
43+
return true;
44+
}
45+
return false;
46+
}
3947
};
4048

4149
#if __cplusplus >= 202002L

src/analysis/lattices/int.h

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ template<typename T>
3434
struct Integer {
3535
using Element = T;
3636
Element getBottom() const noexcept { return std::numeric_limits<T>::min(); }
37+
Element getTop() const noexcept { return std::numeric_limits<T>::max(); }
3738
LatticeComparison compare(Element a, Element b) const noexcept {
3839
return a > b ? GREATER : a == b ? EQUAL : LESS;
3940
}
@@ -44,6 +45,13 @@ struct Integer {
4445
}
4546
return false;
4647
}
48+
bool meet(Element& self, Element other) const noexcept {
49+
if (self > other) {
50+
self = other;
51+
return true;
52+
}
53+
return false;
54+
}
4755
};
4856

4957
using Int32 = Integer<int32_t>;
@@ -52,10 +60,10 @@ using Int64 = Integer<int64_t>;
5260
using UInt64 = Integer<uint64_t>;
5361

5462
#if __cplusplus >= 202002L
55-
static_assert(Lattice<Int32>);
56-
static_assert(Lattice<Int64>);
57-
static_assert(Lattice<UInt32>);
58-
static_assert(Lattice<UInt64>);
63+
static_assert(FullLattice<Int32>);
64+
static_assert(FullLattice<Int64>);
65+
static_assert(FullLattice<UInt32>);
66+
static_assert(FullLattice<UInt64>);
5967
#endif // __cplusplus >= 202002L
6068

6169
} // namespace wasm::analysis

src/analysis/lattices/inverted.h

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
/*
2+
* Copyright 2023 WebAssembly Community Group participants
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License");
5+
* you may not use this file except in compliance with the License.
6+
* You may obtain a copy of the License at
7+
*
8+
* http://www.apache.org/licenses/LICENSE-2.0
9+
*
10+
* Unless required by applicable law or agreed to in writing, software
11+
* distributed under the License is distributed on an "AS IS" BASIS,
12+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
* See the License for the specific language governing permissions and
14+
* limitations under the License.
15+
*/
16+
17+
#ifndef wasm_analysis_lattices_inverted_h
18+
#define wasm_analysis_lattices_inverted_h
19+
20+
#include <utility>
21+
22+
#include "../lattice.h"
23+
24+
namespace wasm::analysis {
25+
26+
// Reverses the order of an arbitrary full lattice. For example,
27+
// `Inverted<UInt32>` would order uint32_t values by > rather than by <.
28+
template<FullLattice L> struct Inverted {
29+
using Element = typename L::Element;
30+
31+
L lattice;
32+
Inverted(L&& lattice) : lattice(std::move(lattice)) {}
33+
34+
Element getBottom() const noexcept { return lattice.getTop(); }
35+
Element getTop() const noexcept { return lattice.getBottom(); }
36+
LatticeComparison compare(const Element& a, const Element& b) const noexcept {
37+
return reverseComparison(lattice.compare(a, b));
38+
}
39+
bool join(Element& self, Element other) const noexcept {
40+
return lattice.meet(self, other);
41+
}
42+
bool meet(Element& self, Element other) const noexcept {
43+
return lattice.join(self, other);
44+
}
45+
};
46+
47+
} // namespace wasm::analysis
48+
49+
#endif // wasm_analysis_lattices_inverted_h

test/gtest/lattices.cpp

Lines changed: 113 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616

1717
#include "analysis/lattices/bool.h"
1818
#include "analysis/lattices/int.h"
19+
#include "analysis/lattices/inverted.h"
1920
#include "gtest/gtest.h"
2021

2122
using namespace wasm;
@@ -25,6 +26,11 @@ TEST(BoolLattice, GetBottom) {
2526
EXPECT_FALSE(lattice.getBottom());
2627
}
2728

29+
TEST(BoolLattice, GetTop) {
30+
analysis::Bool lattice;
31+
EXPECT_TRUE(lattice.getTop());
32+
}
33+
2834
TEST(BoolLattice, Compare) {
2935
analysis::Bool lattice;
3036
EXPECT_EQ(lattice.compare(false, false), analysis::EQUAL);
@@ -50,18 +56,49 @@ TEST(BoolLattice, Join) {
5056
ASSERT_TRUE(elem);
5157
}
5258

59+
TEST(BoolLattice, Meet) {
60+
analysis::Bool lattice;
61+
bool elem = true;
62+
63+
EXPECT_FALSE(lattice.meet(elem, true));
64+
ASSERT_TRUE(elem);
65+
66+
EXPECT_TRUE(lattice.meet(elem, false));
67+
ASSERT_FALSE(elem);
68+
69+
EXPECT_FALSE(lattice.meet(elem, true));
70+
ASSERT_FALSE(elem);
71+
72+
EXPECT_FALSE(lattice.meet(elem, false));
73+
ASSERT_FALSE(elem);
74+
}
75+
5376
TEST(IntLattice, GetBottom) {
5477
analysis::Int32 int32;
55-
EXPECT_EQ(int32.getBottom(), (int32_t)(1ll << 31));
78+
EXPECT_EQ(int32.getBottom(), (int32_t)(1ull << 31));
5679

5780
analysis::Int64 int64;
58-
EXPECT_EQ(int64.getBottom(), (int64_t)(1ll << 63));
81+
EXPECT_EQ(int64.getBottom(), (int64_t)(1ull << 63));
5982

6083
analysis::UInt32 uint32;
6184
EXPECT_EQ(uint32.getBottom(), (uint32_t)0);
6285

6386
analysis::UInt64 uint64;
64-
EXPECT_EQ(uint64.getBottom(), (uint32_t)0);
87+
EXPECT_EQ(uint64.getBottom(), (uint64_t)0);
88+
}
89+
90+
TEST(IntLattice, GetTop) {
91+
analysis::Int32 int32;
92+
EXPECT_EQ(int32.getTop(), (int32_t)((1ull << 31) - 1));
93+
94+
analysis::Int64 int64;
95+
EXPECT_EQ(int64.getTop(), (int64_t)((1ull << 63) - 1));
96+
97+
analysis::UInt32 uint32;
98+
EXPECT_EQ(uint32.getTop(), (uint32_t)-1ull);
99+
100+
analysis::UInt64 uint64;
101+
EXPECT_EQ(uint64.getTop(), (uint64_t)-1ull);
65102
}
66103

67104
TEST(IntLattice, Compare) {
@@ -84,3 +121,76 @@ TEST(IntLattice, Join) {
84121
EXPECT_TRUE(int32.join(elem, 100));
85122
ASSERT_EQ(elem, 100);
86123
}
124+
125+
TEST(IntLattice, Meet) {
126+
analysis::Int32 int32;
127+
int elem = 0;
128+
129+
EXPECT_FALSE(int32.meet(elem, 10));
130+
ASSERT_EQ(elem, 0);
131+
132+
EXPECT_FALSE(int32.meet(elem, 0));
133+
ASSERT_EQ(elem, 0);
134+
135+
EXPECT_TRUE(int32.meet(elem, -100));
136+
ASSERT_EQ(elem, -100);
137+
}
138+
139+
TEST(InvertedLattice, GetBottom) {
140+
analysis::Inverted inverted(analysis::Bool{});
141+
EXPECT_TRUE(inverted.getBottom());
142+
}
143+
144+
TEST(InvertedLattice, GetTop) {
145+
analysis::Inverted inverted(analysis::Bool{});
146+
EXPECT_FALSE(inverted.getTop());
147+
}
148+
149+
TEST(InvertedLattice, Compare) {
150+
analysis::Inverted inverted(analysis::Bool{});
151+
EXPECT_EQ(inverted.compare(false, false), analysis::EQUAL);
152+
EXPECT_EQ(inverted.compare(false, true), analysis::GREATER);
153+
EXPECT_EQ(inverted.compare(true, false), analysis::LESS);
154+
EXPECT_EQ(inverted.compare(true, true), analysis::EQUAL);
155+
}
156+
157+
TEST(InvertedLattice, Join) {
158+
analysis::Inverted inverted(analysis::Bool{});
159+
bool elem = true;
160+
161+
EXPECT_FALSE(inverted.join(elem, true));
162+
ASSERT_TRUE(elem);
163+
164+
EXPECT_TRUE(inverted.join(elem, false));
165+
ASSERT_FALSE(elem);
166+
167+
EXPECT_FALSE(inverted.join(elem, true));
168+
ASSERT_FALSE(elem);
169+
170+
EXPECT_FALSE(inverted.join(elem, false));
171+
ASSERT_FALSE(elem);
172+
}
173+
174+
TEST(InvertedLattice, Meet) {
175+
analysis::Inverted inverted(analysis::Bool{});
176+
bool elem = false;
177+
178+
EXPECT_FALSE(inverted.meet(elem, false));
179+
ASSERT_FALSE(elem);
180+
181+
EXPECT_TRUE(inverted.meet(elem, true));
182+
ASSERT_TRUE(elem);
183+
184+
EXPECT_FALSE(inverted.meet(elem, false));
185+
ASSERT_TRUE(elem);
186+
187+
EXPECT_FALSE(inverted.meet(elem, true));
188+
ASSERT_TRUE(elem);
189+
}
190+
191+
TEST(InvertedLattice, DoubleInverted) {
192+
using DoubleInverted = analysis::Inverted<analysis::Inverted<analysis::Bool>>;
193+
DoubleInverted identity(analysis::Inverted<analysis::Bool>{analysis::Bool{}});
194+
EXPECT_FALSE(identity.getBottom());
195+
EXPECT_TRUE(identity.getTop());
196+
}

0 commit comments

Comments
 (0)