diff --git a/src/ir/CMakeLists.txt b/src/ir/CMakeLists.txt index 919069770c5..5521529cd91 100644 --- a/src/ir/CMakeLists.txt +++ b/src/ir/CMakeLists.txt @@ -2,6 +2,7 @@ FILE(GLOB ir_HEADERS *.h) set(ir_SOURCES ExpressionAnalyzer.cpp ExpressionManipulator.cpp + constraint.cpp drop.cpp effects.cpp eh-utils.cpp diff --git a/src/ir/abstract.h b/src/ir/abstract.h index 04b04e34223..d0f3794908c 100644 --- a/src/ir/abstract.h +++ b/src/ir/abstract.h @@ -56,7 +56,8 @@ enum Op { GtS, GtU, GeS, - GeU + GeU, + Invalid }; inline bool hasAnyRotateShift(BinaryOp op) { diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp new file mode 100644 index 00000000000..fabcbfa06ca --- /dev/null +++ b/src/ir/constraint.cpp @@ -0,0 +1,156 @@ +/* + * Copyright 2026 WebAssembly Community Group participants + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +#include + +#include "ir/constraint.h" +#include "ir/properties.h" +#include "wasm.h" + +namespace wasm::constraint { + +namespace { + +// Evaluate whether a => b, where a and b are operations on constants. +Result provesConstantPair(Abstract::Op aOp, + const Literal& aConstant, + Abstract::Op bOp, + const Literal& bConstant) { + // x == X =?=> x == Y. True iff X == Y. + if (aOp == Abstract::Eq && bOp == Abstract::Eq) { + return aConstant == bConstant ? True : False; + } + + // x == X =?=> x != Y. True iff X != Y. + if (aOp == Abstract::Eq && bOp == Abstract::Ne) { + return aConstant == bConstant ? False : True; + } + + // x != X =?=> x == Y. False if X = Y, else unknown. + if (aOp == Abstract::Ne && bOp == Abstract::Eq) { + if (aConstant == bConstant) { + return False; + } + } + + // x != X =?=> x != Y. True if X = Y, else unknown. + if (aOp == Abstract::Ne && bOp == Abstract::Ne) { + if (aConstant == bConstant) { + return True; + } + } + + // TODO: handle >, >=, <, and <= + return Unknown; +} + +// Core comparison of two constraints: whether a => b +Result provesPair(const Constraint& a, const Constraint& b) { + // A thing always implies itself. + if (a == b) { + return True; + } + + // Comparisons of two constants. + auto* aConstant = std::get_if(&a.term); + auto* bConstant = std::get_if(&b.term); + if (aConstant && bConstant) { + return provesConstantPair(a.op, *aConstant, b.op, *bConstant); + } + + return Unknown; +} + +} // anonymous namespace + +Result AndedConstraintSet::proves(const Constraint& condition) const { + // Sometimes a single constraint is enough to determine the condition. + for (auto& c : *this) { + auto result = provesPair(c, condition); + if (result != Unknown) { + return result; + } + } + + // TODO smarts for multiple constraints + + // Otherwise, who knows. + return Unknown; +} + +Result AndedConstraintSet::proves(const AndedConstraintSet& other) const { + if (other.empty()) { + // The empty set of constraints is always true. + return True; + } + + bool hasUnknown = false; + + for (auto& c : other) { + auto result = proves(c); + if (result == False) { + // The entire conjunction is proven false. + return False; + } + if (result == Unknown) { + hasUnknown = true; + } + } + + return hasUnknown ? Unknown : True; +} + +void AndedConstraintSet::fuzzyAnd(const Constraint& c) { + if (size() < MaxConstraints) { + push_back(c); + return; + } + + // Otherwise, just do not add this one. + // TODO: We could try to be clever and see if one of the existing ones makes + // more sense to drop. +} + +void AndedConstraintSet::fuzzyOr(const AndedConstraintSet& other) { + // If one is empty (no constraints, everything is true, and we can prove + // nothing useful) then it does not add anything to the other. + if (empty()) { + *this = other; + return; + } + if (other.empty()) { + return; + } + + // If this is already implied by current constraints, then it is redundant. + // E.g. if we are { x = 10 } and other is { x >= 0 } then all we need is + // { x >= 0 } as the result of the OR. + if (proves(other) == True) { + *this = other; + return; + } + if (other.proves(*this) == True) { + return; + } + + // TODO smarts: handle <= > and so forth + + // Otherwise, we don't know how to nicely OR these things, and expand to the + // trivial set of no constraints. + clear(); +} + +} // namespace wasm::constraint diff --git a/src/ir/constraint.h b/src/ir/constraint.h new file mode 100644 index 00000000000..23ef83d2594 --- /dev/null +++ b/src/ir/constraint.h @@ -0,0 +1,125 @@ +/* + * Copyright 2026 WebAssembly Community Group participants + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +// +// Constraints on the values of things, like x >=0, x < 42, and x == y. Allows +// inference whether other things are true given a set of constraints, like +// { x == 10 } => { x >= 5 }. +// + +#ifndef wasm_ir_constraint_h +#define wasm_ir_constraint_h + +#include + +#include "ir/abstract.h" +#include "support/inplace_vector.h" +#include "support/utilities.h" +#include "wasm.h" + +namespace wasm::constraint { + +// A term in a constraint, either a local index or literal value. +struct Term : public std::variant { + bool operator==(const Term&) const = default; +}; + +// A constraint: some operation and some value, like "is equal to 17" or "is +// less than local 6". +struct Constraint { + Abstract::Op op = Abstract::Invalid; + Term term; + + bool operator==(const Constraint&) const = default; +}; + +// We limit constraints to a low number to ensure good performance even with +// simple brute-force solving. +// TODO: use a generic constraint solver..? +inline constexpr std::size_t MaxConstraints = 3; + +// What we infer from one thing about another: true/false, or unknown. +enum Result { True, False, Unknown }; + +// A set of constraints connected by the logical "and" operation. That is, all +// the constraints are simultaneously true about some value. In the examples in +// the comments below, `x` is used for the thing all the constraints are talking +// about, which looks like a local, but it could be a global or a struct field +// or anything else in general. +struct AndedConstraintSet : inplace_vector { + // Check a condition against this set, that is, whether the existing + // constraints prove that it must be true, false, or unknown: whether + // + // { this } => { condition } + // + // https://en.wikipedia.org/wiki/Material_conditional#Truth_table + Result proves(const Constraint& condition) const; + + // Check an entire other set. + Result proves(const AndedConstraintSet& other) const; + + // Add a constraint to the set, ANDed with the others. This is a fuzzy + // operation because our capacity is bounded - we cannot have more than + // MaxConstraints. If too many are added, we will drop some, which means we + // will be able to prove less things (but we will never prove anything + // incorrectly). + void fuzzyAnd(const Constraint& c); + + // Merge constraints using OR. We cannot represent such a thing directly + // (we only use AND), so we approximate it in a fuzzy way. For example, this + // would be valid: + // + // fuzzyOr({ x == 5 }, { x == 10 }) == { x >= 5 && x <= 10 } + // + // Note how the result here still accepts the values 5 and 10, but it also + // allows more. Formally, this has the following mathematical property: + // + // (X || Y) => fuzzyOr(X, Y) + // + // That is, if X or Y is true, the result of fuzzOr is also true. But the + // reverse is not always the case: fuzzyOr may be true without X || Y being + // true (see the truth table linked above, and the value 8 in the example). + // + // Returning to the example, we can use this to optimize as follows: if + // two code paths reaching a location have x == 5 and x == 10, so the value in + // the merge location is either 5 or 10, then if we see some i32.ge_s that + // does x >= 0 then we can evaluate it with proves(): + // + // { x >= 5 && x <= 10 }.proves({ x >= 0 }) == True + // + // And it is valid to optimize that i32.ge_s into a constant 1, since + // + // { x == 5 || x == 10 } => + // { x >= 5 && x <= 10 } => + // { x >= 0 } + // + // I.e. the constraints imply the truth of the thing we are evaluating. + // + // Note that the fuzziness here means that fuzzyOr() can do a better or a + // worse job. It is always valid for fuzzyOr to return { } or any other + // always-true thing (see the truth table linked above). But then: + // + // { x == 5 || x == 10 } => + // { } =!!> + // { x >= 0 } + // + // If we become too fuzzy, we lose the ability to imply anything useful. + void fuzzyOr(const AndedConstraintSet& other); +}; + +} // namespace wasm::constraint + +#endif // wasm_ir_constraint_h diff --git a/test/gtest/CMakeLists.txt b/test/gtest/CMakeLists.txt index 4bd358032d7..8db86712bba 100644 --- a/test/gtest/CMakeLists.txt +++ b/test/gtest/CMakeLists.txt @@ -9,6 +9,7 @@ set(unittest_SOURCES arena.cpp cast-check.cpp cfg.cpp + constraint.cpp dataflow.cpp delta_debugging.cpp dfa_minimization.cpp diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp new file mode 100644 index 00000000000..8bb2ba38908 --- /dev/null +++ b/test/gtest/constraint.cpp @@ -0,0 +1,208 @@ +#include "ir/constraint.h" +#include "ir/abstract.h" +#include "gtest/gtest.h" + +using namespace wasm; +using namespace wasm::Abstract; +using namespace wasm::constraint; + +TEST(ConstraintTest, TestEq) { + // Sets start empty. + AndedConstraintSet s; + EXPECT_TRUE(s.empty()); + + // x == 5 (we use "x" for the name of the thing being compared, in these + // comments). + Constraint c{Eq, {Literal(int32_t(5))}}; + + // We can't infer anything using an empty set. + EXPECT_EQ(s.proves(c), Unknown); + + // If we add it, then things check out: a thing always proves itself true. + s.fuzzyAnd(c); + EXPECT_EQ(s.size(), 1); + EXPECT_EQ(s.proves(c), True); + + // x == 10, a different number: we can infer false. + EXPECT_EQ(s.proves(Constraint{Eq, {Literal(int32_t(10))}}), False); + + // x != 15: we can infer true. + EXPECT_EQ(s.proves(Constraint{Ne, {Literal(int32_t(15))}}), True); + + // x != 5: we can infer false. + EXPECT_EQ(s.proves(Constraint{Ne, {Literal(int32_t(5))}}), False); +} + +TEST(ConstraintTest, TestNe) { + AndedConstraintSet s; + // x != 5 + Constraint c{Ne, {Literal(int32_t(5))}}; + s.fuzzyAnd(c); + + // Checks out versus itself. + EXPECT_EQ(s.proves(c), True); + + // x == 10: we don't know. + EXPECT_EQ(s.proves(Constraint{Eq, {Literal(int32_t(10))}}), Unknown); + + // x != 15: we don't know. + EXPECT_EQ(s.proves(Constraint{Ne, {Literal(int32_t(15))}}), Unknown); + + // x == 5: we can infer false. + EXPECT_EQ(s.proves(Constraint{Eq, {Literal(int32_t(5))}}), False); +} + +TEST(ConstraintTest, TestMulti) { + AndedConstraintSet s; + // x != 5 && x != 10 + Constraint c{Ne, {Literal(int32_t(5))}}; + Constraint d{Ne, {Literal(int32_t(10))}}; + s.fuzzyAnd(c); + s.fuzzyAnd(d); + + // Each checks out versus itself. + EXPECT_EQ(s.proves(c), True); + EXPECT_EQ(s.proves(d), True); + + // x == 5: false. + EXPECT_EQ(s.proves(Constraint{Eq, {Literal(int32_t(5))}}), False); + + // x == 10: false. + EXPECT_EQ(s.proves(Constraint{Eq, {Literal(int32_t(10))}}), False); + + // x == 15: we don't know. + EXPECT_EQ(s.proves(Constraint{Eq, {Literal(int32_t(15))}}), Unknown); + + // x != 15: we don't know. + EXPECT_EQ(s.proves(Constraint{Ne, {Literal(int32_t(15))}}), Unknown); +} + +TEST(ConstraintTest, TestSets) { + // x == 5 + Constraint c{Eq, {Literal(int32_t(5))}}; + + AndedConstraintSet s; + + // Any set always proves itself to be true. + EXPECT_EQ(s.proves(s), True); + + // Ditto after adding something. + s.fuzzyAnd(c); + EXPECT_EQ(s.proves(s), True); + + // Another set, empty. + AndedConstraintSet t; + + // Any set always proves an empty set to be true. + EXPECT_EQ(s.proves(t), True); + + // Make both sets contain the same stuff. + t.fuzzyAnd(c); + EXPECT_EQ(s.proves(t), True); + + // Now t has *different* stuff, x == 10, which given s is false. + t.clear(); + t.fuzzyAnd(Constraint{Eq, {Literal(int32_t(10))}}); + EXPECT_EQ(s.proves(t), False); + + // Same, with x != 10. Now we know it is true. + t.clear(); + t.fuzzyAnd(Constraint{Ne, {Literal(int32_t(10))}}); + EXPECT_EQ(s.proves(t), True); + + // In reverse, we can infer nothing: knowing x != 10 does not say if x == 5. + EXPECT_EQ(t.proves(s), Unknown); +} + +TEST(ConstraintTest, TestSetsUnknown) { + // x != 5 + // x != 10 + AndedConstraintSet s; + s.fuzzyAnd(Constraint{Ne, {Literal(int32_t(5))}}); + s.fuzzyAnd(Constraint{Ne, {Literal(int32_t(10))}}); + + // x != 20, which is unknown by s. + AndedConstraintSet t; + t.fuzzyAnd(Constraint{Ne, {Literal(int32_t(20))}}); + EXPECT_EQ(s.proves(t), Unknown); + + // Add x == 10, which is false by s, and so the whole thing is false. + t.fuzzyAnd(Constraint{Eq, {Literal(int32_t(10))}}); + EXPECT_EQ(s.proves(t), False); +} + +TEST(ConstraintTest, TestOrTrivial) { + // { x == 5 } + AndedConstraintSet s; + s.fuzzyAnd(Constraint{Eq, {Literal(int32_t(5))}}); + + // { } + AndedConstraintSet empty; + + // Anything ORed with the empty set is unchanged. + auto t = s; + t.fuzzyOr(empty); + EXPECT_EQ(t, s); + + // Flipped. + t = empty; + t.fuzzyOr(s); + EXPECT_EQ(t, s); + + // ORing with oneself changes nothing + t = s; + t.fuzzyOr(s); + EXPECT_EQ(t, s); +} + +TEST(ConstraintTest, TestOrImplies) { + // { x == 5 } + AndedConstraintSet s; + s.fuzzyAnd(Constraint{Eq, {Literal(int32_t(5))}}); + + // { x != 10 } + AndedConstraintSet t; + t.fuzzyAnd(Constraint{Ne, {Literal(int32_t(10))}}); + + // ORing these leaves us with x != 10. + auto u = s; + u.fuzzyOr(t); + EXPECT_EQ(u, t); + + // Flipped. + u = t; + u.fuzzyOr(s); + EXPECT_EQ(u, t); +} + +TEST(ConstraintTest, TestMaxCapacity) { + EXPECT_EQ(MaxConstraints, 3); + + // Max out with x != 10, 20, 30 + Constraint not10{Ne, {Literal(int32_t(10))}}; + Constraint not20{Ne, {Literal(int32_t(20))}}; + Constraint not30{Ne, {Literal(int32_t(30))}}; + + AndedConstraintSet s; + s.fuzzyAnd(not10); + s.fuzzyAnd(not20); + s.fuzzyAnd(not30); + + // We can prove all those. + EXPECT_EQ(s.proves(not10), True); + EXPECT_EQ(s.proves(not20), True); + EXPECT_EQ(s.proves(not30), True); + + // Add another, exceeding the capacity. + Constraint not40{Ne, {Literal(int32_t(40))}}; + s.fuzzyAnd(not40); + + // We can prove the old ones but not the new. + EXPECT_EQ(s.proves(not10), True); + EXPECT_EQ(s.proves(not20), True); + EXPECT_EQ(s.proves(not30), True); + EXPECT_EQ(s.proves(not40), Unknown); +} + +// TODO: test a fuzzyOr of { x = 10 } and { x >= 0 }, once we support +// inequalities