Library ICool

Context-sensitive instrumentation of the semantics
Require Import Utf8.
Require Import StdNotations.
Require Import Cool.
Require Import List.

Definition lift_opt (X Y : Type) (f : Xoption Y) (x:option X) : option Y :=
  match x with NoneNone | Some vf v end.

Notation "X ** F" := (lift_opt F X) (at level 80).

A context-sensitive analysis is parametrised by:
  • CC the set of call-contexts
  • AC the set of allocation contexts
  • ∅ the initial call-context
  • push for modeling a method call
  • alloc for modeling the creation of a new address

Module Type Context.
  Parameter CC : Set.
  Parameter bullet : CC.
  Parameter AC : Set.
For alloc the class parameter is redundant. Likewise, for the method parameter of push. This information could be (painfully) recovered from the program counter.
  Parameter alloc : CCPCClass → (Varoption AC) → AC.
  Parameter push : CCPCMeth → (Varoption AC) → CC.
  Notation "∅" := bullet.

End Context.

Module ISemantics(Ctx : Context).
  Import Ctx.

The instrumented semantics carries along the computation an address cache Acache mapping addresses to their abstraction
  Definition Acache := Addroption AC.
Frames are instrumented by the call context
  Record IFrame :Set := MkF {
    pc : nat ;
    env : Env ;
    cc : CC}.
States are instrumented with an address cache
  Record IState : Set := MkS {
    heap : Heap ;
    stack : list IFrame ;
    acache : Addroption AC
We write IState and IFrame as triples i.e., a , b , c

In order to call the alloc and push context function, the instrumented semantics need to apply the adress cache ac to an environment e.

In the paper, abs e ac is written e^ac
  Definition abs (e: Env) (ac:Acache) : Varoption AC :=
    fun ve v ** ac.

Except for New, intra-procedural statements do not modify the instrumentation.
  • The New statement updates the address cache
  • The Call statement updates the call-context
  • The Ret statement restores the call-context
  Inductive isos (P:Program) : IStateIStateProp :=
  | isos_intra : ∀ pc i e h e' h' s cc ac, nthp P pc = Some i → ¬ (∃ c, i = New c) → intra i (e,h) (e',h') →
    isos P ([ h , ( [ pc , e ,cc ]::s) , ac ]) ([ h' , ( [ pc+1 , e' , cc]::s) , ac ])
  | isos_alloc : ∀ pc e h s cc ac c a, nthp P pc = Some (New c) →
    h a = None
    isos P
    ([ h , ([pc, e,cc]::s), ac])
    ([ h [ aSome ( c, Null) ] , ([pc+1 , e [ v0Some a] , cc] ::s) , ac [ aSome (alloc cc pc c (abs e ac))]])
  | isos_call : ∀ pc m e h s ac cc,
    nthp P pc = Some (Call m) →
    isos P
    ([ h, [pc,e,cc]::s, ac])
    ([ h, [lk P (dp h e,m),e, push cc pc m (abs e ac)]::[pc,e,cc] ::s, ac])
  | isos_ret : ∀ (pc pc':nat) h (e e': Env) (s:list IFrame) (cc cc':CC) (ac:Acache),
    nthp P pc = Some Ret
    isos P
    ([ h, ([pc,e,cc]::[pc',e',cc']::s) , ac])
    ([ h, ([pc'+1, e' [v0e(v0)] , cc']::s) ,ac]).

The initial instrumented state is0
  Definition h0 : Heap := fun aNone.
  Definition ac0 : Acache := fun aNone.
  Definition e0 : Env := fun vNone.

  Definition is0 : IState := [h0 , [ 0 , e0 , ∅ ] ::nil , ac0].

Instrumented reachable states Iacc.
  Inductive IAcc (P:Program) : IStateProp :=
  | IAcc0 : IAcc P is0
  | IAccIsos : ∀ s s', IAcc P sisos P s s'IAcc P s'.

An alternative definition - to get the (right) induction principle over the length of the derivation
  Inductive IAccN (P:Program) : natIStateProp :=
    IAccNO : IAccN P 0 is0
  | IAccNS : ∀ n s s', IAccN P n sisos P s s'IAccN P (Datatypes.S n) s'.

  Lemma IAccIAccN : ∀ P is, IAcc P is → ∃ n, IAccN P n is.

  Lemma IAccNIAcc : ∀ P n is, IAccN P n isIAcc P is.

To recover a non-instrumented state State from an instrumented state IState , we define an erasure function EE which traverses the istate and removes the instrumentation.
  Definition eraseFrame (f : IFrame) : Frame :=
    let (pc,e,cc) := f in (pc, e).

  Definition eraseStack (sf : list IFrame) : list Frame := eraseFrame sf.

  Definition EE : IStateState := fun islet (h,s,ac) := is in (h,eraseStack s).

  Lemma new_or_not_new : ∀ (i:St) , (∃ c, i = New c) ∨ ¬ (∃ c, i = New c).

The instrumentation is not intrusive.
  • Lemma AccIAcc shows that there all the reachable states are captured
  • Lemma IAccAcc shows that the instrumentation does not enable new states
   Lemma AccIAcc : ∀ P s, Acc P s → ∃ is, IAcc P iss = EE is.
The proof is by induction over the definition of Acc and case analysis of the definition of sos. The proof follows because is a 1-1 mapping between the sos and isos rules

   Lemma IAccAcc : ∀ P is, IAcc P isAcc P (EE is).
The proof is by induction over the definition of IAcc and case analysis over isos.

Semantic invariants
The soundness proof the context-sensitive control-flow analysis depends on several semantic invariants that we detail now:
  • Absence of dangling pointers: All the addresses in the stack frame are bound in the heap and all the fields of the objects in the heap refer themselves to addresses allocated in the heap (or possibly the null pointer).

   Definition wf_heap (h:Heap) : Prop :=
     (∀ a t o, h a = Some (t, o) → ∀ fd a', o fd = Some a'h a'None).

   Definition wf_env (e:Env) (h:Heap): Prop :=
     ∀ r a, e r = Some ah aNone.

   Definition wf_H (st : IState) : Prop :=
     ∀ (ac:Acache) (h:Heap) (s:list IFrame), (st = [h , s , ac ]) →
       wf_heap h
       (∀ (pc:PC) (e:Env) cc, (In ([pc , e, cc]) s) → wf_env e h).

The initial state is0 is trivially well-formed.
   Lemma wf_H_is0 : wf_H is0.

   Lemma IAcc_wf_H : ∀ P is, IAcc P iswf_H is.
The proof is by induction over the defintition of IAcc

We define an ordering le_ac over adress caches. Basically, le_ac ac ac' holds if ac(a) = ac'(a) or ac(a) is not defined.
   Definition le_ac (ac ac' : Acache) : Prop :=
     ∀ a ab, ac a = Some abac' a = Some ab.

The relation le_ac is reflexive le_ac_refl and transitive le_ac_trans.

We proof that an address is defined in the heap only and only if it is defined in the adress cache
   Lemma IAccAc : ∀ P is, IAcc P is → ∀ a, heap is a = Noneacache is a = None.

We prove that the frames of a semantic state follow a stack discipline. Roughly speaking, if we a state [h,f0::f1::s, ac] is reachable then
  • a state [h',f1::s,ac'] was *previously* reachable such that
  • the program counter of f1 is a call
  • the call context of f0 is obtained by computing push from the context of f1
  • there are more addresses in ac than in ac'
   Lemma IAccNret : ∀ P n (h:Heap) (pc0:PC) (e:Env) cc0 pc' e' cc' s1 ac,
     IAccN P n ( [ h, ([pc0, e, cc0]) :: ([pc', e', cc']) :: s1, ac]) →
     ∃ n', n' < n
     ∃ h', ∃ m,
       nthp P pc' = Some (Call m) ∧
       ∃ ac', le_ac ac' ac
         push cc' pc' m (abs e' ac') = cc0
         IAccN P n' ([h', ([pc', e', cc']) :: s1, ac']).
The proof is by *strong* induction over n
intra-procedural cases are solved by the induction hypothesis at step n-1
the call case is trivially solved
the handle the ret case, the induction hypothesis is used twice to unwind the stack

End ISemantics.

This page has been generated by coqdoc