Library CPA_CFA

CPA beats oo-CFA

Require Import Utf8.
Require Import List.
Require Import StdNotations.
Require Import Cool.
Require Import ICool.
Require Import PointsToAnalysis.
Require Import Fix.

We compare two analyses oo-CFA and CPA which do not use the same call-context CC but share the same allocation context AC.

Parameter AC : Set.

and the same allocation function alloc. Note that alloc is independent from the call context CC (A typical choice is to take as allocation context the allocation site)

Parameter alloc : PC → Class → (Var → option AC) → AC.

Here is the specification of ooCFA

Module ooCtx.

oo-CFA keeps as call context CC the list of program points of the callers

  Definition CC := list PC.
  Definition bullet :CC := nil.
  Definition AC := AC.
  Definition alloc : CC → PC → Class → (Var → option AC) → AC := fun cc ⇒ alloc.
  Definition push : CC → PC → Meth → (Var → option AC) → CC := fun cc pc _ _ ⇒ pc::cc.
End ooCtx.

Module CPACtx.

CPA keeps as call-context CC the abstract environment of the caller And the static method name of the call.

  Definition AC := AC.
  Definition CC := option (Meth × (Var → option AC)).
  Definition bullet : CC := None.

  Definition alloc : CC → PC → Class → (Var → option AC) → AC := fun cc⇒ alloc.
  Definition push : CC → PC → Meth → (Var → option AC) → CC := fun cc pc m e ⇒ Some (m,e).
End CPACtx.

What is striking is that CPA is directly computable by fixpoint iteration. The abstract domain is finite (as soon as there are finitely many allocation contexts). This is not the case for oo-CFA – as soon as there is a recursion in the abstract program. Yet, CPA is (strictly) more precise than oo-CFA

For the purpose of the proof we shall introduce another analysis Ω-CFA. It is straightforward that Ω-CFA is more precise than both CPA and oo-CFA because it keeps more context than both.

Module ΩCtx.
  Definition AC := AC.
  Definition CC := list (Meth × (Var → option AC) × PC)%type.
  Definition bullet : CC := nil.

  Definition alloc : CC → PC → Class → (Var → option AC) → AC := fun cc ⇒ alloc.
  Definition push : CC → PC → Meth → (Var → option AC) → CC := fun cc pc m reg ⇒ (m,reg,pc)::cc.

End ΩCtx.

Module ooCFA := Analysis(ooCtx).
Module CPA := Analysis(CPACtx).
Module ΩCFA := Analysis(ΩCtx).
Import CPA.
Import ooCFA.
Import ΩCFA.

As a warm-up, we prove that ΩCFA is more precise than ooCFA. The structure of the proof is the following:

we provide a translation function τ_oo_Ω converting the result of ooCFA into the result of ΩCFA
we show that the translation can be seen as a concretisation function: Lemma Ω_le_oo : ∀ P, ΩCFA.Ana P ⊆ τ_oo_Ω (ooCFA.Ana P).
we show that the translation is precise

Section ΩCFAooCFA.

  Definition α_Ω_oo (l : ΩCtx.CC) : ooCtx.CC :=
    List.map (@snd _ _) l.

  Definition τ_E_oo_Ω (E: ooCFA.CCEnv) : ΩCFA.CCEnv :=
    fun cc ⇒ E (α_Ω_oo cc).

  Definition τ_oo_Ω (A: ooCFA.Atom → Prop) : ΩCFA.Atom → Prop :=
    ΩCFA.mkA (ooCFA.gHC A) (ooCFA.gHO A) (τ_E_oo_Ω (ooCFA.gEnv A)).

The translation functions are monotonic

  Lemma τ_oo_Ω_mono : ∀ A A', A ⊆ A' → τ_oo_Ω A ⊆ τ_oo_Ω A'.

  Lemma ΩooEnvSpec : ∀ P cc pc r a E hc ho,
    ΩCFA.EnvSpec P hc ho (τ_E_oo_Ω E) cc pc r a
    → ooCFA.EnvSpec P hc ho E (α_Ω_oo cc) pc r a.
  Proof.

Proof by case analysis over ΩCFA.EnvSpec

  Qed.

  Lemma ΩooObjectSpec : ∀ P hc E a f b,
    HObjectSpec P hc (τ_E_oo_Ω E) a f b →
    ooCFA.HObjectSpec P hc E a f b.

  Lemma ΩooClassSpec : ∀ P E a b,
    HClassSpec P (τ_E_oo_Ω E) a b →
    ooCFA.HClassSpec P E a b.

  Lemma Ω_le_oo : ∀ P, ΩCFA.Ana P ⊆ τ_oo_Ω (ooCFA.Ana P).
  Proof.

The proof is by fixpoint transfer lfp_corrct

  Qed.

  Definition α_Ωoo_iframe (ifr : ΩCFA.ISem.IFrame) : ooCFA.ISem.IFrame :=
    let (pc,e,cc) := ifr in
      [pc , e , α_Ω_oo cc].

  Definition α_Ωoo_istate (is : ΩCFA.ISem.IState) : ooCFA.ISem.IState :=
    let (h,s,ac) := is in
      [h , List.map α_Ωoo_iframe s , ac].

  Lemma Ω_EE_oo : ∀ P A, ΩCFA.γ_C P (τ_oo_Ω A) ⊆ ooCFA.γ_C P A.
  Proof.

For each instrumented state Ωis ∈ ΩCFA.γ_C P (τ_oo_Ω A), we have to find oois ∈ ooCFA.γ_C P A. We prove that, oois = α_Ωoo_istate Ωis

  Qed.

  Lemma Ωbeatsoo : ∀ P, ΩCFA.γ_C P (ΩCFA.Ana P) ⊆ ooCFA.γ_C P (ooCFA.Ana P).
  Proof.

By Ω_EE_oo, we have ΩCFA.γ_C P (τ_oo_Ω (ooCFA.Ana P) ⊆ ooCFA.γ_C P (ooCFA.Ana P)

By Ω_le_oo, we also have ΩCFA.Ana P ⊆ τ_oo_Ω (ooCFA.Ana P).

The proof follows by monotonie of γ_C ans transitivity of ⊆

Qed.

End ΩCFAooCFA.

Section CPAΩCFA.

For proving that CPA is more precise than ΩCFA, we use a similar methodology.

In the previous case, the translation was based on an abstraction function. Here, it is not possible to map a CPACtx.CC to a single ΩCtx.CC.

Definition α_CPA_Ω (P: Program) (e: CPACtx.CC) : ΩCtx.CC → Prop :=
  fun ctx ⇒ match e with
               | None ⇒ ctx = nil
               | Some (m,e) ⇒ ∃ l , ∃ pco , nthp P pco = Some (Call m) ∧ ctx = (m,e,pco)::l
             end.

Definition τ_E_Ω (P:Program) (E: ΩCtx.CC → PC → ΩCFA.AEnv) : CPACtx.CC → PC → CPA.AEnv :=
  fun e pc r a ⇒ ∃ ctx, α_CPA_Ω P e ctx ∧ E ctx pc r a.

Lemma τ_E_Ω_mono : ∀ P E E', ΩCFA.leEnv E E' →
  ∀ cc pc r a, τ_E_Ω P E cc pc r a → τ_E_Ω P E' cc pc r a.

Definition τ_Ω (P:Program) (Ab: ΩCFA.Atom → Prop) : CPA.Atom → Prop :=
  CPA.mkA (ΩCFA.gHC Ab) (ΩCFA.gHO Ab) (τ_E_Ω P (ΩCFA.gEnv Ab)).

Lemma τ_Ω_mono : ∀ P Ab Ab',
  Ab ⊆ Ab' → (τ_Ω P Ab) ⊆ (τ_Ω P Ab').

In the following, we prove properties relative to the initial conditions of ΩCFA namely EnvSpecIFxLength EnvSpecIFxRoot, EnvSpecIFxIn and EnvSpecIFxPC.

By construction, all the contexts computed by the analysis are suffixes of the initial context. As a consequence, these are necessarily longer

Lemma EnvSpecIFxLength : ∀ P l e HC HO pco l' pc r a,
EnvSpecIFx P l pco e HC HO l' pc r a → length l ≤ length l'.
Proof.

The proof is by induction over the iterates of the fixpoint computation

The base case is absurd

For the inductive case, we perform a case analysis

For a call, the context is a push from a previously computed (longer) context and the proof follows by induction hypothesis.

For a return, we apply directly the induction hypothesis – we return to a previously computed context

None of the interprocedural statement modifies the context ; the proof follows by induction hypothesis

Qed.

Roughly speaking, EnvSpecIFxRoot states that whatever the initial call-context, the result of the analysis is the same for suffixes of this call context

Lemma EnvSpecIFxRoot : ∀ P l e HC HO pco ls l' pc r a,
EnvSpecIFx P l pco e HC HO (ls ++ l) pc r a →
EnvSpecIFx P l' pco e HC HO (ls ++ l') pc r a.
Proof.

The proof is by induction over the iterates of the fixpoint computation

The base case is absurd

For the inductive case, we perform a case analysis

For a call, the call context cc0 is necessarily a suffix of ls++l. As a result, the proof follows by induction hypothesis

For a return and intra-procedural statements the proof follows by induction hypothesis.

Qed.

Lemma EnvSpecFxIn : ∀ P HT HO m o pco l ll p r a,
EnvSpecFx P HT HO (ll++(m, o, pco) :: l) p r a →
o ∈ (EnvSpecFx P HT HO l pco).
Proof.

The proof is by induction over the iterates of the fixpoint computation

Qed.

Lemma EnvSpecIFxPC : ∀ P HT HO m o pco pco' l ll pc r a,
  nthp P pco = nthp P pco' →
  EnvSpecFx P HT HO (ll++(m, o, pco) :: l) pc r a →
  EnvSpecIFx P l pco' o HT HO (ll++ (m,o,pco') :: l) pc r a.
Proof.

The proof is by induction over the iterates of EnvSpecFx

and case analysis over EnvSpecI

The base case is trivially absurd

To solve the other subgoals, we unroll the definition of EnvSpecIFx and use the induction hypothesis

Qed.

Lemma EnvSpecSwap : ∀ P HC HO m o pco pco' l l' pc' e v v',
  nthp P pco = nthp P pco'→
  EnvSpecFx P HC HO ((m, o, pco') :: l') pc' v' (e v') →
  EnvSpecFx P HC HO ((m, o, pco) :: l) pc' v (e v) →
   EnvSpecFx P HC HO ((m, o, pco) :: l) pc' v' (e v').
Proof.

By EnvSpecIFxPC we obtain EnvSpecIFx P l' pco o HT HO ((m, o, pco) :: l') pc' v (e v)

By EnvSpecIFxRoot, we obtain EnvSpecIFx P l pco o HT HO0 ((m, o, pco) :: l) pc' v (e v)

By EnvSpecFxIn we obtain o ∈ EnvSpecFx P HT HO l pco

We conclude by EnvSpecFxTrans

Qed.

Lemma α_EnvSpecFx : ∀ P HC HO cc ctx ctx' pc' v v' e,
  α_CPA_Ω P cc ctx →
  EnvSpecFx P HC HO ctx pc' v (e v) →
  α_CPA_Ω P cc ctx' →
  EnvSpecFx P HC HO ctx' pc' v' (e v') →
   EnvSpecFx P HC HO ctx pc' v' (e v').
Proof.

The proof is by case analysis over cc using EnvSpecSwap

Qed.

Lemma mem_τ : ∀ P HT HO cc pc' e,
e ∈ τ_E_Ω P (EnvSpecFx P HT HO) cc pc' →
∃ l, (α_CPA_Ω P cc l) ∧ ( e ∈ (EnvSpecFx P HT HO l pc')) .
Proof.

The proof follows from α_EnvSpecFx

Qed.

Lemma CPAΩ_EnvSpec : ∀ P HT HO, CPA.leEnv (CPA.EnvSpecFx P HT HO) (τ_E_Ω P (ΩCFA.EnvSpecFx P HT HO) ).
Proof.

The proof is by induction over CPA.EnvSpecFx and case analysis over CPA.EnvSpecF.

The base case is trivially absurd

The case ESI_init is solved by definition of EnvSpecI

The call case is solved by induction hypothesis using mem_τ'.

By induction hypothesis and mem_τ we exhibit a caller environment.

By ESI_ret0, we have to prove that the context of the return is ((m, e, pc') :: l)

This is done by EnvSpecFxTrans , EnvSpecIFxRoot and EnvSpecIFxPC

Other cases keep the context unchanged. Hence, they are discharged by induction hypothesis

Qed.

Lemma CPAΩ_mem : ∀ P HT HO,
  ∀ cc pc es, es ∈ (CPA.EnvSpecFx P HT HO cc pc) →
    ∃ l, es ∈ (ΩCFA.EnvSpecFx P HT HO) l pc.

Lemma CPAΩ_HClass : ∀ P HT HO,
  ∀ a t, CPA.HClassSpec P (CPA.EnvSpecFx P HT HO) a t → ΩCFA.HClassSpec P (ΩCFA.EnvSpecFx P HT HO) a t.
Proof.

By definition of ΩCFA.HClassSpec using CPAΩ_mem.

Qed.

Lemma CPAΩ_HObject : ∀ P HT HO,
∀ a f b, CPA.HObjectSpec P HT (CPA.EnvSpecFx P HT HO) a f b → ΩCFA.HObjectSpec P HT (ΩCFA.EnvSpecFx P HT HO) a f b.
Proof.

By definition of ΩCFA.HObjectSpec using CPAΩ_mem.

Qed.

Lemma CPAΩCFA_AnaI' : ∀ P, CPA.AnaI' P CPACtx.bullet 0 CPA.e0 ⊆ τ_Ω P (AnaI' P bullet 0 e0).
Proof.
Qed.

Lemma CPAΩCFA : ∀ P, CPA.Ana P ⊆ τ_Ω P (ΩCFA.Ana P).

Lemma γ_E_CPAΩ : ∀ ae ac e,
  CPA.γ_E ac ae e →
  γ_E ac ae e.
Proof.
  auto.
Qed.

Lemma γ_E_τ_bullet : ∀ P HT HO ac pc e,
γ_E ac (τ_E_Ω P (EnvSpecFx P HT HO) CPACtx.bullet pc) e →
   γ_E ac (EnvSpecFx P HT HO bullet pc) e.

Lemma γ_F_τ_Ω : ∀ P HT HO ac l,
  CPA.γ_F P (τ_E_Ω P (ΩCFA.EnvSpecFx P HT HO)) ac l →
   ∃l' : list IFrame,
   eraseStack l' = CPA.ISem.eraseStack l ∧ γ_F P (ΩCFA.EnvSpecFx P HT HO) ac l'.
Proof.
Qed.

Lemma γ_τ_Ω : ∀ P, CPA.γ_C P (τ_Ω P (ΩCFA.AnaI' P bullet 0 e0)) ⊆ γ_C P (ΩCFA.Ana P).
Proof.
Qed.

Lemma CPAbeatsΩCFA : ∀ P, CPA.γ_C P (CPA.Ana P) ⊆ ΩCFA.γ_C P (ΩCFA.Ana P).
Proof.
Qed.

Lemma CPAbeatsooCFA : ∀ P, CPA.γ_C P (CPA.Ana P) ⊆ ooCFA.γ_C P (ooCFA.Ana P).
Proof.

By transitivity, CPAbeatsΩCFA and Ωbeatsoo

End CPAΩCFA.

This page has been generated by coqdoc