Library mcertikos.proc.PSleeperCode
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 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 TacticsForTesting.
Require Import AbstractDataType.
Require Import QueueIntroGenSpec.
Require Import PSleeperCSource.
Require Import PSleeper.
Module PSLEEPERCODE.
Section WithPrimitives.
Context `{real_params_ops : RealParamsOps}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{multi_oracle_prop: MultiOracleProp}.
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 t_struct_TCB_node_size :
sizeof t_struct_TCB_node = 16%Z.
Proof. simpl; auto. Qed.
Lemma t_struct_TDQ_node_size :
sizeof t_struct_TDQ_node = 8%Z.
Proof. simpl; auto. Qed.
Section GETSTATE.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetStateBody.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma get_state_body_correct: ∀ m d env le proc_index state,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
Mem.load Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16)
= Some (Vint state) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_get_state_body E0 le (m, d)
(Out_return (Some (Vint state, tint))).
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_get_state_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 0) with (Int.unsigned proc_index × 16); try ring.
simpl.
repeat vcgen.
Qed.
End GetStateBody.
Theorem get_state_code_correct:
spec_le (get_state ↦ get_state_spec_low) (〚get_state ↦ f_tcb_get_state 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_state_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_get_state)
(Vint n::nil)
(create_undef_temps (fn_temps f_tcb_get_state)))) m´.
Qed.
End GETSTATE.
Section TCBGETCPUID.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TcbGetCPUIDBody.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma tcb_get_CPU_ID_body_correct: ∀ m d env le proc_index cpu_id,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
Mem.load Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16 + 4)
= Some (Vint cpu_id) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_get_CPU_ID_state_body E0 le (m, d)
(Out_return (Some (Vint cpu_id, tint))).
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_get_CPU_ID_state_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 4) with (Int.unsigned proc_index × 16 + 4); try ring.
simpl.
repeat vcgen.
Qed.
End TcbGetCPUIDBody.
Theorem tcb_get_CPU_ID_code_correct:
spec_le (tcb_get_CPU_ID ↦ tcb_get_CPU_ID_spec_low) (〚tcb_get_CPU_ID ↦ f_tcb_get_CPU_ID_state 〛L).
Proof.
fbigstep_pre L.
fbigstep (tcb_get_CPU_ID_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_get_CPU_ID_state)
(Vint n::nil)
(create_undef_temps (fn_temps f_tcb_get_CPU_ID_state)))) m´.
Qed.
End TCBGETCPUID.
Section GETPREV.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetPrevBody.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma get_prev_body_correct: ∀ m d env le proc_index prev,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
Mem.load Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16 + 8)
= Some (Vint prev) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_get_prev_body E0 le (m, d)
(Out_return (Some (Vint prev, tint))).
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_get_prev_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 8) with (Int.unsigned proc_index × 16 + 8); try ring.
simpl.
repeat vcgen.
Qed.
End GetPrevBody.
Theorem get_prev_code_correct:
spec_le (get_prev ↦ get_prev_spec_low) (〚get_prev ↦ f_tcb_get_prev 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_prev_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_get_prev)
(Vint n::nil)
(create_undef_temps (fn_temps f_tcb_get_prev)))) m´.
Qed.
End GETPREV.
Section GETNEXT.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetNextBody.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma get_next_body_correct: ∀ m d env le proc_index next,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
Mem.load Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16 + 12)
= Some (Vint next) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_get_next_body E0 le (m, d)
(Out_return (Some (Vint next, tint))).
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_get_next_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 12) with (Int.unsigned proc_index × 16 + 12); try ring.
simpl.
repeat vcgen.
Qed.
End GetNextBody.
Theorem get_next_code_correct:
spec_le (get_next ↦ get_next_spec_low) (〚get_next ↦ f_tcb_get_next 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_next_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_get_next)
(Vint n::nil)
(create_undef_temps (fn_temps f_tcb_get_next)))) m´.
Qed.
End GETNEXT.
Section SETSTATE.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetStateBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma set_state_body_correct: ∀ m m´ d env le proc_index state,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
PTree.get _state le = Some (Vint state) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16)
(Vint state) = Some (m´, d) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_set_state_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_set_state_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 0) with (Int.unsigned proc_index × 16); try ring.
simpl.
repeat vcgen.
Qed.
End SetStateBody.
Theorem set_state_code_correct:
spec_le (set_state ↦ set_state_spec_low) (〚set_state ↦ f_tcb_set_state 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
fbigstep (set_state_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_set_state)
(Vint n::Vint v::nil)
(create_undef_temps (fn_temps f_tcb_set_state)))) H0.
Qed.
End SETSTATE.
Section TCBSETCPUID.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TcbSetCPUIDBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma tcb_set_CPU_ID_body_correct: ∀ m m´ d env le proc_index cpu_id,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
PTree.get _cpu_id le = Some (Vint cpu_id) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16 + 4)
(Vint cpu_id) = Some (m´, d) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_set_CPU_ID_state_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_set_CPU_ID_state_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 4) with (Int.unsigned proc_index × 16 + 4); try ring.
simpl.
repeat vcgen.
Qed.
End TcbSetCPUIDBody.
Theorem tcb_set_CPU_ID_code_correct:
spec_le (tcb_set_CPU_ID ↦ tcb_set_CPU_ID_spec_low) (〚tcb_set_CPU_ID ↦ f_tcb_set_CPU_ID_state〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
fbigstep (tcb_set_CPU_ID_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_set_CPU_ID_state)
(Vint n::Vint v::nil)
(create_undef_temps (fn_temps f_tcb_set_CPU_ID_state)))) H0.
Qed.
End TCBSETCPUID.
Section SETPREV.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetPrevBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma set_prev_body_correct: ∀ m m´ d env le proc_index prev,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
PTree.get _prev le = Some (Vint prev) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16 + 8)
(Vint prev) = Some (m´, d) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_set_prev_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_set_prev_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 8) with (Int.unsigned proc_index × 16 + 8); try ring.
simpl.
repeat vcgen.
Qed.
End SetPrevBody.
Theorem set_prev_code_correct:
spec_le (set_prev ↦ set_prev_spec_low) (〚set_prev ↦ f_tcb_set_prev 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
fbigstep (set_prev_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_set_prev)
(Vint n::Vint v::nil)
(create_undef_temps (fn_temps f_tcb_set_prev)))) H0.
Qed.
End SETPREV.
Section SETNEXT.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetNextBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma set_next_body_correct: ∀ m m´ d env le proc_index next,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
PTree.get _next le = Some (Vint next) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16 + 12)
(Vint next) = Some (m´, d) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_set_next_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_set_next_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 12) with (Int.unsigned proc_index × 16 + 12); try ring.
simpl.
repeat vcgen.
Qed.
End SetNextBody.
Theorem set_next_code_correct:
spec_le (set_next ↦ set_next_spec_low) (〚set_next ↦ f_tcb_set_next 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
fbigstep (set_next_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_set_next)
(Vint n::Vint v::nil)
(create_undef_temps (fn_temps f_tcb_set_next)))) H0.
Qed.
End SETNEXT.
Section TCBINIT.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TCBInitBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis hbtcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma tcb_init_body_correct: ∀ m0 m1 m2 m3 m4 d env le proc_index,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
Mem.store Mint32 (m0, d) btcbpool_loc (Int.unsigned proc_index × 16)
(Vint (Int.repr TSTATE_DEAD)) = Some (m1, d) →
Mem.store Mint32 (m1, d) btcbpool_loc (Int.unsigned proc_index × 16 + 4)
(Vint (Int.repr 0)) = Some (m2, d) →
Mem.store Mint32 (m2, d) btcbpool_loc (Int.unsigned proc_index × 16 + 8)
(Vint (Int.repr num_proc)) = Some (m3, d) →
Mem.store Mint32 (m3, d) btcbpool_loc (Int.unsigned proc_index × 16 + 12)
(Vint (Int.repr num_proc)) = Some (m4, d) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m0, d): mem) f_tcb_init_body E0 le (m4, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_init_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
- rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 0) with (Int.unsigned proc_index × 16); try ring.
simpl.
repeat vcgen.
- rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 4) with (Int.unsigned proc_index × 16 + 4); try ring.
simpl.
repeat vcgen.
- rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 8) with (Int.unsigned proc_index × 16 + 8); try ring.
simpl.
repeat vcgen.
- rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 12) with (Int.unsigned proc_index × 16 + 12); try ring.
simpl.
repeat vcgen.
Qed.
End TCBInitBody.
Theorem tcb_init_code_correct:
spec_le (tcb_init ↦ tcb_init_spec_low) (〚tcb_init ↦ f_tcb_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m, m´, m1, m2, m3, H1.
destruct H0; destruct H2; destruct H3; simpl in ×.
fbigstep (tcb_init_body_correct (Genv.globalenv p) b0 H m m1 m2 m3 m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_init)
(Vint n::nil)
(create_undef_temps (fn_temps f_tcb_init)))) muval.
Qed.
End TCBINIT.
Section GETHEAD.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetHeadBody.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis hbtcbqpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma get_head_body_correct: ∀ m d env le chan_index head,
env = PTree.empty _ →
PTree.get _chan_index le = Some (Vint chan_index) →
Mem.load Mint32 (m, d) btcbpool_loc ((Int.unsigned chan_index) × 8 + num_proc × 16)
= Some (Vint head) →
0 ≤ (Int.unsigned chan_index) < num_chan →
exec_stmt ge env le ((m, d): mem) f_tdq_get_head_body E0 le (m, d)
(Out_return (Some (Vint head, tint))).
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tdq_get_head_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; unfold t_struct_TDQ_node in *; subst.
repeat vcgen.
rewrite H.
replace 16384 with (num_proc × 16); try ring.
replace (0 + (num_proc × 16) + 8 × Int.unsigned chan_index + 0)
with (Int.unsigned chan_index × 8 + num_proc × 16); try ring.
simpl.
repeat vcgen.
Qed.
End GetHeadBody.
Theorem get_head_code_correct:
spec_le (get_head ↦ get_head_spec_low) (〚get_head ↦ f_tdq_get_head 〛L).
Proof.
fbigstep_pre L.
destruct m´.
simpl in *; subst.
destruct H2.
fbigstep (get_head_body_correct (Genv.globalenv p) b0 H m l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tdq_get_head)
(Vint n::nil)
(create_undef_temps (fn_temps f_tdq_get_head)))) muval.
Qed.
End GETHEAD.
Section GETTAIL.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetTailBody.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis hbtcbqpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma get_tail_body_correct: ∀ m d env le chan_index tail,
env = PTree.empty _ →
PTree.get _chan_index le = Some (Vint chan_index) →
Mem.load Mint32 (m, d) btcbpool_loc ((Int.unsigned chan_index) × 8 + 4 + num_proc × 16) = Some (Vint tail) →
0 ≤ (Int.unsigned chan_index) < num_chan →
exec_stmt ge env le ((m, d): mem) f_tdq_get_tail_body E0 le (m, d)
(Out_return (Some (Vint tail, tint))).
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tdq_get_tail_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; unfold t_struct_TDQ_node in *; subst.
repeat vcgen.
rewrite H.
replace 16384 with (num_proc × 16); try ring.
replace (0 + (num_proc × 16) + 8 × Int.unsigned chan_index + 4)
with (Int.unsigned chan_index × 8 + 4 + num_proc × 16); try ring.
simpl.
repeat vcgen.
Qed.
End GetTailBody.
Theorem get_tail_code_correct:
spec_le (get_tail ↦ get_tail_spec_low) (〚get_tail ↦ f_tdq_get_tail 〛L).
Proof.
fbigstep_pre L.
destruct m´; simpl in *; subst.
destruct H2.
fbigstep (get_tail_body_correct (Genv.globalenv p) b0 H m l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tdq_get_tail)
(Vint n::nil)
(create_undef_temps (fn_temps f_tdq_get_tail)))) muval.
Qed.
End GETTAIL.
Section SETHEAD.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetHeadBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis hbtcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma set_head_body_correct: ∀ m m´ d env le chan_index head,
env = PTree.empty _ →
PTree.get _chan_index le = Some (Vint chan_index) →
PTree.get _head le = Some (Vint head) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned chan_index × 8 + num_proc × 16) (Vint head)
= Some (m´, d) →
0 ≤ (Int.unsigned chan_index) < num_chan →
exec_stmt ge env le ((m, d): mem) f_tdq_set_head_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tdq_set_head_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; unfold t_struct_TDQ_node in *; subst.
repeat vcgen.
rewrite H.
replace 16384 with (num_proc × 16); try ring.
replace (0 + (num_proc × 16) + 8 × Int.unsigned chan_index + 0)
with (Int.unsigned chan_index × 8 + num_proc × 16); try ring.
simpl.
rewrite Int.unsigned_repr; try omega.
repeat vcgen.
Qed.
End SetHeadBody.
Theorem set_head_code_correct:
spec_le (set_head ↦ set_head_spec_low) (〚set_head ↦ f_tdq_set_head 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
fbigstep (set_head_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tdq_set_head)
(Vint n::Vint v::nil)
(create_undef_temps (fn_temps f_tdq_set_head)))) H0.
Qed.
End SETHEAD.
Section SETTAIL.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetTailBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis hbtcbqpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma set_tail_body_correct: ∀ m m´ d env le chan_index tail,
env = PTree.empty _ →
PTree.get _chan_index le = Some (Vint chan_index) →
PTree.get _tail le = Some (Vint tail) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned chan_index × 8 + 4 + num_proc × 16) (Vint tail)
= Some (m´, d) →
0 ≤ (Int.unsigned chan_index) < num_chan →
exec_stmt ge env le ((m, d): mem) f_tdq_set_tail_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tdq_set_tail_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; unfold t_struct_TDQ_node in *; subst.
repeat vcgen.
rewrite H.
replace 16384 with (num_proc × 16); try ring.
replace (0 + (num_proc × 16) + 8 × Int.unsigned chan_index + 4)
with (Int.unsigned chan_index × 8 + 4 + num_proc × 16); try ring.
simpl.
rewrite Int.unsigned_repr; try omega.
repeat vcgen.
Qed.
End SetTailBody.
Theorem set_tail_code_correct:
spec_le (set_tail ↦ set_tail_spec_low) (〚set_tail ↦ f_tdq_set_tail 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
fbigstep (set_tail_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tdq_set_tail)
(Vint n::Vint v::nil)
(create_undef_temps (fn_temps f_tdq_set_tail)))) H0.
Qed.
End SETTAIL.
Section TDQINIT.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TDQInitBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis hbtcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma tdq_init_body_correct: ∀ m m1 m´ d env le chan_index,
env = PTree.empty _ →
PTree.get _chan_index le = Some (Vint chan_index) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned chan_index × 8 + num_proc × 16)
(Vint (Int.repr num_proc)) = Some (m1, d) →
Mem.store Mint32 (m1, d) btcbpool_loc (Int.unsigned chan_index × 8 + 4 + num_proc × 16)
(Vint (Int.repr num_proc)) = Some (m´, d) →
0 ≤ (Int.unsigned chan_index) < num_chan →
exec_stmt ge env le ((m, d): mem) f_tdq_init_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tdq_init_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; unfold t_struct_TDQ_node in *; subst.
repeat vcgen.
- rewrite H.
replace 16384 with (num_proc × 16); try ring.
replace (0 + (num_proc × 16) + 8 × Int.unsigned chan_index + 0)
with (Int.unsigned chan_index × 8 + num_proc × 16); try ring.
simpl.
rewrite Int.unsigned_repr; try omega.
repeat vcgen.
- rewrite H.
replace 16384 with (num_proc × 16); try ring.
replace (0 + (num_proc × 16) + 8 × Int.unsigned chan_index + 4)
with (Int.unsigned chan_index × 8 + 4 + num_proc × 16); try ring.
simpl.
rewrite Int.unsigned_repr; try omega.
repeat vcgen.
Qed.
End TDQInitBody.
Theorem tdq_init_code_correct:
spec_le (tdq_init ↦ tdq_init_spec_low) (〚tdq_init ↦ f_tdq_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m, m´, m1, H1.
fbigstep (tdq_init_body_correct (Genv.globalenv p) b0 H m m1 m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tdq_init)
(Vint n::nil)
(create_undef_temps (fn_temps f_tdq_init)))) H0.
Qed.
End TDQINIT.
End WithPrimitives.
End PSLEEPERCODE.
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 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 TacticsForTesting.
Require Import AbstractDataType.
Require Import QueueIntroGenSpec.
Require Import PSleeperCSource.
Require Import PSleeper.
Module PSLEEPERCODE.
Section WithPrimitives.
Context `{real_params_ops : RealParamsOps}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{multi_oracle_prop: MultiOracleProp}.
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 t_struct_TCB_node_size :
sizeof t_struct_TCB_node = 16%Z.
Proof. simpl; auto. Qed.
Lemma t_struct_TDQ_node_size :
sizeof t_struct_TDQ_node = 8%Z.
Proof. simpl; auto. Qed.
Section GETSTATE.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetStateBody.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma get_state_body_correct: ∀ m d env le proc_index state,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
Mem.load Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16)
= Some (Vint state) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_get_state_body E0 le (m, d)
(Out_return (Some (Vint state, tint))).
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_get_state_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 0) with (Int.unsigned proc_index × 16); try ring.
simpl.
repeat vcgen.
Qed.
End GetStateBody.
Theorem get_state_code_correct:
spec_le (get_state ↦ get_state_spec_low) (〚get_state ↦ f_tcb_get_state 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_state_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_get_state)
(Vint n::nil)
(create_undef_temps (fn_temps f_tcb_get_state)))) m´.
Qed.
End GETSTATE.
Section TCBGETCPUID.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TcbGetCPUIDBody.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma tcb_get_CPU_ID_body_correct: ∀ m d env le proc_index cpu_id,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
Mem.load Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16 + 4)
= Some (Vint cpu_id) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_get_CPU_ID_state_body E0 le (m, d)
(Out_return (Some (Vint cpu_id, tint))).
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_get_CPU_ID_state_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 4) with (Int.unsigned proc_index × 16 + 4); try ring.
simpl.
repeat vcgen.
Qed.
End TcbGetCPUIDBody.
Theorem tcb_get_CPU_ID_code_correct:
spec_le (tcb_get_CPU_ID ↦ tcb_get_CPU_ID_spec_low) (〚tcb_get_CPU_ID ↦ f_tcb_get_CPU_ID_state 〛L).
Proof.
fbigstep_pre L.
fbigstep (tcb_get_CPU_ID_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_get_CPU_ID_state)
(Vint n::nil)
(create_undef_temps (fn_temps f_tcb_get_CPU_ID_state)))) m´.
Qed.
End TCBGETCPUID.
Section GETPREV.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetPrevBody.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma get_prev_body_correct: ∀ m d env le proc_index prev,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
Mem.load Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16 + 8)
= Some (Vint prev) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_get_prev_body E0 le (m, d)
(Out_return (Some (Vint prev, tint))).
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_get_prev_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 8) with (Int.unsigned proc_index × 16 + 8); try ring.
simpl.
repeat vcgen.
Qed.
End GetPrevBody.
Theorem get_prev_code_correct:
spec_le (get_prev ↦ get_prev_spec_low) (〚get_prev ↦ f_tcb_get_prev 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_prev_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_get_prev)
(Vint n::nil)
(create_undef_temps (fn_temps f_tcb_get_prev)))) m´.
Qed.
End GETPREV.
Section GETNEXT.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetNextBody.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma get_next_body_correct: ∀ m d env le proc_index next,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
Mem.load Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16 + 12)
= Some (Vint next) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_get_next_body E0 le (m, d)
(Out_return (Some (Vint next, tint))).
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_get_next_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 12) with (Int.unsigned proc_index × 16 + 12); try ring.
simpl.
repeat vcgen.
Qed.
End GetNextBody.
Theorem get_next_code_correct:
spec_le (get_next ↦ get_next_spec_low) (〚get_next ↦ f_tcb_get_next 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_next_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_get_next)
(Vint n::nil)
(create_undef_temps (fn_temps f_tcb_get_next)))) m´.
Qed.
End GETNEXT.
Section SETSTATE.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetStateBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma set_state_body_correct: ∀ m m´ d env le proc_index state,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
PTree.get _state le = Some (Vint state) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16)
(Vint state) = Some (m´, d) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_set_state_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_set_state_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 0) with (Int.unsigned proc_index × 16); try ring.
simpl.
repeat vcgen.
Qed.
End SetStateBody.
Theorem set_state_code_correct:
spec_le (set_state ↦ set_state_spec_low) (〚set_state ↦ f_tcb_set_state 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
fbigstep (set_state_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_set_state)
(Vint n::Vint v::nil)
(create_undef_temps (fn_temps f_tcb_set_state)))) H0.
Qed.
End SETSTATE.
Section TCBSETCPUID.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TcbSetCPUIDBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma tcb_set_CPU_ID_body_correct: ∀ m m´ d env le proc_index cpu_id,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
PTree.get _cpu_id le = Some (Vint cpu_id) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16 + 4)
(Vint cpu_id) = Some (m´, d) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_set_CPU_ID_state_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_set_CPU_ID_state_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 4) with (Int.unsigned proc_index × 16 + 4); try ring.
simpl.
repeat vcgen.
Qed.
End TcbSetCPUIDBody.
Theorem tcb_set_CPU_ID_code_correct:
spec_le (tcb_set_CPU_ID ↦ tcb_set_CPU_ID_spec_low) (〚tcb_set_CPU_ID ↦ f_tcb_set_CPU_ID_state〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
fbigstep (tcb_set_CPU_ID_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_set_CPU_ID_state)
(Vint n::Vint v::nil)
(create_undef_temps (fn_temps f_tcb_set_CPU_ID_state)))) H0.
Qed.
End TCBSETCPUID.
Section SETPREV.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetPrevBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma set_prev_body_correct: ∀ m m´ d env le proc_index prev,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
PTree.get _prev le = Some (Vint prev) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16 + 8)
(Vint prev) = Some (m´, d) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_set_prev_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_set_prev_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 8) with (Int.unsigned proc_index × 16 + 8); try ring.
simpl.
repeat vcgen.
Qed.
End SetPrevBody.
Theorem set_prev_code_correct:
spec_le (set_prev ↦ set_prev_spec_low) (〚set_prev ↦ f_tcb_set_prev 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
fbigstep (set_prev_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_set_prev)
(Vint n::Vint v::nil)
(create_undef_temps (fn_temps f_tcb_set_prev)))) H0.
Qed.
End SETPREV.
Section SETNEXT.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetNextBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis htcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma set_next_body_correct: ∀ m m´ d env le proc_index next,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
PTree.get _next le = Some (Vint next) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned proc_index × 16 + 12)
(Vint next) = Some (m´, d) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m, d): mem) f_tcb_set_next_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_set_next_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 12) with (Int.unsigned proc_index × 16 + 12); try ring.
simpl.
repeat vcgen.
Qed.
End SetNextBody.
Theorem set_next_code_correct:
spec_le (set_next ↦ set_next_spec_low) (〚set_next ↦ f_tcb_set_next 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
fbigstep (set_next_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_set_next)
(Vint n::Vint v::nil)
(create_undef_temps (fn_temps f_tcb_set_next)))) H0.
Qed.
End SETNEXT.
Section TCBINIT.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TCBInitBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis hbtcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma tcb_init_body_correct: ∀ m0 m1 m2 m3 m4 d env le proc_index,
env = PTree.empty _ →
PTree.get _proc_index le = Some (Vint proc_index) →
Mem.store Mint32 (m0, d) btcbpool_loc (Int.unsigned proc_index × 16)
(Vint (Int.repr TSTATE_DEAD)) = Some (m1, d) →
Mem.store Mint32 (m1, d) btcbpool_loc (Int.unsigned proc_index × 16 + 4)
(Vint (Int.repr 0)) = Some (m2, d) →
Mem.store Mint32 (m2, d) btcbpool_loc (Int.unsigned proc_index × 16 + 8)
(Vint (Int.repr num_proc)) = Some (m3, d) →
Mem.store Mint32 (m3, d) btcbpool_loc (Int.unsigned proc_index × 16 + 12)
(Vint (Int.repr num_proc)) = Some (m4, d) →
0 ≤ (Int.unsigned proc_index) < num_proc →
exec_stmt ge env le ((m0, d): mem) f_tcb_init_body E0 le (m4, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tcb_init_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; subst.
repeat vcgen.
- rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 0) with (Int.unsigned proc_index × 16); try ring.
simpl.
repeat vcgen.
- rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 4) with (Int.unsigned proc_index × 16 + 4); try ring.
simpl.
repeat vcgen.
- rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 8) with (Int.unsigned proc_index × 16 + 8); try ring.
simpl.
repeat vcgen.
- rewrite H0.
replace (0 + 0 + 16 × Int.unsigned proc_index + 12) with (Int.unsigned proc_index × 16 + 12); try ring.
simpl.
repeat vcgen.
Qed.
End TCBInitBody.
Theorem tcb_init_code_correct:
spec_le (tcb_init ↦ tcb_init_spec_low) (〚tcb_init ↦ f_tcb_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m, m´, m1, m2, m3, H1.
destruct H0; destruct H2; destruct H3; simpl in ×.
fbigstep (tcb_init_body_correct (Genv.globalenv p) b0 H m m1 m2 m3 m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tcb_init)
(Vint n::nil)
(create_undef_temps (fn_temps f_tcb_init)))) muval.
Qed.
End TCBINIT.
Section GETHEAD.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetHeadBody.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis hbtcbqpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma get_head_body_correct: ∀ m d env le chan_index head,
env = PTree.empty _ →
PTree.get _chan_index le = Some (Vint chan_index) →
Mem.load Mint32 (m, d) btcbpool_loc ((Int.unsigned chan_index) × 8 + num_proc × 16)
= Some (Vint head) →
0 ≤ (Int.unsigned chan_index) < num_chan →
exec_stmt ge env le ((m, d): mem) f_tdq_get_head_body E0 le (m, d)
(Out_return (Some (Vint head, tint))).
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tdq_get_head_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; unfold t_struct_TDQ_node in *; subst.
repeat vcgen.
rewrite H.
replace 16384 with (num_proc × 16); try ring.
replace (0 + (num_proc × 16) + 8 × Int.unsigned chan_index + 0)
with (Int.unsigned chan_index × 8 + num_proc × 16); try ring.
simpl.
repeat vcgen.
Qed.
End GetHeadBody.
Theorem get_head_code_correct:
spec_le (get_head ↦ get_head_spec_low) (〚get_head ↦ f_tdq_get_head 〛L).
Proof.
fbigstep_pre L.
destruct m´.
simpl in *; subst.
destruct H2.
fbigstep (get_head_body_correct (Genv.globalenv p) b0 H m l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tdq_get_head)
(Vint n::nil)
(create_undef_temps (fn_temps f_tdq_get_head)))) muval.
Qed.
End GETHEAD.
Section GETTAIL.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetTailBody.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis hbtcbqpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma get_tail_body_correct: ∀ m d env le chan_index tail,
env = PTree.empty _ →
PTree.get _chan_index le = Some (Vint chan_index) →
Mem.load Mint32 (m, d) btcbpool_loc ((Int.unsigned chan_index) × 8 + 4 + num_proc × 16) = Some (Vint tail) →
0 ≤ (Int.unsigned chan_index) < num_chan →
exec_stmt ge env le ((m, d): mem) f_tdq_get_tail_body E0 le (m, d)
(Out_return (Some (Vint tail, tint))).
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tdq_get_tail_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; unfold t_struct_TDQ_node in *; subst.
repeat vcgen.
rewrite H.
replace 16384 with (num_proc × 16); try ring.
replace (0 + (num_proc × 16) + 8 × Int.unsigned chan_index + 4)
with (Int.unsigned chan_index × 8 + 4 + num_proc × 16); try ring.
simpl.
repeat vcgen.
Qed.
End GetTailBody.
Theorem get_tail_code_correct:
spec_le (get_tail ↦ get_tail_spec_low) (〚get_tail ↦ f_tdq_get_tail 〛L).
Proof.
fbigstep_pre L.
destruct m´; simpl in *; subst.
destruct H2.
fbigstep (get_tail_body_correct (Genv.globalenv p) b0 H m l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tdq_get_tail)
(Vint n::nil)
(create_undef_temps (fn_temps f_tdq_get_tail)))) muval.
Qed.
End GETTAIL.
Section SETHEAD.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetHeadBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis hbtcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma set_head_body_correct: ∀ m m´ d env le chan_index head,
env = PTree.empty _ →
PTree.get _chan_index le = Some (Vint chan_index) →
PTree.get _head le = Some (Vint head) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned chan_index × 8 + num_proc × 16) (Vint head)
= Some (m´, d) →
0 ≤ (Int.unsigned chan_index) < num_chan →
exec_stmt ge env le ((m, d): mem) f_tdq_set_head_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tdq_set_head_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; unfold t_struct_TDQ_node in *; subst.
repeat vcgen.
rewrite H.
replace 16384 with (num_proc × 16); try ring.
replace (0 + (num_proc × 16) + 8 × Int.unsigned chan_index + 0)
with (Int.unsigned chan_index × 8 + num_proc × 16); try ring.
simpl.
rewrite Int.unsigned_repr; try omega.
repeat vcgen.
Qed.
End SetHeadBody.
Theorem set_head_code_correct:
spec_le (set_head ↦ set_head_spec_low) (〚set_head ↦ f_tdq_set_head 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
fbigstep (set_head_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tdq_set_head)
(Vint n::Vint v::nil)
(create_undef_temps (fn_temps f_tdq_set_head)))) H0.
Qed.
End SETHEAD.
Section SETTAIL.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetTailBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis hbtcbqpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma set_tail_body_correct: ∀ m m´ d env le chan_index tail,
env = PTree.empty _ →
PTree.get _chan_index le = Some (Vint chan_index) →
PTree.get _tail le = Some (Vint tail) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned chan_index × 8 + 4 + num_proc × 16) (Vint tail)
= Some (m´, d) →
0 ≤ (Int.unsigned chan_index) < num_chan →
exec_stmt ge env le ((m, d): mem) f_tdq_set_tail_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tdq_set_tail_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; unfold t_struct_TDQ_node in *; subst.
repeat vcgen.
rewrite H.
replace 16384 with (num_proc × 16); try ring.
replace (0 + (num_proc × 16) + 8 × Int.unsigned chan_index + 4)
with (Int.unsigned chan_index × 8 + 4 + num_proc × 16); try ring.
simpl.
rewrite Int.unsigned_repr; try omega.
repeat vcgen.
Qed.
End SetTailBody.
Theorem set_tail_code_correct:
spec_le (set_tail ↦ set_tail_spec_low) (〚set_tail ↦ f_tdq_set_tail 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m.
destruct m´.
fbigstep (set_tail_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tdq_set_tail)
(Vint n::Vint v::nil)
(create_undef_temps (fn_temps f_tdq_set_tail)))) H0.
Qed.
End SETTAIL.
Section TDQINIT.
Let L: compatlayer (cdata RData) := TCBPool_LOC ↦ tcbpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TDQInitBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable btcbpool_loc: block.
Hypothesis hbtcbpool_loc: Genv.find_symbol ge TCBPool_LOC = Some btcbpool_loc.
Lemma tdq_init_body_correct: ∀ m m1 m´ d env le chan_index,
env = PTree.empty _ →
PTree.get _chan_index le = Some (Vint chan_index) →
Mem.store Mint32 (m, d) btcbpool_loc (Int.unsigned chan_index × 8 + num_proc × 16)
(Vint (Int.repr num_proc)) = Some (m1, d) →
Mem.store Mint32 (m1, d) btcbpool_loc (Int.unsigned chan_index × 8 + 4 + num_proc × 16)
(Vint (Int.repr num_proc)) = Some (m´, d) →
0 ≤ (Int.unsigned chan_index) < num_chan →
exec_stmt ge env le ((m, d): mem) f_tdq_init_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val.
generalize t_struct_TCB_node_size.
generalize t_struct_TDQ_node_size.
intros.
subst.
unfold f_tdq_init_body; subst.
unfold t_struct_TCB in *; unfold t_struct_TCB_node in *; unfold t_struct_TDQ_node in *; subst.
repeat vcgen.
- rewrite H.
replace 16384 with (num_proc × 16); try ring.
replace (0 + (num_proc × 16) + 8 × Int.unsigned chan_index + 0)
with (Int.unsigned chan_index × 8 + num_proc × 16); try ring.
simpl.
rewrite Int.unsigned_repr; try omega.
repeat vcgen.
- rewrite H.
replace 16384 with (num_proc × 16); try ring.
replace (0 + (num_proc × 16) + 8 × Int.unsigned chan_index + 4)
with (Int.unsigned chan_index × 8 + 4 + num_proc × 16); try ring.
simpl.
rewrite Int.unsigned_repr; try omega.
repeat vcgen.
Qed.
End TDQInitBody.
Theorem tdq_init_code_correct:
spec_le (tdq_init ↦ tdq_init_spec_low) (〚tdq_init ↦ f_tdq_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m, m´, m1, H1.
fbigstep (tdq_init_body_correct (Genv.globalenv p) b0 H m m1 m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tdq_init)
(Vint n::nil)
(create_undef_temps (fn_temps f_tdq_init)))) H0.
Qed.
End TDQINIT.
End WithPrimitives.
End PSLEEPERCODE.