Infer 静态分析：CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED 错误详解与 @Expensive 子类型规则

静态分析代码质量开发工具【免费下载链接】inferA static analyzer for Java, C, C, and Objective-C项目地址https://gitcode.com/gh_mirrors/infer/infer点击查看免费下载导读本篇技术指南围绕 Facebook Infer 静态分析器的CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED错误类型展开它由 Annotation Reachability注解可达性检查器在注解可达性代价模型下触发当一个标注了Expensive昂贵的方法覆盖了一个未标注该注解的方法时Infer 会报告该错误以维持Expensive注解在继承体系上的类型系统一致性。读完本文你将理解该错误的语义与触发条件、它在注解可达性框架中的底层实现原理、如何修复与抑制以及如何通过命令行参数启用相关检查并运行仓库内置测试用例验证行为。错误含义Expensive覆盖了未标注方法根据仓库中的官方错误文档 CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED.md该错误的完整定义是A method annotated withExpensiveoverrides an un-annotated method.一个标注了Expensive的方法覆盖了一个未标注的方法。该错误在 Infer 的 issue 注册表中登记如下IssueType.mllet checkers_expensive_overrides_unexpensive register ~category:NoCategory ~id:CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED ~hum:Expensive Overrides Unannotated Error AnnotationReachability ~user_documentation:[%blob ./documentation/issues/CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED.md]issue idCHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED可读名称humExpensive Overrides Unannotated类别categoryNoCategory不属于缺陷、资源泄漏等预定义类别严重级别Error所属检查器AnnotationReachability注解可达性这一规则本质上是一条子类型sub-typing一致性规则Expensive注解被当作一个可继承的类型约束如果父类或接口中的方法没有标注它子类实现却标注了就破坏了继承链上的注解一致性Infer 会将其判定为一个需要修正的违规。触发场景与官方示例官方文档给出了触发该错误的完整示例接口 实现类interface I { void foo(); } class A implements I { Expensive public void foo() {} }I.foo()在接口中未标注Expensive而A.foo()作为其实现被标注为Expensive因此 Infer 报告CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED。这个示例在仓库的测试用例中得到了完整复刻。查看 ExpensiveSubtypingExample.java它继承自ExpensiveInterfaceExample.C并新增了带注解的重写方法package codetoanalyze.java.checkers; import com.facebook.infer.annotation.Expensive; public class ExpensiveSubtypingExample extends ExpensiveInterfaceExample.C { Expensive public void m3() {} public void m4() {} }对应的期望输出expected issue记录在 issues.expcodetoanalyze/java/annotreach/basic/ExpensiveSubtypingExample.java, codetoanalyze.java.checkers.ExpensiveSubtypingExample.m3():void, 0, CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED, no_bucket, ERROR, []注意该记录中 trace 为空[]因为它是pre_check预检查阶段在方法定义处直接报告的类型系统违规不涉及调用路径。底层实现ExpensiveAnnotationSpec 与子类型检查该错误的判定逻辑实现在 annotationReachability.ml 的ExpensiveAnnotationSpec模块中第 454-501 行。其中核心函数是check_expensive_subtyping_rules第 463-475 行let check_expensive_subtyping_rules {InterproceduralAnalysis.proc_desc; tenv; err_log} overridden_pname let proc_name Procdesc.get_proc_name proc_desc in let loc Procdesc.get_loc proc_desc in if not (method_is_expensive tenv overridden_pname) then let description Format.asprintf Method %a overrides unannotated method %a and cannot be annotated with %a MF.pp_monospaced (Procname.to_string proc_name) MF.pp_monospaced (Procname.to_string overridden_pname) MF.pp_monospaced ( ^ Annotations.expensive) in Reporting.log_issue proc_desc err_log ~loc AnnotationReachability IssueType.checkers_expensive_overrides_unexpensive description逻辑要点如下触发时机该检查挂在pre_check回调中第 492-498 行。当当前过程proc_name自身被判定为Expensiveis_expensive tenv proc_name时通过PatternMatch.override_iter遍历其所有被覆盖的方法基类方法或接口方法。判定条件对每个overridden_pname若method_is_expensive tenv overridden_pname为假——即被覆盖的方法既没有Expensive注解is_expensive也不匹配“modeled expensive”模型is_modeled_expensive见第 54-64 行用于把某些内置函数按Expensive建模——则在当前方法定义位置loc报告该错误。报告文本格式为Method 子类方法 overrides unannotated method 被覆盖方法 and cannot be annotated with Expensive。可见该错误报告的并不是“方法调用了昂贵方法”而是继承体系上注解标注不一致这一纯类型层面的违规。为什么需要这条规则注解可达性的子类型语义要理解这条规则的动机需要回到ExpensiveAnnotationSpec的整体设计annotationReachability.ml源sourcePerformanceCritical——标注了它的方法中不允许调用昂贵方法汇sinkExpensive——标注了它的方法被视为昂贵调用目标当PerformanceCritical方法直接或传递地调用Expensive方法时报告配套错误CHECKERS_CALLS_EXPENSIVE_METHOD定义见 CHECKERS_CALLS_EXPENSIVE_METHOD.md注册于 IssueType.ml。测试文件 ExpensiveInheritanceExample.java 的注释第 33-37 行明确解释了这条子类型规则的用途The objective of this test is to document the limitations of the checker, which just implements a type system. This means that the checker is flow insensitive and is only based on the static type information. Especially, it does not try to resolve dynamic dispatch. However, the checker is still exhaustive thanks to the sub-typing rule for the Expensive annotation.翻译过来该检查器只实现了一个类型系统它是流不敏感flow insensitive的、仅依赖静态类型信息并不尝试解析动态分发dynamic dispatch。因此当通过基类引用调用方法时Infer 只能依据静态类型判断目标是否昂贵正是因为Expensive的子类型规则——一旦子类实现被标注为昂贵任何以父类类型引用发生的调用都会被保守地视为昂贵调用——检查才是穷尽的exhaustive不会漏报。而CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED正是这条子类型规则在继承边界上的“前提守卫”。该测试文件issues.exp也验证了相关行为reportsBecauseFooIsExpensiveInA(A a)以类型A调用a.foo()时虽然实际对象可能动态分派到未标注的B.foo()Infer 仍按静态类型A报告CHECKERS_CALLS_EXPENSIVE_METHOD而doesReportBecauseTypeFlowInsensitive(A a)表明即使代码中写了instanceof B分支Infer 也不会做流敏感分析依然照A.foo报告。如何修复让继承链上的注解保持一致由于该错误只在被覆盖方法未标注Expensive时触发源码判定条件if not (method_is_expensive tenv overridden_pname)修复方式有两种补齐基类/接口注解在接口或基类方法上同样标注Expensive使子类重写不再构成注解不一致。仍以官方示例为例interface I { Expensive void foo(); } class A implements I { Expensive public void foo() {} }移除子类注解如果该方法实际并不昂贵则去掉A.foo()上的Expensive使其与未标注的父类方法保持一致此时代价检查器将不再把A.foo视作昂贵目标但继承自父类未标注方法的一切调用也都不再被报告为昂贵调用。选择哪种方式取决于业务语义只有当重写方法确实昂贵例如涉及网络、数据库或重计算时才应当补齐注解否则应移除。如何抑制SuppressLint 与命令行开关基于注解抑制该错误属于Error级别的检查器报告与 Infer 其他检查器一样支持SuppressLint按位抑制。仓库测试 ExpensiveInheritanceExample.java 就展示了这种用法SuppressLint(CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED) // Suppressing the sub-typing violation warning here as foo() is not annotated as Expensive // in the interface. This report is legit but is not relevant for the current test. Expensive public void foo() {}该测试借助SuppressLint(CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED)屏蔽了这条“合法但与当前测试无关”的报告以便集中验证调用侧行为。命令行启用CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED由 Annotation Reachability 检查器在启用代价检查时触发。对应的开关定义于 Config.mland annotation_reachability_expensive CLOpt.mk_bool ~long:annotation-reachability-expensive ~in_help:InferCommand.[(Analyze, manual_java)] ~default:false check if methods annotated with PerformanceCritical can call expensive methods (annotated \ Expensive or modeled, with annotation reachability checker)参数名--annotation-reachability-expensive默认值false不启用启用后检查PerformanceCritical方法是否可能调用Expensive或按模型视为昂贵的方法并一并启用上述子类型一致性检查因为ExpensiveAnnotationSpec.spec只在Config.annotation_reachability_expensive为真时才被加入检查器规格列表见 annotationReachability.ml。例如在项目根目录下对 Java 工程执行infer run --annotation-reachability-expensive -- javac Example.java另外--annotation-reachability-apply-superclass-annotations控制注解查找是否上溯到父类默认行为见check_attributes第 115-127 行会影响“被覆盖方法是否已标注”的判定范围。局限性与注意事项从源码和测试可以总结出以下边界使用时应心中有数仅针对 Javacheck_attributes与子类型遍历逻辑只对Procname.Java生效annotationReachability.ml该检查器面向 Java 代码不适用于 C/C/OC 等其他前端。静态类型驱动、流不敏感如前所述它不解析动态分发也不关心运行时类型instanceof等分支不会影响判定ExpensiveInheritanceExample.java。与CHECKERS_CALLS_EXPENSIVE_METHOD的联动本错误是注解一致性层面的“守卫”而调用侧违规由CHECKERS_CALLS_EXPENSIVE_METHOD报告两者同属 Annotation Reachability 检查器可通过--annotation-reachability-expensive一并启用。模型化方法某些未加注解的方法可能通过--annotation-reachability-custom-models旧格式或--annotation-reachability-custom-pairs含 allow/block 正则的新格式见 Config.ml被“modeled as”昂贵方法从而不触发本错误。总结CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED是 Infer 注解可达性检查器为维持Expensive子类型规则一致性而设置的类型级守卫它强制“昂贵”注解在继承链上要么父接口/基类同步标注、要么子类移除标注从而保证PerformanceCritical方法调用检查在静态类型层面不会漏报。理解它的触发条件、底层实现annotationReachability.ml、修复与抑制方式以及--annotation-reachability-expensive开关的语义你就能在 Java 项目中正确部署代价注解体系并准确解读 Infer 产出的相关报告。赞分享静态分析代码质量开发工具【免费下载链接】inferA static analyzer for Java, C, C, and Objective-C项目地址https://gitcode.com/gh_mirrors/infer/infer点击查看免费下载相关推荐Ty 类型检查器中 duplicate-base 规则详解Ruff 如何静态捕获重复基类错误Ty 类型检查器中 duplicate base 规则详解Ruff 如何静态捕获重复基类错误 导读 duplicate base 是 ruff 仓库中 Ty开发工具Lint格式化静态分析CLIInfer 的 BAD_GENERATORErlang 推导式生成器类型错误的静态检测Infer 的 BAD_GENERATORErlang 推导式生成器类型错误的静态检测 本篇文章基于 Facebook Infer 开源仓库Java、C、C静态分析代码质量开发工具Roc 类型系统详解静态类型、结构类型、Nominal 类型与泛化规则Roc 类型系统详解静态类型、结构类型、Nominal 类型与泛化规则 Roc 是一门静态类型、类型可推断的语言——你很少需要手写类型但写了就会被检查。本文创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考