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 mSome (getClassName c, m)
  | Nonematch parentClass c with
    | NoneNone
    | 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: TSignatureTClassoption (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.
    applyH0.
    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: TMethodLookupModeTProgramTQualifiedMethodNameTThreadId
      THeapoption TLocoption (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):
      TMethodLookupModeProp :=
  | 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: TMethodTLocTThreadIdTHeapTHeapProp :=
  | 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): TQualifiedMethodNameTThreadId
      (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): TQualifiedMethodNameTMethodLookupModeTThreadId
      (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.
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: TMethodTLocTThreadIdTHeapTHeapProp :=
  | 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 TKindTThreadIdTCurrentMethod
      → (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.