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 : X → option Y) (x:option X) : option Y :=
match x with None ⇒ None | Some v ⇒ f 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 : CC → PC → Class → (Var → option AC) → AC.
  Parameter push : CC → PC → Meth → (Var → option 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 := Addr → option 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 : Addr → option 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) : Var → option AC :=
fun v ⇒ e 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) : IState → IState → Prop :=
  | 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 [ a ↦ Some ( c, Null) ] , ([pc+1 , e [ v0 ↦ Some a] , cc] ::s) , ac [ a ↦ Some (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' [v0 ↦ e(v0)] , cc']::s) ,ac]).

The initial instrumented state is0

  Definition h0 : Heap := fun a ⇒ None.
  Definition ac0 : Acache := fun a ⇒ None.
  Definition e0 : Env := fun v ⇒ None.

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

Instrumented reachable states Iacc.

  Inductive IAcc (P:Program) : IState → Prop :=
  | IAcc0 : IAcc P is0
  | IAccIsos : ∀ s s', IAcc P s → isos 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) : nat → IState → Prop :=
    IAccNO : IAccN P 0 is0
  | IAccNS : ∀ n s s', IAccN P n s → isos 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 is → IAcc 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 := List.map eraseFrame sf.

  Definition EE : IState → State := fun is ⇒ let (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 is ∧ s = EE is.
Proof.

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

   Qed.

   Lemma IAccAcc : ∀ P is, IAcc P is → Acc P (EE is).
   Proof.

The proof is by induction over the definition of IAcc and case analysis over isos.

Qed.

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 a → h a ≠ None.

   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 is → wf_H is.
   Proof.

The proof is by induction over the defintition of IAcc

Qed.

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 ab → ac' 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 = None ↔ acache 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']).
   Proof.

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

Qed.

End ISemantics.

This page has been generated by coqdoc