[red-knot] [WIP] Combine terminal statement support with statically known branches

[dcreager]

This example from @sharkdp shows how terminal statements can appear in statically known branches: #15676 (comment)

def _(cond: bool):
    x = "a"
    if cond:
        x = "b"
        if True:
            return

    reveal_type(x)  # revealed: "a", "b"; should be "a"

We currently don't handle that correctly, since we don't apply the True visibility constraint to the reachability flag that we set when we encounter a terminal statement.

Work in progress

[dcreager]

This is not currently working because of visibility constraint simplification:

def _(cond: bool):
    x = "a"
    if cond:
        x = "b"
        # ← {0}
        if True:
            return
            # ← {1}
        # ← {2}

    reveal_type(x)  # revealed: Literal["a"]

At point {1}, we're marking the x = "b" binding as non-visible (by setting a visibility constraint of ALWAYS_FALSE).

But at point {2}, after we merge the two flows back together (the then flow and the artifically inserted else flow), we simplify the result relative to point {0}. That sees that there weren't any new bindings of x, and resets the visibility of x = "b" back to what it was at point {0}, forgetting the unreachability that we just introduced.

So I think I need to skip the simplification step when a flow contains a terminal statement.

[dcreager]

At first I replaced this with reachability: ScopedVisibilityConstraintId, but I realized that scope_start_visibility is already what we need: the start of the scope is visible iff the flow is still reachable.

[dcreager]

Commenting out these two if clauses is how we verify that this is truly an optimization — we should get the same results for the tests with and without it

[carljm]

So I think I need to skip the simplification step when a flow contains a terminal statement.

This sounds right. The simplification step is a bit of a performance hack. I think it could be eliminated if we used BDDs instead of syntax trees to represent visibility constraints (since BDDs self-simplify). But I think it should never be wrong to skip the simplification, just potentially hurt performance. Which in this case shouldn't be too bad, since it would only occur when there's a terminal statement in the branch, which won't be the common case.

[codspeed-hq]

CodSpeed Performance Report

Merging #15817 will degrade performances by 14.12%

_{Comparing dcreager/static-terminal (0f278da) with main (4f2aea8)}

Summary

❌ 2 regressions
✅ 30 untouched benchmarks

⚠️ Please fix the performance issues or acknowledge them on CodSpeed.

Benchmarks breakdown

	Benchmark	BASE	HEAD	Change
❌	red_knot_check_file[cold]	89.4 ms	95.2 ms	-6.07%
❌	red_knot_check_file[incremental]	4.7 ms	5.5 ms	-14.12%