1// errorcheck -0 -d=ssa/prove/debug=1
2
3//go:build amd64
4
5// Copyright 2016 The Go Authors. All rights reserved.
6// Use of this source code is governed by a BSD-style
7// license that can be found in the LICENSE file.
8
9package main
10
11import "math"
12
13func f0(a []int) int {
14	a[0] = 1
15	a[0] = 1 // ERROR "Proved IsInBounds$"
16	a[6] = 1
17	a[6] = 1 // ERROR "Proved IsInBounds$"
18	a[5] = 1 // ERROR "Proved IsInBounds$"
19	a[5] = 1 // ERROR "Proved IsInBounds$"
20	return 13
21}
22
23func f1(a []int) int {
24	if len(a) <= 5 {
25		return 18
26	}
27	a[0] = 1 // ERROR "Proved IsInBounds$"
28	a[0] = 1 // ERROR "Proved IsInBounds$"
29	a[6] = 1
30	a[6] = 1 // ERROR "Proved IsInBounds$"
31	a[5] = 1 // ERROR "Proved IsInBounds$"
32	a[5] = 1 // ERROR "Proved IsInBounds$"
33	return 26
34}
35
36func f1b(a []int, i int, j uint) int {
37	if i >= 0 && i < len(a) {
38		return a[i] // ERROR "Proved IsInBounds$"
39	}
40	if i >= 10 && i < len(a) {
41		return a[i] // ERROR "Proved IsInBounds$"
42	}
43	if i >= 10 && i < len(a) {
44		return a[i] // ERROR "Proved IsInBounds$"
45	}
46	if i >= 10 && i < len(a) {
47		return a[i-10] // ERROR "Proved IsInBounds$"
48	}
49	if j < uint(len(a)) {
50		return a[j] // ERROR "Proved IsInBounds$"
51	}
52	return 0
53}
54
55func f1c(a []int, i int64) int {
56	c := uint64(math.MaxInt64 + 10) // overflows int
57	d := int64(c)
58	if i >= d && i < int64(len(a)) {
59		// d overflows, should not be handled.
60		return a[i]
61	}
62	return 0
63}
64
65func f2(a []int) int {
66	for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
67		a[i+1] = i
68		a[i+1] = i // ERROR "Proved IsInBounds$"
69	}
70	return 34
71}
72
73func f3(a []uint) int {
74	for i := uint(0); i < uint(len(a)); i++ {
75		a[i] = i // ERROR "Proved IsInBounds$"
76	}
77	return 41
78}
79
80func f4a(a, b, c int) int {
81	if a < b {
82		if a == b { // ERROR "Disproved Eq64$"
83			return 47
84		}
85		if a > b { // ERROR "Disproved Less64$"
86			return 50
87		}
88		if a < b { // ERROR "Proved Less64$"
89			return 53
90		}
91		// We can't get to this point and prove knows that, so
92		// there's no message for the next (obvious) branch.
93		if a != a {
94			return 56
95		}
96		return 61
97	}
98	return 63
99}
100
101func f4b(a, b, c int) int {
102	if a <= b {
103		if a >= b {
104			if a == b { // ERROR "Proved Eq64$"
105				return 70
106			}
107			return 75
108		}
109		return 77
110	}
111	return 79
112}
113
114func f4c(a, b, c int) int {
115	if a <= b {
116		if a >= b {
117			if a != b { // ERROR "Disproved Neq64$"
118				return 73
119			}
120			return 75
121		}
122		return 77
123	}
124	return 79
125}
126
127func f4d(a, b, c int) int {
128	if a < b {
129		if a < c {
130			if a < b { // ERROR "Proved Less64$"
131				if a < c { // ERROR "Proved Less64$"
132					return 87
133				}
134				return 89
135			}
136			return 91
137		}
138		return 93
139	}
140	return 95
141}
142
143func f4e(a, b, c int) int {
144	if a < b {
145		if b > a { // ERROR "Proved Less64$"
146			return 101
147		}
148		return 103
149	}
150	return 105
151}
152
153func f4f(a, b, c int) int {
154	if a <= b {
155		if b > a {
156			if b == a { // ERROR "Disproved Eq64$"
157				return 112
158			}
159			return 114
160		}
161		if b >= a { // ERROR "Proved Leq64$"
162			if b == a { // ERROR "Proved Eq64$"
163				return 118
164			}
165			return 120
166		}
167		return 122
168	}
169	return 124
170}
171
172func f5(a, b uint) int {
173	if a == b {
174		if a <= b { // ERROR "Proved Leq64U$"
175			return 130
176		}
177		return 132
178	}
179	return 134
180}
181
182// These comparisons are compile time constants.
183func f6a(a uint8) int {
184	if a < a { // ERROR "Disproved Less8U$"
185		return 140
186	}
187	return 151
188}
189
190func f6b(a uint8) int {
191	if a < a { // ERROR "Disproved Less8U$"
192		return 140
193	}
194	return 151
195}
196
197func f6x(a uint8) int {
198	if a > a { // ERROR "Disproved Less8U$"
199		return 143
200	}
201	return 151
202}
203
204func f6d(a uint8) int {
205	if a <= a { // ERROR "Proved Leq8U$"
206		return 146
207	}
208	return 151
209}
210
211func f6e(a uint8) int {
212	if a >= a { // ERROR "Proved Leq8U$"
213		return 149
214	}
215	return 151
216}
217
218func f7(a []int, b int) int {
219	if b < len(a) {
220		a[b] = 3
221		if b < len(a) { // ERROR "Proved Less64$"
222			a[b] = 5 // ERROR "Proved IsInBounds$"
223		}
224	}
225	return 161
226}
227
228func f8(a, b uint) int {
229	if a == b {
230		return 166
231	}
232	if a > b {
233		return 169
234	}
235	if a < b { // ERROR "Proved Less64U$"
236		return 172
237	}
238	return 174
239}
240
241func f9(a, b bool) int {
242	if a {
243		return 1
244	}
245	if a || b { // ERROR "Disproved Arg$"
246		return 2
247	}
248	return 3
249}
250
251func f10(a string) int {
252	n := len(a)
253	// We optimize comparisons with small constant strings (see cmd/compile/internal/gc/walk.go),
254	// so this string literal must be long.
255	if a[:n>>1] == "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" {
256		return 0
257	}
258	return 1
259}
260
261func f11a(a []int, i int) {
262	useInt(a[i])
263	useInt(a[i]) // ERROR "Proved IsInBounds$"
264}
265
266func f11b(a []int, i int) {
267	useSlice(a[i:])
268	useSlice(a[i:]) // ERROR "Proved IsSliceInBounds$"
269}
270
271func f11c(a []int, i int) {
272	useSlice(a[:i])
273	useSlice(a[:i]) // ERROR "Proved IsSliceInBounds$"
274}
275
276func f11d(a []int, i int) {
277	useInt(a[2*i+7])
278	useInt(a[2*i+7]) // ERROR "Proved IsInBounds$"
279}
280
281func f12(a []int, b int) {
282	useSlice(a[:b])
283}
284
285func f13a(a, b, c int, x bool) int {
286	if a > 12 {
287		if x {
288			if a < 12 { // ERROR "Disproved Less64$"
289				return 1
290			}
291		}
292		if x {
293			if a <= 12 { // ERROR "Disproved Leq64$"
294				return 2
295			}
296		}
297		if x {
298			if a == 12 { // ERROR "Disproved Eq64$"
299				return 3
300			}
301		}
302		if x {
303			if a >= 12 { // ERROR "Proved Leq64$"
304				return 4
305			}
306		}
307		if x {
308			if a > 12 { // ERROR "Proved Less64$"
309				return 5
310			}
311		}
312		return 6
313	}
314	return 0
315}
316
317func f13b(a int, x bool) int {
318	if a == -9 {
319		if x {
320			if a < -9 { // ERROR "Disproved Less64$"
321				return 7
322			}
323		}
324		if x {
325			if a <= -9 { // ERROR "Proved Leq64$"
326				return 8
327			}
328		}
329		if x {
330			if a == -9 { // ERROR "Proved Eq64$"
331				return 9
332			}
333		}
334		if x {
335			if a >= -9 { // ERROR "Proved Leq64$"
336				return 10
337			}
338		}
339		if x {
340			if a > -9 { // ERROR "Disproved Less64$"
341				return 11
342			}
343		}
344		return 12
345	}
346	return 0
347}
348
349func f13c(a int, x bool) int {
350	if a < 90 {
351		if x {
352			if a < 90 { // ERROR "Proved Less64$"
353				return 13
354			}
355		}
356		if x {
357			if a <= 90 { // ERROR "Proved Leq64$"
358				return 14
359			}
360		}
361		if x {
362			if a == 90 { // ERROR "Disproved Eq64$"
363				return 15
364			}
365		}
366		if x {
367			if a >= 90 { // ERROR "Disproved Leq64$"
368				return 16
369			}
370		}
371		if x {
372			if a > 90 { // ERROR "Disproved Less64$"
373				return 17
374			}
375		}
376		return 18
377	}
378	return 0
379}
380
381func f13d(a int) int {
382	if a < 5 {
383		if a < 9 { // ERROR "Proved Less64$"
384			return 1
385		}
386	}
387	return 0
388}
389
390func f13e(a int) int {
391	if a > 9 {
392		if a > 5 { // ERROR "Proved Less64$"
393			return 1
394		}
395	}
396	return 0
397}
398
399func f13f(a, b int64) int64 {
400	if b != math.MaxInt64 {
401		return 42
402	}
403	if a > b {
404		if a == 0 { // ERROR "Disproved Eq64$"
405			return 1
406		}
407	}
408	return 0
409}
410
411func f13g(a int) int {
412	if a < 3 {
413		return 5
414	}
415	if a > 3 {
416		return 6
417	}
418	if a == 3 { // ERROR "Proved Eq64$"
419		return 7
420	}
421	return 8
422}
423
424func f13h(a int) int {
425	if a < 3 {
426		if a > 1 {
427			if a == 2 { // ERROR "Proved Eq64$"
428				return 5
429			}
430		}
431	}
432	return 0
433}
434
435func f13i(a uint) int {
436	if a == 0 {
437		return 1
438	}
439	if a > 0 { // ERROR "Proved Less64U$"
440		return 2
441	}
442	return 3
443}
444
445func f14(p, q *int, a []int) {
446	// This crazy ordering usually gives i1 the lowest value ID,
447	// j the middle value ID, and i2 the highest value ID.
448	// That used to confuse CSE because it ordered the args
449	// of the two + ops below differently.
450	// That in turn foiled bounds check elimination.
451	i1 := *p
452	j := *q
453	i2 := *p
454	useInt(a[i1+j])
455	useInt(a[i2+j]) // ERROR "Proved IsInBounds$"
456}
457
458func f15(s []int, x int) {
459	useSlice(s[x:])
460	useSlice(s[:x]) // ERROR "Proved IsSliceInBounds$"
461}
462
463func f16(s []int) []int {
464	if len(s) >= 10 {
465		return s[:10] // ERROR "Proved IsSliceInBounds$"
466	}
467	return nil
468}
469
470func f17(b []int) {
471	for i := 0; i < len(b); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
472		// This tests for i <= cap, which we can only prove
473		// using the derived relation between len and cap.
474		// This depends on finding the contradiction, since we
475		// don't query this condition directly.
476		useSlice(b[:i]) // ERROR "Proved IsSliceInBounds$"
477	}
478}
479
480func f18(b []int, x int, y uint) {
481	_ = b[x]
482	_ = b[y]
483
484	if x > len(b) { // ERROR "Disproved Less64$"
485		return
486	}
487	if y > uint(len(b)) { // ERROR "Disproved Less64U$"
488		return
489	}
490	if int(y) > len(b) { // ERROR "Disproved Less64$"
491		return
492	}
493}
494
495func f19() (e int64, err error) {
496	// Issue 29502: slice[:0] is incorrectly disproved.
497	var stack []int64
498	stack = append(stack, 123)
499	if len(stack) > 1 {
500		panic("too many elements")
501	}
502	last := len(stack) - 1
503	e = stack[last]
504	// Buggy compiler prints "Disproved Leq64" for the next line.
505	stack = stack[:last]
506	return e, nil
507}
508
509func sm1(b []int, x int) {
510	// Test constant argument to slicemask.
511	useSlice(b[2:8]) // ERROR "Proved slicemask not needed$"
512	// Test non-constant argument with known limits.
513	if cap(b) > 10 {
514		useSlice(b[2:])
515	}
516}
517
518func lim1(x, y, z int) {
519	// Test relations between signed and unsigned limits.
520	if x > 5 {
521		if uint(x) > 5 { // ERROR "Proved Less64U$"
522			return
523		}
524	}
525	if y >= 0 && y < 4 {
526		if uint(y) > 4 { // ERROR "Disproved Less64U$"
527			return
528		}
529		if uint(y) < 5 { // ERROR "Proved Less64U$"
530			return
531		}
532	}
533	if z < 4 {
534		if uint(z) > 4 { // Not provable without disjunctions.
535			return
536		}
537	}
538}
539
540// fence1–4 correspond to the four fence-post implications.
541
542func fence1(b []int, x, y int) {
543	// Test proofs that rely on fence-post implications.
544	if x+1 > y {
545		if x < y { // ERROR "Disproved Less64$"
546			return
547		}
548	}
549	if len(b) < cap(b) {
550		// This eliminates the growslice path.
551		b = append(b, 1) // ERROR "Disproved Less64U$"
552	}
553}
554
555func fence2(x, y int) {
556	if x-1 < y {
557		if x > y { // ERROR "Disproved Less64$"
558			return
559		}
560	}
561}
562
563func fence3(b, c []int, x, y int64) {
564	if x-1 >= y {
565		if x <= y { // Can't prove because x may have wrapped.
566			return
567		}
568	}
569
570	if x != math.MinInt64 && x-1 >= y {
571		if x <= y { // ERROR "Disproved Leq64$"
572			return
573		}
574	}
575
576	c[len(c)-1] = 0 // Can't prove because len(c) might be 0
577
578	if n := len(b); n > 0 {
579		b[n-1] = 0 // ERROR "Proved IsInBounds$"
580	}
581}
582
583func fence4(x, y int64) {
584	if x >= y+1 {
585		if x <= y {
586			return
587		}
588	}
589	if y != math.MaxInt64 && x >= y+1 {
590		if x <= y { // ERROR "Disproved Leq64$"
591			return
592		}
593	}
594}
595
596// Check transitive relations
597func trans1(x, y int64) {
598	if x > 5 {
599		if y > x {
600			if y > 2 { // ERROR "Proved Less64$"
601				return
602			}
603		} else if y == x {
604			if y > 5 { // ERROR "Proved Less64$"
605				return
606			}
607		}
608	}
609	if x >= 10 {
610		if y > x {
611			if y > 10 { // ERROR "Proved Less64$"
612				return
613			}
614		}
615	}
616}
617
618func trans2(a, b []int, i int) {
619	if len(a) != len(b) {
620		return
621	}
622
623	_ = a[i]
624	_ = b[i] // ERROR "Proved IsInBounds$"
625}
626
627func trans3(a, b []int, i int) {
628	if len(a) > len(b) {
629		return
630	}
631
632	_ = a[i]
633	_ = b[i] // ERROR "Proved IsInBounds$"
634}
635
636func trans4(b []byte, x int) {
637	// Issue #42603: slice len/cap transitive relations.
638	switch x {
639	case 0:
640		if len(b) < 20 {
641			return
642		}
643		_ = b[:2] // ERROR "Proved IsSliceInBounds$"
644	case 1:
645		if len(b) < 40 {
646			return
647		}
648		_ = b[:2] // ERROR "Proved IsSliceInBounds$"
649	}
650}
651
652// Derived from nat.cmp
653func natcmp(x, y []uint) (r int) {
654	m := len(x)
655	n := len(y)
656	if m != n || m == 0 {
657		return
658	}
659
660	i := m - 1
661	for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment 1$"
662		x[i] == // ERROR "Proved IsInBounds$"
663			y[i] { // ERROR "Proved IsInBounds$"
664		i--
665	}
666
667	switch {
668	case x[i] < // todo, cannot prove this because it's dominated by i<=0 || x[i]==y[i]
669		y[i]: // ERROR "Proved IsInBounds$"
670		r = -1
671	case x[i] > // ERROR "Proved IsInBounds$"
672		y[i]: // ERROR "Proved IsInBounds$"
673		r = 1
674	}
675	return
676}
677
678func suffix(s, suffix string) bool {
679	// todo, we're still not able to drop the bound check here in the general case
680	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
681}
682
683func constsuffix(s string) bool {
684	return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
685}
686
687// oforuntil tests the pattern created by OFORUNTIL blocks. These are
688// handled by addLocalInductiveFacts rather than findIndVar.
689func oforuntil(b []int) {
690	i := 0
691	if len(b) > i {
692	top:
693		println(b[i]) // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$"
694		i++
695		if i < len(b) {
696			goto top
697		}
698	}
699}
700
701func atexit(foobar []func()) {
702	for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
703		f := foobar[i]
704		foobar = foobar[:i] // ERROR "IsSliceInBounds"
705		f()
706	}
707}
708
709func make1(n int) []int {
710	s := make([]int, n)
711	for i := 0; i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
712		s[i] = 1 // ERROR "Proved IsInBounds$"
713	}
714	return s
715}
716
717func make2(n int) []int {
718	s := make([]int, n)
719	for i := range s { // ERROR "Induction variable: limits \[0,\?\), increment 1"
720		s[i] = 1 // ERROR "Proved IsInBounds$"
721	}
722	return s
723}
724
725// The range tests below test the index variable of range loops.
726
727// range1 compiles to the "efficiently indexable" form of a range loop.
728func range1(b []int) {
729	for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
730		b[i] = v + 1    // ERROR "Proved IsInBounds$"
731		if i < len(b) { // ERROR "Proved Less64$"
732			println("x")
733		}
734		if i >= 0 { // ERROR "Proved Leq64$"
735			println("x")
736		}
737	}
738}
739
740// range2 elements are larger, so they use the general form of a range loop.
741func range2(b [][32]int) {
742	for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
743		b[i][0] = v[0] + 1 // ERROR "Proved IsInBounds$"
744		if i < len(b) {    // ERROR "Proved Less64$"
745			println("x")
746		}
747		if i >= 0 { // ERROR "Proved Leq64$"
748			println("x")
749		}
750	}
751}
752
753// signhint1-2 test whether the hint (int >= 0) is propagated into the loop.
754func signHint1(i int, data []byte) {
755	if i >= 0 {
756		for i < len(data) { // ERROR "Induction variable: limits \[\?,\?\), increment 1$"
757			_ = data[i] // ERROR "Proved IsInBounds$"
758			i++
759		}
760	}
761}
762
763func signHint2(b []byte, n int) {
764	if n < 0 {
765		panic("")
766	}
767	_ = b[25]
768	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
769		b[i] = 123 // ERROR "Proved IsInBounds$"
770	}
771}
772
773// indexGT0 tests whether prove learns int index >= 0 from bounds check.
774func indexGT0(b []byte, n int) {
775	_ = b[n]
776	_ = b[25]
777
778	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
779		b[i] = 123 // ERROR "Proved IsInBounds$"
780	}
781}
782
783// Induction variable in unrolled loop.
784func unrollUpExcl(a []int) int {
785	var i, x int
786	for i = 0; i < len(a)-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$"
787		x += a[i] // ERROR "Proved IsInBounds$"
788		x += a[i+1]
789	}
790	if i == len(a)-1 {
791		x += a[i]
792	}
793	return x
794}
795
796// Induction variable in unrolled loop.
797func unrollUpIncl(a []int) int {
798	var i, x int
799	for i = 0; i <= len(a)-2; i += 2 { // ERROR "Induction variable: limits \[0,\?\], increment 2$"
800		x += a[i] // ERROR "Proved IsInBounds$"
801		x += a[i+1]
802	}
803	if i == len(a)-1 {
804		x += a[i]
805	}
806	return x
807}
808
809// Induction variable in unrolled loop.
810func unrollDownExcl0(a []int) int {
811	var i, x int
812	for i = len(a) - 1; i > 0; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
813		x += a[i]   // ERROR "Proved IsInBounds$"
814		x += a[i-1] // ERROR "Proved IsInBounds$"
815	}
816	if i == 0 {
817		x += a[i]
818	}
819	return x
820}
821
822// Induction variable in unrolled loop.
823func unrollDownExcl1(a []int) int {
824	var i, x int
825	for i = len(a) - 1; i >= 1; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
826		x += a[i]   // ERROR "Proved IsInBounds$"
827		x += a[i-1] // ERROR "Proved IsInBounds$"
828	}
829	if i == 0 {
830		x += a[i]
831	}
832	return x
833}
834
835// Induction variable in unrolled loop.
836func unrollDownInclStep(a []int) int {
837	var i, x int
838	for i = len(a); i >= 2; i -= 2 { // ERROR "Induction variable: limits \[2,\?\], increment 2$"
839		x += a[i-1] // ERROR "Proved IsInBounds$"
840		x += a[i-2] // ERROR "Proved IsInBounds$"
841	}
842	if i == 1 {
843		x += a[i-1]
844	}
845	return x
846}
847
848// Not an induction variable (step too large)
849func unrollExclStepTooLarge(a []int) int {
850	var i, x int
851	for i = 0; i < len(a)-1; i += 3 {
852		x += a[i]
853		x += a[i+1]
854	}
855	if i == len(a)-1 {
856		x += a[i]
857	}
858	return x
859}
860
861// Not an induction variable (step too large)
862func unrollInclStepTooLarge(a []int) int {
863	var i, x int
864	for i = 0; i <= len(a)-2; i += 3 {
865		x += a[i]
866		x += a[i+1]
867	}
868	if i == len(a)-1 {
869		x += a[i]
870	}
871	return x
872}
873
874// Not an induction variable (min too small, iterating down)
875func unrollDecMin(a []int, b int) int {
876	if b != math.MinInt64 {
877		return 42
878	}
879	var i, x int
880	for i = len(a); i >= b; i -= 2 {
881		x += a[i-1]
882		x += a[i-2]
883	}
884	if i == 1 { // ERROR "Disproved Eq64$"
885		x += a[i-1]
886	}
887	return x
888}
889
890// Not an induction variable (min too small, iterating up -- perhaps could allow, but why bother?)
891func unrollIncMin(a []int, b int) int {
892	if b != math.MinInt64 {
893		return 42
894	}
895	var i, x int
896	for i = len(a); i >= b; i += 2 {
897		x += a[i-1]
898		x += a[i-2]
899	}
900	if i == 1 { // ERROR "Disproved Eq64$"
901		x += a[i-1]
902	}
903	return x
904}
905
906// The 4 xxxxExtNto64 functions below test whether prove is looking
907// through value-preserving sign/zero extensions of index values (issue #26292).
908
909// Look through all extensions
910func signExtNto64(x []int, j8 int8, j16 int16, j32 int32) int {
911	if len(x) < 22 {
912		return 0
913	}
914	if j8 >= 0 && j8 < 22 {
915		return x[j8] // ERROR "Proved IsInBounds$"
916	}
917	if j16 >= 0 && j16 < 22 {
918		return x[j16] // ERROR "Proved IsInBounds$"
919	}
920	if j32 >= 0 && j32 < 22 {
921		return x[j32] // ERROR "Proved IsInBounds$"
922	}
923	return 0
924}
925
926func zeroExtNto64(x []int, j8 uint8, j16 uint16, j32 uint32) int {
927	if len(x) < 22 {
928		return 0
929	}
930	if j8 >= 0 && j8 < 22 {
931		return x[j8] // ERROR "Proved IsInBounds$"
932	}
933	if j16 >= 0 && j16 < 22 {
934		return x[j16] // ERROR "Proved IsInBounds$"
935	}
936	if j32 >= 0 && j32 < 22 {
937		return x[j32] // ERROR "Proved IsInBounds$"
938	}
939	return 0
940}
941
942// Process fence-post implications through 32to64 extensions (issue #29964)
943func signExt32to64Fence(x []int, j int32) int {
944	if x[j] != 0 {
945		return 1
946	}
947	if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
948		return 1
949	}
950	return 0
951}
952
953func zeroExt32to64Fence(x []int, j uint32) int {
954	if x[j] != 0 {
955		return 1
956	}
957	if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
958		return 1
959	}
960	return 0
961}
962
963// Ensure that bounds checks with negative indexes are not incorrectly removed.
964func negIndex() {
965	n := make([]int, 1)
966	for i := -1; i <= 0; i++ { // ERROR "Induction variable: limits \[-1,0\], increment 1$"
967		n[i] = 1
968	}
969}
970func negIndex2(n int) {
971	a := make([]int, 5)
972	b := make([]int, 5)
973	c := make([]int, 5)
974	for i := -1; i <= 0; i-- {
975		b[i] = i
976		n++
977		if n > 10 {
978			break
979		}
980	}
981	useSlice(a)
982	useSlice(c)
983}
984
985// Check that prove is zeroing these right shifts of positive ints by bit-width - 1.
986// e.g (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) && ft.isNonNegative(n) -> 0
987func sh64(n int64) int64 {
988	if n < 0 {
989		return n
990	}
991	return n >> 63 // ERROR "Proved Rsh64x64 shifts to zero"
992}
993
994func sh32(n int32) int32 {
995	if n < 0 {
996		return n
997	}
998	return n >> 31 // ERROR "Proved Rsh32x64 shifts to zero"
999}
1000
1001func sh32x64(n int32) int32 {
1002	if n < 0 {
1003		return n
1004	}
1005	return n >> uint64(31) // ERROR "Proved Rsh32x64 shifts to zero"
1006}
1007
1008func sh16(n int16) int16 {
1009	if n < 0 {
1010		return n
1011	}
1012	return n >> 15 // ERROR "Proved Rsh16x64 shifts to zero"
1013}
1014
1015func sh64noopt(n int64) int64 {
1016	return n >> 63 // not optimized; n could be negative
1017}
1018
1019// These cases are division of a positive signed integer by a power of 2.
1020// The opt pass doesnt have sufficient information to see that n is positive.
1021// So, instead, opt rewrites the division with a less-than-optimal replacement.
1022// Prove, which can see that n is nonnegative, cannot see the division because
1023// opt, an earlier pass, has already replaced it.
1024// The fix for this issue allows prove to zero a right shift that was added as
1025// part of the less-than-optimal reqwrite. That change by prove then allows
1026// lateopt to clean up all the unnecessary parts of the original division
1027// replacement. See issue #36159.
1028func divShiftClean(n int) int {
1029	if n < 0 {
1030		return n
1031	}
1032	return n / int(8) // ERROR "Proved Rsh64x64 shifts to zero"
1033}
1034
1035func divShiftClean64(n int64) int64 {
1036	if n < 0 {
1037		return n
1038	}
1039	return n / int64(16) // ERROR "Proved Rsh64x64 shifts to zero"
1040}
1041
1042func divShiftClean32(n int32) int32 {
1043	if n < 0 {
1044		return n
1045	}
1046	return n / int32(16) // ERROR "Proved Rsh32x64 shifts to zero"
1047}
1048
1049// Bounds check elimination
1050
1051func sliceBCE1(p []string, h uint) string {
1052	if len(p) == 0 {
1053		return ""
1054	}
1055
1056	i := h & uint(len(p)-1)
1057	return p[i] // ERROR "Proved IsInBounds$"
1058}
1059
1060func sliceBCE2(p []string, h int) string {
1061	if len(p) == 0 {
1062		return ""
1063	}
1064	i := h & (len(p) - 1)
1065	return p[i] // ERROR "Proved IsInBounds$"
1066}
1067
1068func and(p []byte) ([]byte, []byte) { // issue #52563
1069	const blocksize = 16
1070	fullBlocks := len(p) &^ (blocksize - 1)
1071	blk := p[:fullBlocks] // ERROR "Proved IsSliceInBounds$"
1072	rem := p[fullBlocks:] // ERROR "Proved IsSliceInBounds$"
1073	return blk, rem
1074}
1075
1076func rshu(x, y uint) int {
1077	z := x >> y
1078	if z <= x { // ERROR "Proved Leq64U$"
1079		return 1
1080	}
1081	return 0
1082}
1083
1084func divu(x, y uint) int {
1085	z := x / y
1086	if z <= x { // ERROR "Proved Leq64U$"
1087		return 1
1088	}
1089	return 0
1090}
1091
1092func modu1(x, y uint) int {
1093	z := x % y
1094	if z < y { // ERROR "Proved Less64U$"
1095		return 1
1096	}
1097	return 0
1098}
1099
1100func modu2(x, y uint) int {
1101	z := x % y
1102	if z <= x { // ERROR "Proved Leq64U$"
1103		return 1
1104	}
1105	return 0
1106}
1107
1108func issue57077(s []int) (left, right []int) {
1109	middle := len(s) / 2
1110	left = s[:middle] // ERROR "Proved IsSliceInBounds$"
1111	right = s[middle:] // ERROR "Proved IsSliceInBounds$"
1112	return
1113}
1114
1115func issue51622(b []byte) int {
1116	if len(b) >= 3 && b[len(b)-3] == '#' { // ERROR "Proved IsInBounds$"
1117		return len(b)
1118	}
1119	return 0
1120}
1121
1122func issue45928(x int) {
1123	combinedFrac := x / (x | (1 << 31)) // ERROR "Proved Neq64$"
1124	useInt(combinedFrac)
1125}
1126
1127//go:noinline
1128func useInt(a int) {
1129}
1130
1131//go:noinline
1132func useSlice(a []int) {
1133}
1134
1135func main() {
1136}
1137