1. 从“跑一遍看看”说起具体执行为什么值得单独拎出来讲刚接触形式化方法那会儿我对“具体执行”这个词是有点不屑的。程序跑一遍看看结果这不是最基础的操作吗写个测试用例输入几个值看输出对不对这有什么好讲的后来踩的坑多了才明白具体执行Concrete Execution在形式化方法体系里远不止“跑一遍”这么简单。它是整个形式化验证链条的起点和锚点是抽象解释、符号执行、模型检测这些高级技术的参照系。你后面做的所有抽象、推理、证明最终都要回到具体执行上来对账——如果具体执行这一层就搞错了上面盖的楼全是空中楼阁。这篇文章想聊的就是形式化方法里 Part A 这个位置上的具体执行。它是什么、为什么它被放在第一部分、它和后面那些听起来更高级的技术是什么关系、实际做项目时怎么把它用扎实。适合两类人看一类是刚开始学形式化方法、被各种抽象概念绕晕的朋友另一类是在工程里做程序分析、测试、验证想搞清楚“形式化到底怎么落地”的从业者。我会尽量少堆术语多用实际写代码、跑程序时会遇到的场景来解释。先给一个最直白的定义具体执行就是给定一个程序和一个具体的输入一组确定的初始状态按照程序的语义一步一步走得到确定的执行轨迹和最终结果。这里的“具体”是相对于“符号”和“抽象”而言的——输入是具体的值不是符号表达式状态是具体的不是抽象域里的元素。听起来像废话但正是这种“确定性”和“可复现性”让它成为整个形式化方法大厦的地基。为什么 Part A 要讲这个因为形式化方法的核心目标是“证明程序在所有可能输入下都满足某个性质”。但“所有可能输入”是个无穷集合你不可能真的跑完。所以你需要一套办法从有限的具体执行出发去推断无穷的行为。具体执行就是那个“有限”的起点。你得先能精确地描述一次执行发生了什么才能去谈“所有执行”会怎样。这就像学数学先学算术再学代数跳过算术直接搞代数符号你都认识但意义你把握不住。2. 具体执行到底“具体”在哪拆开来看它的四个要素2.1 程序状态从变量到内存的完整快照具体执行的第一步是搞清楚“状态”是什么。一个程序在任意时刻的状态可以理解成一张完整的快照所有变量的当前值、程序计数器下一条要执行的指令位置、调用栈的内容、堆内存里对象的布局、甚至文件描述符和网络连接的状态。在形式化方法里我们通常会把状态建模成一个从变量名到值的映射记作 σ。比如 σ {x ↦ 3, y ↦ 5, pc ↦ 7}表示变量 x 是 3y 是 5下一条执行第 7 行。这里有个容易忽略的点状态的粒度取决于你的分析目标。如果你只关心数值计算那把整数变量建模好就够了如果你要分析并发程序那线程调度状态、锁的持有情况都必须进状态如果你做内存安全验证那堆上的对象图和指针关系就是状态的核心。我见过不少初学者一上来就想建一个“万能状态模型”结果复杂度爆炸什么都分析不了。正确的做法是先明确你要验证什么性质再决定状态里放什么。具体执行阶段的状态建模宁可窄一点、精确一点也不要宽而模糊。2.2 执行步一条指令如何改变状态有了状态下一步就是定义“执行步”——也就是一条指令如何把当前状态变成下一个状态。在形式化方法里这通常用一个转移关系来描述记作 σ → σ读作“从状态 σ 执行一步到达状态 σ”。对于一条赋值语句x x 1转移关系就是如果当前 σ 里 x 的值是 v那么 σ 就是把 x 映射到 v1、其他变量保持不变的新状态。这个转移关系的定义必须精确到不留歧义。举个例子x x 1在 C 语言里和在某些函数式语言里语义就不一样C 里是原地修改函数式语言里可能是绑定新值。再比如整数溢出C 的有符号整数溢出是未定义行为那你的转移关系在溢出时应该怎么定义是报错、是回绕、还是进入一个特殊状态这些细节在具体执行阶段就必须定死因为后面所有推理都依赖它。我个人的经验是转移关系的定义要跟着语言的官方语义走不要自己发明。如果语言标准说溢出是未定义行为那你的形式化模型里就应该有一个明确的“未定义”状态而不是偷偷让它回绕。2.3 执行轨迹一串状态连起来的故事单个执行步是原子操作把很多步连起来就得到一条执行轨迹Execution Traceσ₀ → σ₁ → σ₂ → ... → σₙ。这条轨迹就是“具体执行”的完整记录。σ₀ 是初始状态由具体输入决定σₙ 是终止状态如果程序能终止的话。轨迹这个概念在调试和验证里都极其有用。调试时你看的就是轨迹哪一步之后变量变成了意外的值哪一步走进了不该走的分支。验证时轨迹是你要推理的对象你想证明“对所有可能的初始状态所有轨迹的终止状态都满足性质 P”。注意这里的量词结构——“对所有初始状态”和“所有轨迹”这就是为什么具体执行只是起点它只给你一条轨迹而验证要管所有轨迹。2.4 终止与发散不是所有执行都会停下来具体执行还有一个绕不开的问题程序可能不终止。一个while(true){}的具体执行就是无限长的轨迹永远不会到达终止状态。在形式化方法里这被称为发散Divergence。处理发散是具体执行语义定义里的一个关键决策你是把发散建模成一个特殊的“底”状态记作 ⊥还是允许轨迹是无穷的这两种做法各有道理。把发散建模成 ⊥ 的好处是状态空间是完整的每个执行要么到终止状态要么到 ⊥便于做归纳推理。允许无穷轨迹的好处是更贴近实际语义尤其是做活性Liveness性质验证时无穷轨迹是必须的。我在实际项目里的选择是如果只关心安全性Safety性质用 ⊥ 建模发散更省事如果要验证“程序最终会做某事”这类活性性质就必须保留无穷轨迹。这个选择会影响你后面所有工具和证明策略的选型所以在 Part A 阶段就要想清楚。3. 为什么具体执行是形式化方法的第一块基石3.1 它是抽象解释和符号执行的“地面真值”抽象解释Abstract Interpretation和符号执行Symbolic Execution是形式化方法里两个重量级技术。抽象解释把具体状态抽象成抽象域里的元素比如用区间 [1, 10] 来概括所有可能的值符号执行把具体输入换成符号变量用路径约束来描述执行。这两个技术听起来比具体执行高级得多但它们正确性的最终判据都是具体执行。抽象解释的可靠性要求是抽象域里的每个元素都必须“覆盖”它对应的所有具体状态。这个“覆盖”关系怎么定义就是靠具体执行的语义。符号执行的路径约束求解出来的解必须对应一条真实的具体执行轨迹否则就是假阳性。所以你看具体执行是整个技术栈的语义基准。基准错了上面全错。这也是为什么形式化方法的教材和课程几乎无一例外把具体执行放在最前面讲——它不是最简单的部分而是最根本的部分。3.2 它让“程序行为”这个模糊概念变得可操作“程序行为”这个词平时说起来很顺口但真要严格定义很多人会卡壳。具体执行给了我们一个可操作的定义程序的行为就是它所有可能的具体执行轨迹的集合。这个定义的好处是它把“行为”这个抽象概念化归成了“轨迹集合”这个数学对象。一旦变成集合你就可以做集合运算求交、求并、包含判断。验证“程序满足性质 P”就变成了“所有轨迹的终止状态都在 P 定义的集合里”。这个化归是形式化方法能成为“方法”的关键一步。没有它验证就只是“我觉得没问题”有了它验证就是“我证明了这个集合包含关系成立”。而具体执行就是构造这个集合的原材料。3.3 它暴露了“未定义行为”和“环境交互”这些硬骨头写代码的人都知道程序的行为不只取决于代码本身还取决于运行环境输入数据、内存布局、调度顺序、外部设备的响应。具体执行把这些因素都摆到台面上逼你在建模时做决定。比如一个读取未初始化变量的程序它的具体执行是什么是读到某个任意值还是直接崩溃C 标准说这是未定义行为那你的形式化模型就必须显式地处理这个“未定义”。我见过很多项目在具体执行阶段偷懒把未定义行为当成“不会发生”或者“随便给个值”结果后面做验证时证明出来的结论在实际运行中根本不成立。未定义行为不是边缘情况它是形式化验证必须正面处理的中心问题。Part A 讲具体执行很大程度上就是让你在最早的时候把这些硬骨头啃下来而不是留到后面变成定时炸弹。4. 动手实现一个最小具体执行器从零到能跑4.1 语言选型和整体架构要真正理解具体执行最好的办法是自己写一个最小实现。我选一个极简的命令式语言只有赋值、条件、循环、顺序执行这几种结构变量都是整数。用 Python 来写解释器因为 Python 的字典天然适合表示状态映射代码量能控制在两百行以内逻辑清晰。整体架构分三块语法树定义、状态表示、执行引擎。语法树用类来表示每个节点有一个eval方法接收当前状态返回新状态。状态就是一个 Python 字典键是变量名值是整数。执行引擎负责从初始状态出发反复调用根节点的eval直到状态不再变化终止或者检测到发散。这个架构的好处是语义和实现一一对应语法树的每个节点对应一条语言的语法结构eval方法对应转移关系执行引擎对应轨迹生成。你写完之后对“具体执行”的每个概念都会有肌肉记忆。4.2 状态和转移关系的代码落地先定义状态。我用一个简单的类包一下字典方便加一些辅助方法class State: def __init__(self, mappingNone): self.vars dict(mapping) if mapping else {} self.pc 0 # 程序计数器这里简化处理 def get(self, name): return self.vars.get(name, 0) # 未初始化默认为 0实际项目要处理未定义 def set(self, name, value): new_state State(self.vars) new_state.vars[name] value new_state.pc self.pc 1 return new_state def __repr__(self): return fState({self.vars}, pc{self.pc})注意set方法返回的是新状态不是原地修改。这是有意为之具体执行的轨迹是一串不可变的状态每一步都产生新状态旧状态保留。这样你才能完整回放轨迹做调试和验证。如果原地修改轨迹就丢了。然后是语法树节点。赋值节点class Assign: def __init__(self, name, expr): self.name name self.expr expr def eval(self, state): value self.expr.eval(state) return state.set(self.name, value)表达式节点这里只展示加法和变量引用class Var: def __init__(self, name): self.name name def eval(self, state): return state.get(self.name) class Add: def __init__(self, left, right): self.left left self.right right def eval(self, state): return self.left.eval(state) self.right.eval(state)条件节点和顺序节点class If: def __init__(self, cond, then_branch, else_branch): self.cond cond self.then_branch then_branch self.else_branch else_branch def eval(self, state): if self.cond.eval(state) ! 0: return self.then_branch.eval(state) else: return self.else_branch.eval(state) class Seq: def __init__(self, first, second): self.first first self.second second def eval(self, state): intermediate self.first.eval(state) return self.second.eval(intermediate)循环节点是最需要小心的。我用一个While节点它的eval会反复执行循环体直到条件为假。为了防止无限循环我加一个步数上限class While: def __init__(self, cond, body, max_steps10000): self.cond cond self.body body self.max_steps max_steps def eval(self, state): steps 0 current state while self.cond.eval(current) ! 0: current self.body.eval(current) steps 1 if steps self.max_steps: raise RuntimeError(Possible divergence: step limit exceeded) return current这个max_steps就是处理发散的一种实用手段用步数上限来近似“发散”。超过上限就报错提示可能不终止。实际的形式化工具里这个上限要么是用户指定的要么是通过更精细的终止性分析来判定的。4.3 跑一条完整轨迹并打印出来有了这些节点就可以构造一个程序并执行了。比如计算x 1; y 2; while (x 5) { y y * x; x x 1; }program Seq( Assign(x, Const(1)), Seq( Assign(y, Const(2)), While( LessThan(Var(x), Const(5)), Seq( Assign(y, Mul(Var(y), Var(x))), Assign(x, Add(Var(x), Const(1))) ) ) ) ) initial State() final program.eval(initial) print(final)跑出来最终状态是{x: 5, y: 48}。你可以手动验算一下x 从 1 到 4y 依次乘 1、2、3、4初始 y2所以 2×1×2×3×4 48。对上了。但光看最终状态不够我想看轨迹。改一下执行引擎让它记录每一步的状态def execute_with_trace(program, initial): trace [initial] current initial # 这里需要把 eval 改成逐步执行简化起见用递归展开 # 实际实现里可以用生成器或者显式栈 ...完整实现会稍长但思路是把eval从“直接返回最终状态”改成“每执行一步就 yield 一个状态”然后用一个列表收集。这样你就能打印出完整的执行轨迹看到 x 和 y 每一步怎么变。这个轨迹就是具体执行的产物也是后面做符号执行时路径约束的来源。5. 具体执行和符号执行、抽象解释的边界在哪5.1 一张表看清三者的分工维度具体执行符号执行抽象解释输入具体值符号变量具体状态集合状态具体状态符号状态 路径约束抽象域元素输出一条轨迹路径条件集合不变式覆盖单条路径多条路径受约束求解限制所有路径受抽象域限制精度精确路径内精确保守近似代价低中到高中典型用途测试、调试、语义基准漏洞挖掘、测试生成编译优化、静态验证这张表的核心信息是具体执行是精度最高、代价最低、但覆盖最窄的技术。它精确到每一步但只能覆盖一条路径。符号执行和抽象解释都是在“覆盖”和“精度”之间做权衡。理解这个权衡你就理解了形式化方法的技术版图。5.2 什么时候该用具体执行什么时候不该具体执行最适合的场景是你需要一个确定的、可复现的参照。比如你写了一个抽象解释器想验证它是否可靠那就拿具体执行的结果来对账抽象域里的结果必须包含具体执行的结果。再比如你做符号执行求解出来的测试输入必须能真的跑出一条具体轨迹来否则就是假阳性。不该用具体执行的时候也很明确当你需要覆盖大量输入空间时。具体执行一次只走一条路输入空间大了根本跑不过来。这时候就得上符号执行或者抽象解释。但注意这不是说具体执行就没用了——即使在上层技术里具体执行仍然作为“具体化”步骤存在符号执行求解出具体输入后还是要跑一遍具体执行来确认。5.3 一个常见的误解具体执行等于测试很多人把具体执行和测试划等号这是个误解。测试是“选一组输入跑程序看结果”具体执行是“给定输入按语义走一遍得到轨迹”。测试是具体执行的一种应用但具体执行本身是语义层面的概念不依赖于“选输入”这个动作。在形式化方法里具体执行更多是作为语义定义的一部分而不是测试活动的一部分。你可以不跑任何测试但仍然在形式化模型里定义具体执行语义。这个区分很重要因为它决定了你把具体执行放在“验证方法”里还是“语义基础”里。Part A 的定位是后者。6. 实操中容易踩的坑和排查清单6.1 状态建模的粒度陷阱最常见的坑是状态建模太粗或太细。太粗比如只建模几个关键变量其他变量忽略那你的具体执行轨迹可能和真实程序对不上后面所有推理都失去意义。太细比如把每个临时变量、每个寄存器都建模状态空间爆炸执行一步要处理几百个字段效率极低。我的经验法则是状态里只放“影响你要验证的性质”的变量以及“影响控制流”的变量。其他变量如果只是中间计算不影响最终性质可以合并或者抽象掉。但合并的时候要小心确保合并后的状态仍然能精确地驱动控制流。这个平衡点需要根据具体项目调没有万能公式。6.2 循环和递归的终止性处理循环和递归是具体执行里最容易出问题的地方。一个没写好的循环可能让你的执行器卡死。除了前面说的步数上限还有几种处理方式一是做简单的终止性分析比如循环变量单调递增且有上界就认为会终止二是用“燃料Fuel”机制给每个循环分配固定的执行预算用完就停三是把循环展开固定次数超过就当作发散。我实际用下来步数上限加清晰的报错信息是最实用的。报错信息里要包含当前状态和已经执行的步数方便你判断是真发散还是上限设小了。千万别静默地返回一个错误结果那比崩溃还糟糕。6.3 未定义行为的显式建模前面提过未定义行为这里展开说。以整数除零为例很多语言里x / 0是未定义行为。在你的具体执行器里如果直接让 Python 抛ZeroDivisionError那你的形式化模型就和语言标准不一致了。正确的做法是在转移关系里显式定义一个“未定义”状态当执行到除零时转移到这个状态并记录原因。class Div: def eval(self, state): left self.left.eval(state) right self.right.eval(state) if right 0: return UndefinedState(reasondivision by zero, previousstate) return left // right这样你的轨迹里就会出现一个明确的“未定义”节点后面做验证时你可以选择把包含未定义状态的轨迹排除掉或者单独分析。显式建模未定义行为是形式化方法区别于“随便跑跑”的关键标志。6.4 常见问题速查表现象可能原因排查方向解决建议执行结果和预期不符状态建模遗漏变量对比真实程序的所有变量补全影响控制流和性质的变量执行器卡死循环无终止或上限过大打印每步状态看是否在循环加步数上限检查循环条件轨迹中间状态异常转移关系定义有歧义对照语言标准逐条检查显式定义边界情况溢出、除零发散误报上限设太小看报错时的步数和状态调大上限或做终止性分析未定义行为被忽略转移关系没处理边界检查所有可能出错的运算加 UndefinedState 分支这张表是我自己踩坑踩出来的基本上覆盖了具体执行器开发中 80% 的问题。每次遇到新问题先往这张表里对对不上再深入分析。7. 把具体执行用扎实几个工程上的实用建议7.1 轨迹要可回放、可序列化具体执行产生的轨迹不要只存在内存里。把它序列化成 JSON 或者类似的格式存到文件里。好处有三个一是调试时可以反复回放不用重新跑二是可以和别人共享别人能精确复现你的执行三是可以作为回归测试的基准每次改完执行器跑一遍旧轨迹看结果是否一致。序列化的格式我一般用{steps: [{pc: 0, vars: {...}}, ...], result: terminated | diverged | undefined}。简单直接人也能读。7.2 给执行器加断言和不变式检查在具体执行的过程中可以插入断言检查。比如你预期某个变量在执行过程中永远不为负那就在每次状态更新后检查一下如果为负就报错并打印轨迹。这个机制在调试复杂程序时特别有用能帮你快速定位是哪一步开始偏离预期的。断言检查的代价是执行变慢所以生产环境可以关掉但开发和验证阶段一定要开。具体执行的价值很大程度上在于它能精确地告诉你“哪一步错了”断言就是把这个价值放大。7.3 和测试框架结合但别混为一谈具体执行器可以很方便地和测试框架结合把测试用例的输入喂给执行器把执行结果和预期对比。但记住这只是具体执行的一个应用。在形式化方法的语境里具体执行更重要的是作为语义基准而不是测试工具。我见过一些团队把具体执行器当成测试工具用结果忽略了它在语义定义上的作用后面做符号执行时发现语义对不上返工成本很高。建议的做法是把具体执行器分成两层底层是纯语义的执行引擎上层是测试适配层。底层不依赖任何测试框架只负责按语义走轨迹上层负责读测试用例、对比结果、生成报告。这样底层可以复用到符号执行、抽象解释的验证里不会被测试框架绑死。7.4 文档化你的语义决策具体执行阶段做的每一个语义决策——状态里放什么、转移关系怎么定义、发散怎么处理、未定义行为怎么建模——都要写下来。不是写在代码注释里而是单独写一份语义说明文档。这份文档是后面所有工作的合同符号执行、抽象解释、模型检测都要以这份文档为准。如果后面发现语义定义有问题改文档然后同步改所有实现。我自己的习惯是语义文档用表格加伪代码的形式写每个语言结构一行左边是语法右边是转移规则。这样一目了然也方便和语言标准对照。8. 从具体执行出发下一步往哪走具体执行跑通了轨迹能打印了语义决策也文档化了接下来自然要问然后呢答案取决于你的目标。如果你想验证安全性性质下一步是抽象解释把具体状态抽象成抽象域元素然后计算不变式。如果你想找漏洞下一步是符号执行把具体输入换成符号变量收集路径约束然后求解。如果你想做模型检测下一步是把具体执行语义编码成状态转移系统然后用模型检测算法搜索。但不管往哪走具体执行都是你的参照系。抽象解释的结果要包含具体执行的结果符号执行的解要能跑出具体执行的轨迹模型检测找到的反例要能对应一条具体执行。具体执行是形式化方法里的“米原器”所有其他技术都要和它对齐。我个人在实际项目里的体会是具体执行这一层花的时间永远不亏。你在这里多花一天把语义抠清楚后面就少花一周去修因为语义不一致导致的 bug。形式化方法听起来高深但它的力量恰恰来自这种对基础的较真。Part A 讲具体执行讲的就是这种较真。最后分享一个小技巧如果你觉得自己的具体执行器行为诡异但又说不清哪里不对就找一个最简单的程序——比如只有一条赋值语句——跑一遍把轨迹打印出来和手工计算的结果逐字段对比。如果最简单的都对不上那问题一定在状态建模或转移关系上不在复杂的控制流上。这个“最小可复现”的排查思路我在形式化方法里用了无数次几乎每次都能快速定位问题。
