Infer 注解可达性分析Annotation Reachability检测器从PerformanceCritical到Expensive的调用链追踪【免费下载链接】inferA static analyzer for Java, C, C, and Objective-C项目地址: https://gitcode.com/gh_mirrors/infer/infer导读本文深入讲解 Infer 静态分析器中的Annotation Reachability注解可达性检测器。该检测器允许你定义源注解source→ 汇注解sink的配对例如A与B并会在任意标注了A的方法直接或间接调用标注了B的方法时发出告警。它同时内置了PerformanceCritical到达Expensive、NoAllocation到达new等开箱即用的检查还支持用正则表达式把任意方法建模成仿佛带有某注解从而在完全没有注解的语言中也能工作。读完本文你将掌握该检测器的激活方式、全部命令行参数、自定义源/汇/消毒器配置的 JSON 格式以及它在 Infer 中的底层实现原理。快速激活与支持的语言在infer run或infer analyze时加上--annotation-reachability即可激活该检测器文档原文Activate with--annotation-reachability。激活后Infer 会为每个注解配对执行分析只要存在一条调用路径从标注了源注解的方法出发最终直接或间接到达标注了汇注解的方法就会输出一条告警。支持语言如下表以当前仓库文档为准语言支持状态C / C / ObjC支持C# / .NET不支持Erlang支持Hack不支持Java支持Python不支持Rust不支持Swift实验性支持需要说明的是虽然 Java 是主战场源码中大量逻辑针对Procname.Java但 C/C/ObjC 与 Erlang 同样受支持Erlang 的方法名在建模正则匹配时使用了Verbose级别的名称打印见 annotationReachability.ml 中check_modeled_annotation的Procname.is_erlang分支这与 Java/C 使用的FullNameOnly不同。内置检查除了用户自定义的源/汇配对检测器还内置了两组标准检查分别由独立开关控制PerformanceCritical→Expensive开启--annotation-reachability-expensive后检测器会检查标注了PerformanceCritical的方法是否调用了昂贵方法。昂贵的定义在源码中为标注了Expensive的方法或被建模为昂贵的方法。对应的实现是 annotationReachability.ml 中的ExpensiveAnnotationSpeclet spec { kind ExpensiveAnnotationSpec ; sink_predicate (fun tenv pname - let has_annot ia Annotations.ia_ends_with ia expensive_annot.class_name in check_attributes has_annot tenv pname || is_modeled_expensive tenv pname ) ; source_annotation_list [performance_critical_annot] ; issue_type IssueType.checkers_calls_expensive_method ; ... }check_attributes会同时检查方法自身的注解与所在类上的注解is_modeled_expensive则调用Inferconfig.modeled_expensive_matcher即用--modeled-expensive系列正则配置把方法建模成昂贵方法。此外该 Spec 还带一个pre_checkcheck_expensive_subtyping_rules会在分析阶段检查覆盖override了未注解父类方法却又标注Expensive的方法并报告CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED源码中实际使用的IssueType为checkers_expensive_overrides_unexpensive提醒开发者这种标注违背了 Liskov 替换原则。NoAllocation→new开启--annotation-reachability-no-allocation后检测器会检查标注了NoAllocation的方法是否发生了内存分配。对应实现为NoAllocationAnnotationSpeclet spec { kind NoAllocationAnnotationSpec ; sink_predicate (fun tenv pname - is_allocator tenv pname) ; sanitizer_predicate (fun tenv pname - check_attributes Annotations.ia_is_ignore_allocations tenv pname) ; sink_annotation dummy_constructor_annot ; source_annotation_list [no_allocation_annot] ; issue_type IssueType.checkers_allocates_memory ; ... }这里的汇不再是某个真实注解而是一个伪构造器注解__infer_is_constructor。is_allocator判定调用构造器即为分配但排除了Throwable子类与BuiltinDecl声明的内置函数。值得注意的细节是字段访问也会被建模为分配式的伪调用。源码中字段访问被替换成名为__infer_field_字段名的伪方法dummy_pname_for_field因此在 Java 中NoAllocation方法里读取Sil.Load一个字段也会被视为汇路径报告时用 accesses 而不是 calls 描述见report_src_to_snk_path中的access_or_call逻辑。而标注了IgnoreAllocations即源码Annotations.ignore_allocations的方法可作为消毒器sanitizer阻断该路径。同一方法既是源又是汇开启--annotation-reachability-report-source-and-sink后若某方法同时满足源注解与汇注解的判定检测器会单独报告一条长度为 0 的路径report_src_and_sink因为这种情形不存在真实的调用点。全部命令行参数以下参数定义位于 Config.ml约第 578–635 行均属于infer analyzeJava 手册条目manual_java类参数可在命令行以--annotation-reachability-*形式传入参数类型默认值说明--annotation-reachabilityboolfalse激活整个检测器在 Checker.ml 中注册--annotation-reachability-apply-superclass-annotationsbooltrue是否把超类/接口上的注解也应用到未被其覆盖的方法上--annotation-reachability-check-loopsboolfalse开启后在 trace 中标记嵌套在循环内的调用点is_in_loop信息--annotation-reachability-custom-modelsJSON空列表用正则把方法建模为仿佛带有某注解--annotation-reachability-custom-pairsJSON空自定义源/汇/消毒器配对--annotation-reachability-expensiveboolfalse检查PerformanceCritical调用Expensive/建模昂贵方法--annotation-reachability-no-allocationboolfalse检查NoAllocation方法是否分配内存--annotation-reachability-report-source-and-sinkboolfalse报告同时标注为源与汇的方法其中--annotation-reachability-apply-superclass-annotations直接决定check_attributes中使用PatternMatch.Java.check_class_attributes含超类还是check_current_class_attributes仅当前类--annotation-reachability-check-loops控制是否调用Procdesc.Loop.compute_loop_nodes计算循环节点并把 inside a loop 信息写进 trace。自定义配对custom pairs源、汇与消毒器--annotation-reachability-custom-pairs接受一个 JSON 列表每个元素定义一个或多个配对{ sources: [Source1, Source2], sinks: [Sink1], sanitizers: [Sanitizer1], name: MyCheck, description: 自定义检查说明, minimize_sources: true, minimize_sinks: false }字段说明依据 Config.ml 的文档字符串与 annotationReachability.ml 中的custom_spec类型定义sources必填源注解类名列表任意方法标注了其中之一即视为源sinks必填汇注解类名列表每个汇会生成一个独立的 spec见parse_custom_specs中对 sinks 的List.mapsanitizers可选默认[]消毒器注解列表。若调用链中间某方法或最终被调者标注了消毒器注解该路径会被阻断sanitizer_predicate返回 true 时astate不变、不记录调用点name可选默认报告名称前缀将追加在 issue 描述的开头description可选默认附加描述追加在 issue 描述末尾minimize_sources可选默认false开启后若一条源→汇路径的后缀本身也是一条源→汇路径则不再重复报告。例如存在source1() - source2() - sink()时只报告source2() - sink()minimize_sinks可选默认true开启后若一条源→汇路径的前缀本身也是一条源→汇路径则不再重复报告。例如存在source() - sink1() - sink2()时只报告source() - sink1()。注意注解类名的匹配方式是ia_ends_with即按类名后缀匹配见 annotations.ml 的annot_ends_with因此上述 JSON 示例中写Source1可匹配com.my.annotation.Source1无需写出完整包名。对应报告类型为CHECKERS_ANNOTATION_REACHABILITY_ERROR源码中StandardAnnotationSpec统一使用IssueType.checkers_annotation_reachability_error。自定义建模custom models让没有注解的方法带上注解--annotation-reachability-custom-models接受一个 JSON对象映射用正则表达式把方法建模为仿佛标注了某注解。格式依据 Config.ml 的文档字符串{ Annotation: [com\\.Myclass\\.foo.*] }等价于更精细的 allow/block 形式{ Annotation: { allow: [foo.*], block: [foobar] } }语义当 allow 列表中任一正则匹配方法名、且 block 列表中无任何正则匹配时该方法被当作标注了Annotation。若只有 allow 匹配器可以直接用字符串列表代替对象旧格式。解析逻辑位于parse_custom_models它区分\List _旧格式全部为正匹配与Assoc _新格式拆成allow/block两个正负匹配器列表正则使用 OCamlStr.regexp并通过Str.string_match ... 0从头匹配完整方法名。在check_modeled_annotation中方法名的生成取决于语言Erlang 用Verbose打印其他语言用FullNameOnly因此不同语言下正则需要匹配的字符串形式不同。这一机制让检测器在没有任何注解的语言/代码库中同样可用——只需用正则把关键方法建模成源或汇即可。报告的问题类型Issue Types该检测器共上报以下问题类型来自文档的 List of Issue Types 一节问题类型含义与触发场景CHECKERS_ALLOCATES_MEMORYNoAllocation方法直接或间接执行了分配/字段访问伪调用CHECKERS_ANNOTATION_REACHABILITY_ERROR自定义源注解方法到达自定义汇注解方法CHECKERS_CALLS_EXPENSIVE_METHODPerformanceCritical方法到达Expensive或建模为昂贵的方法CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED方法覆盖了未标注Expensive的父类/接口方法自身却标注了Expensive底层原理Interprocedural 摘要与调用链回溯从源码结构看该检测器是一个典型的过程间interprocedural数据流分析核心组件集中在 annotationReachability.ml 与 annotationReachabilityDomain.ml1. 域Domain结构。域是一个两层映射Annot.t → SinkMap其中SinkMap Procname.t → CallSitesCallSites是call_site_info的有限集合call_site_info {call_site: CallSite.t; is_in_loop: bool}。即某个汇注解 → 可能到达的汇方法 → 该汇方法被调用时的调用点集合。每一次函数调用都会记录其调用点call site与被调者为后续回溯路径提供证据。2. 转移函数Transfer Functions。MakeTransferFunctions处理两类指令Sil.Call对每个 spec先判断被调者是否满足sink_predicate是则记录直接调用再通过add_transitive_calls读取被调者的摘要analyze_dependency callee_pname把被调者能到达的汇调用点传播到当前函数间接调用Sil.Load仅 Java把字段访问转换成伪方法调用__infer_field_字段名从而让NoAllocation等检查能覆盖字段访问。3. 路径回溯与报告。分析收敛后check_srcs_and_find_snk对每个标注了源注解的方法从它出发沿SinkMap递归step_forward向前走直至到达汇方法end_of_stack期间用add_to_trace逐层构建调用链 trace每个 trace 元素包含调用位置与被调者定义位置。find_paths_to_snk中对每个汇过程只挑选一个调用点前推CallSites.min_elt以避免路径爆炸。当调用链超过 3 个元素源定义 调用点 汇定义时报告描述中会出现 transitively传递到达字样。4. 最小化与消毒。minimize_sources/minimize_sinks在step_forward中通过method_overrides_annot检查中间方法是否也是源/汇是则剪枝该路径消毒器则在check_direct_call与add_transitive_calls两处同时生效被调者为消毒器、或当前调用者为消毒器均阻断。5. 伪方法还原。报告阶段通过get_original_pname把__infer_field_*、__infer_is_constructor等伪名还原为真实字段/构造器名并区分 accesses字段访问与 calls方法调用的措辞若注解来自基类方法或接口报告会追加 , inherited from ... 与 , defined on ... 说明来源。从注册信息看该检测器位于 checkers/annotationReachability.ml 的checker入口由registerCheckers.ml登记其结果作为 payload 保存在Payloads中供跨函数摘要复用每次分析都会执行parse_custom_specs与建模解析并合并内置 specexpensive_specs no_alloc_specs custom_specs。典型使用示例以 Java 为例假设业务代码中有PerformanceCritical public void render() { draw(); } Expensive public void draw() { /* 昂贵操作 */ }运行infer run --annotation-reachability-expensive -- javac MyApp.java检测器将报告一条CHECKERS_CALLS_EXPENSIVE_METHODrender标注PerformanceCritical传递到达此处为直接调用标注Expensive的draw。若draw本身没有注解但满足正则建模也可通过--annotation-reachability-custom-models把它建模为昂贵方法infer run --annotation-reachability-expensive \ --annotation-reachability-custom-models {Expensive: [com\\.example\\.MyApp\\.draw]} \ -- javac MyApp.java再如自定义配对源A到达汇B其中间方法标注Sanitizer可阻断infer run --annotation-reachability \ --annotation-reachability-custom-pairs \ {sources: [A], sinks: [B], sanitizers: [Sanitizer]} \ -- javac MyApp.java报告文本格式由report_src_to_snk_path生成大致形如Method render (annotated with PerformanceCritical) calls draw (annotated with Expensive)并附带从源定义到汇定义的完整 trace字段访问场景则表现为... accesses 字段 ...。小结Annotation Reachability 是 Infer 中一个高度可配置的过程间数据流检测器既有PerformanceCritical → Expensive、NoAllocation → 分配两条内置检查线也允许通过 JSON 自定义源/汇/消毒器配对还能用正则建模让没有注解的语言与代码库参与分析。结合 annotationReachability.ml 中摘要传播 调用点记录 路径回溯的实现你可以把它改造成符合自身架构约束的调用链守卫例如性能红线、资源配额、安全策略传播等场景。【免费下载链接】inferA static analyzer for Java, C, C, and Objective-C项目地址: https://gitcode.com/gh_mirrors/infer/infer创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考