Infer#:將 Facebook 的靜態分析器帶工具帶到 C# 和 .NET


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 比較結果:

infer reportdiff --report-current feature-report.json --report-previous master-report.json
這將輸出三個文件,其中添加在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 已經宣布將繼續擴展其功能,增加對沖突條件和線程安全違規檢測的支持。



免責聲明!

本站轉載的文章為個人學習借鑒使用,本站對版權不負任何法律責任。如果侵犯了您的隱私權益,請聯系本站郵箱yoyou2525@163.com刪除。



 
粵ICP備18138465號   © 2018-2025 CODEPRJ.COM