Library mcertikos.proc.VMCSIntroGenSpec
This file provide the contextual refinement proof between MBoot layer and MALInit layer
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import Conventions.
Require Import VEPTInit.
Require Import ObjVMCS.
Require Import AbstractDataType.
Require Import mCertiKOSType.
Require Import Z64Lemma.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import Conventions.
Require Import VEPTInit.
Require Import ObjVMCS.
Require Import AbstractDataType.
Require Import mCertiKOSType.
Require Import Z64Lemma.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Section SPECIFICATION.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation LDATA := RData.
Notation LDATAOps := (cdata LDATA).
Notation v_vmcs_size := 4096.
Inductive vmcs_get_revid_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
vmcs_get_revid_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 v:
find_symbol s VMCS_LOC = Some b0 →
Mem.load Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + 0) = Some (Vint v) →
kernel_mode (snd m´0) →
vmcs_get_revid_spec_low_step s WB nil m´0 (Vint v) m´0.
Inductive vmcs_set_revid_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
vmcs_set_revid_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 v:
find_symbol s VMCS_LOC = Some b0 →
Mem.store Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + 0) (Vint v) = Some m0 →
kernel_mode (snd m´0) →
vmcs_set_revid_spec_low_step s WB (Vint v :: nil) m´0 Vundef m0.
Inductive vmcs_get_abrtid_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
vmcs_get_abrtid_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 v:
find_symbol s VMCS_LOC = Some b0 →
Mem.load Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + 4) = Some (Vint v) →
kernel_mode (snd m´0) →
vmcs_get_abrtid_spec_low_step s WB nil m´0 (Vint v) m´0.
Inductive vmcs_set_abrtid_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
vmcs_set_abrtid_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 v:
find_symbol s VMCS_LOC = Some b0 →
Mem.store Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + 4) (Vint v) = Some m0 →
kernel_mode (snd m´0) →
vmcs_set_abrtid_spec_low_step s WB (Vint v :: nil) m´0 Vundef m0.
Inductive vmcs_readz_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmcs_readz_spec_low_intro s (m´0: mwd LDATAOps) b b0 enc res res´ rs sig:
find_symbol s vmcs_readz = Some b →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned enc) = Some res´ →
Mem.load Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 8) = Some (Vint res) →
sig = mksignature (AST.Tint::nil) (Some AST.Tint) cc_default →
extcall_arguments rs m´0 sig (Vint enc :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
high_level_invariant (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
vmcs_readz_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)
#EAX <- (Vint res)) m´0.
Inductive vmcs_writez_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmcs_writez_spec_low_intro s (m´0 m0: mwd LDATAOps) b b0 enc v res´ rs sig:
find_symbol s vmcs_writez = Some b →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned enc) = Some res´ →
Mem.store Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 8) (Vint v) = Some m0 →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m´0 sig (Vint enc :: Vint v :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
high_level_invariant (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR EAX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
vmcs_writez_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)) m0.
Inductive vmcs_readz64_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmcs_readz64_spec_low_intro s (m´0: mwd LDATAOps) b b0 enc v1 v2 res res´ rs sig:
find_symbol s vmcs_readz64 = Some b →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned enc) = Some res´ →
Mem.load Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 8) = Some (Vint v1) →
Mem.load Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 12) = Some (Vint v2) →
VZ64 (Int64.unsigned res) = VZ64 (Z64ofwords (Int.unsigned v2) (Int.unsigned v1)) →
sig = mksignature (AST.Tint::nil) (Some AST.Tlong) cc_default →
extcall_arguments rs m´0 sig (Vint enc :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
high_level_invariant (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
vmcs_readz64_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)
#EAX <- (Vint v1) #EDX <- (Vint v2)) m´0.
Inductive vmcs_writez64_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmcs_writez64_spec_low_intro s (m´0 m0 m1: mwd LDATAOps) b b0 enc v1 v2 res´ rs sig:
find_symbol s vmcs_writez64 = Some b →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned enc) = Some res´ →
Mem.store Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 8) (Vint v1) = Some m0 →
Mem.store Mint32 m0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 12) (Vint v2) = Some m1 →
sig = mksignature (AST.Tint::AST.Tlong::nil) None cc_default →
extcall_arguments rs m´0 sig (Vint enc :: Vint v2 :: Vint v1 :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
high_level_invariant (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: IR ECX :: IR EDX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
vmcs_writez64_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)) m1.
Inductive vmcs_write_ident_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmcs_write_ident_spec_low_intro s (m´0 m0: mwd LDATAOps) b b0 b´ ofs enc res´ sig rs:
find_symbol s vmcs_write_ident = Some b →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
(∃ ident, find_symbol s ident = Some b´) →
vmcs_ZtoEncoding (Int.unsigned enc) = Some res´ →
Mem.store Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 8) (Vptr b´ ofs) = Some m0 →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m´0 sig (Vint enc :: Vptr b´ ofs :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
high_level_invariant (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR EAX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
vmcs_write_ident_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)) m0.
Inductive rcr0_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
rcr0_spec_low_intro s (m´0: mwd LDATAOps) b rs:
find_symbol s rcr0 = Some b →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
rcr0_spec_low_step s rs m´0 (rs#RA<- Vundef#PC <- (rs#RA)
#EAX <- Vzero) m´0.
Inductive rcr3_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
rcr3_spec_low_intro s (m´0: mwd LDATAOps) b rs:
find_symbol s rcr3 = Some b →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
rcr3_spec_low_step s rs m´0 (rs#RA<- Vundef#PC <- (rs#RA)
#EAX <- Vzero) m´0.
Inductive rcr4_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
rcr4_spec_low_intro s (m´0: mwd LDATAOps) b rs:
find_symbol s rcr4 = Some b →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
rcr4_spec_low_step s rs m´0 (rs#RA<- Vundef#PC <- (rs#RA)
#EAX <- Vzero) m´0.
Inductive vmx_enable_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmx_enable_spec_low_intro s (m´0: mwd LDATAOps) b rs:
find_symbol s vmx_enable = Some b →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
vmx_enable_spec_low_step s rs m´0 (rs#RA<- Vundef#PC <- (rs#RA)) m´0.
Inductive rdmsr_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
rdmsr_spec_low_intro s (m´0: mwd LDATAOps) b rs i sig:
find_symbol s rdmsr = Some b →
rs PC = Vptr b Int.zero →
sig = mksignature (AST.Tint::nil) (Some AST.Tlong) cc_default →
extcall_arguments rs m´0 sig (Vint i :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
rdmsr_spec_low_step s rs m´0 (rs´#EAX<- Vzero#EDX <- Vzero#PC <- (rs#RA)) m´0.
Inductive wrmsr_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
wrmsr_spec_low_intro s (m´0: mwd LDATAOps) b rs v i0 i1 sig:
find_symbol s wrmsr = Some b →
rs PC = Vptr b Int.zero →
sig = mksignature (AST.Tint::AST.Tlong::nil) (Some AST.Tint) cc_default →
extcall_arguments rs m´0 sig (Vint v :: Vint i1 :: Vint i0 :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR ECX :: IR EDX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
wrmsr_spec_low_step s rs m´0 (rs´#PC <- (rs#RA) #EAX <- Vzero) m´0.
Inductive vmptr_ld_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmptr_ld_spec_low_intro s (m´0: mwd LDATAOps) b b0 rs:
find_symbol s vmptrld = Some b →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
high_level_invariant (snd m´0) →
find_symbol s VMCS_LOC = Some b0 →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
vmptr_ld_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)) m´0.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Notation Tint64 := (Tlong Unsigned noattr).
Definition vmcs_get_revid_spec_low: compatsem LDATAOps :=
csem vmcs_get_revid_spec_low_step (type_of_list_type (nil)) Tint32.
Definition vmcs_set_revid_spec_low: compatsem LDATAOps :=
csem vmcs_set_revid_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.
Definition vmcs_get_abrtid_spec_low: compatsem LDATAOps :=
csem vmcs_get_abrtid_spec_low_step (type_of_list_type (nil)) Tint32.
Definition vmcs_set_abrtid_spec_low: compatsem LDATAOps :=
csem vmcs_set_abrtid_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.
Definition vmcs_readz_spec_low: compatsem LDATAOps :=
asmsem_withsig vmcs_readz vmcs_readz_spec_low_step (mksignature (AST.Tint::nil) (Some AST.Tint) cc_default).
Definition vmcs_writez_spec_low: compatsem LDATAOps :=
asmsem_withsig vmcs_writez vmcs_writez_spec_low_step (mksignature (AST.Tint::AST.Tint::nil) None cc_default).
Definition vmcs_readz64_spec_low: compatsem LDATAOps :=
asmsem_withsig vmcs_readz64 vmcs_readz64_spec_low_step (mksignature (AST.Tint::nil) (Some AST.Tlong) cc_default).
Definition vmcs_writez64_spec_low: compatsem LDATAOps :=
asmsem_withsig vmcs_writez64 vmcs_writez64_spec_low_step (mksignature (AST.Tint::AST.Tlong::nil) None cc_default).
Definition vmcs_write_ident_spec_low: compatsem LDATAOps :=
asmsem_withsig vmcs_write_ident vmcs_write_ident_spec_low_step (mksignature (AST.Tint::AST.Tint::nil) None cc_default).
Definition rcr0_spec_low: compatsem LDATAOps :=
asmsem_withsig rcr0 rcr0_spec_low_step (mksignature nil (Some AST.Tint) cc_default).
Definition rcr3_spec_low: compatsem LDATAOps :=
asmsem_withsig rcr3 rcr3_spec_low_step (mksignature nil (Some AST.Tint) cc_default).
Definition rcr4_spec_low: compatsem LDATAOps :=
asmsem_withsig rcr4 rcr4_spec_low_step (mksignature nil (Some AST.Tint) cc_default).
Definition rdmsr_spec_low: compatsem LDATAOps :=
asmsem_withsig rdmsr rdmsr_spec_low_step (mksignature (AST.Tint::nil) (Some AST.Tlong) cc_default).
Definition wrmsr_spec_low: compatsem LDATAOps :=
asmsem_withsig wrmsr wrmsr_spec_low_step (mksignature (AST.Tint::AST.Tlong::nil) (Some AST.Tint) cc_default).
Definition vmptr_ld_spec_low: compatsem LDATAOps :=
asmsem_withsig vmptrld vmptr_ld_spec_low_step (mksignature nil None cc_default).
Definition vmx_enable_spec_low: compatsem LDATAOps :=
asmsem_withsig vmx_enable vmx_enable_spec_low_step (mksignature nil None cc_default).
End WITHMEM.
End SPECIFICATION.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation LDATA := RData.
Notation LDATAOps := (cdata LDATA).
Notation v_vmcs_size := 4096.
Inductive vmcs_get_revid_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
vmcs_get_revid_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 v:
find_symbol s VMCS_LOC = Some b0 →
Mem.load Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + 0) = Some (Vint v) →
kernel_mode (snd m´0) →
vmcs_get_revid_spec_low_step s WB nil m´0 (Vint v) m´0.
Inductive vmcs_set_revid_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
vmcs_set_revid_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 v:
find_symbol s VMCS_LOC = Some b0 →
Mem.store Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + 0) (Vint v) = Some m0 →
kernel_mode (snd m´0) →
vmcs_set_revid_spec_low_step s WB (Vint v :: nil) m´0 Vundef m0.
Inductive vmcs_get_abrtid_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
vmcs_get_abrtid_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 v:
find_symbol s VMCS_LOC = Some b0 →
Mem.load Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + 4) = Some (Vint v) →
kernel_mode (snd m´0) →
vmcs_get_abrtid_spec_low_step s WB nil m´0 (Vint v) m´0.
Inductive vmcs_set_abrtid_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
vmcs_set_abrtid_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 v:
find_symbol s VMCS_LOC = Some b0 →
Mem.store Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + 4) (Vint v) = Some m0 →
kernel_mode (snd m´0) →
vmcs_set_abrtid_spec_low_step s WB (Vint v :: nil) m´0 Vundef m0.
Inductive vmcs_readz_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmcs_readz_spec_low_intro s (m´0: mwd LDATAOps) b b0 enc res res´ rs sig:
find_symbol s vmcs_readz = Some b →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned enc) = Some res´ →
Mem.load Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 8) = Some (Vint res) →
sig = mksignature (AST.Tint::nil) (Some AST.Tint) cc_default →
extcall_arguments rs m´0 sig (Vint enc :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
high_level_invariant (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
vmcs_readz_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)
#EAX <- (Vint res)) m´0.
Inductive vmcs_writez_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmcs_writez_spec_low_intro s (m´0 m0: mwd LDATAOps) b b0 enc v res´ rs sig:
find_symbol s vmcs_writez = Some b →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned enc) = Some res´ →
Mem.store Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 8) (Vint v) = Some m0 →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m´0 sig (Vint enc :: Vint v :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
high_level_invariant (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR EAX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
vmcs_writez_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)) m0.
Inductive vmcs_readz64_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmcs_readz64_spec_low_intro s (m´0: mwd LDATAOps) b b0 enc v1 v2 res res´ rs sig:
find_symbol s vmcs_readz64 = Some b →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned enc) = Some res´ →
Mem.load Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 8) = Some (Vint v1) →
Mem.load Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 12) = Some (Vint v2) →
VZ64 (Int64.unsigned res) = VZ64 (Z64ofwords (Int.unsigned v2) (Int.unsigned v1)) →
sig = mksignature (AST.Tint::nil) (Some AST.Tlong) cc_default →
extcall_arguments rs m´0 sig (Vint enc :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
high_level_invariant (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
vmcs_readz64_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)
#EAX <- (Vint v1) #EDX <- (Vint v2)) m´0.
Inductive vmcs_writez64_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmcs_writez64_spec_low_intro s (m´0 m0 m1: mwd LDATAOps) b b0 enc v1 v2 res´ rs sig:
find_symbol s vmcs_writez64 = Some b →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned enc) = Some res´ →
Mem.store Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 8) (Vint v1) = Some m0 →
Mem.store Mint32 m0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 12) (Vint v2) = Some m1 →
sig = mksignature (AST.Tint::AST.Tlong::nil) None cc_default →
extcall_arguments rs m´0 sig (Vint enc :: Vint v2 :: Vint v1 :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
high_level_invariant (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: IR ECX :: IR EDX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
vmcs_writez64_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)) m1.
Inductive vmcs_write_ident_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmcs_write_ident_spec_low_intro s (m´0 m0: mwd LDATAOps) b b0 b´ ofs enc res´ sig rs:
find_symbol s vmcs_write_ident = Some b →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
(∃ ident, find_symbol s ident = Some b´) →
vmcs_ZtoEncoding (Int.unsigned enc) = Some res´ →
Mem.store Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m´0)) + (Int.unsigned enc) × 4 + 8) (Vptr b´ ofs) = Some m0 →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m´0 sig (Vint enc :: Vptr b´ ofs :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
high_level_invariant (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR EAX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
vmcs_write_ident_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)) m0.
Inductive rcr0_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
rcr0_spec_low_intro s (m´0: mwd LDATAOps) b rs:
find_symbol s rcr0 = Some b →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
rcr0_spec_low_step s rs m´0 (rs#RA<- Vundef#PC <- (rs#RA)
#EAX <- Vzero) m´0.
Inductive rcr3_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
rcr3_spec_low_intro s (m´0: mwd LDATAOps) b rs:
find_symbol s rcr3 = Some b →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
rcr3_spec_low_step s rs m´0 (rs#RA<- Vundef#PC <- (rs#RA)
#EAX <- Vzero) m´0.
Inductive rcr4_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
rcr4_spec_low_intro s (m´0: mwd LDATAOps) b rs:
find_symbol s rcr4 = Some b →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
rcr4_spec_low_step s rs m´0 (rs#RA<- Vundef#PC <- (rs#RA)
#EAX <- Vzero) m´0.
Inductive vmx_enable_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmx_enable_spec_low_intro s (m´0: mwd LDATAOps) b rs:
find_symbol s vmx_enable = Some b →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
vmx_enable_spec_low_step s rs m´0 (rs#RA<- Vundef#PC <- (rs#RA)) m´0.
Inductive rdmsr_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
rdmsr_spec_low_intro s (m´0: mwd LDATAOps) b rs i sig:
find_symbol s rdmsr = Some b →
rs PC = Vptr b Int.zero →
sig = mksignature (AST.Tint::nil) (Some AST.Tlong) cc_default →
extcall_arguments rs m´0 sig (Vint i :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
rdmsr_spec_low_step s rs m´0 (rs´#EAX<- Vzero#EDX <- Vzero#PC <- (rs#RA)) m´0.
Inductive wrmsr_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
wrmsr_spec_low_intro s (m´0: mwd LDATAOps) b rs v i0 i1 sig:
find_symbol s wrmsr = Some b →
rs PC = Vptr b Int.zero →
sig = mksignature (AST.Tint::AST.Tlong::nil) (Some AST.Tint) cc_default →
extcall_arguments rs m´0 sig (Vint v :: Vint i1 :: Vint i0 :: nil) →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR ECX :: IR EDX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
wrmsr_spec_low_step s rs m´0 (rs´#PC <- (rs#RA) #EAX <- Vzero) m´0.
Inductive vmptr_ld_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sprimcall_sem (mem := mwd LDATAOps):=
vmptr_ld_spec_low_intro s (m´0: mwd LDATAOps) b b0 rs:
find_symbol s vmptrld = Some b →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m´0 →
kernel_mode (snd m´0) →
high_level_invariant (snd m´0) →
find_symbol s VMCS_LOC = Some b0 →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
vmptr_ld_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)) m´0.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Notation Tint64 := (Tlong Unsigned noattr).
Definition vmcs_get_revid_spec_low: compatsem LDATAOps :=
csem vmcs_get_revid_spec_low_step (type_of_list_type (nil)) Tint32.
Definition vmcs_set_revid_spec_low: compatsem LDATAOps :=
csem vmcs_set_revid_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.
Definition vmcs_get_abrtid_spec_low: compatsem LDATAOps :=
csem vmcs_get_abrtid_spec_low_step (type_of_list_type (nil)) Tint32.
Definition vmcs_set_abrtid_spec_low: compatsem LDATAOps :=
csem vmcs_set_abrtid_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.
Definition vmcs_readz_spec_low: compatsem LDATAOps :=
asmsem_withsig vmcs_readz vmcs_readz_spec_low_step (mksignature (AST.Tint::nil) (Some AST.Tint) cc_default).
Definition vmcs_writez_spec_low: compatsem LDATAOps :=
asmsem_withsig vmcs_writez vmcs_writez_spec_low_step (mksignature (AST.Tint::AST.Tint::nil) None cc_default).
Definition vmcs_readz64_spec_low: compatsem LDATAOps :=
asmsem_withsig vmcs_readz64 vmcs_readz64_spec_low_step (mksignature (AST.Tint::nil) (Some AST.Tlong) cc_default).
Definition vmcs_writez64_spec_low: compatsem LDATAOps :=
asmsem_withsig vmcs_writez64 vmcs_writez64_spec_low_step (mksignature (AST.Tint::AST.Tlong::nil) None cc_default).
Definition vmcs_write_ident_spec_low: compatsem LDATAOps :=
asmsem_withsig vmcs_write_ident vmcs_write_ident_spec_low_step (mksignature (AST.Tint::AST.Tint::nil) None cc_default).
Definition rcr0_spec_low: compatsem LDATAOps :=
asmsem_withsig rcr0 rcr0_spec_low_step (mksignature nil (Some AST.Tint) cc_default).
Definition rcr3_spec_low: compatsem LDATAOps :=
asmsem_withsig rcr3 rcr3_spec_low_step (mksignature nil (Some AST.Tint) cc_default).
Definition rcr4_spec_low: compatsem LDATAOps :=
asmsem_withsig rcr4 rcr4_spec_low_step (mksignature nil (Some AST.Tint) cc_default).
Definition rdmsr_spec_low: compatsem LDATAOps :=
asmsem_withsig rdmsr rdmsr_spec_low_step (mksignature (AST.Tint::nil) (Some AST.Tlong) cc_default).
Definition wrmsr_spec_low: compatsem LDATAOps :=
asmsem_withsig wrmsr wrmsr_spec_low_step (mksignature (AST.Tint::AST.Tlong::nil) (Some AST.Tint) cc_default).
Definition vmptr_ld_spec_low: compatsem LDATAOps :=
asmsem_withsig vmptrld vmptr_ld_spec_low_step (mksignature nil None cc_default).
Definition vmx_enable_spec_low: compatsem LDATAOps :=
asmsem_withsig vmx_enable vmx_enable_spec_low_step (mksignature nil None cc_default).
End WITHMEM.
End SPECIFICATION.