Library Sem_Cond


Semantics of jump operations

@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 Numeric.
Require Import AllStructures.

Module of this type provides detailed semantics of conditional and unconditional jump instructions TCondInstr.
Module Type SEM_COND.

Included modules

  Declare Module M_AllStructures : ALL_STRUCTURES.

  Import M_AllStructures.
  Import M_Program.M_ProgramStructures.
  Import M_Program.
  Import M_RuntimeStructures.M_Heap.
  Import M_RuntimeStructures.
  Import M_Arithmetics.
  Import M_ValuesAndTypes.
  Import ArithmeticOperators.

  Module M_IntNumProperties := NumericProperties M_Numeric_Int.

  Import List.ListNotations.
  Open Local Scope Z_scope.

Auxiliary definitions


  Let intArith := M_Arithmetics.M_IntArithmetic.arithmetic.

Dynamic semantics

The dynamic semantics of jump operations, provided as a relation on the top of the stack represented as a list of values. The meaning of the offset option is:
  • None - current thread will go the next instruction in the method body,
  • Some off - current thread will jump by the given offset off.
  Inductive semCond: TCondInstr → list TValue → list TValue → option TOffset → Prop:=
    | SemCond_goto: ∀ off,
      semCond (CI_Goto off) [] [] (Some off)

    | SemCond_if_true: ∀ cmpop k arg off,
      let arithmetic := arithmeticForKind k in
      M_ArithmeticTypes.arithCmpZero arithmetic cmpop arg true →
      semCond (CI_If k cmpop off) [arg] [] (Some off)

    | SemCond_if_false: ∀ cmpop k arg off,
      let arithmetic := arithmeticForKind k in
      M_ArithmeticTypes.arithCmpZero arithmetic cmpop arg false →
      semCond (CI_If k cmpop off) [arg] [] None

    | SemCond_cmp_true: ∀ cmpop k arg1 arg2 off,
      let arithmetic := arithmeticForKind k in
      M_ArithmeticTypes.arithCmpValues arithmetic cmpop arg1 arg2 true →
      semCond (CI_Cmp k cmpop off) [arg2;arg1] [] (Some off)

    | SemCond_cmp_false: ∀ cmpop k arg1 arg2 off,
      let arithmetic := arithmeticForKind k in
      M_ArithmeticTypes.arithCmpValues arithmetic cmpop arg1 arg2 false →
      semCond (CI_Cmp k cmpop off) [arg2;arg1] [] None

    | SemCond_tableswitch_found: ∀ low index default table,
      let lowZ := M_Numeric_Int.toZ low in
      let high1Z := lowZ + Z.of_nat (length table) in
      let indexZ := M_Numeric_Int.toZ index in
      indexZ ≥ lowZ → indexZ < high1Z →
      let off := nth (Z.to_nat (indexZ - lowZ)) table default in
      semCond (CI_Tableswitch low default table) [VInt index] [] (Some off)

    | SemCond_tableswitch_default: ∀ low index default table,
      let lowZ := M_Numeric_Int.toZ low in
      let high1Z := lowZ + Z.of_nat (length table) in
      let indexZ := M_Numeric_Int.toZ index in
      indexZ < lowZ ∨ indexZ ≥ high1Z →
      semCond (CI_Tableswitch low default table) [VInt index] [] (Some default)

    | SemCond_lookupswitch_found: ∀ default table key off,
      In (key, off) table →
      semCond (CI_Lookupswitch default table) [VInt key] [] (Some off)

    | SemCond_lookupswitch_default: ∀ key default table,
      (∀ off, ¬ In (key, off) table) →
      semCond (CI_Lookupswitch default table) [VInt key] [] (Some default)
  .

Static semantics

Lower level support for static semantics

Static semantics of if_<op> operation. For an comparison operator, a list of available operand kinds is given.
  Inductive staticSemCondIf : TCmpOp → list TKind → Prop :=
    | IfStaticSem_Eq: staticSemCondIf CmpOp_eq [KRef; KInt]
    | IfStaticSem_Ne: staticSemCondIf CmpOp_ne [KRef; KInt]
    | IfStaticSem_Le: staticSemCondIf CmpOp_le [KInt]
    | IfStaticSem_Lt: staticSemCondIf CmpOp_lt [KInt]
    | IfStaticSem_Ge: staticSemCondIf CmpOp_ge [KInt]
    | IfStaticSem_Gt: staticSemCondIf CmpOp_gt [KInt].

Each case mentioned in the above definition has its counterpart in the values-level semantics of operators.
  Lemma PstaticSemCondIf: ∀ cmpop kinds,
    staticSemCondIf cmpop kinds →
    ∀ k, In k kinds →
      ∀ res,
        ∃ arg,
             kindOfValue arg = k
          ∧ M_ArithmeticTypes.arithCmpZero (arithmeticForKind k) cmpop 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
    | _ ⇒ idtac
    end;
    destruct res.
16 non-trivial cases to show manually eq KRef true
    ∃ (VRef null).
    split; [simpl; reflexivity| constructor].
eq KRef false
    destruct PNotNullExists as [x H].
    ∃ (VRef x).
    split; [simpl; reflexivity|constructor].
    assumption.
eq KInt true
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_eq_t; constructor].
eq KInt false
    ∃ (VInt M_Numeric_Int.one).
    split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_eq_f; constructor].
ne KRef true
    destruct PNotNullExists as [x H].
    ∃ (VRef x).
    split; [simpl; reflexivity|constructor].
    assumption.
ne KRef false
    ∃ (VRef null).
    split; [simpl; reflexivity|constructor].
ne KInt true
    ∃ (VInt M_Numeric_Int.one).
    split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_ne_t; constructor].
ne KInt false
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_ne_f; constructor].
le KInt true
    ∃ (VInt M_Numeric_Int.minus_one).
    split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_le_t; constructor].
le KInt false
    ∃ (VInt M_Numeric_Int.one).
    split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_le_f; constructor].
lt KInt true
    ∃ (VInt M_Numeric_Int.minus_one).
    split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_lt_t; constructor].
lt KInt false
    ∃ (VInt M_Numeric_Int.one).
    split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_lt_f; constructor].
ge KInt true
    ∃ (VInt M_Numeric_Int.one).
    split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_ge_t; constructor].
ge KInt false
    ∃ (VInt M_Numeric_Int.minus_one).
    split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_ge_f; constructor].
gt KInt true
    ∃ (VInt M_Numeric_Int.one).
    split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_gt_t; constructor].
gt KInt false
    ∃ (VInt M_Numeric_Int.minus_one).
    split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_gt_f; constructor].
  Qed.

Static semantics of cmp_<op> operation. For an comparison operator, a list of available operand kinds is given.
  Inductive staticSemCondCmp : TCmpOp → list TKind → Prop :=
    | CmpStaticSem_Eq: staticSemCondCmp CmpOp_eq [KRef; KInt]
    | CmpStaticSem_Ne: staticSemCondCmp CmpOp_ne [KRef; KInt]
    | CmpStaticSem_Le: staticSemCondCmp CmpOp_le [KInt]
    | CmpStaticSem_Lt: staticSemCondCmp CmpOp_lt [KInt]
    | CmpStaticSem_Ge: staticSemCondCmp CmpOp_ge [KInt]
    | CmpStaticSem_Gt: staticSemCondCmp CmpOp_gt [KInt].

Each case mentioned in the above definition has its counterpart in the values-level semantics of operators.
  Lemma PstaticSemCondCmp: ∀ cmpop kinds,
    staticSemCondCmp cmpop kinds →
    ∀ k, In k kinds →
      ∀ res,
        ∃ arg1 arg2,
             kindOfValue arg1 = k
          ∧ kindOfValue arg2 = k
          ∧ M_ArithmeticTypes.arithCmpValues (arithmeticForKind k) cmpop 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
    | _ ⇒ idtac
    end;
    destruct res.
16 non-trivial cases to show manually eq KRef true
    ∃ (VRef null).
    ∃ (VRef null).
    split; [simpl; reflexivity | split; [simpl; reflexivity|constructor]].
    reflexivity.
eq KRef false
    destruct PNotNullExists as [x H].
    ∃ (VRef x).
    ∃ (VRef null).
    split; [simpl; reflexivity | split; [simpl; reflexivity|constructor]].
    intuition.
eq KInt true
    ∃ (VInt M_Numeric_Int.zero).
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity | split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_eq_t; constructor]].
eq KInt false
    ∃ (VInt M_Numeric_Int.one).
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity | split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_eq_f; constructor]].
ne KRef true
    destruct PNotNullExists as [x H].
    ∃ (VRef x).
    ∃ (VRef null).
    split; [simpl; reflexivity | split; [simpl; reflexivity|constructor]].
    assumption.
ne KRef false
    ∃ (VRef null).
    ∃ (VRef null).
    split; [simpl; reflexivity | split; [simpl; reflexivity|constructor]].
    reflexivity.
ne KInt true
    ∃ (VInt M_Numeric_Int.one).
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity | split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_ne_t; constructor]].
ne KInt false
    ∃ (VInt M_Numeric_Int.zero).
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity | split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_ne_f; constructor]].
le KInt true
    ∃ (VInt M_Numeric_Int.minus_one).
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity | split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_le_t; constructor]].
le KInt false
    ∃ (VInt M_Numeric_Int.one).
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity | split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_le_f; constructor]].
lt KInt true
    ∃ (VInt M_Numeric_Int.minus_one).
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity | split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_lt_t; constructor]].
lt KInt false
    ∃ (VInt M_Numeric_Int.one).
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity | split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_lt_f; constructor]].
ge KInt true
    ∃ (VInt M_Numeric_Int.one).
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity | split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_ge_t; constructor]].
ge KInt false
    ∃ (VInt M_Numeric_Int.minus_one).
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity | split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_ge_f; constructor]].
gt KInt true
    ∃ (VInt M_Numeric_Int.one).
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity | split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_gt_t; constructor]].
gt KInt false
    ∃ (VInt M_Numeric_Int.minus_one).
    ∃ (VInt M_Numeric_Int.zero).
    split; [simpl; reflexivity | split; [simpl; reflexivity
      | rewrite <- M_IntNumProperties.example_is_gt_f; constructor]].
  Qed.

Static semantics

The static (kind-level) semantics of jump operations, provided as a relation on the top of the stack projected to a list of kinds. Additionally, a possible resulting offset is given (note that this relation may be non-deterministic). For the meaning of offset, see semCond.
  Inductive staticSemCond: TCondInstr → list TKind → list TKind → option TOffset → Prop:=
    | StaticSemCond_goto: ∀ off,
      staticSemCond (CI_Goto off) [] [] (Some off)

    | StaticSemCond_if_true: ∀ cmpop k kinds off,
      staticSemCondIf cmpop kinds →
      In k kinds →
      staticSemCond (CI_If k cmpop off) [k] [] (Some off)

    | StaticSemCond_if_false: ∀ cmpop k kinds off,
      staticSemCondIf cmpop kinds →
      In k kinds →
      staticSemCond (CI_If k cmpop off) [k] [] (None)

    | StaticSemCond_cmp_true: ∀ cmpop k kinds off,
      staticSemCondCmp cmpop kinds →
      In k kinds →
      staticSemCond (CI_Cmp k cmpop off) [k;k] [] (Some off)

    | StaticSemCond_cmp_false: ∀ cmpop k kinds off,
      staticSemCondCmp cmpop kinds →
      In k kinds →
      staticSemCond (CI_Cmp k cmpop off) [k;k] [] (None)

    | StaticSemCond_tableswitch_found: ∀ low default table off,
      In off table →
      staticSemCond (CI_Tableswitch low default table) [KInt] [] (Some off)
      

    | StaticSemCond_tableswitch_default: ∀ low default table,
      staticSemCond (CI_Tableswitch low default table) [KInt] [] (Some default)
      

    | StaticSemCond_lookupswitch_found: ∀ default table off,
      In off (snd (split table)) →
      staticSemCond (CI_Lookupswitch default table) [KInt] [] (Some off)

    | StaticSemCond_lookupswitch_default: ∀ default table,
      staticSemCond (CI_Lookupswitch default table) [KInt] [] (Some default)
      
  .

Each case in the dynamic semantics is covered by an appropriate case in the static semantics.
  Lemma staticSemCondConsistent: ∀ (ci: TCondInstr) (ooff: option TOffset)
    (vs vs': list TValue),
      semCond ci vs vs' ooff →
      staticSemCond ci (kindOfValues vs) (kindOfValues vs') ooff.
  Proof.
    intros.
    destruct H.

SemCond_goto
    constructor.

SemCond_if_true
    assert (Pconsistent := (M_Arithmetics.PArithmeticConsistentKindCmpZero) cmpop k arg true H).
    simpl in ×.
    rewrite Pconsistent; clear Pconsistent.
    destruct cmpop;
      (econstructor; [econstructor |
        destruct k;
        simpl in *;
        try intuition trivial;
        try inversion H
      ]).

SemCond_if_false
    assert (Pconsistent := (M_Arithmetics.PArithmeticConsistentKindCmpZero) cmpop k arg false H).
    simpl in ×.
    rewrite Pconsistent; clear Pconsistent.
    destruct cmpop;
      (econstructor; [econstructor |
        destruct k;
        simpl in *;
        try intuition trivial;
        try inversion H
      ]).

SemCond_cmp_true
    assert (Pconsistent := (M_Arithmetics.PArithmeticConsistentKindCmpValues) cmpop k arg1 arg2 true H).
    decompose [and] Pconsistent; clear Pconsistent.
    simpl in ×.
    rewrite H0; clear H0.
    rewrite H1; clear H1.
    destruct cmpop;
      (econstructor; [econstructor |
        destruct k;
        simpl in *;
        try intuition trivial;
        try inversion H
      ]).
SemCond_cmp_false
    assert (Pconsistent := (M_Arithmetics.PArithmeticConsistentKindCmpValues) cmpop k arg1 arg2 false H).
    decompose [and] Pconsistent; clear Pconsistent.
    simpl in ×.
    rewrite H0; clear H0.
    rewrite H1; clear H1.
    destruct cmpop;
      (econstructor; [econstructor |
        destruct k;
        simpl in *;
        try intuition trivial;
        try inversion H
      ]).
SemCond_tableswitch_found
    apply StaticSemCond_tableswitch_found.     apply nth_In.
    rewrite <- (Nat2Z.id (length table)).
    apply (Z2Nat.inj_lt).
    omega.
    apply Nat2Z.is_nonneg.
    unfold high1Z in *; omega.

SemCond_tableswitch_default
    apply StaticSemCond_tableswitch_default.

SemCond_lookupswitch_found
    apply StaticSemCond_lookupswitch_found.
    change (In (snd (key, off)) (snd (split table))).
    apply in_split_r.
    assumption.

SemCond_lookupswitch_default
    apply StaticSemCond_lookupswitch_default.
  Qed.

Every case in the static semantics is motivated by a corresponding step in the dynamic semantics.
  Lemma staticSemCondComplete: ∀ (ci: TCondInstr) (ooff: option TOffset)
    (ks ks': list TKind),
      staticSemCond ci ks ks' ooff →
      ∃ vs vs',
           kindOfValues vs = ks
        ∧ kindOfValues vs' = ks'
        ∧ semCond ci vs vs' ooff.
  Proof.
    intros.
    inversion H; subst; clear H.

StaticSemCond_goto
    ∃ [].
    ∃ [].
    intuition constructor.

StaticSemCond_if_true
    apply PstaticSemCondIf with cmpop kinds k true in H0.
    destruct H0 as [arg H].
    ∃ [arg].
    ∃ [].
    simpl.
    intuition.
    f_equal; eassumption.
    constructor.
    assumption.
    assumption.

StaticSemCond_if_false
    apply PstaticSemCondIf with cmpop kinds k false in H0.
    destruct H0 as [arg H].
    ∃ [arg].
    ∃ [].
    simpl.
    intuition.
    f_equal; eassumption.
    constructor.
    assumption.
    assumption.

StaticSemCond_cmp_true
    apply PstaticSemCondCmp with cmpop kinds k true in H0.
    destruct H0 as [arg1 H].
    destruct H as [arg2 H].
    ∃ [arg2;arg1].
    ∃ [].
    simpl.
    intuition.
    f_equal.
    eassumption.
    f_equal; eassumption.
    constructor.
    assumption.
    assumption.

StaticSemCond_cmp_false
    apply PstaticSemCondCmp with cmpop kinds k false in H0.
    destruct H0 as [arg1 H].
    destruct H as [arg2 H].
    ∃ [arg2;arg1].
    ∃ [].
    simpl.
    intuition.
    f_equal.
    eassumption.
    f_equal; eassumption.
    constructor.
    assumption.
    assumption.

The following cases regard tableswitch and lookupswitch. Unfortunately some of them require to show that for any i we can find an integer different form i, which requires restriction on size of table and some kind of Pigeonhole principle. We left them unproved for now... SemCond_tableswitch_found
    admit.
SemCond_tableswitch_default
    admit.
SemCond_lookupswitch_found
    admit.
SemCond_lookupswitch_default
    admit.
  Qed.
End SEM_COND.