This web-page embeds a prototype relational, modular static analyser for the typed λ-calculus as described in the paper Stable Relations and Abstract Interpretation of Higher-Order Programs. We extended the analyser to support pairs, records, sums, and recursive functions. Recursive datatypes are not supported at the moment. We also implemented Hindley-Milner type inference thanks to the excellent Inferno library.
The analyser infers relations between the inputs and the outputs of programs. Programs are analysed in a compositional manner. In particular, functions are analysed only once, at their definition site. As we note in the paper, the abstract domain we currently use loses a lot of information when an unknown function (i.e., a parameter of a function) is applied. Precision is satisfying in the other cases.
Warning: the analyser 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.
You can also download the associated Coq development, or browse the associated documentation directly.
The following options are available:
Learn from patterns: refine the knowledge in the branches of a pattern matching construct.
Fail when a type mismatch is found: when a type mismatch is found while performing operations on the abstract domain, fail immediatly. This should not happen.
Fixpoint unrolling: tells how many iterations must be unfolded before a standard fixpoint computation is started (only useful for recursive functions).
Delay widening: tells how many iterations must be performed during fixpoint computation before widening must be employed (only useful for recursive functions).
Copyright © Inria 2020-2021
Powered by OCaml, Js_of_ocaml and the ACE code editor.