/ go Public

# cmd/compile: prove pass doesn't draw signed int conclusions from range checks#25115

Open
opened this issue Apr 26, 2018 · 5 comments
Open

# cmd/compile: prove pass doesn't draw signed int conclusions from range checks #25115

opened this issue Apr 26, 2018 · 5 comments
Labels
compiler/runtime Issues related to the Go compiler and/or runtime. Performance
Milestone

### josharian commented Apr 26, 2018

 This might be fixed by outstanding prove CLs, but just in case, consider this snippet from math/expm1.go: ``` var k int // ... switch { case k == -1: return 0.5*(x-e) - 0.5 case k == 1: if x < -0.25 { return -2 * (e - (x + 0.5)) } return 1 + 2*(x-e) case k <= -2 || k > 56: // suffice to return exp(x)-1 y := 1 - (e - x) y = Float64frombits(Float64bits(y) + uint64(k)<<52) // add k to y's exponent return y - 1 } if k < 20 { t := Float64frombits(0x3ff0000000000000 - (0x20000000000000 >> uint(k))) // t=1-2**-k y := t - (e - x) y = Float64frombits(Float64bits(y) + uint64(k)<<52) // add k to y's exponent return y }``` Note the switch case `k <= -2 || k > 56`. The compiler rewrites this into a single unsigned comparison: `uint(x) > 57`. See `func walkinrange` in walk.go. After the `k < 20` check (in particular, when considering `uint64(k)<<52`, the prove pass has signed limits of [-9223372036854775808, 19] for k and no unsigned limits. But I believe that we should know that k is in [-2, 19]. I might have the culprit/analysis wrong...but in any case, we should know more about `uint64(k)` here. Noticed while exploring #25087. cc @rasky The text was updated successfully, but these errors were encountered:
added this to the Unplanned milestone Apr 26, 2018
mentioned this issue Apr 26, 2018
modified the milestones: Unplanned, Go1.13 Dec 12, 2018

### josharian commented Jun 3, 2019

 @zdjones does your outstanding CL fix this issue as well?

### josharian commented Jun 3, 2019

 Punting to 1.14 in any case.

modified the milestones: Go1.13, Go1.14 Jun 3, 2019

 Other prove changes since last year have updated this. It appears the signed limits are correct now. I think we can close this? After the `k < 20`, on the `true` branch, prove currently learns limits for `k` as signed: `[-1,19]` and unsigned: `[2,18446744073709551614]` (not sure the unsigned is correct, haven't looked into). After branching into the `k < 20` path, there are no more branches, so prove learns no new facts on that path before returning on line 230. I've included some extended debugging output below to show where this is from. The first column is the line number in math/expm1.go. `V168` is `k (int)` and `v266` is `20 (int constant)`. ``````// b73 is the first of the SSA blocks within the k < 20 "Block" 227 Checkpoint: b73 DFS Descending, idom:b56 ... 226 parent=b56, update v168 v266 signed < 226 parent=b56, new limits v168 v266 signed < sm,SM,um,UM=-1,19,2,18446744073709551614 229 Checkpoint: b74 DFS Descending, idom:b73 229 Checkpoint: b75 DFS Descending, idom:b74 // b76 is SSA block where the the k < 20 "Block" returns. 230 Checkpoint: b76 DFS Descending, idom:b75 // This is prove walking back up the dominator tree, undoing learned facts that are no longer live. 230 Restore: b76 DFS Descending(simplify) ``````

### josharian commented Jul 26, 2019

 I suspect this is “fixed” because the walkinrange optimization is broken. #30645

### zdjones commented Jul 26, 2019

 Ha. I'll keep it on my radar until the walkinrange gets fixed, then I'll take another look.

modified the milestones: Go1.14, Backlog Oct 9, 2019
added the compiler/runtime Issues related to the Go compiler and/or runtime. label Jul 13, 2022