package ssa
-import "math"
+import (
+ "fmt"
+ "math"
+)
type branch int
umin, umax uint64 // umin <= value <= umax, unsigned
}
+func (l limit) String() string {
+ return fmt.Sprintf("sm,SM,um,UM=%d,%d,%d,%d", l.min, l.max, l.umin, l.umax)
+}
+
var noLimit = limit{math.MinInt64, math.MaxInt64, 0, math.MaxUint64}
// a limitFact is a limit known for a particular value.
// update updates the set of relations between v and w in domain d
// restricting it to r.
-func (ft *factsTable) update(v, w *Value, d domain, r relation) {
+func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
if lessByID(w, v) {
v, w = w, v
r = reverseBits[r]
}
ft.limitStack = append(ft.limitStack, limitFact{v.ID, old})
ft.limits[v.ID] = lim
+ if v.Block.Func.pass.debug > 2 {
+ v.Block.Func.Config.Warnl(parent.Line, "parent=%s, new limits %s %s %s", parent, v, w, lim.String())
+ }
}
}
if branch != unknown {
ft.checkpoint()
c := parent.Control
- updateRestrictions(ft, boolean, nil, c, lt|gt, branch)
+ updateRestrictions(parent, ft, boolean, nil, c, lt|gt, branch)
if tr, has := domainRelationTable[parent.Control.Op]; has {
// When we branched from parent we learned a new set of
// restrictions. Update the factsTable accordingly.
- updateRestrictions(ft, tr.d, c.Args[0], c.Args[1], tr.r, branch)
+ updateRestrictions(parent, ft, tr.d, c.Args[0], c.Args[1], tr.r, branch)
}
}
// updateRestrictions updates restrictions from the immediate
// dominating block (p) using r. r is adjusted according to the branch taken.
-func updateRestrictions(ft *factsTable, t domain, v, w *Value, r relation, branch branch) {
+func updateRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r relation, branch branch) {
if t == 0 || branch == unknown {
// Trivial case: nothing to do, or branch unknown.
// Shoult not happen, but just in case.
}
for i := domain(1); i <= t; i <<= 1 {
if t&i != 0 {
- ft.update(v, w, i, r)
+ ft.update(parent, v, w, i, r)
}
}
}
m := ft.get(nil, b.Control, boolean)
if m == lt|gt {
if b.Func.pass.debug > 0 {
- b.Func.Config.Warnl(b.Line, "Proved boolean %s", b.Control.Op)
+ if b.Func.pass.debug > 1 {
+ b.Func.Config.Warnl(b.Line, "Proved boolean %s (%s)", b.Control.Op, b.Control)
+ } else {
+ b.Func.Config.Warnl(b.Line, "Proved boolean %s", b.Control.Op)
+ }
}
return positive
}
if m == eq {
if b.Func.pass.debug > 0 {
- b.Func.Config.Warnl(b.Line, "Disproved boolean %s", b.Control.Op)
+ if b.Func.pass.debug > 1 {
+ b.Func.Config.Warnl(b.Line, "Disproved boolean %s (%s)", b.Control.Op, b.Control)
+ } else {
+ b.Func.Config.Warnl(b.Line, "Disproved boolean %s", b.Control.Op)
+ }
}
return negative
}
m := ft.get(a0, a1, d)
if m != 0 && tr.r&m == m {
if b.Func.pass.debug > 0 {
- b.Func.Config.Warnl(b.Line, "Proved %s", c.Op)
+ if b.Func.pass.debug > 1 {
+ b.Func.Config.Warnl(b.Line, "Proved %s (%s)", c.Op, c)
+ } else {
+ b.Func.Config.Warnl(b.Line, "Proved %s", c.Op)
+ }
}
return positive
}
if m != 0 && ((lt|eq|gt)^tr.r)&m == m {
if b.Func.pass.debug > 0 {
- b.Func.Config.Warnl(b.Line, "Disproved %s", c.Op)
+ if b.Func.pass.debug > 1 {
+ b.Func.Config.Warnl(b.Line, "Disproved %s (%s)", c.Op, c)
+ } else {
+ b.Func.Config.Warnl(b.Line, "Disproved %s", c.Op)
+ }
}
return negative
}
m := ft.get(a0, a1, signed)
if m != 0 && tr.r&m == m {
if b.Func.pass.debug > 0 {
- b.Func.Config.Warnl(b.Line, "Proved non-negative bounds %s", c.Op)
+ if b.Func.pass.debug > 1 {
+ b.Func.Config.Warnl(b.Line, "Proved non-negative bounds %s (%s)", c.Op, c)
+ } else {
+ b.Func.Config.Warnl(b.Line, "Proved non-negative bounds %s", c.Op)
+ }
}
return positive
}
case OpConst64:
return v.AuxInt >= 0
+ case OpConst32:
+ return int32(v.AuxInt) >= 0
+
case OpStringLen, OpSliceLen, OpSliceCap,
OpZeroExt8to64, OpZeroExt16to64, OpZeroExt32to64:
return true
--- /dev/null
+// errorcheck -0 -d=append,slice,ssa/prove/debug=1
+
+// Copyright 2015 The Go Authors. All rights reserved.
+// Use of this source code is governed by a BSD-style
+// license that can be found in the LICENSE file.
+
+// Check optimization results for append and slicing.
+
+package main
+
+func a1(x []int, y int) []int {
+ x = append(x, y) // ERROR "append: len-only update \(in local slice\)$"
+ return x
+}
+
+func a2(x []int, y int) []int {
+ return append(x, y)
+}
+
+func a3(x *[]int, y int) {
+ *x = append(*x, y) // ERROR "append: len-only update$"
+}
+
+// s1_if_false_then_anything
+func s1_if_false_then_anything(x **[]int, xs **string, i, j int) {
+ z := (**x)[0:i]
+ z = z[i : i+1]
+ println(z) // if we get here, then we have proven that i==i+1 (this cannot happen, but the program is still being analyzed...)
+
+ zs := (**xs)[0:i] // since i=i+1 is proven, i+1 is "in bounds", ha-ha
+ zs = zs[i : i+1] // ERROR "Proved boolean IsSliceInBounds$"
+ println(zs)
+}
+
+func s1(x **[]int, xs **string, i, j int) {
+ var z []int
+ z = (**x)[2:]
+ z = (**x)[2:len(**x)] // ERROR "Proved boolean IsSliceInBounds$"
+ z = (**x)[2:cap(**x)] // ERROR "Proved IsSliceInBounds$"
+ z = (**x)[i:i] // -ERROR "Proved IsSliceInBounds"
+ z = (**x)[1:i:i] // ERROR "Proved boolean IsSliceInBounds$"
+ z = (**x)[i:j:0]
+ z = (**x)[i:0:j] // ERROR "Disproved IsSliceInBounds$"
+ z = (**x)[0:i:j] // ERROR "Proved boolean IsSliceInBounds$"
+ z = (**x)[0:] // ERROR "slice: omit slice operation$"
+ z = (**x)[2:8] // ERROR "Disproved Eq(32|64)$"
+ z = (**x)[2:2] // ERROR "Disproved Eq(32|64)$" "Proved boolean IsSliceInBounds$"
+ z = (**x)[0:i] // ERROR "Proved boolean IsSliceInBounds$"
+ z = (**x)[2:i:8] // ERROR "Disproved IsSliceInBounds$" "Proved IsSliceInBounds$" "Proved boolean IsSliceInBounds$"
+ z = (**x)[i:2:i] // ERROR "Proved IsSliceInBounds$" "Proved boolean IsSliceInBounds$"
+
+ z = z[0:i] // ERROR "Proved boolean IsSliceInBounds"
+ z = z[0:i : i+1]
+ z = z[i : i+1] // ERROR "Proved boolean IsSliceInBounds$"
+
+ println(z)
+
+ var zs string
+ zs = (**xs)[2:]
+ zs = (**xs)[2:len(**xs)] // ERROR "Proved IsSliceInBounds$" "Proved boolean IsSliceInBounds$"
+ zs = (**xs)[i:i] // -ERROR "Proved boolean IsSliceInBounds"
+ zs = (**xs)[0:] // ERROR "slice: omit slice operation$"
+ zs = (**xs)[2:8]
+ zs = (**xs)[2:2] // ERROR "Proved boolean IsSliceInBounds$"
+ zs = (**xs)[0:i] // ERROR "Proved boolean IsSliceInBounds$"
+
+ zs = zs[0:i] // See s1_if_false_then_anything above to explain the counterfactual bounds check result below
+ zs = zs[i : i+1] // ERROR "Proved boolean IsSliceInBounds$"
+ println(zs)
+}