Module SliceAgree

Lemmas about agreement between relevant variables.

Require Import Bool.
Require Import BinPos.
Require Import List.
Require Import TheoryList.
Require Import Arith.

Require Import Coqlib.
Require Import Integers.
Require Import Errors.
Require Import Globalenvs.
Require Import AST.
Require Import RTL.
Require Import Maps.
Require Import Registers.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Op.
Require Import Utils.

Require Import ValueAnalysis.
Require Import UtilTacs.
Require Import UtilLemmas.
Require Import UtilBase.
Require Import VarsUseDef.
Require Import RTLWfFunction.
Require Import RTLPaths.
Require Import SliceObs.
Require Import SliceRelVar.
Require Import SliceGen.
Require Import SliceObs_proof.
Require Import SliceRelVar_proof.
Require Import Sliceproof.
Require Import SliceRegVint.
Require Import Scope.

Section AGREE.

  Variable f : function.
  Variable fsc : Scope.family f.
  Variable exit_n : node.
  Variable reg_vint : reg.
  Hypothesis WFF: check_wf f = OK (exit_n, reg_vint).
  Variable nc : t_criterion.
  Variable sliced_f : function.
  Variable of : obs_function.
  Hypothesis FOK: slice_function f nc fsc exit_n reg_vint = OK (sliced_f, of).

  Notation nobs' := (nobs (_s_dobs of)).

  Hypothesis exit_no_succ:
    forall s, ~ succ_node f (_exit of) s.

  Notation slice_nodes := of.(_slice_nodes).
  Notation succ_node' := (succ_node f).
  Notation in_slice n := (In n of.(_slice_nodes)).
  Notation def' := (def f).
  Notation use' := (use f).
  Notation rvs := (_rvs of).

  Variable ge : genv.

  Notation exit_n' := (_exit of).
  Notation reg_vint' := (_reg_vint of).
  Notation valid_rs' := (valid_rs f reg_vint').

  Notation In_dec_node := (List.In_dec positive_eq_dec).

  Lemma reg_vint_eq:
    reg_vint' = reg_vint.
Proof.
    unfolds in WFF.
    optDecN WFF CONDS; trim.
    monadInv WFF.
    unfolds in FOK.
    monadInv FOK.
    unfolds in EQ0.
    monadInv EQ0.
    optDec EQ3; trim.
    optDec EQ3; trim.
    optDec EQ3; trim.
    inv EQ3; auto.
  Qed.

  Let EXIT_NO_SUCC : forall s : RTL.node, ~ succ_node' exit_n' s.
Proof.
    eapply exit_no_succ; eauto.
  Qed.

  Definition rvs_agree (n : node) (s : varset) (rs1 rs2 : regset) (m1 m2 : mem) : Prop :=
    valid_rs' n rs1 /\
    valid_rs' n rs2 /\
    Regset.For_all
    (fun x =>
      if positive_eq_dec x memvar then m1 = m2 else
        let r := var_to_reg x in
          rs1 # r = rs2 # r
    ) s.

  Lemma rvs_agree_refl:
    forall n s rs m,
      valid_rs' n rs ->
      rvs_agree n s rs rs m m.
Proof.
    intros.
    unfolds.
    repeat (split; auto).
    unfolds; intros.
    optDecG; auto.
  Qed.

  Lemma agree_preserves_slice_uses:
    forall n rs rs2 args m m2,
      in_slice n ->
      rvs_agree n (rvs n) rs rs2 m m2 ->
      (forall r, In r args -> Regset.In (reg_to_var r) (use' n)) ->
      rs ## args = rs2 ## args.
Proof.
    introsv IN_SLICE AGREE ALL_IN_USE.
    unfold Regmap.get.
    apply map_ext_In; intros.
    apply ALL_IN_USE in H.

    eapply in_slice_use_in_rvs in H; eauto.
    apply AGREE in H.
    optDec H.
    lia2.
    rewrite var_to_var in H. auto.
  Qed.

  Lemma agree_preserves_slice_eval_op:
    forall n rs rs2 m m2 args sp op _res _pc',
      (fn_code f) ! n = Some (Iop op args _res _pc') ->
      in_slice n ->
      rvs_agree n (rvs n) rs rs2 m m2 ->
      eval_operation ge sp op rs2 ## args m2 = eval_operation ge sp op rs ## args m.
Proof.
    introsv IOP IN_SLICE AGREE.
    assert (IN_USE: forall r, In r args -> Regset.In (reg_to_var r) (use' n)).
      intros.
      unfold use. rewrite IOP.
      destruct op; simpl; apply In_regs_to_vars in H; auto.
      destruct c; auto.
      apply Regset.add_2. asmp.
    destruct op; simpl; gen (agree_preserves_slice_uses _ _ _ args _ _ IN_SLICE AGREE);
      rewrite H; auto.
    destruct c; simpl; auto.
    assert (USES_MEM: Regset.In memvar (rvs n)).
      eapply in_slice_use_in_rvs; eauto.
      unfold use.
      rewrite IOP.
      apply Regset.add_1. refl.
    apply AGREE in USES_MEM.
    simpl in USES_MEM. inv USES_MEM.
    refl.
  Qed.

  Lemma agree_with_mem_eq:
    forall n rs rs2 m m2,
      rvs_agree n (rvs n) rs rs2 m m2 ->
      Regset.In memvar (rvs n) ->
        m = m2.
Proof.
    intros.
    apply H in H0; auto.
  Qed.

  Lemma eval_op_agree_succ_preserved:
    forall sp op rs args v pc res pc' rs' m m'
      (EVAL: eval_operation ge sp op rs ## args m = Some v)
      (DEFRES: def' pc = Regset.singleton (reg_to_var res))
      (SUCC: succ_node' pc pc')
      (NODEFMEM: ~ Regset.In memvar (def' pc))
      (AGREE: rvs_agree pc (rvs pc) rs rs' m m'),
      Regset.For_all
        (fun x =>
           if positive_eq_dec x memvar then m = m' else
             let r := var_to_reg x in
             (rs # res <- v) # r = (rs' # res <- v) # r
        ) (rvs pc').
Proof.
    intros.
    unfold rvs_agree, Regset.For_all in *; intros.
    destruct AGREE as [VRS [VRS' AGREE]].
    optDecG.
    subst. eapply not_in_def_implies_rvs with (n := pc) in H; eauto.
    apply AGREE in H; auto.
    destruct (positive_eq_dec res (var_to_reg x)).
    subst. repeat rewrite Regmap.gss; refl.
    eapply not_in_def_implies_rvs with (n := pc) in H; eauto.
    apply AGREE in H; auto.
    optDec H; trim.
    repeat rewrite Regmap.gso; auto.
    rewrite DEFRES.
    intro. apply regset_in_singleton_eq in H0.
    subst. rewrite var_to_var in n0.
    cong.
  Qed.

  Lemma agree_preserves_slice_load_eval_addr:
    forall n rs rs2 m m2 chunk addr sp args _dst _pc',
      (fn_code f) ! n = Some (Iload chunk addr args _dst _pc') ->
      in_slice n ->
      rvs_agree n (rvs n) rs rs2 m m2 ->
      eval_addressing ge sp addr rs2 ## args = eval_addressing ge sp addr rs ## args.
Proof.
    introsv I IN_SLICE AGREE.
    assert (IN_USE: forall r, In r args -> Regset.In (reg_to_var r) (use' n)).
      intros.
      unfold use. rewrite I.
      apply Regset.add_2. apply In_regs_to_vars; asmp.
    destruct addr; simpl;
      gen (agree_preserves_slice_uses _ _ _ args _ _ IN_SLICE AGREE);
      rewrite H; auto;
    unfold symbol_address; rewrite symbols_preserved; auto.
  Qed.

  Lemma agree_preserves_used_mem:
    forall pc rs rs' m m'
      (AGREE : rvs_agree pc (rvs pc) rs rs' m m')
      (PC_IN : in_slice pc)
      (USE : Regset.In memvar (use' pc)),
      m = m'.
Proof.
    intros.
    exploit in_slice_use_in_rvs; eauto; intros.
    apply AGREE in H.
    optDec H; trim.
  Qed.
 
  Lemma out_no_entry:
    forall n,
      ~ in_slice n ->
      n <> f.(fn_entrypoint).
Proof.
    intros.
    intro. subst n. apply H. eapply entry_in_slice; eauto.
  Qed.

  Lemma iop_out_preserves_agree:
    forall pc op args res pc' rs rs' m m' v
      (INST : (fn_code f) ! pc = Some (Iop op args res pc'))
      (PC_OUT: ~ in_slice pc)
      (AGREE : rvs_agree pc (rvs pc) rs rs' m m'),
      rvs_agree pc' (rvs pc') rs # res <- v rs' m m'.
Proof.
    intros.
    unfold rvs_agree, Regset.For_all in *.
    destruct AGREE as [VRS [VRS' AGREE]].
    split.
    dup PC_OUT NENTRY. apply out_no_entry in NENTRY.
    dup NENTRY V0.
    apply VRS in V0.
    assert (res <> reg_vint').
      intro. subst res.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      rewrite reg_vint_eq.
      apply regset_in_singleton.
    unfolds.
    intros.
    rewrite PMap.gso; auto.
    split.
    dup PC_OUT NENTRY. apply out_no_entry in NENTRY.
    dup NENTRY V0.
    apply VRS' in V0.
    assert (res <> reg_vint').
      intro. subst res.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      rewrite reg_vint_eq.
      apply regset_in_singleton.
    unfolds.
    auto.
    intros.
    optDecG.
    eapply not_in_slice_succ_rvs in H; eauto.
    apply AGREE in H.
    optDec H; trim.
    exists (Iop op args res pc'); split; simpl; eauto.
    destruct (positive_eq_dec res (var_to_reg x)); subst.
    eapply not_in_slice_succ_rvs in H; eauto.
    eapply not_in_slice_def_not_in_rvs in H; eauto; trim.
    unfold def; rewrite INST.
    rewrite reg_to_reg; auto.
    apply regset_in_singleton.
    exists (Iop op args (var_to_reg x) pc'); split; simpl; eauto.
    repeat rewrite Regmap.gso; auto.
    eapply not_in_slice_succ_rvs in H; eauto.
    apply AGREE in H.
    optDec H; trim.
    exists (Iop op args res pc'); split; simpl; eauto.
  Qed.

  Lemma load_in_preserves_agree:
    forall pc chunk addr args dst v pc' rs rs' m m'
      (PC_IN : in_slice pc)
      (INST : (fn_code f) ! pc = Some (Iload chunk addr args dst pc'))
      (AGREE : rvs_agree pc (rvs pc) rs rs' m m'),
      rvs_agree pc' (rvs pc') rs # dst <- v rs' # dst <- v m m'.
Proof.
    intros.
    unfold rvs_agree, Regset.For_all in *; intros.
    destruct AGREE as [VRS [VRS' AGREE]].
    assert (NENTRY: pc <> (fn_entrypoint f)).
      intro; subst pc; apply entry_inst in WFF; decs WFF; trim.
    split.
    dup NENTRY V0.
    apply VRS in V0.
    assert (dst <> reg_vint').
      intro. subst dst.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      rewrite reg_vint_eq.
      apply regset_in_singleton.
    unfolds.
    intros.
    rewrite PMap.gso; auto.
    split.
    dup NENTRY V0.
    apply VRS' in V0.
    assert (dst <> reg_vint').
      intro. subst dst.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      rewrite reg_vint_eq.
      apply regset_in_singleton.
    unfolds.
    intros.
    rewrite PMap.gso; auto.
    intros.
    optDecG; subst.
    eapply not_in_def_implies_rvs with (n := pc) in H; eauto.
    apply AGREE in H; auto.
    exists (Iload chunk addr args dst pc'); split; auto; simpl; auto.
    unfold def; rewrite INST.
    intro. apply regset_in_singleton_eq in H0. symmetry in H0. apply no_memvar_to_reg in H0. contra.
    destruct (positive_eq_dec (var_to_reg x) dst); subst.
    repeat rewrite Regmap.gss. refl.
    eapply not_in_def_implies_rvs with (n := pc) in H; eauto.
    apply AGREE in H. optDec H; trim.
    repeat rewrite Regmap.gso; auto.
    exists (Iload chunk addr args dst pc'); split; auto; simpl; auto.
    unfold def; rewrite INST.
    intro. apply regset_in_singleton_eq in H0. symmetry in H0. subst.
    rewrite var_to_var in n0. cong.
  Qed.

  Lemma load_out_preserves_agree:
    forall pc chunk addr args dst pc' rs rs' m m' v
      (INST : (fn_code f) ! pc = Some (Iload chunk addr args dst pc'))
      (PC_OUT: ~ in_slice pc)
      (AGREE : rvs_agree pc (rvs pc) rs rs' m m'),
      rvs_agree pc' (rvs pc') rs # dst <- v rs' m m'.
Proof.
    intros.
    unfold rvs_agree, Regset.For_all in *.
    destruct AGREE as [VRS [VRS' AGREE]].
    assert (NENTRY: pc <> (fn_entrypoint f)).
      intro; subst pc; apply entry_inst in WFF; decs WFF; trim.
    split.
    dup NENTRY V0.
    apply VRS in V0.
    assert (dst <> reg_vint').
      intro. subst dst.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      rewrite reg_vint_eq.
      apply regset_in_singleton.
    unfolds.
    intros.
    rewrite PMap.gso; auto.
    split.
    dup NENTRY V0.
    apply VRS' in V0.
    unfolds; auto.
    intros.
    optDecG.
    eapply not_in_slice_succ_rvs in H; eauto.
    apply AGREE in H.
    optDec H; trim.
    exists (Iload chunk addr args dst pc'); split; simpl; eauto.
    destruct (positive_eq_dec dst (var_to_reg x)); subst.
    eapply not_in_slice_succ_rvs in H; eauto.
    eapply not_in_slice_def_not_in_rvs in H; eauto; trim.
    unfold def; rewrite INST.
    rewrite reg_to_reg; auto.
    apply regset_in_singleton.
    exists (Iload chunk addr args (var_to_reg x) pc'); split; simpl; eauto.
    repeat rewrite Regmap.gso; auto.
    eapply not_in_slice_succ_rvs in H; eauto.
    apply AGREE in H.
    optDec H; trim.
    exists (Iload chunk addr args dst pc'); split; simpl; eauto.
  Qed.


  Lemma agree_preserves_slice_store_eval_addr:
    forall n rs rs2 m m2 chunk addr sp args _dst _pc',
      (fn_code f) ! n = Some (Istore chunk addr args _dst _pc') ->
      in_slice n ->
      rvs_agree n (rvs n) rs rs2 m m2 ->
      eval_addressing ge sp addr rs2 ## args = eval_addressing ge sp addr rs ## args.
Proof.
    introsv I IN_SLICE AGREE.
    assert (IN_USE: forall r, In r args -> Regset.In (reg_to_var r) (use' n)).
      intros.
      unfold use. rewrite I.
      apply Regset.add_2. apply In_regs_to_vars. right. asmp.
    destruct addr; simpl; gen (agree_preserves_slice_uses _ _ _ args _ _ IN_SLICE AGREE); rewrite H; auto.
  Qed.

  Lemma agree_preserves_storev:
    forall chunk addr args pc' n rs rs2 m m2 m' v src
      (INST: (fn_code f) ! n = Some (Istore chunk addr args src pc'))
      (PC_IN: in_slice n)
      (AGREE: rvs_agree n (rvs n) rs rs2 m m2)
      (STOREV: Mem.storev chunk m v rs # src = Some m'),
      Mem.storev chunk m2 v rs2 # src = Some m'.
Proof.
    intros.
    destruct AGREE as [VRS [VRS' AGREE]].
    assert (m = m2).
      apply (AGREE memvar).
      eapply in_slice_use_in_rvs; eauto.
      unfold use; rewrite INST.
      apply Regset.add_1; now auto.
    subst.
    unfolds in STOREV.
    destruct v; trim.
    simpl.
    unfold rvs_agree, Regset.For_all in AGREE.
    assert (Regset.In (reg_to_var src) (rvs n)).
      eapply in_slice_use_in_rvs; eauto.
      unfold use; rewrite INST.
      apply Regset.add_2. apply In_regs_to_vars. left; refl.
    apply AGREE in H.
    optDec H; trim.
    apply no_memvar_to_reg in e. contra.
    rewrite var_to_var in H. rewrite <- H. asmp.
  Qed.

  Lemma store_preserves_agree:
    forall pc chunk addr args src pc' rs rs' m m' m''
      (INST : (fn_code f) ! pc = Some (Istore chunk addr args src pc'))
      (AGREE : rvs_agree pc (rvs pc) rs rs' m m''),
      rvs_agree pc' (rvs pc') rs rs' m' m'.
Proof.
    intros.
    destruct AGREE as [VRS [VRS' AGREE]].
    assert (NENTRY: pc <> (fn_entrypoint f)).
      intro; subst pc; apply entry_inst in WFF; decs WFF; trim.
    split.
    dup NENTRY V0.
    apply VRS in V0.
    unfolds; auto.
    split.
    dup NENTRY V0.
    apply VRS' in V0.
    unfolds; auto.
    unfold rvs_agree, Regset.For_all in *; intros.
    destruct (In_dec_node pc slice_nodes) as [PC_IN | PC_OUT].
    Case "pc in slice".
      optDecG; trim.
      eapply not_in_def_implies_rvs with (n := pc) in H; eauto.
      apply AGREE in H. optDec H; trim.
      exists (Istore chunk addr args src pc'); split; auto.
      simpl; auto.
      unfold def; rewrite INST.
      intro.
      apply regset_in_singleton_eq in H0. contra.
    Case "~ pc in slice".
      eapply not_in_slice_succ_rvs with (n := pc) in H; eauto.
      dup H INRVS.
      apply AGREE in H.
      destruct (positive_eq_dec x 1); auto.
      exists (Istore chunk addr args src pc'); simpl; auto.
  Qed.

  Lemma store_preserves_agree':
    forall pc chunk addr args src pc' rs rs' m m' m''
      (INST : (fn_code f) ! pc = Some (Istore chunk addr args src pc'))
      (PC_OUT: ~ in_slice pc)
      (AGREE : rvs_agree pc (rvs pc) rs rs' m m''),
      rvs_agree pc' (rvs pc') rs rs' m' m''.
Proof.
    intros.
    destruct AGREE as [VRS [VRS' AGREE]].
    assert (NENTRY: pc <> (fn_entrypoint f)).
      intro; subst pc; apply entry_inst in WFF; decs WFF; trim.
    split.
    dup NENTRY V0.
    apply VRS in V0.
    unfolds; auto.
    split.
    dup NENTRY V0.
    apply VRS' in V0.
    unfolds; auto.
    unfold rvs_agree, Regset.For_all in *; intros.
    eapply not_in_slice_succ_rvs with (n := pc) in H; eauto.
    destruct (positive_eq_dec x 1); subst.
    SCase "memvar in rvs(pc)".
      eapply not_in_slice_def_not_in_rvs with (f := f) in H; eauto; trim.
      unfold def. rewrite INST.
      apply regset_in_singleton.
    SCase "x in rvs(pc)".
      apply AGREE in H.
      destruct (positive_eq_dec x 1); trim.
    exists (Istore chunk addr args src pc'); simpl.
    split; eauto.
  Qed.

  Lemma builtin_preserves_agree:
    forall pc ef args res pc' rs rs' m m' m'' v
      (PC_IN : in_slice pc)
      (INST : (fn_code f) ! pc = Some (Ibuiltin ef args res pc'))
      (AGREE : rvs_agree pc (rvs pc) rs rs' m m''),
      rvs_agree pc' (rvs pc') rs # res <- v rs' # res <- v m' m'.
Proof.
    intros.
    unfold rvs_agree, Regset.For_all in *.
    destruct AGREE as [VRS [VRS' AGREE]].
    assert (NENTRY: pc <> (fn_entrypoint f)).
      intro; subst pc; apply entry_inst in WFF; decs WFF; trim.
    split.
    dup NENTRY V0.
    apply VRS in V0.
    assert (res <> reg_vint').
      intro. subst res.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      destruct ef;
        try solve [apply Regset.add_2; rewrite reg_vint_eq; apply regset_in_singleton];
        solve [rewrite reg_vint_eq; apply regset_in_singleton].
    unfolds.
    intros.
    rewrite PMap.gso; auto.
    split.
    dup NENTRY V0.
    apply VRS' in V0.
    assert (res <> reg_vint').
      intro. subst res.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      destruct ef;
        try solve [apply Regset.add_2; rewrite reg_vint_eq; apply regset_in_singleton];
        solve [rewrite reg_vint_eq; apply regset_in_singleton].
    unfolds.
    intros.
    rewrite PMap.gso; auto.
    intros.
    optDecG; trim.
    destruct (positive_eq_dec res (var_to_reg x)); subst.
    repeat rewrite Regmap.gss; auto.
    eapply not_in_def_implies_rvs with (n := pc) in H; eauto.
    apply AGREE in H. optDec H; trim.
    repeat rewrite Regmap.gso; auto.
    exists (Ibuiltin ef args res pc'); split; auto.
    simpl; auto.
    unfold def; rewrite INST.
    intro.
    destruct ef;
      try solve [eapply Regset.add_3 in H0; eauto;
                 apply regset_in_singleton_eq in H0; subst; rewrite var_to_var in n0; cong];
    apply regset_in_singleton_eq in H0; subst; rewrite var_to_var in n0; cong.
  Qed.

  Definition is_builtin_annot ef :=
    match ef with
        | EF_annot _ _
        | EF_annot_val _ _ => True
        | _ => False
    end.

  Definition is_builtin_annot_dec ef : {is_builtin_annot ef} + {~is_builtin_annot ef}.
Proof.
    destruct ef; simpl; auto.
  Defined.

  Lemma annot_preserves_agree:
    forall pc ef args res pc' rs rs' m m' v
      (PC_IN : in_slice pc)
      (INST : (fn_code f) ! pc = Some (Ibuiltin ef args res pc'))
      (ISA : is_builtin_annot ef)
      (AGREE : rvs_agree pc (rvs pc) rs rs' m m'),
      rvs_agree pc' (rvs pc') rs # res <- v rs' # res <- v m m'.
Proof.
    intros pc ef args res pc' rs rs' m m' v PC_IN INST ISA AGREE.
    unfold rvs_agree, Regset.For_all in *.
    destruct AGREE as [VRS [VRS' AGREE]].
    assert (NENTRY: pc <> (fn_entrypoint f)).
      intro; subst pc; apply entry_inst in WFF; decs WFF; trim.
    split.
    dup NENTRY V0.
    apply VRS in V0.
    assert (res <> reg_vint').
      intro. subst res.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      destruct ef;
        try solve [apply Regset.add_2; rewrite reg_vint_eq; apply regset_in_singleton];
        solve [rewrite reg_vint_eq; apply regset_in_singleton].
    unfolds.
    intros.
    rewrite PMap.gso; auto.
    split.
    dup NENTRY V0.
    apply VRS' in V0.
    assert (res <> reg_vint').
      intro. subst res.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      destruct ef;
        try solve [apply Regset.add_2; rewrite reg_vint_eq; apply regset_in_singleton];
        solve [rewrite reg_vint_eq; apply regset_in_singleton].
    unfolds.
    intros.
    rewrite PMap.gso; auto.
    intros.
    optDecG; trim.
    eapply not_in_def_implies_rvs with (n := pc) in H; eauto.
    apply AGREE in H. optDec H; trim.
    exists (Ibuiltin ef args res pc'); split; auto.
    unfold def; rewrite INST.
    intro.
    destruct ef; eauto;
      apply regset_in_singleton_eq in H0; subst;
      exploit Psucc_not_one; eauto.

    destruct (positive_eq_dec res (var_to_reg x)).
    subst res.
    repeat rewrite PMap.gss; auto.
    repeat rewrite PMap.gso; auto.
    eapply not_in_def_implies_rvs with (n := pc) in H; eauto.
    apply AGREE in H. optDec H; trim.
    exists (Ibuiltin ef args res pc'); split; auto.
    unfold def; rewrite INST.
    intro.
    destruct ef;
      try solve [eapply Regset.add_3 in H0; eauto;
                 apply regset_in_singleton_eq in H0; subst; rewrite var_to_var in n0; cong];
    apply regset_in_singleton_eq in H0; subst; rewrite var_to_var in n0; cong.
  Qed.

  Lemma annot_preserves_agree':
    forall pc ef args res pc' rs rs' m m' v
      (PC'_OUT : ~ in_slice pc)
      (ISA : is_builtin_annot ef)
      (INST : (fn_code f) ! pc = Some (Ibuiltin ef args res pc'))
      (AGREE : rvs_agree pc (rvs pc) rs rs' m m'),
      rvs_agree pc' (rvs pc') rs # res <- v rs' m m'.
Proof.
    unfold rvs_agree, Regset.For_all in *.
    intros.
    destruct AGREE as [VRS [VRS' AGREE]].
    assert (NENTRY: pc <> (fn_entrypoint f)).
      intro; subst pc; apply entry_inst in WFF; decs WFF; trim.
    split.
    dup NENTRY V0.
    apply VRS in V0.
    assert (res <> reg_vint').
      intro. subst res.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      destruct ef;
        try solve [apply Regset.add_2; rewrite reg_vint_eq; apply regset_in_singleton];
        solve [rewrite reg_vint_eq; apply regset_in_singleton].
    unfolds.
    intros.
    rewrite PMap.gso; auto.
    split.
    dup NENTRY V0.
    apply VRS' in V0.
    assert (res <> reg_vint').
      intro. subst res.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      destruct ef;
        try solve [apply Regset.add_2; rewrite reg_vint_eq; apply regset_in_singleton];
        solve [rewrite reg_vint_eq; apply regset_in_singleton].
    unfolds; auto.
    intros.
    destruct (positive_eq_dec x 1); subst.
    Case "x = 1 (trivial)".
      eapply not_in_slice_succ_rvs in H; eauto.
      apply AGREE in H; auto.
      eexists; eauto.
    Case "x <> 1".
      eapply not_in_slice_succ_rvs in H; eauto.
      destruct (positive_eq_dec res (var_to_reg x)); subst.
      SCase "res = var_to_reg x (contradiction)".
        eapply not_in_slice_def_not_in_rvs with (f := f) in H; eauto; trim.
        unfold def; rewrite INST.
        rewrite reg_to_reg; auto.
        destruct ef; try apply Regset.add_2; apply regset_in_singleton.
      SCase "res <> var_to_reg x".
        repeat rewrite Regmap.gso; auto.
        apply AGREE in H.
        optDec H; trim.
      exists (Ibuiltin ef args res pc'); split; simpl; eauto.
  Qed.

  Lemma not_annot_preserves_agree':
    forall pc ef args res pc' rs rs' m m' m'' v t v'
      (PC'_OUT : ~ in_slice pc)
      (NOTA : ~ is_builtin_annot ef)
      (EF: external_call ef ge rs ## args m t v' m')
      (INST : (fn_code f) ! pc = Some (Ibuiltin ef args res pc'))
      (AGREE : rvs_agree pc (rvs pc) rs rs' m m''),
      rvs_agree pc' (rvs pc') rs # res <- v rs' m' m''.
Proof.
    unfold rvs_agree, Regset.For_all in *.
    intros.
    destruct AGREE as [VRS [VRS' AGREE]].
    assert (NENTRY: pc <> (fn_entrypoint f)).
      intro; subst pc; apply entry_inst in WFF; decs WFF; trim.
    split.
    dup NENTRY V0.
    apply VRS in V0.
    assert (res <> reg_vint').
      intro. subst res.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      destruct ef;
        try solve [apply Regset.add_2; rewrite reg_vint_eq; apply regset_in_singleton];
        solve [rewrite reg_vint_eq; apply regset_in_singleton].
    unfolds.
    intros.
    rewrite PMap.gso; auto.
    split.
    dup NENTRY V0.
    apply VRS' in V0.
    assert (res <> reg_vint').
      intro. subst res.
      assert (FIN: f_In pc f) by (intro; trim).
      eapply def_rvint_entry in FIN; eauto.
      unfold def.
      rewrite INST.
      destruct ef;
        try solve [apply Regset.add_2; rewrite reg_vint_eq; apply regset_in_singleton];
        solve [rewrite reg_vint_eq; apply regset_in_singleton].
    unfolds; auto.
    intros.
    destruct (positive_eq_dec x 1); subst.
    Case "x = 1 (contradiction)".
      eapply in_slice_mem_def with (n := pc) in H; eauto.
      contra.
      exists (Ibuiltin ef args res pc'); split; simpl; eauto.
      unfold def; rewrite INST.
      destruct ef; try (apply Regset.add_1; refl).
      eelim NOTA; simpl; eauto.
      eelim NOTA; simpl; eauto.
      eapply not_in_slice_succ_rvs; eauto.
      exists (Ibuiltin ef args res pc'); split; simpl; eauto.
    Case "x <> 1".
      eapply not_in_slice_succ_rvs in H; eauto.
      destruct (positive_eq_dec res (var_to_reg x)); subst.
      SCase "res = var_to_reg x (contradiction)".
        eapply not_in_slice_def_not_in_rvs with (f := f) in H; eauto; trim.
        unfold def; rewrite INST.
        rewrite reg_to_reg; auto.
        destruct ef; try apply Regset.add_2; apply regset_in_singleton.
      SCase "res <> var_to_reg x".
        repeat rewrite Regmap.gso; auto.
        apply AGREE in H.
        optDec H; trim.
      exists (Ibuiltin ef args res pc'); split; simpl; eauto.
  Qed.

  Lemma agree_preserves_external_call':
    forall pc ef args t v res pc' rs rs' m m' m''
      (PC_IN : in_slice pc)
      (INST : (fn_code f) ! pc = Some (Ibuiltin ef args res pc'))
      (AGREE : rvs_agree pc (rvs pc) rs rs' m m'')
      (EXT: external_call ef ge rs ## args m t v m'),
      match ef with
          | EF_annot _ _
          | EF_annot_val _ _ =>
            external_call ef ge rs' ## args m'' t v m''
          | _ => external_call ef ge rs' ## args m'' t v m'
      end.
Proof.
    intros.
    dup AGREE AGREE'.
    destruct AGREE as [VRS [VRS' AGREE]].
    destruct (is_builtin_annot_dec ef) as [ISA|NOTA].
    Case "is_builtin_annot".
      unfolds in ISA. destruct ef; trim; inv EXT;
      erewrite <- agree_preserves_slice_uses; eauto.
      constructor; auto.
      intros. unfold use; rewrite INST. apply In_regs_to_vars; auto.
      rewrite <- H.
      constructor; auto.
      intros. unfold use; rewrite INST. apply In_regs_to_vars; auto.
    Case "~ is_builtin_annot".
      assert (m = m'').
        apply (AGREE memvar).
        eapply in_slice_use_in_rvs; eauto.
        unfold use; rewrite INST.
        destruct ef; try (apply Regset.add_1; now auto); elim NOTA; simpl; auto.
      subst.
      gen (agree_preserves_slice_uses pc rs rs' args m'' m'' PC_IN AGREE').
      rewrite <- H.
      destruct ef; apply external_call_symbols_preserved with (F1 := fundef) (ge1 := ge); auto;
      inv EXT; constructor; auto.
      intros.
      unfold use; rewrite INST.
      destruct ef; try apply Regset.add_2; apply In_regs_to_vars; auto.
  Qed.

Definition is_const_icond (i : instruction) : bool :=
  match i with
    | Icond cond args _ _ =>
      match cond with
          | Cmaskzero i =>
            match args with
              | nil => false
              | x :: nil => Int.eq_dec i Int.zero && positive_eq_dec x reg_vint'
              | _ => false
            end
          | Cmasknotzero i =>
            match args with
              | nil => false
              | x :: nil => Int.eq_dec i Int.zero && positive_eq_dec x reg_vint'
              | _ => false
            end
          | _ => false
      end
    | _ => false
  end.

Lemma const_eval_cond:
  forall
    rs rs' m m' n cond args ifso ifnot
    (INST: (fn_code f) ! n = Some (Icond cond args ifso ifnot)),
    is_const_icond (Icond cond args ifso ifnot) = true ->
    rvs_agree n (rvs n) rs rs' m m' ->
    eval_condition cond rs' ## args m' = eval_condition cond rs ## args m.
Proof.
  introsv INST CONST AGREE; intros.
  assert (IN_USE: forall r, In r args -> Regset.In (reg_to_var r) (use' n)).
    intros.
    unfold use. rewrite INST.
    destruct cond; simpl; try optDecG; try subst i;
    apply In_regs_to_vars in H; auto; unfolds in CONST; try projInv CONST.
    apply Regset.add_2; auto.
  unfolds in AGREE.
  destruct AGREE as [VRS [VRS' AGREE]].
  unfold valid_rs in *.
  simpls.
  destruct cond; trim; destruct args; trim; destruct args; trim;
  boolrw; destruct CONST; projInv H; projInv H0; subst r i; simpls.
  destruct (positive_eq_dec n (fn_entrypoint f)).
  subst n.
  apply entry_inst in WFF. decs WFF.
  rewrite H1 in INST; trim.
  rewrite VRS; auto; rewrite VRS'; auto.
  destruct (positive_eq_dec n (fn_entrypoint f)).
  subst n.
  apply entry_inst in WFF. decs WFF.
  rewrite H1 in INST; trim.
  simpls.
  rewrite VRS; auto; rewrite VRS'; auto.
Qed.

Lemma const_eval_not_cond:
  forall n rs rs2 m m2 args cond ifso ifnot,
    is_const_icond (Icond cond args ifso ifnot) = false ->
    (fn_code f) ! n = Some (Icond cond args ifso ifnot) ->
    in_slice n ->
    rvs_agree n (rvs n) rs rs2 m m2 ->
    eval_condition cond rs2 ## args m2 = eval_condition cond rs ## args m.
Proof.
  introsv NCONST IOP IN_SLICE AGREE.
  assert (IN_USE: forall r, In r args -> Regset.In (reg_to_var r) (use' n)).
    intros.
    unfold use. rewrite IOP.
    destruct cond; simpl; try optDecG; try subst i;
    apply In_regs_to_vars in H; auto; unfolds in NCONST; try projInv NCONST.
    apply Regset.add_2; auto.
  destruct cond; simpl;
  gen (agree_preserves_slice_uses _ _ _ args _ _ IN_SLICE AGREE);
  rewrite H; auto.
  assert (USES_MEM: Regset.In memvar (rvs n)).
    eapply in_slice_use_in_rvs; eauto.
    unfold use.
    rewrite IOP.
    apply Regset.add_1. refl.
  destruct c; simpl; auto;
  apply AGREE in USES_MEM;
  simpl in USES_MEM; inv USES_MEM;
  refl.
Qed.

Lemma agree_preserves_slice_eval_cond:
  forall n rs rs2 m m2 args cond ifso ifnot,
    (fn_code f) ! n = Some (Icond cond args ifso ifnot) ->
    in_slice n ->
    rvs_agree n (rvs n) rs rs2 m m2 ->
    eval_condition cond rs2 ## args m2 = eval_condition cond rs ## args m.
Proof.
  introsv IOP IN_SLICE AGREE.
  case_eq (is_const_icond (Icond cond args ifso ifnot)); introsv CONST.
  eapply const_eval_cond; eauto.
  eapply const_eval_not_cond; eauto.
Qed.

Lemma eval_icond_true:
  forall
    pc rs m
    (VRS: valid_rs' pc rs)
    (NOENTRY: pc <> f.(fn_entrypoint)),
    eval_condition (Cmaskzero Int.zero) rs ## (reg_vint' :: nil) m = Some true.
Proof.
  intros.
  unfolds in VRS.
  apply VRS in NOENTRY.
  simpl.
  rewrite NOENTRY; auto.
Qed.

Lemma eval_icond_false:
  forall
    pc rs m
    (VRS: valid_rs' pc rs)
    (NOENTRY: pc <> f.(fn_entrypoint)),
    eval_condition (Cmasknotzero Int.zero) rs ## (reg_vint' :: nil) m = Some false.
Proof.
  intros.
  unfolds in VRS.
  apply VRS in NOENTRY.
  simpl.
  rewrite NOENTRY; auto.
Qed.

Lemma jumptable_preserves_agree:
  forall n rs rs2 m m2 arg tbl,
    (fn_code f) ! n = Some (Ijumptable arg tbl) ->
    in_slice n ->
    rvs_agree n (rvs n) rs rs2 m m2 ->
    rs2 # arg = rs # arg.
Proof.
  introsv IOP IN_SLICE AGREE.
  assert (IN_USE: Regset.In (reg_to_var arg) (use' n)).
    intros.
    unfold use. rewrite IOP.
    apply regset_in_singleton.
  eapply in_slice_use_in_rvs in IN_USE; eauto.
  apply AGREE in IN_USE.
  optDec IN_USE.
  apply no_memvar_to_reg in e. contra.
  rewrite var_to_var in IN_USE.
  symmetry. asmp.
Qed.

Lemma succ_no_def_agree:
  forall n s rs rs2 m m2,
    rvs_agree n (rvs n) rs rs2 m m2 ->
    succ_node' n s ->
    def' n = Regset.empty ->
    rvs_agree s (rvs s) rs rs2 m m2.
Proof.
  introsv AGREE SUCC DEF_EMPTY.
  unfold rvs_agree, Regset.For_all in *.
  destruct AGREE as [VRS [VRS' AGREE]].
  assert (NENTRY: n <> (fn_entrypoint f)).
    intro; subst n; apply entry_inst in WFF; decs WFF.
    unfold def in DEF_EMPTY.
    rewrite H in DEF_EMPTY; trim.
  split.
  dup NENTRY V0.
  apply VRS in V0.
  unfolds; auto.
  split.
  dup NENTRY V0.
  apply VRS' in V0.
  unfolds; auto.
  introsv IN_RVS_S.
  eapply not_in_def_implies_rvs with (n := n) in IN_RVS_S; eauto.
  apply AGREE; auto.
  unfold def in *.
  destruct ((fn_code f) ! n); try destruct i; intro; trim;
  rewrite DEF_EMPTY in H; trim.
Qed.

End AGREE.
Generated by coq2html