Source file test/prove_popcount.go

     1  // errorcheck -0 -d=ssa/prove/debug=1
     2  
     3  //go:build amd64.v3 || arm64
     4  
     5  // Copyright 2025 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  
     9  // FIXME(@Jorropo): this file exists because I havn't yet bothered to
    10  // make prove work on the pure go function call fallback.
    11  // My idea was to wait until CL 637936 is merged, then we can always emit
    12  // the PopCount SSA operation and translate them to pure function calls
    13  // in late-opt.
    14  
    15  package main
    16  
    17  import "math/bits"
    18  
    19  func onesCountsBounds(x uint64, ensureAllBranchesCouldHappen func() bool) int {
    20  	z := bits.OnesCount64(x)
    21  	if ensureAllBranchesCouldHappen() && z > 64 { // ERROR "Disproved Less64$"
    22  		return 42
    23  	}
    24  	if ensureAllBranchesCouldHappen() && z <= 64 { // ERROR "Proved Leq64$"
    25  		return 4242
    26  	}
    27  	if ensureAllBranchesCouldHappen() && z < 0 { // ERROR "Disproved Less64$"
    28  		return 424242
    29  	}
    30  	if ensureAllBranchesCouldHappen() && z >= 0 { // ERROR "Proved Leq64$"
    31  		return 42424242
    32  	}
    33  	return z
    34  }
    35  
    36  func onesCountsTight(x uint64, ensureAllBranchesCouldHappen func() bool) int {
    37  	const maxv = 0xff0f
    38  	const minv = 0xff00
    39  	x = max(x, minv)
    40  	x = min(x, maxv)
    41  
    42  	z := bits.OnesCount64(x)
    43  
    44  	if ensureAllBranchesCouldHappen() && z > bits.OnesCount64(maxv) { // ERROR "Disproved Less64$"
    45  		return 42
    46  	}
    47  	if ensureAllBranchesCouldHappen() && z <= bits.OnesCount64(maxv) { // ERROR "Proved Leq64$"
    48  		return 4242
    49  	}
    50  	if ensureAllBranchesCouldHappen() && z < bits.OnesCount64(minv) { // ERROR "Disproved Less64$"
    51  		return 424242
    52  	}
    53  	if ensureAllBranchesCouldHappen() && z >= bits.OnesCount64(minv) { // ERROR "Proved Leq64$"
    54  		return 42424242
    55  	}
    56  	return z
    57  }
    58  
    59  func main() {
    60  }
    61  

View as plain text