Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

effects: make :terminates_globally functional on recursive functions #44210

Merged
merged 1 commit into from
Feb 20, 2022
Merged

effects: make :terminates_globally functional on recursive functions #44210

merged 1 commit into from
Feb 20, 2022

Conversation

aviatesk
Copy link
Member

As with loop, it's hard to prove termination of recursive call automatically.
But with this commit we can manually specify termination at least.

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 aviatesk requested a review from Keno February 16, 2022 16:01
Keno
Keno reviewed Feb 16, 2022
View reviewed changes
base/compiler/abstractinterpretation.jl Outdated
@@ -596,9 +596,18 @@ function abstract_call_method(interp::AbstractInterpreter, method::Method, @nosp
end
if edgecycle
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's also the code that deals with frame cycles in merge_call_chain!, which will need similar treatment.

Keno
Keno approved these changes Feb 16, 2022
View reviewed changes
Copy link
Member

@Keno Keno left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems fine conceptually.

aviatesk
aviatesk commented Feb 17, 2022
View reviewed changes
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
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 .

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@aviatesk
effects: make :terminates_globally functional on recursive functions
127a8ba 
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 aviatesk merged commit 2816a6f into master Feb 20, 2022
@aviatesk aviatesk deleted the avi/recureffects branch February 20, 2022 04:17
@aviatesk aviatesk added the backport 1.8 Change should be backported to release-1.8 label Feb 20, 2022
aviatesk added a commit that referenced this pull request Feb 20, 2022
@aviatesk
effects: make :terminates_globally functional on recursive functions (
e84a9de 
#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
```
@aviatesk aviatesk mentioned this pull request Feb 20, 2022
Merged
33 tasks
@KristofferC KristofferC removed the backport 1.8 Change should be backported to release-1.8 label Feb 24, 2022
staticfloat pushed a commit to JuliaCI/julia-buildkite-testing that referenced this pull request Mar 2, 2022
@aviatesk @staticfloat
effects: make :terminates_globally functional on recursive functions (
63717d9 
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
@aviatesk @LilithHafner
effects: make :terminates_globally functional on recursive functions (
9d8e971 
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
Reviewers

@vtjnash vtjnash vtjnash left review comments

@Keno Keno Keno approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@aviatesk @vtjnash @Keno @KristofferC