1. 从“跑一遍”到“算清楚”具体执行为什么值得单独拎出来讲形式化方法这四个字很多人第一次听到会觉得离自己很远像是学术论文里的东西。但只要你写过代码、调过Bug、做过测试你其实已经在跟它打交道了只是没意识到而已。形式化方法的核心思路是用数学化的手段描述系统应该怎么运行然后用工具去验证它是不是真的这么运行。而“具体执行”Concrete Execution就是这条链路里最接地气的一环——它不抽象、不推导、不证明就是拿着具体的输入值一步一步把程序跑一遍看看到底发生了什么。你可以把它理解成“带着记录仪的试车”。平时你开车只知道从A点到了B点中间发动机抖没抖、刹车踩了几脚、油耗多少全靠感觉。具体执行不一样它把每一个中间状态都记下来变量在每一步的值是什么、条件判断走了哪个分支、循环执行了多少次、内存里的数据怎么变的。这些信息在符号执行和模型检验里都是基础燃料没有它们后面的分析根本跑不起来。这篇文章适合谁看如果你是做软件测试、程序分析、嵌入式开发或者安全审计的具体执行是你绕不开的基本功。如果你是在校学生正在啃形式化方法这门课Part A 通常就是整个课程的第一道门槛把这部分吃透了后面符号执行、抽象解释、定理证明才不会听得云里雾里。哪怕你只是个普通开发者理解具体执行的思路也能让你在调试复杂逻辑时多一套系统化的方法而不是靠print大法到处碰运气。我见过太多人一上来就直奔符号执行结果连“路径约束怎么收集”都搞不明白根子就在具体执行这一层没打牢。所以这篇文章我会把具体执行拆开揉碎从设计思路到实操细节再到常见坑全部过一遍。你不需要有形式化方法的背景只要会写基本的代码就能跟上。2. 具体执行的整体设计与核心思路拆解2.1 具体执行到底在做什么一句话说清楚具体执行就是给定一个程序和一个具体的输入按照程序的语义一步一步执行记录每一步的状态变化。这里的“具体”是相对于“符号”而言的输入不是符号变量而是实实在在的数值比如x 5、name abc。因为输入是确定的所以程序的执行路径也是确定的不会出现分支爆炸的问题。这听起来好像没什么技术含量不就是跑程序吗但关键在于“记录”和“可控”。普通的运行只是看最终输出具体执行要的是中间过程。举个例子下面这段代码def foo(x, y): z x y if z 10: return z * 2 else: return z - 1如果你用foo(3, 4)去跑普通执行只告诉你结果是6。但具体执行会告诉你第一步x3, y4第二步z7第三步判断7 10为假走 else 分支第四步返回7 - 1 6。这些中间状态才是后续分析真正需要的东西。2.2 为什么不用普通调试代替具体执行有人可能会问我用调试器单步跟踪不就行了何必专门搞一套具体执行这个问题我当初也想过后来在实际项目里踩了坑才明白调试器和具体执行的目标完全不同。调试器是给人看的它的输出是给人类阅读的格式随意、不结构化。你单步十次看到的是一堆散乱的信息想把它喂给另一个分析工具几乎不可能。具体执行是给工具看的它的输出是结构化的状态序列每一步的变量绑定、路径条件、内存状态都有明确的格式可以直接被后续的符号执行引擎或者验证器消费。另一个区别是可控性。调试器依赖人工操作你点一下走一步。具体执行可以自动化给定输入就能批量跑跑完自动收集所有路径信息。在做大规模测试或者路径覆盖分析的时候这个差异是致命的。你不可能手动调试一万个测试用例但具体执行可以。还有一个容易被忽略的点具体执行可以处理“非标准语义”。比如在分析底层代码时你需要自定义某些指令的行为调试器通常不允许你改语义但具体执行框架可以。你可以告诉它“这条指令按我的规则来”这在分析特定领域的程序时非常有用。2.3 具体执行在形式化方法工具链中的位置把形式化方法的工具链想象成一条流水线最左边是源代码最右边是“程序满足某条性质”的结论。中间有好几个环节具体执行是排在最前面的那个。它的下游通常是符号执行。符号执行需要知道程序有哪些路径、每条路径上的约束是什么。这些信息从哪来就是从具体执行来的。你先用具体输入跑一遍记录下路径和状态然后符号执行引擎在此基础上把具体值替换成符号值开始推导。没有具体执行打底符号执行就是空中楼阁。再往 downstream 走是模型检验和定理证明。模型检验需要把程序转换成状态机而状态机的状态转移关系很大程度上依赖具体执行提供的状态序列。定理证明需要把程序语义形式化成逻辑公式具体执行记录的状态变化就是公式的实例化依据。所以你看具体执行虽然简单但它是整条链路的基石。基石的精度和完整性直接决定了上层分析的质量。我在实际项目里见过太多因为具体执行阶段记录不全导致后面符号执行漏路径、模型检验状态爆炸的案例。返工的成本远高于一开始就把这一层做扎实。2.4 设计具体执行引擎时的核心权衡自己动手写一个具体执行引擎或者选一个现成的框架来用都会面临几个关键权衡。我把它们列出来你在做技术选型的时候可以对照着看。第一个权衡是解释执行 vs 编译执行。解释执行就是写一个解释器逐条读取程序指令模拟它的行为。优点是灵活你可以随时插入记录逻辑改语义也方便。缺点是慢尤其是分析大规模程序的时候解释器的开销会让人抓狂。编译执行是把程序转换成某种中间表示然后直接在那个表示上跑。优点是快缺点是灵活性差想改语义就得改编译器。第二个权衡是状态记录的粒度。你可以只记录变量的值也可以连内存地址、栈帧、寄存器都记下来。粒度越细信息越全但存储开销越大。我一般建议根据下游需求来定如果只是做路径覆盖分析记录变量和分支条件就够了如果要做内存安全分析那必须把内存状态也记下来。第三个权衡是路径爆炸的处理。虽然具体执行的输入是确定的路径不会爆炸但如果你要做的是“多输入批量执行”那路径数量还是会随输入数量线性增长。这时候需要考虑并行化和状态剪枝。并行化好理解多开几个进程同时跑。状态剪枝是指如果两条路径在某个点之后完全一样就没必要重复记录。这个优化在实际项目里能省不少时间。3. 核心细节解析与实操要点3.1 程序状态的表示变量、内存和路径条件具体执行的核心是“状态”这个概念。一个状态至少包含三部分变量绑定、内存模型和路径条件。变量绑定就是当前所有活跃变量的值。比如x3, y4, z7。这部分通常用哈希表或者环境链表来实现。哈希表查询快但插入和删除慢环境链表适合处理作用域嵌套但查询慢。实际实现里常见的是两者的混合用链表维护作用域每个作用域内部用哈希表。内存模型稍微复杂一点。对于高级语言你可能只需要模拟堆和栈对于低级语言你得模拟整个地址空间。我建议初学者先从简单的开始把内存当成一个从地址到值的映射不要一上来就搞分页、缓存这些复杂的东西。等基本流程跑通了再逐步细化。路径条件是一组布尔表达式的合取。比如走到某一步时路径条件是x 0 y 10。这些条件在具体执行阶段是已知真假的因为输入是具体的。但记录下来之后到了符号执行阶段它们就变成了约束求解器的输入。所以具体执行阶段一定要把路径条件记全不能漏。注意路径条件的顺序很重要。有些约束求解器对条件的顺序敏感顺序不对可能导致求解时间暴涨。建议按照程序执行的先后顺序记录不要事后重排。3.2 指令语义的定义每条指令到底做了什么具体执行引擎需要为每一种指令定义语义。所谓语义就是“执行这条指令之后状态怎么变”。比如加法指令z x y语义就是读取x和y的值相加把结果写入z。听起来简单但实际实现的时候有很多细节。首先是类型处理。x和y可能是整数、浮点数、字符串甚至自定义对象。不同类型的加法语义完全不同。整数加法可能溢出浮点加法有精度问题字符串加法是拼接。你的引擎必须能区分这些情况否则执行结果就是错的。其次是指令的副作用。有些指令不只是改变量值还会改变控制流、抛出异常、修改全局状态。比如函数调用指令它会把当前状态压栈创建一个新状态执行完再恢复。这些副作用必须在语义定义里写清楚不能遗漏。我自己的经验是先把指令集缩小到最小可用集合比如只支持赋值、算术、条件跳转和函数调用。把这几种的语义写对、测透再逐步扩展。一上来就支持所有指令很容易陷入细节泥潭最后哪个都没写对。3.3 执行轨迹的记录格式怎么存、存什么执行轨迹是具体执行的输出也是下游工具的输入。它的格式设计直接影响到整个工具链的可用性。我见过一些项目具体执行引擎写得挺好但轨迹格式设计得一塌糊涂导致后面每个工具都要写一个适配层维护成本极高。一个好的轨迹格式应该满足几个条件自描述、可扩展、易解析。自描述是指光看轨迹文件就能知道每一步在干什么不需要额外的文档。可扩展是指以后想加新字段不会破坏已有的解析器。易解析是指用常见的解析库就能读不需要写复杂的词法分析器。我通常推荐用 JSON Lines 格式每一行是一个 JSON 对象代表一步执行。比如{step: 1, type: assign, var: z, value: 7, pc: 2} {step: 2, type: branch, condition: z 10, result: false, pc: 3} {step: 3, type: return, value: 6, pc: 4}这种格式的好处是每一行独立可以流式处理不需要一次性加载整个文件。而且 JSON 的解析库到处都是不用担心兼容性。提示轨迹文件可能会很大尤其是分析长时间运行的程序时。建议加上压缩比如 gzip 或者 zstd。实测下来压缩率通常能到 10:1 以上对存储和传输都友好。3.4 输入生成策略具体值从哪来具体执行需要具体输入。输入从哪来这取决于你的目标。如果只是验证某个特定场景手动指定输入就行。如果要做路径覆盖那就需要自动生成输入。自动生成输入的常见策略有三种随机生成、基于约束生成和基于搜索生成。随机生成最简单但覆盖率低很多路径可能永远跑不到。基于约束生成需要先做符号执行拿到路径约束然后用求解器生成满足约束的输入。基于搜索生成是用启发式算法比如遗传算法逐步逼近未覆盖的路径。我一般建议先用随机生成快速跑一遍看看覆盖率怎么样。如果覆盖率已经满足需求就不用折腾更复杂的策略。如果覆盖率不够再上基于约束的方法。不要一上来就搞最复杂的容易过度工程。还有一个实用技巧把输入空间划分成等价类每个等价类选一个代表值。比如对于整数输入可以选-1, 0, 1, 最大值, 最小值这几个边界值。这样能用最少的输入覆盖最多的路径。4. 实操过程与核心环节实现4.1 环境准备与工具选型动手之前先把环境搭好。具体执行引擎可以自己写也可以用现成的。自己写的好处是可控坏处是工作量大。用现成的好处是快坏处是可能不满足你的定制需求。如果你选择自己写我推荐用 Python 或者 OCaml。Python 开发快生态好适合做原型。OCaml 性能好模式匹配强适合做正式的工具。如果你选择用现成的可以看看 KLEE、Manticore、angr 这些框架。它们都支持具体执行而且文档比较全。不管选哪种先把依赖装好。Python 的话pip install几个核心库就行。OCaml 的话用opam管理依赖。现成框架的话按照官方文档走通常有 Docker 镜像省去环境配置的麻烦。注意如果你用的是现成框架先跑一遍官方提供的示例确认环境没问题。我见过太多人环境没配好就开始写代码结果报错报了半天最后发现是依赖版本不对。4.2 一个最小可用的具体执行引擎实现下面我用 Python 写一个最小可用的具体执行引擎支持赋值、算术、条件跳转和返回。代码不长但涵盖了核心逻辑。class State: def __init__(self): self.vars {} self.path_conditions [] self.pc 0 def copy(self): s State() s.vars self.vars.copy() s.path_conditions self.path_conditions.copy() s.pc self.pc return s def execute(instructions, inputs): state State() state.vars.update(inputs) trace [] while state.pc len(instructions): inst instructions[state.pc] trace.append({ pc: state.pc, inst: inst, vars: state.vars.copy() }) if inst[0] assign: _, var, expr inst state.vars[var] eval(expr, {}, state.vars) state.pc 1 elif inst[0] branch: _, cond, target inst result eval(cond, {}, state.vars) state.path_conditions.append((cond, result)) if result: state.pc target else: state.pc 1 elif inst[0] return: _, expr inst return eval(expr, {}, state.vars), trace return None, trace这段代码的核心是State类和execute函数。State保存变量、路径条件和程序计数器。execute逐条执行指令每一步都记录到trace里。branch指令会更新路径条件并根据条件结果决定跳转目标。用起来也很简单instructions [ (assign, z, x y), (branch, z 10, 4), (assign, r, z - 1), (return, r), (assign, r, z * 2), (return, r), ] result, trace execute(instructions, {x: 3, y: 4}) print(result) # 6 for t in trace: print(t)跑出来的结果就是6轨迹里能看到每一步的变量状态和路径条件。这个引擎虽然简单但已经能处理基本的程序了。你可以在此基础上扩展比如加循环、加函数调用、加内存模型。4.3 轨迹分析与路径覆盖统计有了轨迹之后下一步是分析。最常见的分析是路径覆盖统计程序一共有多少条路径具体执行覆盖了多少条。路径覆盖的计算方法很简单把所有可能的路径枚举出来然后看轨迹里实际走了哪些。对于小规模程序可以暴力枚举。对于大规模程序需要用符号执行或者图算法来辅助。我通常的做法是先把程序转换成控制流图CFG然后从入口到出口枚举所有路径。每一条路径对应一个路径条件。具体执行的轨迹会告诉你实际走了哪条路径把这条路径标记为已覆盖。最后统计覆盖率。def count_paths(cfg): # 简化版假设 cfg 是邻接表 from functools import lru_cache lru_cache(maxsizeNone) def dfs(node): if node exit: return 1 return sum(dfs(next_node) for next_node in cfg.get(node, [])) return dfs(entry)这个递归函数会返回从入口到出口的路径总数。实际项目里CFG 可能有环需要先做拓扑排序或者用动态规划处理。但核心思路是一样的把路径计数问题转化成图上的计数问题。覆盖率统计完之后如果发现有些路径没覆盖到就需要生成新的输入去覆盖它们。这时候可以回到 3.4 节讲的输入生成策略针对未覆盖路径的约束条件生成输入。4.4 与符号执行的衔接从具体到符号的过渡具体执行的最终目的是为符号执行铺路。衔接的关键在于把具体执行记录的状态序列转换成符号执行需要的初始状态和路径约束。具体做法是取具体执行轨迹的最后一步状态把其中的具体值替换成符号变量。比如轨迹最后x3, y4, z7符号执行就从xs1, ys2, zs1s2开始。路径条件也从具体的7 10 false变成符号的s1 s2 10。这个替换过程需要小心处理。不是所有变量都能替换成符号有些变量可能是常量或者外部输入替换错了会导致符号执行结果不对。我一般建议只替换那些真正影响路径的变量其他的保持具体值。提示具体执行和符号执行的衔接点往往是 Bug 的高发区。建议在这个环节加详细的日志记录哪些变量被替换了、替换成了什么。出问题的时候日志能帮你快速定位。5. 常见问题与排查技巧实录5.1 执行结果和预期不一致怎么办这是最常见的问题。具体执行跑出来的结果和你手动算的不一样。原因可能有很多我按排查优先级列一下。第一检查输入。输入值是不是搞错了比如该传3传成了3类型不对导致语义不同。第二检查指令语义。你的引擎对某条指令的语义定义是不是和实际语言规范不一致比如整数除法的舍入方向、浮点数的精度处理。第三检查路径条件。分支判断的条件是不是写反了写成了第四检查状态复制。如果用了多线程或者状态共享是不是有竞态条件导致状态被意外修改排查的时候建议从最简单的输入开始逐步增加复杂度。先用x0, y0跑再用x1, y0跑一步一步来。每步都对比预期结果和实际结果定位到具体是哪一步开始出错的。5.2 轨迹文件过大导致分析卡顿轨迹文件大了之后解析和查询都会变慢。我遇到过轨迹文件几十 GB 的情况直接加载到内存里根本不现实。解决办法有几个。第一用流式解析不要一次性加载。JSON Lines 格式天然支持流式一行一行读读完就丢。第二建索引。在轨迹文件旁边建一个索引文件记录每一步的偏移量。查询的时候先查索引再定位到具体位置。第三压缩。前面提过gzip 或者 zstd 能把体积压到十分之一以下。第四采样。如果不需要每一步的细节可以每隔 N 步记录一次减少数据量。我一般建议组合使用流式解析 压缩 索引。这套组合下来几十 GB 的轨迹文件也能在普通机器上处理。5.3 路径条件记录不全导致符号执行漏路径这个问题很隐蔽具体执行阶段看不出来到了符号执行阶段才发现有些路径没覆盖到。根子在于具体执行阶段漏记了某些路径条件。常见的原因有分支指令的语义定义不完整只记录了if的条件没记录else的条件循环指令的边界条件没记录异常处理的路径条件没记录。排查方法是拿一个已知路径数量的程序跑具体执行看记录的路径条件数量是不是和预期一致。如果不一致就逐条对比找出漏掉的是哪条。预防措施是在具体执行引擎里加一个断言每执行一条分支指令必须记录至少一个路径条件。如果没记录直接报错。这样能在早期发现问题而不是等到符号执行阶段才暴露。5.4 常见问题速查表问题现象可能原因排查方法解决方案执行结果与预期不符输入错误、语义定义错误、路径条件错误从简单输入开始逐步排查修正输入或语义定义轨迹文件过大记录粒度过细、未压缩检查记录字段和文件大小流式解析、压缩、采样符号执行漏路径路径条件记录不全对比路径条件数量和预期补全分支语义、加断言执行速度慢解释执行开销大、状态复制频繁性能分析编译执行、状态共享内存占用高状态未及时释放、轨迹缓存过大内存分析及时释放、限制缓存大小5.5 几个我踩过的坑和对应的技巧第一个坑是浮点数精度。具体执行的时候浮点数的计算结果可能和预期有微小差异。比如0.1 0.2不等于0.3。如果你的路径条件里有浮点数比较这个差异可能导致走错分支。解决办法是浮点数比较用容差不要用精确相等。第二个坑是字符串编码。处理字符串的时候编码问题可能导致执行结果不对。比如 UTF-8 和 GBK 混用同一个字符串的字节表示不同。解决办法是统一用 UTF-8并且在输入输出的时候显式指定编码。第三个坑是递归深度。如果程序有递归具体执行可能会栈溢出。解决办法是把递归转换成迭代或者加大栈空间。Python 的话可以用sys.setrecursionlimit但治标不治本最好还是改成迭代。第四个坑是外部调用。如果程序调用了外部库或者系统调用具体执行引擎可能没法模拟。解决办法是用桩函数stub替代外部调用返回预设的值。桩函数的返回值要根据实际场景来定不能随便返回。提示桩函数的返回值最好做成可配置的这样在不同测试场景下可以灵活调整。硬编码的桩函数在复杂场景下会限制你的分析能力。6. 具体执行的扩展方向与个人经验具体执行本身不复杂但它的扩展空间很大。往上走可以接符号执行、抽象解释、模型检验。往横走可以支持多线程、分布式、异构计算。往下走可以优化状态表示、加速执行、减少内存占用。我个人在实际操作中的体会是具体执行这一层最值得投入的时间是“状态表示的优化”和“轨迹格式的设计”。这两块做好了后面的所有环节都会受益。状态表示优化能直接提升执行速度轨迹格式设计能直接降低工具链的维护成本。另外一个小技巧是把具体执行引擎做成可插拔的。核心逻辑不变但状态表示、轨迹格式、输入生成策略都可以替换。这样在面对不同项目的时候可以快速适配不用每次都重写。这个内容后续还可以这样扩展加一个可视化模块把执行轨迹画成图直观展示路径和状态变化。或者加一个差分执行模块同时跑两个版本的代码对比轨迹差异快速定位行为变化。这些都是实际项目中很有用的功能而且实现起来并不复杂。 
长河君 · 2026/10/17 11:10:41 · 阅读 1.2k 形式化方法入门：具体执行引擎的设计与实现
1. 从“跑一遍”到“算清楚”具体执行为什么值得单独拎出来讲形式化方法这四个字很多人第一次听到会觉得离自己很远像是学术论文里的东西。但只要你写过代码、调过Bug、做过测试你其实已经在跟它打交道了只是没意识到而已。形式化方法的核心思路是用数学化的手段描述系统应该怎么运行然后用工具去验证它是不是真的这么运行。而“具体执行”Concrete Execution就是这条链路里最接地气的一环——它不抽象、不推导、不证明就是拿着具体的输入值一步一步把程序跑一遍看看到底发生了什么。你可以把它理解成“带着记录仪的试车”。平时你开车只知道从A点到了B点中间发动机抖没抖、刹车踩了几脚、油耗多少全靠感觉。具体执行不一样它把每一个中间状态都记下来变量在每一步的值是什么、条件判断走了哪个分支、循环执行了多少次、内存里的数据怎么变的。这些信息在符号执行和模型检验里都是基础燃料没有它们后面的分析根本跑不起来。这篇文章适合谁看如果你是做软件测试、程序分析、嵌入式开发或者安全审计的具体执行是你绕不开的基本功。如果你是在校学生正在啃形式化方法这门课Part A 通常就是整个课程的第一道门槛把这部分吃透了后面符号执行、抽象解释、定理证明才不会听得云里雾里。哪怕你只是个普通开发者理解具体执行的思路也能让你在调试复杂逻辑时多一套系统化的方法而不是靠print大法到处碰运气。我见过太多人一上来就直奔符号执行结果连“路径约束怎么收集”都搞不明白根子就在具体执行这一层没打牢。所以这篇文章我会把具体执行拆开揉碎从设计思路到实操细节再到常见坑全部过一遍。你不需要有形式化方法的背景只要会写基本的代码就能跟上。2. 具体执行的整体设计与核心思路拆解2.1 具体执行到底在做什么一句话说清楚具体执行就是给定一个程序和一个具体的输入按照程序的语义一步一步执行记录每一步的状态变化。这里的“具体”是相对于“符号”而言的输入不是符号变量而是实实在在的数值比如x 5、name abc。因为输入是确定的所以程序的执行路径也是确定的不会出现分支爆炸的问题。这听起来好像没什么技术含量不就是跑程序吗但关键在于“记录”和“可控”。普通的运行只是看最终输出具体执行要的是中间过程。举个例子下面这段代码def foo(x, y): z x y if z 10: return z * 2 else: return z - 1如果你用foo(3, 4)去跑普通执行只告诉你结果是6。但具体执行会告诉你第一步x3, y4第二步z7第三步判断7 10为假走 else 分支第四步返回7 - 1 6。这些中间状态才是后续分析真正需要的东西。2.2 为什么不用普通调试代替具体执行有人可能会问我用调试器单步跟踪不就行了何必专门搞一套具体执行这个问题我当初也想过后来在实际项目里踩了坑才明白调试器和具体执行的目标完全不同。调试器是给人看的它的输出是给人类阅读的格式随意、不结构化。你单步十次看到的是一堆散乱的信息想把它喂给另一个分析工具几乎不可能。具体执行是给工具看的它的输出是结构化的状态序列每一步的变量绑定、路径条件、内存状态都有明确的格式可以直接被后续的符号执行引擎或者验证器消费。另一个区别是可控性。调试器依赖人工操作你点一下走一步。具体执行可以自动化给定输入就能批量跑跑完自动收集所有路径信息。在做大规模测试或者路径覆盖分析的时候这个差异是致命的。你不可能手动调试一万个测试用例但具体执行可以。还有一个容易被忽略的点具体执行可以处理“非标准语义”。比如在分析底层代码时你需要自定义某些指令的行为调试器通常不允许你改语义但具体执行框架可以。你可以告诉它“这条指令按我的规则来”这在分析特定领域的程序时非常有用。2.3 具体执行在形式化方法工具链中的位置把形式化方法的工具链想象成一条流水线最左边是源代码最右边是“程序满足某条性质”的结论。中间有好几个环节具体执行是排在最前面的那个。它的下游通常是符号执行。符号执行需要知道程序有哪些路径、每条路径上的约束是什么。这些信息从哪来就是从具体执行来的。你先用具体输入跑一遍记录下路径和状态然后符号执行引擎在此基础上把具体值替换成符号值开始推导。没有具体执行打底符号执行就是空中楼阁。再往 downstream 走是模型检验和定理证明。模型检验需要把程序转换成状态机而状态机的状态转移关系很大程度上依赖具体执行提供的状态序列。定理证明需要把程序语义形式化成逻辑公式具体执行记录的状态变化就是公式的实例化依据。所以你看具体执行虽然简单但它是整条链路的基石。基石的精度和完整性直接决定了上层分析的质量。我在实际项目里见过太多因为具体执行阶段记录不全导致后面符号执行漏路径、模型检验状态爆炸的案例。返工的成本远高于一开始就把这一层做扎实。2.4 设计具体执行引擎时的核心权衡自己动手写一个具体执行引擎或者选一个现成的框架来用都会面临几个关键权衡。我把它们列出来你在做技术选型的时候可以对照着看。第一个权衡是解释执行 vs 编译执行。解释执行就是写一个解释器逐条读取程序指令模拟它的行为。优点是灵活你可以随时插入记录逻辑改语义也方便。缺点是慢尤其是分析大规模程序的时候解释器的开销会让人抓狂。编译执行是把程序转换成某种中间表示然后直接在那个表示上跑。优点是快缺点是灵活性差想改语义就得改编译器。第二个权衡是状态记录的粒度。你可以只记录变量的值也可以连内存地址、栈帧、寄存器都记下来。粒度越细信息越全但存储开销越大。我一般建议根据下游需求来定如果只是做路径覆盖分析记录变量和分支条件就够了如果要做内存安全分析那必须把内存状态也记下来。第三个权衡是路径爆炸的处理。虽然具体执行的输入是确定的路径不会爆炸但如果你要做的是“多输入批量执行”那路径数量还是会随输入数量线性增长。这时候需要考虑并行化和状态剪枝。并行化好理解多开几个进程同时跑。状态剪枝是指如果两条路径在某个点之后完全一样就没必要重复记录。这个优化在实际项目里能省不少时间。3. 核心细节解析与实操要点3.1 程序状态的表示变量、内存和路径条件具体执行的核心是“状态”这个概念。一个状态至少包含三部分变量绑定、内存模型和路径条件。变量绑定就是当前所有活跃变量的值。比如x3, y4, z7。这部分通常用哈希表或者环境链表来实现。哈希表查询快但插入和删除慢环境链表适合处理作用域嵌套但查询慢。实际实现里常见的是两者的混合用链表维护作用域每个作用域内部用哈希表。内存模型稍微复杂一点。对于高级语言你可能只需要模拟堆和栈对于低级语言你得模拟整个地址空间。我建议初学者先从简单的开始把内存当成一个从地址到值的映射不要一上来就搞分页、缓存这些复杂的东西。等基本流程跑通了再逐步细化。路径条件是一组布尔表达式的合取。比如走到某一步时路径条件是x 0 y 10。这些条件在具体执行阶段是已知真假的因为输入是具体的。但记录下来之后到了符号执行阶段它们就变成了约束求解器的输入。所以具体执行阶段一定要把路径条件记全不能漏。注意路径条件的顺序很重要。有些约束求解器对条件的顺序敏感顺序不对可能导致求解时间暴涨。建议按照程序执行的先后顺序记录不要事后重排。3.2 指令语义的定义每条指令到底做了什么具体执行引擎需要为每一种指令定义语义。所谓语义就是“执行这条指令之后状态怎么变”。比如加法指令z x y语义就是读取x和y的值相加把结果写入z。听起来简单但实际实现的时候有很多细节。首先是类型处理。x和y可能是整数、浮点数、字符串甚至自定义对象。不同类型的加法语义完全不同。整数加法可能溢出浮点加法有精度问题字符串加法是拼接。你的引擎必须能区分这些情况否则执行结果就是错的。其次是指令的副作用。有些指令不只是改变量值还会改变控制流、抛出异常、修改全局状态。比如函数调用指令它会把当前状态压栈创建一个新状态执行完再恢复。这些副作用必须在语义定义里写清楚不能遗漏。我自己的经验是先把指令集缩小到最小可用集合比如只支持赋值、算术、条件跳转和函数调用。把这几种的语义写对、测透再逐步扩展。一上来就支持所有指令很容易陷入细节泥潭最后哪个都没写对。3.3 执行轨迹的记录格式怎么存、存什么执行轨迹是具体执行的输出也是下游工具的输入。它的格式设计直接影响到整个工具链的可用性。我见过一些项目具体执行引擎写得挺好但轨迹格式设计得一塌糊涂导致后面每个工具都要写一个适配层维护成本极高。一个好的轨迹格式应该满足几个条件自描述、可扩展、易解析。自描述是指光看轨迹文件就能知道每一步在干什么不需要额外的文档。可扩展是指以后想加新字段不会破坏已有的解析器。易解析是指用常见的解析库就能读不需要写复杂的词法分析器。我通常推荐用 JSON Lines 格式每一行是一个 JSON 对象代表一步执行。比如{step: 1, type: assign, var: z, value: 7, pc: 2} {step: 2, type: branch, condition: z 10, result: false, pc: 3} {step: 3, type: return, value: 6, pc: 4}这种格式的好处是每一行独立可以流式处理不需要一次性加载整个文件。而且 JSON 的解析库到处都是不用担心兼容性。提示轨迹文件可能会很大尤其是分析长时间运行的程序时。建议加上压缩比如 gzip 或者 zstd。实测下来压缩率通常能到 10:1 以上对存储和传输都友好。3.4 输入生成策略具体值从哪来具体执行需要具体输入。输入从哪来这取决于你的目标。如果只是验证某个特定场景手动指定输入就行。如果要做路径覆盖那就需要自动生成输入。自动生成输入的常见策略有三种随机生成、基于约束生成和基于搜索生成。随机生成最简单但覆盖率低很多路径可能永远跑不到。基于约束生成需要先做符号执行拿到路径约束然后用求解器生成满足约束的输入。基于搜索生成是用启发式算法比如遗传算法逐步逼近未覆盖的路径。我一般建议先用随机生成快速跑一遍看看覆盖率怎么样。如果覆盖率已经满足需求就不用折腾更复杂的策略。如果覆盖率不够再上基于约束的方法。不要一上来就搞最复杂的容易过度工程。还有一个实用技巧把输入空间划分成等价类每个等价类选一个代表值。比如对于整数输入可以选-1, 0, 1, 最大值, 最小值这几个边界值。这样能用最少的输入覆盖最多的路径。4. 实操过程与核心环节实现4.1 环境准备与工具选型动手之前先把环境搭好。具体执行引擎可以自己写也可以用现成的。自己写的好处是可控坏处是工作量大。用现成的好处是快坏处是可能不满足你的定制需求。如果你选择自己写我推荐用 Python 或者 OCaml。Python 开发快生态好适合做原型。OCaml 性能好模式匹配强适合做正式的工具。如果你选择用现成的可以看看 KLEE、Manticore、angr 这些框架。它们都支持具体执行而且文档比较全。不管选哪种先把依赖装好。Python 的话pip install几个核心库就行。OCaml 的话用opam管理依赖。现成框架的话按照官方文档走通常有 Docker 镜像省去环境配置的麻烦。注意如果你用的是现成框架先跑一遍官方提供的示例确认环境没问题。我见过太多人环境没配好就开始写代码结果报错报了半天最后发现是依赖版本不对。4.2 一个最小可用的具体执行引擎实现下面我用 Python 写一个最小可用的具体执行引擎支持赋值、算术、条件跳转和返回。代码不长但涵盖了核心逻辑。class State: def __init__(self): self.vars {} self.path_conditions [] self.pc 0 def copy(self): s State() s.vars self.vars.copy() s.path_conditions self.path_conditions.copy() s.pc self.pc return s def execute(instructions, inputs): state State() state.vars.update(inputs) trace [] while state.pc len(instructions): inst instructions[state.pc] trace.append({ pc: state.pc, inst: inst, vars: state.vars.copy() }) if inst[0] assign: _, var, expr inst state.vars[var] eval(expr, {}, state.vars) state.pc 1 elif inst[0] branch: _, cond, target inst result eval(cond, {}, state.vars) state.path_conditions.append((cond, result)) if result: state.pc target else: state.pc 1 elif inst[0] return: _, expr inst return eval(expr, {}, state.vars), trace return None, trace这段代码的核心是State类和execute函数。State保存变量、路径条件和程序计数器。execute逐条执行指令每一步都记录到trace里。branch指令会更新路径条件并根据条件结果决定跳转目标。用起来也很简单instructions [ (assign, z, x y), (branch, z 10, 4), (assign, r, z - 1), (return, r), (assign, r, z * 2), (return, r), ] result, trace execute(instructions, {x: 3, y: 4}) print(result) # 6 for t in trace: print(t)跑出来的结果就是6轨迹里能看到每一步的变量状态和路径条件。这个引擎虽然简单但已经能处理基本的程序了。你可以在此基础上扩展比如加循环、加函数调用、加内存模型。4.3 轨迹分析与路径覆盖统计有了轨迹之后下一步是分析。最常见的分析是路径覆盖统计程序一共有多少条路径具体执行覆盖了多少条。路径覆盖的计算方法很简单把所有可能的路径枚举出来然后看轨迹里实际走了哪些。对于小规模程序可以暴力枚举。对于大规模程序需要用符号执行或者图算法来辅助。我通常的做法是先把程序转换成控制流图CFG然后从入口到出口枚举所有路径。每一条路径对应一个路径条件。具体执行的轨迹会告诉你实际走了哪条路径把这条路径标记为已覆盖。最后统计覆盖率。def count_paths(cfg): # 简化版假设 cfg 是邻接表 from functools import lru_cache lru_cache(maxsizeNone) def dfs(node): if node exit: return 1 return sum(dfs(next_node) for next_node in cfg.get(node, [])) return dfs(entry)这个递归函数会返回从入口到出口的路径总数。实际项目里CFG 可能有环需要先做拓扑排序或者用动态规划处理。但核心思路是一样的把路径计数问题转化成图上的计数问题。覆盖率统计完之后如果发现有些路径没覆盖到就需要生成新的输入去覆盖它们。这时候可以回到 3.4 节讲的输入生成策略针对未覆盖路径的约束条件生成输入。4.4 与符号执行的衔接从具体到符号的过渡具体执行的最终目的是为符号执行铺路。衔接的关键在于把具体执行记录的状态序列转换成符号执行需要的初始状态和路径约束。具体做法是取具体执行轨迹的最后一步状态把其中的具体值替换成符号变量。比如轨迹最后x3, y4, z7符号执行就从xs1, ys2, zs1s2开始。路径条件也从具体的7 10 false变成符号的s1 s2 10。这个替换过程需要小心处理。不是所有变量都能替换成符号有些变量可能是常量或者外部输入替换错了会导致符号执行结果不对。我一般建议只替换那些真正影响路径的变量其他的保持具体值。提示具体执行和符号执行的衔接点往往是 Bug 的高发区。建议在这个环节加详细的日志记录哪些变量被替换了、替换成了什么。出问题的时候日志能帮你快速定位。5. 常见问题与排查技巧实录5.1 执行结果和预期不一致怎么办这是最常见的问题。具体执行跑出来的结果和你手动算的不一样。原因可能有很多我按排查优先级列一下。第一检查输入。输入值是不是搞错了比如该传3传成了3类型不对导致语义不同。第二检查指令语义。你的引擎对某条指令的语义定义是不是和实际语言规范不一致比如整数除法的舍入方向、浮点数的精度处理。第三检查路径条件。分支判断的条件是不是写反了写成了第四检查状态复制。如果用了多线程或者状态共享是不是有竞态条件导致状态被意外修改排查的时候建议从最简单的输入开始逐步增加复杂度。先用x0, y0跑再用x1, y0跑一步一步来。每步都对比预期结果和实际结果定位到具体是哪一步开始出错的。5.2 轨迹文件过大导致分析卡顿轨迹文件大了之后解析和查询都会变慢。我遇到过轨迹文件几十 GB 的情况直接加载到内存里根本不现实。解决办法有几个。第一用流式解析不要一次性加载。JSON Lines 格式天然支持流式一行一行读读完就丢。第二建索引。在轨迹文件旁边建一个索引文件记录每一步的偏移量。查询的时候先查索引再定位到具体位置。第三压缩。前面提过gzip 或者 zstd 能把体积压到十分之一以下。第四采样。如果不需要每一步的细节可以每隔 N 步记录一次减少数据量。我一般建议组合使用流式解析 压缩 索引。这套组合下来几十 GB 的轨迹文件也能在普通机器上处理。5.3 路径条件记录不全导致符号执行漏路径这个问题很隐蔽具体执行阶段看不出来到了符号执行阶段才发现有些路径没覆盖到。根子在于具体执行阶段漏记了某些路径条件。常见的原因有分支指令的语义定义不完整只记录了if的条件没记录else的条件循环指令的边界条件没记录异常处理的路径条件没记录。排查方法是拿一个已知路径数量的程序跑具体执行看记录的路径条件数量是不是和预期一致。如果不一致就逐条对比找出漏掉的是哪条。预防措施是在具体执行引擎里加一个断言每执行一条分支指令必须记录至少一个路径条件。如果没记录直接报错。这样能在早期发现问题而不是等到符号执行阶段才暴露。5.4 常见问题速查表问题现象可能原因排查方法解决方案执行结果与预期不符输入错误、语义定义错误、路径条件错误从简单输入开始逐步排查修正输入或语义定义轨迹文件过大记录粒度过细、未压缩检查记录字段和文件大小流式解析、压缩、采样符号执行漏路径路径条件记录不全对比路径条件数量和预期补全分支语义、加断言执行速度慢解释执行开销大、状态复制频繁性能分析编译执行、状态共享内存占用高状态未及时释放、轨迹缓存过大内存分析及时释放、限制缓存大小5.5 几个我踩过的坑和对应的技巧第一个坑是浮点数精度。具体执行的时候浮点数的计算结果可能和预期有微小差异。比如0.1 0.2不等于0.3。如果你的路径条件里有浮点数比较这个差异可能导致走错分支。解决办法是浮点数比较用容差不要用精确相等。第二个坑是字符串编码。处理字符串的时候编码问题可能导致执行结果不对。比如 UTF-8 和 GBK 混用同一个字符串的字节表示不同。解决办法是统一用 UTF-8并且在输入输出的时候显式指定编码。第三个坑是递归深度。如果程序有递归具体执行可能会栈溢出。解决办法是把递归转换成迭代或者加大栈空间。Python 的话可以用sys.setrecursionlimit但治标不治本最好还是改成迭代。第四个坑是外部调用。如果程序调用了外部库或者系统调用具体执行引擎可能没法模拟。解决办法是用桩函数stub替代外部调用返回预设的值。桩函数的返回值要根据实际场景来定不能随便返回。提示桩函数的返回值最好做成可配置的这样在不同测试场景下可以灵活调整。硬编码的桩函数在复杂场景下会限制你的分析能力。6. 具体执行的扩展方向与个人经验具体执行本身不复杂但它的扩展空间很大。往上走可以接符号执行、抽象解释、模型检验。往横走可以支持多线程、分布式、异构计算。往下走可以优化状态表示、加速执行、减少内存占用。我个人在实际操作中的体会是具体执行这一层最值得投入的时间是“状态表示的优化”和“轨迹格式的设计”。这两块做好了后面的所有环节都会受益。状态表示优化能直接提升执行速度轨迹格式设计能直接降低工具链的维护成本。另外一个小技巧是把具体执行引擎做成可插拔的。核心逻辑不变但状态表示、轨迹格式、输入生成策略都可以替换。这样在面对不同项目的时候可以快速适配不用每次都重写。这个内容后续还可以这样扩展加一个可视化模块把执行轨迹画成图直观展示路径和状态变化。或者加一个差分执行模块同时跑两个版本的代码对比轨迹差异快速定位行为变化。这些都是实际项目中很有用的功能而且实现起来并不复杂。