Library mcertikos.conlib.conmtlib.EAsmCommon

This file provide the semantics for the Asm instructions. Since we introduce paging mechanisms, the semantics of memory load and store are different from Compcert Asm

Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import AuxLemma.
Require Import CommonTactic.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import Decision.
Require Import LAsm.
Require Import GlobIdent.

Require Import SingleConfiguration.

Section ESemanticsCommon.

  Context `{conf : SingleConfiguration}.
  Context `{Hmwd: UseMemWithData mem}.

  Context `{data_prf : CompatData PData}.
  Context `{Hstencil: Stencil}.
  Context `{L: compatlayer (cdata PData)}.
  Context `{ass_def: !AccessorsDefined L}.

  Local Instance ec_ops: ExternalCallsOps (mwd (cdata PData)) := CompatExternalCalls.compatlayer_extcall_ops L.
  Local Instance lcfg_ops: LayerConfigurationOps := compatlayer_configuration_ops L.

EAsm threads can be in one of three states: environment, available, or running. Environment threads can only take oracle steps and will never change states. Available threads have not been run yet, but may be "yielded back" to, at which time they become running threads. Running threads have a current register state and take normal steps.

  Inductive ThreadState :=
    | Environment
    | Available
    | Running (rs: regset).

  Fixpoint initial_map {A} (z: A) (i: Z → A) (tids: list Z): ZMap.t A :=
    match tids with
      | nil ⇒ ZMap.init z
      | tid::tids´ ⇒ ZMap.set tid (i tid) (initial_map z i tids´)
    end.

  Definition init_regset {F V} (ge: Genv.t F V) i :=
    if decide (i = main_thread) then
      let pc := symbol_offset ge 1%positive Int.zero in
      Running ((Pregmap.init Vundef) # PC <- pc # ESP <- Vzero)
    else
      Available.

  Definition init_dproc (i : Z) :=
    if zeq main_thread i then main_init_dproc else nomain_init_dproc.

End ESemanticsCommon.

Lemma nb_last_op:
  ∀ e l nb,
    getLogEventNB e = Some nb → last_op l = Some e →
    lastEvType l = Some LogYieldTy.
Proof.
  unfold lastEvType; intros e l nb Hnb Hlop; rewrite Hlop.
  destruct e as [? e]; destruct e; auto; discriminate.
Qed.

Ltac nb_last_op_solve :=
  match goal with
  | [ H: lastEvType _ ≠ Some LogYieldTy |- _ ] ⇒
    contradiction H; eapply nb_last_op; eauto
  end.

Ltac exec_contr :=
  match goal with
  | [ H: exec_instr _ _ _ _ _ = _ |- _ ] ⇒ inv H
  end.

Ltac rewrite_inv :=
  repeat match goal with
         | [ H : ?a = _, H´ : ?a = _ |- _ ] ⇒
           rewrite H´ in H; inv H
         end.