Sémantique dynamique et analyse de flot de contrôle pour Java

Abstract

Dans ce mémoire, nous nous intéressons à étudier le langage Java sur deux volets: la sémantique dynamique et l'analyse de flot de contrôle.

Dans la première partie de ce travail nous élaborons une sémantique dynamique formelle sous forme d'un ensemble de règles d'évaluation. Cette sémantique dynamique avec la sémantique statique élaborée dans l'équipe dans le cadre de la maîtrise de Mme Fourati constituent les fondements théoriques pour les techniques d'analyse, d'optimisation et de vérification de programmes Java.

Dans la deuxième partie nous concevons une technique d'analyse de flot de contrôle. Cette analyse est préalable à toutes les analyses statiques visant à optimisier le code ou à le vérifier. L'analyse de flot de contrôle de Java se heurte à deux obstacles majeurs: les appels dynamiques et les exceptions. Nous présentons une technique qui permet de résoudre ces deux problèmes ensemble. Cette méthode agit en deux phases: la première au niveau intraprocédural (dans une seule procédure) et la deuxième au niveau interprocédural (entre procédures). Des algorithmes de construction du graphe de flot de contrôle pour un programme Java sont proposés.

Abstract (AI English translation)

Information popover about translation disclaimer

In this thesis, we are interested in studying the Java language on two aspects: dynamic semantics and control flow analysis.

In the first part of this work we develop a formal dynamic semantics in the form of a set of evaluation rules. This dynamic semantics with the static semantics developed in the team as part of Ms. Fourati's master's degree constitute the theoretical foundations for the techniques of analysis, optimization and verification of Java programs.

In the second part we design a control flow analysis technique. This analysis is prior to all static analyzes aimed at optimizing the code or verifying it. Java control flow analysis faces two major obstacles: dynamic calls and exceptions. We present a technique that solves these two problems together. This method acts in two phases: the first at the intraprocedural level (within a single procedure) and the second at the interprocedural level (between procedures). Algorithms for constructing the control flow graph for a Java program are proposed.