diff options
-rw-r--r-- | mppa_k1c/Asmexpand.ml | 2 | ||||
-rw-r--r-- | mppa_k1c/Asmgen.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmgenproof.v | 10 | ||||
-rw-r--r-- | mppa_k1c/PostpassScheduling.v | 2 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 18 |
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 |