6 La sémantique opérationnelle à grands pas de C--
Soit Z32 l'ensemble de tous les entiers signés 32 bits: Z32 =
[−231, 231−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:
|
e |
::= |
x |
variable |
|
| |
e plus e |
addition |
|
| |
call f (e, …, e) |
appel de fonction |
|
et où les instructions sont de la forme:
|
c |
::= |
x=e |
affectation |
|
| |
skip |
ne rien faire |
|
| |
c;c |
séquence |
|
| |
if (e) then c else c |
test |
|
| |
while (e) c |
boucle |
|
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 (ℓ, c, e), où ℓ 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 Z32 à des variables.
Définissons des règles permettant de déduire des jugements de
la forme ρ ⊢πe ⇒ V, 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
e1 plus e2 plutôt que e1+e2 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 ρ ⊢πc ⇒ ρ'
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 ρ [x ↦ V] désigne la fonction de domaine dom ρ ∪ {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 e1 et avant l'exécution de
e2.
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 ρ
⊢πc ⇒ ρ' soit déductible.
Exercice 1
Si ρ (x) n'est pas défini, while (x) skip
termine-t-il?
Exercice 2
Montrer que while (x) skip termine à partir de
ρ si et seulement si x in dom ρ et ρ (x) = 0.
L'appel de fonction fait aussi ce qu'on attend de lui:
(10)
où [x1↦ V1, …, xn↦ Vn] est l'environnement qui à x1 associe
V1, ..., à xn associe Vn.
Exercice 3
Que se passe-t-il si on appelle une fonction f sur le mauvais
nombre d'arguments, i.e., si on cherche à évaluer call f
(e1, …, en) alors que π (f) = ((x1, …, xm), c) et m ≠ n?
Que se passe-t-il si f ∉dom π?
Exercice 4
Montrer que cette sémantique est déterministe: si ρ ⊢πc ⇒
ρ' et ρ ⊢πc ⇒ ρ'' 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.
Exercice 5
En Caml, on n'a pas besoin de la construction while. Au
lieu d'écrire:
while e do c;;
on peut en effet écrire
let rec f () =
if e
then begin
c;
f ()
end
else ()
in f ();;
où f
est un nom frais (non utilisé dans e
ou
c
). Peut-on recoder les boucles while par un codage
similaire dans le langage de cette section? Et en C? Et en C--?
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.
6.2 La sémantique de C--
Un programme π est pour nous un couple (ρπ,
funπ):
-
L'environnement global ρπ:
string
→ Addr 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 funπ:
string
→
var_declaration list
×
loc_code
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.
Exercice 6
La définition de π permet-elle d'allouer deux variables à la même
adresse? Ceci est-il souhaitable? Si oui, pourquoi? Si non,
comment réparer la définition?
Exercice 7
La définition de funπ n'autorise pas à avoir deux
fonctions de même nom. Mais il peut y avoir deux
CFUN
(loc, f, params, code) avec le même
f fourni à la fonction compile
. Comment
traduisez-vous ces dernières
var_declaration
en entrées pour
funπ, pour tenir compte de cette différence
conceptuelle?
On définit une série de jugements de sémantique opérationnelle de la
forme μ, ρ ⊢πe ⇒ v, μ', qui dit qu'en partant d'une mémoire μ :
Addr → Z32, et d'un environnement ρ :
string
→ Addr qui dit à quelles adresses
sont stockées les variables, l'expression C-- e peut s'évaluer en
la valeur v in Z32, 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)
Exercice 8
Quelle règle s'applique-t-elle dans le cas d'une variable locale
(x in dom ρ) qui a le même nom qu'une variable globale (x in dom
ρπ)?
Exercice 9
Que se passe-t-il si x est une variable globale pour laquelle
aucune mémoire n'est allouée (ρπ(x) ∉dom μ?)
(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,
.main_3:
.string "r"
.align 4
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.
Exercice 10
La sémantique ci-dessus n'oblige pas à stocker toute chaîne présente
dans le programme. Que se passe-t-il si s n'est stockée nulle
part?
Pour toute mémoire μ, pour toute adresse a in Addr, pour toute
valeur v in Z32, notons μ [a ↦ v] 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)
Exercice 11
Que se passe-t-il si on écrit x=1
en C--
mais que x
n'est pas dans dom ρ? ... ni
dans dom ρ ni dans dom ρπ? Ceci arrive lorsque
x
n'aura pas été déclarée, typiquement par
int x
. Comment réagit
mcc
dans ce cas? Comment réagit
gcc
dans ce cas?
Exercice 12
Pourquoi demande-t-on ρ (x) in dom μ', resp. ρπ(x) in dom μ'
dans ces règles? Autrement dit, quel genre de comportement étrange
l'omission de ces conditions autoriserait-il?
Passons aux instructions de la forme x[i]=e. On comprend l'addition
a+v comme étant effectuée modulo 232.
(17)
(18)
Exercice 13
Dans quel ordre cette règle évalue-t-elle e et e'? Que spécifie
la norme ANSI C?
Exercice 14
Pourquoi demandons-nous que v in Z32 et a+v in Addr dans ces
règles?
Disons qu'une mémoire μ' étend μ, ce que nous noterons μ'
⊑ μ, si et seulement si dom μ' ⊇ dom μ et μ'|dom μ = μ. On
note [x1 ↦ a1, …, xn ↦ an] la fonction qui à chaque xi
associe ai, 1≤ i≤ n. Ceci est bien défini lorsque les xi sont
distinctes deux à deux.
(19)
Exercice 15
Dans quel ordre sont évalués les arguments d'un appel de fonction
CALL
comme ci-dessus? Que dit la norme
ANSI C à ce sujet?
Exercice 16
Pourquoi demande-t-on μ'n ⊑ μn, ..., μ'2 ⊑ μ2, μ'1 ⊑ μ1
dans (19)? Pour répondre à cette question, imaginez
que μ'n=μn, ..., μ'2=μ2 dans (19), et
demandez-vous si votre compilateur produit effectivement du code
correspondant à la spécification.
Exercice 17
Pourquoi, sur le même principe, ne demanderions-nous pas des
mémoires auxiliaires qui étendent μ', plutôt que de réutiliser
directement μ' dans l'évaluation de e', dans les règles
(17) et (18)?
Exercice 18
Que se passe-t-il si la fonction f n'est pas définie? Si f est
définie avec un nombre d'arguments différent de n? Si la liste
des paramètres formels de f n'est pas de la forme
CDECL
(l1, x1), …,
CDECL
(ln, xn) mais contient un élément
de la forme CFUN
(…)?
Exercice 19
Pourquoi demande-t-on a1 ∉dom μ1, ..., an ∉dom μn
dans les prémisses de (19)?
Exercice 20
Rien n'empêche les variables x1, ..., xn d'être non distinctes.
Si c'est le cas, la notation [x1 ↦ a1, …, xn ↦ an] 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 232.
(20)
Exercice 21
Dans quel cas le modulo 232 est-il nécessaire?
(21)
Exercice 22
On aurait pu s'attendre que la négation bit à bit soit décrite en
termes des bits de v. Montrer que la définition ci-dessus est
équivalente, autrement dit que −v−1 est bit la négation bit à bit
de v.
(22)
(23)
Exercice 23
Que se passe-t-il si on applique M_POST_INC
à autre chose qu'une variable?
Exercice 24
Écrire les règles sémantiques pour
M_PRE_INC
,
M_POST_DEC
,
M_PRE_DEC
.
(24)
Exercice 25
Pourquoi μ'2 ⊑ μ2?
Exercice 26
Dans quel ordre sont évalués les arguments?
Exercice 27
Écrire les règles sémantiques pour S_DIV
,
S_MOD
, S_ADD
,
S_SUB
.
(25)
Exercice 28
Écrire le reste de la sémantique!