Module BTL_ResetAnnots

Require Import Coqlib Maps.
Require Import AST Smallstep Linking IPass Globalenvs.
Require Import BTL_Invariants BTL.
Require Import OptionMonad.

Definition reset_iinfo (num : positive) (ii : inst_info) : inst_info := {|
  addr_aval := None;
  istore_num := SNumSrc num;
  inst_promotion := IPromNone;
  meminv_annot := None;
  iinfo_shadow := ii.(iinfo_shadow);
|}.

Fixpoint transf_iblock (ib : iblock) (n : positive) {struct ib}: iblock * positive :=
  match ib with
  | BF _ _ | Bnop _ => (ib, n)
  | Bop op args dst ii =>
      (Bop op args dst (reset_iinfo n ii), n)
  | Bload trap chk addr args dst ii =>
      (Bload trap chk addr args dst (reset_iinfo n ii), n)
  | Bstore chk addr args src ii =>
      (Bstore chk addr args src (reset_iinfo n ii),
       Pos.succ n)
  | Bseq ib1 ib2 =>
      let (ib1', n1) := transf_iblock ib1 n in
      let (ib2', n2) := transf_iblock ib2 n1 in
      (Bseq ib1' ib2', n2)
  | Bcond cond args ib1 ib2 iinfo =>
      let (ib1', n1) := transf_iblock ib1 n in
      let (ib2', n2) := transf_iblock ib2 n1 in
      (Bcond cond args ib1' ib2' (reset_iinfo n iinfo), n2)
  end.

Definition transf_function (f : function) : BTL.function :=
  let code' := PTree.map (fun _ ib =>
                   mk_ibinfo (fst (transf_iblock (entry ib) 1)) (binfo ib))
                 (BTL.fn_code f) in
  BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) code' (fn_entrypoint f) (fn_gm f) (fn_info f).

Definition transf_fundef (f : fundef) : fundef :=
  AST.transf_fundef transf_function f.

Definition transf_program (p : program) : BTL.program :=
  AST.transform_program transf_fundef p.

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

Lemma transf_program_match p:
  match_prog p (transf_program p).

Proof.

apply match_transform_program; reflexivity.
Qed.

Section Correctness.

Variable prog : program.
Variable tprog: program.
Variable annot: annot_sem.

Hypothesis TRANSL: match_prog prog tprog.

Let ge0 := Genv.globalenv prog.
Let ge1 := Genv.globalenv tprog.

Lemma ge_find_symbol (s : ident):
Genv.find_symbol ge1 s = Genv.find_symbol ge0 s.

Proof.

apply (Genv.find_symbol_match TRANSL).
Qed.

Lemma ge_find_function fp rs f:
find_function ge0 fp rs = Some f ->
find_function ge1 fp rs = Some (transf_fundef f).

Proof.

intro F0; apply (find_function_match TRANSL) in F0 as (? & ? & ? & ? & _); subst; eauto.
Qed.

Local Hint Resolve ge_find_symbol : core.

Definition transf_stackframe (sf : stackframe) : stackframe :=
  match sf with
  | BTL.Stackframe res f sp pc rs => BTL.Stackframe res (transf_function f) sp pc rs
  end.

Definition transf_state (s : state) : state :=
  match s with
  | State stk f sp pc rs m bc =>
      State (map transf_stackframe stk) (transf_function f) sp pc rs m bc
  | Callstate stk f args m bc =>
      Callstate (map transf_stackframe stk) (transf_fundef f) args m bc
  | Returnstate stk v m bc =>
      Returnstate (map transf_stackframe stk) v m bc
  end.

Lemma transf_istep sp bc rs m ib rs' m' fin
  (ISTEP: iblock_istep AnnotNone ge0 sp bc rs m ib rs' m' fin):
  forall n,
  iblock_istep annot ge1 sp bc rs m (fst (transf_iblock ib n)) rs' m' fin.

Proof.

  induction ISTEP; intro n; simpl.
  1,2:solve [econstructor; eauto].
  - constructor.
    + erewrite Op.eval_operation_preserved; eauto.
    + apply AssertTrue; constructor.
  - econstructor.
    + eapply has_loaded_preserved; eauto.
    + eapply may_undef_prop_lax in UDP as <-.
      eapply MayUndefTrue; constructor.
  - econstructor. 3:eauto.
    + erewrite Op.eval_addressing_preserved; eauto.
    + eapply AssertTrue; constructor.
  - specialize (IHISTEP n).
    do 2 autodestruct; simpl in *; intros.
    apply exec_seq_stop; assumption.
  - specialize (IHISTEP1 n).
    destruct transf_iblock as (ib1', n1).
    specialize (IHISTEP2 n1).
    destruct transf_iblock as (ib2', n2).
    eapply exec_seq_continue; eauto.
  - do 2 autodestruct; intros E2 E1; simpl.
    econstructor; eauto.
      { eapply AssertTrue; constructor. }
    destruct b; epose proof (IH := IHISTEP _).
    + rewrite E1 in IH; exact IH.
    + rewrite E2 in IH; exact IH.
Qed.

Lemma transf_step st0 t st1
(STEP : step AnnotNone ge0 st0 t st1):
step annot ge1 (transf_state st0) t (transf_state st1).

Proof.

  inv STEP; simpl.
  - econstructor.
    + simpl; rewrite PTree.gmap, PC; simpl; reflexivity.
    + simpl.
      case STEP0 as (rs' & m' & fin & ISTEP & FIN).
      exists rs', m', fin; split.
      * apply transf_istep; assumption.
      * revert FIN;
        inversion 1; simpl; econstructor; eauto;
        solve [destruct fd; eauto
              |eapply Events.eval_builtin_args_preserved; eauto
              |eapply Events.external_call_symbols_preserved; eauto using (Genv.senv_match TRANSL)
              |eapply ge_find_function; eauto].
  - apply exec_function_internal with (f:=transf_function f); auto.
  - constructor.
    eapply Events.external_call_symbols_preserved; eauto using (Genv.senv_match TRANSL).
  - constructor.
Qed.

Theorem transf_program_correct:
forward_simulation (sem AnnotNone prog) (sem annot tprog).

Proof.

  apply forward_simulation_step with (fun s s' => s' = transf_state s); simpl.
  - apply (Genv.senv_match TRANSL).
  - intros s1 INI; eexists; split; [|reflexivity].
    inversion INI; eexists.
    + eapply (Genv.init_mem_match TRANSL); eauto.
    + rewrite ge_find_symbol, (match_program_gen_main _ _ _ _ _ TRANSL). eassumption.
    + apply (Genv.find_funct_ptr_transf TRANSL). eassumption.
    + destruct f; simpl in *; assumption.
  - intros ? ? ? ->.
    inversion 1; subst; constructor.
  - intros ? ? ? STEP ? ->; eexists; split; [|reflexivity].
    eauto using transf_step.
Qed.

End Correctness.

Program Definition ipass (annot : annot_sem) : IPass (sem AnnotNone) (sem annot) :=
  {|
    ipass_spec := mkpass match_prog;
    ipass_impl := fun p => Errors.OK (transf_program p);
  |}.

Next Obligation.

apply transf_program_match; assumption. Qed.

Next Obligation.

apply transf_program_correct; assumption. Qed.