Formulog extends Datalog with mechanisms for constructing logical terms and reasoning about them with satisfiability modulo theories (SMT) solving; a first-order functional language aids inspecting and manipulating complex terms. This combination of features makes it possible to write complex SMT-based program analyses in a way close to their formal specification, while being satisfactorily performant thanks to powerful Datalog optimizations and eficient evaluation techniques.
satisfiability of a term that is not well sorted under SMT, or passing a bit-vector-valued SMT term to a function expecting a concrete bit vector. At the same time, it needs to be possible to construct expressive SMT formulas. We strike this balance through a bimodal type system that treats terms occurring in SMT formulas more liberally than terms outside of formulas.
We first present Formulog by example (Section 2); we then discuss our prototype and several case studies (Section 3).
We present Formulog by example. The canonical “hello world” program for Datalog computes graph transitive closure. An analogous problem for Formulog is computing non-empty paths in a proposition graph, i.e., a directed graph where edges are labeled with SMT propositions, where we consider a path to exist only if the conjunction of the propositions along it (the path condition) is satisfiable. Consider the example graph in Figure 1, which has edges labeled with signed comparisons between symbolic 32-bit vectors (like the proposition < , where and are SMT variables of the 32-bit vector sort). There is no path from node 2 to node 1, as no sequence of edges leads from node 2 to node 1. There is also no satisfiable path from node 1 to node 4. While a path exists structurally, the conjunction of the edge conditions—the path condition < ∧ < ∧ < —is not satisafible. However, there is a (non-empty) path from node 2 to itself, since the path condition < ∧ < ∧ > + is satisfiable under the theory of bit vectors (the addition of and can wrap, unlike the theory of mathematical integers). We break down the Formulog program computing non-empty paths on the example proposition graph piece-by-piece (Figure 2):
Lines 1-2. We declare edge as a ternary input (EDB) relation. Formulog is strongly typed: edge relates two terms of type node (an alias for i32, a 32-bit vector) and a term of type bool smt, i.e., an SMT proposition.
Lines 4-7. We enumerate the edge relation for our example graph. The third attribute is the SMT proposition. SMT terms are complex terms. To build such a term, users can take advantage of a library of constructors like bv_slt, which represents signed bit vector less-than; 1 type node = i32 2 input edge(node, node, bool smt) 3 4 edge(1, 2, `bv_slt(#x[i32], #y[i32])`). 5 edge(2, 3, `bv_slt(#y[i32], #z[i32])`). 6 edge(3, 4, `bv_slt(#z[i32], #x[i32])`). 7 edge(4, 2, `bv_sgt(#y[i32], bv_add(#z[i32], #x[i32]))`). 8 9 fun mem(x: ’a, xs: ’a list) : bool = 10 match xs with [] => false | h :: t => x = h || mem(x, t) end 11 12 output path(node, node, node list, bool smt) 13 path(X, Y, [Y], Phi) :14 edge(X, Y, Phi), 15 is_sat(Phi) = true. 16 path(X, Z, Y :: Path, `Phi /\ Constraint`) :17 edge(X, Y, Phi), 18 path(Y, Z, Path, Constraint), 19 mem(Y, Path) = false, 20 is_sat(`Phi /\ Constraint`) = true. 21 22 output path_conditions(node, node, bool smt list) 23 path_conditions(X, Y, Conditions) :24 path(X, Y, _, _), 25 Conditions = path(X, Y, _, ??). it constructs a term of type bool smt out of two terms of type bv[] smt (where is a positive integer; i32 is shorthand for bv[32]). Quasiquoting (with backticks) enables a type checking mode that flexibly mixes concrete and SMT terms. Additionally, thanks to the SMT theory of algebraic data types, arbitrary user-defined data types can be used within formulas. The notation #[ ] denotes an SMT variable of sort named .
Lines 9-10. Formulog supports first-order, polymorphic, recursive ML-style functions. Here
the mem function checks list membership. Such functions are syntactic sugar, and could be
translated into (likely less eficient) Datalog, following a translation similar in spirit to that
of Pacak and Erdweg [
Line 12. We declare the path output (IDB) relation, relating two nodes, a path (a list of nodes), and a path condition (an SMT proposition).
path is the non-recursive case: there is a path between two nodes if there is an edge between them labeled with a satisfiable formula. Datalog variables have initial capitals. The function is_sat takes a term of type bool smt and returns a bool indicating the satisfiability of its argument.
Lines 16-21. The second rule defining path is the recursive case; it makes use of both the user-defined function mem and the built-in function is_sat.
Lines 22-26. We declare a relation path_conditions relating two nodes and a list of
the path conditions for paths between them. This relation’s sole rule takes advantage of
Formulog’s flexible approach to stratified aggregation: the notation path(X, Y, _, ??)
treats the relation path as a function that takes two arguments (grouping variables X and Y)
and returns a list of all the elements in the fourth column—i.e., the path conditions (the term ??
is a wildcard). In addition to stratified aggregation, Formulog supports stratified negation.
This combination of features—and Formulog’s take on them—distinguishes Formulog from other
systems combining logic programming and constraint solving, like Calypso [
We implemented a prototype of Formulog in ∼ 24K lines of Java.1 The prototype is designed as
a relatively standard Datalog engine augmented with an ML-style interpreter that evaluates the
functional code and discharges SMT queries to external SMT solvers; it uses caching to take
advantage of incremental SMT solving [
Refinement Type Checker (1.2K LOC). This type checker uses SMT solving to prove
subtyping between refinement types, which requires checking logical validity. Our implementation
translates the original formalism [
Java Pointer Analysis (1.5K LOC). SMT solving helps statically resolve the memory
locations Java variables might point to; this is a direct translation of the formal specification of Feng
et al. [
LLVM Symbolic Evaluator (1K LOC). This tool evaluates a fragment of LLVM bitcode
on symbolic inputs, up to a bounded depth. When it reaches a branch conditioned on a symbolic
value, it explores each branch (assuming both are possible given the path so far). By writing
the symbolic executor in Formulog, we can automatically parallelize exploration; by using the
magic set transformation, we can guide the symbolic executor to avoid uninteresting paths.
These optimizations help it compete with industrial-strength CBMC [
The case studies make heavy use of the ML fragment of Formulog: the ratio of the number of
functions to the number of Horn clauses is 1:4 for the points-to analysis and 3:4 for the other
case studies. The ability to easily integrate functional code with Horn clauses is a key feature
of the Formulog programming experience, and the presence of large amounts of functional
code diferentiates Formulog-based analyses from analyses written in a more standard dialect
of Datalog, like Souflé [
We have shown that Formulog’s combination of Datalog, SMT solving, and first-order functional
programming makes it an appropriate language for coding up complex SMT-based program
analyses. Even though our prototype Formulog runtime is not heavily optimized, it achieves
satisfactory performance on our case studies, even in comparison to heavily optimized systems.
In the future, we hope to improve its performance via compilation, à la Souflé [
We also intend to expand Formulog’s applications beyond being a language for writing program analyses. One direction is to use Formulog as an intermediate verification language (i.e., an analysis produces Formulog code, instead of being written in Formulog). In particular, we are currently exploring the possibility of symbolically executing Datalog programs by translating them to Formulog programs. Furthermore, while we have focused on program analysis applications because we are most familiar with them, we are hopeful that Formulog will prove useful in other domains, such as knowledge representation and reasoning.
This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Contract No. FA8750-19-C-0004. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Defense Advanced Research Projects Agency (DARPA).