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 if end.Block == ind.Block {
882
883
884 continue
885 }
886
887 check := ind.Block.Controls[0]
888
889 check.Args[0], check.Args[1] = check.Args[1], check.Args[0]
890
891
892 for i, v := range check.Args {
893 if v != end {
894 continue
895 }
896
897 check.SetArg(i, start)
898 goto replacedEnd
899 }
900 panic(fmt.Sprintf("unreachable, ind: %v, start: %v, end: %v", ind, start, end))
901 replacedEnd:
902
903 for i, v := range ind.Args {
904 if v != start {
905 continue
906 }
907
908 ind.SetArg(i, end)
909 goto replacedStart
910 }
911 panic(fmt.Sprintf("unreachable, ind: %v, start: %v, end: %v", ind, start, end))
912 replacedStart:
913
914 if nxt.Args[0] != ind {
915
916 nxt.Args[0], nxt.Args[1] = nxt.Args[1], nxt.Args[0]
917 }
918
919 switch nxt.Op {
920 case OpAdd8:
921 nxt.Op = OpSub8
922 case OpAdd16:
923 nxt.Op = OpSub16
924 case OpAdd32:
925 nxt.Op = OpSub32
926 case OpAdd64:
927 nxt.Op = OpSub64
928 case OpSub8:
929 nxt.Op = OpAdd8
930 case OpSub16:
931 nxt.Op = OpAdd16
932 case OpSub32:
933 nxt.Op = OpAdd32
934 case OpSub64:
935 nxt.Op = OpAdd64
936 default:
937 panic("unreachable")
938 }
939
940 if f.pass.debug > 0 {
941 f.Warnl(ind.Pos, "Inverted loop iteration")
942 }
943 }
944
945 ft := newFactsTable(f)
946 ft.checkpoint()
947
948 var lensVars map[*Block][]*Value
949 var logicVars map[*Block][]*Value
950
951
952 for _, b := range f.Blocks {
953 for _, v := range b.Values {
954 if v.Uses == 0 {
955
956
957 continue
958 }
959 switch v.Op {
960 case OpStringLen:
961 ft.update(b, v, ft.zero, signed, gt|eq)
962 case OpSliceLen:
963 if ft.lens == nil {
964 ft.lens = map[ID]*Value{}
965 }
966
967
968
969 if l, ok := ft.lens[v.Args[0].ID]; ok {
970 ft.update(b, v, l, signed, eq)
971 } else {
972 ft.lens[v.Args[0].ID] = v
973 }
974 ft.update(b, v, ft.zero, signed, gt|eq)
975 if v.Args[0].Op == OpSliceMake {
976 if lensVars == nil {
977 lensVars = make(map[*Block][]*Value)
978 }
979 lensVars[b] = append(lensVars[b], v)
980 }
981 case OpSliceCap:
982 if ft.caps == nil {
983 ft.caps = map[ID]*Value{}
984 }
985
986 if c, ok := ft.caps[v.Args[0].ID]; ok {
987 ft.update(b, v, c, signed, eq)
988 } else {
989 ft.caps[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 OpCtz64, OpCtz32, OpCtz16, OpCtz8, OpBitLen64, OpBitLen32, OpBitLen16, OpBitLen8:
999 ft.update(b, v, ft.zero, signed, gt|eq)
1000
1001 case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
1002 ft.update(b, v, v.Args[1], unsigned, lt|eq)
1003 ft.update(b, v, v.Args[0], unsigned, lt|eq)
1004 for i := 0; i < 2; i++ {
1005 if isNonNegative(v.Args[i]) {
1006 ft.update(b, v, v.Args[i], signed, lt|eq)
1007 ft.update(b, v, ft.zero, signed, gt|eq)
1008 }
1009 }
1010 if logicVars == nil {
1011 logicVars = make(map[*Block][]*Value)
1012 }
1013 logicVars[b] = append(logicVars[b], v)
1014 case OpOr64, OpOr32, OpOr16, OpOr8:
1015
1016 if v.Args[0].isGenericIntConst() {
1017 ft.update(b, v, v.Args[0], unsigned, gt|eq)
1018 }
1019 if v.Args[1].isGenericIntConst() {
1020 ft.update(b, v, v.Args[1], unsigned, gt|eq)
1021 }
1022 case OpDiv64u, OpDiv32u, OpDiv16u, OpDiv8u,
1023 OpRsh8Ux64, OpRsh8Ux32, OpRsh8Ux16, OpRsh8Ux8,
1024 OpRsh16Ux64, OpRsh16Ux32, OpRsh16Ux16, OpRsh16Ux8,
1025 OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8,
1026 OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8:
1027 ft.update(b, v, v.Args[0], unsigned, lt|eq)
1028 case OpMod64u, OpMod32u, OpMod16u, OpMod8u:
1029 ft.update(b, v, v.Args[0], unsigned, lt|eq)
1030 ft.update(b, v, v.Args[1], unsigned, lt)
1031 case OpPhi:
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047 sameConstOp := true
1048 min := 0
1049 max := 0
1050
1051 if !v.Args[min].isGenericIntConst() {
1052 break
1053 }
1054
1055 for k := range v.Args {
1056 if v.Args[k].Op != v.Args[min].Op {
1057 sameConstOp = false
1058 break
1059 }
1060 if v.Args[k].AuxInt < v.Args[min].AuxInt {
1061 min = k
1062 }
1063 if v.Args[k].AuxInt > v.Args[max].AuxInt {
1064 max = k
1065 }
1066 }
1067
1068 if sameConstOp {
1069 ft.update(b, v, v.Args[min], signed, gt|eq)
1070 ft.update(b, v, v.Args[max], signed, lt|eq)
1071 }
1072
1073
1074
1075
1076
1077 }
1078 }
1079 }
1080
1081
1082 type walkState int
1083 const (
1084 descend walkState = iota
1085 simplify
1086 )
1087
1088 type bp struct {
1089 block *Block
1090 state walkState
1091 }
1092 work := make([]bp, 0, 256)
1093 work = append(work, bp{
1094 block: f.Entry,
1095 state: descend,
1096 })
1097
1098 idom := f.Idom()
1099 sdom := f.Sdom()
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111 for len(work) > 0 {
1112 node := work[len(work)-1]
1113 work = work[:len(work)-1]
1114 parent := idom[node.block.ID]
1115 branch := getBranch(sdom, parent, node.block)
1116
1117 switch node.state {
1118 case descend:
1119 ft.checkpoint()
1120
1121
1122
1123 if iv, ok := indVars[node.block]; ok {
1124 addIndVarRestrictions(ft, parent, iv)
1125 }
1126 if lens, ok := lensVars[node.block]; ok {
1127 for _, v := range lens {
1128 switch v.Op {
1129 case OpSliceLen:
1130 ft.update(node.block, v, v.Args[0].Args[1], signed, eq)
1131 case OpSliceCap:
1132 ft.update(node.block, v, v.Args[0].Args[2], signed, eq)
1133 }
1134 }
1135 }
1136
1137 if branch != unknown {
1138 addBranchRestrictions(ft, parent, branch)
1139
1140
1141 if logic, ok := logicVars[parent]; ok {
1142 for _, v := range logic {
1143
1144 ft.update(parent, v, v.Args[1], unsigned, lt|eq)
1145 ft.update(parent, v, v.Args[0], unsigned, lt|eq)
1146 for i := 0; i < 2; i++ {
1147 if isNonNegative(v.Args[i]) {
1148 ft.update(parent, v, v.Args[i], signed, lt|eq)
1149 ft.update(parent, v, ft.zero, signed, gt|eq)
1150 }
1151 }
1152 }
1153 }
1154 if ft.unsat {
1155
1156
1157
1158 removeBranch(parent, branch)
1159 ft.restore()
1160 break
1161 }
1162
1163
1164
1165 }
1166
1167
1168 addLocalInductiveFacts(ft, node.block)
1169
1170 work = append(work, bp{
1171 block: node.block,
1172 state: simplify,
1173 })
1174 for s := sdom.Child(node.block); s != nil; s = sdom.Sibling(s) {
1175 work = append(work, bp{
1176 block: s,
1177 state: descend,
1178 })
1179 }
1180
1181 case simplify:
1182 simplifyBlock(sdom, ft, node.block)
1183 ft.restore()
1184 }
1185 }
1186
1187 ft.restore()
1188
1189 ft.cleanup(f)
1190 }
1191
1192
1193
1194 func getBranch(sdom SparseTree, p *Block, b *Block) branch {
1195 if p == nil {
1196 return unknown
1197 }
1198 switch p.Kind {
1199 case BlockIf:
1200
1201
1202
1203
1204
1205
1206 if sdom.IsAncestorEq(p.Succs[0].b, b) && len(p.Succs[0].b.Preds) == 1 {
1207 return positive
1208 }
1209 if sdom.IsAncestorEq(p.Succs[1].b, b) && len(p.Succs[1].b.Preds) == 1 {
1210 return negative
1211 }
1212 case BlockJumpTable:
1213
1214
1215 for i, e := range p.Succs {
1216 if sdom.IsAncestorEq(e.b, b) && len(e.b.Preds) == 1 {
1217 return jumpTable0 + branch(i)
1218 }
1219 }
1220 }
1221 return unknown
1222 }
1223
1224
1225
1226
1227 func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) {
1228 d := signed
1229 if ft.isNonNegative(iv.min) && ft.isNonNegative(iv.max) {
1230 d |= unsigned
1231 }
1232
1233 if iv.flags&indVarMinExc == 0 {
1234 addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq)
1235 } else {
1236 addRestrictions(b, ft, d, iv.min, iv.ind, lt)
1237 }
1238
1239 if iv.flags&indVarMaxInc == 0 {
1240 addRestrictions(b, ft, d, iv.ind, iv.max, lt)
1241 } else {
1242 addRestrictions(b, ft, d, iv.ind, iv.max, lt|eq)
1243 }
1244 }
1245
1246
1247
1248 func addBranchRestrictions(ft *factsTable, b *Block, br branch) {
1249 c := b.Controls[0]
1250 switch {
1251 case br == negative:
1252 addRestrictions(b, ft, boolean, nil, c, eq)
1253 case br == positive:
1254 addRestrictions(b, ft, boolean, nil, c, lt|gt)
1255 case br >= jumpTable0:
1256 idx := br - jumpTable0
1257 val := int64(idx)
1258 if v, off := isConstDelta(c); v != nil {
1259
1260
1261 c = v
1262 val -= off
1263 }
1264 old, ok := ft.limits[c.ID]
1265 if !ok {
1266 old = noLimit
1267 }
1268 ft.limitStack = append(ft.limitStack, limitFact{c.ID, old})
1269 if val < old.min || val > old.max || uint64(val) < old.umin || uint64(val) > old.umax {
1270 ft.unsat = true
1271 if b.Func.pass.debug > 2 {
1272 b.Func.Warnl(b.Pos, "block=%s outedge=%d %s=%d unsat", b, idx, c, val)
1273 }
1274 } else {
1275 ft.limits[c.ID] = limit{val, val, uint64(val), uint64(val)}
1276 if b.Func.pass.debug > 2 {
1277 b.Func.Warnl(b.Pos, "block=%s outedge=%d %s=%d", b, idx, c, val)
1278 }
1279 }
1280 default:
1281 panic("unknown branch")
1282 }
1283 if tr, has := domainRelationTable[c.Op]; has {
1284
1285
1286 d := tr.d
1287 if d == signed && ft.isNonNegative(c.Args[0]) && ft.isNonNegative(c.Args[1]) {
1288 d |= unsigned
1289 }
1290 switch c.Op {
1291 case OpIsInBounds, OpIsSliceInBounds:
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305 switch br {
1306 case negative:
1307 d = unsigned
1308 if ft.isNonNegative(c.Args[0]) {
1309 d |= signed
1310 }
1311 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq))
1312 case positive:
1313 addRestrictions(b, ft, signed, ft.zero, c.Args[0], lt|eq)
1314 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r)
1315 }
1316 default:
1317 switch br {
1318 case negative:
1319 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq))
1320 case positive:
1321 addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r)
1322 }
1323 }
1324
1325 }
1326 }
1327
1328
1329
1330 func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r relation) {
1331 if t == 0 {
1332
1333
1334 return
1335 }
1336 for i := domain(1); i <= t; i <<= 1 {
1337 if t&i == 0 {
1338 continue
1339 }
1340 ft.update(parent, v, w, i, r)
1341 }
1342 }
1343
1344
1345
1346
1347
1348
1349
1350 func addLocalInductiveFacts(ft *factsTable, b *Block) {
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361 if len(b.Preds) != 2 {
1362 return
1363 }
1364
1365 for _, i1 := range b.Values {
1366 if i1.Op != OpPhi {
1367 continue
1368 }
1369
1370
1371
1372 min, i2 := i1.Args[0], i1.Args[1]
1373 if i1q, delta := isConstDelta(i2); i1q != i1 || delta != 1 {
1374 continue
1375 }
1376
1377
1378
1379
1380
1381
1382
1383
1384 uniquePred := func(b *Block) *Block {
1385 if len(b.Preds) == 1 {
1386 return b.Preds[0].b
1387 }
1388 return nil
1389 }
1390 pred, child := b.Preds[1].b, b
1391 for ; pred != nil; pred, child = uniquePred(pred), pred {
1392 if pred.Kind != BlockIf {
1393 continue
1394 }
1395 control := pred.Controls[0]
1396
1397 br := unknown
1398 if pred.Succs[0].b == child {
1399 br = positive
1400 }
1401 if pred.Succs[1].b == child {
1402 if br != unknown {
1403 continue
1404 }
1405 br = negative
1406 }
1407 if br == unknown {
1408 continue
1409 }
1410
1411 tr, has := domainRelationTable[control.Op]
1412 if !has {
1413 continue
1414 }
1415 r := tr.r
1416 if br == negative {
1417
1418
1419 r = (lt | eq | gt) ^ r
1420 }
1421
1422
1423 var max *Value
1424 if r == lt && control.Args[0] == i2 {
1425 max = control.Args[1]
1426 } else if r == gt && control.Args[1] == i2 {
1427 max = control.Args[0]
1428 } else {
1429 continue
1430 }
1431
1432
1433
1434
1435
1436
1437 ft.checkpoint()
1438 ft.update(b, min, max, tr.d, gt|eq)
1439 proved := ft.unsat
1440 ft.restore()
1441
1442 if proved {
1443
1444 if b.Func.pass.debug > 0 {
1445 printIndVar(b, i1, min, max, 1, 0)
1446 }
1447 ft.update(b, min, i1, tr.d, lt|eq)
1448 ft.update(b, i1, max, tr.d, lt)
1449 }
1450 }
1451 }
1452 }
1453
1454 var ctzNonZeroOp = map[Op]Op{OpCtz8: OpCtz8NonZero, OpCtz16: OpCtz16NonZero, OpCtz32: OpCtz32NonZero, OpCtz64: OpCtz64NonZero}
1455 var mostNegativeDividend = map[Op]int64{
1456 OpDiv16: -1 << 15,
1457 OpMod16: -1 << 15,
1458 OpDiv32: -1 << 31,
1459 OpMod32: -1 << 31,
1460 OpDiv64: -1 << 63,
1461 OpMod64: -1 << 63}
1462
1463
1464
1465 func simplifyBlock(sdom SparseTree, ft *factsTable, b *Block) {
1466 for _, v := range b.Values {
1467 switch v.Op {
1468 case OpSlicemask:
1469
1470 x, delta := isConstDelta(v.Args[0])
1471 if x == nil {
1472 break
1473 }
1474
1475
1476 lim, ok := ft.limits[x.ID]
1477 if !ok {
1478 break
1479 }
1480 if lim.umin > uint64(-delta) {
1481 if v.Args[0].Op == OpAdd64 {
1482 v.reset(OpConst64)
1483 } else {
1484 v.reset(OpConst32)
1485 }
1486 if b.Func.pass.debug > 0 {
1487 b.Func.Warnl(v.Pos, "Proved slicemask not needed")
1488 }
1489 v.AuxInt = -1
1490 }
1491 case OpCtz8, OpCtz16, OpCtz32, OpCtz64:
1492
1493
1494
1495 x := v.Args[0]
1496 lim, ok := ft.limits[x.ID]
1497 if !ok {
1498 break
1499 }
1500 if lim.umin > 0 || lim.min > 0 || lim.max < 0 {
1501 if b.Func.pass.debug > 0 {
1502 b.Func.Warnl(v.Pos, "Proved %v non-zero", v.Op)
1503 }
1504 v.Op = ctzNonZeroOp[v.Op]
1505 }
1506 case OpRsh8x8, OpRsh8x16, OpRsh8x32, OpRsh8x64,
1507 OpRsh16x8, OpRsh16x16, OpRsh16x32, OpRsh16x64,
1508 OpRsh32x8, OpRsh32x16, OpRsh32x32, OpRsh32x64,
1509 OpRsh64x8, OpRsh64x16, OpRsh64x32, OpRsh64x64:
1510
1511
1512 bits := 8 * v.Type.Size()
1513 if v.Args[1].isGenericIntConst() && v.Args[1].AuxInt >= bits-1 && ft.isNonNegative(v.Args[0]) {
1514 if b.Func.pass.debug > 0 {
1515 b.Func.Warnl(v.Pos, "Proved %v shifts to zero", v.Op)
1516 }
1517 switch bits {
1518 case 64:
1519 v.reset(OpConst64)
1520 case 32:
1521 v.reset(OpConst32)
1522 case 16:
1523 v.reset(OpConst16)
1524 case 8:
1525 v.reset(OpConst8)
1526 default:
1527 panic("unexpected integer size")
1528 }
1529 v.AuxInt = 0
1530 break
1531 }
1532
1533 fallthrough
1534 case OpLsh8x8, OpLsh8x16, OpLsh8x32, OpLsh8x64,
1535 OpLsh16x8, OpLsh16x16, OpLsh16x32, OpLsh16x64,
1536 OpLsh32x8, OpLsh32x16, OpLsh32x32, OpLsh32x64,
1537 OpLsh64x8, OpLsh64x16, OpLsh64x32, OpLsh64x64,
1538 OpRsh8Ux8, OpRsh8Ux16, OpRsh8Ux32, OpRsh8Ux64,
1539 OpRsh16Ux8, OpRsh16Ux16, OpRsh16Ux32, OpRsh16Ux64,
1540 OpRsh32Ux8, OpRsh32Ux16, OpRsh32Ux32, OpRsh32Ux64,
1541 OpRsh64Ux8, OpRsh64Ux16, OpRsh64Ux32, OpRsh64Ux64:
1542
1543
1544 by := v.Args[1]
1545 lim, ok := ft.limits[by.ID]
1546 if !ok {
1547 break
1548 }
1549 bits := 8 * v.Args[0].Type.Size()
1550 if lim.umax < uint64(bits) || (lim.max < bits && ft.isNonNegative(by)) {
1551 v.AuxInt = 1
1552 if b.Func.pass.debug > 0 {
1553 b.Func.Warnl(v.Pos, "Proved %v bounded", v.Op)
1554 }
1555 }
1556 case OpDiv16, OpDiv32, OpDiv64, OpMod16, OpMod32, OpMod64:
1557
1558
1559
1560
1561
1562 if b.Func.Config.arch != "386" && b.Func.Config.arch != "amd64" {
1563 break
1564 }
1565 divr := v.Args[1]
1566 divrLim, divrLimok := ft.limits[divr.ID]
1567 divd := v.Args[0]
1568 divdLim, divdLimok := ft.limits[divd.ID]
1569 if (divrLimok && (divrLim.max < -1 || divrLim.min > -1)) ||
1570 (divdLimok && divdLim.min > mostNegativeDividend[v.Op]) {
1571
1572
1573
1574
1575 v.AuxInt = 1
1576 if b.Func.pass.debug > 0 {
1577 b.Func.Warnl(v.Pos, "Proved %v does not need fix-up", v.Op)
1578 }
1579 }
1580 }
1581
1582
1583 for i, arg := range v.Args {
1584 switch arg.Op {
1585 case OpConst64, OpConst32, OpConst16, OpConst8:
1586 continue
1587 }
1588 lim, ok := ft.limits[arg.ID]
1589 if !ok {
1590 continue
1591 }
1592
1593 var constValue int64
1594 typ := arg.Type
1595 bits := 8 * typ.Size()
1596 switch {
1597 case lim.min == lim.max:
1598 constValue = lim.min
1599 case lim.umin == lim.umax:
1600
1601 switch bits {
1602 case 64:
1603 constValue = int64(lim.umin)
1604 case 32:
1605 constValue = int64(int32(lim.umin))
1606 case 16:
1607 constValue = int64(int16(lim.umin))
1608 case 8:
1609 constValue = int64(int8(lim.umin))
1610 default:
1611 panic("unexpected integer size")
1612 }
1613 default:
1614 continue
1615 }
1616 var c *Value
1617 f := b.Func
1618 switch bits {
1619 case 64:
1620 c = f.ConstInt64(typ, constValue)
1621 case 32:
1622 c = f.ConstInt32(typ, int32(constValue))
1623 case 16:
1624 c = f.ConstInt16(typ, int16(constValue))
1625 case 8:
1626 c = f.ConstInt8(typ, int8(constValue))
1627 default:
1628 panic("unexpected integer size")
1629 }
1630 v.SetArg(i, c)
1631 if b.Func.pass.debug > 1 {
1632 b.Func.Warnl(v.Pos, "Proved %v's arg %d (%v) is constant %d", v, i, arg, constValue)
1633 }
1634 }
1635 }
1636
1637 if b.Kind != BlockIf {
1638 return
1639 }
1640
1641
1642 parent := b
1643 for i, branch := range [...]branch{positive, negative} {
1644 child := parent.Succs[i].b
1645 if getBranch(sdom, parent, child) != unknown {
1646
1647
1648 continue
1649 }
1650
1651
1652 ft.checkpoint()
1653 addBranchRestrictions(ft, parent, branch)
1654 unsat := ft.unsat
1655 ft.restore()
1656 if unsat {
1657
1658
1659 removeBranch(parent, branch)
1660
1661
1662
1663
1664
1665 break
1666 }
1667 }
1668 }
1669
1670 func removeBranch(b *Block, branch branch) {
1671 c := b.Controls[0]
1672 if b.Func.pass.debug > 0 {
1673 verb := "Proved"
1674 if branch == positive {
1675 verb = "Disproved"
1676 }
1677 if b.Func.pass.debug > 1 {
1678 b.Func.Warnl(b.Pos, "%s %s (%s)", verb, c.Op, c)
1679 } else {
1680 b.Func.Warnl(b.Pos, "%s %s", verb, c.Op)
1681 }
1682 }
1683 if c != nil && c.Pos.IsStmt() == src.PosIsStmt && c.Pos.SameFileAndLine(b.Pos) {
1684
1685 b.Pos = b.Pos.WithIsStmt()
1686 }
1687 if branch == positive || branch == negative {
1688 b.Kind = BlockFirst
1689 b.ResetControls()
1690 if branch == positive {
1691 b.swapSuccessors()
1692 }
1693 } else {
1694
1695 }
1696 }
1697
1698
1699 func isNonNegative(v *Value) bool {
1700 if !v.Type.IsInteger() {
1701 v.Fatalf("isNonNegative bad type: %v", v.Type)
1702 }
1703
1704
1705
1706
1707 switch v.Op {
1708 case OpConst64:
1709 return v.AuxInt >= 0
1710
1711 case OpConst32:
1712 return int32(v.AuxInt) >= 0
1713
1714 case OpConst16:
1715 return int16(v.AuxInt) >= 0
1716
1717 case OpConst8:
1718 return int8(v.AuxInt) >= 0
1719
1720 case OpStringLen, OpSliceLen, OpSliceCap,
1721 OpZeroExt8to64, OpZeroExt16to64, OpZeroExt32to64,
1722 OpZeroExt8to32, OpZeroExt16to32, OpZeroExt8to16,
1723 OpCtz64, OpCtz32, OpCtz16, OpCtz8,
1724 OpCtz64NonZero, OpCtz32NonZero, OpCtz16NonZero, OpCtz8NonZero,
1725 OpBitLen64, OpBitLen32, OpBitLen16, OpBitLen8:
1726 return true
1727
1728 case OpRsh64Ux64, OpRsh32Ux64:
1729 by := v.Args[1]
1730 return by.Op == OpConst64 && by.AuxInt > 0
1731
1732 case OpRsh64x64, OpRsh32x64, OpRsh8x64, OpRsh16x64, OpRsh32x32, OpRsh64x32,
1733 OpSignExt32to64, OpSignExt16to64, OpSignExt8to64, OpSignExt16to32, OpSignExt8to32:
1734 return isNonNegative(v.Args[0])
1735
1736 case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
1737 return isNonNegative(v.Args[0]) || isNonNegative(v.Args[1])
1738
1739 case OpMod64, OpMod32, OpMod16, OpMod8,
1740 OpDiv64, OpDiv32, OpDiv16, OpDiv8,
1741 OpOr64, OpOr32, OpOr16, OpOr8,
1742 OpXor64, OpXor32, OpXor16, OpXor8:
1743 return isNonNegative(v.Args[0]) && isNonNegative(v.Args[1])
1744
1745
1746
1747 }
1748 return false
1749 }
1750
1751
1752 func isConstDelta(v *Value) (w *Value, delta int64) {
1753 cop := OpConst64
1754 switch v.Op {
1755 case OpAdd32, OpSub32:
1756 cop = OpConst32
1757 case OpAdd16, OpSub16:
1758 cop = OpConst16
1759 case OpAdd8, OpSub8:
1760 cop = OpConst8
1761 }
1762 switch v.Op {
1763 case OpAdd64, OpAdd32, OpAdd16, OpAdd8:
1764 if v.Args[0].Op == cop {
1765 return v.Args[1], v.Args[0].AuxInt
1766 }
1767 if v.Args[1].Op == cop {
1768 return v.Args[0], v.Args[1].AuxInt
1769 }
1770 case OpSub64, OpSub32, OpSub16, OpSub8:
1771 if v.Args[1].Op == cop {
1772 aux := v.Args[1].AuxInt
1773 if aux != -aux {
1774 return v.Args[0], -aux
1775 }
1776 }
1777 }
1778 return nil, 0
1779 }
1780
1781
1782
1783 func isCleanExt(v *Value) bool {
1784 switch v.Op {
1785 case OpSignExt8to16, OpSignExt8to32, OpSignExt8to64,
1786 OpSignExt16to32, OpSignExt16to64, OpSignExt32to64:
1787
1788 return v.Args[0].Type.IsSigned() && v.Type.IsSigned()
1789
1790 case OpZeroExt8to16, OpZeroExt8to32, OpZeroExt8to64,
1791 OpZeroExt16to32, OpZeroExt16to64, OpZeroExt32to64:
1792
1793 return !v.Args[0].Type.IsSigned()
1794 }
1795 return false
1796 }
1797
View as plain text