Library mcertikos.mm.MPTBitCode
*********************************************************************** * * * 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 MPTBit.
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 PTNewGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealPTB.
Require Import XOmega.
Require Import AbstractDataType.
Require Import MPTBitCSource.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Module MPTBITCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
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}.
Section PTRESV2.
Let L: compatlayer (cdata RData) := palloc ↦ gensem palloc_spec
⊕ pt_insert ↦ gensem ptInsert0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PTResv2Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
palloc
Variable bpalloc: block.
Hypothesis hpalloc1 : Genv.find_symbol ge palloc = Some bpalloc.
Hypothesis hpalloc2 : Genv.find_funct_ptr ge bpalloc = Some (External (EF_external palloc (signature_of_type (Tcons tint Tnil) tint cc_default)) (Tcons tint Tnil) tint cc_default).
pt_insert2
Variable bptinsert: block.
Hypothesis hpt_insert1 : Genv.find_symbol ge pt_insert = Some bptinsert.
Hypothesis hpt_insert2 : Genv.find_funct_ptr ge bptinsert = Some (External (EF_external pt_insert (signature_of_type (Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))) tint cc_default)) (Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))) tint cc_default).
Lemma pt_resv2_body_correct: ∀ m d d´ env le proc_index vaddr perm proc_index2 vaddr2 perm2 v,
env = PTree.empty _ →
PTree.get tproc_index le = Some (Vint proc_index) →
PTree.get tvaddr le = Some (Vint vaddr) →
PTree.get tperm le = Some (Vint perm) →
PTree.get tproc_index2 le = Some (Vint proc_index2) →
PTree.get tvaddr2 le = Some (Vint vaddr2) →
PTree.get tperm2 le = Some (Vint perm2) →
ptResv2_spec (Int.unsigned proc_index) (Int.unsigned vaddr) (Int.unsigned perm) (Int.unsigned proc_index2) (Int.unsigned vaddr2) (Int.unsigned perm2) d = Some (d´, Int.unsigned v) →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) pt_resv2_body E0 le´ (m, d´) (Out_return (Some (Vint v, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold pt_resv2_body.
inversion H7.
functional inversion H6; subst.
{
rewrite <- Int.unsigned_repr with 1048577 in H8; try omega.
apply unsigned_inj in H8.
rewrite <- H8.
functional inversion H9;subst.
{
destruct _x.
omega.
}
{
change 0 with (Int.unsigned Int.zero) in H9.
esplit.
repeat vcgen.
}
{
change 0 with (Int.unsigned Int.zero) in H9.
esplit.
repeat vcgen.
}
}
{
rewrite <- Int.unsigned_repr with 1048577 in H8; try omega.
apply unsigned_inj in H8.
rewrite <- H8.
functional inversion H9;subst.
{
destruct _x0.
destruct a0.
generalize (valid_nps H17); intro npsrange.
esplit.
repeat vcgen.
}
{
omega.
}
{
omega.
}
}
{
functional inversion H8; subst.
{
destruct _x1.
destruct a0.
generalize (valid_nps H17); intro npsrange.
functional inversion H10; functional inversion H28; subst; esplit; repeat vcgen.
destruct _x2.
destruct a1.
simpl in a0.
instantiate (1:= v0).
repeat vcgen.
discharge_cmp.
omega.
destruct _x2.
destruct a1.
simpl in a0.
omega.
repeat vcgen.
repeat vcgen.
}
{
omega.
}
{
omega.
}
}
Grab Existential Variables.
apply le.
apply le.
apply le.
apply le.
apply le.
Qed.
End PTResv2Body.
Theorem pt_resv2_code_correct:
spec_le (pt_resv2 ↦ ptResv2_spec_low) (〚pt_resv2 ↦ f_pt_resv2 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (pt_resv2_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_pt_resv2)
(Vint n::Vint vadr::Vint p0::Vint n´::Vint vadr´::Vint p´::nil)
(create_undef_temps (fn_temps f_pt_resv2)))) H0.
Qed.
End PTRESV2.
Section PTNEW.
Let L: compatlayer (cdata RData) := is_used ↦ gensem is_pt_used_spec
⊕ set_bit ↦ gensem set_pt_bit_spec
⊕ container_split ↦ gensem container_split_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PTNewBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variables (id quota: int).
set_bit
Variable bsetbit: block.
Hypothesis hset_bit1 : Genv.find_symbol ge set_bit = Some bsetbit.
Hypothesis hset_bit2 : Genv.find_funct_ptr ge bsetbit = Some (External (EF_external set_bit (signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default)) (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
is_used
Variable bisused: block.
Hypothesis his_used1 : Genv.find_symbol ge is_used = Some bisused.
Hypothesis his_used2 : Genv.find_funct_ptr ge bisused = Some (External (EF_external is_used (signature_of_type (Tcons tint Tnil) tint cc_default)) (Tcons tint Tnil) tint cc_default).
container_split
Variable bsplit: block.
Hypothesis hsplit1 : Genv.find_symbol ge container_split = Some bsplit.
Hypothesis hsplit2 :
Genv.find_funct_ptr ge bsplit = Some (External
(EF_external container_split (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).
Section Pt_New_loop_proof.
Variable minit: memb.
Variable adt: RData.
Variable n: int.
Hypothesis n_property: 0 < Int.unsigned n < num_proc ∧ ZMap.get (Int.unsigned n) (pb adt) ≠ PTTrue ∨ Int.unsigned n = num_proc.
Hypothesis lt_n_not_free: (∀ x : Z, (0 < x < Int.unsigned n →
ZMap.get x (pb adt) = PTTrue)).
Hypothesis pe : pg adt = true.
Hypothesis ipt: ipt adt = true.
Hypothesis ihost: ihost adt = true.
Hypothesis ptb_defined: PTB_defined (pb adt) 0 num_proc.
Hypothesis hinv: high_level_invariant adt.
Definition pt_new_index_valid (index: int) : Prop := (ZMap.get (Int.unsigned index) (pb adt) ≠ PTTrue ∧ ∀ x, 0 < x < (Int.unsigned index) → ZMap.get x (pb adt) = PTTrue).
Lemma pt_new_index_unique : ∀ index1 index2, pt_new_index_valid index1 → pt_new_index_valid index2 → Int.unsigned index1 > 0 → Int.unsigned index2 > 0 → index1 = index2.
Proof.
intros index1 index2 valid1 valid2.
unfold pt_new_index_valid in ×.
destruct valid1 as [valid1a valid1b].
destruct valid2 as [valid2a valid2b].
case_eq (Int.unsigned index1).
intros.
omega.
intro.
case_eq (Int.unsigned index2).
intros.
omega.
intros.
rewrite H in ×.
rewrite H0 in ×.
generalize (Zgt_pos_0 p); intro ppos.
generalize (Zgt_pos_0 p0); intro p0pos.
assert(Z.pos p0 < Z.pos p → False).
intro.
assert(ZMap.get (Z.pos p0) (pb adt) = PTTrue).
apply valid1b.
split.
omega.
assumption.
contradiction.
assert(Z.pos p < Z.pos p0 → False).
intro.
assert(ZMap.get (Z.pos p) (pb adt) = PTTrue).
apply valid2b.
split.
omega.
assumption.
contradiction.
assert(Z.pos p = Z.pos p0) by omega.
assert(Int.unsigned index1 = Int.unsigned index2).
{
rewrite H.
rewrite H0.
rewrite H5.
trivial.
}
apply unsigned_inj.
assumption.
intros.
generalize (Zlt_neg_0 p0).
omega.
intros.
generalize (Zlt_neg_0 p).
omega.
Qed.
Lemma pt_new_index_invalid_used : ∀ index, 0 < Int.unsigned index < num_proc → is_pt_used_spec (Int.unsigned index) adt = Some 1 → ZMap.get (Int.unsigned index) (pb adt) = PTTrue.
Proof.
intros.
unfold is_pt_used_spec in H0.
rewrite ipt, ihost in ×.
rewrite zle_lt_true in H0.
destruct (ikern adt).
destruct (ZMap.get (Int.unsigned index) (pb adt)).
discriminate H0.
trivial.
discriminate H0.
discriminate H0.
omega.
Qed.
Lemma pt_new_index_valid_used : ∀ index, 0 < Int.unsigned index < num_proc → is_pt_used_spec (Int.unsigned index) adt = Some 0 → ZMap.get (Int.unsigned index) (pb adt) ≠ PTTrue.
Proof.
intros.
unfold is_pt_used_spec in H0.
rewrite ipt, ihost in ×.
rewrite zle_lt_true in H0.
destruct (ikern adt).
destruct (ZMap.get (Int.unsigned index) (pb adt)).
discriminate H0.
discriminate H0.
intro.
discriminate H1.
discriminate H0.
omega.
Qed.
Definition pt_new_loop_body_P (le: temp_env) (m: mem): Prop :=
le ! tid = Some (Vint id) ∧ le ! tquota = Some (Vint quota) ∧
PTree.get tpt_new_index le = Some (Vint Int.one) ∧
PTree.get tpt_new_free_index le = Some (Vint (Int.repr num_proc)) ∧
m = (minit, adt).
Definition pt_new_loop_body_Q (le : temp_env) (m: mem): Prop :=
le ! tid = Some (Vint id) ∧ le ! tquota = Some (Vint quota) ∧
PTree.get tpt_new_free_index le = Some (Vint n) ∧ m = (minit, adt).
Lemma pt_new_loop_correct_aux : LoopProofSimpleWhile.t pt_new_while_condition pt_new_while_body ge (PTree.empty _) (pt_new_loop_body_P) (pt_new_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ index,
le ! tid = Some (Vint id) ∧ le ! tquota = Some (Vint quota) ∧
PTree.get tpt_new_index le = Some (Vint index) ∧
(0 < Int.unsigned index ≤ num_proc) ∧
m = (minit, adt) ∧
w = num_proc - Int.unsigned index ∧
(PTree.get tpt_new_free_index le = Some (Vint n) ∨
PTree.get tpt_new_free_index le = Some (Vint (Int.repr num_proc)) ∧ (Int.unsigned index ≤ Int.unsigned n) ∧ (∀ x: Z, (0 < x < Int.unsigned index) → ZMap.get x (pb adt) = PTTrue))
)
.
apply Zwf_well_founded.
intros.
unfold pt_new_loop_body_P in H.
destruct H as [Hid [Hquota [ptnewindexle tmpH]]].
destruct tmpH as [ptnewfreeindexle msubst].
subst.
change (Int.one) with (Int.repr 1) in ptnewindexle.
esplit. esplit.
repeat vcgen.
right.
repeat vcgen.
intros.
unfold pt_new_while_condition.
unfold pt_new_while_body.
unfold pt_new_loop_body_Q.
destruct H as [index tmpH].
destruct tmpH as [Hid [Hquota [ptnewindexle tmpH]]].
destruct tmpH as [indexrange tmpH].
destruct tmpH as [msubst tmpH].
destruct tmpH as [nval casefreeindex].
destruct indexrange as [indexlow indexhigh].
apply Zle_lt_or_eq in indexhigh.
subst.
destruct hinv.
generalize (valid_iptt ipt); intro ikern.
Caseeq indexhigh.
intro indexhigh.
Caseeq casefreeindex.
intro freeindexle.
Caseeq n_property.
{
intro tmpH.
destruct tmpH as [nrange nfree].
esplit. esplit.
repeat vcgen.
}
{
intro nval.
esplit. esplit.
repeat vcgen.
assert(usedcase: is_pt_used_spec (Int.unsigned index) adt = Some 0 ∨
is_pt_used_spec (Int.unsigned index) adt = Some 1).
unfold is_pt_used_spec.
unfold PTB_defined in ptb_defined.
assert(tmp: 0 ≤ Int.unsigned index < num_proc) by omega.
specialize (ptb_defined (Int.unsigned index) tmp).
rewrite zle_lt_true.
destruct (ZMap.get (Int.unsigned index) (pb adt)).
assert(PTBUndef = PTBUndef) by reflexivity.
contradiction.
rewrite ipt, ihost, ikern; right; trivial.
rewrite ipt, ihost, ikern; left; trivial.
omega.
Caseeq usedcase.
intro.
unfold is_pt_used_spec in H0.
rewrite ipt, ihost, ikern in H0.
assert(0 < Int.unsigned index < Int.unsigned n) by omega.
generalize (lt_n_not_free (Int.unsigned index) H1); intro.
rewrite zle_lt_true, H2 in H0.
discriminate H0.
omega.
intro.
esplit. esplit.
change 1 with (Int.unsigned Int.one) in H0.
repeat vcgen.
∃ (num_proc - Int.unsigned index - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
repeat vcgen.
rewrite <- Int.repr_unsigned with n in freeindexle.
rewrite nval in freeindexle.
assumption.
apply lt_n_not_free; eauto.
omega.
}
intro tcond.
destruct tcond as [freeindexle tcond].
destruct tcond as [indleqn leind].
Caseeq n_property.
{
intro tmpH.
destruct tmpH as [nrange nfree].
∃ (Vint Int.one), true.
repeat vcgen.
assert(usedcase: is_pt_used_spec (Int.unsigned index) adt = Some 0 ∨
is_pt_used_spec (Int.unsigned index) adt = Some 1).
unfold is_pt_used_spec.
unfold PTB_defined in ptb_defined.
assert(tmp: 0 ≤ Int.unsigned index < num_proc) by omega.
specialize (ptb_defined (Int.unsigned index) tmp).
rewrite zle_lt_true.
destruct (ZMap.get (Int.unsigned index) (pb adt)).
assert(PTBUndef = PTBUndef) by reflexivity.
contradiction.
rewrite ipt, ihost, ikern; right; trivial.
rewrite ipt, ihost, ikern; left; trivial.
omega.
Caseeq usedcase.
intro.
esplit. esplit.
change 0 with (Int.unsigned Int.zero) in H0.
repeat vcgen.
∃ (num_proc - Int.unsigned index - 1).
repeat vcgen.
esplit.
repeat vcgen.
left.
rewrite PTree.gso.
rewrite PTree.gss.
f_equal.
f_equal.
apply pt_new_index_unique.
unfold pt_new_index_valid.
split.
apply pt_new_index_valid_used.
omega.
change 0 with (Int.unsigned Int.zero).
assumption.
assumption.
unfold pt_new_index_valid.
auto.
vcgen.
omega.
vcgen.
intro.
esplit. esplit.
change 1 with (Int.unsigned Int.one) in H0.
repeat vcgen.
∃ (num_proc - Int.unsigned index - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
repeat vcgen.
assert(Int.unsigned index ≠ Int.unsigned n).
intro.
apply pt_new_index_invalid_used in H0.
rewrite H1 in ×.
contradiction.
omega.
omega.
assert(LessOrEqual: 0≤ x< Int.unsigned index ∨ x = Int.unsigned index).
omega.
Caseeq LessOrEqual.
intros.
apply leind.
omega.
intros.
subst x.
apply pt_new_index_invalid_used in H0.
assumption.
omega.
}
{
intro nval.
∃ (Vint Int.one), true.
repeat vcgen.
assert(usedcase: is_pt_used_spec (Int.unsigned index) adt = Some 0 ∨
is_pt_used_spec (Int.unsigned index) adt = Some 1).
unfold is_pt_used_spec.
unfold PTB_defined in ptb_defined.
assert(tmp: 0 ≤ Int.unsigned index < num_proc) by omega.
specialize (ptb_defined (Int.unsigned index) tmp).
rewrite zle_lt_true.
destruct (ZMap.get (Int.unsigned index) (pb adt)).
assert(PTBUndef = PTBUndef) by reflexivity.
contradiction.
rewrite ipt, ihost, ikern; right; trivial.
rewrite ipt, ihost, ikern; left; trivial.
omega.
Caseeq usedcase.
intro.
unfold is_pt_used_spec in H0.
rewrite ipt, ihost, ikern in H0.
assert(0 < Int.unsigned index < Int.unsigned n) by omega.
generalize (lt_n_not_free (Int.unsigned index) H1); intro.
rewrite zle_lt_true, H2 in H0.
discriminate H0.
omega.
intro.
esplit. esplit.
change 1 with (Int.unsigned Int.one) in H0.
repeat vcgen.
∃ (num_proc - Int.unsigned index - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
repeat vcgen.
apply lt_n_not_free; eauto.
omega.
}
intros.
Caseeq casefreeindex.
intro.
esplit. esplit.
repeat vcgen.
intro.
destruct H0 as [indexle H0].
destruct H0 as [indexrange xfree].
Caseeq n_property.
{
intro tmpH.
destruct tmpH as [nrange nfree].
esplit. esplit.
repeat vcgen.
}
{
intro nval.
esplit. esplit.
repeat vcgen.
rewrite <- Int.repr_unsigned with n.
rewrite nval.
assumption.
}
Grab Existential Variables.
apply true.
apply Vundef.
Qed.
End Pt_New_loop_proof.
Lemma pt_new_loop_correct:
∀ m adt le n,
pg adt = true →
ipt adt = true →
ihost adt = true →
0 < Int.unsigned n < num_proc ∧ ZMap.get (Int.unsigned n) (pb adt) ≠ PTTrue ∨ Int.unsigned n = num_proc →
(∀ x : Z, (0 < x < Int.unsigned n →
ZMap.get x (pb adt) = PTTrue)) →
PTB_defined (pb adt) 0 num_proc →
high_level_invariant adt →
le ! tid = Some (Vint id) → le ! tquota = Some (Vint quota) →
le ! tpt_new_index = Some (Vint Int.one) →
le ! tpt_new_free_index = Some (Vint (Int.repr num_proc)) →
∃ le´, exec_stmt ge (PTree.empty _) le ((m, adt): mem)
(Swhile pt_new_while_condition pt_new_while_body) E0 le´ (m, adt) Out_normal ∧
le´ ! tid = Some (Vint id) ∧ le´ ! tquota = Some (Vint quota) ∧
le´ ! tpt_new_free_index = Some (Vint n).
Proof.
intros m adt le n pe ipt ihost n_property lt_n_not_free ptb_defined hinv Hid Hquota leindex lefreeindex.
generalize (pt_new_loop_correct_aux m adt n n_property lt_n_not_free ipt ihost ptb_defined hinv).
intro LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, adt) _)).
intro pre.
destruct pre as [le´ pre].
destruct pre as [m´ pre].
destruct pre as [pre1 pre2].
∃ le´.
unfold pt_new_loop_body_Q in pre2.
decompose [and] pre2; subst.
eauto.
unfold pt_new_loop_body_P.
auto.
Qed.
Lemma pt_new_body_correct:
∀ m d d´ env le n,
env = PTree.empty _ →
pt_new_spec (Int.unsigned id) (Int.unsigned quota) d = Some (d´, Int.unsigned n) →
cused (ZMap.get (Int.unsigned n) (AC d)) = false →
high_level_invariant d →
le ! tid = Some (Vint id) → le ! tquota = Some (Vint quota) →
∃ le´,
exec_stmt ge env le ((m, d): mem) pt_new_body E0 le´ (m, d´) (Out_return (Some (Vint n, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold pt_new_body.
functional inversion H0.
{
destruct _x1.
destruct a0.
subst.
exploit (pt_new_loop_correct m d
(PTree.set tpt_new_free_index (Vint (Int.repr 64))
(PTree.set tpt_new_index (Vint (Int.repr 1)) le)) n); repeat vcgen.
destruct H.
decompose [and] H.
esplit.
repeat vcgen.
unfold set_pt_bit_spec.
rewrite H9, H10, H11.
rewrite zle_lt_true.
unfold ZtoPTBit.
reflexivity.
omega.
unfold container_split_spec; simpl; inv H2.
rewrite H11, H10, H8, H1.
destruct (zlt_lt 0 (Int.unsigned n) 64); try omega.
rewrite H7; auto.
}
{
subst.
destruct (first_free_PT (pb d´) 64).
destruct s.
destruct a.
destruct H2.
inversion H15.
exploit (pt_new_loop_correct m d´ (PTree.set tpt_new_free_index (Vint (Int.repr 64))
(PTree.set tpt_new_index (Vint (Int.repr 1)) le)) n); repeat vcgen.
apply e; eauto.
omega.
destruct H.
decompose [and] H.
esplit.
repeat vcgen.
}
Qed.
End PTNewBody.
Theorem pt_new_code_correct:
spec_le (pt_new ↦ pt_new_spec_low) (〚pt_new ↦ f_pt_new 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (pt_new_body_correct s (Genv.globalenv p) makeglobalenv id q b1 Hb1fs Hb1fp b0 Hb0fs Hb0fp
b2 Hb2fs Hb2fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_pt_new)
(Vint id :: Vint q :: nil)
(create_undef_temps (fn_temps f_pt_new)))) H0.
Qed.
End PTNEW.
Section PTRESV.
Let L: compatlayer (cdata RData) := palloc ↦ gensem palloc_spec
⊕ pt_insert ↦ gensem ptInsert0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PTResvBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
palloc
Variable bpalloc: block.
Hypothesis hpalloc1 : Genv.find_symbol ge palloc = Some bpalloc.
Hypothesis hpalloc2 : Genv.find_funct_ptr ge bpalloc = Some (External (EF_external palloc (signature_of_type (Tcons tint Tnil) tint cc_default)) (Tcons tint Tnil) tint cc_default).
pt_insert2
Variable bptinsert: block.
Hypothesis hpt_insert1 : Genv.find_symbol ge pt_insert = Some bptinsert.
Hypothesis hpt_insert2 : Genv.find_funct_ptr ge bptinsert = Some (External (EF_external pt_insert (signature_of_type (Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))) tint cc_default)) (Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))) tint cc_default).
Lemma pt_resv_body_correct: ∀ m d d´ env le proc_index vaddr perm v,
env = PTree.empty _ →
PTree.get tproc_index le = Some (Vint proc_index) →
PTree.get tvaddr le = Some (Vint vaddr) →
PTree.get tperm le = Some (Vint perm) →
ptResv_spec (Int.unsigned proc_index)
(Int.unsigned vaddr) (Int.unsigned perm) d = Some (d´, Int.unsigned v) →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) pt_resv_body E0 le´ (m, d´) (Out_return (Some (Vint v, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold pt_resv_body.
inversion H4.
functional inversion H3; subst.
{
rewrite <- Int.unsigned_repr with 1048577 in H5; try omega.
apply unsigned_inj in H5.
rewrite <- H5.
functional inversion H6;subst.
{
destruct _x.
destruct a0.
generalize (valid_nps H12); intro npsrange.
esplit.
repeat vcgen.
}
{
change 0 with (Int.unsigned Int.zero) in H6.
esplit.
repeat vcgen.
}
{
change 0 with (Int.unsigned Int.zero) in H6.
esplit.
repeat vcgen.
}
}
{
functional inversion H5; subst.
{
destruct _x0.
destruct a0.
generalize (valid_nps H12); intro npsrange.
esplit.
repeat vcgen.
}
{
change 0 with (Int.unsigned Int.zero) in H5.
esplit.
repeat vcgen.
}
{
change 0 with (Int.unsigned Int.zero) in H5.
esplit.
repeat vcgen.
}
}
Grab Existential Variables.
apply le.
apply le.
apply le.
Qed.
End PTResvBody.
Theorem pt_resv_code_correct:
spec_le (pt_resv ↦ ptResv_spec_low) (〚pt_resv ↦ f_pt_resv 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (pt_resv_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_pt_resv)
(Vint n::Vint vadr::Vint p0::nil)
(create_undef_temps (fn_temps f_pt_resv)))) H0.
Qed.
End PTRESV.
Section PMAPINIT.
Let L: compatlayer (cdata RData) := set_bit ↦ gensem set_pt_bit_spec
⊕ pt_init ↦ gensem pt_init_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 PMapInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
set_bit
Variable bsetbit: block.
Hypothesis hset_bit1 : Genv.find_symbol ge set_bit = Some bsetbit.
Hypothesis hset_bit2 : Genv.find_funct_ptr ge bsetbit = Some (External (EF_external set_bit (signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default)) (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
pt_init
Variable bptinit: block.
Hypothesis hpt_init1 : Genv.find_symbol ge pt_init = Some bptinit.
Hypothesis hpt_init2 : Genv.find_funct_ptr ge bptinit = Some (External (EF_external pt_init (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
Definition pmap_init_mk_rdata adt index := adt {pb: Calculate_pb (Z.to_nat index) (pb adt)}.
Section Pmap_Init_loop_proof.
Variable minit: memb.
Variable adt: RData.
Hypothesis iihost: ihost adt = true.
Hypothesis hinv: high_level_invariant adt.
Definition pmap_init_loop_body_P (le: temp_env) (m: mem): Prop :=
PTree.get ti le = Some (Vint Int.one) ∧
ipt adt = true ∧
ihost adt = true ∧
m = (minit, pmap_init_mk_rdata adt 0).
Definition pmap_init_loop_body_Q (le : temp_env) (m: mem): Prop :=
m = (minit, pmap_init_mk_rdata adt (num_proc - 1)).
Lemma pmap_init_loop_correct_aux : LoopProofSimpleWhile.t pmap_init_while_condition pmap_init_while_body ge (PTree.empty _) (pmap_init_loop_body_P) (pmap_init_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le (m: mem) w ⇒ ∃ i,
PTree.get ti le = Some (Vint i) ∧
1 ≤ Int.unsigned i ≤ num_proc ∧
ipt adt = true ∧
ihost adt = true ∧
m = (minit, pmap_init_mk_rdata adt (Int.unsigned i - 1)) ∧
w = num_proc - Int.unsigned i
)
.
apply Zwf_well_founded.
unfold pmap_init_loop_body_P.
intros.
destruct H as [tile tmpH].
destruct tmpH as [ipt tmpH].
destruct tmpH as [ihost mval].
subst.
esplit. esplit.
change (Int.one) with (Int.repr 1) in tile.
repeat vcgen.
intros.
destruct H as [i tmpH].
destruct tmpH as [tile tmpH].
destruct tmpH as [irange tmpH].
destruct tmpH as [ipt tmpH].
destruct tmpH as [ihost tmpH].
destruct tmpH as [mval nval].
unfold pmap_init_while_body.
unfold pmap_init_while_condition.
destruct irange as [ilow ihigh].
apply Zle_lt_or_eq in ihigh.
destruct m.
injection mval; intros; subst.
destruct hinv.
generalize (valid_iptt ipt); intro ikern.
Caseeq ihigh.
intro ihigh.
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
unfold set_pt_bit_spec.
simpl.
rewrite ipt, ihost, ikern.
rewrite zle_lt_true.
reflexivity.
repeat vcgen.
∃ (num_proc - Int.unsigned i - 1).
repeat vcgen.
esplit.
repeat vcgen.
unfold pmap_init_mk_rdata.
assert(tmpeq: Int.unsigned i + 1 - 1 = Int.unsigned i - 1 + 1) by omega; rewrite tmpeq; clear tmpeq.
change (Int.unsigned i - 1 + 1) with (Z.succ (Int.unsigned i - 1)).
rewrite Z2Nat.inj_succ with (n:=(Int.unsigned i - 1)).
assert(icase: Int.unsigned i - 1 = 0 ∨ Int.unsigned i - 1 > 0) by omega.
Caseeq icase.
intro.
rewrite H0.
unfold Z.to_nat.
assert(tmpeq: Int.unsigned i = 1) by omega; rewrite tmpeq; clear tmpeq.
unfold Calculate_pb.
trivial.
intro.
Opaque Z.of_nat.
simpl.
replace (Z.of_nat (S (Z.to_nat (Int.unsigned i - 1)))) with (Z.succ(Z.of_nat (Z.to_nat (Int.unsigned i - 1)))) by (rewrite <- Nat2Z.inj_succ; reflexivity).
rewrite Z2Nat.id.
unfold Z.succ.
replace (Int.unsigned i - 1 + 1) with (Int.unsigned i) by omega.
case_eq (Z.to_nat (Int.unsigned i - 1)).
intro.
assert(Int.unsigned i - 1 = 0).
{
change 0%nat with (Z.to_nat 0) in H1.
apply Z2Nat.inj; eauto; omega.
}
omega.
intros.
reflexivity.
omega.
omega.
intro ival.
unfold pmap_init_loop_body_Q.
esplit. esplit.
repeat vcgen.
rewrite ival.
reflexivity.
Qed.
End Pmap_Init_loop_proof.
Lemma pmap_init_loop_correct: ∀ m d d´ d´´ le,
PTree.get ti le = Some (Vint Int.one) →
high_level_invariant d →
ipt d = true →
ihost d = true →
d´ = pmap_init_mk_rdata d 0 →
d´´ = pmap_init_mk_rdata d (num_proc - 1) →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d´): mem) (Swhile pmap_init_while_condition pmap_init_while_body) E0 le´ (m, d´´) Out_normal.
Proof.
intros m d d´ d´´ le tile hinv ipt ihost m´val m´´val.
generalize (pmap_init_loop_correct_aux m d hinv).
unfold pmap_init_loop_body_P.
unfold pmap_init_loop_body_Q.
intro LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d´) _)).
intro pre.
destruct pre as [le´´ tmppre].
destruct tmppre as [m´´´ tmppre].
destruct tmppre as [stmp m´´´val].
∃ le´´.
subst.
repeat vcgen.
subst.
repeat vcgen.
Qed.
Lemma deq: ∀ d,
((((((((((((d { ioapic / s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))}) {
lapic
: (((mkLApicData
{|
LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |}) { l1 : l1 (lapic d)}) { l2
: l2 (lapic d)}) { l3 : l3 (lapic d)}}) { ioapic
: ((ioapic d) { s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))}) {
s
: (ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))) {
CurrentIrq : None}}}) { vmxinfo : real_vmxinfo}) { pg
: true}) { LAT : real_LAT (LAT d)}) { nps : real_nps}) { AC
: AC_init}) { init : true}) { PT : 0}) { ptpool
: real_pt (ptpool d)}) { idpde : CalRealIDPDE.real_idpde (idpde d)})
{ pb : Calculate_pb (Z.to_nat (64 - 1)) (pb d)} = ((((((((((((d { ioapic / s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))}) {
lapic
: (((mkLApicData
{|
LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |}) { l1 :
l1 (lapic d)}) { l2 : l2 (lapic d)}) { l3
: l3 (lapic d)}}) { ioapic
: ((ioapic d) { s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ s
: (ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))) {
CurrentIrq : None}}}) { vmxinfo : real_vmxinfo}) {
pg : true}) { LAT : real_LAT (LAT d)}) { nps : real_nps})
{ AC : AC_init}) { init : true}) { PT : 0}) { ptpool
: real_pt (ptpool d)}) { idpde
: CalRealIDPDE.real_idpde (idpde d)}) { pb
: Calculate_pb (Z.to_nat (64 - 1))
(pb
(((((((((((d { ioapic / s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1))}) {
lapic
: (((mkLApicData
{|
LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |}) { l1 :
l1 (lapic d)}) { l2 :
l2 (lapic d)}) { l3 :
l3 (lapic d)}}) { ioapic
: ((ioapic d) { s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1))}) {
s
: (ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1))) {
CurrentIrq : None}}}) { vmxinfo : real_vmxinfo})
{ pg : true}) { LAT : real_LAT (LAT d)}) { nps
: real_nps}) { AC : AC_init}) { init : true}) { PT
: 0}) { ptpool : real_pt (ptpool d)}) { idpde
: CalRealIDPDE.real_idpde (idpde d)})}.
Proof.
reflexivity.
Qed.
Lemma deq2: ∀ d,
((((((((((((d { ioapic / s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))}) {
lapic
: (((mkLApicData
{|
LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |}) { l1 : l1 (lapic d)}) { l2
: l2 (lapic d)}) { l3 : l3 (lapic d)}}) { ioapic
: ((ioapic d) { s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))}) {
s
: (ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))) {
CurrentIrq : None}}}) { vmxinfo : real_vmxinfo}) { pg
: true}) { LAT : real_LAT (LAT d)}) { nps : real_nps}) { AC
: AC_init}) { init : true}) { PT : 0}) { ptpool
: real_pt (ptpool d)}) { idpde : CalRealIDPDE.real_idpde (idpde d)})
{ pb : ZMap.set 0 PTTrue (pb d)} = ((((((((((((d { ioapic / s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))}) {
lapic
: (((mkLApicData
{|
LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |}) { l1 :
l1 (lapic d)}) { l2 : l2 (lapic d)}) { l3
: l3 (lapic d)}}) { ioapic
: ((ioapic d) { s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ s
: (ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))) {
CurrentIrq : None}}}) { vmxinfo : real_vmxinfo}) {
pg : true}) { LAT : real_LAT (LAT d)}) { nps : real_nps})
{ AC : AC_init}) { init : true}) { PT : 0}) { ptpool
: real_pt (ptpool d)}) { idpde
: CalRealIDPDE.real_idpde (idpde d)}) { pb
: Calculate_pb (Z.to_nat 0)
(pb
(((((((((((d { ioapic / s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1))}) {
lapic
: (((mkLApicData
{|
LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |}) { l1 :
l1 (lapic d)}) { l2 :
l2 (lapic d)}) { l3 :
l3 (lapic d)}}) { ioapic
: ((ioapic d) { s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1))}) {
s
: (ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1))) {
CurrentIrq : None}}}) { vmxinfo : real_vmxinfo})
{ pg : true}) { LAT : real_LAT (LAT d)}) { nps
: real_nps}) { AC : AC_init}) { init : true}) { PT
: 0}) { ptpool : real_pt (ptpool d)}) { idpde
: CalRealIDPDE.real_idpde (idpde d)})}.
Proof.
reflexivity.
Qed.
Lemma pmap_init_body_correct: ∀ m d d´ env le mbi_adr,
env = PTree.empty _ →
PTree.get tmbi_adr le = Some (Vint mbi_adr) →
PTree.get ti le = Some Vundef →
pmap_init_spec (Int.unsigned mbi_adr) d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) pmap_init_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
functional inversion H2.
subst.
simpl in ×.
unfold pmap_init_body.
set (di := ((((((((((((d { ioapic / s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))}) {
lapic
: (((mkLApicData
{|
LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |}) { l1 : l1 (lapic d)}) { l2
: l2 (lapic d)}) { l3 : l3 (lapic d)}}) { ioapic
: ((ioapic d) { s
: ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))}) {
s
: (ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))) {
CurrentIrq : None}}}) { vmxinfo : real_vmxinfo}) { pg
: true}) { LAT : real_LAT (LAT d)}) { nps : real_nps}) { AC
: AC_init}) { init : true}) { PT : 0}) { ptpool
: real_pt (ptpool d)}) { idpde : CalRealIDPDE.real_idpde (idpde d)})).
exploit (pmap_init_loop_correct m di (pmap_init_mk_rdata di 0) (pmap_init_mk_rdata di (num_proc - 1))
(PTree.set ti (Vint (Int.repr 1))
(set_opttemp None Vundef (set_opttemp None Vundef le)))); try rewrite <- H; try assumption; try reflexivity; try (rewrite PTree.gss; reflexivity).
generalize pt_init_inv; intro.
inversion H.
eapply semprops_high_level_invariant.
repeat econstructor.
unfold pt_init_spec.
instantiate (1:= d).
rewrite H4, H5, H6, H7, H8, H9, H10, H11.
reflexivity.
assumption.
intro stmt.
unfold di in ×.
destruct stmt.
∃ x.
change E0 with (E0 ** E0).
econstructor.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
vcgen.
unfold pt_init_spec.
rewrite H4, H5, H6, H7, H8, H9, H10, H11.
reflexivity.
change E0 with (E0 ** E0).
econstructor.
repeat vcgen.
unfold set_pt_bit_spec.
simpl.
rewrite H4, H5, H6.
reflexivity.
change E0 with (E0 ** E0).
econstructor.
repeat vcgen.
unfold pmap_init_mk_rdata, real_ptb in ×.
Opaque Z.of_nat Z.to_nat Z.sub Z.add.
rewrite <- deq in H.
rewrite <- deq2 in H.
apply H.
Grab Existential Variables.
∃ 0.
vm_compute.
auto.
Qed.
End PMapInitBody.
Theorem pmap_init_code_correct:
spec_le (pmap_init ↦ pmap_init_spec_low) (〚pmap_init ↦ f_pmap_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (pmap_init_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_pmap_init)
(Vint mbi_adr::nil)
(create_undef_temps (fn_temps f_pmap_init)))) H0.
Qed.
End PMAPINIT.
End WithPrimitives.
End MPTBITCODE.