Skip to content

cmd/compile: missed prove inferences with uint conversions #16653

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
josharian opened this issue Aug 10, 2016 · 4 comments
Closed

cmd/compile: missed prove inferences with uint conversions #16653

josharian opened this issue Aug 10, 2016 · 4 comments
Labels
FrozenDueToAge NeedsFix The path to resolution is known, but the work has not been done. Performance
Milestone
Unplanned

Comments

@josharian
Copy link
Contributor

[moved from private email with @brtzsnr]

Consider this code, adapted from test/prove.go:

package p

func f(a []int, i int) int {
    if i >= 0 && i < len(a) {
        return a[i]
    }
    if i >= 10 && i < len(a) {
        return a[i]
    }
    return 0
}

func g(a []int, i int) int {
    if uint(i) < uint(len(a)) {
        return a[i]
    }
    if i >= 10 && i < len(a) {
        return a[i]
    }
    return 0
}

Functions f and g are equivalent. The only difference between them is the expression i >= 0 && i < len(a) in f vs uint(i) < uint(len(a)). And these are equivalent, because we know that len(a) is non-negative. But compiling with go tool compile -d=ssa/prove/debug=3 x.go, we get:

x.go:5: Proved non-negative bounds IsInBounds
x.go:8: Proved non-negative bounds IsInBounds
x.go:15: Proved IsInBounds
x.go:18: Disproved IsInBounds

Going from "x.go:5: Proved non-negative bounds IsInBounds" to "x.go:15: Proved IsInBounds" is a bit unfortunate, but ok. Going from "x.go:8: Proved non-negative bounds IsInBounds" to "x.go:18: Disproved IsInBounds" seems incorrect.
@josharian josharian added this to the Go1.8 milestone Aug 10, 2016
@brtzsnr
Copy link
Contributor

brtzsnr commented Aug 10, 2016 •
edited
Loading

The problem in this case is that the second return a[i] is deadcode. The second condition can be reached only if i >= len(a) so the index is out of bounds which is why prove prints "Disproved".

There is indeed a missed optimization and the second condition is not fully removed. If you find a correctness issue, let me know. Otherwise, I'll address this once the go1.8 opens and I have some spare time.

edit: The difference between the output is because it looks at different facts to establish the truth value. For f it uses i >= 10 && i < len(a) and for g it uses uint(i) < uint(len(a)).

tl;dr: It's not a bug. It's dead code.

@josharian josharian changed the title cmd/compile: bad prove inferences with uint conversions cmd/compile: missed prove inferences with uint conversions Aug 10, 2016
@josharian
Copy link
Contributor Author

Thanks, Alexandru. I have a CL that I hope to mail soon (that you know about) that will make this kind of show up a lot more. Good to know that I don't have to hold that CL for this. :)

@gopherbot
Copy link
Contributor

CL https://golang.org/cl/27652 mentions this issue.

gopherbot pushed a commit that referenced this issue Aug 25, 2016
@josharian
cmd/compile: optimize integer "in range" expressions
6286188 
Use unsigned comparisons to reduce from
two comparisons to one for integer "in range"
checks, such as a <= b && b < c.
We already do this for bounds checks.
Extend it to user code.

This is much easier to do in the front end than SSA.
A back end optimization would be more powerful,
but this is a good start.

This reduces the power of some of SSA prove
inferences (#16653), but those regressions appear
to be rare and not worth holding this CL for.

Fixes #15844.
Fixes #16697.

strconv benchmarks:

name                          old time/op  new time/op   delta
Atof64Decimal-8               41.4ns ± 3%   38.9ns ± 2%   -5.89%  (p=0.000 n=24+25)
Atof64Float-8                 48.5ns ± 0%   46.8ns ± 3%   -3.64%  (p=0.000 n=20+23)
Atof64FloatExp-8              97.7ns ± 4%   93.5ns ± 1%   -4.25%  (p=0.000 n=25+20)
Atof64Big-8                    187ns ± 8%    162ns ± 2%  -13.54%  (p=0.000 n=24+22)
Atof64RandomBits-8             250ns ± 6%    233ns ± 5%   -6.76%  (p=0.000 n=25+25)
Atof64RandomFloats-8           160ns ± 0%    152ns ± 0%   -5.00%  (p=0.000 n=21+22)
Atof32Decimal-8               41.1ns ± 1%   38.7ns ± 2%   -5.86%  (p=0.000 n=24+24)
Atof32Float-8                 46.1ns ± 1%   43.5ns ± 3%   -5.63%  (p=0.000 n=21+24)
Atof32FloatExp-8               101ns ± 4%    100ns ± 2%   -1.59%  (p=0.000 n=24+23)
Atof32Random-8                 136ns ± 3%    133ns ± 3%   -2.83%  (p=0.000 n=22+22)
Atoi-8                        33.8ns ± 3%   30.6ns ± 3%   -9.51%  (p=0.000 n=24+25)
AtoiNeg-8                     31.6ns ± 3%   29.1ns ± 2%   -8.05%  (p=0.000 n=23+24)
Atoi64-8                      48.6ns ± 1%   43.8ns ± 1%   -9.81%  (p=0.000 n=20+23)
Atoi64Neg-8                   47.1ns ± 4%   42.0ns ± 2%  -10.83%  (p=0.000 n=25+25)
FormatFloatDecimal-8           177ns ± 9%    178ns ± 6%     ~     (p=0.460 n=25+25)
FormatFloat-8                  282ns ± 6%    282ns ± 3%     ~     (p=0.954 n=25+22)
FormatFloatExp-8               259ns ± 7%    255ns ± 6%     ~     (p=0.089 n=25+24)
FormatFloatNegExp-8            253ns ± 6%    254ns ± 6%     ~     (p=0.941 n=25+24)
FormatFloatBig-8               340ns ± 6%    341ns ± 8%     ~     (p=0.600 n=22+25)
AppendFloatDecimal-8          79.4ns ± 0%   80.6ns ± 6%     ~     (p=0.861 n=20+25)
AppendFloat-8                  175ns ± 3%    174ns ± 0%     ~     (p=0.722 n=25+20)
AppendFloatExp-8               142ns ± 4%    142ns ± 2%     ~     (p=0.948 n=25+24)
AppendFloatNegExp-8            137ns ± 2%    138ns ± 2%   +0.70%  (p=0.001 n=24+25)
AppendFloatBig-8               218ns ± 3%    218ns ± 4%     ~     (p=0.596 n=25+25)
AppendFloatBinaryExp-8        80.0ns ± 4%   78.0ns ± 1%   -2.43%  (p=0.000 n=24+21)
AppendFloat32Integer-8        82.3ns ± 3%   79.3ns ± 4%   -3.69%  (p=0.000 n=24+25)
AppendFloat32ExactFraction-8   143ns ± 2%    143ns ± 0%     ~     (p=0.177 n=23+19)
AppendFloat32Point-8           175ns ± 3%    175ns ± 3%     ~     (p=0.062 n=24+25)
AppendFloat32Exp-8             139ns ± 2%    137ns ± 4%   -1.05%  (p=0.001 n=24+24)
AppendFloat32NegExp-8          134ns ± 0%    137ns ± 4%   +2.06%  (p=0.000 n=22+25)
AppendFloat64Fixed1-8         97.8ns ± 0%   98.6ns ± 3%     ~     (p=0.711 n=20+25)
AppendFloat64Fixed2-8          110ns ± 3%    110ns ± 5%   -0.45%  (p=0.037 n=24+24)
AppendFloat64Fixed3-8          102ns ± 3%    102ns ± 3%     ~     (p=0.684 n=24+24)
AppendFloat64Fixed4-8          112ns ± 3%    110ns ± 0%   -1.43%  (p=0.000 n=25+18)
FormatInt-8                   3.18µs ± 4%   3.10µs ± 6%   -2.54%  (p=0.001 n=24+25)
AppendInt-8                   1.81µs ± 5%   1.80µs ± 5%     ~     (p=0.648 n=25+25)
FormatUint-8                   812ns ± 6%    816ns ± 6%     ~     (p=0.777 n=25+25)
AppendUint-8                   536ns ± 4%    538ns ± 3%     ~     (p=0.798 n=20+22)
Quote-8                        605ns ± 6%    602ns ± 9%     ~     (p=0.573 n=25+25)
QuoteRune-8                   99.5ns ± 8%  100.2ns ± 7%     ~     (p=0.432 n=25+25)
AppendQuote-8                  361ns ± 3%    363ns ± 4%     ~     (p=0.085 n=25+25)
AppendQuoteRune-8             23.3ns ± 3%   22.4ns ± 2%   -3.79%  (p=0.000 n=25+24)
UnquoteEasy-8                  146ns ± 4%    145ns ± 5%     ~     (p=0.112 n=24+24)
UnquoteHard-8                  804ns ± 6%    771ns ± 6%   -4.10%  (p=0.000 n=25+24)

Change-Id: Ibd384e46e90f1cfa40503c8c6352a54c65b72980
Reviewed-on: https://go-review.googlesource.com/27652
Run-TryBot: Josh Bleecher Snyder <josharian@gmail.com>
Reviewed-by: Matthew Dempsky <mdempsky@google.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
@quentinmit quentinmit added the NeedsFix The path to resolution is known, but the work has not been done. label Oct 11, 2016
@rsc rsc modified the milestones: Go1.9, Go1.8 Oct 21, 2016
@randall77 randall77 modified the milestones: Go1.10, Go1.9 May 31, 2017
@bradfitz bradfitz modified the milestones: Go1.10, Go1.11 Nov 28, 2017
@bradfitz bradfitz modified the milestones: Go1.11, Unplanned Jun 19, 2018
@zdjones
Copy link
Contributor

zdjones commented Jul 19, 2019

@josharian Can we close this issue?
Prove has changed since then, but still never reaches the bounds check on line 18 because it's dead code. Prove knows that the conditional on line 17 can't be true, so it prunes the if block without looking inside it.

f.go:5:11: Proved IsInBounds (v20)
f.go:8:11: Proved IsInBounds (v41)
f.go:15:11: Proved IsInBounds (v17)
f.go:17:2: Disproved Less64 (v32)

I don't think there is an issue here to fix, unless we want to optimize dead code before we remove it.

@golang golang locked and limited conversation to collaborators Jul 18, 2020
@rsc rsc unassigned brtzsnr Jun 23, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
FrozenDueToAge NeedsFix The path to resolution is known, but the work has not been done. Performance
Projects
None yet
Milestone
Unplanned
Development

No branches or pull requests
8 participants
@bradfitz @brtzsnr @josharian @rsc @quentinmit @zdjones @randall77 @gopherbot