1. 程式人生 > 實用技巧 >Infer#:將 Facebook 的靜態分析器帶工具帶到 C# 和 .NET

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 已經宣佈將繼續擴充套件其功能,增加對衝突條件和執行緒安全違規檢測的支援。