Library RuntimeStructures

Require Import List.
Require Import Common.
Require Import ValuesNTypes.
Require Import ProgramStructures.
Require Import Heap.

JVM runtime structures

@author Patryk Czarnik Module of this type provides structures used by the JVM during runtime. They form the semantic domain of the JVM semantics formalisation. Structures used in both -- the runtime and the program (instructions) -- are defined in other modules: ProgramStructures and Values, and are referenced from here.

Module Type RUNTIME_STRUCTURES.

Included modules

  Declare Module M_Heap: HEAP.
  Import M_Heap.M_ProgramStructures.M_ValuesAndTypes.
  Import M_Heap.M_ProgramStructures.
  Import M_Heap.

  Open Local Scope type_scope.
  Import List.ListNotations.

Local variables array

Introduced using abstract type TVarsA with operations on it and specification of those operations.

The type of local variables array. Generic declaration, parametrised with what is carried by the variables. This section is parametrised with the type of a single element to be carried by the structures so that the definitions can be used in multiple ways. In the most basic usage t is equal to TValue and then the structures represent components of a running JVM and is such way they are used in actual "dynamic" semantics. For the purposes of static semantics, bytecode verification procedure, and some variants of abstract interpretation, t can be equal to TKind, TValue, or an abstract generalisation of values (e.g. integer intervals).

This parametrised approach avoids code duplication and make the definitions here reusable.

Parameter TVarsGeneric: Set → Type.

Section GenericVarsDefinition.

Type of atoms carried by variables.

Variable t: Set.

The empty array, no variable is set.

Parameter varsEmpty: TVarsGeneric t.

Returns a value from the given variable.

Parameter varsGet: TVar → TVarsGeneric t → option t.

Sets the value of the given variable.

Parameter varsSet: TVar → t → TVarsGeneric t → TVarsGeneric t.

Arrays are equivalent if they have the same elements.

Definition varsEquiv (vars1 vars2: TVarsGeneric t): Prop :=
∀ var, varsGet var vars1 = varsGet var vars2.

Specification of variable arrays.

Section VarsProperties.

A variables array.

Variable vars: TVarsGeneric t.

Some variables.

Variable x y: TVar.

An atom.

Variable v: t.

vars_empty is empty.

Axiom PvarsEmptyGet: varsGet x varsEmpty = None.

vars_set really sets a value

Axiom PvarsSetGet:
varsGet x (varsSet x v vars) = Some v.

vars_set does not change other variables

      Axiom PvarsSetGetOther:
        x ≠ y →
        varsGet y vars = varsGet y (varsSet x v vars).

Equal things are equivalent.

Axiom PvarsEqEquiv:
varsEquiv vars vars.

Setting the same value results in an equvalent array.

      Axiom PvarsSetSameEquiv:
        varsGet x vars = Some v →
        varsEquiv (varsSet x v vars) vars.
    End VarsProperties.
  End GenericVarsDefinition.
  Arguments varsEmpty [t].
  Arguments varsGet [t] _ _.
  Arguments varsSet [t] _ _ _.
  Arguments varsEquiv [t] _ _.
  Arguments PvarsEmptyGet [t] _.
  Arguments PvarsSetGet [t] _ _ _.
  Arguments PvarsSetGetOther [t] _ _ _ _ _.
  Arguments PvarsEqEquiv [t] _ _.
  Arguments PvarsSetSameEquiv [t] _ _ _ _ _.

  Section GenericStackDefinition.

Type of atoms stored on the stack.

Variable t: Set.

Local values stack.

The type of local values stack. Defined simply as a list.

Definition TLocalStackGeneric: Set := list t.
End GenericStackDefinition.

Concretisation of the generic structures introduced above

Local variables table.

Definition TVars := TVarsGeneric TVarValue.

Operand stack.

Definition TLocalStack := TLocalStackGeneric TValue.

Kind-level shadow of variables table.

Definition TVarsKShadow := TVarsGeneric TVarKind.

Kind-level shadow of operand stack.

Definition TLocalStackKShadow := TLocalStackGeneric TKind.

Type-level shadow of variables table.

Definition TVarsTShadow := TVarsGeneric TType.

Type-level shadow of operand stack.

Definition TLocalStackTShadow := TLocalStackGeneric TType.

Projections between actual and "shadow" structures

They are usable for reasoning about static and dynamic semantics correspondence.

For a real array of variables returns the corresponding array of kind-level shadows.

Parameter varsKAbstraction: TVars → TVarsKShadow.

For an array of kind-level shadows returns an array of example (but consistent) values.

  Parameter varsKConcretisation: TVarsKShadow → TVars.

  Axiom PvarsKAbstractionConsistent: ∀ vars var,
    varsGet var (varsKAbstraction vars) = option_map kindOfVarValue (varsGet var vars).

  Axiom PvarsKAbstractionConsistentSome: ∀ vars var v,
    varsGet var vars = Some v →
    varsGet var (varsKAbstraction vars) = Some (kindOfVarValue v).

  Axiom PvarsKAbstractionConsistentSet: ∀ vars var v,
    varsKAbstraction (varsSet var v vars) =
    varsSet var (kindOfVarValue v) (varsKAbstraction vars).

  Axiom PvarsKConcretisationConsistent: ∀ kvars var,
    option_map kindOfVarValue (varsGet var (varsKConcretisation kvars)) = varsGet var kvars.

  Axiom PvarsKConcretisationConsistentSome: ∀ kvars var k,
    varsGet var kvars = Some k →
    ∃ v, kindOfVarValue v = k ∧
      varsGet var (varsKConcretisation kvars) = Some v.

  Axiom PvarsKConcretisationAbstraction: ∀ varssh,
    varsKAbstraction (varsKConcretisation varssh) = varssh.

For a real stack of values returns the corresponding stack of kind-level shadows.

Definition localStackKAbstraction: TLocalStack → TLocalStackKShadow :=
map kindOfValue.

For a stack of kind-level shadows returns a stack of example (but consistent) values.

  Definition localStackKConcretisation: TLocalStackKShadow → TLocalStack :=
    map defaultForKind.

  Axiom PlocalStackKConcretisationAbstraction: ∀ sksh,
    localStackKAbstraction (localStackKConcretisation sksh) = sksh.

Frame (corresponding to method call)

Record TFrame: Type := frameMake {

The variables array.

frameGetVars: TVars;

The local values stack.

frameGetLocalStack: TLocalStack;

The program counter.

frameGetPC: TPC
}.

Kind-level shadow of frame.

    Record TFrameKShadow := frameKShadowMake {
      frameKShadowGetVars: TVarsKShadow;
      frameKShadowGetLocalStack: TLocalStackKShadow;
      frameKShadowGetPC: TPC
    }.

For a real frame returns the corresponding kind-level shadow.

  Definition frameKAbstraction (fr: TFrame): TFrameKShadow :=
    frameKShadowMake
      (varsKAbstraction (frameGetVars fr))
      (localStackKAbstraction (frameGetLocalStack fr))
      (frameGetPC fr).

For a kind-level shadow of frame returns an example frame corresponding to the shadow.

  Definition frameKConcretisation (fr: TFrameKShadow): TFrame :=
    frameMake
      (varsKConcretisation (frameKShadowGetVars fr))
      (localStackKConcretisation (frameKShadowGetLocalStack fr))
      (frameKShadowGetPC fr).

  Axiom PframeKConcretisationAbstraction: ∀ frsh,
    frameKAbstraction (frameKConcretisation frsh) = frsh.

Information about the current method to be stored on the call stack.

Record TCurrentMethod: Set := cmMake {

Qualified method name (class of declaration and signature).

cmQName: TQualifiedMethodName;

Current method (class of the actual definition of the method).

cmCurrentClass: TClassName;

The location of the context object; in case of static methods it is the class object of the containing class.

    cmCtxObjectLoc: TLoc
  }.

  Definition cmDeclClass (cm: TCurrentMethod): TClassName :=
    fst (cmQName cm).

  Definition cmSignature (cm: TCurrentMethod): TSignature :=
    snd (cmQName cm).

Threads and whole JVMs

A frame together with details of the method running within it:

the name of the method,

Definition TRichFrame :=
TCurrentMethod × TFrame.

Evaluation state: normal, represented with null, or exceptional, represented as a location pointing to an exception object.

Definition TEvalState := TLoc.

A thread consists of a frame stack.

  Record TThread := threadMake {
    threadGetId: TThreadId;
    threadGetEvalState: TEvalState;
    threadGetCallStack: list TRichFrame
  }.

The Java Virtual Machine under run defined as one heap and a number of threads.

  Record TJVM := jvmMake {
    jvmGetHeap: THeap;
    jvmGetThreads: list TThread
  }.

Result or exception

Normal or exceptional result of an instruction, to be used at various levels of the hierarchical formalisation.

This is a simple monadic structure.

  Inductive TResultOrException (A: Type): Type :=
  | Result (result: A)
  | Exception (cn: TClassName).
  Arguments Result [A] result.
  Arguments Exception [A] cn.
End RUNTIME_STRUCTURES.

Additional definitions related to runtime structures

Definitions and properties independent of a particular module implementation.

Module RuntimeStructuresFacts
  (_RuntimeStructures: RUNTIME_STRUCTURES).

  Import _RuntimeStructures.
  Import M_Heap.M_ProgramStructures.M_ValuesAndTypes.
  Import M_Heap.M_ProgramStructures.
  Import List.ListNotations.

  Lemma PlocalStackKAbstractionApp: ∀ pref tl,
    localStackKAbstraction (pref ++ tl)
      = (localStackKAbstraction pref ) ++ (localStackKAbstraction tl ).
  Proof.
    unfold localStackKAbstraction.
    apply map_app.
  Qed.

Helper definitions for lists and operand stacks

p is a prefix of l

Definition prefix {A: Set} (p l: list A): Prop :=
∃ tl, p ++ tl = l.

p is a refix of l -- inductive version

  Inductive prefixInd {A: Set}: list A → list A → Prop :=
  | Prefix_nil: ∀ l2,
    @prefixInd A nil l2
  | Prefix_cons: ∀ x l1 l2,
    @prefixInd A l1 l2 →
    @prefixInd A (x ::l1) (x ::l2).

  Lemma PprefixTrivial: ∀ {A: Set} (p tl: list A),
    prefix p (p ++tl).
  Proof.
    intros.
    ∃ tl.
    reflexivity.
  Qed.

  Lemma PprefixMap:
    ∀ {t1 t2: Set} (f: t1 → t2) (p l: list t1),
    prefix p l →
    prefix (map f p) (map f l).
  Proof.
    unfold prefix.
    intros.
    destruct H as [tl H].
    ∃ (map f tl).
    rewrite <- map_app.
    f_equal.
    assumption.
  Qed.

  Lemma PprefixNilImpliesNil: ∀ {t: Set} (p: list t),
    prefix p [] → p = [].
  Proof.
    unfold prefix.
    intros.
    destruct H as [tl H].
    apply app_eq_nil in H.
    tauto.
  Qed.

l2 is equal to l1 with a prefix fragment p1 replaced with p2. p1 or p2 can be empty; p1 has to be a prefix of l1 and p2 is a prefix of l2.

  Definition stackTopValues {t: Set} (p1 p2 l1 l2: list t): Prop :=
     ∃ tl,
       p1 ++tl = l1 ∧ p2 ++tl = l2.

  Lemma PstackTopValuesTrivial: ∀ {t: Set} (p1 p2 tl: list t),
    stackTopValues p1 p2 (p1 ++tl) (p2 ++tl).
  Proof.
    intros.
    ∃ tl.
    intuition reflexivity.
  Qed.

  Lemma PstackTopValuesSame: ∀ {t: Set} (l1 l2: list t),
    stackTopValues l1 l2 l1 l2.
  Proof.
    intros.
    ∃ [].
    split;
      apply app_nil_r.
  Qed.

  Lemma PstackTopValuesNilCons: ∀ {t: Set} (e: t) (l: list t),
    stackTopValues [] [e ] l (e ::l).
  Proof.
    intros.
    ∃ l.
    intuition reflexivity.
  Qed.

  Lemma PstackTopValuesMap:
    ∀ {t1 t2: Set} (f: t1 → t2) (p1 p2 l1 l2: list t1),
    stackTopValues p1 p2 l1 l2 →
    stackTopValues (map f p1) (map f p2) (map f l1) (map f l2).
  Proof.
    unfold stackTopValues.
    intros.
    destruct H as [tl1 H].
    ∃ (map f tl1).
    destruct H.
    split;
      rewrite <- map_app;
      f_equal;
      assumption.
  Qed.

  Lemma PstackTopValues_implies_prefix_l:
    ∀ {t: Set} (p1 p2 l1 l2: list t),
      stackTopValues p1 p2 l1 l2 → prefix p1 l1.
  Proof.
    intros.
    destruct H as [tl H].
    ∃ tl.
    tauto.
  Qed.

  Lemma PstackTopValues_implies_prefix_r:
    ∀ {t: Set} (p1 p2 l1 l2: list t),
      stackTopValues p1 p2 l1 l2 → prefix p2 l2.
  Proof.
    intros.
    destruct H as [tl H].
    ∃ tl.
    tauto.
  Qed.

The following tactics may be used to obtain a set of simple equalities of elements and list fragments from prefix or stackTopValues property given for fixed (or partially fixed) lists. The are very useful in manual proofs related to particular program runs.

  Ltac destructPrefix H :=
    destruct H as [tl H];
    simpl in H;
    simplify_eq H;
    intros.

  Ltac destructStackTopValues H :=
    destruct H as [tl H];
    simpl in H;
    destruct H as [H' H''];
    simplify_eq H'; clear H';
    simplify_eq H''; clear H'';
    intros.

Local variables initialisation

Initialisation of a local variables table based on a method signature and an operand stack, described as an inductive property.

  Inductive initVarsInd: list TType → TLocalStack → TLocalStack → TVars → Prop :=
  | InitVars_nil: ∀ sk,
    initVarsInd nil sk sk varsEmpty
  | initVars_one: ∀ t sig sk1 sk2 vars v vv,
    initVarsInd sig sk1 sk2 vars →
    ValVarMapping v (One vv) →
    let vars' := (varsSet (varFromNat (sizeOfTypes sig)) vv vars) in
    initVarsInd (t ::sig) (v ::sk1) sk2 vars'
  | initVars_two: ∀ t sig sk1 sk2 vars v vv1 vv2,
    initVarsInd sig sk1 sk2 vars →
    ValVarMapping v (Two vv1 vv2) →
    let vars' := (varsSet (varFromNat (sizeOfTypes sig)) vv1 vars) in
    let vars'' := (varsSet (varFromNat ((sizeOfTypes sig )+1)) vv2 vars') in
    initVarsInd (t ::sig) (v ::sk1) sk2 vars''.

Initialisation of a local variables table based on a method signature and an operand stack.

  Function initVars (args: list TValue) {struct args}: TVars :=
    match args with
    | nil ⇒ varsEmpty
    | (v::tl) ⇒
      let vars_tl := initVars tl in
      match transformValToVar v with
      | One vv ⇒
        varsSet (varFromNat (sizeOfValues args)) vv vars_tl
      | Two vv1 vv2 ⇒
        let vars' := (varsSet (varFromNat (sizeOfValues tl)) vv1 vars_tl) in
        varsSet (varFromNat ((sizeOfValues tl)+1)) vv2 vars'
      end
    end.

Resut or exception

Applies a function to the value held by a TResultOrException.

  Definition mapROX {A B: Type} (f: A → B) (arg: TResultOrException A): TResultOrException B :=
  match arg with
  | Result a ⇒ Result (f a)
  | Exception cn ⇒ Exception cn
  end.
End RuntimeStructuresFacts.