Module SliceRegVint

Some properties of well-formed functions.

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

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

Require Import Utils.
Require Import UtilTacs.
Require Import UtilBase.
Require Import UtilLemmas.
Require Import VarsUseDef.
Require Import RTLWfFunction.
Require Import RTLPaths.
Require Import CountingSem.
Require Import HeaderBounds.

Definition valid_rs (f : function) (reg_vint : reg) (pc : node) (rs : regset) :=
  pc <> f.(fn_entrypoint) -> rs # reg_vint = Vint Int.zero.

Lemma step_def_0:
  forall f fsc sp ge pc rs m cs rcs pc' rs' m' cs' rcs'
         (STEP: cstep ge f fsc sp (CST (State pc rs m) cs rcs) (CST (State pc' rs' m') cs' rcs'))
         (DEF: def f pc = Regset.empty),
    rs' = rs.

Proof.

  intros.
  unfold def in DEF.
  inv STEP. inv H3; auto.
  rewrite H4 in DEF. inv DEF.
  rewrite H5 in DEF. inv DEF.
  rewrite H4 in DEF.
  destruct ef; inv DEF; case_match (Ordered.OrderedPositive.compare 1%positive (reg_to_var res)) as COMP in H0; trim.
Qed.

Section WFF.

  Variable f: function.
  Variable exit_n : node.
  Variable reg_vint : reg.
  Hypothesis WFF: check_wf f = OK (exit_n, reg_vint).


  Lemma valid_rs_function_step:
    forall
      fsc sp ge pc rs m cs rcs pc' rs' m' cs' rcs'
      (VRS: valid_rs f reg_vint pc rs)
      (STEP: cstep ge f fsc sp (CST (State pc rs m) cs rcs) (CST (State pc' rs' m') cs' rcs')),
      valid_rs f reg_vint pc' rs'.

Proof.

    intros.
    unfold valid_rs in *.
    intro NENTRY.
    unfolds in WFF.
    optDecN WFF CONDS; trim.
    monadInv WFF. rename EQ1 into VRSF.
    unfolds in VRSF.
    optDecN VRSF EIN; trim.
    monadInv VRSF.
    optDecN EQ1 FOLD; trim.
    inv EQ1.
    assert (EX: exists i, f.(fn_code) ! pc = Some i).
      apply step_succ_node in STEP. apply succ_f_In in STEP. apply f_In_ex in STEP; auto.
    destruct EX as [i' INST'].
    apply forall_ptree_true with (i := pc) (x := i') in FOLD; auto.
    optDec FOLD.
    Case "pc = entrypoint".
      subst pc.
      unfolds in EQ0.
      destruct i; trim; destruct o; trim.
      optDec EQ0; trim.
      subst i.
      destruct l; trim.
      inv EQ0.
      inv STEP; trim. inv H3; trim.
      rewrite INST' in H4. inv H4; trim.
      rewrite EIN in INST'. inv INST'.
      simpls. inv H8.
      rewrite PMap.gss; auto.
    Case "pc <> entrypoint".
      rewrite negb_true_iff in FOLD.
      apply VRS in n.
      unfold def in FOLD.
      inv STEP; trim. inv H3; trim.
      SCase "Iop".
        destruct (positive_eq_dec res reg_vint).
        subst res.
        rewrite H4 in FOLD.
        apply Regset.MF.not_mem_iff in FOLD.
        exfalso. apply FOLD.
        apply regset_in_singleton.
        rewrite PMap.gso; auto.
      SCase "Iload".
        destruct (positive_eq_dec dst reg_vint).
        subst dst.
        unfold def in *.
        rewrite H5 in FOLD.
        apply Regset.MF.not_mem_iff in FOLD.
        exfalso. apply FOLD.
        apply regset_in_singleton.
        rewrite PMap.gso; auto.
      SCase "Ibuiltin".
        destruct (positive_eq_dec res reg_vint).
        subst res.
        unfold def in *.
        rewrite H4 in FOLD.
        apply Regset.MF.not_mem_iff in FOLD.
        exfalso. apply FOLD.
        destruct ef;
          solve [apply Regset.add_2; apply regset_in_singleton | apply regset_in_singleton].
        rewrite PMap.gso; auto.
  Qed.

  Lemma entry_inst:
    exists s,
      f.(fn_code) ! (fn_entrypoint f) = Some (Iop (Op.Ointconst Int.zero) nil reg_vint s).

Proof.

    intros.
    unfolds in WFF.
    optDecN WFF CONDS; trim.
    monadInv WFF. rename EQ1 into VRSF.
    unfolds in VRSF.
    optDecN VRSF EIN; trim.
    monadInv VRSF.
    optDecN EQ1 FOLD; trim.
    inv EQ1.
    eapply ptree_forall in FOLD; eauto.
    optDec FOLD; trim.
    unfolds in EQ0.
    destruct i; trim; destruct o; trim.
    optDec EQ0; trim.
    subst i.
    destruct l; trim.
    inv EQ0.
    exists n; auto.
  Qed.

  Lemma def_rvint_entry:
    forall n,
      f_In n f ->
      Regset.In (reg_to_var reg_vint) (def f n) ->
      n = f.(fn_entrypoint).

Proof.

    intros.
    unfolds in WFF.
    optDecN WFF CONDS; trim.
    monadInv WFF. rename EQ1 into VRSF.
    unfolds in VRSF.
    optDecN VRSF EIN; trim.
    monadInv VRSF.
    optDecN EQ1 FOLD; trim.
    inv EQ1.
    apply f_In_ex in H. destruct H as [i' INST].
    apply forall_ptree_true with (i := n) (x := i') in FOLD; auto.
    optDec FOLD; trim.
    rewrite negb_true_iff in FOLD.
    apply Regset.mem_1 in H0.
    trim.
  Qed.

  Lemma def_not_entry:
    forall n,
      f_In n f ->
      n <> f.(fn_entrypoint) ->
      ~ Regset.In (reg_to_var reg_vint) (def f n).

Proof.

    intros.
    unfolds in WFF.
    optDecN WFF CONDS; trim.
    monadInv WFF. rename EQ1 into VRSF.
    unfolds in VRSF.
    optDecN VRSF EIN; trim.
    monadInv VRSF.
    optDecN EQ1 FOLD; trim.
    inv EQ1.
    apply f_In_ex in H. destruct H as [i' INST'].
    eapply ptree_forall with (i := n) in FOLD; eauto.
    optDec FOLD; trim.
    boolrw.
    rewrite negb_true_iff in FOLD.
    intro CONTRA.
    apply Regset.mem_1 in CONTRA; trim.
  Qed.

End WFF.