cmd/compile: make poset use sufficient conditions for OrderedOrEqual
When assessing whether A <= B, the poset's OrderedOrEqual has a passing
condition which permits A <= B, but is not sufficient to infer that A <= B.
This CL removes that incorrect passing condition.
Having identified that A and B are in the poset, the method will report that
A <= B if any of these three conditions are true:
(1) A and B are the same node in the poset.
- This means we know that A == B.
(2) There is a directed path, strict or not, from A -> B
- This means we know that, at least, A <= B, but A < B is possible.
(3) There is a directed path from B -> A, AND that path has no strict edges.
- This means we know that B <= A, but do not know that B < A.
In condition (3), we do not have enough information to say that A <= B, rather
we only know that B == A (which satisfies A <= B) is possible. The way I
understand it, a strict edge shows a known, strictly-ordered relation (<) but
the lack of a strict edge does not show the lack of a strictly-ordered relation.
The difference is highlighted by the example in #34802, where a bounds check is
incorrectly removed by prove, such that negative indexes into a slice
succeed:
n := make([]int, 1)
for i := -1; i <= 0; i++ {
fmt.Printf("i is %d\n", i)
n[i] = 1 // No Bounds check, program runs, assignment to n[-1] succeeds!!
}
When prove is checking the negative/failed branch from the bounds check at n[i],
in the signed domain we learn (0 > i || i >= len(n)). Because prove can't learn
the OR condition, we check whether we know that i is non-negative so we can
learn something, namely that i >= len(n). Prove uses the poset to check whether
we know that i is non-negative. At this point the poset holds the following
relations as a directed graph:
-1 <= i <= 0
-1 < 0
In poset.OrderedOrEqual, we are testing for 0 <= i. In this case, condition (3)
above is true because there is a non-strict path from i -> 0, and that path
does NOT have any strict edges. Because this condition is true, the poset
reports to prove that i is known to be >= 0. Knowing, incorrectly, that i >= 0,
prove learns from the failed bounds check that i >= len(n) in the signed domain.
When the slice, n, was created, prove learned that len(n) == 1. Because i is
also the induction variable for the loop, upon entering the loop, prove previously
learned that i is in [-1,0]. So when prove attempts to learn from the failed
bounds check, it finds the new fact, i > len(n), unsatisfiable given that it
previously learned that i <= 0 and len(n) = 1.
Fixes #34802
Change-Id: I235f4224bef97700c3aa5c01edcc595eb9f13afc
Reviewed-on: https://go-review.googlesource.com/c/go/+/200759
Run-TryBot: Zach Jones <zachj1@gmail.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: Giovanni Bajo <rasky@develer.com>
Reviewed-by: Keith Randall <khr@golang.org>
diff --git a/src/cmd/compile/internal/ssa/poset.go b/src/cmd/compile/internal/ssa/poset.go
index 378ecc9..e74cabb 100644
--- a/src/cmd/compile/internal/ssa/poset.go
+++ b/src/cmd/compile/internal/ssa/poset.go
@@ -813,8 +813,7 @@
return false
}
- return i1 == i2 || po.reaches(i1, i2, false) ||
- (po.reaches(i2, i1, false) && !po.reaches(i2, i1, true))
+ return i1 == i2 || po.reaches(i1, i2, false)
}
// Equal reports whether n1==n2. It returns false either when it is
diff --git a/src/cmd/compile/internal/ssa/poset_test.go b/src/cmd/compile/internal/ssa/poset_test.go
index 0a4f991..6f048a3 100644
--- a/src/cmd/compile/internal/ssa/poset_test.go
+++ b/src/cmd/compile/internal/ssa/poset_test.go
@@ -184,7 +184,7 @@
{OrderedOrEqual, 4, 12},
{OrderedOrEqual_Fail, 12, 4},
{OrderedOrEqual, 4, 7},
- {OrderedOrEqual, 7, 4},
+ {OrderedOrEqual_Fail, 7, 4},
// Dag #1: 1<4<=7<12
{Checkpoint, 0, 0},
@@ -448,7 +448,7 @@
{SetOrderOrEqual, 20, 100},
{SetOrder, 100, 110},
{OrderedOrEqual, 10, 30},
- {OrderedOrEqual, 30, 10},
+ {OrderedOrEqual_Fail, 30, 10},
{Ordered_Fail, 10, 30},
{Ordered_Fail, 30, 10},
{Ordered, 10, 40},
diff --git a/test/prove.go b/test/prove.go
index 00fc94e..eba0f79 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -934,6 +934,28 @@
return 0
}
+// Ensure that bounds checks with negative indexes are not incorrectly removed.
+func negIndex() {
+ n := make([]int, 1)
+ for i := -1; i <= 0; i++ { // ERROR "Induction variable: limits \[-1,0\], increment 1$"
+ n[i] = 1
+ }
+}
+func negIndex2(n int) {
+ a := make([]int, 5)
+ b := make([]int, 5)
+ c := make([]int, 5)
+ for i := -1; i <= 0; i-- {
+ b[i] = i
+ n++
+ if n > 10 {
+ break
+ }
+ }
+ useSlice(a)
+ useSlice(c)
+}
+
//go:noinline
func useInt(a int) {
}
