This repository has been archived by the owner on Aug 3, 2020. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 27
/
prove.go
774 lines (712 loc) · 18.5 KB
/
prove.go
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
// Copyright 2016 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"
"math"
)
type branch int
const (
unknown = iota
positive
negative
)
// relation represents the set of possible relations between
// pairs of variables (v, w). Without a priori knowledge the
// mask is lt | eq | gt meaning v can be less than, equal to or
// greater than w. When the execution path branches on the condition
// `v op w` the set of relations is updated to exclude any
// relation not possible due to `v op w` being true (or false).
//
// E.g.
//
// r := relation(...)
//
// if v < w {
// newR := r & lt
// }
// if v >= w {
// newR := r & (eq|gt)
// }
// if v != w {
// newR := r & (lt|gt)
// }
type relation uint
const (
lt relation = 1 << iota
eq
gt
)
// domain represents the domain of a variable pair in which a set
// of relations is known. For example, relations learned for unsigned
// pairs cannot be transferred to signed pairs because the same bit
// representation can mean something else.
type domain uint
const (
signed domain = 1 << iota
unsigned
pointer
boolean
)
type pair struct {
v, w *Value // a pair of values, ordered by ID.
// v can be nil, to mean the zero value.
// for booleans the zero value (v == nil) is false.
d domain
}
// fact is a pair plus a relation for that pair.
type fact struct {
p pair
r relation
}
// a limit records known upper and lower bounds for a value.
type limit struct {
min, max int64 // min <= value <= max, signed
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.
type limitFact struct {
vid ID
limit limit
}
// factsTable keeps track of relations between pairs of values.
type factsTable struct {
facts map[pair]relation // current known set of relation
stack []fact // previous sets of relations
// known lower and upper bounds on individual values.
limits map[ID]limit
limitStack []limitFact // previous entries
// For each slice s, a map from s to a len(s)/cap(s) value (if any)
// TODO: check if there are cases that matter where we have
// more than one len(s) for a slice. We could keep a list if necessary.
lens map[ID]*Value
caps map[ID]*Value
}
// checkpointFact is an invalid value used for checkpointing
// and restoring factsTable.
var checkpointFact = fact{}
var checkpointBound = limitFact{}
func newFactsTable() *factsTable {
ft := &factsTable{}
ft.facts = make(map[pair]relation)
ft.stack = make([]fact, 4)
ft.limits = make(map[ID]limit)
ft.limitStack = make([]limitFact, 4)
return ft
}
// get returns the known possible relations between v and w.
// If v and w are not in the map it returns lt|eq|gt, i.e. any order.
func (ft *factsTable) get(v, w *Value, d domain) relation {
if v.isGenericIntConst() || w.isGenericIntConst() {
reversed := false
if v.isGenericIntConst() {
v, w = w, v
reversed = true
}
r := lt | eq | gt
lim, ok := ft.limits[v.ID]
if !ok {
return r
}
c := w.AuxInt
switch d {
case signed:
switch {
case c < lim.min:
r = gt
case c > lim.max:
r = lt
case c == lim.min && c == lim.max:
r = eq
case c == lim.min:
r = gt | eq
case c == lim.max:
r = lt | eq
}
case unsigned:
// TODO: also use signed data if lim.min >= 0?
var uc uint64
switch w.Op {
case OpConst64:
uc = uint64(c)
case OpConst32:
uc = uint64(uint32(c))
case OpConst16:
uc = uint64(uint16(c))
case OpConst8:
uc = uint64(uint8(c))
}
switch {
case uc < lim.umin:
r = gt
case uc > lim.umax:
r = lt
case uc == lim.umin && uc == lim.umax:
r = eq
case uc == lim.umin:
r = gt | eq
case uc == lim.umax:
r = lt | eq
}
}
if reversed {
return reverseBits[r]
}
return r
}
reversed := false
if lessByID(w, v) {
v, w = w, v
reversed = !reversed
}
p := pair{v, w, d}
r, ok := ft.facts[p]
if !ok {
if p.v == p.w {
r = eq
} else {
r = lt | eq | gt
}
}
if reversed {
return reverseBits[r]
}
return r
}
// update updates the set of relations between v and w in domain d
// restricting it to r.
func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
if lessByID(w, v) {
v, w = w, v
r = reverseBits[r]
}
p := pair{v, w, d}
oldR := ft.get(v, w, d)
ft.stack = append(ft.stack, fact{p, oldR})
ft.facts[p] = oldR & r
// Extract bounds when comparing against constants
if v.isGenericIntConst() {
v, w = w, v
r = reverseBits[r]
}
if v != nil && w.isGenericIntConst() {
c := w.AuxInt
// Note: all the +1/-1 below could overflow/underflow. Either will
// still generate correct results, it will just lead to imprecision.
// In fact if there is overflow/underflow, the corresponding
// code is unreachable because the known range is outside the range
// of the value's type.
old, ok := ft.limits[v.ID]
if !ok {
old = noLimit
}
lim := old
// Update lim with the new information we know.
switch d {
case signed:
switch r {
case lt:
if c-1 < lim.max {
lim.max = c - 1
}
case lt | eq:
if c < lim.max {
lim.max = c
}
case gt | eq:
if c > lim.min {
lim.min = c
}
case gt:
if c+1 > lim.min {
lim.min = c + 1
}
case lt | gt:
if c == lim.min {
lim.min++
}
if c == lim.max {
lim.max--
}
case eq:
lim.min = c
lim.max = c
}
case unsigned:
var uc uint64
switch w.Op {
case OpConst64:
uc = uint64(c)
case OpConst32:
uc = uint64(uint32(c))
case OpConst16:
uc = uint64(uint16(c))
case OpConst8:
uc = uint64(uint8(c))
}
switch r {
case lt:
if uc-1 < lim.umax {
lim.umax = uc - 1
}
case lt | eq:
if uc < lim.umax {
lim.umax = uc
}
case gt | eq:
if uc > lim.umin {
lim.umin = uc
}
case gt:
if uc+1 > lim.umin {
lim.umin = uc + 1
}
case lt | gt:
if uc == lim.umin {
lim.umin++
}
if uc == lim.umax {
lim.umax--
}
case eq:
lim.umin = uc
lim.umax = uc
}
}
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.Pos, "parent=%s, new limits %s %s %s", parent, v, w, lim.String())
}
}
}
// isNonNegative returns true if v is known to be non-negative.
func (ft *factsTable) isNonNegative(v *Value) bool {
if isNonNegative(v) {
return true
}
l, has := ft.limits[v.ID]
return has && (l.min >= 0 || l.umax <= math.MaxInt64)
}
// checkpoint saves the current state of known relations.
// Called when descending on a branch.
func (ft *factsTable) checkpoint() {
ft.stack = append(ft.stack, checkpointFact)
ft.limitStack = append(ft.limitStack, checkpointBound)
}
// restore restores known relation to the state just
// before the previous checkpoint.
// Called when backing up on a branch.
func (ft *factsTable) restore() {
for {
old := ft.stack[len(ft.stack)-1]
ft.stack = ft.stack[:len(ft.stack)-1]
if old == checkpointFact {
break
}
if old.r == lt|eq|gt {
delete(ft.facts, old.p)
} else {
ft.facts[old.p] = old.r
}
}
for {
old := ft.limitStack[len(ft.limitStack)-1]
ft.limitStack = ft.limitStack[:len(ft.limitStack)-1]
if old.vid == 0 { // checkpointBound
break
}
if old.limit == noLimit {
delete(ft.limits, old.vid)
} else {
ft.limits[old.vid] = old.limit
}
}
}
func lessByID(v, w *Value) bool {
if v == nil && w == nil {
// Should not happen, but just in case.
return false
}
if v == nil {
return true
}
return w != nil && v.ID < w.ID
}
var (
reverseBits = [...]relation{0, 4, 2, 6, 1, 5, 3, 7}
// maps what we learn when the positive branch is taken.
// For example:
// OpLess8: {signed, lt},
// v1 = (OpLess8 v2 v3).
// If v1 branch is taken than we learn that the rangeMaks
// can be at most lt.
domainRelationTable = map[Op]struct {
d domain
r relation
}{
OpEq8: {signed | unsigned, eq},
OpEq16: {signed | unsigned, eq},
OpEq32: {signed | unsigned, eq},
OpEq64: {signed | unsigned, eq},
OpEqPtr: {pointer, eq},
OpNeq8: {signed | unsigned, lt | gt},
OpNeq16: {signed | unsigned, lt | gt},
OpNeq32: {signed | unsigned, lt | gt},
OpNeq64: {signed | unsigned, lt | gt},
OpNeqPtr: {pointer, lt | gt},
OpLess8: {signed, lt},
OpLess8U: {unsigned, lt},
OpLess16: {signed, lt},
OpLess16U: {unsigned, lt},
OpLess32: {signed, lt},
OpLess32U: {unsigned, lt},
OpLess64: {signed, lt},
OpLess64U: {unsigned, lt},
OpLeq8: {signed, lt | eq},
OpLeq8U: {unsigned, lt | eq},
OpLeq16: {signed, lt | eq},
OpLeq16U: {unsigned, lt | eq},
OpLeq32: {signed, lt | eq},
OpLeq32U: {unsigned, lt | eq},
OpLeq64: {signed, lt | eq},
OpLeq64U: {unsigned, lt | eq},
OpGeq8: {signed, eq | gt},
OpGeq8U: {unsigned, eq | gt},
OpGeq16: {signed, eq | gt},
OpGeq16U: {unsigned, eq | gt},
OpGeq32: {signed, eq | gt},
OpGeq32U: {unsigned, eq | gt},
OpGeq64: {signed, eq | gt},
OpGeq64U: {unsigned, eq | gt},
OpGreater8: {signed, gt},
OpGreater8U: {unsigned, gt},
OpGreater16: {signed, gt},
OpGreater16U: {unsigned, gt},
OpGreater32: {signed, gt},
OpGreater32U: {unsigned, gt},
OpGreater64: {signed, gt},
OpGreater64U: {unsigned, gt},
// TODO: OpIsInBounds actually test 0 <= a < b. This means
// that the positive branch learns signed/LT and unsigned/LT
// but the negative branch only learns unsigned/GE.
OpIsInBounds: {unsigned, lt},
OpIsSliceInBounds: {unsigned, lt | eq},
}
)
// prove removes redundant BlockIf branches that can be inferred
// from previous dominating comparisons.
//
// By far, the most common redundant pair are generated by bounds checking.
// For example for the code:
//
// a[i] = 4
// foo(a[i])
//
// The compiler will generate the following code:
//
// if i >= len(a) {
// panic("not in bounds")
// }
// a[i] = 4
// if i >= len(a) {
// panic("not in bounds")
// }
// foo(a[i])
//
// The second comparison i >= len(a) is clearly redundant because if the
// else branch of the first comparison is executed, we already know that i < len(a).
// The code for the second panic can be removed.
func prove(f *Func) {
ft := newFactsTable()
// Find length and capacity ops.
for _, b := range f.Blocks {
for _, v := range b.Values {
if v.Uses == 0 {
// We don't care about dead values.
// (There can be some that are CSEd but not removed yet.)
continue
}
switch v.Op {
case OpSliceLen:
if ft.lens == nil {
ft.lens = map[ID]*Value{}
}
ft.lens[v.Args[0].ID] = v
case OpSliceCap:
if ft.caps == nil {
ft.caps = map[ID]*Value{}
}
ft.caps[v.Args[0].ID] = v
}
}
}
// current node state
type walkState int
const (
descend walkState = iota
simplify
)
// work maintains the DFS stack.
type bp struct {
block *Block // current handled block
state walkState // what's to do
}
work := make([]bp, 0, 256)
work = append(work, bp{
block: f.Entry,
state: descend,
})
idom := f.Idom()
sdom := f.sdom()
// DFS on the dominator tree.
for len(work) > 0 {
node := work[len(work)-1]
work = work[:len(work)-1]
parent := idom[node.block.ID]
branch := getBranch(sdom, parent, node.block)
switch node.state {
case descend:
if branch != unknown {
ft.checkpoint()
c := parent.Control
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(parent, ft, tr.d, c.Args[0], c.Args[1], tr.r, branch)
}
}
work = append(work, bp{
block: node.block,
state: simplify,
})
for s := sdom.Child(node.block); s != nil; s = sdom.Sibling(s) {
work = append(work, bp{
block: s,
state: descend,
})
}
case simplify:
succ := simplifyBlock(ft, node.block)
if succ != unknown {
b := node.block
b.Kind = BlockFirst
b.SetControl(nil)
if succ == negative {
b.swapSuccessors()
}
}
if branch != unknown {
ft.restore()
}
}
}
}
// getBranch returns the range restrictions added by p
// when reaching b. p is the immediate dominator of b.
func getBranch(sdom SparseTree, p *Block, b *Block) branch {
if p == nil || p.Kind != BlockIf {
return unknown
}
// If p and p.Succs[0] are dominators it means that every path
// from entry to b passes through p and p.Succs[0]. We care that
// no path from entry to b passes through p.Succs[1]. If p.Succs[0]
// has one predecessor then (apart from the degenerate case),
// there is no path from entry that can reach b through p.Succs[1].
// TODO: how about p->yes->b->yes, i.e. a loop in yes.
if sdom.isAncestorEq(p.Succs[0].b, b) && len(p.Succs[0].b.Preds) == 1 {
return positive
}
if sdom.isAncestorEq(p.Succs[1].b, b) && len(p.Succs[1].b.Preds) == 1 {
return negative
}
return unknown
}
// updateRestrictions updates restrictions from the immediate
// dominating block (p) using r. r is adjusted according to the branch taken.
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.
return
}
if branch == negative {
// Negative branch taken, complement the relations.
r = (lt | eq | gt) ^ r
}
for i := domain(1); i <= t; i <<= 1 {
if t&i == 0 {
continue
}
ft.update(parent, v, w, i, r)
// Additional facts we know given the relationship between len and cap.
if i != signed && i != unsigned {
continue
}
if v.Op == OpSliceLen && r< == 0 && ft.caps[v.Args[0].ID] != nil {
// len(s) > w implies cap(s) > w
// len(s) >= w implies cap(s) >= w
// len(s) == w implies cap(s) >= w
ft.update(parent, ft.caps[v.Args[0].ID], w, i, r|gt)
}
if w.Op == OpSliceLen && r> == 0 && ft.caps[w.Args[0].ID] != nil {
// same, length on the RHS.
ft.update(parent, v, ft.caps[w.Args[0].ID], i, r|lt)
}
if v.Op == OpSliceCap && r> == 0 && ft.lens[v.Args[0].ID] != nil {
// cap(s) < w implies len(s) < w
// cap(s) <= w implies len(s) <= w
// cap(s) == w implies len(s) <= w
ft.update(parent, ft.lens[v.Args[0].ID], w, i, r|lt)
}
if w.Op == OpSliceCap && r< == 0 && ft.lens[w.Args[0].ID] != nil {
// same, capacity on the RHS.
ft.update(parent, v, ft.lens[w.Args[0].ID], i, r|gt)
}
}
}
// simplifyBlock simplifies block known the restrictions in ft.
// Returns which branch must always be taken.
func simplifyBlock(ft *factsTable, b *Block) branch {
for _, v := range b.Values {
if v.Op != OpSlicemask {
continue
}
add := v.Args[0]
if add.Op != OpAdd64 && add.Op != OpAdd32 {
continue
}
// Note that the arg of slicemask was originally a sub, but
// was rewritten to an add by generic.rules (if the thing
// being subtracted was a constant).
x := add.Args[0]
y := add.Args[1]
if x.Op == OpConst64 || x.Op == OpConst32 {
x, y = y, x
}
if y.Op != OpConst64 && y.Op != OpConst32 {
continue
}
// slicemask(x + y)
// if x is larger than -y (y is negative), then slicemask is -1.
lim, ok := ft.limits[x.ID]
if !ok {
continue
}
if lim.umin > uint64(-y.AuxInt) {
if v.Args[0].Op == OpAdd64 {
v.reset(OpConst64)
} else {
v.reset(OpConst32)
}
if b.Func.pass.debug > 0 {
b.Func.Config.Warnl(v.Pos, "Proved slicemask not needed")
}
v.AuxInt = -1
}
}
if b.Kind != BlockIf {
return unknown
}
// First, checks if the condition itself is redundant.
m := ft.get(nil, b.Control, boolean)
if m == lt|gt {
if b.Func.pass.debug > 0 {
if b.Func.pass.debug > 1 {
b.Func.Config.Warnl(b.Pos, "Proved boolean %s (%s)", b.Control.Op, b.Control)
} else {
b.Func.Config.Warnl(b.Pos, "Proved boolean %s", b.Control.Op)
}
}
return positive
}
if m == eq {
if b.Func.pass.debug > 0 {
if b.Func.pass.debug > 1 {
b.Func.Config.Warnl(b.Pos, "Disproved boolean %s (%s)", b.Control.Op, b.Control)
} else {
b.Func.Config.Warnl(b.Pos, "Disproved boolean %s", b.Control.Op)
}
}
return negative
}
// Next look check equalities.
c := b.Control
tr, has := domainRelationTable[c.Op]
if !has {
return unknown
}
a0, a1 := c.Args[0], c.Args[1]
for d := domain(1); d <= tr.d; d <<= 1 {
if d&tr.d == 0 {
continue
}
// tr.r represents in which case the positive branch is taken.
// m represents which cases are possible because of previous relations.
// If the set of possible relations m is included in the set of relations
// need to take the positive branch (or negative) then that branch will
// always be taken.
// For shortcut, if m == 0 then this block is dead code.
m := ft.get(a0, a1, d)
if m != 0 && tr.r&m == m {
if b.Func.pass.debug > 0 {
if b.Func.pass.debug > 1 {
b.Func.Config.Warnl(b.Pos, "Proved %s (%s)", c.Op, c)
} else {
b.Func.Config.Warnl(b.Pos, "Proved %s", c.Op)
}
}
return positive
}
if m != 0 && ((lt|eq|gt)^tr.r)&m == m {
if b.Func.pass.debug > 0 {
if b.Func.pass.debug > 1 {
b.Func.Config.Warnl(b.Pos, "Disproved %s (%s)", c.Op, c)
} else {
b.Func.Config.Warnl(b.Pos, "Disproved %s", c.Op)
}
}
return negative
}
}
// HACK: If the first argument of IsInBounds or IsSliceInBounds
// is a constant and we already know that constant is smaller (or equal)
// to the upper bound than this is proven. Most useful in cases such as:
// if len(a) <= 1 { return }
// do something with a[1]
if (c.Op == OpIsInBounds || c.Op == OpIsSliceInBounds) && ft.isNonNegative(c.Args[0]) {
m := ft.get(a0, a1, signed)
if m != 0 && tr.r&m == m {
if b.Func.pass.debug > 0 {
if b.Func.pass.debug > 1 {
b.Func.Config.Warnl(b.Pos, "Proved non-negative bounds %s (%s)", c.Op, c)
} else {
b.Func.Config.Warnl(b.Pos, "Proved non-negative bounds %s", c.Op)
}
}
return positive
}
}
return unknown
}
// isNonNegative returns true is v is known to be greater or equal to zero.
func isNonNegative(v *Value) bool {
switch v.Op {
case OpConst64:
return v.AuxInt >= 0
case OpConst32:
return int32(v.AuxInt) >= 0
case OpStringLen, OpSliceLen, OpSliceCap,
OpZeroExt8to64, OpZeroExt16to64, OpZeroExt32to64:
return true
case OpRsh64x64:
return isNonNegative(v.Args[0])
}
return false
}