Ce sujet traite de deux modifications du compilateur zyva du cours. La première partie traite d'une première modification et les deux parties suivantes d'une seconde modification. Les deux modifications sont indépendantes, et les parties le sont également dans une large mesure.
La boucle for
est la construction naturelle pour parcourir
les tableaux. Par exemple, on affiche un tableau t
comportant
n
éléments de type integer
par :
procedure affiche(t:array of integer, n:integer) ; begin for i := 0 to n-1 do writeln(t[i]) end ; |
On notera que l'indice de boucle (c'est-à-dire la variable i
)
n'est pas déclaré explicitement. De fait, notre boucle for est
celle de Caml, dont voici la sémantique informelle.
L'instruction «for i := e1 to e2 do B
» évalue d'abord les deux expressions e1 et e2 (les bornes) en deux valeurs entières (typeinteger
) n et p.Ensuite, le corps B (une instruction) est exécuté de façon répétée dans un environnement où l'indice i (un nom de variable) est lié successivement aux valeurs entières n, n+1, …, p−1, p. Le corps n'est pas exécuté si n > p.
L'affectation de l'indice de boucle i dans le corps B est interdite.
Question 1. On essaie tout d'abord d'opérer une tranformation « source to source » de la boucle for en boucle while.
Une procédure contenant une bouclefor
:sera transformée en :
procedure p(…) ; var … begin … for i := e1 to e2 do B ; … end ;
procedure p(…) ; var i:integer ; … begin … i := e1 ; while i <= e2 do begin B ; i := i+1 end ; … end ;
Donner un exemple qui montre que la transformation décrite ci-dessus ne respecte pas la sémantique de la boucle for.
program ; function prec(x:integer):integer ; begin writeln(x) ; g := x-1 end ; procedure affiche(n:integer) ; begin for i := 0 to prec(n) do writeln(i) end ; begin affiche(2) end. |
2 0 1Alors que le programme transformé affiche 5 entiers :
2 0 2 1 2Plus généralement, la sémantique de la boucle for demande une et une seule évaluation de la borne supérieure e2, tandis que le programme transformé évalue cette borne à chaque évaluation du test.
Plutôt que de suivre la technique de la question 1, on va intégrer complètement la nouvelle construction. La définition des arbres de syntaxe abstraite est étendue par l'ajout des lignes suivantes à la fin du fichier pp.mli.
| For of string * expression * expression * instruction (* For (i, e1, e2, B) est l'arbre de syntaxe abstraite de for i := e1 to e2 do B *) |
Cela revient à ajouter une nouvelle instruction à Pseudo-Pascal.
Question 2. Modifier les analyseurs lexical et syntaxique de zyva (fichiers lexer.mll et parser.mly, donnés en annexe) pour intégrer la nouvelle instruction.
%token FOR TO |
instruction
.
instruction: … /* Comme avant */ | FOR IDENT COLONEQUAL expression TO expression DO instruction { For ($2, $4, $6, $8) } ; |
keywords
, en insérant la ligne suivante par exemple entre les lignes 11
et 12 du fichier lexer.mll.
add_keyword "for" FOR ; add_keyword "to" TO ; |
Question 3. On se propose de rejeter les programmes qui ne respectent
pas la condition « l'affectation de l'indice de boucle dans le corps
de la boucle est interdite ».
Écrire, en Caml, une fonction
checkCorrect
de
type Pp.instruction -> bool
, qui prend en argument une
instruction et renvoie true
, si et seulement si l'interdiction
est respectée.
open Pp (* 'vars' est la liste des indices actifs *) let rec doCheck vars stm = match stm with | Set (x,_)|Read_int (x) -> not (List.mem x vars) | For (x,_,_,body) -> doCheck (x::vars) body | Sequence stms -> doChecks vars stms | While (_,body) -> doCheck body | _ -> true and doChecks vars stms = match stms with | [] -> true | stm::rem -> doCheck vars stm && doChecks vars rem let checkCorrect stm = doCheck [] stm |
Question 4. Proposer une sémantique précise de la boucle for. Pour répondre à cette question, le plus simple est sans doute de compléter l'interpréteur de zyva (fichier interpret.ml donné en annexe), mais on pourra aussi donner des règles d'inférence dans le style de celles du poly, section 3.4.2.
instr
d'interprétation des instructions.
and instr env = function … | For (i, e1, e2, body) -> let i1 = expr_int env e1 in let i2 = expr_int env e2 in let icell = ref (Vint i1) in let env = {env with locals = (i, xcell)::env.locals} in (* Je n'utilise pas la fonction 'extend' donnée qui est mal adaptée ici *) for y=i1 to i2 do icell := Vint y ; (* Important : mettre l'indice à jour *) instr env body done … |
Répondre par des règles d'inférence SOS est un peu plus tordu. Rappelons que les jugements d'exécution d'une instruction sont de la forme générale ρ / σ ⊣ i ⇒ / σ' pour « dans l'état-mémoire σ et l'environnement ρ, l'exécution de l'instruction i produit un nouvel état mémoire σ'. » Pour bien tenir compte du traitement des bornes de la boucle for, j'introduis une nouvelle construction de syntaxe abstraite : la boucle « en cours », notée ForI (labx, vmax, B), où labx est une adresse, vmax est un entier et B est une instruction. La sémantique de cette construction est donnée par les deux règles :
|
|||||
|
On donne ensuite la règle du for lui-même :
|
On remarquera que les deux sémantiques donnent un résultat différent lorsque l'indice de boucle est affecté dans le corps. Ce n'est pas trop grave, au vu du dernier paragraphe de la sémantique informelle qui interdit cette opération.
Question 5. Modifier le générateur de code intermédiaire pour traiter la boucle for. Le générateur est le fichier trans.ml donnée en annexe. Les interfaces code.mli (définition du code intermédiaire) gen.mli (temporaires et étiquettes) et env.mli (environnements de Pseudo-Pascal) sont données en annexe.
cinstruction
de
compilation des instructions.
let rec cinstruction env stm = match stm with | Set (s,e) -> … (* Comme avant *) | For (x, e1, e2, body) -> (* Se donner trois étiquettes *) let lab_test = Gen.new_label () and lab_enter = Gen.new_label () and lab_out = Gen.new_label () in (* Se donner deux temporaires (indice et limite) *) let t_x = Gen.new_temp () and t_up = Gen.new_temp () in (* Renvoyer une seule instruction -> Seq *) Seq [ Move_temp (tx, cexpr env e1) ; Move_temp (t_up, cexpr env e2) ; Label lab_test ; Cjump (Rle, t_x, t_up, lab_enter, lab_out) ; Label lab_enter ; cinstruction (Env.add_local_vars env [x, t_x]) (* Attention à l'environnement *) body ; Move_temp (t_x, Bin (Plus, t_x, Const 1)) ; Jump lab_test ; Label lab_out ; ] |
Question 6. Proposer une transformation correcte de la
boucle for en boucle while équivalente.
Concrètement, on expliquera comment transformer la
procédure p
de la question 1.
Attention On veillera à traiter correctement le cas où la
procédure p
utilise une variable de nom i en dehors du corps
de la boucle.
procedure p(…) ; var i', i'':integer ; … begin … i' := e1 ; i'' := e2 ; while i' <= i'' do begin B' ; i' := i' + 1 end ; … end ; |
For (i, e1, e2, I)[i ← i'] | = | For (i, e1[i ← i'], e2[i ← i'], I) | |||
For (j, e1, e2, I)[i ← i'] | = | For (j, e1[i ← i'], e2[i ← i'], I[i ← i']) | (j ≠ i) | ||
Set (i, e)[i ← i'] | –Interdit– | ||||
Set (j, e)[i ← i'] | = | Set (j, e[i ← i']) | (j ≠ i) | ||
Sequence [I1; …; In][i ← i'] | = | Sequence [I1[i ← i']; …; In[i ← i']] | |||
If (e, I1, I2)[i ← i'] | = | If (e[i ← i'], I1[i ← i'], I2[i ← i']) | |||
While (e, I)[i ← i'] | = | While (e[i ← i'], I[i ← i']) | |||
Call (p, e1, …, en)[i ← i'] | = | Call (p, e1[i ← i'], …, en[i ← i']) |
Get (i)[i ← i'] | = | Get (i') | |||
Get (j)[i ← i'] | = | Get (j) | (j ≠ i) | ||
Bin (op, e1, e2)[i ← i'] | = | Bin (op, e1[i ← i'], e2[i ← i']) | |||
⋮ |
Dans cette partie (et dans la suivante)
on se propose d'étendre zyva pour qu'il
traite les calculs flottants.
Seuls deux points importants seront traités, d'abord l'utilisation du
coprocesseur flottant du MIPS, puis, dans la partie suivante,
la distinction entre opérations flottantes et entières à l'aide du typage.
Le processeur MIPS peut donc être équipé d'un coprocesseur chargé des
calculs flottants. Nous allons uniquement considérer des nombres flottants
double précision (type real
de
Pseudo-Pascal) dont la taille est de deux mots mémoire ou 8 octets.
$f0
,
$f2
, …, $f30
(de deux en deux).
Chaque registre double $f
<n> (n pair)
regroupe en fait deux registres simple
précision, notés $f
<n> et $f
<n+1>.
En pratique, tout se passe le plus souvent comme
si le coprocesseur possédait bien 16 registres doubles.
add.d $f0, $f2, $f4
range la somme (addition flottante double précision) du
contenu des registres
$f2
et $f4
dans le registre $f0
.
mov.d
de transfert entre
registres du copresseur dont l'usage est similaire à celui de
l'instruction move
du processeur.
Par exemple, l'instruction mov.d $f0, $f2
copie le contenu du
registre (double) $f2
dans le registre (double) $f0
.
Question 7. Énoncer des conventions d'appel pour les fonctions qui prennent des arguments flottants et rendent un résultat flottant. On illustrera ensuite ces conventions en « compilant » la fonction Pseudo-Pascal suivante :
function fadd(x,y : real) : real ; begin fadd := x + y end |
real
sont passés dans les registres
$f2
, $f4
, $f6
et $f8
,
puis dans la pile ; tandis que le résultat de d'une fonction est rendu
dans le registre $f0
quand il est
de type real
.fadd: add.d $f0, $f2, $f4 j $ra |
Question 8. On suppose que le compilateur zyva est
suffisament sophistiqué pour introduire des conversion des entiers
(type integer
) vers les flottants
(type real
) quand c'est utile.
Comme par exemple dans la fonction suivante ou l'addition demande la
conversion préalable de l'entier n
:
function fiadd(x:real; n:integer):real; begin fiadd := x+n end ; |
Pour réaliser ces conversions, le processeur MIPS emploie les instructions suivantes :
mtc1
(Move To Coprocessor 1).
Par exemple, l'instruction mtc1 $v0, $f2
copie le contenu du
registre $v0
(du processeur), dans le registre $f2
(du
coprocesseur).
cvt.d.w
. De sorte que, par exemple,
l'instruction cvt.d.w $f0, $f2
convertit l'entier contenu dans le
registre $f2
en flottant double
précision et range ce résultat dans le registre (double) $f0
du
coprocesseur.
Donner un code possible résultat de la compilation
de fiadd
.
$a0
), on a
par exemple :
fiadd: mtc1 $a0, $f0 # Transfert vers le coprocesseur ($f1 inchangé) cvt.d.w $f0, $f0 # conversion vers la paire $f0, $f1 add.d $f0, $f2, $f0 j $ra |
Question 9. Compiler manuellement la fonction suivante :
function ffiadd(x : real; n:integer):real; begin ffiadd := fadd(x,fiadd(x, n)) end; |
Attention : On demande un code tel que produit par le
compilateur zyva qui n'a pas connaissance des registres
modifiés par les fonction appelées, mais s'appuie sur des conventions
d'emploi des registres clairement énoncées.
Le coprocesseur peut lire un flottant en mémoire par l'instruction
l.d
et écrire un flottant en mémoire
par l'instruction s.d
. Ces deux
instructions fonctionnent comme les instructions lw
et sw
du processeur. Par exemple l.d $f0, 0($a0)
charge les deux mots
mémoire d'adresses $a0
et $a0
+4 dans le
registre (double) f0.
$f16
à $f30
sont traités
comme des callee-save.
ffiadd_f=12 ffiadd: subu $sp, $sp, ffiadd_f sw $ra, 8($sp) s.d $f16, 0($sp) # Libérer le callee-save $f16 mov.d $f16, $f2 # L'argument 'x' est dans $f16 mov.d $f2, $f16 # inutile jal fiadd # arguments dans $f2 et $a0 mov.d $f2, $f16 mov.d $f4, $f0 jal fadd # arguments dans $f2 et $f4 lw $ra, 8($sp) l.d $f16, 0($sp) addu $sp, $sp, ffiadd_f j $ra |
$ra
(usage général) et $f16
(flottant) entraîne la
consommation de 1+2 = 3 mots de pile.
Le programmeur Pseudo-Pascal ne fait aucune distinction entre opérations entières et opérations flottantes. C'est-à-dire qu'il écrit par exemple.
function test(n:integer ; x:real) : real ; begin n := n + n ; x := x + x ; test := x + n end ; |
Ici, la première addition est une addition entière (en dernière
analyse add
), tandis que les
deux suivantes sont des additions flottantes
(en dernière analyse add.d
).
En outre, la dernière addition ne peut s'effectuer qu'une fois l'entier n
converti (ou « promu ») en flottant.
On dit que l'opérateur « + » est surchargé, il peut signifier
des opérations différentes selon les types de ses arguments.
Question 10. Comment peut-on justifier l'introduction par le compilateur de conversions implicites des entiers vers les flottants ? On remarquera que l'utilisation implicite de la conversion inverse des flottants vers les entiers n'est pas autorisée.
Le compilateur zyva modifié procède à la résolution de la surcharge lors d'une phase sémantique de vérification des types. Concrètement, on va réécrire la syntaxe abstraite du programme en syntaxe abstraite typée.
La syntaxe abstraite est donnée dans l'annexe pp2.mli (attention la syntaxe abstraite a un peu changé par rapport à la première partie), la syntaxe abstraite typée est donnée dans le fichier tpp.mli. Les deux syntaxes abstraites non-typée et typée font référence aux types des opérations et des comparaisons définies dans le fichier primitive.mli.
Pour ce qui nous intéresse, la syntaxe typée étend et précise la syntaxe non-typéee au sens suivant :
binop
) de la syntaxe non-typée sont partitionnés
entre calcul (constructeur Op
) et comparaisons
(constructeur Cmp
). Ils apparaissent comme arguments du constructeur
des expressions Bin
.Les opérateurs (type fun_prim
) de la syntaxe typée sont
partitionnés de même et aussi entre opérations entières et flottantes
(constructeurs IOp
et ICmp
d'une part, et
FOp
et FCmp
d'autre part). Ils apparaissent comme
arguments du constructeur des expressions Prim_call
, qui
représente l'application des
opérateurs. Il y a quelques nouveaux opérateurs et notamment la
promotion d'un entier en flottant (ItoF
).
On notera que Prim_call
prend une liste d'expressions en
second argument, car tous les opérateurs n'ont pas exactement deux arguments.
Par exemple, la promotion d'une expression de type entier e en flottant
et l'addition de deux expressions entières s'expriment ainsi en
syntaxe typée :
Prim_call (ItoF, [e]) : Real Prim_call (IOp (Add), [e1; e2]) : Integer |
Noter la syntaxe spéciale « … : t » qui met en valeur le dernier argument des constructeurs de la syntaxe typée (le type justement).
Question 11. L'action du vérificateur de type est donc une traduction de la syntaxe abstraite non-typée vers la syntaxe abstraite typée. On peut l'exprimer par des règles d'inférence qui prouvent des propositions de la forme : Γ ⊣ e ⇒ e':t, à lire comme : « dans l'environnement Γ, l'expression e non-typée e se traduit en expression typée e', de type t.
Voici par exemple, comment sont typées les constantes entières, les variables et l'addition entière :
|
||||||||
|
Écrire les règles de l'addition flottante. Attention : Les règles doivent être suffisament puissantes pour typer tous les exemples d'addition de cette partie. Par ailleurs, le typage doit être déterministe, c'est-à-dire autoriser au plus une façon de typer une addition donnée.
real
, puis celui où un argument est de type integer
et l'autre de type real
.
|
|||||
|
real
, second
argument de type entier » symétrique de la seconde règle ci-dessus.La solution qui consiste à ne retenir que la première règle (addition de deux flottants) et une règle de promotion n'est pas complètement satisfaisante.
|
Supposons donnée une variable x
de type real
et
considérons l'affectation x := 1 + 2
.
Les règles autorisent alors, soit de promouvoir d'abord les deux
arguments 1
et 2
puis d'effecture une addition flottante,
soit d'effectuer une addition entière puis de promouvoir le résultat.
Même si la valeur affectée à x
est la même dans les deux cas, ce
n'est pas très déterministe. On notera aussi que, dans le cas de la
division1/2
, alors les deux valeurs peuvent différer.
On obtient alors 0.5
dans le premier cas et 0.0
dans le second.
Question 12. Le fichier typer.ml (la dernière annexe), réalise un vérificateur de type. Il est incomplet dans le sens qu'il ne réalise aucune promotion des entiers vers les flottants. Modifiez-le, afin d'introduire ces conversions partout où c'est possible. Ne pas se laisser impressionner par la longueur du code, une modification mineure permet de répondre à la question.
check
du programme donné.
(* Introduire une conversion d'un entier en flottant *) let promote e = Function_prim (ItoF, [e], Real) (* Verifier que l'expression 'e' a bien le type 'expected' *) let check expected e = let found = get_type e in if expected <> found then match expected, found with | Real, Integer -> promote e | _ -> raise (Bad (expected, found)) else e |
Ce document a été traduit de LATEX par HEVEA