Lvc.Liveness

Require Import AllInRel List Map Env DecSolve.
Require Import IL Annotation AutoIndTac Bisim Exp MoreExp Filter.

Set Implicit Arguments.

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
    | Functional ⇒ true
    | FunctionalAndImperative ⇒ true
    | _ ⇒ false
  end.

Definition isImperative (o:overapproximation) :=
  match o with
    | Imperative ⇒ true
    | FunctionalAndImperative ⇒ true
    | _ ⇒ false
  end.

Inductive Definition of Liveness

Inductive live_sound (i:overapproximation) : list (set var ×params) → stmt → ann (set var) → Prop :=
| LOpr x Lv b lv e (al:ann (set var))
  : live_sound i Lv b al
  → live_exp_sound e lv
  → (getAnn al \ singleton x ) ⊆ lv
  → x ∈ getAnn al
  → live_sound i Lv (stmtLet x e b) (ann1 lv al)
| LIf Lv e b1 b2 lv al1 al2
  : live_sound i Lv b1 al1
  → live_sound i Lv b2 al2
  → live_exp_sound e lv
  → getAnn al1 ⊆ lv
  → getAnn al2 ⊆ lv
  → live_sound i Lv (stmtIf e b1 b2) (ann2 lv al1 al2)
| LGoto l Y Lv lv blv Z
  : get Lv (counted l) (blv ,Z )

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_exp_sound y lv)
  → live_sound i Lv (stmtApp l Y) (ann0 lv)
| LReturn Lv e lv
  : live_exp_sound e lv
  → live_sound i Lv (stmtReturn e) (ann0 lv)
| LExtern x Lv b lv Y al f
  : live_sound i Lv b al
  → (∀ n y, get Y n y → live_exp_sound y lv)
  → (getAnn al \{{x }}) ⊆ lv
  → x ∈ getAnn al
  → live_sound i Lv (stmtExtern x f Y b) (ann1 lv al)
| LLet Lv s Z b lv als alb
  : live_sound i ((getAnn als ,Z )::Lv) s als
  → live_sound i ((getAnn als ,Z )::Lv) b alb
  → (of_list Z ) ⊆ getAnn als

Functional Liveness requires the globals of a function to be live at the definition (for building the closure)

  → (if isFunctional i then (getAnn als \ of_list Z ⊆ lv) else True)
  → getAnn alb ⊆ lv
  → live_sound i Lv (stmtFun Z s b)(ann2 lv als alb).

Relation between different overapproximations

Lemma live_sound_overapproximation_I Lv s slv
: live_sound FunctionalAndImperative Lv s slv → live_sound Imperative Lv s slv.

Lemma live_sound_overapproximation_F Lv s slv
: live_sound FunctionalAndImperative Lv s slv → live_sound Functional Lv s slv.

live_sound ensures that the annotation matches the program

Lemma live_sound_annotation i Lv s slv
: live_sound i Lv s slv → annotation s slv.

Some monotonicity properties

Definition live_ann_subset (lvZ lvZ´ : set var × list var) :=
  match lvZ, lvZ´ with
    | (lv,Z), (lv´,Z´) ⇒ lv´ ⊆ lv ∧ Z = Z´
  end.

Instance live_ann_subset_refl : Reflexive live_ann_subset.
Qed.

Lemma live_sound_monotone i LV LV´ s lv
: live_sound i LV s lv
  → PIR2 live_ann_subset LV LV´
  → live_sound i LV´ s lv.

Lemma live_sound_monotone2 i LV s lv a
: live_sound i LV s lv
  → getAnn lv ⊆ a
  → live_sound i LV s (setTopAnn lv a).

Live variables always contain the free variables

Lemma freeVars_live s lv Lv
: live_sound Functional Lv s lv → IL.freeVars s ⊆ getAnn lv.

Liveness is stable under renaming

Definition live_rename_L_entry (ϱ:env var) (x:set var × params)
:= (lookup_set ϱ (fst x), lookup_list ϱ (snd x)).

Definition live_rename_L (ϱ:env var) DL
:= List.map (live_rename_L_entry ϱ) DL.

Lemma live_rename_sound i DL s an (ϱ:env var)
: live_sound i DL s an
→ live_sound i (live_rename_L ϱ DL) (rename ϱ s) (mapAnn (lookup_set ϱ) an).

For functional programs, only free variables are significant

Inductive approxF : F.block → F.block → Prop :=
| approxFI E E´ Z s
    : agree_on eq (IL.freeVars s \ of_list Z) E E´
    → approxF (F.blockI E Z s) (F.blockI E´ Z s).

Inductive freeVarSimF : F.state → F.state → Prop :=
  freeVarSimFI (E E´:onv val) L L´ s
  (LA: PIR2 approxF L L´)
  (AG:agree_on eq (IL.freeVars s) E E´)
  : freeVarSimF (L , E , s ) (L´, E´, s ).

Lemma freeVarSimF_sim σ1 σ2
  : freeVarSimF σ1 σ2 → bisim σ1 σ2.

Since live variables contain free variables, liveness contains all variables significant to an IL/F program

Inductive approxF´ : list (set var × params) → F.block → F.block → Prop :=
  approxFI´ DL E E´ Z s lv
  : live_sound Functional ((getAnn lv , Z )::DL) s lv
    → agree_on eq (getAnn lv \ of_list Z) E E´
    → approxF´ ((getAnn lv ,Z )::DL) (F.blockI E Z s) (F.blockI E´ Z s).

Inductive liveSimF : F.state → F.state → Prop :=
  liveSimFI (E E´:onv val) L L´ s Lv lv
            (LS:live_sound Functional Lv s lv)
            (LA:AIR3 approxF´ Lv L L´)
            (AG:agree_on eq (getAnn lv) E E´)
  : liveSimF (L , E , s ) (L´, E´, s ).

Lemma liveSim_freeVarSim σ1 σ2
  : liveSimF σ1 σ2 → freeVarSimF σ1 σ2.

Live variables contain all variables significant to an IL/I program

Inductive approxI
  : list (set var × params) → I.block → I.block → Prop :=
  approxII DL Z s lv
  : live_sound Imperative ((getAnn lv , Z )::DL) s lv
    → approxI ((getAnn lv ,Z )::DL) (I.blockI Z s) (I.blockI Z s).

Inductive liveSimI : I.state → I.state → Prop :=
  liveSimII (E E´:onv val) L s Lv lv
  (LS:live_sound Imperative Lv s lv)
  (LA:AIR3 approxI Lv L L)
  (AG:agree_on eq (getAnn lv) E E´)
  : liveSimI (L , E , s ) (L , E´, s ).

Lemma liveSimI_sim σ1 σ2
  : liveSimI σ1 σ2 → bisim σ1 σ2.