nea, neatop - nML Exception Analyzer

Sukyoung Ryu
ROPAS
Dept. of Computer Science
KAIST (Korea Advanced Institute of Science and Technology)

Synopsis

nea

neatop [ -I lib-dir ] [ -F file ] [ -d ] [ -p ] [ -t ] file

Description

• Batch analyzer (nea)
  • Inputs are nML files and outputs are analysis results.

    eg. % nea file.n

  • In case of incremental analysis, two options should be provided. For nML type checker, every included directory should be mentioned by "-I <dir>". And for nML EA, all the previously analyzed file names should be listed by "-F <file>". The order of previously analyzed file names does not matter.

    eg. % nea -I kb -F kb/kb1.n kb/kb2.n

  • Options

    -I <dir>	Add the given directory to the list of directories searched for typechecked file (.nty).
    -F <file>	Add the given file to the list of files searched for pre-analyzed ea file (.nea).
    -d	Print debugging information.
    -p	Print absyn.
    -t	Print time profile information.

• Toplevel analyzer (neatop)

  Input to the toplevel can span several lines. It terminates by ;; (a double-semicolon).

  eg. % neatop
        nML Exception Analyzer, Version 0.9, 08/06/2001, Sukyoung Ryu [ROPAS/KAIST]
        #

• Analysis results

  For each function of the program, nML EA reports a set of pairs <exn,loc> of an exception exn and its birth (construction, not declaration) place loc. For example,

  •     emitPar (type/e2m.n:862.14-121)
            { <NotImplemented, type/e2m.n:58.40-54> }
    tells that function emitPar defined at "type/e2m.n:862.14-121" may have an uncaught exception NotImplemented, which is constructed at "type/e2m.n:58.40-54."
  •     /unnamed ftn/ (type/e2m.n:962.21-40)
            {}
    tells that the unnamed function at "type/e2m.n:962.21-40" has no uncaught exception.
  •     /emitBlock _ / (type/e2m.n:857.18-258)
            { <NotSafe, type/e2m.n:58.40-54> }
    tells that curried function emitBlock (of type t -> t' -> t''), given one argument, returns a function which may have an uncaught exception NotSafe when it is called.
  •     /handler ftn/ (ppc/ppcEm2Ppc.n:3.9-112)
            {}
    tells that handler function at "ppc/ppcEm2Ppc.n:3.9-112" has no uncaught exception. Handler function is the match expression in handle expression: e handle match. If handler's match is not exhaustive, then the analysis says that the handler function (match) has uncaught exceptions.

Restrictions

• nML compiler 0.91 (n/nml-0.91) and nML Control Flow Analyzer (CFA) should be installed to use nML EA.
• Every file should be type-checked.

Papers

• "A Cost-effective Estimation of Uncaught Exceptions in SML Programs", Kwangkeun Yi and Sukyoung Ryu, Theoretical Computer Science, Vol. 273, No. 1, 2001 (invited paper)
• "Towards A Cost-Effective Estimation of Uncaught Exceptions in SML Programs", Kwangkeun Yi and Sukyoung Ryu, Lecture Notes in Computer Science, Vol. 1302, pp.98-113, The 4th International Static Analysis Symposium, Paris, Sept. 1997, (slides)
• "Estimating Uncaught Exceptions in Standard ML Programs from Type-based Equations", Kwangkeun Yi and Sukyoung Ryu and Ki-Hyun Pyun, Proceedings of the 20th Annual International Computer Software and Applications Conference, pp. 455-460, Seoul, August 1996

Report

[ ps / pdf / html ]

Download

nea.tar.gz