Library Semantics

The semantics --- top level definitions

@author Patryk Czarnik

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

Require Import Sem_Frame.
Require Import Sem_Monitor.
Require Import Sem_Heap.
Require Import Sem_Call.

Module of this type provides the semantics of JVML instructions. This is the top of the hierarchical semantics definition.

The semantics, given in small-step operational fashion, is expressed as a relation. In this way it is possible to formalise properties required by the JVM specification rather than a particular implementation. This formalisation can be non-deterministic in places where the original description leaves a certain freedom to implementors. This would be impossible in case of a formalisation as a computable function.

Module Type SEMANTICS.

Included modules

Declare Module M_AllStructures : ALL_STRUCTURES.

The following modules define the details of some classes of instructions.

  Declare Module M_Sem_Frame : SEM_FRAME
    with Module M_AllStructures := M_AllStructures.

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

  Declare Module M_Sem_Heap : SEM_HEAP
    with Module M_AllStructures := M_AllStructures
    with Module M_Sem_Monitor := M_Sem_Monitor.

  Declare Module M_Sem_Call : SEM_CALL
    with Module M_AllStructures := M_AllStructures
    with Module M_Sem_Monitor := M_Sem_Monitor.

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

  Import List.ListNotations.
  Open Local Scope type_scope.

Auxiliary definitions

one_thread_changed th1 th2 jvm1 jvm2 jvm2 is a JVM state jvm1 with exactly one thread changed from th1 to th2. Heap and other threads remain the same.

  Inductive oneThreadChanged: TThread → TThread → TJVM → TJVM → Prop :=
  | OneThreadChanged_this: ∀ (h: THeap) (th1 th2: TThread) (threads: list TThread),
    oneThreadChanged th1 th2 (jvmMake h (th1 ::threads)) (jvmMake h (th2 ::threads))
  | OneThreadChanged_other: ∀ (h: THeap) (tho th1 th2: TThread) (threads1 threads2: list TThread),
    oneThreadChanged th1 th2 (jvmMake h threads1) (jvmMake h threads2) →
    oneThreadChanged th1 th2 (jvmMake h (tho ::threads1)) (jvmMake h (tho ::threads2)).

A simplified version of the above property for one thread programs.

  Inductive oneThreadChanged1: TThread → TThread → TJVM → TJVM → Prop :=
  | OneThreadChanged1_onlyone: ∀ (h: THeap) (th1 th2: TThread),
    oneThreadChanged1 th1 th2 (jvmMake h [th1 ]) (jvmMake h [th2 ]).

For single-thread programs one_thread is deterministic. Forward-style property.

  Lemma PoneThreadChanged_1thread: ∀ th1 th2 h,
    oneThreadChanged th1 th2 (jvmMake h [th1 ]) (jvmMake h [th2 ]).
  Proof.
    intros.
    constructor.
  Qed.

Inversion-style property.

  Lemma PoneThreadChanged_1thread_inv: ∀ th1 th2 th h jvm2,
    oneThreadChanged th1 th2 (jvmMake h [th ]) jvm2 →
      th = th1
      ∧ jvmGetHeap jvm2 = h
      ∧ jvmGetThreads jvm2 = [th2 ].
  Proof.
    intros.
    inversion H; clear H; subst;
      simpl.
    tauto.
    inversion H6.
  Qed.

one_thread_and_heap_changed (th1,h1) (th2,h2) jvm1 jvm2 jvm2 is a JVM state jvm1 with exactly one thread changed from th1 to th2 and the heap chaged from h1 to h2.

  Inductive oneThreadAndHeapChanged: (TThread × THeap) → (TThread × THeap) → TJVM → TJVM → Prop :=
  | OneThreadAndHeapChanged_this: ∀ th1 h1 th2 h2 threads,
    oneThreadAndHeapChanged (th1 , h1 ) (th2 , h2 ) (jvmMake h1 (th1 ::threads)) (jvmMake h2 (th2 ::threads))
  | OneThreadAndHeapChanged_other: ∀ th1 h1 th2 h2 tho threads1 threads2,
    oneThreadAndHeapChanged (th1 , h1 ) (th2 , h2 ) (jvmMake h1 threads1) (jvmMake h2 threads2) →
    oneThreadAndHeapChanged (th1 , h1 ) (th2 , h2 ) (jvmMake h1 (tho ::threads1)) (jvmMake h2 (tho ::threads2)).

A simplified version of the above property for one thread programs.

  Inductive oneThreadAndHeapChanged1: (TThread × THeap) → (TThread × THeap) → TJVM → TJVM → Prop :=
  | OneThreadAndHeapChanged_onlyone: ∀ th1 h1 th2 h2,
    oneThreadAndHeapChanged1 (th1 , h1 ) (th2 , h2 ) (jvmMake h1 [th1 ]) (jvmMake h2 [th2 ]).

For single-thread programs one_thread_and_heap_changed is deterministic. Forward-style property.

  Lemma PoneThreadAndHeapChanged_1thread: ∀ th1 th2 h1 h2,
    oneThreadAndHeapChanged (th1 , h1 ) (th2 , h2 ) (jvmMake h1 [th1 ]) (jvmMake h2 [th2 ]).
  Proof.
    intros.
    constructor.
  Qed.

Inversion-style property.

  Lemma PoneThreadAndHeapChanged_1thread_inv: ∀ th1 th2 th h1 h2 h jvm2,
    oneThreadAndHeapChanged (th1 , h1 ) (th2 , h2 ) (jvmMake h [th ]) jvm2 →
         h = h1 ∧ th = th1
      ∧ jvmGetHeap jvm2 = h2
      ∧ jvmGetThreads jvm2 = [th2 ].
  Proof.
    intros.
    inversion H; clear H; subst;
      simpl.
    tauto.
    inversion H8.
  Qed.

Which of the threads constituting jvm can be selected for execution. Currently, fully non-deterministic choice is supported.

  Inductive selectedThread: TJVM → TThread → Prop :=
  | SelectedThread_this: ∀ h th threads,
    selectedThread (jvmMake h (th ::threads)) th
  | SelectedThread_other: ∀ h th threads tho,
    selectedThread (jvmMake h threads) th →
    selectedThread (jvmMake h (tho ::threads)) th.

A simplified version of the above property for one thread programs.

  Inductive selectedThread1: TJVM → TThread → Prop :=
  | selectedThread_onlyone: ∀ (h: THeap) (th1: TThread),
    selectedThread1 (jvmMake h [th1 ]) th1.

  Lemma oneThreadSelected: ∀ (h: THeap) (th: TThread),
    selectedThread (jvmMake h [th ]) th.
  Proof.
    constructor.
  Qed.

  Lemma oneThreadSelectedAlways: ∀ (h: THeap) (th th': TThread),
    selectedThread (jvmMake h [th ]) th' →
    th = th'.
  Proof.
    intros.
    inversion H; subst; clear H.
    reflexivity.
    inversion H4.
  Qed.

Detailed semantics

Semantics of IThrow

Detailed semantics of IThrow (JVM athrow) instruction. Although the semantics is structurally simple, we describe it here separately just to keep the definition of semInstr conceptually consistent.

Inductive semThrow (p: TProgram): (TLoc → option TClassName) → TLoc → TResultOrException TLoc → Prop:=

I_Throw when completed normally (that is, it throws a given exception).

  | SemThrow_ok: ∀ heapView eloc ecn ecl,
    heapView eloc = Some ecn →
    getClass p ecn = Some ecl →
    isAncestorClassOrSelf class_Throwable ecl →
      semThrow p heapView eloc (Result eloc)

I_Throw invoked for null value.

| SemThrow_null: ∀ heapView,
semThrow p heapView null (Exception StandardNames.NullPointerException).

Thread-level semantics

The semantics of top-level CoJaq instructions. semInstr p code instr (th1, h1) result means that execution of instruction instr is possible (i.e. defined in the semantics) in thread state th1 and heap state h1 and it leads to a result.

The result can be of form Result (th2, h2), which means a successful execution of the instruction which changes the thread and heap state to th2 and h2. The result can also have the form of Exception className, which means that the execution results in an exception of class className.

We use the latter case to describe exceptions explicitly described in JVM Specification, such as NullPointerException. This way of specifying deterministic exceptions corresponds to JVM Specification, where only exception class names are given.

This relation defines the semantics of top-level CoJaq instructions at the level of the call stack and JVM structure. The heap and the frames forming up the call stack are treated here as black boxes. Only the top frame internals are used in some cases.

Details of how the instructions use (and possibly modify) those structures are specified in the lower levels of the hierarchical semantics definition, namely in modules Sem_Frame, Sem_Heap, and Sem_Call.

Inductive semInstr (p: TProgram) (code: TCode): TInstruction → (TThread × THeap) → TResultOrException (TThread × THeap) → Prop:=

I_Frame instruction, when completed normally.

  | SemInstr_frame: ∀ finstr thid cm h th fr th' fr' frs,
    th = threadMake thid null ((cm , fr )::frs) →
    th' = threadMake thid null ((cm , fr')::frs) →
    M_Sem_Frame.semFrame code finstr fr (Result fr') →
      semInstr p code (I_Frame finstr) (th , h ) (Result (th', h ))

I_Frame instruction, when completed abruptly.

  | SemInstr_frame_exn: ∀ finstr thid cm h th fr frs ecn,
    th = threadMake thid null ((cm , fr )::frs) →
    M_Sem_Frame.semFrame code finstr fr (Exception ecn) →
      semInstr p code (I_Frame finstr) (th , h ) (Exception ecn)

I_Heap instruction, when completed normally.

  | SemInstr_heap: ∀ hinstr thid cm th vars pc sk vs h th' pc' sk' vs' h' frs,
    th = threadMake thid null ((cm , frameMake vars sk pc )::frs) →
    th' = threadMake thid null ((cm , frameMake vars sk' pc')::frs) →
    stackTopValues vs vs' sk sk' →
    pc' = next code pc →
    M_Sem_Heap.semHeap p code hinstr (threadGetId th) (vs , h ) (Result (vs', h')) →
      semInstr p code (I_Heap hinstr) (th , h ) (Result (th', h'))

I_Heap instruction, when completed abruptly.

  | SemInstr_heap_exn: ∀ hinstr thid cm th vars pc sk vs h ecn frs,
    th = threadMake thid null ((cm , frameMake vars sk pc )::frs) →
    prefix vs sk →
    M_Sem_Heap.semHeap p code hinstr (threadGetId th) (vs , h ) (Exception ecn) →
      semInstr p code (I_Heap hinstr) (th , h ) (Exception ecn)

I_Invoke instruction, when completed normally.

  | SemInstr_invoke: ∀ mode cn msig h th thid cm vars pc sk vs h' th' sk' vs' frs fr_caller fr_caller' fr_starting,
    th = threadMake thid null (fr_caller ::frs) →
    fr_caller = (cm , frameMake vars sk pc ) →
    th' = threadMake thid null (fr_starting ::fr_caller'::frs) →
    fr_caller' = (cm , frameMake vars sk' pc ) →
    stackTopValues vs vs' sk sk' →
    M_Sem_Call.semInvoke p mode (cn , msig ) thid cm (vs , h ) (Result (vs', h', fr_starting )) →
      semInstr p code (I_Invoke mode cn msig) (th , h ) (Result (th', h'))

I_Invoke instruction, when completed abruptly.

  | SemInstr_invoke_exn: ∀ mode cn msig h th thid cm vars pc sk vs frs ecn fr_caller,
    th = threadMake thid null (fr_caller ::frs) →
    fr_caller = (cm , frameMake vars sk pc ) →
    prefix vs sk →
    M_Sem_Call.semInvoke p mode (cn , msig ) thid cm (vs , h ) (Exception ecn) →
      semInstr p code (I_Invoke mode cn msig) (th , h ) (Exception ecn)

I_Return instruction, when completed normally.

  | SemInstr_return: ∀ argk h th thid cm_called cm_caller vars sk pc h' th' sk' pc' vs' frs fr_ending vs2,
    th = threadMake thid null ((cm_called , fr_ending )::(cm_caller , frameMake vars sk pc )::frs) →
    th' = threadMake thid null ((cm_caller , frameMake vars sk' pc')::frs) →
    prefix vs2 (frameGetLocalStack fr_ending) →
    stackTopValues [] vs' sk sk' →
    pc' = next code pc →
    M_Sem_Call.semReturn p argk thid cm_called (vs2 , h ) (Result (vs', h')) →
      semInstr p code (I_Return argk) (th , h ) (Result (th', h'))

I_Return instruction, when completed abruptly.

  | SemInstr_return_exn: ∀ argk h th thid cm_called cm_caller fr_caller frs fr_ending vs2 ecn,
    th = threadMake thid null ((cm_called , fr_ending )::(cm_caller , fr_caller )::frs) →
    prefix vs2 (frameGetLocalStack fr_ending) →
    M_Sem_Call.semReturn p argk thid cm_called (vs2 , h ) (Exception ecn) →
      semInstr p code (I_Return argk) (th , h ) (Exception ecn)

I_Throw when completed normally (that is, it throws a given exception).

  | SemInstr_athrow: ∀ thid cm th sk vars pc th' frs h eloc,
    th = threadMake thid null ((cm , frameMake vars sk pc )::frs) →
    th' = threadMake thid eloc ((cm , frameMake vars [] pc )::frs) →
    prefix [VRef eloc ] sk →
    semThrow p (getLocClass h thid) eloc (Result eloc) →
      semInstr p code I_Throw (th , h ) (Result (th', h ))

I_Throw instruction, when completed abruptly.

  | SemInstr_athrow_null: ∀ thid cm th sk vars pc frs h loc ecn,
    th = threadMake thid null ((cm , frameMake vars sk pc )::frs) →
    prefix [VRef loc ] sk →
    semThrow p (getLocClass h thid) loc (Exception ecn) →
      semInstr p code I_Throw (th , h ) (Exception ecn)
  .

Semantics step within a thread. In general the state of heap has also an impact on the operation and can be modified. stepThread p (ts1, h1) (ts2, h2) means that a single semantics step is possible from thread state ts1 and heap state h1 and it results in the thread state changed to th2 and the heap state (possibly) changed to h2.

In practice, the step is either execution of a single JVML instruction, or an artificial step related to exception handling.

Inductive stepInThread (p: TProgram): (TThread × THeap) → (TThread × THeap) → Prop :=

Execution of an instruction which completes normally. Throwing a user exception with athrow is also handled here.

  | StepInThread_instruction_ok: ∀ instr cm code thid fr frs h h' th th',
    th = threadMake thid null ((cm , fr )::frs) →
    getMethodBodyFromProgram p (cmQName cm) = Some code →
    getInstruction code (frameGetPC fr) = Some instr →
    semInstr p code instr (th , h ) (Result (th', h')) →
    stepInThread p (th , h ) (th', h')

Execution of an instruction which completes with an explicit system exception (NullPointerException etc.).

  | StepInThread_instruction_exn: ∀ instr cm code thid fr fr' frs h h' th th' ecn eloc,
    th = threadMake thid null ((cm , fr )::frs) →
    th' = threadMake thid eloc ((cm , fr')::frs) →
    getMethodBodyFromProgram p (cmQName cm) = Some code →
    getInstruction code (frameGetPC fr) = Some instr →
    semInstr p code instr (th , h ) (Exception ecn) →
    systemException h h' eloc ecn →
    stepInThread p (th , h ) (th', h')

Exception caught in the current frame.

  | StepInThread_caught: ∀ cm m thid fr frs h fr' th th' ecn eloc handler,
    th = threadMake thid eloc ((cm , fr )::frs) →
    th' = threadMake thid null ((cm , fr')::frs) →
    getReferenceType h thid eloc = Some (RTObject ecn) →
    getMethodFromProgram p (cmQName cm) = Some m →
    validExceptionHandler p m (frameGetPC fr) ecn (Some handler) →
    fr' = frameMake (frameGetVars fr) [VRef eloc ] (handlerTarget handler) →
    stepInThread p (th , h ) (th', h )

Uncaught exception causes abrupt termination of the current method and folding the call stack.

  | StepInThread_uncaught: ∀ cm m thid fr frs h h' th th' ecn eloc,
    th = threadMake thid eloc ((cm , fr )::frs) →
    th' = threadMake thid eloc frs →
    getReferenceType h thid eloc = Some (RTObject ecn) →
    getMethodFromProgram p (cmQName cm) = Some m →
    validExceptionHandler p m (frameGetPC fr) ecn None →
    (if isMethodSynchronized m
       then M_Sem_Monitor.semMonitor Op_Unlock thid (cmCtxObjectLoc cm) h (Result h')
       else h' = h) →
    stepInThread p (th , h ) (th', h')

Uncaught exception that causes another exception (namely IllegalMonitorStateException) when trying to unlock a monitor corresponding to a synchronized method.

Observation: this is an infinite loop!

  | StepInThread_uncaught_exn: ∀ cm m thid fr frs h h' th th' ecn eloc ecn' eloc',
    th = threadMake thid eloc ((cm , fr )::frs) →
    th' = threadMake thid eloc' ((cm , fr )::frs)->
    getReferenceType h thid eloc = Some (RTObject ecn) →
    getMethodFromProgram p (cmQName cm) = Some m →
    validExceptionHandler p m (frameGetPC fr) ecn None →
    isMethodSynchronized m = true →
    M_Sem_Monitor.semMonitor Op_Unlock thid (cmCtxObjectLoc cm) h (Exception ecn') →
    systemException h h' eloc' ecn' →
    stepInThread p (th , h ) (th', h').

Top-level definition

step p jvm1 jvm2 holds iff a single step is possible from JVM state jvm1 to JVM state jvm2. It is designed as a relation (not a function) to make a non-deterministic semantics expressible in this formalism.

In practice, a step in whole JVM state takes place when a step in one of its threads takes place.

  Inductive step (p: TProgram): TJVM → TJVM → Prop :=
  | Step_thread: ∀ jvm th h jvm' th' h',
    selectedThread jvm th →
    stepInThread p (th , h ) (th', h') →
    oneThreadAndHeapChanged (th , h ) (th', h') jvm jvm' →
    step p jvm jvm'.

Reflexive-transitive closure of step relation.

Definition steps (p: TProgram): TJVM → TJVM → Prop :=
clos_refl_trans TJVM (step p).

End SEMANTICS.