抽象解释引擎Skill abstract-interpretation-engine

---

名称: 抽象解释引擎 描述: ‘实现抽象解释用于静态分析。使用场景: (1) 构建静态分析器, (2) 程序验证, (3) 静态分析。’ 版本: 1.0.0 标签:

• 静态分析
• 抽象解释
• 固定点
• 验证 难度: 高级 语言:
• python
• ocaml 依赖项:
• 数据流分析框架

可操作的触发器

触发器:

• “实现抽象解释”
• “构建静态分析器”
• “计算程序不变量”
• “分析变量范围”
• “检测空指针解引用”

即用提示

行动提示:

• “实现符号抽象域 (-, 0, +) 用于静态分析, 包含格结构和比较”
• “构建整数变量的区间分析, 带有widening操作符”
• “实现空值分析以检测潜在的空解引用”
• “创建抽象解释框架, 包含格、转移函数和固定点计算”

可选斜杠命令

命令: []

直接执行脚本

脚本: examples/abstract_interpreter.py

抽象解释引擎

状态: 准备使用 | 自动触发: 是 | 脚本: python examples/abstract_interpreter.py

触发器

当用户提到以下内容时激活此技能:

• 实现抽象解释
• 构建静态分析器
• 计算程序不变量
• 通过静态分析进行bug检测

行动提示

直接使用这些提示:

实现符号抽象域, 包含:
- 格: Bot < {-} < {-, 0} < {-, 0, +} < {0, +} < + < Top
- 并集、交集、小于操作
- 针对 +, -, *, / 的转移函数

构建区间分析:
- 整数的区间域 [l, u]
- Widening操作符以确保终止
- 算术操作的转移函数
- 处理循环widening阈值

实现空值分析:
- 格: Bottom < MaybeNull < NotNull < Top
- 通过赋值跟踪可空变量
- 处理条件语句和分支

使用时机

• 静态程序分析
• Bug检测
• 程序验证
• 类型推断

此技能功能

1. 定义抽象域 - 过近似
2. 实现转移 - 抽象语义
3. 计算固定点 - 混沌迭代
4. 处理widening - 确保终止

测试案例

程序	抽象状态	描述
x := 5; y := x + 1	x ∈ [5,5], y ∈ [6,6]	常量传播
while x > 0: x := x - 1	x ∈ [0, ∞) 循环后	循环头部的widening
if x > 0: y := 1 else: y := 0	y ∈ {0, 1}	分支合并处的并集

使用脚本

cd abstract-interpretation-engine
python examples/abstract_interpreter.py --domain sign --program "x := 5; y := x + 1"
python examples/abstract_interpreter.py --domain interval --file program.cfg

核心理论

具体域:     C ⊆ P(Σ)
抽象域:     A 带有 α: C → A, γ: A → C

健全性:           c ⊆ γ(α(c))
Galois连接:   ∀c∈C, a∈A. α(c) ⊑ a ⇔ c ⊆ γ(a)

实现

from dataclasses import dataclass, field
from typing import Dict, List, Set, Callable, Generic, TypeVar, Optional
from abc import ABC, abstractmethod

# 抽象域
class AbstractValue(ABC):
    """抽象值"""
    
    @abstractmethod
    def lub(self, other: 'AbstractValue') -> 'AbstractValue':
        """最小上界"""
        pass
    
    @abstractmethod
    def glb(self, other: 'AbstractValue') -> 'AbstractValue':
        """最大下界"""
        pass
    
    @abstractmethod
    def less_or_equal(self, other: 'AbstractValue') -> bool:
        """偏序 ≤"""
        pass

# 区间域
@dataclass
class Interval(AbstractValue):
    """区间 [lo, hi]"""
    lo: Optional[int]
    hi: Optional[int]
    
    def __post_init__(self):
        # 处理无穷
        if self.lo is None:
            self.lo = float('-inf')
        if self.hi is None:
            self.hi = float('inf')
    
    def lub(self, other: AbstractValue) -> 'AbstractValue':
        if not isinstance(other, Interval):
            return Top()
        return Interval(
            min(self.lo, other.lo),
            max(self.hi, other.hi)
        )
    
    def glb(self, other: AbstractValue) -> 'AbstractValue':
        if not isinstance(other, Interval):
            return Bottom()
        return Interval(
            max(self.lo, other.lo),
            min(self.hi, other.hi)
        )
    
    def less_or_equal(self, other: AbstractValue) -> bool:
        if not isinstance(other, Interval):
            return False
        return self.lo >= other.lo and self.hi <= other.hi
    
    def __repr__(self):
        return f"[{self.lo}, {self.hi}]"

@dataclass
class Top(AbstractValue):
    """顶部元素 (未知)"""
    
    def lub(self, other: AbstractValue) -> AbstractValue:
        return self
    
    def glb(self, other: AbstractValue) -> AbstractValue:
        return other
    
    def less_or_equal(self, other: AbstractValue) -> bool:
        return isinstance(other, Top)

@dataclass
class Bottom(AbstractValue):
    """底部元素 (不可达)"""
    
    def lub(self, other: AbstractValue) -> AbstractValue:
        return other
    
    def glb(self, other: AbstractValue) -> AbstractValue:
        return self
    
    def less_or_equal(self, other: AbstractValue) -> bool:
        return True

# 符号域
class Sign(AbstractValue):
    """符号抽象域: -, 0, +"""
    
    NEG = "negative"
    ZERO = "zero"
    POS = "positive"
    UNKNOWN = "unknown"
    
    def __init__(self, sign: str):
        self.sign = sign
    
    def lub(self, other: AbstractValue) -> AbstractValue:
        if not isinstance(other, Sign):
            return Top()
        
        signs = {self.sign, other.sign}
        
        if UNKNOWN in signs:
            return Sign(UNKNOWN)
        
        if NEG in signs and POS in signs:
            return Sign(UNKNOWN)
        
        if NEG in signs or ZERO in signs:
            return Sign(NEG) if NEG in signs else Sign(ZERO)
        
        return Sign(POS)
    
    def glb(self, other: AbstractValue) -> AbstractValue:
        if not isinstance(other, Sign):
            return Bottom()
        
        if self.sign == other.sign:
            return self
        
        return Bottom()  # 不一致
    
    def less_or_equal(self, other: AbstractValue) -> bool:
        if isinstance(other, Top):
            return True
        if not isinstance(other, Sign):
            return False
        
        order = {Bottom(), Sign(NEG), Sign(ZERO), Sign(POS), Top()}
        return order.index(self) <= order.index(other)

# 抽象环境
class AbstractEnvironment(Dict[str, AbstractValue]):
    """映射变量到抽象值"""
    
    def __getitem__(self, key: str) -> AbstractValue:
        return super().__getitem__(key)
    
    def lub(self, other: 'AbstractEnvironment') -> 'AbstractEnvironment':
        result = AbstractEnvironment()
        all_keys = set(self.keys()) | set(other.keys())
        
        for k in all_keys:
            v1 = self.get(k, Bottom())
            v2 = other.get(k, Bottom())
            result[k] = v1.lub(v2)
        
        return result

# 抽象语义
class AbstractInterpreter:
    """抽象解释器"""
    
    def __init__(self, domain: AbstractValue):
        self.domain = domain
        self.cfg: Dict[str, 'Stmt'] = {}
        self.env: AbstractEnvironment = {}
    
    def interpret(self, program: 'Program') -> Dict[str, AbstractEnvironment]:
        """
        抽象解释程序
        
        返回: 从节点到抽象状态的映射
        """
        
        states = {}
        
        # 固定点的工作列表
        worklist = list(program.cfg.keys())
        visited = set()
        
        # 初始化入口
        entry = program.entry
        states[entry] = AbstractEnvironment()
        
        while worklist:
            node = worklist.pop(0)
            
            if node not in states:
                states[node] = AbstractEnvironment()
            
            # 获取前驱状态
            preds = program.cfg.predecessors(node)
            
            if preds:
                # 并集状态
                new_state = states[preds[0]].copy()
                for pred in preds[1:]:
                    new_state = new_state.lub(states[pred])
            else:
                new_state = AbstractEnvironment()
            
            # 应用转移
            stmt = self.cfg.get(node)
            if stmt:
                new_state = self.transfer(stmt, new_state)
            
            # 检查是否改变
            if node not in visited or new_state != states[node]:
                states[node] = new_state
                visited.add(node)
                
                # 添加后继
                for succ in program.cfg.successors(node):
                    if succ not in worklist:
                        worklist.append(succ)
        
        return states
    
    def transfer(self, stmt: 'Stmt', env: AbstractEnvironment) -> AbstractEnvironment:
        """应用抽象转移函数"""
        
        result = AbstractEnvironment(env)
        
        match stmt:
            case Assign(x, expr):
                result[x] = self.eval_expr(expr, env)
            
            case If(cond, then, else_):
                # 两个分支
                then_env = self.transfer_block(then, env)
                else_env = self.transfer_block(else_, env)
                return then_env.lub(else_env)
            
            case While(cond, body):
                # 将由固定点处理
                pass
        
        return result
    
    def eval_expr(self, expr: 'Expr', env: AbstractEnvironment) -> AbstractValue:
        """抽象评估表达式"""
        
        match expr:
            case Const(n):
                return Interval(n, n)
            
            case Var(x):
                return env.get(x, Bottom())
            
            case BinOp(op, e1, e2):
                v1 = self.eval_expr(e1, env)
                v2 = self.eval_expr(e2, env)
                
                return self.abstract_binop(op, v1, v2)
            
            case _:
                return Top()
    
    def abstract_binop(self, op: str, v1: AbstractValue, v2: AbstractValue) -> AbstractValue:
        """抽象二元操作"""
        
        if isinstance(v1, Bottom) or isinstance(v2, Bottom):
            return Bottom()
        
        if isinstance(v1, Top) or isinstance(v2, Top):
            return Top()
        
        if isinstance(v1, Interval) and isinstance(v2, Interval):
            return self.interval_binop(op, v1, v2)
        
        return Top()
    
    def interval_binop(self, op: str, i1: Interval, i2: Interval) -> AbstractValue:
        """区间算术"""
        
        lo1, hi1 = i1.lo, i1.hi
        lo2, hi2 = i2.lo, i2.hi
        
        # 处理无穷
        if lo1 == float('-inf') or hi1 == float('inf'):
            return Top()
        if lo2 == float('-inf') or hi2 == float('inf'):
            return Top()
        
        if op == '+':
            return Interval(lo1 + lo2, hi1 + hi2)
        elif op == '-':
            return Interval(lo1 - hi2, hi1 - lo2)
        elif op == '*':
            products = [lo1*lo2, lo1*hi2, hi1*lo2, hi1*hi2]
            return Interval(min(products), max(products))
        
        return Top()

# Widening
class Widening:
    """用于终止的widening操作符"""
    
    @staticmethod
    def widen_interval(i1: Interval, i2: Interval) -> Interval:
        """Widen区间"""
        
        lo = i1.lo if i2.lo >= i1.lo else float('-inf')
        hi = i1.hi if i2.hi <= i1.hi else float('inf')
        
        return Interval(lo, hi)
    
    @staticmethod
    def widen_sign(s1: Sign, s2: Sign) -> AbstractValue:
        """Widen符号"""
        
        # 如果两者已知且相等, 保持
        if s1.sign == s2.sign:
            return s1
        
        return Top()

抽象域

域	元素	操作
符号	-, 0, +	lub, glb
区间	[l, u]	+, -, *
多面体	线性约束	交集
关系	数值关系	并集、交集
指针	点对集	别名

Widening

def widening_fixpoint(transition, initial, widening, max_iterations=1000):
    """使用widening计算固定点"""
    
    prev = initial
    curr = initial
    
    for i in range(max_iterations):
        curr = transition(prev)
        
        # 应用widening
        curr = widening(prev, curr)
        
        if curr.less_or_equal(prev):
            return curr
        
        prev = curr
    
    return curr  # 可能未收敛

关键概念

概念	描述
Galois连接	具体/抽象之间的 α ↔ γ
健全性	过近似
Widening	强制终止
固定点	稳定状态

提示

• 选择合适的抽象域
• 对循环应用widening
• 平衡精度与速度
• 验证健全性

相关技能

• dataflow-analysis-framework - 数据流
• invariant-generator - 不变量生成
• symbolic-execution-engine - 符号执行

规范参考

参考	为何重要
Cousot & Cousot, “Abstract Interpretation” (POPL 1977)	建立框架的基础论文
Cousot, “Theoretical Basis for Abstract Interpretation”	数学基础
Nielson, Nielson & Hankin, “Principles of Program Analysis”	静态分析综合教科书
Graf & Saidi, “Construction of Abstract State Graphs”	谓词抽象
Blazy, Leroy, et al., “Formal Verification of a C Value Analysis Based on Abstract Interpretation” (SAS 2013)	Coq中的验证抽象解释器

权衡与限制

域权衡

域	精度	成本	使用示例
符号	低	O(1)	除零检测
区间	中	O(1)	数组边界
多面体	高	昂贵	关系不变量
八边形	中-高	适中	数值分析

何时不使用抽象解释

• 用于可判定分析: 考虑有限状态模型检查
• 用于路径敏感分析: 考虑符号执行
• 用于过程间: 需要调用字符串或分析总结技术

复杂度分析

• 时间复杂度: 通常 O(f × n) 其中 f = 转移函数复杂度, n = 程序大小
• 空间复杂度: O(d × n) 其中 d = 抽象域大小 × 程序点数量
• Widening: 保证终止但可能失去精度
• 工作列表算法: 通常比朴素迭代收敛更快

限制

• 不精确: 设计如此 (过近似); 可能产生假阳性
• 域选择关键: 错误域 = 无用分析
• 过程间分析: 显著更复杂
• 健全性负担: 必须分析所有路径; 部分分析不健全

评估标准

高质量抽象解释器应具备:

标准	需要关注的点
健全性	从不遗漏真实bug (无假阴性)
精度	假阳性少
终止	正确使用widening
效率	可扩展到大型程序
域	适合目标属性
模块性	易于添加新域

质量指标

✅ 好: 健全、终止、域精度适当 ⚠️ 警告: 边缘情况不健全、域不精确 ❌ 差: 遗漏真实bug (不健全)、不终止

研究工具与工件

工业级抽象解释器:

工具	组织	可学习内容
Astrée	AbsInt	工业C静态分析
Facebook Infer	Facebook/Meta	组合分离逻辑
Frama-C	CEA/Inria	C验证平台
Polyspace	MathWorks	工业静态分析
Clang Static Analyzer	LLVM	源码级分析
PA研究工具	多种	学术原型

学术工具

• APRON - 数值抽象域库
• ELINA - 数值分析的机器学习
• PHA - 多面体分析器
• Juliet (NIST) - 静态分析器测试套件

研究前沿

1. 抽象域

• 目标: 更精确的过近似
• 当前: 多面体、八边形、区域、同余
• 研究: 模板多面体 (Sankaranarayanan et al.), 缩减积
• 挑战: 精度与性能

2. 概率程序的抽象解释

• 目标: 分析随机性程序
• 技术: 概率关系推理、分布语义
• 论文: “Abstract Interpretation of Probabilistic Programs” (Minks)
• 应用: 机器学习验证、安全

3. 非终止分析

• 目标: 证明程序不永远循环
• 技术: 排名函数、循环总结
• 论文: “Proving Non-Termination” (Gupta et al.)
• 工具: AProVE (终止证明器)

4. 并发执行

• 目标: 结合具体和符号执行
• 技术: 路径合并、符号简化
• 论文: “DART: Directed Automated Random Testing” (Godefroid et al.)
• 工具: KLEE, Manticore, S2E

实现陷阱

陷阱	实际后果	解决方案
不健全	遗漏真实bug	跟踪所有路径, 总是并集
非终止	分析挂起	每个循环应用widening
不精确	太多假阳性	选择更好域
路径爆炸	指数增长	总结、增量
堆建模	指针分析bug	仔细选择别名域

"Widening是微妙"问题

Widening必须正确应用否则失去精度:

# 朴素widening - 失去精度
def widen(i1, i2):
    if i2.lo < i1.lo: lo = -inf
    if i2.hi > i1.hi: hi = +inf
    return Interval(lo, hi)

# 更好 - 仅在增长时widening
def widen(i1, i2):
    lo = i1.lo if i2.lo >= i1.lo else float('-inf')
    hi = i1.hi if i2.hi <= i1.hi else float('inf')
    return Interval(lo, hi)

"路径敏感"权衡

更精确但昂贵:

# 路径不敏感 (更便宜)
if x > 0: y = x  # y: [1, +inf]
else: y = -x     # y: [1, +inf]
# 并集: y: [1, +inf]

# 路径敏感 (昂贵)  
if x > 0: y = x  # Then-分支: y: [1, +inf]
else: y = -x     # Else-分支: y: [1, +inf]
# 保持分离状态!