Library mcertikos.proc.PAbQueueAtomicCode
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 CLemmas.
Require Import TacticsForTesting.
Require Import CalRealProcModule.
Require Import CommonTactic.
Require Import XOmega.
Require Import AbstractDataType.
Require Import PAbQueueAtomic.
Require Import CVIntroGenSpec.
Require Import ObjCV.
Require Import PAbQueueAtomicCSource.
Module PAbQueueAtomicCode.
Section WithPrimitives.
Context `{real_params: RealParams}.
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}.
Lemma chpool_size: sizeof t_struct_chpool_t = 16.
Proof.
reflexivity.
Qed.
Section GETSYNCCHANTO.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GETSYNCCHANTOBODY.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma get_sync_chan_to_body_correct: ∀ m d env le chanid to,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
Mem.load Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16)
= Some (Vint to) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_get_sync_chan_to_body E0 le (m, d)
(Out_return (Some (Vint to, tint))).
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_get_sync_chan_to_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n + 0) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End GETSYNCCHANTOBODY.
Theorem get_sync_chan_to_code_correct:
spec_le (get_sync_chan_to ↦ get_sync_chan_to_spec_low) (〚get_sync_chan_to ↦ f_get_sync_chan_to 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_sync_chan_to_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_get_sync_chan_to)
(Vint chanid::nil)
(create_undef_temps (fn_temps f_get_sync_chan_to)))) m´.
Qed.
End GETSYNCCHANTO.
Section GETSYNCCHANPADDR.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GETSYNCCHANTOBODY.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma get_sync_chan_paddr_body_correct: ∀ m d env le chanid to,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
Mem.load Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16 + 4)
= Some (Vint to) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_get_sync_chan_paddr_body E0 le (m, d)
(Out_return (Some (Vint to, tint))).
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_get_sync_chan_paddr_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End GETSYNCCHANTOBODY.
Theorem get_sync_chan_paddr_code_correct:
spec_le (get_sync_chan_paddr ↦ get_sync_chan_paddr_spec_low) (〚get_sync_chan_paddr ↦ f_get_sync_chan_paddr 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_sync_chan_paddr_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_get_sync_chan_paddr)
(Vint chanid::nil)
(create_undef_temps (fn_temps f_get_sync_chan_paddr)))) m´.
Qed.
End GETSYNCCHANPADDR.
Section GETSYNCCHANCOUNT.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GETSYNCCHANTOBODY.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma get_sync_chan_count_body_correct: ∀ m d env le chanid to,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
Mem.load Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16 + 8)
= Some (Vint to) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_get_sync_chan_count_body E0 le (m, d)
(Out_return (Some (Vint to, tint))).
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_get_sync_chan_count_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End GETSYNCCHANTOBODY.
Theorem get_sync_chan_count_code_correct:
spec_le (get_sync_chan_count ↦ get_sync_chan_count_spec_low) (〚get_sync_chan_count ↦ f_get_sync_chan_count 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_sync_chan_count_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_get_sync_chan_count)
(Vint chanid::nil)
(create_undef_temps (fn_temps f_get_sync_chan_count)))) m´.
Qed.
End GETSYNCCHANCOUNT.
Section GETSYNCCHANBUSY.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GETSYNCCHANTOBODY.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma get_sync_chan_busy_body_correct: ∀ m d env le chanid to,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
Mem.load Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16 + 12)
= Some (Vint to) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_get_sync_chan_busy_body E0 le (m, d)
(Out_return (Some (Vint to, tint))).
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_get_sync_chan_busy_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End GETSYNCCHANTOBODY.
Theorem get_sync_chan_busy_code_correct:
spec_le (get_sync_chan_busy ↦ get_sync_chan_busy_spec_low) (〚get_sync_chan_busy ↦ f_get_sync_chan_busy 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_sync_chan_busy_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_get_sync_chan_busy)
(Vint chanid::nil)
(create_undef_temps (fn_temps f_get_sync_chan_busy)))) m´.
Qed.
End GETSYNCCHANBUSY.
Section SETSYNCCHANTO.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SETSYNCCHANTOBODY.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma set_sync_chan_to_body_correct: ∀ m m´ d env le chanid to,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
PTree.get _n_to le = Some (Vint to) →
Mem.store Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16) (Vint to) = Some (m´, d) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_set_sync_chan_to_body E0 le (m´, d) Out_normal.
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_set_sync_chan_to_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n + 0) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End SETSYNCCHANTOBODY.
Theorem set_sync_chan_to_code_correct:
spec_le (set_sync_chan_to ↦ set_sync_chan_to_spec_low) (〚set_sync_chan_to ↦ f_set_sync_chan_to 〛L).
Proof.
fbigstep_pre L.
destruct m as (m, d).
destruct m´ as (m´, d´).
subst.
destruct H0.
destruct H2.
simpl.
fbigstep (set_sync_chan_to_body_correct (Genv.globalenv p) b0 H m m´ d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_sync_chan_to)
(Vint chanid::Vint to::nil)
(create_undef_temps (fn_temps f_set_sync_chan_to)))) muval.
Qed.
End SETSYNCCHANTO.
Section SETSYNCCHANPADDR.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SETSYNCCHANPADDRBODY.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma set_sync_chan_paddr_body_correct: ∀ m m´ d env le chanid paddr,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
PTree.get _n_paddr le = Some (Vint paddr) →
Mem.store Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16 + 4) (Vint paddr) = Some (m´, d) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_set_sync_chan_paddr_body E0 le ((m´, d) : mem) Out_normal.
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_set_sync_chan_paddr_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End SETSYNCCHANPADDRBODY.
Theorem set_sync_chan_paddr_code_correct:
spec_le (set_sync_chan_paddr ↦ set_sync_chan_paddr_spec_low) (〚set_sync_chan_paddr ↦ f_set_sync_chan_paddr 〛L).
Proof.
fbigstep_pre L.
destruct m as (m, d).
destruct m´ as (m´, d´).
subst.
destruct H0.
destruct H2.
simpl.
fbigstep (set_sync_chan_paddr_body_correct
(Genv.globalenv p) b0 H m m´ d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_sync_chan_paddr)
(Vint chanid::Vint paddr::nil)
(create_undef_temps (fn_temps f_set_sync_chan_paddr)))) muval.
Qed.
End SETSYNCCHANPADDR.
Section SETSYNCCHANCOUNT.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SETSYNCCHANCOUNTBODY.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma set_sync_chan_count_body_correct: ∀ m m´ d env le chanid count,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
PTree.get _n_count le = Some (Vint count) →
Mem.store Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16 + 8) (Vint count) = Some (m´, d) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_set_sync_chan_count_body E0 le (m´, d) Out_normal.
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_set_sync_chan_count_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End SETSYNCCHANCOUNTBODY.
Theorem set_sync_chan_count_code_correct:
spec_le (set_sync_chan_count ↦ set_sync_chan_count_spec_low) (〚set_sync_chan_count ↦ f_set_sync_chan_count 〛L).
Proof.
fbigstep_pre L.
destruct m as (m, d).
destruct m´ as (m´, d´).
subst.
destruct H0.
destruct H2.
simpl.
fbigstep (set_sync_chan_count_body_correct
(Genv.globalenv p) b0 H m m´ d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_sync_chan_count)
(Vint chanid::Vint count::nil)
(create_undef_temps (fn_temps f_set_sync_chan_count)))) muval.
Qed.
End SETSYNCCHANCOUNT.
Section SETSYNCCHANBUSY.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SETSYNCCHANBUSYBODY.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma set_sync_chan_busy_body_correct: ∀ m m´ d env le chanid busy,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
PTree.get _n_busy le = Some (Vint busy) →
Mem.store Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16 + 12) (Vint busy) = Some (m´, d) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_set_sync_chan_busy_body E0 le (m´, d) Out_normal.
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_set_sync_chan_busy_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End SETSYNCCHANBUSYBODY.
Theorem set_sync_chan_busy_code_correct:
spec_le (set_sync_chan_busy ↦ set_sync_chan_busy_spec_low) (〚set_sync_chan_busy ↦ f_set_sync_chan_busy 〛L).
Proof.
fbigstep_pre L.
destruct m as (m, d).
destruct m´ as (m´, d´).
subst.
destruct H0.
destruct H2.
simpl.
fbigstep (set_sync_chan_busy_body_correct
(Genv.globalenv p) b0 H m m´ d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_sync_chan_busy)
(Vint chanid::Vint busy::nil)
(create_undef_temps (fn_temps f_set_sync_chan_busy)))) muval.
Qed.
End SETSYNCCHANBUSY.
Section INITSYNCCHAN.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section INITSYNCCHANBODY.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma init_sync_chan_body_correct: ∀ m0 m1 m2 m3 m4 d env le chanid,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
Mem.store Mint32 (m0, d) bsyncchanpool_loc (Int.unsigned chanid × 16) (Vint (Int.repr num_chan))
= Some (m1, d) →
Mem.store Mint32 (m1, d) bsyncchanpool_loc (Int.unsigned chanid × 16 + 4) (Vint Int.zero)
= Some (m2, d) →
Mem.store Mint32 (m2, d) bsyncchanpool_loc (Int.unsigned chanid × 16 + 8) (Vint Int.zero)
= Some (m3, d) →
Mem.store Mint32 (m3, d) bsyncchanpool_loc (Int.unsigned chanid × 16 + 12) (Vint Int.zero)
= Some (m4, d) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m0, d): mem) f_init_sync_chan_body E0 le (m4, d) Out_normal.
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_init_sync_chan_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
- rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n + 0) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
- rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
- rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
- rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H4.
unfold n in ×.
repeat vcgen.
Qed.
End INITSYNCCHANBODY.
Theorem init_sync_chan_code_correct:
spec_le (init_sync_chan ↦ init_sync_chan_spec_low) (〚init_sync_chan ↦ f_init_sync_chan 〛L).
Proof.
fbigstep_pre L.
destruct m as (m, d).
destruct m´ as (m´, d´).
destruct m1 as (m1, d1).
destruct m2 as (m2, d2).
destruct m3 as (m3, d3).
subst.
destruct H0; destruct H1; destruct H2; destruct H3; destruct H5; simpl in ×.
fbigstep (init_sync_chan_body_correct
(Genv.globalenv p) b0 H m m1 m2 m3 m´ d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_init_sync_chan)
(Vint chanid::nil)
(create_undef_temps (fn_temps f_init_sync_chan)))) muval.
Qed.
End INITSYNCCHAN.
Section GETKERNELPA.
Let L: compatlayer (cdata RData) := pt_read ↦ gensem ptRead_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GETKERNELPABODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bpt_read : block.
Hypothesis hpt_read1 : Genv.find_symbol ge pt_read = Some bpt_read.
Hypothesis hpt_read2 : Genv.find_funct_ptr ge bpt_read
= Some (External (EF_external pt_read
(signature_of_type (Tcons tint (Tcons tint Tnil)) tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
Lemma get_kernel_pa_body_correct: ∀ m d env le pid va pa,
env = PTree.empty _ →
PTree.get _pid le = Some (Vint pid) →
PTree.get _va le = Some (Vint va) →
high_level_invariant d →
get_kernel_pa_spec (Int.unsigned pid) (Int.unsigned va) d = Some (Int.unsigned pa) →
0 ≤ (Int.unsigned pid) < num_proc →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_get_kernel_pa_body E0 le´ (m, d)
(Out_return (Some (Vint pa, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold f_get_kernel_pa_body.
functional inversion H3; subst.
assert(0 ≤ paddr ≤ Int.max_unsigned).
{ functional inversion H8; subst.
omega.
functional inversion H; subst.
destruct H2.
unfold pdi, pti, pt in ×.
unfold PTE_Arg in H14.
subdestruct.
unfold PDE_Arg in Hdestruct.
subdestruct.
unfold consistent_pmap_domain in valid_pmap_domain.
assert(0 ≤ (Int.unsigned va) < 4294967296).
{ unfold PDX, PTX in ×.
clearAllExceptTwo muval a1.
xomega. }
generalize (valid_pmap_domain (Int.unsigned pid) H4 (Int.unsigned va) H2 pdt _x2 H19 padr p H20).
intro tmp.
destruct tmp.
generalize (valid_nps H7); intro.
destruct p; simpl.
omega.
omega.
destruct b; omega.
omega. }
rewrite <- Int.repr_unsigned with pa.
rewrite <- H6.
esplit.
unfold exec_stmt.
change E0 with (E0 ** E0).
econstructor.
- repeat vcgen.
instantiate (1:= (Int.repr paddr)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
- d3 vcgen.
+ repeat vcgen.
+ discharge_cmp.
econstructor.
ptreesolve.
xomega.
xomega.
xomega.
xomega.
Qed.
End GETKERNELPABODY.
Theorem get_kernel_pa_code_correct:
spec_le (get_kernel_pa ↦ get_kernel_pa_spec_low) (〚get_kernel_pa ↦ f_get_kernel_pa 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (get_kernel_pa_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp m´0 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_get_kernel_pa)
(Vint pid :: Vint vaddr :: nil)
(create_undef_temps (fn_temps f_get_kernel_pa)))) H1.
Qed.
End GETKERNELPA.
End WithPrimitives.
End PAbQueueAtomicCode.
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 CLemmas.
Require Import TacticsForTesting.
Require Import CalRealProcModule.
Require Import CommonTactic.
Require Import XOmega.
Require Import AbstractDataType.
Require Import PAbQueueAtomic.
Require Import CVIntroGenSpec.
Require Import ObjCV.
Require Import PAbQueueAtomicCSource.
Module PAbQueueAtomicCode.
Section WithPrimitives.
Context `{real_params: RealParams}.
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}.
Lemma chpool_size: sizeof t_struct_chpool_t = 16.
Proof.
reflexivity.
Qed.
Section GETSYNCCHANTO.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GETSYNCCHANTOBODY.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma get_sync_chan_to_body_correct: ∀ m d env le chanid to,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
Mem.load Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16)
= Some (Vint to) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_get_sync_chan_to_body E0 le (m, d)
(Out_return (Some (Vint to, tint))).
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_get_sync_chan_to_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n + 0) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End GETSYNCCHANTOBODY.
Theorem get_sync_chan_to_code_correct:
spec_le (get_sync_chan_to ↦ get_sync_chan_to_spec_low) (〚get_sync_chan_to ↦ f_get_sync_chan_to 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_sync_chan_to_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_get_sync_chan_to)
(Vint chanid::nil)
(create_undef_temps (fn_temps f_get_sync_chan_to)))) m´.
Qed.
End GETSYNCCHANTO.
Section GETSYNCCHANPADDR.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GETSYNCCHANTOBODY.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma get_sync_chan_paddr_body_correct: ∀ m d env le chanid to,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
Mem.load Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16 + 4)
= Some (Vint to) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_get_sync_chan_paddr_body E0 le (m, d)
(Out_return (Some (Vint to, tint))).
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_get_sync_chan_paddr_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End GETSYNCCHANTOBODY.
Theorem get_sync_chan_paddr_code_correct:
spec_le (get_sync_chan_paddr ↦ get_sync_chan_paddr_spec_low) (〚get_sync_chan_paddr ↦ f_get_sync_chan_paddr 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_sync_chan_paddr_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_get_sync_chan_paddr)
(Vint chanid::nil)
(create_undef_temps (fn_temps f_get_sync_chan_paddr)))) m´.
Qed.
End GETSYNCCHANPADDR.
Section GETSYNCCHANCOUNT.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GETSYNCCHANTOBODY.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma get_sync_chan_count_body_correct: ∀ m d env le chanid to,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
Mem.load Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16 + 8)
= Some (Vint to) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_get_sync_chan_count_body E0 le (m, d)
(Out_return (Some (Vint to, tint))).
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_get_sync_chan_count_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End GETSYNCCHANTOBODY.
Theorem get_sync_chan_count_code_correct:
spec_le (get_sync_chan_count ↦ get_sync_chan_count_spec_low) (〚get_sync_chan_count ↦ f_get_sync_chan_count 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_sync_chan_count_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_get_sync_chan_count)
(Vint chanid::nil)
(create_undef_temps (fn_temps f_get_sync_chan_count)))) m´.
Qed.
End GETSYNCCHANCOUNT.
Section GETSYNCCHANBUSY.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GETSYNCCHANTOBODY.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma get_sync_chan_busy_body_correct: ∀ m d env le chanid to,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
Mem.load Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16 + 12)
= Some (Vint to) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_get_sync_chan_busy_body E0 le (m, d)
(Out_return (Some (Vint to, tint))).
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_get_sync_chan_busy_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End GETSYNCCHANTOBODY.
Theorem get_sync_chan_busy_code_correct:
spec_le (get_sync_chan_busy ↦ get_sync_chan_busy_spec_low) (〚get_sync_chan_busy ↦ f_get_sync_chan_busy 〛L).
Proof.
fbigstep_pre L.
fbigstep (get_sync_chan_busy_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_get_sync_chan_busy)
(Vint chanid::nil)
(create_undef_temps (fn_temps f_get_sync_chan_busy)))) m´.
Qed.
End GETSYNCCHANBUSY.
Section SETSYNCCHANTO.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SETSYNCCHANTOBODY.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma set_sync_chan_to_body_correct: ∀ m m´ d env le chanid to,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
PTree.get _n_to le = Some (Vint to) →
Mem.store Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16) (Vint to) = Some (m´, d) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_set_sync_chan_to_body E0 le (m´, d) Out_normal.
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_set_sync_chan_to_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n + 0) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End SETSYNCCHANTOBODY.
Theorem set_sync_chan_to_code_correct:
spec_le (set_sync_chan_to ↦ set_sync_chan_to_spec_low) (〚set_sync_chan_to ↦ f_set_sync_chan_to 〛L).
Proof.
fbigstep_pre L.
destruct m as (m, d).
destruct m´ as (m´, d´).
subst.
destruct H0.
destruct H2.
simpl.
fbigstep (set_sync_chan_to_body_correct (Genv.globalenv p) b0 H m m´ d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_sync_chan_to)
(Vint chanid::Vint to::nil)
(create_undef_temps (fn_temps f_set_sync_chan_to)))) muval.
Qed.
End SETSYNCCHANTO.
Section SETSYNCCHANPADDR.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SETSYNCCHANPADDRBODY.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma set_sync_chan_paddr_body_correct: ∀ m m´ d env le chanid paddr,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
PTree.get _n_paddr le = Some (Vint paddr) →
Mem.store Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16 + 4) (Vint paddr) = Some (m´, d) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_set_sync_chan_paddr_body E0 le ((m´, d) : mem) Out_normal.
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_set_sync_chan_paddr_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End SETSYNCCHANPADDRBODY.
Theorem set_sync_chan_paddr_code_correct:
spec_le (set_sync_chan_paddr ↦ set_sync_chan_paddr_spec_low) (〚set_sync_chan_paddr ↦ f_set_sync_chan_paddr 〛L).
Proof.
fbigstep_pre L.
destruct m as (m, d).
destruct m´ as (m´, d´).
subst.
destruct H0.
destruct H2.
simpl.
fbigstep (set_sync_chan_paddr_body_correct
(Genv.globalenv p) b0 H m m´ d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_sync_chan_paddr)
(Vint chanid::Vint paddr::nil)
(create_undef_temps (fn_temps f_set_sync_chan_paddr)))) muval.
Qed.
End SETSYNCCHANPADDR.
Section SETSYNCCHANCOUNT.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SETSYNCCHANCOUNTBODY.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma set_sync_chan_count_body_correct: ∀ m m´ d env le chanid count,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
PTree.get _n_count le = Some (Vint count) →
Mem.store Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16 + 8) (Vint count) = Some (m´, d) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_set_sync_chan_count_body E0 le (m´, d) Out_normal.
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_set_sync_chan_count_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End SETSYNCCHANCOUNTBODY.
Theorem set_sync_chan_count_code_correct:
spec_le (set_sync_chan_count ↦ set_sync_chan_count_spec_low) (〚set_sync_chan_count ↦ f_set_sync_chan_count 〛L).
Proof.
fbigstep_pre L.
destruct m as (m, d).
destruct m´ as (m´, d´).
subst.
destruct H0.
destruct H2.
simpl.
fbigstep (set_sync_chan_count_body_correct
(Genv.globalenv p) b0 H m m´ d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_sync_chan_count)
(Vint chanid::Vint count::nil)
(create_undef_temps (fn_temps f_set_sync_chan_count)))) muval.
Qed.
End SETSYNCCHANCOUNT.
Section SETSYNCCHANBUSY.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SETSYNCCHANBUSYBODY.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma set_sync_chan_busy_body_correct: ∀ m m´ d env le chanid busy,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
PTree.get _n_busy le = Some (Vint busy) →
Mem.store Mint32 (m, d) bsyncchanpool_loc ((Int.unsigned chanid) × 16 + 12) (Vint busy) = Some (m´, d) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m, d): mem) f_set_sync_chan_busy_body E0 le (m´, d) Out_normal.
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_set_sync_chan_busy_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
Qed.
End SETSYNCCHANBUSYBODY.
Theorem set_sync_chan_busy_code_correct:
spec_le (set_sync_chan_busy ↦ set_sync_chan_busy_spec_low) (〚set_sync_chan_busy ↦ f_set_sync_chan_busy 〛L).
Proof.
fbigstep_pre L.
destruct m as (m, d).
destruct m´ as (m´, d´).
subst.
destruct H0.
destruct H2.
simpl.
fbigstep (set_sync_chan_busy_body_correct
(Genv.globalenv p) b0 H m m´ d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_set_sync_chan_busy)
(Vint chanid::Vint busy::nil)
(create_undef_temps (fn_temps f_set_sync_chan_busy)))) muval.
Qed.
End SETSYNCCHANBUSY.
Section INITSYNCCHAN.
Let L: compatlayer (cdata RData) := SYNCCHPOOL_LOC ↦ syncchpool_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section INITSYNCCHANBODY.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bsyncchanpool_loc: block.
Hypothesis hsyncchanpool_loc: Genv.find_symbol ge SYNCCHPOOL_LOC = Some bsyncchanpool_loc.
Lemma init_sync_chan_body_correct: ∀ m0 m1 m2 m3 m4 d env le chanid,
env = PTree.empty _ →
PTree.get _chanid le = Some (Vint chanid) →
Mem.store Mint32 (m0, d) bsyncchanpool_loc (Int.unsigned chanid × 16) (Vint (Int.repr num_chan))
= Some (m1, d) →
Mem.store Mint32 (m1, d) bsyncchanpool_loc (Int.unsigned chanid × 16 + 4) (Vint Int.zero)
= Some (m2, d) →
Mem.store Mint32 (m2, d) bsyncchanpool_loc (Int.unsigned chanid × 16 + 8) (Vint Int.zero)
= Some (m3, d) →
Mem.store Mint32 (m3, d) bsyncchanpool_loc (Int.unsigned chanid × 16 + 12) (Vint Int.zero)
= Some (m4, d) →
0 ≤ (Int.unsigned chanid) < num_chan →
kernel_mode d →
exec_stmt ge env le ((m0, d): mem) f_init_sync_chan_body E0 le (m4, d) Out_normal.
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize chpool_size; intros chpool_size.
unfold f_init_sync_chan_body; subst.
unfold t_struct_chpool_t; subst.
repeat vcgen; fold t_struct_chpool_t; try (rewrite chpool_size; omega).
- rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n + 0) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
- rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
- rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H1.
unfold n in ×.
repeat vcgen.
- rewrite chpool_size.
set (n := Int.unsigned chanid); fold n in H1.
replace (0 + 16 × n) with (n × 16); try ring.
Opaque Z.add Z.sub Z.div Z.mul.
simpl.
simpl in H4.
unfold n in ×.
repeat vcgen.
Qed.
End INITSYNCCHANBODY.
Theorem init_sync_chan_code_correct:
spec_le (init_sync_chan ↦ init_sync_chan_spec_low) (〚init_sync_chan ↦ f_init_sync_chan 〛L).
Proof.
fbigstep_pre L.
destruct m as (m, d).
destruct m´ as (m´, d´).
destruct m1 as (m1, d1).
destruct m2 as (m2, d2).
destruct m3 as (m3, d3).
subst.
destruct H0; destruct H1; destruct H2; destruct H3; destruct H5; simpl in ×.
fbigstep (init_sync_chan_body_correct
(Genv.globalenv p) b0 H m m1 m2 m3 m´ d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_init_sync_chan)
(Vint chanid::nil)
(create_undef_temps (fn_temps f_init_sync_chan)))) muval.
Qed.
End INITSYNCCHAN.
Section GETKERNELPA.
Let L: compatlayer (cdata RData) := pt_read ↦ gensem ptRead_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GETKERNELPABODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bpt_read : block.
Hypothesis hpt_read1 : Genv.find_symbol ge pt_read = Some bpt_read.
Hypothesis hpt_read2 : Genv.find_funct_ptr ge bpt_read
= Some (External (EF_external pt_read
(signature_of_type (Tcons tint (Tcons tint Tnil)) tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
Lemma get_kernel_pa_body_correct: ∀ m d env le pid va pa,
env = PTree.empty _ →
PTree.get _pid le = Some (Vint pid) →
PTree.get _va le = Some (Vint va) →
high_level_invariant d →
get_kernel_pa_spec (Int.unsigned pid) (Int.unsigned va) d = Some (Int.unsigned pa) →
0 ≤ (Int.unsigned pid) < num_proc →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_get_kernel_pa_body E0 le´ (m, d)
(Out_return (Some (Vint pa, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold f_get_kernel_pa_body.
functional inversion H3; subst.
assert(0 ≤ paddr ≤ Int.max_unsigned).
{ functional inversion H8; subst.
omega.
functional inversion H; subst.
destruct H2.
unfold pdi, pti, pt in ×.
unfold PTE_Arg in H14.
subdestruct.
unfold PDE_Arg in Hdestruct.
subdestruct.
unfold consistent_pmap_domain in valid_pmap_domain.
assert(0 ≤ (Int.unsigned va) < 4294967296).
{ unfold PDX, PTX in ×.
clearAllExceptTwo muval a1.
xomega. }
generalize (valid_pmap_domain (Int.unsigned pid) H4 (Int.unsigned va) H2 pdt _x2 H19 padr p H20).
intro tmp.
destruct tmp.
generalize (valid_nps H7); intro.
destruct p; simpl.
omega.
omega.
destruct b; omega.
omega. }
rewrite <- Int.repr_unsigned with pa.
rewrite <- H6.
esplit.
unfold exec_stmt.
change E0 with (E0 ** E0).
econstructor.
- repeat vcgen.
instantiate (1:= (Int.repr paddr)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
- d3 vcgen.
+ repeat vcgen.
+ discharge_cmp.
econstructor.
ptreesolve.
xomega.
xomega.
xomega.
xomega.
Qed.
End GETKERNELPABODY.
Theorem get_kernel_pa_code_correct:
spec_le (get_kernel_pa ↦ get_kernel_pa_spec_low) (〚get_kernel_pa ↦ f_get_kernel_pa 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (get_kernel_pa_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp m´0 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_get_kernel_pa)
(Vint pid :: Vint vaddr :: nil)
(create_undef_temps (fn_temps f_get_kernel_pa)))) H1.
Qed.
End GETKERNELPA.
End WithPrimitives.
End PAbQueueAtomicCode.