FA-43036 / Borrow checking / Open access

Branch liveness loses references demanded only on its second successor · case 01

Branch liveness loses references demanded only on its second successor.

Verified by executionVariant 1 · 13 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

The static analyzer mishandles successor union: branch liveness loses references demanded only on its second successor.

VERIFIED REPAIR

Apply the specified transfer or inference rule at this site: elif op=='branch': live.update(set(a)|set(b)).

Unsuccessful approach: The partial repair uses elif op=='branch': live.update(a), which still violates the stipulated analysis contract.

Case contract

Backward reference-demand transfer over a finite straight-line IR. ops execute forward and analysis traverses backward. use/return demand one reference; call demands all actual references. def and storage_dead kill a local. assign(d,s) propagates demand from destination to source, killing destination. reborrow(d,p) kills child demand and adds parent unconditionally because construction reads parent. phi(d,sources) propagates destination demand to every source. drop(ref,needs_drop) demands only when destructor can observe referent. branch supplies two already-computed successor demand sets, both unioned. Return sorted entry-demand names.

Why this case matters

A finite offline static-analysis model of ownership and borrowing; it does not execute the analyzed program.

1 / The failure

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(ops):
    live=set()
    for op,a,b in reversed(ops):
        if op=='use': live.add(a)
        elif op=='return': live.add(a)
        elif op=='call': live.update(a)
        elif op=='def': live.discard(a)
        elif op=='storage_dead': live.discard(a)
        elif op=='assign':
            needed=a in live; live.discard(a)
            if needed: live.add(b)
        elif op=='reborrow':
            live.discard(a); live.add(b)
        elif op=='phi':
            needed=a in live; live.discard(a)
            if needed: live.update(b)
        elif op=='drop':
            if b: live.add(a)
        elif op=='branch': live.update(set(a)&set(b))
    return sorted(live)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='r'+str(N)
check('empty',solve([]),[])
check('use',solve([('use',x,None)]),[x])
check('return',solve([('return',x,None)]),[x])
check('call',solve([('call',['a',x],None)]),['a',x])
check('definition',solve([('def','a',None),('use','a',None),('use',x,None)]),[x])
check('dead boundary',solve([('storage_dead','a',None),('use','a',None)]),[])
check('assign demanded',solve([('assign','a',x),('use','a',None)]),[x])
check('reborrow constructor',solve([('reborrow','a',x),('use','a',None)]),[x])
check('phi second origin',solve([('phi','a',['b',x]),('use','a',None)]),['b',x])
check('trivial drop',solve([('drop',x,False)]),[])
check('observing drop',solve([('drop',x,True)]),[x])
check('branch union',solve([('branch',['a'],[x])]),['a',x])
check('variable arity',solve([('call',list(range(N+1)),None)]),list(range(N+1)))
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
empty	`[]`	`[]`	Passed
use	`['r1']`	`['r1']`	Passed
return	`['r1']`	`['r1']`	Passed
call	`['a', 'r1']`	`['a', 'r1']`	Passed
definition	`['r1']`	`['r1']`	Passed
dead boundary	`[]`	`[]`	Passed
assign demanded	`['r1']`	`['r1']`	Passed
reborrow constructor	`['r1']`	`['r1']`	Passed
phi second origin	`['b', 'r1']`	`['b', 'r1']`	Passed
trivial drop	`[]`	`[]`	Passed
observing drop	`['r1']`	`['r1']`	Passed
branch union	`[]`	`['a', 'r1']`	Failed
variable arity	`[0, 1]`	`[0, 1]`	Passed

SHA-256 / 7615684f92a04469ae20b24746b256b22641351baecdadf885bc32f4b2618bf9

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(ops):
    live=set()
    for op,a,b in reversed(ops):
        if op=='use': live.add(a)
        elif op=='return': live.add(a)
        elif op=='call': live.update(a)
        elif op=='def': live.discard(a)
        elif op=='storage_dead': live.discard(a)
        elif op=='assign':
            needed=a in live; live.discard(a)
            if needed: live.add(b)
        elif op=='reborrow':
            live.discard(a); live.add(b)
        elif op=='phi':
            needed=a in live; live.discard(a)
            if needed: live.update(b)
        elif op=='drop':
            if b: live.add(a)
        elif op=='branch': live.update(a)
    return sorted(live)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='r'+str(N)
check('empty',solve([]),[])
check('use',solve([('use',x,None)]),[x])
check('return',solve([('return',x,None)]),[x])
check('call',solve([('call',['a',x],None)]),['a',x])
check('definition',solve([('def','a',None),('use','a',None),('use',x,None)]),[x])
check('dead boundary',solve([('storage_dead','a',None),('use','a',None)]),[])
check('assign demanded',solve([('assign','a',x),('use','a',None)]),[x])
check('reborrow constructor',solve([('reborrow','a',x),('use','a',None)]),[x])
check('phi second origin',solve([('phi','a',['b',x]),('use','a',None)]),['b',x])
check('trivial drop',solve([('drop',x,False)]),[])
check('observing drop',solve([('drop',x,True)]),[x])
check('branch union',solve([('branch',['a'],[x])]),['a',x])
check('variable arity',solve([('call',list(range(N+1)),None)]),list(range(N+1)))
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
empty	`[]`	`[]`	Passed
use	`['r1']`	`['r1']`	Passed
return	`['r1']`	`['r1']`	Passed
call	`['a', 'r1']`	`['a', 'r1']`	Passed
definition	`['r1']`	`['r1']`	Passed
dead boundary	`[]`	`[]`	Passed
assign demanded	`['r1']`	`['r1']`	Passed
reborrow constructor	`['r1']`	`['r1']`	Passed
phi second origin	`['b', 'r1']`	`['b', 'r1']`	Passed
trivial drop	`[]`	`[]`	Passed
observing drop	`['r1']`	`['r1']`	Passed
branch union	`['a']`	`['a', 'r1']`	Failed
variable arity	`[0, 1]`	`[0, 1]`	Passed

SHA-256 / cb33a101bec7017ed3ed7a475340f37429dd8cf66396a4f472aaaf55f19f15ed

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(ops):
    live=set()
    for op,a,b in reversed(ops):
        if op=='use': live.add(a)
        elif op=='return': live.add(a)
        elif op=='call': live.update(a)
        elif op=='def': live.discard(a)
        elif op=='storage_dead': live.discard(a)
        elif op=='assign':
            needed=a in live; live.discard(a)
            if needed: live.add(b)
        elif op=='reborrow':
            live.discard(a); live.add(b)
        elif op=='phi':
            needed=a in live; live.discard(a)
            if needed: live.update(b)
        elif op=='drop':
            if b: live.add(a)
        elif op=='branch': live.update(set(a)|set(b))
    return sorted(live)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='r'+str(N)
check('empty',solve([]),[])
check('use',solve([('use',x,None)]),[x])
check('return',solve([('return',x,None)]),[x])
check('call',solve([('call',['a',x],None)]),['a',x])
check('definition',solve([('def','a',None),('use','a',None),('use',x,None)]),[x])
check('dead boundary',solve([('storage_dead','a',None),('use','a',None)]),[])
check('assign demanded',solve([('assign','a',x),('use','a',None)]),[x])
check('reborrow constructor',solve([('reborrow','a',x),('use','a',None)]),[x])
check('phi second origin',solve([('phi','a',['b',x]),('use','a',None)]),['b',x])
check('trivial drop',solve([('drop',x,False)]),[])
check('observing drop',solve([('drop',x,True)]),[x])
check('branch union',solve([('branch',['a'],[x])]),['a',x])
check('variable arity',solve([('call',list(range(N+1)),None)]),list(range(N+1)))
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
empty	`[]`	`[]`	Passed
use	`['r1']`	`['r1']`	Passed
return	`['r1']`	`['r1']`	Passed
call	`['a', 'r1']`	`['a', 'r1']`	Passed
definition	`['r1']`	`['r1']`	Passed
dead boundary	`[]`	`[]`	Passed
assign demanded	`['r1']`	`['r1']`	Passed
reborrow constructor	`['r1']`	`['r1']`	Passed
phi second origin	`['b', 'r1']`	`['b', 'r1']`	Passed
trivial drop	`[]`	`[]`	Passed
observing drop	`['r1']`	`['r1']`	Passed
branch union	`['a', 'r1']`	`['a', 'r1']`	Passed
variable arity	`[0, 1]`	`[0, 1]`	Passed

SHA-256 / b6e537905467c375d1a94f1167707d079a663a06707c381a5902435053ddbd24

Verification & scope

The explicitly stated toy language is the complete scope; this is not a production compiler or a claim about Rust semantics. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.

Observations recorded using Python 3.12.14 at 2026-09-29T14:43:57.725831+00:00.

Case digest / 9c2ea64141923d0e41bc62cb6cb396c7e18b49432515708e07cb20daedfba242