Facebook開源了適用于分析C、Java和Objective-C代碼的靜態分析工具Infer。
Infer是Facebook的開發團隊在代碼提交內部評審時,用來執行增量分析的一款靜態分析工具,在代碼提交到代碼庫或者部署到用戶的設備之前找出bug。由OCaml語言編寫的Infer目前能檢測出空指針訪問、資源泄露以及內存泄露,可對C、Java或Objective-C代碼進行檢測。Facebook使用Infer自動驗證iOS和安卓上的移動應用的代碼,bug報告的正確率達80%。
Infer通過捕獲編譯命令,把要被編譯的文件轉換為可用于分析潛在錯誤的中間語言格式。整個過程是增量進行的,意味著通常只有那些有修改過并提交編譯的文件才會被Infer分析。Infer還集成了大量的構建或編譯工具,包括Gradle、Maven、Buck、Xcodebuild、clang、make和javac。
有一些類型的錯誤能用Infer檢測出,關于它們的更多細節內容可見此頁。Infer未來有望能加強對數組越界錯誤、轉換異常和污染數據泄露的檢測,Facebook目前已開始著手開發這些功能,但暫不可用。
在被問及能否增強Infer的功能,以使其可找出其他錯誤,并能應用于其他語言編寫的代碼時,Facebook的發言人答復InfoQ:“我們認為,關于Infer,這才只是一個開始,公司未來將持續致力于釋放更多的價值給程序員”,并表示Facebook希望能與社區一起合作,來進一步完善Infer:
Infer做的不錯,不過仍有許多跨工程組織的開放問題有待解決。一旦Facebook開源了Infer,就可以同許多工程組織、研究組織和學術組織進行合作,通過社區的努力,有可能最終Infer會增加一些新特性,能用來發現新類型的bug,甚至可以應用到新的語言上。
據Facebook透露,Infer根植于兩大基本理論之上,其一是霍爾邏輯,一種用于推理計算機程序正確性的形式系統,另一個是抽象解釋,該理論用于測度程序語義的逼近結果,此外還涉及其它一些研究成果,例如Separation Logic和Bi-abduction。
Infer的源代碼可在GitHub上獲取。