Skip to content

ConstraintAnalysis: Handle contradictions we find during other work #8906

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kripken merged 2 commits into from
Jul 15, 2026
+73 −0
Merged

ConstraintAnalysis: Handle contradictions we find during other work #8906

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0917a82
go
kripken Jul 14, 2026
4972466
test
kripken Jul 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions src/ir/constraint.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -330,6 +330,9 @@ void BasicBlockConstraintMap::approximateAndInternal(Index index,
const Constraint& c,
bool flip,
bool isCopy) {
// We should not be applying constraints when already unreachable.
assert(!unreachable);

Constraint actual = c;
if (flip) {
LocalConstraint flipped{index, c};
Expand Down Expand Up @@ -377,6 +380,10 @@ void BasicBlockConstraintMap::approximateAndInternal(Index index,
// flipped one too.
if (!flip && std::holds_alternative<Index>(actual.term)) {
approximateAndInternal(index, actual, true, isCopy);
if (unreachable) {
// We just found a contradiction.
return;
}
}

// If this constraint is simply "== x", then we are equal to that other local
Expand All @@ -386,6 +393,9 @@ void BasicBlockConstraintMap::approximateAndInternal(Index index,
if (actual.op == Abstract::Eq) {
for (auto& otherC : get(*other)) {
approximateAndInternal(index, otherC, false, true);
if (unreachable) {
return;
}
}
}
}
Expand Down
63 changes: 63 additions & 0 deletions test/lit/passes/constraint-analysis.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1317,6 +1317,69 @@
)
)

;; CHECK: (func $contadiction-during-flipping (type $1)
;; CHECK-NEXT: (local $x i32)
;; CHECK-NEXT: (local $y i32)
;; CHECK-NEXT: (local.set $y
;; CHECK-NEXT: (i32.const 1)
;; CHECK-NEXT: )
;; CHECK-NEXT: (if
;; CHECK-NEXT: (i32.eq
;; CHECK-NEXT: (local.get $y)
;; CHECK-NEXT: (local.get $x)
;; CHECK-NEXT: )
;; CHECK-NEXT: (then
;; CHECK-NEXT: (drop
;; CHECK-NEXT: (unreachable)
;; CHECK-NEXT: )
;; CHECK-NEXT: )
;; CHECK-NEXT: )
;; CHECK-NEXT: )
;; OPTIN: (func $contadiction-during-flipping (type $1)
;; OPTIN-NEXT: (local $x i32)
;; OPTIN-NEXT: (local $y i32)
;; OPTIN-NEXT: (local.set $y
;; OPTIN-NEXT: (i32.const 1)
;; OPTIN-NEXT: )
;; OPTIN-NEXT: (if
;; OPTIN-NEXT: (i32.eq
;; OPTIN-NEXT: (local.get $x)
;; OPTIN-NEXT: (local.get $y)
;; OPTIN-NEXT: )
;; OPTIN-NEXT: (then
;; OPTIN-NEXT: (drop
;; OPTIN-NEXT: (unreachable)
;; OPTIN-NEXT: )
;; OPTIN-NEXT: )
;; OPTIN-NEXT: )
;; OPTIN-NEXT: )
(func $contadiction-during-flipping
(local $x i32)
(local $y i32)
(local.set $y
(i32.const 1)
)
;; $x == 0, $y == 1, so they are never equal, and the if body is
;; unreachable. We find this out while applying the secondary facts of a
;; constraint: we add $y == $x, and then apply $x's constraints to $y,
;; ending up in $y with $y == 1 && $y == 0.
(if
(i32.eq
(local.get $y)
(local.get $x)
)
(then
;; This becomes unreachable.
(drop
(i32.eq
(local.get $y)
(local.get $x)
)
)
)
)
)

;; CHECK: (func $conditional-br_if (type $0) (param $param i32)
;; CHECK-NEXT: (block $block
;; CHECK-NEXT: (drop
Expand Down
Loading