• 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
prove.go 33 KB