path: root/scheduling/RTLtoBTLproof.v

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

Require Import Errors Linking RTLtoBTL.

Require Import Linking.

Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
  dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f);
  dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f);
  code_expand: forall pc ib, (fn_code tf)!pc=Some ib -> is_expand ib.(entry);
  preserv_fnsig: fn_sig tf = RTL.fn_sig f;
  preserv_fnparams: fn_params tf = RTL.fn_params f;
  preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f
}.

Inductive match_fundef: RTL.fundef -> fundef -> Prop :=
  | match_Internal dupmap f tf: match_function dupmap f tf -> match_fundef (Internal f) (Internal tf)
  | match_External ef: match_fundef (External ef) (External ef).

Inductive match_stackframes: RTL.stackframe -> stackframe -> Prop :=
  | match_stackframe_intro 
      dupmap res f sp pc rs f' pc'
      (TRANSF: match_function dupmap f f')
      (DUPLIC: dupmap!pc' = Some pc)
      : match_stackframes (RTL.Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs).

Lemma verify_function_correct dupmap f f' tt:
  verify_function dupmap f' f = OK tt ->
  fn_sig f' = RTL.fn_sig f ->
  fn_params f' = RTL.fn_params f ->
  fn_stacksize f' = RTL.fn_stacksize f ->
  (forall pc ib, (fn_code f')!pc=Some ib -> is_expand ib.(entry)) ->
  match_function dupmap f f'.
Proof.
  unfold verify_function; intro VERIF. monadInv VERIF.
  constructor; eauto.
  - eapply verify_cfg_correct; eauto.
  - eapply verify_is_copy_correct; eauto.
Qed.

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.
  eapply expand_code_correct; 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: RTL.program) (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 BTL_SIMULATES_RTL.

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

Hypothesis TRANSL: match_prog prog tprog.

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

Local Open Scope nat_scope.

(** * Match relation from a RTL state to a BTL state

The "option iblock" parameter represents the current BTL execution state.
Thus, each RTL single step is symbolized by a new BTL "option iblock"
starting at the equivalent PC.

The simulation diagram for match_states_intro is as follows:

<<

        RTL state       match_states_intro        BTL state
      [pcR0,rs0,m0] ---------------------------- [pcB0,rs0,m0]
           |                                         |
           |                                         |
   RTL_RUN | *E0                                     | BTL_RUN
           |                                         |
           |                   MIB                   |
      [pcR1,rs,m] -------------------------------- [ib]

>>
*)

Inductive match_strong_state: (option iblock) -> RTL.state -> state -> Prop :=
  | match_strong_state_intro
      ib dupmap st f sp rs m st' f' pcB0 pcR0 pcR1 rs0 m0 isfst ib0
      (STACKS: list_forall2 match_stackframes st st')
      (TRANSF: match_function dupmap f f')
      (ATpc0: (fn_code f')!pcB0 = Some ib0)
      (DUPLIC: dupmap!pcB0 = Some pcR0)
      (MIB: match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None)
      (IS_EXPD: is_expand ib)
      (RTL_RUN: star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 (RTL.State st f sp pcR1 rs m))
      (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m)
      : match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0)
  .

Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
  | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *)
      ib st f sp rs m st' f' pcB0 pcR1 rs0 m0
      (MSTRONG: match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0))
      (NGOTO: is_goto ib = false)
      : match_states (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0)
  | match_states_call
      st st' f f' args m
      (STACKS: list_forall2 match_stackframes st st')
      (TRANSF: match_fundef f f')
      : match_states None (RTL.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 None (RTL.Returnstate st v m) (Returnstate st' v m)
  .

Lemma match_strong_state_equiv sp st st' ib f f' rs m rs0 m0 pcB0 pcR1:
  match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0) ->
  match is_goto ib with
  | true =>
      exists ib' succ,
        iblock_istep tge sp rs0 m0 (entry ib') rs m (Some (Bgoto succ))
  | false => match_states (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0)
  end.
Proof.
  destruct (is_goto ib) eqn:EQ.
  - intros. destruct ib; try destruct fi; try discriminate.
    inv H. simpl in BTL_RUN.
    rewrite <- iblock_istep_run_equiv in BTL_RUN.
    repeat eexists; eauto.
  - intros. econstructor; eauto.
Qed.

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: RTL.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 -> funsig tf = RTL.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:
  RTL.initial_state prog s1 ->
  exists ib s2, initial_state tprog s2 /\ match_states ib s1 s2.
Proof.
  intros. inv H.
  exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
  eexists. 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 ib s1 s2 r:
  match_states ib s1 s2 -> RTL.final_state s1 r -> final_state s2 r.
Proof.
  intros. inv H0. inv H. inv STACKS. constructor.
Qed.

Lemma find_function_preserved ri rs0 fd
  (FIND : RTL.find_function ge ri rs0 = Some fd)
  : exists fd', find_function tge ri rs0 = Some fd'
                /\ transf_fundef fd = OK fd'.
Proof.
  pose symbols_preserved as SYMPRES.
  destruct ri.
  + simpl in FIND; apply functions_translated in FIND.
    destruct FIND as (tf & cunit & TFUN & GFIND & LO).
    eexists; split. eauto. assumption.
  + simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate.
    apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF).
    eexists; split. simpl. rewrite symbols_preserved.
    rewrite GFS. eassumption. assumption.
Qed.

(** Representing an intermediate BTL state

We keep a measure of code that remains to be executed with the omeasure
type defined below. Intuitively, each RTL step corresponds to either
   - a single BTL step if we are on the last instruction of the block
   - no BTL step (as we use a "big step" semantics) but a change in
     the measure which represents the new intermediate state of the BTL code
 *)
Fixpoint measure ib: nat :=
  match ib with
  | Bseq ib1 ib2
  | Bcond _ _ ib1 ib2 _ => measure ib1 + measure ib2
  | ib => 1
  end.

Definition omeasure (oib: option iblock): nat :=
 match oib with
 | None => 0
 | Some ib => measure ib
 end.

Remark measure_pos: forall ib,
  measure ib > 0.
Proof.
  induction ib; simpl; auto; lia.
Qed.

Lemma list_nth_z_rev_dupmap:
  forall dupmap ln ln' (pc pc': node) val,
  list_nth_z ln val = Some pc ->
  list_forall2 (fun n' n => dupmap!n' = Some n) ln' ln ->
  exists (pc': node),
     list_nth_z ln' val = Some pc'
  /\ dupmap!pc' = Some pc.
Proof.
  induction ln; intros until val; intros LNZ LFA.
  - inv LNZ.
  - inv LNZ. destruct (zeq val 0) eqn:ZEQ.
    + inv H0. destruct ln'; inv LFA.
      simpl. exists p. split; auto.
    + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto.
      intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence.
Qed.

Lemma opt_simu_intro
  sp f f' st st' pcR1 pcB0 ib rs m rs0 m0 t s1'
  (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) t s1')
  (MSTRONG : match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m)
              (State st' f' sp pcB0 rs0 m0))
  (NGOTO : is_goto ib = false)
  : exists (oib' : option iblock),
     (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2')
  \/ (omeasure oib' < omeasure (Some ib) /\ t=E0 /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)).
Proof.
  inv MSTRONG. inv MIB.
  - (* mib_BF *)
    inv H0;
    inversion STEP; subst; try_simplify_someHyps; intros.
    + (* Breturn *)
      eexists; left; eexists; split.
      * econstructor; eauto. econstructor.
        eexists; eexists; split.
        eapply iblock_istep_run_equiv in BTL_RUN.
        eapply BTL_RUN. econstructor; eauto.
        erewrite preserv_fnstacksize; eauto.
      * econstructor; eauto.
    + (* Bcall *)
      rename H10 into FIND.
      eapply find_function_preserved in FIND.
      destruct FIND as (fd' & FF & TRANSFUN).
      eexists; left; eexists; split.
      * econstructor; eauto. econstructor.
        eexists; eexists; split.
        eapply iblock_istep_run_equiv in BTL_RUN.
        eapply BTL_RUN. econstructor; eauto.
        eapply function_sig_translated; eauto.
      * repeat (econstructor; eauto).
        eapply transf_fundef_correct; eauto.
    + (* Btailcall *)
      rename H9 into FIND.
      eapply find_function_preserved in FIND.
      destruct FIND as (fd' & FF & TRANSFUN).
      eexists; left; eexists; split.
      * econstructor; eauto. econstructor.
        eexists; eexists; split.
        eapply iblock_istep_run_equiv in BTL_RUN.
        eapply BTL_RUN. econstructor; eauto.
        eapply function_sig_translated; eauto.
        erewrite preserv_fnstacksize; eauto.
      * repeat (econstructor; eauto).
        eapply transf_fundef_correct; eauto.
    + (* Bbuiltin *)
      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
      remember H1 as ODUPLIC; clear HeqODUPLIC.
      apply DMC in H1 as [ib [FNC MI]]; clear DMC.
      eexists; left; eexists; split.
      * econstructor; eauto. econstructor.
        eexists; eexists; split.
        eapply iblock_istep_run_equiv in BTL_RUN.
        eapply BTL_RUN. econstructor; eauto.
        pose symbols_preserved as SYMPRES.
        eapply eval_builtin_args_preserved; eauto.
        eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
      * econstructor; eauto.
        { econstructor; eauto. eapply code_expand; eauto.  
          apply star_refl. }
        inversion MI; subst; try_simplify_someHyps.
        inv H3; try_simplify_someHyps.
    + (* Bjumptable *)
      exploit list_nth_z_rev_dupmap; eauto.
      intros (pc'0 & LNZ & DM).
      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
      remember DM as ODUPLIC; clear HeqODUPLIC.
      apply DMC in DM as [ib [FNC MI]]; clear DMC.
      eexists; left; eexists; split.
      * econstructor; eauto. econstructor.
        eexists; eexists; split.
        eapply iblock_istep_run_equiv in BTL_RUN.
        eapply BTL_RUN. econstructor; eauto.
      * econstructor; eauto.
        { econstructor; eauto. eapply code_expand; eauto.  
          apply star_refl. }
        inversion MI; subst; try_simplify_someHyps.
        inv H4; try_simplify_someHyps.
  - (* mib_exit *)
    discriminate.
  - (* mib_seq *) admit.
    (* inv H.
    + (* Bnop *)
      inversion STEP; subst; try_simplify_someHyps.
      exists (Some b2); right; repeat (split; auto).
      econstructor; eauto. inv IS_EXPD; auto; discriminate.
      eapply star_right; eauto.
    + (* Bop *)
      inversion STEP; subst; try_simplify_someHyps.
      exists (Some b2); right; repeat (split; auto).
      econstructor; eauto. inv IS_EXPD; auto; discriminate.
      eapply star_right; eauto.
      erewrite eval_operation_preserved in H10.
      erewrite H10 in BTL_RUN; simpl in BTL_RUN; auto.
      intros; rewrite <- symbols_preserved; trivial.
    + (* Bload *)
      inversion STEP; subst; try_simplify_someHyps.
      exists (Some (b2)); right; repeat (split; auto).
      econstructor; eauto. inv IS_EXPD; auto; discriminate.
      eapply star_right; eauto.
      erewrite eval_addressing_preserved in H10.
      erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto.
      intros; rewrite <- symbols_preserved; trivial.
    + (* Bstore *)
      inversion STEP; subst; try_simplify_someHyps.
      exists (Some b2); right; repeat (split; auto).
      econstructor; eauto. inv IS_EXPD; auto; discriminate.
      eapply star_right; eauto.
      erewrite eval_addressing_preserved in H10.
      erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto.
      intros; rewrite <- symbols_preserved; trivial.
    + (* Absurd case *)
      inv IS_EXPD. inv H4. inv H.
    + (* Absurd Bcond (Bcond are not allowed in the left part of a Bseq *)
              inv IS_EXPD; discriminate.*)
  - (* mib_cond *) admit. (*
    inversion STEP; subst; try_simplify_someHyps.
    intros; rewrite H12 in BTL_RUN. destruct b.
    * (* Ifso *)
      exists (Some bso); right; repeat (split; eauto).
      simpl; assert (measure bnot > 0) by apply measure_pos; lia.
      inv H2; econstructor; eauto.
      1,3: inv IS_EXPD; auto; discriminate.
      all: eapply star_right; eauto.
    * (* Ifnot *)
      exists (Some bnot); right; repeat (split; eauto).
      simpl; assert (measure bso > 0) by apply measure_pos; lia.
      inv H2; econstructor; eauto.
      1,3: inv IS_EXPD; auto; discriminate.
                             all: eapply star_right; eauto.*)
Admitted.

(** * Main RTL to BTL simulation theorem

Two possible executions:

<<

 **Last instruction:**

    RTL state         match_states          BTL state
       s1 ------------------------------------ s2
       |                                       |
  STEP |       Classical lockstep simu         | 
       |                                       | 
       s1' ----------------------------------- s2' 


 **Middle instruction:**

    RTL state         match_states [oib]    BTL state
       s1 ------------------------------------ s2
       |                               _______/
  STEP | *E0       ___________________/         
       |          / match_states [oib']         
       s1' ______/
   Where omeasure oib' < omeasure oib

>>
*)

Theorem opt_simu s1 t s1' oib s2:
 RTL.step ge s1 t s1' ->
 match_states oib s1 s2 ->
 exists (oib' : option iblock),
     (exists s2', step tge s2 t s2' /\ match_states oib' s1' s2')
  \/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2) 
 .
Proof.
  inversion 2; subst; clear H0.
  - (* State *)
    exploit opt_simu_intro; eauto.
  - (* Callstate *)
    inv H.
    + (* Internal function *)
      inv TRANSF.
      rename H0 into TRANSF.
      eapply dupmap_entrypoint in TRANSF as ENTRY.
      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
      apply DMC in ENTRY as DMC'.
      destruct DMC' as [ib [CENTRY MI]]; clear DMC.
      eexists; left; eexists; split.
      * eapply exec_function_internal.
        erewrite preserv_fnstacksize; eauto.
      * econstructor; eauto.
        eapply code_expand; eauto.
        all: erewrite preserv_fnparams; eauto.
        constructor.
    + (* External function *)
      inv TRANSF.
      eexists; left; eexists; split.
      * eapply exec_function_external.
        eapply external_call_symbols_preserved.
        eapply senv_preserved. eauto.
      * econstructor; eauto.
  - (* Returnstate *)
    inv H. inv STACKS. inv H1.
    eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
    remember DUPLIC as ODUPLIC; clear HeqODUPLIC.
    apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC.
    eexists; left; eexists; split.
    + eapply exec_return.
    + econstructor; eauto.
      eapply code_expand; eauto.
      constructor.
Qed.

Local Hint Resolve plus_one star_refl: core.

Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (BTL.semantics tprog).
Proof.
  eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ omeasure) match_states).
  constructor 1; simpl.
  - apply well_founded_ltof.
  - eapply transf_initial_states.
  - eapply transf_final_states.
  - intros s1 t s1' STEP i s2 MATCH. exploit opt_simu; eauto. clear MATCH STEP.
    destruct 1 as (oib' & [ (s2' & STEP & MATCH) | (MEASURE & TRACE & MATCH) ]).
    + repeat eexists; eauto.
    + subst. repeat eexists; eauto.
  - eapply senv_preserved.
Qed.

End BTL_SIMULATES_RTL.