News

Facebook Shares Homegrown Mobile Code Testing Tool

• By David Ramel
• June 12, 2015

Adding to the list of internally developed software projects open sourced by Facebook is Infer, a static code analyzer used to spot bugs in mobile programs before they're shipped off to serve a billion users.

Facebook Infer is used internally to find null pointer dereferences and resource and memory leaks on code modified by engineers before it's moved to production.

It's currently used to scan Objective-C code for iOS apps and Java code in Android apps. It's also capable of scanning C code and non-Android Java code. The tool itself is written in OCaml.

Facebook yesterday said it hopes the open source community can help the company extend its capabilities and put it to more uses (currently Facebook is providing binaries only for Mac OS X and 64-bit Linux).

If you want to help out, though, you'd better have your math chops in order -- really high order -- as the engineers who developed it have been involved in groundbreaking highly theoretical computer science and brand-new mathematical logic.

That means you should be conversant in formulas like the frame rule:

That comes from the Wikipedia entry on "separation logic," a new way of reasoning about programs whose invention was attributed to -- among others -- Peter O'Hearn, who was one of three Facebook engineers penning yesterday's blog post that announced the open sourcing of Infer.

O'Hearn and fellow engineers Cristiano Calcagno and Dino Distefano, listed as co-authors on the blog post, came to Facebook when their London-based startup Monoidics -- formed on the basis of their breakthrough academic mathematical research -- was acquired by the social giant in 2013.

They brought separation logic and another breakthrough, bi-abduction, to Facebook's software development methodology, continuous development and deployment, where Infer has been tweaked and improved.

Static code analyzers test program without running the programs, which is the province of dynamic testing. Static code testing tools are numerous, but the unique scale of coding at Facebook required something new. As O'Hearn, Calcagno and Distefano explained:

Facebook Infer uses logic to do reasoning about a program's execution, but reasoning at this scale -- for large applications built from millions of lines of source code -- is hard. Theoretically, the number of possibilities that need to be checked is more than the number of estimated atoms in the observable universe. Furthermore, at Facebook our code is not a fixed artifact but an evolving system, updated frequently and concurrently by many developers. It is not unusual to see more than a thousand modifications to our mobile code submitted for review in a given day. The requirements on the program analyzer then become even more challenging because we expect a tool to report quickly on these code modifications -- in the region of 10 minutes -- to fit in with developers' workflow. Coping with this scale and velocity requires advanced mathematical techniques. Facebook Infer uses two such techniques: separation logic and bi-abduction.

It's been working well, the engineers said, as Infer has led to bug fix rates of about 80 percent, which they said is good for automated testing tools.

The trio said they look forward to further advances in their testing methodology, which they call program verification.

"In program verification, certainly, a tremendous amount remains to be done," they said. "But, with continued progress, we believe there is also much more value that can be unlocked for programmers. We look forward to a future in which, with your help, program verification technology can prove more and more useful in helping programmers develop reliable code, fast."

Binaries for Mac OS X and 64-bit Linux (Python 2.7 is required) can be downloaded here. Infer is also now on GitHub.