Skip to content

Commit

Permalink
effects: make :terminates_globally functional on recursive functions
Browse files Browse the repository at this point in the history
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 committed Feb 19, 2022
1 parent f5d9b86 commit 127a8ba
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 127a8ba

Please sign in to comment.