From 74901c6df6ceb92da58ef5db2592fc05561dce01 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Tue, 24 Aug 2021 11:35:58 +0200
Subject: RTLTunneling: fix comments and authors information

---
 backend/RTLTunneling.v | 23 +++++++++--------------
 1 file changed, 9 insertions(+), 14 deletions(-)

(limited to 'backend/RTLTunneling.v')

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").
 
-- 
cgit