Library Sem_Call

Semantics of call and return

@author Patryk Czarnik, Jacek Chrząszcz

Require Import Recdef.
Require Import Logic.
Require Import Relations.
Require Import List.
Require Import Common.
Require Import ValuesNTypes.
Require Import ProgramStructures.
Require Import Program.
Require Import RuntimeStructures.
Require Import AllStructures.
Require Import Sem_Monitor.

Module of this type provides detailed semantics of call and return.

Module Type SEM_CALL.

Included modules

  Declare Module M_AllStructures : ALL_STRUCTURES.

  Declare Module M_Sem_Monitor : SEM_MONITOR
    with Module M_AllStructures := M_AllStructures.

  Import M_AllStructures.
  Import M_Program.M_ProgramStructures.M_ValuesAndTypes.
  Import M_Program.M_ProgramStructures.
  Import M_ProgramStructuresFacts.
  Import M_Program.
  Import M_RuntimeStructures.M_Heap.
  Import M_RuntimeStructures.
  Import M_RuntimeStructuresFacts.

  Import List.ListNotations.
  Open Local Scope type_scope.

Auxiliary definitions

Initialisation of frame for an invoked method.

  Definition initFrame (m: TMethod) (args: list TValue): TFrame :=
    let vars := initVars args in
    frameMake vars [] (getMethodBeginning m).

Class hierarchy lookup procedure (here as a deterministic function) used for finding valid implementation of a virtual method.

We go up in the class hierarchy until an implementation is found. In case no implementation is found for a method, None is the result.

  Function lookupMethod (msig: TSignature) (c: TClass) {wf isParentClass c} : option (TClassName × TMethod) :=
  match getMethod msig c with
  | Some m ⇒ Some (getClassName c , m)
  | None ⇒ match parentClass c with
    | None ⇒ None
    | Some c' ⇒ lookupMethod msig c'
    end
  end.

Proof obligations: parentClass c = Some c' -> isParentClass c' c

unfold isParentClass; trivial.

well_founded isParentClass

exact PparentClassWf.
Save.

Class hierarchy lookup procedure (here as inductive property) used for finding valid implementation of a virtual method.

  Inductive lookupMethodInd: TSignature → TClass → option (TClassName × TMethod) → Prop :=
  | LookupMethod_found: ∀ msig c m,
    getMethod msig c = Some m →
    lookupMethodInd msig c (Some (getClassName c , m ))
  | LookupMethod_step: ∀ msig c res parent,
    getMethod msig c = None →
    parentClass c = Some parent →
    lookupMethodInd msig parent res →
    lookupMethodInd msig c res
  | LookupMethod_fail: ∀ msig c,
    getMethod msig c = None →
    parentClass c = None →
    lookupMethodInd msig c None.

The two formulations of lookup are equivalent.

  Lemma PlookupMethod_eqv_lookupMethodInd: ∀ msig c res,
    lookupMethod msig c = res ↔ lookupMethodInd msig c res.
  Proof.
    intros msig c.
    induction (PparentClassWf c).
    intro res.
    rewrite lookupMethod_equation.
    case_eq (getMethod msig x).
    split; intros.
    subst.
    constructor.
    assumption.
    inversion H2; subst; clear H2.
    rewrite H1 in H3; clear H1.
    simplify_eq H3; clear H3; intros; subst.
    reflexivity.
    rewrite H1 in H3; discriminate H3.
    rewrite H1 in H3; discriminate H3.

    case_eq (parentClass x).
    split; intros.
    subst.
    econstructor.
    assumption.
    eassumption.
    apply → H0.
    reflexivity.
    assumption.
    inversion H3; subst; clear H3.
    rewrite H2 in H4; discriminate H4.
    rewrite H1 in H5.
    injection H5; intros; subst.
    apply <- H0.
    assumption.
    assumption.
    rewrite H1 in H5; discriminate H5.

    split; intros.
    subst.
    constructor.
    assumption.
    assumption.
    inversion H3;subst; clear H3.
    rewrite H2 in H4; discriminate H4.
    rewrite H1 in H5; discriminate H5.
    reflexivity.
  Qed.

Lookup specified as a semantic rule

  Inductive TMethodLookupMode: Set :=
  | MLM_Direct
  | MLM_Virtual.

Finding a method directly or according to the virtual lookup strategy.

  Inductive getMethodToCall: TMethodLookupMode → TProgram → TQualifiedMethodName → TThreadId →
      THeap → option TLoc → option (TClassName × TMethod) → Prop:=

  | GetMethod_direct: ∀ p cn msig c m thid h loc_opt,
    getClass p cn = Some c →
    getMethod msig c = Some m →
    getMethodToCall MLM_Direct p (cn , msig ) thid h loc_opt (Some (cn , m ))

  | GetMethod_virtual: ∀ p cn msig actual_cn actual_class m_opt thid h mloc,
    Some actual_cn = getLocClass h thid mloc →
    getClass p actual_cn = Some actual_class →
    lookupMethodInd msig actual_class m_opt →
    getMethodToCall MLM_Virtual p (cn , msig ) thid h (Some mloc) m_opt.

Dynamic semantics

States whether the given mehod qmn invoked from method cm using invokespecial should be obtained by a virtual method lookup or it is pointed directly. In practice, the answer is MLM_Direct in large majority of cases.

  Inductive invokeSpecialMode (p: TProgram) (qmn: TQualifiedMethodName) (cm: TCurrentMethod):
      TMethodLookupMode → Prop :=
  | InvokeSpecial_Direct: ∀ currentClass targetClass m,
    getClass p (cmCurrentClass cm) = Some currentClass →
    getClass p (fst qmn) = Some targetClass →
    getMethod (snd qmn) targetClass = Some m →
    (hasSuperFlag currentClass = true
     ∨ ¬ isAncestorClass targetClass currentClass
     ∨ isConstructor m = true) →
    invokeSpecialMode p qmn cm MLM_Direct

  | InvokeSpecial_Virtual: ∀ currentClass targetClass m,
    getClass p (cmCurrentClass cm) = Some currentClass →
    getClass p (fst qmn) = Some targetClass →
    getMethod (snd qmn) targetClass = Some m →
    hasSuperFlag currentClass = true →
    isAncestorClass targetClass currentClass →
    isConstructor m = false →
    invokeSpecialMode p qmn cm MLM_Virtual.

  Inductive maybeLock: TMethod → TLoc → TThreadId → THeap → THeap → Prop :=
  | ML_Synchronized: ∀ m mloc thid h h',
    isMethodSynchronized m = true →
    M_Sem_Monitor.semMonitor Op_Lock thid mloc h (Result h') →
    maybeLock m mloc thid h h'
  | ML_NotSychnronized: ∀ m mloc thid h,
    isMethodSynchronized m = false →
    maybeLock m mloc thid h h.

Semantics of a static method invocation. It is separated here just to follow the same convention as with callVirtualMethod.

  Inductive callStaticMethod (p: TProgram): TQualifiedMethodName → TThreadId →
      (list TValue × THeap) → TResultOrException ((list TValue ) × THeap × TRichFrame) → Prop:=

  | CallStatic_ok: ∀ cn mn types thid actual_cn m h mloc vs args fr_starting h',
    getMethodToCall MLM_Direct p (cn , (mn , types )) thid h None (Some (actual_cn , m )) →
    getClassObjectLoc h cn = Some mloc→
    let nargs := length types in
    args = vs →
    fr_starting = initFrame m args →
    maybeLock m mloc thid h h' →
    callStaticMethod p (cn , (mn , types )) thid
      (vs , h ) (Result ([], h', (cmMake (cn , (mn , types )) actual_cn mloc , fr_starting ))).

Semantics of an instance method invocation separated here to avoid duplication in semInvoke.

  Inductive callInstanceMethod (p: TProgram): TQualifiedMethodName → TMethodLookupMode → TThreadId →
      (list TValue × THeap) → TResultOrException ((list TValue ) × THeap × TRichFrame) → Prop:=

  | CallInstance_ok: ∀ cn mn types lmode thid actual_cn m h mloc vs args fr_starting h',
    mloc ≠ null →
    getMethodToCall lmode p (cn , (mn , types )) thid h (Some mloc) (Some (actual_cn , m )) →
    let nargs := length types in
    args = firstn nargs vs →
    [VRef mloc ] = skipn nargs vs →
    fr_starting = initFrame m (args ++[VRef mloc ]) →
    maybeLock m mloc thid h h' →
    callInstanceMethod p (cn , (mn , types )) lmode thid
      (vs , h ) (Result ([], h', (cmMake (cn , (mn , types )) actual_cn mloc , fr_starting )))

  | CallInstance_null: ∀ cn mn types lmode thid h vs,
    let nargs := length types in
    [VRef null ] = skipn nargs vs →
    callInstanceMethod p (cn , (mn , types )) lmode thid
      (vs , h ) (Exception StandardNames.NullPointerException)

  | CallInstance_notFound: ∀ cn mn types lmode thid h mloc vs,
    mloc ≠ null →
    getMethodToCall lmode p (cn , (mn , types )) thid h (Some mloc) None →
    let nargs := length types in
    [VRef mloc ] = skipn nargs vs →
    callInstanceMethod p (cn , (mn , types )) lmode thid
      (vs , h ) (Exception StandardNames.AbstractMethodError).

Final relation specifying the semantics of I_Invoke instruction.

  Inductive semInvoke (p:TProgram): TInvocationMode → TQualifiedMethodName → TThreadId → TCurrentMethod →
      (list TValue × THeap) → TResultOrException ((list TValue ) × THeap × TRichFrame) → Prop:=

invoke_static

  | SemInvokeStatic: ∀ qmn thid cm vs h result,
    callStaticMethod p qmn thid (vs , h ) result →
    semInvoke p InvokeStatic qmn thid cm (vs , h ) result

invoke_virtual

  | SemInvokeVirtual: ∀ qmn thid cm vs h result,
    callInstanceMethod p qmn MLM_Virtual thid (vs , h ) result →
    semInvoke p InvokeVirtual qmn thid cm (vs , h ) result

and invoke_interface - in our model they do not differ

  | SemInvokeInterface: ∀ qmn thid cm vs h result,
    callInstanceMethod p qmn MLM_Virtual thid (vs , h ) result →
    semInvoke p InvokeInterface qmn thid cm (vs , h ) result

invoke_special

  | SemInvokeSpecial: ∀ qmn thid mode cm vs h result,
    invokeSpecialMode p qmn cm mode →
    callInstanceMethod p qmn mode thid (vs , h ) result →
    semInvoke p InvokeSpecial qmn thid cm (vs , h ) result
.

  Inductive maybeUnlock: TMethod → TLoc → TThreadId → THeap → THeap → Prop :=
  | MU_Synchronized: ∀ m mloc thid h h',
    isMethodSynchronized m = true →
    M_Sem_Monitor.semMonitor Op_Unlock thid mloc h (Result h') →
    maybeUnlock m mloc thid h h'
  | MU_NotSychnronized: ∀ m mloc thid h,
    isMethodSynchronized m = false →
    maybeUnlock m mloc thid h h.

Dynamic semantics of I_Return instruction.

  Inductive semReturn (p:TProgram):
    option TKind → TThreadId → TCurrentMethod
      → (list TValue × THeap) → TResultOrException (list TValue × THeap) → Prop :=

return (void)

  | SemReturnVoid: ∀ cm m thid h h',
    getMethodFromProgram p (cmQName cm) = Some m →
    maybeUnlock m (cmCtxObjectLoc cm) thid h h' →
    semReturn p None thid cm ([], h ) (Result ([], h'))

return (return a value)

  | SemReturnValue: ∀ k cm m thid v h h',
    getMethodFromProgram p (cmQName cm) = Some m →
    maybeUnlock m (cmCtxObjectLoc cm) thid h h' →
    kindOfValue v = k →
    semReturn p (Some k) thid cm ([v ], h ) (Result ([v ], h')).
End SEM_CALL.