effects: make :terminates_globally functional on recursive functions
#44210
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
aviatesk
force-pushed
the
avi/recureffects
branch
from
2d8290e to
8e44096
Compare
Keno
reviewed
Feb 16, 2022
| if edge === nothing | ||
| edgecycle = edgelimited = true | ||
| end | ||
| if edgecycle |
There was a problem hiding this comment.
There's also the code that deals with frame cycles in merge_call_chain!, which will need similar treatment.
aviatesk
force-pushed
the
avi/recureffects
branch
from
8e44096 to
651476b
Compare
aviatesk
commented
Feb 17, 2022
base/compiler/typeinfer.jl
Outdated
Comment on lines
730
to
746
| tristate_merge!(parent, Effects(EFFECTS_TOTAL, terminates=TRISTATE_UNKNOWN)) | ||
| terminates_globally = is_effect_overrided(parent, :terminates_globally) | ||
| frames = InferenceState[parent] | ||
| while true | ||
| add_cycle_backedge!(child, parent, parent.currpc) | ||
| union_caller_cycle!(ancestor, child) | ||
| tristate_merge!(child, Effects(EFFECTS_TOTAL, terminates=TRISTATE_UNKNOWN)) | ||
| terminates_globally |= is_effect_overrided(child, :terminates_globally) | ||
| push!(frames, child) | ||
| child = parent | ||
| child === ancestor && break | ||
| parent = child.parent::InferenceState | ||
| end | ||
| if !terminates_globally | ||
| for frame in frames | ||
| tristate_merge!(frame, Effects(EFFECTS_TOTAL, terminates=TRISTATE_UNKNOWN)) | ||
| end | ||
| end | ||
| return nothing |
There was a problem hiding this comment.
With this change, terminates is encoded into ipo_effect_bits of :terminates_globally-functions no matter if they are involved with cycles.
I think it is valid to skip tainting frames in a cycle as long as any of them is annotated as :terminates_globally, but I would like to check my understanding with your review, @Keno .
There was a problem hiding this comment.
you could write malicious functions that violate that, but I don't know if that is the intention of the annotation
f(x) = while x; g(); end
@assume_effects :terminates_globally g() = f(false)There was a problem hiding this comment.
Ah, that's a good example, thanks.
So "termination" implied by :terminates_globally annotation subsumes constant-prop', but merge_call_chain! isn't a good place to handle it. Maybe we just want to just override edge effects in abstract_call_method when the edge effect is specified by annotation, rather than trying hard to figure out the appropriate ipo_purity_bitss for frames in a cycle.
As with loop, it's hard to prove termination of recursive call automatically.
But with this commit we can manually specify termination at least.
```julia
Base.@assume_effects :terminates_globally function recur_termination1(x)
x == 1 && return 1
1 < x < 20 || throw("bad")
return x * recur_termination1(x-1)
end
@test fully_eliminated() do
recur_termination1(12)
end
Base.@assume_effects :terminates_globally function recur_termination2(x)
x == 1 && return 1
1 < x < 20 || throw("bad")
return _recur_termination2(x)
end
_recur_termination2(x) = x * recur_termination2(x-1)
@test fully_eliminated() do
recur_termination2(12)
end
```
aviatesk
force-pushed
the
avi/recureffects
branch
from
651476b to
127a8ba
Compare
aviatesk
added a commit
that referenced
this pull request
Feb 20, 2022
#44210) As with loop, it's hard to prove termination of recursive call automatically. But with this commit we can manually specify termination at least. ```julia Base.@assume_effects :terminates_globally function recur_termination1(x) x == 1 && return 1 1 < x < 20 || throw("bad") return x * recur_termination1(x-1) end @test fully_eliminated() do recur_termination1(12) end Base.@assume_effects :terminates_globally function recur_termination2(x) x == 1 && return 1 1 < x < 20 || throw("bad") return _recur_termination2(x) end _recur_termination2(x) = x * recur_termination2(x-1) @test fully_eliminated() do recur_termination2(12) end ```
33 tasks
staticfloat
pushed a commit
to JuliaCI/julia-buildkite-testing
that referenced
this pull request
Mar 2, 2022
JuliaLang#44210) As with loop, it's hard to prove termination of recursive call automatically. But with this commit we can manually specify termination at least. ```julia Base.@assume_effects :terminates_globally function recur_termination1(x) x == 1 && return 1 1 < x < 20 || throw("bad") return x * recur_termination1(x-1) end @test fully_eliminated() do recur_termination1(12) end Base.@assume_effects :terminates_globally function recur_termination2(x) x == 1 && return 1 1 < x < 20 || throw("bad") return _recur_termination2(x) end _recur_termination2(x) = x * recur_termination2(x-1) @test fully_eliminated() do recur_termination2(12) end ```
LilithHafner
pushed a commit
to LilithHafner/julia
that referenced
this pull request
Mar 8, 2022
JuliaLang#44210) As with loop, it's hard to prove termination of recursive call automatically. But with this commit we can manually specify termination at least. ```julia Base.@assume_effects :terminates_globally function recur_termination1(x) x == 1 && return 1 1 < x < 20 || throw("bad") return x * recur_termination1(x-1) end @test fully_eliminated() do recur_termination1(12) end Base.@assume_effects :terminates_globally function recur_termination2(x) x == 1 && return 1 1 < x < 20 || throw("bad") return _recur_termination2(x) end _recur_termination2(x) = x * recur_termination2(x-1) @test fully_eliminated() do recur_termination2(12) end ```
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
As with loop, it's hard to prove termination of recursive call automatically.
But with this commit we can manually specify termination at least.