[release-branch.go1.13-security] 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 #34807

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>
Reviewed-on: https://go-review.googlesource.com/c/go/+/201060
Run-TryBot: Alexander Rakoczy <alex@golang.org>
Reviewed-on: https://team-review.git.corp.google.com/c/golang/go-private/+/575398
Reviewed-by: Filippo Valsorda <valsorda@google.com>

3 files changed, 25 insertions, 4 deletions

diff --git a/src/cmd/compile/internal/ssa/poset.go b/src/cmd/compile/internal/ssa/poset.go
index 071297f8fa..cf966c924c 100644
--- a/src/cmd/compile/internal/ssa/poset.go
+++ b/src/cmd/compile/internal/ssa/poset.go
@@ -814,8 +814,7 @@ func (po *poset) OrderedOrEqual(n1, n2 *Value) bool {
 		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 cb739d9a0c..92c818a601 100644
--- a/src/cmd/compile/internal/ssa/poset_test.go
+++ b/src/cmd/compile/internal/ssa/poset_test.go
@@ -186,7 +186,7 @@ func TestPoset(t *testing.T) {
 		{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},
@@ -450,7 +450,7 @@ func TestSetEqual(t *testing.T) {
 		{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 6e92b9eec2..f6dd9f0955 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -853,6 +853,28 @@ func unrollIncMin(a []int) int {
 	return x
 }
 
+// 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) {
 }