Build your Own Scalable Static Analysis with the Infer Platform
Jules Villard, Meta
VeTSS Summer School 2023
INTRODUCTION:
Infer is an open-source static analysis platform that is used to find bugs in code at Meta. Every month, Infer runs on thousands of code changes and detects thousands of bugs that are fixed by developers before they reach production.
Over the years, Infer has evolved from a standalone analyser based on Separation Logic to a powerful platform for quickly implementing cross-language modular interprocedural analyses. Static analysis writers only need to provide an intraprocedural analysis that computes the summary for a single procedure and Infer will transform it into a compositional interprocedural analysis that scales to millions of lines of real code.
The goal of this tutorial is to get hands-on experience with Infer and its capabilities as a static analysis platform.
PREPARATION:
**No preparation needed**, come as you are!
– But if you insist:
– You can follow along the tutorial and hack on the internals of Infer too! To do so it would be most beneficial to install Infer ahead of time *from source* following these instructions since it can take sometimes several hours to complete: https://github.com/facebook/infer/blob/main/INSTALL.md#install-infer-from-source
– The curious reader might enjoy the following (optional) infer-related literature:
– Scaling Static Analyses at Facebook, CACM 2019
– Finding Real Bugs in Big Programs with Incorrectness Logic, OOPSLA 2022
– The lab will be online at https://github.com/facebook/infer/blob/main/infer/src/labs/README.md (there is a lab there already, which will be updated fairly heavily before the school begins)
SPEAKER:
Jules Villard is a Software Engineer in the Static Analysis Tools team at Meta in London. He is currently working on the Infer static analysis platform and its Pulse memory and value analysis.
His research interest is on formal verification techniques and semantics of programming languages, especially if they are compositional.
by