Lvc.TrueLiveness
Require Import AllInRel List Map Env DecSolve.
Require Import IL Annotation AutoIndTac Bisim Exp MoreExp Filter.
Require Export Liveness.
Set Implicit Arguments.
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_exp_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.
Lemma argsLive_liveSound lv blv Y Z
: argsLive lv blv Y Z
→ ∀ (n : nat) (y : exp),
get (filter_by (fun y : var ⇒ B[y ∈ blv]) Z Y) n y →
live_exp_sound y lv.
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_exp_sound y lv.
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 (exp_eval E) Y = Some v
→ omap (exp_eval E´) Y = Some v´
→ agree_on eq blv (V [Z <-- List.map Some v]) (V [Z <-- List.map Some v´]).
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 (exp_eval E) Y = Some v
→ omap (exp_eval E´) Y = Some v´
→ agree_on eq blv (V [Z <-- List.map Some v]) (V´ [Z <-- List.map Some v´]).
Inductive true_live_sound (i:overapproximation)
: list (set var ×params) → stmt → ann (set var) → Prop :=
| TLOpr x Lv b lv e al
: true_live_sound i Lv b al
→ (x ∈ getAnn al → live_exp_sound e lv)
→ (getAnn al\{{x}}) ⊆ lv
→ true_live_sound i Lv (stmtLet x e b) (ann1 lv al)
| TLIf Lv e b1 b2 lv al1 al2
: true_live_sound i Lv b1 al1
→ true_live_sound i Lv b2 al2
→ (exp2bool e = None → live_exp_sound e lv)
→ (exp2bool e ≠ Some false → getAnn al1 ⊆ lv)
→ (exp2bool e ≠ Some true → getAnn al2 ⊆ lv)
→ true_live_sound i Lv (stmtIf e b1 b2) (ann2 lv al1 al2)
| TLGoto l Y Lv lv blv Z
: get Lv (counted l) (blv,Z)
→ (if isImperative i then (blv \ of_list Z ⊆ lv) else True)
→ argsLive lv blv Y Z
→ length Y = length Z
→ true_live_sound i Lv (stmtApp l Y) (ann0 lv)
| TLReturn Lv e lv
: live_exp_sound e lv
→ true_live_sound i Lv (stmtReturn e) (ann0 lv)
| TLExtern x Lv b lv Y al f
: true_live_sound i Lv b al
→ (∀ n y, get Y n y → live_exp_sound y lv)
→ (getAnn al\{{x}}) ⊆ lv
→ true_live_sound i Lv (stmtExtern x f Y b) (ann1 lv al)
| TLLet Lv s Z b lv als alb
: true_live_sound i ((getAnn als,Z)::Lv) s als
→ true_live_sound i ((getAnn als,Z)::Lv) b alb
→ (if isFunctional i then (getAnn als \ of_list Z ⊆ lv) else True)
→ getAnn alb ⊆ lv
→ true_live_sound i Lv (stmtFun Z s b)(ann2 lv als alb).
Lemma true_live_sound_overapproximation_I Lv s slv
: true_live_sound FunctionalAndImperative Lv s slv → true_live_sound Imperative Lv s slv.
Lemma true_live_sound_overapproximation_F Lv s slv
: true_live_sound FunctionalAndImperative Lv s slv → true_live_sound Functional Lv s slv.
Lemma true_live_sound_annotation i Lv s slv
: true_live_sound i Lv s slv → annotation s slv.
Require Import IL Annotation AutoIndTac Bisim Exp MoreExp Filter.
Require Export Liveness.
Set Implicit Arguments.
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_exp_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.
Lemma argsLive_liveSound lv blv Y Z
: argsLive lv blv Y Z
→ ∀ (n : nat) (y : exp),
get (filter_by (fun y : var ⇒ B[y ∈ blv]) Z Y) n y →
live_exp_sound y lv.
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_exp_sound y lv.
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 (exp_eval E) Y = Some v
→ omap (exp_eval E´) Y = Some v´
→ agree_on eq blv (V [Z <-- List.map Some v]) (V [Z <-- List.map Some v´]).
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 (exp_eval E) Y = Some v
→ omap (exp_eval E´) Y = Some v´
→ agree_on eq blv (V [Z <-- List.map Some v]) (V´ [Z <-- List.map Some v´]).
Inductive true_live_sound (i:overapproximation)
: list (set var ×params) → stmt → ann (set var) → Prop :=
| TLOpr x Lv b lv e al
: true_live_sound i Lv b al
→ (x ∈ getAnn al → live_exp_sound e lv)
→ (getAnn al\{{x}}) ⊆ lv
→ true_live_sound i Lv (stmtLet x e b) (ann1 lv al)
| TLIf Lv e b1 b2 lv al1 al2
: true_live_sound i Lv b1 al1
→ true_live_sound i Lv b2 al2
→ (exp2bool e = None → live_exp_sound e lv)
→ (exp2bool e ≠ Some false → getAnn al1 ⊆ lv)
→ (exp2bool e ≠ Some true → getAnn al2 ⊆ lv)
→ true_live_sound i Lv (stmtIf e b1 b2) (ann2 lv al1 al2)
| TLGoto l Y Lv lv blv Z
: get Lv (counted l) (blv,Z)
→ (if isImperative i then (blv \ of_list Z ⊆ lv) else True)
→ argsLive lv blv Y Z
→ length Y = length Z
→ true_live_sound i Lv (stmtApp l Y) (ann0 lv)
| TLReturn Lv e lv
: live_exp_sound e lv
→ true_live_sound i Lv (stmtReturn e) (ann0 lv)
| TLExtern x Lv b lv Y al f
: true_live_sound i Lv b al
→ (∀ n y, get Y n y → live_exp_sound y lv)
→ (getAnn al\{{x}}) ⊆ lv
→ true_live_sound i Lv (stmtExtern x f Y b) (ann1 lv al)
| TLLet Lv s Z b lv als alb
: true_live_sound i ((getAnn als,Z)::Lv) s als
→ true_live_sound i ((getAnn als,Z)::Lv) b alb
→ (if isFunctional i then (getAnn als \ of_list Z ⊆ lv) else True)
→ getAnn alb ⊆ lv
→ true_live_sound i Lv (stmtFun Z s b)(ann2 lv als alb).
Lemma true_live_sound_overapproximation_I Lv s slv
: true_live_sound FunctionalAndImperative Lv s slv → true_live_sound Imperative Lv s slv.
Lemma true_live_sound_overapproximation_F Lv s slv
: true_live_sound FunctionalAndImperative Lv s slv → true_live_sound Functional Lv s slv.
Lemma true_live_sound_annotation i Lv s slv
: true_live_sound i Lv s slv → annotation s slv.