用 Ruby 进行程序分析

程序分析

方法

程序分析（Program Analysis）

目的

不执行程序，也能知道：会不会崩溃、有没有漏洞、逻辑对不对、性能瓶颈在哪
常见目标：- 找 Bug / 空指针、数组越界、死循环
查安全漏洞：缓冲区溢出、SQL 注入、内存泄漏
做优化：编译器优化、死代码删除、并行化
做验证：证明程序满足某种规范（如无溢出、符合协议）

按照是否实际执行程序分为两类，实际中可以结合使用。

静态分析（Static Analysis）
- 不运行程序，只看源码/字节码/二进制
- 优点：覆盖广、早发现、成本低
- 缺点：可能误报（假阳性）、难以处理复杂控制流
- 例子：Clang Static Analyzer、SonarQube、FindBugs、Coverity
动态分析（Dynamic Analysis）
- 程序运行时收集信息
- 优点：准确、几乎无误报
- 缺点：只能测到跑到的路径，覆盖率有限
- 例子：ASan（内存检测）、Valgrind、gdb 调试、性能 profiling、fuzz

核心方法，注意和具体应用结合。

控制流图 CFG：把程序画成“节点=语句，边=跳转”的图
数据流分析 DFA：沿着 CFG 传播信息（变量在哪定义、在哪使用）。具体可以用来。
指针分析：搞清楚指针到底指向谁
抽象解释：用“抽象值”代替真实值，做可靠但保守的推断
符号执行：用符号代替具体输入，自动推导路径条件
模型检验：穷举状态空间，验证是否满足性质（如“不会死锁”）

补充

控制流分析
指针分析
函数间分析。
指针分析
污点分析

典型应用场景

编译器优化（LLVM/GCC 内部大量使用）
代码质量门禁（CI/CD 自动扫描）
漏洞挖掘与渗透测试
智能合约安全审计（Solidity 静态分析）
恶意代码分析、逆向工程
并发程序死锁检测

难点

精度 vs 效率：分析越准越慢
指针、并发、动态特性（反射/JNI/动态加载）很难精确分析
误报率高，工程上要做大量降噪

~~你想往哪个方向聊？我可以展开：~~

~~基础概念（CFG/数据流/符号执行）~~
~~工具实战（Clang、LLVM Pass、Frida、Angr）~~
~~学术方向（论文、抽象解释、模型检验）~~
~~应用方向（漏洞挖掘、智能合约分析、逆向）~~

用途：
1. 编译器优化（寄存器分配、公共子表达式、死代码）
2. 普通 Bug 检测（空指针、越界、未初始化、内存泄漏）
3. 安全漏洞（污点分析、SQLi、XSS、命令注入、隐私泄露）
4. 程序理解（程序切片、依赖分析、逆向、二进制分析）

例子：

画一个污点分析的数据流传递函数
写一段极简 CFG + 数据流迭代求解的演示代码
用 LLVM Pass 实现一个数据流分析

应用

~~数据流分析（Data Flow Analysis, DFA）~~

~~数据流分析 = 在控制流图 CFG上，沿着执行路径传播信息，算出程序在每个程序点的保守信息。~~
~~它是静态分析的基石。~~

举一些引用的例子。

编译器优化：

可达定义分析（Reaching Definitions） - 算：某个变量的定义，能到达程序哪一行 - 用途：- 死代码消除 - 变量替换、优化 - 检测未初始化变量
活跃变量分析（Live Variable Analysis） - 算：变量在某行之后是否还会被使用 - 用途：- 寄存器分配（编译器核心） - 检测无用赋值 - 优化掉死存储
可用表达式分析（Available Expressions） - 算：某个表达式在到达该点前是否已经计算过 - 用途：- 公共子表达式消除 - 冗余计算优化
非常忙表达式（Very Busy Expressions） - 算：离开该点后表达式一定会被用到 - 用途：- 代码提升、循环优化

找 Bug、查漏洞

空指针检测 - 数据流跟踪： ptr = null; → 沿路径传播“可能空”信息 - 找到： ptr->field 这种危险点
数组越界 / 缓冲区溢出 - 跟踪数组下标变量的取值范围 - 判断是否可能超出数组长度
内存泄漏 / 双重释放 - 跟踪 malloc/free 状态：- 已分配 / 已释放 / 未知 - 发现：只 malloc 不 free、free 两次
未初始化变量使用 - 跟踪变量是否被定义过 - 若在任何路径上未定义就使用 → 报 Bug
资源泄漏（文件句柄、锁、socket） - 类似内存泄漏 - 跟踪 fopen/fclose、lock/unlock

安全领域：污点分析（Taint Analysis）

污点传播分析 - 标记外部输入为污点：- argv 、网络包、表单数据、文件读入 - 沿着赋值、函数调用、指针传播污点 - 检测污点是否流入危险函数：- system() 、 exec - SQL 查询 - 日志输出、XSS 输出用途： - SQL 注入检测 - XSS 漏洞检测 - 命令注入 - 敏感数据泄露
隐私泄露分析 - 跟踪身份证、手机号、经纬度等敏感数据 - 看是否未经加密就发送到网络

代码质量与重构类分析

死代码检测 - 哪些语句永远不会执行到 - 哪些变量赋值后再也不用
函数副作用分析 - 函数是否修改全局变量 - 是否写文件、发网络 - 用于：编译器优化、并行化、缓存优化
循环不变量检测 - 循环内哪些计算结果不变，可以提到循环外 - 编译器优化常用
指针别名分析（Alias Analysis） - 两个指针是否可能指向同一块内存 - 是几乎所有优化、漏洞检测的基础依赖

程序理解、逆向、二进制分析

控制依赖 + 数据依赖分析 - 构建程序依赖图（PDG） - 用于：- 程序切片 - 逆向分析逻辑 - 漏洞定位
程序切片（Program Slicing） - 只保留影响某变量的代码 - 用途：- 调试 - 代码精简 - 逆向分析恶意代码
二进制层面数据流 - 不需要源码，在汇编/IR 上做 - 用于：- 恶意软件行为分析 - 漏洞挖掘（Angr、BinaryNinja 内部都用）

并发程序相关

数据竞争检测 - 跟踪共享变量读写 - 看是否存在无锁并发访问
死锁检测 - 跟踪锁的获取顺序 - 发现循环等待

类型检查

类型系统

无类型 λ 演算

只有项（term），没有类型。
一切都是函数：λx.x、(λx.x)y

简单类型 λ 演算

语法
- 基类型：bool, nat, …
- 函数类型：σ → τ
- 项：变量、λ 抽象、应用
类型规则
- 抽象：x:σ ⊢ M:τ ⇒ ⊢ (λx:σ.M): σ→τ
- 应用：M:σ→τ, N:σ ⇒ M N: τ
对应直觉主义命题逻辑（Curry–Howard 同构）

System F

新增能力
- 可以对类型变量进行抽象：Λα.λx:α.x
- 类型：∀α. α→α
- 可以实例化：(Λα.λx:α.x)[nat] ⇒ λx:nat.x
对应二阶直觉主义逻辑

System Fω

在 System F 基础上加入类型算子（type operator），即： - 类型可以作为 “函数”，接受类型参数生成新类型。
例如： - List : * → * - Functor : (* → *) → *
层级：
- 项：值
- 类型：*
- 种类（kind）：对类型分类，如 * → *
支持高阶多态

依赖类型

核心：
- 类型可以依赖项 ∀x:nat. P(x)
- 项可以依赖类型多态
- 类型和项在同一语法世界里
对应高阶直觉主义逻辑

其他类型系统

Hindley–Milner（HM） - ML、OCaml、Haskell 的核心 - 基于 System F 子集 - 支持全局类型推导，无需写类型注解
CIC（归纳构造演算） - CoC（构造演算） + 归纳类型 - Coq 的理论根基

参考资料

类型推断

Hindley–Milner 类型系统
推理规则

变量（Var）： $\frac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau}$
抽象（Abs）： $\frac{\Gamma, x : \tau_1 \vdash e : \tau_2}{\Gamma \vdash \lambda x. e : \tau_1 \to \tau_2}$
应用（App）： $\frac{\Gamma \vdash e_1 : \tau_1 \to \tau_2 \quad \Gamma \vdash e_2 : \tau_1}{\Gamma \vdash e_1 e_2 : \tau_2}$
Let 多态（Let-Poly）： $\frac{\Gamma \vdash e_1 : \sigma \quad \Gamma, x : \sigma \vdash e_2 : \tau}{\Gamma \vdash \text{let } x = e_1 \text{ in } e_2 : \tau}$，其中 $\sigma$ 是类型模式（$\forall \alpha. \tau$）。
实例化（Inst）： $\frac{\Gamma \vdash e : \forall \alpha. \tau}{\Gamma \vdash e : \tau[\alpha := \tau’]}$
泛化（Gen）： $\frac{\Gamma \vdash e : \tau \quad \alpha \notin \text{ftv}(\Gamma)}{\Gamma \vdash e : \forall \alpha. \tau}$，其中 $\text{ftv}(\Gamma)$ 是 $\Gamma$ 中的自由类型变量。

Hindley–Milner 类型推断的核心算法就叫 W 算法（Algorithm W）。

不仅仅是单向的，是在解等式约束，可以有类型变量。
实现 type_of/infer 函数，类型变量可以用编号，也可以用对象。
参考 OCaml 代码的实现，下面代码仍然有 bug。

# 代码有 bug。
require 'sxp'

$type_variable_counter = 0

def new_type_variable 
  :"t#{$type_variable_counter+=1}"
end

def free_vars(type)
  case type
  in :int | :bool then []
  in Symbol then [type] #  if type=~/^t\d+$/
  in [:'->', param_type, return_type] then free_vars(param_type) | free_vars(return_type)
  else []
  end
end

def apply_subst(subst, type)
  case type
  in Symbol then subst.fetch(type, type)
  in [:'->', param_type, return_type] then [:'->', apply_subst(subst, param_type), apply_subst(subst, return_type)]
  else type
  end
end

def unify(type1, type2, subst)
  type1_applied = apply_subst(subst, type1)
  type2_applied = apply_subst(subst, type2)
  
  return subst if type1_applied == type2_applied
  p [:test, type1_applied, type2_applied]
  case [type1_applied, type2_applied]
  in [Symbol => type_var, other_type] if type_var=~/^t\d+$/
    raise "循环类型" if free_vars(other_type).include?(type_var)
    subst.merge(type_var => other_type)
  in [other_type, Symbol => type_var] if type_var=~/^t\d+$/
    unify(type_var, other_type, subst)
  in [[:'->', *xs], [:'->',*ys]]
    xs.zip(ys).each do |param1, param2|
      subst = unify(param1, param2, subst)
    end
    subst
  # in [[:'->', param1, ret1], [:'->', param2, ret2]]
  #   subst1 = unify(param1, param2, subst)
  #   ret1_applied = apply_subst(subst1, ret1)
  #   ret2_applied = apply_subst(subst1, ret2)
  #   unify(ret1_applied, ret2_applied, subst1)
  else
    p [type1, type2]
    raise "unification fail: #{type1_applied} != #{type2_applied}"
  end
end

def generalize(type_env, type)
  env_free_vars = type_env.values.flat_map { |schema| free_vars(schema[2]) }.uniq
  [:forall, free_vars(type) - env_free_vars, type]
end

def instantiate(schema)
  case schema
  in [:forall, type_vars, inner_type]
    p schema
    subst = type_vars.to_h { |var| [var, new_type_variable] }
    apply_subst(subst, inner_type)
  else
    schema
  end
end

def apply_subst_to_env(subst, type_env)
  type_env.transform_values { |schema|
  if schema.is_a?(Array) && schema.first == :forall
    [:forall, schema[1], apply_subst(subst, schema[2])]
  else
    schema
  end 
  }
end

def type_of(expression, type_env, subst)
  case expression
  in Integer
    [:int, subst]
  in true | false | :true | :false
    [:bool, subst]
  in Symbol
    p env: type_env.keys, expr: expression
    [instantiate(type_env.fetch(expression)), subst]
  in [:begin, *expressions]
    type = nil
    expressions.each do |expr|
      type, subst = type_of(expr, type_env, subst)
    end
    [type, subst]
  in [:lambda, [param], body]
    fresh_var = new_type_variable
    body_type, subst1 = type_of(body, type_env.merge(param => fresh_var), subst)
    [[:'->', apply_subst(subst1, fresh_var), body_type], subst1]
  in [func_expr, *xs] if func_expr!=:let # apply
    p func_expr: func_expr, subst: subst, env: type_env
    func_type, subst = type_of(func_expr, type_env, subst)
    p func_type: func_type, subst: subst
    arg_types = xs.map{|e|
      e_type, subst = type_of(e, apply_subst_to_env(subst, type_env), subst)
      e_type
    }
#    arg_type, subst = type_of(arg_expr, apply_subst_to_env(subst, type_env), subst)
    func_type_applied = apply_subst(subst, func_type) # 这行需要么？
    p func_type_applied: func_type_applied, subst: subst
    return_type_var = new_type_variable
    subst = unify(func_type_applied, [:'->', *arg_types, return_type_var], subst)
    [apply_subst(subst, return_type_var), subst]
  in [:let, var_name, expr1, expr2]
    type1, subst1 = type_of(expr1, type_env, subst)
    env1 = apply_subst_to_env(subst1, type_env)
    schema = generalize(env1, type1)
    type2, subst2 = type_of(expr2, env1.merge(var_name => schema), subst1)
    [type2, subst2]
  end
end

def run(code)
  expr = SXP.read(code)
  env = {
    :true => :bool, 
    :false => :bool,
    :+ => [:'->', :int, :int, :int],
  }
  type, _ = type_of(expr, env, {})
  puts "🎉type: #{type}"
  puts
end

# ------------------------------------------------------------------------------
# 测试
# ------------------------------------------------------------------------------
run "42" # 整数类型
run "true" # 布尔类型
run "(+ 1 2)"
run "(lambda (x) x)" # lambda
run "((lambda (x) x) 42)" # apply
run "(let id (lambda (x) x) (begin (id 42) (id true)))" # let 多态
run "(lambda (id) (begin (id 42) (id true))) (lambda (x) x))" rescue p $! # 故意报错



# run "(let id (lambda (x) x) (let f (lambda (y) (id y)) f))"
# run "(let id (lambda (x) x) (id true))"
# run "(lambda (x) (lambda (y) x))"
# run "((lambda (x) (lambda (y) x)) 42)"
# run "(let k (lambda (x) (lambda (y) x)) ((k 1) 2))"
# run "(lambda (f) (lambda (g) (lambda (x) (f (g x)))))"
# run "(let id (lambda (x) x) (let const (lambda (y) (lambda (z) y)) (const id)))"
# run "(let x 1 (let y 2 (let z 3 x)))"
# run "(let b true (let f (lambda (x) b) (f false)))"

    

动态分析

代码覆盖

属于动态分析，需要执行代码并做记录。

Ruby 本身没有直接“按行插装记录执行行”的内置方法，但可以通过 Ruby 的元编程特性、内置的追踪工具和代码解析能力来实现这个需求。下面我会给你介绍几种最实用的方案，从简单到进阶，都基于 Ruby 自带的功能。

使用 set_trace_func（Ruby 内置），能捕获代码执行的每一个事件（如行执行、方法调用、类定义等），可以直接用来记录执行过的代码行，以及执行轨迹。

# 定义追踪器：记录执行过的代码行
trace_log = []

# 设置追踪函数
set_trace_func lambda { |event, file, line, id, binding, classname|
  # 只关注 "line" 事件（代码行执行），过滤掉其他事件（如call/return等）
  if event == 'line'
    # 跳过追踪器自身的代码（避免无限递归）
    return if file == __FILE__ && line.between?(1, 20) # 根据实际行数调整

    # 读取当前执行行的代码内容
    begin
      code_line = File.readlines(file)[line - 1]&.strip
    rescue Errno::ENOENT
      code_line = "无法读取文件: #{file}"
    end

    # 记录关键信息：文件、行号、代码内容
 trace_log << { file: file, line: line, code: code_line, timestamp: Time.now }

    # 实时打印（也可以只存日志不打印）
    puts "[执行行] #{file}:#{line} | #{code_line}"
  end
}

# ========== 测试代码（你要追踪的逻辑）==========
def test_method
  a = 10
  b = 20
  c = a + b
  puts "结果: #{c}"
end

test_method

# ========== 停止追踪并输出日志 ==========
set_trace_func nil # 关闭追踪

puts "\n===== 执行记录汇总 ====="
trace_log.each do |log|
  puts "#{log[:file]}:#{log[:line]} - #{log[:code]}"
end

使用内置的 Coverage 库，统计每行执行次数，不包括执行顺序，可以计算得到覆盖率。也支持分支覆盖和方法覆盖。

require 'coverage'

# 启动覆盖率统计（:line 表示按行统计）
Coverage.start #(lines: true)

# ========== 要追踪的代码 ==========
def foo
  a = 1
  b = 2
  if a > b
    puts "a 更大"
  else
    puts "b 更大"
  end
end

foo

# ========== 停止统计并输出结果 ==========
p result = Coverage.result

# 解析结果：key 是文件路径，value 是 {行号: 执行次数}
result.each do |file, lines|
  puts "\n文件: #{file}"
  lines.each do |line_num, count|
    next if count.nil? # nil 表示该行不存在/未执行
    # 读取行内容
    code = File.readlines(file)[line_num - 1]&.strip
    puts "行 #{line_num}: #{count > 0 ? "执行过(#{count}次)" : "未执行"} | #{code}"
  end
end

输出效果

b 更大

文件: test.rb
行 3: 执行过(1次) | def foo
行 4: 执行过(1次) | a = 1
行 5: 执行过(1次) | b = 2
行 6: 执行过(1次) | if a > b
行 7: 未执行 | puts "a 更大"
行 8: 执行过(1次) | else
行 9: 执行过(1次) | puts "b 更大"
行 10: 执行过(1次) | end
行 11: 执行过(1次) | end
行 14: 执行过(1次) | foo

~~关键注意事项~~

~~set_trace_func 会追踪所有代码行（包括 Ruby 内置库），需要过滤掉不需要的文件（如 Ruby 标准库路径）；~~
~~Coverage 库只统计“是否执行”和“执行次数”，无法实时记录执行顺序；~~

插桩会影响代码执行性能，仅用于调试/测试环境，不要在生产环境启用。

总结

快速追踪执行行：用 set_trace_func，Ruby 内置、无需额外依赖，适合简单场景；
统计执行行覆盖率：用 Coverage 库（Ruby 2.5+），专门用于行执行次数统计；
精准插装特定代码：用 RubyVM::InstructionSequence 解析代码，结合元编程自定义插装逻辑。

~~这三种方案都基于 Ruby 自带功能，无需安装任何 gem，可根据你的具体需求（实时记录/统计次数/精准控制）选择。~~

静态分析

指针分析

数据流分析

到达定值分析
到达定值分析（Reaching Definitions Analysis）静态确定程序中每个变量的赋值（定值）能到达哪些后续使用点。

~~是编译原理中最基础、最重要的前向数据流分析（Forward Data-Flow Analysis） 技术之一。它的核心作用是~~

根据 AST 构建控制流图 CFG ，得到基本块、赋值语句。

核心概念

定值 (Definition)：指任何可能为变量赋值的语句（如 x = 5、x = y + z）。
到达 (Reaching)：如果从定值 d 之后存在一条路径到达程序点 p，且路径上没有对同一变量的其他赋值（即 d 未被“杀死”），则称 d 到达 p。
赋值语句
- 杀死 (Kill)：对同一变量的新赋值，会“杀死”该变量之前的所有旧定值。
- 生成 (Gen)：一条赋值语句会生成一个新的定值。

基本原理与公式

分析方向：前向分析（从程序入口到出口）
交汇操作 (Meet)：并集 (Union)（只要一条路径能到达，就认为可达）
数据流方程：
- 入口 (IN)：一个基本块入口处的定值集合，等于其所有前驱基本块出口定值的并集。$in[B] = \bigcup_{\text{前驱} P} out[P]$
- 出口 (OUT)：一个基本块出口处的定值集合，等于入口定值集杀死该块内定义变量的旧定值，再生成该块内的新定值。$out[B] = (in[B] - kill[B]) \cup gen[B]$

特点总结

类型：May 分析（保守估计，可能存在误报，但无漏报）
复杂度：多项式时间，高效可解
应用：编译器优化、程序静态分析、软件漏洞检测

主要用途

常量传播 (Constant Propagation) 若变量在某点只有一个定值（常量），可直接替换。
公共子表达式消除 判断两处表达式是否使用相同变量定值，避免重复计算。
死代码删除 若定值后无任何使用，可删除该语句。
循环优化 识别循环不变量（定值在循环外）。
调试与缺陷检测 检测未初始化变量（使用点无任何定值到达）。

~~要不要我帮你用一段简单的C代码（比如包含分支和循环）做一次完整的到达定值分析，一步步算出 IN 和 OUT 集合？~~

~~下面我给你一套可直接运行的方案：用 Ruby + sxp 库解析 Scheme 表达式，做基础数据流分析（ reaching definitions 到达定值分析）。~~

解析 Scheme S-表达式，提取变量定义与使用，做到达定值数据流分析。

# gem install sxp
require 'sxp'

# 辅助：从表达式中收集变量定义与使用
def collect_def_use(expr, defs = [], uses = [])
  case expr
  when Symbol
    uses << expr
  when Array
    case expr[0]
    when :set!
      # (set! var val)
      var = expr[1]
      defs << var
      collect_def_use(expr[2], defs, uses)
    when :define
      # (define var val)
      var = expr[1]
      defs << var
      collect_def_use(expr[2], defs, uses) if expr.size > 2
    else
      expr.each { |e| collect_def_use(e, defs, uses) }
    end
  end
  { defs: defs.uniq, uses: uses.uniq }
end

# 到达定值数据流分析
def reaching_definitions(instructions)
  # 每条指令: { expr:, def:, use: }
  blocks = instructions.map do |expr|
    du = collect_def_use(expr)
    { expr: expr, def: du[:defs], use: du[:uses] }
  end

  # 初始化 in/out
  in_arr = Array.new(blocks.size) { Set.new }
  out_arr = Array.new(blocks.size) { Set.new }

  # 迭代不动点
  changed = true
  while changed
    changed = false

    blocks.each_with_index do |blk, i|
      old_out = out_arr[i].dup

      # in[n] = union(out[pred])
      if i > 0
        in_arr[i] = out_arr[i-1].dup
      else
        in_arr[i] = Set.new
      end

      # out[n] = (in[n] - kill[n]) ∪ gen[n]
      kill = blk[:def].to_set
      gen = blk[:def].map { |v| [v, i] }.to_set

      out_arr[i] = (in_arr[i] - kill) + gen

      changed = true if out_arr[i] != old_out
    end
  end

  { blocks: blocks, in: in_arr, out: out_arr }
end

# 示例 Scheme 代码
scheme_code = <<~SCHEME
  (define a 1)
  (set! a (+ a 2))
  (define b (* a 3))
SCHEME

# 1. 用 sxp 解析
ast = SXP.read scheme_code
puts "=== 解析后的 AST ==="
pp ast

# 2. 数据流分析
result = reaching_definitions(ast)

# 3. 输出结果
puts "\n=== 到达定值分析结果 ==="
result[:blocks].each_with_index do |blk, i|
  puts "指令 #{i}:"
  puts "  表达式: #{blk[:expr].inspect}"
  puts "  def: #{blk[:def].inspect}"
  puts "  use: #{blk[:use].inspect}"
  puts "  in: #{result[:in][i].to_a.inspect}"
  puts "  out: #{result[:out][i].to_a.inspect}"
  puts
end

reaching_definitions
遍历 AST，收集每条语句： - def 被赋值的变量 - use 被引用的变量
标准数据流迭代算法： - 按照方向更新 - in[n] =进入节点前可达的定值 - out[n] =离开节点后可达的定值 - 迭代到不动点为止

扩展成完整工具链：

控制流图 CFG 构建
活跃变量分析（liveness analysis）
常量传播 / 常量折叠
编译优化（删除无用赋值）
直接输出 IR 或汇编

~~你现在是想做教学演示，还是要真正写一个 Scheme 编译器前端？我可以按你的方向帮你精修。~~

控制流分析

对于 lambda 类似于指针分析。

程序验证

要验证 {Pre} S {Post} 正确，只需证明 Pre ⇒ WP(S, Post) 用 Z3 检查 Not(Pre → WP(S, Post)) 为不可满足（unsat），即找不到反例。

用 SXP 库解析 lisp 字符串
支持： skip / 赋值 := / 顺序 seq / if / while
基于最弱前置条件 WP
用 Z3 求解验证
循环语句循环不变式

先装依赖：

gem install sxp
gem install z3
apt install libz3-dev

下面是完整可运行代码，直接复制就能跑：

require 'sxp'
require 'z3'

# -----------------------------------------------------------------------------
# 1. 替换函数 Q[e/x]
# -----------------------------------------------------------------------------
def substitute(expr, x, e)
  case expr
  when Symbol then
    expr == x ? e : expr
  when Array then
    expr.map { |child| substitute(child, x, e) }
  else
    expr
  end
end

# -----------------------------------------------------------------------------
# 2. S表达式 转 Z3 表达式
# -----------------------------------------------------------------------------
def sxp_to_z3(expr)
  case expr
  when Integer
    expr
  when Symbol
    Z3.Int(expr.to_s)
  when Array
    op, *args = expr
    z3_args = args.map { |a| sxp_to_z3(a) }
    case op
    when :+ then z3_args.reduce(:+)
    when :- then z3_args.reduce(:-)
    when :* then z3_args.reduce(:*)
    when :'/' then z3_args.reduce(:/)
    when :> then z3_args[0] > z3_args[1]
    when :>= then z3_args[0] >= z3_args[1]
    when :< then z3_args[0] < z3_args[1]
    when :<= then z3_args[0] <= z3_args[1]
    when :== then z3_args[0] == z3_args[1]
    when :'=' then z3_args[0] == z3_args[1]
    when :!= then z3_args[0] != z3_args[1]
    when :implies then Z3.Implies(z3_args[0], z3_args[1])
    when :and then z3_args.reduce(:&)
    when :'||' then z3_args.reduce(:|)
    when :not then !z3_args[0]
    else raise "不支持运算符: #{op}"
    end
  else
    expr
  end
end
 

# -----------------------------------------------------------------------------
# 3. 最弱前置条件 WP 计算（核心）
# -----------------------------------------------------------------------------

def wp(stmt, post, vcs)
  case stmt
  in [:skip]
    post
  in [:set, x, e]
    # wp(x := e, Q) = Q[e/x]
    substitute(post, x, e)
  in [:seq, s1, s2]
    # wp(S1;S2, Q) = wp(S1, wp(S2, Q))
    wp(s1, wp(s2, post, vcs), vcs)
  in [:seq, *stmts]
    # wp(S1;S2;...;Sn, Q) = wp(S1, wp(S2, ..., wp(Sn, Q)...))
    stmts.reverse.reduce(post) { |acc, s| wp(s, acc, vcs) }
  in [:if, b, s1, s2]
    # wp(if b then S1 else S2, Q) = (b → wp(S1,Q)) ∧ (¬b → wp(S2,Q))
    wp1 = wp(s1, post, vcs)
    wp2 = wp(s2, post, vcs)
    [:and, [:implies, b, wp1], [:implies, [:not, b], wp2]]
  in [:while, b, inv, body]
    # wp(while b do S, Q) = I
    # 其中 I 是循环不变式，需要用户提供
    # 生成验证条件：
    # 1. 不变式初始化：inv
    # 2. 归纳：inv ∧ b → wp(body, inv)
    # 3. 退出：inv ∧ ¬b → post
    # 注意 2 和 3 有隐含的 forall。
    # vcs << inv
    puts "循环不变式是 #{inv}"
    vcs << [:implies, [:and, inv, b], wp(body, inv, vcs)]
    vcs << [:implies, [:and, inv, [:not, b]], post]
    
    inv
  else
    raise "不支持语句: #{stmt}"
  end
end
 
SXP.write wp(SXP.read("(set x (+ x 1))"), SXP.read("(> x 5)"), [])
SXP.write wp(SXP.read("(seq (set x 1) (set y (+ x 2)))"), SXP.read("(= y 3)"), [])
SXP.write wp(SXP.read("(if (> x 0) (set y x) (set y (- 0 x)))"), SXP.read("(> y 0)"), [])
SXP.write wp(SXP.read("(seq (set x 1) (set y 2) (set z (+ x y)))"), SXP.read("(= z 3)"), [])
puts "==="
stmt4 = SXP.read("(seq (set sum 0) (set i 1) (while (<= i n) (and (= sum (/ (* (- i 1) i) 2)) (<= 1 i) (<= i (+ n 1))) (seq (set sum (+ sum i)) (set i (+ i 1)))))")
post4 = SXP.read("(= sum (/ (* n (+ n 1)) 2))")
vcs4 = []
SXP.write wp(stmt4, post4, vcs4)
puts "==="
#p vcs4
SXP.write vcs4

# exit

# -----------------------------------------------------------------------------
# 4. 验证条件检查（使用 Z3）
# -----------------------------------------------------------------------------
def check_valid(formula)
  solver = Z3::Solver.new
  SXP.write(formula)
  solver.assert(!sxp_to_z3(formula))
  solver.check
  !solver.satisfiable?
end
# -----------------------------------------------------------------------------
# 5. 整体验证入口
# -----------------------------------------------------------------------------
def verify(pre_sxp, prog_sxp, post_sxp)
  puts "=" * 60
  puts "📌 前置条件 P: #{pre_sxp}"
  puts "📌 程序: #{prog_sxp}"
  puts "📌 后置条件 Q: #{post_sxp}"
  puts "=" * 60

  vcs = []
  wp = wp(prog_sxp, post_sxp, vcs)
  vcs.unshift [:implies, pre_sxp, wp]
  
  puts "\n🔍 生成验证条件："
  all_ok = true
  
  SXP.write(vcs)
  vcs.each_with_index do |vc, i|
    puts "VC#{i+1}:"
    if check_valid(vc)
      puts "✅ 成立"
    else
      puts "❌ 不成立"
      all_ok = false
    end
  end

  puts "\n" + (all_ok ? "🎉 验证通过！" : "⚠️ 验证失败！")
end

 

# -----------------------------------------------------------------------------
# 6. 从 SXP 字符串解析 + 示例（while 求和）
# -----------------------------------------------------------------------------
if __FILE__ == $0
  # SXP 字符串：
  # 计算 1+2+...+n，i从1到n，sum累加
  sxp_str = <<~SXP
    (seq
      (set sum 0)
      (set i 1)
      (while (<= i n)
        (and (= sum (/ (* (- i 1) i) 2)) (<= 1 i) (<= i (+ n 1)))
        (seq
          (set sum (+ sum i))
          (set i (+ i 1))
        )
      )
    )
  SXP

  prog = SXP.read(sxp_str)
  pre = SXP.read("(< 1 n)") # [:<=, 1, :n]
#  post = [:==, :sum, [:/, [:* ,:n, [:+, :n, 1]], 2]]
  post = SXP.read("(== sum (/ (* n (+ n 1)) 2))")
  verify(pre, prog, post)
end

支持的语法（SXP 格式）

(skip)
(:= x e)
(seq S1 S2)
(if b S1 S2)
(while b INV S) 带循环不变式

示例功能

这个例子验证的是：

pre: 1 ≤ n
prog: sum=0; i=1; while(i≤n) { sum=sum+i; i=i+1; }
post: sum = n*(n+1)/2

~~完全是标准程序验证 + WP + Z3范式。~~

~~你接下来想让我帮你：~~
1. ~~再写一个 if + while 混合的例子？~~

还是解释一下循环不变式怎么写。

符号执行

用ruby 的 sxp 库，参照 A Peer Architecture for Lightweight Symbolic Execution 这篇论文，实现一个对 scheme 语言做符号执行的工具。

符号执行是静态方法，但是通常用动态执行来获得一个外部调用的执行结果。
对于条件分支（if语句和while语句）每次探索一条执行分支，每次执行路径条件取值不同。
可以用直接递归时复制然后追加条件，也可以维护一个 stack。

论文和工具（因为是动态语言，参考一些对针对 Python 的工作）

Deconstructing Dynamic Symbolic Execution：实现了 PyExZ3
A Peer Architecture for Lightweight Symbolic Execution：利用反射在执行中获得路径条件。
PySymEx

核心语句

思路1：同时走不同的分支，需要复制整个环境。

  def handle_if(s_expr, env, pc) # 第三个参数是路径条件
    cond_expr, then_expr, else_expr = s_expr[1], s_expr[2], s_expr[3]
    cond_val = execute_s_expr(cond_expr, env, pc) # 执行条件表达式
    cond_bool = cond_val.to_boolean_expr          # 转换为Z3布尔表达式

    # 处理then分支：添加 cond = true 约束
    then_pc = pc.clone
    then_pc.add_constraint(cond_bool)
    if then_pc.satisfiable?
      execute_s_expr(then_expr, env.child, then_pc)
      @paths << then_pc
    end

    # 处理else分支：添加 cond = false 约束
    else_pc = pc.clone
    else_pc.add_constraint(Z3.not(cond_bool))
    if else_pc.satisfiable?
      execute_s_expr(else_expr, env.child, else_pc)
      @paths << else_pc
    end
  end

思路2：保存条件语句的条件序列，每次走不同的分支。

class BoolProxy < SymbolicProxy
  @@path = []
  @@cond = []

  def self.reset; @@path = []; @@cond = []; end
  def self.path; @@path; end

  # 反射：Ruby 条件判断自动调用 !
  def !
    BoolProxy.new(Z3.not(@expr))
  end

  # 核心：控制条件分支路径
  # 反射：条件分支自动触发
  def to_bool
    t = Z3.sat? Z3.and(*@@cond, @expr)
    f = Z3.sat? Z3.and(*@@cond, Z3.not(@expr))
	# 强制分支（只有一条可行）
    return true  if t && !f
    return false if f && !t
	# 深度限制
    raise 'depth' if @@path.size >= 10
	# 按预设路径执行
    if @@path.size > @@cond.size
      b = @@path[@@cond.size]
      @@cond << (b ? @expr : Z3.not(@expr))
      return b
    end
	# 默认走 true 分支
    @@path << true
    @@cond << @expr
    true
  end
end

# ========== 符号执行引擎：路径循环 ==========
module PeerCheck
  def self.sym = IntProxy.new(SMT.var)

  def self.run(fn, *args)
    loop do
      BoolProxy.reset
      fn.call(*args) rescue puts "⚠️ 异常: #{$!}"

      # 回溯分支：移除已探索的 false 分支
      while !@@path.empty? && !@@path.last
        @@path.pop
      end
      break if @@path.empty?
      # 翻转最后一个分支
      @@path[-1] = false
    end
  end
end

~~参考资料~~

Symbolic Execution of Python Programs with PyExZ3 (2013) The paper Deconstructing Dynamic Symbolic Execution explains the basic ideas behind dynamic symbolic execution and the architecture of the PyExZ3 tool (as of git tag v1.0). Bruni, Disney and Flanagan wrote about encoding symbolic execution for Python in Python in the same way in their 2008 paper A Peer Architecture for Lightweight Symbolic Execution - they use proxies rather than multiple inheritance for representing symbolic versions of Python types.
~~PySymEx: Symbolic Execution for Python Programs (2021)~~

require 'sxp'
require 'z3'
require 'set'

# 1. 符号值封装类：区分具体值和Z3符号值，重载基本运算
class SymbolicValue
  attr_reader :value, :is_symbolic

  def initialize(value, is_symbolic: false)
    @value = value          # 具体值（Numeric）或Z3表达式
    @is_symbolic = is_symbolic # 是否为符号值
  end

  # 重载基本算术/比较运算，支持符号计算
  def +(other)
    op(:add, other)
  end

  def -(other)
    op(:sub, other)
  end

  def *(other)
    op(:mul, other)
  end

  def ==(other)
    op(:eq, other)
  end

  def >(other)
    op(:gt, other)
  end

  def <(other)
    op(:lt, other)
  end

  # 转换为Z3布尔表达式（用于路径约束）
  def to_boolean_expr
    @is_symbolic ? @value : Z3.bool_val(@value)
  end

  # 辅助：统一处理运算逻辑
  private def op(z3_op, other)
    if @is_symbolic || other.is_symbolic
      z3_expr = Z3.send(z3_op, @value, other.value)
      SymbolicValue.new(z3_expr, is_symbolic: true)
    else
      SymbolicValue.new(@value.send(z3_op == :eq ? :== : z3_op, other.value))
    end
  end

  def to_s
    @is_symbolic ? "Symbolic(#{@value})" : "Concrete(#{@value})"
  end
end

# 2. 路径条件类：管理Z3约束，支持分支克隆和可满足性检查
class PathCondition
  attr_reader :solver, :constraints

  def initialize(parent_solver = nil)
    @solver = Z3::Solver.new
    # 继承父路径的约束（分支时克隆）
    parent_solver&.assertions&.each { |a| @solver.assert(a) }
    @constraints = []
  end

  # 添加约束到路径条件
  def add_constraint(expr)
    @constraints << expr
    @solver.assert(expr)
  end

  # 检查约束是否可满足
  def satisfiable?
    @solver.check == Z3::Sat
  end

  # 获取符号变量的可行值模型
  def model
    @solver.model if satisfiable?
  end

  # 克隆路径条件（用于分支执行）
  def clone
    new_pc = PathCondition.new(@solver)
    new_pc.instance_variable_set(:@constraints, @constraints.dup)
    new_pc
  end
end

# 3. Scheme环境类：维护变量绑定，支持作用域嵌套
class SymbolicEnv
  def initialize(parent = nil)
    @bindings = {}  # 变量绑定表 { symbol => SymbolicValue/Proc }
    @parent = parent # 父环境（支持嵌套作用域）
  end

  # 定义变量
  def define(name, value)
    @bindings[name.to_sym] = value
  end

  # 查找变量（递归查找父环境）
  def lookup(name)
    sym = name.to_sym
    @bindings.fetch(sym) do
      @parent&.lookup(sym) || raise("Undefined variable: #{name}")
    end
  end

  # 创建子环境
  def child
    SymbolicEnv.new(self)
  end
end

# 4. 核心符号执行器：处理Scheme S表达式
class SymbolicExecutor
  attr_reader :paths

  def initialize
    @global_env = SymbolicEnv.new # 全局环境
    @paths = []                   # 存储所有可行路径
    setup_builtins               # 预定义Scheme内置函数
  end

  # 预定义Scheme内置函数（+、-、*、比较等）
  def setup_builtins
    builtins = {
      :+ => ->(a, b) { a + b },
      :- => ->(a, b) { a - b },
      :* => ->(a, b) { a * b },
      :'=' => ->(a, b) { a == b },
      :> => ->(a, b) { a > b },
      :< => ->(a, b) { a < b }
    }
    builtins.each { |name, fn| @global_env.define(name, fn) }
  end

  # 定义符号变量（绑定到全局环境）
  def define_symbolic_var(name, type: :int)
    z3_var = case type
             when :int then Z3.int(name)
             when :bool then Z3.bool(name)
             else Z3.int(name)
             end
    @global_env.define(name, SymbolicValue.new(z3_var, is_symbolic: true))
  end

  # 解析并执行Scheme代码
  def execute(scheme_code)
    s_expr = SXP::Reader.parse(scheme_code) # 解析为S表达式
    initial_pc = PathCondition.new         # 初始路径条件（无约束）
    execute_s_expr(s_expr, @global_env.child, initial_pc)
    @paths.select(&:satisfiable?) # 过滤不可满足的路径
  end

  # 递归执行S表达式
  private def execute_s_expr(s_expr, env, pc)
    case s_expr
    when Symbol  # 变量引用（如 x）
      env.lookup(s_expr)
    when Numeric # 具体数值（如 5）
      SymbolicValue.new(s_expr)
    when Array   # 复合表达式（如 (if (> x 5) (+ x 1) (- x 1))）
      handle_complex_expr(s_expr, env, pc)
    else         # 其他字面量（如字符串）
      SymbolicValue.new(s_expr)
    end
  end

  # 处理复合表达式（if/lambda/函数调用等）
  private def handle_complex_expr(s_expr, env, pc)
    case s_expr.first
    when :define # (define var val)：变量定义
      var, val_expr = s_expr[1], s_expr[2]
      val = execute_s_expr(val_expr, env, pc)
      env.define(var, val)
      val
    when :if     # (if cond then else)：条件分支（核心路径探索）
      handle_if(s_expr, env, pc)
    when :lambda # (lambda (params) body)：lambda表达式（简化版闭包）
      params, body = s_expr[1], s_expr[2]
      ->(*args) {
        lambda_env = env.child
        params.zip(args).each { |p, a| lambda_env.define(p, a) }
        execute_s_expr(body, lambda_env, PathCondition.new)
      }
    when :quote  # (quote expr)：直接返回字面量
      s_expr[1]
    else         # 函数调用（如 (+ x 1)）
      handle_function_call(s_expr, env, pc)
    end
  end

  # 处理if分支：克隆路径条件，探索正反分支
  private def handle_if(s_expr, env, pc)
    cond_expr, then_expr, else_expr = s_expr[1], s_expr[2], s_expr[3]
    cond_val = execute_s_expr(cond_expr, env, pc) # 执行条件表达式
    cond_bool = cond_val.to_boolean_expr          # 转换为Z3布尔表达式

    # 处理then分支：添加 cond = true 约束
    then_pc = pc.clone
    then_pc.add_constraint(cond_bool)
    if then_pc.satisfiable?
      execute_s_expr(then_expr, env.child, then_pc)
      @paths << then_pc
    end

    # 处理else分支：添加 cond = false 约束
    else_pc = pc.clone
    else_pc.add_constraint(Z3.not(cond_bool))
    if else_pc.satisfiable?
      execute_s_expr(else_expr, env.child, else_pc)
      @paths << else_pc
    end
  end

  # 处理函数调用
  private def handle_function_call(s_expr, env, pc)
    fn = execute_s_expr(s_expr[0], env, pc)       # 解析函数
    args = s_expr[1..-1].map { |a| execute_s_expr(a, env, pc) } # 解析参数
    fn.call(*args) if fn.is_a?(Proc)              # 执行函数
  end

  # 打印所有可行路径
  def print_paths
    puts "\n=== 符号执行结果：共 #{@paths.size} 条可行路径 ==="
    @paths.each_with_index do |pc, i|
      puts "\n路径 ##{i+1}:"
      puts "约束条件：#{pc.constraints.map(&:to_s).join(' ∧ ')}"
      next unless pc.satisfiable?
      puts "可行值模型："
      pc.model.each { |var, val| puts "  #{var} = #{val}" }
    end
  end
end

# ===================== 示例：执行Scheme代码 =====================
if __FILE__ == $0
  # 示例1：简单条件分支（符号变量x）
  executor1 = SymbolicExecutor.new
  executor1.define_symbolic_var(:x, type: :int) # 定义符号变量x（整数）
  scheme_code1 = <<~SCHEME
    (if (> x 5)
        (+ x 1)   ; then分支：x>5时执行
        (- x 1))  ; else分支：x≤5时执行
  SCHEME
  puts "执行Scheme代码：\n#{scheme_code1}"
  executor1.execute(scheme_code1)
  executor1.print_paths

  # 示例2：嵌套分支（符号变量a、b）
  executor2 = SymbolicExecutor.new
  executor2.define_symbolic_var(:a, type: :int)
  executor2.define_symbolic_var(:b, type: :int)
  scheme_code2 = <<~SCHEME
    (if (> a b)
        (if (= a 10)
            (+ a b)
            (- a b))
        (* a b))
  SCHEME
  puts "\n--- 分割线 ---"
  puts "执行Scheme代码：\n#{scheme_code2}"
  executor2.execute(scheme_code2)
  executor2.print_paths
end

PeerCheck 极简版

# PeerCheck 极简版
# PeerCheck 极简版
require 'z3'

# ========== SMT 接口 ==========
module SMT
  def self.var = Z3.Int("s#{rand(1000)}")
  def self.int(n) = n # Z3.int(n)
  def self.bool(b) = b # Z3.bool(b)
end

# ========== 统一代理基类：反射自动转发所有运算符 ==========
class SymbolicProxy
  attr_reader :expr

  def initialize(expr)
    @expr = expr
  end

  # 反射：自动捕获 + - * / == < > <= >= 等所有运算符
  def method_missing(name, *args)
    p method_missing:name
    return super unless %i[+ - * / == < > <= >=].include?(name)

    other = args.first
    rhs = other.is_a?(SymbolicProxy) ? other.expr : SMT.int(other)
    res = @expr.send(name, rhs)
    p res.class
    res.is_a?(Z3::BoolExpr) ? BoolProxy.new(res) : IntProxy.new(res)
  end
  def ==(other)
    return BoolProxy.new(Z3.Eq(@expr, SMT.int(other))).to_bool
  end

  # 反射：声明支持的运算符
  def respond_to_missing?(name, *)
    %i[+ - * / == < > <= >=].include?(name)
  end

  # 支持 1 + proxy 这种反向运算
  def coerce(other)
    [IntProxy.new(SMT.int(other)), self]
  end
end

# ========== 整数代理 ==========
class IntProxy < SymbolicProxy
end

$path = []
$cond = []
# ========== 布尔代理 + 路径控制 ==========
class BoolProxy < SymbolicProxy
 

  # 反射：Ruby 条件判断自动调用 !
  def !
    BoolProxy.new(Z3.not(@expr))
  end

  # 核心：控制条件分支路径
  # 反射：条件分支自动触发
  def to_bool
    p :to_bool
  #   t = Z3.sat? Z3.and(*$cond, @expr)
  #   f = Z3.sat? Z3.and(*$cond, Z3.not(@expr))
	# # 强制分支（只有一条可行）
  #   return true  if t && !f
  #   return false if f && !t
	# 深度限制
    raise 'depth' if $path.size >= 10
	# 按预设路径执行
    if $path.size > $cond.size
      b = $path[$cond.size]
      $cond << (b ? @expr : !@expr)
      return b
    end
	# 默认走 true 分支
    $path << true
    $cond << @expr
    true
  end
end

# ========== 符号执行引擎：路径循环 ==========
module PeerCheck
  def self.sym = IntProxy.new(SMT.var)

  def self.run(fn, *args)
    $path.clear
    loop do
      $cond.clear
      begin
      fn.call(*args) 
       rescue
        puts cond:$cond,path:$path
        solver = Z3::Solver.new
        solver.assert Z3.And(*$cond)
        if solver.satisfiable? 
          p solver.model
        end
        # raise # 
        puts "⚠️ 异常: #{$!}"
      end
      # 回溯分支：移除已探索的 false 分支
      while !$path.empty? && !$path.last
        $path.pop
      end
      break if $path.empty?
      # 翻转最后一个分支
      $path[-1] = false
    end
  end
end

# ========== 测试用例 ==========
def succ(x)
  raise "bug!" if x == 42768
  x + 1
end

def abs(x)
  x >= 0 ? x : -x
end
 
def quick_sort(arr)
  return arr if arr.size <= 1
  pivot = arr[0]
  less  = arr[1..].select { |v| v <= pivot }
  more  = arr[1..].select { |v| v > pivot }
  quick_sort(less) + [pivot] + quick_sort(more)
end

# 运行
PeerCheck.run(method(:succ), PeerCheck.sym)
PeerCheck.run(method(:abs), PeerCheck.sym)
p :ok

模型检验

CPS 变换

核心思路

原子表达式变换数字 / 变量：直接调用续延返回自身 scheme 原: 5 CPS: (k 5)
Lambda 函数变换给函数追加续延参数 k 函数体用自身的 k 做续延 scheme 原: (lambda (x) (+ x 1)) CPS: (lambda (x k) (+ x 1 k))
函数调用变换（核心）从右到左求值参数每个参数求值后，用临时变量接收结果，生成新续延最终调用 CPS 化的函数，传入最终续延 k scheme 原: (+ 1 2) CPS: (1 (lambda (t1) (2 (lambda (t2) (+ t1 t2 k)))))
嵌套表达式变换完美处理嵌套调用，自动生成链式续延： scheme 原: (+ (* 2 3) 4) CPS: (2 (lambda (t1) (3 (lambda (t2) (* t1 t2 (lambda (t3) (4 (lambda (t4) (+ t3 t4 k)))))))))

运行结果

require 'sxp'

# Scheme CPS 变换器
class CPS
  def initialize
    @tmp = 0
  end

  # 入口
  def convert(expr)
    cps(expr, [:lambda, [:v], :v])
  end

  private

  # 核心 CPS 变换
  def cps(expr, k)
    case expr
    # 原子：数字、符号
    when Numeric, Symbol
      [k, expr]

    # 列表表达式：lambda / if / call
    when Array
      head, *rest = expr

      case head
      when :lambda
        # lambda 变换
        params, body = rest
        new_params = params + [:k]
        new_body = cps(body, :k)
        [:lambda, new_params, new_body]

      when :if
        # if 条件表达式 CPS（核心新增）
        test, then_expr, else_expr = rest
        # 先求条件值，然后把 k 传给两个分支
        cps(test, [:lambda, [:test],
              [:if, :test,
               cps(then_expr, k),  # 为真 → 走 then 并调用续延 k
               cps(else_expr, k)   # 为假 → 走 else 并调用续延 k
              ]])

      else
        # 函数调用
        cps_call(expr, k)
      end
    end
  end

  # 函数调用 CPS（从右向左求值）
  def cps_call(call, k)
    func, *args = call
    return cps(func, k) if args.empty?

    tmp = new_tmp
    last_arg = args.pop
    new_call = [func, *args, tmp]

    cps(last_arg, [:lambda, [tmp], cps_call(new_call, k)])
  end

  # 生成临时变量 t1, t2...
  def new_tmp
    @tmp += 1
    "t#{@tmp}".to_sym
  end
end

# ==================== 测试工具 ====================
def test(input)
  puts "原始：#{input}"
  expr = SXP.read(input)
  cps_expr = CPS.new.convert(expr)
  puts "CPS：\n#{SXP.generate(cps_expr, indent: true)}"
  puts "=" * 70
end

# ==================== 测试用例 ====================
test "10"
test "(add1 5)"
test "(+ (* 2 3) 4)"
test "(lambda (x) (+ x 1))"

# if 表达式
test "(if x 10 20)"
test "(if (> x 0) x (- x))"
test "(if (even? n) (* n 2) (+ n 1))"

分析 Ruby 代码

AST

参考资料

有两本教材介绍了传统的方法：

用 Ruby 进行程序分析

程序分析

方法

应用

类型检查

类型系统

参考资料

类型推断

动态分析

代码覆盖

静态分析

数据流分析

控制流分析

程序验证

符号执行

模型检验

相关工具

datalog

调用 Z3

clang+llvm

CPS 变换

分析 Ruby 代码

参考资料

相关论文

符号执行