分离逻辑自动化

Symbolic heap 片段 ​

分离逻辑公理库分离逻辑Separation logic以分离合取表达互不重叠资源并局部推理堆内存的程序逻辑。的 symbolic heap 常写作

$$\mathrm{\exists }\overrightarrow{z}.\mathrm{\Pi }\wedge \mathrm{\Sigma },$$

其中 $\mathrm{\Pi }$ 是等式、不等式等纯约束，空间部分 $\mathrm{\Sigma }$ 由

$$emp,x\mapsto v,P\ast Q$$

及 list segment 等归纳谓词构成。$P\ast Q$ 要求堆可分成互不重叠的两部分分别满足 $P,Q$。

自动化主要解决 satisfiability、entailment

$$P⊢Q,$$

以及在程序命令前后更新 symbolic heap。它不是把普通一阶求解器换一个语法外壳；堆分割和归纳展开是核心搜索结构。

归纳 list segment 可定义为

$$ls(x,y)\equiv (x=y\wedge emp)\vee \mathrm{\exists }z.x\mapsto z\ast ls(z,y).$$

unfold 一次暴露头单元，fold 则把已证明的头和尾重新封装。定义的 base case 和 ownership 范围若不同，entailment 规则也随之改变。

允许 cyclic heap 时，普通 list predicate 可能不适用；工具若默认 acyclic 但输入没有该前置，会把真实循环结构当不可满足。

指针更新轨迹 ​

前态

$$x\mapsto a\ast y\mapsto b$$

表示两个独立单元。执行 x->val := c 后，symbolic execution 消耗 $x\mapsto a$，产生 $x\mapsto c$，保留 frame $y\mapsto b$：

$$x\mapsto c\ast y\mapsto b.$$

这一步由frame rule公理库框架规则Frame rule若命令不修改额外资源，则可把该资源同时附加到前置和后置断言。局部化。若 $x=y$，前态本身因两个 singleton heap 重叠而不可满足；纯约束和空间约束必须联合检查。

如果更新还可能释放或重新分配地址，简单替换 points-to 值不够，需建模 allocation freshness 与 dangling pointer。

执行 free(x) 应消耗 $x\mapsto a$，后态不能继续 frame 该单元。随后 dereference 若没有重新取得 points-to 权限，应报告 use-after-free。仅把值改成特殊 freed 而仍允许普通读写规则，会混淆无所有权与一个可读取哨兵值。

分配 x:=malloc() 产生 fresh 地址及新单元；freshness 是相对于当前 heap domain，不只是与某几个命名指针不等。

entailment 与匹配 ​

要证明

$$x\mapsto a\ast y\mapsto b⊢y\mapsto b\ast x\mapsto a,$$

可用 separating conjunction 的交换性规范化。证明 list segment entailment 时，求解器可能 unfold 一个归纳谓词，匹配头节点，再递归处理尾段。

盲目双向展开会造成无限搜索。成熟算法用规则优先级、memoization、cyclic proof 或片段限制保证终止/完备性。

cyclic proof 若回到相似 entailment，必须满足 global progress condition，确保某个归纳结构严格展开；仅因目标文本重复就闭环，会接受 $P⊢Q$ 的循环自证。

反例模型需要给出具体有限 heap 划分，显示哪个地址重叠或哪个 list link 断裂。求解器返回“not proved”可能是算法不完备/超时，不等于 entailment 为假。

纯部分交给SAT/SMT公理库可满足公式Satisfiable formula存在至少一个真值赋值使其为真的命题公式。，但空间匹配产生的地址等式会反向影响纯约束；一次性先解完纯部分再不回看可能漏推论。

Frame inference 与 bi-abduction ​

Frame inference 给定 $P,Q$ 寻找 $F$ 使

$$P⊢Q\ast F,$$

即从当前资源中分出命令需要的 $Q$，剩余 $F$ 保持不变。

Bi-abduction 同时寻找 anti-frame $A$ 与 frame $F$：

$$P\ast A⊢Q\ast F.$$

$A$ 是调用安全还缺少的前置资源，$F$ 是调用后未触及资源。沿调用图组合这些结果，可推断函数前后置契约。

解一般不唯一。取 $A=Q,F=P$ 之类平凡解可能可靠却毫无局部性；算法需最小化或规范化，并处理推断契约在所有路径上的一致性。

例如当前有 $x\mapsto y$，调用 disposeList(x) 需要 $ls(x,null)$。bi-abduction 可推断缺少尾段 $ls(y,null)$，而 frame 为空。若直接推断一个完全独立新链满足 callee 前置，会与已有头指针不相连，虽在过宽逻辑下可满足，却不是合理最小 anti-frame。

跨多个调用合成契约时，前一调用的 frame 可成为后一调用资源；路径 join 要找到各分支共同可保证的 heap，而不是把互斥分支资源用 separating conjunction 同时要求。

内存错误与失败边界 ​

dereference 要求当前 symbolic heap 能提供相应 points-to；找不到时可能是确切 null/use-after-free 错误，也可能是抽象或函数摘要太弱。报告前需区分不可满足路径与缺失资源。

并发 separation logic 还需权限、资源不变量和原子规则。顺序 symbolic heap 自动化不能直接验证数据竞态。

fractional permission 区分只读共享与独占写：多个线程可持有分数读权限，总和受限；写入通常要求完整权限。若求解器只检查地址不重叠，会错误拒绝合法共享读，或错误允许两个写者。

内存模型中的 weak ordering、原子指令和 reclamation（hazard pointer/epoch）需要专门逻辑；简单 points-to 所有权无法表达“对象已逻辑删除但仍被读者安全访问”的时序协议。

任意归纳谓词 entailment 一般不可判定；工具声称自动化时必须说明支持片段、超时和 unknown。将 unknown 当 valid 会产生不可靠证明。

参考资料

• John C. Reynolds, “Separation Logic: A Logic for Shared Mutable Data Structures,” LICS, 2002, pp. 55–74。
• Cristiano Calcagno et al., “Compositional Shape Analysis by Means of Bi-Abduction,” POPL, 2009, pp. 289–300。
• James Brotherston, Dino Distefano, and Rasmus L. Petersen, “Automated Cyclic Entailment Proofs in Separation Logic,” CADE-23, 2011, pp. 131–146。
• Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn, “A Decidable Fragment of Separation Logic,” FSTTCS, 2004, pp. 97–109。