2 files changed, 135 insertions, 0 deletions
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
new file mode 100644
index 00000000..8ec72f90
--- /dev/null
+++ b/mppa_k1c/PostpassScheduling.v
@@ -0,0 +1,38 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import Asmblock.
+
+(** Oracle taking as input a basic block,
+    returns a basic block with its instruction reordered *)
+Axiom schedule: bblock -> bblock.
+
+(** Oracle taking as input a basic block
+    splits it into several bblocks (representing bundles *)
+Axiom split: bblock -> list bblock.
+
+(* TODO - separate the postpass_schedule in two phases *)
+
+Definition postpass_schedule (lb : list bblock) : list bblock :=
+  match lb with
+  | nil => nil
+  | (cons b lb) => split (schedule b) ++ lb
+  end.
+
+Definition transf_function (f: function) : function :=
+  mkfunction (fn_sig f) (postpass_schedule (fn_blocks f)).
+
+Definition transf_fundef (f: fundef) : fundef :=
+  AST.transf_fundef transf_function f.
+
+Definition transf_program (p: program) : program :=
+  AST.transform_program transf_fundef p.
+\ No newline at end of file
diff --git a/mppa_k1c/PostpassSchedulingProof.v b/mppa_k1c/PostpassSchedulingProof.v
new file mode 100644
index 00000000..3e3201bb
--- /dev/null
+++ b/mppa_k1c/PostpassSchedulingProof.v
@@ -0,0 +1,97 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Correctness proof for the [Debugvar] pass. *)
+
+Require Import Coqlib Errors.
+Require Import Integers Floats AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Op Locations Machblock Conventions Asmblock.
+Require Import PostpassScheduling.
+
+(** * Relational characterization of the transformation *)
+
+Definition match_prog (p tp: Asmblock.program) :=
+  match_program (fun _ f tf => tf = transf_fundef f) eq p tp.
+
+Lemma transf_program_match:
+  forall p, match_prog p (transf_program p).
+Proof.
+  intros. eapply match_transform_program; eauto.
+Qed.
+
+Section PRESERVATION.
+
+Variables prog tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma symbols_preserved:
+  forall id,
+  Genv.find_symbol tge id = Genv.find_symbol ge id.
+Proof (Genv.find_symbol_transf TRANSL).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_transf TRANSL).
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_transf TRANSL).
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  Genv.find_funct_ptr tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_ptr_transf TRANSL).
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_intro:
+      forall s1 s2, s1 = s2 -> match_states s1 s2.
+
+(** TODO - continue *)
+
+(* Lemma transf_initial_states:
+  forall st1, initial_state prog st1 ->
+  exists st2, initial_state tprog st2 /\ match_states st1 st2.
+Proof.
+  intros. inv H.
+  econstructor; split.
+  eapply initial_state_intro with (m0 := m0).
+  eapply (Genv.init_mem_transf TRANSL); eauto.
+(*   rewrite (match_program_main TRANSL), symbols_preserved; eauto.
+  apply function_ptr_translated; auto.
+  rewrite sig_function_translated. auto. *)
+  constructor; auto. constructor.
+Qed.
+
+Lemma transf_final_states:
+  forall st1 st2 r,
+  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
+Proof.
+  intros. inv H0. inv H. inv H5. econstructor; eauto.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (Linear.semantics prog) (Linear.semantics tprog).
+Proof.
+  eapply forward_simulation_opt.
+  apply senv_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  eexact transf_step_correct.
+Qed.
+ *)
+End PRESERVATION.