cmd/compile: access to negative slice indices improperly permitted #34802
Milestone
Comments
|
Interesting. This succeeds on 1.13.1 and master, but fails on 1.12.9. Sounds like a regression somewhere. Perhaps because of the recent improvements to the prove pass? /cc @randall77 @rasky @zdjones |
|
Bisected to ddef157 |
This comment was marked as off-topic.
This comment was marked as off-topic.
ianlancetaylor
changed the title
|
@gopherbot Please open a backport to 1.13. If this is indeed a compiler bug present in 1.13, we should backport it. |
|
Backport issue(s) opened: #34807 (for 1.13). Remember to create the cherry-pick CL(s) as soon as the patch is submitted to master, according to https://golang.org/wiki/MinorReleases. |
This comment was marked as off-topic.
This comment was marked as off-topic.
|
There are tests that check that negative indexes panic. Those tests just don't cover this case (induction variable which starts at a negative value). |
|
@randall77 could a negative index corrupt memory in this case? |
|
I'll look into this in detail tomorrow. |
|
@networkimprov yes, it can overwrite values on the stack. $ cat x.go
package main
import (
"fmt"
)
var n int
func main() {
var a [5]int
var b [5]int
var c [5]int
for i := -1; i <= 0; i-- {
b[i] = i
n++
if n > 100 {
break
}
}
for i := range a {
fmt.Println(a[i], b[i], c[i])
}
}
0:1 /tmp $ go run x.go
0 0 -5
0 0 -4
0 0 -3
0 0 -2
0 0 -1 |
|
Found the issue, mailing the fix shortly. |
|
Change https://golang.org/cl/200759 mentions this issue: |
|
Change https://golang.org/cl/201060 mentions this issue: |
gopherbot
pushed a commit
that referenced
this issue
Oct 14, 2019
…ions 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>
gopherbot
pushed a commit
that referenced
this issue
Oct 17, 2019
…nt 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>
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
What version of Go are you using (
go version)?go version go1.13.1 darwin/amd64
Does this issue reproduce with the latest release?
Yes
What operating system and processor architecture are you using (
go env)?GO111MODULE=""
GOARCH="amd64"
GOBIN=""
GOCACHE="/Users/aaron/Library/Caches/go-build"
GOENV="/Users/aaron/Library/Application Support/go/env"
GOEXE=""
GOFLAGS=""
GOHOSTARCH="amd64"
GOHOSTOS="darwin"
GONOPROXY=""
GONOSUMDB=""
GOOS="darwin"
GOPATH="/Users/aaron/go"
GOPRIVATE=""
GOPROXY="https://proxy.golang.org,direct"
GOROOT="/usr/local/go"
GOSUMDB="sum.golang.org"
GOTMPDIR=""
GOTOOLDIR="/usr/local/go/pkg/tool/darwin_amd64"
GCCGO="gccgo"
AR="ar"
CC="clang"
CXX="clang++"
CGO_ENABLED="1"
GOMOD=""
CGO_CFLAGS="-g -O2"
CGO_CPPFLAGS=""
CGO_CXXFLAGS="-g -O2"
CGO_FFLAGS="-g -O2"
CGO_LDFLAGS="-g -O2"
PKG_CONFIG="pkg-config"
GOGCCFLAGS="-fPIC -m64 -pthread -fno-caret-diagnostics -Qunused-arguments -fmessage-length=0 -fdebug-prefix-map=/var/folders/n0/33wyl5yn1x77xsgjmz3p53zw0000gn/T/go-build007240201=/tmp/go-build -gno-record-gcc-switches -fno-common"
What did you do?
Accessed a negative slice index. Example: https://play.golang.org/p/Abpv3H1sgol
What did you expect to see?
Expected to see error
What did you see instead?
No error
The text was updated successfully, but these errors were encountered: