FA-43306 / Borrow checking / Open access
Assignment is incorrectly given the lifetime-extension rule of a let initializer · case 01
Assignment is incorrectly given the lifetime-extension rule of a let initializer.
ROOT CAUSE
The static analyzer mishandles assignment no extension: assignment is incorrectly given the lifetime-extension rule of a let initializer.
VERIFIED REPAIR
Apply the specified transfer or inference rule at this site: if d['assignment_extended']: errors.append('assignment-no-extension').
Unsuccessful approach: The partial repair uses if d['assignment_extended'] and d['temp_end']>d['block_end']: errors.append('assignment-no-extension'), which still violates the stipulated analysis contract.
Case contract
Check temporary storage scopes using statement, block and full-expression integer boundaries. A borrowed temporary must cover use points; ordinary call arguments end at call boundary; let reference initializers may extend to block end but assignment RHS may not; operand temporaries end after enclosing expression; condition temporaries cannot leak into the then block; short-circuit RHS temporaries exist only on executed branch; a destructor observation is a use point; a reference to a promoted constant uses static storage; explicit owner binding prevents premature temporary destruction. Input is a fully explicit descriptor of the stated toy IR. Return rule identifiers in declaration order; absent optional obligations use the provided neutral defaults. No rule is an assertion about a production language.
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(d):
errors=[]
if not set(d['uses'])<=set(d['alive']): errors.append('temporary-use')
if d['arg_end']>d['call_end']: errors.append('argument-scope')
if d['let_extended'] and d['temp_end']!=d['block_end']: errors.append('let-extension')
if False: errors.append('assignment-no-extension')
if d['operand_end']<d['expr_end']: errors.append('operand-expression')
if d['condition'] and bool(d['then_uses']): errors.append('condition-escape')
if d['rhs_created'] and not d['rhs_executed']: errors.append('short-circuit-creation')
if not set(d['drop_uses'])<=set(d['alive']): errors.append('destructor-use')
if d['promoted'] and not d['static_storage']: errors.append('promotion-storage')
if d['bound_temp_end']<d['owner_end']: errors.append('bound-owner-scope')
return errors
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'uses': [], 'alive': [], 'call_end': 0, 'arg_end': 0, 'let_extended': False, 'temp_end': 0, 'block_end': 0, 'assignment_extended': False, 'expr_end': 0, 'operand_end': 0, 'condition': False, 'then_uses': [], 'rhs_created': False, 'rhs_executed': True, 'drop_uses': [], 'promoted': False, 'static_storage': True, 'owner_end': 0, 'bound_temp_end': 0}
check('well formed empty obligations',solve(base),[])
check('temporary-use regression 0', solve(dict(base, **({'uses':[N],'alive':[N+1]}))), ['temporary-use'])
check('temporary-use regression 1', solve(dict(base, **({'uses':[N,N+1],'alive':[N+1,N+2]}))), ['temporary-use'])
check('argument-scope regression 0', solve(dict(base, **({'arg_end':N+1,'call_end':N}))), ['argument-scope'])
check('argument-scope regression 1', solve(dict(base, **({'arg_end':N+2,'call_end':N+1}))), ['argument-scope'])
check('let-extension regression 0', solve(dict(base, **({'let_extended':True,'temp_end':N,'block_end':N+1}))), ['let-extension'])
check('let-extension regression 1', solve(dict(base, **({'let_extended':True,'temp_end':N,'block_end':N+2}))), ['let-extension'])
check('assignment-no-extension regression 0', solve(dict(base, **({'assignment_extended':True}))), ['assignment-no-extension'])
check('assignment-no-extension regression 1', solve(dict(base, **({'assignment_extended':True,'block_end':N}))), ['assignment-no-extension'])
check('operand-expression regression 0', solve(dict(base, **({'operand_end':N,'expr_end':N+1}))), ['operand-expression'])
check('operand-expression regression 1', solve(dict(base, **({'operand_end':N+1,'expr_end':N+2}))), ['operand-expression'])
check('condition-escape regression 0', solve(dict(base, **({'condition':True,'then_uses':[N]}))), ['condition-escape'])
check('condition-escape regression 1', solve(dict(base, **({'condition':True,'then_uses':[N+1]}))), ['condition-escape'])
check('short-circuit-creation regression 0', solve(dict(base, **({'rhs_created':True,'rhs_executed':False}))), ['short-circuit-creation'])
check('short-circuit-creation regression 1', solve(dict(base, **({'rhs_created':True,'rhs_executed':False,'expr_end':N,'operand_end':N}))), ['short-circuit-creation'])
check('destructor-use regression 0', solve(dict(base, **({'drop_uses':[N+1],'alive':[N]}))), ['destructor-use'])
check('destructor-use regression 1', solve(dict(base, **({'drop_uses':[N,N+1],'alive':[N]}))), ['destructor-use'])
check('promotion-storage regression 0', solve(dict(base, **({'promoted':True,'static_storage':False}))), ['promotion-storage'])
check('promotion-storage regression 1', solve(dict(base, **({'promoted':True,'static_storage':False,'block_end':N}))), ['promotion-storage'])
check('bound-owner-scope regression 0', solve(dict(base, **({'bound_temp_end':N,'owner_end':N+1}))), ['bound-owner-scope'])
check('bound-owner-scope regression 1', solve(dict(base, **({'bound_temp_end':N+1,'owner_end':N+2}))), ['bound-owner-scope'])
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 |
|---|---|---|---|
| well formed empty obligations | [] | [] | Passed |
| temporary-use regression 0 | ['temporary-use'] | ['temporary-use'] | Passed |
| temporary-use regression 1 | ['temporary-use'] | ['temporary-use'] | Passed |
| argument-scope regression 0 | ['argument-scope'] | ['argument-scope'] | Passed |
| argument-scope regression 1 | ['argument-scope'] | ['argument-scope'] | Passed |
| let-extension regression 0 | ['let-extension'] | ['let-extension'] | Passed |
| let-extension regression 1 | ['let-extension'] | ['let-extension'] | Passed |
| assignment-no-extension regression 0 | [] | ['assignment-no-extension'] | Failed |
| assignment-no-extension regression 1 | [] | ['assignment-no-extension'] | Failed |
| operand-expression regression 0 | ['operand-expression'] | ['operand-expression'] | Passed |
| operand-expression regression 1 | ['operand-expression'] | ['operand-expression'] | Passed |
| condition-escape regression 0 | ['condition-escape'] | ['condition-escape'] | Passed |
| condition-escape regression 1 | ['condition-escape'] | ['condition-escape'] | Passed |
| short-circuit-creation regression 0 | ['short-circuit-creation'] | ['short-circuit-creation'] | Passed |
| short-circuit-creation regression 1 | ['short-circuit-creation'] | ['short-circuit-creation'] | Passed |
| destructor-use regression 0 | ['destructor-use'] | ['destructor-use'] | Passed |
| destructor-use regression 1 | ['destructor-use'] | ['destructor-use'] | Passed |
| promotion-storage regression 0 | ['promotion-storage'] | ['promotion-storage'] | Passed |
| promotion-storage regression 1 | ['promotion-storage'] | ['promotion-storage'] | Passed |
| bound-owner-scope regression 0 | ['bound-owner-scope'] | ['bound-owner-scope'] | Passed |
| bound-owner-scope regression 1 | ['bound-owner-scope'] | ['bound-owner-scope'] | Passed |
SHA-256 / 4c9dd11bd23ec43b93c43006528d8826e731f5cb2f3aac5ad21d71cd2d37d0ba
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(d):
errors=[]
if not set(d['uses'])<=set(d['alive']): errors.append('temporary-use')
if d['arg_end']>d['call_end']: errors.append('argument-scope')
if d['let_extended'] and d['temp_end']!=d['block_end']: errors.append('let-extension')
if d['assignment_extended'] and d['temp_end']>d['block_end']: errors.append('assignment-no-extension')
if d['operand_end']<d['expr_end']: errors.append('operand-expression')
if d['condition'] and bool(d['then_uses']): errors.append('condition-escape')
if d['rhs_created'] and not d['rhs_executed']: errors.append('short-circuit-creation')
if not set(d['drop_uses'])<=set(d['alive']): errors.append('destructor-use')
if d['promoted'] and not d['static_storage']: errors.append('promotion-storage')
if d['bound_temp_end']<d['owner_end']: errors.append('bound-owner-scope')
return errors
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'uses': [], 'alive': [], 'call_end': 0, 'arg_end': 0, 'let_extended': False, 'temp_end': 0, 'block_end': 0, 'assignment_extended': False, 'expr_end': 0, 'operand_end': 0, 'condition': False, 'then_uses': [], 'rhs_created': False, 'rhs_executed': True, 'drop_uses': [], 'promoted': False, 'static_storage': True, 'owner_end': 0, 'bound_temp_end': 0}
check('well formed empty obligations',solve(base),[])
check('temporary-use regression 0', solve(dict(base, **({'uses':[N],'alive':[N+1]}))), ['temporary-use'])
check('temporary-use regression 1', solve(dict(base, **({'uses':[N,N+1],'alive':[N+1,N+2]}))), ['temporary-use'])
check('argument-scope regression 0', solve(dict(base, **({'arg_end':N+1,'call_end':N}))), ['argument-scope'])
check('argument-scope regression 1', solve(dict(base, **({'arg_end':N+2,'call_end':N+1}))), ['argument-scope'])
check('let-extension regression 0', solve(dict(base, **({'let_extended':True,'temp_end':N,'block_end':N+1}))), ['let-extension'])
check('let-extension regression 1', solve(dict(base, **({'let_extended':True,'temp_end':N,'block_end':N+2}))), ['let-extension'])
check('assignment-no-extension regression 0', solve(dict(base, **({'assignment_extended':True}))), ['assignment-no-extension'])
check('assignment-no-extension regression 1', solve(dict(base, **({'assignment_extended':True,'block_end':N}))), ['assignment-no-extension'])
check('operand-expression regression 0', solve(dict(base, **({'operand_end':N,'expr_end':N+1}))), ['operand-expression'])
check('operand-expression regression 1', solve(dict(base, **({'operand_end':N+1,'expr_end':N+2}))), ['operand-expression'])
check('condition-escape regression 0', solve(dict(base, **({'condition':True,'then_uses':[N]}))), ['condition-escape'])
check('condition-escape regression 1', solve(dict(base, **({'condition':True,'then_uses':[N+1]}))), ['condition-escape'])
check('short-circuit-creation regression 0', solve(dict(base, **({'rhs_created':True,'rhs_executed':False}))), ['short-circuit-creation'])
check('short-circuit-creation regression 1', solve(dict(base, **({'rhs_created':True,'rhs_executed':False,'expr_end':N,'operand_end':N}))), ['short-circuit-creation'])
check('destructor-use regression 0', solve(dict(base, **({'drop_uses':[N+1],'alive':[N]}))), ['destructor-use'])
check('destructor-use regression 1', solve(dict(base, **({'drop_uses':[N,N+1],'alive':[N]}))), ['destructor-use'])
check('promotion-storage regression 0', solve(dict(base, **({'promoted':True,'static_storage':False}))), ['promotion-storage'])
check('promotion-storage regression 1', solve(dict(base, **({'promoted':True,'static_storage':False,'block_end':N}))), ['promotion-storage'])
check('bound-owner-scope regression 0', solve(dict(base, **({'bound_temp_end':N,'owner_end':N+1}))), ['bound-owner-scope'])
check('bound-owner-scope regression 1', solve(dict(base, **({'bound_temp_end':N+1,'owner_end':N+2}))), ['bound-owner-scope'])
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 |
|---|---|---|---|
| well formed empty obligations | [] | [] | Passed |
| temporary-use regression 0 | ['temporary-use'] | ['temporary-use'] | Passed |
| temporary-use regression 1 | ['temporary-use'] | ['temporary-use'] | Passed |
| argument-scope regression 0 | ['argument-scope'] | ['argument-scope'] | Passed |
| argument-scope regression 1 | ['argument-scope'] | ['argument-scope'] | Passed |
| let-extension regression 0 | ['let-extension'] | ['let-extension'] | Passed |
| let-extension regression 1 | ['let-extension'] | ['let-extension'] | Passed |
| assignment-no-extension regression 0 | [] | ['assignment-no-extension'] | Failed |
| assignment-no-extension regression 1 | [] | ['assignment-no-extension'] | Failed |
| operand-expression regression 0 | ['operand-expression'] | ['operand-expression'] | Passed |
| operand-expression regression 1 | ['operand-expression'] | ['operand-expression'] | Passed |
| condition-escape regression 0 | ['condition-escape'] | ['condition-escape'] | Passed |
| condition-escape regression 1 | ['condition-escape'] | ['condition-escape'] | Passed |
| short-circuit-creation regression 0 | ['short-circuit-creation'] | ['short-circuit-creation'] | Passed |
| short-circuit-creation regression 1 | ['short-circuit-creation'] | ['short-circuit-creation'] | Passed |
| destructor-use regression 0 | ['destructor-use'] | ['destructor-use'] | Passed |
| destructor-use regression 1 | ['destructor-use'] | ['destructor-use'] | Passed |
| promotion-storage regression 0 | ['promotion-storage'] | ['promotion-storage'] | Passed |
| promotion-storage regression 1 | ['promotion-storage'] | ['promotion-storage'] | Passed |
| bound-owner-scope regression 0 | ['bound-owner-scope'] | ['bound-owner-scope'] | Passed |
| bound-owner-scope regression 1 | ['bound-owner-scope'] | ['bound-owner-scope'] | Passed |
SHA-256 / 27cd0c54b7ba5a926df8596a0c1ce28c78203b1d50de8d7022def6bd6db2b304
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(d):
errors=[]
if not set(d['uses'])<=set(d['alive']): errors.append('temporary-use')
if d['arg_end']>d['call_end']: errors.append('argument-scope')
if d['let_extended'] and d['temp_end']!=d['block_end']: errors.append('let-extension')
if d['assignment_extended']: errors.append('assignment-no-extension')
if d['operand_end']<d['expr_end']: errors.append('operand-expression')
if d['condition'] and bool(d['then_uses']): errors.append('condition-escape')
if d['rhs_created'] and not d['rhs_executed']: errors.append('short-circuit-creation')
if not set(d['drop_uses'])<=set(d['alive']): errors.append('destructor-use')
if d['promoted'] and not d['static_storage']: errors.append('promotion-storage')
if d['bound_temp_end']<d['owner_end']: errors.append('bound-owner-scope')
return errors
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'uses': [], 'alive': [], 'call_end': 0, 'arg_end': 0, 'let_extended': False, 'temp_end': 0, 'block_end': 0, 'assignment_extended': False, 'expr_end': 0, 'operand_end': 0, 'condition': False, 'then_uses': [], 'rhs_created': False, 'rhs_executed': True, 'drop_uses': [], 'promoted': False, 'static_storage': True, 'owner_end': 0, 'bound_temp_end': 0}
check('well formed empty obligations',solve(base),[])
check('temporary-use regression 0', solve(dict(base, **({'uses':[N],'alive':[N+1]}))), ['temporary-use'])
check('temporary-use regression 1', solve(dict(base, **({'uses':[N,N+1],'alive':[N+1,N+2]}))), ['temporary-use'])
check('argument-scope regression 0', solve(dict(base, **({'arg_end':N+1,'call_end':N}))), ['argument-scope'])
check('argument-scope regression 1', solve(dict(base, **({'arg_end':N+2,'call_end':N+1}))), ['argument-scope'])
check('let-extension regression 0', solve(dict(base, **({'let_extended':True,'temp_end':N,'block_end':N+1}))), ['let-extension'])
check('let-extension regression 1', solve(dict(base, **({'let_extended':True,'temp_end':N,'block_end':N+2}))), ['let-extension'])
check('assignment-no-extension regression 0', solve(dict(base, **({'assignment_extended':True}))), ['assignment-no-extension'])
check('assignment-no-extension regression 1', solve(dict(base, **({'assignment_extended':True,'block_end':N}))), ['assignment-no-extension'])
check('operand-expression regression 0', solve(dict(base, **({'operand_end':N,'expr_end':N+1}))), ['operand-expression'])
check('operand-expression regression 1', solve(dict(base, **({'operand_end':N+1,'expr_end':N+2}))), ['operand-expression'])
check('condition-escape regression 0', solve(dict(base, **({'condition':True,'then_uses':[N]}))), ['condition-escape'])
check('condition-escape regression 1', solve(dict(base, **({'condition':True,'then_uses':[N+1]}))), ['condition-escape'])
check('short-circuit-creation regression 0', solve(dict(base, **({'rhs_created':True,'rhs_executed':False}))), ['short-circuit-creation'])
check('short-circuit-creation regression 1', solve(dict(base, **({'rhs_created':True,'rhs_executed':False,'expr_end':N,'operand_end':N}))), ['short-circuit-creation'])
check('destructor-use regression 0', solve(dict(base, **({'drop_uses':[N+1],'alive':[N]}))), ['destructor-use'])
check('destructor-use regression 1', solve(dict(base, **({'drop_uses':[N,N+1],'alive':[N]}))), ['destructor-use'])
check('promotion-storage regression 0', solve(dict(base, **({'promoted':True,'static_storage':False}))), ['promotion-storage'])
check('promotion-storage regression 1', solve(dict(base, **({'promoted':True,'static_storage':False,'block_end':N}))), ['promotion-storage'])
check('bound-owner-scope regression 0', solve(dict(base, **({'bound_temp_end':N,'owner_end':N+1}))), ['bound-owner-scope'])
check('bound-owner-scope regression 1', solve(dict(base, **({'bound_temp_end':N+1,'owner_end':N+2}))), ['bound-owner-scope'])
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 |
|---|---|---|---|
| well formed empty obligations | [] | [] | Passed |
| temporary-use regression 0 | ['temporary-use'] | ['temporary-use'] | Passed |
| temporary-use regression 1 | ['temporary-use'] | ['temporary-use'] | Passed |
| argument-scope regression 0 | ['argument-scope'] | ['argument-scope'] | Passed |
| argument-scope regression 1 | ['argument-scope'] | ['argument-scope'] | Passed |
| let-extension regression 0 | ['let-extension'] | ['let-extension'] | Passed |
| let-extension regression 1 | ['let-extension'] | ['let-extension'] | Passed |
| assignment-no-extension regression 0 | ['assignment-no-extension'] | ['assignment-no-extension'] | Passed |
| assignment-no-extension regression 1 | ['assignment-no-extension'] | ['assignment-no-extension'] | Passed |
| operand-expression regression 0 | ['operand-expression'] | ['operand-expression'] | Passed |
| operand-expression regression 1 | ['operand-expression'] | ['operand-expression'] | Passed |
| condition-escape regression 0 | ['condition-escape'] | ['condition-escape'] | Passed |
| condition-escape regression 1 | ['condition-escape'] | ['condition-escape'] | Passed |
| short-circuit-creation regression 0 | ['short-circuit-creation'] | ['short-circuit-creation'] | Passed |
| short-circuit-creation regression 1 | ['short-circuit-creation'] | ['short-circuit-creation'] | Passed |
| destructor-use regression 0 | ['destructor-use'] | ['destructor-use'] | Passed |
| destructor-use regression 1 | ['destructor-use'] | ['destructor-use'] | Passed |
| promotion-storage regression 0 | ['promotion-storage'] | ['promotion-storage'] | Passed |
| promotion-storage regression 1 | ['promotion-storage'] | ['promotion-storage'] | Passed |
| bound-owner-scope regression 0 | ['bound-owner-scope'] | ['bound-owner-scope'] | Passed |
| bound-owner-scope regression 1 | ['bound-owner-scope'] | ['bound-owner-scope'] | Passed |
SHA-256 / 8589ce56094dd4ae30c738257aa27e119bcd55227a7446b3f1492883db8f8c12
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:44:00.507096+00:00.
Case digest / 70530f853d7c15d8391675567c1053b32998180778c76a1284c175a5d319dcfc