Library PointsToAnalysis
Specification of the points-to analysis
Require Import Utf8.
Require Import List.
Require Import StdNotations.
Require Import Fix.
Require Import Cool.
Require Import ICool.
Module Analysis(Ctx : Context).
Require Import List.
Require Import StdNotations.
Require Import Fix.
Require Import Cool.
Require Import ICool.
Module Analysis(Ctx : Context).
The principle of context-sensitive analyses is to abstract the set of instrumented states IAcc.
- addresses are abstracted by allocation contexts AC
- call-stacks by the call contexts CC
- sets of environments Env are abstracted in a non-relational manner (see Andersen's analysis)
The analysis is defined over the following abstract domains
Definition HClass := AC → Class → Prop.
Definition HObject := AC → Field → option AC → Prop.
Definition AEnv := Var → option AC → Prop.
Definition CCEnv := CC → PC → AEnv.
Definition HObject := AC → Field → option AC → Prop.
Definition AEnv := Var → option AC → Prop.
Definition CCEnv := CC → PC → AEnv.
Because the analysis essentially computes relations, we could model the result
of the analysis as three mutually inductive relations (HC,HO,E) ∈ HClass * HObject * CCEnv
However, this is not a wise choice. In Coq, dealing with mutually recursive relations is technically feasible but complicated.
Instead, as it is customary in abstract interpretation, the result of the analysis is expressed as the least fixpoint of a functional.
In the following, we define three functional
Eventually, we define ASpecF the global functional of the analysis
- HClassSpec defines HC w.r.t E
- HObjectSpec defines HO w.r.t HC and E
- EnvSpec defines E w.r.t HC and HO and E
Eventually, we define ASpecF the global functional of the analysis
To define these objects, two auxiliary definitions are needed
For e : Var → option AC and pe : Var → option AC → Prop ,
We write e ∈ pe iff ∀ v, e v ∈ pe(v)
Definition mem (e: Var → option AC) (pe : Var → option AC → Prop) :=
∀ v, pe v (e v).
Notation "A ∈ B" := (mem A B) (at level 90).
∀ v, pe v (e v).
Notation "A ∈ B" := (mem A B) (at level 90).
The dispatch function dp is abstracted by the adp relation defined below
Definition adp (HC: HClass) (e: Var → option AC) (d : Var → Class) : Prop :=
∀ v , match e v with
| None ⇒ d v = Udf
| Some a ⇒ HC a (d v)
end.
∀ v , match e v with
| None ⇒ d v = Udf
| Some a ⇒ HC a (d v)
end.
HClassSpec is the simplest relation. Its role is to dynamically bind an allocation context a to its class c.
For most analysis, this binding needs not being computed because the class c is usually a function of a.
For instance, when AC is the allocation point. Yet, in full generality, this could be a dynamic property.
Inductive HClassSpec (P:Program) (E :CCEnv) : HClass :=
| HTS_alloc : ∀ pc cc t es, nthp P pc = Some (New t) →
es ∈ (E cc pc) →
HClassSpec P E (alloc cc pc t es) t.
HObjectSpec is a points-to graph. Each side-effect write statement adds edges in the abstract heap.
At allocation time, we also record that the fields are null – this could be left implicit at the cost of complicating the concretisation function
Inductive HObjectSpec (P:Program) (HT : HClass) (E : CCEnv) : HObject :=
| HOS_alloc : ∀ pc f t cc es, nthp P pc = Some (New t) →
es ∈ (E cc pc) →
HObjectSpec P HT E (alloc cc pc t es) f None
| HOS_write : ∀ pc f cc e, nthp P pc = Some (Write f) → e ∈ (E cc pc) →
∀ a b, e v0 = (Some a) → e v1 = b →
HObjectSpec P HT E a f b.
Section EnvSpec.
| HOS_alloc : ∀ pc f t cc es, nthp P pc = Some (New t) →
es ∈ (E cc pc) →
HObjectSpec P HT E (alloc cc pc t es) f None
| HOS_write : ∀ pc f cc e, nthp P pc = Some (Write f) → e ∈ (E cc pc) →
∀ a b, e v0 = (Some a) → e v1 = b →
HObjectSpec P HT E a f b.
Section EnvSpec.
Instead of EnvSpec, we define EnvSpecI a generalisation of EnvSpec parametrised by :
- an initial context cci
- an initial program counter pci
- and an initial abstract environment ei
We will need EnvSpecI to state intermediate lemmas and compare CPA and ∞-CFA.
EnvSpec is EnvSpecI with cci=∅ , pci = 0 and ei = λ x . null
Hypothesis P:Program.
Hypothesis cci : CC.
Hypothesis pci : PC.
Hypothesis ei : Var → option AC.
Inductive EnvSpecI (HT : HClass) (HO : HObject) (EE : CCEnv) : CCEnv :=
| ESI_init : ∀ r, EnvSpecI HT HO EE cci pci r (ei r)
| ESI_call : ∀ cc m pc t (e:Var → option AC),
nthp P pc = Some (Call m) →
e ∈ EE cc pc →
adp HT e t →
∀ r, EnvSpecI HT HO EE (push cc pc m e) (lk P (t,m)) r (e r)
| ESI_ret0 : ∀ pc pc' m cc' e er,
nthp P pc = Some Ret →
nthp P pc' = Some (Call m) →
er ∈ (EE (push cc' pc' m e) pc) →
e ∈ (EE cc' pc') →
EnvSpecI HT HO EE cc' (pc'+1) v0 (er v0)
| ESI_ret' : ∀ pc' m r cc' er,
nthp P pc' = Some (Call m) →
er ∈ (EE cc' pc') →
r ≠ v0 →
EnvSpecI HT HO EE cc' (pc'+1) r (er r)
| intra_read_r0 : ∀ cc pc a f b e,
nthp P pc = Some (Read f) →
e ∈ (EE cc pc) →
e v0 = (Some a) →
HO a f b →
EnvSpecI HT HO EE cc (pc+1) v0 b
| intra_read_r' : ∀ cc pc r f e,
nthp P pc = Some (Read f) →
e ∈ (EE cc pc) →
EnvSpecI HT HO EE cc (pc+1) r (e r)
| intra_copy_r0 : ∀ cc pc r r' e,
nthp P pc = Some (Copy r r') →
e ∈ (EE cc pc) →
EnvSpecI HT HO EE cc (pc+1) r (e r')
| intra_copy_r' : ∀ cc pc r r' r'' e,
nthp P pc = Some (Copy r r') → r'' ≠ r →
e ∈ (EE cc pc) →
EnvSpecI HT HO EE cc (pc+1) r'' (e r'')
| intra_write : ∀ cc pc f r e,
nthp P pc = Some (Write f) →
e ∈ (EE cc pc) →
EnvSpecI HT HO EE cc (pc+1) r (e r)
| intra_alloc_r0 : ∀ cc pc t es,
nthp P pc = Some (New t) →
es ∈ (EE cc pc) →
EnvSpecI HT HO EE cc (pc+1) v0 (Some (alloc cc pc t es))
| intra_alloc_r' : ∀ cc pc r t es,
nthp P pc = Some (New t) →
es ∈ (EE cc pc) →
r ≠ v0 →
EnvSpecI HT HO EE cc (pc+1) r (es r).
The type Atom is a sum type combining the elements of the different relations computed by the analysis
Hence, the result of the context-sensitive points-to analysis is a set of atoms : Atom → Prop
Inductive Atom :=
| HC : AC → Class → Atom
| HO : AC → Field → option AC → Atom
| Ecc : CC → PC → Var → option AC → Atom.
Definition AIState := Atom → Prop.
| HC : AC → Class → Atom
| HO : AC → Field → option AC → Atom
| Ecc : CC → PC → Var → option AC → Atom.
Definition AIState := Atom → Prop.
The following aux. functions filter atoms according to the constructor
Definition gHC (S : AIState) : HClass := fun a t ⇒ S (HC a t).
Definition gHO (S: AIState) : HObject := fun a f b ⇒ S (HO a f b).
Definition gEnv (S:AIState) : CCEnv := fun cc pc r a ⇒ S (Ecc cc pc r a).
Definition mkA (Ht : HClass) (Ho : HObject) (E : CCEnv) : AIState :=
fun a ⇒
match a with
| HC a t ⇒ Ht a t
| HO a f a' ⇒ Ho a f a'
| Ecc c cp r a ⇒ E c cp r a
end.
Definition gHO (S: AIState) : HObject := fun a f b ⇒ S (HO a f b).
Definition gEnv (S:AIState) : CCEnv := fun cc pc r a ⇒ S (Ecc cc pc r a).
Definition mkA (Ht : HClass) (Ho : HObject) (E : CCEnv) : AIState :=
fun a ⇒
match a with
| HC a t ⇒ Ht a t
| HO a f a' ⇒ Ho a f a'
| Ecc c cp r a ⇒ E c cp r a
end.
Given these definitions, we can eventually give the functional ASpecFI of the points-to analysis
Inductive ASpecFI (AS :AIState) : AIState :=
| AnaObjectF : ∀ a f b, HObjectSpec P (gHC AS) (gEnv AS) a f b →
ASpecFI AS (HO a f b)
| AnaTagF : ∀ a t,
HClassSpec P (gEnv AS) a t → ASpecFI AS (HC a t)
| AnaEnvF : ∀ cc pc r a,
EnvSpecI (gHC AS) (gHO AS) (gEnv AS) cc pc r a →
ASpecFI AS (Ecc cc pc r a).
| AnaObjectF : ∀ a f b, HObjectSpec P (gHC AS) (gEnv AS) a f b →
ASpecFI AS (HO a f b)
| AnaTagF : ∀ a t,
HClassSpec P (gEnv AS) a t → ASpecFI AS (HC a t)
| AnaEnvF : ∀ cc pc r a,
EnvSpecI (gHC AS) (gHO AS) (gEnv AS) cc pc r a →
ASpecFI AS (Ecc cc pc r a).
AnaI is the result of the analysis starting from initial conditions cci pci ei
For proving "CPA beats ooCFA" this specification is not totally adequate.
Therefore, we provide an equivalent definition AnaI' which in essence computes the fixpoint in a *staged* fashion.
Inductive CCEnvT :=
Ecc' : CC → PC → Var → option AC → CCEnvT.
Definition mkCCEnv (e : CCEnvT → Prop) : CCEnv :=
fun cc pc r a ⇒ e (Ecc' cc pc r a).
Definition destCCEnv (e: CCEnv) : CCEnvT → Prop :=
fun t ⇒ let (cc,pc,r,a):= t in e cc pc r a.
Definition EnvSpecF (HC : HClass) (HO:HObject) (E: CCEnvT → Prop) : (CCEnvT → Prop) :=
destCCEnv (EnvSpecI HC HO (mkCCEnv E)).
Definition EnvSpecIFx (HC : HClass) (HO:HObject) := mkCCEnv (lfpK _ (EnvSpecF HC HO)).
Definition ASpecCurry (A : AIState) (A' : AIState) : AIState :=
ASpecFI (mkA (gHC A) (gHO A) (gEnv A')).
Definition ASpecFI' (A : AIState) : AIState :=
ASpecCurry A (mkA (gHC A) (gHO A) (EnvSpecIFx (gHC A) (gHO A))).
Definition AnaI' := lfpK _ ASpecFI'.
Ecc' : CC → PC → Var → option AC → CCEnvT.
Definition mkCCEnv (e : CCEnvT → Prop) : CCEnv :=
fun cc pc r a ⇒ e (Ecc' cc pc r a).
Definition destCCEnv (e: CCEnv) : CCEnvT → Prop :=
fun t ⇒ let (cc,pc,r,a):= t in e cc pc r a.
Definition EnvSpecF (HC : HClass) (HO:HObject) (E: CCEnvT → Prop) : (CCEnvT → Prop) :=
destCCEnv (EnvSpecI HC HO (mkCCEnv E)).
Definition EnvSpecIFx (HC : HClass) (HO:HObject) := mkCCEnv (lfpK _ (EnvSpecF HC HO)).
Definition ASpecCurry (A : AIState) (A' : AIState) : AIState :=
ASpecFI (mkA (gHC A) (gHO A) (gEnv A')).
Definition ASpecFI' (A : AIState) : AIState :=
ASpecCurry A (mkA (gHC A) (gHO A) (EnvSpecIFx (gHC A) (gHO A))).
Definition AnaI' := lfpK _ ASpecFI'.
To reason about these fixpoint we prove that the functional are monotone mono and continuous cont.
Proving monotony is only annoying but not difficult; proving continuity is usually less intuitive.
Both properties are yet very compositional.
Lemma AnaAnaI' : AnaI ⊆ AnaI'.
Lemma AnaI'Ana : AnaI' ⊆ AnaI.
End EnvSpec.
Definition e0 : Var → option AC := fun r ⇒ None.
The result of the points-to analysis from initial conditions
Definition Ana (P:Program) : AIState := AnaI P ∅ 0 e0.
Definition Ana' (P:Program) : AIState := AnaI' P ∅ 0 e0.
Definition EnvSpecFx (P:Program) (HC : HClass) (HO:HObject) := EnvSpecIFx P ∅ 0 e0 HC HO.
Definition ASpecF (P:Program) := ASpecFI P ∅ 0 e0.
Definition EnvSpec (P:Program) (HC : HClass) (HO:HObject) : CCEnv → CCEnv :=
EnvSpecI P ∅ 0 e0 HC HO.
Definition Ana' (P:Program) : AIState := AnaI' P ∅ 0 e0.
Definition EnvSpecFx (P:Program) (HC : HClass) (HO:HObject) := EnvSpecIFx P ∅ 0 e0 HC HO.
Definition ASpecF (P:Program) := ASpecFI P ∅ 0 e0.
Definition EnvSpec (P:Program) (HC : HClass) (HO:HObject) : CCEnv → CCEnv :=
EnvSpecI P ∅ 0 e0 HC HO.
EnvSpecFx is the fixpoint of EnvSpec
Lemma EnvSpecFx_fix : ∀ P HC HO, leEnv (EnvSpecFx P HC HO) (EnvSpec P HC HO (EnvSpecFx P HC HO)).
Lemma EnvSpecFx_pf : ∀ P HC HO, leEnv (EnvSpec P HC HO (EnvSpecFx P HC HO)) (EnvSpecFx P HC HO).
Lemma gEnvAna'EnvSpecFx : ∀ P, leEnv (gEnv (Ana' P)) (EnvSpecFx P (gHC (Ana' P)) (gHO (Ana' P))).
Lemma EnvSpecFxgEnvAna' : ∀ P, leEnv (EnvSpecFx P (gHC (Ana' P)) (gHO (Ana' P ))) (gEnv (Ana' P)).
Lemma EnvSpecFx_pf : ∀ P HC HO, leEnv (EnvSpec P HC HO (EnvSpecFx P HC HO)) (EnvSpecFx P HC HO).
Lemma gEnvAna'EnvSpecFx : ∀ P, leEnv (gEnv (Ana' P)) (EnvSpecFx P (gHC (Ana' P)) (gHO (Ana' P))).
Lemma EnvSpecFxgEnvAna' : ∀ P, leEnv (EnvSpecFx P (gHC (Ana' P)) (gHO (Ana' P ))) (gEnv (Ana' P)).
The correctness theorem is stated via concretisation functions
Definition γ_H (ac : Acache) (HC : HClass) (HO : HObject) (h : Heap) : Prop :=
∀ a, match h a , ac a with
| None , None ⇒ True
| Some (c,o) , Some aa ⇒ HC aa c ∧ ∀ f, HO aa f ( (o f) ** ac)
| _ , _ ⇒ False
end.
Definition γ_E (ac: Acache) (E : AEnv) (e : Env) : Prop :=
(abs e ac) ∈ E.
Inductive γ_F (P:Program) (E:CCEnv) : Acache → list IFrame → Prop :=
| F_init : ∀ ac e pc, γ_E ac (E ∅ pc) e → γ_F P E ac ((MkF pc e ∅ ) ::nil)
| F_cons : ∀ ac ac' e e' pc' pc l m cc,
γ_F P E ac ( (MkF pc e cc) :: l) →
nthp P pc = Some (Call m) → le_ac ac ac' →
γ_E ac' (E (push cc pc m (abs e ac)) pc') e' →
γ_F P E ac' ( (MkF pc' e' (push cc pc m (abs e ac))) :: (MkF pc e cc) :: l).
Inductive γ (P:Program) (S:AIState) : IState → Prop :=
| G : ∀ ac l h (Hf : γ_F P (gEnv S) ac l) (Hh : γ_H ac (gHC S) (gHO S) h), γ P S (MkS h l ac).
∀ a, match h a , ac a with
| None , None ⇒ True
| Some (c,o) , Some aa ⇒ HC aa c ∧ ∀ f, HO aa f ( (o f) ** ac)
| _ , _ ⇒ False
end.
Definition γ_E (ac: Acache) (E : AEnv) (e : Env) : Prop :=
(abs e ac) ∈ E.
Inductive γ_F (P:Program) (E:CCEnv) : Acache → list IFrame → Prop :=
| F_init : ∀ ac e pc, γ_E ac (E ∅ pc) e → γ_F P E ac ((MkF pc e ∅ ) ::nil)
| F_cons : ∀ ac ac' e e' pc' pc l m cc,
γ_F P E ac ( (MkF pc e cc) :: l) →
nthp P pc = Some (Call m) → le_ac ac ac' →
γ_E ac' (E (push cc pc m (abs e ac)) pc') e' →
γ_F P E ac' ( (MkF pc' e' (push cc pc m (abs e ac))) :: (MkF pc e cc) :: l).
Inductive γ (P:Program) (S:AIState) : IState → Prop :=
| G : ∀ ac l h (Hf : γ_F P (gEnv S) ac l) (Hh : γ_H ac (gHC S) (gHO S) h), γ P S (MkS h l ac).
The concretisations are monotonic
Lemma γ_mono : ∀ P s s', s ⊆ s' → (γ P s ) ⊆ (γ P s' ).
Lemma γ_F_γ_E : ∀ P ac E e l pc cc, γ_F P E ac ((MkF pc e cc)::l) → γ_E ac (E cc pc) e.
Lemma γ_is0 : ∀ P, γ P (Ana P) is0.
Proof.
The proof is by definition of γ
Qed.
Lemma γ_E_abs : ∀ ac cc0 pc0 e A,
γ_E ac (gEnv A cc0 pc0) e →
(abs e ac) ∈ (gEnv A cc0 pc0).
Lemma γ_E_lift : ∀ ac cc0 pc0 e A r',
γ_E ac (gEnv A cc0 pc0) e →
gEnv A cc0 pc0 r' (e r' ** ac).
Lemma γ_E_copy : ∀ P cc pc r r' e ac,
nthp P pc = Some (Copy r r') →
γ_E ac (gEnv (Ana P) cc pc) e →
γ_E ac (gEnv (ASpecF P (Ana P)) cc (pc + 1)) (e [r ↦ e r']).
Lemma γ_E_read : ∀ P f cc pc e h' a t o ac,
nthp P pc = Some (Read f) →
e v0 = Some a →
h' a = Some (t, o) →
γ_H ac (gHC (Ana P)) (gHO (Ana P)) h' →
γ_E ac (gEnv (Ana P) cc pc) e →
γ_E ac (gEnv (ASpecF P (Ana P)) cc (pc + 1)) (e [v0 ↦ o f]).
Lemma γ_E_write : ∀ P cc pc f e ac,
nthp P pc = Some (Write f) →
γ_E ac (gEnv (Ana P) cc pc) e →
γ_E ac (gEnv (ASpecF P (Ana P)) cc (pc + 1)) e.
Proof.
Qed.
Lemma γ_H_write : ∀ P f ac cc0 pc0 e' a t o h,
nthp P pc0 = Some (Write f) →
e' v0 = Some a →
h a = Some (t, o) →
γ_E ac (gEnv (Ana P) cc0 pc0) e' →
γ_H ac (gHC (Ana P)) (gHO (Ana P)) h →
γ_H ac (gHC (ASpecF P (Ana P))) (gHO (ASpecF P (Ana P)))
(h [a ↦ Some (t, o [f ↦ e' v1])]).
Lemma γ_E_new : ∀ P ac pc0 cc0 c e h a
(Ha :forall v', e v' ≠ Some a) ,
nthp P pc0 = Some (New c) →
h a = None →
γ_H ac (gHC (Ana P)) (gHO (Ana P)) h →
γ_E ac (gEnv (Ana P) cc0 pc0) e →
γ_E (ac [a ↦ Some (alloc cc0 pc0 c (abs e ac))])
(gEnv (ASpecF P (Ana P)) cc0 (pc0 + 1)) (e [v0 ↦ Some a]).
Proof.
Lemma γ_H_new : ∀ P ac pc0 cc0 c e h a,
γ_E ac (gEnv (Ana P) cc0 pc0) e →
nthp P pc0 = Some (New c) →
wf_heap h →
h a = None →
γ_H ac (gHC (Ana P)) (gHO (Ana P)) h →
γ_H (ac [a ↦ Some (alloc cc0 pc0 c (abs e ac))])
(gHC (ASpecF P (Ana P))) (gHO (ASpecF P (Ana P)))
(h [a ↦ Some (c, Null)]).
Lemma γ_H_ASpecF : ∀ ac P h',
γ_H ac (gHC (Ana P)) (gHO (Ana P)) h' →
γ_H ac (gHC (ASpecF P (Ana P))) (gHO (ASpecF P (Ana P))) h'.
Lemma γ_E_call : ∀ P pc0 m cc0 h ac e,
nthp P pc0 = Some (Call m) →
γ_E ac (gEnv (Ana P) cc0 pc0) e →
γ_H ac (gHC (Ana P)) (gHO (Ana P)) h →
wf_env e h →
γ_E ac
(gEnv (ASpecF P (Ana P)) (push cc0 pc0 m (abs e ac)) (lk P (dp h e, m))) e.
Lemma γ_E_ret : ∀ P pc0 pc' m cc0 e e' ac ac',
nthp P pc0 = Some Ret →
nthp P pc' = Some (Call m) →
le_ac ac' ac →
(∀v : Var, ∀a : Addr, e' v = Some a → ac' a ≠ None) →
γ_E ac' (gEnv (Ana P) cc0 pc') e' →
γ_E ac (gEnv (Ana P) (push cc0 pc' m (abs e' ac')) pc0) e →
γ_E ac (gEnv (ASpecF P (Ana P)) cc0 (pc' + 1)) (e' [v0 ↦ e v0]).
Lemma ISoundness : ∀ P s, IAcc P s → γ P (Ana P) s.
Proof.
Lemma γ_E_abs : ∀ ac cc0 pc0 e A,
γ_E ac (gEnv A cc0 pc0) e →
(abs e ac) ∈ (gEnv A cc0 pc0).
Lemma γ_E_lift : ∀ ac cc0 pc0 e A r',
γ_E ac (gEnv A cc0 pc0) e →
gEnv A cc0 pc0 r' (e r' ** ac).
Lemma γ_E_copy : ∀ P cc pc r r' e ac,
nthp P pc = Some (Copy r r') →
γ_E ac (gEnv (Ana P) cc pc) e →
γ_E ac (gEnv (ASpecF P (Ana P)) cc (pc + 1)) (e [r ↦ e r']).
Lemma γ_E_read : ∀ P f cc pc e h' a t o ac,
nthp P pc = Some (Read f) →
e v0 = Some a →
h' a = Some (t, o) →
γ_H ac (gHC (Ana P)) (gHO (Ana P)) h' →
γ_E ac (gEnv (Ana P) cc pc) e →
γ_E ac (gEnv (ASpecF P (Ana P)) cc (pc + 1)) (e [v0 ↦ o f]).
Lemma γ_E_write : ∀ P cc pc f e ac,
nthp P pc = Some (Write f) →
γ_E ac (gEnv (Ana P) cc pc) e →
γ_E ac (gEnv (ASpecF P (Ana P)) cc (pc + 1)) e.
Proof.
Qed.
Lemma γ_H_write : ∀ P f ac cc0 pc0 e' a t o h,
nthp P pc0 = Some (Write f) →
e' v0 = Some a →
h a = Some (t, o) →
γ_E ac (gEnv (Ana P) cc0 pc0) e' →
γ_H ac (gHC (Ana P)) (gHO (Ana P)) h →
γ_H ac (gHC (ASpecF P (Ana P))) (gHO (ASpecF P (Ana P)))
(h [a ↦ Some (t, o [f ↦ e' v1])]).
Lemma γ_E_new : ∀ P ac pc0 cc0 c e h a
(Ha :forall v', e v' ≠ Some a) ,
nthp P pc0 = Some (New c) →
h a = None →
γ_H ac (gHC (Ana P)) (gHO (Ana P)) h →
γ_E ac (gEnv (Ana P) cc0 pc0) e →
γ_E (ac [a ↦ Some (alloc cc0 pc0 c (abs e ac))])
(gEnv (ASpecF P (Ana P)) cc0 (pc0 + 1)) (e [v0 ↦ Some a]).
Proof.
Lemma γ_H_new : ∀ P ac pc0 cc0 c e h a,
γ_E ac (gEnv (Ana P) cc0 pc0) e →
nthp P pc0 = Some (New c) →
wf_heap h →
h a = None →
γ_H ac (gHC (Ana P)) (gHO (Ana P)) h →
γ_H (ac [a ↦ Some (alloc cc0 pc0 c (abs e ac))])
(gHC (ASpecF P (Ana P))) (gHO (ASpecF P (Ana P)))
(h [a ↦ Some (c, Null)]).
Lemma γ_H_ASpecF : ∀ ac P h',
γ_H ac (gHC (Ana P)) (gHO (Ana P)) h' →
γ_H ac (gHC (ASpecF P (Ana P))) (gHO (ASpecF P (Ana P))) h'.
Lemma γ_E_call : ∀ P pc0 m cc0 h ac e,
nthp P pc0 = Some (Call m) →
γ_E ac (gEnv (Ana P) cc0 pc0) e →
γ_H ac (gHC (Ana P)) (gHO (Ana P)) h →
wf_env e h →
γ_E ac
(gEnv (ASpecF P (Ana P)) (push cc0 pc0 m (abs e ac)) (lk P (dp h e, m))) e.
Lemma γ_E_ret : ∀ P pc0 pc' m cc0 e e' ac ac',
nthp P pc0 = Some Ret →
nthp P pc' = Some (Call m) →
le_ac ac' ac →
(∀v : Var, ∀a : Addr, e' v = Some a → ac' a ≠ None) →
γ_E ac' (gEnv (Ana P) cc0 pc') e' →
γ_E ac (gEnv (Ana P) (push cc0 pc' m (abs e' ac')) pc0) e →
γ_E ac (gEnv (ASpecF P (Ana P)) cc0 (pc' + 1)) (e' [v0 ↦ e v0]).
Lemma ISoundness : ∀ P s, IAcc P s → γ P (Ana P) s.
Proof.
The proof is by strong induction over the length of the derivation.
The base case is solved by γ_is0
The inductive case is by case analysis over the definition of isos using the lemma:
γ_E_copy, γ_E_read, γ_E_write, γ_H_write, γ_E_new, γ_H_new, γ_E_call, γ_E_ret
and the semantics invariants IAccNret , IAccAc and IAcc_wf_H
Qed.
Definition γ_C (P:Program) (A : Atom → Prop): State → Prop :=
fun s ⇒ ∃ is, γ P A is ∧ s = EE is.
Lemma γ_C_mono : ∀ P A A', A ⊆ A' → γ_C P A ⊆ γ_C P A'.
Theorem Soundness : ∀ P s, Acc P s → γ_C P (Ana P) s.
Definition γ_C (P:Program) (A : Atom → Prop): State → Prop :=
fun s ⇒ ∃ is, γ P A is ∧ s = EE is.
Lemma γ_C_mono : ∀ P A A', A ⊆ A' → γ_C P A ⊆ γ_C P A'.
Theorem Soundness : ∀ P s, Acc P s → γ_C P (Ana P) s.
Lemma EnvSpecFxTrans states a transitivity result of EnvSpecFx.
(This is needed to compare CPA and ooCFA)
Lemma EnvSpecFxTrans : ∀ P HT HO o pco l l' pc r a,
o ∈ EnvSpecFx P HT HO l pco →
EnvSpecIFx P l pco o HT HO l' pc r a →
EnvSpecFx P HT HO l' pc r a.
Proof.
o ∈ EnvSpecFx P HT HO l pco →
EnvSpecIFx P l pco o HT HO l' pc r a →
EnvSpecFx P HT HO l' pc r a.
Proof.
The proof is by induction over the iterates of EnvSpecIFx
As usual the base case is trivially absurd
For the inductive case, we do a case analysis over EnvSpecF
The initial case is trivial verified
For the other cases, we use the fact that EnvSpecFx is a fixpoint to unroll its definition.
This allows to apply the induction hypothesis and conclude.
This page has been generated by coqdoc