path: root/scheduling/BTLtoRTLproof.v

Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import RTL Op Registers OptionMonad BTL.

Require Import Errors Linking BTLtoRTL.


(*****************************)
(* Put this in an other file *)

Require Import Linking.

Lemma transf_function_correct f f':
  transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
Proof.
  unfold transf_function; unfold bind. repeat autodestruct.
  intros H _ _ X. inversion X; subst; clear X.
  eexists; eapply verify_function_correct; simpl; 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: program) (tp: RTL.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 RTL_SIMULATES_BTL.

Variable prog: program.
Variable tprog: RTL.program.

Hypothesis TRANSL: match_prog prog tprog.

Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
Qed.

Lemma senv_preserved: Senv.equiv ge tge.
Proof.
  eapply (Genv.senv_match TRANSL).
Qed.

Lemma functions_translated (v: val) (f: fundef):
  Genv.find_funct ge v = Some f ->
  exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge 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_translated v f:
  Genv.find_funct_ptr ge v = Some f ->
  exists tf,
  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
Proof.
  intros.
  exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
Qed.

Lemma function_sig_translated f tf: transf_fundef f = OK tf -> RTL.funsig tf = funsig f.
Proof.
  intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
  erewrite preserv_fnsig; eauto.
Qed.

Lemma transf_initial_states s1:
  initial_state prog s1 ->
  exists s2, RTL.initial_state tprog s2 /\ match_states s1 s2.
Proof.
  intros. inv H.
  exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
  eexists. split.
  - econstructor; eauto.
    + eapply (Genv.init_mem_transf_partial TRANSL); eauto.
    + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
      symmetry. eapply match_program_main. eauto.
    + erewrite function_sig_translated; eauto.
  - constructor; eauto.
    constructor.
    apply transf_fundef_correct; auto.
Qed.

Lemma transf_final_states s1 s2 r:
  match_states s1 s2 -> final_state s1 r -> RTL.final_state s2 r.
Proof.
  intros. inv H0. inv H. inv STACKS. constructor.
Qed.

(* FIXME: unused ?
Definition is_goto (i: final): option exit :=
  match i with
  | Bgoto pc => Some pc
  | _ => None
  end.
*)

(* variant of [star RTL.step] but requiring proposition [P] on the [refl] (stutttering) case. *)
Inductive cond_star_step (P: Prop): RTL.state -> trace -> RTL.state -> Prop :=
  | css_refl s: P -> cond_star_step P s E0 s
  | css_plus s1 t s2: plus RTL.step tge s1 t s2 -> cond_star_step P s1 t s2
  .

Lemma css_plus_trans P Q s0 s1 s2 t:
  plus RTL.step tge s0 E0 s1 ->
  cond_star_step P s1 t s2 ->
  cond_star_step Q s0 t s2.
Proof.
  intros PLUS STAR.
  eapply css_plus.
  inv STAR; auto.
  eapply plus_trans; eauto.
Qed.

Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
 (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin):
 forall pc0 opc isfst
 (MIB: match_iblock dupmap (RTL.fn_code f') isfst pc0 ib opc)
 ,
  match ofin with 
  | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
  | Some fin =>
     (* A CHANGER ? *)
     exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin None
                /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
  end.
Proof.
  induction IBIS; simpl; intros.
  - assert (X: opc = None). { inv MIB; auto. }
    subst.
    repeat eexists; eauto.
    eapply css_refl; auto.
  - inv MIB. exists pc'; split; auto.
    apply plus_one. apply exec_Inop; trivial.
  - inv MIB. exists pc'; split; auto.
    apply plus_one. eapply exec_Iop; eauto.
    erewrite <- eval_operation_preserved; eauto.
    intros; rewrite symbols_preserved; trivial.
  - inv MIB. exists pc'; split; auto.
    apply plus_one. eapply exec_Iload; eauto.
    erewrite <- eval_addressing_preserved; eauto.
    intros; rewrite symbols_preserved; trivial.
  - inv MIB. exists pc'; split; auto.
    apply plus_one. eapply exec_Istore; eauto.
    erewrite <- eval_addressing_preserved; eauto.
    intros; rewrite symbols_preserved; trivial.
  - inv MIB.
    exploit IHIBIS; eauto.
  - inv MIB.
    exploit IHIBIS1; eauto.
    intros (pc1 & EQpc1 & STEP1); inv EQpc1.
    exploit IHIBIS2; eauto.
    destruct ofin; simpl.
    + intros (ifst2 & pc2 & M2 & STEP2).
      repeat eexists; eauto.
      eapply css_plus_trans; eauto.
    + intros (pc2 & EQpc2 & STEP2); inv EQpc2.
      eexists; split; auto.
      eapply plus_trans; eauto.
  - inv MIB.
    destruct b; exploit IHIBIS; eauto.
    + (* taking ifso *)
      destruct ofin; simpl.
      * (* ofin is Some final *)
        intros (isfst' & pc1 & MI & STAR).
        repeat eexists; eauto.
        eapply css_plus_trans.
        eapply plus_one. eapply exec_Icond; eauto.
        eauto.
      * (* ofin is None *)
        intros (pc1 & OPC & PLUS). inv OPC.
        inv H10; eexists; split; eauto.
        all:
          eapply plus_trans;
          [ eapply plus_one; eapply exec_Icond; eauto
          | eauto | eauto ].
    + (* taking ifnot *)
      destruct ofin; simpl.
      * (* ofin is Some final *)
        intros (isfst' & pc1 & MI & STAR).
        repeat eexists; eauto.
        eapply css_plus_trans.
        eapply plus_one. eapply exec_Icond; eauto.
        eauto.
      * (* ofin is None *)
        intros (pc1 & OPC & PLUS). inv OPC.
        inv H10; eexists; split; eauto.
        all:
          eapply plus_trans;
          [ eapply plus_one; eapply exec_Icond; eauto
          | eauto | eauto ].
Qed.

Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s
 (STACKS: list_forall2 match_stackframes stack stack')
 (TRANSF: match_function dupmap f f')
 (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin))
 (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None)
 (FS : final_step ge stack f sp rs1 m1 fin t s)
 :exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
Proof.
  intros; exploit iblock_istep_simulation; eauto.
  simpl. intros (isfst' & pc1 & MI & STAR).
  induction FS.
  - inv MI.
    + inv STAR; inv H3.
    + inv STAR; try discriminate.
      eexists; split. eauto.
      econstructor; eauto.

  - inv MI.
    inv STAR.
    + inv H5. eexists; split.
      eapply plus_one. eapply exec_Ireturn; eauto.
      erewrite <- preserv_fnstacksize; eauto.
      econstructor; eauto.
    + inv H5. eexists; split.
      eapply plus_trans. eauto.
      eapply plus_one. eapply exec_Ireturn; eauto.
      erewrite <- preserv_fnstacksize; eauto. eauto.
      econstructor; eauto.
  - inv MI.
    inv STAR.
    + inv H5.
      pose symbols_preserved as SYMPRES.
      destruct ros.
      * simpl in H. apply functions_translated in H.
        destruct H as (tf & cunit & TFUN & GFIND & LO).
        eexists; split.
        eapply plus_one. eapply exec_Icall; eauto.
        apply function_sig_translated. assumption.
        admit.
        (* TODO ?? *)
      * admit.
    + admit.
  - admit.
  - inv MI. pose symbols_preserved as SYMPRES.
    inv STAR.
    + inv H5. eexists; split.
      eapply plus_one. eapply exec_Ibuiltin; eauto.
      eapply eval_builtin_args_preserved; eauto.
      eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
      econstructor; eauto.
    + inv H5. eexists; split.
      eapply plus_trans. eauto.
      eapply plus_one. eapply exec_Ibuiltin; eauto.
      eapply eval_builtin_args_preserved; eauto.
      eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
      eauto. econstructor; eauto.
(* Icond *)
  - admit.
  - admit.
Admitted.

(* BROUILLON

Inductive iblock_istep_gen sp dupmap stack f pc0 cfg ib: trace -> bool -> option final -> option node -> Prop :=
  | ibis_synced opc pc1
      (HOPC: opc = Some pc1)
      (MIB : match_iblock dupmap cfg true pc0 ib opc)
      : iblock_istep_gen sp dupmap stack f pc0 cfg ib E0 true None opc
  | ibis_stutter rs1 m1 fin ofin s t
      (HFIN: ofin = Some fin)
      (MIB : match_iblock dupmap cfg false pc0 ib None)
      (FS : final_step ge stack f sp rs1 m1 fin t s)
      : iblock_istep_gen sp dupmap stack f pc0 cfg ib t false ofin None.

Lemma iblock_step_simulation
 sp dupmap stack stack' f f' rs0 m0 rs1 m1 ib ofin pc0 opc t s isfst
 (STACKS: list_forall2 match_stackframes stack stack')
 (TRANSF: match_function dupmap f f')
 (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin)
 (*(MIB : match_iblock dupmap cfg' isfst pc0 ib opc)*)
 (*(FS : final_step ge stack f sp rs1 m1 fin t s)*)
(*FNC : (fn_code f) ! pc = Some ib*)
 (IBGEN: iblock_istep_gen sp dupmap stack f pc0 (RTL.fn_code f') ib t isfst ofin opc)
 :exists s', (if isfst then plus RTL.step else star RTL.step) tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
Proof.
  (* TODO: généraliser ce lemme pour pouvoir le prouver par induction sur IBIS:
       => il faut en particulier généraliser l'hypothèse MIB qui relie le iblock_istep ib en cours d'exécution.
          avec le code RTL à partir de pc0. 
       => ici, le "isfst" a déjà été généralisé: quand il vaut "false", ça veut dire qu'on a le droit de faire du "stuttering" côté RTL.
       => il reste à comprendre comment généraliser le "None" en "opc"
          ainsi que l'hypothese OFIN pour autoriser le cas "ofin=None" (nécessaire pour l'induction).
          Idée: si "ofin = None" alors il y a un pc1 tq "opc = Some pc1" qui permet d'exécuter la suite du bloc...

    Au final, il faut sans doute introduire un "Inductive" pour capturer ces idées dans un prédicat "lisible"/"manipulable"...
  *)
  (* XXX keep IBIS, MIB, and FS ? *)
  induction IBIS.
  - admit.
  - inv IBGEN; try_simplify_someHyps.
    inv MIB. eexists; split.
    apply plus_one. econstructor; eauto.
    (*
  - inversion IBGEN; subst; try_simplify_someHyps.
    exploit iblock_istep_simulation; eauto.
    inv MIB.
    eexists. split. apply plus_one.
    eapply exec_Inop; eauto.
    try_simplify_someHyps.
      admit.
  - (* exec_op *)
    admit. (* cas absurde car hypothese OFIN trop restrictive *)
  - (* exec_load_TRAP *)
    admit. (* cas absurde car hypothese OFIN trop restrictive *)
  - (* exec_load_store *)
    admit. (* cas absurde car hypothese OFIN trop restrictive *)
  - (* exec_seq_stop *)
    (*inv MIB.*)
    eapply IHIBIS; eauto.
    (* TODO: c'est ici qu'on voit que l'hypothèse MIB est trop restrictive actuellement 
       normalement, l'hypothèse d'induction IHIBIS devrait permettre de conclure quasi-directement ici.
    *)
    admit.
  - (* exec_seq_continue *)
    (* TODO: ici l'hypothèse d'induction IHIBIS1 n'est pas utilisable à cause de OFIN trop restrictive *)
    try_simplify_someHyps.
    (*inv MIB.*)
    admit.
  - (* exec_cond *)
    try_simplify_someHyps.
    (*inv MIB.*)
       admit.*)
Admitted.

*)

Theorem plus_simulation s1 t s1':
  step ge s1 t s1' ->
  forall s2 (MS: match_states s1 s2),
  exists s2',
     plus RTL.step tge s2 t s2'
  /\ match_states s1' s2'.
Proof.
  destruct 1; intros; inv MS.
  - eapply dupmap_correct in DUPLIC; eauto.
    destruct DUPLIC as (ib' & FNC & MIB).
    try_simplify_someHyps. destruct STEP as (rs' & m' & fin & IBIS & FS).
    intros; exploit iblock_step_simulation; eauto.
  (* exec_function_internal *)
  - inversion TRANSF as [dupmap f0 f0' MATCHF|]; subst. eexists. split.
    + eapply plus_one. apply RTL.exec_function_internal.
      erewrite <- preserv_fnstacksize; eauto.
    + erewrite <- preserv_fnparams; eauto.
      eapply match_states_intro; eauto.
      apply dupmap_entrypoint. assumption.
  (* exec_function_external *)
  - inversion TRANSF as [|]; subst. eexists. split.
    + eapply plus_one. econstructor.
      eapply external_call_symbols_preserved; eauto. apply senv_preserved.
    + constructor. assumption.
  (* exec_return *)
  - inversion STACKS as [|a1 al b1 bl H1 HL]; subst.
    destruct b1 as [res' f' sp' pc' rs'].
    eexists. split.
    + eapply plus_one. constructor.
    + inv H1. econstructor; eauto.
Qed.

Theorem transf_program_correct:
  forward_simulation (semantics prog) (RTL.semantics tprog).
Proof.
  eapply forward_simulation_plus with match_states.
  - eapply senv_preserved.
  - eapply transf_initial_states.
  - eapply transf_final_states.
  - eapply plus_simulation.
Qed.

End RTL_SIMULATES_BTL.