Library mcertikos.layerlib.DevicePrimSemantics
This file defines the general semantics for primitives at all layers
Require Import Coqlib.
Require Import Maps.
Require Import Globalenvs.
Require Import AsmX.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import AST.
Require Import AuxStateDataType.
Require Import Constant.
Require Import FlatMemory.
Require Import GlobIdent.
Require Import Integers.
Require Import Conventions.
Require Import LAsm.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import compcert.cfrontend.Ctypes.
Require Import compcert.cfrontend.Cop.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Export mCertiKOSType.
Section Semantics.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context {RData} `{HD: CompatData RData}.
Section Set_Tf.
Variable set_tf_spec: val → RData → option RData.
Inductive primcall_set_tf_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_set_tf_sem_intro:
∀ m (rs: regset) adt adt´ pc,
set_tf_spec pc adt = Some adt´ →
pc = rs#EAX →
∀ N_TYPE_RA: Val.has_type (rs RA) AST.Tint,
∀ N_INJECT_NEUTRAL: (∀ v r, ZtoPreg v = Some r
→ val_inject (Mem.flat_inj (Mem.nextblock m)) (rs#r) (rs#r)),
primcall_set_tf_sem s rs (m, adt) (rs#PC <- (rs#RA)) (m, adt´).
Class SetTfInvariants :=
{
set_tf_low_level_invariant s m pc rs d d´:
set_tf_spec pc d = Some d´ →
asm_invariant s rs m →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
set_tf_high_level_invariant pc d d´:
set_tf_spec pc d = Some d´ →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: SetTfInvariants}.
Require Import FutureTactic.
Local Instance primcall_set_tf_sem_propertes:
PrimcallProperties primcall_set_tf_sem.
Proof.
constructor; intros; inv H.
-
inv H0; split; congruence.
Qed.
Local Instance primcall_set_tf_sem_invariants:
PrimcallInvariants primcall_set_tf_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto.
val_inject_simpl.
+
repeat apply set_reg_wt.
simpl.
eapply N_TYPE_RA; apply PregToZ_correct; simpl; reflexivity.
assumption.
-
eapply set_tf_low_level_invariant; eauto.
-
eapply set_tf_high_level_invariant; eauto.
Qed.
Definition primcall_set_tf_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_set_tf_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some GlobIdent.set_tf;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End Set_Tf.
Section Save_Context.
Variable save_context_spec: regset → RData → RData.
Inductive primcall_save_context_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_savecontext_sem_intro:
∀ m (rs: regset) adt adt´,
save_context_spec rs adt = adt´ →
∀ N_TYPE_RA: Val.has_type (rs RA) AST.Tint,
∀ N_INJECT_NEUTRAL: (∀ v r, ZtoPreg v = Some r
→ val_inject (Mem.flat_inj (Mem.nextblock m)) (rs#r) (rs#r)),
primcall_save_context_sem s rs (m, adt) (rs#PC <- (rs#RA)) (m, adt´).
Class SaveContextInvariants :=
{
save_context_low_level_invariant s m rs d d´:
save_context_spec rs d = d´ →
asm_invariant s rs m →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
save_context_high_level_invariant rs d d´:
save_context_spec rs d = d´ →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: SaveContextInvariants}.
Require Import FutureTactic.
Local Instance primcall_save_context_sem_propertes:
PrimcallProperties primcall_save_context_sem.
Proof.
constructor; intros; inv H.
-
inv H0; split; congruence.
Qed.
Local Instance primcall_save_context_sem_invariants:
PrimcallInvariants primcall_save_context_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto.
val_inject_simpl.
+
repeat apply set_reg_wt.
simpl.
eapply N_TYPE_RA; apply PregToZ_correct; simpl; reflexivity.
assumption.
-
eapply save_context_low_level_invariant; eauto.
-
eapply save_context_high_level_invariant; eauto.
Qed.
Definition primcall_save_context_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_save_context_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some GlobIdent.save_context;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End Save_Context.
Section Restore_Context.
Variable restore_context_spec: RData → (regset × RData).
Inductive primcall_restore_context_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_restorecontext_sem_intro:
∀ m (rs rs´: regset) adt adt´,
restore_context_spec adt = (rs´, adt´)
→ ∀ N_TYPE: wt_regset rs´,
∀ N_INJECT_NEUTRAL: (∀ r, val_inject (Mem.flat_inj (Mem.nextblock m)) (rs´#r) (rs´#r)),
primcall_restore_context_sem s rs (m, adt)
(rs´# PC <- (rs#RA))
(m, adt´).
Class RestoreContextInvariants :=
{
restore_context_low_level_invariant m rs´ d d´:
restore_context_spec d = (rs´, d´) →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
restore_context_high_level_invariant rs´ d d´:
restore_context_spec d = (rs´, d´) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: RestoreContextInvariants}.
Local Instance primcall_restore_context_sem_propertes:
PrimcallProperties primcall_restore_context_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst. split; congruence.
Qed.
Local Instance primcall_restore_context_sem_invariants:
PrimcallInvariants primcall_restore_context_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto.
val_inject_simpl.
+
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl.
try (eapply N_TYPE; apply PregToZ_correct; simpl; reflexivity);
try assumption.
unfold wt_regset in inv_reg_wt.
eapply inv_reg_wt; eauto.
-
eapply restore_context_low_level_invariant; eauto.
-
eapply restore_context_high_level_invariant; eauto.
Qed.
Definition primcall_restore_context_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_restore_context_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some GlobIdent.restore_context;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End Restore_Context.
Section Serial_Intr_Handler_Asm.
Variable serial_intr_handler_asm_spec: regset → RData → option (RData × regset).
Inductive primcall_serial_intr_handler_asm_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_serialintrhandlerasm_sem_intro:
∀ m (rs rs´: regset) adt adt´ b,
serial_intr_handler_asm_spec rs adt = Some (adt´, rs´) →
∀ N_INJECT_NEUTRAL: (∀ r, val_inject (Mem.flat_inj (Mem.nextblock m)) (rs#r) (rs#r)),
∀ Hsymbol: find_symbol s GlobIdent.serial_intr_handler_asm = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ HRS: rs = rs´,
primcall_serial_intr_handler_asm_sem s rs (m, adt) ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs´) #PC <- (rs#RA) #RA <- Vundef) (m, adt´).
Class SerialIntrHandlerAsmInvariants :=
{
serial_intr_handler_asm_low_level_invariant s m rs rs´ d d´:
serial_intr_handler_asm_spec rs d = Some (d´, rs´) →
asm_invariant s rs m →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
serial_intr_handler_asm_high_level_invariant rs rs´ d d´:
serial_intr_handler_asm_spec rs d = Some (d´, rs´) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: SerialIntrHandlerAsmInvariants}.
Local Instance primcall_serial_intr_handler_asm_sem_propertes:
PrimcallProperties primcall_serial_intr_handler_asm_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst. split; congruence.
Qed.
Local Instance primcall_serial_intr_handler_asm_sem_invariants:
PrimcallInvariants primcall_serial_intr_handler_asm_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL;
apply PregToZ_correct; simpl; reflexivity).
+
repeat apply set_reg_wt; try constructor.
simpl.
unfold wt_regset in inv_reg_wt.
eapply inv_reg_wt.
assumption.
-
eapply serial_intr_handler_asm_low_level_invariant; eauto.
-
eapply serial_intr_handler_asm_high_level_invariant; eauto.
Qed.
Definition primcall_serial_intr_handler_asm_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_serial_intr_handler_asm_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some GlobIdent.serial_intr_handler_asm;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End Serial_Intr_Handler_Asm.
End Semantics.
Require Import Maps.
Require Import Globalenvs.
Require Import AsmX.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import AST.
Require Import AuxStateDataType.
Require Import Constant.
Require Import FlatMemory.
Require Import GlobIdent.
Require Import Integers.
Require Import Conventions.
Require Import LAsm.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import compcert.cfrontend.Ctypes.
Require Import compcert.cfrontend.Cop.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Export mCertiKOSType.
Section Semantics.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context {RData} `{HD: CompatData RData}.
Section Set_Tf.
Variable set_tf_spec: val → RData → option RData.
Inductive primcall_set_tf_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_set_tf_sem_intro:
∀ m (rs: regset) adt adt´ pc,
set_tf_spec pc adt = Some adt´ →
pc = rs#EAX →
∀ N_TYPE_RA: Val.has_type (rs RA) AST.Tint,
∀ N_INJECT_NEUTRAL: (∀ v r, ZtoPreg v = Some r
→ val_inject (Mem.flat_inj (Mem.nextblock m)) (rs#r) (rs#r)),
primcall_set_tf_sem s rs (m, adt) (rs#PC <- (rs#RA)) (m, adt´).
Class SetTfInvariants :=
{
set_tf_low_level_invariant s m pc rs d d´:
set_tf_spec pc d = Some d´ →
asm_invariant s rs m →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
set_tf_high_level_invariant pc d d´:
set_tf_spec pc d = Some d´ →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: SetTfInvariants}.
Require Import FutureTactic.
Local Instance primcall_set_tf_sem_propertes:
PrimcallProperties primcall_set_tf_sem.
Proof.
constructor; intros; inv H.
-
inv H0; split; congruence.
Qed.
Local Instance primcall_set_tf_sem_invariants:
PrimcallInvariants primcall_set_tf_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto.
val_inject_simpl.
+
repeat apply set_reg_wt.
simpl.
eapply N_TYPE_RA; apply PregToZ_correct; simpl; reflexivity.
assumption.
-
eapply set_tf_low_level_invariant; eauto.
-
eapply set_tf_high_level_invariant; eauto.
Qed.
Definition primcall_set_tf_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_set_tf_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some GlobIdent.set_tf;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End Set_Tf.
Section Save_Context.
Variable save_context_spec: regset → RData → RData.
Inductive primcall_save_context_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_savecontext_sem_intro:
∀ m (rs: regset) adt adt´,
save_context_spec rs adt = adt´ →
∀ N_TYPE_RA: Val.has_type (rs RA) AST.Tint,
∀ N_INJECT_NEUTRAL: (∀ v r, ZtoPreg v = Some r
→ val_inject (Mem.flat_inj (Mem.nextblock m)) (rs#r) (rs#r)),
primcall_save_context_sem s rs (m, adt) (rs#PC <- (rs#RA)) (m, adt´).
Class SaveContextInvariants :=
{
save_context_low_level_invariant s m rs d d´:
save_context_spec rs d = d´ →
asm_invariant s rs m →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
save_context_high_level_invariant rs d d´:
save_context_spec rs d = d´ →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: SaveContextInvariants}.
Require Import FutureTactic.
Local Instance primcall_save_context_sem_propertes:
PrimcallProperties primcall_save_context_sem.
Proof.
constructor; intros; inv H.
-
inv H0; split; congruence.
Qed.
Local Instance primcall_save_context_sem_invariants:
PrimcallInvariants primcall_save_context_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto.
val_inject_simpl.
+
repeat apply set_reg_wt.
simpl.
eapply N_TYPE_RA; apply PregToZ_correct; simpl; reflexivity.
assumption.
-
eapply save_context_low_level_invariant; eauto.
-
eapply save_context_high_level_invariant; eauto.
Qed.
Definition primcall_save_context_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_save_context_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some GlobIdent.save_context;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End Save_Context.
Section Restore_Context.
Variable restore_context_spec: RData → (regset × RData).
Inductive primcall_restore_context_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_restorecontext_sem_intro:
∀ m (rs rs´: regset) adt adt´,
restore_context_spec adt = (rs´, adt´)
→ ∀ N_TYPE: wt_regset rs´,
∀ N_INJECT_NEUTRAL: (∀ r, val_inject (Mem.flat_inj (Mem.nextblock m)) (rs´#r) (rs´#r)),
primcall_restore_context_sem s rs (m, adt)
(rs´# PC <- (rs#RA))
(m, adt´).
Class RestoreContextInvariants :=
{
restore_context_low_level_invariant m rs´ d d´:
restore_context_spec d = (rs´, d´) →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
restore_context_high_level_invariant rs´ d d´:
restore_context_spec d = (rs´, d´) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: RestoreContextInvariants}.
Local Instance primcall_restore_context_sem_propertes:
PrimcallProperties primcall_restore_context_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst. split; congruence.
Qed.
Local Instance primcall_restore_context_sem_invariants:
PrimcallInvariants primcall_restore_context_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto.
val_inject_simpl.
+
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl.
try (eapply N_TYPE; apply PregToZ_correct; simpl; reflexivity);
try assumption.
unfold wt_regset in inv_reg_wt.
eapply inv_reg_wt; eauto.
-
eapply restore_context_low_level_invariant; eauto.
-
eapply restore_context_high_level_invariant; eauto.
Qed.
Definition primcall_restore_context_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_restore_context_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some GlobIdent.restore_context;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End Restore_Context.
Section Serial_Intr_Handler_Asm.
Variable serial_intr_handler_asm_spec: regset → RData → option (RData × regset).
Inductive primcall_serial_intr_handler_asm_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_serialintrhandlerasm_sem_intro:
∀ m (rs rs´: regset) adt adt´ b,
serial_intr_handler_asm_spec rs adt = Some (adt´, rs´) →
∀ N_INJECT_NEUTRAL: (∀ r, val_inject (Mem.flat_inj (Mem.nextblock m)) (rs#r) (rs#r)),
∀ Hsymbol: find_symbol s GlobIdent.serial_intr_handler_asm = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ HRS: rs = rs´,
primcall_serial_intr_handler_asm_sem s rs (m, adt) ((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs´) #PC <- (rs#RA) #RA <- Vundef) (m, adt´).
Class SerialIntrHandlerAsmInvariants :=
{
serial_intr_handler_asm_low_level_invariant s m rs rs´ d d´:
serial_intr_handler_asm_spec rs d = Some (d´, rs´) →
asm_invariant s rs m →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
serial_intr_handler_asm_high_level_invariant rs rs´ d d´:
serial_intr_handler_asm_spec rs d = Some (d´, rs´) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: SerialIntrHandlerAsmInvariants}.
Local Instance primcall_serial_intr_handler_asm_sem_propertes:
PrimcallProperties primcall_serial_intr_handler_asm_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst. split; congruence.
Qed.
Local Instance primcall_serial_intr_handler_asm_sem_invariants:
PrimcallInvariants primcall_serial_intr_handler_asm_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL;
apply PregToZ_correct; simpl; reflexivity).
+
repeat apply set_reg_wt; try constructor.
simpl.
unfold wt_regset in inv_reg_wt.
eapply inv_reg_wt.
assumption.
-
eapply serial_intr_handler_asm_low_level_invariant; eauto.
-
eapply serial_intr_handler_asm_high_level_invariant; eauto.
Qed.
Definition primcall_serial_intr_handler_asm_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_serial_intr_handler_asm_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some GlobIdent.serial_intr_handler_asm;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End Serial_Intr_Handler_Asm.
End Semantics.