(* *********************************************************************)
(*                                                                     *)
(*              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.
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` *)
  | 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 tso then
            if peq tpc tnot 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.