Library mcertikos.proc.VEPTInitCode
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 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 VEPTInitCSource.
Require Import VEPTInit.
Require Import VMCSIntroGenSpec.
Module VEPTINITCODE.
Definition v_vmcs_size := 4096.
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 VMCSGETREVID.
Let L: compatlayer (cdata RData) :=
VMCS_LOC ↦ v_vmcs
⊕ get_CPU_ID ↦ gensem get_CPU_ID_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 VMCSGetRevidBody.
Notation v_vmcs_struct_unfolded :=
(Tstruct 5100%positive
(Fcons 5200%positive tuint
(Fcons 5300%positive tuint
(Fcons 5400%positive (Tarray tuchar 4088 noattr) Fnil)))
noattr).
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bvmcs_loc: block).
Hypothesis hvmcs_loc : Genv.find_symbol ge VMCS_LOC = Some bvmcs_loc.
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 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 VEPTInitCSource.
Require Import VEPTInit.
Require Import VMCSIntroGenSpec.
Module VEPTINITCODE.
Definition v_vmcs_size := 4096.
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 VMCSGETREVID.
Let L: compatlayer (cdata RData) :=
VMCS_LOC ↦ v_vmcs
⊕ get_CPU_ID ↦ gensem get_CPU_ID_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 VMCSGetRevidBody.
Notation v_vmcs_struct_unfolded :=
(Tstruct 5100%positive
(Fcons 5200%positive tuint
(Fcons 5300%positive tuint
(Fcons 5400%positive (Tarray tuchar 4088 noattr) Fnil)))
noattr).
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bvmcs_loc: block).
Hypothesis hvmcs_loc : Genv.find_symbol ge VMCS_LOC = Some bvmcs_loc.
get_CPU_ID
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External
(EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma vmcs_get_revid_body_correct:
∀ m d env le v,
env = PTree.empty _ →
Mem.loadv Mint32 ((m, d) : mem)
(Vptr bvmcs_loc (Int.repr (v_vmcs_size × (CPU_ID d) + 0)))
= Some (Vint v) →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_vmcs_get_revid_body E0 le´ (m, d)
(Out_return (Some (Vint v, tint))).
Proof.
intros.
generalize max_unsigned_val; intro muval.
assert (cpu_id_range: 0 ≤ (CPU_ID d) < TOTAL_CPU).
{ inv H1; auto. }
assert (get_CPU_ID_call: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
inv H2; rewrite H3, H4.
rewrite Int.unsigned_repr; [reflexivity | omega]. }
assert (v_vmcs_size_val: sizeof v_vmcs_struct_unfolded = 4096).
{ simpl; unfold align; simpl; auto. }
assert (v_vmcs_size_range : 0 ≤ sizeof v_vmcs_struct_unfolded ≤ Int.max_unsigned).
{ omega. }
unfold f_vmcs_get_revid_body; subst.
unfold t_struct_vmcsStruct; subst.
esplit.
change E0 with (E0 ** E0).
unfold exec_stmt.
econstructor; repeat vcgen.
Qed.
End VMCSGetRevidBody.
Theorem vmcs_get_revid_code_correct:
spec_le
(vmcs_get_revid ↦ vmcs_get_revid_spec_low)
(〚vmcs_get_revid ↦ f_vmcs_get_revid 〛L).
Proof.
fbigstep_pre L.
destruct m´.
simpl in ×.
destruct H1.
assert (match CPU_ID l with
| 0 ⇒ 0
| Z.pos y´ ⇒ Z.pos y´~0~0~0~0~0~0~0~0~0~0~0~0
| Z.neg y´ ⇒ Z.neg y´~0~0~0~0~0~0~0~0~0~0~0~0
end = v_vmcs_size × (CPU_ID l)).
{ unfold v_vmcs_size.
simpl; ring. }
rewrite H3 in H0.
assert (0 ≤ v_vmcs_size × CPU_ID l + 0 ≤ Int.max_unsigned).
{ rewrite muval.
inv hinv.
unfold v_vmcs_size.
omega. }
fbigstep
(vmcs_get_revid_body_correct s (Genv.globalenv p) makeglobalenv
b0 H
b2 Hb2fs Hb2fp
m l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmcs_get_revid) nil
(create_undef_temps
(fn_temps f_vmcs_get_revid)))) muval.
Qed.
End VMCSGETREVID.
Section VMCSSETREVID.
Let L: compatlayer (cdata RData) :=
VMCS_LOC ↦ v_vmcs
⊕ get_CPU_ID ↦ gensem get_CPU_ID_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 VMCSSetRevidBody.
Notation v_vmcs_struct_unfolded :=
(Tstruct 5100%positive
(Fcons 5200%positive tuint
(Fcons 5300%positive tuint
(Fcons 5400%positive (Tarray tuchar 4088 noattr) Fnil)))
noattr).
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bvmcs_loc: block).
Hypothesis hvmcs_loc : Genv.find_symbol ge VMCS_LOC = Some bvmcs_loc.
get_CPU_ID
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External
(EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma vmcs_set_revid_body_correct:
∀ m m´ d env le revid,
env = PTree.empty _ →
PTree.get tid le = Some (Vint revid)->
Mem.store Mint32 ((m, d):mem) bvmcs_loc (v_vmcs_size × (CPU_ID d) + 0) (Vint revid)
= Some (m´, d) →
high_level_invariant d →
kernel_mode d →
∃ le´, exec_stmt ge env le ((m, d): mem) f_vmcs_set_revid_body E0 le´ (m´, d)
Out_normal.
Proof.
intros.
generalize max_unsigned_val; intro muval.
assert (cpu_id_range: 0 ≤ (CPU_ID d) < TOTAL_CPU).
{ inv H2; auto. }
assert (get_CPU_ID_call: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
inv H3; rewrite H4, H5.
rewrite Int.unsigned_repr; [reflexivity | omega]. }
assert (v_vmcs_size_val: sizeof v_vmcs_struct_unfolded = 4096).
{ simpl; unfold align; simpl; auto. }
assert (v_vmcs_size_range : 0 ≤ sizeof v_vmcs_struct_unfolded ≤ Int.max_unsigned).
{ omega. }
unfold f_vmcs_set_revid_body; subst.
unfold t_struct_vmcsStruct; subst.
esplit.
change E0 with (E0 ** E0).
unfold exec_stmt.
econstructor; repeat vcgen.
rewrite v_vmcs_size_val.
fold v_vmcs_size.
replace (0 + v_vmcs_size × CPU_ID d + 0) with (v_vmcs_size × CPU_ID d + 0); try ring.
Opaque v_vmcs_size.
simpl.
Transparent v_vmcs_size.
rewrite Int.unsigned_repr; try (unfold v_vmcs_size; omega).
repeat vcgen.
Qed.
End VMCSSetRevidBody.
Theorem vmcs_set_revid_code_correct:
spec_le
(vmcs_set_revid ↦ vmcs_set_revid_spec_low)
(〚vmcs_set_revid ↦ f_vmcs_set_revid 〛L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
simpl in ×.
destruct H1.
assert (match CPU_ID l with
| 0 ⇒ 0
| Z.pos y´ ⇒ Z.pos y´~0~0~0~0~0~0~0~0~0~0~0~0
| Z.neg y´ ⇒ Z.neg y´~0~0~0~0~0~0~0~0~0~0~0~0
end = v_vmcs_size × (CPU_ID l)).
{ unfold v_vmcs_size.
simpl; ring. }
rewrite H3 in H0.
assert (0 ≤ v_vmcs_size × CPU_ID l + 0 ≤ Int.max_unsigned).
{ rewrite muval.
inv hinv.
unfold v_vmcs_size.
omega. }
destruct H0; subst.
fbigstep
(vmcs_set_revid_body_correct s (Genv.globalenv p) makeglobalenv
b0 H
b2 Hb2fs Hb2fp
m m0 l0 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmcs_set_revid)
(Vint v::nil)
(create_undef_temps
(fn_temps f_vmcs_set_revid)))) muval.
Qed.
End VMCSSETREVID.
Section VMCSGETABRTID.
Notation v_vmcs_struct_unfolded :=
(Tstruct 5100%positive
(Fcons 5200%positive tuint
(Fcons 5300%positive tuint
(Fcons 5400%positive (Tarray tuchar 4088 noattr) Fnil)))
noattr).
Let L: compatlayer (cdata RData) :=
VMCS_LOC ↦ v_vmcs
⊕ get_CPU_ID ↦ gensem get_CPU_ID_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 VMCSGetAbrtIdBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bvmcs_loc: block).
Hypothesis hvmcs_loc : Genv.find_symbol ge VMCS_LOC = Some bvmcs_loc.
get_CPU_ID
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External
(EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma vmcs_get_abrtid_body_correct:
∀ m d env le v,
env = PTree.empty _ →
Mem.loadv Mint32 ((m, d):mem) (Vptr bvmcs_loc (Int.repr (v_vmcs_size × (CPU_ID d) + 4)))
= Some (Vint v) →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_vmcs_get_abrtid_body E0 le´ (m, d)
(Out_return (Some (Vint v, tint))).
Proof.
intros.
generalize max_unsigned_val; intro muval.
assert (cpu_id_range: 0 ≤ (CPU_ID d) < TOTAL_CPU).
{ inv H1; auto. }
assert (get_CPU_ID_call: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
inv H2; rewrite H3, H4.
rewrite Int.unsigned_repr; [reflexivity | omega]. }
assert (v_vmcs_size_val: sizeof v_vmcs_struct_unfolded = 4096).
{ simpl; unfold align; simpl; auto. }
assert (v_vmcs_size_range : 0 ≤ sizeof v_vmcs_struct_unfolded ≤ Int.max_unsigned).
{ omega. }
unfold f_vmcs_get_abrtid_body; subst.
unfold t_struct_vmcsStruct; subst.
esplit.
change E0 with (E0 ** E0).
unfold exec_stmt.
econstructor; repeat vcgen.
Qed.
End VMCSGetAbrtIdBody.
Theorem vmcs_get_abrtid_code_correct:
spec_le
(vmcs_get_abrtid ↦ vmcs_get_abrtid_spec_low)
(〚vmcs_get_abrtid ↦ f_vmcs_get_abrtid 〛L).
Proof.
fbigstep_pre L.
destruct m´.
simpl in ×.
destruct H1.
assert (match CPU_ID l with
| 0 ⇒ 0
| Z.pos y´ ⇒ Z.pos y´~0~0~0~0~0~0~0~0~0~0~0~0
| Z.neg y´ ⇒ Z.neg y´~0~0~0~0~0~0~0~0~0~0~0~0
end = v_vmcs_size × (CPU_ID l)).
{ unfold v_vmcs_size.
simpl; ring. }
rewrite H3 in H0.
assert (0 ≤ v_vmcs_size × CPU_ID l + 4 ≤ Int.max_unsigned).
{ rewrite muval.
inv hinv.
unfold v_vmcs_size.
omega. }
fbigstep
(vmcs_get_abrtid_body_correct s (Genv.globalenv p) makeglobalenv
b0 H
b2 Hb2fs Hb2fp
m l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmcs_get_abrtid) nil
(create_undef_temps
(fn_temps f_vmcs_get_abrtid))))
muval.
Qed.
End VMCSGETABRTID.
Section VMCSSETABRTID.
Notation v_vmcs_struct_unfolded :=
(Tstruct 5100%positive
(Fcons 5200%positive tuint
(Fcons 5300%positive tuint
(Fcons 5400%positive (Tarray tuchar 4088 noattr) Fnil)))
noattr).
Let L: compatlayer (cdata RData) :=
VMCS_LOC ↦ v_vmcs
⊕ get_CPU_ID ↦ gensem get_CPU_ID_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 VMCSSetAbrtidBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bvmcs_loc: block).
Hypothesis hvmcs_loc : Genv.find_symbol ge VMCS_LOC = Some bvmcs_loc.
get_CPU_ID
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External
(EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma vmcs_set_abrtid_body_correct:
∀ m m´ d env le abrtid,
env = PTree.empty _ →
PTree.get tcode le = Some (Vint abrtid)->
Mem.store Mint32 ((m, d):mem) bvmcs_loc (v_vmcs_size × (CPU_ID d) + 4) (Vint abrtid)
= Some (m´, d) →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_vmcs_set_abrtid_body E0 le´ (m´, d)
Out_normal.
Proof.
intros.
generalize max_unsigned_val; intro muval.
assert (cpu_id_range: 0 ≤ (CPU_ID d) < TOTAL_CPU).
{ inv H2; auto. }
assert (get_CPU_ID_call: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
inv H3; rewrite H4, H5.
rewrite Int.unsigned_repr; [reflexivity | omega]. }
assert (v_vmcs_size_val: sizeof v_vmcs_struct_unfolded = 4096).
{ simpl; unfold align; simpl; auto. }
assert (v_vmcs_size_range : 0 ≤ sizeof v_vmcs_struct_unfolded ≤ Int.max_unsigned).
{ omega. }
unfold f_vmcs_set_abrtid_body; subst.
unfold t_struct_vmcsStruct; subst.
esplit.
change E0 with (E0 ** E0).
unfold exec_stmt.
econstructor; repeat vcgen.
intros; subst.
rewrite v_vmcs_size_val.
fold v_vmcs_size.
replace (0 + v_vmcs_size × CPU_ID d + 4) with (v_vmcs_size × CPU_ID d + 4); try ring.
Opaque v_vmcs_size.
simpl.
Transparent v_vmcs_size.
rewrite Int.unsigned_repr; try (unfold v_vmcs_size; omega).
repeat vcgen.
Qed.
End VMCSSetAbrtidBody.
Theorem vmcs_set_abrtid_code_correct:
spec_le
(vmcs_set_abrtid ↦ vmcs_set_abrtid_spec_low) (〚vmcs_set_abrtid ↦ f_vmcs_set_abrtid 〛 L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
simpl in ×.
destruct H1.
assert (match CPU_ID l with
| 0 ⇒ 0
| Z.pos y´ ⇒ Z.pos y´~0~0~0~0~0~0~0~0~0~0~0~0
| Z.neg y´ ⇒ Z.neg y´~0~0~0~0~0~0~0~0~0~0~0~0
end = v_vmcs_size × (CPU_ID l)).
{ unfold v_vmcs_size.
simpl; ring. }
rewrite H3 in H0.
assert (0 ≤ v_vmcs_size × CPU_ID l + 4 ≤ Int.max_unsigned).
{ rewrite muval.
inv hinv.
unfold v_vmcs_size.
omega. }
destruct H0; subst.
fbigstep
(vmcs_set_abrtid_body_correct s (Genv.globalenv p) makeglobalenv
b0 H
b2 Hb2fs Hb2fp
m m0 l0 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmcs_set_abrtid)
(Vint v::nil)
(create_undef_temps
(fn_temps f_vmcs_set_abrtid)))) muval.
Qed.
End VMCSSETABRTID.
End WithPrimitives.
End VEPTINITCODE.