feat(life): A1——@life 新增 stores(x)/borrows(x)(复用 escape/noescape 契约位);ret/owns 显式报未实现
§14 路线 A 第一步(零语义变化): - stores(x) 归到"强制逃逸"位、borrows(x) 归到"强制不逃逸"位(同一对契约位,调用点已在最后套用、.vpi 已有 esce=/escn= 通道) - _WillFreeMergeTag 白名单同步扩 stores/borrows;ret/owns 显式 fail-fast "not implemented yet (planned A2/A3)",不做静默忽略 - 矛盾契约报文改为 escape/stores 与 noescape/borrows 两两对立
This commit is contained in:
1 parent
71730d920c
commit
6000734704
1 file changed
+15
-4
@@ -367,8 +367,16 @@ def _WillFreeMergeTag(fn: ast.FunctionDef*, tag: ast.AST*, mask: int) -> int:
|
||||
is_wf: int = string.strcmp(tnm, "willFree")
|
||||
is_esc: int = string.strcmp(tnm, "escape")
|
||||
is_nesc: int = string.strcmp(tnm, "noescape")
|
||||
if is_wf != 0 and is_esc != 0 and is_nesc != 0:
|
||||
fatal_error(tag, "@life(...) accepts only `willFree(<param>)` / `escape(<param>)` / `noescape(<param>)` tags", "LifetimeError")
|
||||
# A1(§14):stores ≡ escape("确定存进长命存储"的强声明)、borrows ≡ noescape(借出口径)。
|
||||
# 二者复用同一对契约位,位本身由 compute_escape_directives 收。
|
||||
is_st: int = string.strcmp(tnm, "stores")
|
||||
is_bw: int = string.strcmp(tnm, "borrows")
|
||||
# A2/A3 的标签(ret / owns)先**显式**报"未实现",不做静默忽略(静默 = 用户以为标注生效了)。
|
||||
if string.strcmp(tnm, "owns") == 0 or string.strcmp(tnm, "ret") == 0:
|
||||
fatal_error(tag, f"@life tag `{tnm}(...)` is not implemented yet (planned A2/A3); use willFree/escape/noescape/stores/borrows for now", "LifetimeError")
|
||||
return mask
|
||||
if is_wf != 0 and is_esc != 0 and is_nesc != 0 and is_st != 0 and is_bw != 0:
|
||||
fatal_error(tag, "@life(...) accepts only `willFree(...)` / `escape(...)` / `noescape(...)` / `stores(...)` / `borrows(...)` tags", "LifetimeError")
|
||||
return mask
|
||||
if tc.args is None or len(tc.args) == 0:
|
||||
fatal_error(tag, f"@life tag `{tnm}(...)` needs at least one parameter name or 0-based position", "LifetimeError")
|
||||
@@ -422,6 +430,9 @@ def compute_escape_directives(fd: ast.AST*, out: sizet*) -> int:
|
||||
if tnm2 is None: continue
|
||||
is_esc2: int = string.strcmp(tnm2, "escape")
|
||||
is_nesc2: int = string.strcmp(tnm2, "noescape")
|
||||
# A1(§14):stores 归到"强制逃逸"位、borrows 归到"强制不逃逸"位(复用同一对契约位)
|
||||
if string.strcmp(tnm2, "stores") == 0: is_esc2 = 0
|
||||
if string.strcmp(tnm2, "borrows") == 0: is_nesc2 = 0
|
||||
if is_esc2 != 0 and is_nesc2 != 0: continue
|
||||
if tcl.args is None or len(tcl.args) == 0:
|
||||
fatal_error(tg, f"@life tag `{tnm2}(...)` needs at least one parameter name or 0-based position", "LifetimeError")
|
||||
@@ -434,12 +445,12 @@ def compute_escape_directives(fd: ast.AST*, out: sizet*) -> int:
|
||||
if idx2 < 0: continue
|
||||
if is_esc2 == 0:
|
||||
if ((int(out[1]) >> idx2) & 1) != 0:
|
||||
fatal_error(tg, f"contradictory lifetime tags: parameter #{idx2} is marked both escape(...) and noescape(...)", "LifetimeError")
|
||||
fatal_error(tg, f"contradictory lifetime tags: parameter #{idx2} is marked both escape/stores(...) and noescape/borrows(...)", "LifetimeError")
|
||||
continue
|
||||
out[0] = out[0] | (sizet(1) << idx2)
|
||||
else:
|
||||
if ((int(out[0]) >> idx2) & 1) != 0:
|
||||
fatal_error(tg, f"contradictory lifetime tags: parameter #{idx2} is marked both escape(...) and noescape(...)", "LifetimeError")
|
||||
fatal_error(tg, f"contradictory lifetime tags: parameter #{idx2} is marked both escape/stores(...) and noescape/borrows(...)", "LifetimeError")
|
||||
continue
|
||||
out[1] = out[1] | (sizet(1) << idx2)
|
||||
return 0
|
||||
|
||||
Reference in new issue
Block a user