Write RTLTunneling.v

1 files changed, 125 insertions, 0 deletions

diff --git a/backend/RTLTunneling.v b/backend/RTLTunneling.v
index e69de29b..4885002f 100644
--- a/backend/RTLTunneling.v
+++ b/backend/RTLTunneling.v
@@ -0,0 +1,125 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*          TODO: Proper author information                            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** 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.
+
+(* This is a port of tunneling for LTL. See Tunneling.v *)
+
+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.
+(* 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` *)
+  | 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`} *)
+  | Some (tpc, dpc) =>
+      let dpc := Z.abs dpc in
+      match i with
+      | Inop s =>
+          let (ts,ds) := get td s in
+          if peq tpc ts then
+            if zlt ds dpc then OK tt
+            else Error (msg "bad distance in Inop")
+          else Error (msg "invalid skip of Inop")
+      | Icond _ _ ifso ifnot _ =>
+          let (tso,dso) := get td ifso in
+          let (tnot,dnot) := get td ifnot in
+          if peq tpc ifso then
+            if peq tpc ifnot then
+              if zlt dso dpc then
+                if zlt dnot dpc then OK tt
+                else Error (msg "bad distance on else branch")
+              else Error (msg "bad distance on then branch")
+            else Error (msg "invalid skip of else branch")
+          else Error (msg "invalid skip of then branch")
+      | _ => Error (msg "cannot skip this instruction")
+      end
+  end.
+
+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)
+  | Iop op args res s => Iop op args res (t s)
+  | Iload trap chunk addr args dst s => Iload trap chunk addr args dst (t s)
+  | Istore chunk addr args src s => Istore chunk addr args src (t s)
+  | Icall sig ros args res s => Icall sig ros args res (t s)
+  | Ibuiltin ef args res s => Ibuiltin ef args res (t s)
+  | Icond cond args ifso ifnot info =>
+      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)
+  | _ => i
+  end.
+
+Definition tunnel_function (f: RTL.function): res RTL.function :=
+  let td := branch_target f in
+  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` *)
+      (fn_sig f)
+      (fn_params f)
+      (fn_stacksize f)
+      (PTree.map1 (tunnel_instr td) c) (* rq: `map1` est un map sans le pointeur *)
+      (td (fn_entrypoint f)))
+  else Error (msg "Some node of the union-find is not in the CFG").
+
+Definition tunnel_fundef (f: fundef): res fundef :=
+  transf_partial_fundef tunnel_function f.
+
+Definition transf_program (p: program): res program :=
+  transform_partial_program tunnel_fundef p.
+