1 files changed, 190 insertions, 0 deletions
diff --git a/kvx/lib/RTLpathScheduler.v b/kvx/lib/RTLpathScheduler.v
new file mode 100644
index 00000000..57ae6c7f
--- /dev/null
+++ b/kvx/lib/RTLpathScheduler.v
@@ -0,0 +1,190 @@
+(** RTLpath Scheduling from an external oracle. 
+
+This module is inspired from [Duplicate] and [Duplicateproof]
+
+*)
+
+Require Import AST Linking Values Maps Globalenvs Smallstep Registers.
+Require Import Coqlib Maps Events Errors Op.
+Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory.
+
+
+Local Open Scope error_monad_scope.
+Local Open Scope positive_scope.
+
+
+
+(** External oracle returning the new RTLpath function and a mapping of new path_entries to old path_entries 
+
+NB: the new RTLpath function is generated from the fn_code, the fn_entrypoint and the fn_path
+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 * (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;
+  preserv_fnparams: fn_params f1 = fn_params f2;
+  preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2;
+  preserv_entrypoint: dupmap!(f2.(fn_entrypoint)) = Some f1.(fn_entrypoint);
+  dupmap_path_entry1: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f1) pc1;
+  dupmap_path_entry2: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f2) pc2;
+  dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> sstep_simu dupmap f1 f2 pc1 pc2
+}.
+
+(* 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'.
+
+Theorem transf_function_preserves:
+  forall f f',
+  transf_function f = OK f' ->
+     fn_sig f = fn_sig f' /\ fn_params f = fn_params f' /\ fn_stacksize f = fn_stacksize f'.
+Proof.
+  intros. exploit transf_function_correct; eauto.
+  destruct 1 as (dupmap & [SIG PARAM SIZE ENTRY CORRECT]).
+  intuition.
+Qed.
+
+Definition transf_fundef (f: fundef) : res fundef :=
+  transf_partial_fundef transf_function f.
+
+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).
+
+Inductive match_fundef: RTLpath.fundef -> RTLpath.fundef -> Prop :=
+  | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f')
+  | match_External ef: match_fundef (External ef) (External ef).
+
+Inductive match_stackframes: stackframe -> stackframe -> Prop :=
+  | match_stackframe_intro dupmap res f sp pc rs1 rs2 f' pc' path
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc' = Some pc)
+      (LIVE: liveness_ok_function f)
+      (PATH: f.(fn_path)!pc = Some path)
+      (EQUIV: forall v, eqlive_reg (ext path.(input_regs)) (rs1 # res <- v) (rs2 # res <- v)):
+      match_stackframes (Stackframe res f sp pc rs1) (Stackframe res f' sp pc' rs2).
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_intro dupmap st f sp pc rs1 rs2 m st' f' pc' path
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc' = Some pc)
+      (LIVE: liveness_ok_function f)
+      (PATH: f.(fn_path)!pc = Some path)
+      (EQUIV: eqlive_reg (ext path.(input_regs)) rs1 rs2):
+      match_states (State st f sp pc rs1 m) (State st' f' sp pc' rs2 m)
+  | match_states_call st st' f f' args m
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_fundef f f')
+      (LIVE: liveness_ok_fundef f):
+      match_states (Callstate st f args m) (Callstate st' f' args m)
+  | match_states_return st st' v m
+      (STACKS: list_forall2 match_stackframes st st'):
+      match_states (Returnstate st v m) (Returnstate st' v m).
+
+Lemma match_stackframes_equiv stf1 stf2 stf3:
+  match_stackframes stf1 stf2 -> equiv_stackframe stf2 stf3 -> match_stackframes stf1 stf3.
+Proof.
+  destruct 1; intros EQ; inv EQ; try econstructor; eauto.
+  intros; eapply eqlive_reg_trans; eauto.
+  rewrite eqlive_reg_triv in * |-.
+  eapply eqlive_reg_update.
+  eapply eqlive_reg_monotonic; eauto.
+  simpl; auto.
+Qed.
+
+Lemma match_stack_equiv stk1 stk2:
+  list_forall2 match_stackframes stk1 stk2 -> 
+  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
+  list_forall2 match_stackframes stk1 stk3.
+Proof.
+  Local Hint Resolve match_stackframes_equiv: core.
+  induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
+Qed.
+
+Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3.
+Proof.
+  Local Hint Resolve match_stack_equiv: core.
+  destruct 1; intros EQ; inv EQ; econstructor; eauto.
+  intros; eapply eqlive_reg_triv_trans; eauto.
+Qed.
+
+Lemma eqlive_match_stackframes stf1 stf2 stf3:
+  eqlive_stackframes stf1 stf2 -> match_stackframes stf2 stf3 -> match_stackframes stf1 stf3.
+Proof.
+  destruct 1; intros MS; inv MS; try econstructor; eauto.
+  try_simplify_someHyps. intros; eapply eqlive_reg_trans; eauto.
+Qed.
+
+Lemma eqlive_match_stack stk1 stk2:
+  list_forall2 eqlive_stackframes stk1 stk2 -> 
+  forall stk3, list_forall2 match_stackframes stk2 stk3 -> 
+  list_forall2 match_stackframes stk1 stk3.
+Proof.
+  induction 1; intros stk3 MS; inv MS; econstructor; eauto.
+  eapply eqlive_match_stackframes; eauto.
+Qed.
+
+Lemma eqlive_match_states s1 s2 s3: eqlive_states s1 s2 -> match_states s2 s3 -> match_states s1 s3.
+Proof.
+  Local Hint Resolve eqlive_match_stack: core.
+  destruct 1; intros MS; inv MS; try_simplify_someHyps; econstructor; eauto.
+  eapply eqlive_reg_trans; eauto.
+Qed.
+
+Lemma eqlive_stackframes_refl stf1 stf2: match_stackframes stf1 stf2 -> eqlive_stackframes stf1 stf1.
+Proof.
+  destruct 1; econstructor; eauto.
+  intros; eapply eqlive_reg_refl; eauto.
+Qed.
+
+Lemma eqlive_stacks_refl stk1 stk2:
+  list_forall2 match_stackframes stk1 stk2 -> list_forall2 eqlive_stackframes stk1 stk1.
+Proof.
+  induction 1; simpl; econstructor; eauto.
+  eapply eqlive_stackframes_refl; eauto.
+Qed.
+
+Lemma transf_fundef_correct f f':
+  transf_fundef f = OK f' -> match_fundef f f'.
+Proof.
+  intros TRANSF; destruct f; simpl; monadInv TRANSF.
+  + exploit transf_function_correct; eauto.
+    intros (dupmap & MATCH_F).
+    eapply match_Internal; eauto.
+  + eapply match_External.
+Qed.
+