前往小程序,Get更优阅读体验!
立即前往
首页
学习
活动
专区
工具
TVP
发布
社区首页 >专栏 >Infer#:将 Facebook 的静态分析器带工具带到 C# 和 .NET

Infer#:将 Facebook 的静态分析器带工具带到 C# 和 .NET

作者头像
张善友
发布2020-12-29 10:51:32
1.3K0
发布2020-12-29 10:51:32
举报
文章被收录于专栏:张善友的专栏

NET团队借助Infer#,将Facebook的跨程序静态分析功能引入 到.NET 生态系统中可用的静态分析器选项。

2015 年,Facebook开源了静态分析工具Infer。它支持 Java 和 C/C++/Objective-C 代码,并能够检测许多潜在问题,包括空指针异常、资源泄漏、注释可访问性、缺少锁保护以及 Android 和 Java 代码中的并发竞争条件;和空指针取消引用、内存泄漏、编码约定和属于 C 系列的语言不可用 API。

微软高级软件工程师辛石说,Infer#并不是唯一可用于.NET的静态分析器。但是,Infer# 为 .NET平台带来了独特的功能。Infer# 与众不同的是它专注于跨函数分析,这在其他分析器中找不到,而增量分析则找不到。

PreFast 会检测某些无效异常和内存泄漏的实例,但其分析纯粹是过程内分析。同时,JetBrains Resharper 严重依赖开发人员注释进行内存安全验证。

例如,辛石描述了 Infer# 如何检测以下代码段中涉及三个不同函数的空引用:

static void Main(string[]) args) { var returnNull = ReturnNull(); _ = returnNull.Value; } private static NullObj ReturnNull() { return null; } internal class NullObj { internal string Value { get; set; } }

差异工作流是 如何配置Facebook Infer 在项目的两个版本上运行的能力,并比较了引入或修复了哪些问题。这使得在 CI 工作流中集成"Infer"并使其在主分支被接受之前自动处理 PR 成为可能。

例如,辛石 解释道,您可以通过执行以下命令来获取 在feature a 和 master分支之间更改的文件列表:

git diff --name-only origin/feature..origin/master > files-to-analyze.txt

然后,对于每个分支,您将检查出来并运行infer:

git checkout <branch> infer capture -- make -j 4 infer analyze --changed-files-index files-to-analyze.txt cp infer-out/report.json <branch>-report.json

最后,您将使用 Infer 的命令来reportdiff 比较结果:

代码语言:javascript
复制
infer reportdiff --report-current feature-report.json --report-previous master-report.json
代码语言:javascript
复制
这将输出三个文件,其中添加在feature分支中的问题,在feature中修复的问题和保持不变的问题。

分析增量更改的能力使 Infer 能够在大型代码库上有效运行。 .NET团队已经在在其产品(包括 Roslyn、.NET SDK 和核心软件)上一直在使用ASP.NET。

为了支持过程间和差分分析,Infer使用分离逻辑,这使得对计算机内存的操作进行推理并证明某些内存安全条件成为可能。为此,Infer 将所有代码转换为称为 SIL 的中间表示形式。SIL 利用小脚谓词框架。

使 Infer 能够分析 .NET 源代码的核心问题是将其转换为 IN(推断分析的语言)。为此,源语言构造需要在 OCaml 中表示。

为了简化此过程,并简化将 Infer# 扩展到 C# 以外的其他 .NET 语言,.NET团队引入了 中间语言SIL无关的 JSON 序列化

从源代码的低级表示中工作的好处是双重的:首先,CIL 是所有 .NET 语言的基础(例如,除了最常见的 C#),因此 InferSharp 支持所有 .NET 语言,第二,CIL 不分任何句法糖,从而减少翻译所需的语言内容,从而简化翻译。

Microsoft SIL 序列化器与一个去序列化包相结合,该包提取 OCaml 中的 SIL 数据结构,并使其可用于 Infer 的后端分析。

目前,Infer# 支持空取消引用和内存泄漏检测,但 Microsoft 已经宣布将继续扩展其功能,增加对冲突条件和线程安全违规检测的支持。

本文参与 腾讯云自媒体同步曝光计划,分享自作者个人站点/博客。
原始发表:2020-12-26 ,如有侵权请联系 cloudcommunity@tencent.com 删除

本文分享自 作者个人站点/博客 前往查看

如有侵权,请联系 cloudcommunity@tencent.com 删除。

本文参与 腾讯云自媒体同步曝光计划  ,欢迎热爱写作的你一起参与!

评论
登录后参与评论
0 条评论
热度
最新
推荐阅读
目录
  • NET团队借助Infer#,将Facebook的跨程序静态分析功能引入 到.NET 生态系统中可用的静态分析器选项。
  • 2015 年,Facebook开源了静态分析工具Infer。它支持 Java 和 C/C++/Objective-C 代码,并能够检测许多潜在问题,包括空指针异常、资源泄漏、注释可访问性、缺少锁保护以及 Android 和 Java 代码中的并发竞争条件;和空指针取消引用、内存泄漏、编码约定和属于 C 系列的语言不可用 API。
相关产品与服务
文件存储
文件存储(Cloud File Storage,CFS)为您提供安全可靠、可扩展的共享文件存储服务。文件存储可与腾讯云服务器、容器服务、批量计算等服务搭配使用,为多个计算节点提供容量和性能可弹性扩展的高性能共享存储。腾讯云文件存储的管理界面简单、易使用,可实现对现有应用的无缝集成;按实际用量付费,为您节约成本,简化 IT 运维工作。
领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档