Module cleanuplabels_proof

Require Import Coqlib Integers Maps Values AST Globalenvs.
Require Import CUAST InteractionSemantics Footprint.
Require Import IS_local.
Require Import Memory Blockset Op_fp Linear Linear_local val_casted.
Require Import InjRels LDSimDefs_local LDSim_local.
Require Import Errors CleanupLabels cleanuplabels.
Local Notation empfp:=FP.emp.
Local Notation footprint:=FP.t.
Definition match_cu (su tu:Linear_comp_unit):=
  match_comp_unit_gen (fun f tf => OK (transf_fundef f) = OK tf) eq su tu.
Lemma transf_program_match:
  forall p tp, transf_program p = OK tp -> match_cu p tp.
Section PRESERVATION.
Variable scu tcu: Linear_comp_unit.
Variable sge tge: Linear.genv.
Hypothesis SGEINIT: globalenv_generic scu sge.
Hypothesis TGEINIT: globalenv_generic tcu tge.
Hypothesis S_EQ: sge.(Genv.genv_next) = tge.(Genv.genv_next).
Hypothesis TRANSF: match_cu scu tcu.
Lemma ge_match: ge_match_strict sge tge.
Lemma genv_match: Genv.match_genvs (match_globdef (fun f tf => OK (transf_fundef f) = OK tf) eq) sge tge.
Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol sge s.

Lemma funct_ptr_translated:
  forall (b: block) (f: Linear.fundef),
  Genv.find_funct_ptr sge b = Some f ->
  Genv.find_funct_ptr tge b = Some (transf_fundef f).
Lemma functions_translated:
  forall (v: val) (f: Linear.fundef),
  Genv.find_funct sge v = Some f ->
  Genv.find_funct tge v = Some (transf_fundef f).
Lemma senv_preserved:
  Senv.equiv sge tge.
Lemma sig_preserved:
  forall f, funsig (transf_fundef f) = funsig f.
Lemma stacksize_preserved:
  forall f, fn_stacksize (transf_function f) = fn_stacksize f.
Lemma find_function_translated:
  forall ros rs f, find_function sge ros rs = Some f ->
  find_function tge ros rs = Some (transf_fundef f).
Definition match_locset(l1 l2:locset):Prop:=
  forall loc, Val.lessdef (l1 loc)(l2 loc).
Inductive match_stackframes: stackframe -> stackframe -> Prop :=
  | match_stackframe_intro:
      forall f sp rs ls0 c,
    match_locset rs ls0->
    incl c f.(fn_code) ->
    match_stackframes (Stackframe f sp rs c)
    (Stackframe (transf_function f) sp ls0
       (remove_unused_labels (labels_branched_to (fn_code f)) c)).
Lemma match_locset_refl: forall l, match_locset l l.
Definition state:Type:=core*mem.
Inductive match_states: state -> state -> Prop :=
  | match_states_intro:
      forall s f sp c ls m ts ls0 m' ls2 f' ls3,
      list_forall2 match_stackframes s ts ->
      match_locset ls ls0->
      Mem.extends m m'->
      incl c f.(fn_code) ->
      match_locset ls2 ls3 ->
      match_states (Core_State s f sp c ls (mk_load_frame ls2 f'), m)
                   (Core_State ts (transf_function f) sp (remove_unused_labels (labels_branched_to f.(fn_code)) c) ls0
                    (mk_load_frame ls3 (transf_function f')), m')
  | match_states_in:
      forall s ls m ts ls0 m' f,
      list_forall2 match_stackframes s ts ->
      match_locset ls ls0->
      Mem.extends m m'->
      match_states (Core_CallstateIn s (Internal f) ls (mk_load_frame ls f), m)
                   (Core_CallstateIn ts (transf_fundef (Internal f)) ls0 (mk_load_frame ls0 (transf_function f)), m')
  | match_states_call:
      forall s ls m ts ls0 m' fd f0 ls2 ls3,
      list_forall2 match_stackframes s ts ->
      match_locset ls ls0->
      Mem.extends m m'->
      match_locset ls2 ls3 ->
      match_states (Core_Callstate s fd ls (mk_load_frame ls2 f0), m)
                   (Core_Callstate ts (transf_fundef fd) ls0 (mk_load_frame ls3 (transf_function f0)), m')
  | match_states_return:
      forall s ls m ts ls0 m' f ls2 ls3,
      list_forall2 match_stackframes s ts ->
      match_locset ls ls0 ->
      Mem.extends m m' ->
      match_locset ls2 ls3 ->
      match_states (Core_Returnstate s ls (mk_load_frame ls2 f), m)
                   (Core_Returnstate ts ls0 (mk_load_frame ls3 (transf_function f)), m').
Definition measure (st: core) : nat :=
  match st with
  | Core_State s f sp c ls m => List.length c
  | _ => O
  end.
Definition MS (_ : bool) n mu fp fp' cm cm': Prop :=
  match_states cm cm' /\
  Injections.FPMatch' mu fp fp' /\
  let (c, m) := cm in
  let (c', m') := cm' in
  (forall b, Bset.belongsto (Injections.SharedSrc mu) b -> Mem.valid_block m b) /\
  (forall b, Bset.belongsto (Injections.SharedTgt mu) b -> Mem.valid_block m' b) /\
  (proper_mu sge tge inject_id mu) /\
  (MemClosures_local.unmapped_closed mu m m') /\
  n = measure c /\ true = true.
Ltac invMS :=
  match goal with
  | H: MS _ _ _ _ _ ?cm1 ?cm2 |- _ =>
    destruct cm1 as [sc Hm]; destruct cm2 as [tc Lm];
    unfold MS in H; simpl in H;
    destruct H as [MS [FPMATCH [SVALID [TVALID [AGMU [RCPRESV [INDEX FLAG]]]]]]]
  | H: MS _ _ _ _ _ ?cm1 ?cm2 |- _ =>
    unfold MS in H; simpl in H;
    destruct H as [MS [FPMATCH [SVALID [TVALID [AGMU [RCPRESV [INDEX FLAG]]]]]]]
  end.
Lemma match_parent_locset:
  forall s ts,
  list_forall2 match_stackframes s ts ->
  match_locset (parent_locset s) (parent_locset ts).
Lemma val_lessdef_list_refl: forall s, Val.lessdef_list s s.
Lemma v_v0_inj_refl: forall mu v v0,
Val.inject (Bset.inj_to_meminj (Injections.inj mu)) v v0 ->
LDSimDefs.G_arg (Injections.SharedSrc mu) v ->
inject_incr (Bset.inj_to_meminj (Injections.inj mu)) inject_id -> v = v0.
Lemma same_val_from_matchlocset : forall mu rp rs rs1,
LDSimDefs.G_arg (Injections.SharedSrc mu) (get_result rp rs) ->
match_locset rs rs1 ->
Some (get_result rp rs1) = Some (get_result rp rs).
Lemma set_locset_lessdef:
  forall ls ls' v v' l,
    match_locset ls ls' -> Val.lessdef v v' ->
    match_locset (Locations.Locmap.set l v ls) (Locations.Locmap.set l v' ls').
Lemma setpair_locset_lessdef:
  forall ls ls' v v' l,
    match_locset ls ls' -> Val.lessdef v v' ->
    match_locset (Locations.Locmap.setpair l v ls) (Locations.Locmap.setpair l v' ls').
Lemma undef_locset_lessdef:
  forall ls ls' rl,
    match_locset ls ls' -> match_locset (LTL.undef_regs rl ls) (LTL.undef_regs rl ls').
Lemma call_locset_lessdef:
  forall ls ls',
    match_locset ls ls' ->
    match_locset (LTL.call_regs ls) (LTL.call_regs ls').
Lemma remove_unused_labels_cons:
  forall bto i c,
  remove_unused_labels bto (i :: c) =
  match i with
  | Llabel lbl =>
      if Labelset.mem lbl bto then i :: remove_unused_labels bto c else remove_unused_labels bto c
  | _ =>
      i :: remove_unused_labels bto c
  end.
Lemma lessdef_list : forall rs ls0 args,
match_locset rs ls0 ->
Val.lessdef_list (LTL.reglist rs args) (LTL.reglist ls0 args).
Lemma find_function_lessdef:
  forall ros ls tfd ls',
    find_function sge ros ls = Some tfd -> match_locset ls ls' ->
    find_function sge ros ls' = Some tfd.
Lemma return_locset_lessdef:
  forall ls ls0 ls' ls0',
    match_locset ls ls' -> match_locset ls0 ls0' ->
    match_locset (LTL.return_regs ls0 ls) (LTL.return_regs ls0' ls').
Lemma setres_locset_lessdef:
  forall res ls ls' vres vres',
    match_locset ls ls' ->
    Val.lessdef vres vres' ->
    match_locset (Locations.Locmap.setres res vres ls)
                   (Locations.Locmap.setres res vres' ls').
Lemma match_locset0: forall s ts rs0,
list_forall2 match_stackframes s ts ->
match_locset (parent_locset0 rs0 s) (parent_locset0 rs0 ts).

Lemma match_locset0_match_ld : forall locset_inv1 locset_inv2 s ts,
match_locset locset_inv1 locset_inv2 ->
list_forall2 match_stackframes s ts ->
match_locset (parent_locset0 locset_inv1 s) (parent_locset0 locset_inv2 ts).
Definition instr_branches_to (i: instruction) (lbl: label) : Prop :=
  match i with
  | Lgoto lbl' => lbl = lbl'
  | Lcond cond args lbl' => lbl = lbl'
  | Ljumptable arg tbl => In lbl tbl
  | _ => False
  end.
Remark add_label_branched_to_incr:
  forall ls i, Labelset.Subset ls (add_label_branched_to ls i).
Remark add_label_branched_to_contains:
  forall ls i lbl, instr_branches_to i lbl -> Labelset.In lbl (add_label_branched_to ls i).
Lemma labels_branched_to_correct:
  forall c i lbl,
  In i c -> instr_branches_to i lbl -> Labelset.In lbl (labels_branched_to c).
Lemma find_label_commut:
  forall lbl bto, Labelset.In lbl bto ->
  forall c c', find_label lbl c = Some c' ->
  find_label lbl (remove_unused_labels bto c) = Some (remove_unused_labels bto c').
Corollary find_label_translated:
  forall f i c' lbl c,
  incl (i :: c') (fn_code f) ->
  find_label lbl (fn_code f) = Some c ->
  instr_branches_to i lbl ->
  find_label lbl (fn_code (transf_function f)) =
     Some (remove_unused_labels (labels_branched_to (fn_code f)) c).
Lemma find_label_incl:
  forall lbl c c', find_label lbl c = Some c' -> incl c' c.
Lemma find_function_temp : forall locset_inv1 locset_inv2 f' loc,
match_locset locset_inv1 locset_inv2 ->
Genv.find_funct sge (locset_inv1 loc) = Some f' ->
Genv.find_funct tge (locset_inv2 loc) = Some (transf_fundef f').
Lemma find_function_matchlocset : forall locset_inv1 locset_inv2 locset_src locset_tgt s ts ros f',
match_locset locset_inv1 locset_inv2 ->
match_locset locset_src locset_tgt ->
list_forall2 match_stackframes s ts ->
find_function sge ros (LTL.return_regs (parent_locset0 locset_inv1 s) locset_src) = Some f' ->
(find_function tge ros (LTL.return_regs (parent_locset0 locset_inv2 ts) locset_tgt) =
 Some (transf_fundef f')).
Lemma incl_less : forall a b f,
incl (a::b) f.(fn_code) -> incl b f.(fn_code).
Lemma incl_rel : forall a,
incl a.(fn_code) a.(fn_code).
Lemma locset_lessdef_args:
  forall ls ls' args,
    match_locset ls ls' ->
    Val.lessdef_list (map (fun p : rpair Locations.loc => Locations.Locmap.getpair p ls) args)
                     (map (fun p : rpair Locations.loc => Locations.Locmap.getpair p ls') args).
Lemma fp_matchemp : forall mu Hfp Lfp,
 Injections.FPMatch' mu Hfp Lfp ->
 Injections.FPMatch' mu (FP.union Hfp empfp) (FP.union Lfp empfp).
Lemma valid_block_sm' : forall mu sm tm sm' tm',
mem_init_inj mu sm tm ->
LDefs.HLRely mu sm sm' tm tm' ->
forall b0 : block, Bset.belongsto (Injections.SharedSrc mu) b0 -> Mem.valid_block sm' b0 /\
forall b0 : block, Bset.belongsto (Injections.SharedTgt mu) b0 -> Mem.valid_block tm' b0.

Ltac resolvfp:=
  match goal with
  | |- context[FP.union _ empfp] => rewrite FP.fp_union_emp; resolvfp
  | |- context[FP.union empfp _] => rewrite FP.emp_union_fp; resolvfp
  | H: Some _ = Some _ |- _ => inv H; resolvfp
  | H: FP.subset ?fp1' ?fp1 |- Injections.FPMatch' ?mu (FP.union ?fp1 _) (FP.union ?fp1' _) =>
    eapply Injections.fp_match_union'; resolvfp
  | H: Injections.FPMatch' _ ?fp1 ?fp1' |- Injections.FPMatch' ?mu (FP.union ?fp1 _) (FP.union ?fp1' _) =>
    eapply Injections.fp_match_union'; auto; resolvfp
  | H: Injections.FPMatch' _ ?fp1 ?fp1' |- Injections.FPMatch' ?mu (FP.union ?fp1 _) ?fp1' =>
    eapply Injections.fp_match_union_S'; auto; resolvfp
  | H: FP.subset ?fp1' ?fp1 |- FP.subset (FP.union ?fp1' _) (FP.union ?fp1 _) =>
    eapply FP.subset_parallel_union; resolvfp
  | H: FP.subset ?fp1' ?fp1 |- FP.subset (FP.union ?fp1' _) (FP.union (FP.union ?fp1 _) _) =>
    eapply FP.subset_parallel_union; resolvfp
  | H: FP.subset ?fp1' ?fp1 |- FP.subset (FP.union (FP.union ?fp1' _) _) (FP.union (FP.union ?fp1 _) _)=>
    eapply FP.subset_parallel_union; resolvfp
  | H: FP.subset ?fp ?fp' |- FP.subset ?fp (FP.union ?fp1 ?fp') =>
    rewrite FP.union_comm_eq; resolvfp
  | H: FP.subset ?fp ?fp' |- FP.subset ?fp (FP.union ?fp' _) =>
    apply FP.subset_union_subset; auto
  | |- Injections.FPMatch' _ _ empfp => apply Injections.fp_match_emp'
  | H: FP.subset ?fp1 ?fp2 |- Injections.FPMatch' _ ?fp2 ?fp1 =>
    apply Injections.fp_match_subset_T' with fp2; try exact H; resolvfp
  | H: FP.subset ?fp2 ?fp1 |- Injections.FPMatch' _ (FP.union ?fp1 _) ?fp2 =>
    apply Injections.fp_match_union_S'; resolvfp
  | H: FP.subset ?fp2 ?fp1 |- Injections.FPMatch' _ ?fp1 (FP.union ?fp2 _) =>
    apply Injections.fp_match_union_T'; resolvfp
  | H: FP.subset ?fp2 ?fp1 |- Injections.FPMatch' _ ?fp1 (FP.union (FP.union ?fp2 _) _) =>
    apply Injections.fp_match_union_T'; resolvfp
  | H: FP.subset ?fp2 ?fp1 |- Injections.FPMatch' _ (FP.union ?fp1 _) (FP.union (FP.union ?fp2 _) _) =>
    apply Injections.fp_match_union'; resolvfp
  | H: (forall b, Bset.belongsto (FP.blocks ?fp2) _ -> ~ Injections.SharedTgt ?mu _)
    |- Injections.FPMatch' _ _ ?fp2 =>
    apply Injections.fp_match_local_block; auto
  | |- FP.subset ?fp ?fp => apply FP.subset_refl
  | H: fp_inject _ ?fp ?fp', H': proper_mu _ _ _ _ |- Injections.FPMatch' _ ?fp ?fp' =>
    eapply fp_inject_fp_match; inv H'; eauto
  | H: fp_inject inject_id ?fp ?fp'|- FP.subset ?fp' ?fp =>
    apply fp_inject_id_fp_subset
  | H: proper_mu _ _ _ _ |- Injections.FPMatch' _ ?fp ?fp => inv H; eapply fp_match_id; eauto
  | _ => idtac
  end.

Ltac eresolvfp:= resolvfp; eauto.

Ltac resvalid:=
  match goal with
  | H: (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m1 x), H': Mem.free ?m1 _ _ _ = Some ?m2
    |- (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m2 x)
    => let X := fresh in
      intros ? X; apply H in X; eapply Mem.valid_block_free_1; eauto
  | H: (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m1 x), H': Mem.alloc ?m1 _ _ = (?m2,_)
    |- (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m2 x)
    => let X := fresh in
      intros ? X; apply H in X; eapply Mem.valid_block_alloc; eauto
  | H: (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m1 x), H': Mem.store _ ?m1 _ _ _ = Some ?m2
    |- (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m2 x)
    => let X := fresh in
      intros ? X; apply H in X; eapply Mem.store_valid_block_1; eauto
  | H: (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m1 x),
    H1: LDefs.Rely ?S ?m1 ?m2
    |- (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m2 x)
    => intros ? X; unfold Mem.valid_block in *; apply H in X; inversion H1 as [EQNEXT ? ?]; rewrite EQNEXT;auto
  | H1: Mem.store _ ?m1 _ _ _ = Some ?m2,
        H2: Mem.store _ ?m1' _ _ _ = Some ?m2',
            H3: proper_mu _ _ _ _
    |- MemClosures_local.unmapped_closed _ ?m2 ?m2'
    => inv H3; eapply MemClosures_local.store_val_inject_unmapped_closed_preserved;
      try (rewrite Z.add_0_r); try eassumption;
      try (compute; eauto; fail); try omega
  | H1: Mem.free ?m1 _ _ _ = Some ?m2,
        H2: Mem.free ?m1' _ _ _ = Some ?m2',
            H3: proper_mu _ _ _ _
    |- MemClosures_local.unmapped_closed _ ?m2 ?m2'
    => inv H3; eapply MemClosures_local.free_inject_unmapped_closed_preserved; eauto;
      try (rewrite Z.add_0_r); try eassumption;
      try (compute; eauto; fail); try omega
  | H1: Mem.alloc ?m1 _ _ = (?m2, _),
        H2: Mem.alloc ?m1' _ _ = (?m2', _),
            H3: proper_mu _ _ _ _
    |- MemClosures_local.unmapped_closed _ ?m2 ?m2'
    => inv H3; eapply MemClosures_local.unchanged_on_unmapped_closed_preserved; eauto;
      try (eapply Mem.alloc_unchanged_on; eauto; fail)
  | _ => idtac
  end.

Ltac Ex_index :=
  match goal with
  | |- context[Core_State ?s ?f ?sp ?pc ?rs] => exists (measure (Core_State s f sp pc rs))
  | |- context[Core_Callstate] => exists 0%nat
  | |- context[Core_Returnstate ?s ?v] => exists (measure (Core_Returnstate s v))
  end.
Ltac Right := right; do 4 eexists; split; [apply plus_one|resolvfp].
Ltac FP:= match goal with |- ?P /\ _ => assert P; [eresolvfp| try (split;[auto; fail|])] end.
Ltac Left := left; Ex_index; split; [auto|eresolvfp].
Ltac splitMS :=
  split;
  [econstructor; eresolvfp |
   split; [eresolvfp|
           split; [try resvalid; auto |
                   split; [try resvalid; auto
                          |split; [auto|
                                   split; [try resvalid; eauto|
                                           split; eauto]]]]]].
Ltac inv_eq:=
  repeat match goal with
         | H:?P , H1: ?P |- _ => clear H
         | H: context[match ?x with _ => _ end] |- _ => destruct x eqn:?; inversion H ;subst
         | H:?P = ?Q, H1:context [ ?P ] |- _ => rewrite H in H1
         | H:?P = ?Q |- context [ ?P ] => rewrite H
         end;
  simpl in *;subst;try contradiction;try discriminate.
Ltac Hsimpl:=
  repeat match goal with
         | H1:?a,H2:?a->?b|-_=>specialize (H2 H1)
         | H:_/\_|-_=> destruct H
         | H:exists _,_|-_=>destruct H
         end.
Ltac Esimpl:=
  repeat match goal with
         | H:_|-_/\_=>split
         | H:_|-exists _,_=>eexists
         end.

Ltac resolv_ls :=
  match goal with
  | |- match_locset (Locations.Locmap.set _ _ _) (Locations.Locmap.set _ _ _) =>
    apply set_locset_lessdef; auto; resolv_ls
  | |- match_locset (LTL.undef_regs _ _) (LTL.undef_regs _ _) =>
    apply undef_locset_lessdef; auto; resolv_ls
  | |- match_locset (LTL.return_regs _ _) (LTL.return_regs _ _) =>
    apply return_locset_lessdef; auto; resolv_ls
  | |- match_locset (LTL.call_regs _ _) (LTL.return_regs _ _) =>
    apply call_locset_lessdef; auto; resolv_ls
  | |- match_locset (Locations.Locmap.setres _ _ _) (Locations.Locmap.setres _ _ _) =>
    apply setres_locset_lessdef; auto; resolv_ls
  | |- match_locset (Locations.Locmap.setpair _ _ _) (Locations.Locmap.setpair _ _ _) =>
    apply setpair_locset_lessdef; auto; resolv_ls
  | _ => idtac
  end.
Lemma val_inject_proper_mu : forall mu l,
    proper_mu sge tge inject_id mu -> LDSimDefs.G_arg (Injections.SharedSrc mu) l->
    Val.inject (Bset.inj_to_meminj (Injections.inj mu)) l l.
Lemma match_loc_inject_list: forall mu l1 l2,
  proper_mu sge tge inject_id mu ->
  LDSimDefs.G_args (Injections.SharedSrc mu) l1 ->
  Val.lessdef_list l1 l2 ->
  Val.inject_list (Bset.inj_to_meminj (Injections.inj mu)) l1 l2.
Lemma cleanuplabels_local_ldsim:
  @local_ldsim_properties Linear_IS Linear_IS nat lt sge tge sge tge MS.
End PRESERVATION.
Theorem transf_local_ldsim:
  forall su tu,
    cleanuplabels.transf_program su = OK tu->
    forall sge sG tge tG,
      init_genv_local Linear_IS su sge sG-> init_genv_local Linear_IS tu tge tG->
      Genv.genv_next sge = Genv.genv_next tge-> local_ldsim sG tG sge tge.