静态分析代码质量开发工具【免费下载链接】inferA static analyzer for Java, C, C, and Objective-C项目地址https://gitcode.com/gh_mirrors/infer/infer点击查看免费下载在 Erlang 这种以模式匹配、消息传递和让它崩溃哲学著称的函数式语言中静态分析的价值尤为特殊许多运行时错误如列表模式匹配失败并不需要等到生产环境才暴露。本文基于 Infer 仓库中 Erlang 分析器的一手资料infer/src/erlang/README.md系统讲解如何在 Erlang 代码上运行 Infer包括环境构建、使用 Pulse 检测no match of rhs等可靠性问题以及通过 Topl 自定义时序属性写已关闭文件、污点传播等实现远超内置检查器的用户级规则。读完本文你将掌握infer -- erlc的完整用法并能用.topl属性文件把业务级安全规则编码为可自动执行的静态检查。环境准备构建 Erlang 分析器使用 Infer 分析 Erlang 代码前需要先从源码安装 Infer。与默认同时构建 Java 和 C/ObjC 分析器不同Erlang 分析器需要显式指定构建目标./build-infer.sh erlang从 build-infer.sh 的源码可以看到erlang是脚本支持的独立构建目标之一与clang、java、hack、python并列。脚本内部通过CONFIGURE_PREPEND_OPTS --disable-c-analyzers等方式组合配置选项如果在 configure 阶段指定了--disable-erlang-analyzers则 Erlang 分析器会被跳过所以务必确认构建日志中包含 Erlang 支持。除了 Infer 本身还必须安装 Erlang 编译器erlc——它是 Infer 捕获 Erlang 源码的入口工具。此外分析 OTP 库函数如file:write/2时推断模块来自 OTP 的信息会显著提升分析质量因此建议安装完整的 Erlang/OTP 发行版。Erlang 前端工作原理从 erlc 到 SIL 的完整链路在动手跑命令之前先理解 Infer 如何读懂 Erlang这有助于你判断分析结果的适用范围。整条链路分布在 infer/lib/erlang/ 与 infer/src/erlang/ 中包装编译器用户在命令行调用infer -- erlc ...时Infer 实际执行的是 erlang.sh一个 bash 包装脚本它调用 erlang.escript 生成一条新的编译命令。注入 parse transformerlang.escript 会先用erlc -o tmp/ebin infer_parse_transform.erl编译仓库自带的 infer_parse_transform.erl然后通过修改erl_opts强制追加debug_info和{parse_transform, infer_parse_transform}把记录编译文件列表的逻辑注入到erlc或rebar3的调用参数中脚本支持--with_otp_specs选项用于把 OTP 模块的 spec 一并纳入分析。抽取 AST编译完成后extract.escript 从.beam文件的abstract_codechunk 中恢复 Erlang 抽象语法树要求编译时带debug_info按模块输出为 JSON 文件支持--beam、--directory、--list、--otp多种 beam 来源方式--specs-only则只保留-spec、-type等声明。解析与翻译ErlangJsonParser.ml 将 JSON 解析为 ErlangAst.ml 中定义的抽象形式对应 Erlang 官方 abstract format随后 ErlangScopes.ml 的annotate_scopes为变量标注词法作用域ErlangEnvironment.ml 的initialize_environment建立模块级环境记录 record、type、spec、import/export 等信息最后由 ErlangTranslator.ml 的translate_module将每个函数翻译成 Infer 的中间表示 SIL CFG。翻译器会为 Erlang 值建立统一的盒装表示例如原子通过内置函数__erlang_make_atom创建、整数通过__erlang_make_integer创建字段加载通过Env.load_field_from_expr生成指令。对暂不支持的构造翻译器会生成call_unsupported占位调用模块名固定为unsupported。理解这一点后你就能预期分析结果覆盖的是翻译器支持的语言子集遇到不支持构造时相关路径会被保守处理。可靠性检查用 Pulse 检测 no match of rhsErlang 中形如Pattern Expr的匹配表达式match expression当右侧值与左侧模式不兼容时会抛出badmatch运行时错误。Infer 的 Pulse 分析器可以在静态层面发现这类问题报告的 issue 类型即 no match of rhs。将下面的代码保存为ex1.erl原样取自 README-module(ex1). -export([bad/0, good/0]). bad() - [H | _] get_list(0), H. good() - [H | _] get_list(2), H. get_list(X) when X 0 - []; get_list(X) when X 0 - [X | get_list(X - 1)].关键点在于get_list(0)返回空列表[]此时[H | _] []必然匹配失败而get_list(2)返回[2 | get_list(1)]可以正常解构。运行infer --pulse-only -- erlc ex1.erl--pulse-only表示只运行 Pulse 这一分离逻辑分析器Pulse 也是 Topl 的底层基础。分析结束后在infer-out/report.txt或通过infer explore交互查看中会看到bad/0处的 no match of rhs 报告而good/0不会报警。这一场景对应 infer/tests/codetoanalyze/erlang/ 下的端到端测试测试驱动脚本 erlc.make 展示了与 README 等价的调用形态——$(INFER_BIN) $(INFER_OPTIONS) -- erlc -o _build $(SOURCES)即让erlc作为真实编译器参与捕获Infer 拦截其产物进行分析。用户自定义属性Topl 时序属性框架内置检查器覆盖不了所有需求。Infer 提供ToplTemporal Property framework基于 Pulse 构建用于静态验证时序属性把一段属性文件描述的非确定性自动机翻译成分析任务当程序执行能从起始状态驱动到error状态时即报告问题。完整的属性语言参考见 infer/documentation/checkers/Topl.md。Topl 属性的通用形式如下property Name message Optional error message // 可省略 prefix Prefix // 可有 0、1 或多条 sourceState - targetState: Pattern(Arg1,...,ArgN,Ret) when Condition ActionPattern决定哪类指令驱动该转移可以是匹配函数名的正则方法有 N 个参数时需绑定 N1 个转移变量前 N 个绑定实参、最后一个绑定返回值即使返回类型是 void 也如此也可以是特殊关键字#ArrayWrite标签*表示任何情况下都触发的转移。Condition是布尔条件可引用转移变量、寄存器支持比较运算符、!、、、、、合取、整数常量以及字段访问Identifier:Type.FieldName如X:Cons.head目前仅 Erlang 支持和可达性谓词Ident1 ~~ Ident2表示Ident2可从Ident1经指针/字段在堆上到达。Action是寄存器赋值序列形式为register : TransitionVariable小写字母开头的标识符即寄存器无需声明。场景一写入已关闭文件WriteAfterClose这是 README 提供的第一个完整示例。先创建属性文件WriteAfterClose.toplproperty WriteAfterClose start - start: * start - closed: file:close/1(A,Ret) f:A closed - error: file:write/2(F,D,Ret) when Ff该自动机有三个状态start起始、closed文件已关闭、error出错。start - start: *表示属性可以在程序的任意位置开始跟踪当调用file:close/1时把第一个实参保存到寄存器f并转移到closed当在closed状态下调用file:write/2且其文件参数F等于之前关闭的那个文件f时进入error。注意这里把模式写成file:close/1这种带引号、含斜杠的精确函数名形式对应测试目录 file/property.topl 中的写法。再创建被测模块ex2.erl-module(ex2). -export([bad/1,good/1]). good(F) - nop(F), file:write(F, hi). bad(F) - op(F), file:write(F, hi). nop(_) - ok. op(F) - file:close(F).good/1在file:write/2前只做了无副作用的nop而bad/1先调用了op/1内部执行file:close(F)再写文件明显违反属性。运行infer --topl-only --topl-properties WriteAfterClose.topl -- erlc ex2.erl参数含义--topl-only只运行 Topl 分析--topl-properties指定属性文件路径该选项在 infer/src/base/Config.ml 中定义为路径列表支持重复传入多个属性文件当前标注为 EXPERIMENTAL。运行后 Infer 会报告bad/1中的TOPL_ERROR并给出完整 tracecall to file:close/1→call to file:write/2。仓库中的同类测试见 topl_file.erl 与 issues.exp其期望输出正是上述两步调用链。场景二污点传播TaintREADME 中 Taint 小节没有给出代码但仓库测试补全了完整的可运行版本。基础污点属性的写法测试 taint/property.topl如下property Taint message a value returned by source/0 is sent as argument to sink/1 prefix topl_taint start - start: * start - tracking: source(Ret) x : Ret tracking - error: sink(Arg, VoidRet) when x Arg解读source(Ret)的返回值存入寄存器x转移至tracking此后任何sink(Arg, VoidRet)调用只要实参Arg与x相等就触发error。prefix topl_taint声明前缀用于把source这样的裸模式扩展为topl_taint:source一类的全限定匹配。配套的被测模块 topl_taint.erl 提供了大量_Bad/_Ok命名约定用例test_a_Bad() - sink(source()). % 直接污点 → 报告 test_b_Ok() - sink(1). % 干净数据 → 不报告 test_c_Bad() - X source(), sink(X). % 变量中转 → 报告 test_d_Bad() - call_sink_indirectly(tito(source())). % 跨函数传递 → 报告值得注意的细节sink/1的实现是sink(dirty) - erlang:error(taint_error); sink(_) - ok.即它在运行时确实会因dirty崩溃——注释中说明这是为了让 TOPL 测试不与 Pulse 的运行时崩溃检测相互干扰而特意设计的。消息传递send/receive污点Erlang 进程间的!send与receive是污点分析的难点但 Topl 测试仍见 topl_taint.erl 的test_send*系列证明 Infer 对命名函数spawn(topl_taint, tito_process, [])形式的进程通信可以建模fn_test_send2_Bad这类把source()经 tito 进程转发的用例能报告污点而匿名fun形式的进程fn_test_send6_Bad目前无法跟踪测试注释明确说明其违规不会被报告。这些用例是理解分析器能力边界的第一手资料。场景三带转换的污点Taint with TransformationsREADME 的第三个标题 Taint with Transformations 同样未给出代码仓库中以taint-genserver和specs两个测试目录展示了带转换的两种形态用 spec 声明污点源specs/property.toplproperty SourceIsSpec start - start: * start - track: specs:__infer_assume_type_dirty(Arg, Ret) when Ret ! 0 dirty : Arg track - error: .*:sink(Arg, Ret) when Arg dirty这里__infer_assume_type_dirty是 Infer 前端注入的辅助函数配合--with_otp_specs捕获的 OTP spec 使用when Ret ! 0表示断言失败假定类型不匹配时才把参数标记为脏数据等价于把 spec 约束转换为污点源而模式.*:sink展示了正则写法——不限定模块名匹配任意模块中的sink函数。GenServer 场景taint-genserver/property.topl把source/0带斜杠的精确 arity 匹配等模式用于追踪经gen_server:call往返传播的污点数据演示属性从单函数调用向跨模块、跨进程转换的扩展。更多属性能力字段、区间与可达性测试目录 infer/tests/codetoanalyze/erlang/topl/ 还展示了若干进阶写法字段访问条件fields/property.topltopl_fields:bar(T, R) when 11 (T:Cons.head):Integer.value——对 Erlang cons 列表的头部字段做数值比较支持链式字段访问。区间检查less/property.toplwhen 11 T:Integer.value T:Integer.value 14组合多个条件。堆可达性reach-simple/property.topltrack - error: sink(Arg, Ret) when Arg ~~ dirty——不要求实参与寄存器相等只要脏对象能沿字段从Arg可达即判违规。跨函数的状态机process/property.toplerlang:exit(Pid, Reason, Ret) pid:Pid后用erlang:send匹配对应向已终止进程发消息的业务规则issues.exp中可见SendAfterClose.start[2]~~SendAfterClose.closed[0]这类状态跳转 trace 输出。若要查看某个属性的详细执行路径可运行infer explore交互式查看每条TOPL_ERROR的完整 trace。测试体系如何验证你的属性文件仓库为 ErlangTopl 提供了完整的端到端测试体系可作为自己编写属性时的参考答案每个测试目录如 file、taint、fields包含三件套被测.erl源码、property.topl属性文件、Makefile声明INFER_OPTIONS --topl-only --topl-properties property.topl --enable-issue-type TOPL_ERROR_LATENT。期望输出记录在issues.exp中形如codetoanalyze/erlang/topl/file/topl_file.erl, bad/1, 0, TOPL_ERROR, no_bucket, ERROR, [...]包含函数名、issue 类型TOPL_ERROR/TOPL_ERROR_LATENT以及 trace 中每一步触发的函数调用。驱动脚本 erlc.make 显示测试通过$(INFER_BIN) --results-dir ... $(INFER_OPTIONS) -- erlc -o _build $(SOURCES)运行与你手动执行 README 命令的形态完全一致。编写自己的属性时可参照以下路径快速起步先抄一个最简start - start: * 两个业务转移的属性骨架用message给出可读的错误描述再对照infer explore的 trace 逐步细化when条件。已知局限与性能注意基于 Topl.md 与 Erlang 前端源码使用时有几点需要明确误报少、漏报多Topl 建立在 Pulse 之上Pulse 以最小化误报为目标代价是可能漏报false negative这是设计取舍。寄存器数量决定分析成本属性内寄存器越多分析时间增长越快。多个属性各自使用少量寄存器时理论上影响可控当前实现尚未充分优化单个属性内寄存器过多则指数级开销难以避免。仓库实践中的经验值是最多 3 个寄存器。前端覆盖范围Erlang 翻译器ErlangTranslator.ml对不支持的语言构造生成call_unsupported占位节点见源码中的call_unsupported函数这些构造处的分析精度会下降fun匿名函数的进程通信目前也无法跟踪见上文fn_test_send6_Bad用例。OTP 支持erlang.escript的--with_otp_specs选项可纳入 OTP 模块的 spec帮助属性匹配file:*、maps:*等内置函数分析 OTP 相关代码时建议启用并保证 OTP 库可用。属性匹配的粒度方法名模式是正则而非精确比较source会同时匹配source/0、source/1等不同 arity需要精确 arity 时应写成source/0这种带斜杠的形式taint-genserver 中可见该用法。总结在 Erlang 上运行 Infer 的完整心智模型可以概括为三步用./build-infer.sh erlang构建分析器并确保erlc可用通过infer -- erlc走完parse transform → beam 抽取 AST → JSON → SIL CFG的捕获链路再根据目标选择分析器——内置可靠性检查用--pulse-only如 no match of rhs自定义业务规则用--topl-only --topl-properties xxx.topl。文中所有示例代码均可原样复制运行属性语法、测试期望输出与源码实现都可在 infer/src/erlang/README.md、infer/tests/codetoanalyze/erlang/topl 与 infer/src/topl 中交叉验证。赞分享静态分析代码质量开发工具【免费下载链接】inferA static analyzer for Java, C, C, and Objective-C项目地址https://gitcode.com/gh_mirrors/infer/infer点击查看免费下载相关推荐Infer Topl 状态机时序属性分析框架从属性定义到源码实现Infer Topl 状态机时序属性分析框架从属性定义到源码实现 Topl 是构建在 InferFacebook/Meta 开源的 Java、C、C、O静态分析代码质量开发工具Infer 中的 Topl 时序属性分析框架从污点传播到自定义状态机检查Infer 中的 Topl 时序属性分析框架从污点传播到自定义状态机检查 导读 ToplTemporal properties时序属性是构建在 Infe静态分析代码质量开发工具GoFr 统一认证指南为 HTTP 与 gRPC 服务启用 Basic Auth、API Key 与 OAuth 2.0/JWTGoFr 统一认证指南为 HTTP 与 gRPC 服务启用 Basic Auth、API Key 与 OAuth 2.0/JWT GoFr gofr.dev静态分析代码质量开发工具创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考