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.



The available analyses are:

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:

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

The following options are available:

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:

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:

Author: Benoît Montagu
Copyright © Inria 2020-2021
Powered by OCaml, Js_of_ocaml and the ACE code editor.