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 jumpTable0
23 )
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45 type relation uint
46
47 const (
48 lt relation = 1 << iota
49 eq
50 gt
51 )
52
53 var relationStrings = [...]string{
54 0: "none", lt: "<", eq: "==", lt | eq: "<=",
55 gt: ">", gt | lt: "!=", gt | eq: ">=", gt | eq | lt: "any",
56 }
57
58 func (r relation) String() string {
59 if r < relation(len(relationStrings)) {
60 return relationStrings[r]
61 }
62 return fmt.Sprintf("relation(%d)", uint(r))
63 }
64
65
66
67
68
69 type domain uint
70
71 const (
72 signed domain = 1 << iota
73 unsigned
74 pointer
75 boolean
76 )
77
78 var domainStrings = [...]string{
79 "signed", "unsigned", "pointer", "boolean",
80 }
81
82 func (d domain) String() string {
83 s := ""
84 for i, ds := range domainStrings {
85 if d&(1<<uint(i)) != 0 {
86 if len(s) != 0 {
87 s += "|"
88 }
89 s += ds
90 d &^= 1 << uint(i)
91 }
92 }
93 if d != 0 {
94 if len(s) != 0 {
95 s += "|"
96 }
97 s += fmt.Sprintf("0x%x", uint(d))
98 }
99 return s
100 }
101
102 type pair struct {
103
104
105
106 v, w *Value
107 d domain
108 }
109
110
111 type fact struct {
112 p pair
113 r relation
114 }
115
116
117 type limit struct {
118 min, max int64
119 umin, umax uint64
120 }
121
122 func (l limit) String() string {
123 return fmt.Sprintf("sm,SM,um,UM=%d,%d,%d,%d", l.min, l.max, l.umin, l.umax)
124 }
125
126 func (l limit) intersect(l2 limit) limit {
127 if l.min < l2.min {
128 l.min = l2.min
129 }
130 if l.umin < l2.umin {
131 l.umin = l2.umin
132 }
133 if l.max > l2.max {
134 l.max = l2.max
135 }
136 if l.umax > l2.umax {
137 l.umax = l2.umax
138 }
139 return l
140 }
141
142 var noLimit = limit{math.MinInt64, math.MaxInt64, 0, math.MaxUint64}
143
144
145 type limitFact struct {
146 vid ID
147 limit limit
148 }
149
150
151
152
153
154
155
156
157 type factsTable struct {
158
159
160
161
162
163 unsat bool
164 unsatDepth int
165
166 facts map[pair]relation
167 stack []fact
168
169
170
171
172 orderS *poset
173 orderU *poset
174
175
176 limits map[ID]limit
177 limitStack []limitFact
178
179
180
181
182 lens map[ID]*Value
183 caps map[ID]*Value
184
185
186 zero *Value
187 }
188
189
190
191 var checkpointFact = fact{}
192 var checkpointBound = limitFact{}
193
194 func newFactsTable(f *Func) *factsTable {
195 ft := &factsTable{}
196 ft.orderS = f.newPoset()
197 ft.orderU = f.newPoset()
198 ft.orderS.SetUnsigned(false)
199 ft.orderU.SetUnsigned(true)
200 ft.facts = make(map[pair]relation)
201 ft.stack = make([]fact, 4)
202 ft.limits = make(map[ID]limit)
203 ft.limitStack = make([]limitFact, 4)
204 ft.zero = f.ConstInt64(f.Config.Types.Int64, 0)
205 return ft
206 }
207
208
209
210 func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
211 if parent.Func.pass.debug > 2 {
212 parent.Func.Warnl(parent.Pos, "parent=%s, update %s %s %s", parent, v, w, r)
213 }
214
215 if ft.unsat {
216 return
217 }
218
219
220
221 if v == w {
222 if r&eq == 0 {
223 ft.unsat = true
224 }
225 return
226 }
227
228 if d == signed || d == unsigned {
229 var ok bool
230 order := ft.orderS
231 if d == unsigned {
232 order = ft.orderU
233 }
234 switch r {
235 case lt:
236 ok = order.SetOrder(v, w)
237 case gt:
238 ok = order.SetOrder(w, v)
239 case lt | eq:
240 ok = order.SetOrderOrEqual(v, w)
241 case gt | eq:
242 ok = order.SetOrderOrEqual(w, v)
243 case eq:
244 ok = order.SetEqual(v, w)
245 case lt | gt:
246 ok = order.SetNonEqual(v, w)
247 default:
248 panic("unknown relation")
249 }
250 if !ok {
251 if parent.Func.pass.debug > 2 {
252 parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r)
253 }
254 ft.unsat = true
255 return
256 }
257 } else {
258 if lessByID(w, v) {
259 v, w = w, v
260 r = reverseBits[r]
261 }
262
263 p := pair{v, w, d}
264 oldR, ok := ft.facts[p]
265 if !ok {
266 if v == w {
267 oldR = eq
268 } else {
269 oldR = lt | eq | gt
270 }
271 }
272
273 if oldR == r {
274 return
275 }
276 ft.stack = append(ft.stack, fact{p, oldR})
277 ft.facts[p] = oldR & r
278
279 if oldR&r == 0 {
280 if parent.Func.pass.debug > 2 {
281 parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r)
282 }
283 ft.unsat = true
284 return
285 }
286 }
287
288
289 if v.isGenericIntConst() {
290 v, w = w, v
291 r = reverseBits[r]
292 }
293 if v != nil && w.isGenericIntConst() {
294
295
296
297
298
299 old, ok := ft.limits[v.ID]
300 if !ok {
301 old = noLimit
302 if v.isGenericIntConst() {
303 switch d {
304 case signed:
305 old.min, old.max = v.AuxInt, v.AuxInt
306 if v.AuxInt >= 0 {
307 old.umin, old.umax = uint64(v.AuxInt), uint64(v.AuxInt)
308 }
309 case unsigned:
310 old.umin = v.AuxUnsigned()
311 old.umax = old.umin
312 if int64(old.umin) >= 0 {
313 old.min, old.max = int64(old.umin), int64(old.umin)
314 }
315 }
316 }
317 }
318 lim := noLimit
319 switch d {
320 case signed:
321 c := w.AuxInt
322 switch r {
323 case lt:
324 lim.max = c - 1
325 case lt | eq:
326 lim.max = c
327 case gt | eq:
328 lim.min = c
329 case gt:
330 lim.min = c + 1
331 case lt | gt:
332 lim = old
333 if c == lim.min {
334 lim.min++
335 }
336 if c == lim.max {
337 lim.max--
338 }
339 case eq:
340 lim.min = c
341 lim.max = c
342 }
343 if lim.min >= 0 {
344
345 lim.umin = uint64(lim.min)
346 }
347 if lim.max != noLimit.max && old.min >= 0 && lim.max >= 0 {
348
349
350
351 lim.umax = uint64(lim.max)
352 }
353 case unsigned:
354 uc := w.AuxUnsigned()
355 switch r {
356 case lt:
357 lim.umax = uc - 1
358 case lt | eq:
359 lim.umax = uc
360 case gt | eq:
361 lim.umin = uc
362 case gt:
363 lim.umin = uc + 1
364 case lt | gt:
365 lim = old
366 if uc == lim.umin {
367 lim.umin++
368 }
369 if uc == lim.umax {
370 lim.umax--
371 }
372 case eq:
373 lim.umin = uc
374 lim.umax = uc
375 }
376
377
378
379 }
380 ft.limitStack = append(ft.limitStack, limitFact{v.ID, old})
381 lim = old.intersect(lim)
382 ft.limits[v.ID] = lim
383 if v.Block.Func.pass.debug > 2 {
384 v.Block.Func.Warnl(parent.Pos, "parent=%s, new limits %s %s %s %s", parent, v, w, r, lim.String())
385 }
386 if lim.min > lim.max || lim.umin > lim.umax {
387 ft.unsat = true
388 return
389 }
390 }
391
392
393 if d != signed && d != unsigned {
394 return
395 }
396
397
398
399
400
401
402 if v.Op == OpSliceLen && r< == 0 && ft.caps[v.Args[0].ID] != nil {
403
404
405
406 ft.update(parent, ft.caps[v.Args[0].ID], w, d, r|gt)
407 }
408 if w.Op == OpSliceLen && r> == 0 && ft.caps[w.Args[0].ID] != nil {
409
410 ft.update(parent, v, ft.caps[w.Args[0].ID], d, r|lt)
411 }
412 if v.Op == OpSliceCap && r> == 0 && ft.lens[v.Args[0].ID] != nil {
413
414
415
416 ft.update(parent, ft.lens[v.Args[0].ID], w, d, r|lt)
417 }
418 if w.Op == OpSliceCap && r< == 0 && ft.lens[w.Args[0].ID] != nil {
419
420 ft.update(parent, v, ft.lens[w.Args[0].ID], d, r|gt)
421 }
422
423
424
425
426 if r == lt || r == lt|eq {
427 v, w = w, v
428 r = reverseBits[r]
429 }
430 switch r {
431 case gt:
432 if x, delta := isConstDelta(v); x != nil && delta == 1 {
433
434
435
436
437 ft.update(parent, x, w, d, gt|eq)
438 } else if x, delta := isConstDelta(w); x != nil && delta == -1 {
439
440 ft.update(parent, v, x, d, gt|eq)
441 }
442 case gt | eq:
443 if x, delta := isConstDelta(v); x != nil && delta == -1 {
444
445
446
447 lim, ok := ft.limits[x.ID]
448 if ok && ((d == signed && lim.min > opMin[v.Op]) || (d == unsigned && lim.umin > 0)) {
449 ft.update(parent, x, w, d, gt)
450 }
451 } else if x, delta := isConstDelta(w); x != nil && delta == 1 {
452
453 lim, ok := ft.limits[x.ID]
454 if ok && ((d == signed && lim.max < opMax[w.Op]) || (d == unsigned && lim.umax < opUMax[w.Op])) {
455 ft.update(parent, v, x, d, gt)
456 }
457 }
458 }
459
460
461
462 if r == gt || r == gt|eq {
463 if x, delta := isConstDelta(v); x != nil && d == signed {
464 if parent.Func.pass.debug > 1 {
465 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)
466 }
467 underflow := true
468 if l, has := ft.limits[x.ID]; has && delta < 0 {
469 if (x.Type.Size() == 8 && l.min >= math.MinInt64-delta) ||
470 (x.Type.Size() == 4 && l.min >= math.MinInt32-delta) {
471 underflow = false
472 }
473 }
474 if delta < 0 && !underflow {
475
476 ft.update(parent, x, v, signed, gt)
477 }
478 if !w.isGenericIntConst() {
479
480
481
482 if delta < 0 && !underflow {
483 ft.update(parent, x, w, signed, r)
484 }
485 } else {
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503 var min, max int64
504 var vmin, vmax *Value
505 switch x.Type.Size() {
506 case 8:
507 min = w.AuxInt - delta
508 max = int64(^uint64(0)>>1) - delta
509
510 vmin = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, min)
511 vmax = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, max)
512
513 case 4:
514 min = int64(int32(w.AuxInt) - int32(delta))
515 max = int64(int32(^uint32(0)>>1) - int32(delta))
516
517 vmin = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, min)
518 vmax = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, max)
519
520 case 2:
521 min = int64(int16(w.AuxInt) - int16(delta))
522 max = int64(int16(^uint16(0)>>1) - int16(delta))
523
524 vmin = parent.NewValue0I(parent.Pos, OpConst16, parent.Func.Config.Types.Int16, min)
525 vmax = parent.NewValue0I(parent.Pos, OpConst16, parent.Func.Config.Types.Int16, max)
526
527 case 1:
528 min = int64(int8(w.AuxInt) - int8(delta))
529 max = int64(int8(^uint8(0)>>1) - int8(delta))
530
531 vmin = parent.NewValue0I(parent.Pos, OpConst8, parent.Func.Config.Types.Int8, min)
532 vmax = parent.NewValue0I(parent.Pos, OpConst8, parent.Func.Config.Types.Int8, max)
533
534 default:
535 panic("unimplemented")
536 }
537
538 if min < max {
539
540 ft.update(parent, x, vmin, d, r)
541 ft.update(parent, vmax, x, d, r|eq)
542 } else {
543
544
545
546 if l, has := ft.limits[x.ID]; has {
547 if l.max <= min {
548 if r&eq == 0 || l.max < min {
549
550 ft.update(parent, vmax, x, d, r|eq)
551 }
552 } else if l.min > max {
553
554 ft.update(parent, x, vmin, d, r)
555 }
556 }
557 }
558 }
559 }
560 }
561
562
563
564
565 if isCleanExt(v) {
566 switch {
567 case d == signed && v.Args[0].Type.IsSigned():
568 fallthrough
569 case d == unsigned && !v.Args[0].Type.IsSigned():
570 ft.update(parent, v.Args[0], w, d, r)
571 }
572 }
573 if isCleanExt(w) {
574 switch {
575 case d == signed && w.Args[0].Type.IsSigned():
576 fallthrough
577 case d == unsigned && !w.Args[0].Type.IsSigned():
578 ft.update(parent, v, w.Args[0], d, r)
579 }
580 }
581 }
582
583 var opMin = map[Op]int64{
584 OpAdd64: math.MinInt64, OpSub64: math.MinInt64,
585 OpAdd32: math.MinInt32, OpSub32: math.MinInt32,
586 }
587
588 var opMax = map[Op]int64{
589 OpAdd64: math.MaxInt64, OpSub64: math.MaxInt64,
590 OpAdd32: math.MaxInt32, OpSub32: math.MaxInt32,
591 }
592
593 var opUMax = map[Op]uint64{
594 OpAdd64: math.MaxUint64, OpSub64: math.MaxUint64,
595 OpAdd32: math.MaxUint32, OpSub32: math.MaxUint32,
596 }
597
598
599 func (ft *factsTable) isNonNegative(v *Value) bool {
600 if isNonNegative(v) {
601 return true
602 }
603
604 var max int64
605 switch v.Type.Size() {
606 case 1:
607 max = math.MaxInt8
608 case 2:
609 max = math.MaxInt16
610 case 4:
611 max = math.MaxInt32
612 case 8:
613 max = math.MaxInt64
614 default:
615 panic("unexpected integer size")
616 }
617
618
619
620 if l, has := ft.limits[v.ID]; has && (l.min >= 0 || l.umax <= uint64(max)) {
621 return true
622 }
623
624
625 if x, delta := isConstDelta(v); x != nil {
626 if l, has := ft.limits[x.ID]; has {
627 if delta > 0 && l.min >= -delta && l.max <= max-delta {
628 return true
629 }
630 if delta < 0 && l.min >= -delta {
631 return true
632 }
633 }
634 }
635
636
637 if isCleanExt(v) && ft.isNonNegative(v.Args[0]) {
638 return true
639 }
640
641
642 return ft.orderS.OrderedOrEqual(ft.zero, v)
643 }
644
645
646
647 func (ft *factsTable) checkpoint() {
648 if ft.unsat {
649 ft.unsatDepth++
650 }
651 ft.stack = append(ft.stack, checkpointFact)
652 ft.limitStack = append(ft.limitStack, checkpointBound)
653 ft.orderS.Checkpoint()
654 ft.orderU.Checkpoint()
655 }
656
657
658
659
660 func (ft *factsTable) restore() {
661 if ft.unsatDepth > 0 {
662 ft.unsatDepth--
663 } else {
664 ft.unsat = false
665 }
666 for {
667 old := ft.stack[len(ft.stack)-1]
668 ft.stack = ft.stack[:len(ft.stack)-1]
669 if old == checkpointFact {
670 break
671 }
672 if old.r == lt|eq|gt {
673 delete(ft.facts, old.p)
674 } else {
675 ft.facts[old.p] = old.r
676 }
677 }
678 for {
679 old := ft.limitStack[len(ft.limitStack)-1]
680 ft.limitStack = ft.limitStack[:len(ft.limitStack)-1]
681 if old.vid == 0 {
682 break
683 }
684 if old.limit == noLimit {
685 delete(ft.limits, old.vid)
686 } else {
687 ft.limits[old.vid] = old.limit
688 }
689 }
690 ft.orderS.Undo()
691 ft.orderU.Undo()
692 }
693
694 func lessByID(v, w *Value) bool {
695 if v == nil && w == nil {
696
697 return false
698 }
699 if v == nil {
700 return true
701 }
702 return w != nil && v.ID < w.ID
703 }
704
705 var (
706 reverseBits = [...]relation{0, 4, 2, 6, 1, 5, 3, 7}
707
708
709
710
711
712
713
714 domainRelationTable = map[Op]struct {
715 d domain
716 r relation
717 }{
718 OpEq8: {signed | unsigned, eq},
719 OpEq16: {signed | unsigned, eq},
720 OpEq32: {signed | unsigned, eq},
721 OpEq64: {signed | unsigned, eq},
722 OpEqPtr: {pointer, eq},
723
724 OpNeq8: {signed | unsigned, lt | gt},
725 OpNeq16: {signed | unsigned, lt | gt},
726 OpNeq32: {signed | unsigned, lt | gt},
727 OpNeq64: {signed | unsigned, lt | gt},
728 OpNeqPtr: {pointer, lt | gt},
729
730 OpLess8: {signed, lt},
731 OpLess8U: {unsigned, lt},
732 OpLess16: {signed, lt},
733 OpLess16U: {unsigned, lt},
734 OpLess32: {signed, lt},
735 OpLess32U: {unsigned, lt},
736 OpLess64: {signed, lt},
737 OpLess64U: {unsigned, lt},
738
739 OpLeq8: {signed, lt | eq},
740 OpLeq8U: {unsigned, lt | eq},
741 OpLeq16: {signed, lt | eq},
742 OpLeq16U: {unsigned, lt | eq},
743 OpLeq32: {signed, lt | eq},
744 OpLeq32U: {unsigned, lt | eq},
745 OpLeq64: {signed, lt | eq},
746 OpLeq64U: {unsigned, lt | eq},
747
748
749
750
751 OpIsInBounds: {signed | unsigned, lt},
752 OpIsSliceInBounds: {signed | unsigned, lt | eq},
753 }
754 )
755
756
757 func (ft *factsTable) cleanup(f *Func) {
758 for _, po := range []*poset{ft.orderS, ft.orderU} {
759
760
761 if checkEnabled {
762 if err := po.CheckEmpty(); err != nil {
763 f.Fatalf("poset not empty after function %s: %v", f.Name, err)
764 }
765 }
766 f.retPoset(po)
767 }
768 }
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801 func prove(f *Func) {
802
803
804 var indVars map[*Block]indVar
805 for _, v := range findIndVar(f) {
806 ind := v.ind
807 if len(ind.Args) != 2 {
808
809 panic("unexpected induction with too many parents")
810 }
811
812 nxt := v.nxt
813 if !(ind.Uses == 2 &&
814 nxt.Uses == 1) {
815
816 if indVars == nil {
817 indVars = make(map[*Block]indVar)
818 }
819 indVars[v.entry] = v
820 continue
821 } else {
822
823
824 }
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862 start, end := v.min, v.max
863 if v.flags&indVarCountDown != 0 {
864 start, end = end, start
865 }
866
867 if !(start.Op == OpConst8 || start.Op == OpConst16 || start.Op == OpConst32 || start.Op == OpConst64) {
868
869 continue
870 }
871 if end.Op == OpConst8 || end.Op == OpConst16 || end.Op == OpConst32 || end.Op == OpConst64 {
872
873
874
875
876
877
878 continue
879 }
880
881 header := ind.Block
882 check := header.Controls[0]
883 if check == nil {
884
885 continue
886 }
887 switch check.Op {
888 case OpLeq64, OpLeq32, OpLeq16, OpLeq8,
889 OpLess64, OpLess32, OpLess16, OpLess8:
890 default:
891
892 continue
893 }
894 if !((check.Args[0] == ind && check.Args[1] == end) ||
895 (check.Args[1] == ind && check.Args[0] == end)) {
896
897 continue
898 }
899 if end.Block == ind.Block {
900
901
902 continue
903 }
904
905
906 check.Args[0], check.Args[1] = check.Args[1], check.Args[0]
907
908
909 for i, v := range check.Args {
910 if v != end {
911 continue
912 }
913
914 check.SetArg(i, start)
915 goto replacedEnd
916 }
917 panic(fmt.Sprintf("unreachable, ind: %v, start: %v, end: %v", ind, start, end))
918 replacedEnd:
919
920 for i, v := range ind.Args {
921 if v != start {
922 continue
923 }
924
925 ind.SetArg(i, end)
926 goto replacedStart
927 }
928 panic(fmt.Sprintf("unreachable, ind: %v, start: %v, end: %v", ind, start, end))
929 replacedStart:
930
931 if nxt.Args[0] != ind {
932
933 nxt.Args[0], nxt.Args[1] = nxt.Args[1], nxt.Args[0]
934 }
935
936 switch nxt.Op {
937 case OpAdd8:
938 nxt.Op = OpSub8
939 case OpAdd16:
940 nxt.Op = OpSub16
941 case OpAdd32:
942 nxt.Op = OpSub32
943 case OpAdd64:
944 nxt.Op = OpSub64
945 case OpSub8:
946 nxt.Op = OpAdd8
947 case OpSub16:
948 nxt.Op = OpAdd16
949 case OpSub32:
950 nxt.Op = OpAdd32
951 case OpSub64:
952 nxt.Op = OpAdd64
953 default:
954 panic("unreachable")
955 }
956
957 if f.pass.debug > 0 {
958 f.Warnl(ind.Pos, "Inverted loop iteration")
959 }
960 }
961
962 ft := newFactsTable(f)
963 ft.checkpoint()
964
965 var lensVars map[*Block][]*Value
966 var logicVars map[*Block][]*Value
967
968
969 for _, b := range f.Blocks {
970 for _, v := range b.Values {
971 if v.Uses == 0 {
972
973
974 continue
975 }
976 switch v.Op {
977 case OpStringLen:
978 ft.update(b, v, ft.zero, signed, gt|eq)
979 case OpSliceLen:
980 if ft.lens == nil {
981 ft.lens = map[ID]*Value{}
982 }
983
984
985
986 if l, ok := ft.lens[v.Args[0].ID]; ok {
987 ft.update(b, v, l, signed, eq)
988 } else {
989 ft.lens[v.Args[0].ID] = v
990 }
991 ft.update(b, v, ft.zero, signed, gt|eq)
992 if v.Args[0].Op == OpSliceMake {
993 if lensVars == nil {
994 lensVars = make(map[*Block][]*Value)
995 }
996 lensVars[b] = append(lensVars[b], v)
997 }
998 case OpSliceCap:
999 if ft.caps == nil {
1000 ft.caps = map[ID]*Value{}
1001 }
1002
1003 if c, ok := ft.caps[v.Args[0].ID]; ok {
1004 ft.update(b, v, c, signed, eq)
1005 } else {
1006 ft.caps[v.Args[0].ID] = v
1007 }
1008 ft.update(b, v, ft.zero, signed, gt|eq)
1009 if v.Args[0].Op == OpSliceMake {
1010 if lensVars == nil {
1011 lensVars = make(map[*Block][]*Value)
1012 }
1013 lensVars[b] = append(lensVars[b], v)
1014 }
1015 case OpCtz64, OpCtz32, OpCtz16, OpCtz8, OpBitLen64, OpBitLen32, OpBitLen16, OpBitLen8:
1016 ft.update(b, v, ft.zero, signed, gt|eq)
1017
1018 case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
1019 ft.update(b, v, v.Args[1], unsigned, lt|eq)
1020 ft.update(b, v, v.Args[0], unsigned, lt|eq)
1021 for i := 0; i < 2; i++ {
1022 if isNonNegative(v.Args[i]) {
1023 ft.update(b, v, v.Args[i], signed, lt|eq)
1024 ft.update(b, v, ft.zero, signed, gt|eq)
1025 }
1026 }
1027 if logicVars == nil {
1028 logicVars = make(map[*Block][]*Value)
1029 }
1030 logicVars[b] = append(logicVars[b], v)
1031 case OpOr64, OpOr32, OpOr16, OpOr8:
1032
1033 if v.Args[0].isGenericIntConst() {
1034 ft.update(b, v, v.Args[0], unsigned, gt|eq)
1035 }
1036 if v.Args[1].isGenericIntConst() {
1037 ft.update(b, v, v.Args[1], unsigned, gt|eq)
1038 }
1039 case OpDiv64u, OpDiv32u, OpDiv16u, OpDiv8u,
1040 OpRsh8Ux64, OpRsh8Ux32, OpRsh8Ux16, OpRsh8Ux8,
1041 OpRsh16Ux64, OpRsh16Ux32, OpRsh16Ux16, OpRsh16Ux8,
1042 OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8,
1043 OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8:
1044 ft.update(b, v, v.Args[0], unsigned, lt|eq)
1045 case OpMod64u, OpMod32u, OpMod16u, OpMod8u:
1046 ft.update(b, v, v.Args[0], unsigned, lt|eq)
1047 ft.update(b, v, v.Args[1], unsigned, lt)
1048 case OpPhi:
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064 sameConstOp := true
1065 min := 0
1066 max := 0
1067
1068 if !v.Args[min].isGenericIntConst() {
1069 break
1070 }
1071
1072 for k := range v.Args {
1073 if v.Args[k].Op != v.Args[min].Op {
1074 sameConstOp = false
1075 break
1076 }
1077 if v.Args[k].AuxInt < v.Args[min].AuxInt {
1078 min = k
1079 }
1080 if v.Args[k].AuxInt > v.Args[max].AuxInt {
1081 max = k
1082 }
1083 }
1084
1085 if sameConstOp {
1086 ft.update(b, v, v.Args[min], signed, gt|eq)
1087 ft.update(b, v, v.Args[max], signed, lt|eq)
1088 }
1089
1090
1091
1092
1093
1094 }
1095 }
1096 }
1097
1098
1099 type walkState int
1100 const (
1101 descend walkState = iota
1102 simplify
1103 )
1104
1105 type bp struct {
1106 block *Block
1107 state walkState
1108 }
1109 work := make([]bp, 0, 256)
1110 work = append(work, bp{
1111 block: f.Entry,
1112 state: descend,
1113 })
1114
1115 idom := f.Idom()
1116 sdom := f.Sdom()
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128 for len(work) > 0 {
1129 node := work[len(work)-1]
1130 work = work[:len(work)-1]
1131 parent := idom[node.block.ID]
1132 branch := getBranch(sdom, parent, node.block)
1133
1134 switch node.state {
1135 case descend:
1136 ft.checkpoint()
1137
1138
1139
1140 if iv, ok := indVars[node.block]; ok {
1141 addIndVarRestrictions(ft, parent, iv)
1142 }
1143 if lens, ok := lensVars[node.block]; ok {
1144 for _, v := range lens {
1145 switch v.Op {
1146 case OpSliceLen:
1147 ft.update(node.block, v, v.Args[0].Args[1], signed, eq)
1148 case OpSliceCap:
1149 ft.update(node.block, v, v.Args[0].Args[2], signed, eq)
1150 }
1151 }
1152 }
1153
1154 if branch != unknown {
1155 addBranchRestrictions(ft, parent, branch)
1156
1157
1158 if logic, ok := logicVars[parent]; ok {
1159 for _, v := range logic {
1160
1161 ft.update(parent, v, v.Args[1], unsigned, lt|eq)
1162 ft.update(parent, v, v.Args[0], unsigned, lt|eq)
1163 for i := 0; i < 2; i++ {
1164 if isNonNegative(v.Args[i]) {
1165 ft.update(parent, v, v.Args[i], signed, lt|eq)
1166 ft.update(parent, v, ft.zero, signed, gt|eq)
1167 }
1168 }
1169 }
1170 }
1171 if ft.unsat {
1172
1173
1174
1175 removeBranch(parent, branch)
1176 ft.restore()
1177 break
1178 }
1179
1180
1181
1182 }
1183
1184
1185 addLocalInductiveFacts(ft, node.block)
1186
1187 work = append(work, bp{
1188 block: node.block,
1189 state: simplify,
1190 })
1191 for s := sdom.Child(node.block); s != nil; s = sdom.Sibling(s) {
1192 work = append(work, bp{
1193 block: s,
1194 state: descend,
1195 })
1196 }
1197
1198 case simplify:
1199 simplifyBlock(sdom, ft, node.block)
1200 ft.restore()
1201 }
1202 }
1203
1204 ft.restore()
1205
1206 ft.cleanup(f)
1207 }
1208
1209
1210
1211 func getBranch(sdom SparseTree, p *Block, b *Block) branch {
1212 if p == nil {
1213 return unknown
1214 }
1215 switch p.Kind {
1216 case BlockIf:
1217
1218
1219
1220
1221
1222
1223 if sdom.IsAncestorEq(p.Succs[0].b, b) && len(p.Succs[0].b.Preds) == 1 {
1224 return positive
1225 }
1226 if sdom.IsAncestorEq(p.Succs[1].b, b) && len(p.Succs[1].b.Preds) == 1 {
1227 return negative
1228 }
1229 case BlockJumpTable:
1230
1231
1232 for i, e := range p.Succs {
1233 if sdom.IsAncestorEq(e.b, b) && len(e.b.Preds) == 1 {
1234 return jumpTable0 + branch(i)
1235 }
1236 }
1237 }
1238 return unknown
1239 }
1240
1241
1242
1243
1244 func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) {
1245 d := signed
1246 if ft.isNonNegative(iv.min) && ft.isNonNegative(iv.max) {
1247 d |= unsigned
1248 }
1249
1250 if iv.flags&indVarMinExc == 0 {
1251 addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq)
1252 } else {
1253 addRestrictions(b, ft, d, iv.min, iv.ind, lt)
1254 }
1255
1256 if iv.flags&indVarMaxInc == 0 {
1257 addRestrictions(b, ft, d, iv.ind, iv.max, lt)
1258 } else {
1259 addRestrictions(b, ft, d, iv.ind, iv.max, lt|eq)
1260 }
1261 }
1262
1263
1264
1265 func addBranchRestrictions(ft *factsTable, b *Block, br branch) {
1266 c := b.Controls[0]
1267 switch {
1268 case br == negative:
1269 addRestrictions(b, ft, boolean, nil, c, eq)
1270 case br == positive:
1271 addRestrictions(b, ft, boolean, nil, c, lt|gt)
1272 case br >= jumpTable0:
1273 idx := br - jumpTable0
1274 val := int64(idx)
1275 if v, off := isConstDelta(c); v != nil {
1276
1277
1278 c = v
1279 val -= off
1280 }
1281 old, ok := ft.limits[c.ID]
1282 if !ok {
1283 old = noLimit
1284 }
1285 ft.limitStack = append(ft.limitStack, limitFact{c.ID, old})
1286 if val < old.min || val > old.max || uint64(val) < old.umin || uint64(val) > old.umax {
1287 ft.unsat = true
1288 if b.Func.pass.debug > 2 {
1289 b.Func.Warnl(b.Pos, "block=%s outedge=%d %s=%d unsat", b, idx, c, val)
1290 }
1291 } else {
1292 ft.limits[c.ID] = limit{val, val, uint64(val), uint64(val)}
1293 if b.Func.pass.debug > 2 {
1294 b.Func.Warnl(b.Pos, "block=%s outedge=%d %s=%d", b, idx, c, val)
1295 }
1296 }
1297 default:
1298 panic("unknown branch")
1299 }
1300 if tr, has := domainRelationTable[c.Op]; has {
1301
1302
1303 d := tr.d
1304 if d == signed && ft.isNonNegative(c.Args[0]) && ft.isNonNegative(c.Args[1]) {
1305 d |= unsigned
1306 }
1307 switch c.Op {
1308 case OpIsInBounds, OpIsSliceInBounds:
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322 switch br {
1323 case negative:
1324 d = unsigned
1325 if ft.isNonNegative(c.Args[0]) {
1326 d |= signed
1327 }
1328 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq))
1329 case positive:
1330 addRestrictions(b, ft, signed, ft.zero, c.Args[0], lt|eq)
1331 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r)
1332 }
1333 default:
1334 switch br {
1335 case negative:
1336 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq))
1337 case positive:
1338 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r)
1339 }
1340 }
1341
1342 }
1343 }
1344
1345
1346
1347 func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r relation) {
1348 if t == 0 {
1349
1350
1351 return
1352 }
1353 for i := domain(1); i <= t; i <<= 1 {
1354 if t&i == 0 {
1355 continue
1356 }
1357 ft.update(parent, v, w, i, r)
1358 }
1359 }
1360
1361
1362
1363
1364
1365
1366
1367 func addLocalInductiveFacts(ft *factsTable, b *Block) {
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378 if len(b.Preds) != 2 {
1379 return
1380 }
1381
1382 for _, i1 := range b.Values {
1383 if i1.Op != OpPhi {
1384 continue
1385 }
1386
1387
1388
1389 min, i2 := i1.Args[0], i1.Args[1]
1390 if i1q, delta := isConstDelta(i2); i1q != i1 || delta != 1 {
1391 continue
1392 }
1393
1394
1395
1396
1397
1398
1399
1400
1401 uniquePred := func(b *Block) *Block {
1402 if len(b.Preds) == 1 {
1403 return b.Preds[0].b
1404 }
1405 return nil
1406 }
1407 pred, child := b.Preds[1].b, b
1408 for ; pred != nil; pred, child = uniquePred(pred), pred {
1409 if pred.Kind != BlockIf {
1410 continue
1411 }
1412 control := pred.Controls[0]
1413
1414 br := unknown
1415 if pred.Succs[0].b == child {
1416 br = positive
1417 }
1418 if pred.Succs[1].b == child {
1419 if br != unknown {
1420 continue
1421 }
1422 br = negative
1423 }
1424 if br == unknown {
1425 continue
1426 }
1427
1428 tr, has := domainRelationTable[control.Op]
1429 if !has {
1430 continue
1431 }
1432 r := tr.r
1433 if br == negative {
1434
1435
1436 r = (lt | eq | gt) ^ r
1437 }
1438
1439
1440 var max *Value
1441 if r == lt && control.Args[0] == i2 {
1442 max = control.Args[1]
1443 } else if r == gt && control.Args[1] == i2 {
1444 max = control.Args[0]
1445 } else {
1446 continue
1447 }
1448
1449
1450
1451
1452
1453
1454 ft.checkpoint()
1455 ft.update(b, min, max, tr.d, gt|eq)
1456 proved := ft.unsat
1457 ft.restore()
1458
1459 if proved {
1460
1461 if b.Func.pass.debug > 0 {
1462 printIndVar(b, i1, min, max, 1, 0)
1463 }
1464 ft.update(b, min, i1, tr.d, lt|eq)
1465 ft.update(b, i1, max, tr.d, lt)
1466 }
1467 }
1468 }
1469 }
1470
1471 var ctzNonZeroOp = map[Op]Op{OpCtz8: OpCtz8NonZero, OpCtz16: OpCtz16NonZero, OpCtz32: OpCtz32NonZero, OpCtz64: OpCtz64NonZero}
1472 var mostNegativeDividend = map[Op]int64{
1473 OpDiv16: -1 << 15,
1474 OpMod16: -1 << 15,
1475 OpDiv32: -1 << 31,
1476 OpMod32: -1 << 31,
1477 OpDiv64: -1 << 63,
1478 OpMod64: -1 << 63}
1479
1480
1481
1482 func simplifyBlock(sdom SparseTree, ft *factsTable, b *Block) {
1483 for _, v := range b.Values {
1484 switch v.Op {
1485 case OpSlicemask:
1486
1487 x, delta := isConstDelta(v.Args[0])
1488 if x == nil {
1489 break
1490 }
1491
1492
1493 lim, ok := ft.limits[x.ID]
1494 if !ok {
1495 break
1496 }
1497 if lim.umin > uint64(-delta) {
1498 if v.Args[0].Op == OpAdd64 {
1499 v.reset(OpConst64)
1500 } else {
1501 v.reset(OpConst32)
1502 }
1503 if b.Func.pass.debug > 0 {
1504 b.Func.Warnl(v.Pos, "Proved slicemask not needed")
1505 }
1506 v.AuxInt = -1
1507 }
1508 case OpCtz8, OpCtz16, OpCtz32, OpCtz64:
1509
1510
1511
1512 x := v.Args[0]
1513 lim, ok := ft.limits[x.ID]
1514 if !ok {
1515 break
1516 }
1517 if lim.umin > 0 || lim.min > 0 || lim.max < 0 {
1518 if b.Func.pass.debug > 0 {
1519 b.Func.Warnl(v.Pos, "Proved %v non-zero", v.Op)
1520 }
1521 v.Op = ctzNonZeroOp[v.Op]
1522 }
1523 case OpRsh8x8, OpRsh8x16, OpRsh8x32, OpRsh8x64,
1524 OpRsh16x8, OpRsh16x16, OpRsh16x32, OpRsh16x64,
1525 OpRsh32x8, OpRsh32x16, OpRsh32x32, OpRsh32x64,
1526 OpRsh64x8, OpRsh64x16, OpRsh64x32, OpRsh64x64:
1527
1528
1529 bits := 8 * v.Type.Size()
1530 if v.Args[1].isGenericIntConst() && v.Args[1].AuxInt >= bits-1 && ft.isNonNegative(v.Args[0]) {
1531 if b.Func.pass.debug > 0 {
1532 b.Func.Warnl(v.Pos, "Proved %v shifts to zero", v.Op)
1533 }
1534 switch bits {
1535 case 64:
1536 v.reset(OpConst64)
1537 case 32:
1538 v.reset(OpConst32)
1539 case 16:
1540 v.reset(OpConst16)
1541 case 8:
1542 v.reset(OpConst8)
1543 default:
1544 panic("unexpected integer size")
1545 }
1546 v.AuxInt = 0
1547 break
1548 }
1549
1550 fallthrough
1551 case OpLsh8x8, OpLsh8x16, OpLsh8x32, OpLsh8x64,
1552 OpLsh16x8, OpLsh16x16, OpLsh16x32, OpLsh16x64,
1553 OpLsh32x8, OpLsh32x16, OpLsh32x32, OpLsh32x64,
1554 OpLsh64x8, OpLsh64x16, OpLsh64x32, OpLsh64x64,
1555 OpRsh8Ux8, OpRsh8Ux16, OpRsh8Ux32, OpRsh8Ux64,
1556 OpRsh16Ux8, OpRsh16Ux16, OpRsh16Ux32, OpRsh16Ux64,
1557 OpRsh32Ux8, OpRsh32Ux16, OpRsh32Ux32, OpRsh32Ux64,
1558 OpRsh64Ux8, OpRsh64Ux16, OpRsh64Ux32, OpRsh64Ux64:
1559
1560
1561 by := v.Args[1]
1562 lim, ok := ft.limits[by.ID]
1563 if !ok {
1564 break
1565 }
1566 bits := 8 * v.Args[0].Type.Size()
1567 if lim.umax < uint64(bits) || (lim.max < bits && ft.isNonNegative(by)) {
1568 v.AuxInt = 1
1569 if b.Func.pass.debug > 0 {
1570 b.Func.Warnl(v.Pos, "Proved %v bounded", v.Op)
1571 }
1572 }
1573 case OpDiv16, OpDiv32, OpDiv64, OpMod16, OpMod32, OpMod64:
1574
1575
1576
1577
1578
1579 if b.Func.Config.arch != "386" && b.Func.Config.arch != "amd64" {
1580 break
1581 }
1582 divr := v.Args[1]
1583 divrLim, divrLimok := ft.limits[divr.ID]
1584 divd := v.Args[0]
1585 divdLim, divdLimok := ft.limits[divd.ID]
1586 if (divrLimok && (divrLim.max < -1 || divrLim.min > -1)) ||
1587 (divdLimok && divdLim.min > mostNegativeDividend[v.Op]) {
1588
1589
1590
1591
1592 v.AuxInt = 1
1593 if b.Func.pass.debug > 0 {
1594 b.Func.Warnl(v.Pos, "Proved %v does not need fix-up", v.Op)
1595 }
1596 }
1597 }
1598
1599
1600 for i, arg := range v.Args {
1601 switch arg.Op {
1602 case OpConst64, OpConst32, OpConst16, OpConst8:
1603 continue
1604 }
1605 lim, ok := ft.limits[arg.ID]
1606 if !ok {
1607 continue
1608 }
1609
1610 var constValue int64
1611 typ := arg.Type
1612 bits := 8 * typ.Size()
1613 switch {
1614 case lim.min == lim.max:
1615 constValue = lim.min
1616 case lim.umin == lim.umax:
1617
1618 switch bits {
1619 case 64:
1620 constValue = int64(lim.umin)
1621 case 32:
1622 constValue = int64(int32(lim.umin))
1623 case 16:
1624 constValue = int64(int16(lim.umin))
1625 case 8:
1626 constValue = int64(int8(lim.umin))
1627 default:
1628 panic("unexpected integer size")
1629 }
1630 default:
1631 continue
1632 }
1633 var c *Value
1634 f := b.Func
1635 switch bits {
1636 case 64:
1637 c = f.ConstInt64(typ, constValue)
1638 case 32:
1639 c = f.ConstInt32(typ, int32(constValue))
1640 case 16:
1641 c = f.ConstInt16(typ, int16(constValue))
1642 case 8:
1643 c = f.ConstInt8(typ, int8(constValue))
1644 default:
1645 panic("unexpected integer size")
1646 }
1647 v.SetArg(i, c)
1648 if b.Func.pass.debug > 1 {
1649 b.Func.Warnl(v.Pos, "Proved %v's arg %d (%v) is constant %d", v, i, arg, constValue)
1650 }
1651 }
1652 }
1653
1654 if b.Kind != BlockIf {
1655 return
1656 }
1657
1658
1659 parent := b
1660 for i, branch := range [...]branch{positive, negative} {
1661 child := parent.Succs[i].b
1662 if getBranch(sdom, parent, child) != unknown {
1663
1664
1665 continue
1666 }
1667
1668
1669 ft.checkpoint()
1670 addBranchRestrictions(ft, parent, branch)
1671 unsat := ft.unsat
1672 ft.restore()
1673 if unsat {
1674
1675
1676 removeBranch(parent, branch)
1677
1678
1679
1680
1681
1682 break
1683 }
1684 }
1685 }
1686
1687 func removeBranch(b *Block, branch branch) {
1688 c := b.Controls[0]
1689 if b.Func.pass.debug > 0 {
1690 verb := "Proved"
1691 if branch == positive {
1692 verb = "Disproved"
1693 }
1694 if b.Func.pass.debug > 1 {
1695 b.Func.Warnl(b.Pos, "%s %s (%s)", verb, c.Op, c)
1696 } else {
1697 b.Func.Warnl(b.Pos, "%s %s", verb, c.Op)
1698 }
1699 }
1700 if c != nil && c.Pos.IsStmt() == src.PosIsStmt && c.Pos.SameFileAndLine(b.Pos) {
1701
1702 b.Pos = b.Pos.WithIsStmt()
1703 }
1704 if branch == positive || branch == negative {
1705 b.Kind = BlockFirst
1706 b.ResetControls()
1707 if branch == positive {
1708 b.swapSuccessors()
1709 }
1710 } else {
1711
1712 }
1713 }
1714
1715
1716 func isNonNegative(v *Value) bool {
1717 if !v.Type.IsInteger() {
1718 v.Fatalf("isNonNegative bad type: %v", v.Type)
1719 }
1720
1721
1722
1723
1724 switch v.Op {
1725 case OpConst64:
1726 return v.AuxInt >= 0
1727
1728 case OpConst32:
1729 return int32(v.AuxInt) >= 0
1730
1731 case OpConst16:
1732 return int16(v.AuxInt) >= 0
1733
1734 case OpConst8:
1735 return int8(v.AuxInt) >= 0
1736
1737 case OpStringLen, OpSliceLen, OpSliceCap,
1738 OpZeroExt8to64, OpZeroExt16to64, OpZeroExt32to64,
1739 OpZeroExt8to32, OpZeroExt16to32, OpZeroExt8to16,
1740 OpCtz64, OpCtz32, OpCtz16, OpCtz8,
1741 OpCtz64NonZero, OpCtz32NonZero, OpCtz16NonZero, OpCtz8NonZero,
1742 OpBitLen64, OpBitLen32, OpBitLen16, OpBitLen8:
1743 return true
1744
1745 case OpRsh64Ux64, OpRsh32Ux64:
1746 by := v.Args[1]
1747 return by.Op == OpConst64 && by.AuxInt > 0
1748
1749 case OpRsh64x64, OpRsh32x64, OpRsh8x64, OpRsh16x64, OpRsh32x32, OpRsh64x32,
1750 OpSignExt32to64, OpSignExt16to64, OpSignExt8to64, OpSignExt16to32, OpSignExt8to32:
1751 return isNonNegative(v.Args[0])
1752
1753 case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
1754 return isNonNegative(v.Args[0]) || isNonNegative(v.Args[1])
1755
1756 case OpMod64, OpMod32, OpMod16, OpMod8,
1757 OpDiv64, OpDiv32, OpDiv16, OpDiv8,
1758 OpOr64, OpOr32, OpOr16, OpOr8,
1759 OpXor64, OpXor32, OpXor16, OpXor8:
1760 return isNonNegative(v.Args[0]) && isNonNegative(v.Args[1])
1761
1762
1763
1764 }
1765 return false
1766 }
1767
1768
1769 func isConstDelta(v *Value) (w *Value, delta int64) {
1770 cop := OpConst64
1771 switch v.Op {
1772 case OpAdd32, OpSub32:
1773 cop = OpConst32
1774 case OpAdd16, OpSub16:
1775 cop = OpConst16
1776 case OpAdd8, OpSub8:
1777 cop = OpConst8
1778 }
1779 switch v.Op {
1780 case OpAdd64, OpAdd32, OpAdd16, OpAdd8:
1781 if v.Args[0].Op == cop {
1782 return v.Args[1], v.Args[0].AuxInt
1783 }
1784 if v.Args[1].Op == cop {
1785 return v.Args[0], v.Args[1].AuxInt
1786 }
1787 case OpSub64, OpSub32, OpSub16, OpSub8:
1788 if v.Args[1].Op == cop {
1789 aux := v.Args[1].AuxInt
1790 if aux != -aux {
1791 return v.Args[0], -aux
1792 }
1793 }
1794 }
1795 return nil, 0
1796 }
1797
1798
1799
1800 func isCleanExt(v *Value) bool {
1801 switch v.Op {
1802 case OpSignExt8to16, OpSignExt8to32, OpSignExt8to64,
1803 OpSignExt16to32, OpSignExt16to64, OpSignExt32to64:
1804
1805 return v.Args[0].Type.IsSigned() && v.Type.IsSigned()
1806
1807 case OpZeroExt8to16, OpZeroExt8to32, OpZeroExt8to64,
1808 OpZeroExt16to32, OpZeroExt16to64, OpZeroExt32to64:
1809
1810 return !v.Args[0].Type.IsSigned()
1811 }
1812 return false
1813 }
1814
View as plain text