issue80517_2.go

     1  // run
     2  
     3  // Copyright 2026 The Go Authors. All rights reserved.
     4  // Use of this source code is governed by a BSD-style
     5  // license that can be found in the LICENSE file.
     6  
     7  // The prove pass must not use a fact that only becomes valid after a
     8  // later value executes to simplify an earlier value. Here make([]byte, n)
     9  // teaches prove that n >= 0, but that is only true after the make runs.
    10  // A buggy prove lets that fact travel back in time and rewrites the
    11  // earlier signed shift n>>1 into an unsigned shift, corrupting the result
    12  // for negative n.
    13  
    14  package main
    15  
    16  var sink []byte
    17  
    18  //go:noinline
    19  func trigger(n int) (res int) {
    20  	defer func() { recover() }()
    21  	if n < 100 {
    22  		res = n >> 1           // signed arithmetic shift right
    23  		sink = make([]byte, n) // only asserts n >= 0 after this point
    24  	}
    25  	return
    26  }
    27  
    28  func main() {
    29  	if got := trigger(-2); got != -1 {
    30  		println("n>>1 =", got, "want -1")
    31  		panic("prove miscompiled a signed shift")
    32  	}
    33  }
    34
View as plain text