Library AndersenSound
Require Import Arith List Omega TheoryList.
Require Import ListUtil Maps Tactics.
Require Import Machine AndersenModel Pointer.
Set Implicit Arguments.
Inductive followPath : var -> nat -> state -> nat -> Prop :=
| Path_Done : forall v s,
followPath v 0 s (VarMap.sel (vars s) v)
| Path_Step : forall v n s v',
followPath v n s v'
-> v' <> 0
-> followPath v (S n) s (NatMap.sel (heap s) v').
Inductive abstract_followPath
: var -> nat -> abstract_state -> allocation_site -> Prop :=
| APath_Done : forall v s a,
AllocSet.In a (VarMap.sel (avars s) v) = true
-> abstract_followPath v 0 s a
| APath_Step : forall v n s v' a,
abstract_followPath v n s v'
-> AllocSet.In a (AllocMap.sel (aheap s) v') = true
-> abstract_followPath v (S n) s a.
Hint Constructors followPath abstract_followPath.
Definition pathCompatible (conc : state) (abs : abstract_state)
v1 n1 v2 n2 :=
forall r, followPath v1 n1 conc r
-> r <> 0
-> followPath v2 n2 conc r
-> exists r',
abstract_followPath v1 n1 abs r'
/\ abstract_followPath v2 n2 abs r'.
Definition allPaths conc abs :=
forall v1 n1 v2 n2, pathCompatible conc abs v1 n1 v2 n2.
Record compatible (conc : state) (abs : abstract_state) : Prop := {
compatInitial : NatMap.sel (heap conc) 0 = 0;
compatInBounds : forall v n v', followPath v n conc v' -> v' <= limit conc;
compatZeroed : forall a, a > limit conc -> NatMap.sel (heap conc) a = 0;
compatPaths : allPaths conc abs
}.
Hint Constructors reachable_flowInsensitive.
Lemma abstractAllocate' : forall v program next,
In (Allocate v) program
-> exists site, In (AbsAllocate v site) (abstractProgram' next program).
Lemma abstractAllocate : forall v program,
In (Allocate v) program
-> exists site, In (AbsAllocate v site) (abstractProgram program).
Ltac VarMap_split :=
match goal with
| [ |- context[VarMap.sel (VarMap.upd ?M ?A ?V) ?A'] ] =>
let Haddr := fresh "Haddr" with Heq := fresh "Heq" in
(destruct (VarMap.sel_upd M A V A') as [[Haddr Heq] | [Haddr Heq]];
rewrite Heq; simplify)
end.
Ltac nat_split :=
match goal with
| [ |- context[match ?N with O => _ | S _ => _ end] ] => destruct N; simplify
end.
Hint Rewrite VarMap.sel_upd_eq : Maps.
Hint Rewrite VarMap.sel_upd_neq using (intuition; fail) : Maps.
Ltac mySimplify := repeat progress (simplify;
autorewrite with Maps;
try match goal with
| [ H : _ |- _ ] =>
rewrite VarMap.sel_upd_eq in H
|| (rewrite VarMap.sel_upd_eq in H; [idtac | intuition; fail])
end).
Hint Resolve AllocSet.In_add_eq.
Lemma pathCompatible_symm : forall conc abs v1 n1 v2 n2,
pathCompatible conc abs v1 n1 v2 n2
-> pathCompatible conc abs v2 n2 v1 n1.
Hint Resolve pathCompatible_symm.
Lemma followPath_write_var : forall v v' conc' n r,
v <> v'
-> followPath v' n conc' r
-> forall conc pc addr lim, conc' = Build_state pc (VarMap.upd (vars conc) v addr) (heap conc) lim
-> followPath v' n conc r.
Hint Resolve followPath_write_var.
Lemma abstract_followPath_write_var : forall v v' n abs r,
v <> v'
-> abstract_followPath v' n abs r
-> forall site, abstract_followPath v' n
(Build_abstract_state (VarMap.upd (avars abs) v site) (aheap abs)) r.
Hint Resolve abstract_followPath_write_var.
Lemma compatible_write_var : forall conc abs v addr site pc lim,
let conc' := Build_state
pc
(VarMap.upd (vars conc) v addr)
(heap conc)
lim in
let abs' := Build_abstract_state
(VarMap.upd (avars abs) v site)
(aheap abs) in
allPaths conc abs
-> (forall n1 n2, pathCompatible conc' abs' v n1 v n2)
-> (forall v' n n', v <> v' -> pathCompatible conc' abs' v n v' n')
-> allPaths conc' abs'.
unfold allPaths; mySimplify.
destruct (VarMap.sel_upd (vars conc) v (limit conc) v1);
destruct (VarMap.sel_upd (vars conc) v (limit conc) v2);
mySimplify.
generalize (H v1 n1 v2 n2); unfold pathCompatible; mySimplify.
assert (followPath v1 n1 conc r); eauto.
assert (followPath v2 n2 conc r); eauto.
destruct (H3 _ H10 H8 H11) as [r' Hr'].
mySimplify.
Qed.
Lemma followPath_SO : forall s v n r,
NatMap.sel (heap s) (VarMap.sel (vars s) v) = 0
-> followPath v n s r
-> r = VarMap.sel (vars s) v \/ r = 0.
Hint Resolve followPath_SO.
Lemma followPath_SO' : forall s v n r,
NatMap.sel (heap s) (VarMap.sel (vars s) v) = 0
-> followPath v n s r
-> (n = 0 /\ r = VarMap.sel (vars s) v)
\/ (n = 1 /\ r = 0).
Lemma followPath_S : forall s v n r,
NatMap.sel (heap s) (VarMap.sel (vars s) v) = 0
-> followPath v (S n) s r
-> r = 0.
Lemma step_Allocate : forall v program conc abs,
In (Allocate v) program
-> compatible conc abs
-> exists ins', In ins' (abstractProgram program)
/\ compatible (exec (Allocate v) conc) (abstract_exec ins' abs).
Lemma abstractCopy' : forall src dst program next,
In (Copy src dst) program
-> In (AbsCopy src dst) (abstractProgram' next program).
Lemma abstractCopy : forall src dst program,
In (Copy src dst) program
-> In (AbsCopy src dst) (abstractProgram program).
Hint Resolve abstractCopy.
Lemma followPath_swap_var : forall v1 n conc1 r,
followPath v1 n conc1 r
-> forall conc2 v2, VarMap.sel (vars conc1) v1 = VarMap.sel (vars conc2) v2
-> heap conc2 = heap conc1
-> followPath v2 n conc2 r.
Hint Resolve AllocSet.incl_In.
Lemma abstract_followPath_incl : forall v1 abs1 abs2 v2 n r,
AllocSet.incl (VarMap.sel (avars abs1) v1) (VarMap.sel (avars abs2) v2) = true
-> aheap abs1 = aheap abs2
-> abstract_followPath v1 n abs1 r
-> abstract_followPath v2 n abs2 r.
Hint Resolve AllocSet.incl_union_right AllocSet.incl_refl.
Lemma step_Copy : forall dst src program conc abs,
In (Copy dst src) program
-> compatible conc abs
-> exists ins', In ins' (abstractProgram program)
/\ compatible (exec (Copy dst src) conc) (abstract_exec ins' abs).
Lemma abstractRead' : forall src dst program next,
In (Read src dst) program
-> In (AbsRead src dst) (abstractProgram' next program).
Lemma abstractRead : forall src dst program,
In (Read src dst) program
-> In (AbsRead src dst) (abstractProgram program).
Hint Resolve abstractRead.
Lemma followPath_read : forall v1 n conc1 r,
followPath v1 n conc1 r
-> forall conc2, heap conc1 = heap conc2
-> forall v2, VarMap.sel (vars conc2) v2 <> 0
-> VarMap.sel (vars conc1) v1
= NatMap.sel (heap conc2) (VarMap.sel (vars conc2) v2)
-> followPath v2 (S n) conc2 r.
Lemma abstract_followPath_expand : forall v n abs r,
abstract_followPath v n abs r
-> forall abs', aheap abs = aheap abs'
-> (forall v', AllocSet.incl (VarMap.sel (avars abs) v')
(VarMap.sel (avars abs') v') = true)
-> abstract_followPath v n abs' r.
Lemma incl_fold_union' : forall ls s s' f,
AllocSet.incl s s' = true
-> AllocSet.incl s
(fold_left
(fun known (site : allocation_site) => AllocSet.union known (f site))
ls
s') = true.
Lemma incl_fold_union : forall ls s f,
AllocSet.incl s
(fold_left
(fun known (site : allocation_site) => AllocSet.union known (f site))
ls
s) = true.
Lemma abstract_followPath_read : forall v1 abs1 n' r,
abstract_followPath v1 n' abs1 r
-> forall n, n' = S n
-> forall abs2, aheap abs1 = aheap abs2
-> forall v2, (forall a, AllocSet.In a (VarMap.sel (avars abs1) v1) = true
-> AllocSet.incl (AllocMap.sel (aheap abs1) a)
(VarMap.sel (avars abs2) v2) = true)
-> abstract_followPath v2 n abs2 r.
Lemma incl_fold_union_read : forall a f ls s i,
ls = AllocSet.elems s
-> AllocSet.In a s = true
-> AllocSet.incl (f a)
(fold_left
(fun known (site : allocation_site) =>
AllocSet.union known (f site))
ls
i)
= true.
Lemma step_Read : forall dst src program conc abs,
In (Read dst src) program
-> compatible conc abs
-> exists ins', In ins' (abstractProgram program)
/\ compatible (exec (Read dst src) conc) (abstract_exec ins' abs).
Lemma abstractWrite' : forall src dst program next,
In (Write src dst) program
-> In (AbsWrite src dst) (abstractProgram' next program).
Lemma abstractWrite : forall src dst program,
In (Write src dst) program
-> In (AbsWrite src dst) (abstractProgram program).
Hint Resolve abstractWrite.
Lemma abstract_followPath_write_preserve : forall v n abs1 r,
abstract_followPath v n abs1 r
-> forall abs2, avars abs1 = avars abs2
-> (forall addr, AllocSet.incl
(AllocMap.sel (aheap abs1) addr)
(AllocMap.sel (aheap abs2) addr) = true)
-> abstract_followPath v n abs2 r.
Ltac AllocMap_split :=
match goal with
| [ |- context[AllocMap.sel (AllocMap.upd ?M ?A ?V) ?A'] ] =>
let Haddr := fresh "Haddr" with Heq := fresh "Heq" in
(destruct (AllocMap.sel_upd M A V A') as [[Haddr Heq] | [Haddr Heq]];
rewrite Heq; simplify)
end.
Hint Resolve AllocSet.incl_union_left.
Lemma incl_write_bonanza' : forall addr h s ls i,
(forall addr', AllocSet.incl (AllocMap.sel h addr') (AllocMap.sel i addr') = true)
-> AllocSet.incl (AllocMap.sel h addr)
(AllocMap.sel
(fold_left
(fun known (site : allocation_site) =>
AllocMap.upd known site (AllocSet.union (AllocMap.sel h site) s))
ls
i) addr) = true.
Lemma incl_write_bonanza : forall addr h s ls,
AllocSet.incl (AllocMap.sel h addr)
(AllocMap.sel
(fold_left
(fun known (site : allocation_site) =>
AllocMap.upd known site (AllocSet.union (AllocMap.sel h site) s))
ls
h) addr) = true.
Ltac NatMap_split :=
match goal with
| [ |- context[NatMap.sel (NatMap.upd ?M ?A ?V) ?A'] ] =>
let Haddr := fresh "Haddr" with Heq := fresh "Heq" in
(destruct (NatMap.sel_upd M A V A') as [[Haddr Heq] | [Haddr Heq]];
rewrite Heq; simplify)
end.
Lemma fold_left_sum : forall ns n1 n2,
fold_left (fun x y => S (x + y)) ns (n1 + n2)
= n1 + fold_left (fun x y => S (x + y)) ns n2.
Lemma followPath_case : forall v n conc' r conc a src,
vars conc' = vars conc
-> heap conc' = NatMap.upd (heap conc) a (VarMap.sel (vars conc) src)
-> followPath v n conc' r
-> followPath v n conc r
\/ exists n', followPath src n' conc r.
Lemma followPath_nothing_new : forall v n conc' r conc a src,
vars conc' = vars conc
-> heap conc' = NatMap.upd (heap conc) a (VarMap.sel (vars conc) src)
-> followPath v n conc' r
-> exists v', exists n', followPath v' n' conc r.
Lemma allPaths_step : forall conc' conc a src v n r,
vars conc' = vars conc
-> heap conc' = NatMap.upd (heap conc) a (VarMap.sel (vars conc) src)
-> followPath v n conc' r
-> followPath v n conc r
\/ exists n1, exists n2,
n = S (n1 + n2)
/\ followPath v n1 conc a
/\ followPath src n2 conc' r.
Lemma follow_conjoin : forall v1 n1 conc v2 n2 r,
followPath v1 n1 conc (VarMap.sel (vars conc) v2)
-> followPath v2 n2 conc r
-> followPath v1 (n1 + n2) conc r.
Lemma abstract_follow_conjoin : forall conc abs abs' v n1 a dst src n2 r',
allPaths conc abs
-> avars abs' = avars abs
-> (forall addr,
AllocSet.incl (AllocMap.sel (aheap abs) addr)
(AllocMap.sel (aheap abs') addr) = true)
-> (forall r, AllocSet.In r (VarMap.sel (avars abs) dst) = true
-> AllocSet.incl (VarMap.sel (avars abs) src) (AllocMap.sel (aheap abs') r) = true)
-> a = VarMap.sel (vars conc) dst
-> a <> 0
-> followPath v n1 conc a
-> abstract_followPath src n2 abs' r'
-> abstract_followPath v (S (n1 + n2)) abs' r'.
Lemma allPaths_write : forall conc' conc src abs abs' dst,
vars conc' = vars conc
-> heap conc' = NatMap.upd (heap conc) (VarMap.sel (vars conc) dst) (VarMap.sel (vars conc) src)
-> VarMap.sel (vars conc) dst <> 0
-> avars abs' = avars abs
-> (forall addr,
AllocSet.incl (AllocMap.sel (aheap abs) addr)
(AllocMap.sel (aheap abs') addr) = true)
-> (forall r, AllocSet.In r (VarMap.sel (avars abs) dst) = true
-> AllocSet.incl (VarMap.sel (avars abs) src) (AllocMap.sel (aheap abs') r) = true)
-> allPaths conc abs
-> forall n v1 n1 r, r <> 0
-> followPath v1 n1 conc' r
-> forall v2 n2, followPath v2 n2 conc' r
-> n1 + n2 <= n
-> exists r',
abstract_followPath v1 n1 abs' r'
/\ abstract_followPath v2 n2 abs' r'.
Lemma sel_bonanza' : forall addr (f : allocation_site -> AllocSet.set) ls h,
AllocMap.sel h addr = f addr
-> AllocMap.sel
(fold_left
(fun known site =>
AllocMap.upd known site (f site))
ls h)
addr = f addr.
Lemma sel_bonanza : forall addr (f : allocation_site -> AllocSet.set) ls h,
In addr ls
-> AllocMap.sel
(fold_left
(fun known site =>
AllocMap.upd known site (f site))
ls h)
addr = f addr.
Lemma sel_updated' : forall r (f : allocation_site -> AllocSet.set) ls h,
AllocMap.sel h r = f r
-> AllocMap.sel
(fold_left
(fun known site => AllocMap.upd known site (f site)) ls h) r = f r.
Lemma sel_updated : forall r src f ls dst h,
ls = AllocSet.elems dst
-> AllocSet.In r dst = true
-> AllocSet.incl src
(AllocMap.sel
(fold_left
(fun known (site : allocation_site) =>
AllocMap.upd known site
(AllocSet.union (f site) src))
ls h) r) = true.
Lemma step_Write : forall dst src program conc abs,
In (Write dst src) program
-> compatible conc abs
-> exists ins', In ins' (abstractProgram program)
/\ compatible (exec (Write dst src) conc) (abstract_exec ins' abs).
Lemma followPath_goto : forall conc conc' v n r,
vars conc' = vars conc
-> heap conc' = heap conc
-> followPath v n conc r
-> followPath v n conc' r.
Lemma step_Goto : forall n conc abs,
compatible conc abs
-> compatible (exec (Goto n) conc) abs.
Section allocation_site_model_is_conservative.
Variable program : list instruction.
Lemma allocation_site_step :
forall conc abs, compatible conc abs
-> forall program ins, In ins program
-> compatible (exec ins conc) abs
\/ exists ins', In ins' (abstractProgram program)
/\ compatible (exec ins conc) (abstract_exec ins' abs).
Theorem allocation_site_model_is_conservative :
forall conc conc', reachable_flowInsensitive program exec conc conc'
-> forall abs, compatible conc abs
-> exists abs', reachable_flowInsensitive (abstractProgram program)
abstract_exec abs abs'
/\ compatible conc' abs'.
Definition abstract_initState :=
Build_abstract_state
(VarMap.init AllocSet.empty)
(AllocMap.init AllocSet.empty).
Lemma andersen_start :
forall conc, reachable_flowInsensitive program exec initState conc
-> exists abs, reachable_flowInsensitive (abstractProgram program)
abstract_exec abstract_initState abs
/\ compatible conc abs.
Theorem andersen_sound : forall v1 v2,
(forall abs, reachable_flowInsensitive (abstractProgram program)
abstract_exec abstract_initState abs
-> forall site, AllocSet.In site
(AllocSet.intersect (VarMap.sel (avars abs) v1) (VarMap.sel (avars abs) v2))
= false)
-> mustNotAlias program v1 v2.
End allocation_site_model_is_conservative.
Index
This page has been generated by coqdoc