Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation

Pierre Lermusiaux (1) , Benoît Montagu (1)

1 EPICURE - Analyse sémantique et compilation pour la sécurité des environnements d'exécution

Exception handling is a key feature in modern programming languages. Exceptions can be used to deal with errors, or as a means to control the flow of execution of a program. Since they might unexpectedly terminate a program, unhandled exceptions are a serious safety concern. We propose a static analysis to detect uncaught exceptions in functional programs, that is defined as an abstract interpreter. It computes a description of the values potentially returned by a program using a novel abstract domain, that can express inductively defined sets of values. Simultaneously, the analysis infers the possibly raised exceptions, by computing in the abstract exception monad . This abstract interpreter has been implemented as an effective static analyser for a large subset of programs, that supports mutable data types, the module system, and dynamically extensible data types such as the exception type. The analyser has been evaluated on several hundreds of programs.

Mots clés: Static Analysis; Exceptions; Higher-Order Programs; Abstract Interpretation; Abstract Domain for Trees

Domaines: Langage de programmation [cs.PL]

Pierre Lermusiaux, Benoît Montagu. Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation. ESOP 2024 - 33rd European Symposium on Programming, Apr 2024, Luxembourg, Luxembourg. pp.391-420, ⟨10.1007/978-3-031-57267-8_15⟩. ⟨hal-04547480⟩