cmd/compile/internal/ssa: prove support induction variable pair

We have two induction variables i and j in the following loop:

for i, j := 0, len(s)-1; i < j; i, j = i+1, j-1 {
    // loop body
}

This CL enables the prove pass to handle cases where one if block
uses two induction variables.

Updates #45078

Change-Id: I8b8dc8b7b2d160a796dab1d1e29a00ef4e8e8157
Reviewed-on: https://go-review.googlesource.com/c/go/+/757700
Auto-Submit: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
Reviewed-by: Dmitri Shuralyov <dmitshur@google.com>
Reviewed-by: Keith Randall <khr@golang.org>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>

1 files changed, 18 insertions, 0 deletions

diff --git a/test/prove.go b/test/prove.go
index c1815f2bfb..30f5e77e76 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -2527,6 +2527,24 @@ func ex76269shouldNotIndVar() {
 	}
 }
 
+func issue45078reverse(s []int) {
+	for i, j := 0, len(s)-1; i < j; i, j = i+1, j-1 { // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Induction variable: limits \(\?,\?\], increment 1$"
+		tmp := s[i] // ERROR "Proved IsInBounds$"
+		s[i] = s[j] // ERROR "Proved IsInBounds$"
+		s[j] = tmp  // ERROR "Proved IsInBounds$"
+	}
+}
+
+func ex45078reverse(s []int, low, high int) {
+	if low >= 0 && high < len(s) {
+		for i, j := low, high; i < j; i, j = i+1, j-1 { // ERROR "Induction variable: limits \[\?,\?\), increment 1$" "Induction variable: limits \(\?,\?\], increment 1$"
+			tmp := s[i] // ERROR "Proved IsInBounds$"
+			s[i] = s[j] // ERROR "Proved IsInBounds$"
+			s[j] = tmp  // ERROR "Proved IsInBounds$"
+		}
+	}
+}
+
 func mulIntoAnd(a, b uint) uint {
 	if a > 1 || b > 1 {
 		return 0