Library mcertikos.proc.PKContextNewCode
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 LoopProof.
Require Import VCGen.
Require Import RealParams.
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 AbstractDataType.
Require Import PKContextNew.
Require Import PKContextNewCSource.
Require Import SleeperGenSpec.
Module PKCONTEXTNEWCODE.
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}.
Local Open Scope Z_scope.
Section SLEEPERINC.
Let L: compatlayer (cdata RData) := SLEEPER_LOC ↦ sleeper_loc_type
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SLEEPERINCBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variable bsleeper_loc: block.
Hypothesis hsleeper_loc: Genv.find_symbol ge SLEEPER_LOC = Some bsleeper_loc.
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External (EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma sleeper_inc_body_correct: ∀ m m´ d env le curid sl,
env = PTree.empty _ →
curid = (CPU_ID d) →
Mem.load Mint32 ((m, d):mem) bsleeper_loc (curid × 4) = Some (Vint sl) →
Mem.store Mint32 ((m, d):mem) bsleeper_loc (curid × 4) (Vint (Int.repr (Int.unsigned sl + 1))) = Some (m´, d) →
0 ≤ Int.unsigned sl < num_proc →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_sleeper_inc_body E0 le´ (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
assert (int_size_val: sizeof tuint = 4).
{ simpl; reflexivity. }
intros; subst.
assert (cpu_id_range: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H5; trivial. }
set (cpuid := CPU_ID d).
fold cpuid in cpu_id_range, H1, H2.
assert (array_range: 0 ≤ sizeof tuint × cpuid < Int.max_unsigned).
{ rewrite int_size_val, muval.
omega. }
destruct H4.
assert (cpuid_val: cpuid = (Int.unsigned (Int.repr cpuid))).
{ rewrite Int.unsigned_repr; [reflexivity | omega]. }
unfold f_sleeper_inc_body; subst.
esplit; repeat vcgen.
- unfold get_CPU_ID_spec.
rewrite H, H0.
repeat f_equal.
exact cpuid_val.
- rewrite int_size_val.
rewrite <- cpuid_val.
replace (0 + 4 × CPU_ID d) with (CPU_ID d × 4); try ring.
simpl; simpl in H1.
vcgen; try exact H1.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
- repeat vcgen.
- repeat vcgen.
- rewrite int_size_val.
rewrite <- cpuid_val.
replace (0 + 4 × CPU_ID d) with (CPU_ID d × 4); try ring.
repeat vcgen.
simpl; simpl in H2.
vcgen.
exact H2.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
Qed.
End SLEEPERINCBody.
Theorem sleeper_inc_code_correct:
spec_le (sleeper_inc ↦ sleeper_inc_spec_low) (〚sleeper_inc ↦ f_sleeper_inc 〛L).
Proof.
fbigstep_pre L.
Require Import TacticsForTesting.
fbigsteptest (sleeper_inc_body_correct s (Genv.globalenv p)
makeglobalenv b0 H b2 Hb2fs Hb2fp m´0 m0 d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sleeper_inc)
(nil)
(create_undef_temps (fn_temps f_sleeper_inc)))) muval.
reflexivity.
omega.
intro stmt.
destruct stmt.
repeat fbigstep_post.
Qed.
End SLEEPERINC.
Section SLEEPERDEC.
Let L: compatlayer (cdata RData) := SLEEPER_LOC ↦ sleeper_loc_type
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SLEEPERDECBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variable bsleeper_loc: block.
Hypothesis hsleeper_loc: Genv.find_symbol ge SLEEPER_LOC = Some bsleeper_loc.
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External (EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma sleeper_dec_body_correct: ∀ m m´ d env le curid sl,
env = PTree.empty _ →
curid = (CPU_ID d) →
Mem.load Mint32 ((m, d):mem) bsleeper_loc (curid × 4) = Some (Vint sl) →
Mem.store Mint32 ((m, d):mem) bsleeper_loc (curid × 4) (Vint (Int.repr (Int.unsigned sl - 1))) = Some (m´, d) →
0 ≤ Int.unsigned sl < num_proc →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_sleeper_dec_body E0 le´ (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
assert (int_size_val: sizeof tuint = 4).
{ simpl; reflexivity. }
intros; subst.
assert (cpu_id_range: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H5; trivial. }
set (cpuid := CPU_ID d).
fold cpuid in cpu_id_range, H1, H2.
assert (array_range: 0 ≤ sizeof tuint × cpuid < Int.max_unsigned).
{ rewrite int_size_val, muval.
omega. }
destruct H4.
assert (cpuid_val: cpuid = (Int.unsigned (Int.repr cpuid))).
{ rewrite Int.unsigned_repr; [reflexivity | omega]. }
unfold f_sleeper_dec_body; subst.
esplit; repeat vcgen.
- unfold get_CPU_ID_spec.
rewrite H, H0.
repeat f_equal.
exact cpuid_val.
- rewrite int_size_val.
rewrite <- cpuid_val.
replace (0 + 4 × CPU_ID d) with (CPU_ID d × 4); try ring.
simpl; simpl in H1.
vcgen; try exact H1.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
- repeat vcgen.
- repeat vcgen.
- rewrite int_size_val.
rewrite <- cpuid_val.
replace (0 + 4 × CPU_ID d) with (CPU_ID d × 4); try ring.
simpl; simpl in H2.
repeat vcgen.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
Qed.
End SLEEPERDECBody.
Theorem sleeper_dec_code_correct:
spec_le (sleeper_dec ↦ sleeper_dec_spec_low) (〚sleeper_dec ↦ f_sleeper_dec 〛L).
Proof.
fbigstep_pre L.
assert (Int.unsigned sl < num_proc) by omega.
fbigstep (sleeper_dec_body_correct s (Genv.globalenv p)
makeglobalenv b0 H b2 Hb2fs Hb2fp m´0 m0 d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sleeper_dec)
(nil)
(create_undef_temps (fn_temps f_sleeper_dec)))) muval.
Qed.
End SLEEPERDEC.
Section SLEEPERZZZ.
Let L: compatlayer (cdata RData) := SLEEPER_LOC ↦ sleeper_loc_type
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SLEEPERZZZBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variable bsleeper_loc: block.
Hypothesis hsleeper_loc: Genv.find_symbol ge SLEEPER_LOC = Some bsleeper_loc.
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External (EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma sleeper_zzz_body_correct: ∀ m d env le curid to res,
env = PTree.empty _ →
curid = (CPU_ID d) →
Mem.load Mint32 ((m, d): mem) bsleeper_loc (curid × 4) = Some (Vint to) →
res = match Int.eq to Int.zero with
| true ⇒ Int.one
| _ ⇒ Int.zero
end →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_sleeper_zzz_body E0 le´ (m, d)
(Out_return (Some (Vint res, tint))).
Proof.
generalize max_unsigned_val; intro muval.
assert (int_size_val: sizeof tuint = 4).
{ simpl; reflexivity. }
intros; subst.
assert (cpu_id_range: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H4; trivial. }
set (cpuid := CPU_ID d).
fold cpuid in cpu_id_range, H1.
assert (array_range: 0 ≤ sizeof tuint × cpuid < Int.max_unsigned).
{ rewrite int_size_val, muval.
omega. }
destruct H3.
assert (cpuid_val: cpuid = (Int.unsigned (Int.repr cpuid))).
{ rewrite Int.unsigned_repr; [reflexivity | omega]. }
case_eq (zeq (Int.unsigned to) 0); intros.
- set (res := Vint (if Int.eq to Int.zero then Int.one else Int.zero)).
unfold f_sleeper_zzz_body; subst.
assert (res = Vint Int.one).
{ assert (to = Int.zero) by eauto using unsigned_inj.
unfold res.
rewrite H3.
rewrite Int.eq_true.
reflexivity. }
esplit; repeat vcgen.
+ unfold get_CPU_ID_spec.
rewrite H, H0.
repeat f_equal.
exact cpuid_val.
+ rewrite int_size_val.
rewrite <- cpuid_val.
replace (0 + 4 × CPU_ID d) with (CPU_ID d × 4); try ring.
simpl; simpl in H1.
vcgen; try exact H1.
+ rewrite int_size_val; rewrite Int.unsigned_repr; omega.
+ rewrite int_size_val; rewrite Int.unsigned_repr; omega.
+ repeat vcgen.
+ repeat vcgen.
+ simpl.
rewrite H3.
repeat vcgen.
- set (res := Vint (if Int.eq to Int.zero then Int.one else Int.zero)).
unfold f_sleeper_zzz_body; subst.
assert (res = Vint Int.zero).
{ assert (to ≠ Int.zero).
{ unfold not; intros.
elim n; subst.
rewrite Int.unsigned_zero; reflexivity. }
unfold res.
rewrite Int.eq_false; trivial.
}
esplit; repeat vcgen.
+ unfold get_CPU_ID_spec.
rewrite H, H0.
repeat f_equal.
exact cpuid_val.
+ rewrite int_size_val.
rewrite <- cpuid_val.
replace (0 + 4 × CPU_ID d) with (CPU_ID d × 4); try ring.
simpl; simpl in H1.
vcgen; try exact H1.
+ rewrite int_size_val; rewrite Int.unsigned_repr; omega.
+ rewrite int_size_val; rewrite Int.unsigned_repr; omega.
+ repeat vcgen.
+ repeat vcgen.
+ simpl.
rewrite H3.
repeat vcgen.
Qed.
End SLEEPERZZZBody.
Theorem sleeper_zzz_code_correct:
spec_le (sleeper_zzz ↦ sleeper_zzz_spec_low) (〚sleeper_zzz ↦ f_sleeper_zzz 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (sleeper_zzz_body_correct s (Genv.globalenv p)
makeglobalenv b0 H b2 Hb2fs Hb2fp m´0 d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sleeper_zzz)
(nil)
(create_undef_temps (fn_temps f_sleeper_zzz)))) muval.
Qed.
End SLEEPERZZZ.
End WithPrimitives.
End PKCONTEXTNEWCODE.
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 LoopProof.
Require Import VCGen.
Require Import RealParams.
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 AbstractDataType.
Require Import PKContextNew.
Require Import PKContextNewCSource.
Require Import SleeperGenSpec.
Module PKCONTEXTNEWCODE.
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}.
Local Open Scope Z_scope.
Section SLEEPERINC.
Let L: compatlayer (cdata RData) := SLEEPER_LOC ↦ sleeper_loc_type
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SLEEPERINCBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variable bsleeper_loc: block.
Hypothesis hsleeper_loc: Genv.find_symbol ge SLEEPER_LOC = Some bsleeper_loc.
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External (EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma sleeper_inc_body_correct: ∀ m m´ d env le curid sl,
env = PTree.empty _ →
curid = (CPU_ID d) →
Mem.load Mint32 ((m, d):mem) bsleeper_loc (curid × 4) = Some (Vint sl) →
Mem.store Mint32 ((m, d):mem) bsleeper_loc (curid × 4) (Vint (Int.repr (Int.unsigned sl + 1))) = Some (m´, d) →
0 ≤ Int.unsigned sl < num_proc →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_sleeper_inc_body E0 le´ (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
assert (int_size_val: sizeof tuint = 4).
{ simpl; reflexivity. }
intros; subst.
assert (cpu_id_range: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H5; trivial. }
set (cpuid := CPU_ID d).
fold cpuid in cpu_id_range, H1, H2.
assert (array_range: 0 ≤ sizeof tuint × cpuid < Int.max_unsigned).
{ rewrite int_size_val, muval.
omega. }
destruct H4.
assert (cpuid_val: cpuid = (Int.unsigned (Int.repr cpuid))).
{ rewrite Int.unsigned_repr; [reflexivity | omega]. }
unfold f_sleeper_inc_body; subst.
esplit; repeat vcgen.
- unfold get_CPU_ID_spec.
rewrite H, H0.
repeat f_equal.
exact cpuid_val.
- rewrite int_size_val.
rewrite <- cpuid_val.
replace (0 + 4 × CPU_ID d) with (CPU_ID d × 4); try ring.
simpl; simpl in H1.
vcgen; try exact H1.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
- repeat vcgen.
- repeat vcgen.
- rewrite int_size_val.
rewrite <- cpuid_val.
replace (0 + 4 × CPU_ID d) with (CPU_ID d × 4); try ring.
repeat vcgen.
simpl; simpl in H2.
vcgen.
exact H2.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
Qed.
End SLEEPERINCBody.
Theorem sleeper_inc_code_correct:
spec_le (sleeper_inc ↦ sleeper_inc_spec_low) (〚sleeper_inc ↦ f_sleeper_inc 〛L).
Proof.
fbigstep_pre L.
Require Import TacticsForTesting.
fbigsteptest (sleeper_inc_body_correct s (Genv.globalenv p)
makeglobalenv b0 H b2 Hb2fs Hb2fp m´0 m0 d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sleeper_inc)
(nil)
(create_undef_temps (fn_temps f_sleeper_inc)))) muval.
reflexivity.
omega.
intro stmt.
destruct stmt.
repeat fbigstep_post.
Qed.
End SLEEPERINC.
Section SLEEPERDEC.
Let L: compatlayer (cdata RData) := SLEEPER_LOC ↦ sleeper_loc_type
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SLEEPERDECBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variable bsleeper_loc: block.
Hypothesis hsleeper_loc: Genv.find_symbol ge SLEEPER_LOC = Some bsleeper_loc.
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External (EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma sleeper_dec_body_correct: ∀ m m´ d env le curid sl,
env = PTree.empty _ →
curid = (CPU_ID d) →
Mem.load Mint32 ((m, d):mem) bsleeper_loc (curid × 4) = Some (Vint sl) →
Mem.store Mint32 ((m, d):mem) bsleeper_loc (curid × 4) (Vint (Int.repr (Int.unsigned sl - 1))) = Some (m´, d) →
0 ≤ Int.unsigned sl < num_proc →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_sleeper_dec_body E0 le´ (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
assert (int_size_val: sizeof tuint = 4).
{ simpl; reflexivity. }
intros; subst.
assert (cpu_id_range: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H5; trivial. }
set (cpuid := CPU_ID d).
fold cpuid in cpu_id_range, H1, H2.
assert (array_range: 0 ≤ sizeof tuint × cpuid < Int.max_unsigned).
{ rewrite int_size_val, muval.
omega. }
destruct H4.
assert (cpuid_val: cpuid = (Int.unsigned (Int.repr cpuid))).
{ rewrite Int.unsigned_repr; [reflexivity | omega]. }
unfold f_sleeper_dec_body; subst.
esplit; repeat vcgen.
- unfold get_CPU_ID_spec.
rewrite H, H0.
repeat f_equal.
exact cpuid_val.
- rewrite int_size_val.
rewrite <- cpuid_val.
replace (0 + 4 × CPU_ID d) with (CPU_ID d × 4); try ring.
simpl; simpl in H1.
vcgen; try exact H1.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
- repeat vcgen.
- repeat vcgen.
- rewrite int_size_val.
rewrite <- cpuid_val.
replace (0 + 4 × CPU_ID d) with (CPU_ID d × 4); try ring.
simpl; simpl in H2.
repeat vcgen.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
- rewrite int_size_val; rewrite Int.unsigned_repr; omega.
Qed.
End SLEEPERDECBody.
Theorem sleeper_dec_code_correct:
spec_le (sleeper_dec ↦ sleeper_dec_spec_low) (〚sleeper_dec ↦ f_sleeper_dec 〛L).
Proof.
fbigstep_pre L.
assert (Int.unsigned sl < num_proc) by omega.
fbigstep (sleeper_dec_body_correct s (Genv.globalenv p)
makeglobalenv b0 H b2 Hb2fs Hb2fp m´0 m0 d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sleeper_dec)
(nil)
(create_undef_temps (fn_temps f_sleeper_dec)))) muval.
Qed.
End SLEEPERDEC.
Section SLEEPERZZZ.
Let L: compatlayer (cdata RData) := SLEEPER_LOC ↦ sleeper_loc_type
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SLEEPERZZZBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variable bsleeper_loc: block.
Hypothesis hsleeper_loc: Genv.find_symbol ge SLEEPER_LOC = Some bsleeper_loc.
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External (EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma sleeper_zzz_body_correct: ∀ m d env le curid to res,
env = PTree.empty _ →
curid = (CPU_ID d) →
Mem.load Mint32 ((m, d): mem) bsleeper_loc (curid × 4) = Some (Vint to) →
res = match Int.eq to Int.zero with
| true ⇒ Int.one
| _ ⇒ Int.zero
end →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_sleeper_zzz_body E0 le´ (m, d)
(Out_return (Some (Vint res, tint))).
Proof.
generalize max_unsigned_val; intro muval.
assert (int_size_val: sizeof tuint = 4).
{ simpl; reflexivity. }
intros; subst.
assert (cpu_id_range: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H4; trivial. }
set (cpuid := CPU_ID d).
fold cpuid in cpu_id_range, H1.
assert (array_range: 0 ≤ sizeof tuint × cpuid < Int.max_unsigned).
{ rewrite int_size_val, muval.
omega. }
destruct H3.
assert (cpuid_val: cpuid = (Int.unsigned (Int.repr cpuid))).
{ rewrite Int.unsigned_repr; [reflexivity | omega]. }
case_eq (zeq (Int.unsigned to) 0); intros.
- set (res := Vint (if Int.eq to Int.zero then Int.one else Int.zero)).
unfold f_sleeper_zzz_body; subst.
assert (res = Vint Int.one).
{ assert (to = Int.zero) by eauto using unsigned_inj.
unfold res.
rewrite H3.
rewrite Int.eq_true.
reflexivity. }
esplit; repeat vcgen.
+ unfold get_CPU_ID_spec.
rewrite H, H0.
repeat f_equal.
exact cpuid_val.
+ rewrite int_size_val.
rewrite <- cpuid_val.
replace (0 + 4 × CPU_ID d) with (CPU_ID d × 4); try ring.
simpl; simpl in H1.
vcgen; try exact H1.
+ rewrite int_size_val; rewrite Int.unsigned_repr; omega.
+ rewrite int_size_val; rewrite Int.unsigned_repr; omega.
+ repeat vcgen.
+ repeat vcgen.
+ simpl.
rewrite H3.
repeat vcgen.
- set (res := Vint (if Int.eq to Int.zero then Int.one else Int.zero)).
unfold f_sleeper_zzz_body; subst.
assert (res = Vint Int.zero).
{ assert (to ≠ Int.zero).
{ unfold not; intros.
elim n; subst.
rewrite Int.unsigned_zero; reflexivity. }
unfold res.
rewrite Int.eq_false; trivial.
}
esplit; repeat vcgen.
+ unfold get_CPU_ID_spec.
rewrite H, H0.
repeat f_equal.
exact cpuid_val.
+ rewrite int_size_val.
rewrite <- cpuid_val.
replace (0 + 4 × CPU_ID d) with (CPU_ID d × 4); try ring.
simpl; simpl in H1.
vcgen; try exact H1.
+ rewrite int_size_val; rewrite Int.unsigned_repr; omega.
+ rewrite int_size_val; rewrite Int.unsigned_repr; omega.
+ repeat vcgen.
+ repeat vcgen.
+ simpl.
rewrite H3.
repeat vcgen.
Qed.
End SLEEPERZZZBody.
Theorem sleeper_zzz_code_correct:
spec_le (sleeper_zzz ↦ sleeper_zzz_spec_low) (〚sleeper_zzz ↦ f_sleeper_zzz 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (sleeper_zzz_body_correct s (Genv.globalenv p)
makeglobalenv b0 H b2 Hb2fs Hb2fp m´0 d (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sleeper_zzz)
(nil)
(create_undef_temps (fn_temps f_sleeper_zzz)))) muval.
Qed.
End SLEEPERZZZ.
End WithPrimitives.
End PKCONTEXTNEWCODE.