Library mcertikos.proc.PProcCode
Require Import TacticsForTesting.
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 EPTIntroGenSpec.
Require Import PProc.
Require Import AbstractDataType.
Require Import PProcCSource.
Require Import GlobalOracleProp.
Module PPROCCODE.
Definition EptSize := 8413184.
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.
Lemma tptrsize: sizeof (Tpointer tchar noattr) = 4.
Proof. reflexivity. Qed.
Lemma tulongsize: sizeof tulong = 8.
Proof. reflexivity. Qed.
Lemma teptstructsize: sizeof t_struct_ept = 8413184.
Proof. reflexivity. Qed.
Section SETEPML4E.
Notation ept_st_unfolding :=
(Tstruct _eptStruct
(Fcons _pml4 (Tarray (Tpointer tuchar noattr) 1024 noattr)
(Fcons _pdpt (Tarray (Tpointer tuchar noattr) 1024 noattr)
(Fcons _pdt
(Tarray (Tarray (Tpointer tuchar noattr)
1024 noattr) 4
noattr)
(Fcons _ptab
(Tarray (Tarray (Tarray tulong 512
noattr)
512 noattr) 4
noattr) Fnil)))) noattr).
Let L: compatlayer (cdata RData) :=
EPT_LOC ↦ v_ept
⊕ 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.
Section SetEPML4EBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bept_loc: block.
Hypothesis hept_loc1 : Genv.find_symbol ge EPT_LOC = Some bept_loc.
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 EPTIntroGenSpec.
Require Import PProc.
Require Import AbstractDataType.
Require Import PProcCSource.
Require Import GlobalOracleProp.
Module PPROCCODE.
Definition EptSize := 8413184.
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.
Lemma tptrsize: sizeof (Tpointer tchar noattr) = 4.
Proof. reflexivity. Qed.
Lemma tulongsize: sizeof tulong = 8.
Proof. reflexivity. Qed.
Lemma teptstructsize: sizeof t_struct_ept = 8413184.
Proof. reflexivity. Qed.
Section SETEPML4E.
Notation ept_st_unfolding :=
(Tstruct _eptStruct
(Fcons _pml4 (Tarray (Tpointer tuchar noattr) 1024 noattr)
(Fcons _pdpt (Tarray (Tpointer tuchar noattr) 1024 noattr)
(Fcons _pdt
(Tarray (Tarray (Tpointer tuchar noattr)
1024 noattr) 4
noattr)
(Fcons _ptab
(Tarray (Tarray (Tarray tulong 512
noattr)
512 noattr) 4
noattr) Fnil)))) noattr).
Let L: compatlayer (cdata RData) :=
EPT_LOC ↦ v_ept
⊕ 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.
Section SetEPML4EBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bept_loc: block.
Hypothesis hept_loc1 : Genv.find_symbol ge EPT_LOC = Some bept_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 set_EPML4E_body_correct:
∀ m m´ m´´ d env le ofs,
env = PTree.empty _ →
Mem.store Mint32 ((m, d) : mem) bept_loc (EptSize × (CPU_ID d) + 4) Vzero
= Some (m´, d) →
Mem.store Mint32 (m´, d) bept_loc (EptSize × (CPU_ID d) + 0) (Vptr bept_loc ofs)
= Some (m´´, d) →
Int.unsigned ofs = EptSize × (CPU_ID d) + PgSize + EPTEPERM →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_set_EPML4E_body E0 le´ (m´´, d) Out_normal.
Proof.
intros.
subst.
unfold f_set_EPML4E_body.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tulongsize; intro tulongsize.
generalize teptstructsize; intro teptstructsize.
generalize tcharsize; intro tcharsize.
assert (CPU_ID_range: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H3; eauto. }
assert (CPU_ID_range_aux: 0 ≤ CPU_ID d < Int.max_unsigned).
{ omega. }
assert (get_cpu_id_spec: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold ObjMultiprocessor.get_CPU_ID_spec.
inv H4.
rewrite H, H5; rewrite Int.unsigned_repr; eauto.
omega. }
assert (eptsize_range : 0 ≤ sizeof ept_st_unfolding ≤ Int.max_unsigned).
{ fold t_struct_ept; omega. }
assert (eptsize_cpuid_range : 0 ≤ sizeof ept_st_unfolding × (CPU_ID d) ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
unfold t_struct_ept.
esplit; repeat vcgen.
- fold t_struct_ept.
rewrite teptstructsize.
rewrite tptrsize.
replace (0 + 8413184 × CPU_ID d + 0 + 4 × 1) with (8413184 × CPU_ID d + 4); try omega.
fold EptSize.
Opaque EptSize.
simpl.
Transparent EptSize.
rewrite Int.unsigned_repr; try (unfold EptSize; omega).
repeat vcgen.
- fold t_struct_ept.
rewrite teptstructsize.
rewrite tptrsize.
replace (0 + 8413184 × CPU_ID d + 0 + 4 × 0) with (8413184 × CPU_ID d + 0); try omega.
rewrite tcharsize.
replace (0 + 8413184 × CPU_ID d + 4096 + 1 × 7) with (8413184 × CPU_ID d + 4096 + 7); try omega.
fold EptSize.
Opaque EptSize.
simpl.
Transparent EptSize.
rewrite Int.unsigned_repr; try (unfold EptSize; omega).
rewrite <- Int.repr_unsigned with ofs in H1.
rewrite H2 in H1.
repeat vcgen.
- fold t_struct_ept.
rewrite teptstructsize.
omega.
Qed.
End SetEPML4EBody.
Theorem set_EPML4E_code_correct:
spec_le (set_EPML4E ↦ setEPML4_spec_low) (〚set_EPML4E ↦ f_set_EPML4E 〛L).
Proof.
Transparent Z.add Z.mul.
set (L´ := L) in ×.
unfold L in ×.
Opaque Z.add Z.mul Z.sub Z.div.
fbigstep_pre L´.
destruct m.
destruct m0.
destruct m´.
destruct H0; destruct H1; subst.
simpl in *; subst.
fold EptSize in ×.
fbigstep (set_EPML4E_body_correct s (Genv.globalenv p) makeglobalenv
b0 H
b2 Hb2fs Hb2fp
m m0 m1 l1 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_EPML4E)
(Vint pml4_idx::nil)
(create_undef_temps
(fn_temps f_set_EPML4E)))) H4.
Qed.
End SETEPML4E.
Section SETEPDPTE.
Notation ept_st_unfolding :=
(Tstruct _eptStruct
(Fcons _pml4 (Tarray (Tpointer tuchar noattr) 1024 noattr)
(Fcons _pdpt (Tarray (Tpointer tuchar noattr) 1024 noattr)
(Fcons _pdt
(Tarray (Tarray (Tpointer tuchar noattr)
1024 noattr) 4
noattr)
(Fcons _ptab
(Tarray (Tarray (Tarray tulong 512
noattr)
512 noattr) 4
noattr) Fnil)))) noattr).
Let L: compatlayer (cdata RData) :=
EPT_LOC ↦ v_ept
⊕ 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.
Section SETEPDPTEBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bept_loc: block.
Hypothesis hept_loc1 : Genv.find_symbol ge EPT_LOC = Some bept_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 set_EPDPTE_body_correct:
∀ m m´ m´´ d env le ofs pdpt_idx,
env = PTree.empty _ →
PTree.get tpdpt_idx le = Some (Vint pdpt_idx) →
Mem.store Mint32 ((m, d) : mem) bept_loc (EptSize × (CPU_ID d) +
PgSize + (Int.unsigned pdpt_idx) × 8 + 4) Vzero
= Some (m´, d) →
Mem.store Mint32 (m´, d) bept_loc (EptSize × (CPU_ID d) +
PgSize + (Int.unsigned pdpt_idx) × 8)
(Vptr bept_loc ofs) = Some (m´´, d) →
Int.unsigned ofs = EptSize × (CPU_ID d) + ((Int.unsigned pdpt_idx) + 2) ×
PgSize + EPTEPERM →
0 ≤ Int.unsigned pdpt_idx ≤ EPT_PDPT_INDEX (Int.max_unsigned) →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_set_EPDPTE_body E0 le´ (m´´, d) Out_normal.
Proof.
intros.
subst.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tulongsize; intro tulongsize.
generalize teptstructsize; intro teptstructsize.
generalize tcharsize; intro tcharsize.
assert (CPU_ID_range: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H5; eauto. }
assert (CPU_ID_range_aux: 0 ≤ CPU_ID d < Int.max_unsigned).
{ omega. }
assert (get_cpu_id_spec: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold ObjMultiprocessor.get_CPU_ID_spec.
inv H6.
rewrite H, H7; rewrite Int.unsigned_repr; eauto.
omega. }
assert (eptsize_range : 0 ≤ sizeof ept_st_unfolding ≤ Int.max_unsigned).
{ fold t_struct_ept; omega. }
assert (eptsize_cpuid_range : 0 ≤ sizeof ept_st_unfolding × (CPU_ID d) ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
assert (eptsize_cpuid_4096_range : 0 ≤ sizeof ept_st_unfolding × (CPU_ID d) + 4096 ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
assert(pdptmax: EPT_PDPT_INDEX Int.max_unsigned = 3)
by (rewrite muval; unfold EPT_PDPT_INDEX; reflexivity).
assert(pdpt_idx_range: 0 ≤ Int.unsigned pdpt_idx ≤ 3)
by (clearAllExceptTwo H4 pdptmax; omega).
assert(range1: 0 ≤ sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) ≤ Int.max_unsigned)
by (simpl; clearAllExceptOne muval; omega).
assert(range2: 0 ≤ Int.unsigned (Int.repr (sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr))) ×
Int.unsigned pdpt_idx ≤ Int.max_unsigned).
{ simpl.
clearAllExceptTwo muval pdpt_idx_range.
rewrite muval.
rewrite Int.unsigned_repr; omega. }
assert (range3: 0 ≤ 0 + sizeof ept_st_unfolding × CPU_ID d + 8192 ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
assert (range4: sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) = 4096) by (simpl; auto).
assert (range5: 0 ≤ 0 + sizeof ept_st_unfolding × CPU_ID d + 8192 +
sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) ×
Int.unsigned pdpt_idx ≤ Int.max_unsigned).
{ fold t_struct_ept.
rewrite teptstructsize.
rewrite range4.
omega. }
assert (unfolded_mul:
match CPU_ID d with
| 0 ⇒ 0
| Z.pos y´ ⇒
Z.pos
(y´ + (y´ + y´~0~0~0~0~0~0~0~0~0)~0)~0~0~0~0~0~0~0~0~0~0~0~0~0
| Z.neg y´ ⇒
Z.neg
(y´ + (y´ + y´~0~0~0~0~0~0~0~0~0)~0)~0~0~0~0~0~0~0~0~0~0~0~0~0
end = 8413184 × CPU_ID d) by (simpl; ring).
unfold f_set_EPDPTE_body.
unfold t_struct_ept.
esplit.
unfold exec_stmt.
change E0 with (E0 ** E0).
econstructor.
- repeat vcgen.
- change E0 with (E0 ** E0).
econstructor.
+ repeat vcgen.
rewrite unfolded_mul; fold EptSize; unfold Mem.storev; rewrite tptrsize.
rewrite Int.unsigned_repr; try (unfold EptSize; omega).
replace (EptSize × CPU_ID d + 4096 + 4 × (Int.unsigned pdpt_idx × 2 + 1))
with (EptSize × CPU_ID d + 4096 + Int.unsigned pdpt_idx × 8 + 4); try ring.
repeat vcgen.
+ repeat vcgen.
rewrite unfolded_mul; fold EptSize; unfold Mem.storev; rewrite tptrsize.
replace (EptSize × CPU_ID d + 4096 + 4 × (Int.unsigned pdpt_idx × 2))
with (EptSize × CPU_ID d + 4096 + Int.unsigned pdpt_idx × 8); try ring.
rewrite <- Int.repr_unsigned with ofs in H2.
rewrite H3 in H2.
rewrite tcharsize.
replace (EptSize × CPU_ID d + 8192 + 4096 × Int.unsigned pdpt_idx + 4 × 0 + 1 × 7)
with (EptSize × CPU_ID d + (Int.unsigned pdpt_idx + 2) × 4096 + 7); try ring.
rewrite Int.unsigned_repr; try (unfold EptSize; omega).
repeat vcgen.
Qed.
End SETEPDPTEBody.
Theorem set_EPDPTE_code_correct:
spec_le (set_EPDPTE ↦ setEPDPTE_spec_low) (〚set_EPDPTE ↦ f_set_EPDPTE 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
Opaque Z.mul Z.add Z.sub.
fbigstep_pre L´.
destruct m.
destruct m0.
destruct m´.
destruct H0; destruct H1; subst.
simpl in *; subst.
fold EptSize in ×.
fbigstep (set_EPDPTE_body_correct s (Genv.globalenv p) makeglobalenv
b0 H
b2 Hb2fs Hb2fp
m m0 m1 l1 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_EPDPTE)
(Vint pml4_idx::Vint pdpt::nil)
(create_undef_temps
(fn_temps f_set_EPDPTE)))) muval.
Qed.
End SETEPDPTE.
Section SETEPDTE.
Notation ept_st_unfolding :=
(Tstruct _eptStruct
(Fcons _pml4 (Tarray (Tpointer tuchar noattr) 1024 noattr)
(Fcons _pdpt (Tarray (Tpointer tuchar noattr) 1024 noattr)
(Fcons _pdt
(Tarray (Tarray (Tpointer tuchar noattr)
1024 noattr) 4
noattr)
(Fcons _ptab
(Tarray (Tarray (Tarray tulong 512
noattr)
512 noattr) 4
noattr) Fnil)))) noattr).
Let L: compatlayer (cdata RData) :=
EPT_LOC ↦ v_ept
⊕ 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.
Section SETEPDTEBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bept_loc: block.
Hypothesis hept_loc1 : Genv.find_symbol ge EPT_LOC = Some bept_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 set_EPDTE_body_correct:
∀ m m´ m´´ d env le ofs pdpt_idx pdir_idx,
env = PTree.empty _ →
PTree.get tpdpt_idx le = Some (Vint pdpt_idx) →
PTree.get tpdir_idx le = Some (Vint pdir_idx) →
Mem.store Mint32 ((m, d): mem) bept_loc
(EptSize × (CPU_ID d) +
((Int.unsigned pdpt_idx) + 2) × PgSize +
((Int.unsigned pdir_idx) × 8) + 4) Vzero = Some (m´, d) →
Mem.store Mint32 (m´, d) bept_loc
(EptSize × (CPU_ID d) +
((Int.unsigned pdpt_idx) + 2) × PgSize +
((Int.unsigned pdir_idx) × 8)) (Vptr bept_loc ofs) = Some (m´´, d) →
Int.unsigned ofs = EptSize × (CPU_ID d) +
(6 + (Int.unsigned pdpt_idx) × 512 +
(Int.unsigned pdir_idx)) × PgSize + EPTEPERM →
0 ≤ Int.unsigned pdpt_idx ≤ EPT_PDPT_INDEX Int.max_unsigned →
0 ≤ Int.unsigned pdir_idx ≤ EPT_PDIR_INDEX Int.max_unsigned →
high_level_invariant d →
kernel_mode d →
∃ le´, exec_stmt ge env le ((m, d): mem) f_set_EPDTE_body E0 le´ (m´´, d) Out_normal.
Proof.
intros.
subst.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tulongsize; intro tulongsize.
generalize teptstructsize; intro teptstructsize.
generalize tcharsize; intro tcharsize.
assert (CPU_ID_range: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H7; eauto. }
assert (CPU_ID_range_aux: 0 ≤ CPU_ID d < Int.max_unsigned).
{ omega. }
assert (get_cpu_id_spec: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold ObjMultiprocessor.get_CPU_ID_spec.
inv H8.
rewrite H, H9; rewrite Int.unsigned_repr; eauto.
omega. }
assert (eptsize_range : 0 ≤ sizeof ept_st_unfolding ≤ Int.max_unsigned).
{ fold t_struct_ept; omega. }
assert (eptsize_cpuid_range : 0 ≤ sizeof ept_st_unfolding × (CPU_ID d) ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
assert (eptsize_cpuid_4096_range : 0 ≤ sizeof ept_st_unfolding × (CPU_ID d) + 4096 ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
assert(pdptmax: EPT_PDPT_INDEX Int.max_unsigned = 3)
by (rewrite muval; unfold EPT_PDPT_INDEX; reflexivity).
assert(pdpt_idx_range: 0 ≤ Int.unsigned pdpt_idx ≤ 3)
by (clearAllExceptTwo H5 pdptmax; omega).
assert(pdirmax: EPT_PDIR_INDEX Int.max_unsigned = 511)
by (rewrite muval; unfold EPT_PDIR_INDEX;reflexivity).
assert(pdir_idx_range: 0 ≤ Int.unsigned pdir_idx ≤ 511)
by (clearAllExceptTwo H6 pdirmax; omega).
assert(range1: 0 ≤ sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) ≤ Int.max_unsigned)
by (simpl; clearAllExceptOne muval; omega).
assert(range2: 0 ≤ Int.unsigned (Int.repr (sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr))) ×
Int.unsigned pdpt_idx ≤ Int.max_unsigned).
{ simpl.
clearAllExceptTwo muval pdpt_idx_range.
rewrite muval.
rewrite Int.unsigned_repr; omega. }
assert (range3: 0 ≤ 0 + sizeof ept_st_unfolding × CPU_ID d + 8192 ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
assert (range4: sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) = 4096) by (simpl; auto).
assert (range5: sizeof (Tarray tulong 512 noattr) = 4096) by (simpl; reflexivity).
assert (range6: 0 ≤ 0 + sizeof ept_st_unfolding × CPU_ID d + 8192 +
sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) ×
Int.unsigned pdpt_idx ≤ Int.max_unsigned).
{ fold t_struct_ept.
rewrite teptstructsize.
rewrite range4.
omega. }
assert (ptr_size: sizeof (Tpointer tuchar noattr) = 4) by (simpl; auto).
assert (unfolded_mul:
match CPU_ID d with
| 0 ⇒ 0
| Z.pos y´ ⇒
Z.pos
(y´ + (y´ + y´~0~0~0~0~0~0~0~0~0)~0)~0~0~0~0~0~0~0~0~0~0~0~0~0
| Z.neg y´ ⇒
Z.neg
(y´ + (y´ + y´~0~0~0~0~0~0~0~0~0)~0)~0~0~0~0~0~0~0~0~0~0~0~0~0
end = 8413184 × CPU_ID d) by (simpl; ring).
unfold f_set_EPDTE_body.
unfold t_struct_ept.
esplit; unfold exec_stmt.
change E0 with (E0 ** E0); econstructor; [ repeat vcgen | change E0 with (E0 ** E0); econstructor].
- repeat vcgen.
rewrite unfolded_mul.
rewrite tptrsize.
fold EptSize.
replace (EptSize × CPU_ID d + 8192 + 4096 × Int.unsigned pdpt_idx + 4 × (Int.unsigned pdir_idx × 2 + 1))
with (EptSize × CPU_ID d + (Int.unsigned pdpt_idx + 2) × 4096 + Int.unsigned pdir_idx × 8 + 4); try ring.
unfold Mem.storev.
rewrite Int.unsigned_repr; try (unfold EptSize; omega).
exact H2.
- repeat vcgen.
rewrite unfolded_mul.
rewrite <- Int.repr_unsigned with ofs in H3.
rewrite H4 in H3.
fold EptSize.
rewrite tptrsize.
replace (EptSize × CPU_ID d + 8192 + 4096 × Int.unsigned pdpt_idx + 4 × (Int.unsigned pdir_idx × 2))
with (EptSize × CPU_ID d + (Int.unsigned pdpt_idx + 2) × 4096 + Int.unsigned pdir_idx × 8); try ring.
rewrite range5.
rewrite tulongsize.
rewrite tcharsize.
replace (EptSize × CPU_ID d + 24576 + 2097152 × Int.unsigned pdpt_idx + 4096 × Int.unsigned pdir_idx + 8 × 0 + 1 × 7)
with (EptSize × CPU_ID d + (6 + Int.unsigned pdpt_idx × 512 + Int.unsigned pdir_idx) × 4096 + 7); try ring.
unfold Mem.storev.
rewrite Int.unsigned_repr; try (unfold EptSize; omega).
exact H3.
Qed.
End SETEPDTEBody.
Theorem set_EPDTE_code_correct:
spec_le (set_EPDTE ↦ setEPDTE_spec_low) (〚set_EPDTE ↦ f_set_EPDTE 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
Opaque Z.mul Z.add Z.sub.
fbigstep_pre L´.
destruct m.
destruct m0.
destruct m´.
destruct H0; destruct H1; simpl in *; subst.
fold EptSize in ×.
fbigstep (set_EPDTE_body_correct s (Genv.globalenv p) makeglobalenv
b0 H
b2 Hb2fs Hb2fp
m m0 m1 l1 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_EPDTE)
(Vint pml4_idx::Vint pdpt::Vint pdir::nil)
(create_undef_temps (fn_temps f_set_EPDTE)))) muval.
Qed.
End SETEPDTE.
Section GETEPTE.
Notation ept_st_unfolding :=
(Tstruct _eptStruct
(Fcons _pml4 (Tarray (Tpointer tuchar noattr) 1024 noattr)
(Fcons _pdpt (Tarray (Tpointer tuchar noattr) 1024 noattr)
(Fcons _pdt
(Tarray (Tarray (Tpointer tuchar noattr)
1024 noattr) 4
noattr)
(Fcons _ptab
(Tarray (Tarray (Tarray tulong 512
noattr)
512 noattr) 4
noattr) Fnil)))) noattr).
Let L: compatlayer (cdata RData) :=
EPT_LOC ↦ v_ept
⊕ 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.
Section GETEPTEBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bept_loc: block.
Hypothesis hept_loc1 : Genv.find_symbol ge EPT_LOC = Some bept_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 get_EPTE_body_correct:
∀ m d env le pdpt_idx pdir_idx ptab_idx hpa_val,
env = PTree.empty _ →
PTree.get tpdpt_idx le = Some (Vint pdpt_idx) →
PTree.get tpdir_idx le = Some (Vint pdir_idx) →
PTree.get tptab_idx le = Some (Vint ptab_idx) →
Mem.load Mint64 m bept_loc (EptSize × (CPU_ID d) +
(6 + (Int.unsigned pdpt_idx) × 512 + (Int.unsigned pdir_idx)) × PgSize +
((Int.unsigned ptab_idx) × 8)) = Some (Vlong (Int64.repr (Int.unsigned hpa_val))) →
0 ≤ Int.unsigned pdpt_idx ≤ EPT_PDPT_INDEX (Int.max_unsigned) →
0 ≤ Int.unsigned pdir_idx ≤ EPT_PDIR_INDEX (Int.max_unsigned) →
0 ≤ Int.unsigned ptab_idx ≤ EPT_PTAB_INDEX (Int.max_unsigned) →
high_level_invariant d →
kernel_mode d →
∃ le´, exec_stmt ge env le ((m, d): mem) f_get_EPTE_body E0 le´ (m, d) (Out_return (Some (Vint hpa_val, tint))).
Proof.
intros.
subst.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tulongsize; intro tulongsize.
generalize teptstructsize; intro teptstructsize.
generalize tcharsize; intro tcharsize.
assert (CPU_ID_range: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H7; eauto. }
assert (CPU_ID_range_aux: 0 ≤ CPU_ID d < Int.max_unsigned).
{ omega. }
assert (get_cpu_id_spec: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold ObjMultiprocessor.get_CPU_ID_spec.
inv H8.
rewrite H, H9; rewrite Int.unsigned_repr; eauto.
omega. }
assert (eptsize_range : 0 ≤ sizeof ept_st_unfolding ≤ Int.max_unsigned).
{ fold t_struct_ept; omega. }
assert (eptsize_cpuid_range : 0 ≤ sizeof ept_st_unfolding × (CPU_ID d) ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
assert (eptsize_cpuid_4096_range : 0 ≤ sizeof ept_st_unfolding × (CPU_ID d) + 4096 ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
assert(pdptmax: EPT_PDPT_INDEX Int.max_unsigned = 3)
by (rewrite muval; unfold EPT_PDPT_INDEX; reflexivity).
assert(pdpt_idx_range: 0 ≤ Int.unsigned pdpt_idx ≤ 3)
by (clearAllExceptTwo H4 pdptmax; omega).
assert(pdirmax: EPT_PDIR_INDEX Int.max_unsigned = 511)
by (rewrite muval; unfold EPT_PDIR_INDEX;reflexivity).
assert(pdir_idx_range: 0 ≤ Int.unsigned pdir_idx ≤ 511)
by (clearAllExceptTwo H5 pdirmax; omega).
assert(ptabmax: EPT_PTAB_INDEX Int.max_unsigned = 511)
by (rewrite muval; unfold EPT_PTAB_INDEX; reflexivity).
assert (ptab_idx_range: 0 ≤ Int.unsigned ptab_idx ≤ 511)
by (clearAllExceptTwo H6 ptabmax; omega).
assert(range1: 0 ≤ sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) ≤ Int.max_unsigned)
by (simpl; clearAllExceptOne muval; omega).
assert(range2: 0 ≤ Int.unsigned (Int.repr (sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr))) ×
Int.unsigned pdpt_idx ≤ Int.max_unsigned).
{ simpl.
clearAllExceptTwo muval pdpt_idx_range.
rewrite muval.
rewrite Int.unsigned_repr; omega. }
assert (range3: 0 ≤ 0 + sizeof ept_st_unfolding × CPU_ID d + 8192 ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
assert (range4: sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) = 4096) by (simpl; auto).
assert (range5: sizeof (Tarray tulong 512 noattr) = 4096) by (simpl; reflexivity).
assert (range6: sizeof (Tarray (Tarray tulong 512 noattr) 512 noattr) = 2097152)
by (simpl; reflexivity).
assert (range7: sizeof(Tarray (Tarray (Tpointer tuchar noattr) 1024 noattr) 4 noattr) = 16384)
by (simpl; reflexivity).
assert (range8: 0 ≤ 0 + sizeof ept_st_unfolding × CPU_ID d + 8192 +
sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) ×
Int.unsigned pdpt_idx ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; rewrite range4; omega. }
assert (unfolded_mul:
match CPU_ID d with
| 0 ⇒ 0
| Z.pos y´ ⇒
Z.pos
(y´ + (y´ + y´~0~0~0~0~0~0~0~0~0)~0)~0~0~0~0~0~0~0~0~0~0~0~0~0
| Z.neg y´ ⇒
Z.neg
(y´ + (y´ + y´~0~0~0~0~0~0~0~0~0)~0)~0~0~0~0~0~0~0~0~0~0~0~0~0
end = 8413184 × CPU_ID d) by (simpl; ring).
unfold f_get_EPTE_body.
unfold t_struct_ept.
esplit; unfold exec_stmt.
change E0 with (E0 ** E0); econstructor; [repeat vcgen | ].
repeat vcgen.
- rewrite unfolded_mul.
fold EptSize.
rewrite range5.
rewrite tulongsize.
replace (EptSize × CPU_ID d + 24576 + 2097152 × Int.unsigned pdpt_idx +
4096 × Int.unsigned pdir_idx + 8 × Int.unsigned ptab_idx) with
(EptSize × CPU_ID d +
(6 + Int.unsigned pdpt_idx × 512 + Int.unsigned pdir_idx) × 4096 +
Int.unsigned ptab_idx × 8); try ring.
Opaque EptSize Z.mul Z.add.
simpl.
Transparent EptSize Z.mul Z.add.
rewrite Int.unsigned_repr; try (unfold EptSize; omega).
repeat vcgen.
- unfold sem_cast.
repeat vcgen.
generalize max_unsigned64_val; intro mulval.
assert (hpa_range: 0 ≤ Int.unsigned hpa_val ≤ Int.max_unsigned)
by apply Int.unsigned_range_2.
rewrite muval in hpa_range.
rewrite mulval.
clearAllExceptTwo mulval hpa_range.
omega.
Qed.
End GETEPTEBody.
Theorem get_EPTE_code_correct:
spec_le (get_EPTE ↦ getEPTE_spec_low) (〚get_EPTE ↦ f_get_EPTE 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
Opaque Z.mul Z.add Z.sub.
fbigstep_pre L´.
destruct m´.
simpl in ×.
destruct H5.
fold EptSize in ×.
fbigstep (get_EPTE_body_correct s (Genv.globalenv p) makeglobalenv
b0 H
b2 Hb2fs Hb2fp
m l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_get_EPTE)
(Vint pml4_idx::Vint pdpt::Vint pdir::Vint ptab::nil)
(create_undef_temps (fn_temps f_get_EPTE)))) muval.
Qed.
End GETEPTE.
Section SETEPTE.
Notation ept_st_unfolding :=
(Tstruct _eptStruct
(Fcons _pml4 (Tarray (Tpointer tuchar noattr) 1024 noattr)
(Fcons _pdpt (Tarray (Tpointer tuchar noattr) 1024 noattr)
(Fcons _pdt
(Tarray (Tarray (Tpointer tuchar noattr)
1024 noattr) 4
noattr)
(Fcons _ptab
(Tarray (Tarray (Tarray tulong 512
noattr)
512 noattr) 4
noattr) Fnil)))) noattr).
Let L: compatlayer (cdata RData) :=
EPT_LOC ↦ v_ept
⊕ 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.
Section SETEPTEBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bept_loc: block.
Hypothesis hept_loc1 : Genv.find_symbol ge EPT_LOC = Some bept_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 set_EPTE_body_correct:
∀ m m´ d env le pdpt_idx pdir_idx ptab_idx hpa,
env = PTree.empty _ →
PTree.get tpdpt_idx le = Some (Vint pdpt_idx) →
PTree.get tpdir_idx le = Some (Vint pdir_idx) →
PTree.get tptab_idx le = Some (Vint ptab_idx) →
PTree.get hpa_val le = Some (Vint hpa) →
Mem.store Mint64 ((m, d): mem) bept_loc
(EptSize × (CPU_ID d) + (6 + (Int.unsigned pdpt_idx) × 512 + (Int.unsigned pdir_idx)) × PgSize +
((Int.unsigned ptab_idx) × 8)) (Vlong (Int64.repr (Int.unsigned hpa))) = Some (m´, d) →
0 ≤ Int.unsigned pdpt_idx ≤ EPT_PDPT_INDEX (Int.max_unsigned) →
0 ≤ Int.unsigned pdir_idx ≤ EPT_PDIR_INDEX (Int.max_unsigned) →
0 ≤ Int.unsigned ptab_idx ≤ EPT_PTAB_INDEX (Int.max_unsigned) →
high_level_invariant d →
kernel_mode d →
∃ le´, exec_stmt ge env le ((m, d): mem) f_set_EPTE_body E0 le´ (m´, d) Out_normal.
Proof.
intros.
subst.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tulongsize; intro tulongsize.
generalize teptstructsize; intro teptstructsize.
generalize tcharsize; intro tcharsize.
assert (CPU_ID_range: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H8; eauto. }
assert (CPU_ID_range_aux: 0 ≤ CPU_ID d < Int.max_unsigned).
{ omega. }
assert (get_cpu_id_spec: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold ObjMultiprocessor.get_CPU_ID_spec.
inv H9.
rewrite H, H10; rewrite Int.unsigned_repr; eauto.
omega. }
assert (eptsize_range : 0 ≤ sizeof ept_st_unfolding ≤ Int.max_unsigned).
{ fold t_struct_ept; omega. }
assert (eptsize_cpuid_range : 0 ≤ sizeof ept_st_unfolding × (CPU_ID d) ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
assert (eptsize_cpuid_4096_range : 0 ≤ sizeof ept_st_unfolding × (CPU_ID d) + 4096 ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
assert(pdptmax: EPT_PDPT_INDEX Int.max_unsigned = 3)
by (rewrite muval; unfold EPT_PDPT_INDEX; reflexivity).
assert(pdpt_idx_range: 0 ≤ Int.unsigned pdpt_idx ≤ 3)
by (clearAllExceptTwo H5 pdptmax; omega).
assert(pdirmax: EPT_PDIR_INDEX Int.max_unsigned = 511)
by (rewrite muval; unfold EPT_PDIR_INDEX;reflexivity).
assert(pdir_idx_range: 0 ≤ Int.unsigned pdir_idx ≤ 511)
by (clearAllExceptTwo H6 pdirmax; omega).
assert(ptabmax: EPT_PTAB_INDEX Int.max_unsigned = 511)
by (rewrite muval; unfold EPT_PTAB_INDEX; reflexivity).
assert (ptab_idx_range: 0 ≤ Int.unsigned ptab_idx ≤ 511)
by (clearAllExceptTwo H7 ptabmax; omega).
assert(range1: 0 ≤ sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) ≤ Int.max_unsigned)
by (simpl; clearAllExceptOne muval; omega).
assert(range2: 0 ≤ Int.unsigned (Int.repr (sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr))) ×
Int.unsigned pdpt_idx ≤ Int.max_unsigned).
{ simpl.
clearAllExceptTwo muval pdpt_idx_range.
rewrite muval.
rewrite Int.unsigned_repr; omega. }
assert (range3: 0 ≤ 0 + sizeof ept_st_unfolding × CPU_ID d + 8192 ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; omega. }
assert (range4: sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) = 4096) by (simpl; auto).
assert (range5: sizeof (Tarray tulong 512 noattr) = 4096) by (simpl; reflexivity).
assert (range6: sizeof (Tarray (Tarray tulong 512 noattr) 512 noattr) = 2097152)
by (simpl; reflexivity).
assert (range7: sizeof(Tarray (Tarray (Tpointer tuchar noattr) 1024 noattr) 4 noattr) = 16384)
by (simpl; reflexivity).
assert (range8: 0 ≤ 0 + sizeof ept_st_unfolding × CPU_ID d + 8192 +
sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) ×
Int.unsigned pdpt_idx ≤ Int.max_unsigned).
{ fold t_struct_ept; rewrite teptstructsize; rewrite range4; omega. }
assert (unfolded_mul:
match CPU_ID d with
| 0 ⇒ 0
| Z.pos y´ ⇒
Z.pos
(y´ + (y´ + y´~0~0~0~0~0~0~0~0~0)~0)~0~0~0~0~0~0~0~0~0~0~0~0~0
| Z.neg y´ ⇒
Z.neg
(y´ + (y´ + y´~0~0~0~0~0~0~0~0~0)~0)~0~0~0~0~0~0~0~0~0~0~0~0~0
end = 8413184 × CPU_ID d) by (simpl; ring).
unfold f_set_EPTE_body.
unfold t_struct_ept.
esplit.
unfold exec_stmt.
change E0 with (E0**E0); econstructor; repeat vcgen.
rewrite unfolded_mul; fold EptSize.
rewrite range5.
rewrite tulongsize.
replace (EptSize × CPU_ID d + 24576 + 2097152 × Int.unsigned pdpt_idx + 4096 × Int.unsigned pdir_idx
+ 8 × Int.unsigned ptab_idx)
with (EptSize × CPU_ID d + (6 + Int.unsigned pdpt_idx × 512 + Int.unsigned pdir_idx) × 4096 +
Int.unsigned ptab_idx × 8); try ring.
unfold Mem.storev.
rewrite Int.unsigned_repr; try (unfold EptSize; omega).
exact H4.
Qed.
End SETEPTEBody.
Theorem set_EPTE_code_correct:
spec_le (set_EPTE ↦ setEPTE_spec_low) (〚set_EPTE ↦ f_set_EPTE 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
Opaque Z.mul Z.add Z.sub.
fbigstep_pre L´.
destruct m.
destruct m´.
destruct H0.
simpl in ×.
destruct H5.
fold EptSize in ×.
subst.
fbigstep (set_EPTE_body_correct s (Genv.globalenv p) makeglobalenv
b0 H
b2 Hb2fs Hb2fp
m m0 l0 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_EPTE)
(Vint pml4_idx::Vint pdpt::Vint pdir::Vint ptab::Vint hpa::nil)
(create_undef_temps (fn_temps f_set_EPTE)))) muval.
Qed.
End SETEPTE.
End WithPrimitives.
End PPROCCODE.