Soufflé

Logic-Defined Static Analysis

Soufflé is a variant of Datalog designed for tool builders crafting static analyzers. It synthesizes a parallel C++ program from a declarative Datalog specification, combining the clarity of logic programming with the performance of compiled native code.

The project commenced at Oracle Labs in Brisbane and was open-sourced in March 2016. Today it is supported by The University of Sydney, the University of Innsbruck, University College London, and the University of Athens.

Soufflé's synthesis pipeline uses semi-naïve evaluation as the interpreter, transforms the specification into relational algebra, and then emits templatized C++ — a staged compilation approach that yields highly optimized executables for program analysis workloads.

Soufflé brings a fresh approach to static program analysis by letting developers express complex analyses as declarative Datalog rules instead of hand-written imperative code. The tool synthesizes a parallel C++ program from a high-level logic specification, which means analysis designers can focus on what to compute rather than how to implement it efficiently. This shift from manual coding to logic-based specification dramatically reduces development time and opens the door to rapid prototyping of new analysis techniques.

At the heart of Soufflé lies the idea of applying Futamura projections and partial evaluation to Datalog. By treating the analysis specification as a program and the input data as partially known, the system can specialize and optimize the evaluation strategy ahead of time. The result is a staged compilation pipeline that produces highly optimized, parallel C++ code tailored to the specific relations and rules of a given analysis, delivering native execution speed from a concise logical description.

Soufflé is designed from the ground up for large-scale, real-world static analysis workloads. It handles points-to analysis for Java, taint tracking, and security checks that involve millions of facts and complex recursive rules. The engine processes extensional database relations loaded from external sources and computes intensional database relations through a semi-naïve evaluation strategy, scaling effectively across multiple cores thanks to its synthesized parallel runtime.

The language itself is a carefully crafted variant of Datalog that extends the classic logic-programming paradigm with features needed by analysis engineers. It supports stratified negation, aggregation, functors, and user-defined data types, all while preserving a clean declarative semantics. These extensions make it possible to encode sophisticated static analysis algorithms in a form that remains readable, maintainable, and amenable to automatic optimization by the synthesis engine.

Rapid prototyping is one of Soufflé's standout strengths. Because analyses are expressed as concise sets of logical rules, researchers and tool builders can experiment with different analysis designs, tweak rule orderings, and explore trade-offs without rewriting low-level graph traversal or fixed-point iteration code. This deep design-space exploration capability accelerates the discovery of effective analysis strategies and lowers the barrier to entry for newcomers in the program analysis community.

The synthesis process generates specialized data structures for each logical relation, choosing representations that minimize memory footprint and maximize cache locality for the specific access patterns observed in the rules. This data-structure specialization, combined with parallel execution, means that Soufflé-derived analyzers can rival or surpass the performance of hand-tuned C++ implementations while requiring only a fraction of the development effort.

Soufflé is open source and distributed under the MIT license, with an active community of contributors and users spanning academia and industry. The project provides comprehensive documentation, a growing ecosystem of example analyses, and a welcoming development process. Whether you are building a security scanner, a refactoring tool, or a novel static checker, Soufflé offers a solid foundation for turning logic into high-performance analysis code.