TechPrufer
Get started
Meta
Meta logoMeta · Feature trail

Static Analysis Frameworks

1 post · Feb 2014 – Feb 2019

What this trail covers

Meta's static analysis capabilities continue to evolve with the introduction of Infer, a static program analyzer that identifies bugs before mobile code is shipped. Infer uses mathematical logic for symbolic reasoning, approximating human analysis of program execution. It reports problems caused by null pointer access and resource/memory leaks, which are responsible for a large percentage of app crashes. Infer runs incrementally, analyzing code modifications and automatically writing comments on This post details the development and open-sourcing of flint, a token-oriented C++ linter written in D. Flint was developed to address the performance and C++11 feature support limitations of existing linters. It preserves comment information and allows for custom lint rules. The translation from C++ to D resulted in a smaller, faster, and more maintainable tool. Flint includes checks for blocklisted tokens/identifiers, reserved identifiers, include guards, incorrect memset arguments, questionable includes, specific file inclusion patterns, self-initialization, smart pointer usage, open-source dependencies, namespace-scoped statics in headers, include order, exception handling, constructor patterns, throw specifications, heap exceptions, conflicting using directives, namespace usage in headers, and improper use of library internals.

All Meta trails
  1. Open-sourcing SPARTA to make abstract interpretation easyThis post introduces SPARTA, a new C++ library of software components for building high-performance static analyzers. SPARTA encapsulates complex implementation details of abstract interpretation, providing building blocks for data structures like finite lattices, power set domains, and abstract environments. It enables engineers to focus on program properties, analysis granularity, and property representation. The library's design ensures soundness, efficiency, and scalability, as evidenced by its adoption in ReDex for register allocation and liveness analysis, leading to substantial performance gains and reduced code complexity. SPARTA is language-independent and its algorithms generalize across different static analysis scopes, including intraprocedural and interprocedural analyses.
  2. Team behind Infer wins POPL 2019 Most Influential Paper AwardThis post announces that the team behind Infer has won the POPL 2019 Most Influential Paper Award for their work on 'Compositional Shape Analysis by Means of Bi-abduction.' It details how this research led to the development of Infer, Facebook's static program analyzer, which is used to scan source code for bugs before shipping. The post highlights Infer's sophisticated interprocedural and interfile analysis capabilities, its scalability to large codebases, and its impact in fixing thousands of potential bugs monthly. It also mentions the development of AL, a declarative language for creating new checkers, and Infer's application to concurrency bugs and multithreaded rendering. Both Infer and AL have been open-sourced.
  3. Finding inter-procedural bugs at scale with Infer static analyzerThis post details the capabilities of the Infer static analyzer, highlighting its ability to find inter-procedural bugs at scale. It explains the concept of compositional, summary-based analysis using pre/post specifications and provides examples of Infer finding null dereference bugs in DuckDuckGo's Android app and OpenSSL. The post contrasts Infer's inter-procedural and inter-file analysis with intra-procedural tools like Findbugs, Error-prone, and Clang Static Analyzer, emphasizing Infer's effectiveness in large, rapidly changing codebases. It also touches upon the challenges of false positives in static analysis at scale.
  4. AL: A new declarative language for detecting bugs with InferIntroduced AL, a new declarative language for writing intraprocedural static analysis checkers for Infer. AL allows engineers to express bug detection rules using simple formulas based on abstract syntax trees, significantly reducing the expertise and effort required to extend Infer's capabilities. This enables faster iteration and the detection of a wider range of bugs.
  5. Peter O’Hearn elected Fellow of the Royal Academy of EngineeringThis post announces Peter O'Hearn's election as a Fellow of the Royal Academy of Engineering for his pioneering work on separation logic, which underpins Facebook's open-source static analysis tool, Infer. It highlights Infer's impact in catching over 1,000 bugs per month and its scalability to large codebases.
  7. Open-sourcing Facebook Infer: Identify bugs before you shipThis post announces the open-sourcing of Facebook Infer, a static program analyzer. It details Infer's motivation for catching bugs early in the mobile development lifecycle, its incremental analysis approach, and its high fix rate. The post highlights the novel techniques of separation logic and bi-abduction used for symbolic reasoning at scale and velocity. It also traces the history of Infer from theoretical computer science research to its application at Facebook and expresses a vision for the future of program verification.
  8. Under the Hood: Building and open-sourcing flintThis post introduces flint, a new token-oriented C++ linter developed in D. It details the motivation for building a custom linter due to limitations in existing tools (speed, C++11 support). The post explains flint's token-based design, its implementation in D (highlighting benefits over C++), and a detailed list of 19 specific lint checks it performs, covering various aspects of C++ code quality and best practices.