Control-Flow Analysers for the λ-calculus

This web-page embeds prototypes of static analysers for the untyped λ-calculus, extended with booleans and arithmetic operations, as described in the paper Trace-Based Control-Flow Analysis.

Warning: the analysers can take a very long time to run in your browser! Do not be surprised if your browser warns you that some script is taking a lot of time.

The output text only displays the analysis result for the last declaration of the program.

Documentation

Options

The available analyses are:

nabla: ∇-CFA, a control-flow analysis based on widening
global: a classic CFA based on a global environment (as used in constraint-based CFA)
global-independent-attribute: a variation of the global analysis, where each function is accompanied with only one environment of abstract values. This is in contrast with the global analysis, that associates each function to a set of possible environments. Not described in the paper.

The primitive operations ?int and ?bool produce an unknown integer or boolean, respectively, in a non-deterministic manner. The following integer operations are +, -, *, <=, <, >=, > and =. The semantics of arithmetic operations is that of unbounded integers. The analysers perform approximations when the capacity of an integer might exceed the precision provided by your machine or your browser.

You are free to choose the abstract domain to represent sets of integers:

two-points: ⊥ and ⊤.
flat: the flat domain of integers, with ⊥ and ⊤.
signs: the domain of signs. It has the abstract elements: ⊥, ⊤, ]-∞,0], ]-∞,-1], {0}, ]-∞,-1]∪[1,+∞[, [0,+∞[, and [1,+∞[.
intervals: the domain of intervals.

You are free to choose the following approximations for call sites:

last 0 call sites: no distinction of call sites, as in 0-CFA.
last 1 call sites: only the most recent call site is distinguished, as in 1-CFA.
last 2 call sites: only the two most recent call sites are distinguished, as in 2-CFA.
max 0 cyclic call sites: occurrences of call sites are limited to 0. This is the same as 0-CFA.
max 1 cyclic call sites: occurrences of call sites are limited to at most 1.
max 2 cyclic call sites: occurrences of call sites are limited to at most 2.

The following options are available:

Refine branches: refine the knowledge in the branches of a test.
Branch is context: consider branches (if ... then ... else ...) as a call site for the two branches.
Let binding is context: consider let-binding (let ... in ...) as a call site for the body of the let.
No environment restriction: do not restrict the environment to the free variables of the program that is being analysed.
Kill unreachable parts: do not analyse parts of the code that are not reachable.
Debug: print some statistics about the analyses.
Share program points for identical integers: helps reduce the number of states to explore.
Share program points for identical variables of the same scope: helps reduce the number of states to explore.

Syntax of programs

Functions are the only supported recursive values in programs. Mutually recursive definitions are currently not supported.

The syntax of programs is defined by the following EBNF grammar:

program ::=                                    (Program)
          | decl+

decl ::=                                       (Declaration)
       | "val" "rec"? x x* "=" expr            (Value declaration)

expr ::=                                       (Expressions)
       | x                                     (Variable)
       | i                                     (Integer)
       | "?int"                                (Unknown integer)
       | expr binop expr                       (Binary operation)
       | unop expr                             (Unary operation)
       | "true"                                (True boolean)
       | "false"                               (False boolean)
       | "?bool"                               (Unknown integer)
       | "fun" x+ "->" expr                    (Anonymous function)
       | expr expr                             (Application)
       | "if" expr "then" expr "else" expr     (Branching)
       | "let" "rec"? x x* "=" expr "in" expr  (Let definition)
       | "(" expr ")"                          (Parenthesized expression)
       | "begin" expr "end"                    (Parenthesized expression)

binop ::=                                      (Binary operators)
        | "+"                                  (Addition)
        | "-"                                  (Subtraction)
        | "*"                                  (Multiplication)
        | "&&"                                 (Boolean conjunction)
        | "||"                                 (Boolean disjunction)
        | "<"                                  (Lesser than integer test)
        | "<="                                 (Lesser than or equal integer test)
        | ">"                                  (Greater than integer test)
        | ">="                                 (Greater than or equal integer test)
        | "="                                  (Equality integer test)
        | "<>"                                 (Inequality integer test)

unop ::=                                       (Unary operators)
       | "-"                                   (Negation)

x ::=                                          (Variables)
    | alpha (alpha | Alpha | digit | symb)*

i ::=                                          (Integers)
    | '0'
    | ['1'-'9'] digit*

alpha ::=                                      (Alphabetic symbols, lower case)
        | ['a'-'z']

Alpha ::=                                      (Alphabetic symbols, upper case)
        | ['A'-'Z']

digit ::=                                      (Digit)
        | ['0'-'9']

symb ::=                                       (Symbol)
       | "_"
       | "\'"

Syntax of outputs

The results are of the form { bools = B; ints = I; closures = C }, where:

B is the set of possible booleans.
I is the set of possible integers.
C is the set of possible closures, that are composed of the piece of code of the closure and an abstract environment.
- For the λ-abstractions in closures, we display their code, and the location at which they occur in the program text.
  For example, λ[42:3] x -> x is the identify function that occurs at line 42, column 3 of the program text.
- The environments in closures differ, depending on the analysis and on the context sensitivity. The global and global-independent-attribute refer to pairs of a program point and an abstract call string.
  For example, the global analysis may return the abstract closure (λ[42:3] x -> y) {[y -> 6:8 @ 23:9], [y -> 6:8 @ 23:9 @ 10:4 # *]}. It is a closure with two possible environments, that give an abstract value to the local variable y. The first possible value is the instance of the binding variable at line 6 colomn 8 in the calling context composed of the single application site located at ligne 23 column 9. The second possible abstract value for y is the instance of the same binder for the call sites that is composed of at least two calls, and starting with a call at line 23 column 9, then a call at line 10 column 4.

The symbols ⊥ or ∅ always indicates the empty set. The symbol ⊤ indicates the full set.

The output also contains some statistics about this run of the analyser:

Running time: how much time it took for the analyser to complete.
States: how many states were explored in the abstract call graph.
Edges: how many distinct edges were taken in the exploration of the abstract call graph.
Max fanout: the maximal fanout degree of the abstract call graph. This gives an indication of the size of the disjunctions in the abstract domains.
Iterations: how many iterations were necessary to reach a fixpoint.