Library mcertikos.proc.VVMCSIntroCode
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import compcert.lib.Integers.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import VMCSInitGenSpec.
Require Import ObjVMCS.
Require Import VVMCSIntroCSource.
Require Import VVMCSIntro.
Hint Resolve Int.unsigned_range_2.
Hint Resolve CLemmas.Z_lor_range_lo.
Hint Resolve Z_lor_range.
Function unsigned64 (x : int64) : Z64 :=
VZ64 (Int64.unsigned x).
Function unpack64 (x: Z64): Z :=
match x with
| VZ64 z ⇒ z
end.
Function repr64 (x : Z64) : int64 :=
Int64.repr (unpack64 x).
Lemma unsigned64_repr: ∀ x: Z64,
0 ≤ unpack64(x) ≤ Int64.max_unsigned →
unsigned64 (repr64 x) = x.
Proof.
unfold repr64, unpack64, unsigned64.
intros. destruct x. rewrite Int64.unsigned_repr; auto.
Qed.
Print Int64.repr_unsigned.
Lemma repr64_unsigned: ∀ x: int64,
repr64 (unsigned64 x) = x.
Proof.
unfold repr64, unpack64, unsigned64.
apply Int64.repr_unsigned.
Qed.
Module VMCSINTROCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Section VMXSETTSCOFFSET.
Let L: compatlayer (cdata RData) :=
vmcs_writez64 ↦ gensem vmcs_writez64_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXSetTscOffsetBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import compcert.lib.Integers.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import VMCSInitGenSpec.
Require Import ObjVMCS.
Require Import VVMCSIntroCSource.
Require Import VVMCSIntro.
Hint Resolve Int.unsigned_range_2.
Hint Resolve CLemmas.Z_lor_range_lo.
Hint Resolve Z_lor_range.
Function unsigned64 (x : int64) : Z64 :=
VZ64 (Int64.unsigned x).
Function unpack64 (x: Z64): Z :=
match x with
| VZ64 z ⇒ z
end.
Function repr64 (x : Z64) : int64 :=
Int64.repr (unpack64 x).
Lemma unsigned64_repr: ∀ x: Z64,
0 ≤ unpack64(x) ≤ Int64.max_unsigned →
unsigned64 (repr64 x) = x.
Proof.
unfold repr64, unpack64, unsigned64.
intros. destruct x. rewrite Int64.unsigned_repr; auto.
Qed.
Print Int64.repr_unsigned.
Lemma repr64_unsigned: ∀ x: int64,
repr64 (unsigned64 x) = x.
Proof.
unfold repr64, unpack64, unsigned64.
apply Int64.repr_unsigned.
Qed.
Module VMCSINTROCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Section VMXSETTSCOFFSET.
Let L: compatlayer (cdata RData) :=
vmcs_writez64 ↦ gensem vmcs_writez64_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXSetTscOffsetBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmcs_writez64
Variable bvmcs_writez64: block.
Hypothesis hvmcs_writez64_1 : Genv.find_symbol ge vmcs_writez64 = Some bvmcs_writez64.
Hypothesis hvmcs_writez64_2 : Genv.find_funct_ptr ge bvmcs_writez64 =
let arg_type := (Tcons tuint (Tcons tulong Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
Some (External (EF_external
vmcs_writez64
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Lemma vmx_set_tsc_offset_body_correct:
∀ m d d´ env le tsc_offset,
env = PTree.empty _ →
PTree.get ttsc_offset le = Some (Vlong tsc_offset) →
vmx_set_tsc_offset_spec (unsigned64 tsc_offset) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_set_tsc_offset_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned64_val; intro muval.
intros; subst.
unfold vmx_set_tsc_offset_body.
functional inversion H1; subst.
esplit.
repeat vcgen; try discriminate.
Qed.
End VMXSetTscOffsetBody.
Theorem vmx_set_tsc_offset__code_correct:
spec_le
(vmx_set_tsc_offset ↦ vmx_set_tsc_offset_spec_low)
(〚vmx_set_tsc_offset ↦ f_vmx_set_tsc_offset 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_set_tsc_offset_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_set_tsc_offset)
(Vlong tsc_offset :: nil)
(create_undef_temps (fn_temps f_vmx_set_tsc_offset)))) muval.
Qed.
End VMXSETTSCOFFSET.
Section VMXGETTSCOFFSET.
Let L: compatlayer (cdata RData) :=
vmcs_readz64 ↦ gensem vmcs_readz64_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXGetTscOffsetBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Hypothesis hvmcs_writez64_1 : Genv.find_symbol ge vmcs_writez64 = Some bvmcs_writez64.
Hypothesis hvmcs_writez64_2 : Genv.find_funct_ptr ge bvmcs_writez64 =
let arg_type := (Tcons tuint (Tcons tulong Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
Some (External (EF_external
vmcs_writez64
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Lemma vmx_set_tsc_offset_body_correct:
∀ m d d´ env le tsc_offset,
env = PTree.empty _ →
PTree.get ttsc_offset le = Some (Vlong tsc_offset) →
vmx_set_tsc_offset_spec (unsigned64 tsc_offset) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_set_tsc_offset_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned64_val; intro muval.
intros; subst.
unfold vmx_set_tsc_offset_body.
functional inversion H1; subst.
esplit.
repeat vcgen; try discriminate.
Qed.
End VMXSetTscOffsetBody.
Theorem vmx_set_tsc_offset__code_correct:
spec_le
(vmx_set_tsc_offset ↦ vmx_set_tsc_offset_spec_low)
(〚vmx_set_tsc_offset ↦ f_vmx_set_tsc_offset 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_set_tsc_offset_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_set_tsc_offset)
(Vlong tsc_offset :: nil)
(create_undef_temps (fn_temps f_vmx_set_tsc_offset)))) muval.
Qed.
End VMXSETTSCOFFSET.
Section VMXGETTSCOFFSET.
Let L: compatlayer (cdata RData) :=
vmcs_readz64 ↦ gensem vmcs_readz64_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXGetTscOffsetBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmcs_readz64
Variable bvmcs_readz64: block.
Hypothesis hvmcs_readz64_1 : Genv.find_symbol ge vmcs_readz64 = Some bvmcs_readz64.
Hypothesis hvmcs_readz64_2 : Genv.find_funct_ptr ge bvmcs_readz64 =
let arg_type := (Tcons tuint Tnil) in
let ret_type := tulong in
let cal_conv := cc_default in
Some (External (EF_external
vmcs_readz64
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Lemma vmx_get_tsc_offset_body_correct:
∀ m d env le v,
env = PTree.empty _ →
vmx_get_tsc_offset_spec d = Some (unsigned64 v) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_tsc_offset_body E0 le´ (m, d)
(Out_return (Some (Vlong v, tulong))).
Proof.
generalize max_unsigned64_val; intro muval.
intros; subst.
unfold vmx_get_tsc_offset_body.
functional inversion H0; subst.
esplit.
repeat vcgen; try discriminate.
unfold vmcs_readz64_spec.
rewrite H3, H2, H1, H4, H5, H6, H7; simpl.
rewrite H. reflexivity.
Qed.
End VMXGetTscOffsetBody.
Theorem vmx_get_tsc_offset__code_correct:
spec_le
(vmx_get_tsc_offset ↦ vmx_get_tsc_offset_spec_low)
(〚vmx_get_tsc_offset ↦ f_vmx_get_tsc_offset 〛L).
Proof.
fbigstep_pre L.
fbigstep (vmx_get_tsc_offset_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
m´0 labd (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_get_tsc_offset)
(nil)
(create_undef_temps (fn_temps f_vmx_get_tsc_offset)))) muval.
Qed.
End VMXGETTSCOFFSET.
Section VMXGETEXITFAULTADDR.
Let L: compatlayer (cdata RData) :=
vmcs_readz ↦ gensem vmcs_readz_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXGetExitFaultAddrBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Hypothesis hvmcs_readz64_1 : Genv.find_symbol ge vmcs_readz64 = Some bvmcs_readz64.
Hypothesis hvmcs_readz64_2 : Genv.find_funct_ptr ge bvmcs_readz64 =
let arg_type := (Tcons tuint Tnil) in
let ret_type := tulong in
let cal_conv := cc_default in
Some (External (EF_external
vmcs_readz64
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Lemma vmx_get_tsc_offset_body_correct:
∀ m d env le v,
env = PTree.empty _ →
vmx_get_tsc_offset_spec d = Some (unsigned64 v) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_tsc_offset_body E0 le´ (m, d)
(Out_return (Some (Vlong v, tulong))).
Proof.
generalize max_unsigned64_val; intro muval.
intros; subst.
unfold vmx_get_tsc_offset_body.
functional inversion H0; subst.
esplit.
repeat vcgen; try discriminate.
unfold vmcs_readz64_spec.
rewrite H3, H2, H1, H4, H5, H6, H7; simpl.
rewrite H. reflexivity.
Qed.
End VMXGetTscOffsetBody.
Theorem vmx_get_tsc_offset__code_correct:
spec_le
(vmx_get_tsc_offset ↦ vmx_get_tsc_offset_spec_low)
(〚vmx_get_tsc_offset ↦ f_vmx_get_tsc_offset 〛L).
Proof.
fbigstep_pre L.
fbigstep (vmx_get_tsc_offset_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
m´0 labd (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_get_tsc_offset)
(nil)
(create_undef_temps (fn_temps f_vmx_get_tsc_offset)))) muval.
Qed.
End VMXGETTSCOFFSET.
Section VMXGETEXITFAULTADDR.
Let L: compatlayer (cdata RData) :=
vmcs_readz ↦ gensem vmcs_readz_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXGetExitFaultAddrBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmcs_readz
Variable bvmcs_readz: block.
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz =
Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_get_exit_fault_addr_body_correct:
∀ m d env le v,
env = PTree.empty _ →
vmx_get_exit_fault_addr_spec d = Some (Int.unsigned v) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_exit_fault_addr_body E0 le´ (m, d)
(Out_return (Some (Vint v, tuint))).
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
unfold vmx_get_exit_fault_addr_body.
functional inversion H0; subst.
esplit.
repeat vcgen; try discriminate.
unfold vmcs_readz_spec.
rewrite H3, H2, H1, H4, H5.
simpl.
rewrite H6.
rewrite H.
reflexivity.
Qed.
End VMXGetExitFaultAddrBody.
Theorem vmx_get_exit_fault_addr__code_correct:
spec_le
( vmx_get_exit_fault_addr ↦ vmx_get_exit_fault_addr_spec_low )
(〚 vmx_get_exit_fault_addr ↦ f_vmx_get_exit_fault_addr〛L).
Proof.
fbigstep_pre L.
fbigstep (vmx_get_exit_fault_addr_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
m´0 labd (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_get_exit_fault_addr)
(nil)
(create_undef_temps (fn_temps f_vmx_get_exit_fault_addr)))) muval.
Qed.
End VMXGETEXITFAULTADDR.
Section VMXGETEXITREASON.
Let L: compatlayer (cdata RData) :=
vmcs_readz ↦ gensem vmcs_readz_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXGetExitReasonBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz =
Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_get_exit_fault_addr_body_correct:
∀ m d env le v,
env = PTree.empty _ →
vmx_get_exit_fault_addr_spec d = Some (Int.unsigned v) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_exit_fault_addr_body E0 le´ (m, d)
(Out_return (Some (Vint v, tuint))).
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
unfold vmx_get_exit_fault_addr_body.
functional inversion H0; subst.
esplit.
repeat vcgen; try discriminate.
unfold vmcs_readz_spec.
rewrite H3, H2, H1, H4, H5.
simpl.
rewrite H6.
rewrite H.
reflexivity.
Qed.
End VMXGetExitFaultAddrBody.
Theorem vmx_get_exit_fault_addr__code_correct:
spec_le
( vmx_get_exit_fault_addr ↦ vmx_get_exit_fault_addr_spec_low )
(〚 vmx_get_exit_fault_addr ↦ f_vmx_get_exit_fault_addr〛L).
Proof.
fbigstep_pre L.
fbigstep (vmx_get_exit_fault_addr_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
m´0 labd (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_get_exit_fault_addr)
(nil)
(create_undef_temps (fn_temps f_vmx_get_exit_fault_addr)))) muval.
Qed.
End VMXGETEXITFAULTADDR.
Section VMXGETEXITREASON.
Let L: compatlayer (cdata RData) :=
vmcs_readz ↦ gensem vmcs_readz_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXGetExitReasonBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmcs_readz
Variable bvmcs_readz: block.
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz =
Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_get_exit_reason_body_correct:
∀ m d env le v,
env = PTree.empty _ →
vmx_get_exit_reason_spec d = Some (Int.unsigned v) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_exit_reason_body E0 le´ (m, d)
(Out_return (Some (Vint v, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
unfold vmx_get_exit_reason_body.
functional inversion H0; subst.
esplit.
repeat vcgen; try discriminate.
- Case ("read 17410").
unfold vmcs_readz_spec.
rewrite H1, H3, H2, H4, H5, H6; simpl.
discharge_cmp.
- discharge_cmp.
rewrite <- Int.repr_unsigned with v.
rewrite <- H.
reflexivity.
Qed.
End VMXGetExitReasonBody.
Theorem vmx_get_exit_reason__code_correct:
spec_le
(vmx_get_exit_reason ↦ vmx_get_exit_reason_spec_low)
(〚vmx_get_exit_reason ↦ f_vmx_get_exit_reason 〛L).
Proof.
fbigstep_pre L.
fbigstep (vmx_get_exit_reason_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
m´0 labd (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_get_exit_reason)
(nil)
(create_undef_temps (fn_temps f_vmx_get_exit_reason)))) muval.
Qed.
End VMXGETEXITREASON.
Section VMXCHECKINTSHADOW.
Let L: compatlayer (cdata RData) :=
vmcs_readz ↦ gensem vmcs_readz_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXCheckIntShadowBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz =
Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_get_exit_reason_body_correct:
∀ m d env le v,
env = PTree.empty _ →
vmx_get_exit_reason_spec d = Some (Int.unsigned v) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_exit_reason_body E0 le´ (m, d)
(Out_return (Some (Vint v, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
unfold vmx_get_exit_reason_body.
functional inversion H0; subst.
esplit.
repeat vcgen; try discriminate.
- Case ("read 17410").
unfold vmcs_readz_spec.
rewrite H1, H3, H2, H4, H5, H6; simpl.
discharge_cmp.
- discharge_cmp.
rewrite <- Int.repr_unsigned with v.
rewrite <- H.
reflexivity.
Qed.
End VMXGetExitReasonBody.
Theorem vmx_get_exit_reason__code_correct:
spec_le
(vmx_get_exit_reason ↦ vmx_get_exit_reason_spec_low)
(〚vmx_get_exit_reason ↦ f_vmx_get_exit_reason 〛L).
Proof.
fbigstep_pre L.
fbigstep (vmx_get_exit_reason_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
m´0 labd (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_get_exit_reason)
(nil)
(create_undef_temps (fn_temps f_vmx_get_exit_reason)))) muval.
Qed.
End VMXGETEXITREASON.
Section VMXCHECKINTSHADOW.
Let L: compatlayer (cdata RData) :=
vmcs_readz ↦ gensem vmcs_readz_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXCheckIntShadowBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmcs_readz
Variable bvmcs_readz: block.
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz =
Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_check_int_shadow_body_correct:
∀ m d env le v,
env = PTree.empty _ →
vmx_check_int_shadow_spec d = Some (Int.unsigned v) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_check_int_shadow_body E0 le´ (m, d)
(Out_return (Some (Vint v, tint))).
Proof.
generalize max_unsigned_val; intro muval.
assert (Hone_or_two: Z.lor 1 2 = 3). reflexivity.
intros; subst.
unfold vmx_check_int_shadow_body.
functional inversion H0; subst.
- Case ("does not have shadowed int").
esplit.
destruct (zeq (Z.land (Int.unsigned ctrls) 3) 0); try discriminate H6.
+ repeat vcgenfull; try discriminate.
SCase ("read 18468").
× unfold vmcs_readz_spec.
rewrite H1, H3, H2, H4, H5, H6; simpl.
discharge_cmp.
× rewrite Hone_or_two; rewrite e; repeat vcgen.
× rewrite H; repeat vcgen.
+ rewrite H; repeat vcgen.
- Case ("has shadowed int").
esplit.
destruct (zeq (Z.land (Int.unsigned ctrls) 3) 0); try discriminate H6.
+ repeat vcgenfull; try discriminate.
+ repeat vcgen.
unfold vmcs_readz_spec.
rewrite H1, H3, H2, H4, H5, H6; simpl.
discharge_cmp.
× rewrite Hone_or_two; discharge_cmp; repeat vcgen.
× unfold Int.one; rewrite H; repeat vcgen.
Qed.
End VMXCheckIntShadowBody.
Theorem vmx_check_int_shadow__code_correct:
spec_le
(vmx_check_int_shadow ↦ vmx_check_int_shadow_spec_low)
(〚vmx_check_int_shadow ↦ f_vmx_check_int_shadow 〛L).
Proof.
fbigstep_pre L.
fbigstep (vmx_check_int_shadow_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
m´0 labd (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_check_int_shadow)
(nil)
(create_undef_temps (fn_temps f_vmx_check_int_shadow)))) muval.
Qed.
End VMXCHECKINTSHADOW.
Section VMXCHECKPENDINGEVENT.
Let L: compatlayer (cdata RData) :=
vmcs_readz ↦ gensem vmcs_readz_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXCheckPendingEventBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz =
Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_check_int_shadow_body_correct:
∀ m d env le v,
env = PTree.empty _ →
vmx_check_int_shadow_spec d = Some (Int.unsigned v) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_check_int_shadow_body E0 le´ (m, d)
(Out_return (Some (Vint v, tint))).
Proof.
generalize max_unsigned_val; intro muval.
assert (Hone_or_two: Z.lor 1 2 = 3). reflexivity.
intros; subst.
unfold vmx_check_int_shadow_body.
functional inversion H0; subst.
- Case ("does not have shadowed int").
esplit.
destruct (zeq (Z.land (Int.unsigned ctrls) 3) 0); try discriminate H6.
+ repeat vcgenfull; try discriminate.
SCase ("read 18468").
× unfold vmcs_readz_spec.
rewrite H1, H3, H2, H4, H5, H6; simpl.
discharge_cmp.
× rewrite Hone_or_two; rewrite e; repeat vcgen.
× rewrite H; repeat vcgen.
+ rewrite H; repeat vcgen.
- Case ("has shadowed int").
esplit.
destruct (zeq (Z.land (Int.unsigned ctrls) 3) 0); try discriminate H6.
+ repeat vcgenfull; try discriminate.
+ repeat vcgen.
unfold vmcs_readz_spec.
rewrite H1, H3, H2, H4, H5, H6; simpl.
discharge_cmp.
× rewrite Hone_or_two; discharge_cmp; repeat vcgen.
× unfold Int.one; rewrite H; repeat vcgen.
Qed.
End VMXCheckIntShadowBody.
Theorem vmx_check_int_shadow__code_correct:
spec_le
(vmx_check_int_shadow ↦ vmx_check_int_shadow_spec_low)
(〚vmx_check_int_shadow ↦ f_vmx_check_int_shadow 〛L).
Proof.
fbigstep_pre L.
fbigstep (vmx_check_int_shadow_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
m´0 labd (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_check_int_shadow)
(nil)
(create_undef_temps (fn_temps f_vmx_check_int_shadow)))) muval.
Qed.
End VMXCHECKINTSHADOW.
Section VMXCHECKPENDINGEVENT.
Let L: compatlayer (cdata RData) :=
vmcs_readz ↦ gensem vmcs_readz_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXCheckPendingEventBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmcs_readz
Variable bvmcs_readz: block.
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz =
Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_check_pending_event_body_correct:
∀ m d env le v,
env = PTree.empty _ →
vmx_check_pending_event_spec d = Some (Int.unsigned v) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_check_pending_event_body E0 le´ (m, d)
(Out_return (Some (Vint v, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
unfold vmx_check_pending_event_body.
functional inversion H0; subst.
- Case ("does not have pending event").
esplit.
destruct (zeq (Z.land (Int.unsigned ctrls) 2147483648) 0); try discriminate H7.
+ SCase ("read 16406").
repeat vcgen; try discriminate.
unfold vmcs_readz_spec.
rewrite H1, H3, H2, H4, H5, H6; simpl.
discharge_cmp.
× rewrite _x0; repeat vcgen.
× rewrite H; repeat vcgen.
- Case ("has pending event").
esplit.
destruct (zeq (Z.land (Int.unsigned ctrls) 2147483648) 0); try discriminate H7.
SCase ("read 16406").
repeat vcgen; inv H7.
unfold vmcs_readz_spec.
rewrite H1, H3, H2, H4, H5, H6; simpl.
discharge_cmp.
simpl.
assert (0 ≤ Z.land (Int.unsigned ctrls) 2147483648 ≤ Int.max_unsigned).
{ eapply Z_land_range; try auto.
rewrite muval; omega. }
rewrite <- Int.unsigned_repr with (z := 0) in n; try omega.
rewrite <- Int.unsigned_repr with (z := Z.land (Int.unsigned ctrls) 2147483648) in n; auto.
assert (Int.repr (Z.land (Int.unsigned ctrls) 2147483648) ≠ (Int.repr 0)).
{ unfold not; intros.
elim n.
rewrite <- H8; auto. }
eapply Int.eq_false in H8.
unfold Int.zero; rewrite H8; simpl.
+ repeat vcgen.
+ rewrite H; repeat vcgen.
Qed.
End VMXCheckPendingEventBody.
Theorem vmx_check_pending_event__code_correct:
spec_le
(vmx_check_pending_event ↦ vmx_check_pending_event_spec_low)
(〚vmx_check_pending_event ↦ f_vmx_check_pending_event 〛L).
Proof.
fbigstep_pre L.
fbigstep (vmx_check_pending_event_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
m´0 labd (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_check_pending_event)
(nil)
(create_undef_temps (fn_temps f_vmx_check_pending_event)))) muval.
Qed.
End VMXCHECKPENDINGEVENT.
Section VMXINJECTEVENT.
Let L: compatlayer (cdata RData) :=
vmcs_readz ↦ gensem vmcs_readz_spec
⊕ vmcs_writez ↦ gensem vmcs_writez_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXInjectEventBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz =
Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_check_pending_event_body_correct:
∀ m d env le v,
env = PTree.empty _ →
vmx_check_pending_event_spec d = Some (Int.unsigned v) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_check_pending_event_body E0 le´ (m, d)
(Out_return (Some (Vint v, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
unfold vmx_check_pending_event_body.
functional inversion H0; subst.
- Case ("does not have pending event").
esplit.
destruct (zeq (Z.land (Int.unsigned ctrls) 2147483648) 0); try discriminate H7.
+ SCase ("read 16406").
repeat vcgen; try discriminate.
unfold vmcs_readz_spec.
rewrite H1, H3, H2, H4, H5, H6; simpl.
discharge_cmp.
× rewrite _x0; repeat vcgen.
× rewrite H; repeat vcgen.
- Case ("has pending event").
esplit.
destruct (zeq (Z.land (Int.unsigned ctrls) 2147483648) 0); try discriminate H7.
SCase ("read 16406").
repeat vcgen; inv H7.
unfold vmcs_readz_spec.
rewrite H1, H3, H2, H4, H5, H6; simpl.
discharge_cmp.
simpl.
assert (0 ≤ Z.land (Int.unsigned ctrls) 2147483648 ≤ Int.max_unsigned).
{ eapply Z_land_range; try auto.
rewrite muval; omega. }
rewrite <- Int.unsigned_repr with (z := 0) in n; try omega.
rewrite <- Int.unsigned_repr with (z := Z.land (Int.unsigned ctrls) 2147483648) in n; auto.
assert (Int.repr (Z.land (Int.unsigned ctrls) 2147483648) ≠ (Int.repr 0)).
{ unfold not; intros.
elim n.
rewrite <- H8; auto. }
eapply Int.eq_false in H8.
unfold Int.zero; rewrite H8; simpl.
+ repeat vcgen.
+ rewrite H; repeat vcgen.
Qed.
End VMXCheckPendingEventBody.
Theorem vmx_check_pending_event__code_correct:
spec_le
(vmx_check_pending_event ↦ vmx_check_pending_event_spec_low)
(〚vmx_check_pending_event ↦ f_vmx_check_pending_event 〛L).
Proof.
fbigstep_pre L.
fbigstep (vmx_check_pending_event_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
m´0 labd (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_check_pending_event)
(nil)
(create_undef_temps (fn_temps f_vmx_check_pending_event)))) muval.
Qed.
End VMXCHECKPENDINGEVENT.
Section VMXINJECTEVENT.
Let L: compatlayer (cdata RData) :=
vmcs_readz ↦ gensem vmcs_readz_spec
⊕ vmcs_writez ↦ gensem vmcs_writez_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXInjectEventBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmcs_readz
Variable bvmcs_readz: block.
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz =
Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz =
Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
vmcs_writez
Variable bvmcs_writez: block.
Hypothesis hvmcs_writez1 : Genv.find_symbol ge vmcs_writez = Some bvmcs_writez.
Hypothesis hvmcs_writez2 : Genv.find_funct_ptr ge bvmcs_writez =
let arg_type := (Tcons tint (Tcons tint Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
Some (External (EF_external vmcs_writez
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Lemma vmx_inject_event_body_correct:
∀ m d d´ env le type vector errcode ev,
env = PTree.empty _ →
PTree.get _type le = Some (Vint type) →
PTree.get _vector le = Some (Vint vector) →
PTree.get _errcode le = Some (Vint errcode) →
PTree.get _ev le = Some (Vint ev) →
vmx_inject_event_spec (Int.unsigned type) (Int.unsigned vector)
(Int.unsigned errcode) (Int.unsigned ev) d
= Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_inject_event_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
unfold vmx_inject_event_body.
functional inversion H4; subst.
- Case ("intr_info & VMCS_INTERRUPTION_INFO_VALID == 0 && ev == 1").
destruct (zeq (Z.land i 2147483648) 0); try discriminate H11.
destruct (zeq (Int.unsigned ev) 1); try discriminate H12.
unfold i in ×.
SCase ("assertion: get vmcs VMCS_ENTRY_INTR_INFO").
assert (read16406 : match vmcs_readz_spec 16406 d with
| Some a ⇒ ret (d, a)
| None ⇒ None
end =
ret (d, Int.unsigned (Int.repr (Int.unsigned (Int.repr (Int.unsigned intr_info)))))).
{ unfold vmcs_readz_spec.
rewrite H5, H7, H6, H8, H9, H10; simpl.
repeat zdestruct; discharge_cmp. }
SSCase ("assertion: set vmcs VMCS_ENTRY_INTR_INFO").
assert (write16408 : vmcs_writez_spec 16408 (Int.unsigned errcode)
d {vmcs : ZMap.set
(CPU_ID d)
(VMCSValid
revid abrtid
(ZMap.set
16406
(Vint (Int.repr (Z.lor (Z.lor (Z.lor 2147483648
(Int.unsigned type))
(Int.unsigned vector))
2048))) d0)) (vmcs d)} =
ret d {vmcs : ZMap.set (CPU_ID d) (VMCSValid revid abrtid d2) (vmcs d)}).
{ unfold vmcs_writez_spec.
unfold d2, d1, i3, i2, i1 in ×.
repeat zdestruct.
discharge_cmp.
rewrite H5, H7, H6, H8.
rewrite ZMap.gss.
rewrite ZMap.set2.
assert (vmcs_double_update:
∀ d vmcs1 vmcs2,
d {vmcs: vmcs1} {vmcs: vmcs2} = d {vmcs: vmcs2}).
{ unfold update_vmcs; simpl; auto. }
rewrite vmcs_double_update.
reflexivity. }
esplit.
repeat vcgenfull; try discriminate;
repeat (try apply Z_lor_range; try vcgen; try omega).
- Case ("intr_info & VMCS_INTERRUPTION_INFO_VALID == 0 && ev != 1").
destruct (zeq (Z.land i 2147483648) 0); try discriminate H11.
destruct (zeq (Int.unsigned ev) 1); try discriminate H12.
unfold i in ×.
SCase ("assertion: get vmcs VMCS_ENTRY_INTR_INFO").
assert (read16406 : match vmcs_readz_spec 16406 d with
| Some a ⇒ ret (d, a)
| None ⇒ None
end =
ret (d, Int.unsigned (Int.repr (Int.unsigned (Int.repr (Int.unsigned intr_info)))))).
{ unfold vmcs_readz_spec.
rewrite H5, H7, H6, H8, H9, H10; simpl.
repeat zdestruct; discharge_cmp. }
esplit.
repeat vcgenfull; try discriminate;
repeat (try apply Z_lor_range; try vcgen; try omega).
- Case ("assertion: another get vmcs VMCS_ENTRY_INTR_INFO").
assert ( read16406´neq0 : match vmcs_readz_spec 16406 d´ with
| Some a ⇒ ret (d´, a)
| None ⇒ None
end = ret (d´, Int.unsigned intr_info)).
{ unfold vmcs_readz_spec.
rewrite H5, H7, H6, H8, H9, H10; simpl.
reflexivity. }
SCase ("intr_info & VMCS_INTERRUPTION_INFO_VALID != 0").
unfold i in ×.
unfold is_invalid in ×.
esplit.
repeat vcgenfull; try discriminate;
repeat (try apply Z_lor_range; try vcgen; try omega).
Qed.
End VMXInjectEventBody.
Theorem vmx_inject_event__code_correct:
spec_le
(vmx_inject_event ↦ vmx_inject_event_spec_low)
(〚vmx_inject_event ↦ f_vmx_inject_event 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
Require Import TacticsForTesting.
fbigsteptest (vmx_inject_event_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_inject_event)
(Vint type :: Vint vector :: Vint errcode :: Vint ev :: nil)
(create_undef_temps (fn_temps f_vmx_inject_event)))) muval;
try discriminate.
intro tmpH; destruct tmpH as [le´ stmt].
repeat fbigstep_post.
Qed.
End VMXINJECTEVENT.
Section VMXSETINTERCEPTINTWIN.
Let L: compatlayer (cdata RData) :=
vmcs_readz ↦ gensem vmcs_readz_spec
⊕ vmcs_writez ↦ gensem vmcs_writez_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXSetInterceptionIntwinBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Hypothesis hvmcs_writez1 : Genv.find_symbol ge vmcs_writez = Some bvmcs_writez.
Hypothesis hvmcs_writez2 : Genv.find_funct_ptr ge bvmcs_writez =
let arg_type := (Tcons tint (Tcons tint Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
Some (External (EF_external vmcs_writez
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Lemma vmx_inject_event_body_correct:
∀ m d d´ env le type vector errcode ev,
env = PTree.empty _ →
PTree.get _type le = Some (Vint type) →
PTree.get _vector le = Some (Vint vector) →
PTree.get _errcode le = Some (Vint errcode) →
PTree.get _ev le = Some (Vint ev) →
vmx_inject_event_spec (Int.unsigned type) (Int.unsigned vector)
(Int.unsigned errcode) (Int.unsigned ev) d
= Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_inject_event_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
unfold vmx_inject_event_body.
functional inversion H4; subst.
- Case ("intr_info & VMCS_INTERRUPTION_INFO_VALID == 0 && ev == 1").
destruct (zeq (Z.land i 2147483648) 0); try discriminate H11.
destruct (zeq (Int.unsigned ev) 1); try discriminate H12.
unfold i in ×.
SCase ("assertion: get vmcs VMCS_ENTRY_INTR_INFO").
assert (read16406 : match vmcs_readz_spec 16406 d with
| Some a ⇒ ret (d, a)
| None ⇒ None
end =
ret (d, Int.unsigned (Int.repr (Int.unsigned (Int.repr (Int.unsigned intr_info)))))).
{ unfold vmcs_readz_spec.
rewrite H5, H7, H6, H8, H9, H10; simpl.
repeat zdestruct; discharge_cmp. }
SSCase ("assertion: set vmcs VMCS_ENTRY_INTR_INFO").
assert (write16408 : vmcs_writez_spec 16408 (Int.unsigned errcode)
d {vmcs : ZMap.set
(CPU_ID d)
(VMCSValid
revid abrtid
(ZMap.set
16406
(Vint (Int.repr (Z.lor (Z.lor (Z.lor 2147483648
(Int.unsigned type))
(Int.unsigned vector))
2048))) d0)) (vmcs d)} =
ret d {vmcs : ZMap.set (CPU_ID d) (VMCSValid revid abrtid d2) (vmcs d)}).
{ unfold vmcs_writez_spec.
unfold d2, d1, i3, i2, i1 in ×.
repeat zdestruct.
discharge_cmp.
rewrite H5, H7, H6, H8.
rewrite ZMap.gss.
rewrite ZMap.set2.
assert (vmcs_double_update:
∀ d vmcs1 vmcs2,
d {vmcs: vmcs1} {vmcs: vmcs2} = d {vmcs: vmcs2}).
{ unfold update_vmcs; simpl; auto. }
rewrite vmcs_double_update.
reflexivity. }
esplit.
repeat vcgenfull; try discriminate;
repeat (try apply Z_lor_range; try vcgen; try omega).
- Case ("intr_info & VMCS_INTERRUPTION_INFO_VALID == 0 && ev != 1").
destruct (zeq (Z.land i 2147483648) 0); try discriminate H11.
destruct (zeq (Int.unsigned ev) 1); try discriminate H12.
unfold i in ×.
SCase ("assertion: get vmcs VMCS_ENTRY_INTR_INFO").
assert (read16406 : match vmcs_readz_spec 16406 d with
| Some a ⇒ ret (d, a)
| None ⇒ None
end =
ret (d, Int.unsigned (Int.repr (Int.unsigned (Int.repr (Int.unsigned intr_info)))))).
{ unfold vmcs_readz_spec.
rewrite H5, H7, H6, H8, H9, H10; simpl.
repeat zdestruct; discharge_cmp. }
esplit.
repeat vcgenfull; try discriminate;
repeat (try apply Z_lor_range; try vcgen; try omega).
- Case ("assertion: another get vmcs VMCS_ENTRY_INTR_INFO").
assert ( read16406´neq0 : match vmcs_readz_spec 16406 d´ with
| Some a ⇒ ret (d´, a)
| None ⇒ None
end = ret (d´, Int.unsigned intr_info)).
{ unfold vmcs_readz_spec.
rewrite H5, H7, H6, H8, H9, H10; simpl.
reflexivity. }
SCase ("intr_info & VMCS_INTERRUPTION_INFO_VALID != 0").
unfold i in ×.
unfold is_invalid in ×.
esplit.
repeat vcgenfull; try discriminate;
repeat (try apply Z_lor_range; try vcgen; try omega).
Qed.
End VMXInjectEventBody.
Theorem vmx_inject_event__code_correct:
spec_le
(vmx_inject_event ↦ vmx_inject_event_spec_low)
(〚vmx_inject_event ↦ f_vmx_inject_event 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
Require Import TacticsForTesting.
fbigsteptest (vmx_inject_event_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_inject_event)
(Vint type :: Vint vector :: Vint errcode :: Vint ev :: nil)
(create_undef_temps (fn_temps f_vmx_inject_event)))) muval;
try discriminate.
intro tmpH; destruct tmpH as [le´ stmt].
repeat fbigstep_post.
Qed.
End VMXINJECTEVENT.
Section VMXSETINTERCEPTINTWIN.
Let L: compatlayer (cdata RData) :=
vmcs_readz ↦ gensem vmcs_readz_spec
⊕ vmcs_writez ↦ gensem vmcs_writez_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXSetInterceptionIntwinBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmcs_readz
Variable bvmcs_readz: block.
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz =
Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz =
Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
vmcs_writez
Variable bvmcs_writez: block.
Hypothesis hvmcs_writez1 : Genv.find_symbol ge vmcs_writez = Some bvmcs_writez.
Hypothesis hvmcs_writez2 : Genv.find_funct_ptr ge bvmcs_writez =
let arg_type := (Tcons tint (Tcons tint Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
Some (External (EF_external vmcs_writez
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Lemma vmx_set_intercept_intwin_body_correct:
∀ m d d´ env le enable,
env = PTree.empty _ →
PTree.get tenable le = Some (Vint enable) →
vmx_set_intercept_intwin_spec (Int.unsigned enable) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_set_intercept_intwin_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros. subst.
unfold vmx_set_intercept_intwin_body.
functional inversion H1; subst.
- Case ("enable == 1").
destruct (zeq (Int.unsigned enable) 1); try discriminate H8.
esplit.
repeat vcgen; try discriminate.
+ SCase ("get value").
unfold vmcs_readz_spec.
rewrite H2, H4, H3, H5, H6, H7; simpl.
repeat zdestruct.
discharge_cmp.
+ SCase ("set value").
unfold vmcs_writez_spec.
rewrite H2, H4, H3, H5, H6; simpl.
repeat zdestruct.
discharge_cmp.
+ SCase ("arithmetic").
apply Z_lor_range. rewrite muval. apply Int.unsigned_range_2. omega.
- Case ("enable != 1").
destruct (zeq (Int.unsigned enable) 1); try discriminate H8.
esplit.
repeat vcgen; try discriminate.
+ SCase ("get value").
unfold vmcs_readz_spec.
rewrite H2, H4, H3, H5, H6, H7; simpl.
repeat zdestruct.
discharge_cmp.
+ SCase ("set value").
rewrite Int.unsigned_not, Int.unsigned_repr, muval; simpl.
unfold vmcs_writez_spec.
rewrite H2, H4, H3, H5, H6; simpl.
repeat zdestruct.
discharge_cmp.
omega.
+ SCase ("arithmetic").
rewrite Int.unsigned_not, Int.unsigned_repr, muval; simpl; try omega.
apply Z_land_range; try omega.
apply Int.unsigned_range_2.
Qed.
End VMXSetInterceptionIntwinBody.
Theorem vmx_set_intercept_intwin__code_correct:
spec_le
(vmx_set_intercept_intwin ↦ vmx_set_intercept_intwin_spec_low)
(〚vmx_set_intercept_intwin ↦ f_vmx_set_intercept_intwin 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_set_intercept_intwin_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_set_intercept_intwin)
(Vint enable :: nil)
(create_undef_temps (fn_temps f_vmx_set_intercept_intwin)))) muval.
Qed.
End VMXSETINTERCEPTINTWIN.
End WithPrimitives.
End VMCSINTROCODE.
Hypothesis hvmcs_writez1 : Genv.find_symbol ge vmcs_writez = Some bvmcs_writez.
Hypothesis hvmcs_writez2 : Genv.find_funct_ptr ge bvmcs_writez =
let arg_type := (Tcons tint (Tcons tint Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
Some (External (EF_external vmcs_writez
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Lemma vmx_set_intercept_intwin_body_correct:
∀ m d d´ env le enable,
env = PTree.empty _ →
PTree.get tenable le = Some (Vint enable) →
vmx_set_intercept_intwin_spec (Int.unsigned enable) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_set_intercept_intwin_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros. subst.
unfold vmx_set_intercept_intwin_body.
functional inversion H1; subst.
- Case ("enable == 1").
destruct (zeq (Int.unsigned enable) 1); try discriminate H8.
esplit.
repeat vcgen; try discriminate.
+ SCase ("get value").
unfold vmcs_readz_spec.
rewrite H2, H4, H3, H5, H6, H7; simpl.
repeat zdestruct.
discharge_cmp.
+ SCase ("set value").
unfold vmcs_writez_spec.
rewrite H2, H4, H3, H5, H6; simpl.
repeat zdestruct.
discharge_cmp.
+ SCase ("arithmetic").
apply Z_lor_range. rewrite muval. apply Int.unsigned_range_2. omega.
- Case ("enable != 1").
destruct (zeq (Int.unsigned enable) 1); try discriminate H8.
esplit.
repeat vcgen; try discriminate.
+ SCase ("get value").
unfold vmcs_readz_spec.
rewrite H2, H4, H3, H5, H6, H7; simpl.
repeat zdestruct.
discharge_cmp.
+ SCase ("set value").
rewrite Int.unsigned_not, Int.unsigned_repr, muval; simpl.
unfold vmcs_writez_spec.
rewrite H2, H4, H3, H5, H6; simpl.
repeat zdestruct.
discharge_cmp.
omega.
+ SCase ("arithmetic").
rewrite Int.unsigned_not, Int.unsigned_repr, muval; simpl; try omega.
apply Z_land_range; try omega.
apply Int.unsigned_range_2.
Qed.
End VMXSetInterceptionIntwinBody.
Theorem vmx_set_intercept_intwin__code_correct:
spec_le
(vmx_set_intercept_intwin ↦ vmx_set_intercept_intwin_spec_low)
(〚vmx_set_intercept_intwin ↦ f_vmx_set_intercept_intwin 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_set_intercept_intwin_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_set_intercept_intwin)
(Vint enable :: nil)
(create_undef_temps (fn_temps f_vmx_set_intercept_intwin)))) muval.
Qed.
End VMXSETINTERCEPTINTWIN.
End WithPrimitives.
End VMCSINTROCODE.