Facebook has open sourced Infer, a static analysis tool for C, Java and Objective-C.
Facebook Infer is a static analyzer that runs incrementally on code submitted internally for review by their teams, finding bugs before the code is committed to the codebase or deployed on people’s devices. Infer currently signals Null pointer accesses, resource and memory leaks, it runs on C, Java and Objective-C code, and has been written in OCaml. Facebook uses Infer to automatically verify the code of their mobile applications for iOS and Android, correctly reporting on bugs in 80% of the cases.
Infer catches compilation commands, and translates files that are to be compiled into an intermediate language that is analyzed for possible errors. The process is incremental, meaning that only files that were modified and submitted to compilation are usually analyzed. Infer is integrated with a number of build or compilation tools: Gradle, Maven, Buck, Xcodebuild, clang, make, javac.
This page contains more details on the type of errors found by Infer. The tool will be probably enhanced to detect array bounds errors , cast exceptions and leaking of tainted data, considering that Facebook has been working on these but the features are not yet ready.
When asked about enhancing the tool to discover other errors and covering other languages, a Facebook spokesperson told InfoQ that “Facebook feels that this journey is only one percent finished and the company is continually working to unlock more value for programmers in the future”, expressing their intent to collaborate with the community to take it further:
Infer does things well, but there are still a number of open problems across engineering organizations to be addressed. There are a lot of engineering organizations, research and academia groups that Facebook can collaborate with once it’s shared openly and from that community Facebook might eventually see new features added, new bugs checked or even new languages.
According to Facebook, Infer is built on two foundational theories, Hoare Logic – a formal system for reasoning about a computer correctness - and Abstract Interpretation - a theory for sound approximation of a program’s semantics-, and other researches such as Separation Logic and Bi-abduction.
The source code of this tool can be found on GitHub.
