issue80517_3.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  // Same time-traveling prove bug as issue80517_2.go, but the victims are a
     8  // signed division and a signed modulo. make([]byte, n) teaches prove that
     9  // n >= 0 only after it runs; a buggy prove lets that fact travel back and
    10  // rewrites the earlier n/4 and n%3 into unsigned operations, corrupting
    11  // the result for negative n.
    12  
    13  package main
    14  
    15  var sink []byte
    16  
    17  //go:noinline
    18  func trigger(n int) (q, r int) {
    19  	defer func() { recover() }()
    20  	if n < 100 {
    21  		q = n / 4              // signed division
    22  		r = n % 3              // signed modulo
    23  		sink = make([]byte, n) // only asserts n >= 0 after this point
    24  	}
    25  	return
    26  }
    27  
    28  func main() {
    29  	if q, r := trigger(-8); q != -2 || r != -2 {
    30  		println("n/4 =", q, "want -2;  n%3 =", r, "want -2")
    31  		panic("prove miscompiled a signed div/mod")
    32  	}
    33  }
    34
View as plain text