非死book開源靜態代碼分析工具Infer

為了減少測試與人工代碼檢查的工作量，軟件供應商一般利用靜態代碼分析工具來進行程序正確性和穩定性的檢查。Monoidics就是在2009年成立、專門設計代碼分析工具的公司。該公司所開發的Infer靜態代碼分析工具提供了大規模代碼檢查的高效解決方案。2013年7月，社交網站巨頭 非死book收購了Monoidics公司，用來提升其大規模代碼檢查的效率。近日， 非死book公開宣布開源Infer工具 ，為廣大用戶提供代碼檢查方面的便利。

靜態代碼分析是利用詞法分析、語法分析、抽象語法樹分析以及語義分析等手段，檢查代碼中潛在錯誤的過程。該過程與動態分析相對應，不需要執行應用程序，直接通過對代碼掃描發現隱含的程序問題，并給出一定的修改建議。傳統的靜態代碼分析是通過人工途徑進行的。該方法既需要耗費大量的時間和人力，又很難保證檢查結果的可信性。但是，軟件的正確性和穩定性又十分重要。一旦發布后才發現bug，應用程序就需要用戶進行主動更新，會嚴重損害用戶的使用體驗。因此，自動化的代碼檢查工具就成為軟件開發商所迫切需要的解決方案。

然而，自動化的靜態代碼分析并不容易。針對多達數百萬行的代碼進行語法、語義等分析，需要考慮到可能多達上千萬種的可能性。而且，代碼可能被多個開發人員進行高頻率修改。以非死book為例，在一天內，一個移動平臺的程序代碼可能會有超過一千處的修改。為了能夠很好的與開發人員進行交互，分析工具就需要在若干分鐘內完成大規模代碼的分析工作，才能夠不影響開發人員下一天的修改工作。

為此，Infer采用了 Separation邏輯 和 bi-abduction 兩種數學手段來提高代碼分析的效率。Separation邏輯是 Hoare 邏輯 的擴展，主要用來程序中單獨小段的分析。在每一步，Separation邏輯保證了對每一個小段的分析有合理的，而且能夠迅速完成。Bi- abduction則是用來發現每個小段程序的行為屬性。通過利用這兩個技術，Infer實現了增量分析，有效減少大規模代碼修改過程中的分析時間。而且，Infer會針對可疑的代碼給出高質量的報告，幫助開發人員盡快確定bug是否存在或如何進行修改。

目前，非死book已經利用Infer來分析Android和iOS上的移動應用程序、非死book Messenger以及Instagram等。每個月，Infer都會在開發人員正式提交代碼之前發現數百個可能的bug，有效減少了發現并解決bug的時間，提高了非死book的產品開發效率。而且，Infer所匯報的問題中80%都被開發人員所接受并進行解決，表現出很好的可信性。當前，非死book主要利用Infer進行Android平臺和iOS平臺Objective-C代碼的分析。 據透露 ，Infer能夠處理的語言還包括非Android平臺的C語言和Java語言。未來，非死book表示會計劃擴展Infer的能力，使其能夠對更多語言進行分析。