Skip to content

Commit

Permalink
effects: make :terminates_globally functional on recursive functions (
Browse files Browse the repository at this point in the history
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
```
  • Loading branch information
aviatesk authored and LilithHafner committed Mar 8, 2022
1 parent 245fd29 commit 9d8e971
Show file tree
Hide file tree
Showing 2 changed files with 41 additions and 12 deletions.
35 changes: 23 additions & 12 deletions base/compiler/abstractinterpretation.jl
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ function abstract_call_gf_by_type(interp::AbstractInterpreter, @nospecialize(f),
const_result = abstract_call_method_with_const_args(interp, result, f, this_arginfo, match, sv)
effects = result.edge_effects
if const_result !== nothing
(;rt, effects, const_result) = const_result
(; rt, effects, const_result) = const_result
end
tristate_merge!(sv, effects)
push!(const_results, const_result)
Expand Down Expand Up @@ -589,15 +589,27 @@ function abstract_call_method(interp::AbstractInterpreter, method::Method, @nosp
if edge === nothing
edgecycle = edgelimited = true
end
if edgecycle
if is_effect_overrided(sv, :terminates_globally)
# this frame is known to terminate
edge_effects = Effects(edge_effects, terminates=ALWAYS_TRUE)
elseif is_effect_overrided(method, :terminates_globally)
# this edge is known to terminate
edge_effects = Effects(edge_effects, terminates=ALWAYS_TRUE)
elseif edgecycle
# Some sort of recursion was detected. Even if we did not limit types,
# we cannot guarantee that the call will terminate.
edge_effects = tristate_merge(edge_effects,
Effects(EFFECTS_TOTAL, terminates=TRISTATE_UNKNOWN))
# we cannot guarantee that the call will terminate
edge_effects = Effects(edge_effects, terminates=TRISTATE_UNKNOWN)
end
return MethodCallResult(rt, edgecycle, edgelimited, edge, edge_effects)
end

is_effect_overrided(sv::InferenceState, effect::Symbol) = is_effect_overrided(sv.linfo, effect)
function is_effect_overrided(linfo::MethodInstance, effect::Symbol)
def = linfo.def
return isa(def, Method) && is_effect_overrided(def, effect)
end
is_effect_overrided(method::Method, effect::Symbol) = getfield(decode_effects_override(method.purity), effect)

# keeps result and context information of abstract method call, will be used by succeeding constant-propagation
struct MethodCallResult
rt
Expand Down Expand Up @@ -2067,14 +2079,13 @@ end

function handle_control_backedge!(frame::InferenceState, from::Int, to::Int)
if from > to
def = frame.linfo.def
if isa(def, Method)
effects = decode_effects_override(def.purity)
if effects.terminates_globally || effects.terminates_locally
return nothing
end
if is_effect_overrided(frame, :terminates_globally)
# this frame is known to terminate
elseif is_effect_overrided(frame, :terminates_locally)
# this backedge is known to terminate
else
tristate_merge!(frame, Effects(EFFECTS_TOTAL, terminates=TRISTATE_UNKNOWN))
end
tristate_merge!(frame, Effects(EFFECTS_TOTAL, terminates=TRISTATE_UNKNOWN))
end
return nothing
end
Expand Down
18 changes: 18 additions & 0 deletions test/compiler/inline.jl
Original file line number Diff line number Diff line change
Expand Up @@ -1070,6 +1070,24 @@ end
issue41694(2)
end

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_termination21(x)
x == 1 && return 1
1 < x < 20 || throw("bad")
return recur_termination22(x)
end
recur_termination22(x) = x * recur_termination21(x-1)
@test fully_eliminated() do
recur_termination21(12) + recur_termination22(12)
end

global x44200::Int = 0
function f44200()
global x = 0
Expand Down

0 comments on commit 9d8e971

Please sign in to comment.