Flix is a declarative language for specifying and solving fixed-point computations on lattices, such as static program analyses [3]. The syntax and semantics of Flix are inspired by Datalog, but extended to support user-defined lattices and monotone functions. Flix is open-source and available on GitHub [4].
Static analyzers implemented in general-purpose languages, such as C++ or Java, can be difficult to understand and maintain. A more elegant approach is to express the mutual dependencies of a fixed-point computation in a declarative manner. Thus, there is interest in using a declarative language such as Datalog to implement pointer analyses [1].
However, Datalog does not support lattices or functions, which limits its expressivity. While it is sometimes possible to work around these limitations, it can be slow and cumbersome. Furthermore, most Datalog implementations have poor integration with existing tools.
Flix allows users to define their own lattices and functions. Rules over relations and lattices are expressed in a logic language with Datalog-like syntax, while functions are written in a pure functional language with Scala-like syntax. The functional language, while small, supports algebraic data types, sets, and pattern matching. Flix also supports interop with JVM languages.
Flix is implemented in Scala, with a standard front-end for parsing, weeding, resolving, and typechecking. The back-end has two components, a solver for the logic language and an interpreter for the functional language. As an initial step to improve performance, we have implemented a bytecode generator to replace the interpreter.
In order to generate JVM bytecode for the functional language, the abstract syntax tree requires a number of transformations. For example, pattern matching must be desugared into lower-level primitives, such as if-then-else expressions and nested lambda functions. Lambdas need to be converted to closures and then lifted. Finally, there are interesting design decisions about how to compile closures to bytecode, and how to implement interop to allow Flix code to call functions written in Scala, or any other JVM language.
On an implementation of the Strong Update analysis [2], running the generated bytecode is 1.7x faster than using the interpreter. On a purely functional benchmark (i.e. one that does not use the solver for evaluating rules) such as an n-body simulation [5], the generated bytecode is 19x faster.
[1] M. Bravenboer and Y. Smaragdakis. Strictly declarative specification of sophisticated points-to analyses. OOPSLA ’09. http://dx.doi.org/10.1145/1640089.1640108
[2] O. Lhoták and K.-C. A. Chung. Points-to analysis with efficient strong updates. POPL ’11. http://dx.doi.org/10.1145/1925844.1926389
[3] M. Madsen, M.-H. Yee, and O. Lhoták. From Datalog to Flix: a declarative language for fixed points on lattices. PLDI ’16. http://dx.doi.org/10.1145/2908080.2908096
[4] https://github.com/flix/flix
[5] http://benchmarksgame.alioth.debian.org/u64q/nbody-description.html
