Lvc.Liveness.TrueLiveness

Require Import Util LengthEq AllInRel Map Env DecSolve.
Require Import IL Annotation AutoIndTac Exp SetOperations.
Require Export Liveness Filter LabelsDefined OUnion.

Set Implicit Arguments.

Specification of True Liveness


Local Hint Resolve incl_empty minus_incl incl_right incl_left.

Inductive argsLive (Caller Callee:set var) : args params Prop :=
| AL_nil : argsLive Caller Callee nil nil
| AL_cons y z Y Z
  : argsLive Caller Callee Y Z
     (z Callee live_op_sound y Caller)
     argsLive Caller Callee (y::Y) (z::Z).

Lemma argsLive_length lv bv Y Z
  : argsLive lv bv Y Z
     length Y = length Z.
Proof.
  intros. general induction H; simpl; eauto.
Qed.

Hint Resolve argsLive_length : len.

Lemma argsLive_liveSound lv blv Y Z
  : argsLive lv blv Y Z
     (n : nat) (y : op),
      get (filter_by (fun y : varB[y blv]) Z Y) n y
      live_op_sound y lv.
Proof.
  intros. general induction H; simpl in × |- ×.
  - isabsurd.
  - decide (z blv); eauto.
    inv H1; eauto.
Qed.

Lemma argsLive_live_exp_sound lv blv Y Z y z n
  : argsLive lv blv Y Z
     get Y n y
     get Z n z
     z blv
     live_op_sound y lv.
Proof.
  intros. general induction n; inv H0; inv H1; inv H; intuition; eauto.
Qed.

Lemma live_exp_sound_argsLive lv blv Y Z
  : length Y = length Z
     ( n y z, get Y n y get Z n z z blv live_op_sound y lv)
     argsLive lv blv Y Z.
Proof.
  intros. length_equify.
  general induction H; eauto 20 using argsLive, get.
Qed.

Lemma argsLive_agree_on' (V E E':onv val) lv blv Y Z v v'
  : argsLive lv blv Y Z
      agree_on eq lv E E'
      omap (op_eval E) Y = Some v
      omap (op_eval E') Y = Some v'
      agree_on eq blv (V [Z <-- List.map Some v]) (V [Z <-- List.map Some v']).
Proof.
  intros. general induction H; simpl in × |- *; eauto.
  - monad_inv H2. monad_inv H3.
    decide (z blv).
    +erewrite <- op_eval_live in EQ0; eauto.
     × assert (x1 = x) by congruence.
        subst. simpl.
        eauto using agree_on_update_same, agree_on_incl.
    + eapply agree_on_update_dead_both; eauto.
Qed.

Lemma argsLive_agree_on (V V' E E':onv val) lv blv Y Z v v'
  : agree_on eq (blv \ of_list Z) V V'
     argsLive lv blv Y Z
     agree_on eq lv E E'
     omap (op_eval E) Y = Some v
     omap (op_eval E') Y = Some v'
     agree_on eq blv (V [Z <-- List.map Some v]) (V' [Z <-- List.map Some v']).
Proof.
  intros. etransitivity; eauto using argsLive_agree_on'.
  eapply update_with_list_agree; eauto with len.
Qed.

Lemma filter_by_incl_argsLive lv blv Y Z
  : Y = Z
     list_union (Op.freeVars filter_by (fun xif [x \In blv] then true else false) Z Y) lv
     argsLive lv blv Y Z.
Proof.
  intros LEN INCL. length_equify.
  general induction LEN; simpl in *; eauto using argsLive.
  - econstructor.
    + cases in INCL; try congruence; eauto.
      × eapply IHLEN. rewrite <- INCL.
        simpl List.map. rewrite list_union_cons. eauto with cset.
    + intros. cases in INCL.
      simpl List.map in INCL.
      rewrite list_union_cons in INCL.
      eapply live_op_sound_incl;[eapply Op.live_freeVars|].
      rewrite <- INCL. eauto with cset.
Qed.

The inductive predicate


Inductive true_live_sound (i:overapproximation)
  : list params list (set var) stmt ann (set var) Prop :=
| TLOpr ZL Lv x b lv e al
  : true_live_sound i ZL Lv b al
      (x getAnn al isCall e live_exp_sound e lv)
      (getAnn al\ singleton x) lv
      true_live_sound i ZL Lv (stmtLet x e b) (ann1 lv al)
| TLIf ZL Lv e b1 b2 lv al1 al2
  : (op2bool e Some false true_live_sound i ZL Lv b1 al1)
      (op2bool e Some true true_live_sound i ZL Lv b2 al2)
      (op2bool e = None live_op_sound e lv)
      (op2bool e Some false getAnn al1 lv)
      (op2bool e Some true getAnn al2 lv)
      true_live_sound i ZL Lv (stmtIf e b1 b2) (ann2 lv al1 al2)
| TLGoto ZL Lv l Y lv blv Z
  : get ZL (counted l) Z
     get Lv (counted l) blv
     (if isImperative i then (blv \ of_list Z lv) else True)
     argsLive lv blv Y Z
     length Y = length Z
     true_live_sound i ZL Lv (stmtApp l Y) (ann0 lv)
| TLReturn ZL Lv e lv
  : live_op_sound e lv
     true_live_sound i ZL Lv (stmtReturn e) (ann0 lv)
| TLLet ZL Lv F t lv als alt
  : true_live_sound i (fst F ++ ZL) (getAnn als ++ Lv) t alt
     length F = length als
     ( n Zs a, get F n Zs
                 get als n a
                 true_live_sound i (fst F ++ ZL) (getAnn als ++ Lv) (snd Zs) a)
     ( n Zs a, get F n Zs
                 get als n a
                 if isFunctional i then (getAnn a \ of_list (fst Zs)) lv
                 else True)
     getAnn alt lv
     true_live_sound i ZL Lv (stmtFun F t)(annF lv als alt).

Some properties of the predicate


Lemma true_live_sound_overapproximation_I ZL Lv s slv
  : true_live_sound FunctionalAndImperative ZL Lv s slv
     true_live_sound Imperative ZL Lv s slv.
Proof.
  intros. general induction H; simpl in × |- *; econstructor; simpl; eauto.
Qed.

Lemma true_live_sound_overapproximation_F ZL Lv s slv
  : true_live_sound FunctionalAndImperative ZL Lv s slv
     true_live_sound Functional ZL Lv s slv.
Proof.
  intros. general induction H; simpl in × |- *; econstructor; simpl; eauto.
Qed.

Lemma argsLive_monotone lv blv blv' Y Z
  : argsLive lv blv Y Z
     blv' blv
     argsLive lv blv' Y Z.
Proof.
  intros Args LE.
  general induction Args; eauto using argsLive.
Qed.

Lemma true_live_sound_monotone i ZL LV LV' s lv
: true_live_sound i ZL LV s lv
   PIR2 Subset LV' LV
   true_live_sound i ZL LV' s lv.
Proof.
  intros LS LE.
  general induction LS; simpl; eauto 20 using true_live_sound, PIR2_app.
  - PIR2_inv.
    econstructor; eauto.
    cases; eauto with cset.
    eauto using argsLive_monotone.
Qed.