From 8e44096711665eeca5cda2b8135326ddc0e6d442 Mon Sep 17 00:00:00 2001
From: Shuhei Kadowaki <aviatesk@gmail.com>
Date: Thu, 17 Feb 2022 01:00:34 +0900
Subject: [PATCH] effects: make `:terminates_globally` functional on recursive
 functions

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
```
---
 base/compiler/abstractinterpretation.jl | 15 ++++++++++++---
 test/compiler/inline.jl                 | 18 ++++++++++++++++++
 2 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/base/compiler/abstractinterpretation.jl b/base/compiler/abstractinterpretation.jl
index 6a9837547834b..68e9f5f6a4a66 100644
--- a/base/compiler/abstractinterpretation.jl
+++ b/base/compiler/abstractinterpretation.jl
@@ -596,9 +596,18 @@ function abstract_call_method(interp::AbstractInterpreter, method::Method, @nosp
     end
     if 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, unless specified explicitly
+        if decode_effects_override(method.purity).terminates_globally
+            terminates_override = ALWAYS_TRUE
+        else
+            def = sv.linfo.def
+            if isa(def, Method) && decode_effects_override(def.purity).terminates_globally
+                terminates_override = ALWAYS_TRUE
+            else
+                terminates_override = TRISTATE_UNKNOWN
+            end
+        end
+        edge_effects = Effects(edge_effects, terminates = terminates_override)
     end
     return MethodCallResult(rt, edgecycle, edgelimited, edge, edge_effects)
 end
diff --git a/test/compiler/inline.jl b/test/compiler/inline.jl
index 9347acc83f13f..34fcc3c3b3614 100644
--- a/test/compiler/inline.jl
+++ b/test/compiler/inline.jl
@@ -1069,3 +1069,21 @@ end
 @test fully_eliminated() do
     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