Files
Viper_RegressionTesting/NewLifetimeRetOkTest/App/main.vp
T
TermiNexus b737bedceb test(lifetime): A2 补“形参位↔实参位映射”双向钉桩(受控用例)
背景:NewLifetimeRetXmodTest 曾漏检 —— ret(borrows=x) 的 pi→实参映射把模块限定函数
`m.f(...)` 误当方法(给 pi=0 加 self 偏移),取到模块名而非实参。
为防同类回归,在正向工程 NewLifetimeRetOkTest 里加两个“错就编译失败”的钉桩:

- (4a) 模块限定函数:retdep.Identity2(fr, hp)(borrows=1)。
  实参 0 故意是**本帧**指针、实参 1 是**堆**指针 ⇒ 正确映射取实参 1=堆(可存进堆字段);
  若误加 self 偏移 → 取成实参 0(本帧)→ 结果 FRAME → 该行报错。
- (4b) 方法:box.SelfRef(fr)(borrows=self)。
  接收者是**堆**对象、用户实参是**本帧**指针 ⇒ 正确映射取接收者=堆(可存进堆字段);
  若忘了 self 偏移 → 取成实参 0(本帧)→ 结果 FRAME → 该行报错。

即两个方向任一偏移错都会让本正向工程编译失败(正向工程的“错就报错”比再堆一个负向
工程更能锁死偏移量)。README 的 NewLifetimeRetOkTest 行同步说明。
2026-10-10 13:24:27 +08:00

95 lines
4.0 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
from stdint import *
import stdio
import retdep
# =============================================================================
# 正向工程:A2 `@life(ret(...))` 契约**不得误报**(编译必须成功、运行退出码 0)
#
# 对照负向工程:
# · NewLifetimeRetEscapeTest —— 同模块 `ret(frame)` 的结果存进长命存储 → 必须报;
# · NewLifetimeRetXmodTest —— 跨模块 `ret(borrows=x)`(经 .vpi 的 escr=)→ 必须报。
#
# 本工程覆盖:
# (1) 非帧契约(heap / static / borrows=none)→ 结果可存进**堆对象字段**(长命左值);
# (2) ret(frame) → 结果只在本帧内使用 → 合法(不是"无害",而是调用点按声明**放行**);
# (3) ret(borrows=x) → 结果的生命期 = 实参 x 的生命期(本帧实参 → 帧内使用合法);
# (4) 同模块(本文件契约表)与跨模块(retdep.vp,经 .vpi 的 escr=)两条取用路径都走一遍。
#
# 注意:本文件**不得**把 `ret(frame)` / `ret(borrows=x)` 的结果写进堆对象字段
# (`h.p = …`)——那是负向工程负责证明会被拒的写法。
# =============================================================================
novirtual class Holder:
p: int*
c: char*
# 方法版 borrows 的钉桩:`ret(borrows=self)` ⇒ 结果的生命期 = **接收者**(不是实参)。
# 调用点故意让接收者是**堆**对象、用户实参是**本帧**指针:
# 映射正确 → 结果=堆(可存进长命存储);
# 若把方法误当"无 self"而不偏移 → 取成实参 0(本帧)→ 结果 FRAME → 报错 ⇒ 用例失败。
novirtual class BorrowBox:
v: int*
@life(noescape(self, x), ret(borrows=self))
def SelfRef(self, x: int*) -> int*:
return self.v
# ---- 同模块契约(走本文件 EscDirTable,不经 .vpi)----
@life(ret(heap))
def LocalHeap() -> int*:
return new heap hlife int
@life(ret(frame))
def LocalFrame() -> int*:
l: int* = new stack int
return l
export def main() -> int:
h: Holder* = new heap hlife Holder()
# (1) 非帧契约 → 存进堆对象字段(左值长命、右值非帧)→ 放行
h.p = retdep.MkHeap() # 跨模块 ret(heap)
h.c = retdep.MkStatic() # 跨模块 ret(static)
h.p = retdep.Fresh() # 跨模块 ret(borrows=none)
h.p = LocalHeap() # 同模块 ret(heap)
# (2) ret(frame):结果只在本帧内使用 → 放行
pf: int* = retdep.FrameRet() # 跨模块 ret(frame)
pl: int* = LocalFrame() # 同模块 ret(frame)
# (3) ret(borrows=x):结果生命期 = 实参生命期;实参在本帧 → 结果只在本帧用 → 放行
base: int* = new stack int
pb: int* = retdep.IdentBorrow(base)
# (4) 形参位↔实参位映射的**两个方向**都用"错就报错"的方式钉住(对照 §14.3.1):
# (4a) 模块限定函数 `retdep.Identity2(fr, hp)`:**不**含 self ⇒ 形参位 = 实参位。
# 实参 0 故意用**本帧**指针、实参 1 用**堆**指针;borrows=1 → 结果应为堆 → 可存进 h.p。
# 若误按方法偏移一格 → 取成实参 0(本帧)→ 结果 FRAME → 本行报错。
# (4b) 方法 `box.SelfRef(fr)`:**含** self ⇒ 形参位要偏移。接收者用**堆**对象、实参用**本帧**指针;
# borrows=self → 结果应为堆(接收者)→ 可存进 out.v。
# 若忘了偏移 → 取成实参 0(本帧)→ 结果 FRAME → 本行报错。
fr: int* = new stack int
hp: int* = new heap hlife int
h.p = retdep.Identity2(fr, hp)
box: BorrowBox* = new heap hlife BorrowBox()
box.v = new heap hlife int
out: BorrowBox* = new heap hlife BorrowBox()
out.v = box.SelfRef(fr)
if pf is None: return 1
if pl is None: return 2
if pb is None: return 3
if h.p is None: return 4
if out.v is None: return 5
stdio.printf("RetOkTest OK: @life(ret(...)) contracts accepted\n")
return 0