Better living through incrementality - Immediate static analysis feedback without loss of precision

Sebastian Erdweg

Static analyses are best known for detecting errors at compile time and thus helping developers to write correct code. That’s an honorable quest and not for nothing static analysis is sometimes referred to as lightweight verification. But static analysis has a second quest of equal importance: to aid program understanding. Development tools such as IDEs use information computed by static analyses to explain the program to the developer (variable v has type int, variables v1 and v2 point to the same object), to provide exploration functionality (jump to declaration, find call sites), to guide developers (uninitialized read, dead code), and to provide sophisticated edit actions (refactorings). IDEs must provide all these features without interrupting the workflow of the developer. In particular, IDEs must react quickly to code changes. That is, the underlying static analyses need to be incremental.

We present IncA, a language-independent framework for incremental static analysis that does not compromise on precision. IncA provides a DSL for the definition of static analyses and incrementalizes them automatically. We explain how the IncA compiler translates analysis specifications into Datalog-style rules and how the IncA runtime solves these rules incrementally. We particularly discuss how IncA incrementalizes fixpoint computations, which are ubiquitous in data-flow analysis.

---

Previous: Dan Frumin | ReLoC - A Mechanised Relational Logic for Fine-Grained Concurrency
Next: | Towards Language Parametric Web-Based Development Environments