FormuLog: Datalog for static analysis involving logical formulae

TL;DR

FormuLog extends Datalog to handle logical formulae, enabling the implementation of complex static analyses like symbolic execution and model checking that were previously infeasible with standard Datalog.

Contribution

It introduces a novel extension of Datalog, called FormuLog, to represent and manipulate logical formulae for advanced static analysis tasks.

Findings

Successfully implemented symbolic execution and model checking analyses.

Identified key performance optimizations for scaling to real-world problems.

Prototype implementation demonstrating the language's capabilities.

Abstract

Datalog has become a popular language for writing static analyses. Because Datalog is very limited, some implementations of Datalog for static analysis have extended it with new language features. However, even with these features it is hard or impossible to express a large class of analyses because they use logical formulae to represent program state. FormuLog fills this gap by extending Datalog to represent, manipulate, and reason about logical formulae. We have used FormuLog to implement declarative versions of symbolic execution and abstract model checking, analyses previously out of the scope of Datalog-based languages. While this paper focuses on the design of FormuLog and one of the analyses we have implemented in it, it also touches on a prototype implementation of the language and identifies performance optimizations that we believe will be necessary to scale FormuLog to real-world static analysis problems.