1
2
3
4
5 package ssa
6
7 import (
8 "cmd/internal/src"
9 "fmt"
10 "math"
11 )
12
13 type branch int
14
15 const (
16 unknown branch = iota
17 positive
18 negative
19 )
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41 type relation uint
42
43 const (
44 lt relation = 1 << iota
45 eq
46 gt
47 )
48
49 var relationStrings = [...]string{
50 0: "none", lt: "<", eq: "==", lt | eq: "<=",
51 gt: ">", gt | lt: "!=", gt | eq: ">=", gt | eq | lt: "any",
52 }
53
54 func (r relation) String() string {
55 if r < relation(len(relationStrings)) {
56 return relationStrings[r]
57 }
58 return fmt.Sprintf("relation(%d)", uint(r))
59 }
60
61
62
63
64
65 type domain uint
66
67 const (
68 signed domain = 1 << iota
69 unsigned
70 pointer
71 boolean
72 )
73
74 var domainStrings = [...]string{
75 "signed", "unsigned", "pointer", "boolean",
76 }
77
78 func (d domain) String() string {
79 s := ""
80 for i, ds := range domainStrings {
81 if d&(1<<uint(i)) != 0 {
82 if len(s) != 0 {
83 s += "|"
84 }
85 s += ds
86 d &^= 1 << uint(i)
87 }
88 }
89 if d != 0 {
90 if len(s) != 0 {
91 s += "|"
92 }
93 s += fmt.Sprintf("0x%x", uint(d))
94 }
95 return s
96 }
97
98 type pair struct {
99 v, w *Value
100
101
102 d domain
103 }
104
105
106 type fact struct {
107 p pair
108 r relation
109 }
110
111
112 type limit struct {
113 min, max int64
114 umin, umax uint64
115 }
116
117 func (l limit) String() string {
118 return fmt.Sprintf("sm,SM,um,UM=%d,%d,%d,%d", l.min, l.max, l.umin, l.umax)
119 }
120
121 func (l limit) intersect(l2 limit) limit {
122 if l.min < l2.min {
123 l.min = l2.min
124 }
125 if l.umin < l2.umin {
126 l.umin = l2.umin
127 }
128 if l.max > l2.max {
129 l.max = l2.max
130 }
131 if l.umax > l2.umax {
132 l.umax = l2.umax
133 }
134 return l
135 }
136
137 var noLimit = limit{math.MinInt64, math.MaxInt64, 0, math.MaxUint64}
138
139
140 type limitFact struct {
141 vid ID
142 limit limit
143 }
144
145
146
147
148
149
150
151
152 type factsTable struct {
153
154
155
156
157
158 unsat bool
159 unsatDepth int
160
161 facts map[pair]relation
162 stack []fact
163
164
165
166
167 orderS *poset
168 orderU *poset
169
170
171 limits map[ID]limit
172 limitStack []limitFact
173
174
175
176
177 lens map[ID]*Value
178 caps map[ID]*Value
179
180
181 zero *Value
182 }
183
184
185
186 var checkpointFact = fact{}
187 var checkpointBound = limitFact{}
188
189 func newFactsTable(f *Func) *factsTable {
190 ft := &factsTable{}
191 ft.orderS = f.newPoset()
192 ft.orderU = f.newPoset()
193 ft.orderS.SetUnsigned(false)
194 ft.orderU.SetUnsigned(true)
195 ft.facts = make(map[pair]relation)
196 ft.stack = make([]fact, 4)
197 ft.limits = make(map[ID]limit)
198 ft.limitStack = make([]limitFact, 4)
199 ft.zero = f.ConstInt64(f.Config.Types.Int64, 0)
200 return ft
201 }
202
203
204
205 func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
206 if parent.Func.pass.debug > 2 {
207 parent.Func.Warnl(parent.Pos, "parent=%s, update %s %s %s", parent, v, w, r)
208 }
209
210 if ft.unsat {
211 return
212 }
213
214
215
216 if v == w {
217 if r&eq == 0 {
218 ft.unsat = true
219 }
220 return
221 }
222
223 if d == signed || d == unsigned {
224 var ok bool
225 order := ft.orderS
226 if d == unsigned {
227 order = ft.orderU
228 }
229 switch r {
230 case lt:
231 ok = order.SetOrder(v, w)
232 case gt:
233 ok = order.SetOrder(w, v)
234 case lt | eq:
235 ok = order.SetOrderOrEqual(v, w)
236 case gt | eq:
237 ok = order.SetOrderOrEqual(w, v)
238 case eq:
239 ok = order.SetEqual(v, w)
240 case lt | gt:
241 ok = order.SetNonEqual(v, w)
242 default:
243 panic("unknown relation")
244 }
245 if !ok {
246 if parent.Func.pass.debug > 2 {
247 parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r)
248 }
249 ft.unsat = true
250 return
251 }
252 } else {
253 if lessByID(w, v) {
254 v, w = w, v
255 r = reverseBits[r]
256 }
257
258 p := pair{v, w, d}
259 oldR, ok := ft.facts[p]
260 if !ok {
261 if v == w {
262 oldR = eq
263 } else {
264 oldR = lt | eq | gt
265 }
266 }
267
268 if oldR == r {
269 return
270 }
271 ft.stack = append(ft.stack, fact{p, oldR})
272 ft.facts[p] = oldR & r
273
274 if oldR&r == 0 {
275 if parent.Func.pass.debug > 2 {
276 parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r)
277 }
278 ft.unsat = true
279 return
280 }
281 }
282
283
284 if v.isGenericIntConst() {
285 v, w = w, v
286 r = reverseBits[r]
287 }
288 if v != nil && w.isGenericIntConst() {
289
290
291
292
293
294 old, ok := ft.limits[v.ID]
295 if !ok {
296 old = noLimit
297 if v.isGenericIntConst() {
298 switch d {
299 case signed:
300 old.min, old.max = v.AuxInt, v.AuxInt
301 if v.AuxInt >= 0 {
302 old.umin, old.umax = uint64(v.AuxInt), uint64(v.AuxInt)
303 }
304 case unsigned:
305 old.umin = v.AuxUnsigned()
306 old.umax = old.umin
307 if int64(old.umin) >= 0 {
308 old.min, old.max = int64(old.umin), int64(old.umin)
309 }
310 }
311 }
312 }
313 lim := noLimit
314 switch d {
315 case signed:
316 c := w.AuxInt
317 switch r {
318 case lt:
319 lim.max = c - 1
320 case lt | eq:
321 lim.max = c
322 case gt | eq:
323 lim.min = c
324 case gt:
325 lim.min = c + 1
326 case lt | gt:
327 lim = old
328 if c == lim.min {
329 lim.min++
330 }
331 if c == lim.max {
332 lim.max--
333 }
334 case eq:
335 lim.min = c
336 lim.max = c
337 }
338 if lim.min >= 0 {
339
340 lim.umin = uint64(lim.min)
341 }
342 if lim.max != noLimit.max && old.min >= 0 && lim.max >= 0 {
343
344
345
346 lim.umax = uint64(lim.max)
347 }
348 case unsigned:
349 uc := w.AuxUnsigned()
350 switch r {
351 case lt:
352 lim.umax = uc - 1
353 case lt | eq:
354 lim.umax = uc
355 case gt | eq:
356 lim.umin = uc
357 case gt:
358 lim.umin = uc + 1
359 case lt | gt:
360 lim = old
361 if uc == lim.umin {
362 lim.umin++
363 }
364 if uc == lim.umax {
365 lim.umax--
366 }
367 case eq:
368 lim.umin = uc
369 lim.umax = uc
370 }
371
372
373
374 }
375 ft.limitStack = append(ft.limitStack, limitFact{v.ID, old})
376 lim = old.intersect(lim)
377 ft.limits[v.ID] = lim
378 if v.Block.Func.pass.debug > 2 {
379 v.Block.Func.Warnl(parent.Pos, "parent=%s, new limits %s %s %s %s", parent, v, w, r, lim.String())
380 }
381 if lim.min > lim.max || lim.umin > lim.umax {
382 ft.unsat = true
383 return
384 }
385 }
386
387
388 if d != signed && d != unsigned {
389 return
390 }
391
392
393
394
395
396
397 if v.Op == OpSliceLen && r< == 0 && ft.caps[v.Args[0].ID] != nil {
398
399
400
401 ft.update(parent, ft.caps[v.Args[0].ID], w, d, r|gt)
402 }
403 if w.Op == OpSliceLen && r> == 0 && ft.caps[w.Args[0].ID] != nil {
404
405 ft.update(parent, v, ft.caps[w.Args[0].ID], d, r|lt)
406 }
407 if v.Op == OpSliceCap && r> == 0 && ft.lens[v.Args[0].ID] != nil {
408
409
410
411 ft.update(parent, ft.lens[v.Args[0].ID], w, d, r|lt)
412 }
413 if w.Op == OpSliceCap && r< == 0 && ft.lens[w.Args[0].ID] != nil {
414
415 ft.update(parent, v, ft.lens[w.Args[0].ID], d, r|gt)
416 }
417
418
419
420
421 if r == lt || r == lt|eq {
422 v, w = w, v
423 r = reverseBits[r]
424 }
425 switch r {
426 case gt:
427 if x, delta := isConstDelta(v); x != nil && delta == 1 {
428
429
430
431
432 ft.update(parent, x, w, d, gt|eq)
433 } else if x, delta := isConstDelta(w); x != nil && delta == -1 {
434
435 ft.update(parent, v, x, d, gt|eq)
436 }
437 case gt | eq:
438 if x, delta := isConstDelta(v); x != nil && delta == -1 {
439
440
441
442 lim, ok := ft.limits[x.ID]
443 if ok && ((d == signed && lim.min > opMin[v.Op]) || (d == unsigned && lim.umin > 0)) {
444 ft.update(parent, x, w, d, gt)
445 }
446 } else if x, delta := isConstDelta(w); x != nil && delta == 1 {
447
448 lim, ok := ft.limits[x.ID]
449 if ok && ((d == signed && lim.max < opMax[w.Op]) || (d == unsigned && lim.umax < opUMax[w.Op])) {
450 ft.update(parent, v, x, d, gt)
451 }
452 }
453 }
454
455
456
457 if r == gt || r == gt|eq {
458 if x, delta := isConstDelta(v); x != nil && d == signed {
459 if parent.Func.pass.debug > 1 {
460 parent.Func.Warnl(parent.Pos, "x+d %s w; x:%v %v delta:%v w:%v d:%v", r, x, parent.String(), delta, w.AuxInt, d)
461 }
462 if !w.isGenericIntConst() {
463
464
465
466 if l, has := ft.limits[x.ID]; has && delta < 0 {
467 if (x.Type.Size() == 8 && l.min >= math.MinInt64-delta) ||
468 (x.Type.Size() == 4 && l.min >= math.MinInt32-delta) {
469 ft.update(parent, x, w, signed, r)
470 }
471 }
472 } else {
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490 var min, max int64
491 var vmin, vmax *Value
492 switch x.Type.Size() {
493 case 8:
494 min = w.AuxInt - delta
495 max = int64(^uint64(0)>>1) - delta
496
497 vmin = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, min)
498 vmax = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, max)
499
500 case 4:
501 min = int64(int32(w.AuxInt) - int32(delta))
502 max = int64(int32(^uint32(0)>>1) - int32(delta))
503
504 vmin = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, min)
505 vmax = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, max)
506
507 default:
508 panic("unimplemented")
509 }
510
511 if min < max {
512
513 ft.update(parent, x, vmin, d, r)
514 ft.update(parent, vmax, x, d, r|eq)
515 } else {
516
517
518
519 if l, has := ft.limits[x.ID]; has {
520 if l.max <= min {
521 if r&eq == 0 || l.max < min {
522
523 ft.update(parent, vmax, x, d, r|eq)
524 }
525 } else if l.min > max {
526
527 ft.update(parent, x, vmin, d, r)
528 }
529 }
530 }
531 }
532 }
533 }
534
535
536
537
538 if isCleanExt(v) {
539 switch {
540 case d == signed && v.Args[0].Type.IsSigned():
541 fallthrough
542 case d == unsigned && !v.Args[0].Type.IsSigned():
543 ft.update(parent, v.Args[0], w, d, r)
544 }
545 }
546 if isCleanExt(w) {
547 switch {
548 case d == signed && w.Args[0].Type.IsSigned():
549 fallthrough
550 case d == unsigned && !w.Args[0].Type.IsSigned():
551 ft.update(parent, v, w.Args[0], d, r)
552 }
553 }
554 }
555
556 var opMin = map[Op]int64{
557 OpAdd64: math.MinInt64, OpSub64: math.MinInt64,
558 OpAdd32: math.MinInt32, OpSub32: math.MinInt32,
559 }
560
561 var opMax = map[Op]int64{
562 OpAdd64: math.MaxInt64, OpSub64: math.MaxInt64,
563 OpAdd32: math.MaxInt32, OpSub32: math.MaxInt32,
564 }
565
566 var opUMax = map[Op]uint64{
567 OpAdd64: math.MaxUint64, OpSub64: math.MaxUint64,
568 OpAdd32: math.MaxUint32, OpSub32: math.MaxUint32,
569 }
570
571
572 func (ft *factsTable) isNonNegative(v *Value) bool {
573 if isNonNegative(v) {
574 return true
575 }
576
577 var max int64
578 switch v.Type.Size() {
579 case 1:
580 max = math.MaxInt8
581 case 2:
582 max = math.MaxInt16
583 case 4:
584 max = math.MaxInt32
585 case 8:
586 max = math.MaxInt64
587 default:
588 panic("unexpected integer size")
589 }
590
591
592
593 if l, has := ft.limits[v.ID]; has && (l.min >= 0 || l.umax <= uint64(max)) {
594 return true
595 }
596
597
598 if x, delta := isConstDelta(v); x != nil {
599 if l, has := ft.limits[x.ID]; has {
600 if delta > 0 && l.min >= -delta && l.max <= max-delta {
601 return true
602 }
603 if delta < 0 && l.min >= -delta {
604 return true
605 }
606 }
607 }
608
609
610 if isCleanExt(v) && ft.isNonNegative(v.Args[0]) {
611 return true
612 }
613
614
615 return ft.orderS.OrderedOrEqual(ft.zero, v)
616 }
617
618
619
620 func (ft *factsTable) checkpoint() {
621 if ft.unsat {
622 ft.unsatDepth++
623 }
624 ft.stack = append(ft.stack, checkpointFact)
625 ft.limitStack = append(ft.limitStack, checkpointBound)
626 ft.orderS.Checkpoint()
627 ft.orderU.Checkpoint()
628 }
629
630
631
632
633 func (ft *factsTable) restore() {
634 if ft.unsatDepth > 0 {
635 ft.unsatDepth--
636 } else {
637 ft.unsat = false
638 }
639 for {
640 old := ft.stack[len(ft.stack)-1]
641 ft.stack = ft.stack[:len(ft.stack)-1]
642 if old == checkpointFact {
643 break
644 }
645 if old.r == lt|eq|gt {
646 delete(ft.facts, old.p)
647 } else {
648 ft.facts[old.p] = old.r
649 }
650 }
651 for {
652 old := ft.limitStack[len(ft.limitStack)-1]
653 ft.limitStack = ft.limitStack[:len(ft.limitStack)-1]
654 if old.vid == 0 {
655 break
656 }
657 if old.limit == noLimit {
658 delete(ft.limits, old.vid)
659 } else {
660 ft.limits[old.vid] = old.limit
661 }
662 }
663 ft.orderS.Undo()
664 ft.orderU.Undo()
665 }
666
667 func lessByID(v, w *Value) bool {
668 if v == nil && w == nil {
669
670 return false
671 }
672 if v == nil {
673 return true
674 }
675 return w != nil && v.ID < w.ID
676 }
677
678 var (
679 reverseBits = [...]relation{0, 4, 2, 6, 1, 5, 3, 7}
680
681
682
683
684
685
686
687 domainRelationTable = map[Op]struct {
688 d domain
689 r relation
690 }{
691 OpEq8: {signed | unsigned, eq},
692 OpEq16: {signed | unsigned, eq},
693 OpEq32: {signed | unsigned, eq},
694 OpEq64: {signed | unsigned, eq},
695 OpEqPtr: {pointer, eq},
696
697 OpNeq8: {signed | unsigned, lt | gt},
698 OpNeq16: {signed | unsigned, lt | gt},
699 OpNeq32: {signed | unsigned, lt | gt},
700 OpNeq64: {signed | unsigned, lt | gt},
701 OpNeqPtr: {pointer, lt | gt},
702
703 OpLess8: {signed, lt},
704 OpLess8U: {unsigned, lt},
705 OpLess16: {signed, lt},
706 OpLess16U: {unsigned, lt},
707 OpLess32: {signed, lt},
708 OpLess32U: {unsigned, lt},
709 OpLess64: {signed, lt},
710 OpLess64U: {unsigned, lt},
711
712 OpLeq8: {signed, lt | eq},
713 OpLeq8U: {unsigned, lt | eq},
714 OpLeq16: {signed, lt | eq},
715 OpLeq16U: {unsigned, lt | eq},
716 OpLeq32: {signed, lt | eq},
717 OpLeq32U: {unsigned, lt | eq},
718 OpLeq64: {signed, lt | eq},
719 OpLeq64U: {unsigned, lt | eq},
720
721
722
723
724 OpIsInBounds: {signed | unsigned, lt},
725 OpIsSliceInBounds: {signed | unsigned, lt | eq},
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 func prove(f *Func) {
761 ft := newFactsTable(f)
762 ft.checkpoint()
763
764 var lensVars map[*Block][]*Value
765
766
767 for _, b := range f.Blocks {
768 for _, v := range b.Values {
769 if v.Uses == 0 {
770
771
772 continue
773 }
774 switch v.Op {
775 case OpStringLen:
776 ft.update(b, v, ft.zero, signed, gt|eq)
777 case OpSliceLen:
778 if ft.lens == nil {
779 ft.lens = map[ID]*Value{}
780 }
781 ft.lens[v.Args[0].ID] = v
782 ft.update(b, v, ft.zero, signed, gt|eq)
783 if v.Args[0].Op == OpSliceMake {
784 if lensVars == nil {
785 lensVars = make(map[*Block][]*Value)
786 }
787 lensVars[b] = append(lensVars[b], v)
788 }
789 case OpSliceCap:
790 if ft.caps == nil {
791 ft.caps = map[ID]*Value{}
792 }
793 ft.caps[v.Args[0].ID] = v
794 ft.update(b, v, ft.zero, signed, gt|eq)
795 if v.Args[0].Op == OpSliceMake {
796 if lensVars == nil {
797 lensVars = make(map[*Block][]*Value)
798 }
799 lensVars[b] = append(lensVars[b], v)
800 }
801 }
802 }
803 }
804
805
806
807 var indVars map[*Block]indVar
808 for _, v := range findIndVar(f) {
809 if indVars == nil {
810 indVars = make(map[*Block]indVar)
811 }
812 indVars[v.entry] = v
813 }
814
815
816 type walkState int
817 const (
818 descend walkState = iota
819 simplify
820 )
821
822 type bp struct {
823 block *Block
824 state walkState
825 }
826 work := make([]bp, 0, 256)
827 work = append(work, bp{
828 block: f.Entry,
829 state: descend,
830 })
831
832 idom := f.Idom()
833 sdom := f.Sdom()
834
835
836
837
838
839
840
841
842
843
844
845 for len(work) > 0 {
846 node := work[len(work)-1]
847 work = work[:len(work)-1]
848 parent := idom[node.block.ID]
849 branch := getBranch(sdom, parent, node.block)
850
851 switch node.state {
852 case descend:
853 ft.checkpoint()
854
855
856
857 if iv, ok := indVars[node.block]; ok {
858 addIndVarRestrictions(ft, parent, iv)
859 }
860 if lens, ok := lensVars[node.block]; ok {
861 for _, v := range lens {
862 switch v.Op {
863 case OpSliceLen:
864 ft.update(node.block, v, v.Args[0].Args[1], signed, eq)
865 case OpSliceCap:
866 ft.update(node.block, v, v.Args[0].Args[2], signed, eq)
867 }
868 }
869 }
870
871 if branch != unknown {
872 addBranchRestrictions(ft, parent, branch)
873 if ft.unsat {
874
875
876
877 removeBranch(parent, branch)
878 ft.restore()
879 break
880 }
881
882
883
884 }
885
886
887 addLocalInductiveFacts(ft, node.block)
888
889 work = append(work, bp{
890 block: node.block,
891 state: simplify,
892 })
893 for s := sdom.Child(node.block); s != nil; s = sdom.Sibling(s) {
894 work = append(work, bp{
895 block: s,
896 state: descend,
897 })
898 }
899
900 case simplify:
901 simplifyBlock(sdom, ft, node.block)
902 ft.restore()
903 }
904 }
905
906 ft.restore()
907
908
909 for _, po := range []*poset{ft.orderS, ft.orderU} {
910
911
912 if checkEnabled {
913 if err := po.CheckEmpty(); err != nil {
914 f.Fatalf("prove poset not empty after function %s: %v", f.Name, err)
915 }
916 }
917 f.retPoset(po)
918 }
919 }
920
921
922
923 func getBranch(sdom SparseTree, p *Block, b *Block) branch {
924 if p == nil || p.Kind != BlockIf {
925 return unknown
926 }
927
928
929
930
931
932
933 if sdom.IsAncestorEq(p.Succs[0].b, b) && len(p.Succs[0].b.Preds) == 1 {
934 return positive
935 }
936 if sdom.IsAncestorEq(p.Succs[1].b, b) && len(p.Succs[1].b.Preds) == 1 {
937 return negative
938 }
939 return unknown
940 }
941
942
943
944
945 func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) {
946 d := signed
947 if ft.isNonNegative(iv.min) && ft.isNonNegative(iv.max) {
948 d |= unsigned
949 }
950
951 if iv.flags&indVarMinExc == 0 {
952 addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq)
953 } else {
954 addRestrictions(b, ft, d, iv.min, iv.ind, lt)
955 }
956
957 if iv.flags&indVarMaxInc == 0 {
958 addRestrictions(b, ft, d, iv.ind, iv.max, lt)
959 } else {
960 addRestrictions(b, ft, d, iv.ind, iv.max, lt|eq)
961 }
962 }
963
964
965
966 func addBranchRestrictions(ft *factsTable, b *Block, br branch) {
967 c := b.Controls[0]
968 switch br {
969 case negative:
970 addRestrictions(b, ft, boolean, nil, c, eq)
971 case positive:
972 addRestrictions(b, ft, boolean, nil, c, lt|gt)
973 default:
974 panic("unknown branch")
975 }
976 if tr, has := domainRelationTable[c.Op]; has {
977
978
979 d := tr.d
980 if d == signed && ft.isNonNegative(c.Args[0]) && ft.isNonNegative(c.Args[1]) {
981 d |= unsigned
982 }
983 switch c.Op {
984 case OpIsInBounds, OpIsSliceInBounds:
985
986
987
988
989
990
991
992
993
994
995
996
997
998 switch br {
999 case negative:
1000 d = unsigned
1001 if ft.isNonNegative(c.Args[0]) {
1002 d |= signed
1003 }
1004 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq))
1005 case positive:
1006 addRestrictions(b, ft, signed, ft.zero, c.Args[0], lt|eq)
1007 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r)
1008 }
1009 default:
1010 switch br {
1011 case negative:
1012 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq))
1013 case positive:
1014 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r)
1015 }
1016 }
1017
1018 }
1019 }
1020
1021
1022
1023 func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r relation) {
1024 if t == 0 {
1025
1026
1027 return
1028 }
1029 for i := domain(1); i <= t; i <<= 1 {
1030 if t&i == 0 {
1031 continue
1032 }
1033 ft.update(parent, v, w, i, r)
1034 }
1035 }
1036
1037
1038
1039
1040
1041
1042
1043
1044 func addLocalInductiveFacts(ft *factsTable, b *Block) {
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055 if len(b.Preds) != 2 {
1056 return
1057 }
1058
1059 for _, i1 := range b.Values {
1060 if i1.Op != OpPhi {
1061 continue
1062 }
1063
1064
1065
1066 min, i2 := i1.Args[0], i1.Args[1]
1067 if i1q, delta := isConstDelta(i2); i1q != i1 || delta != 1 {
1068 continue
1069 }
1070
1071
1072
1073
1074
1075
1076
1077
1078 uniquePred := func(b *Block) *Block {
1079 if len(b.Preds) == 1 {
1080 return b.Preds[0].b
1081 }
1082 return nil
1083 }
1084 pred, child := b.Preds[1].b, b
1085 for ; pred != nil; pred, child = uniquePred(pred), pred {
1086 if pred.Kind != BlockIf {
1087 continue
1088 }
1089 control := pred.Controls[0]
1090
1091 br := unknown
1092 if pred.Succs[0].b == child {
1093 br = positive
1094 }
1095 if pred.Succs[1].b == child {
1096 if br != unknown {
1097 continue
1098 }
1099 br = negative
1100 }
1101 if br == unknown {
1102 continue
1103 }
1104
1105 tr, has := domainRelationTable[control.Op]
1106 if !has {
1107 continue
1108 }
1109 r := tr.r
1110 if br == negative {
1111
1112
1113 r = (lt | eq | gt) ^ r
1114 }
1115
1116
1117 var max *Value
1118 if r == lt && control.Args[0] == i2 {
1119 max = control.Args[1]
1120 } else if r == gt && control.Args[1] == i2 {
1121 max = control.Args[0]
1122 } else {
1123 continue
1124 }
1125
1126
1127
1128
1129
1130
1131 ft.checkpoint()
1132 ft.update(b, min, max, tr.d, gt|eq)
1133 proved := ft.unsat
1134 ft.restore()
1135
1136 if proved {
1137
1138 if b.Func.pass.debug > 0 {
1139 printIndVar(b, i1, min, max, 1, 0)
1140 }
1141 ft.update(b, min, i1, tr.d, lt|eq)
1142 ft.update(b, i1, max, tr.d, lt)
1143 }
1144 }
1145 }
1146 }
1147
1148 var ctzNonZeroOp = map[Op]Op{OpCtz8: OpCtz8NonZero, OpCtz16: OpCtz16NonZero, OpCtz32: OpCtz32NonZero, OpCtz64: OpCtz64NonZero}
1149 var mostNegativeDividend = map[Op]int64{
1150 OpDiv16: -1 << 15,
1151 OpMod16: -1 << 15,
1152 OpDiv32: -1 << 31,
1153 OpMod32: -1 << 31,
1154 OpDiv64: -1 << 63,
1155 OpMod64: -1 << 63}
1156
1157
1158
1159 func simplifyBlock(sdom SparseTree, ft *factsTable, b *Block) {
1160 for _, v := range b.Values {
1161 switch v.Op {
1162 case OpSlicemask:
1163
1164 x, delta := isConstDelta(v.Args[0])
1165 if x == nil {
1166 continue
1167 }
1168
1169
1170 lim, ok := ft.limits[x.ID]
1171 if !ok {
1172 continue
1173 }
1174 if lim.umin > uint64(-delta) {
1175 if v.Args[0].Op == OpAdd64 {
1176 v.reset(OpConst64)
1177 } else {
1178 v.reset(OpConst32)
1179 }
1180 if b.Func.pass.debug > 0 {
1181 b.Func.Warnl(v.Pos, "Proved slicemask not needed")
1182 }
1183 v.AuxInt = -1
1184 }
1185 case OpCtz8, OpCtz16, OpCtz32, OpCtz64:
1186
1187
1188
1189 x := v.Args[0]
1190 lim, ok := ft.limits[x.ID]
1191 if !ok {
1192 continue
1193 }
1194 if lim.umin > 0 || lim.min > 0 || lim.max < 0 {
1195 if b.Func.pass.debug > 0 {
1196 b.Func.Warnl(v.Pos, "Proved %v non-zero", v.Op)
1197 }
1198 v.Op = ctzNonZeroOp[v.Op]
1199 }
1200 case OpRsh8x8, OpRsh8x16, OpRsh8x32, OpRsh8x64,
1201 OpRsh16x8, OpRsh16x16, OpRsh16x32, OpRsh16x64,
1202 OpRsh32x8, OpRsh32x16, OpRsh32x32, OpRsh32x64,
1203 OpRsh64x8, OpRsh64x16, OpRsh64x32, OpRsh64x64:
1204
1205
1206 bits := 8 * v.Type.Size()
1207 if v.Args[1].isGenericIntConst() && v.Args[1].AuxInt >= bits-1 && ft.isNonNegative(v.Args[0]) {
1208 if b.Func.pass.debug > 0 {
1209 b.Func.Warnl(v.Pos, "Proved %v shifts to zero", v.Op)
1210 }
1211 switch bits {
1212 case 64:
1213 v.reset(OpConst64)
1214 case 32:
1215 v.reset(OpConst32)
1216 case 16:
1217 v.reset(OpConst16)
1218 case 8:
1219 v.reset(OpConst8)
1220 default:
1221 panic("unexpected integer size")
1222 }
1223 v.AuxInt = 0
1224 continue
1225 }
1226
1227 fallthrough
1228 case OpLsh8x8, OpLsh8x16, OpLsh8x32, OpLsh8x64,
1229 OpLsh16x8, OpLsh16x16, OpLsh16x32, OpLsh16x64,
1230 OpLsh32x8, OpLsh32x16, OpLsh32x32, OpLsh32x64,
1231 OpLsh64x8, OpLsh64x16, OpLsh64x32, OpLsh64x64,
1232 OpRsh8Ux8, OpRsh8Ux16, OpRsh8Ux32, OpRsh8Ux64,
1233 OpRsh16Ux8, OpRsh16Ux16, OpRsh16Ux32, OpRsh16Ux64,
1234 OpRsh32Ux8, OpRsh32Ux16, OpRsh32Ux32, OpRsh32Ux64,
1235 OpRsh64Ux8, OpRsh64Ux16, OpRsh64Ux32, OpRsh64Ux64:
1236
1237
1238 by := v.Args[1]
1239 lim, ok := ft.limits[by.ID]
1240 if !ok {
1241 continue
1242 }
1243 bits := 8 * v.Args[0].Type.Size()
1244 if lim.umax < uint64(bits) || (lim.max < bits && ft.isNonNegative(by)) {
1245 v.AuxInt = 1
1246 if b.Func.pass.debug > 0 {
1247 b.Func.Warnl(v.Pos, "Proved %v bounded", v.Op)
1248 }
1249 }
1250 case OpDiv16, OpDiv32, OpDiv64, OpMod16, OpMod32, OpMod64:
1251
1252
1253
1254
1255
1256 if b.Func.Config.arch != "386" && b.Func.Config.arch != "amd64" {
1257 break
1258 }
1259 divr := v.Args[1]
1260 divrLim, divrLimok := ft.limits[divr.ID]
1261 divd := v.Args[0]
1262 divdLim, divdLimok := ft.limits[divd.ID]
1263 if (divrLimok && (divrLim.max < -1 || divrLim.min > -1)) ||
1264 (divdLimok && divdLim.min > mostNegativeDividend[v.Op]) {
1265
1266
1267
1268
1269 v.AuxInt = 1
1270 if b.Func.pass.debug > 0 {
1271 b.Func.Warnl(v.Pos, "Proved %v does not need fix-up", v.Op)
1272 }
1273 }
1274 }
1275 }
1276
1277 if b.Kind != BlockIf {
1278 return
1279 }
1280
1281
1282 parent := b
1283 for i, branch := range [...]branch{positive, negative} {
1284 child := parent.Succs[i].b
1285 if getBranch(sdom, parent, child) != unknown {
1286
1287
1288 continue
1289 }
1290
1291
1292 ft.checkpoint()
1293 addBranchRestrictions(ft, parent, branch)
1294 unsat := ft.unsat
1295 ft.restore()
1296 if unsat {
1297
1298
1299 removeBranch(parent, branch)
1300
1301
1302
1303
1304
1305 break
1306 }
1307 }
1308 }
1309
1310 func removeBranch(b *Block, branch branch) {
1311 c := b.Controls[0]
1312 if b.Func.pass.debug > 0 {
1313 verb := "Proved"
1314 if branch == positive {
1315 verb = "Disproved"
1316 }
1317 if b.Func.pass.debug > 1 {
1318 b.Func.Warnl(b.Pos, "%s %s (%s)", verb, c.Op, c)
1319 } else {
1320 b.Func.Warnl(b.Pos, "%s %s", verb, c.Op)
1321 }
1322 }
1323 if c != nil && c.Pos.IsStmt() == src.PosIsStmt && c.Pos.SameFileAndLine(b.Pos) {
1324
1325 b.Pos = b.Pos.WithIsStmt()
1326 }
1327 b.Kind = BlockFirst
1328 b.ResetControls()
1329 if branch == positive {
1330 b.swapSuccessors()
1331 }
1332 }
1333
1334
1335 func isNonNegative(v *Value) bool {
1336 if !v.Type.IsInteger() {
1337 v.Fatalf("isNonNegative bad type: %v", v.Type)
1338 }
1339
1340
1341
1342
1343 switch v.Op {
1344 case OpConst64:
1345 return v.AuxInt >= 0
1346
1347 case OpConst32:
1348 return int32(v.AuxInt) >= 0
1349
1350 case OpConst16:
1351 return int16(v.AuxInt) >= 0
1352
1353 case OpConst8:
1354 return int8(v.AuxInt) >= 0
1355
1356 case OpStringLen, OpSliceLen, OpSliceCap,
1357 OpZeroExt8to64, OpZeroExt16to64, OpZeroExt32to64,
1358 OpZeroExt8to32, OpZeroExt16to32, OpZeroExt8to16,
1359 OpCtz64, OpCtz32, OpCtz16, OpCtz8:
1360 return true
1361
1362 case OpRsh64Ux64, OpRsh32Ux64:
1363 by := v.Args[1]
1364 return by.Op == OpConst64 && by.AuxInt > 0
1365
1366 case OpRsh64x64, OpRsh32x64, OpRsh8x64, OpRsh16x64, OpRsh32x32, OpRsh64x32,
1367 OpSignExt32to64, OpSignExt16to64, OpSignExt8to64, OpSignExt16to32, OpSignExt8to32:
1368 return isNonNegative(v.Args[0])
1369
1370 case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
1371 return isNonNegative(v.Args[0]) || isNonNegative(v.Args[1])
1372
1373 case OpMod64, OpMod32, OpMod16, OpMod8,
1374 OpDiv64, OpDiv32, OpDiv16, OpDiv8,
1375 OpOr64, OpOr32, OpOr16, OpOr8,
1376 OpXor64, OpXor32, OpXor16, OpXor8:
1377 return isNonNegative(v.Args[0]) && isNonNegative(v.Args[1])
1378
1379
1380
1381 }
1382 return false
1383 }
1384
1385
1386 func isConstDelta(v *Value) (w *Value, delta int64) {
1387 cop := OpConst64
1388 switch v.Op {
1389 case OpAdd32, OpSub32:
1390 cop = OpConst32
1391 }
1392 switch v.Op {
1393 case OpAdd64, OpAdd32:
1394 if v.Args[0].Op == cop {
1395 return v.Args[1], v.Args[0].AuxInt
1396 }
1397 if v.Args[1].Op == cop {
1398 return v.Args[0], v.Args[1].AuxInt
1399 }
1400 case OpSub64, OpSub32:
1401 if v.Args[1].Op == cop {
1402 aux := v.Args[1].AuxInt
1403 if aux != -aux {
1404 return v.Args[0], -aux
1405 }
1406 }
1407 }
1408 return nil, 0
1409 }
1410
1411
1412
1413 func isCleanExt(v *Value) bool {
1414 switch v.Op {
1415 case OpSignExt8to16, OpSignExt8to32, OpSignExt8to64,
1416 OpSignExt16to32, OpSignExt16to64, OpSignExt32to64:
1417
1418 return v.Args[0].Type.IsSigned() && v.Type.IsSigned()
1419
1420 case OpZeroExt8to16, OpZeroExt8to32, OpZeroExt8to64,
1421 OpZeroExt16to32, OpZeroExt16to64, OpZeroExt32to64:
1422
1423 return !v.Args[0].Type.IsSigned()
1424 }
1425 return false
1426 }
1427
View as plain text