Fusion des modifications faites sur les branches "tailcalls" et "smallstep".

En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 28 insertions, 28 deletions

diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index 4fbdc9f..15f4676 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -30,8 +30,8 @@ Require Import LTL.
   dead code (as the "goto L3" in the example above).
 *)
 
-Definition is_goto_block (b: option block) : option node :=
-  match b with Some (Bgoto s) => Some s | _ => None end.
+Definition is_goto_instr (b: option instruction) : option node :=
+  match b with Some (Lnop s) => Some s | _ => None end.
 
 (** [branch_target f pc] returns the node of the CFG that is at
   the end of the branch sequence starting at [pc].  If the instruction
@@ -70,7 +70,7 @@ Fixpoint branch_target_rec (f: LTL.function) (pc: node) (count: nat)
   match count with
   | Datatypes.O => None
   | Datatypes.S count' =>
-      match is_goto_block f.(fn_code)!pc with
+      match is_goto_instr f.(fn_code)!pc with
       | Some s => branch_target_rec f s count'
       | None => Some pc
       end
@@ -86,34 +86,32 @@ Definition branch_target (f: LTL.function) (pc: node) :=
   replacing the destinations of the [Bgoto] and [Bcond] instructions
   with their final target, as computed by [branch_target]. *)
 
-Fixpoint tunnel_block (f: LTL.function) (b: block) {struct b} : block :=
+Definition tunnel_instr (f: LTL.function) (b: instruction) : instruction :=
   match b with
-  | Bgetstack s r b =>
-      Bgetstack s r (tunnel_block f b)
-  | Bsetstack r s b =>
-      Bsetstack r s (tunnel_block f b)
-  | Bop op args res b =>
-      Bop op args res (tunnel_block f b)
-  | Bload chunk addr args dst b =>
-      Bload chunk addr args dst (tunnel_block f b)
-  | Bstore chunk addr args src b =>
-      Bstore chunk addr args src (tunnel_block f b)
-  | Bcall sig ros b =>
-      Bcall sig ros (tunnel_block f b)
-  | Balloc b =>
-      Balloc (tunnel_block f b)
-  | Bgoto s =>
-      Bgoto (branch_target f s)
-  | Bcond cond args s1 s2 =>
-      Bcond cond args (branch_target f s1) (branch_target f s2)
-  | Breturn =>
-      Breturn
+  | Lnop s =>
+      Lnop (branch_target f s)
+  | Lop op args res s =>
+      Lop op args res (branch_target f s)
+  | Lload chunk addr args dst s =>
+      Lload chunk addr args dst (branch_target f s)
+  | Lstore chunk addr args src s =>
+      Lstore chunk addr args src (branch_target f s)
+  | Lcall sig ros args res s =>
+      Lcall sig ros args res (branch_target f s)
+  | Ltailcall sig ros args =>
+      Ltailcall sig ros args
+  | Lalloc arg res s =>
+      Lalloc arg res (branch_target f s)
+  | Lcond cond args s1 s2 =>
+      Lcond cond args (branch_target f s1) (branch_target f s2)
+  | Lreturn or =>
+      Lreturn or
   end.
 
 Lemma wf_tunneled_code:
   forall (f: LTL.function),
-  let tc := PTree.map (fun pc b => tunnel_block f b) (fn_code f) in
-  forall (pc: node), Plt pc (Psucc (fn_entrypoint f)) \/ tc!pc = None.
+  let tc := PTree.map (fun pc b => tunnel_instr f b) (fn_code f) in
+  forall (pc: node), Plt pc (fn_nextpc f) \/ tc!pc = None.
 Proof.
   intros. elim (fn_code_wf f pc); intro.
   left; auto. right; unfold tc.
@@ -123,9 +121,11 @@ Qed.
 Definition tunnel_function (f: LTL.function) : LTL.function :=
   mkfunction
     (fn_sig f)
+    (fn_params f)
     (fn_stacksize f)
-    (PTree.map (fun pc b => tunnel_block f b) (fn_code f))
-    (fn_entrypoint f)
+    (PTree.map (fun pc b => tunnel_instr f b) (fn_code f))
+    (branch_target f (fn_entrypoint f))
+    (fn_nextpc f)
     (wf_tunneled_code f).
 
 Definition tunnel_fundef (f: LTL.fundef) : LTL.fundef :=