Fork me on GitHub
Flix. Functional. Logical.

A logic and functional programming language for the implementation of static analyses.

Get Started with Flix

Requires the Java Runtime Environment 1.8

Download Documentation
Recent News
Short, precise.

Flix embraces the database paradigm:

  • Data is represented as tables.

  • Constraints (queries) express dataflow between tables.

  • Functions enable queries on tables to filter, aggregate and compute new values.

  • The result of a query may be inserted into a table. This process may be repeated until a fixpoint is reached.

  • Lattices allow multiple rows to be combined into one row with the use of a least upper bound operator.

Graph Reachability

Path(x, y) :- Edge(x, y).
Path(x, z) :- Path(x, y), Edge(y, z).

Shortest Paths

Dist(origin, 0).
Dist(y, dx + d) :-
    Edge(x, d, y),
    Dist(x, dx).

Examples of how to compute the transitive closure and shortest paths of graphs.

Fully-featured, batteries included.

Languages Features

  • Declarative and Functional

  • Algebraic Data Types

  • Pattern Matching

  • Namespaces

  • Parallel Rule Evaluation

  • Tail call optimization

Additional Features

  • Datalog Support

  • Static Type System

  • Formal Semantics

  • Scala and Prolog-style Syntax

  • Free & Open Source

Tools & Ecosystem

  • Integrated browser-based Debugger and Profiler

  • Built-in Delta Debugger

  • Built-in QuickChecker

  • Built-in Static Program Verifier

  • Runs on the Java Virtual Machine

  • Tutorials & Documentation

Flix Loves Static Analysis.

Flix is ideal for implementation of static analyses, especially points-to and dataflow analyses, including the IFDS and IDE frameworks.

Points-To Analysis

VarPointsTo(v, o) :- NewObj(v, o).

VarPointsTo(v1, o) :-
    Assign(s, v1, v2),
    VarPointsTo(v2, o).

VarPointsTo(v1, o2) :-
    Load(v1, v2, f),
    VarPointsTo(v2, o1),
    HeapPointsTo(o1, f, o2).

HeapPointsTo(o1, f, o2) :-
    Store(f, v2),
    VarPointsTo(v1, o1),
    VarPointsTo(v2, o2).

A points-to analysis aims to discover to what object(s) every local variable and field of an object can point-to. The mutually recursive dependencies between local variables and the heap is easy to express in Flix.

IFDS

PathEdge(d1,m,d3) :-
    PathEdge(d1,n,d2),
    EshIntra(n,d2,d3),
    CFG(n,m).

PathEdge(d1,m,d3) :-
    PathEdge(d1,n,d2),
    SummaryEdge(n,d2,d3),
    CFG(n,m).

PathEdge(d3,start,d3) :-
    PathEdge(d1,call,d2),
    CallGraph(call,target),
    EshCallStart(call,d2,target,d3),
    StartNode(target,start).

SummaryEdge(call, d4, d5s) :-
    CallGraph(call,target),
    StartNode(target,start),
    EndNode(target,end),
    EshCallStart(call,d4,target,d1),
    PathEdge(d1,end,d2),
    EshEndReturn(target,d2,call,d5s).
                        

The IFDS analysis by Reps et al. is a graph reachability problem that can be used to solve certain static analyses. Both IFDS and its extension IDE can be expressed in Flix. Something which is not possible in pure Datalog.

Parity Analysis

enum Parity {
            case Top,
  case Odd,          case Even,
            case Bot
}

def leq(e1: Parity, e2: Parity): Bool =
  match (e1, e2) with {
    case (Bot, _)       => true
    case (Odd, Odd)     => true
    case (Even, Even)   => true
    case (_, Top)       => true
    case _              => false
}

def lub(e1: Parity, e2: Parity): Parity =
  match (e1, e2) with {
    case (Bot, x)       => x
    case (x, Bot)       => x
    case (Odd, Odd)     => Odd
    case (Even, Even)   => Even
    case _              => Top
}

A parity analysis aims to discover, for every local variable in a program, whether it is odd or even. We can conveniently express such an analysis as several constraints over a lattice (see above for the lattice definition).

Try the Online Editor
def f: Bool = List.exists(x -> x % 42 == 0, List.range(1, 100))

            
def f: Int =
    List.foldLeft((x, y) -> x + y, 0,
        List.map(x -> x + 1,
            List.range(1, 10)))

            
enum Shape {
    case Circle(Int),
    case Square(Int),
    case Rectangle(Int, Int)
}

def area(s: Shape): Int = match s with {
  case Circle(r)       => 3 * r * r
  case Square(l)       => l * l
  case Rectangle(l, w) => l * w
}

def f: Int = area(Rectangle(10, 20))

            
rel Edge(x: Int, y: Int)
rel Path(x: Int, y: Int)
Edge(1, 2).
Edge(2, 3).

Path(x, y) :- Edge(x, y).
Path(x, z) :- Path(x, y), Edge(y, z).

            
Free, Open Source and Ready to Use.

Free and Open Source

Flix is open source and available free of charge. The source code for Flix is hosted on GitHub and all development is public.

Flix is dual-licensed under the Apache 2.0 License and the MIT license allowing unrestricted commercial and personal use.

Integrates with Java and Scala

Flix runs on the Java Virtual Machine and provides APIs for both Java and Scala ensuring that interoperability is easy and convenient.

Easily add facts from your front-end into Flix and explore the solution as Java objects.

Available on Windows, Linux and Mac OS X

Flix comes packaged as a single JAR-file that runs on any operating system where the Java Runtime Environment is available, including Windows, Linux and Mac OS X. Flix requires Java 1.8.

Sponsors
We kindly thank EJ Technologies for providing us with JProfiler and JetBrains for providing us with IntelliJ IDEA.