非死book開源項目非死book Infer: 靜態代碼檢查工具

• 原文鏈接 : Open-sourcing 非死book Infer: Identify bugs before you ship
• 譯文出自 : 開發技術前線 www.devtf.cn
• 譯者 : Mr.Simple
</ul> </blockquote>

今天，我們開源了一個名叫非死book Infer的 靜態程序分析庫，該庫用于在程序分發之前定位代碼bug。靜態分析器是一個不需要運行代碼就可以準確地找出代碼bug的自動化工具。它是傳統的動態測試的 補充，傳統的動態測試允許每次只運行一個獨立的代碼單元來檢測程序的正確性，靜態分析則允許一次性檢測多個、甚至所有代碼。非死book Infer使用數學邏輯來推理程序的運行，當在查找程序時來推測程序員在代碼中所要做的操作。我們內部使用非死book Infer來分析非死book的Android和iOS應用，例如非死book messagers, Instagram等等。現在，這個分析器能夠發現空指針、內存泄漏等能夠使應用奔潰的大量代碼bug.

每個月我們都會修復使用非死book Infer發現的數百個潛在的bug，從而避免這些bug提交到我們的代碼倉庫。這些成果大大減少了我們研發人員查找bug的時間，也使得我們的用戶能夠使用更高質量的應用。



動機

非死book喜歡在產品完成之后盡可能快的分發出去，而不是在一連串冗長的手動測試之后。這種方式在移動應用端的風險比web端更大。當一個 web的bug被發現時，我們可以馬上修復并且提交到服務器上。但是為了修復移動應用的bug,我們需要像應用市場更新應用安裝文件。因此，這也使得在將 應用分發給用戶之前發現bug變得更有價值。結合靜態分析和自動測試能夠幫助非死book在將產品分發出去之前找到crashed和內存泄漏，這使得 我們的應用端應用的研發更為有效、迅速。

為了符合開發者的工作流程，當開發者提交了代碼后非死book Infer增量地執行以分析代碼的修改。當發現潛在bug時分析器會自動地在代碼中添加評論。這些bug報告都是高質量的，因此我們可以幫助開發者快速的 找到問題所在。在最近的幾個月中，bug的修復率已經高達80%,對于一個自動化工具來說那是相當高了。

在現在的開發模式中，我們運行分析器來分析我們的Android和iOS代碼，但是我們還可以做更多的事。非死book Infer還可以分析c語言項目和java代碼，我們計劃在未來擴展它的兼容性。有你的幫助，我們希望非死book Infer 能夠有更廣闊的用途。

核心技術 : 邏輯分離和bi-abduction

非死book infer使用邏輯來推理程序的執行,但是通過這種方式來推理上百萬行代碼量的應用時會變得非常困難。從理論上講，需要檢查的代碼數量會多過預計的數量。 此外，在非死book我們的代碼并不是手工修復代碼，而是一個不斷進化的系統，這個系統被很多開發者頻繁的更新。一天之內大量代碼的修改在我們的移動 開發中并不常見。因此這個代碼分析器的需求變得更有挑戰，因為我們期望一個能夠快速檢查代碼修改的工具，這個時間應該在10分鐘之內。這樣的規模和速度需 要更高級的數學模型，非死book Infer使用了兩種技術: 邏輯分離和bi-abduction。

邏輯分離是使非死book Infer分析能夠推斷出應用存儲的獨立小部分的一種理論，從而不用考慮每一步存儲的完整性。因為考慮每一步的存儲完整性對當今的大型可尋址虛擬內存處理器來說是一個很蛋疼的事。

Bi-abduction是一種邏輯推理技巧，可以使非死book Infer挖掘到應用代碼獨立部分的行為特性。在其運行時把這些特性存儲下來之后，非死book只需要分析軟件中發生改變的部分，其他的部分可以直接套用先前的分析結果。

結合這幾種方法，我們的分析器能夠在數分鐘之內在上百萬行代碼中找到被修改的代碼中存在的復雜問題。

歷史 : 從代碼檢查理論到為十多億人服務的蛻變

軟件的自動檢查在計算機科學社區是一個長期依賴的目標。非死book Infer在這個領域構建了一個基本實現， 包含霍爾邏輯和抽象解釋。在加入非死book之前，我們參與到了其他基礎設施的開發工作，“邏輯分離”作為能夠實現軟件自動檢查的結果出現在人們的視 野中。

邏輯分離是在計算機科學領域的一個重大突破-一種新的數學邏輯被用于描述計算機內存的變化（類似于布爾邏輯用來描述電路）。我們專注于將這個理論運 用和自動化,創建一系列原型工具(例如Smallfoot, Space Invader, Abductor)來支撐這些推理邏輯，最終發現了bi-abduction是模塊化分析程序的一種有效形式。

基于上述研究成果,我們2009年創建了一個名為Monoidics的公司。Monoidics在2013年加入非死book，從那以后我們采 用持續開發和部署的風格來開發我們的產品，在我們的分析器團隊和非死book移動軟件開發工程師的不斷努力的迭代開發下我們的分析器得到了很大的提 升。我們也展示了當運用到非死book代碼庫時代碼檢查技術能夠得到快速的發展。

展望未來

程序檢查是一個有著活躍研究社區和前景光明的領域。在非死book,我們說過這趟旅行我們只完成了1%。在程序檢查領域還有很多的工作需要我們 去完成。但是，隨著我們的不斷努力，我們相信這個領域的成果會讓軟件工程師解放出更多的價值。我們可以展望未來，有你的幫助，程序檢查技術能夠提供更多、 更有用的技術來使得我們的代碼更可靠、更高效。

你可以下載和試用非死book Infer或者移步到fbinfer.com
以了解更多的詳細情況。

致謝： Infer工程@FB團隊包括Sam Blackshear, Jeremy Dubreil, Andrzej Kotulski, Martino Luca, Irene Papakonstantinou, Dulma Rodriguez, and Jules Villard, in addition to Calcagno, Distefano, and O’Hearn. We thank our FB colleagues Mathieu Baudet, Dominik Gabi, and Pieter Hooimeijer for their help, and Bryan O’Sullivan, David Mortenson, and Jim Purbrick for their support. Outside of 非死book, we particularly acknowledge the scientific contributions of David Pym, John Reynolds, Hongseok Yang和Josh Berdine.