Library Sem_Frame

Semantics of in-frame operations

@author Patryk Czarnik

Require Import Logic.
Require Import Relations.
Require Import List.
Require Import Common.
Require Import Program.
Require Import ProgramStructures.
Require Import RuntimeStructures.
Require Import ValuesNTypes.
Require Import AllStructures.

Require Import Sem_Stackop.
Require Import Sem_Var.
Require Import Sem_Cond.

Module of this type provides detailed semantics of instructions operating within single frames TFrameInstr.

Module Type SEM_FRAME.

Included modules

Declare Module M_AllStructures : ALL_STRUCTURES.

M_SemStackop defines detailed semantics of FI_Stackop instruction.

Declare Module M_Sem_Stackop : SEM_STACKOP
with Module M_AllStructures := M_AllStructures.

M_SemVar defines detailed semantics of FI_Var instruction.

Declare Module M_Sem_Var : SEM_VAR
with Module M_AllStructures := M_AllStructures.

M_SemCond defines detailed semantics of FI_Cond instruction.

  Declare Module M_Sem_Cond : SEM_COND
    with Module M_AllStructures := M_AllStructures.

  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_RuntimeStructuresFacts.

  Open Local Scope type_scope.
  Import List.ListNotations.

Auxiliary definitions

Calulation of pc to go to basing on the result of semCond detailed semantics.

  Definition calculatePC off_opt code pc :=
    match off_opt with
      | None ⇒ next code pc
      | Some off ⇒ jump off pc
    end.

Dynamic semantics

Dynamic semantics of frame instructions TFrameInstr. Details of subsequent instruction classes are given in separate modules.

Inductive semFrame (code: TCode): TFrameInstr → TFrame → TResultOrException TFrame → Prop:=

FI_Stackop - normal completion

  | SemFrame_stackop: ∀ op pc vars sk vs pc' sk' vs',
    M_Sem_Stackop.semStack op vs (Result vs') →
    stackTopValues vs vs' sk sk' →
    pc' = next code pc →
    semFrame code (FI_Stackop op) (frameMake vars sk pc) (Result (frameMake vars sk' pc'))

FI_Stackop - exceptional completion

  | SemFrame_stackop_exn: ∀ op pc vars sk vs ecn,
    M_Sem_Stackop.semStack op vs (Exception ecn) →
    prefix vs sk →
    semFrame code (FI_Stackop op) (frameMake vars sk pc) (Exception ecn)

FI_Var - normal completion (there are no explicit exceptions for this and the following classes of instructions)

  | SemFrame_var: ∀ op pc vars sk vs pc' vars' sk' vs',
    M_Sem_Var.semVar op (vs , vars ) (vs', vars') →
    stackTopValues vs vs' sk sk' →
    pc' = next code pc →
    semFrame code (FI_Var op) (frameMake vars sk pc) (Result (frameMake vars' sk' pc'))

FI_Cond

  | SemFrame_cond: ∀ op pc vars sk vs pc' sk' vs' off_opt,
    M_Sem_Cond.semCond op vs vs' off_opt →
    stackTopValues vs vs' sk sk' →
    pc' = calculatePC off_opt code pc →
    semFrame code (FI_Cond op) (frameMake vars sk pc) (Result (frameMake vars sk' pc'))

FI_Jsr

  | SemFrame_jsr: ∀ off pc vars sk pc' sk',
    stackTopValues [] [VAddr pc ] sk sk' →
    pc' = jump off pc →
    semFrame code (FI_Jsr off) (frameMake vars sk pc) (Result (frameMake vars sk' pc'))

FI_Ret

  | SemFrame_ret: ∀ var pc vars sk pc',
    varsGet var vars = Some (VVAddr pc') →
    semFrame code (FI_Ret var) (frameMake vars sk pc) (Result (frameMake vars sk pc'))
  .

Static semantics

Static (kind-level) semantics of frame instructions TFrameInstr.

  Inductive staticSemFrame (code: TCode): TFrameInstr → TFrameKShadow → TResultOrException TFrameKShadow → Prop:=
  | StaticSemFrame_stackop: ∀ op pc kvars ksk ks pc' ksk' ks',
    M_Sem_Stackop.staticSemStack op ks (Result ks') →
    stackTopValues ks ks' ksk ksk' →
    pc' = next code pc →
    staticSemFrame code (FI_Stackop op) (frameKShadowMake kvars ksk pc) (Result (frameKShadowMake kvars ksk' pc'))

  | StaticSemFrame_stackop_exn: ∀ op pc kvars ksk ks ecn,
    M_Sem_Stackop.staticSemStack op ks (Exception ecn) →
    prefix ks ksk →
    staticSemFrame code (FI_Stackop op) (frameKShadowMake kvars ksk pc) (Exception ecn)

  | StaticSemFrame_var: ∀ op pc kvars ksk ks pc' kvars' ksk' ks',
    M_Sem_Var.staticSemVar op (ks , kvars ) (ks', kvars') →
    stackTopValues ks ks' ksk ksk' →
    pc' = next code pc →
    staticSemFrame code (FI_Var op) (frameKShadowMake kvars ksk pc) (Result (frameKShadowMake kvars' ksk' pc'))

  | StaticSemFrame_cond: ∀ op pc kvars ksk ks pc' ksk' ks' off_opt,
    M_Sem_Cond.staticSemCond op ks ks' off_opt →
    stackTopValues ks ks' ksk ksk' →
    pc' = calculatePC off_opt code pc →
    staticSemFrame code (FI_Cond op) (frameKShadowMake kvars ksk pc) (Result (frameKShadowMake kvars ksk' pc'))

  | StaticSemFrame_jsr: ∀ off pc kvars ksk pc' ksk',
    stackTopValues [] [KAddr pc ] ksk ksk' →
    pc' = jump off pc →
    staticSemFrame code (FI_Jsr off) (frameKShadowMake kvars ksk pc) (Result (frameKShadowMake kvars ksk' pc'))

  | StaticSemFrame_ret: ∀ var pc kvars ksk pc',
    varsGet var kvars = Some (VKAddr pc') →
    staticSemFrame code (FI_Ret var) (frameKShadowMake kvars ksk pc) (Result (frameKShadowMake kvars ksk pc'))
  .

Guarantees that every step in the dynamic semantics is reflected in the static semantics.

  Lemma staticSemFrameConsistent:
    ∀ (code: TCode) (fi: TFrameInstr) (fr1: TFrame) (result_fr2: TResultOrException TFrame),
      semFrame code fi fr1 result_fr2 →
      staticSemFrame code fi (frameKAbstraction fr1) (mapROX frameKAbstraction result_fr2).
  Proof.
    intros.
    inversion H; subst; clear H;
      simpl.

SemFrame_stackop

    econstructor.
    assert (aux := M_Sem_Stackop.staticSemStackConsistent op vs (Result vs')).
    apply aux; clear aux.
    assumption.
    simpl.
    unfold kindOfValues, localStackKAbstraction.
    apply PstackTopValuesMap.
    assumption.
    simpl.
    reflexivity.

SemFrame_stackop_exn

    econstructor.
    assert (aux := M_Sem_Stackop.staticSemStackConsistent op vs (Exception ecn)).
    apply aux; clear aux.
    assumption.
    simpl.
    unfold kindOfValues, localStackKAbstraction.
    apply PprefixMap.
    assumption.

SemFrame_var

    econstructor.
    apply M_Sem_Var.staticSemVarConsistent.
    eassumption.
    simpl.
    unfold kindOfValues, localStackKAbstraction.
    apply PstackTopValuesMap.
    assumption.
    simpl.
    reflexivity.

SemFrame_cond

    econstructor.
    apply M_Sem_Cond.staticSemCondConsistent.
    eassumption.
    simpl.
    unfold kindOfValues, localStackKAbstraction.
    apply PstackTopValuesMap.
    assumption.
    simpl.
    reflexivity.

SemFrame_jsr

    econstructor.
    simpl.
    replace [KAddr pc] with (localStackKAbstraction [VAddr pc]).
    replace (@nil TKind) with (localStackKAbstraction (@nil TValue)).
    eapply PstackTopValuesMap.
    assumption.
    reflexivity.
    reflexivity.
    reflexivity.

SemFrame_ret

    econstructor.
    simpl.
    replace (VKAddr pc') with (kindOfVarValue (VVAddr pc')).
    apply PvarsKAbstractionConsistentSome.
    assumption.
    reflexivity.
  Qed.

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

  Lemma staticSemFrameComplete:
    ∀ (code: TCode) (fi: TFrameInstr) (frsh1: TFrameKShadow) (result_frsh2: TResultOrException TFrameKShadow),
      staticSemFrame code fi frsh1 result_frsh2 →
      ∃ fr1 fr2,
           frameKAbstraction fr1 = frsh1
        ∧ mapROX frameKAbstraction fr2 = result_frsh2
        ∧ semFrame code fi fr1 fr2.
  Proof.
    intros.
    inversion H; subst; clear H.

StaticSemFrame_stackop

    destruct (M_Sem_Stackop.staticSemStackComplete _ _ _ H0) as [vs1 H]; clear H0.
    destruct H as [result_vs2 H].
    decompose [and] H; clear H.
    destruct H1 as [tl H].     decompose [and] H; clear H.
    destruct result_vs2 as [vs2 | exn_cn];
      simpl in H3;
      simplify_eq H3;
      intros.
    ∃ (frameMake
      (varsKConcretisation kvars)
      (vs1 ++ localStackKConcretisation tl)
      pc).
    ∃ (Result (frameMake
      (varsKConcretisation kvars)
      (vs2 ++ localStackKConcretisation tl)
       (next code pc))).
    unfold frameKAbstraction; simpl.
    split;[|split].
    f_equal.
    apply PvarsKConcretisationAbstraction.
    rewrite PlocalStackKAbstractionApp.
    rewrite <- H1.
    f_equal.
    assumption.
    apply PlocalStackKConcretisationAbstraction.
    f_equal.
    f_equal.
    apply PvarsKConcretisationAbstraction.
    rewrite PlocalStackKAbstractionApp.
    rewrite <- H2.
    f_equal.
    assumption.
    apply PlocalStackKConcretisationAbstraction.

    econstructor.
    eassumption.
    apply PstackTopValuesTrivial.
    reflexivity.

StaticSemFrame_stackop_exn

    destruct (M_Sem_Stackop.staticSemStackComplete _ _ _ H0) as [vs1 H]; clear H0.
    destruct H as [result_vs2 H].
    decompose [and] H; clear H.
    destruct result_vs2 as [vs2 | exn_cn'];
      simpl in H3;
      simplify_eq H3;
      clear H3;
      intros;
      subst.
    destruct H1 as [tl H1]; subst.
    ∃ (frameMake
      (varsKConcretisation kvars)
      (vs1 ++ localStackKConcretisation tl)
      pc).
    ∃ (Exception ecn).
    unfold frameKAbstraction; simpl.
    split;[|split].
    f_equal.
    apply PvarsKConcretisationAbstraction.
    rewrite PlocalStackKAbstractionApp.
    f_equal.
    apply PlocalStackKConcretisationAbstraction.
    reflexivity.

    econstructor.
    eassumption.
    apply PprefixTrivial.

StaticSemFrame_var

    destruct (M_Sem_Var.staticSemVarComplete _ _ _ _ _ H0) as [vs1 H]; clear H0.
    destruct H as [vs2 H].
    destruct H as [vars1 H].
    destruct H as [vars2 H].
    decompose [and] H; clear H.
    destruct H1 as [tl H].     decompose [and] H; clear H.
    ∃ (frameMake
      vars1
      (vs1 ++ localStackKConcretisation tl)
      pc).
    ∃ (Result (frameMake
      vars2
      (vs2 ++ localStackKConcretisation tl)
       (next code pc))).
    unfold frameKAbstraction; simpl.
    split; [f_equal | split].
    assumption.
    rewrite PlocalStackKAbstractionApp.
    rewrite <- H1.
    f_equal.
    assumption.
    apply PlocalStackKConcretisationAbstraction.
    f_equal; f_equal.
    assumption.
    rewrite PlocalStackKAbstractionApp.
    rewrite <- H5.
    f_equal.
    assumption.
    apply PlocalStackKConcretisationAbstraction.

    econstructor.
    eassumption.
    apply PstackTopValuesTrivial.
    reflexivity.

StaticSemFrame_cond

    destruct (M_Sem_Cond.staticSemCondComplete _ _ _ _ H0) as [vs1 H]; clear H0.
    destruct H as [vs2 H].
    decompose [and] H; clear H.
    destruct H1 as [tl H].     decompose [and] H; clear H.
    ∃ (frameMake
      (varsKConcretisation kvars)
      (vs1 ++ localStackKConcretisation tl)
      pc).
    ∃ (Result (frameMake
      (varsKConcretisation kvars)
      (vs2 ++ localStackKConcretisation tl)
       (calculatePC off_opt code pc))).
    unfold frameKAbstraction; simpl.
    split;[|split].
    f_equal.
    apply PvarsKConcretisationAbstraction.
    rewrite PlocalStackKAbstractionApp.
    rewrite <- H1.
    f_equal.
    assumption.
    apply PlocalStackKConcretisationAbstraction.
    f_equal; f_equal.
    apply PvarsKConcretisationAbstraction.
    rewrite PlocalStackKAbstractionApp.
    rewrite <- H2.
    f_equal.
    assumption.
    apply PlocalStackKConcretisationAbstraction.

    econstructor.
    eassumption.
    apply PstackTopValuesTrivial.
    reflexivity.

StaticSemFrame_jsr

    destruct H0 as [tl H].     decompose [and] H; clear H; subst.
    ∃ (frameMake
      (varsKConcretisation kvars)
      (localStackKConcretisation tl)
      pc).
    ∃ (Result (frameMake
      (varsKConcretisation kvars)
      ((VAddr pc) :: localStackKConcretisation tl)
      (jump off pc))).
    unfold frameKAbstraction; simpl.
    split;[|split].
    f_equal.
    apply PvarsKConcretisationAbstraction.
    apply PlocalStackKConcretisationAbstraction.
    f_equal; f_equal.
    apply PvarsKConcretisationAbstraction.
    f_equal.
    apply PlocalStackKConcretisationAbstraction.
    constructor.
    apply PstackTopValuesNilCons.
    reflexivity.

StaticSemFrame_ret

    apply PvarsKConcretisationConsistentSome in H0.
    destruct H0 as [vv H].
    decompose [and] H; clear H.
    destruct vv;
      simpl in H0;
      simplify_eq H0; clear H0; intros;
      subst.

    ∃ (frameMake
      (varsKConcretisation kvars)
      (localStackKConcretisation ksk)
      pc).
    ∃ (Result (frameMake
      (varsKConcretisation kvars)
      (localStackKConcretisation ksk)
      pc')).
    unfold frameKAbstraction; simpl.
    split;[|split].
    f_equal.
    apply PvarsKConcretisationAbstraction.
    apply PlocalStackKConcretisationAbstraction.
    f_equal; f_equal.
    apply PvarsKConcretisationAbstraction.
    apply PlocalStackKConcretisationAbstraction.
    constructor.
    assumption.
  Qed.

In-frame program execution

The semantics of I_Frame instructions formulated so that analysis of execution of single methods is possible and more convenient that analysis at whole JVM states level.

Small-step semantics at one method and one frame level, handling only the instructions from I_Frame category.

It does not support exceptions, even those which are handled within a method. stepFrame holds only if a non-exceptional execution is possible.

  Inductive stepFrame (code: TCode): TFrame → TFrame → Prop:=
  | StepFrame_one:
    ∀ finstr fr1 fr2,
    getInstruction code (frameGetPC fr1) = Some (I_Frame finstr) →
    semFrame code finstr fr1 (Result fr2) →
    stepFrame code fr1 fr2.

Transitive closure of the above relation.

Definition stepsFrame (code: TCode): TFrame → TFrame → Prop :=
clos_refl_trans TFrame (stepFrame code).
End SEM_FRAME.