So You Want to Analyze Scheme Programs With Datalog?

TL;DR

This paper implements a control-flow analysis for Scheme using the Souffl'e Datalog engine, demonstrating its scalability and polynomial complexity, bridging theoretical analysis and practical implementation.

Contribution

It introduces a Datalog-based control-flow analysis for Scheme, leveraging Souffl'e to achieve scalable and efficient analysis of complex language features.

Findings

Polynomial complexity of the analysis demonstrated

Scalability results show efficient analysis of large codebases

Implementation supports key Scheme features like call/cc and set!

Abstract

Static analysis approximates the results of a program by examining only its syntax. For example, control-flow analysis (CFA) determines which syntactic lambdas (for functional languages) or (for object-oriented) methods may be invoked at each call site within a program. Rich theoretical results exist studying control flow analysis for Scheme-like languages, but implementations are often complex and specialized. By contrast, object-oriented languages (Java in particular) enjoy high-precision control-flow analyses that scale to thousands (or more) of lines of code. State-of-the-art implementations (such as DOOP on Souffl\'e) structure the analysis using Horn-SAT (Datalog) to enable compilation of the analysis to efficient implementations such as high-performance relational algebra kernels. In this paper, we present an implementation of control-flow analysis for a significant subset of Scheme (including set!, call/cc, and primitive operations) using the Souffl\'e Datalog engine. We present an evaluation on a worst-case term demonstrating the polynomial complexity of our m-CFA and remark upon scalability results using Souffl\'e.