From fddc08f94a9f6c7f513e3a1570032e1a1e569189 Mon Sep 17 00:00:00 2001 From: zdjones Date: Fri, 11 Oct 2019 16:04:47 +0100 Subject: [PATCH] [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 TryBot-Result: Gobot Gobot Reviewed-by: Giovanni Bajo Reviewed-by: Keith Randall Reviewed-on: https://go-review.googlesource.com/c/go/+/201060 Run-TryBot: Alexander Rakoczy Reviewed-on: https://team-review.git.corp.google.com/c/golang/go-private/+/575398 Reviewed-by: Filippo Valsorda --- src/cmd/compile/internal/ssa/poset.go | 3 +-- src/cmd/compile/internal/ssa/poset_test.go | 4 ++-- test/prove.go | 22 ++++++++++++++++++++++ 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) { } -- 2.48.1