Library AndersenIter
Require Import Arith List TheoryList.
Require Import ListUtil Tactics Maps.
Require Import Pointer Machine AndersenModel AndersenSound.
Lemma incl_add : forall s a,
AllocSet.incl s (AllocSet.add s a) = true.
Lemma incl_add2 : forall s1 s2 a,
AllocSet.incl s1 s2 = true
-> AllocSet.incl (AllocSet.add s1 a) (AllocSet.add s2 a) = true.
Hint Resolve incl_add2.
Lemma incl_union2 : forall s1 s2 s3 s4,
AllocSet.incl s1 s3 = true
-> AllocSet.incl s2 s4 = true
-> AllocSet.incl (AllocSet.union s1 s2)
(AllocSet.union s3 s4) = true.
Hint Resolve incl_union2.
Lemma incl_fold1 : forall (f : allocation_site -> AllocSet.set) x ls s,
AllocSet.In x (fold_left
(fun known site =>
AllocSet.union known (f site))
ls s) = true
-> (AllocSet.In x s = true
\/ exists y, In y ls /\ AllocSet.In x (f y) = true).
Lemma incl_fold2 : forall (f : allocation_site -> AllocSet.set) x ls s,
(AllocSet.In x s = true
\/ exists y, In y ls /\ AllocSet.In x (f y) = true)
-> AllocSet.In x (fold_left
(fun known site =>
AllocSet.union known (f site))
ls s) = true.
Lemma incl_elems : forall t1 t2 y,
AllocSet.incl t1 t2 = true
-> In y (AllocSet.elems t1)
-> In y (AllocSet.elems t2).
Lemma incl_fold_read : forall (f1 f2 : allocation_site -> AllocSet.set) s1 s2 t1 t2,
(forall a, AllocSet.incl (f1 a) (f2 a) = true)
-> AllocSet.incl s1 s2 = true
-> AllocSet.incl t1 t2 = true
-> AllocSet.incl
(fold_left
(fun known site =>
AllocSet.union known (f1 site))
(AllocSet.elems t1) s1)
(fold_left
(fun known site =>
AllocSet.union known (f2 site))
(AllocSet.elems t2) s2) = true.
Hint Resolve incl_fold_read.
Lemma incl_fold3' : forall a (f : allocation_site -> AllocSet.set) s ls h,
AllocMap.sel h a = AllocSet.union (f a) s
-> AllocMap.sel
(fold_left (fun known site =>
AllocMap.upd known site (AllocSet.union (f site) s))
ls h) a = AllocSet.union (f a) s.
Lemma incl_fold3 : forall f s a ls h,
if In_eq_dec eq_nat_dec a ls
then AllocMap.sel (fold_left (fun known site =>
AllocMap.upd known site (AllocSet.union (f site) s))
ls h) a = AllocSet.union (f a) s
else AllocMap.sel (fold_left (fun known site =>
AllocMap.upd known site (AllocSet.union (f site) s))
ls h) a = AllocMap.sel h a.
Lemma incl_fold_write : forall a s1 s2 t1 t2 h1 h2,
AllocSet.incl (AllocMap.sel h1 a) (AllocMap.sel h2 a) = true
-> AllocSet.incl s1 s2 = true
-> AllocSet.incl t1 t2 = true
-> AllocSet.incl
(AllocMap.sel (fold_left (fun known site =>
AllocMap.upd known site (AllocSet.union (AllocMap.sel h1 site) s1))
(AllocSet.elems t1) h1) a)
(AllocMap.sel (fold_left (fun known site =>
AllocMap.upd known site (AllocSet.union (AllocMap.sel h2 site) s2))
(AllocSet.elems t2) h2) a) = true.
Hint Resolve incl_fold_write.
Definition ins_sites i :=
match i with
| AbsAllocate _ site => AllocSet.add AllocSet.empty site
| _ => AllocSet.empty
end.
Module VarSet : SET with Definition dom := var := AllocSet.
Definition ins_vars i :=
match i with
| AbsAllocate v _ => VarSet.add VarSet.empty v
| AbsCopy v1 v2 => VarSet.add (VarSet.add VarSet.empty v1) v2
| AbsRead v1 v2 => VarSet.add (VarSet.add VarSet.empty v1) v2
| AbsWrite v1 v2 => VarSet.add (VarSet.add VarSet.empty v1) v2
end.
Section prog.
Variable program : list abstract_instruction.
Definition pSites := fold_left AllocSet.union (map ins_sites program).
Definition pVars := fold_left VarSet.union (map ins_vars program).
End prog.
Section fixed_point.
Variable program : list abstract_instruction.
Definition progSites := pSites program AllocSet.empty.
Definition progVars := pVars program VarSet.empty.
Record approx' (abs1 abs2 : abstract_state) : Prop := {
approxVars : forall v, AllocSet.incl
(VarMap.sel (avars abs1) v) (VarMap.sel (avars abs2) v) = true;
approxHeap : forall a, AllocSet.incl
(AllocMap.sel (aheap abs1) a) (AllocMap.sel (aheap abs2) a) = true
}.
Lemma increasing' : forall abs ins,
approx' abs (abstract_exec ins abs).
Lemma monotonic' : forall abs abs' ins,
approx' abs abs'
-> approx' (abstract_exec ins abs) (abstract_exec ins abs').
Lemma approx_refl' : forall s, approx' s s.
Lemma approx_trans' : forall s1 s2 s3,
approx' s1 s2 -> approx' s2 s3 -> approx' s1 s3.
Lemma approx_init' : forall s, approx' abstract_initState s.
Record valid (abs : abstract_state) : Prop := {
validVarsDom : forall v, VarSet.In v progVars = false
-> AllocSet.incl (VarMap.sel (avars abs) v) AllocSet.empty = true;
validHeapDom : forall a, AllocSet.In a progSites = false
-> AllocSet.incl (AllocMap.sel (aheap abs) a) AllocSet.empty = true;
validVars : forall v, AllocSet.incl (VarMap.sel (avars abs) v) progSites = true;
validHeap : forall a, AllocSet.incl (AllocMap.sel (aheap abs) a) progSites = true
}.
Definition astate := sig valid.
Definition approx (abs1 abs2 : astate) := approx' (proj1_sig abs1) (proj1_sig abs2).
Record approxStrict (abs1 abs2 : astate) : Prop := {
strictApprox : approx abs2 abs1;
strictNe : (exists v, VarSet.In v progVars = true
/\ AllocSet.incl (VarMap.sel (avars (proj1_sig abs1)) v)
(VarMap.sel (avars (proj1_sig abs2)) v) = false)
\/ exists a, AllocSet.In a progSites = true
/\ AllocSet.incl (AllocMap.sel (aheap (proj1_sig abs1)) a)
(AllocMap.sel (aheap (proj1_sig abs2)) a) = false
}.
Definition ainstruction := sig (fun ins => In ins program).
Lemma fold_In_union : forall a ls s,
AllocSet.In a s = true
-> AllocSet.In a (fold_left AllocSet.union ls s) = true.
Hint Resolve VarSet.incl_In VarSet.incl_union_left.
Lemma fold_In_unionv : forall a ls s,
VarSet.In a s = true
-> VarSet.In a (fold_left VarSet.union ls s) = true.
Lemma allocate_site : forall v a prog s,
In (AbsAllocate v a) prog
-> AllocSet.In a (pSites prog s) = true.
Lemma incl_add3 : forall x s1 s2,
AllocSet.In x s2 = true
-> AllocSet.incl s1 s2 = true
-> AllocSet.incl (AllocSet.add s1 x) s2 = true.
Lemma incl_union : forall s1 s2 s3,
AllocSet.incl s1 s3 = true
-> AllocSet.incl s2 s3 = true
-> AllocSet.incl (AllocSet.union s1 s2) s3 = true.
Lemma incl_valid_read : forall (f : allocation_site -> AllocSet.set) s2 ls s1,
AllocSet.incl s1 s2 = true
-> (forall site, AllocSet.incl (f site) s2 = true)
-> AllocSet.incl
(fold_left
(fun known site => AllocSet.union known (f site))
ls s1) s2 = true.
Lemma incl_valid_write : forall a s1 s2 f ls h,
AllocSet.incl s1 s2 = true
-> (forall a, AllocSet.incl (f a) s2 = true)
-> (forall a, AllocSet.incl (AllocMap.sel h a) s2 = true)
-> AllocSet.incl
(AllocMap.sel
(fold_left
(fun known site => AllocMap.upd known site
(AllocSet.union (f site) s1))
ls h) a)
s2 = true.
Hint Resolve VarSet.In_add_eq VarSet.In_add_neq VarSet.incl_union_right.
Lemma allocate_var : forall v a prog s,
In (AbsAllocate v a) prog
-> VarSet.In v (pVars prog s) = true.
Lemma copy_var : forall v a prog s,
In (AbsCopy v a) prog
-> VarSet.In v (pVars prog s) = true.
Lemma read_var : forall v a prog s,
In (AbsRead v a) prog
-> VarSet.In v (pVars prog s) = true.
Lemma write_var : forall v a prog s,
In (AbsWrite v a) prog
-> VarSet.In v (pVars prog s) = true.
Lemma sel_write_valid : forall f s a ls h,
AllocMap.sel
(fold_left (fun known site => AllocMap.upd known site
(AllocSet.union (f site) s))
ls h) a
= if In_eq_dec eq_nat_dec a ls
then AllocSet.union (f a) s
else AllocMap.sel h a.
Lemma aexec' : forall ins abs, In ins program -> valid abs -> valid (abstract_exec ins abs).
Definition aexec : ainstruction -> astate -> astate.
Definition ainitState : astate.
Lemma ainstr_widen : forall h t,
{ins : abstract_instruction | In ins t}
-> {ins : abstract_instruction | In ins (h :: t)}.
Definition aprogram' : forall (prog : list abstract_instruction),
list (sig (fun ins => In ins prog)).
Definition aprogram := aprogram' program.
Theorem increasing : forall abs ins,
approx abs (aexec ins abs).
Hint Resolve increasing.
Theorem monotonic : forall abs abs' ins,
approx abs abs'
-> approx (aexec ins abs) (aexec ins abs').
Hint Resolve monotonic.
Theorem approx_refl : forall s, approx s s.
Hint Resolve approx_refl.
Theorem approx_trans : forall s1 s2 s3,
approx s1 s2 -> approx s2 s3 -> approx s1 s3.
Hint Resolve approx_trans.
Theorem approx_init : forall s, approx ainitState s.
Hint Resolve approx_init.
Hint Resolve AllocSet.incl_empty.
Theorem approxStrict_approx : forall s1 s2,
approx s2 s1
-> ~approxStrict s1 s2
-> approx s1 s2.
Hint Resolve approxStrict_approx.
Theorem approxStrict_trans : forall s1 s2 s3,
approx s2 s1 -> approxStrict s2 s3 -> approxStrict s1 s3.
Hint Resolve approxStrict_trans.
Definition approx_dec : forall abs1 abs2, {approx abs1 abs2} + {~approx abs1 abs2}.
Definition approxStrict_dec : forall abs1 abs2, {approxStrict abs1 abs2} + {~approxStrict abs1 abs2}.
Hint Resolve approxStrict_dec.
Fixpoint distinct (ls : list nat) : Prop :=
match ls with
| nil => True
| h::t => AllS (fun x => x <> h) t
/\ distinct t
end.
Definition cardinality_atLeast s n :=
exists ls, distinct ls
/\ length ls = n
/\ AllS (fun x => AllocSet.In x s = true) ls.
Definition cardinality s n :=
cardinality_atLeast s n
/\ forall n', cardinality_atLeast s n' -> n' <= n.
Definition bound := length (AllocSet.elems progSites).
Definition neq_nat_dec : forall (x y : nat), {x <> y} + {~x <> y}.
Definition distinctify : forall (ls : list allocation_site),
{ls' : list allocation_site | distinct ls'
/\ forall x, In x ls <-> In x ls'}.
Lemma incl_S : forall (ls : list allocation_site) a,
In a ls
-> exists ls', length ls = S (length ls')
/\ incl ls (a :: ls').
Lemma incl_trans' : forall (a : allocation_site) ls1 ls2,
distinct (a :: ls1)
-> incl (a :: ls1) (a :: ls2)
-> incl ls1 ls2.
Lemma incl_length : forall (ls1 ls2 : list allocation_site),
incl ls1 ls2
-> distinct ls1
-> length ls1 <= length ls2.
Lemma card : forall s,
AllocSet.incl s progSites = true
-> {n : nat
| n <= bound
/\ cardinality s n}.
Definition var_bounded : forall (abs : astate) (v : var),
AllocSet.incl (VarMap.sel (avars (proj1_sig abs)) v) progSites = true.
Definition site_bounded : forall (abs : astate) (s : allocation_site),
AllocSet.incl (AllocMap.sel (aheap (proj1_sig abs)) s) progSites = true.
Definition size (abs : astate) :=
fold_right plus 0 (map (fun x => proj1_sig (card _ (var_bounded abs x)))
(VarSet.elems progVars))
+ fold_right plus 0 (map (fun x => proj1_sig (card _ (site_bounded abs x)))
(AllocSet.elems progSites)).
Lemma mult_le : forall n x m y,
x <= n * m
-> y <= n
-> y + x <= n * S m.
Lemma size_bounded : forall abs,
size abs <= bound * (length (VarSet.elems progVars) + length (AllocSet.elems progSites)).
Lemma fold_plus_ge : forall (A : Set) f1 f2 (ls : list A),
AllS (fun x => f1 x >= f2 x) ls
-> fold_right plus 0 (map f1 ls) >= fold_right plus 0 (map f2 ls).
Lemma fold_plus_gt : forall (A : Set) f1 f2 x,
f1 x > f2 x
-> forall (ls : list A), AllS (fun x => f1 x >= f2 x) ls
-> In x ls
-> fold_right plus 0 (map f1 ls) > fold_right plus 0 (map f2 ls).
Lemma sum_plus1 : forall x1 y1 x2 y2,
x1 > x2
-> y1 >= y2
-> x1 + y1 > x2 + y2.
Lemma sum_plus2 : forall x1 y1 x2 y2,
x1 >= x2
-> y1 > y2
-> x1 + y1 > x2 + y2.
Lemma incl_cardinality' : forall s1 s2 c,
AllocSet.incl s1 s2 = true
-> cardinality_atLeast s1 c
-> cardinality_atLeast s2 c.
Lemma incl_cardinality : forall s1 s2 c1 c2,
AllocSet.incl s1 s2 = true
-> cardinality s1 c1
-> cardinality s2 c2
-> c1 <= c2.
Lemma incl_gt : forall (x : allocation_site) ls2 ls1,
distinct ls1
-> incl ls1 ls2
-> ~In x ls1
-> In x ls2
-> length ls2 > length ls1.
Lemma set_grew : forall s1 s2 c1 c2,
AllocSet.incl s2 s1 = true
-> AllocSet.incl s1 s2 = false
-> cardinality s1 c1
-> cardinality s2 c2
-> c1 > c2.
Lemma size_approxStrict : forall abs abs',
approxStrict abs abs'
-> size abs > size abs'.
Lemma approxStrict_wf' : forall n a,
bound * (length (VarSet.elems progVars) + length (AllocSet.elems progSites)) - size a <= n
-> Acc approxStrict a.
Theorem approxStrict_wf : well_founded approxStrict.
Hint Resolve approxStrict_wf.
Definition fixed_point' : {fp : astate
| forall s, reachable_flowInsensitive aprogram aexec ainitState s
-> approx s fp}.
Lemma In_map : forall (A B : Set) x (f : A -> B) ls,
In x ls
-> In (f x) (map f ls).
Lemma in_aprogram' : forall i prog,
In i prog ->
exists H : In i prog,
In (exist (fun i0 => In i0 prog) i H)
(aprogram' prog).
Lemma in_aprogram : forall i,
In i program
-> exists H, In (exist (fun i => In i program) i H) aprogram.
Axiom valid_irrel : forall s (H1 H2 : valid s), H1 = H2.
Lemma reachable_a : forall s1 (Hv1 : valid s1) s2,
reachable_flowInsensitive program abstract_exec s1 s2
-> exists Hv2 : valid s2,
reachable_flowInsensitive aprogram aexec (exist _ _ Hv1) (exist _ _ Hv2).
Definition fixed_point : {fp : abstract_state
| forall s, reachable_flowInsensitive program abstract_exec abstract_initState s
-> approx' s fp}.
End fixed_point.
Index
This page has been generated by coqdoc