Lvc.ConstantPropagationAnalysis
Require Import CSet Le.
Require Import Plus Util AllInRel CSet.
Require Import Val Var Env EnvTy IL Annotation Lattice DecSolve Analysis Filter Lattice.
Require Import CMap.
Set Implicit Arguments.
Open Scope map_scope.
Definition Dom := Map [var, withTop val].
Definition join (v v´ : option (withTop val)) : option (withTop val) :=
match v, v´ with
| Some (wTA v), Some (wTA v´) ⇒ if [v = v´] then Some (wTA v) else Some Top
| Some (Top), _ ⇒ Some Top
| _, Some Top ⇒ Some Top
| Some (wTA v), None ⇒ Some (wTA v)
| None, Some (wTA v) ⇒ Some (wTA v)
| None, None ⇒ None
end.
Definition joinDom (d d´:Dom) : Dom := map2 join d d´.
Definition domain {X} `{OrderedType X} {Y} (d:Map [X, Y])
: set X := of_list (List.map fst (elements d)).
Inductive le : option (withTop val) → option (withTop val) → Prop :=
| leTop v : le (Some (wTA v)) (Some Top)
| leBot w : le None (Some w)
| leRefl v : le v v.
Instance le_dec x y : Computable (le x y).
Defined.
Lemma not_le_irreflexive x y
: ¬le x y → x ≠ y.
Instance le_find_dec d d´ x : Computable ((fun x0 : var ⇒ le (find x0 d) (find x0 d´)) x).
Definition leDom (d d´: Dom) : Prop :=
(∀ x, x ∈ domain d ∪ domain d´ → le (find x d) (find x d´)).
Lemma leDom_irreflexive x y
: ¬leDom x y → ¬Equal x y.
Definition set_quant_dec X `{OrderedType X} s P `{Proper _ (_eq ==> iff) P} `{∀ x, Computable (P x) } : bool :=
SetInterface.fold (fun x b ⇒ if [P x] then b else false) s true.
Instance set_quant_computable X `{OrderedType X} s P `{Proper _ (_eq ==> iff) P}
`{∀ x, Computable (P x) } :
Computable (∀ x, x ∈ s → P x).
Instance leDom_dec
: ∀ d d´ : Dom, Computable (leDom d d´).
Instance Equal_computable (s t:Map [var, withTop val])
: Computable (Equal s t).
Defined.
Lemma not_domain_find {X} `{OrderedType X} {Y} (d:Map [X, Y]) x
: x ∉ domain d → find x d = None.
Lemma findA_get A B (L:list (A × B)) f v
: findA f L = Some v
→ ∃ x n, get L n x ∧ snd x = v ∧ f (fst x).
Transparent compare. Qed.
Lemma InA_map X Y (R:X→X→Prop) (R´:Y→Y→Prop) `{Reflexive _ R´} (f:Y→X) L x
: InA R x (List.map f L)
→ ∃ y, InA R´ y L ∧ R x (f y).
Lemma domain_find {X} `{OrderedType X} {Y} (d:Map [X, Y]) x
: x ∈ domain d → ∃ v, find x d = Some v.
Lemma lt_join x y x´ y´
: le y x
→ le y´ x´
→ le (join y y´) (join x x´).
Lemma join_bot_right (y:Dom) x0
: join (find x0 y) ⎣⎦ = find x0 y.
Lemma join_bot_left (y:Dom) x0
: join ⎣⎦ (find x0 y) = find x0 y.
Lemma leDom_join x y x´ y´
: leDom y x
→ leDom y´ x´
→ leDom (joinDom y y´) (joinDom x x´).
Set Implicit Arguments.
Instance Dom_semilattice_ltDom : PartialOrder Dom := {
poLe := leDom;
poLe_dec := leDom_dec;
poEq := Equal;
poEq_dec := _
}.
Instance set_var_semilattice : BoundedSemiLattice Dom := {
bottom := (@empty var _ _ (withTop val));
join := joinDom
}.
Qed.
Fixpoint list_update_at {X} (L:list X) (n:nat) (v:X) :=
match L, n with
| x::L, 0 ⇒ v::L
| x::L, S n ⇒ x::list_update_at L n v
| _, _ ⇒ nil
end.
Lemma list_update_at_length X (l:list X) off v
: length (list_update_at l off v) = length l.
Lemma list_update_at_get_1 X (l:list X) off v v´ n
: get (list_update_at l off v´) n v
→ n ≠ off
→ get l n v.
Lemma list_update_at_get_2 X (l:list X) off v v´ n
: get (list_update_at l off v´) n v
→ n = off
→ v = v´.
Fixpoint update_with_list X `{OrderedType X} Y XL YL (m:Map [X, Y]) :=
match XL, YL with
| x::XL, y::YL ⇒ (update_with_list XL YL m)[x <- y]
| _, _ ⇒ m
end.
Local Notation "f [ w <-- x ]" := (update_with_list w x f) (at level 29, left associativity).
Definition domupd (d:Dom) x (o:option val) : Dom :=
match o with
| Some xv ⇒ (d [x <- wTA xv])
| None ⇒ (d [x <- Top])
end.
Definition domenv (d:Dom) (x:var) : option val :=
match find x d with
| Some (wTA v) ⇒ Some v
| _ ⇒ None
end.
Definition constant_propagation_transform st (a:list (Dom × params)×Dom) :=
match st, a with
| stmtLet x e s as st, (AL, d) ⇒
let d´ := d in
let d´´ := domupd d´ x (exp_eval (domenv d´) e) in
(AL, anni1 d´´)
| stmtIf e s t as st, (AL, d) ⇒
let ai :=
if [exp_eval (domenv d) e = Some val_true] then
match e with
| BinOp 3 (Var x) (Con c) ⇒ anni2opt (Some (d[x <- wTA c])) None
| _ ⇒ anni2opt (Some d) None
end
else if [exp_eval (domenv d) e = Some val_false] then
match e with
| Var x ⇒ anni2opt None (Some (d[x <- wTA 0]))
| _ ⇒ anni2opt None (Some d)
end
else
anni2opt (Some d) (Some d)
in
(AL, ai)
| stmtApp f Y as st, (AL, d) ⇒
let df := nth (counted f) AL (bottom, nil) in
let Yc := List.map (fun e ⇒ match exp_eval (domenv d) e with
| Some v ⇒ wTA v
| None ⇒ Top
end ) Y in
let d´ := (d [snd df <-- Yc]) in
(list_update_at AL (counted f) (joinDom (fst df) d´, snd df), anni1 d´)
| stmtReturn e as st, (AL, d) ⇒
(AL, anni1 d)
| stmtExtern x f Y s as st, (AL, d) ⇒
(AL, anni1 d)
| stmtFun Z s t as st, (AL, d) ⇒
(AL, anni2 d d)
end.
Instance list_equal_computable X `{@EqDec X eq _}
: ∀ (L L´:list X), Computable (eq L L´).
Instance Dom_params_semilattice : PartialOrder (Dom × params) := {
poLe p p´ := poLe (fst p) (fst p´) ∧ snd p = snd p´;
poLe_dec := _;
poEq p p´ := poEq (fst p) (fst p´) ∧ snd p = snd p´;
poEq_dec := _
}.
Defined.
Definition constant_propagation_analysis :=
SSA.makeForwardAnalysis _ Dom_params_semilattice constant_propagation_transform (fun Z an ⇒ (an, Z)) fst.
Require Import Plus Util AllInRel CSet.
Require Import Val Var Env EnvTy IL Annotation Lattice DecSolve Analysis Filter Lattice.
Require Import CMap.
Set Implicit Arguments.
Open Scope map_scope.
Definition Dom := Map [var, withTop val].
Definition join (v v´ : option (withTop val)) : option (withTop val) :=
match v, v´ with
| Some (wTA v), Some (wTA v´) ⇒ if [v = v´] then Some (wTA v) else Some Top
| Some (Top), _ ⇒ Some Top
| _, Some Top ⇒ Some Top
| Some (wTA v), None ⇒ Some (wTA v)
| None, Some (wTA v) ⇒ Some (wTA v)
| None, None ⇒ None
end.
Definition joinDom (d d´:Dom) : Dom := map2 join d d´.
Definition domain {X} `{OrderedType X} {Y} (d:Map [X, Y])
: set X := of_list (List.map fst (elements d)).
Inductive le : option (withTop val) → option (withTop val) → Prop :=
| leTop v : le (Some (wTA v)) (Some Top)
| leBot w : le None (Some w)
| leRefl v : le v v.
Instance le_dec x y : Computable (le x y).
Defined.
Lemma not_le_irreflexive x y
: ¬le x y → x ≠ y.
Instance le_find_dec d d´ x : Computable ((fun x0 : var ⇒ le (find x0 d) (find x0 d´)) x).
Definition leDom (d d´: Dom) : Prop :=
(∀ x, x ∈ domain d ∪ domain d´ → le (find x d) (find x d´)).
Lemma leDom_irreflexive x y
: ¬leDom x y → ¬Equal x y.
Definition set_quant_dec X `{OrderedType X} s P `{Proper _ (_eq ==> iff) P} `{∀ x, Computable (P x) } : bool :=
SetInterface.fold (fun x b ⇒ if [P x] then b else false) s true.
Instance set_quant_computable X `{OrderedType X} s P `{Proper _ (_eq ==> iff) P}
`{∀ x, Computable (P x) } :
Computable (∀ x, x ∈ s → P x).
Instance leDom_dec
: ∀ d d´ : Dom, Computable (leDom d d´).
Instance Equal_computable (s t:Map [var, withTop val])
: Computable (Equal s t).
Defined.
Lemma not_domain_find {X} `{OrderedType X} {Y} (d:Map [X, Y]) x
: x ∉ domain d → find x d = None.
Lemma findA_get A B (L:list (A × B)) f v
: findA f L = Some v
→ ∃ x n, get L n x ∧ snd x = v ∧ f (fst x).
Transparent compare. Qed.
Lemma InA_map X Y (R:X→X→Prop) (R´:Y→Y→Prop) `{Reflexive _ R´} (f:Y→X) L x
: InA R x (List.map f L)
→ ∃ y, InA R´ y L ∧ R x (f y).
Lemma domain_find {X} `{OrderedType X} {Y} (d:Map [X, Y]) x
: x ∈ domain d → ∃ v, find x d = Some v.
Lemma lt_join x y x´ y´
: le y x
→ le y´ x´
→ le (join y y´) (join x x´).
Lemma join_bot_right (y:Dom) x0
: join (find x0 y) ⎣⎦ = find x0 y.
Lemma join_bot_left (y:Dom) x0
: join ⎣⎦ (find x0 y) = find x0 y.
Lemma leDom_join x y x´ y´
: leDom y x
→ leDom y´ x´
→ leDom (joinDom y y´) (joinDom x x´).
Set Implicit Arguments.
Instance Dom_semilattice_ltDom : PartialOrder Dom := {
poLe := leDom;
poLe_dec := leDom_dec;
poEq := Equal;
poEq_dec := _
}.
Instance set_var_semilattice : BoundedSemiLattice Dom := {
bottom := (@empty var _ _ (withTop val));
join := joinDom
}.
Qed.
Fixpoint list_update_at {X} (L:list X) (n:nat) (v:X) :=
match L, n with
| x::L, 0 ⇒ v::L
| x::L, S n ⇒ x::list_update_at L n v
| _, _ ⇒ nil
end.
Lemma list_update_at_length X (l:list X) off v
: length (list_update_at l off v) = length l.
Lemma list_update_at_get_1 X (l:list X) off v v´ n
: get (list_update_at l off v´) n v
→ n ≠ off
→ get l n v.
Lemma list_update_at_get_2 X (l:list X) off v v´ n
: get (list_update_at l off v´) n v
→ n = off
→ v = v´.
Fixpoint update_with_list X `{OrderedType X} Y XL YL (m:Map [X, Y]) :=
match XL, YL with
| x::XL, y::YL ⇒ (update_with_list XL YL m)[x <- y]
| _, _ ⇒ m
end.
Local Notation "f [ w <-- x ]" := (update_with_list w x f) (at level 29, left associativity).
Definition domupd (d:Dom) x (o:option val) : Dom :=
match o with
| Some xv ⇒ (d [x <- wTA xv])
| None ⇒ (d [x <- Top])
end.
Definition domenv (d:Dom) (x:var) : option val :=
match find x d with
| Some (wTA v) ⇒ Some v
| _ ⇒ None
end.
Definition constant_propagation_transform st (a:list (Dom × params)×Dom) :=
match st, a with
| stmtLet x e s as st, (AL, d) ⇒
let d´ := d in
let d´´ := domupd d´ x (exp_eval (domenv d´) e) in
(AL, anni1 d´´)
| stmtIf e s t as st, (AL, d) ⇒
let ai :=
if [exp_eval (domenv d) e = Some val_true] then
match e with
| BinOp 3 (Var x) (Con c) ⇒ anni2opt (Some (d[x <- wTA c])) None
| _ ⇒ anni2opt (Some d) None
end
else if [exp_eval (domenv d) e = Some val_false] then
match e with
| Var x ⇒ anni2opt None (Some (d[x <- wTA 0]))
| _ ⇒ anni2opt None (Some d)
end
else
anni2opt (Some d) (Some d)
in
(AL, ai)
| stmtApp f Y as st, (AL, d) ⇒
let df := nth (counted f) AL (bottom, nil) in
let Yc := List.map (fun e ⇒ match exp_eval (domenv d) e with
| Some v ⇒ wTA v
| None ⇒ Top
end ) Y in
let d´ := (d [snd df <-- Yc]) in
(list_update_at AL (counted f) (joinDom (fst df) d´, snd df), anni1 d´)
| stmtReturn e as st, (AL, d) ⇒
(AL, anni1 d)
| stmtExtern x f Y s as st, (AL, d) ⇒
(AL, anni1 d)
| stmtFun Z s t as st, (AL, d) ⇒
(AL, anni2 d d)
end.
Instance list_equal_computable X `{@EqDec X eq _}
: ∀ (L L´:list X), Computable (eq L L´).
Instance Dom_params_semilattice : PartialOrder (Dom × params) := {
poLe p p´ := poLe (fst p) (fst p´) ∧ snd p = snd p´;
poLe_dec := _;
poEq p p´ := poEq (fst p) (fst p´) ∧ snd p = snd p´;
poEq_dec := _
}.
Defined.
Definition constant_propagation_analysis :=
SSA.makeForwardAnalysis _ Dom_params_semilattice constant_propagation_transform (fun Z an ⇒ (an, Z)) fst.