Library ValuesNTypes

A model of values used in Java Virtual Machine.

@author Patryk Czarnik

Require Import Common.
Require Import Numeric.
Require Import FNumeric.
Require Import Char.
Require Import List.

Values used within JVM and their types

Module of this type provides Coq types and operations for

values used within the JVM
types of those values
kinds -- a sort of simplified types

Module Type VALUES_AND_TYPES.
Local Open Scope Z_scope.

Prerequisities

Some auxiliary definitions before the main part.

Names

Class name.

Parameter TClassName: Set.

Class names are distinguishable.

Axiom PClassName_eqDec: eqDecS TClassName.

Field or method name.

Parameter TShortName: Set.

Short names are distinguishable.

Axiom PShortName_eqDec: eqDecS TShortName.

Program counter

Program counter -- a pointer to an instruction within method.

Parameter TPC: Set.

Equality on PCs is decidable.

Axiom PPC_eqDec: eqDecS TPC.

PC offset.

Parameter TOffset: Set.

Applies an offset to the given PC and returns the target PC.

Parameter jump: TOffset → TPC → TPC.

Numeric values

Imported modules

Numeric (for integer values) borrowed from Bicolano

  Declare Module M_Numeric_Bool: NUMERIC
    with Definition power := 1.
  Declare Module M_Numeric_Byte: NUMERIC
    with Definition power := 7.
  Declare Module M_Numeric_Short: NUMERIC
    with Definition power := 15.
  Declare Module M_Numeric_Int: NUMERIC
    with Definition power := 31.
  Declare Module M_Numeric_Long: NUMERIC
    with Definition power := 63.

  Declare Module M_Char: CHAR
    with Definition power := 16.

  Declare Module M_Numeric_Float: FNUMERIC
    with Definition precision := IEEE754.IEEE754_def.Single.
  Declare Module M_Numeric_Double: FNUMERIC
    with Definition precision := IEEE754.IEEE754_def.Double.

Locations

Location in the heap.

Parameter TLoc: Set.

Locations are distinguishable.

Axiom PLoc_eqDec: eqDecS TLoc.

The null location.

Parameter null: TLoc.

There exists a non-null location - useful for static semantics-related properties.

Axiom PNotNullExists: ∃ (loc: TLoc ), loc ≠ null.

Main definitions

JVM values

JVM values stored on operand stack

Inductive TValue: Set :=

Reference to an object or array

| VRef (loc: TLoc)

Return address for jsr / ret instructions

| VAddr (pc: TPC)

32-bit integer (Java int)

| VInt (ival: M_Numeric_Int.t)

32-bit floating point number (Java float)

| VFloat (fval: M_Numeric_Float.t)

64-bit integer (Java long)

| VLong (lval: M_Numeric_Long.t)

64-bit floating point number (Java double)

| VDouble (dval: M_Numeric_Double.t).

JVM values stored in local variables. 64-bit values (long and double are split into pairs when stored in variables, as all Java variables has 32 bits of size.

Inductive TVarValue: Set :=

Reference to an object or array

| VVRef (loc: TLoc)

Return address for jsr / ret instructions

| VVAddr (pc: TPC)

32-bit integer (Java int)

| VVInt (ival: M_Numeric_Int.t)

32-bit floating point number (Java float)

| VVFloat (fval: M_Numeric_Float.t)

First half of 64-bit integer (Java long)

| VVLong1 (lval: M_Numeric_Long.t)

Second half of 64-bit integer (Java long)

| VVLong2 (fake: unit)

First half of 64-bit float (Java double)

| VVDouble1 (dval: M_Numeric_Double.t)

Second half of 64-bit float (Java double)

| VVDouble2 (fake: unit).

JVM array values

Inductive TAValue: Set :=

Reference to an object or array

| VARef (loc: TLoc): TAValue

16-bit unsigned integer corresponding to a character (Java char)

| VAChar (cval: M_Char.t): TAValue

A logical value (Java boolean)

| VABool (zval: M_Numeric_Bool.t): TAValue

8-bit integer (Java byte)

| VAByte (bval: M_Numeric_Byte.t): TAValue

16-bit signed integer (Java short)

| VAShort (sval: M_Numeric_Short.t): TAValue

32-bit integer (Java int)

| VAInt (ival: M_Numeric_Int.t): TAValue

32-bit floating point number (Java float)

| VAFloat (fval: M_Numeric_Float.t): TAValue

64-bit integer (Java long)

| VALong (lval: M_Numeric_Long.t): TAValue

64-bit floating point number (Java double)

| VADouble (dval: M_Numeric_Double.t): TAValue.

Types

Java types reflected in JVM

Note: The type of return address is never used in the formalisation (as far as we do not perform 'bytecode verification'), and it never occurs explicitly in bytecode programs (in method signatures etc.).

For simplicity, we consider return address values to have the reference type Object.

Kinds of values

Kind of value is a simplified form of type which does not consider the actual class of a reference but treats all references in the same way.

Most of JVM instructions are defined for arguments of specific kinds. CoJaq formalisation makes many meta-instructions parametrised with kind of their arguments.

The set of kinds differs depending on runtime structure in which such values are stored. Therefore we provide several definitions of set of kinds below.

Kind of a value stored on operand stack.

Inductive TKind: Set :=

Reference to an object or array

| KRef

Return address. The address is required here to enable static semantics to control the PC

| KAddr (pc: TPC)

Java int

| KInt

Java float

| KFloat

Java long

| KLong

Java double

| KDouble.

Kind of a value stored in local variables.

Inductive TVarKind: Set :=

Reference to an object or array

| VKRef

Return address. The address is required here to enable static semantics to control the PC

| VKAddr (pc: TPC)

Java int

| VKInt

Java float

| VKFloat

First half of Java long

| VKLong1

Second half of Java long

| VKLong2

First half of Java double

| VKDouble1

Second half of Java double

| VKDouble2.

Kinds of variable load/store instructions. The set differs from TKind because the original astore instruction may be used for references and jsr/ret return addresses, which are of separate kinds.

Inductive TVarIKind: Set :=

Reference or return address

| VIKRef

Java int

| VIKInt

Java float

| VIKFloat

Java long

| VIKLong

Java double

| VIKDouble.

Kind of array store instructions. The set differs form the set of kinds stored in arrays because Byte and Boolean are glued together.

Inductive TArrayIKind: Set :=

Reference to an object or array

| AIKRef

16-bit integer corresponding to a character (Java char)

| AIKChar

Java byte or boolean - glued together in JVM array instructions

| AIKByteBool

16-bit integer (Java short)

| AIKShort

32-bit integer (Java int)

| AIKInt

32-bit floating point number (Java float)

| AIKFloat

64-bit integer (Java long)

| AIKLong

64-bit floating point number (Java double)

| AIKDouble.

Mappings and transformations

Kind for value or type

Returns the kind of the given value.

Returns the list of kinds corresponding to the given values.

Definition kindOfValues: list TValue → list TKind := map kindOfValue.

Returns the kind of the given variable value.

Returns the array kind of the given value.

Returns the kind corresponding to the given type.

Returns the list of kinds corresponding to the given types.

Definition kindOfTypes: list TType → list TKind := map kindOfType.

Returns the array instructon kind corresponding to the given type.

Default values

Default values for given kinds or types. Those values stand as initial values for object and array initialisation. They also constitute a proof that each kind in inhabited.

For any kind returns a value of that kind. It can be seen as a constructive proof that all kinds are inhabited. For some reasons we prefer to use 1 instead of 0 for numeric values.

Values used for initialisation of fields.

exampleForKind really returns a value of the desired kind.

  Lemma PexampleForKindConsistent: ∀ k, kindOfValue (exampleForKind k) = k.
  Proof.
    intros.
    destruct k; simpl; reflexivity.
  Qed.

defaultForKind really returns a value of the desired kind.

  Lemma PdefaultForKindConsistent: ∀ k, kindOfValue (defaultForKind k) = k.
  Proof.
    intros.
    destruct k; simpl; reflexivity.
  Qed.

Direct expression of the kind inhabitance property.

  Lemma PForEachKindExistsAValue:
    ∀ (k: TKind), ∃ (v: TValue ), kindOfValue v = k.
  Proof.
    intro k.
    ∃ (exampleForKind k).
    apply PexampleForKindConsistent.
  Qed.

For any list of kinds, there exists a list of corresponding values.

  Lemma PForEachKindListExistsValueList:
    ∀ (ks: list TKind), ∃ (vs: list TValue ), kindOfValues vs = ks.
  Proof.
    intros.
    induction ks.
    ∃ nil.
      simpl; reflexivity.
    destruct IHks as [tail].
    eexists (_::tail).
    simpl.
    f_equal.
    apply PexampleForKindConsistent.
    assumption.
  Qed.

The default and initial value for any type, as specified for Java fields.

  Definition defaultValueForType (t: TType): TValue :=
    match t with
    | ReferenceType _ ⇒ (VRef null)
    | BaseType BTChar ⇒ (VInt (M_Numeric_Int.zero))
    | BaseType BTBool ⇒ (VInt (M_Numeric_Int.zero))
    | BaseType BTByte ⇒ (VInt (M_Numeric_Int.zero))
    | BaseType BTShort ⇒ (VInt (M_Numeric_Int.zero))
    | BaseType BTInt ⇒ (VInt (M_Numeric_Int.zero))
    | BaseType BTFloat ⇒ (VFloat (M_Numeric_Float.zero))
    | BaseType BTLong ⇒ (VLong (M_Numeric_Long.zero))
    | BaseType BTDouble ⇒ (VDouble (M_Numeric_Double.zero))
    end.

  Lemma PdefaultValueForType_ForKind_Consistent:
    ∀ t: TType,
    defaultValueForType t = defaultForKind (kindOfType t).
  Proof.
    destruct t;
      [|destruct bt];
      simpl;
      reflexivity.
  Qed.

The default and initial value for any type, as specified for Java table cells.

  Definition defaultArrayValueForType (t: TType): TAValue :=
    match t with
    | ReferenceType _ ⇒ (VARef null)
    | BaseType BTChar ⇒ (VAChar (M_Char.zero))
    | BaseType BTBool ⇒ (VABool (M_Numeric_Bool.zero))
    | BaseType BTByte ⇒ (VAByte (M_Numeric_Byte.zero))
    | BaseType BTShort ⇒ (VAShort (M_Numeric_Short.zero))
    | BaseType BTInt ⇒ (VAInt (M_Numeric_Int.zero))
    | BaseType BTFloat ⇒ (VAFloat (M_Numeric_Float.zero))
    | BaseType BTLong ⇒ (VALong (M_Numeric_Long.zero))
    | BaseType BTDouble ⇒ (VADouble (M_Numeric_Double.zero))
    end.

Conversions between numeric values

Conversion between stack and variable values

For actual values

This relation defines correspondence between operand stack values and variable values. A single stack value can be represented as one or two variables.

  Inductive ValVarMapping: TValue → TOneOrTwo TVarValue → Prop :=
  | VVMap_Ref : ∀ loc, ValVarMapping (VRef loc) (One (VVRef loc))
  | VVMap_Addr : ∀ pc, ValVarMapping (VAddr pc) (One (VVAddr pc))
  | VVMap_Int : ∀ ival, ValVarMapping (VInt ival) (One (VVInt ival))
  | VVMap_Float : ∀ fval, ValVarMapping (VFloat fval) (One (VVFloat fval))
  | VVMap_Long : ∀ lval, ValVarMapping (VLong lval) (Two (VVLong1 lval) (VVLong2 tt))
  | VVMap_Double : ∀ dval, ValVarMapping (VDouble dval) (Two (VVDouble1 dval) (VVDouble2 tt)).

Any stack value can be transformed into one or a pair of variable values.

  Definition transformValToVar (v: TValue) : TOneOrTwo TVarValue :=
    match v with
    | VRef loc ⇒ One (VVRef loc)
    | VAddr pc ⇒ One (VVAddr pc)
    | VInt ival ⇒ One (VVInt ival)
    | VFloat fval ⇒ One (VVFloat fval)
    | VLong lval ⇒ Two (VVLong1 lval) (VVLong2 tt)
    | VDouble dval ⇒ Two (VVDouble1 dval) (VVDouble2 tt)
    end.

The above definitions (functional and inductive) are equivalent.

  Lemma PvalVarMapping_transform_equiv: ∀ v vv,
    ValVarMapping v vv ↔ transformValToVar v = vv.
  Proof.
    intros.
    split; intro H.
    destruct v;
      simpl;
      inversion H; clear H; subst;
      reflexivity.
    destruct v;
      simpl in H;
      subst;
      constructor.
  Qed.

For kinds

  Inductive ValVarKindMapping: TKind → TOneOrTwo TVarKind → Prop :=
  | VVKMap_Ref: ValVarKindMapping KRef (One VKRef)
  | VVKMap_Addr: ∀ pc, ValVarKindMapping (KAddr pc) (One (VKAddr pc))
  | VVKMap_Int: ValVarKindMapping KInt (One VKInt )
  | VVKMap_Float: ValVarKindMapping KFloat (One VKFloat)
  | VVKMap_Long: ValVarKindMapping KLong (Two VKLong1 VKLong2)
  | VVKMap_Double: ValVarKindMapping KDouble (Two VKDouble1 VKDouble2).

  Definition transformKToVarK (k: TKind) : TOneOrTwo TVarKind :=
    match k with
    | KRef ⇒ One VKRef
    | KAddr pc ⇒ One (VKAddr pc)
    | KInt ⇒ One VKInt
    | KFloat ⇒ One VKFloat
    | KLong ⇒ Two VKLong1 VKLong2
    | KDouble ⇒ Two VKDouble1 VKDouble2
    end.

The above definitions (functional and inductive) are equivalent.

  Lemma PvalVarKindMapping_transform_equiv: ∀ k vk,
    ValVarKindMapping k vk ↔ transformKToVarK k = vk.
  Proof.
    intros.
    split; intro H.
    destruct k;
      simpl;
      inversion H; clear H; subst;
      reflexivity.
    destruct k;
      simpl in H;
      subst;
      constructor.
  Qed.

Consistency of mappings defined for values and for kinds

  Lemma PtransformValToVarValConsistent: ∀ v,
    transformKToVarK (kindOfValue v) = map_oneOrTwo kindOfVarValue (transformValToVar v).
  Proof.
    destruct v; simpl; reflexivity.
  Qed.

  Lemma PValVarMappingConsistent: ∀ v vv12,
    ValVarMapping v vv12 → ValVarKindMapping (kindOfValue v) (map_oneOrTwo kindOfVarValue vv12).
  Proof.
    intros.
    destruct v; destruct vv12;
      inversion H; subst; clear H;
      simpl;
      constructor.
  Qed.

  Lemma PValVarMappingConsistentInv_AVal_EVar: ∀ v vk12,
    ValVarKindMapping (kindOfValue v) vk12 →
    ∃ vv12,
         vk12 = (map_oneOrTwo kindOfVarValue vv12 )
      ∧ ValVarMapping v vv12.
  Proof.
    intros.
    ∃ (transformValToVar v).
    destruct v; destruct vk12;
      inversion H; subst; clear H;
      simpl;
      intuition constructor.
  Qed.

  Lemma PValVarMappingConsistentInv_AVar_EVal: ∀ k vv12,
    ValVarKindMapping k (map_oneOrTwo kindOfVarValue vv12) →
    ∃ v,
         k = kindOfValue v
      ∧ ValVarMapping v vv12.
  Proof.
    intros.
    destruct k;
      inversion H; clear H;
      destruct vv12;
    match goal with
    | [Heq: (One ?vk1 = _) |- _] ⇒
      simpl in Heq;
      simplify_eq Heq; clear Heq; intros H;
      destruct elem;
      simpl in H;
      simplify_eq H; clear H; intros
    | [Heq: (Two ?vk1 ?vk2 = _) |- _] ⇒
      simpl in Heq;
      simplify_eq Heq; clear Heq; intros H1 H2;
      destruct elem1;
      destruct elem2;
      simpl in H1, H2;
      simplify_eq H1; clear H1;
      simplify_eq H2; clear H2;
      intros
    | _ ⇒ idtac
    end.

   ∃ (VRef loc).
   intuition constructor.

   subst pc1 pc0.
   ∃ (VAddr pc).
   intuition constructor.

   ∃ (VInt ival).
   intuition constructor.

   ∃ (VFloat fval).
   intuition constructor.

   destruct fake.    ∃ (VLong lval).
   intuition constructor.

   destruct fake.
   ∃ (VDouble dval).
   intuition constructor.
  Qed.

  Lemma PValVarMappingConsistentInv_EVal_EVar: ∀ k vk12,
    ValVarKindMapping k vk12 →
    ∃ v vv12,
         k = (kindOfValue v )
      ∧ vk12 = (map_oneOrTwo kindOfVarValue vv12 )
      ∧ ValVarMapping v vv12.
  Proof.

This one could probably be inferred from one of the previous (with defaultForKind k as v), but it was easier to provide a separate proof.

    intros.
    ∃ (defaultForKind k).
    ∃ (transformValToVar (defaultForKind k)).
    destruct k; destruct vk12;
      inversion H; subst; clear H;
      simpl;
      intuition constructor.
  Qed.

Conversion between stack and array values

For actual values

Transforms a value av storable in arrays into appropriate value to operate in stack.

  Definition transformAToValue (av: TAValue) : TValue :=
    match av with
    | VARef loc ⇒ VRef loc
    | VAChar cval ⇒ VInt (char2int cval)
    | VABool zval ⇒ VInt (bool2int zval)
    | VAByte bval ⇒ VInt (byte2int bval)
    | VAShort sval ⇒ VInt (short2int sval)
    | VAInt ival ⇒ VInt ival
    | VAFloat fval ⇒ VFloat fval
    | VALong lval ⇒ VLong lval
    | VADouble dval ⇒ VDouble dval
    end.

  Definition transformVARef (v: TValue) : option TAValue :=
    match v with
    | VRef loc ⇒ Some (VARef loc)
    | _ ⇒ None
    end.

  Definition transformVAChar (v: TValue) : option TAValue :=
    match v with
    | VInt iv ⇒ Some (VAChar (int2char iv))
    | _ ⇒ None
    end.

  Definition transformVAByte (v: TValue) : option TAValue :=
    match v with
    | VInt iv ⇒ Some (VAByte (int2byte iv))
    | _ ⇒ None
    end.

  Definition transformVABool (v: TValue) : option TAValue :=
    match v with
    | VInt iv ⇒ Some (VABool (int2bool iv))
    | _ ⇒ None
    end.

  Definition transformVAShort (v: TValue) : option TAValue :=
    match v with
    | VInt iv ⇒ Some (VAShort (int2short iv))
    | _ ⇒ None
    end.

  Definition transformVAInt (v: TValue) : option TAValue :=
    match v with
    | VInt iv ⇒ Some (VAInt iv)
    | _ ⇒ None
    end.

  Definition transformVAFloat (v: TValue) : option TAValue :=
    match v with
    | VFloat iv ⇒ Some (VAFloat iv)
    | _ ⇒ None
    end.

  Definition transformVALong (v: TValue) : option TAValue :=
    match v with
    | VLong iv ⇒ Some (VALong iv)
    | _ ⇒ None
    end.

  Definition transformVADouble (v: TValue) : option TAValue :=
    match v with
    | VDouble iv ⇒ Some (VADouble iv)
    | _ ⇒ None
    end.

Transforms a JVM value v into appropriate value storable in arrays of component type t. In case the transformation is impossible None is returned

  Definition transformAFromValue (t: TType) (v: TValue) : option TAValue :=
    match t with
    | ReferenceType _ ⇒ transformVARef v
    | BaseType BTChar ⇒ transformVAChar v
    | BaseType BTBool ⇒ transformVABool v
    | BaseType BTByte ⇒ transformVAByte v
    | BaseType BTShort ⇒ transformVAShort v
    | BaseType BTInt ⇒ transformVAInt v
    | BaseType BTFloat ⇒ transformVAFloat v
    | BaseType BTLong ⇒ transformVALong v
    | BaseType BTDouble ⇒ transformVADouble v
    end.

For kinds

Appropriate kind of value for a given kind of array (in JVM e.g. bytes stored in arrays are represented as ints outside arrays).

Consistency of mappings defined for values and for kinds

  Lemma PtransformAToValueKindConsistent: ∀ av,
    kindOfValue (transformAToValue av) = kindOfArrayKind (kindOfAValue av).
  Proof.
    destruct av; simpl; reflexivity.
  Qed.

  Lemma PtransformAFromValueKindConsistent: ∀ t v av,
    transformAFromValue t v = Some av →
    kindOfValue v = kindOfArrayKind (kindOfAValue av).
  Proof.
    intros.
    destruct t; [|destruct bt];
      destruct v;
      simpl in H;
      try discriminate H;
      injection H; clear H; intro H;
      subst;
      simpl;
      reflexivity.
  Qed.

Size of values

We have two categories of values.

  Inductive TValueCategory: Set :=
  | cat1
  | cat2.

Returns the size of values of the given kind expressed in the number of variables required to hold the value.

  Definition sizeOfCat (cat: TValueCategory): nat :=
    match cat with
    | cat1 ⇒ 1%nat
    | cat2 ⇒ 2%nat
    end.

  Definition catOfKind (k: TKind): TValueCategory :=
    match k with
    | KRef ⇒ cat1
    | KAddr pc⇒ cat1
    | KInt ⇒ cat1
    | KFloat ⇒ cat1
    | KLong ⇒ cat2
    | KDouble ⇒ cat2
    end.

  Inductive isCat: TValueCategory → TKind → Prop :=
  | IsCat_Ref: isCat cat1 KRef
  | IsCat_Addr: ∀ pc, isCat cat1 (KAddr pc)
  | IsCat_Int: isCat cat1 KInt
  | IsCat_Float: isCat cat1 KFloat
  | IsCat_Long: isCat cat2 KLong
  | IsCat_Double: isCat cat2 KDouble.

  Lemma PisCatOK: ∀ cat k,
    isCat cat k ↔ catOfKind k = cat.
  Proof.
    intros.
    destruct k;
      destruct cat;
      simpl;
      (split;
      [ intro H;
        inversion H; clear H; subst;
        try reflexivity
      | intro H;
        simplify_eq H;
        try constructor]).
  Qed.

  Inductive isCatVIK: TValueCategory → TVarIKind → Prop :=
  | IsCatVIK_Ref: isCatVIK cat1 VIKRef
  | IsCatVIK_Int: isCatVIK cat1 VIKInt
  | IsCatVIK_Float: isCatVIK cat1 VIKFloat
  | IsCatVIK_Long: isCatVIK cat2 VIKLong
  | IsCatVIK_Double: isCatVIK cat2 VIKDouble.

Returns the size of values of the given kind expressed in the number of variables required to hold the value.

  Definition sizeOfKind (k: TKind): nat :=
    sizeOfCat (catOfKind k).

  Lemma PsizeOfKindCat1: ∀ k, isCat cat1 k ↔ sizeOfKind k = 1%nat.
  Proof.
    intro k.
    split; intro H.
    destruct k; simpl; inversion H; intuition.
    destruct k; simpl in H.
    constructor.
    constructor.
    constructor.
    constructor.
    discriminate H.
    discriminate H.
  Qed.

  Lemma PsizeOfKindCat2: ∀ k, isCat cat2 k ↔ sizeOfKind k = 2%nat.
  Proof.
    intro k.
    split; intro H.
    destruct k; simpl; inversion H; intuition.
    destruct k; simpl in H.
    discriminate H.
    discriminate H.
    discriminate H.
    discriminate H.
    constructor.
    constructor.
  Qed.

Returns the size of the given value expressed in the number of variables required to hold the value.

Definition sizeOfValue (v: TValue): nat :=
sizeOfKind (kindOfValue v).

Returns the sum of sizes of the given values expressed in the number of variables required to hold values of those types.

  Definition sizeOfValues (ts: list TValue): nat :=
    let f res t := plus res (sizeOfValue t) in
    fold_left f ts O.

Returns the size of values of the given type expressed in the number of variables required to hold the value.

Definition sizeOfType (t: TType): nat :=
sizeOfKind (kindOfType t).

Returns the sum of sizes of the given types expressed in the number of variables required to hold values of those types.

  Definition sizeOfTypes (ts: list TType): nat :=
    let f res t := plus res (sizeOfType t) in
    fold_left f ts O.
End VALUES_AND_TYPES.