Skip to content

Commit 0d962bc

Browse files
kripkenkripken
authored
Constraints: Fix float comparisons (#9041)
We were doing `Literal == Literal`, but the right semantics are the wasm ones that we are modelling, where `0 == -0` in floats, for example. Use `Literal::eq` instead of `operator==`, and also make `Literal::eq` handle refs properly.
1 parent ad982e2 commit 0d962bc

5 files changed

Lines changed: 142 additions & 39 deletions

File tree

‎src/ir/constraint.cpp‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -170,9 +170,9 @@ Result provesConstantPair(Abstract::Op aOp,
170170
if (aOp == Eq) {
171171
switch (bOp) {
172172
case Eq:
173-
return TrueFalse(aConstant == bConstant);
173+
return TrueFalse(aConstant.eq(bConstant));
174174
case Ne:
175-
return TrueFalse(aConstant != bConstant);
175+
return TrueFalse(aConstant.ne(bConstant));
176176
case LtS:
177177
return TrueFalse(aConstant.ltS(bConstant));
178178
case LeS:
@@ -196,14 +196,14 @@ Result provesConstantPair(Abstract::Op aOp,
196196

197197
// a != A =?=> a == B. False if A = B, else unknown.
198198
if (aOp == Ne && bOp == Eq) {
199-
if (aConstant == bConstant) {
199+
if (aConstant.eq(bConstant).getInteger()) {
200200
return False;
201201
}
202202
}
203203

204204
// a != A =?=> a != B. True if A = B, else unknown.
205205
if (aOp == Ne && bOp == Ne) {
206-
if (aConstant == bConstant) {
206+
if (aConstant.eq(bConstant).getInteger()) {
207207
return True;
208208
}
209209
}
@@ -383,6 +383,10 @@ bool isImmediateContradiction(const Constraint& c) {
383383
return false;
384384
}
385385

386+
if (!cc->type.isInteger()) {
387+
return false;
388+
}
389+
386390
auto minSigned = cc->type == Type::i32 ? std::numeric_limits<int32_t>::min()
387391
: std::numeric_limits<int64_t>::min();
388392
auto maxSigned = cc->type == Type::i32 ? std::numeric_limits<int32_t>::max()

‎src/literal.h‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -358,9 +358,9 @@ class Literal {
358358
bool operator!=(const Literal& other) const;
359359
bool operator<(const Literal& other) const;
360360

361-
bool isNaN();
362-
bool isCanonicalNaN();
363-
bool isArithmeticNaN();
361+
bool isNaN() const;
362+
bool isCanonicalNaN() const;
363+
bool isArithmeticNaN() const;
364364

365365
static uint32_t NaNPayload(float f);
366366
static uint64_t NaNPayload(double f);
@@ -425,9 +425,10 @@ class Literal {
425425
Literal rotL(const Literal& other) const;
426426
Literal rotR(const Literal& other) const;
427427

428-
// Note that these functions perform equality checks based
429-
// on the type of the literal, so that (unlike the == operator)
430-
// a float nan would not be identical to itself.
428+
// Note that these functions perform equality checks based on the type of the
429+
// literal, and using the wasm semantics. That is, eq() works like i32.eq or
430+
// ref.eq. For example, f32.eq of 0 and -0 returns 1 (they are equal), while
431+
// the == operator would return false (because they are different Literals).
431432
Literal eq(const Literal& other) const;
432433
Literal ne(const Literal& other) const;
433434
Literal ltS(const Literal& other) const;

‎src/wasm/literal.cpp‎

Lines changed: 45 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -583,7 +583,7 @@ bool Literal::operator<(const Literal& other) const {
583583
return externalize() < other.externalize();
584584
}
585585

586-
bool Literal::isNaN() {
586+
bool Literal::isNaN() const {
587587
if (type == Type::f32 && std::isnan(getf32())) {
588588
return true;
589589
}
@@ -594,15 +594,15 @@ bool Literal::isNaN() {
594594
return false;
595595
}
596596

597-
bool Literal::isCanonicalNaN() {
597+
bool Literal::isCanonicalNaN() const {
598598
if (!isNaN()) {
599599
return false;
600600
}
601601
return (type == Type::f32 && NaNPayload(getf32()) == (1u << 22)) ||
602602
(type == Type::f64 && NaNPayload(getf64()) == (1ull << 51));
603603
}
604604

605-
bool Literal::isArithmeticNaN() {
605+
bool Literal::isArithmeticNaN() const {
606606
if (!isNaN()) {
607607
return false;
608608
}
@@ -1602,37 +1602,53 @@ Literal Literal::rotR(const Literal& other) const {
16021602
}
16031603

16041604
Literal Literal::eq(const Literal& other) const {
1605-
switch (type.getBasic()) {
1606-
case Type::i32:
1607-
return Literal(i32 == other.i32);
1608-
case Type::i64:
1609-
return Literal(i64 == other.i64);
1610-
case Type::f32:
1611-
return Literal(getf32() == other.getf32());
1612-
case Type::f64:
1613-
return Literal(getf64() == other.getf64());
1614-
case Type::v128:
1615-
case Type::none:
1616-
case Type::unreachable:
1617-
WASM_UNREACHABLE("unexpected type");
1605+
if (type != other.type) {
1606+
return Literal(int32_t(0));
1607+
}
1608+
if (type.isBasic()) {
1609+
switch (type.getBasic()) {
1610+
case Type::i32:
1611+
return Literal(i32 == other.i32);
1612+
case Type::i64:
1613+
return Literal(i64 == other.i64);
1614+
case Type::f32:
1615+
return Literal(getf32() == other.getf32());
1616+
case Type::f64:
1617+
return Literal(getf64() == other.getf64());
1618+
case Type::v128:
1619+
case Type::none:
1620+
case Type::unreachable:
1621+
WASM_UNREACHABLE("unexpected type");
1622+
}
1623+
}
1624+
if (type.isRef()) {
1625+
return Literal(int32_t(*this == other));
16181626
}
16191627
WASM_UNREACHABLE("unexpected type");
16201628
}
16211629

16221630
Literal Literal::ne(const Literal& other) const {
1623-
switch (type.getBasic()) {
1624-
case Type::i32:
1625-
return Literal(i32 != other.i32);
1626-
case Type::i64:
1627-
return Literal(i64 != other.i64);
1628-
case Type::f32:
1629-
return Literal(getf32() != other.getf32());
1630-
case Type::f64:
1631-
return Literal(getf64() != other.getf64());
1632-
case Type::v128:
1633-
case Type::none:
1634-
case Type::unreachable:
1635-
WASM_UNREACHABLE("unexpected type");
1631+
if (type != other.type) {
1632+
return Literal(int32_t(1));
1633+
}
1634+
if (type.isBasic()) {
1635+
switch (type.getBasic()) {
1636+
case Type::i32:
1637+
return Literal(i32 != other.i32);
1638+
case Type::i64:
1639+
return Literal(i64 != other.i64);
1640+
case Type::f32:
1641+
return Literal(getf32() != other.getf32());
1642+
case Type::f64:
1643+
return Literal(getf64() != other.getf64());
1644+
case Type::v128:
1645+
case Type::none:
1646+
case Type::unreachable:
1647+
WASM_UNREACHABLE("unexpected type");
1648+
}
1649+
}
1650+
if (type.isRef()) {
1651+
return Literal(int32_t(*this != other));
16361652
}
16371653
WASM_UNREACHABLE("unexpected type");
16381654
}

‎test/gtest/constraint.cpp‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1174,3 +1174,31 @@ TEST(ConstraintTest, GetSpanGC) {
11741174
EXPECT_EQ((Constraint{Eq, {Literal::makeNull(HeapType::eq)}}.getSpan()),
11751175
std::nullopt);
11761176
}
1177+
1178+
TEST(ConstraintTest, FloatNegativeZero) {
1179+
// f == 0.0 proves f == -0.0 is True.
1180+
AndedConstraintSet s;
1181+
s.set(Constraint{Eq, {Literal(double(0.0))}});
1182+
EXPECT_EQ(s.proves(Constraint{Eq, {Literal(double(-0.0))}}), True);
1183+
EXPECT_EQ(s.proves(Constraint{Ne, {Literal(double(-0.0))}}), False);
1184+
EXPECT_EQ(s.proves(Constraint{Eq, {Literal(double(1.0))}}), False);
1185+
EXPECT_EQ(s.proves(Constraint{Ne, {Literal(double(1.0))}}), True);
1186+
1187+
// f == -0.0 proves f == 0.0 is True.
1188+
AndedConstraintSet sNeg;
1189+
sNeg.set(Constraint{Eq, {Literal(double(-0.0))}});
1190+
EXPECT_EQ(sNeg.proves(Constraint{Eq, {Literal(double(0.0))}}), True);
1191+
EXPECT_EQ(sNeg.proves(Constraint{Ne, {Literal(double(0.0))}}), False);
1192+
1193+
// f != 0.0 proves f == -0.0 is False, and f != -0.0 is True.
1194+
AndedConstraintSet sNe;
1195+
sNe.set(Constraint{Ne, {Literal(double(0.0))}});
1196+
EXPECT_EQ(sNe.proves(Constraint{Eq, {Literal(double(-0.0))}}), False);
1197+
EXPECT_EQ(sNe.proves(Constraint{Ne, {Literal(double(-0.0))}}), True);
1198+
1199+
// Same for f32.
1200+
AndedConstraintSet s32;
1201+
s32.set(Constraint{Eq, {Literal(float(0.0f))}});
1202+
EXPECT_EQ(s32.proves(Constraint{Eq, {Literal(float(-0.0f))}}), True);
1203+
EXPECT_EQ(s32.proves(Constraint{Ne, {Literal(float(-0.0f))}}), False);
1204+
}

‎test/lit/passes/constraint-analysis.wast‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4556,6 +4556,60 @@
45564556
)
45574557
)
45584558

4559+
;; CHECK: (func $float-negative-zero (type $1)
4560+
;; CHECK-NEXT: (local $f f64)
4561+
;; CHECK-NEXT: (if
4562+
;; CHECK-NEXT: (i32.const 1)
4563+
;; CHECK-NEXT: (then
4564+
;; CHECK-NEXT: (nop)
4565+
;; CHECK-NEXT: )
4566+
;; CHECK-NEXT: )
4567+
;; CHECK-NEXT: (if
4568+
;; CHECK-NEXT: (i32.const 1)
4569+
;; CHECK-NEXT: (then
4570+
;; CHECK-NEXT: (nop)
4571+
;; CHECK-NEXT: )
4572+
;; CHECK-NEXT: )
4573+
;; CHECK-NEXT: )
4574+
;; OPTIN: (func $float-negative-zero (type $1)
4575+
;; OPTIN-NEXT: (local $f f64)
4576+
;; OPTIN-NEXT: (if
4577+
;; OPTIN-NEXT: (i32.const 1)
4578+
;; OPTIN-NEXT: (then
4579+
;; OPTIN-NEXT: (nop)
4580+
;; OPTIN-NEXT: )
4581+
;; OPTIN-NEXT: )
4582+
;; OPTIN-NEXT: (if
4583+
;; OPTIN-NEXT: (i32.const 1)
4584+
;; OPTIN-NEXT: (then
4585+
;; OPTIN-NEXT: (nop)
4586+
;; OPTIN-NEXT: )
4587+
;; OPTIN-NEXT: )
4588+
;; OPTIN-NEXT: )
4589+
(func $float-negative-zero
4590+
(local $f f64)
4591+
;; Negative zero is equal to zero, even though it has a different bit
4592+
;; pattern. Both conditions here should be optimized to 1.
4593+
(if
4594+
(f64.eq
4595+
(local.get $f)
4596+
(f64.const -0)
4597+
)
4598+
(then
4599+
(nop)
4600+
)
4601+
)
4602+
(if
4603+
(f64.eq
4604+
(local.get $f)
4605+
(f64.const 0)
4606+
)
4607+
(then
4608+
(nop)
4609+
)
4610+
)
4611+
)
4612+
45594613
;; CHECK: (func $tee (type $1)
45604614
;; CHECK-NEXT: (local $x i32)
45614615
;; CHECK-NEXT: (local $y i32)

0 commit comments

Comments
 (0)