Infer Cost 分析(复杂度分析)实战指南:WCET 上界推断、差分回归检测与 costs-report 解析
2026/9/24 16:01:54 网站建设 项目流程
  • 静态分析
  • 代码质量
  • 开发工具

【免费下载链接】infer

A static analyzer for Java, C, C++, and Objective-C

项目地址:https://gitcode.com/gh_mirrors/infer/infer
点击查看免费下载

本文围绕 Infer 静态分析器中的Cost(Complexity Analysis)检查器展开,系统讲解它如何基于控制流图与符号多项式为程序推断最坏情况执行代价(WCET)的上界,如何通过infer reportdiff在代码变更中自动发现复杂度回归(如从 O(n) 恶化到 O(n²)),以及costs-report.json报告的结构与五种关联 Issue 的触发条件。读完本文,你将掌握--cost/--cost-only的实际用法、差分分析的标准操作流程,并能结合仓库源码理解分析的三阶段流水线。本文以 version-1.3.0 的 checker-cost 文档 为主体骨架,并辅以当前仓库的源码、配置与测试用例进行纵深印证。

一、Cost 分析概览:它到底算什么

Cost 分析用于静态计算函数在资源使用上的渐近复杂度上界,最主要的资源就是执行代价(execution cost)。它既可以独立输出每个过程的多项式代价,也可以借助infer reportdiff检测两次运行之间复杂度的变化,从而在 CI 阶段拦截"性能悄然恶化"的提交。

从文档给出的定位看,该检查器:

  • 激活方式:--cost(与默认分析一起运行)或--cost-only(只运行代价分析);
  • 输出能力:对每个过程给出代价多项式、多项式次数、过程名、行号等信息,写入costs-report.json
  • 支持语言:C/C++/ObjC 为 Yes,Java 为 Yes,Hack 为 Experimental,C#/.Net、Erlang、Python、Rust、Swift 均不支持(当前版本以 Java 为主要分析对象,对 C/C++ 与 Objective-C 仅有有限支持)。

需要强调的是,costs-report.json与普通 issue 报告是两条独立的输出通道:常规检查器把发现的问题写入report.json,而代价分析的结果则单独落到costs-report.json,这为后续差分比较提供了数据基础(详见后文"差分模式"一节)。

二、快速上手:如何运行 Cost 分析

文档给出了两种运行方式:

# 方式一:与默认分析一同运行 infer --cost # 方式二:只运行代价分析 infer --cost-only

针对单个 Java 文件的示例:

infer --cost-only -- javac File.java

该命令会对File.java执行代价分析,结果写入infer-out/costs-report.json

仓库中还保留了完整的回归测试链供读者验证分析行为:

  • 测试用例位于 infer/tests/codetoanalyze/java/performance/Cost_test.java(以及同目录的Cost_test_deps.javaArrayCost.javaSwitch.java等),其中foo_constantbar_constantcond_constantloop0_constantloop1_constant等函数分别覆盖了常量代价、条件分支、定界循环等典型场景;
  • 测试驱动脚本见 infer/tests/cost.make,它通过infer report -q把代价 issue 导出并与期望文件cost-issues.exp做无差异比对(check_no_diff),确保分析结果可复现、可回归。

三、分析原理:三阶段流水线与 CFG 上的代价计算

文档明确指出,代价分析的输入是源码,源码先被翻译成 Infer 的中间语言(SIL)并生成控制流图(CFG),随后分析在中间表示上分三个阶段进行:

  1. 数值区间分析:基于 InferBo(BufferOverrun) 为访问内存的指令计算取值区间;
  2. 循环界分析:为循环的迭代次数确定上界,并为 CFG 中的节点生成约束;
  3. 约束求解:求解第二步生成的约束,最终算出执行代价的上界。

这一分析思路主要基于 Stefan Bygde 的博士论文《Static WCET Analysis based on Abstract Interpretation and Counting of Elements》中的理论框架。

从当前仓库源码可以清晰地对应到上述三个阶段:

  • 阶段 1 的 InferBo 区间信息,在 infer/src/cost/cost.ml 中通过BufferOverrunAnalysis.cached_compute_invariant_map获取,并封装进extras记录(inferbo_invariant_map字段);
  • 阶段 2 的循环界与节点执行次数上界,由 infer/src/cost/boundMap.ml 的BoundMap.compute_upperbound_map计算,其输入同时包括 InferBo 不变量图、控制依赖图与循环不变量图(见 infer/src/cost/cost.ml 的compute_bound_map函数);
  • 阶段 3 的约束求解在 infer/src/cost/constraintSolver.ml 中完成:ConstraintSolver.collect_constraints收集约束,ConstraintSolver.compute_costs求解,最终由get_node_nb_exec得到每个节点的最大执行次数。

文档还点明了每个 CFG 节点的代价构成:节点总代价 = 指令代价 × 节点执行次数(两个向量的标量积),再交给约束求解器根据入边/出边汇总出整个过程的执行代价。这在 infer/src/cost/cost.ml 的WorstCaseCost模块中得到精确印证:exec_node取出单条指令的代价记录instr_cost_record与该节点的执行次数nb_exec相乘,compute沿 CFG 所有节点累加即得过程总代价。

关于单条指令的代价语义,infer/src/cost/cost.ml 的InstrBasicCostWithReason模块做了细化:

  • 基础原子操作(LoadStorePrune等)计为单位代价 1(unit_cost_atomic_operation);
  • 函数调用默认按被调函数的 summary 代入代价,若没有 summary 或无法建模则按 1 估算(未建模调用可通过--cost-log-unknown-calls输出日志);
  • 若开启--inclusive-cost(默认开启,见 infer/src/base/Config.ml 中inclusive_cost的定义),调用点会把被调函数的完整代价包含进来——这正是"调用foo后复杂度从线性变平方"这一差分示例得以成立的关键机制;
  • 纯元数据指令(如ExitScopeNullifyLoopBackEdge)计零代价,前端插入的哑解引用也不计数。

四、代价的资源类型:不止执行代价

虽然分析最初为执行代价设计,但 Infer 已将其泛化为可针对不同资源做回归检测。version-1.3.0 文档列出三类资源:

  1. 执行代价(execution cost):采用简单的顺序执行模型与抽象代价语义,SIL 中每条基本指令视为一个单位执行代价;
  2. 分配代价(allocation cost):只对分配内存的原语操作(如new)计代价,目前处于实验模式,因此结果不会写入costs-report.json
  3. 自动释放池大小(autoreleasepool size):当对象被加入 Objective-C 的@autoreleasepool时计代价,通常发生在两种情况:非 ARC 代码中显式调用autorelease;或非 ARC 被调函数向 ARC 调用方返回(autoreleased)对象指针(反之亦然)。

对照当前仓库源码,代价种类的具体实现位于 infer/src/base/costKind.ml:

type t = OperationCost | AllocationCost

也就是说,当前代码枚举了两个活跃的代价种类OperationCost(执行/时间)与AllocationCost(分配),并通过enabled_cost_kinds决定哪些种类会参与普通模式的检查报告(目前仅OperationCost启用)。这与文档"分配代价处于实验模式、不写入 costs-report.json"的描述一致——infer/src/atd/jsoncost.atd 中的item类型只包含exec_cost字段,没有 alloc 字段;且 infer/src/base/costKind.ml 的to_json_cost_infoAllocationCost直接assert false,从数据结构上杜绝了分配代价进入 JSON 报告。Objective-C 侧@autoreleasepool语句的翻译在 Clang 前端 infer/src/clang/cTrans.ml 的objCAutoreleasePoolStmt_trans中处理,其调用objc_autorelease_pool_push/objc_autorelease_pool_pop内建函数建模。分配代价的建模模型集中在 infer/src/cost/costAllocationModels.ml,而new/malloc等分配点会经由 infer/src/cost/cost.ml 的dispatch_allocation计费。

五、执行代价示例:从 O(n) 到 O(n²) 的自动检测

文档给出了一个非常直观的例子。假设原始代码如下:

void loop(ArrayList<Integer> list){ for (int i = 0; i <= list.size(); i++){ } }

Infer 为中间语言的每条指令赋予符号代价后,会静态推断出一个多项式(例如8 · |list| + 16,其中|list|表示列表长度)。忽略具体常数,该程序的渐近复杂度为O(|list|),即关于输入规模的线性循环。

随后开发者在该循环体内加入一个调用:

void loop(ArrayList<Integer> list){ for (int i = 0; i <= list.size(); i++){ foo(i); // newly added function call } }

假设foo的代价关于其参数是线性的,那么 Infer 会自动检测到loop的复杂度从O(|list|)提升为O(|list|²),并上报 EXECUTION_TIME_COMPLEXITY_INCREASE 问题。

这个"复杂度随调用上升"的行为,正是得益于 infer/src/cost/cost.ml 中get_call_cost_record的"跨过程代入"(instantiate_cost):被调函数的代价 summary 会以调用点的实参符号(由 InferBo 求值得到)代入并乘以循环迭代次数。CostDomain.BasicCost底层是 infer/src/cost/costDomain.ml 中的Polynomials.NonNegativePolynomial,天然支持多项式加法、乘法与次数(degree)提取,从而能比较"常数为 0 次"、"线性为 1 次"、"二次为 2 次"的阶数差异。

六、差分模式:用 reportdiff 比较两次运行的复杂度

与其他只在单次运行中于report.json输出 issue 的分析不同,代价分析拥有专门的差分模式:每次运行都会在costs-report.json中记录每个过程的代价多项式、多项式次数、过程名与行号;差分模式下,Infer 比较两次运行生成的costs-report.json,从而发现复杂度的上升或下降。

文档给出的完整操作流程如下:

# 1. 第一次运行:对 File.java 做代价分析,并把结果备份到结果目录之外 infer --cost-only -- javac File.java cp infer-out/costs-report.json previous-costs-report.json # 2. 按上文示例修改 File.java(在循环内加入 foo(i)) # 3. 第二次运行 infer --cost-only -- javac File.java cp infer-out/costs-report.json current-costs-report.json # 4. 对比两次代价报告 infer reportdiff --costs-current current-costs-report.json --costs-previous previous-costs-report.json # 5. 查看新发现的复杂度上升问题 # 结果位于 infer-out/differential/introduced.json

说明:version-1.3.0 文档第一步中写为inter-out/costs-report.json,实为infer-out/costs-report.json的笔误;且备份文件应放在结果目录之外,因为第二次运行会清空结果目录。

关于infer reportdiff的行为,可以参考仓库中的手册 infer/man/man1/infer-reportdiff.txt:它接受--costs-current path(最新版本的代价报告)与--costs-previous path(基线版本的代价报告),并把比较结果写入结果目录的differential/子目录下三个文件:introduced.json(当前新增)、fixed.json(之前存在现已消失)、preexisting.json(两者都存在)。命令行选项的注册在 infer/src/base/Config.ml(costs_currentcosts_previous,分别对应长选项--costs-current--costs-previous),比较逻辑实现在 infer/src/integration/ReportDiff.ml:先load_costs读取两份 JSON 报告,再交给Differential.issues_of_reports ~current_report ~previous_report ~current_costs ~previous_costs完成分类。

costs-report.json的文件名由 infer/src/base/ResultsDirEntryName.ml 中的ReportCostsJson定义(生成costs-report.json),其 JSON 结构由 infer/src/atd/jsoncost.atd 描述:

type hum_info = { hum_polynomial : string; hum_degree : string; big_o : string; } type info = { polynomial_version : int; polynomial : string; ?degree : int option; hum : hum_info; trace : json_trace_item list; } type sub_item = {hash: string ; loc: loc ; procedure_name: string ; procedure_id: string } type item = { inherit sub_item; is_on_ui_thread : bool; exec_cost : info; } type report = item list

每个过程对应一条item,其中procedure_name/procedure_id标识过程,loc给出位置与行号,is_on_ui_thread标记是否运行在 UI 线程,exec_cost携带代价多项式、次数与人类可读的 Big-O 表示(hum)。还有一个值得注意的细节:infer/src/cost/costDomain.ml 中BasicCost.version = 13,其注释说明该版本号用于防止infer reportdiff反序列化失败——即代价多项式内部表示一旦变化,需要递增版本号以保持差分兼容。

另外,infer/src/base/Config.ml 还提供--from-json-costs-report选项,可以直接从既有 JSON 报告加载代价结果,便于离线/流水线场景复用。

七、Cost 检查器报告的 Issue 类型

代价分析关联的 Issue 共有五种,全部围绕"执行代价"展开。其注册机制在 infer/src/base/IssueType.ml:complexity_increase(第 465 行)生成%s_COMPLEXITY_INCREASEunreachable_cost_callinfinite_cost_callexpensive_cost_call分别生成%s_UNREACHABLE_AT_EXITINFINITE_%sEXPENSIVE_%s形式(其中%s由代价种类名代入,如EXECUTION_TIME)。各类型的启用与报告策略定义在 infer/src/base/CostIssues.ml 的enabled_cost_map与 infer/src/base/costKind.ml 的enabled_cost_kinds,最终由 infer/src/cost/cost.ml 的Check.check_and_report统一检查上报。

Issue 类型触发条件默认状态说明
EXECUTION_TIME_COMPLEXITY_INCREASE复杂度阶数上升(如常数→线性、对数→二次)启用(仅差分模式)只在infer reportdiff差分比较时上报;见 infer/documentation/issues/EXECUTION_TIME_COMPLEXITY_INCREASE.md
EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD复杂度阶数上升且过程运行在 UI 线程启用(仅差分模式)在上一类基础上叠加 UI 线程判定
EXECUTION_TIME_UNREACHABLE_AT_EXIT程序的执行无法到达出口节点默认禁用例如exit(0)Preconditions.checkState(false)使状态被裁剪为 bottom;见 infer/documentation/issues/EXECUTION_TIME_UNREACHABLE_AT_EXIT.md
EXPENSIVE_EXECUTION_TIME代价非恒定且非 Top(实验性)默认禁用例如线性代价函数;见 infer/documentation/issues/EXPENSIVE_EXECUTION_TIME.md
INFINITE_EXECUTION_TIME无法确定静态上界,返回 T(未知代价)默认禁用见下文"未知代价"小节;见 infer/documentation/issues/INFINITE_EXECUTION_TIME.md

UI 线程判定(UI_THREAD 变体)

EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD需要过程运行在 UI(主)线程。website/docs/all-issue-types.md 中列出了判定条件:方法、其某个 override、其类或祖先类带有@UiThread注解;方法或其 override 带有@OnEvent@OnClick等注解;方法或其调用者调用了Litho.ThreadUtils的如assertMainThread之类的方法。该标志在 infer/src/cost/cost.ml 的checker函数中计算:

let is_on_ui_thread = (not (Procname.is_objc_method proc_name)) && ConcurrencyModels.runs_on_ui_thread tenv proc_name

即非 ObjC 方法且被并发模型判定为运行在 UI 线程时置真,并随 summary 一起写入costs-report.jsonis_on_ui_thread字段,供差分阶段区分两个变体。

未知代价(T)与 INFINITE_EXECUTION_TIME

当静态分析无法确定上界时,代价为 Top(记为 T),对应 INFINITE_EXECUTION_TIME。infer/documentation/issues/INFINITE_EXECUTION_TIME.md 给出三类典型场景:

  • 表达力受限:InferBo 的区间分析限于仿射表达式,无法自动推断平方根等界,例如while (i * i < x) { i++; }期望square root(x)却得到 T;
  • 未建模库调用:如遍历input.toCharArray()的结果,Infer 没有String.toCharArray返回值范围的模型,无法确定循环上界;
  • 级联 Top:分析是过程间的,只要某个被调函数代价为 T,调用方也大概率得到 T。

从源码看,T 代价的传播机制在 infer/src/cost/costDomain.ml:BasicCostWithReason除了携带cost,还记录top_pname_opt指向"首个把代价污染为 Top 的被调函数",便于诊断;infer/src/cost/cost.ml 的get_modeled_cost_unless_top则故意在建模代价为 Top 时退回到默认低估值,避免 Top 沿调用链向上污染造成大规模误报。

代价为 Top / 不可达时的上报策略

infer/src/cost/cost.ml 的Check模块还体现了两个启发式策略:一是report_top_and_unreachable只在过程顶层上报"无法计算"(Top)或"出口不可达"的 Issue,避免在 CFG 内部节点重复报噪声;二是just_throws_exception启发式——若函数体极短且只是抛异常(如仅 5 个节点以内、只包含return exn类存储),则把其操作代价清零,防止差分模式下对异常路径产生虚假的复杂度上升。

八、已知局限与适用边界

文档明确列出了静态代价分析在设计与实现上的局限,使用时应予以注意:

  • InferBo 区间限于仿射表达式:由于 InferBo 的区间抽象不是完整多项式,分析无法自动推断涉及平方根的上界;
  • 不处理递归:递归过程的代价无法按当前框架闭合求解;
  • 未知调用返回 T:若程序执行代价依赖于未建模的库调用(例如遍历未建模库返回的集合),则无法计算静态上界,返回 T(未知代价),对应 INFINITE_EXECUTION_TIME。

此外从当前仓库的 infer/src/base/costKind.ml 还可以看出,普通(非差分)模式下当前只对OperationCost启用 Top/不可达检查(enabled_cost_kinds),且EXPENSIVE_EXECUTION_TIMEINFINITE_EXECUTION_TIMEEXECUTION_TIME_UNREACHABLE_AT_EXIT三类默认均为禁用状态,需要依据版本与配置按需启用。

九、深入阅读指引

如果你希望继续深入:

  • 分析主入口与指令代价/最坏情况代价计算:infer/src/cost/cost.ml
  • 代价多项式与代价种类:infer/src/cost/costDomain.ml、infer/src/base/costKind.ml
  • 循环界与约束求解:infer/src/cost/boundMap.ml、infer/src/cost/constraintSolver.ml
  • 建模与报告:infer/src/cost/costModels.ml、infer/src/cost/costAllocationModels.ml、infer/src/base/CostIssues.ml、infer/src/base/IssueType.ml
  • JSON 报告结构:infer/src/atd/jsoncost.atd
  • 差分比较:infer/src/integration/ReportDiff.ml、infer/man/man1/infer-reportdiff.txt
  • 各 Issue 官方文档:EXECUTION_TIME_COMPLEXITY_INCREASE.md、EXECUTION_TIME_UNREACHABLE_AT_EXIT.md、EXPENSIVE_EXECUTION_TIME.md、INFINITE_EXECUTION_TIME.md
  • 测试样例:infer/tests/codetoanalyze/java/performance/Cost_test.java、infer/tests/cost.make

综上,Cost 分析是一个"数值区间分析 + 循环界推导 + 约束求解"三层叠加的过程间静态分析,其核心产出是以多项式表达的渐近复杂度上界;配合costs-report.jsoninfer reportdiff,它能在不改动运行时、不引入基准测试的前提下,于每次代码评审或 CI 中自动发现执行代价的阶数级回归,是大型代码库中控制性能退化的低成本方案。

  • 静态分析
  • 代码质量
  • 开发工具

【免费下载链接】infer

A static analyzer for Java, C, C++, and Objective-C

项目地址:https://gitcode.com/gh_mirrors/infer/infer
点击查看免费下载

相关推荐

上一篇:抖音无水印批量下载工具:一个链接存下整个主页
下一篇:3步轻松备份你的QQ空间历史说说:GetQzonehistory完整指南

创作声明:本文部分内容由AI辅助生成(AIGC),仅供参考

需要专业的网站建设服务?

联系我们获取免费的网站建设咨询和方案报价,让我们帮助您实现业务目标

立即咨询