path: root/mppa_k1c/lib/RTLpathScheduler.v

(** 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 RTLpathLiveproofs 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.

Definition match_prog (p tp: program) :=
  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.

Lemma transf_program_match:
  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
Proof.
  intros. eapply match_transform_partial_program_contextual; eauto.
Qed.

Section PRESERVATION.

Variable prog: program.
Variable tprog: program.

Hypothesis TRANSL: match_prog prog tprog.

Let pge := Genv.globalenv prog.
Let tpge := Genv.globalenv tprog.

(* 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.
  rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
Qed.

Lemma senv_preserved:
  Senv.equiv pge tpge.
Proof.
  eapply (Genv.senv_match TRANSL).
Qed.

Lemma functions_preserved:
  forall (v: val) (f: fundef),
  Genv.find_funct pge v = Some f ->
  exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tpge v = Some tf /\ linkorder cunit prog.
Proof.
  intros. exploit (Genv.find_funct_match TRANSL); eauto.
  intros (cu & tf & A & B & C).
  repeat eexists; intuition eauto.
  + unfold incl; auto.
  + eapply linkorder_refl.
Qed.

Lemma function_ptr_preserved:
  forall v f,
  Genv.find_funct_ptr pge v = Some f ->
  exists tf,
  Genv.find_funct_ptr tpge v = Some tf /\ transf_fundef f = OK tf.
Proof.
  intros.
  exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
Qed.

Lemma function_sig_preserved:
  forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f.
Proof.
  intros. destruct f.
  - simpl in H. monadInv H. simpl. symmetry.
    eapply transf_function_preserves.
    assumption.
  - simpl in H. monadInv H. reflexivity.
Qed.

Theorem transf_initial_states:
  forall s1, initial_state prog s1 ->
  exists s2, initial_state tprog s2 /\ match_states s1 s2.
Proof.
  intros. inv H.
  exploit function_ptr_preserved; eauto. intros (tf & FIND &  TRANSF).
  exists (Callstate nil tf nil m0).
  split.
  - econstructor; eauto.
    + intros; apply (Genv.init_mem_match TRANSL); assumption.
    + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
      symmetry. eapply match_program_main. eauto.
    + destruct f.
      * monadInv TRANSF. rewrite <- H3. symmetry; eapply transf_function_preserves. assumption.
      * monadInv TRANSF. assumption.
  - constructor; eauto.
    + constructor.
    + apply transf_fundef_correct; auto.
    + eapply all_fundef_liveness_ok; eauto.
Qed.

Theorem transf_final_states s1 s2 r:
  final_state s1 r -> match_states s1 s2 -> final_state s2 r.
Proof.
  unfold final_state.
  intros H; inv H.
  intros H; inv H; simpl in * |- *; try congruence.
  inv H1.
  destruct st; simpl in * |- *; try congruence.
  inv STACKS. constructor.
Qed.


Let ge := Genv.globalenv (program_RTL prog).
Let tge := Genv.globalenv (program_RTL tprog).

Lemma senv_sym x y: Senv.equiv x y -> Senv.equiv y x.
Proof.
  unfold Senv.equiv. intuition congruence.
Qed.

Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z.
Proof.
  unfold Senv.equiv. intuition congruence.
Qed.

Lemma senv_preserved_RTL:
  Senv.equiv ge tge.
Proof.
  eapply senv_transitivity. { eapply senv_sym; eapply RTLpath.senv_preserved. }
  eapply senv_transitivity. { eapply senv_preserved. }
  eapply RTLpath.senv_preserved.
Qed.

Lemma symbols_preserved_RTL s: Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  unfold tge, ge. erewrite RTLpath.symbols_preserved; eauto.
  rewrite symbols_preserved.
  erewrite RTLpath.symbols_preserved; eauto.
Qed.

Lemma s_find_function_preserved sp svos rs0 m0 fd:
  sfind_function pge ge sp svos rs0 m0 = Some fd ->
  exists fd', sfind_function tpge tge sp svos rs0 m0 = Some fd'
              /\ transf_fundef fd = OK fd'
              /\ liveness_ok_fundef fd.
Proof.
  Local Hint Resolve symbols_preserved_RTL: core.
  unfold sfind_function. destruct svos; simpl.
  + rewrite (seval_preserved ge tge); auto.
    destruct (seval_sval _ _ _ _); try congruence.
    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:
  ssem ge sp st rs m is ->
  liveness_ok_function f ->
  sistate_simu f dupmap st st' ->
  exists is',
    ssem tge sp st' rs m is' /\ istate_simu f dupmap is is'.
Proof.
  intros SEM LIVE X; eapply X; eauto.
Qed.


Lemma sfmatch_simu dupmap f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s:
  match_function dupmap f f' ->
  liveness_ok_function f ->
  list_forall2 match_stackframes stk stk' ->
  (* s_istate_simu f dupmap st st' -> *)
  sfval_simu f dupmap st.(si_pc) st'.(si_pc) sv sv' ->
  sfmatch pge ge sp st stk f rs0 m0 sv rs m t s ->
  exists s', sfmatch tpge tge sp st' stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'.
Proof.
  Local Hint Resolve transf_fundef_correct: core.
  intros FUN LIVE STK (* SIS *) SFV. destruct SFV; intros SEM; inv SEM; simpl.
  - (* Snone *)
    exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
    intros (path & PATH).
    eexists; split; econstructor; eauto.
    eapply eqlive_reg_refl.
  - (* Scall *)
    exploit s_find_function_preserved; eauto.
    intros (fd' & FIND & TRANSF & LIVE').
    erewrite <- function_sig_preserved; eauto.
    exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
    intros (path & PATH).
    eexists; split; econstructor; eauto.
    + erewrite <- (list_sval_eval_preserved ge tge); auto.
    + simpl. repeat (econstructor; eauto).
  - (* Sreturn *)
    eexists; split; econstructor; eauto.
    + erewrite <- preserv_fnstacksize; eauto.
    + destruct os; auto.
      erewrite <- seval_preserved; eauto.
Qed.

(* The main theorem on simulation of symbolic states ! *)
Theorem smatch_sstate_simu dupmap f f' stk stk' sp st st' rs m t s:
  match_function dupmap f f' ->
  liveness_ok_function f ->
  list_forall2 match_stackframes stk stk' ->
  smatch pge ge sp st stk f rs m t s ->
  sstate_simu f dupmap st st' ->
  exists s', smatch tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
Proof.
  intros MFUNC LIVE STACKS SEM (SIMU1 & SIMU2). destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl.
  - (* sem_early *)
    exploit sistate_simu; eauto.
    unfold istate_simu; rewrite CONT.
    intros (is' & SEM' & (path & PATH & (CONT' & RS' & M') & PC')).
    exists (State stk' f' sp (ipc is') (irs is') (imem is')).
    split.
    + eapply smatch_early; auto. congruence.
    + rewrite M'. econstructor; eauto.
  - (* sem_normal *)
    exploit sistate_simu; eauto.
    unfold istate_simu; rewrite CONT.
    intros (is' & SEM' & (CONT' & RS' & M')).
    rewrite <- eqlive_reg_triv in RS'.
    exploit sfmatch_simu; eauto.
    clear SEM2; intros (s0 & SEM2 & MATCH0).
    exploit sfmatch_equiv; eauto.
    clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s1 & EQ & SEM2).
    exists s1; split.
    + eapply smatch_normal; eauto.
    + eapply match_states_equiv; eauto.
Qed.

Lemma exec_path_simulation dupmap path stk stk' f f' sp rs m pc pc' t s:
  (fn_path f)!pc = Some path ->
  path_step ge pge path.(psize) stk f sp rs m pc t s ->
  list_forall2 match_stackframes stk stk' ->
  dupmap ! pc' = Some pc ->
  match_function dupmap f f' ->
  liveness_ok_function f ->
  exists path' s', (fn_path f')!pc' = Some path' /\ path_step tge tpge path'.(psize) stk' f' sp rs m pc' t s' /\ match_states s s'.
Proof.
  intros PATH STEP STACKS DUPPC MATCHF LIVE.
  exploit initialize_path. { eapply dupmap_path_entry2; eauto. }
  intros (path' & PATH').
  exists path'.
  exploit (sstep_correct f pc pge ge sp path stk rs m t s); eauto.
  intros (st & SYMB & SEM); clear STEP.
  exploit dupmap_correct; eauto.
  clear SYMB; intros (st' & SYMB & SIMU).
  exploit smatch_sstate_simu; eauto.
  intros (s0 & SEM0 & MATCH). 
  exploit sstep_exact; eauto.
  intros (s' & STEP' & EQ).
  exists s'; intuition.
  eapply match_states_equiv; eauto.
Qed.

Lemma step_simulation s1 t s1' s2:
  step ge pge s1 t s1' ->
  match_states s1 s2 ->
  exists s2',
     step tge tpge s2 t s2'
  /\ match_states s1' s2'.
Proof.
  Local Hint Resolve eqlive_stacks_refl transf_fundef_correct: core.
  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. { 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').
    exists s'; split.
    + eapply exec_path; eauto.
    + eapply eqlive_match_states; eauto.
(* exec_function_internal *)
  - inv LIVE.
    exploit initialize_path. { eapply (fn_entry_point_wf f). }
    destruct 1 as (path & PATH).
    inversion TRANSF as [f0 xf tf MATCHF|]; subst. eexists. split.
    + eapply exec_function_internal. erewrite <- preserv_fnstacksize; eauto.
    + erewrite preserv_fnparams; eauto.
      econstructor; eauto. 
      { apply preserv_entrypoint; auto. }
      { apply eqlive_reg_refl. }
(* exec_function_external *)
  - inversion TRANSF as [|]; subst. eexists. split.
    + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved_RTL.
    + constructor. assumption.
(* exec_return *)
  - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split.
    + constructor.
    + inv H1. econstructor; eauto.
Qed.

Theorem transf_program_correct:
  forward_simulation (semantics prog) (semantics tprog).
Proof.
  eapply forward_simulation_step with match_states.
  - eapply senv_preserved.
  - eapply transf_initial_states.
  - intros; eapply transf_final_states; eauto.
  - intros; eapply step_simulation; eauto.
Qed.

End PRESERVATION.