Analyse d'affectation définitive

En informatique , l'analyse d'affectation définie est une analyse de flux de données utilisée par les compilateurs pour garantir de manière prudente qu'une variable ou un emplacement est toujours affecté avant d'être utilisé.

Il existe deux manières courantes de résoudre ce problème. La première consiste à s'assurer que toutes les adresses mémoire sont écrites avant d'être lues. Le théorème de Rice établit que ce problème ne peut être résolu de manière générale pour tous les programmes ; toutefois, il est possible de créer une analyse conservatrice (imprécise) qui n'acceptera que les programmes respectant cette contrainte, tout en rejetant certains programmes corrects. L'analyse d'affectation définitive est une telle analyse. Les spécifications des langages de programmation Java et C# exigent que le compilateur signale une erreur de compilation en cas d'échec de l'analyse. Les deux langages requièrent une forme spécifique de cette analyse, décrite en détail. En Java, cette analyse a été formalisée par Stärk et al. , et certains programmes corrects sont rejetés et doivent être modifiés pour introduire explicitement les affectations inutiles. En C#, cette analyse a été formalisée par Fruja et est à la fois précise et robuste, en ce sens que toutes les variables affectées le long de tous les chemins d'exécution sont considérées comme définitivement affectées. Le langage Cyclone exige également que les programmes passent une analyse d'affectation définie, mais seulement sur les variables de type pointeur, afin de faciliter le portage des programmes C.

La seconde solution consiste à initialiser automatiquement toutes les adresses mémoire à une valeur fixe et prévisible lors de leur définition. Cependant, cette méthode introduit de nouvelles affectations susceptibles de dégrader les performances. Dans ce cas, l'analyse des affectations définies permet une optimisation du compilateur qui élimine les affectations redondantes ( affectations suivies uniquement d'autres affectations sans lecture intermédiaire possible ) . Aucun programme n'est alors rejeté, mais ceux pour lesquels l'analyse ne reconnaît pas d'affectation définie peuvent contenir des initialisations redondantes. L' infrastructure de langage commune (CLI) repose sur cette approche.

On peut dire qu'une variable ou un emplacement se trouve dans l'un des trois états suivants à un moment donné du programme :

• Affectation certaine : On sait avec certitude que la variable est affectée.
• Non assignée, c'est certain : on sait avec certitude que la variable n'est pas assignée.
• Inconnu : La variable peut être assignée ou non assignée ; l'analyse n'est pas suffisamment précise pour déterminer laquelle.

Ce qui suit s'appuie sur la formalisation par Fruja de l'analyse d'affectation définie intraprocédurale (méthode unique) en C#, qui garantit que toutes les variables locales sont initialisées avant leur utilisation. Elle effectue simultanément l'analyse d'affectation définie et la propagation constante des valeurs booléennes. Nous définissons cinq fonctions statiques :

Nous fournissons des équations de flux de données qui définissent les valeurs de ces fonctions sur diverses expressions et instructions, en fonction des valeurs des fonctions sur leurs sous-expressions syntaxiques. Supposons pour l'instant qu'il n'y ait pas d'instructions `goto` , `break` , `continue` , `return` ni de gestion des exceptions . Voici quelques exemples de ces équations :

• Toute expression ou instruction e qui n'affecte pas l'ensemble des variables définitivement affectées : après ( e ) = avant ( e )
• Soit e l'expression d'affectation loc = v . Alors avant ( v ) = avant ( e ), et après ( e ) = après ( v ) U {loc}.
• Soit e l'expression vraie . Alors vrai ( e ) = avant ( e ) et faux ( e ) = variables ( e ). Autrement dit, si e est évaluée à faux , toutes les variables sont ( viduellement ) définitivement affectées, car e n'est pas évaluée à faux.
• Les arguments d'une méthode étant évalués de gauche à droite, avant( arg _{i + 1} ) = après( arg _i ). Une fois l'exécution de la méthode terminée, les paramètres de sortie sont définitivement affectés.
• Soit s l'instruction conditionnelle si ( e ) s ₁ sinon s ₂ . Alors avant ( e ) = avant ( s ), avant (s ₁ ) = vrai ( e ), avant ( s ₂ ) = faux ( e ), et après ( s ) = après ( s ₁ ) intersectent après ( s ₂ ).
• Soit s l' instruction de boucle while while ( e ) s ₁ . Alors before( e ) = before( s ), before( s ₁ ) = true( e ), et after( s ) = false( e ).
• Et ainsi de suite.

Au début de la méthode, aucune variable locale n'est assignée de manière définitive. Le vérificateur parcourt l' arbre de syntaxe abstraite et utilise les équations de flux de données pour faire migrer les informations entre les ensembles jusqu'à atteindre un point fixe . Ensuite, il examine l'ensemble précédent de chaque expression utilisant une variable locale afin de s'assurer qu'elle contient bien cette variable.

L'algorithme est complexifié par l'introduction de sauts de contrôle tels que ` goto` , `break` , `continue` , `return` et la gestion des exceptions. Toute instruction susceptible d'être la cible d'un de ces sauts doit avoir son ensemble de valeurs `before` communiquant avec l'ensemble des variables définitivement affectées à la source du saut. L'introduction de ces sauts peut engendrer un flux de données comportant plusieurs points fixes, comme dans cet exemple :