Un mini compilateur certifié

Le projet compcert initié en 2005 par Xavier Leroy est probablement l'une des réalisations les plus intéréssantes du domaine. Le but de ce projet est de développer un compilateur d'un gros sous-ensemble du langage C vers des architectures réalistes (PowerPC, ARM, x86, ...). Le développement de compcert consiste en un programme Coq d'une centaine de milliers de lignes dont est extrait un compilateur programmé en Caml qui compile du code C vers une de ces architectures. La formalisation en coq permet de prouver que ce compilateur préserve la sémantique du langage de départ. Cela assure donc à l'utilisateur du compilateur que ce dernier n'introduira aucun bug en traduisant le C en assembleur.

Le but de ce devoir sera de développer votre propre compilateur certifié. Bien sûr, nous allons être moins ambitieux que compcert, puisqu'il s'agira de compiler une version simplifiée de IMP vers un assembleur allégé.

Votre travail consistera à prouver le plus grand nombre de lemmes possibles sans changer les énoncés ni les définitions (vous êtes biensûr autorisés à ajouter des lemmes). Vous devrez donc nous rendre le fichier compiler.v complété.

Si vous voulez tester votre compilateur, vous pouvez télécharger l'archive imp.tgz qui contient tout ce qui vous sera nécessaire pour extraire le code du source coq et compiler le compilateur (lisez le fichier README pour les instructions).

Des points bonus seront attribués à ceux qui développeront (dans le langage de leur choix) une machine virtuelle pour exécuter le code assembleur.

Require Import Arith.
Require Import List.

Notation "[]" := nil.
Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).

Un modèle de mémoire simpliste

Dans ce devoir, la mémoire est implémentée par le type store comme une liste d'association entre les variables (de type var) et les valeurs (de type value).

Remarque : Ce modèle de mémoire n'est pas

exactement réaliste: la mémoire utilisée par le programme est fixée par le nombre de variables utilisées, il n'est pas possible de faire de l'allocation dynamique de mémoire. C'est comme si l'on avait uniquement des registres (en nombre fini mais autant que l'on veut).

Definition var := nat.
Definition value := nat.

Definition store : Type := list (var * value).
Definition store_empty : store := nil.

On utilisera les deux prédicats suivants pour accéder à la mémoire. get ρ x v signifie que l'environnement ρ associe à x la valeur v.

Inductive get : store -> var -> value -> Prop :=
| get_head : forall l a x, get ((a,x)::l) a x
| get_tail : forall l a b x y, get l a x -> a<>b -> get ((b,y)::l) a x.

update ρ x v ρ' signifie que l'environnement ρ' est obtenu à partir de ρ en remplaçant la valeur associée à x par v.

Inductive update : store -> var -> value -> store -> Prop :=
  | update_head : forall l a x y, update ((a,x)::l) a y ((a,y)::l)
  | update_tail : forall l l' a b x y, update l a x l' -> a<>b -> update ((b,y)::l) a x ((b,y)::l')
  | update_nil : forall a x, update nil a x ((a, x)::nil).

Le lemme suivant affirme qu'on peut toujours mettre à jour un environnement.

Difficulté : 2.
Astuce: vous aurez besoin du lemme dec_eq_nat de la bibliothèque standard.

Lemma update_total:
forall r x v, exists r', update r x v r'.

update met bien à jour l'environnement.

Difficulté : 1.

Lemma update_get:
forall r r' x v,
update r x v r' -> get r' x v.

Mettre à jour deux fois ne sert à rien.

Difficulté: 2.

Lemma update_update:
forall r x v r',
update r x v r' -> forall r'' v', update r x v' r'' -> update r'' x v r'.

La relation update est une relation fonctionnelle.

Difficulté: 1.
Astuce : Vous devrez utiliser inversion.

Lemma update_function :
forall r x v r1,
update r x v r1 -> forall r2, update r x v r2 -> r1 = r2.

Mini-IMP : Un langage de haut niveau

Le type term permet de représenter les expressions manipulées par notre version de IMP.

Remarque: Il faut noter que le choix d'un langage d'expressions

aussi pauvre va simplifier grandement la compilation. En effet, l'absence d'opérateurs binaires (comme l'addition par exemple) permet de compiler l'evaluation d'expressions sans avoir besoin de variables temporaires. Cela évacue également problèmes d'allocation de registres.

Inductive term : Type :=
   | tcst : nat -> term
   | tvar : var -> term
   | succ : term -> term
   | pred : term -> term.

On utilise la notation #n pour les constantes.

Notation "# n" := (tcst n) (at level 1).

Et la notation ! n pour plonger les variables dans les termes.

Notation "! n" := (tvar n) (at level 1).

Le prédicat eval ρ t v nous indique que le terme t s'évalue en v dans l'environnement ρ.

Inductive eval : store -> term -> value -> Prop :=
  | eval_tcst : forall r n, eval r #n n
  | eval_tvar : forall r x n, get r x n -> eval r !x n
  | eval_succ : forall r t n, eval r t n -> eval r (succ t) (S n)
  | eval_pred_S : forall r t n, eval r t (S n) -> eval r (pred t) n
  | eval_pred_0 : forall r t, eval r t O -> eval r (pred t) O.

Voici ainsi la version de IMP que nous allons utiliser. Une fois de plus, afin de simplifier le travail on force les conditions du while et du ifte à être des variables. Bien sûr, idéalement on aurait pu utiliser des termes et les évaluer mais les preuves auraient ainsi été plus longues.

Inductive imp : Set :=
   | skip : imp
   | seqi : imp -> imp -> imp
   | ass : var -> term -> imp
   | ifte : var -> imp -> imp -> imp
   | while : var -> imp -> imp.

Notation "A ;; B" := (seqi A B) (at level 100, right associativity).
Notation "A <- B" := (ass A B) (at level 80, right associativity).

Quelques exemples de programmes

Definition plus_imp a b :=
     while a
       (a <- pred !a;;
        b <- succ !b).

Definition plus_test a b :=
   0 <- #a;;
   1 <- #b;;
   plus_imp 0 1.

Definition mult_imp t r a b :=
     while a
        (t <- !b;;
         plus_imp b r;;
         b <- !t;;
         a <- pred !a).

Definition mult_test a b :=
    0 <- #a;;
    1 <- #b;;
    mult_imp 2 3 0 1.

Definition fact_test n :=
    0 <- #1;;
    1 <- #n;;
    while 1 (
      3 <- !1;;
      4 <- !0;;
      mult_imp 2 0 3 4;;
      1 <- pred !1
    ).

Voici la sémantique à grand pas de mini-IMP: execute ρ k ρ' signifie que la commande k transforme l'environnement ρ en ρ'.

Inductive execute : store -> imp -> store -> Prop :=
   | execute_skip : forall r, execute r skip r
   | execute_ass : forall r r' t a n,
         eval r t n ->
         update r a n r' ->
         execute r (a <- t) r'
   | execute_seq : forall r1 r2 r3 p q,
         execute r1 p r2 ->
         execute r2 q r3 ->
         execute r1 (p;;q) r3
   | execute_ifte_true : forall r t p1 p2 r' x,
         get r t (S x) ->
         execute r p1 r' ->
         execute r (ifte t p1 p2) r'
   | execute_ifte_false : forall r t p1 p2 r',
         get r t 0 ->
         execute r p2 r' ->
         execute r (ifte t p1 p2) r'
   | execute_while_false : forall r t p,
         get r t 0 ->
         execute r (while t p) r
   | execute_while_true : forall r1 r2 r3 t p n,
         get r1 t (S n) ->
         execute r1 p r2 ->
         execute r2 (while t p) r3 ->
         execute r1 (while t p) r3.

Pour vérifier que vous avez compris:

Difficulté: -1.

Lemma mult_23:
execute [(0,2);(1,3)] (plus_test 2 3) [(0,0);(1,5)].

Notre petit langage d'assemblage

Dans cette section, nous décrirons le langage d'assemblage vers lequel nous allons compiler.

On utilisera au besoin la notation $x pour appuyer la distinction variable/constante.

Definition V (n:nat) : var := n.
Notation "$ x" := (V x) (at level 0).

Les instructions de notre assembleur seront étiquetées par des entiers. Ces étiquettes nous permettront de faire des sauts dans le code à l'aide des instructions jmp et brz.

Definition label: Set := nat.
Definition L (n: nat) : label := n.

Voici la (courte) liste des instructions:

jmp l : permet de sauter à l'étiquette l.
brz x l : saute à l'étiquette l si la variable x est nulle.
set x k : assigne à la variable x la valeur k.
mov x y : assigne à la variable x la valeur associée à la variable y.
inc x y : assigne à la variable x la valeur associée à la variable y plus 1.
dec x y : assigne à la variable x la valeur associée à la variable y moins 1.
hlt : arrête la machine.

Les listes d'instructions seront implémentées par les éléments du type instr.

Un programme en assembleur correspond donc à une liste d'instructions étiquetées.

Definition program : Set := list (label * instr).

Cette p notation nous permet de présenter notre exemple joliment.

Notation "'block' l [[ i ]] p" := ((l, i):: p) (at level 0, right associativity, only parsing).
Notation "'end_program'" := nil (only parsing).

Mais que fait ce programme ?

Definition example : program :=
  block (L 0) [[
     set 0 1;
     set 1 3;
     jmp (L 1)]] block (L 1) [[
     brz $0 (L 2);
     dec $0 $0;
     inc $1 $1;
     jmp (L 1)]] block (L 2) [[
     hlt ]] end_program.

Il nous faut bien un prédicat pour aller chercher l'instruction associée à une étiquette.

Inductive lookup : program -> label -> instr -> Prop :=
  |lookup_head : forall p l i,
     lookup ((l, i)::p) l i
  | lookup_tail : forall p l l' i i',
     lookup p l i -> l <> l' ->
     lookup ((l', i')::p) l i.

Voici la sémantique petit pas de notre assembleur : à vous de comprendre ce qu'elle signifie.

Inductive step: program -> store -> instr -> store -> instr -> Prop :=
  | step_seq: forall p r i1 i2 i3,
      step p r ((i1 ; i2) ; i3) r (i1 ; i2 ; i3)

  | step_brz1: forall p r x n i l, get r x (S n) ->
      step p r (brz x l; i) r i

  | step_brz2: forall p r x l i i',
      get r x 0 ->
      lookup p l i' ->
      step p r (brz x l; i) r i'

  | step_jmp: forall p r l i,
      lookup p l i ->
      step p r (jmp l) r i

  | step_set: forall p r r' x n i,
      update r x n r' ->
      step p r (set x n; i) r' i

  | step_mov: forall p r r' x y v i,
      get r y v -> update r x v r' ->
      step p r (mov x y; i) r' i

  | step_inc: forall p r r' x y v c,
      get r y v -> update r x (S v) r' ->
      step p r (inc x y ; c) r' c

Ici, on utilise la fonction prédécesseur de la bibliothèque standard. Nous sommes contraints de la désigner par Peano.pred car on l'a masquée en définissant term.

  | step_dec: forall p r r' x y v c,
      get r y v -> update r x (Peano.pred v) r' ->
      step p r (dec x y ; c) r' c.

Une notation fort utile pour les petit pas.

Notation "( i1 | r1 ) '--' p '-->' ( i2 | r2 )" :=
(step p i1 r1 i2 r2).

La cloture réflexo-transitive de step est donnée par le prédicat suivant:

Inductive run : program -> store -> instr -> store -> instr -> Prop :=
  | run_refl : forall p r c, run p r c r c
  | run_step_run : forall p r c r' c' r'' c'',
        step p r c r' c' -> run p r' c' r'' c'' -> run p r c r'' c''.

Avec sa notation.

Notation "( i1 | r1 ) '==' p '==>' ( i2 | r2 )" :=
(run p i1 r1 i2 r2).

Il faut prouver que run est bien transitive.

Difficulté: 0.

Lemma run_trans:
   forall p r c r' c',
        (r|c) == p ==> (r'|c') ->
   forall r'' c'', (r'| c') == p ==> (r''| c'')
           -> (r | c) == p ==> (r'' | c'').

Ça peut toujours servir.

Difficulté: 0.

Lemma run_step : forall p r c r' c',
step p r c r' c' -> run p r c r' c'.

launch p ρ₁ ρ₂ signifie que si nous lançons p dans l'environnement ρ₁ en commençant par l'instruction à l'étiquette 0, alors nous aboutissons à une instruction hlt dans un environnement ρ₂.

Inductive launch : program -> store -> store -> Prop:=
  | launch_go : forall p c r1 r2, lookup p (L 0) c ->
      (r1 | c) == p ==> (r2 | hlt )
   -> launch p r1 r2.

On utilisera cette notation pour launch.

Notation "r1 '==' p '==>' r2 " :=
(launch p r1 r2) (at level 0).

Cette preuve est facile, mais si vous n'utilisez pas toute la puissance des tactiques, elle risque aussi d'être longue.

Difficulté: 1.

Lemma example_test:
((0,0)::(1,0)::nil ) == example ==> ((0,0)::(1,4)::nil ).

Compilation des expressions arithmétiques

La fonction ci-dessous implémente la compilation des termes. Elle n'est pas difficile à comprendre: compile_term res acc e produit du code qui va placer le résultat de l'évaluation de e dans la variable res et se poursuivre avec l'instruction acc.

Fixpoint compile_term res acc e := match e with
  | tcst n => (set res n);acc
  | tvar x => (mov res x);acc
  | succ e => compile_term res ((inc res res);acc) e
  | pred e => compile_term res ((dec res res);acc) e
  end.

Il faut donc prouver qu'elle est correcte:

Difficulté: 2.

Lemma compile_term_sound :
forall r e v, eval r e v -> forall p res r' acc, update r res v r' ->
(r | compile_term res acc e) == p ==> (r' | acc).

Linéarisation de IMP

Vous entrez maintenant dans la section principale du devoir: c'est ici qu'on va transformer le code structuré de IMP en une liste d'instructions.

Mais avant ça, il va falloir traiter la partie la plus "bureaucratique" du devoir: la gestion des étiquettes du programme.

Réservations des étiquettes.

Le prédicat reserved l p signifie que l'étiquette l n'apparaît pas dans le programme p.

Inductive reserved : label -> program -> Prop :=
  | reserved_nil : forall l, reserved l nil
  | reserved_tail :
     forall l l' x p, reserved l p -> l <> l' -> reserved l ((l',x)::p).

Si ça n'apparaît pas, ça n'apparaît pas.

Difficulté: 2.
Astuce: Il va falloir utiliser inversion.

Lemma reserved_lookup :
forall p l, reserved l p -> forall c, ~lookup p l c.

Le prédicat safe l p dit que toutes les étiquettes de p n'apparaissent qu'une seule fois et sont strictement inférieures à l.

Inductive safe : label -> program -> Prop :=
  | safe_nil : forall l, safe l nil
  | safe_cons :
     forall p c l l',
       reserved l' p ->
       safe l p -> l' < l -> safe l ((l', c)::p).

Les deux lemmes suivants vont vous être utiles.

Difficulté : 0.

Lemma lt_diff:
forall a b, b < a -> a <> b.

Lemma lt_diff2:
forall a b, a < b -> a <> b.

On peut toujours affaiblir safe.

Lemma safe_weak:
forall l p, safe l p -> forall l', l <= l' -> safe l' p.

Difficulté : 0.

Lemma safe_reserved:
forall l p, safe l p -> forall l', l <= l' -> reserved l' p.

Le prédicat sub_program l p p' signifie que p et p' vérifient safe l et que p est obtenu en enlevant des instructions étiquetées de p'.

Inductive sub_program : label -> program -> program -> Prop :=
  | sub_program_refl: forall l p, safe l p -> sub_program l p p
  | sub_program_cons: forall p q l,
       sub_program l p q -> forall l', l' < l ->
       reserved l' q ->
      forall c, sub_program l p ((l', c)::q).

Difficulté : 0.

Lemma sub_program_nil :
forall l p, safe l p -> sub_program l [] p.

Difficulté : 0.

Lemma sub_program_safe_left:
forall l p p', sub_program l p p' -> safe l p.

Difficulté : 0.

Lemma sub_program_safe_right:
forall l p p', sub_program l p p' -> safe l p'.

On peut également affaiblir sub_program.

Difficulté : 0.

Lemma sub_program_weak :
forall l p p', sub_program l p p' -> forall l', l <= l' -> sub_program l' p p'.

Si p est un sous-programme de p' et si l est associée à c dans p, alors elle l'est aussi dans p'.

Difficulté : 1.

Lemma sub_program_lookup:
forall l p p', sub_program l p p' -> forall l' c, lookup p l' c -> lookup p' l' c.

Le prédicat sub_program est transitif.

Difficulté: 0.

Lemma sub_program_trans:
forall l p p', sub_program l p p' -> forall p'',
sub_program l p' p'' -> sub_program l p p''.

Voici une fonction qui pourrait vous donner du fil à retordre: reserve_labels l k retourne un entier supérieur ou égal à l et la différence reserve_labels( l k) - l est le nombre d'étiquettes qu'il va falloir créer pour compiler k.

Fixpoint reserve_labels label k := match k with
  | skip => label
  | seqi k1 k2 => reserve_labels (reserve_labels label k2) k1
  | ass x t => label
  | ifte x k1 k2 =>
      let else_begin := label in
      let if_end := S label in
      let label := 2 + label in
      reserve_labels (reserve_labels label k1) k2
  | while x k =>
      let while_begin := label in
      let while_end := S label in
      let label := S (S label) in
      reserve_labels label k
end.

Vérifier que reserve_labels_grows l k est toujours supérieur à l.

Difficulté : 1.

Lemma reserve_labels_grows:
forall k l, l <= reserve_labels l k.

La procédure de compilation

Les deux fonctions suivantes sont à comprendre ensemble:

compile_program future prg label k retourne un nouveau programme construit à partir de prg. Les nouvelles étiquettes sont comprises entre label et reserve_labels label k.
compile future label k retourne l'instruction qui une fois exécutée dans le programme compile_program future prg label k simulera k.

Fixpoint compile future label k : instr := match k with
  | skip => future
  | seqi k1 k2 =>
      let c2 := compile future label k2 in
      let label := reserve_labels label k2 in
      compile c2 label k1
  | ass x t => compile_term x future t
  | ifte x k1 k2 =>
      let else_begin := label in
      let if_end := S label in
      let label := S (S label) in
      let c1 := compile (jmp if_end) label k1 in
      brz x else_begin;c1
  | while x k =>
      let while_begin := label in
      jmp while_begin
end.

Fixpoint compile_program future prg label k := match k with
  | skip => prg
  | seqi k1 k2 =>
      let c2 := compile future label k2 in
      let prg := compile_program future prg label k2 in
      let label := reserve_labels label k2 in
      compile_program c2 prg label k1
  | ass x t => prg
  | ifte x k1 k2 =>
      let else_begin := label in
      let if_end := S label in
      let label := 2 + label in

      let prg := compile_program (jmp if_end) prg label k1 in
      let label := reserve_labels label k1 in

      let c2 := compile (jmp if_end) label k2 in
      let prg := compile_program (jmp if_end) prg label k2 in
      let label := reserve_labels label k2 in

      (if_end, future)::(else_begin, c2)::prg
  | while x k =>
      let while_begin := label in
      let while_end := S label in
      let label := S (S label) in
      let c := compile (jmp while_begin) label k in
      let prg := compile_program (jmp while_begin) prg label k in
      let label := reserve_labels label k in
      (while_begin, (brz x while_end);c)::(while_end, future)::prg
end.

compile_main k crée un nouveau programme qui commence et se termine par la simulation de k.

Definition compile_main k :=
   let c := compile hlt 1 k in
   let prg := compile_program hlt nil 1 k in
   (0, c)::prg.

Vous pouvez tester la fonction de compilation :

Definition compile_fact :=
Eval compute in (compile_main (fact_test 4)).

Si l'on peut faire un petit pas dans un prg, alors on peut faire le même petit pas dans tout sur-programme.

Difficulté: 1

Lemma weakening_step:
  forall r c r' c' prg, ( r | c ) -- prg --> ( r' | c' ) -> forall prg' l,
         sub_program l prg prg' ->
         (r | c ) -- prg' --> ( r' | c' ).

Pareil, pour la clôture.

Difficulté : 0.

Lemma weakening :
  forall r c r' c' prg, ( r | c ) == prg ==> ( r' | c' ) -> forall l prg',
         sub_program l prg prg' ->
         (r | c ) == prg' ==> ( r' | c' ).

Voici la collection de tous les lemmes bureaucratiques.

Hint Resolve
sub_program_refl sub_program_cons
safe_nil safe_cons lt_diff lt_diff2
safe_weak safe_reserved
sub_program_nil sub_program_safe_left
sub_program_safe_right sub_program_weak
sub_program_trans reserve_labels_grows : bureaucracy.

On définit un alias pour la tactique eauto with bureaucracy arith qui pourrait tenter de résoudre automatiquement tout ce qui concerne les prédicats safe, reserved et sub_program. Nous conseillons de l'utiliser après les tactiques qui génèrent plusieurs buts (avec ";") pour éviter que vos preuves soient interminables.

Ltac bureaucracy := eauto with bureaucracy arith.

Voici un des lemmes les plus difficiles à prouver: il affirme que le programme généré par compile_program future prg l k n'a ajouté à prg que des étiquettes comprises entre label et reserve_labels l k.

Difficulté: 3.

Lemma reserve_labels_sound : forall k l prg, safe l prg -> forall future,
safe (reserve_labels l k) (compile_program future prg l k)
/\ (forall l', l' < l -> reserved l' prg ->
reserved l' (compile_program future prg l k)).

On ajoute les deux lemmes suivants dans la base de données des lemmes bureaucratiques.

Lemma reserve_labels_sound1 : forall k l prg, safe l prg -> forall future,
   safe (reserve_labels l k) (compile_program future prg l k).

Lemma reserve_labels_sound2 : forall k l prg, safe l prg ->
   forall future l', l' < l -> reserved l' prg ->
        reserved l' (compile_program future prg l k).

Hint Resolve reserve_labels_sound1 reserve_labels_sound2 : bureaucracy.

Ce lemme affirme que compile_programe future prg l k est un sur-programme de prg.

Lemma compile_weakening: forall k l prg, safe l prg ->
forall future,
sub_program (reserve_labels l k) prg (compile_program future prg l k).

Voici le lemme qui affirme la correction de la procédure de compilation.

Difficulté: 3.

Lemma compile_sound:
forall r k r', execute r k r' -> forall label future prg, safe label prg ->
( r | compile future label k ) == (compile_program future prg label k) ==> ( r' | future ).

Bravo ! Vous avez certifié votre premier compilateur.

Theorem compile_main_sound:
forall r r' k, execute r k r' ->
r == compile_main k ==> r'.

L'étape ultime: extraire le code caml du fichier coq.

Extraction "compiler.ml" compile_main.