基于 Infer.AI 抽象解释框架构建你自己的静态检查器（Checker）

静态分析代码质量开发工具【免费下载链接】inferA static analyzer for Java, C, C, and Objective-C项目地址https://gitcode.com/gh_mirrors/infer/infer点击查看免费下载本指南以 Infer 的官方文档 04-absint-framework.md 为主体结合仓库内liveness、Siof两个真实检查器与absint抽象解释框架源码系统讲解 Infer.AI 的使用方法从定义抽象域、编写转移函数、组装分析器到注册检查器并在 CLI 上运行再到把过程内分析升级为模块化过程间分析。读完本文你将具备在 Infer 中从零开发一个可运行、可报错、可跨过程复用的自定义检查器的完整实战能力。Infer.AI 是什么一个你只需写两样东西的抽象解释框架Infer.AI 是 Infer 内置的抽象解释Abstract Interpretation框架用于快速开发基于抽象解释的检查器既支持过程内intraprocedural分析也支持过程间interprocedural分析。使用该框架你只需要定义两样东西抽象域Abstract Domain抽象状态的类型外加leq偏序、join并、widen widening操作转移函数Transfer Functions一个把抽象状态映射为抽象状态的变换器对应程序指令的执行语义。而你得到的是一个可以在 Infer 支持的所有语言C、Objective-C、C、Java上运行的分析。这一点由检查器注册机制保证——你写好的检查器只需在 registerCheckers.ml 中登记一次即可针对指定语言被调用。在框架层面抽象解释的核心接口定义在 AbstractDomain.mlimodule type S要求域实现leq、join、widen三个操作其中widen的签名是widen : prev:t - next:t - num_iters:int - tnum_iters参数供你实现随迭代次数变化的加速策略以保证终止。上手最快的方式过程内分析本节从零开始带你写一个过程内分析。官方推荐的最佳入门材料是仓库内的 labs/README.md 实验练习而本文将以liveness活跃变量分析作为主线实例它同时是 Infer 中一个真实的检查器用于检测死代码存储 DEAD_STORE。三个关键部件域、转移函数、分析器liveness.mlinfer/src/checkers/liveness.ml是经典的编译器基础课风格的活跃变量分析运行在 Infer 的中间表示 SIL 上。它规模很小同时又是理解如何使用抽象解释框架和SIL 长什么样的最佳范例。整个检查器由三部分组成定义域、定义转移函数、把部件交给框架组装成分析。先看域的定义module VarSet AbstractDomain.FiniteSet (Var) module Domain VarSet活跃变量集合是一个幂集域powerset domain直接用框架提供的组合子AbstractDomain.FiniteSet (Var)构造自动获得leq/join/widen实现。liveness为了同时跟踪正常控制流与异常控制流进一步用AbstractDomain.PairWithBottom (CExn) (VarSet)和记录{normal; exn}的ExtendedDomain封装了一个更精细的域并手写了leq、join、widen见 liveness.ml 的ExtendedDomain模块。这正是官方文档所说的抽象域就是抽象状态类型 、join、widen。再看组装分析器的核心代码原文档原样引用module CFG ProcCfg.OneInstrPerNode (ProcCfg.Backward (ProcCfg.Exceptional)) module CheckerAnalyzer AbstractInterpreter.MakeRPO (TransferFunctions (CheckerMode) (CFG))这行代码里包含了三层含义逐层拆解ProcCfg.Backward (ProcCfg.Exceptional)迭代方向为后向活跃变量是后向分析分析沿异常边传播。如果你要一个忽略异常边的前向分析写ProcCfg.Normal即可。更多组合可参考 ProcCfg.mli——该文件定义了Normal无异常控制流的前向 CFG、Exceptional含异常控制流的前向 CFG、ExceptionalNoSinkToExitEdge、Backward反转方向的包装器、OneInstrPerNode把每个 CFG 节点展开为单指令节点等变体。TransferFunctions (CheckerMode) (CFG)使用你在上面定义的转移函数。TransferFunctions是一个函子functor签名为module type TransferFunctions核心要求见 TransferFunctions.mli实现exec_instr : Domain.t - analysis_data - CFG.Node.t - instr_index - instr - Domain.t语义是从抽象状态astate执行一条指令得到新状态astate即抽象解释意义上的转移函数此外还需提供pp_session_name用于 HTML 调试输出。liveness中的转移函数核心逻辑是变量被读取时 gen 进活跃集被赋值时 kill 出活跃集compilers 101-style backward transfer functions见 liveness.ml 中TransferFunctions模块的注释并专门处理了CatchEntry/TryEntry等异常相关 SIL 指令。AbstractInterpreter.MakeRPO选用 reverse post-order 调度器的抽象解释器。MakeRPO与MakeWTO是两个可选的调度器函子定义在 AbstractInterpreter.mliMakeRPO使用逆后序调度MakeWTO使用 Bourdoncle 强连通分量弱拓扑序对循环处理更精细。此外该模块还提供MakeBackwardRPO/MakeBackwardWTO后向分析专用正确分派异常流与MakeDisjunctive析取解释器域为抽象状态集合转移函数在每个析取分支上独立执行。组装完成后CheckerAnalyzer模块对外暴露以下实用函数见 AbstractInterpreter.mli函数作用compute_post ?do_narrowing analysis_data ~initial proc_desc输入一个过程计算并返回其后置条件postconditionexec_cfg cfg analysis_data ~initial输入 CFG返回从节点 id 到状态pre/post的不变式映射exec_pdesc ?do_narrowing analysis_data ~initial proc_desc输入过程描述Procdesc返回节点 id → 状态的不变式映射extract_post / extract_pre / extract_state从不变式映射中取出某节点的后置/前置/状态其中不变式映射的类型为invariant_map Domain.t State.t InvariantMap.t每个状态State.t由{pre; post; visit_count}组成。把检查器挂到 CLI 上接下来把检查器接入 Infer 命令行。对liveness而言需要暴露一个在单个过程上运行的函数let checker ({IntraproceduralAnalysis.proc_desc; err_log} as analysis_data) match Analyzer.compute_post analysis_data ~initial:Domain.empty with | Some post - Logging.progress Computed post %a for %a Domain.pp post Procname.pp (Procdesc.get_proc_name proc_desc); | None - ()然后在 registerCheckers.ml 中把Liveness.checker加入已注册检查器列表搜索 Liveness 可见; {checker Liveness; callbacks [(intraprocedural Liveness.checker, Clang)]}注意intraprocedural这个辅助函数把普通回调包装为过程内回调并绑定到Clang语言即 C/Objective-C/C 前端。注册完成后即可运行infer run --liveness-only -- your_build_command把your_build_command换成任意受支持构建命令如make、xcodebuild、gradle即可在真实代码上运行你的检查器。Infer 支持的构建系统细节可参见 00-getting-started.md 与 01-analyzing-apps-or-projects.md。仓库中其他简单的过程内检查器例子还包括addressTaken.ml检测取地址逃逸与Siof.ml静态初始化顺序问题见下文过程间部分。错误报告Reporting.log_issue有用的分析必须有输出。向 stderr 打印仅适合调试而要报告一条绑定到源码位置、程序员可读的错误应使用Reporting.log_issue实现在 Reporting.ml。liveness中的典型用法见 liveness.ml 的log_report函数let log_report pvar typ loc let message F.asprintf The value written to %a is never used (Pvar.pp Pp.text) pvar in let trace_message F.asprintf Write of unused value (type %a) (Typ.pp_full Pp.text) typ in let ltr [Errlog.make_trace_element 0 loc trace_message []] in Reporting.log_issue proc_desc err_log ~loc ~ltr Liveness IssueType.dead_store messageReporting.log_issue接收过程描述、错误日志err_log、位置loc、错误轨迹ltr、检查器标识与问题类型如IssueType.dead_store最终生成带源码定位与调用轨迹的报告并显示在infer run的输出中。从源码看该函数底层经由log_issue_from_summary/log_issue_from_errlog统一写入错误日志因此无论过程内还是过程间检查器都能复用同一套报告管线。把过程内分析升级为模块化过程间分析假设你已经有一个过程内检查器。抽象解释框架可以轻松把它转换为模块化modular过程间分析。需要强调的是框架只支持模块化分析——全局分析global analyses无法在该框架中表达。转换需要做两件事为你的分析定义过程摘要summary的类型并在 registerCheckers.ml 中声明该检查器是过程间的添加逻辑a在转移函数中使用摘要b把过程内抽象状态转换为摘要。仓库中最合适的范例是Siof.ml静态初始化顺序问题 Static Initialization Order Fiasco 检测infer/src/checkers/Siof.ml。其中第一步声明摘要与注册的完整代码来自原文档(* in src/checkers/SiofDomain.ml *) (* note that as a result the type of summaries is the same as the type of domain elements *) module Summary ... include Summary (* in src/backend/Payloads.ml: register the payload of the analyzer *) type t { ... ; siof: SiofDomain.Summary.t option ... } (* in src/backend/registerCheckers.ml *) let all_checkers [ ... ; {checker SIOF; callbacks [(interprocedural Payloads.Fields.siof Siof.checker, Clang)]} ... ]上述代码在仓库中都有对应实现Payloads记录类型定义在 Payloads.mlsiof: SiofDomain.Summary.t SafeLazy.t option使用SafeLazy惰性求值并按需加载/持久化注册语句在 registerCheckers.mlinterprocedural Payloads.Fields.siof Siof.checker。这里interprocedural payload_field checker辅助函数registerCheckers.ml 第 21 行把回调包装为过程间回调分析一个过程时按需读取依赖过程的 payload并把当前过程的 payload 写回。由于Siof的摘要类型与抽象状态类型相同省去了抽象状态 → 摘要的转换逻辑。第二部分2a在 Siof.ml 的Call分支中核心是用框架提供的analyze_dependency回调match analyze_dependency callee_pname with这行代码的含义是读取callee_pname的摘要如果没有则先计算它。在Siof中拿到被调用者的摘要后会过滤出尚未被初始化的危险全局变量访问并用调用点信息CallSite更新其 trace再与当前抽象状态做Domain.join。你需要在转移函数中加入把摘要应用到当前抽象状态的逻辑通常简单到只需一次 join。因为Siof的摘要类型就是抽象状态本身第二部分2b只需要把分析计算出的 post 直接作为过程摘要返回即Analyzer.compute_post analysis_data ~initial proc_desc见 Siof.ml 的checker函数。到这里你就拥有了一个完整的过程间分析。其余步骤如报告跨编译单元的全局变量访问即真正的 SIOF 报告逻辑只需基于摘要做后处理用Reporting.log_issue输出即可。深入框架域组合子、调度器与异常控制流抽象域组合子库AbstractDomain.mli 提供了丰富的域构造工具绝大多数检查器无需手写leq/join/widen基础提升BottomLifted显式 bottom、TopLifted显式 top、BottomTopLifted同时具备、Flatbottom/top/中间元素不可比的平坦域组合Pair/PairWithBottom笛卡尔积、Stacked下/值/上的分层并域集合与映射FiniteSet幂集域widen 即并集、InvertedSet按超集序join 为交集、Map/InvertedMap/SafeInvertedMap、FiniteMultiMap专用域BooleanAnd/BooleanOr、CountDomain有界计数、MinReprSet等。liveness的VarSet与Siof的GlobalVarSet都直接复用AbstractDomain.FiniteSetlabs实验第三节中还用AbstractDomain.TopLifted解决整数域的终止问题见 labs/README.md 的提示。解释器与异常控制流框架层面对异常流的处理是一等公民。AbstractInterpreter的TransferFunctions类型见 AbstractInterpreter.mli要求额外实现四个函数join_all合并前驱状态、filter_normal只保留非异常具体状态、filter_exceptional只保留异常状态、transform_on_exceptional_edge跨异常边时切换正常/异常状态的语义。liveness.ml的TransferFunctions正是实现了这套接口其exec_instr的注释写明了活跃变量分析的精确语义一条指令之前活跃的变量 指令之后活跃且未被该指令赋值的变量 ∪ 被该指令读取的变量 ∪ 在异常后继节点之前活跃的变量。MakeBackwardRPO/MakeBackwardWTO则负责在后向分析中正确分派异常流。如果域是析取式的域元素为抽象状态列表转移函数在每个析取分支上独立执行可选用MakeDisjunctive并通过DisjunctiveConfig的join_policy/widen_policy见 TransferFunctions.mli如UnderApproximateAfter/UnderApproximateAfterNumIterations控制析取分支数量以实现有界近似。动手实践从实验到线上检查器infer/src/labs 目录是一个完整的自建资源泄漏分析实验labs/README.md即官方推荐的动手指南每个章节的完整答案在00_dummy_checker至05_access_paths_interprocedural子目录中快速开始用 Docker 镜像infer/infer:infer-latest-java-dev进入开发环境或本地构建后仅./build-infer.sh java即可本实验只需 Java 支持调试手段infer -g --resource-leak-lab-only -- javac Leaks.java生成 HTML 调试页展示每条告警对应的 CFG 节点及 pre/post 抽象状态Logging.d_printfln打印到对应 CFG 节点的日志Logging.debug_dev打印到控制台实验路径整数域 → 为分支实现join→ 为循环实现widen/leq并用TopLifted保证终止 → 用analyze_dependency读取被调用者摘要实现过程间分析 → 用FiniteSet/Map/AccessPath构建访问路径域处理别名 → 切换到ProcCfg.Exceptional覆盖异常路径。每个阶段都配有真实测试文件如Leaks.java、LeaksBranch.java、LeaksLoop.java、LeaksInterprocedural.java。进一步阅读检查器注册与回调机制registerCheckers.ml、Payloads.ml抽象解释器与调度器AbstractInterpreter.mli、TransferFunctions.mliCFG 变体ProcCfg.mli域构造器库AbstractDomain.mli端到端实例liveness.ml、Siof.ml动手实验labs/README.md 及 infer/src/labs 目录下的完整分节解答。赞分享静态分析代码质量开发工具【免费下载链接】inferA static analyzer for Java, C, C, and Objective-C项目地址https://gitcode.com/gh_mirrors/infer/infer点击查看免费下载相关推荐Infer 资源泄漏检查器 Lab 实战指南基于抽象解释框架从零构建自己的 CheckerInfer 资源泄漏检查器 Lab 实战指南基于抽象解释框架从零构建自己的 Checker 导读 本文围绕 Facebook Infer 静态分析器中内置的静态分析代码质量开发工具基于 Infer.AI 抽象解释框架构建自定义静态检查器从活变量分析到模块化过程间分析基于 Infer.AI 抽象解释框架构建自定义静态检查器从活变量分析到模块化过程间分析 Infer.AI 是 Infer 内置的抽象解释Abstract I静态分析代码质量开发工具基于 Infer.AI 抽象解释框架构建自定义静态检查器从过程内分析到模块化过程间分析基于 Infer.AI 抽象解释框架构建自定义静态检查器从过程内分析到模块化过程间分析 Infer.AI 是 Facebook Infer 静态分析器中用于快静态分析代码质量开发工具创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考