選自TowardsDataScience
作者： Jesus Rodriguez
機器之心編譯
參與：Geek AI、路
Facebook 的 Project Infer 是如何在部署手機 App 前識別出其中的 Bug 的呢？
Infer 官網地址：https://fbinfer.com/
GitHub 地址：https://github.com/facebook/infer
不久前，一支來自 Facebook 的工程團隊斬獲了 ACM SIGPLAN POPL 最具影響力論文獎，這是機器學習研究社區最受關注的獎項之一。該團隊獲獎論文為「Compositional Shape Analysis by Means of Bi-abduction」，介紹了近年來我最喜歡的機器學習應用之一「Project Infer」背後的科學原理。Project Infer 的目標是：在移動應用程序發佈之前檢測其代碼中的 bug，這樣的技術似乎是科幻電影中的橋段。
移動應用程序中出現 bug 的代價往往很大。在移動應用程序被分發到數千臺移動設備後再發現錯誤，對於任何開發者來說都是一場噩夢。傳統的移動應用程序測試重點關注重建已知的場景，但是實際上還存在許多可能觸發錯誤條件的代碼組合，而它們是傳統的測試方法無法檢測到的。Project Infer 則會掃描移動應用程序的代碼，並檢測出可能的錯誤條件，最後由開發者複核。自從三年前該軟件開源以來，Project Infer 就已經被 AWS、Spotify 及 Uber 等世界頂級公司所採用。
Project Infer 是如何工作的？
Project Infer 使用邏輯推理對軟件程序可能出現的執行結果進行推理。任何大型的移動應用程序都可能包含數億個可能觸發錯誤條件的代碼組合，這使得傳統的代碼分析例程無法擴展到所有可能的情況。Facebook 的 Infer 構建了關於應用程序的增量式知識，提高應用程序整個開發生命週期中的開發效率。
從頂層看，Facebook Infer 的工作流可以分成兩個主要階段：捕獲和分析。而其生命週期也可被分成兩個主要的部分：全局部分和差分部分。
在「捕獲」階段，Infer 使用編譯命令將待分析的文件轉換成其內部的中間語言。而「分析」階段則會探索每個函數可能會觸發哪些錯誤條件。如果 Infer 在分析某個方法或函數時遇到了某些錯誤，它將停止運行有錯誤的方法或函數，但將繼續分析其它方法和函數。下面的動畫演示了 Facebook Infer 在捕獲和分析階段的運行情況。
從程序執行的角度來看，Facebook 的 Infer 可以在兩種模式下使用：全局模式和差分模式。當 Infer 分析給定項目中的所有文件時，Infer 將在全局工作流下運行。對於使用 Gradle 編譯的項目，可使用下面的語法運行 Infer 的全局工作流：
<code>infer run -- gradle build/<code>
在增量式構建的系統（在移動應用程序中很常見）中應用 Infer 時往往會使用差分工作流。在該場景下，我們首先需要運行 Infer 的「捕獲」階段，獲得所有的編譯命令，然後使用 –-reactive 參數來分析代碼的變化。
<code>gradle clean
infer capture -- gradle build
edit some/File.java
# make some changes to some/File.java
infer run --reactive -- gradle build/<code>
可以使用 InferTraceBugs 命令來研究 Infer 生成的報告。
<code>infer run -- gradle build
inferTraceBugs/<code>
Project Infer 背後的科學原理
Facebook Infer 基於兩種新穎的數學技術：分離邏輯（separation logic）和雙向假說推理（bi-abduction）。
分離邏輯使 Infer 能夠對應用程序存儲小的、獨立部分的推理進行分析，而不必在每一步都考慮整個內存。從數學上講，分離邏輯對計算機內存的突變進行推理。分離邏輯的核心元素就是 * 操作，我們稱其為分離合取（separating conjunction），讀作「... 與... 分別成立」。例如，公式「x↦y∗y↦x」可以讀作「x 指向 y 與 y 指向 x 分別成立」（「如果 x，那麼 y」與「如果 y，那麼 x」分別成立），這類似於內存指針的工作原理。大多數對於計算機函數的邏輯推理往往是通過適當地更新「* 合取」，從而模仿 RAM 中的就地操作更新來運行的，而分離邏輯為對計算機程序的推理提供了基礎。
雙向假說推理是分離邏輯的一種邏輯推理形式，它將局部推理的關鍵思想自動化。對於 Infer 來說，雙向假說推理可以被視為一種邏輯推理技術，它使該框架能夠發現應用程序代碼中獨立部分的行為特性。雙向假說推理將假說推理作為「frame 問題」的一種反演：它同時對 anti-frame（缺失部分狀態）和 frame（沒有被某個操作觸及的部分狀態）進行推斷，它是一種新的過程間分析算法的基礎。
從數學上來說，雙向假說推理問題是用下面的語法表述的：A∗?antiframe⊢B∗?frame。其目的是找到一對使得蘊含語句成立的 frame 和 anti-frame。在 Facebook Infer 環境下，雙向假說推理為從原始代碼中推斷出「前綴/後綴」規範提供了一種方法（只要我們知道底層代碼的原語規範）。
Facebook Infer 是不同機器學習領域多年研究成果的集大成者。這些工作產出了一系列重要的研究論文，它們為推理邏輯和機器學習的其它領域做出了突破性貢獻。下面，本文將回顧其中的一些重要論文：
Compositional Shape Analysis by means of Bi-Abduction：這篇論文獲得了著名的 ACM SIGPLAN POPL 最具影響力論文獎，介紹了組合形態分析的原則。基於雙向假說推理的組合形態分析是一種獨立於程序調用者進行過程分析的分析方式。組合形態分析將傳統的形態分析擴展到了計算機程序分析任務中。其思路是通過有效地分析各個獨立的部分並對缺失部分進行推斷來分析程序。
A Local Shape Analysis Based on Separation Logic：該論文介紹了分離邏輯這一描述程序分析的機制。該論文闡述的主要觀點是，我們能夠在並不理解整個內存堆（heap）、只掌握其中一些獨立單元的情況下，對內存堆中的數據結構進行分析。例如，我們在不分析整個堆的情況下推斷出某些特定的單元生成了一個鏈表。
Smallfoot: Modular Automatic Assertion Checking with Separation Logic：該論文提出了 Smallfoot 技術，它是 Facebook Infer 的前身，將分離邏輯用於對軟件程序中輕量級數據結構進行推斷。
AL: A new declarative language for detecting bugs with Infer：AL 為 Facebook Infer 提供了重要的可擴展性模型。從概念上講，AL 使任何工程師可在不瞭解 Infer 內部工作原理的情況下設計出新的檢查程序。AL 是一種聲明式語言，它支持以簡單的交互方式對語法樹進行推理。
Moving Fast with Software Verification：最後這篇論文介紹了 Facebook 如何在內部使用 Project Infer。該論文介紹了 Facebook 工程師如何將 Infer 集成到他們的開發流程中，從而為 Instagram、Facebook Messenger 以及 Facebook 在 Android 和 iOS 平臺上的移動應用程序提供靜態分析支持。
Facebook Infer 是最早發佈、最實用的將機器學習用於軟件編程的應用之一。儘管到目前為止，Infer 的使用對象還侷限於移動應用程序，但是它的許多設計原則適用於通用應用程序。說不定，未來會出現一版用於機器學習程序的 Infer 呢！
原文鏈接：https://towardsdatascience.com/machine-learning-for-detecting-code-bugs-a79f37f144b7
✄------------------------------------------------
加入機器之心（全職記者 / 實習生）：[email protected]
投稿或尋求報道：content@jiqizhixin.com
廣告 & 商務合作：[email protected]
閱讀更多 坤艮機器之心 的文章
