实战指南:WCET 上界推断、差分回归检测与 costs-report 解析)
静态分析代码质量开发工具【免费下载链接】inferA static analyzer for Java, C, C, and Objective-C项目地址https://gitcode.com/gh_mirrors/infer/infer点击查看免费下载本文围绕 Infer 静态分析器中的CostComplexity 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 为 YesJava 为 YesHack 为 ExperimentalC#/.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.java、ArrayCost.java、Switch.java等其中foo_constant、bar_constant、cond_constant、loop0_constant、loop1_constant等函数分别覆盖了常量代价、条件分支、定界循环等典型场景测试驱动脚本见 infer/tests/cost.make它通过infer report -q把代价 issue 导出并与期望文件cost-issues.exp做无差异比对check_no_diff确保分析结果可复现、可回归。三、分析原理三阶段流水线与 CFG 上的代价计算文档明确指出代价分析的输入是源码源码先被翻译成 Infer 的中间语言SIL并生成控制流图CFG随后分析在中间表示上分三个阶段进行数值区间分析基于 InferBoBufferOverrun 为访问内存的指令计算取值区间循环界分析为循环的迭代次数确定上界并为 CFG 中的节点生成约束约束求解求解第二步生成的约束最终算出执行代价的上界。这一分析思路主要基于 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模块做了细化基础原子操作Load、Store、Prune等计为单位代价 1unit_cost_atomic_operation函数调用默认按被调函数的 summary 代入代价若没有 summary 或无法建模则按 1 估算未建模调用可通过--cost-log-unknown-calls输出日志若开启--inclusive-cost默认开启见 infer/src/base/Config.ml 中inclusive_cost的定义调用点会把被调函数的完整代价包含进来——这正是调用foo后复杂度从线性变平方这一差分示例得以成立的关键机制纯元数据指令如ExitScope、Nullify、LoopBackEdge计零代价前端插入的哑解引用也不计数。四、代价的资源类型不止执行代价虽然分析最初为执行代价设计但 Infer 已将其泛化为可针对不同资源做回归检测。version-1.3.0 文档列出三类资源执行代价execution cost采用简单的顺序执行模型与抽象代价语义SIL 中每条基本指令视为一个单位执行代价分配代价allocation cost只对分配内存的原语操作如new计代价目前处于实验模式因此结果不会写入costs-report.json自动释放池大小autoreleasepool size当对象被加入 Objective-C 的autoreleasepool时计代价通常发生在两种情况非 ARC 代码中显式调用autorelease或非 ARC 被调函数向 ARC 调用方返回autoreleased对象指针反之亦然。对照当前仓库源码代价种类的具体实现位于 infer/src/base/costKind.mltype 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_info对AllocationCost直接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(ArrayListInteger list){ for (int i 0; i list.size(); i){ } }Infer 为中间语言的每条指令赋予符号代价后会静态推断出一个多项式例如8 · |list| 16其中|list|表示列表长度。忽略具体常数该程序的渐近复杂度为O(|list|)即关于输入规模的线性循环。随后开发者在该循环体内加入一个调用void loop(ArrayListInteger 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.mlcosts_current、costs_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.mlcomplexity_increase第 465 行生成%s_COMPLEXITY_INCREASEunreachable_cost_call、infinite_cost_call、expensive_cost_call分别生成%s_UNREACHABLE_AT_EXIT、INFINITE_%s、EXPENSIVE_%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.mdEXECUTION_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.mdEXPENSIVE_EXECUTION_TIME代价非恒定且非 Top实验性默认禁用例如线性代价函数见 infer/documentation/issues/EXPENSIVE_EXECUTION_TIME.mdINFINITE_EXECUTION_TIME无法确定静态上界返回 T未知代价默认禁用见下文未知代价小节见 infer/documentation/issues/INFINITE_EXECUTION_TIME.mdUI 线程判定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.json的is_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.mlBasicCostWithReason除了携带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_TIME、INFINITE_EXECUTION_TIME、EXECUTION_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.mlJSON 报告结构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.json与infer reportdiff它能在不改动运行时、不引入基准测试的前提下于每次代码评审或 CI 中自动发现执行代价的阶数级回归是大型代码库中控制性能退化的低成本方案。赞分享静态分析代码质量开发工具【免费下载链接】inferA static analyzer for Java, C, C, and Objective-C项目地址https://gitcode.com/gh_mirrors/infer/infer点击查看免费下载相关推荐基于静态分析的 WCET 上界推断Infer 成本分析Cost Analysis原理与实战指南基于静态分析的 WCET 上界推断Infer 成本分析Cost Analysis原理与实战指南 本文围绕 Infer 静态分析器中的成本分析Cost A静态分析代码质量开发工具Infer Cost 分析器实战指南基于抽象解释与符号计数的 WCET 静态成本分析Infer Cost 分析器实战指南基于抽象解释与符号计数的 WCET 静态成本分析 本指南以 Infer 开源仓库version 1.1.0官方文档 c静态分析代码质量开发工具Statsmodels分位数回归完整诊断指南残差分析与影响点检测Statsmodels分位数回归完整诊断指南残差分析与影响点检测 Statsmodels是Python中最强大的统计建模库之一其分位数回归功能为数据分析师提数据分析数据科学科研上一篇抖音无水印批量下载工具一个链接存下整个主页下一篇3步轻松备份你的QQ空间历史说说GetQzonehistory完整指南创作声明:本文部分内容由AI辅助生成(AIGC),仅供参考