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).
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)
  Export Ctx.

  Module ISem := ISemantics(Ctx).
  Export ISem.

The analysis is defined over the following abstract domains
  Definition HClass := ACClassProp.
  Definition HObject := ACFieldoption ACProp.
  Definition AEnv := Varoption ACProp.
  Definition CCEnv := CCPCAEnv.

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
  • 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 : Varoption AC and pe : Varoption ACProp , We write epe iff v, e vpe(v)
  Definition mem (e: Varoption AC) (pe : Varoption ACProp) :=
    ∀ 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: Varoption AC) (d : VarClass) : Prop :=
    ∀ v , match e v with
                 | Noned v = Udf
                 | Some aHC a (d v)

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.

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 : Varoption 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) →
      eEE 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') →
      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) →
      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 : AtomProp
    Inductive Atom :=
    | HC : ACClassAtom
    | HO : ACFieldoption ACAtom
    | Ecc : CCPCVaroption ACAtom.

    Definition AIState := AtomProp.

The following aux. functions filter atoms according to the constructor
    Definition gHC (S : AIState) : HClass := fun a tS (HC a t).

    Definition gHO (S: AIState) : HObject := fun a f bS (HO a f b).

    Definition gEnv (S:AIState) : CCEnv := fun cc pc r aS (Ecc cc pc r a).

    Definition mkA (Ht : HClass) (Ho : HObject) (E : CCEnv) : AIState :=
      fun a
        match a with
          | HC a tHt a t
          | HO a f a'Ho a f a'
          | Ecc c cp r aE c cp r a

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 tASpecFI 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
    Definition AnaI := lfpK _ ASpecFI.

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' : CCPCVaroption ACCCEnvT.

    Definition mkCCEnv (e : CCEnvTProp) : CCEnv :=
      fun cc pc r ae (Ecc' cc pc r a).

    Definition destCCEnv (e: CCEnv) : CCEnvTProp :=
      fun tlet (cc,pc,r,a):= t in e cc pc r a.

    Definition EnvSpecF (HC : HClass) (HO:HObject) (E: CCEnvTProp) : (CCEnvTProp) :=
      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' : AnaIAnaI'.

  Lemma AnaI'Ana : AnaI'AnaI.

  End EnvSpec.

  Definition e0 : Varoption AC := fun rNone.

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) : CCEnvCCEnv :=
    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)).

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 , NoneTrue
                | Some (c,o) , Some aaHC aa c ∧ ∀ f, HO aa f ( (o f) ** ac)
                | _ , _False

  Definition γ_E (ac: Acache) (E : AEnv) (e : Env) : Prop :=
    (abs e ac) ∈ E.

  Inductive γ_F (P:Program) (E:CCEnv) : Acachelist IFrameProp :=
  | F_init : ∀ ac e pc, γ_E ac (Epc) 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) : IStateProp :=
  | 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', ss' → (γ 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.
The proof is by definition of γ

  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 [re 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 [v0o 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.

  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 [aSome (t, o [fe' 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 [aSome (alloc cc0 pc0 c (abs e ac))])
     (gEnv (ASpecF P (Ana P)) cc0 (pc0 + 1)) (e [v0Some a]).

  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 [aSome (alloc cc0 pc0 c (abs e ac))])
    (gHC (ASpecF P (Ana P))) (gHO (ASpecF P (Ana P)))
    (h [aSome (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 aac' aNone) →
    γ_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' [v0e v0]).

  Lemma ISoundness : ∀ P s, IAcc P sγ P (Ana P) s.
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

  Definition γ_C (P:Program) (A : AtomProp): StateProp :=
    fun s ⇒ ∃ is, γ P A iss = EE is.

  Lemma γ_C_mono : ∀ P A A', AA'γ_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,
    oEnvSpecFx P HT HO l pco
    EnvSpecIFx P l pco o HT HO l' pc r a
    EnvSpecFx P HT HO l' pc r a.
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.

End Analysis.

This page has been generated by coqdoc