Lvc.Liveness.Liveness

Require Import List Map Env AllInRel Exp Rename.
Require Import IL Annotation InRel AutoIndTac .

Set Implicit Arguments.

Notation "DL \\ ZL" := (zip (fun s Ls \ of_list L) DL ZL) (at level 50).

Local Hint Resolve incl_empty minus_incl incl_right incl_left.

Liveness

We have two flavors of liveness: functional and imperative. See comments in inductive definition live_sound.

Inductive overapproximation : Set
  := Functional | Imperative | FunctionalAndImperative.

Definition isFunctional (o:overapproximation) :=
  match o with
    | Functionaltrue
    | FunctionalAndImperativetrue
    | _false
  end.

Definition isImperative (o:overapproximation) :=
  match o with
    | Imperativetrue
    | FunctionalAndImperativetrue
    | _false
  end.

Inductive Definition of Liveness


Inductive live_sound (i:overapproximation)
  : list params list (set var) stmt ann (set var) Prop :=
| LOpr ZL Lv x e s lv (al:ann (set var))
  : live_sound i ZL Lv s al
      live_exp_sound e lv
      (getAnn al \ singleton x) lv
      x getAnn al
      live_sound i ZL Lv (stmtLet x e s) (ann1 lv al)
| LIf Lv ZL e s1 s2 lv al1 al2
  : live_sound i ZL Lv s1 al1
      live_sound i ZL Lv s2 al2
      live_op_sound e lv
      getAnn al1 lv
      getAnn al2 lv
      live_sound i ZL Lv (stmtIf e s1 s2) (ann2 lv al1 al2)
| LGoto ZL Lv l Y lv blv Z
  : get ZL (counted l) Z
     get Lv (counted l) blv
    
Imperative Liveness requires the globals of a function to be live at the call site
     (if isImperative i then ((blv \ of_list Z) lv) else True)
     length Y = length Z
     ( n y, get Y n y live_op_sound y lv)
     live_sound i ZL Lv (stmtApp l Y) (ann0 lv)
| LReturn ZL Lv e lv
  : live_op_sound e lv
     live_sound i ZL Lv (stmtReturn e) (ann0 lv)
| LLet ZL Lv F t lv als alb
  : live_sound i (fst F ++ ZL) (getAnn als ++ Lv) t alb
     length F = length als
     ( n Zs a, get F n Zs
                 get als n a
                 live_sound i (fst F ++ ZL) (getAnn als ++ Lv) (snd Zs) a)
     ( n Zs a, get F n Zs
                 get als n a
                 (of_list (fst Zs)) getAnn a
                  (if isFunctional i then (getAnn a \ of_list (fst Zs)) lv else True))
     getAnn alb lv
     live_sound i ZL Lv (stmtFun F t)(annF lv als alb).

Relation between different overapproximations


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

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

live_sound ensures that the annotation matches the program

Lemma live_sound_annotation i ZL Lv s slv
: live_sound i ZL Lv s slv annotation s slv.
Proof.
  intros. general induction H; econstructor; eauto.
Qed.

Some monotonicity properties


Lemma incl_incl_minus X `{OrderedType X} s t u v
  : t \ u v s t s \ u v.
Proof.
  intros A B. rewrite B; eauto.
Qed.

Lemma incl_minus_exp_live_union s t e v
  : s \ t v live_exp_sound e v s \ t Exp.freeVars e v.
Proof.
  intros. eauto using Exp.freeVars_live with cset.
Qed.

Hint Resolve incl_incl_minus incl_minus_exp_live_union : cset.

Hint Resolve incl_minus_lr : cset.

Lemma live_sound_monotone i ZL LV LV' s lv
: live_sound i ZL LV s lv
   PIR2 Subset LV' LV
   live_sound i ZL LV' s lv.
Proof.
  intros. general induction H; simpl; eauto using live_sound.
  - PIR2_inv.
    econstructor; eauto.
    cases; eauto with cset.
  - econstructor; eauto using PIR2_app.
Qed.

Lemma live_sound_monotone2 i ZL LV s lv a
: live_sound i ZL LV s lv
   getAnn lv a
   live_sound i ZL LV s (setTopAnn lv a).
Proof.
  intros. general induction H; simpl in × |- *;
            eauto using live_sound, live_op_sound_incl,
            live_exp_sound_incl, Subset_trans with cset.
  - econstructor; eauto using live_op_sound_incl.
    cases; eauto with cset.
  - econstructor; eauto with cset.
    + intros. edestruct H3; eauto.
      cases; eauto with cset.
Qed.

Live variables always contain the free variables


Lemma freeVars_live s lv ZL Lv
  : live_sound Functional ZL Lv s lv IL.freeVars s getAnn lv.
Proof.
  intros.
  induction H; simpl; eauto using Exp.freeVars_live, Op.freeVars_live,
                      Op.freeVars_live_list with cset.
  - eapply union_subset_3; eauto with cset.
    + eapply list_union_incl; intros; inv_get; eauto.
      edestruct H3; eauto; simpl in ×. exploit H2; eauto.
      eauto with cset.
Qed.

Liveness is stable under renaming


Lemma live_rename_sound i ZL Lv s an (ϱ:env var)
: live_sound i ZL Lv s an
   live_sound i (lookup_list ϱ ZL) (lookup_set ϱ Lv) (rename ϱ s) (mapAnn (lookup_set ϱ) an).
Proof.
  intros. general induction H; simpl.
  - econstructor; eauto using live_exp_rename_sound.
    + rewrite getAnn_mapAnn.
      rewrite <- lookup_set_singleton'; eauto.
      rewrite lookup_set_minus_incl; eauto.
      eapply lookup_set_incl; eauto.
    + rewrite getAnn_mapAnn.
      eapply lookup_set_spec; eauto.
  - econstructor; eauto using live_op_rename_sound.
    + rewrite getAnn_mapAnn. eapply lookup_set_incl; eauto.
    + rewrite getAnn_mapAnn. eapply lookup_set_incl; eauto.
  - econstructor; eauto with len.
    + cases; eauto.
      rewrite of_list_lookup_list; eauto.
      etransitivity. eapply lookup_set_minus_incl; eauto.
      eapply lookup_set_incl; eauto.
    + rewrite lookup_list_length; eauto with len.
    + intros; inv_get; eauto using live_op_rename_sound.
  - econstructor; eauto using live_op_rename_sound.
  - econstructor; eauto; try rewrite getAnn_mapAnn; eauto with len.
    + repeat rewrite map_map; simpl. rewrite <- map_map.
      rewrite <- map_app.
      setoid_rewrite getAnn_mapAnn.
      setoid_rewrite <- map_map at 3. rewrite <- map_app. eauto.
    + intros; inv_get. simpl.
      repeat rewrite map_map; simpl. rewrite <- map_map.
      rewrite <- map_app.
      setoid_rewrite getAnn_mapAnn.
      setoid_rewrite <- map_map at 3. rewrite <- map_app. eauto.
    + intros; inv_get; simpl.
      exploit H3; eauto; dcr. simpl.
      split.
      × rewrite of_list_lookup_list; eauto.
        rewrite getAnn_mapAnn.
        eapply lookup_set_incl; eauto.
      × cases; eauto.
        rewrite getAnn_mapAnn.
        rewrite of_list_lookup_list; eauto.
        rewrite lookup_set_minus_incl; eauto.
        eapply lookup_set_incl; eauto.
    + eapply lookup_set_incl; eauto.
Qed.