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, 32 insertions, 26 deletions

diff --git a/backend/Constprop.v b/backend/Constprop.v
index d34c6ee..fecfb19 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -632,6 +632,8 @@ Definition transfer (f: function) (pc: node) (before: D.t) :=
           before
       | Icall sig ros args res s =>
           D.set res Unknown before
+      | Itailcall sig ros args =>
+          before
       | Ialloc arg res s =>
           D.set res Unknown before
       | Icond cond args ifso ifnot =>
@@ -649,9 +651,12 @@ Definition transfer (f: function) (pc: node) (before: D.t) :=
 
 Module DS := Dataflow_Solver(D)(NodeSetForward).
 
-Definition analyze (f: RTL.function): option (PMap.t D.t) :=
-  DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) 
-              ((f.(fn_entrypoint), D.top) :: nil).
+Definition analyze (f: RTL.function): PMap.t D.t :=
+  match DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) 
+                    ((f.(fn_entrypoint), D.top) :: nil) with
+  | None => PMap.init D.top
+  | Some res => res
+  end.
 
 (** * Code transformation *)
 
@@ -986,6 +991,16 @@ End STRENGTH_REDUCTION.
     and similarly for the addressing modes of load and store instructions.
     Other instructions are unchanged. *)
 
+Definition transf_ros (approx: D.t) (ros: reg + ident) : reg + ident :=
+  match ros with
+  | inl r =>
+      match D.get r approx with
+      | S symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros
+      | _ => ros
+      end
+  | inr s => ros
+  end.
+
 Definition transf_instr (approx: D.t) (instr: instruction) :=
   match instr with
   | Iop op args res s =>
@@ -1007,16 +1022,9 @@ Definition transf_instr (approx: D.t) (instr: instruction) :=
       let (addr', args') := addr_strength_reduction approx addr args in
       Istore chunk addr' args' src s      
   | Icall sig ros args res s =>
-      let ros' :=
-        match ros with
-        | inl r =>
-            match D.get r approx with
-            | S symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros
-            | _ => ros
-            end
-        | inr s => ros
-        end in
-      Icall sig ros' args res s
+      Icall sig (transf_ros approx ros) args res s
+  | Itailcall sig ros args =>
+      Itailcall sig (transf_ros approx ros) args
   | Ialloc arg res s =>
       Ialloc arg res s
   | Icond cond args s1 s2 =>
@@ -1048,20 +1056,18 @@ Proof.
 Qed.
 
 Definition transf_function (f: function) : function :=
-  match analyze f with
-  | None => f
-  | Some approxs =>
-      mkfunction
-        f.(fn_sig)
-        f.(fn_params)
-        f.(fn_stacksize)
-        (transf_code approxs f.(fn_code))
-        f.(fn_entrypoint)
-        f.(fn_nextpc)
-        (transf_code_wf f approxs f.(fn_code_wf))
-  end.
+  let approxs := analyze f in
+  mkfunction
+    f.(fn_sig)
+    f.(fn_params)
+    f.(fn_stacksize)
+    (transf_code approxs f.(fn_code))
+    f.(fn_entrypoint)
+    f.(fn_nextpc)
+    (transf_code_wf f approxs f.(fn_code_wf)).
 
-Definition transf_fundef := AST.transf_fundef transf_function.
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
 
 Definition transf_program (p: program) : program :=
   transform_program transf_fundef p.