…tions for unsigned domain
Fence-post implications of the form "x-1 >= w && x > min ⇒ x > w"
were not correctly handling unsigned domain, by always checking signed
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.
Reviewed-by: Keith Randall <email@example.com>
(cherry picked from commit 09ea3c0)
Reviewed-by: Austin Clements <firstname.lastname@example.org>
Run-TryBot: Austin Clements <email@example.com>
TryBot-Result: Gobot Gobot <firstname.lastname@example.org>