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, 20 insertions, 10 deletions

diff --git a/backend/PPCgen.v b/backend/PPCgen.v
index ba8ea285..d7a83b0b 100644
--- a/backend/PPCgen.v
+++ b/backend/PPCgen.v
@@ -2,6 +2,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Import Errors.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -268,11 +269,6 @@ Definition transl_op
       Pori (ireg_of r) (ireg_of r) (Csymbol_low_unsigned s ofs) :: k
   | Oaddrstack n, nil =>
       addimm (ireg_of r) GPR1 n k
-  | Oundef, nil =>
-      match mreg_type r with
-      | Tint => Piundef (ireg_of r) :: k
-      | Tfloat => Pfundef (freg_of r) :: k
-      end
   | Ocast8signed, a1 :: nil =>
       Pextsb (ireg_of r) (ireg_of a1) :: k
   | Ocast8unsigned, a1 :: nil =>
@@ -474,6 +470,17 @@ Definition transl_instr (i: Mach.instruction) (k: code) :=
       Pmtctr (ireg_of r) :: Pbctrl :: k
   | Mcall sig (inr symb) =>
       Pbl symb :: k
+  | Mtailcall sig (inl r) =>
+      Pmtctr (ireg_of r) :: 
+      Plwz GPR2 (Cint (Int.repr 12)) GPR1 ::
+      Pmtlr GPR2 ::
+      Pfreeframe :: 
+      Pbctr :: k
+  | Mtailcall sig (inr symb) =>
+      Plwz GPR2 (Cint (Int.repr 12)) GPR1 ::
+      Pmtlr GPR2 ::
+      Pfreeframe :: 
+      Pbs symb :: k
   | Malloc =>
       Pallocblock :: k
   | Mlabel lbl =>
@@ -510,14 +517,17 @@ Fixpoint code_size (c: code) : Z :=
   | instr :: c' => code_size c' + 1
   end.
 
-Definition transf_function (f: Mach.function) : option PPC.code :=
+Open Local Scope string_scope.
+
+Definition transf_function (f: Mach.function) : res PPC.code :=
   let c := transl_function f in
   if zlt Int.max_unsigned (code_size c)
-  then None
-  else Some c.
+  then Errors.Error (msg "code size exceeded")
+  else Errors.OK c.
 
-Definition transf_fundef (f: Mach.fundef) : option PPC.fundef :=
+Definition transf_fundef (f: Mach.fundef) : res PPC.fundef :=
   transf_partial_fundef transf_function f.
 
-Definition transf_program (p: Mach.program) : option PPC.program :=
+Definition transf_program (p: Mach.program) : res PPC.program :=
   transform_partial_program transf_fundef p.
+