6  La sémantique opérationnelle à grands pas de C--

• 6.1  Une sémantique simple pour un sous-ensemble de C--
• 6.2  La sémantique de C--

Définissons, petit à petit, la sémantique de C--, hors exceptions. Les exceptions seront décrites en section 7.

Soit Z₃₂ l’ensemble de tous les entiers signés 32 bits: Z₃₂ = [−2³¹, 2³¹−1]. Soit Addr le sous-ensemble de toutes les adresses.

Nous allons présenter la sémantique de C-- en deux étapes. En section 6.1, nous présenterons une sémantique pour un sous-ensemble extrêmement réduit de C--. L’avantage est que cette sémantique sera très simple. Certaines particularités de C-- nous forceront à décrire une sémantique plus compliquée en section 6.2.

6.1  Une sémantique simple pour un sous-ensemble de C--

Considérons un langage où les expressions sont juste celles de la forme:

et où les instructions sont de la forme:

Pour pouvoir donner une sémantique aux appels de fonction (call), il nous faut nous donner la description d’un programme π. Pour nous, un programme π sera une fonction mathématique, de domaine fini, qui à des noms de fonction f associe un triplet (l, c, e), où l est une liste de variables distinctes deux à deux (les paramètres formels de la fonction f), c est une instruction (le corps de la fonction), et e est une expression (dénotant la valeur retournée par la fonction).

Les expressions et les instructions seront évaluées dans un environnement ρ, qui est une fonction de domaine fini associant une valeur dans Z₃₂ à des variables.

Définissons des règles permettant de déduire des jugements de la forme

signifiant “dans l’environnement ρ, l’expression e a pour valeur V”.

On a d’abord une règle pour la variable:

(1)

Cette règle s’applique dès que x est dans le domaine de ρ. Elle n’a aucune (autre) prémisse.

On a ensuite une règle pour l’addition:

(2)

(La raison pour laquelle nous écrivons l’addition e₁ plus  e₂ plutôt que e₁+e₂ par exemple est pour bien distinguer l’opération syntaxique plus de l’opération mathématique d’addition, notée +.)

Nous traiterons de l’appel de fonctions plus loin.

On peut maintenant définir des jugements de la forme

pour chaque instruction c, signifiant “en partant de l’environnement ρ, l’instruction c termine sur un nouvel environnement ρ′, le programme courant étant π”. De nouveau, les jugements dérivables sont définis par des règles de déduction.

La première est pour l’affectation:

(3)

La notation

désigne la fonction de domaine dom  ρ union {x}, qui à x associe V et à tout y in dom  ρ ∖ {x} associe ρ (y).

L’instruction skip ne fait strictement rien de remarquable:

(4)

La séquence évalue ses arguments… en séquence:

(5)

Elle introduit donc un environnement intermédiaire ρ′ représentant l’environnement après l’exécution de e₁ et avant l’exécution de e₂.

Jusqu’ici, nous avions une règle de déduction par construction syntaxique. Ceci change pour le test. Nous avons une règle lorsque la condition testée est fausse, et une lorsqu’elle est vraie:

(6)

Comme en C, 0 est faux, et tout autre nombre est considéré comme vrai.

(7)

La boucle while  (e)  c est équivalente à if  (e) then  c;while  (e)  c  else skip. Ceci donne lieu, ici aussi, à deux règles pour l’évaluation des boucles.

(8)

(9)

La seconde règle a la particularité que sa seconde prémisse ne porte pas sur une instruction plus petite que celle en conclusion, contrairement aux règles présentées jusqu’ici. Ceci mène à des comportements non terminants. Disons que c termine dans π, à partir de ρ, si et seulement s’il existe ρ′ tel que soit déductible.

L’appel de fonction fait aussi ce qu’on attend de lui:

(10)

où est l’environnement qui à x₁ associe V₁, …, à x_n associe V_n.

Exercice 4   Montrer que cette sémantique est déterministe: si et sont déductibles, alors ρ′ = ρ″. Dites précisément sur quoi vous effectuez une récurrence, et décrivez quelques-uns des cas que vous traitez, notamment ceux utilisés lorsque c est une boucle while.

while e do c;;

let rec f () = 
        if e
           then begin
                  c;
                  f ()
                end
        else ()
in f ();;

Il manque à cette sémantique, notamment, l’allocation mémoire et les pointeurs, les variables globales, la possibilité d’effectuer des effets de bord à l’intérieur des expressions. Ceci sera réparé dans la sémantique de C--, que nous décrivons tout de suite.

De plus, la sémantique de l’appel de fonctions est en réalité un peu bricolée, autrement dit pas très élégante. On verra à la section 7.2 qu’un style de sémantique dit par continuations est plus élégant, tout en étant plus proche du code assembleur que l’on produit classiquement.

6.2  La sémantique de C--

Un programme π est pour nous un couple (ρ_π, fun_π):

• L’environnement global envoie chaque nom de variable globale vers une adresse allouée pour elle. (Les variables globales sont décrites par les CDECL (loc,x) dans la liste de var_declaration fournie à la fonction compile. Le compilateur doit donc allouer une place mémoire pour chaque.)
• La définition envoie chaque fonction définie dans le programme vers son code. (Ce sont les CFUN (loc, f, params, code) dans la liste de var_declaration fournie à la fonction compile.)

On supposera pour simplifier que fun_π contient aussi des entrées pour toutes les fonctions de la libc, comme printf, strcpy, malloc, free, etc. Et que, de même, ρ_π contient aussi des entrées pour toutes les variables globales de la libc, comme errno par exemple.

On définit une série de jugements de sémantique opérationnelle de la forme

qui dit qu’en partant d’une mémoire , et d’un environnement qui dit à quelles adresses sont stockées les variables, l’expression C-- e peut s’évaluer en la valeur v in Z₃₂, et modifier la mémoire en µ′.

Il y a deux sortes de variables. Les variables locales (ou automatiques dans le jargon du C) sont données dans l’environnement ρ:

(11)

Les variables globales sont décrites par l’environnement global ρ_π.

(12)

(13)

L’évaluation des chaînes est un peu plus étrange. Elle retourne une adresse mémoire quelconque où se trouve déjà la représentation de s. Disons que s est stockée à l’adresse a si et seulement si s ne contient pas l’octet 0, il existe une adresse a+k dans la mémoire µ contenant un octet nul, avec k minimal, et la suite de tous les octets aux adresses a, a+1, a+2, …, a+k−1 vaut s.

(14)

En pratique, le compilateur devra allouer de la place pour la chaîne s à la compilation. Ceci est fait pratiquement automatiquement par l’assembleur. Par exemple,

réserve de la place pour les octets ‘r’ et 0, les place à une adresse nommée .main_3. L’instruction mystérieuse .align 4 sert à assurer que ce qui suit commencera à une adresse multiple de 4, ce qui facilite la tâche du processeur pour certaines opérations.

Pour toute mémoire µ, pour toute adresse a in Addr, pour toute valeur v in Z₃₂, notons la mémoire qui à a associe v, et à toute autre adresse a′ ≠ a associe µ (a′).

On a encore deux règles pour SET_VAR, selon que la variable est locale ou globale.

(15)

(16)

Passons aux instructions de la forme x[i]=e. On comprend l’addition a+v comme étant effectuée modulo 2³².

(17)

(18)

Disons qu’une mémoire µ′ étend µ, ce que nous noterons , si et seulement si et µ′_{|dom  µ} = µ. On note la fonction qui à chaque x_i associe a_i, 1≤ i≤ n. Ceci est bien défini lorsque les x_i sont distinctes deux à deux.

(19)

Exercice 16   Pourquoi demande-t-on , …, , dans (19)? Pour répondre à cette question, imaginez que µ′_n=µ_n, …, µ′₂=µ₂ dans (19), et demandez-vous si votre compilateur produit effectivement du code correspondant à la spécification.

Exercice 19   Pourquoi demande-t-on , …, dans les prémisses de (19)?

Exercice 20   Rien n’empêche les variables x₁, …, x_n d’être non distinctes. Si c’est le cas, la notation n’a aucun sens. Réparez la règle (19) pour tenir compte de ce fait.

Passons aux opérations unaires. La négation effectue son calcul modulo 2³².

(20)

(21)

(22)

(23)

(24)

Exercice 25   Pourquoi ?

(25)