Merge remote-tracking branch 'origin/kvx-work' into kvx-work

5 files changed, 24 insertions, 89 deletions

diff --git a/backend/LTLTunnelingaux.ml b/backend/LTLTunnelingaux.ml
index c3b8cf82..66540bc1 100644
--- a/backend/LTLTunnelingaux.ml
+++ b/backend/LTLTunnelingaux.ml
@@ -3,6 +3,7 @@
 (*             The Compcert verified compiler                  *)
 (*                                                             *)
 (*           Sylvain Boulmé  Grenoble-INP, VERIMAG             *)
+(*           Pierre Goutagny ENS-Lyon, VERIMAG                 *)
 (*                                                             *)
 (*  Copyright VERIMAG. All rights reserved.                    *)
 (*  This file is distributed under the terms of the INRIA      *)
diff --git a/backend/RTLTunneling.v b/backend/RTLTunneling.v
index df663f48..878e079f 100644
--- a/backend/RTLTunneling.v
+++ b/backend/RTLTunneling.v
@@ -3,7 +3,8 @@
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
 (*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*          TODO: Proper author information                            *)
+(*          Sylvain Boulmé  Grenoble-INP, VERIMAG                      *)
+(*          Pierre Goutagny ENS-Lyon, VERIMAG                          *)
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
@@ -13,8 +14,6 @@
 
 (** Branch tunneling for the RTL representation *)
 
-(* rq: ce code est commenté avec des remarques sur des éléments du code pas évidents, sur lequels j'ai buté, ou qui changent du tunneling LTL. Ils pourront être enlevés ultérieurement *)
-
 Require Import Coqlib Maps Errors.
 Require Import AST.
 Require Import RTL.
@@ -26,32 +25,30 @@ Definition UF := PTree.t (node * Z).
 (* The oracle returns a map of "nop" node to their target with a distance (ie the number of the "nop" node on the path) to the target. *)
 Axiom branch_target: RTL.function -> UF.
 Extract Constant branch_target => "RTLTunnelingaux.branch_target".
-(* TODO: add an extraction command to link branch_target with its implementation *)
 
 Local Open Scope error_monad_scope.
 
 Definition get (td: UF) (pc: node): node*Z :=
-  match td!pc with (* rq: notation pour `PTree.get pc td` *)
+  match td!pc with 
   | Some (t,d) => (t,Z.abs d)
   | None       => (pc,0)
   end.
 
-(* rq: "coerce" la structure d'abre UF en une fonction qui retrouve le représentant canonique de la classe d'un noeud *)
+
 Definition target (td: UF) (pc: node): node := fst (get td pc).
 Coercion target: UF >-> Funclass.
 
 (* we check that the domain of [td] is included in the domain of [c] *)
-(* rq: pas de basic block en RTL *)
+
 Definition check_included (td: UF) (c: code): option instruction
   := PTree.fold (fun (ok:option instruction) pc _ => if ok then c!pc else None) td (Some (Inop xH)).
-(* rq: PTree.fold replie l'arbre avec un parcours préfixe. La fonction qui prend en argument l'accumulateur, le label du noeud et le pointeur (`positive`) vers ce noeud *)
 
 (* we check the validity of targets and their bound:
 *  the distance of a "nop" node (w.r.t to the target) must be greater than the one of its parents.
 *)
 Definition check_instr (td: UF) (pc: node) (i: instruction): res unit :=
   match td!pc with
-  | None => OK tt (* rq: le type `unit` est le singleton {`tt`} *)
+  | None => OK tt 
   | Some (tpc, dpc) =>
       let dpc := Z.abs dpc in
       match i with
@@ -78,14 +75,12 @@ Definition check_instr (td: UF) (pc: node) (i: instruction): res unit :=
 
 Definition check_code (td: UF) (c: code): res unit :=
   PTree.fold (fun ok pc i => do _ <- ok; check_instr td pc i) c (OK tt).
-(* rq: `do _ <- ok; ...` exécute le bloc à droite du ';' si `ok` est un `OK _`, sinon il passe simplement l'erreur *)
 
 (* The second pass rewrites all LTL instructions, replacing every
  * successor [s] of every instruction by [t s], the canonical representative
  * of its equivalence class in the union-find data structure.
  *)
 
-(* rq: beaucoup plus de cas que pour LTL, car plein d'instructions ont des successeurs *)
 Definition tunnel_instr (t: node -> node) (i: instruction) : instruction :=
   match i with
   | Inop s => Inop (t s)
@@ -98,7 +93,7 @@ Definition tunnel_instr (t: node -> node) (i: instruction) : instruction :=
       let ifso'  := t ifso in
       let ifnot' := t ifnot in
       if peq ifso' ifnot'
-      (* rq: si les deux branches se rejoignent, le if ne sert à rien *)
+      
       then Inop ifso'
       else Icond cond args ifso' ifnot' info
   | Ijumptable arg tbl => Ijumptable arg (List.map t tbl)
@@ -110,11 +105,11 @@ Definition tunnel_function (f: RTL.function): res RTL.function :=
   let c := fn_code f in
   if check_included td c then
     do _ <- check_code td c ; OK
-    (mkfunction (* rq: mkfunction construit un "Record" `RTL.function` *)
+    (mkfunction
       (fn_sig f)
       (fn_params f)
       (fn_stacksize f)
-      (PTree.map1 (tunnel_instr td) c) (* rq: `map1` est un map sans le pointeur *)
+      (PTree.map1 (tunnel_instr td) c)
       (td (fn_entrypoint f)))
   else Error (msg "Some node of the union-find is not in the CFG").
 
diff --git a/backend/RTLTunnelingaux.ml b/backend/RTLTunnelingaux.ml
index 9333e357..43d4bf9f 100644
--- a/backend/RTLTunnelingaux.ml
+++ b/backend/RTLTunnelingaux.ml
@@ -3,7 +3,7 @@
 (*             The Compcert verified compiler                  *)
 (*                                                             *)
 (*           Sylvain Boulmé  Grenoble-INP, VERIMAG             *)
-(*           TODO: Proper author information                   *)
+(*           Pierre Goutagny ENS-Lyon, VERIMAG                 *)
 (*                                                             *)
 (*  Copyright VERIMAG. All rights reserved.                    *)
 (*  This file is distributed under the terms of the INRIA      *)
diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v
index 51ef0f7a..0861143b 100644
--- a/backend/RTLTunnelingproof.v
+++ b/backend/RTLTunnelingproof.v
@@ -3,7 +3,8 @@
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
 (*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*          TODO: Proper author information                            *)
+(*          Sylvain Boulmé  Grenoble-INP, VERIMAG                      *)
+(*          Pierre Goutagny ENS-Lyon, VERIMAG                          *)
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
@@ -23,7 +24,7 @@ Require Import Conventions1.
 
 Local Open Scope nat.
 
-(**) Definition check_included_spec (c:code) (td:UF) (ok: option instruction) :=
+Definition check_included_spec (c:code) (td:UF) (ok: option instruction) :=
   ok <> None -> forall pc, c!pc = None -> td!pc = None.
 
 Lemma check_included_correct (td:UF) (c:code):
@@ -37,7 +38,7 @@ Proof.
     + contradiction.
 Qed.
 
-(**) Inductive target_bounds (target: node -> node) (bound: node -> nat) (pc: node) : option instruction -> Prop :=
+Inductive target_bounds (target: node -> node) (bound: node -> nat) (pc: node) : option instruction -> Prop :=
   | TB_default (TB: target pc = pc) oi:
       target_bounds target bound pc oi
   | TB_nop s
@@ -65,7 +66,7 @@ Proof.
 Qed.
 Local Hint Resolve get_nonneg: core.
 
-(**) Definition bound (td: UF) (pc: node) := Z.to_nat (snd (get td pc)).
+Definition bound (td: UF) (pc: node) := Z.to_nat (snd (get td pc)).
 
 
 (* TODO: à réécrire proprement *)
@@ -117,18 +118,6 @@ Theorem branch_target_bounds:
   tunnel_function f = OK tf ->
   target_bounds (branch_target f) (bound (branch_target f)) pc (f.(fn_code)!pc).
 Proof.
-(* ~old
-  intros t tf pc. unfold tunnel_function.
-  destruct (check_included _ _) eqn:HI; try congruence.
-  destruct (check_code _ _) eqn: HC.
-  - intros _. destruct ((fn_code t) ! pc) eqn:EQ.
-    + exploit check_code_correct; eauto.
-    replace tt with u. auto. {destruct u; auto. }
-    + exploit check_included_correct; eauto. rewrite HI. congruence.
-    intro. apply TB_default. unfold target. unfold get. rewrite H. debug auto.
-  - simpl. congruence.
-*)
-
   intros. unfold tunnel_function in H.
   destruct (check_included _ _) eqn:EQinc; try congruence.
   monadInv H. rename EQ into EQcode.
@@ -144,12 +133,8 @@ Qed.
 
 Definition match_prog (p tp: program) :=
   match_program (fun _ f tf => tunnel_fundef f = OK tf) eq p tp.
-  (* rq: `(fun _ ...)` est la fonction pour matcher des fonctions
-   *     `eq` la fonction pour matcher les variables ? (`varinfo` dans la def)
-   *     `p` et `tp` sont les programmes donc on doit dire s'ils match
-   *)
 
- (**) Lemma transf_program_match:
+Lemma transf_program_match:
   forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
 Proof.
   intros. eapply match_transform_partial_program_contextual; eauto.
@@ -160,12 +145,10 @@ Section PRESERVATION.
 
 
 Variables prog tprog: program.
-Hypothesis TRANSL: match_prog prog tprog. (* rq: on suppose que les programmes match *)
+Hypothesis TRANSL: match_prog prog tprog.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
-(* rq: pour les deux lemmes suivants, j'ai recopié les preuves, mais je ne les comprends pas du tout... D'où vient `exploit` ?? *)
-(* rq: `exploit` vient de Coqlib! Mais je comprends pas encore vraiment ce qui se passe... *)
 Lemma functions_translated:
   forall (v: val) (f: fundef),
   Genv.find_funct ge v = Some f ->
@@ -174,12 +157,7 @@ Proof.
   intros.
   exploit (Genv.find_funct_match TRANSL). apply H.
   intros (cu & tf & A & B & C).
-  (* exists tf. split. apply B. apply A. *)
-  (* rq: on peut remplacer les `split` et `apply` par `eauto`, et ne pas spécifier le
-   * `exists`, avec un `eexists` *)
   eexists. eauto.
-  (* rq: Je ne comprends pas à quoi sert le `intuition`... *)
-  (* repeat eexists; intuition eauto. *)
 Qed.
 
 Lemma function_ptr_translated:
@@ -196,25 +174,13 @@ Qed.
 Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
 Proof.
   apply (Genv.find_symbol_match TRANSL).
-  (* rq: ici pas de `exploit` mais un `apply` parce que `Genv.find_symbol_match
-   * prouve vraiment pile ce qu'on veut *)
 Qed.
 
 Lemma sig_preserved:
   forall f tf, tunnel_fundef f = OK tf -> funsig tf = funsig f.
 Proof.
   intros. destruct f; simpl in H.
-  -
-    (*
-    unfold bind in H.
-    destruct (tunnel_function _) as [x|] eqn:EQ; try congruence.
-    inversion H.
-    unfold tunnel_function in EQ.
-    destruct (check_included _ _) in EQ; try congruence.
-    unfold bind in EQ. destruct (check_code _ _) in EQ; try congruence. inversion EQ. auto.
-    *)
-
-    monadInv H. (* rq: c'est une tactique maison... *)
+  - monadInv H.
     unfold tunnel_function in EQ.
     destruct (check_included _ _) in EQ; try congruence.
     monadInv EQ. auto.
@@ -227,7 +193,6 @@ Proof.
   eapply (Genv.senv_match TRANSL). (* Il y a déjà une preuve de cette propriété très exactement, je ne vais pas réinventer la roue ici *)
 Qed.
 
-(* TODO: vérifier s'il faut faire quelque chose avec le `res` ? *)
 Inductive match_stackframes: stackframe -> stackframe -> Prop :=
   | match_stackframes_intro:
       forall res f tf sp pc rs trs
@@ -237,7 +202,6 @@ Inductive match_stackframes: stackframe -> stackframe -> Prop :=
         (Stackframe res f sp pc rs)
         (Stackframe res tf sp (branch_target f pc) trs).
 
-(* rq: `match_states s1 s2` correspond à s1 ~ s2 *)
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
       forall s ts f tf sp pc rs trs m tm
@@ -266,24 +230,6 @@ Inductive match_states: state -> state -> Prop :=
         (Returnstate s v m)
         (Returnstate ts tv tm).
 
-(* TODO: il faut définir une bonne mesure *)
-(* (**) Definition measure (st: state) : nat :=
-  match st with
-  | State s f sp pc rs m =>
-      match (fn_code f)!pc with
-      | Some (Inop pc') => (bound (branch_target f) pc') * 2 + 1
-      | Some (Icond _ _ ifso ifnot _) => (max
-                                    (bound (branch_target f) ifso)
-                                    (bound (branch_target f) ifnot)
-                                  ) * 2 + 1
-      | Some _ => (bound (branch_target f) pc) * 2
-      | None => 0
-      end
-  | Callstate s f v m => 0
-  | Returnstate s v m => 0
-  end.
-*)
-
 Definition measure (st: state): nat :=
   match st with
   | State s f sp pc rs m => bound (branch_target f) pc
@@ -292,9 +238,7 @@ Definition measure (st: state): nat :=
   end.
 
 
-(* rq: sans les lemmes définis au-dessus je ne vois pas trop comment j'aurais
- * fait... ni comment j'aurais eu l'idée d'en faire des lemmes ? *)
-(**) Lemma transf_initial_states:
+Lemma transf_initial_states:
   forall s1: state, initial_state prog s1 ->
   exists s2: state, initial_state tprog s2 /\ match_states s1 s2.
 Proof.
@@ -316,15 +260,13 @@ Proof.
       * apply Mem.extends_refl.
 Qed.
 
-(**) Lemma transf_final_states:
+Lemma transf_final_states:
   forall (s1 : state)
   (s2 : state) (r : Integers.Int.int),
   match_states s1 s2 ->
   final_state s1 r ->
   final_state s2 r.
 Proof.
-  (* rq: `inv` au lieu de `inversion` fait beaucoup de nettoyage dans les
-   * hypothèses, mais je sais pas trop ce que ça fait exactement *)
   intros. inv H0. inv H. inv VAL. inversion STK. apply final_state_intro.
 Qed.
 
@@ -366,8 +308,7 @@ Proof.
   intro TB. inversion TB as [BT|s|cond args ifso ifnot info]; try (rewrite FATPC in H; congruence).
 Qed.
 
-(* rq: utilisée pour `tunnel_step_correct` mais je ne comprends pas tout *)
-(**) Lemma find_function_translated:
+Lemma find_function_translated:
   forall ros rs trs fd,
   regs_lessdef rs trs ->
   find_function ge ros rs = Some fd ->
@@ -484,8 +425,6 @@ Proof.
   intros args ta H. induction H. apply Val.lessdef_list_nil. apply Val.lessdef_list_cons. apply H. apply IHlist_forall2.
 Qed.
 
-
-(* `Lemma tunnel_step_correct` correspond au diagramme "option simulation" *)
 Lemma tunnel_step_correct:
   forall st1 t st2, step ge st1 t st2 ->
   forall st1' (MS: match_states st1 st1'),
diff --git a/backend/Tunnelinglibs.ml b/backend/Tunnelinglibs.ml
index 7c826ba4..010595be 100644
--- a/backend/Tunnelinglibs.ml
+++ b/backend/Tunnelinglibs.ml
@@ -3,7 +3,7 @@
 (*             The Compcert verified compiler                  *)
 (*                                                             *)
 (*           Sylvain Boulmé  Grenoble-INP, VERIMAG             *)
-(*           TODO: Proper author information                   *)
+(*           Pierre Goutagny ENS-Lyon, VERIMAG                 *)
 (*                                                             *)
 (*  Copyright VERIMAG. All rights reserved.                    *)
 (*  This file is distributed under the terms of the INRIA      *)
@@ -16,7 +16,7 @@
 This file implements the core functions of the tunneling passes, for both RTL
 and LTL, by using a simplified CFG as a transparent interface
 
-See [LTLTunneling.v] and [RTLTunneling.v]
+See [LTLTunneling.v]/[LTLTunnelingaux.ml] and [RTLTunneling.v]/[RTLTunnelingaux.ml].
 
 *)