OCamlFormat open-source released

We are pleased to announce the first public release of OCamlFormat.

OCamlFormat is a tool to automatically format OCaml code. It follows the same basic design as refmt for Reason code, but for OCaml. In particular, it works by parsing source code using the OCaml compiler's standard parser, deciding where to place comments in the parsetree, and printing the parsetree and comments in a uniform style.

At Facebook, we currently use this for the OCaml code of Infer to enable developers to stop thinking about line breaking, indentation, parenthesization, etc., to minimize stylistic nit-picking during code review, and to make it as visually obvious as possible when the parser's interpretation of code does not match the programmer's. We use this both with integration with editors as well as a pre-commit hook.

Development is taking place on github. License is MIT.

See the github page for more info on installation, documentation, contributing, etc.

Open Sourcing Infer, 1 Year On

It's been a little over a year ago since we open-sourced Infer on 9 June 2016!

The Infer GitHub repo has seen a lot of activity since then:

Infer was presented at 13 academic and tech international conferences, and at 8 universities around the world!

Amongst these was Mobile@Scale in March 2016, where we announced our collaboration with Spotify. Around the same time, Uber presented at Droidcon SF their Rave + Infer combo to help their developers move fast, and open-sourced a Gradle plugin for Infer.

Infer has also been used to introduce static analysis to students in university courses, including at UCL, Imperial College, and Queen Mary University.

In May, Reason was released publicly and, simultaneously, Infer became the first ever project to use Reason! Reason is a new syntax for OCaml, the programming language in which Infer is written.

Collaboration with Spotify

Infer/Spotify collaboration

Working on deploying Infer inside Facebook has taught us how important it is to have the analysis tool deeply embedded into the developers' workflow; see our “Moving Fast with Software Verification” paper.

Infer runs as part of our continuous integration (CI) system, where it reports issues on code modifications submitted for review by our engineers. We think it's great when someone can hook up Infer to their workflow, and we're working with several other companies to help integrate Infer into their own CI systems. We've come far enough in a collaboration with Spotify to talk about it now!

Last July, shortly after Infer was open-sourced, we started talking with the Marvin (Android Infrastructure) team at Spotify. They were interested in using Infer on their Android app, but it did not work with their build system. They were using the Gradle build system, but Infer's deployment within Facebook is done using a different build system, Facebook's Buck; we had only an initial, basic integration with Gradle, which did not work with Spotify's app. A Spotify engineer, Deniz Türkoglu, made improvements to our Gradle integration, which he submitted as a pull request to Infer's codebase, which is hosted on GitHub.

Then, in November 2015, two of our engineers, Dulma Churchill and Jules Villard, traveled to the Spotify office in Stockholm to attend a Hack Week there. After running Infer on the Spotify app, we discussed the analyzer reports with Spotify engineers, and we agreed that they identified potential problems in the code. Infer is now running as part of Spotify's CI system, and here is a quote from Deniz on Spotify's perspective on Infer, which we include with his kind permission.

“At Spotify we are continuously working on making our codebase better, and in the Android infrastructure team we use a lot of tools: static analyzers, linters, thread/address sanitizers, etc. In our quest to make our code even better, we started using Infer. Infer found several legitimate issues that other tools had missed. The Infer team was also very helpful in following a few false positives that we encountered, and we now have it running on our build servers.

Infer is a great add-on to a company's toolbox. It's not intrusive — you can simply add it to your flow and it will tell you where you forgot to close that cursor or leaked that context. If you find a false positive, just report it or, even better, make a PR. With more users, it will just keep getting better.”

This collaboration was truly a two-way street: Not only does Infer find issues in Spotify, which helps improve its Android app, but feedback from Spotify led to several improvements in Infer, including resolution of false positives and improvements of Infer's UI and integration with Gradle. The better Gradle integration will make it easier for other people to run Infer on lots of other apps around the world.

We're excited to collaborate with other companies and individuals to help make the world's software better. If you are interested in integrating Infer into CI or otherwise hearing about our experience, drop us a line!

Infer on Open Source Android Apps

We ran Infer on a few open source Android apps with the aim of finding some bugs and getting them fixed. Some of those reports got indeed fixed.

One of the apps analyzed was the search engine DuckDuckGo. We found that many database cursors were not closed. Soon after we reported the issue, a developer fixed it.

We also analyzed the popular email client k-9. We found a file not closed leak and reported it. Interestingly, a developer fixed it by not writing some logging info to the file at all. So Infer helped them to simplify their code.

Conversations is an open source XMPP/Jabber client for Android smart phones. We analyzed it as well and found a file not closed leak, which was also fixed.