mirror of
https://github.com/golang/go
synced 2024-10-14 03:43:28 +00:00
cmd/compile: in prove, add transitive closure of relations
Implement it through a partial order datastructure, which keeps the relations between SSA values in a forest of DAGs and is able to discover contradictions. In make.bash, this patch is able to prove hundreds of conditions which were not proved before. Compilebench: name old time/op new time/op delta Template 371ms ± 2% 368ms ± 1% ~ (p=0.222 n=5+5) Unicode 203ms ± 6% 199ms ± 3% ~ (p=0.421 n=5+5) GoTypes 1.17s ± 4% 1.18s ± 1% ~ (p=0.151 n=5+5) Compiler 5.54s ± 2% 5.59s ± 1% ~ (p=0.548 n=5+5) SSA 12.9s ± 2% 13.2s ± 1% +2.96% (p=0.032 n=5+5) Flate 245ms ± 2% 247ms ± 3% ~ (p=0.690 n=5+5) GoParser 302ms ± 6% 302ms ± 4% ~ (p=0.548 n=5+5) Reflect 764ms ± 4% 773ms ± 3% ~ (p=0.095 n=5+5) Tar 354ms ± 6% 361ms ± 3% ~ (p=0.222 n=5+5) XML 434ms ± 3% 429ms ± 1% ~ (p=0.421 n=5+5) StdCmd 22.6s ± 1% 22.9s ± 1% +1.40% (p=0.032 n=5+5) name old user-time/op new user-time/op delta Template 436ms ± 8% 426ms ± 5% ~ (p=0.579 n=5+5) Unicode 219ms ±15% 219ms ±12% ~ (p=1.000 n=5+5) GoTypes 1.47s ± 6% 1.53s ± 6% ~ (p=0.222 n=5+5) Compiler 7.26s ± 4% 7.40s ± 2% ~ (p=0.389 n=5+5) SSA 17.7s ± 4% 18.5s ± 4% +4.13% (p=0.032 n=5+5) Flate 257ms ± 5% 268ms ± 9% ~ (p=0.333 n=5+5) GoParser 354ms ± 6% 348ms ± 6% ~ (p=0.913 n=5+5) Reflect 904ms ± 2% 944ms ± 4% ~ (p=0.056 n=5+5) Tar 398ms ±11% 430ms ± 7% ~ (p=0.079 n=5+5) XML 501ms ± 7% 489ms ± 5% ~ (p=0.444 n=5+5) name old text-bytes new text-bytes delta HelloSize 670kB ± 0% 670kB ± 0% +0.00% (p=0.008 n=5+5) CmdGoSize 7.22MB ± 0% 7.21MB ± 0% -0.07% (p=0.008 n=5+5) name old data-bytes new data-bytes delta HelloSize 9.88kB ± 0% 9.88kB ± 0% ~ (all equal) CmdGoSize 248kB ± 0% 248kB ± 0% -0.06% (p=0.008 n=5+5) name old bss-bytes new bss-bytes delta HelloSize 125kB ± 0% 125kB ± 0% ~ (all equal) CmdGoSize 145kB ± 0% 144kB ± 0% -0.20% (p=0.008 n=5+5) name old exe-bytes new exe-bytes delta HelloSize 1.43MB ± 0% 1.43MB ± 0% ~ (all equal) CmdGoSize 14.5MB ± 0% 14.5MB ± 0% -0.06% (p=0.008 n=5+5) Fixes #19714 Updates #20393 Change-Id: Ia090f5b5dc1bcd274ba8a39b233c1e1ace1b330e Reviewed-on: https://go-review.googlesource.com/100277 Run-TryBot: Giovanni Bajo <rasky@develer.com> Reviewed-by: David Chase <drchase@google.com>
This commit is contained in:
Giovanni Bajo
parent
5af0b28a73
commit
5c40210987
|
|
@ -610,6 +610,7 @@ var knownFormats = map[string]string{
|
|||
"[]cmd/compile/internal/ssa.ID %v": "",
|
||||
"[]cmd/compile/internal/syntax.token %s": "",
|
||||
"[]string %v": "",
|
||||
"[]uint32 %v": "",
|
||||
"bool %v": "",
|
||||
"byte %08b": "",
|
||||
"byte %c": "",
|
||||
|
|
@ -645,6 +646,8 @@ var knownFormats = map[string]string{
|
|||
"cmd/compile/internal/ssa.Op %s": "",
|
||||
"cmd/compile/internal/ssa.Op %v": "",
|
||||
"cmd/compile/internal/ssa.ValAndOff %s": "",
|
||||
"cmd/compile/internal/ssa.posetNode %v": "",
|
||||
"cmd/compile/internal/ssa.posetTestOp %v": "",
|
||||
"cmd/compile/internal/ssa.rbrank %d": "",
|
||||
"cmd/compile/internal/ssa.regMask %d": "",
|
||||
"cmd/compile/internal/ssa.register %d": "",
|
||||
|
|
@ -693,31 +696,32 @@ var knownFormats = map[string]string{
|
|||
"interface{} %s": "",
|
||||
"interface{} %v": "",
|
||||
"map[*cmd/compile/internal/gc.Node]*cmd/compile/internal/ssa.Value %v": "",
|
||||
"reflect.Type %s": "",
|
||||
"rune %#U": "",
|
||||
"rune %c": "",
|
||||
"string %-*s": "",
|
||||
"string %-16s": "",
|
||||
"string %-6s": "",
|
||||
"string %.*s": "",
|
||||
"string %q": "",
|
||||
"string %s": "",
|
||||
"string %v": "",
|
||||
"time.Duration %d": "",
|
||||
"time.Duration %v": "",
|
||||
"uint %04x": "",
|
||||
"uint %5d": "",
|
||||
"uint %d": "",
|
||||
"uint %x": "",
|
||||
"uint16 %d": "",
|
||||
"uint16 %v": "",
|
||||
"uint16 %x": "",
|
||||
"uint32 %d": "",
|
||||
"uint32 %x": "",
|
||||
"uint64 %08x": "",
|
||||
"uint64 %d": "",
|
||||
"uint64 %x": "",
|
||||
"uint8 %d": "",
|
||||
"uint8 %x": "",
|
||||
"uintptr %d": "",
|
||||
"map[cmd/compile/internal/ssa.ID]uint32 %v": "",
|
||||
"reflect.Type %s": "",
|
||||
"rune %#U": "",
|
||||
"rune %c": "",
|
||||
"string %-*s": "",
|
||||
"string %-16s": "",
|
||||
"string %-6s": "",
|
||||
"string %.*s": "",
|
||||
"string %q": "",
|
||||
"string %s": "",
|
||||
"string %v": "",
|
||||
"time.Duration %d": "",
|
||||
"time.Duration %v": "",
|
||||
"uint %04x": "",
|
||||
"uint %5d": "",
|
||||
"uint %d": "",
|
||||
"uint %x": "",
|
||||
"uint16 %d": "",
|
||||
"uint16 %v": "",
|
||||
"uint16 %x": "",
|
||||
"uint32 %d": "",
|
||||
"uint32 %x": "",
|
||||
"uint64 %08x": "",
|
||||
"uint64 %d": "",
|
||||
"uint64 %x": "",
|
||||
"uint8 %d": "",
|
||||
"uint8 %x": "",
|
||||
"uintptr %d": "",
|
||||
}
|
||||
|
|
|
|||
1181
src/cmd/compile/internal/ssa/poset.go
Normal file
1181
src/cmd/compile/internal/ssa/poset.go
Normal file
File diff suppressed because it is too large
Load diff
682
src/cmd/compile/internal/ssa/poset_test.go
Normal file
682
src/cmd/compile/internal/ssa/poset_test.go
Normal file
|
|
@ -0,0 +1,682 @@
|
|||
// Copyright 2018 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.
|
||||
|
||||
package ssa
|
||||
|
||||
import (
|
||||
"fmt"
|
||||
"testing"
|
||||
)
|
||||
|
||||
const (
|
||||
SetOrder = "SetOrder"
|
||||
SetOrder_Fail = "SetOrder_Fail"
|
||||
SetOrderOrEqual = "SetOrderOrEqual"
|
||||
SetOrderOrEqual_Fail = "SetOrderOrEqual_Fail"
|
||||
Ordered = "Ordered"
|
||||
Ordered_Fail = "Ordered_Fail"
|
||||
OrderedOrEqual = "OrderedOrEqual"
|
||||
OrderedOrEqual_Fail = "OrderedOrEqual_Fail"
|
||||
SetEqual = "SetEqual"
|
||||
SetEqual_Fail = "SetEqual_Fail"
|
||||
Equal = "Equal"
|
||||
Equal_Fail = "Equal_Fail"
|
||||
SetNonEqual = "SetNonEqual"
|
||||
SetNonEqual_Fail = "SetNonEqual_Fail"
|
||||
NonEqual = "NonEqual"
|
||||
NonEqual_Fail = "NonEqual_Fail"
|
||||
Checkpoint = "Checkpoint"
|
||||
Undo = "Undo"
|
||||
)
|
||||
|
||||
type posetTestOp struct {
|
||||
typ string
|
||||
a, b int
|
||||
}
|
||||
|
||||
func vconst(i int) int {
|
||||
if i < -128 || i >= 128 {
|
||||
panic("invalid const")
|
||||
}
|
||||
return 1000 + 128 + i
|
||||
}
|
||||
|
||||
func vconst2(i int) int {
|
||||
if i < -128 || i >= 128 {
|
||||
panic("invalid const")
|
||||
}
|
||||
return 1000 + 256 + i
|
||||
}
|
||||
|
||||
func testPosetOps(t *testing.T, unsigned bool, ops []posetTestOp) {
|
||||
var v [1512]*Value
|
||||
for i := range v {
|
||||
v[i] = new(Value)
|
||||
v[i].ID = ID(i)
|
||||
if i >= 1000 && i < 1256 {
|
||||
v[i].Op = OpConst64
|
||||
v[i].AuxInt = int64(i - 1000 - 128)
|
||||
}
|
||||
if i >= 1256 && i < 1512 {
|
||||
v[i].Op = OpConst64
|
||||
v[i].AuxInt = int64(i - 1000 - 256)
|
||||
}
|
||||
}
|
||||
|
||||
po := newPoset(unsigned)
|
||||
for idx, op := range ops {
|
||||
t.Logf("op%d%v", idx, op)
|
||||
switch op.typ {
|
||||
case SetOrder:
|
||||
if !po.SetOrder(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v failed", idx, op)
|
||||
}
|
||||
case SetOrder_Fail:
|
||||
if po.SetOrder(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v passed", idx, op)
|
||||
}
|
||||
case SetOrderOrEqual:
|
||||
if !po.SetOrderOrEqual(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v failed", idx, op)
|
||||
}
|
||||
case SetOrderOrEqual_Fail:
|
||||
if po.SetOrderOrEqual(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v passed", idx, op)
|
||||
}
|
||||
case Ordered:
|
||||
if !po.Ordered(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v failed", idx, op)
|
||||
}
|
||||
case Ordered_Fail:
|
||||
if po.Ordered(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v passed", idx, op)
|
||||
}
|
||||
case OrderedOrEqual:
|
||||
if !po.OrderedOrEqual(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v failed", idx, op)
|
||||
}
|
||||
case OrderedOrEqual_Fail:
|
||||
if po.OrderedOrEqual(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v passed", idx, op)
|
||||
}
|
||||
case SetEqual:
|
||||
if !po.SetEqual(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v failed", idx, op)
|
||||
}
|
||||
case SetEqual_Fail:
|
||||
if po.SetEqual(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v passed", idx, op)
|
||||
}
|
||||
case Equal:
|
||||
if !po.Equal(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v failed", idx, op)
|
||||
}
|
||||
case Equal_Fail:
|
||||
if po.Equal(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v passed", idx, op)
|
||||
}
|
||||
case SetNonEqual:
|
||||
if !po.SetNonEqual(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v failed", idx, op)
|
||||
}
|
||||
case SetNonEqual_Fail:
|
||||
if po.SetNonEqual(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v passed", idx, op)
|
||||
}
|
||||
case NonEqual:
|
||||
if !po.NonEqual(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v failed", idx, op)
|
||||
}
|
||||
case NonEqual_Fail:
|
||||
if po.NonEqual(v[op.a], v[op.b]) {
|
||||
t.Errorf("FAILED: op%d%v passed", idx, op)
|
||||
}
|
||||
case Checkpoint:
|
||||
po.Checkpoint()
|
||||
case Undo:
|
||||
t.Log("Undo stack", po.undo)
|
||||
po.Undo()
|
||||
default:
|
||||
panic("unimplemented")
|
||||
}
|
||||
|
||||
if false {
|
||||
po.DotDump(fmt.Sprintf("op%d.dot", idx), fmt.Sprintf("Last op: %v", op))
|
||||
}
|
||||
|
||||
if err := po.CheckIntegrity(); err != nil {
|
||||
t.Fatalf("op%d%v: integrity error: %v", idx, op, err)
|
||||
}
|
||||
}
|
||||
|
||||
// Check that the poset is completely empty
|
||||
if err := po.CheckEmpty(); err != nil {
|
||||
t.Error(err)
|
||||
}
|
||||
}
|
||||
|
||||
func TestPoset(t *testing.T) {
|
||||
testPosetOps(t, false, []posetTestOp{
|
||||
{Ordered_Fail, 123, 124},
|
||||
|
||||
// Dag #0: 100<101
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrder, 100, 101},
|
||||
{Ordered, 100, 101},
|
||||
{Ordered_Fail, 101, 100},
|
||||
{SetOrder_Fail, 101, 100},
|
||||
{SetOrder, 100, 101}, // repeat
|
||||
{NonEqual, 100, 101},
|
||||
{NonEqual, 101, 100},
|
||||
{SetEqual_Fail, 100, 101},
|
||||
|
||||
// Dag #1: 4<=7<12
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrderOrEqual, 4, 7},
|
||||
{OrderedOrEqual, 4, 7},
|
||||
{SetOrder, 7, 12},
|
||||
{Ordered, 7, 12},
|
||||
{Ordered, 4, 12},
|
||||
{Ordered_Fail, 12, 4},
|
||||
{NonEqual, 4, 12},
|
||||
{NonEqual, 12, 4},
|
||||
{NonEqual_Fail, 4, 100},
|
||||
{OrderedOrEqual, 4, 12},
|
||||
{OrderedOrEqual_Fail, 12, 4},
|
||||
{OrderedOrEqual, 4, 7},
|
||||
{OrderedOrEqual, 7, 4},
|
||||
|
||||
// Dag #1: 1<4<=7<12
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrder, 1, 4},
|
||||
{Ordered, 1, 4},
|
||||
{Ordered, 1, 12},
|
||||
{Ordered_Fail, 12, 1},
|
||||
|
||||
// Dag #1: 1<4<=7<12, 6<7
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrder, 6, 7},
|
||||
{Ordered, 6, 7},
|
||||
{Ordered, 6, 12},
|
||||
{SetOrder_Fail, 7, 4},
|
||||
{SetOrder_Fail, 7, 6},
|
||||
{SetOrder_Fail, 7, 1},
|
||||
|
||||
// Dag #1: 1<4<=7<12, 1<6<7
|
||||
{Checkpoint, 0, 0},
|
||||
{Ordered_Fail, 1, 6},
|
||||
{SetOrder, 1, 6},
|
||||
{Ordered, 1, 6},
|
||||
{SetOrder_Fail, 6, 1},
|
||||
|
||||
// Dag #1: 1<4<=7<12, 1<4<6<7
|
||||
{Checkpoint, 0, 0},
|
||||
{Ordered_Fail, 4, 6},
|
||||
{Ordered_Fail, 4, 7},
|
||||
{SetOrder, 4, 6},
|
||||
{Ordered, 4, 6},
|
||||
{OrderedOrEqual, 4, 6},
|
||||
{Ordered, 4, 7},
|
||||
{OrderedOrEqual, 4, 7},
|
||||
{SetOrder_Fail, 6, 4},
|
||||
{Ordered_Fail, 7, 6},
|
||||
{Ordered_Fail, 7, 4},
|
||||
{OrderedOrEqual_Fail, 7, 6},
|
||||
{OrderedOrEqual_Fail, 7, 4},
|
||||
|
||||
// Merge: 1<4<6, 4<=7<12, 6<101
|
||||
{Checkpoint, 0, 0},
|
||||
{Ordered_Fail, 6, 101},
|
||||
{SetOrder, 6, 101},
|
||||
{Ordered, 6, 101},
|
||||
{Ordered, 1, 101},
|
||||
|
||||
// Merge: 1<4<6, 4<=7<12, 6<100<101
|
||||
{Checkpoint, 0, 0},
|
||||
{Ordered_Fail, 6, 100},
|
||||
{SetOrder, 6, 100},
|
||||
{Ordered, 1, 100},
|
||||
|
||||
// Undo: 1<4<6<7<12, 6<101
|
||||
{Ordered, 100, 101},
|
||||
{Undo, 0, 0},
|
||||
{Ordered, 100, 101},
|
||||
{Ordered_Fail, 6, 100},
|
||||
{Ordered, 6, 101},
|
||||
{Ordered, 1, 101},
|
||||
|
||||
// Undo: 1<4<6<7<12, 100<101
|
||||
{Undo, 0, 0},
|
||||
{Ordered_Fail, 1, 100},
|
||||
{Ordered_Fail, 1, 101},
|
||||
{Ordered_Fail, 6, 100},
|
||||
{Ordered_Fail, 6, 101},
|
||||
|
||||
// Merge: 1<4<6<7<12, 6<100<101
|
||||
{Checkpoint, 0, 0},
|
||||
{Ordered, 100, 101},
|
||||
{SetOrder, 6, 100},
|
||||
{Ordered, 6, 100},
|
||||
{Ordered, 6, 101},
|
||||
{Ordered, 1, 101},
|
||||
|
||||
// Undo 2 times: 1<4<7<12, 1<6<7
|
||||
{Undo, 0, 0},
|
||||
{Undo, 0, 0},
|
||||
{Ordered, 1, 6},
|
||||
{Ordered, 4, 12},
|
||||
{Ordered_Fail, 4, 6},
|
||||
{SetOrder_Fail, 6, 1},
|
||||
|
||||
// Undo 2 times: 1<4<7<12
|
||||
{Undo, 0, 0},
|
||||
{Undo, 0, 0},
|
||||
{Ordered, 1, 12},
|
||||
{Ordered, 7, 12},
|
||||
{Ordered_Fail, 1, 6},
|
||||
{Ordered_Fail, 6, 7},
|
||||
{Ordered, 100, 101},
|
||||
{Ordered_Fail, 1, 101},
|
||||
|
||||
// Undo: 4<7<12
|
||||
{Undo, 0, 0},
|
||||
{Ordered_Fail, 1, 12},
|
||||
{Ordered_Fail, 1, 4},
|
||||
{Ordered, 4, 12},
|
||||
{Ordered, 100, 101},
|
||||
|
||||
// Undo: 100<101
|
||||
{Undo, 0, 0},
|
||||
{Ordered_Fail, 4, 7},
|
||||
{Ordered_Fail, 7, 12},
|
||||
{Ordered, 100, 101},
|
||||
|
||||
// Recreated DAG #1 from scratch, reusing same nodes.
|
||||
// This also stresses that Undo has done its job correctly.
|
||||
// DAG: 1<2<(5|6), 101<102<(105|106<107)
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrder, 101, 102},
|
||||
{SetOrder, 102, 105},
|
||||
{SetOrder, 102, 106},
|
||||
{SetOrder, 106, 107},
|
||||
{SetOrder, 1, 2},
|
||||
{SetOrder, 2, 5},
|
||||
{SetOrder, 2, 6},
|
||||
{SetEqual_Fail, 1, 6},
|
||||
{SetEqual_Fail, 107, 102},
|
||||
|
||||
// Now Set 2 == 102
|
||||
// New DAG: (1|101)<2==102<(5|6|105|106<107)
|
||||
{Checkpoint, 0, 0},
|
||||
{SetEqual, 2, 102},
|
||||
{Equal, 2, 102},
|
||||
{SetEqual, 2, 102}, // trivially pass
|
||||
{SetNonEqual_Fail, 2, 102}, // trivially fail
|
||||
{Ordered, 1, 107},
|
||||
{Ordered, 101, 6},
|
||||
{Ordered, 101, 105},
|
||||
{Ordered, 2, 106},
|
||||
{Ordered, 102, 6},
|
||||
|
||||
// Undo SetEqual
|
||||
{Undo, 0, 0},
|
||||
{Equal_Fail, 2, 102},
|
||||
{Ordered_Fail, 2, 102},
|
||||
{Ordered_Fail, 1, 107},
|
||||
{Ordered_Fail, 101, 6},
|
||||
{Checkpoint, 0, 0},
|
||||
{SetEqual, 2, 100},
|
||||
{Ordered, 1, 107},
|
||||
{Ordered, 100, 6},
|
||||
|
||||
// SetEqual with new node
|
||||
{Undo, 0, 0},
|
||||
{Checkpoint, 0, 0},
|
||||
{SetEqual, 2, 400},
|
||||
{SetEqual, 401, 2},
|
||||
{Equal, 400, 401},
|
||||
{Ordered, 1, 400},
|
||||
{Ordered, 400, 6},
|
||||
{Ordered, 1, 401},
|
||||
{Ordered, 401, 6},
|
||||
{Ordered_Fail, 2, 401},
|
||||
|
||||
// SetEqual unseen nodes and then connect
|
||||
{Checkpoint, 0, 0},
|
||||
{SetEqual, 500, 501},
|
||||
{SetEqual, 102, 501},
|
||||
{Equal, 500, 102},
|
||||
{Ordered, 501, 106},
|
||||
{Ordered, 100, 500},
|
||||
{SetEqual, 500, 501},
|
||||
{Ordered_Fail, 500, 501},
|
||||
{Ordered_Fail, 102, 501},
|
||||
|
||||
// SetNonEqual relations
|
||||
{Undo, 0, 0},
|
||||
{Checkpoint, 0, 0},
|
||||
{SetNonEqual, 600, 601},
|
||||
{NonEqual, 600, 601},
|
||||
{SetNonEqual, 601, 602},
|
||||
{NonEqual, 601, 602},
|
||||
{NonEqual_Fail, 600, 602}, // non-transitive
|
||||
{SetEqual_Fail, 601, 602},
|
||||
|
||||
// Undo back to beginning, leave the poset empty
|
||||
{Undo, 0, 0},
|
||||
{Undo, 0, 0},
|
||||
{Undo, 0, 0},
|
||||
{Undo, 0, 0},
|
||||
})
|
||||
}
|
||||
|
||||
func TestPosetStrict(t *testing.T) {
|
||||
|
||||
testPosetOps(t, false, []posetTestOp{
|
||||
{Checkpoint, 0, 0},
|
||||
// Build: 20!=30, 10<20<=30<40. The 20<=30 will become 20<30.
|
||||
{SetNonEqual, 20, 30},
|
||||
{SetOrder, 10, 20},
|
||||
{SetOrderOrEqual, 20, 30}, // this is affected by 20!=30
|
||||
{SetOrder, 30, 40},
|
||||
|
||||
{Ordered, 10, 30},
|
||||
{Ordered, 20, 30},
|
||||
{Ordered, 10, 40},
|
||||
{OrderedOrEqual, 10, 30},
|
||||
{OrderedOrEqual, 20, 30},
|
||||
{OrderedOrEqual, 10, 40},
|
||||
|
||||
{Undo, 0, 0},
|
||||
|
||||
// Now do the opposite: first build the DAG and then learn non-equality
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrder, 10, 20},
|
||||
{SetOrderOrEqual, 20, 30}, // this is affected by 20!=30
|
||||
{SetOrder, 30, 40},
|
||||
|
||||
{Ordered, 10, 30},
|
||||
{Ordered_Fail, 20, 30},
|
||||
{Ordered, 10, 40},
|
||||
{OrderedOrEqual, 10, 30},
|
||||
{OrderedOrEqual, 20, 30},
|
||||
{OrderedOrEqual, 10, 40},
|
||||
|
||||
{Checkpoint, 0, 0},
|
||||
{SetNonEqual, 20, 30},
|
||||
{Ordered, 10, 30},
|
||||
{Ordered, 20, 30},
|
||||
{Ordered, 10, 40},
|
||||
{OrderedOrEqual, 10, 30},
|
||||
{OrderedOrEqual, 20, 30},
|
||||
{OrderedOrEqual, 10, 40},
|
||||
{Undo, 0, 0},
|
||||
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrderOrEqual, 30, 35},
|
||||
{OrderedOrEqual, 20, 35},
|
||||
{Ordered_Fail, 20, 35},
|
||||
{SetNonEqual, 20, 35},
|
||||
{Ordered, 20, 35},
|
||||
{Undo, 0, 0},
|
||||
|
||||
// Learn <= and >=
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrderOrEqual, 50, 60},
|
||||
{SetOrderOrEqual, 60, 50},
|
||||
{OrderedOrEqual, 50, 60},
|
||||
{OrderedOrEqual, 60, 50},
|
||||
{Ordered_Fail, 50, 60},
|
||||
{Ordered_Fail, 60, 50},
|
||||
{Equal, 50, 60},
|
||||
{Equal, 60, 50},
|
||||
{NonEqual_Fail, 50, 60},
|
||||
{NonEqual_Fail, 60, 50},
|
||||
{Undo, 0, 0},
|
||||
|
||||
{Undo, 0, 0},
|
||||
})
|
||||
}
|
||||
|
||||
func TestSetEqual(t *testing.T) {
|
||||
testPosetOps(t, false, []posetTestOp{
|
||||
// 10<=20<=30<40, 20<=100<110
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrderOrEqual, 10, 20},
|
||||
{SetOrderOrEqual, 20, 30},
|
||||
{SetOrder, 30, 40},
|
||||
{SetOrderOrEqual, 20, 100},
|
||||
{SetOrder, 100, 110},
|
||||
{OrderedOrEqual, 10, 30},
|
||||
{OrderedOrEqual, 30, 10},
|
||||
{Ordered_Fail, 10, 30},
|
||||
{Ordered_Fail, 30, 10},
|
||||
{Ordered, 10, 40},
|
||||
{Ordered_Fail, 40, 10},
|
||||
|
||||
// Try learning 10==20.
|
||||
{Checkpoint, 0, 0},
|
||||
{SetEqual, 10, 20},
|
||||
{OrderedOrEqual, 10, 20},
|
||||
{Ordered_Fail, 10, 20},
|
||||
{Equal, 10, 20},
|
||||
{SetOrderOrEqual, 10, 20},
|
||||
{SetOrderOrEqual, 20, 10},
|
||||
{SetOrder_Fail, 10, 20},
|
||||
{SetOrder_Fail, 20, 10},
|
||||
{Undo, 0, 0},
|
||||
|
||||
// Try learning 20==10.
|
||||
{Checkpoint, 0, 0},
|
||||
{SetEqual, 20, 10},
|
||||
{OrderedOrEqual, 10, 20},
|
||||
{Ordered_Fail, 10, 20},
|
||||
{Equal, 10, 20},
|
||||
{Undo, 0, 0},
|
||||
|
||||
// Try learning 10==40 or 30==40 or 10==110.
|
||||
{Checkpoint, 0, 0},
|
||||
{SetEqual_Fail, 10, 40},
|
||||
{SetEqual_Fail, 40, 10},
|
||||
{SetEqual_Fail, 30, 40},
|
||||
{SetEqual_Fail, 40, 30},
|
||||
{SetEqual_Fail, 10, 110},
|
||||
{SetEqual_Fail, 110, 10},
|
||||
{Undo, 0, 0},
|
||||
|
||||
// Try learning 40==110, and then 10==40 or 10=110
|
||||
{Checkpoint, 0, 0},
|
||||
{SetEqual, 40, 110},
|
||||
{SetEqual_Fail, 10, 40},
|
||||
{SetEqual_Fail, 40, 10},
|
||||
{SetEqual_Fail, 10, 110},
|
||||
{SetEqual_Fail, 110, 10},
|
||||
{Undo, 0, 0},
|
||||
|
||||
// Try learning 40<20 or 30<20 or 110<10
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrder_Fail, 40, 20},
|
||||
{SetOrder_Fail, 30, 20},
|
||||
{SetOrder_Fail, 110, 10},
|
||||
{Undo, 0, 0},
|
||||
|
||||
// Try learning 30<=20
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrderOrEqual, 30, 20},
|
||||
{Equal, 30, 20},
|
||||
{OrderedOrEqual, 30, 100},
|
||||
{Ordered, 30, 110},
|
||||
{Undo, 0, 0},
|
||||
|
||||
{Undo, 0, 0},
|
||||
})
|
||||
}
|
||||
|
||||
func TestPosetConst(t *testing.T) {
|
||||
testPosetOps(t, false, []posetTestOp{
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrder, 1, vconst(15)},
|
||||
{SetOrderOrEqual, 100, vconst(120)},
|
||||
{Ordered, 1, vconst(15)},
|
||||
{Ordered, 1, vconst(120)},
|
||||
{OrderedOrEqual, 1, vconst(120)},
|
||||
{OrderedOrEqual, 100, vconst(120)},
|
||||
{Ordered_Fail, 100, vconst(15)},
|
||||
{Ordered_Fail, vconst(15), 100},
|
||||
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrderOrEqual, 1, 5},
|
||||
{SetOrderOrEqual, 5, 25},
|
||||
{SetEqual, 20, vconst(20)},
|
||||
{SetEqual, 25, vconst(25)},
|
||||
{Ordered, 1, 20},
|
||||
{Ordered, 1, vconst(30)},
|
||||
{Undo, 0, 0},
|
||||
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrderOrEqual, 1, 5},
|
||||
{SetOrderOrEqual, 5, 25},
|
||||
{SetEqual, vconst(-20), 5},
|
||||
{SetEqual, vconst(-25), 1},
|
||||
{Ordered, 1, 5},
|
||||
{Ordered, vconst(-30), 1},
|
||||
{Undo, 0, 0},
|
||||
|
||||
{Checkpoint, 0, 0},
|
||||
{SetNonEqual, 1, vconst(4)},
|
||||
{SetNonEqual, 1, vconst(6)},
|
||||
{NonEqual, 1, vconst(4)},
|
||||
{NonEqual_Fail, 1, vconst(5)},
|
||||
{NonEqual, 1, vconst(6)},
|
||||
{Equal_Fail, 1, vconst(4)},
|
||||
{Equal_Fail, 1, vconst(5)},
|
||||
{Equal_Fail, 1, vconst(6)},
|
||||
{Equal_Fail, 1, vconst(7)},
|
||||
{Undo, 0, 0},
|
||||
|
||||
{Undo, 0, 0},
|
||||
})
|
||||
|
||||
testPosetOps(t, true, []posetTestOp{
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrder, 1, vconst(15)},
|
||||
{SetOrderOrEqual, 100, vconst(-5)}, // -5 is a very big number in unsigned
|
||||
{Ordered, 1, vconst(15)},
|
||||
{Ordered, 1, vconst(-5)},
|
||||
{OrderedOrEqual, 1, vconst(-5)},
|
||||
{OrderedOrEqual, 100, vconst(-5)},
|
||||
{Ordered_Fail, 100, vconst(15)},
|
||||
{Ordered_Fail, vconst(15), 100},
|
||||
|
||||
{Undo, 0, 0},
|
||||
})
|
||||
|
||||
testPosetOps(t, false, []posetTestOp{
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrderOrEqual, 1, vconst(3)},
|
||||
{SetNonEqual, 1, vconst(0)},
|
||||
{Ordered_Fail, 1, vconst(0)},
|
||||
{Undo, 0, 0},
|
||||
})
|
||||
|
||||
testPosetOps(t, false, []posetTestOp{
|
||||
// Check relations of a constant with itself
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrderOrEqual, vconst(3), vconst2(3)},
|
||||
{Undo, 0, 0},
|
||||
{Checkpoint, 0, 0},
|
||||
{SetEqual, vconst(3), vconst2(3)},
|
||||
{Undo, 0, 0},
|
||||
{Checkpoint, 0, 0},
|
||||
{SetNonEqual_Fail, vconst(3), vconst2(3)},
|
||||
{Undo, 0, 0},
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrder_Fail, vconst(3), vconst2(3)},
|
||||
{Undo, 0, 0},
|
||||
|
||||
// Check relations of two constants among them, using
|
||||
// different instances of the same constant
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrderOrEqual, vconst(3), vconst(4)},
|
||||
{OrderedOrEqual, vconst(3), vconst2(4)},
|
||||
{Undo, 0, 0},
|
||||
{Checkpoint, 0, 0},
|
||||
{SetOrder, vconst(3), vconst(4)},
|
||||
{Ordered, vconst(3), vconst2(4)},
|
||||
{Undo, 0, 0},
|
||||
{Checkpoint, 0, 0},
|
||||
{SetEqual_Fail, vconst(3), vconst(4)},
|
||||
{SetEqual_Fail, vconst(3), vconst2(4)},
|
||||
{Undo, 0, 0},
|
||||
{Checkpoint, 0, 0},
|
||||
{NonEqual, vconst(3), vconst(4)},
|
||||
{NonEqual, vconst(3), vconst2(4)},
|
||||
{Undo, 0, 0},
|
||||
{Checkpoint, 0, 0},
|
||||
{Equal_Fail, vconst(3), vconst(4)},
|
||||
{Equal_Fail, vconst(3), vconst2(4)},
|
||||
{Undo, 0, 0},
|
||||
{Checkpoint, 0, 0},
|
||||
{SetNonEqual, vconst(3), vconst(4)},
|
||||
{SetNonEqual, vconst(3), vconst2(4)},
|
||||
{Undo, 0, 0},
|
||||
})
|
||||
}
|
||||
|
||||
func TestPosetNonEqual(t *testing.T) {
|
||||
testPosetOps(t, false, []posetTestOp{
|
||||
{Checkpoint, 0, 0},
|
||||
{Equal_Fail, 10, 20},
|
||||
{NonEqual_Fail, 10, 20},
|
||||
|
||||
// Learn 10!=20
|
||||
{Checkpoint, 0, 0},
|
||||
{SetNonEqual, 10, 20},
|
||||
{Equal_Fail, 10, 20},
|
||||
{NonEqual, 10, 20},
|
||||
{SetEqual_Fail, 10, 20},
|
||||
|
||||
// Learn again 10!=20
|
||||
{Checkpoint, 0, 0},
|
||||
{SetNonEqual, 10, 20},
|
||||
{Equal_Fail, 10, 20},
|
||||
{NonEqual, 10, 20},
|
||||
|
||||
// Undo. We still know 10!=20
|
||||
{Undo, 0, 0},
|
||||
{Equal_Fail, 10, 20},
|
||||
{NonEqual, 10, 20},
|
||||
{SetEqual_Fail, 10, 20},
|
||||
|
||||
// Undo again. Now we know nothing
|
||||
{Undo, 0, 0},
|
||||
{Equal_Fail, 10, 20},
|
||||
{NonEqual_Fail, 10, 20},
|
||||
|
||||
// Learn 10==20
|
||||
{Checkpoint, 0, 0},
|
||||
{SetEqual, 10, 20},
|
||||
{Equal, 10, 20},
|
||||
{NonEqual_Fail, 10, 20},
|
||||
{SetNonEqual_Fail, 10, 20},
|
||||
|
||||
// Learn again 10==20
|
||||
{Checkpoint, 0, 0},
|
||||
{SetEqual, 10, 20},
|
||||
{Equal, 10, 20},
|
||||
{NonEqual_Fail, 10, 20},
|
||||
{SetNonEqual_Fail, 10, 20},
|
||||
|
||||
// Undo. We still know 10==20
|
||||
{Undo, 0, 0},
|
||||
{Equal, 10, 20},
|
||||
{NonEqual_Fail, 10, 20},
|
||||
{SetNonEqual_Fail, 10, 20},
|
||||
|
||||
// Undo. We know nothing
|
||||
{Undo, 0, 0},
|
||||
{Equal_Fail, 10, 20},
|
||||
{NonEqual_Fail, 10, 20},
|
||||
})
|
||||
}
|
||||
|
|
@ -160,6 +160,11 @@ type factsTable struct {
|
|||
facts map[pair]relation // current known set of relation
|
||||
stack []fact // previous sets of relations
|
||||
|
||||
// order is a couple of partial order sets that record information
|
||||
// about relations between SSA values in the signed and unsigned
|
||||
// domain.
|
||||
order [2]*poset
|
||||
|
||||
// known lower and upper bounds on individual values.
|
||||
limits map[ID]limit
|
||||
limitStack []limitFact // previous entries
|
||||
|
|
@ -178,6 +183,8 @@ var checkpointBound = limitFact{}
|
|||
|
||||
func newFactsTable() *factsTable {
|
||||
ft := &factsTable{}
|
||||
ft.order[0] = newPoset(false) // signed
|
||||
ft.order[1] = newPoset(true) // unsigned
|
||||
ft.facts = make(map[pair]relation)
|
||||
ft.stack = make([]fact, 4)
|
||||
ft.limits = make(map[ID]limit)
|
||||
|
|
@ -202,30 +209,58 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
|
|||
return
|
||||
}
|
||||
|
||||
if lessByID(w, v) {
|
||||
v, w = w, v
|
||||
r = reverseBits[r]
|
||||
}
|
||||
|
||||
p := pair{v, w, d}
|
||||
oldR, ok := ft.facts[p]
|
||||
if !ok {
|
||||
if v == w {
|
||||
oldR = eq
|
||||
} else {
|
||||
oldR = lt | eq | gt
|
||||
if d == signed || d == unsigned {
|
||||
var ok bool
|
||||
idx := 0
|
||||
if d == unsigned {
|
||||
idx = 1
|
||||
}
|
||||
switch r {
|
||||
case lt:
|
||||
ok = ft.order[idx].SetOrder(v, w)
|
||||
case gt:
|
||||
ok = ft.order[idx].SetOrder(w, v)
|
||||
case lt | eq:
|
||||
ok = ft.order[idx].SetOrderOrEqual(v, w)
|
||||
case gt | eq:
|
||||
ok = ft.order[idx].SetOrderOrEqual(w, v)
|
||||
case eq:
|
||||
ok = ft.order[idx].SetEqual(v, w)
|
||||
case lt | gt:
|
||||
ok = ft.order[idx].SetNonEqual(v, w)
|
||||
default:
|
||||
panic("unknown relation")
|
||||
}
|
||||
if !ok {
|
||||
ft.unsat = true
|
||||
return
|
||||
}
|
||||
} else {
|
||||
if lessByID(w, v) {
|
||||
v, w = w, v
|
||||
r = reverseBits[r]
|
||||
}
|
||||
|
||||
p := pair{v, w, d}
|
||||
oldR, ok := ft.facts[p]
|
||||
if !ok {
|
||||
if v == w {
|
||||
oldR = eq
|
||||
} else {
|
||||
oldR = lt | eq | gt
|
||||
}
|
||||
}
|
||||
// No changes compared to information already in facts table.
|
||||
if oldR == r {
|
||||
return
|
||||
}
|
||||
ft.stack = append(ft.stack, fact{p, oldR})
|
||||
ft.facts[p] = oldR & r
|
||||
// If this relation is not satisfiable, mark it and exit right away
|
||||
if oldR&r == 0 {
|
||||
ft.unsat = true
|
||||
return
|
||||
}
|
||||
}
|
||||
// No changes compared to information already in facts table.
|
||||
if oldR == r {
|
||||
return
|
||||
}
|
||||
ft.stack = append(ft.stack, fact{p, oldR})
|
||||
ft.facts[p] = oldR & r
|
||||
// If this relation is not satisfiable, mark it and exit right away
|
||||
if oldR&r == 0 {
|
||||
ft.unsat = true
|
||||
return
|
||||
}
|
||||
|
||||
// Extract bounds when comparing against constants
|
||||
|
|
@ -382,6 +417,8 @@ func (ft *factsTable) checkpoint() {
|
|||
}
|
||||
ft.stack = append(ft.stack, checkpointFact)
|
||||
ft.limitStack = append(ft.limitStack, checkpointBound)
|
||||
ft.order[0].Checkpoint()
|
||||
ft.order[1].Checkpoint()
|
||||
}
|
||||
|
||||
// restore restores known relation to the state just
|
||||
|
|
@ -417,6 +454,8 @@ func (ft *factsTable) restore() {
|
|||
ft.limits[old.vid] = old.limit
|
||||
}
|
||||
}
|
||||
ft.order[0].Undo()
|
||||
ft.order[1].Undo()
|
||||
}
|
||||
|
||||
func lessByID(v, w *Value) bool {
|
||||
|
|
|
|||
|
|
@ -397,8 +397,7 @@ func f13e(a int) int {
|
|||
|
||||
func f13f(a int64) int64 {
|
||||
if a > math.MaxInt64 {
|
||||
// Unreachable, but prove doesn't know that.
|
||||
if a == 0 {
|
||||
if a == 0 { // ERROR "Disproved Eq64$"
|
||||
return 1
|
||||
}
|
||||
}
|
||||
|
|
@ -575,6 +574,37 @@ func fence4(x, y int64) {
|
|||
}
|
||||
}
|
||||
|
||||
// Check transitive relations
|
||||
func trans1(x, y int64) {
|
||||
if x > 5 {
|
||||
if y > x {
|
||||
if y > 2 { // ERROR "Proved Greater64"
|
||||
return
|
||||
}
|
||||
} else if y == x {
|
||||
if y > 5 { // ERROR "Proved Greater64"
|
||||
return
|
||||
}
|
||||
}
|
||||
}
|
||||
if x >= 10 {
|
||||
if y > x {
|
||||
if y > 10 { // ERROR "Proved Greater64"
|
||||
return
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
func trans2(a, b []int, i int) {
|
||||
if len(a) != len(b) {
|
||||
return
|
||||
}
|
||||
|
||||
_ = a[i]
|
||||
_ = b[i] // ERROR "Proved IsInBounds$"
|
||||
}
|
||||
|
||||
//go:noinline
|
||||
func useInt(a int) {
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue