Added a simple postpass oracle that splits a bblock into single instruction bundles

5 files changed, 32 insertions, 4 deletions

diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 3209163f..47284e4b 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -448,6 +448,7 @@ let expand_instruction instr =
         let extra_sz = if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize) in
         let full_sz = Z.add sz (Z.of_uint extra_sz) in
         expand_addptrofs Asmblock.GPR12 Asmblock.GPR12 (Ptrofs.repr (Z.neg full_sz));
+        emit Psemi;
         expand_storeind_ptr Asmblock.GPR14 Asmblock.GPR12 ofs;
         let va_ofs =
             sz in
@@ -456,6 +457,7 @@ let expand_instruction instr =
         save_arguments n va_ofs
       end else begin
         expand_addptrofs Asmblock.GPR12 Asmblock.GPR12 (Ptrofs.repr (Z.neg sz));
+        emit Psemi;
         expand_storeind_ptr Asmblock.GPR14 Asmblock.GPR12 ofs;
         vararg_start_ofs := None
       end
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 6f61747f..58e80be1 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -17,6 +17,7 @@
 
 Require Import Integers.
 Require Import Mach Asm Asmblock Asmblockgen Machblockgen.
+Require Import PostpassScheduling.
 Require Import Errors.
 
 Local Open Scope error_monad_scope.
@@ -24,7 +25,8 @@ Local Open Scope error_monad_scope.
 Definition transf_program (p: Mach.program) : res Asm.program :=
   let mbp := Machblockgen.transf_program p in
   do abp <- Asmblockgen.transf_program mbp;
-  OK (Asm.transf_program abp).
+  do abp' <- PostpassScheduling.transf_program abp;
+  OK (Asm.transf_program abp').
 
 Definition transf_function (f: Mach.function) : res Asm.function :=
   let mbf := Machblockgen.transf_function f in
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 8eb0b693..588019a2 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -16,13 +16,14 @@ Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Mach Conventions Asm Asmgen Machblockgen Asmblockgen.
-Require Import Machblockgenproof Asmblockgenproof.
+Require Import Machblockgenproof Asmblockgenproof PostpassSchedulingproof.
 
 Local Open Scope linking_scope.
 
 Definition block_passes :=
       mkpass Machblockgenproof.match_prog
   ::: mkpass Asmblockgenproof.match_prog
+  ::: mkpass PostpassSchedulingproof.match_prog
   ::: mkpass Asm.match_prog
   ::: pass_nil _.
 
@@ -33,10 +34,12 @@ Lemma transf_program_match:
 Proof.
   intros p tp H.
   unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
-  inversion_clear H. inversion H1. remember (Machblockgen.transf_program p) as mbp.
+  inversion_clear H. apply bind_inversion in H1. destruct H1.
+  inversion_clear H. inversion H2. remember (Machblockgen.transf_program p) as mbp.
   unfold match_prog; simpl.
   exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
   exists x; split. apply Asmblockgenproof.transf_program_match; auto.
+  exists x0; split. apply PostpassSchedulingproof.transf_program_match; auto.
   exists tp; split. apply Asm.transf_program_match; auto. auto.
 Qed.
 
@@ -147,12 +150,13 @@ Theorem transf_program_correct:
   forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
 Proof.
   unfold match_prog in TRANSF. simpl in TRANSF.
-  inv TRANSF. inv H. inv H1. inv H. inv H2. inv H.
+  inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H.
   eapply compose_forward_simulations. 
   exploit Machblockgenproof.transf_program_correct; eauto.
   unfold Machblockgenproof.inv_trans_rao. 
   intros X; apply X.
   eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
+  eapply compose_forward_simulations. apply PostpassSchedulingproof.transf_program_correct; eauto.
   apply Asm.transf_program_correct. eauto.
 Qed.
 
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index 5232f903..1483a5d7 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -19,6 +19,8 @@ Local Open Scope error_monad_scope.
     returns a schedule expressed as a list of bundles *)
 Axiom schedule: bblock -> list bblock.
 
+Extract Constant schedule => "PostpassSchedulingOracle.schedule".
+
 (* TODO - implement the verificator *)
 Definition verified_schedule (bb : bblock) : res (list bblock) := OK (schedule bb).
 
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
new file mode 100644
index 00000000..451a3b26
--- /dev/null
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -0,0 +1,18 @@
+open Asmblock
+
+let bundlize_label l =
+  match l with
+  | [] -> []
+  | l -> [{ header = l; body = []; exit = None }]
+
+let rec bundlize_basic l =
+  match l with
+  | [] -> []
+  | b :: l -> { header = []; body = [b]; exit = None } :: bundlize_basic l
+
+let bundlize_exit e =
+  match e with
+  | Some e -> [{ header = []; body = []; exit = Some e }]
+  | None -> []
+
+let schedule (bb : bblock) : bblock list = bundlize_label bb.header @ bundlize_basic bb.body @ bundlize_exit bb.exit