Library mcertikos.virt.intel.PProcCode
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
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 PProcCSource.
Require Import AbstractDataType.
Module PPROCCODE.
Section WithPrimitives.
Context `{real_params_ops : RealParamsOps}.
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.
Let L: compatlayer (cdata RData) := EPT_LOC ↦ v_ept.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetEPML4EBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bept_loc: block.
Hypothesis hept_loc1 : Genv.find_symbol ge EPT_LOC = Some bept_loc.
Lemma set_EPML4E_body_correct: ∀ m m´ m´´ d env le ofs,
env = PTree.empty _ →
Mem.store Mint32 (m, d) bept_loc 4 Vzero = Some (m´, d) →
Mem.store Mint32 (m´, d) bept_loc 0 (Vptr bept_loc ofs) = Some (m´´, d) →
Int.unsigned ofs = PgSize + EPTEPERM →
exec_stmt ge env le ((m, d): mem) set_EPML4E_body E0 le (m´´, d) Out_normal.
Proof.
intros.
subst.
unfold 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.
repeat vcgen.
rewrite tptrsize, tcharsize.
rewrite Z.add_0_l.
rewrite Z.add_0_l.
unfold Mem.storev.
rewrite Int.unsigned_repr; try omega.
change (4 × 1) with 4.
change (1 × 7) with 7.
rewrite <- Int.repr_unsigned with ofs in H1.
rewrite H2 in H1.
assumption.
Qed.
End SetEPML4EBody.
Theorem set_EPML4E_code_correct:
spec_le (set_EPML4E ↦ setEPML4_spec_low) (〚set_EPML4E ↦ f_set_EPML4E 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m0.
destruct m´.
destruct H0; destruct H1; subst.
fbigstep (set_EPML4E_body_correct (Genv.globalenv p) b0 H m m0 m1 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_EPML4E)
(Vint pml4_idx::nil)
(create_undef_temps (fn_temps f_set_EPML4E)))) H3.
Qed.
End SETEPML4E.
Section SETEPDPTE.
Let L: compatlayer (cdata RData) := EPT_LOC ↦ v_ept.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SETEPDPTEBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bept_loc: block.
Hypothesis hept_loc1 : Genv.find_symbol ge EPT_LOC = Some bept_loc.
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) bept_loc (PgSize + (Int.unsigned pdpt_idx) × 8 + 4) Vzero = Some (m´, d) →
Mem.store Mint32 (m´, d) bept_loc (PgSize + (Int.unsigned pdpt_idx) × 8) (Vptr bept_loc ofs) = Some (m´´, d) →
Int.unsigned ofs = ((Int.unsigned pdpt_idx) + 2) × PgSize + EPTEPERM →
0 ≤ Int.unsigned pdpt_idx ≤ EPT_PDPT_INDEX (Int.max_unsigned) →
exec_stmt ge env le ((m, d): mem) set_EPDPTE_body E0 le (m´´, d) Out_normal.
Proof.
intros.
subst.
unfold set_EPDPTE_body.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tulongsize; intro tulongsize.
generalize teptstructsize; intro teptstructsize.
generalize tcharsize; intro tcharsize.
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 ≤ Int.unsigned (Int.repr (sizeof (Tpointer tuchar noattr))) ×
Int.unsigned (Int.repr 0) ≤ Int.max_unsigned).
{
simpl; clearAllExceptOne muval.
repeat rewrite Int.unsigned_repr; rewrite muval; omega.
}
assert(range4: 0 ≤ Int.unsigned (Int.add Int.zero (Int.repr 8192)) +
Int.unsigned (Int.mul (Int.repr (sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr)))
pdpt_idx) ≤ Int.max_unsigned)
by (simpl; clearAllExceptTwo muval pdpt_idx_range; repeat vcgen).
assert(range5: 0 ≤ Int.unsigned (Int.repr (sizeof (Tpointer tuchar noattr))) ×
Int.unsigned (Int.repr 0) ≤ Int.max_unsigned).
{
simpl; clearAllExceptOne muval.
repeat rewrite Int.unsigned_repr; rewrite muval; clear muval; omega.
}
assert(range6: 0 ≤ Int.unsigned (Int.add Int.zero (Int.repr 8192)) +
Int.unsigned (Int.mul (Int.repr (sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr)))
pdpt_idx) ≤ Int.max_unsigned)
by (simpl; clearAllExceptTwo muval pdpt_idx_range; repeat vcgen).
d12 vcgen.
rewrite tptrsize.
rewrite Z.add_0_l.
rewrite <- Z.mul_comm.
rewrite repr_zero.
unfold Vzero in H1.
unfold Mem.storev.
rewrite <- Int.repr_unsigned with ofs in H3.
rewrite Int.unsigned_repr.
replace (4096 + (Int.unsigned pdpt_idx × 2 + 1) × 4) with
(4096 + Int.unsigned pdpt_idx × 8 + 4) by omega.
eassumption.
rewrite muval.
rewrite pdptmax in H4.
clearAllExceptOne H4.
omega.
repeat vcgen.
vcgen.
vcgen.
repeat vcgen.
vcgen.
repeat vcgen.
vcgen.
rewrite tptrsize.
rewrite tcharsize.
rewrite Z.add_0_l.
rewrite Z.add_0_l.
rewrite Z.mul_0_r.
change (1 × 7) with 7.
assert (sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr) = 4096)
by (simpl; reflexivity).
rewrite H.
replace (8192 + 4096 × Int.unsigned pdpt_idx + 0 + 7)
with ((Int.unsigned pdpt_idx + 2) × 4096 + 7) by omega.
replace (4096 + 4 × (Int.unsigned pdpt_idx × 2))
with (4096 + Int.unsigned pdpt_idx × 8) by omega.
rewrite <- Int.repr_unsigned with ofs in H2.
rewrite H3 in H2.
unfold Mem.storev.
rewrite Int.unsigned_repr.
assumption.
rewrite muval.
rewrite pdptmax in H4.
clearAllExceptOne H4.
omega.
vcgen.
vcgen.
vcgen.
vcgen.
vcgen.
vcgen.
vcgen.
vcgen.
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.
fbigstep (set_EPDPTE_body_correct (Genv.globalenv p) b0 H m m0 m1 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_EPDPTE)
(Vint pml4_idx::Vint pdpt::nil)
(create_undef_temps (fn_temps f_set_EPDPTE)))) H3.
Qed.
End SETEPDPTE.
Section SETEPDTE.
Let L: compatlayer (cdata RData) := EPT_LOC ↦ v_ept.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SETEPDTEBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bept_loc: block.
Hypothesis hept_loc1 : Genv.find_symbol ge EPT_LOC = Some bept_loc.
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) bept_loc
(((Int.unsigned pdpt_idx) + 2) × PgSize +
((Int.unsigned pdir_idx) × 8) + 4) Vzero = Some (m´, d) →
Mem.store Mint32 (m´, d) bept_loc
(((Int.unsigned pdpt_idx) + 2) × PgSize +
((Int.unsigned pdir_idx) × 8)) (Vptr bept_loc ofs) = Some (m´´, d) →
Int.unsigned ofs = (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 →
exec_stmt ge env le ((m, d): mem) set_EPDTE_body E0 le (m´´, d) Out_normal.
Proof.
intros.
subst.
unfold set_EPDTE_body.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tulongsize; intro tulongsize.
generalize teptstructsize; intro teptstructsize.
generalize tcharsize; intro tcharsize.
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(pageval: (sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr)) = 4096)
by (simpl; reflexivity).
assert (pageval´: sizeof (Tarray tulong 512 noattr) = 4096)
by (simpl; reflexivity).
d12 vcgen.
d12 vcgen.
d12 vcgen.
vcgen.
d12 vcgen.
rewrite pageval, tptrsize.
rewrite Z.add_0_l.
rewrite repr_zero.
unfold Vzero in H2.
replace (8192 + 4096 × Int.unsigned pdpt_idx + 4 × (Int.unsigned pdir_idx × 2 + 1))
with ((Int.unsigned pdpt_idx + 2) × 4096 + Int.unsigned pdir_idx × 8 + 4) by omega.
unfold Mem.storev.
rewrite Int.unsigned_repr; [eassumption | ].
clearAllExceptThree muval pdpt_idx_range pdir_idx_range.
omega.
omega.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
d12 vcgen.
repeat rewrite pageval, pageval´, tptrsize, tulongsize, tcharsize.
rewrite Z.add_0_l; rewrite Z.add_0_l.
replace (8192 + 4096 × Int.unsigned pdpt_idx + 4 × (Int.unsigned pdir_idx × 2))
with ((Int.unsigned pdpt_idx + 2) × 4096 + Int.unsigned pdir_idx × 8) by omega.
vcgen.
vcgen.
replace (24576 + 2097152 × Int.unsigned pdpt_idx + 4096 × Int.unsigned pdir_idx + 8 × 0 + 1 × 7)
with ((6 + Int.unsigned pdpt_idx × 512 + Int.unsigned pdir_idx) × 4096 + 7) by omega.
rewrite <- Int.repr_unsigned with ofs in H3.
rewrite H4 in H3.
unfold Mem.storev.
rewrite Int.unsigned_repr.
assumption.
clearAllExceptThree pdir_idx_range pdpt_idx_range muval; repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
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; subst.
fbigstep (set_EPDTE_body_correct (Genv.globalenv p) b0 H m m0 m1 l (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)))) H3.
Qed.
End SETEPDTE.
Section GETEPTE.
Let L: compatlayer (cdata RData) := EPT_LOC ↦ v_ept.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GETEPTEBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bept_loc: block.
Hypothesis hept_loc1 : Genv.find_symbol ge EPT_LOC = Some bept_loc.
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 ((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) →
exec_stmt ge env le ((m, d): mem) get_EPTE_body E0 le (m, d) (Out_return (Some (Vint hpa_val, tint))).
Proof.
intros.
subst.
unfold get_EPTE_body.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tulongsize; intro tulongsize.
generalize teptstructsize; intro teptstructsize.
generalize tcharsize; intro tcharsize.
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(pageval: (sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr)) = 4096)
by (simpl; reflexivity).
assert(pageval´: sizeof (Tarray tulong 512 noattr) = 4096)
by (simpl; reflexivity).
assert(pageval´´: sizeof (Tarray (Tarray tulong 512 noattr) 512 noattr) = 2097152)
by (simpl; reflexivity).
assert(pageval´´´: sizeof(Tarray (Tarray (Tpointer tuchar noattr) 1024 noattr) 4 noattr) = 16384)
by (simpl; reflexivity).
d12 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
vcgen.
rewrite pageval, pageval´, pageval´´, tulongsize.
repeat vcgen.
replace (0 + 24576 + 2097152 × Int.unsigned pdpt_idx + 4096 × Int.unsigned pdir_idx + 8 × Int.unsigned ptab_idx)
with ((6 + Int.unsigned pdpt_idx × 512 + Int.unsigned pdir_idx) × 4096 + Int.unsigned ptab_idx × 8) by omega.
unfold Mem.loadv.
rewrite Int.unsigned_repr;
[ | revert muval; clearAllExceptThree pdpt_idx_range pdir_idx_range ptab_idx_range; intros; omega].
eassumption.
rewrite tulongsize.
clearAllExceptTwo muval ptab_idx_range; repeat vcgen.
rewrite pageval´.
clearAllExceptOne pdir_idx_range; omega.
rewrite pageval´.
clearAllExceptTwo pdir_idx_range muval; omega.
rewrite pageval, pageval´´, pageval´´´; repeat vcgen.
rewrite pageval, pageval´´, pageval´´´; repeat vcgen.
rewrite pageval, pageval´´, pageval´´´; repeat vcgen.
rewrite pageval´; clearAllExceptTwo muval pdir_idx_range; repeat vcgen.
rewrite pageval´; clearAllExceptTwo muval pdir_idx_range; repeat vcgen.
rewrite pageval, pageval´´, pageval´´´; repeat vcgen.
rewrite pageval, pageval´´, pageval´´´; repeat vcgen.
rewrite pageval, pageval´´, pageval´´´; repeat vcgen.
rewrite pageval´; clearAllExceptTwo muval pdir_idx_range; repeat vcgen.
rewrite pageval´; clearAllExceptTwo muval pdir_idx_range; repeat vcgen.
rewrite pageval, pageval´´, pageval´´´; repeat vcgen.
rewrite pageval, pageval´´, pageval´´´; repeat vcgen.
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´.
fbigstep (get_EPTE_body_correct (Genv.globalenv p) b0 H 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)))) H1.
Qed.
End GETEPTE.
Section SETEPTE.
Let L: compatlayer (cdata RData) := EPT_LOC ↦ v_ept.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SETEPTEBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bept_loc: block.
Hypothesis hept_loc1 : Genv.find_symbol ge EPT_LOC = Some bept_loc.
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) bept_loc
((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) →
exec_stmt ge env le ((m, d): mem) set_EPTE_body E0 le (m´, d) Out_normal.
Proof.
intros.
subst.
unfold set_EPTE_body.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tulongsize; intro tulongsize.
generalize teptstructsize; intro teptstructsize.
generalize tcharsize; intro tcharsize.
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(pageval: (sizeof (Tarray (Tpointer tuchar noattr) 1024 noattr)) = 4096)
by (simpl; reflexivity).
assert(pageval´: sizeof (Tarray tulong 512 noattr) = 4096)
by (simpl; reflexivity).
assert(pageval´´: sizeof (Tarray (Tarray tulong 512 noattr) 512 noattr) = 2097152)
by (simpl; reflexivity).
assert(pageval´´´: sizeof(Tarray (Tarray (Tpointer tuchar noattr) 1024 noattr) 4 noattr) = 16384)
by (simpl; reflexivity).
d12 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
rewrite pageval´, pageval´´, tulongsize.
rewrite Z.add_0_l.
unfold Mem.storev.
replace (24576 + 2097152 × Int.unsigned pdpt_idx + 4096 × Int.unsigned pdir_idx + 8 × Int.unsigned ptab_idx)
with ((6 + Int.unsigned pdpt_idx × 512 + Int.unsigned pdir_idx) × 4096 + Int.unsigned ptab_idx × 8) by omega.
unfold cast_int_long.
rewrite Int.unsigned_repr.
assumption.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
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.
fbigstep (set_EPTE_body_correct (Genv.globalenv p) b0 H m m0 l (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)))) H1.
Qed.
End SETEPTE.
End WithPrimitives.
End PPROCCODE.