Library Sem_Var

Semantics of local variable 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 AllStructures.

Module of this type provides detailed semantics of local variable instructions TVarInstr.

Module Type SEM_VAR.

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

  Import List.ListNotations.
  Open Local Scope type_scope.

Var operation constraints

Load and store instructions asymmetrically support kinds of values. Original astore instruction is allowed to store reference and returnAddress values, while the aload instruction is allowed to load only reference values (a returnAddress is not allowed). This specific constraint is described in more general definitions below.

  Inductive isLoadable: TVarIKind → TKind → Prop :=
  | IsLoadable_Ref: isLoadable VIKRef KRef
  | IsLoadable_Int: isLoadable VIKInt KInt
  | IsLoadable_Float: isLoadable VIKFloat KFloat
  | IsLoadable_Long: isLoadable VIKLong KLong
  | IsLoadable_Double: isLoadable VIKDouble KDouble.

  Inductive isStorable: TVarIKind → TKind → Prop :=
  | IsStorable_Ref: isStorable VIKRef KRef
  | IsStorable_Addr: ∀ pc, isStorable VIKRef (KAddr pc)
  | IsStorable_Int: isStorable VIKInt KInt
  | IsStorable_Float: isStorable VIKFloat KFloat
  | IsStorable_Long: isStorable VIKLong KLong
  | IsStorable_Double: isStorable VIKDouble KDouble.

Dynamic semantics

The dynamic semantics of stack operations, provided as a relation on the top of the stack (before and after) represented as a list of values and variable array before and after intruction.

  Inductive semVar: TVarInstr → (list TValue × TVars) → (list TValue × TVars) → Prop :=
  | SemVar_load_1: ∀ vik var vars v vv,
    isLoadable vik (kindOfValue v) →
    ValVarMapping v (One vv) →
    varsGet var vars = Some vv →
    semVar (VI_Load vik var) ([], vars ) ([v ], vars )

  | SemVar_load_2: ∀ vik var vars v vv1 vv2,
    isLoadable vik (kindOfValue v) →
    ValVarMapping v (Two vv1 vv2) →
    varsGet var vars = Some vv1 →
    varsGet (nextVar var) vars = Some vv2 →
    semVar (VI_Load vik var) ([], vars ) ([v ], vars )

  | SemVar_store_1: ∀ vik var vars v vv vars',
    isStorable vik (kindOfValue v) →
    ValVarMapping v (One vv) →
    vars' = varsSet var vv vars →
    semVar (VI_Store vik var) ([v ], vars ) ([], vars')

  | SemVar_store_2: ∀ vik var vars v vv1 vv2 vars'',
    isStorable vik (kindOfValue v) →
    ValVarMapping v (Two vv1 vv2) →
    let vars' := varsSet var vv1 vars in
    vars'' = varsSet (nextVar var) vv2 vars' →
    semVar (VI_Store vik var) ([v ], vars ) ([], vars'')

  | SemVar_iinc: ∀ var c x vars x' vars',
    varsGet var vars = Some (VVInt x) →
    x' = M_Numeric_Int.add x c →
    vars' = varsSet var (VVInt x') vars →
    semVar (VI_Inc var c) ([], vars ) ([], vars').

Static semantics

The static (kind-level) semantics of variable operations, provided as a relation on the top of the stack projected to a list of kinds and variable array "shadows" (kind-level abstractions).

  Inductive staticSemVar: TVarInstr → (list TKind × TVarsKShadow) → (list TKind × TVarsKShadow) → Prop :=
  | StaticSemVar_load_1: ∀ vik k vk var kvars,
    isLoadable vik k →
    ValVarKindMapping k (One vk) →
    varsGet var kvars = Some vk →
    staticSemVar (VI_Load vik var) ([], kvars ) ([k ], kvars )

  | StaticSemVar_load_2: ∀ vik k vk1 vk2 var kvars,
    isLoadable vik k →
    ValVarKindMapping k (Two vk1 vk2) →
    varsGet var kvars = Some vk1 →
    varsGet (nextVar var) kvars = Some vk2 →
    staticSemVar (VI_Load vik var) ([], kvars ) ([k ], kvars )

  | StaticSemVar_store_1: ∀ vik k vk var kvars kvars',
    isStorable vik k →
    ValVarKindMapping k (One vk) →
    kvars' = varsSet var vk kvars →
    staticSemVar (VI_Store vik var) ([k ], kvars ) ([], kvars')

  | StaticSemVar_store_2: ∀ vik k vk1 vk2 var kvars kvars'',
    isStorable vik k →
    ValVarKindMapping k (Two vk1 vk2) →
    let kvars' := varsSet var vk1 kvars in
    kvars'' = varsSet (nextVar var) vk2 kvars' →
    staticSemVar (VI_Store vik var) ([k ], kvars ) ([], kvars'')

  | StaticSemVar_iinc: ∀ var c kvars,
    varsGet var kvars = Some VKInt →

    staticSemVar (VI_Inc var c) ([], kvars ) ([], kvars ).

Correctness

We need the following fact about variable arrays.

Ulimately, it seems to require using equivalence relation expressing extensional equality instead of "phusical equality" of variable arrays in the semantics.

Setting the same value as previous does not change a variables array.

  Axiom PVarsSetSame:
    ∀ (t:Set) (vars: TVarsGeneric t) var v1 v2,
      varsGet var vars = Some v1 →
      v1 = v2 →
      (varsSet var v2 vars ) = vars.

  Lemma PvarsKAbstractionSetSame:
    ∀ vars var v1 v2,
      varsGet var vars = Some v1 →
      kindOfVarValue v1 = kindOfVarValue v2 →
      varsKAbstraction (varsSet var v2 vars) = varsKAbstraction vars.
  Proof.
    intros.
    rewrite PvarsKAbstractionConsistentSet.
    eapply PVarsSetSame.
    apply PvarsKAbstractionConsistentSome.
    eassumption.
    assumption.
  Qed.

Guarantees that every step in the dynamic semantics is covered by the static semantics.

  Lemma staticSemVarConsistent: ∀ (vi: TVarInstr) (vs vs': list TValue) (vars vars': TVars),
      semVar vi (vs , vars ) (vs', vars') →
      staticSemVar vi (kindOfValues vs , varsKAbstraction vars ) (kindOfValues vs', varsKAbstraction vars').
  Proof.
    intros.
    inversion H; subst; clear H.

SemVar_load_1

    apply PValVarMappingConsistent in H6; simpl in H6.
    eapply StaticSemVar_load_1.
    assumption.
    eassumption.
    apply PvarsKAbstractionConsistentSome.
    assumption.

SemVar_load_2

    apply PValVarMappingConsistent in H6; simpl in H6.
    eapply StaticSemVar_load_2.
    assumption.
    eassumption.
    apply PvarsKAbstractionConsistentSome.
    assumption.
    apply PvarsKAbstractionConsistentSome.
    assumption.

SemVar_store_1

    apply PValVarMappingConsistent in H6; simpl in H6.
    eapply StaticSemVar_store_1.
    assumption.
    eassumption.
    apply PvarsKAbstractionConsistentSet.

SemVar_store_2

    apply PValVarMappingConsistent in H6; simpl in H6.
    eapply StaticSemVar_store_2.
    assumption.
    eassumption.
    unfold vars'0.
    rewrite PvarsKAbstractionConsistentSet.
    rewrite PvarsKAbstractionConsistentSet.
    reflexivity.

SemVar_iinc

    rewrite (PvarsKAbstractionSetSame vars var (VVInt x) (VVInt (M_Numeric_Int.add x c))).
    constructor.
    rewrite PvarsKAbstractionConsistent.
    rewrite H5.
    simpl.
    reflexivity.
    assumption.
    simpl.
    reflexivity.
  Qed.

Guarantees that every step in the static semantics is motivated by a corresponding step in the dynamic semantics.

  Lemma staticSemVarComplete: ∀ (vi: TVarInstr) (ks ks': list TKind) (kvars kvars': TVarsKShadow),
      staticSemVar vi (ks , kvars ) (ks', kvars') →
      ∃ vs vs' vars vars',
           kindOfValues vs = ks
        ∧ kindOfValues vs' = ks'
        ∧ varsKAbstraction vars = kvars
        ∧ varsKAbstraction vars' = kvars'
        ∧ semVar vi (vs , vars ) (vs', vars').
  Proof.
    intros.
    inversion H; subst; clear H.

StaticSemVar_load_1

    destruct (PvarsKConcretisationConsistentSome _ _ _ H7) as [vv H]; clear H7.
    decompose [and] H; clear H.
    subst vk.
    destruct (PValVarMappingConsistentInv_AVar_EVal k (One vv) H6) as [v H];
      clear H6.
    decompose [and] H; clear H; subst.
    ∃ [].
    ∃ [v].
    ∃ (varsKConcretisation kvars').
    ∃ (varsKConcretisation kvars').
    repeat (try split).
    apply PvarsKConcretisationAbstraction.
    apply PvarsKConcretisationAbstraction.
    eapply SemVar_load_1.
    assumption.
    eassumption.
    assumption.

StaticSemVar_load_2

    destruct (PvarsKConcretisationConsistentSome _ _ _ H7) as [vv1 H]; clear H7.
    decompose [and] H; clear H.
    destruct (PvarsKConcretisationConsistentSome _ _ _ H8) as [vv2 H]; clear H8.
    decompose [and] H; clear H.
    subst vk1 vk2.
    destruct (PValVarMappingConsistentInv_AVar_EVal k (Two vv1 vv2) H6) as [v H];
      clear H6.
    decompose [and] H; clear H; subst.
    ∃ [].
    ∃ [v].
    ∃ (varsKConcretisation kvars').
    ∃ (varsKConcretisation kvars').
    repeat (try split).
    apply PvarsKConcretisationAbstraction.
    apply PvarsKConcretisationAbstraction.
    eapply SemVar_load_2.
    assumption.
    eassumption.
    assumption.
    assumption.

StaticSemVar_store_1

    destruct (PValVarMappingConsistentInv_EVal_EVar _ _ H6) as [v H_];
      clear H6.
    destruct H_ as [vv12 H].
    decompose [and] H; clear H; subst.
    destruct vv12 as [vv | vv1 vv2]; simpl in H2.

    injection H2; clear H2; intros; subst.
    ∃ [v].
    ∃ [].
    ∃ (varsKConcretisation kvars).
    ∃ (varsSet var vv (varsKConcretisation kvars)).
    repeat (try split).
    apply PvarsKConcretisationAbstraction.
    rewrite PvarsKAbstractionConsistentSet.
    rewrite PvarsKConcretisationAbstraction.
    reflexivity.
    eapply SemVar_store_1.
    assumption.
    eassumption.
    reflexivity.

    discriminate H2.

StaticSemVar_store_2

    unfold kvars'0 in ×.
    destruct (PValVarMappingConsistentInv_EVal_EVar _ _ H6) as [v H_];
      clear H6.
    destruct H_ as [vv12 H].
    decompose [and] H; clear H; subst.
    destruct vv12 as [vv | vv1 vv2]; simpl in H2.

    discriminate H2.

    injection H2; clear H2; intros; subst.
    ∃ [v].
    ∃ [].
    ∃ (varsKConcretisation kvars).
    ∃ (varsSet (nextVar var) vv2 (varsSet var vv1 (varsKConcretisation kvars))).
    repeat (try split).
    apply PvarsKConcretisationAbstraction.
    rewrite PvarsKAbstractionConsistentSet.
    rewrite PvarsKAbstractionConsistentSet.
    rewrite PvarsKConcretisationAbstraction.
    reflexivity.
    eapply SemVar_store_2.
    assumption.
    eassumption.
    reflexivity.

StaticSemVar_iinc

    destruct (PvarsKConcretisationConsistentSome _ _ _ H2) as [v H].
    decompose [and] H; clear H.
    destruct v; simpl in H0; simplify_eq H0; clear H0.
    ∃ [].
    ∃ [].
    ∃ (varsKConcretisation kvars').
    ∃ (varsSet var (VVInt (M_Numeric_Int.add ival c)) ((varsKConcretisation kvars'))).
    repeat (try split).
    apply PvarsKConcretisationAbstraction.
    rewrite PvarsKAbstractionConsistentSet.
    rewrite PvarsKConcretisationAbstraction.
    eapply PVarsSetSame.     eassumption.
    reflexivity.
    econstructor.
    eassumption.
    reflexivity.
    reflexivity.
  Qed.

  Lemma PSemVarInversion_load_1:
    ∀ vik var vs vs' vars vars',
    isCatVIK cat1 vik →
    semVar (VI_Load vik var) (vs , vars ) (vs', vars') →
      ∃ v vv,
      isLoadable vik (kindOfValue v)
    ∧ValVarMapping v (One vv)
    ∧vs = []
    ∧vs' = [v ]
    ∧vars = vars'
    ∧varsGet var vars = Some vv.
  Proof.
    intros.
    inversion H; clear H; subst;
      (inversion H0; clear H0; subst;
       [ ∃ v; ∃ vv; tauto
       | inversion H7; clear H7; subst; inversion H6]).
  Qed.

  Lemma PSemVarInversion_store_1:
    ∀ vik var vs vars vs' vars',
    isCatVIK cat1 vik →
    semVar (VI_Store vik var) (vs , vars ) (vs', vars') →
      ∃ v vv,
      isStorable vik (kindOfValue v)
    ∧ValVarMapping v (One vv)
    ∧vs = [v ]
    ∧vs' = []
    ∧vars' = varsSet var vv vars.
  Proof.
    intros.
    inversion H; clear H; subst;
      (inversion H0; clear H0; subst;
       [ ∃ v; ∃ vv; tauto
       | unfold vars'0 in *; inversion H7; clear H7; subst v;
         inversion H5]).
  Qed.
End SEM_VAR.