Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

In and Out of SSA : a Denotational Specification

Abstract : We present non-standard denotational specifications of the SSA form and of its conversion processes from and to imperative programming languages. Thus, we provide a strong mathematical foundation for this intermediate code representation language used in modern compilers such as GCC or Intel CC. More specifically, we provide (1) a new functional approach to SSA, the Static Single Assignment form, together with its denotational semantics, (2) a collecting denotational semantics for a simple imperative language Imp, (3) a non-standard denotational semantics specifying the conversion of Imp to SSA and (4) a non-standard denotational semantics for the reverse SSA to Imp conversion process. These translations are proven correct, ensuring that the structure of the memory states manipulated by imperative constructs is preserved in compilers' middle ends that use the SSA form as control-flow data representation. Interestingly, a s unexpected by-products of our conversion procedures, we offer (1) a new proof of the reducibility of the RAM computing model to the domain of Kleene's partial recursive functions, to which SSA is strongly related, and, on a more practical note, (2) a new algorithm to perform program slicing in imperative programming languages. All these specifications have been prototyped using GNU Common Lisp. These fundamental results prove that the widely used SSA technology is sound. Our formal denotational framework further suggests that the SSA form could become a target of choice for other optimization analysis techniques such as abstract interpretation or partial evaluation. Indeed, since the SSA form is language-independent, the resulting optimizations would be automatically enabled for any source language supported by compilers such as GCC.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [35 références]  Voir  Masquer  Télécharger

https://hal-mines-paristech.archives-ouvertes.fr/hal-00915979
Contributeur : Claire Medrala <>
Soumis le : lundi 9 décembre 2013 - 15:31:12
Dernière modification le : mercredi 14 octobre 2020 - 03:52:20
Archivage à long terme le : : dimanche 9 mars 2014 - 23:50:30

Fichier

E-285.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00915979, version 1

Citation

Sebastian Pop, Pierre Jouvelot, George André Silber. In and Out of SSA : a Denotational Specification. Workshop Static Single-Assignment Form Seminar,, Apr 2009, Autrans, France. ⟨hal-00915979⟩

Partager

Métriques

Consultations de la notice

549

Téléchargements de fichiers

361