Skip to content

Constraints: Propagate constants when proving #9047

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

Open
kripken wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Constraints: Propagate constants when proving #9047

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
13 changes: 13 additions & 0 deletions src/ir/constraint.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -996,6 +996,19 @@ void BasicBlockConstraintMap::approximateAndInternal(Index index,
}
}

Result BasicBlockConstraintMap::proves(LocalConstraint condition) const {

@aheejin aheejin Aug 27, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we plan to do more here? Like, if the otherConstraints is not equal to a literal but less than / greater than a literal, that also can help prove or disprove a constraint.

// As in approximateAnd, above, if the term is a local that we know something
// about, propagate it.
if (auto* other = std::get_if<Index>(&condition.constraint.term)) {
auto otherConstraints = get(*other);
if (auto lit = otherConstraints.getLiteral()) {
condition.constraint.term = Term{*lit};
}
}

return get(condition.local).proves(condition.constraint);
}

void BasicBlockConstraintMap::noteRefs(Index index, const Constraint& c) {
if (auto* i = std::get_if<Index>(&c.term)) {
refs[*i].insert(index);
Expand Down
5 changes: 2 additions & 3 deletions src/ir/constraint.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -319,9 +319,8 @@ struct BasicBlockConstraintMap {
approximateAndInternal(index, c);
}

// TODO: Add proves() here, which could do things like: if asked x == y, we
// can answer False if we see x == c1, y == c2, and the constants c1, c2
// differ.
// Check a condition on a local, given all we know about all other locals.
Result proves(LocalConstraint condition) const;

bool operator!=(const BasicBlockConstraintMap& other) {
return unreachable != other.unreachable || map != other.map;
Expand Down
3 changes: 1 addition & 2 deletions src/passes/ConstraintAnalysis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -439,8 +439,7 @@ struct ConstraintAnalysis
return;
}

auto localConstraints = constraints.get(parsed->local);
Result result = localConstraints.proves(parsed->constraint);
auto result = constraints.proves(*parsed);
if (result == Unknown) {
// If we parsed something using two locals, like x != y, we can also look
// for the flipped condition among y's constraints TODO
Expand Down
13 changes: 4 additions & 9 deletions test/lit/passes/constraint-analysis-loops.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1526,10 +1526,7 @@
;; CHECK-NEXT: (local $y i32)
;; CHECK-NEXT: (loop $loop
;; CHECK-NEXT: (br_if $loop
;; CHECK-NEXT: (i32.lt_s
;; CHECK-NEXT: (local.get $x)
;; CHECK-NEXT: (local.get $y)
;; CHECK-NEXT: )
;; CHECK-NEXT: (i32.const 0)
;; CHECK-NEXT: )
;; CHECK-NEXT: )
;; CHECK-NEXT: )
Expand All @@ -1538,7 +1535,8 @@
(local $y i32)
(loop $loop
;; x == y == 0, so x < y leads to a contradiction, and we never branch
;; back up to the loop. We should not error here.
;; back up to the loop. We should not error here, and in fact infer a 0
;; for this condition.
(br_if $loop
(i32.lt_s
(local.get $x)
Expand All @@ -1553,10 +1551,7 @@
;; CHECK-NEXT: (local $y i32)
;; CHECK-NEXT: (loop $loop
;; CHECK-NEXT: (br_if $loop
;; CHECK-NEXT: (i32.lt_u
;; CHECK-NEXT: (local.get $x)
;; CHECK-NEXT: (local.get $y)
;; CHECK-NEXT: )
;; CHECK-NEXT: (i32.const 0)
;; CHECK-NEXT: )
;; CHECK-NEXT: )
;; CHECK-NEXT: )
Expand Down
39 changes: 10 additions & 29 deletions test/lit/passes/constraint-analysis.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1483,10 +1483,7 @@
;; 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: (i32.const 0)
;; CHECK-NEXT: (then
;; CHECK-NEXT: (drop
;; CHECK-NEXT: (unreachable)
Expand All @@ -1501,10 +1498,7 @@
;; 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: (i32.const 0)
;; OPTIN-NEXT: (then
;; OPTIN-NEXT: (drop
;; OPTIN-NEXT: (unreachable)
Expand All @@ -1521,7 +1515,8 @@
;; $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.
;; ending up in $y with $y == 1 && $y == 0. We can also infer 0 for the if
;; condition.
(if
(i32.eq
(local.get $y)
Expand Down Expand Up @@ -4722,10 +4717,7 @@
;; CHECK-NEXT: )
;; CHECK-NEXT: )
;; CHECK-NEXT: (drop
;; CHECK-NEXT: (i32.eq
;; CHECK-NEXT: (local.get $x)
;; CHECK-NEXT: (local.get $w)
;; CHECK-NEXT: )
;; CHECK-NEXT: (i32.const 0)
;; CHECK-NEXT: )
;; CHECK-NEXT: )
;; OPTIN: (func $fallthrough-get (type $1)
Expand All @@ -4746,10 +4738,7 @@
;; OPTIN-NEXT: )
;; OPTIN-NEXT: )
;; OPTIN-NEXT: (drop
;; OPTIN-NEXT: (i32.eq
;; OPTIN-NEXT: (local.get $x)
;; OPTIN-NEXT: (local.get $w)
;; OPTIN-NEXT: )
;; OPTIN-NEXT: (i32.const 0)
;; OPTIN-NEXT: )
;; OPTIN-NEXT: )
(func $fallthrough-get
Expand Down Expand Up @@ -4777,8 +4766,7 @@

;; 0 == 42 is 0 at runtime. If we did not mark $z as relevant, we would see
;; $x and $w as both equal to $z, i.e., that they are themselves equal, and
;; misoptimize this to 1. The actual value at runtime is 0.
;; TODO: actually optimize this to 0
;; misoptimize this to 1. We optimize to 0 here.
(drop
(i32.eq
(local.get $x)
Expand All @@ -4805,10 +4793,7 @@
;; CHECK-NEXT: )
;; CHECK-NEXT: )
;; CHECK-NEXT: (drop
;; CHECK-NEXT: (i32.eq
;; CHECK-NEXT: (local.get $x)
;; CHECK-NEXT: (local.get $w)
;; CHECK-NEXT: )
;; CHECK-NEXT: (i32.const 0)
;; CHECK-NEXT: )
;; CHECK-NEXT: )
;; OPTIN: (func $fallthrough-tee (type $0) (param $param i32)
Expand All @@ -4829,10 +4814,7 @@
;; OPTIN-NEXT: )
;; OPTIN-NEXT: )
;; OPTIN-NEXT: (drop
;; OPTIN-NEXT: (i32.eq
;; OPTIN-NEXT: (local.get $x)
;; OPTIN-NEXT: (local.get $w)
;; OPTIN-NEXT: )
;; OPTIN-NEXT: (i32.const 0)
;; OPTIN-NEXT: )
;; OPTIN-NEXT: )
(func $fallthrough-tee (param $param i32)
Expand All @@ -4854,8 +4836,7 @@
)
)

;; As before, this should not be optimized to 1, and could be optimized to
;; 0 (TODO).
;; As before, this is optimized to 0.
(drop
(i32.eq
(local.get $x)
Expand Down
Loading