Branching stub scheduler

3 files changed, 55 insertions, 14 deletions

diff --git a/driver/Compiler.v b/driver/Compiler.v
index 37bb54f7..07889ae5 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -39,7 +39,7 @@ Require Tailcall.
 Require Inlining.
 Require Renumber.
 Require Duplicate.
-Require RTLpath RTLpathLivegen.
+Require RTLpath RTLpathLivegen RTLpathScheduler.
 Require Constprop.
 Require CSE.
 Require ForwardMoves.
@@ -154,6 +154,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 12)
   @@@ time "RTLpath generation" RTLpathLivegen.transf_program
+  @@@ time "RTLpath scheduling" RTLpathScheduler.transf_program
    @@ time "RTL projection" RTLpath.program_RTL
    @@ print (print_RTL 13)
   @@@ time "Register allocation" Allocation.transf_program
@@ -268,6 +269,7 @@ Definition CompCert's_passes :=
   ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog)
   ::: mkpass Unusedglobproof.match_prog
   ::: mkpass RTLpathLivegen.match_prog
+  ::: mkpass RTLpathScheduler.match_prog
   ::: mkpass RTLpath.match_program_RTL
   ::: mkpass Allocproof.match_prog
   ::: mkpass Tunnelingproof.match_prog
@@ -317,8 +319,9 @@ Proof.
   set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *.
   destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate.
   destruct (RTLpathLivegen.transf_program p15) as [p15_1|e] eqn:P15_1; simpl in T; try discriminate.
-  set (p15_2 := RTLpath.program_RTL p15_1) in *.
-  destruct (Allocation.transf_program p15_2) as [p16|e] eqn:P16; simpl in T; try discriminate.
+  destruct (RTLpathScheduler.transf_program p15_1) as [p15_2|e] eqn:P15_2; simpl in T; try discriminate.
+  set (p15_3 := RTLpath.program_RTL p15_2) in *.
+  destruct (Allocation.transf_program p15_3) as [p16|e] eqn:P16; simpl in T; try discriminate.
   set (p17 := Tunneling.tunnel_program p16) in *.
   destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate.
   set (p19 := CleanupLabels.transf_program p18) in *.
@@ -344,7 +347,8 @@ Proof.
   exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match.
   exists p15; split. apply Unusedglobproof.transf_program_match; auto.
   exists p15_1; split. apply RTLpathLivegen.transf_program_match; auto.
-  exists p15_2; split. apply RTLpath.transf_program_match; auto.
+  exists p15_2; split. apply RTLpathScheduler.transf_program_match; auto.
+  exists p15_3; split. apply RTLpath.transf_program_match; auto.
   exists p16; split. apply Allocproof.transf_program_match; auto.
   exists p17; split. apply Tunnelingproof.transf_program_match.
   exists p18; split. apply Linearizeproof.transf_program_match; auto.
@@ -402,7 +406,7 @@ Ltac DestructM :=
       destruct H as (p & M & MM); clear H
   end.
   repeat DestructM. subst tp.
-  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p27)).
+  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p28)).
   {
   eapply compose_forward_simulations.
     eapply SimplExprproof.transl_program_correct; eassumption.
@@ -442,6 +446,8 @@ Ltac DestructM :=
   eapply compose_forward_simulations.
     eapply RTLpathLivegen.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
+    eapply RTLpathScheduler.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
     eapply RTLpath.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply Allocproof.transf_program_correct; eassumption.
diff --git a/mppa_k1c/lib/RTLpathScheduler.v b/mppa_k1c/lib/RTLpathScheduler.v
index 9cdb6f0f..55ee02c6 100644
--- a/mppa_k1c/lib/RTLpathScheduler.v
+++ b/mppa_k1c/lib/RTLpathScheduler.v
@@ -20,11 +20,11 @@ NB: the new RTLpath function is generated from the fn_code, the fn_entrypoint an
 It requires to check that the path structure is wf !
 
 *)
-Axiom untrusted_scheduler: RTLpath.function -> code * node * path_map * (PTree.t node).
+(* Axiom untrusted_scheduler: RTLpath.function -> code * node * path_map * (PTree.t node). *)
 
-(*
-Extract Constant untrusted_scheduler => "TODO".
-*)
+Axiom untrusted_scheduler: RTLpath.function -> code * (PTree.t node).
+
+Extract Constant untrusted_scheduler => "RTLpathScheduleraux.scheduler".
 
 Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop := {
   preserv_fnsig: fn_sig f1 = fn_sig f2;
@@ -36,8 +36,30 @@ Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop :=
   dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> sstep_simu dupmap f1 f2 pc1 pc2
 }.
 
-(* TODO: remove these two stub parameters *)
-Parameter transf_function: RTLpath.function -> res RTLpath.function.
+(* TODO - perform appropriate checks on tc and dupmap *)
+Definition verified_scheduler (f: RTLpath.function) : res (code * (PTree.t node)) :=
+  let (tc, dupmap) := untrusted_scheduler f in OK (tc, dupmap).
+
+Lemma verified_scheduler_wellformed_pm f tc pm dm:
+  fn_path f = pm ->
+  verified_scheduler f = OK (tc, dm) ->
+  wellformed_path_map tc pm.
+Proof.
+Admitted.
+
+Program Definition transf_function (f: RTLpath.function): res RTLpath.function :=
+  match (verified_scheduler f) with
+  | Error e => Error e
+  | OK (tc, dupmap) => 
+      let rtl_tf := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc (fn_entrypoint f) in
+      OK {| fn_RTL := rtl_tf; fn_path := (fn_path f) |}
+  end.
+Next Obligation.
+  destruct f as [rtl_f pm EP_WF PATH_WF]. assumption.
+Qed. Next Obligation.
+  destruct f as [rtl_f pm EP_WF PATH_WF]. simpl.
+  eapply verified_scheduler_wellformed_pm; eauto. simpl. reflexivity.
+Qed.
 
 Parameter transf_function_correct: 
  forall f f', transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
@@ -58,7 +80,6 @@ Definition transf_fundef (f: fundef) : res fundef :=
 Definition transf_program (p: program) : res program :=
   transform_partial_program transf_fundef p.
 
-
 (** * Preservation proof *)
 
 Local Notation ext alive := (fun r => Regset.In r alive).
@@ -186,8 +207,11 @@ Hypothesis TRANSL: match_prog prog tprog.
 Let pge := Genv.globalenv prog.
 Let tpge := Genv.globalenv tprog.
 
-Hypothesis all_fundef_liveness_ok: forall b fd,
+(* Was a Hypothesis *)
+Theorem all_fundef_liveness_ok: forall b fd,
   Genv.find_funct_ptr pge b = Some fd -> liveness_ok_fundef fd.
+Proof.
+Admitted.
 
 Lemma symbols_preserved s: Genv.find_symbol tpge s = Genv.find_symbol pge s.
 Proof.
@@ -250,6 +274,7 @@ Proof.
   - constructor; eauto.
     + constructor.
     + apply transf_fundef_correct; auto.
+    + eapply all_fundef_liveness_ok; eauto.
 Qed.
 
 Theorem transf_final_states s1 s2 r:
@@ -305,9 +330,11 @@ Proof.
     intros; exploit functions_preserved; eauto.
     intros (fd' & cunit & X). eexists. intuition eauto.
     eapply find_funct_liveness_ok; eauto.
+    intros. eapply all_fundef_liveness_ok; eauto.
   + rewrite symbols_preserved. destruct (Genv.find_symbol _ _); try congruence.
     intros; exploit function_ptr_preserved; eauto.
     intros (fd' & X). eexists. intuition eauto.
+    intros. eapply all_fundef_liveness_ok; eauto.
 Qed.
 
 Lemma sistate_simu f dupmap sp st st' rs m is:
@@ -421,7 +448,7 @@ Proof.
   destruct 1 as [path stack f sp rs m pc t s PATH STEP | | | ]; intros MS; inv MS.
 (* exec_path *)
   - try_simplify_someHyps. intros.
-    exploit path_step_eqlive; eauto.
+    exploit path_step_eqlive; eauto. { intros. eapply all_fundef_liveness_ok; eauto. }
     clear STEP EQUIV rs; intros (s2 & STEP & EQLIVE).
     exploit exec_path_simulation; eauto.
     clear STEP; intros (path' & s' & PATH' & STEP' & MATCH').
diff --git a/mppa_k1c/lib/RTLpathScheduleraux.ml b/mppa_k1c/lib/RTLpathScheduleraux.ml
new file mode 100644
index 00000000..1017cf63
--- /dev/null
+++ b/mppa_k1c/lib/RTLpathScheduleraux.ml
@@ -0,0 +1,8 @@
+open RTLpath
+open RTL
+open Maps
+
+let scheduler f =
+  let code = f.fn_RTL.fn_code in
+  let id_ptree = PTree.map (fun n i -> n) code in
+  (code, id_ptree)