effects: Do not over-taint :terminates in abstract cycle

[topolarity]

The idea here is to propagate non-termination-by-recursion through the Effects system naturally rather than eagerly marking all callers in a cycle as non-terminating.

Doing this is important to avoid tainting non-termination from purely abstract cycles, where inference is forced to analyze methods that do not correspond to real calls at runtime, such as _return_type

Resolves #48983.

[vtjnash]

I don't think this premise is true. This proves the absences of recursion in the type graph, but that only implies that the type information is not required to be propagated, not that their is a cycle-free call graph.

[vtjnash]

In fact, it seems the existing code is marking this property much too late, as the cycle detection occurs (and is discarded) as early as line 564 in this file.

[Keno]

The cycle-detection-with-unused-result on 564 is separate and taints all effects (#48981)

[Keno]

I think the general argument goes something like this:
In order to have a runtime non-termination you need to either:

1. Hit an unknown callsite where inference gives up
2. Hit the same method instance so inference declares a cycle (but knows nothing about the runtime behavior)
3. Have a loop
4. Have inference not terminate either

Can you think of another case where inference does terminate, but none of these four conditions are true?

[vtjnash]

5. be called from a method that declares a cycle is hit? I think it is true that all methods in a cycle are non-terminating (regardless of the entry point), and not just the first one.

[Keno]

Right, but presumably as soon as one callsite in a cycle of methods is marked as non-terminating, that should just propagate by the usual rules of effect-propagation, no?

[vtjnash]

Ah, right. Either the call should return and be finished, or it should report a cycle. And in particular, we can even have cycles in the inference types graph, without have cycles in the call graph (because of the behavior of the return_type function)

[Keno]

Yes

[aviatesk]

I agree with deleting the too conservative tainting mechanism within typeinf.jl while keeping the tainting within abstract_call_method as is. And it might be better to conservatively add more tainting mechanisms within abstract_call_method_with_const_args too?

• julia/base/compiler/abstractinterpretation.jl

  Line 1007 in 124abaa

  add_remark!(interp, sv, "[constprop] Edge cycle encountered")

• julia/base/compiler/abstractinterpretation.jl

  Line 1023 in 124abaa

  add_remark!(interp, sv, "[constprop] Fresh constant inference hit a cycle")

[topolarity]

I agree with deleting the too conservative tainting mechanism within typeinf.jl while keeping the tainting within abstract_call_method as is.

Agreed! Just trying to put together a test case now for the gap in my original logic.

And it might be better to conservatively add more tainting mechanisms within abstract_call_method_with_const_args too?

If I understand correctly, the effects observed by abstract_call_method_with_const_args should always be a refinement of the effects observed by abstract_call_method (i.e. even if it discovers new cycles, it should not discover new non-termination)

Since we're already returning nothing instead of any Effects information in these cases, I think it might be enough to just abandon the result as we do now. What do you think?

[topolarity]

Agreed! Just trying to put together a test case now for the gap in my original logic.

I think the original logic is actually sound

This extra tainting makes it difficult for me to come up with a test case that would evade it:

julia/base/compiler/abstractinterpretation.jl

Lines 562 to 569 in 124abaa

	if call_result_unused(si)
	add_remark!(interp, sv, RECURSION_UNUSED_MSG)
	# since we don't use the result (typically),
	# we have a self-cycle in the call-graph, but not in the inference graph (typically):
	# break this edge now (before we record it) by returning early
	# (non-typically, this means that we lose the ability to detect a guaranteed StackOverflow in some cases)
	return MethodCallResult(Any, true, true, nothing, Effects())
	end

but either way I'm fine with doing this tainting in abstract_call_method

[aviatesk]

If I understand correctly, the effects observed by abstract_call_method_with_const_args should always be a refinement of the effects observed by abstract_call_method (i.e. even if it discovers new cycles, it should not discover new non-termination)

Since we're already returning nothing instead of any Effects information in these cases, I think it might be enough to just abandon the result as we do now. What do you think?

Yes, the main reason why I'm suggesting it is because it's generally safe to be conservative.

I intended to taint the parent frame sv there rather than returning some effects representing effects of a callee call with their :terminate tainted. So adding something like this there:

if !(is_effect_overridden(sv, :terminates_globally) ||         # this frame is known to terminate
     is_effect_overridden(match.method, :terminates_globally)) # this edge is known to terminate
    # `abstract_call_method` may have returned this callee's effects with their `:terminates`
    # tainted already, but let's make sure to taint it here conservatively
    merge_effects!(interp, sv, Effects(EFFECTS_TOTAL; terminates=true))
end

This would be safe because while we usually expect our analysis to be monotonic, i.e. results from constprop' absint is more accurate that results from ordinary absint in terms of both type and effects domain, this assumption may not always hold true. In some cases const prop' may sometimes discovr out new cycles that were not detected by abstract_call_method. In such cases (I'm not sure if it ever happens though) it would be better to taint :terminate here conservatively.
Having said that, it is worth noting that such cases are pretty rare, and in most cases, I guess abstract_call_method should almost always have returned effects with their :terminates tainted when we hit these conditions in abstract_call_method_with_const_args. So you can leave this for future if you prefer not to be overly conservative in this PR.

[topolarity]

In some cases const prop' may sometimes discovr out new cycles that were not detected by abstract_call_method. In such cases (I'm not sure if it ever happens though) it would be better to taint :terminate here conservatively.

Yeah, I see what you're saying. At the same time, my devil's advocate position would be that conservatively tainting in anticipation of a bug elsewhere in the code just makes that bug harder to find later, especially since the conservative solution here would be an incomplete band-aid.

If abstract_call_method fails to discover a cycle / report non-termination correctly, we definitely can't count on abstract_call_method_with_const_args to do it correctly for us in general, right?

If that reasoning stands, my preference would be to leave out the extra tainting in _with_const_args, but I'm happy to defer to others if there's a strong intuition from more experienced folks than myself

[aviatesk]

If abstract_call_method fails to discover a cycle / report non-termination correctly, we definitely can't count on abstract_call_method_with_const_args to do it correctly for us in general, right?

Yeah, you're right. I remember we encountered some cases when with_const_args derives less accurate type information than abstract_call_method, but it's probably better to try to make it discover cycles correctly at least.

[vtjnash]

If I understand correctly, the effects observed by abstract_call_method_with_const_args should always be a refinement of the effects observed by abstract_call_method (i.e. even if it discovers new cycles, it should not discover new non-termination)

This is correct. The result of inference between these 2 calls is the intersection of their results. Thus if either can show that it terminates, then it terminates, even if the other one couldn't prove that.