Library mcertikos.layerlib.IntelPrimSemantics
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.
Require Import liblayers.compat.CompatGenSem.
Section Semantics.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context {RData} `{HD: CompatData RData}.
Inductive is_vmx_exit_reg : preg → Prop :=
| EXIT_EAX: is_vmx_exit_reg (IR EAX)
| EXIT_EBX: is_vmx_exit_reg (IR EBX)
| EXIT_EDX: is_vmx_exit_reg (IR EDX)
| EXIT_EDI: is_vmx_exit_reg (IR EDI)
| EXIT_ESI: is_vmx_exit_reg (IR ESI)
| EXIT_EBP: is_vmx_exit_reg (IR EBP).
Section VMX_EXIT.
Variable vmx_exit_spec: regset → RData → option (RData × regset).
Variable get_CPU_ID_spec: RData → option Z.
Class VMXExitInvariants :=
{
vmx_exit_low_level_invariant m rs rs´ d d´:
vmx_exit_spec rs d = Some (d´, rs´) →
(∀ r, is_vmx_exit_reg r →
Val.has_type (rs#r) AST.Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m)) (rs#r) (rs#r)) →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
vmx_exit_high_level_invariant rs rs´ d d´:
vmx_exit_spec rs d = Some (d´, rs´) →
high_level_invariant d →
high_level_invariant d´
}.
Section EXIT.
Inductive primcall_vmx_exit_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_vmx_exit_sem_intro:
∀ m (rs rs´: regset) adt adt´ b cpuid (cpuidVal: get_CPU_ID_spec adt = Some cpuid),
let rs01 := (Pregmap.init Vundef) #EAX <- (rs EAX) #EBX <- (rs EBX)
#EDX <- (rs EDX) #EDI <- (rs EDI)
#ESI <- (rs ESI) #EBP <- (rs EBP) in
vmx_exit_spec rs01 adt = Some (adt´, rs´)
→ ∀ N_TYPE: ∀ r, Val.has_type (rs´#r) AST.Tint,
∀ N_INJECT_NEUTRAL: (∀ r, val_inject (Mem.flat_inj (Mem.nextblock m)) (rs´#r) (rs´#r)),
∀ Hsymbol: find_symbol s vmx_exit = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ HECXVal: rs ECX = Vint (Int.repr (cpuid × (38 × 4))),
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_vmx_exit_sem s rs (m, adt)
(rs0#EBP <- (rs´ EBP)#EDI<- (rs´ EDI)
#PC <- (rs RA)) (m, adt´).
Section WithInv.
Context`{inv_ops: VMXExitInvariants}.
Local Instance primcall_vmx_exit_sem_propertes:
PrimcallProperties primcall_vmx_exit_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst rs01 rs00 rs0 rs1. split; congruence.
Qed.
Local Instance primcall_vmx_exit_sem_invariants:
PrimcallInvariants primcall_vmx_exit_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto. subst rs01 rs1.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; simpl; reflexivity).
+
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl;
try eapply N_TYPE; simpl; try reflexivity.
eapply inv_reg_wt.
-
eapply vmx_exit_low_level_invariant; eauto.
subst rs01. intros.
inv H0. inv inv_inject_neutral.
inv H;
try (split; [eapply inv_reg_wt | eapply inv_reg_inject_neutral]).
-
eapply vmx_exit_high_level_invariant; eauto.
Qed.
Definition primcall_vmx_exit_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_vmx_exit_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some vmx_exit;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End EXIT.
End VMX_EXIT.
Section RETURN.
Variable vmx_return_spec: RData → option RData.
Class VMXReturnInvariants :=
{
vmx_return_low_level_invariant m d d´:
vmx_return_spec d = Some d´ →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
vmx_return_high_level_invariant d d´:
vmx_return_spec d = Some d´ →
high_level_invariant d →
high_level_invariant d´
}.
Local Open Scope Z_scope.
Inductive primcall_vmx_return_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_vmx_return_sem_intro:
∀ m (rs: regset) adt adt´ b,
vmx_return_spec adt = Some adt´
→ ∀ Hsymbol: find_symbol s vmx_return_from_guest = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ HESP: rs ESP ≠ Vundef,
∀ HESP_STACK:
(∀ b1 o,
rs ESP = Vptr b1 o →
Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m)),
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_vmx_return_sem s rs (m, adt) (rs0#PC <- (Vptr b (Int.repr 3))) (m, adt´).
Section WithInv.
Context`{inv_ops: VMXReturnInvariants}.
Local Instance primcall_vmx_return_sem_propertes:
PrimcallProperties primcall_vmx_return_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst rs0 rs1. split; congruence.
Qed.
Local Instance primcall_vmx_return_sem_invariants:
PrimcallInvariants primcall_vmx_return_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto. subst rs1.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; simpl; omega).
specialize (inv_reg_inject_neutral PC).
rewrite HPC in inv_reg_inject_neutral.
inv inv_reg_inject_neutral.
econstructor; eauto.
rewrite Int.add_zero_l in H5.
rewrite <- H5.
reflexivity.
+
simpl.
unfold AsmX.wt_regset in ×.
intros.
specialize (inv_reg_wt r).
destruct r; try assumption; try constructor.
destruct i; try assumption; try constructor.
destruct f; try assumption; try constructor.
destruct c; try assumption; try constructor.
-
eapply vmx_return_low_level_invariant; eauto.
-
eapply vmx_return_high_level_invariant; eauto.
Qed.
Definition primcall_vmx_return_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_vmx_return_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some vmx_return_from_guest;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End RETURN.
Section VMX_ENTER.
Variable vmx_enter_spec: regset → RData → option (RData × regset).
Variable prim_ident : ident.
Inductive is_vmx_enter_reg : preg → Prop :=
| ENTER_EDI: is_vmx_enter_reg (IR EDI)
| ENTER_EBP: is_vmx_enter_reg (IR EBP).
Inductive primcall_vmx_enter_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_vmx_enter_sem_intro:
∀ m (rs rs´: regset) adt adt´ b,
let rs01 := (Pregmap.init Vundef) #EDI <- (rs EDI) #EBP <- (rs EBP) in
vmx_enter_spec rs01 adt = Some (adt´, rs´)
→ ∀ N_TYPE: ∀ r, Val.has_type (rs´#r) AST.Tint,
∀ N_INJECT_NEUTRAL: (∀ r, val_inject (Mem.flat_inj (Mem.nextblock m)) (rs´#r) (rs´#r)),
∀ Hsymbol: find_symbol s prim_ident = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ HESP: rs ESP ≠ Vundef,
∀ HESP_STACK:
(∀ b1 o,
rs ESP = Vptr b1 o →
Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m)),
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_vmx_enter_sem s rs (m, adt)
(rs0#EAX<- (rs´#EAX)#EBX <- (rs´#EBX)#EDX <- (rs´#EDX)
#ESI <- (rs´#ESI)#EDI <- (rs´#EDI)#EBP <- (rs´#EBP)
#PC <- (rs´#RA)) (m, adt´).
Class VMXEnterInvariants :=
{
vmx_enter_low_level_invariant m rs rs´ d d´:
vmx_enter_spec rs d = Some (d´, rs´) →
(∀ r, is_vmx_enter_reg r →
Val.has_type (rs#r) AST.Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m)) (rs#r) (rs#r)) →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
vmx_enter_high_level_invariant rs rs´ d d´:
vmx_enter_spec rs d = Some (d´, rs´) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: VMXEnterInvariants}.
Local Instance primcall_vmx_enter_sem_propertes:
PrimcallProperties primcall_vmx_enter_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst rs00 rs01 rs0 rs1. split; congruence.
Qed.
Local Instance primcall_vmx_enter_sem_invariants:
PrimcallInvariants primcall_vmx_enter_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto. subst rs1.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; simpl; reflexivity).
+
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl;
eapply N_TYPE; simpl; reflexivity.
-
eapply vmx_enter_low_level_invariant; eauto.
subst rs01. intros.
inv H0. inv inv_inject_neutral.
inv H;
try (split; [eapply inv_reg_wt | eapply inv_reg_inject_neutral]).
-
eapply vmx_enter_high_level_invariant; eauto.
Qed.
Definition primcall_vmx_enter_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_vmx_enter_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some prim_ident;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End VMX_ENTER.
Section VMCS_INIT.
Variable vmcs_set_defaults_spec: block → block → block
→ block → block → block → RData → option RData.
Inductive extcall_vmcs_set_defaults_sem (s: stencil) (WB: block → Prop):
list val → (mwd (cdata RData)) → val → (mwd (cdata RData)) → Prop :=
| extcall_vmcs_set_defaults_sem_intro:
∀ m pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b
host_rip_b adt adt´ sig,
vmcs_set_defaults_spec
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b
host_rip_b adt = Some adt´ →
find_symbol s EPT_LOC = Some pml4ept_b →
find_symbol s STACK_LOC = Some stack_b →
find_symbol s idt_LOC = Some idt_b →
find_symbol s msr_bitmap_LOC = Some msr_bitmap_b →
find_symbol s io_bitmap_LOC = Some io_bitmap_b →
find_symbol s vmx_return_from_guest = Some host_rip_b →
sig = nil →
extcall_vmcs_set_defaults_sem s WB sig (m, adt) Vundef (m, adt´).
Definition extcall_vmcs_set_defaults_info: sextcall_info :=
{|
sextcall_step := extcall_vmcs_set_defaults_sem;
sextcall_csig := mkcsig (type_of_list_type nil) Tvoid;
sextcall_valid s := true
|}.
Class VMCSSetDefaultsInvariants :=
{
vmcs_set_defaults_low_level_invariant
n d d´
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b:
vmcs_set_defaults_spec
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b d = Some d´ →
Mem.flat_inj n pml4ept_b = Some (pml4ept_b, 0%Z) →
Mem.flat_inj n stack_b = Some (stack_b, 0%Z) →
Mem.flat_inj n idt_b = Some (idt_b, 0%Z) →
Mem.flat_inj n msr_bitmap_b = Some (msr_bitmap_b, 0%Z) →
Mem.flat_inj n io_bitmap_b = Some (io_bitmap_b, 0%Z) →
Mem.flat_inj n host_rip_b = Some (host_rip_b, 0%Z) →
low_level_invariant n d →
low_level_invariant n d´;
vmcs_set_defaults_high_level_invariant
d d´
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b:
vmcs_set_defaults_spec
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b d = Some d´ →
high_level_invariant d →
high_level_invariant d´;
vmcs_set_defaults_kernel_mode
d d´
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b:
vmcs_set_defaults_spec
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b d = Some d´ →
kernel_mode d →
kernel_mode d´
}.
Section WithInv.
Context`{inv_ops: VMCSSetDefaultsInvariants}.
Instance extcall_vmcs_set_defaults_invs:
ExtcallInvariants extcall_vmcs_set_defaults_info.
Proof.
constructor; intros; inv H.
-
assert (inject_incr (Mem.flat_inj (genv_next s)) (Mem.flat_inj (Mem.nextblock m´))).
{
eapply flat_inj_inject_incr. assumption.
}
eapply vmcs_set_defaults_low_level_invariant; eauto;
eapply stencil_find_symbol_inject´; eauto.
-
eapply vmcs_set_defaults_high_level_invariant; eauto.
-
eapply vmcs_set_defaults_kernel_mode; eauto.
-
reflexivity.
-
split; auto.
-
simpl; trivial.
Qed.
Instance extcall_vmcs_set_defaults_props:
ExtcallProperties extcall_vmcs_set_defaults_info.
Proof.
constructor; intros.
-
inv H. simpl. trivial.
-
inv H. unfold Mem.valid_block in ×.
lift_unfold. trivial.
-
inv H. lift_unfold. trivial.
-
inv H. simpl. apply Mem.unchanged_on_refl.
-
inv H. inv_val_inject. lift_simpl.
destruct H0 as [HT1 HT2].
destruct m1´ as [? ?]. simpl in ×. subst.
∃ Vundef, (m0, adt´).
refine_split; eauto.
+ econstructor; eauto.
+ lift_unfold. split; trivial.
+ simpl. apply Mem.unchanged_on_refl.
-
inv H0.
inv_val_inject.
lift_simpl. destruct H1 as [HT1 HT2].
destruct m1´ as [? ?]. simpl in ×. subst.
∃ f, Vundef, (m0, adt´).
refine_split; eauto.
+ econstructor; eauto.
+ lift_unfold. split; trivial.
+ apply Mem.unchanged_on_refl.
+ simpl. apply Mem.unchanged_on_refl.
+ constructor; congruence.
-
inv H. inv H0.
split; congruence.
-
inv H0. econstructor; eauto.
-
inv H. lift_unfold. trivial.
Qed.
Definition vmcs_set_defaults_compatsem : compatsem (cdata RData) :=
compatsem_inl {|
sextcall_primsem_step := extcall_vmcs_set_defaults_info;
sextcall_props := OK _;
sextcall_invs := OK _
|}.
End WithInv.
End VMCS_INIT.
Section VMCS_writeb.
Variable vmcs_writeb: Z → block → int → RData → option RData.
Inductive extcall_vmcs_writeb_sem (s: stencil) (WB: block → Prop):
list val → (mwd (cdata RData)) → val → (mwd (cdata RData)) → Prop :=
| extcall_vmcs_writeb_sem_intro:
∀ m adt adt´ loc b ofs,
vmcs_writeb (Int.unsigned loc) b ofs adt = Some adt´
→ (∃ ident, find_symbol s ident = Some b)
→ extcall_vmcs_writeb_sem s WB (Vint loc :: Vptr b ofs :: nil) (m, adt) Vundef (m, adt´).
Definition extcall_vmcs_writeb_info: sextcall_info :=
{|
sextcall_step := extcall_vmcs_writeb_sem;
sextcall_csig := mkcsig (type_of_list_type (Tint32 :: Tpointer Tvoid noattr :: nil)) Tvoid;
sextcall_valid s := true
|}.
Class VMCS_writebInvariants :=
{
vmcs_writeb_low_level_invariant n d z b ofs d´:
vmcs_writeb z b ofs d = Some d´ →
Mem.flat_inj n b = Some (b, 0%Z) →
low_level_invariant n d →
low_level_invariant n d´;
vmcs_writeb_high_level_invariant d z b ofs d´:
vmcs_writeb z b ofs d = Some d´ →
high_level_invariant d →
high_level_invariant d´;
vmcs_writeb_kernel_mode d z b ofs d´:
vmcs_writeb z b ofs d = Some d´ →
kernel_mode d →
kernel_mode d´
}.
Section WithInv.
Context`{inv_ops: VMCS_writebInvariants}.
Instance extcall_vmcs_writeb_invs:
ExtcallInvariants extcall_vmcs_writeb_info.
Proof.
constructor; intros; inv H.
-
eapply vmcs_writeb_low_level_invariant; eauto.
destruct H8 as (fun_id & Hf).
eapply stencil_find_symbol_inject´; eauto.
eapply flat_inj_inject_incr. assumption.
-
eapply vmcs_writeb_high_level_invariant; eauto.
-
eapply vmcs_writeb_kernel_mode; eauto.
-
reflexivity.
-
split; auto.
-
simpl; trivial.
Qed.
Instance extcall_vmcs_writeb_props:
ExtcallProperties extcall_vmcs_writeb_info.
Proof.
constructor; intros.
-
inv H. simpl. trivial.
-
inv H. unfold Mem.valid_block in ×.
lift_unfold. trivial.
-
inv H. lift_unfold. trivial.
-
inv H. simpl. apply Mem.unchanged_on_refl.
-
inv H. inv_val_inject. lift_simpl.
destruct H0 as [HT1 HT2].
destruct m1´ as [? ?]. simpl in ×. subst.
∃ Vundef, (m0, adt´).
refine_split; eauto.
+ econstructor; eauto.
+ lift_unfold. split; trivial.
+ simpl. apply Mem.unchanged_on_refl.
-
inv H0.
inv_val_inject.
lift_simpl. destruct H1 as [HT1 HT2].
destruct m1´ as [? ?]. simpl in ×. subst.
∃ f, Vundef, (m0, adt´).
destruct H4 as (fun_id & Hf).
pose proof Hf as Hf´.
apply H in Hf. rewrite H7 in Hf. inv Hf.
refine_split; eauto.
+ econstructor; eauto.
rewrite Int.add_zero. trivial.
+ lift_unfold. split; trivial.
+ apply Mem.unchanged_on_refl.
+ simpl. apply Mem.unchanged_on_refl.
+ constructor; congruence.
-
inv H. inv H0.
split; congruence.
-
inv H0. econstructor; eauto.
-
inv H. lift_unfold. trivial.
Qed.
Definition vmcs_writeb_compatsem : compatsem (cdata RData) :=
compatsem_inl {|
sextcall_primsem_step := extcall_vmcs_writeb_info;
sextcall_props := OK _;
sextcall_invs := OK _
|}.
End WithInv.
End VMCS_writeb.
Section VMX_READ.
Variable vmx_read_spec: RData → option val.
Inductive primcall_vmx_read_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_vmxread_sem_intro:
∀ m (rs: regset) v adt b sig,
vmx_read_spec adt = Some v
→ sig = mksignature (AST.Tint:: nil) (Some AST.Tint) cc_default
→ extcall_arguments rs m sig nil
→ ∀ Hsymbol: find_symbol s vmx_read = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ N_TYPE: Val.has_type v AST.Tint,
∀ N_INJECT_NEUTRAL: val_inject (Mem.flat_inj (Mem.nextblock m)) v v,
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_vmx_read_sem s rs (m, adt) (rs0 # EAX <- v) (m, adt).
Section WithInv.
Local Instance primcall_vmx_read_sem_propertes:
PrimcallProperties primcall_vmx_read_sem.
Proof.
constructor; intros; inv H.
-
inv H0.
specialize (extcall_arguments_determ _ _ _ _ _ H3 H9).
intros HF. inv HF.
subst rs0 rs1. rewrite H4 in H1. inv H1.
split; trivial.
Qed.
Local Instance primcall_vmx_read_sem_invariants:
PrimcallInvariants primcall_vmx_read_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto. subst rs1.
val_inject_simpl.
+
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl.
Qed.
Definition primcall_vmx_read_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_vmx_read_sem;
sprimcall_sig := mksignature nil (Some AST.Tint) cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some GlobIdent.vmx_read;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End VMX_READ.
Section VMCS_WRITE.
Variable vmcs_write_spec: Z → val → RData → option RData.
Variable prim_ident : ident.
Inductive primcall_vmcs_write_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_vmcswrite_sem_intro:
∀ m (rs: regset) z v adt adt´ b sig,
vmcs_write_spec (Int.unsigned z) v adt = Some adt´
→ sig = mksignature (AST.Tint:: AST.Tint:: nil) None cc_default
→ extcall_arguments rs m sig (Vint z :: v ::nil)
→ ∀ Hsymbol: find_symbol s prim_ident = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ N_TYPE: Val.has_type v AST.Tint,
∀ N_INJECT_NEUTRAL: val_inject (Mem.flat_inj (Mem.nextblock m)) v v,
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_vmcs_write_sem s rs (m, adt) rs0 (m, adt´).
Class VMCSWriteInvariants :=
{
vmcs_write_low_level_invariant m z v d d´:
vmcs_write_spec z v d = Some d´ →
Val.has_type v AST.Tint →
val_inject (Mem.flat_inj (Mem.nextblock m)) v v →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
vmcs_write_high_level_invariant z v d d´:
vmcs_write_spec z v d = Some d´ →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: VMCSWriteInvariants}.
Local Instance primcall_vmcs_write_sem_propertes:
PrimcallProperties primcall_vmcs_write_sem.
Proof.
constructor; intros; inv H.
-
inv H0.
specialize (extcall_arguments_determ _ _ _ _ _ H3 H10).
intros HF. inv HF.
split; try congruence.
Qed.
Local Instance primcall_vmcs_write_sem_invariants:
PrimcallInvariants primcall_vmcs_write_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.
-
eapply vmcs_write_low_level_invariant; eauto.
-
eapply vmcs_write_high_level_invariant; eauto.
Qed.
Definition primcall_vmcs_write_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_vmcs_write_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::nil) None cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some prim_ident;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End VMCS_WRITE.
Section VMCS_READ.
Variable vmcs_read_spec: Z → RData → option val.
Variable prim_ident : ident.
Inductive primcall_vmcs_read_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_vmcsread_sem_intro:
∀ m (rs: regset) z v adt b sig,
vmcs_read_spec (Int.unsigned z) adt = Some v
→ sig = mksignature (AST.Tint:: nil) (Some AST.Tint) cc_default
→ extcall_arguments rs m sig (Vint z ::nil)
→ ∀ Hsymbol: find_symbol s prim_ident = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ N_TYPE: Val.has_type v AST.Tint,
∀ N_INJECT_NEUTRAL: val_inject (Mem.flat_inj (Mem.nextblock m)) v v,
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_vmcs_read_sem s rs (m, adt) (rs0 # EAX <- v) (m, adt).
Section WithInv.
Local Instance primcall_vmcs_read_sem_propertes:
PrimcallProperties primcall_vmcs_read_sem.
Proof.
constructor; intros; inv H.
-
inv H0.
specialize (extcall_arguments_determ _ _ _ _ _ H3 H9).
intros HF. inv HF.
subst rs0 rs1. rewrite H4 in H1. inv H1.
split; trivial.
Qed.
Local Instance primcall_vmcs_read_sem_invariants:
PrimcallInvariants primcall_vmcs_read_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto. subst rs1.
val_inject_simpl.
+
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl.
Qed.
Definition primcall_vmcs_read_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_vmcs_read_sem;
sprimcall_sig := mksignature (AST.Tint::nil) (Some AST.Tint) cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some prim_ident;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End VMCS_READ.
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.
Require Import liblayers.compat.CompatGenSem.
Section Semantics.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context {RData} `{HD: CompatData RData}.
Inductive is_vmx_exit_reg : preg → Prop :=
| EXIT_EAX: is_vmx_exit_reg (IR EAX)
| EXIT_EBX: is_vmx_exit_reg (IR EBX)
| EXIT_EDX: is_vmx_exit_reg (IR EDX)
| EXIT_EDI: is_vmx_exit_reg (IR EDI)
| EXIT_ESI: is_vmx_exit_reg (IR ESI)
| EXIT_EBP: is_vmx_exit_reg (IR EBP).
Section VMX_EXIT.
Variable vmx_exit_spec: regset → RData → option (RData × regset).
Variable get_CPU_ID_spec: RData → option Z.
Class VMXExitInvariants :=
{
vmx_exit_low_level_invariant m rs rs´ d d´:
vmx_exit_spec rs d = Some (d´, rs´) →
(∀ r, is_vmx_exit_reg r →
Val.has_type (rs#r) AST.Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m)) (rs#r) (rs#r)) →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
vmx_exit_high_level_invariant rs rs´ d d´:
vmx_exit_spec rs d = Some (d´, rs´) →
high_level_invariant d →
high_level_invariant d´
}.
Section EXIT.
Inductive primcall_vmx_exit_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_vmx_exit_sem_intro:
∀ m (rs rs´: regset) adt adt´ b cpuid (cpuidVal: get_CPU_ID_spec adt = Some cpuid),
let rs01 := (Pregmap.init Vundef) #EAX <- (rs EAX) #EBX <- (rs EBX)
#EDX <- (rs EDX) #EDI <- (rs EDI)
#ESI <- (rs ESI) #EBP <- (rs EBP) in
vmx_exit_spec rs01 adt = Some (adt´, rs´)
→ ∀ N_TYPE: ∀ r, Val.has_type (rs´#r) AST.Tint,
∀ N_INJECT_NEUTRAL: (∀ r, val_inject (Mem.flat_inj (Mem.nextblock m)) (rs´#r) (rs´#r)),
∀ Hsymbol: find_symbol s vmx_exit = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ HECXVal: rs ECX = Vint (Int.repr (cpuid × (38 × 4))),
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_vmx_exit_sem s rs (m, adt)
(rs0#EBP <- (rs´ EBP)#EDI<- (rs´ EDI)
#PC <- (rs RA)) (m, adt´).
Section WithInv.
Context`{inv_ops: VMXExitInvariants}.
Local Instance primcall_vmx_exit_sem_propertes:
PrimcallProperties primcall_vmx_exit_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst rs01 rs00 rs0 rs1. split; congruence.
Qed.
Local Instance primcall_vmx_exit_sem_invariants:
PrimcallInvariants primcall_vmx_exit_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto. subst rs01 rs1.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; simpl; reflexivity).
+
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl;
try eapply N_TYPE; simpl; try reflexivity.
eapply inv_reg_wt.
-
eapply vmx_exit_low_level_invariant; eauto.
subst rs01. intros.
inv H0. inv inv_inject_neutral.
inv H;
try (split; [eapply inv_reg_wt | eapply inv_reg_inject_neutral]).
-
eapply vmx_exit_high_level_invariant; eauto.
Qed.
Definition primcall_vmx_exit_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_vmx_exit_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some vmx_exit;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End EXIT.
End VMX_EXIT.
Section RETURN.
Variable vmx_return_spec: RData → option RData.
Class VMXReturnInvariants :=
{
vmx_return_low_level_invariant m d d´:
vmx_return_spec d = Some d´ →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
vmx_return_high_level_invariant d d´:
vmx_return_spec d = Some d´ →
high_level_invariant d →
high_level_invariant d´
}.
Local Open Scope Z_scope.
Inductive primcall_vmx_return_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_vmx_return_sem_intro:
∀ m (rs: regset) adt adt´ b,
vmx_return_spec adt = Some adt´
→ ∀ Hsymbol: find_symbol s vmx_return_from_guest = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ HESP: rs ESP ≠ Vundef,
∀ HESP_STACK:
(∀ b1 o,
rs ESP = Vptr b1 o →
Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m)),
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_vmx_return_sem s rs (m, adt) (rs0#PC <- (Vptr b (Int.repr 3))) (m, adt´).
Section WithInv.
Context`{inv_ops: VMXReturnInvariants}.
Local Instance primcall_vmx_return_sem_propertes:
PrimcallProperties primcall_vmx_return_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst rs0 rs1. split; congruence.
Qed.
Local Instance primcall_vmx_return_sem_invariants:
PrimcallInvariants primcall_vmx_return_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto. subst rs1.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; simpl; omega).
specialize (inv_reg_inject_neutral PC).
rewrite HPC in inv_reg_inject_neutral.
inv inv_reg_inject_neutral.
econstructor; eauto.
rewrite Int.add_zero_l in H5.
rewrite <- H5.
reflexivity.
+
simpl.
unfold AsmX.wt_regset in ×.
intros.
specialize (inv_reg_wt r).
destruct r; try assumption; try constructor.
destruct i; try assumption; try constructor.
destruct f; try assumption; try constructor.
destruct c; try assumption; try constructor.
-
eapply vmx_return_low_level_invariant; eauto.
-
eapply vmx_return_high_level_invariant; eauto.
Qed.
Definition primcall_vmx_return_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_vmx_return_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some vmx_return_from_guest;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End RETURN.
Section VMX_ENTER.
Variable vmx_enter_spec: regset → RData → option (RData × regset).
Variable prim_ident : ident.
Inductive is_vmx_enter_reg : preg → Prop :=
| ENTER_EDI: is_vmx_enter_reg (IR EDI)
| ENTER_EBP: is_vmx_enter_reg (IR EBP).
Inductive primcall_vmx_enter_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_vmx_enter_sem_intro:
∀ m (rs rs´: regset) adt adt´ b,
let rs01 := (Pregmap.init Vundef) #EDI <- (rs EDI) #EBP <- (rs EBP) in
vmx_enter_spec rs01 adt = Some (adt´, rs´)
→ ∀ N_TYPE: ∀ r, Val.has_type (rs´#r) AST.Tint,
∀ N_INJECT_NEUTRAL: (∀ r, val_inject (Mem.flat_inj (Mem.nextblock m)) (rs´#r) (rs´#r)),
∀ Hsymbol: find_symbol s prim_ident = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ HESP: rs ESP ≠ Vundef,
∀ HESP_STACK:
(∀ b1 o,
rs ESP = Vptr b1 o →
Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m)),
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_vmx_enter_sem s rs (m, adt)
(rs0#EAX<- (rs´#EAX)#EBX <- (rs´#EBX)#EDX <- (rs´#EDX)
#ESI <- (rs´#ESI)#EDI <- (rs´#EDI)#EBP <- (rs´#EBP)
#PC <- (rs´#RA)) (m, adt´).
Class VMXEnterInvariants :=
{
vmx_enter_low_level_invariant m rs rs´ d d´:
vmx_enter_spec rs d = Some (d´, rs´) →
(∀ r, is_vmx_enter_reg r →
Val.has_type (rs#r) AST.Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m)) (rs#r) (rs#r)) →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
vmx_enter_high_level_invariant rs rs´ d d´:
vmx_enter_spec rs d = Some (d´, rs´) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: VMXEnterInvariants}.
Local Instance primcall_vmx_enter_sem_propertes:
PrimcallProperties primcall_vmx_enter_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst rs00 rs01 rs0 rs1. split; congruence.
Qed.
Local Instance primcall_vmx_enter_sem_invariants:
PrimcallInvariants primcall_vmx_enter_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto. subst rs1.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; simpl; reflexivity).
+
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl;
eapply N_TYPE; simpl; reflexivity.
-
eapply vmx_enter_low_level_invariant; eauto.
subst rs01. intros.
inv H0. inv inv_inject_neutral.
inv H;
try (split; [eapply inv_reg_wt | eapply inv_reg_inject_neutral]).
-
eapply vmx_enter_high_level_invariant; eauto.
Qed.
Definition primcall_vmx_enter_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_vmx_enter_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some prim_ident;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End VMX_ENTER.
Section VMCS_INIT.
Variable vmcs_set_defaults_spec: block → block → block
→ block → block → block → RData → option RData.
Inductive extcall_vmcs_set_defaults_sem (s: stencil) (WB: block → Prop):
list val → (mwd (cdata RData)) → val → (mwd (cdata RData)) → Prop :=
| extcall_vmcs_set_defaults_sem_intro:
∀ m pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b
host_rip_b adt adt´ sig,
vmcs_set_defaults_spec
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b
host_rip_b adt = Some adt´ →
find_symbol s EPT_LOC = Some pml4ept_b →
find_symbol s STACK_LOC = Some stack_b →
find_symbol s idt_LOC = Some idt_b →
find_symbol s msr_bitmap_LOC = Some msr_bitmap_b →
find_symbol s io_bitmap_LOC = Some io_bitmap_b →
find_symbol s vmx_return_from_guest = Some host_rip_b →
sig = nil →
extcall_vmcs_set_defaults_sem s WB sig (m, adt) Vundef (m, adt´).
Definition extcall_vmcs_set_defaults_info: sextcall_info :=
{|
sextcall_step := extcall_vmcs_set_defaults_sem;
sextcall_csig := mkcsig (type_of_list_type nil) Tvoid;
sextcall_valid s := true
|}.
Class VMCSSetDefaultsInvariants :=
{
vmcs_set_defaults_low_level_invariant
n d d´
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b:
vmcs_set_defaults_spec
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b d = Some d´ →
Mem.flat_inj n pml4ept_b = Some (pml4ept_b, 0%Z) →
Mem.flat_inj n stack_b = Some (stack_b, 0%Z) →
Mem.flat_inj n idt_b = Some (idt_b, 0%Z) →
Mem.flat_inj n msr_bitmap_b = Some (msr_bitmap_b, 0%Z) →
Mem.flat_inj n io_bitmap_b = Some (io_bitmap_b, 0%Z) →
Mem.flat_inj n host_rip_b = Some (host_rip_b, 0%Z) →
low_level_invariant n d →
low_level_invariant n d´;
vmcs_set_defaults_high_level_invariant
d d´
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b:
vmcs_set_defaults_spec
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b d = Some d´ →
high_level_invariant d →
high_level_invariant d´;
vmcs_set_defaults_kernel_mode
d d´
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b:
vmcs_set_defaults_spec
pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b d = Some d´ →
kernel_mode d →
kernel_mode d´
}.
Section WithInv.
Context`{inv_ops: VMCSSetDefaultsInvariants}.
Instance extcall_vmcs_set_defaults_invs:
ExtcallInvariants extcall_vmcs_set_defaults_info.
Proof.
constructor; intros; inv H.
-
assert (inject_incr (Mem.flat_inj (genv_next s)) (Mem.flat_inj (Mem.nextblock m´))).
{
eapply flat_inj_inject_incr. assumption.
}
eapply vmcs_set_defaults_low_level_invariant; eauto;
eapply stencil_find_symbol_inject´; eauto.
-
eapply vmcs_set_defaults_high_level_invariant; eauto.
-
eapply vmcs_set_defaults_kernel_mode; eauto.
-
reflexivity.
-
split; auto.
-
simpl; trivial.
Qed.
Instance extcall_vmcs_set_defaults_props:
ExtcallProperties extcall_vmcs_set_defaults_info.
Proof.
constructor; intros.
-
inv H. simpl. trivial.
-
inv H. unfold Mem.valid_block in ×.
lift_unfold. trivial.
-
inv H. lift_unfold. trivial.
-
inv H. simpl. apply Mem.unchanged_on_refl.
-
inv H. inv_val_inject. lift_simpl.
destruct H0 as [HT1 HT2].
destruct m1´ as [? ?]. simpl in ×. subst.
∃ Vundef, (m0, adt´).
refine_split; eauto.
+ econstructor; eauto.
+ lift_unfold. split; trivial.
+ simpl. apply Mem.unchanged_on_refl.
-
inv H0.
inv_val_inject.
lift_simpl. destruct H1 as [HT1 HT2].
destruct m1´ as [? ?]. simpl in ×. subst.
∃ f, Vundef, (m0, adt´).
refine_split; eauto.
+ econstructor; eauto.
+ lift_unfold. split; trivial.
+ apply Mem.unchanged_on_refl.
+ simpl. apply Mem.unchanged_on_refl.
+ constructor; congruence.
-
inv H. inv H0.
split; congruence.
-
inv H0. econstructor; eauto.
-
inv H. lift_unfold. trivial.
Qed.
Definition vmcs_set_defaults_compatsem : compatsem (cdata RData) :=
compatsem_inl {|
sextcall_primsem_step := extcall_vmcs_set_defaults_info;
sextcall_props := OK _;
sextcall_invs := OK _
|}.
End WithInv.
End VMCS_INIT.
Section VMCS_writeb.
Variable vmcs_writeb: Z → block → int → RData → option RData.
Inductive extcall_vmcs_writeb_sem (s: stencil) (WB: block → Prop):
list val → (mwd (cdata RData)) → val → (mwd (cdata RData)) → Prop :=
| extcall_vmcs_writeb_sem_intro:
∀ m adt adt´ loc b ofs,
vmcs_writeb (Int.unsigned loc) b ofs adt = Some adt´
→ (∃ ident, find_symbol s ident = Some b)
→ extcall_vmcs_writeb_sem s WB (Vint loc :: Vptr b ofs :: nil) (m, adt) Vundef (m, adt´).
Definition extcall_vmcs_writeb_info: sextcall_info :=
{|
sextcall_step := extcall_vmcs_writeb_sem;
sextcall_csig := mkcsig (type_of_list_type (Tint32 :: Tpointer Tvoid noattr :: nil)) Tvoid;
sextcall_valid s := true
|}.
Class VMCS_writebInvariants :=
{
vmcs_writeb_low_level_invariant n d z b ofs d´:
vmcs_writeb z b ofs d = Some d´ →
Mem.flat_inj n b = Some (b, 0%Z) →
low_level_invariant n d →
low_level_invariant n d´;
vmcs_writeb_high_level_invariant d z b ofs d´:
vmcs_writeb z b ofs d = Some d´ →
high_level_invariant d →
high_level_invariant d´;
vmcs_writeb_kernel_mode d z b ofs d´:
vmcs_writeb z b ofs d = Some d´ →
kernel_mode d →
kernel_mode d´
}.
Section WithInv.
Context`{inv_ops: VMCS_writebInvariants}.
Instance extcall_vmcs_writeb_invs:
ExtcallInvariants extcall_vmcs_writeb_info.
Proof.
constructor; intros; inv H.
-
eapply vmcs_writeb_low_level_invariant; eauto.
destruct H8 as (fun_id & Hf).
eapply stencil_find_symbol_inject´; eauto.
eapply flat_inj_inject_incr. assumption.
-
eapply vmcs_writeb_high_level_invariant; eauto.
-
eapply vmcs_writeb_kernel_mode; eauto.
-
reflexivity.
-
split; auto.
-
simpl; trivial.
Qed.
Instance extcall_vmcs_writeb_props:
ExtcallProperties extcall_vmcs_writeb_info.
Proof.
constructor; intros.
-
inv H. simpl. trivial.
-
inv H. unfold Mem.valid_block in ×.
lift_unfold. trivial.
-
inv H. lift_unfold. trivial.
-
inv H. simpl. apply Mem.unchanged_on_refl.
-
inv H. inv_val_inject. lift_simpl.
destruct H0 as [HT1 HT2].
destruct m1´ as [? ?]. simpl in ×. subst.
∃ Vundef, (m0, adt´).
refine_split; eauto.
+ econstructor; eauto.
+ lift_unfold. split; trivial.
+ simpl. apply Mem.unchanged_on_refl.
-
inv H0.
inv_val_inject.
lift_simpl. destruct H1 as [HT1 HT2].
destruct m1´ as [? ?]. simpl in ×. subst.
∃ f, Vundef, (m0, adt´).
destruct H4 as (fun_id & Hf).
pose proof Hf as Hf´.
apply H in Hf. rewrite H7 in Hf. inv Hf.
refine_split; eauto.
+ econstructor; eauto.
rewrite Int.add_zero. trivial.
+ lift_unfold. split; trivial.
+ apply Mem.unchanged_on_refl.
+ simpl. apply Mem.unchanged_on_refl.
+ constructor; congruence.
-
inv H. inv H0.
split; congruence.
-
inv H0. econstructor; eauto.
-
inv H. lift_unfold. trivial.
Qed.
Definition vmcs_writeb_compatsem : compatsem (cdata RData) :=
compatsem_inl {|
sextcall_primsem_step := extcall_vmcs_writeb_info;
sextcall_props := OK _;
sextcall_invs := OK _
|}.
End WithInv.
End VMCS_writeb.
Section VMX_READ.
Variable vmx_read_spec: RData → option val.
Inductive primcall_vmx_read_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_vmxread_sem_intro:
∀ m (rs: regset) v adt b sig,
vmx_read_spec adt = Some v
→ sig = mksignature (AST.Tint:: nil) (Some AST.Tint) cc_default
→ extcall_arguments rs m sig nil
→ ∀ Hsymbol: find_symbol s vmx_read = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ N_TYPE: Val.has_type v AST.Tint,
∀ N_INJECT_NEUTRAL: val_inject (Mem.flat_inj (Mem.nextblock m)) v v,
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_vmx_read_sem s rs (m, adt) (rs0 # EAX <- v) (m, adt).
Section WithInv.
Local Instance primcall_vmx_read_sem_propertes:
PrimcallProperties primcall_vmx_read_sem.
Proof.
constructor; intros; inv H.
-
inv H0.
specialize (extcall_arguments_determ _ _ _ _ _ H3 H9).
intros HF. inv HF.
subst rs0 rs1. rewrite H4 in H1. inv H1.
split; trivial.
Qed.
Local Instance primcall_vmx_read_sem_invariants:
PrimcallInvariants primcall_vmx_read_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto. subst rs1.
val_inject_simpl.
+
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl.
Qed.
Definition primcall_vmx_read_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_vmx_read_sem;
sprimcall_sig := mksignature nil (Some AST.Tint) cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some GlobIdent.vmx_read;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End VMX_READ.
Section VMCS_WRITE.
Variable vmcs_write_spec: Z → val → RData → option RData.
Variable prim_ident : ident.
Inductive primcall_vmcs_write_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_vmcswrite_sem_intro:
∀ m (rs: regset) z v adt adt´ b sig,
vmcs_write_spec (Int.unsigned z) v adt = Some adt´
→ sig = mksignature (AST.Tint:: AST.Tint:: nil) None cc_default
→ extcall_arguments rs m sig (Vint z :: v ::nil)
→ ∀ Hsymbol: find_symbol s prim_ident = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ N_TYPE: Val.has_type v AST.Tint,
∀ N_INJECT_NEUTRAL: val_inject (Mem.flat_inj (Mem.nextblock m)) v v,
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_vmcs_write_sem s rs (m, adt) rs0 (m, adt´).
Class VMCSWriteInvariants :=
{
vmcs_write_low_level_invariant m z v d d´:
vmcs_write_spec z v d = Some d´ →
Val.has_type v AST.Tint →
val_inject (Mem.flat_inj (Mem.nextblock m)) v v →
low_level_invariant (Mem.nextblock m) d →
low_level_invariant (Mem.nextblock m) d´;
vmcs_write_high_level_invariant z v d d´:
vmcs_write_spec z v d = Some d´ →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: VMCSWriteInvariants}.
Local Instance primcall_vmcs_write_sem_propertes:
PrimcallProperties primcall_vmcs_write_sem.
Proof.
constructor; intros; inv H.
-
inv H0.
specialize (extcall_arguments_determ _ _ _ _ _ H3 H10).
intros HF. inv HF.
split; try congruence.
Qed.
Local Instance primcall_vmcs_write_sem_invariants:
PrimcallInvariants primcall_vmcs_write_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.
-
eapply vmcs_write_low_level_invariant; eauto.
-
eapply vmcs_write_high_level_invariant; eauto.
Qed.
Definition primcall_vmcs_write_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_vmcs_write_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::nil) None cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some prim_ident;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End VMCS_WRITE.
Section VMCS_READ.
Variable vmcs_read_spec: Z → RData → option val.
Variable prim_ident : ident.
Inductive primcall_vmcs_read_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_vmcsread_sem_intro:
∀ m (rs: regset) z v adt b sig,
vmcs_read_spec (Int.unsigned z) adt = Some v
→ sig = mksignature (AST.Tint:: nil) (Some AST.Tint) cc_default
→ extcall_arguments rs m sig (Vint z ::nil)
→ ∀ Hsymbol: find_symbol s prim_ident = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ N_TYPE: Val.has_type v AST.Tint,
∀ N_INJECT_NEUTRAL: val_inject (Mem.flat_inj (Mem.nextblock m)) v v,
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_vmcs_read_sem s rs (m, adt) (rs0 # EAX <- v) (m, adt).
Section WithInv.
Local Instance primcall_vmcs_read_sem_propertes:
PrimcallProperties primcall_vmcs_read_sem.
Proof.
constructor; intros; inv H.
-
inv H0.
specialize (extcall_arguments_determ _ _ _ _ _ H3 H9).
intros HF. inv HF.
subst rs0 rs1. rewrite H4 in H1. inv H1.
split; trivial.
Qed.
Local Instance primcall_vmcs_read_sem_invariants:
PrimcallInvariants primcall_vmcs_read_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto. subst rs1.
val_inject_simpl.
+
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl.
Qed.
Definition primcall_vmcs_read_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_vmcs_read_sem;
sprimcall_sig := mksignature (AST.Tint::nil) (Some AST.Tint) cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some prim_ident;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End VMCS_READ.
End Semantics.