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:
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.
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) | "_" | "\'"
The results are of the form { bools = B; ints = I; closures = C }, where:
global
and global-independent-attribute
refer to
pairs of a program point and an abstract call string.
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.
Author: Benoît
Montagu
Copyright © Inria 2020-2021
Powered by OCaml,
Js_of_ocaml
and the ACE code editor.