• Giovanni Bajo's avatar
    cmd/compile: in prove, fix fence-post implications for unsigned domain · 09ea3c08
    Giovanni Bajo authored
    Fence-post implications of the form "x-1 >= w && x > min ⇒ x > w"
    were not correctly handling unsigned domain, by always checking signed
    limits.
    
    This bug was uncovered once we taught prove that len(x) is always
    >= 0 in the signed domain.
    
    In the code being miscompiled (s[len(s)-1]), prove checks
    whether len(s)-1 >= len(s) in the unsigned domain; if it proves
    that this is always false, it can remove the bound check.
    
    Notice that len(s)-1 >= len(s) can be true for len(s) = 0 because
    of the wrap-around, so this is something prove should not be
    able to deduce.
    
    But because of the bug, the gate condition for the fence-post
    implication was len(s) > MinInt64 instead of len(s) > 0; that
    condition would be good in the signed domain but not in the
    unsigned domain. And since in CL105635 we taught prove that
    len(s) >= 0, the condition incorrectly triggered
    (len(s) >= 0 > MinInt64) and things were going downfall.
    
    Fixes #27251
    Fixes #27289
    
    Change-Id: I3dbcb1955ac5a66a0dcbee500f41e8d219409be5
    Reviewed-on: https://go-review.googlesource.com/132495Reviewed-by: 's avatarKeith Randall <khr@golang.org>
    09ea3c08
Name
Last commit
Last update
..
amd64 Loading commit data...
arm Loading commit data...
arm64 Loading commit data...
gc Loading commit data...
mips Loading commit data...
mips64 Loading commit data...
ppc64 Loading commit data...
s390x Loading commit data...
ssa Loading commit data...
syntax Loading commit data...
test Loading commit data...
types Loading commit data...
wasm Loading commit data...
x86 Loading commit data...