Library Sem_Stackop


Semantics of stack instructions

@author Patryk Czarnik

Require Import List.
Require Import Common.
Require Import Program.
Require Import ProgramStructures.
Require Import RuntimeStructures.
Require Import ValuesNTypes.
Require Import ArithOps.
Require Import Arithmetic.
Require Import AllStructures.

Module of this type provides detailed semantics of local stack instructions TStackInstr.
Module Type SEM_STACKOP.

Included modules

  Declare Module M_AllStructures : ALL_STRUCTURES.

  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 M_Arithmetics.
  Import ArithmeticOperators.

  Import List.ListNotations.
  Open Local Scope type_scope.

Generic operations


  Section GenericOps.
Static and dynamic semantics of generic stack operators, such as dup, given as a mapping between kind-level patterns of the top of the local stack.
  Inductive semStackGeneric : TGenericOp →
    list TValueCategory → list nat → list nat → Prop :=
  | SemStackGeneric_nop: semStackGeneric Op_nop
      [] [] []
  | SemStackGeneric_dup: semStackGeneric Op_dup
      [cat1] [0] [0;0]
  | SemStackGeneric_dup_x1: semStackGeneric Op_dup_x1
      [cat1;cat1] [0;1] [0;1;0]
  | SemStackGeneric_dup_x2_form1: semStackGeneric Op_dup_x2
      [cat1;cat1;cat1] [0;1;2] [0;1;2;0]
  | SemStackGeneric_dup_x2_form2: semStackGeneric Op_dup_x2
      [cat1;cat2] [0;1] [0;1;0]
  | SemStackGeneric_dup2_form1: semStackGeneric Op_dup2
      [cat1;cat1] [0;1] [0;1;0;1]
  | SemStackGeneric_dup2_form2: semStackGeneric Op_dup2
      [cat2] [0] [0;0]
  | SemStackGeneric_dup2_x1_form1: semStackGeneric Op_dup2_x1
      [cat1;cat1;cat1] [0;1;2] [0;1;2;0;1]
  | SemStackGeneric_dup2_x1_form2: semStackGeneric Op_dup2_x1
      [cat2;cat1] [0;1] [0;1;0]
  | SemStackGeneric_dup2_x2_form1: semStackGeneric Op_dup2_x2
      [cat1;cat1;cat1;cat1] [0;1;2;3] [0;1;2;3;0;1]
  | SemStackGeneric_dup2_x2_form2: semStackGeneric Op_dup2_x2
      [cat2;cat1;cat1] [0;1;2] [0;1;2;0]
  | SemStackGeneric_dup2_x2_form3: semStackGeneric Op_dup2_x2
      [cat1;cat1;cat2] [0;1;2] [0;1;2;0;1]
  | SemStackGeneric_dup2_x2_form4: semStackGeneric Op_dup2_x2
      [cat2;cat2] [0;1] [0;1;0]
  | SemStackGeneric_pop: semStackGeneric Op_pop
      [cat1] [0] []
  | SemStackGeneric_pop2_form1: semStackGeneric Op_pop2
      [cat1;cat1] [0;1] []
  | SemStackGeneric_pop2_form2: semStackGeneric Op_pop2
      [cat2] [0] []
  | SemStackGeneric_swap: semStackGeneric Op_swap
      [cat1;cat1] [0;1] [1;0]
  .
  End GenericOps.

Dynamic semantics

The dynamic semantics of stack operations, provided as a relation on the top of the stack represented as a list of values.
  Inductive semStack : TStackInstr → list TValue → TResultOrException (list TValue) → Prop :=
  | SemStack_Generic:
    ∀ op klists pattern pattern',
      semStackGeneric op klists pattern pattern' →
      ∀ (fv: nat → TValue),
        (∀ i cat, nth_error klists i = Some cat → isCat cat (kindOfValue (fv i))) →
      semStack (SI_Generic op) (map fv pattern) (Result (map fv pattern'))

  | SemStack_Const:
    ∀ k arg,
      kindOfValue arg = k →
      semStack (SI_Const k arg) [] (Result [arg])

  | SemStack_UnOp:
    ∀ unop k arg res,
      let arithmetic := arithmeticForKind k in
      M_ArithmeticTypes.arithUnOp arithmetic unop arg res →
      semStack (SI_Unop k unop) [arg] (Result [res])

  | SemStack_BinOp:
    ∀ binop k arg1 arg2 res,
      let arithmetic := arithmeticForKind k in
      M_ArithmeticTypes.arithBinOp arithmetic binop arg1 arg2 (Some res) →
      semStack (SI_Binop k binop) [arg2;arg1] (Result [res])

  | SemStack_BinOp_ArithmeticException:
    ∀ binop k arg1 arg2,
      let arithmetic := arithmeticForKind k in
      M_ArithmeticTypes.arithBinOp arithmetic binop arg1 arg2 None →
      semStack (SI_Binop k binop) [arg2;arg1] (Exception StandardNames.ArithmeticException)

  | SemStack_Cmpi:
    ∀ cmpiop k arg1 arg2 res,
      let arithmetic := arithmeticForKind k in
      M_ArithmeticTypes.arithCmpi arithmetic cmpiop arg1 arg2 res →
      semStack (SI_Cmpi k cmpiop) [arg2;arg1] (Result [res])

  | SemStack_Cast:
    ∀ castop k arg res,
      let arithmetic := arithmeticForKind k in
      M_ArithmeticTypes.arithCast arithmetic castop arg res →
      semStack (SI_Cast k castop) [arg] (Result [res])
  .

Static semantics

Lower level support for static semantics

Static semantics of unary arithmetic operations given as a list of kinds for which a given operator is defined. It is assumed that the parameter and the result are of the same kind.
  Inductive staticSemStackUnOp : TUnOp → list TKind → Prop :=
  | UnOpStaticSem_add : staticSemStackUnOp UnOp_neg [KInt;KFloat;KLong;KDouble]
  .

Completness of the above definition: Each case mentioned there has its counterpart in the values-level semantics of operators.
  Lemma PstaticSemStackUnOp: ∀ unop kinds,
    staticSemStackUnOp unop kinds →
    ∀ k, In k kinds →
      ∃ arg res,
           kindOfValue arg = k
        ∧ kindOfValue res = k
        ∧ M_ArithmeticTypes.arithUnOp (arithmeticForKind k) unop arg res.
  Proof.
    intros.
    (inversion H; subst; clear H;
      destruct k; simpl in *;
      decompose [or] H0; clear H0;
      try contradiction;
    match goal with
    | [Heq: (?k1 = ?k2) |- _] ⇒
      simplify_eq Heq; clear Heq; intros;
      ∃ (defaultForKind k1);
      eexists
    | _ ⇒ idtac
    end);
    (split;
    [apply PdefaultForKindConsistent
    | split;
      [idtac | econstructor]]);
    simpl; reflexivity.
  Qed.

Static semantics of binary arithmetic operations given as a list of kinds for which a given operator is defined. It is assumed that the two parameters and the result are of the same kind.
  Inductive staticSemStackBinOp : TBinOp → list TKind → Prop :=
  | BinOpStaticSem_add : staticSemStackBinOp BinOp_add [KInt;KFloat;KLong;KDouble]
  | BinOpStaticSem_sub : staticSemStackBinOp BinOp_sub [KInt;KFloat;KLong;KDouble]
  | BinOpStaticSem_mul : staticSemStackBinOp BinOp_mul [KInt;KFloat;KLong;KDouble]
  | BinOpStaticSem_div : staticSemStackBinOp BinOp_div [KInt;KFloat;KLong;KDouble]
  | BinOpStaticSem_rem : staticSemStackBinOp BinOp_rem [KInt;KFloat;KLong;KDouble]
  | BinOpStaticSem_xor : staticSemStackBinOp BinOp_xor [KInt;KLong]
  | BinOpStaticSem_and : staticSemStackBinOp BinOp_and [KInt;KLong]
  | BinOpStaticSem_or : staticSemStackBinOp BinOp_or [KInt;KLong]
  | BinOpStaticSem_shl : staticSemStackBinOp BinOp_shl [KInt;KLong]
  | BinOpStaticSem_shr : staticSemStackBinOp BinOp_shr [KInt;KLong]
  | BinOpStaticSem_ushr: staticSemStackBinOp BinOp_ushr [KInt;KLong]
  .

A supplement to the above definition which specifies for which kinds an operation can have no result and cause an arithemtic exception.
  Inductive staticSemStackBinOp_NoResult : TBinOp → list TKind → Prop :=
  | BinOpStaticSemNoResult_div : staticSemStackBinOp_NoResult BinOp_div [KInt;KLong]
  | BinOpStaticSemNoResult_rem : staticSemStackBinOp_NoResult BinOp_rem [KInt;KLong]
  .

Completness of the above definition (positive case): Each case mentioned there has its counterpart in the values-level semantics of operators.
  Lemma PstaticSemStackBinOp: ∀ binop kinds,
    staticSemStackBinOp binop kinds →
    ∀ k, In k kinds →
      ∃ arg1 arg2 res,
           kindOfValue arg1 = k
        ∧ kindOfValue arg2 = k
        ∧ kindOfValue res = k
        ∧ M_ArithmeticTypes.arithBinOp (arithmeticForKind k) binop arg1 arg2 (Some res).
  Proof.
    intros.
    (inversion H; subst; clear H;
      destruct k; simpl in *;
      decompose [or] H0; clear H0;
      try contradiction;
    match goal with
    | [Heq: (?k1 = ?k2) |- _] ⇒
      simplify_eq Heq; clear Heq; intros;
      ∃ (exampleForKind k1);
      ∃ (exampleForKind k1);
      eexists
    | _ ⇒ idtac
    end);
    (split;
    [apply PexampleForKindConsistent
    | split;
      [apply PexampleForKindConsistent
      | split;
        [idtac | econstructor]]]);
    simpl;
    try reflexivity.
    apply M_Numeric_Int.PoneIsNotZero.
    apply M_Numeric_Long.PoneIsNotZero.
    apply M_Numeric_Int.PoneIsNotZero.
    apply M_Numeric_Long.PoneIsNotZero.
  Qed.

Completness of the above definition (exceptional case).
  Lemma PstaticSemStackBinOp_NoResult: ∀ binop kinds,
    staticSemStackBinOp_NoResult binop kinds →
    ∀ k, In k kinds →
      ∃ arg1 arg2,
           kindOfValue arg1 = k
        ∧ kindOfValue arg2 = k
        ∧ M_ArithmeticTypes.arithBinOp (arithmeticForKind k) binop arg1 arg2 None.
  Proof.
    intros.
    inversion H; subst; clear H;
      destruct k; simpl in *;
      decompose [or] H0; clear H0;
      try contradiction;
      match goal with
      | [Heq: (?k1 = ?k2) |- _] ⇒
        simplify_eq Heq; clear Heq; intros
      end.

4 cases remains: idiv, ldiv, irem, lrem
   ∃ (VInt M_Numeric_Int.zero).
   ∃ (VInt M_Numeric_Int.zero).
   simpl; intuition.
   constructor.

   ∃ (VLong M_Numeric_Long.zero).
   ∃ (VLong M_Numeric_Long.zero).
   simpl; intuition.
   constructor.

   ∃ (VInt M_Numeric_Int.zero).
   ∃ (VInt M_Numeric_Int.zero).
   simpl; intuition.
   constructor.

   ∃ (VLong M_Numeric_Long.zero).
   ∃ (VLong M_Numeric_Long.zero).
   simpl; intuition.
   constructor.
  Qed.

Static semantics of binary comparison operators presenting result as int.
  Inductive staticSemStackCmpi : TCmpiOp → list TKind → Prop :=
  | CmpiStaticSem_cmpl : staticSemStackCmpi CmpiOp_cmpl [KFloat;KLong;KDouble]
  | CmpiStaticSem_cmpg : staticSemStackCmpi CmpiOp_cmpg [KFloat;KDouble]
  .

Completness of the above definition: Each case mentioned there has its counterpart in the values-level semantics of operators.
  Lemma PstaticSemStackCmpi: ∀ cmpiop kinds,
    staticSemStackCmpi cmpiop kinds →
    ∀ k, In k kinds →
      ∃ arg1 arg2 res,
           kindOfValue arg1 = k
        ∧ kindOfValue arg2 = k
        ∧ kindOfValue res = KInt
        ∧ M_ArithmeticTypes.arithCmpi (arithmeticForKind k) cmpiop arg1 arg2 res.
  Proof.
    intros.
    (inversion H; subst; clear H;
      destruct k; simpl in *;
      decompose [or] H0; clear H0;
      try contradiction;
    match goal with
    | [Heq: (?k1 = ?k2) |- _] ⇒
      simplify_eq Heq; clear Heq; intros;
      ∃ (defaultForKind k1);
      ∃ (defaultForKind k1);
      eexists
    | _ ⇒ idtac
    end);
    (split;
    [apply PdefaultForKindConsistent
    | split;
      [apply PdefaultForKindConsistent
      | split;
        [idtac | econstructor]]]);
    simpl; reflexivity.
  Qed.

Static semantics of arithmetic cast operations given as a list of kinds for which a given operator is defined. This is the kind of argument, while the kind of result is always defined as kindOfCastOp.
  Inductive staticSemStackCastOp : TCastOp → list TKind → Prop :=
  | CastOpStaticSem_b : staticSemStackCastOp CastOp_b [KInt]
  | CastOpStaticSem_c : staticSemStackCastOp CastOp_c [KInt]
  | CastOpStaticSem_s : staticSemStackCastOp CastOp_s [KInt]
  | CastOpStaticSem_i : staticSemStackCastOp CastOp_i [KFloat;KLong;KDouble]
  | CastOpStaticSem_l : staticSemStackCastOp CastOp_l [KInt;KFloat;KDouble]
  | CastOpStaticSem_f : staticSemStackCastOp CastOp_f [KInt;KLong;KDouble]
  | CastOpStaticSem_d : staticSemStackCastOp CastOp_d [KInt;KFloat;KLong]
  .

Completness of the above definition: Each case mentioned there has its counterpart in the values-level semantics of operators.
  Lemma PstaticSemStackCastOp: ∀ castop kinds,
    staticSemStackCastOp castop kinds →
    ∀ k, In k kinds →
      ∃ arg res,
           kindOfValue arg = k
        ∧ kindOfValue res = (kindOfCastOp castop)
        ∧ M_ArithmeticTypes.arithCast (arithmeticForKind k) castop arg res.
  Proof.
    intros.
    try (inversion H; subst; clear H;
      simpl in *;
      try contradiction;
      destruct k;
      decompose [or] H0; clear H0;
      try contradiction;
    match goal with
    | [Heq: (?k1 = ?k2) |- _] ⇒
      simplify_eq Heq; clear Heq; intros;
      ∃ (defaultForKind k1);
      eexists
    | _ ⇒ idtac
    end;
    (split;
    [apply PdefaultForKindConsistent
    | split;
      [idtac | econstructor]]);
    simpl; reflexivity).
  Qed.

The actual definition

The static (kind-level) semantics of stack operations, provided as a relation on the top of the stack projected to a list of kinds.
  Inductive staticSemStack : TStackInstr → list TKind → TResultOrException (list TKind) → Prop :=
  | StaticSemStack_Generic:
    ∀ op klists pattern pattern',
      semStackGeneric op klists pattern pattern' →
      ∀ (fk: nat → TKind),
        (∀ i cat, nth_error klists i = Some cat → isCat cat (fk i)) →
        staticSemStack (SI_Generic op) (map fk pattern) (Result (map fk pattern'))

  | StaticSemStack_Const:
    ∀ k arg,
      kindOfValue arg = k →
      staticSemStack (SI_Const k arg) [] (Result [k])

  | StaticSemStack_UnOp:
    ∀ unop kinds,
      staticSemStackUnOp unop kinds →
      ∀ k, In k kinds →
        staticSemStack (SI_Unop k unop) [k] (Result [k])

  | StaticSemStack_BinOp:
    ∀ binop kinds,
      staticSemStackBinOp binop kinds →
      ∀ k, In k kinds →
        staticSemStack (SI_Binop k binop) [k;k] (Result [k])

  | StaticSemStack_BinOp_Exn:
    ∀ binop kinds,
      staticSemStackBinOp_NoResult binop kinds →
      ∀ k, In k kinds →
        staticSemStack (SI_Binop k binop) [k;k] (Exception StandardNames.ArithmeticException)

  | StaticSemStack_Cmpi:
    ∀ cmpiop kinds,
      staticSemStackCmpi cmpiop kinds →
      ∀ k, In k kinds →
        staticSemStack (SI_Cmpi k cmpiop) [k;k] (Result [KInt])

  | StaticSemStack_CastOp:
    ∀ castop kinds,
      staticSemStackCastOp castop kinds →
      ∀ k, In k kinds →
        staticSemStack (SI_Cast k castop) [k] (Result [kindOfCastOp castop])
  .

Correctness

Guarantees that every step in the dynamic semantics is covered by the static semantics.
  Lemma staticSemStackConsistent: ∀ (si: TStackInstr) (vs: list TValue) (vsR': TResultOrException (list TValue)),
      semStack si vs vsR' →
      staticSemStack si (kindOfValues vs) (mapROX kindOfValues vsR').
  Proof.
    intros.
    inversion H; clear H; subst;
      simpl.

SemStack_Generic
    assert (L1: ∀ l, kindOfValues (map fv l) = map (fun x ⇒ (kindOfValue (fv x))) l).
      intro l.
      unfold kindOfValues.
      induction l.
      simpl.
      reflexivity.

      simpl.
      rewrite IHl.
      reflexivity.
    rewrite L1.
    rewrite L1.
    econstructor.
    eassumption.
    assumption.

SemStack_Const
    simpl.
    constructor.
    reflexivity.

SemStack_UnOp
    assert (Pconsistent := (M_Arithmetics.PArithmeticConsistentKindUnOp) unop k arg res H0).
    decompose [and] Pconsistent; clear Pconsistent.
    simpl.
    rewrite H; clear H.
    rewrite H1; clear H1.
    destruct unop;
      destruct k;
      try inversion H0;
      (econstructor;
       [econstructor
       |simpl; intuition trivial]).

SemStack_BinOp
    assert (Pconsistent := (M_Arithmetics.PArithmeticConsistentKindBinOp) binop k arg1 arg2 res H0).
    decompose [and] Pconsistent; clear Pconsistent.
    simpl.
    rewrite H; clear H.
    rewrite H2; clear H2.
    rewrite H3; clear H3.
    destruct binop;
      destruct k;
      try inversion H0;
      (econstructor;
       [econstructor
       |simpl; intuition trivial]).

SemStack_BinOp_Exn
    destruct binop;
      destruct k;
      try inversion H0;
      (econstructor;
       [econstructor
       |simpl; intuition trivial]).

SemStack_Cmpi
    assert (Pconsistent := (M_Arithmetics.PArithmeticConsistentKindCmpi) cmpiop k arg1 arg2 res H0).
    decompose [and] Pconsistent; clear Pconsistent.
    simpl.
    rewrite H; clear H.
    rewrite H2; clear H2.
    rewrite H3; clear H3.
    destruct cmpiop;
      destruct k;
      try inversion H0;
      (econstructor;
       [econstructor
       |simpl; intuition trivial]).

SemStack_CastOp
    assert (Pconsistent := (M_Arithmetics.PArithmeticConsistentKindCastOp) castop k arg res H0).
    decompose [and] Pconsistent; clear Pconsistent.
    simpl.
    rewrite H; clear H.
    rewrite H1; clear H1.
    destruct castop;
      destruct k;
      try inversion H0;
      (econstructor;
       [econstructor
       |simpl; intuition trivial]).
Qed.

Auxiliary lemma related to map and lists.
  Lemma PmapPattern: ∀ (fk: nat → TKind) (pattern: list nat),
      kindOfValues (map (fun i ⇒ defaultForKind (fk i)) pattern) = map fk pattern.
  Proof.
    intros.
    induction pattern.
    simpl.
    reflexivity.

    simpl.
    f_equal.
    apply PdefaultForKindConsistent.
    assumption.
  Qed.

Guarantees that every step in the static semantics is motivated by a corresponding step in the dynamic semantics.
  Lemma staticSemStackComplete: ∀ (si: TStackInstr) (ks: list TKind) (ksR': TResultOrException (list TKind)),
      staticSemStack si ks ksR' →
      ∃ vs vsR',
           kindOfValues vs = ks
        ∧ mapROX kindOfValues vsR' = ksR'
        ∧ semStack si vs vsR'.
  Proof.
    intros.
    inversion H; subst; clear H.

StaticSemStack_Generic
    set (fv := fun i ⇒ defaultForKind (fk i)).
    ∃ (map fv pattern).
    ∃ (Result (map fv pattern')).
    intuition.
    apply PmapPattern.
    simpl;
      f_equal.
    apply PmapPattern.
    econstructor.
    eassumption.
    intros.
    replace (kindOfValue (fv i)) with (fk i).
    apply H1.
    assumption.
    symmetry; apply PdefaultForKindConsistent.

StaticSemStack_Const
    ∃ [].
    ∃ (Result [arg]).
    intuition.
    constructor.
    reflexivity.

StaticSemStack_UnOp
    eapply PstaticSemStackUnOp in H0.
    destruct H0 as [arg H].
    destruct H as [res H].
    ∃ [arg].
    ∃ (Result [res]).
    simpl.
    intuition.
    f_equal; eassumption.
    f_equal; f_equal; eassumption.
    constructor.
    assumption.
    assumption.

StaticSemStack_BinOp
    eapply PstaticSemStackBinOp in H0.
    destruct H0 as [arg1 H].
    destruct H as [arg2 H].
    destruct H as [res H].
    ∃ [arg2;arg1].
    ∃ (Result [res]).
    simpl.
    intuition.
    f_equal.
    eassumption.
    f_equal; eassumption.
    f_equal; f_equal; eassumption.
    constructor.
    assumption.
    assumption.

StaticSemStack_BinOp_Exn
    eapply PstaticSemStackBinOp_NoResult in H0.
    destruct H0 as [arg1 H].
    destruct H as [arg2 H].
    ∃ [arg2;arg1].
    ∃ (Exception StandardNames.ArithmeticException).
    simpl.
    intuition.
    f_equal.
    eassumption.
    f_equal; eassumption.
    constructor.
    assumption.
    assumption.

StaticSemStack_Cmpi
    eapply PstaticSemStackCmpi in H0.
    destruct H0 as [arg1 H].
    destruct H as [arg2 H].
    destruct H as [res H].
    ∃ [arg2;arg1].
    ∃ (Result [res]).
    simpl.
    intuition.
    f_equal.
    eassumption.
    f_equal; eassumption.
    f_equal; f_equal; eassumption.
    constructor.
    assumption.
    assumption.

StaticSemStack_CastOp
    eapply PstaticSemStackCastOp in H0.
    destruct H0 as [arg H].
    destruct H as [res H].
    ∃ [arg].
    ∃ (Result [res]).
    simpl.
    intuition.
    f_equal; eassumption.
    f_equal; f_equal; eassumption.
    constructor.
    assumption.
    assumption.
  Qed.
End SEM_STACKOP.