Library mcertikos.devdrivers.DHandlerSwAsmCode
This file provide the contextual refinement proof between MPTInit layer and MPTBit layer
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.
Require Import DHandlerSw.
Require Import DHandlerSwAsmSource.
Require Import HandlerAsmGenSpec.
Require Import DHandlerSwAsmData.
Require Import LAsmModuleSemSpec.
Require Import LRegSet.
Require Import AbstractDataType.
Require Import ObjX86Proof.
Require Import ListLemma.
Section ASM_VERIFICATION.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := dhandlerintro_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.
Ltac accessors_simpl:=
match goal with
| |- exec_storeex _ _ _ _ _ _ _ = _ ⇒
unfold exec_storeex, LoadStoreSem2.exec_storeex2;
simpl; Lregset_simpl_tac;
match goal with
| |- context [Asm.exec_store _ _ _ _ _ _ _] ⇒
unfold Asm.exec_store; simpl;
Lregset_simpl_tac; lift_trivial
end
| |- exec_loadex _ _ _ _ _ _ = _ ⇒
unfold exec_loadex, LoadStoreSem2.exec_loadex2;
simpl; Lregset_simpl_tac;
match goal with
| |- context[Asm.exec_load _ _ _ _ _ _] ⇒
unfold Asm.exec_load; simpl;
Lregset_simpl_tac; lift_trivial
end
end.
Ltac clearAll := repeat match goal with
[H: _ |- _] ⇒ clear H
end.
Lemma serial_intr_handler_asm_code_correct_aux:
∀ ge (s: stencil) (rs rs´: regset) b b´ m0 mtmp mtmp´´ labd labd´
(settfb: find_symbol s set_tf = Some b´)
(settfrw: Mem.store Mint32 m0 b´ 0 (rs EDX) = Some mtmp)
(settfrd: Mem.load Mint32 mtmp b´ 0 = Some (rs EDX))
(settfrw1: Mem.store Mint32 mtmp b´ 0 (Vint Int.zero) = Some mtmp´´),
find_symbol s serial_intr_handler_asm = Some b →
make_globalenv s (serial_intr_handler_asm ↦ serial_intr_handler_asm_function) dhandlersw = ret ge →
rs PC = Vptr b Int.zero →
serial_intr_handler_asm_spec rs labd = Some (labd´, rs´) →
asm_invariant (mem := mwd LDATAOps) s rs (m0, labd) →
low_level_invariant (Mem.nextblock m0) labd →
high_level_invariant labd →
∃ f´ m0´ r_,
lasm_step (serial_intr_handler_asm ↦ serial_intr_handler_asm_function) (dhandlersw (Hmwd:= Hmwd) (Hmem:= Hmem)) serial_intr_handler_asm s rs
(m0, labd) (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) r_) (m0´, labd´)
∧ inject_incr (Mem.flat_inj (Mem.nextblock mtmp´´)) f´
∧ Memtype.Mem.inject f´ mtmp´´ m0´
∧ (Mem.nextblock mtmp´´ ≤ Mem.nextblock m0´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#PC <- (rs#RA) #RA <- Vundef))
(Pregmap.get l r_)).
Proof.
intros. inv H3.
rename H4 into HLOW. rename H5 into Hhigh.
caseEq(Mem.alloc mtmp 0 8).
intros m1 b0 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hnextblocktmp: Mem.nextblock m0 = Mem.nextblock mtmp).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ settfrw); trivial.
}
assert(Hnextblocktmp´´: Mem.nextblock m0 = Mem.nextblock mtmp´´).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ settfrw1); trivial.
}
assert (Hblock: Ple (Genv.genv_next ge) b0 ∧ Plt b0 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
rewrite <- Hnextblocktmp.
split; xomega.
}
exploit Hsave_context; eauto.
intros [[b_save_context [Hsave_context_symbol Hsave_context_fun] prim_save_context]].
exploit Hserial_intr_handler_sw; eauto.
intros [[b_serial_intr_handler_sw [Hswitch_symbol Hswitch_fun]] prim_serial_intr_handler_sw].
exploit Hrestore_context; eauto.
intros [[b_restore_context [Hrestore_context_symbol Hrestore_context_fun] prim_restore_context]].
exploit Hserial_intr_handler_asm; eauto.
intros b_serial_intr_handler_asm.
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
assert (HV1: Mem.valid_access m1 Mint32 b0 0 Freeable).
{
eapply H3; auto; simpl; try omega. unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b0 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply H3; auto; simpl; try omega.
unfold Z.divide. ∃ 1; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert(Hnextblock2: Mem.nextblock m2 = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
}
assert(Hnextblock3: Mem.nextblock m3 = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
}
assert (HV´: Mem.valid_access m3 Mint32 b´ 0 Writable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.valid_access_alloc_other; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_3; eauto.
}
destruct (Mem.valid_access_store _ _ _ _ (Vint Int.zero) HV´) as [mtmp´ HST´].
assert(Hnextblockmtmp´: Mem.nextblock mtmp´ = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST´); trivial.
}
assert (HV3: Mem.range_perm mtmp´ b0 0 8 Cur Freeable).
{
unfold Mem.range_perm. intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
destruct (Mem.range_perm_free _ _ _ _ HV3) as [m4 HFree].
destruct (serial_intr_handler_asm_generate _ _ _ _ _ H2 HLOW Hhigh) as
[labd0[labd1[HEX1[HEX3[HEX2 HP]]]]].
destruct HP as [HIK[HIH[HIK0[HIH0[HIK1 HIH1]]]]].
clear HLOW.
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption.
rewrite H1.
econstructor; eauto.
assert(symofs: symbol_offset ge set_tf Int.zero = Vptr b´ (Int.zero)).
{
unfold symbol_offset.
rewrite (stencil_matches_symbols _ _ Hstencil_matches set_tf).
rewrite settfb.
reflexivity.
}
assert (Hge: ∀ i, find_symbol s i = Genv.find_symbol ge i).
{
intros.
erewrite <- stencil_matches_symbols. reflexivity. assumption.
}
assert (Hgenv: genv_next s = Genv.genv_next ge).
{
erewrite stencil_matches_genv_next. reflexivity. assumption.
}
assert (b0_neq_b´: b´ ≠ b0).
{
exploit (genv_symb_range). eapply settfb. rewrite Hgenv. intros.
destruct Hblock.
generalize H5. generalize H4.
clearAll.
intros.
intro.
rewrite H in H4.
xomega.
}
assert(load_edx_same: Mem.load Mint32 m3 b´ 0 = Mem.load Mint32 mtmp b´ 0).
{
exploit (Mem.load_store_other Mint32 m2 b0 4 _ m3 HST2 Mint32 b´ 0). left. assumption.
exploit (Mem.load_store_other Mint32 m1 b0 0 _ m2 HST1 Mint32 b´ 0). left. assumption.
exploit (Mem.load_alloc_other). eapply HALC. eapply settfrd.
intros.
rewrite H6, H5. rewrite H4. rewrite settfrd. reflexivity.
}
assert (Hbltge: Plt b (Genv.genv_next ge)).
{
exploit (genv_symb_range). eapply H. rewrite Hgenv. intros. assumption.
}
assert (Hbsave_contextltge: Plt b_save_context (Genv.genv_next ge)).
{
exploit (Genv.genv_symb_range). unfold Genv.find_symbol in Hsave_context_symbol.
eapply Hsave_context_symbol. clearAll. auto.
}
assert (Hbrestore_contextltge: Plt b_restore_context (Genv.genv_next ge)).
{
exploit (Genv.genv_symb_range). unfold Genv.find_symbol in Hrestore_context_symbol.
eapply Hrestore_context_symbol. clearAll. auto.
}
assert (Hbhandlerltge: Plt b_serial_intr_handler_sw (Genv.genv_next ge)).
{
exploit (Genv.genv_symb_range). unfold Genv.find_symbol in Hswitch_symbol.
eapply Hswitch_symbol. clearAll. auto.
}
assert (Htmpm1: Mem.nextblock m1 = Pos.succ (Mem.nextblock mtmp)).
{
eapply (Mem.nextblock_alloc). eapply HALC.
}
one_step_forward´.
unfold exec_storeex.
unfold LoadStoreSem1.exec_storeex1.
unfold AddrMake.
simpl.
rewrite symofs.
rewrite HIK, HIH.
unfold Asm.exec_store.
Lregset_simpl_tac.
rewrite symofs.
change (Int.add (Int.add Int.zero Int.zero) Int.zero) with (Int.zero).
unfold Mem.storev.
change (Int.unsigned Int.zero) with 0.
lift_trivial.
unfold lift.
simpl.
rewrite settfrw.
reflexivity.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1. simpl. rewrite HST2.
reflexivity.
one_step_forward´.
unfold exec_loadex.
unfold LoadStoreSem1.exec_loadex1.
unfold AddrMake.
simpl.
rewrite symofs.
rewrite HIK, HIH.
unfold Asm.exec_load.
Lregset_simpl_tac.
simpl.
rewrite symofs.
change (Int.add (Int.add Int.zero Int.zero) Int.zero) with (Int.zero).
unfold Mem.loadv.
change (Int.unsigned Int.zero) with 0.
lift_trivial.
unfold lift.
simpl.
rewrite load_edx_same.
rewrite settfrd.
reflexivity.
Lregset_simpl_tac.
one_step_forward´.
unfold symbol_offset. unfold fundef.
rewrite Hsave_context_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_prim_call _ b_save_context); eauto 1; trivial.
econstructor.
refine_split´; eauto.
econstructor; eauto 1. simpl.
econstructor.
unfold save_context_spec.
Lregset_simpl_tac.
reflexivity.
simpl.
auto.
inv inv_inject_neutral.
intros.
rewrite Hnextblock3.
erewrite Mem.nextblock_alloc; eauto.
rewrite <- Hnextblocktmp.
Lregset_simpl_tac.
generalize (Mem.alloc_result _ _ _ _ _ HALC); intro nb0.
functional inversion H4; subst; simpl; eauto.
rewrite <- Hnextblocktmp.
econstructor.
unfold Mem.flat_inj.
destruct (plt (Mem.nextblock m0) (Pos.succ (Mem.nextblock m0))).
reflexivity.
xomega.
reflexivity.
eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega.
eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega.
eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega.
eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega.
econstructor.
unfold Mem.flat_inj.
destruct (plt b (Pos.succ (Mem.nextblock m0))).
reflexivity.
{
exploit (genv_symb_range). eapply H. rewrite Hgenv. intros.
assert (Pge b (Pos.succ (Mem.nextblock m0))) by xomega.
exploit (Mem.nextblock_alloc). eapply HALC. intros.
destruct Hblock.
generalize H8, H7, H6, H5, Hnextblocktmp. clearAll.
intros. rewrite <- Hnextblocktmp in ×.
assert (Plt (Mem.nextblock m0) b) by xomega. xomega.
}
reflexivity.
simpl.
Lregset_simpl_tac.
one_step_forward´.
unfold symbol_offset. unfold fundef.
rewrite Hswitch_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_external _ b_serial_intr_handler_sw); eauto; trivial. simpl.
constructor_gen_sem_intro.
Lregset_simpl_tac. lift_trivial.
simpl.
econstructor; eauto.
repeat constructor.
red. red. red. red. red. red.
change positive with ident in ×.
rewrite prim_serial_intr_handler_sw.
refine_split´; try reflexivity.
econstructor; eauto.
refine_split´; try reflexivity; try eassumption.
simpl. repeat split.
functional inversion HEX1; subst; simpl in ×.
change (Int.add (Int.add (Int.add
(Int.add Int.zero Int.one)
Int.one) Int.one) Int.one) with (Int.repr 4).
generalize (serial_intr_handler_sw_spec_independent_from_tf _ _ (tf labd ++
{|
DeviceStateDataType.tf_regs := Lregset_fold
{|
LPC := Vptr b_save_context Int.zero;
LRA := Vptr b (Int.repr 4);
LEAX := rs EAX;
LEBX := rs EBX;
LECX := rs ECX;
LEDX := rs EDX;
LESI := rs ESI;
LEDI := rs EDI;
LEBP := rs EBP;
LESP := Vptr b0 Int.zero;
LST0 := rs ST0;
LZF := Vundef;
LCF := Vundef;
LPF := Vundef;
LSF := Vundef;
LOF := Vundef;
LXMM0 := rs XMM0;
LXMM1 := rs XMM1;
LXMM2 := rs XMM2;
LXMM3 := rs XMM3;
LXMM4 := rs XMM4;
LXMM5 := rs XMM5;
LXMM6 := rs XMM6;
LXMM7 := rs XMM7 |};
DeviceStateDataType.tf_trapno := curr_intr_num labd;
DeviceStateDataType.tf_err := 0;
DeviceStateDataType.tf_esp := Vptr b0 Int.zero |} :: nil) HEX3); intro tmp.
apply tmp.
Lregset_simpl_tac.
lift_trivial.
intros. inv H4.
rewrite Hnextblock3; assumption.
discriminate.
discriminate.
Lregset_simpl_tac.
change (Int.add
(Int.add
(Int.add
(Int.add (Int.add Int.zero Int.one) Int.one)
Int.one) Int.one) Int.one) with (Int.repr 5).
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
unfold exec_storeex.
unfold LoadStoreSem1.exec_storeex1.
unfold AddrMake.
simpl.
rewrite symofs.
rewrite HIK1, HIH1.
unfold Asm.exec_store.
Lregset_simpl_tac.
rewrite symofs.
change (Int.add (Int.add Int.zero Int.zero) Int.zero) with (Int.zero).
unfold Mem.storev.
change (Int.unsigned Int.zero) with 0.
lift_trivial.
unfold lift.
simpl.
rewrite HST´.
reflexivity.
one_step_forward´.
unfold symbol_offset. unfold fundef.
rewrite Hrestore_context_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_prim_call _ b_restore_context); eauto 1; trivial.
econstructor.
refine_split´; eauto.
econstructor; eauto 1. simpl.
econstructor.
unfold restore_context_spec.
Lregset_simpl_tac.
simpl.
case_eq (tf labd ++
{|
DeviceStateDataType.tf_regs := Lregset_fold
{|
LPC := Vptr b_save_context Int.zero;
LRA := Vptr b (Int.repr 4);
LEAX := rs EAX;
LEBX := rs EBX;
LECX := rs ECX;
LEDX := rs EDX;
LESI := rs ESI;
LEDI := rs EDI;
LEBP := rs EBP;
LESP := Vptr b0 Int.zero;
LST0 := rs ST0;
LZF := Vundef;
LCF := Vundef;
LPF := Vundef;
LSF := Vundef;
LOF := Vundef;
LXMM0 := rs XMM0;
LXMM1 := rs XMM1;
LXMM2 := rs XMM2;
LXMM3 := rs XMM3;
LXMM4 := rs XMM4;
LXMM5 := rs XMM5;
LXMM6 := rs XMM6;
LXMM7 := rs XMM7 |};
DeviceStateDataType.tf_trapno := curr_intr_num labd;
DeviceStateDataType.tf_err := 0;
DeviceStateDataType.tf_esp := Vptr b0 Int.zero |} :: nil); intros.
apply app_eq_nil in H4.
destruct H4.
inv H5.
rewrite <- H4.
repeat rewrite removelast_app.
repeat rewrite last_concat.
simpl.
reflexivity.
intro contra; inv contra.
intro contra; inv contra.
simpl.
generalize inv_reg_wt; intro tmp_wt.
unfold AsmX.wt_regset in ×.
intros.
specialize (inv_reg_wt r).
destruct r; simpl in *; eauto.
destruct i; simpl in *; eauto.
Lregset_simpl_tac.
destruct f; simpl in *; eauto.
destruct c; simpl in *; eauto.
Lregset_simpl_tac.
auto.
inv inv_inject_neutral.
intros.
rewrite Hnextblockmtmp´.
erewrite Mem.nextblock_alloc; eauto.
rewrite <- Hnextblocktmp.
Lregset_simpl_tac.
generalize (Mem.alloc_result _ _ _ _ _ HALC); intro nb0.
generalize (inv_reg_inject_neutral r); intro.
destruct r; simpl in ×.
econstructor.
unfold Mem.flat_inj.
destruct (plt b_save_context (Pos.succ (Mem.nextblock m0))).
reflexivity.
{
generalize n, Hbsave_contextltge, Hblock, Hnextblocktmp, Htmpm1. clearAll. intros.
assert (Pge b_save_context (Pos.succ (Mem.nextblock m0))) by xomega.
destruct Hblock. rewrite Hnextblocktmp in ×. rewrite <- Htmpm1 in ×.
xomega.
}
reflexivity.
destruct i; simpl in *; eauto;
try (eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega).
econstructor.
unfold Mem.flat_inj.
rewrite nb0.
rewrite <- Hnextblocktmp.
destruct (plt (Mem.nextblock m0) (Pos.succ (Mem.nextblock m0))).
reflexivity.
xomega.
reflexivity.
destruct f; simpl in *; eauto;
try (eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega).
eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega.
destruct c; simpl in *; eauto;
try (eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega).
econstructor.
unfold Mem.flat_inj.
destruct (plt b (Pos.succ (Mem.nextblock m0))).
reflexivity.
{
generalize n, Hbltge, Hblock, Hnextblocktmp, Htmpm1. clearAll. intros.
assert (Pge b (Pos.succ (Mem.nextblock m0))) by xomega.
destruct Hblock. rewrite Hnextblocktmp in ×. rewrite <- Htmpm1 in ×.
xomega.
}
reflexivity.
simpl.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
unfold set; simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
erewrite register_type_load_result.
rewrite HFree. reflexivity.
apply inv_reg_wt.
right. left. simpl. omega.
Lregset_simpl_tac.
rewrite register_type_load_result by (apply inv_reg_wt; eauto).
one_step_forward´.
simpl.
Lregset_simpl_tac.
rewrite app_nil_r.
assert (tf_eq: ∀ d tf1 tf2, d {tf: tf1} {tf: tf2} = d {tf: tf2}) by (intros; reflexivity).
rewrite tf_eq.
functional inversion HEX2; subst.
assert (tf labd´ = tf labd ++
{|
DeviceStateDataType.tf_regs := rs;
DeviceStateDataType.tf_trapno := curr_intr_num labd;
DeviceStateDataType.tf_err := 0;
DeviceStateDataType.tf_esp := rs ESP |} :: nil).
{
generalize HEX3. clearAll. intros.
remember (save_context_spec rs labd) as d1.
functional inversion Heqd1.
functional inversion HEX3.
functional inversion H6;
functional inversion H5; simpl; rewrite <- H; simpl; reflexivity.
}
rewrite H5 in H4.
symmetry in H4.
apply app_eq_nil in H4.
destruct H4.
inv H6.
assert (tf labd1 = tf labd ++
{|
DeviceStateDataType.tf_regs := rs;
DeviceStateDataType.tf_trapno := curr_intr_num labd;
DeviceStateDataType.tf_err := 0;
DeviceStateDataType.tf_esp := rs ESP |} :: nil).
{
generalize HEX3. clearAll. intros.
remember (save_context_spec rs labd) as d1.
functional inversion Heqd1.
functional inversion HEX3.
functional inversion H6;
functional inversion H5; simpl; rewrite <- H; simpl; reflexivity.
}
rewrite H4.
rewrite removelast_app.
simpl.
rewrite app_nil_r.
simpl.
unfold AsmX.wt_regset in inv_reg_wt.
instantiate (2:= (Lregset_fold
{|
LPC := rs RA;
LRA := Vundef;
LEAX := rs EAX;
LEBX := rs EBX;
LECX := rs ECX;
LEDX := rs EDX;
LESI := rs ESI;
LEDI := rs EDI;
LEBP := rs EBP;
LESP := rs ESP;
LST0 := rs ST0;
LZF := rs ZF;
LCF := rs CF;
LPF := rs PF;
LSF := rs SF;
LOF := rs OF;
LXMM0 := rs XMM0;
LXMM1 := rs XMM1;
LXMM2 := rs XMM2;
LXMM3 := rs XMM3;
LXMM4 := rs XMM4;
LXMM5 := rs XMM5;
LXMM6 := rs XMM6;
LXMM7 := rs XMM7 |})).
Lregset_simpl_tac.
eapply star_refl.
intro contra; inv contra.
reflexivity.
reflexivity.
assert (HFB: ∀ b1 delta, Mem.flat_inj (Mem.nextblock m0) b1 ≠ Some (b0, delta)).
{
intros. unfold Mem.flat_inj.
red; intros.
destruct (plt b1 (Mem.nextblock m0)). inv H4.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
rewrite Hnextblocktmp in p.
xomega.
inv H4.
}
rewrite Hnextblocktmp´´ in HFB.
eapply Mem.free_right_inject; eauto; [|intros; specialize (HFB b1 delta); apply HFB; trivial].
rewrite <- Hnextblocktmp´´.
rewrite Hnextblocktmp.
assert (b´plt: Plt b´ (Mem.nextblock m0)).
{
inv inv_inject_neutral.
eapply genv_symb_range in settfb.
generalize Hnextblocktmp, inv_mem_valid, settfb; clearAll.
lift_simpl.
unfold lift; simpl.
intros.
xomega.
}
assert (Mem.inject (Mem.flat_inj (Mem.nextblock mtmp)) mtmp m3).
{
rewrite <- Hnextblocktmp´´ in HFB.
rewrite Hnextblocktmp in HFB.
repeat (eapply Mem.store_outside_inject; [ | | eassumption]
; [|intros b1 delta; intros; specialize (HFB b1 delta); apply HFB; trivial]).
eapply Mem.alloc_right_inject; eauto.
inv inv_inject_neutral.
apply Mem.neutral_inject; trivial.
rewrite <- Hnextblocktmp.
eapply Mem.store_inject_neutral; eauto.
}
exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b´ 0 (Vint Int.zero) H4 settfrw1); eauto.
unfold Mem.flat_inj.
rewrite <- Hnextblocktmp.
destruct (plt b´ (Mem.nextblock m0)).
reflexivity.
xomega.
intros[n2 [store inject]].
simpl in store.
rewrite HST´ in store; inv store.
apply inject.
generalize (Mem.nextblock_free _ _ _ _ _ HFree); intro.
rewrite H4, <- Hnextblocktmp´´, Hnextblocktmp.
generalize (Mem.nextblock_alloc _ _ _ _ _ HALC); intro.
rewrite Hnextblockmtmp´.
rewrite H5.
xomega.
unfold Lregset_fold; simpl.
intros reg.
functional inversion HEX1; subst; simpl in ×.
generalize (serial_intr_handler_sw_spec_does_not_change_tf _ _ HEX3); intro.
functional inversion HEX2; subst; simpl in ×.
rewrite H6 in H4.
symmetry in H4.
apply app_eq_nil in H4.
destruct H4.
inv H5.
rewrite H4.
rewrite last_concat.
simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF; inv HF.
intro contra; inv contra.
Qed.
Lemma serial_intr_handler_asm_code_correct:
asm_spec_le (serial_intr_handler_asm ↦ serial_intr_handler_asm_spec_low)
(〚 serial_intr_handler_asm ↦ serial_intr_handler_asm_function 〛 dhandlersw).
Proof.
eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b =
Some (Internal serial_intr_handler_asm_function)).
{
assert (Hmodule:
get_module_function serial_intr_handler_asm (serial_intr_handler_asm ↦ serial_intr_handler_asm_function)
= OK (Some serial_intr_handler_asm_function)) by reflexivity.
assert (HInternal:
make_internal serial_intr_handler_asm_function
= OK (AST.Internal serial_intr_handler_asm_function)) by reflexivity.
eapply make_globalenv_get_module_function in H0; eauto.
destruct H0 as [?[Hsymbol´ ?]].
inv Hstencil_matches.
rewrite stencil_matches_symbols in Hsymbol´.
rewrite H6 in Hsymbol´. inv Hsymbol´.
assumption.
}
assert(Hnextblocktmp: Mem.nextblock m0 = Mem.nextblock mtmp).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ H3); trivial.
}
assert(Hnextblockm1: Mem.nextblock mtmp = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ H5); trivial.
}
exploit serial_intr_handler_asm_code_correct_aux; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).
split.
lift_simpl.
unfold lift; simpl.
rewrite Hnextblocktmp, Hnextblockm1.
xomega.
∃ f´, (m0´, labd´). esplit.
repeat split; try eassumption.
simpl; unfold lift; simpl.
exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
intros.
simpl.
generalize (Hlessdef l); intro.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
destruct l; simpl in *; try apply H.
assert (PC = PC) by reflexivity; contradiction.
assert (RA = RA) by reflexivity; contradiction.
Qed.
End WITHMEM.
End ASM_VERIFICATION.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.
Require Import DHandlerSw.
Require Import DHandlerSwAsmSource.
Require Import HandlerAsmGenSpec.
Require Import DHandlerSwAsmData.
Require Import LAsmModuleSemSpec.
Require Import LRegSet.
Require Import AbstractDataType.
Require Import ObjX86Proof.
Require Import ListLemma.
Section ASM_VERIFICATION.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := dhandlerintro_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.
Ltac accessors_simpl:=
match goal with
| |- exec_storeex _ _ _ _ _ _ _ = _ ⇒
unfold exec_storeex, LoadStoreSem2.exec_storeex2;
simpl; Lregset_simpl_tac;
match goal with
| |- context [Asm.exec_store _ _ _ _ _ _ _] ⇒
unfold Asm.exec_store; simpl;
Lregset_simpl_tac; lift_trivial
end
| |- exec_loadex _ _ _ _ _ _ = _ ⇒
unfold exec_loadex, LoadStoreSem2.exec_loadex2;
simpl; Lregset_simpl_tac;
match goal with
| |- context[Asm.exec_load _ _ _ _ _ _] ⇒
unfold Asm.exec_load; simpl;
Lregset_simpl_tac; lift_trivial
end
end.
Ltac clearAll := repeat match goal with
[H: _ |- _] ⇒ clear H
end.
Lemma serial_intr_handler_asm_code_correct_aux:
∀ ge (s: stencil) (rs rs´: regset) b b´ m0 mtmp mtmp´´ labd labd´
(settfb: find_symbol s set_tf = Some b´)
(settfrw: Mem.store Mint32 m0 b´ 0 (rs EDX) = Some mtmp)
(settfrd: Mem.load Mint32 mtmp b´ 0 = Some (rs EDX))
(settfrw1: Mem.store Mint32 mtmp b´ 0 (Vint Int.zero) = Some mtmp´´),
find_symbol s serial_intr_handler_asm = Some b →
make_globalenv s (serial_intr_handler_asm ↦ serial_intr_handler_asm_function) dhandlersw = ret ge →
rs PC = Vptr b Int.zero →
serial_intr_handler_asm_spec rs labd = Some (labd´, rs´) →
asm_invariant (mem := mwd LDATAOps) s rs (m0, labd) →
low_level_invariant (Mem.nextblock m0) labd →
high_level_invariant labd →
∃ f´ m0´ r_,
lasm_step (serial_intr_handler_asm ↦ serial_intr_handler_asm_function) (dhandlersw (Hmwd:= Hmwd) (Hmem:= Hmem)) serial_intr_handler_asm s rs
(m0, labd) (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) r_) (m0´, labd´)
∧ inject_incr (Mem.flat_inj (Mem.nextblock mtmp´´)) f´
∧ Memtype.Mem.inject f´ mtmp´´ m0´
∧ (Mem.nextblock mtmp´´ ≤ Mem.nextblock m0´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#PC <- (rs#RA) #RA <- Vundef))
(Pregmap.get l r_)).
Proof.
intros. inv H3.
rename H4 into HLOW. rename H5 into Hhigh.
caseEq(Mem.alloc mtmp 0 8).
intros m1 b0 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hnextblocktmp: Mem.nextblock m0 = Mem.nextblock mtmp).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ settfrw); trivial.
}
assert(Hnextblocktmp´´: Mem.nextblock m0 = Mem.nextblock mtmp´´).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ settfrw1); trivial.
}
assert (Hblock: Ple (Genv.genv_next ge) b0 ∧ Plt b0 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
rewrite <- Hnextblocktmp.
split; xomega.
}
exploit Hsave_context; eauto.
intros [[b_save_context [Hsave_context_symbol Hsave_context_fun] prim_save_context]].
exploit Hserial_intr_handler_sw; eauto.
intros [[b_serial_intr_handler_sw [Hswitch_symbol Hswitch_fun]] prim_serial_intr_handler_sw].
exploit Hrestore_context; eauto.
intros [[b_restore_context [Hrestore_context_symbol Hrestore_context_fun] prim_restore_context]].
exploit Hserial_intr_handler_asm; eauto.
intros b_serial_intr_handler_asm.
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
assert (HV1: Mem.valid_access m1 Mint32 b0 0 Freeable).
{
eapply H3; auto; simpl; try omega. unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b0 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply H3; auto; simpl; try omega.
unfold Z.divide. ∃ 1; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert(Hnextblock2: Mem.nextblock m2 = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
}
assert(Hnextblock3: Mem.nextblock m3 = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
}
assert (HV´: Mem.valid_access m3 Mint32 b´ 0 Writable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.valid_access_alloc_other; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_3; eauto.
}
destruct (Mem.valid_access_store _ _ _ _ (Vint Int.zero) HV´) as [mtmp´ HST´].
assert(Hnextblockmtmp´: Mem.nextblock mtmp´ = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST´); trivial.
}
assert (HV3: Mem.range_perm mtmp´ b0 0 8 Cur Freeable).
{
unfold Mem.range_perm. intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
destruct (Mem.range_perm_free _ _ _ _ HV3) as [m4 HFree].
destruct (serial_intr_handler_asm_generate _ _ _ _ _ H2 HLOW Hhigh) as
[labd0[labd1[HEX1[HEX3[HEX2 HP]]]]].
destruct HP as [HIK[HIH[HIK0[HIH0[HIK1 HIH1]]]]].
clear HLOW.
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption.
rewrite H1.
econstructor; eauto.
assert(symofs: symbol_offset ge set_tf Int.zero = Vptr b´ (Int.zero)).
{
unfold symbol_offset.
rewrite (stencil_matches_symbols _ _ Hstencil_matches set_tf).
rewrite settfb.
reflexivity.
}
assert (Hge: ∀ i, find_symbol s i = Genv.find_symbol ge i).
{
intros.
erewrite <- stencil_matches_symbols. reflexivity. assumption.
}
assert (Hgenv: genv_next s = Genv.genv_next ge).
{
erewrite stencil_matches_genv_next. reflexivity. assumption.
}
assert (b0_neq_b´: b´ ≠ b0).
{
exploit (genv_symb_range). eapply settfb. rewrite Hgenv. intros.
destruct Hblock.
generalize H5. generalize H4.
clearAll.
intros.
intro.
rewrite H in H4.
xomega.
}
assert(load_edx_same: Mem.load Mint32 m3 b´ 0 = Mem.load Mint32 mtmp b´ 0).
{
exploit (Mem.load_store_other Mint32 m2 b0 4 _ m3 HST2 Mint32 b´ 0). left. assumption.
exploit (Mem.load_store_other Mint32 m1 b0 0 _ m2 HST1 Mint32 b´ 0). left. assumption.
exploit (Mem.load_alloc_other). eapply HALC. eapply settfrd.
intros.
rewrite H6, H5. rewrite H4. rewrite settfrd. reflexivity.
}
assert (Hbltge: Plt b (Genv.genv_next ge)).
{
exploit (genv_symb_range). eapply H. rewrite Hgenv. intros. assumption.
}
assert (Hbsave_contextltge: Plt b_save_context (Genv.genv_next ge)).
{
exploit (Genv.genv_symb_range). unfold Genv.find_symbol in Hsave_context_symbol.
eapply Hsave_context_symbol. clearAll. auto.
}
assert (Hbrestore_contextltge: Plt b_restore_context (Genv.genv_next ge)).
{
exploit (Genv.genv_symb_range). unfold Genv.find_symbol in Hrestore_context_symbol.
eapply Hrestore_context_symbol. clearAll. auto.
}
assert (Hbhandlerltge: Plt b_serial_intr_handler_sw (Genv.genv_next ge)).
{
exploit (Genv.genv_symb_range). unfold Genv.find_symbol in Hswitch_symbol.
eapply Hswitch_symbol. clearAll. auto.
}
assert (Htmpm1: Mem.nextblock m1 = Pos.succ (Mem.nextblock mtmp)).
{
eapply (Mem.nextblock_alloc). eapply HALC.
}
one_step_forward´.
unfold exec_storeex.
unfold LoadStoreSem1.exec_storeex1.
unfold AddrMake.
simpl.
rewrite symofs.
rewrite HIK, HIH.
unfold Asm.exec_store.
Lregset_simpl_tac.
rewrite symofs.
change (Int.add (Int.add Int.zero Int.zero) Int.zero) with (Int.zero).
unfold Mem.storev.
change (Int.unsigned Int.zero) with 0.
lift_trivial.
unfold lift.
simpl.
rewrite settfrw.
reflexivity.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1. simpl. rewrite HST2.
reflexivity.
one_step_forward´.
unfold exec_loadex.
unfold LoadStoreSem1.exec_loadex1.
unfold AddrMake.
simpl.
rewrite symofs.
rewrite HIK, HIH.
unfold Asm.exec_load.
Lregset_simpl_tac.
simpl.
rewrite symofs.
change (Int.add (Int.add Int.zero Int.zero) Int.zero) with (Int.zero).
unfold Mem.loadv.
change (Int.unsigned Int.zero) with 0.
lift_trivial.
unfold lift.
simpl.
rewrite load_edx_same.
rewrite settfrd.
reflexivity.
Lregset_simpl_tac.
one_step_forward´.
unfold symbol_offset. unfold fundef.
rewrite Hsave_context_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_prim_call _ b_save_context); eauto 1; trivial.
econstructor.
refine_split´; eauto.
econstructor; eauto 1. simpl.
econstructor.
unfold save_context_spec.
Lregset_simpl_tac.
reflexivity.
simpl.
auto.
inv inv_inject_neutral.
intros.
rewrite Hnextblock3.
erewrite Mem.nextblock_alloc; eauto.
rewrite <- Hnextblocktmp.
Lregset_simpl_tac.
generalize (Mem.alloc_result _ _ _ _ _ HALC); intro nb0.
functional inversion H4; subst; simpl; eauto.
rewrite <- Hnextblocktmp.
econstructor.
unfold Mem.flat_inj.
destruct (plt (Mem.nextblock m0) (Pos.succ (Mem.nextblock m0))).
reflexivity.
xomega.
reflexivity.
eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega.
eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega.
eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega.
eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega.
econstructor.
unfold Mem.flat_inj.
destruct (plt b (Pos.succ (Mem.nextblock m0))).
reflexivity.
{
exploit (genv_symb_range). eapply H. rewrite Hgenv. intros.
assert (Pge b (Pos.succ (Mem.nextblock m0))) by xomega.
exploit (Mem.nextblock_alloc). eapply HALC. intros.
destruct Hblock.
generalize H8, H7, H6, H5, Hnextblocktmp. clearAll.
intros. rewrite <- Hnextblocktmp in ×.
assert (Plt (Mem.nextblock m0) b) by xomega. xomega.
}
reflexivity.
simpl.
Lregset_simpl_tac.
one_step_forward´.
unfold symbol_offset. unfold fundef.
rewrite Hswitch_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_external _ b_serial_intr_handler_sw); eauto; trivial. simpl.
constructor_gen_sem_intro.
Lregset_simpl_tac. lift_trivial.
simpl.
econstructor; eauto.
repeat constructor.
red. red. red. red. red. red.
change positive with ident in ×.
rewrite prim_serial_intr_handler_sw.
refine_split´; try reflexivity.
econstructor; eauto.
refine_split´; try reflexivity; try eassumption.
simpl. repeat split.
functional inversion HEX1; subst; simpl in ×.
change (Int.add (Int.add (Int.add
(Int.add Int.zero Int.one)
Int.one) Int.one) Int.one) with (Int.repr 4).
generalize (serial_intr_handler_sw_spec_independent_from_tf _ _ (tf labd ++
{|
DeviceStateDataType.tf_regs := Lregset_fold
{|
LPC := Vptr b_save_context Int.zero;
LRA := Vptr b (Int.repr 4);
LEAX := rs EAX;
LEBX := rs EBX;
LECX := rs ECX;
LEDX := rs EDX;
LESI := rs ESI;
LEDI := rs EDI;
LEBP := rs EBP;
LESP := Vptr b0 Int.zero;
LST0 := rs ST0;
LZF := Vundef;
LCF := Vundef;
LPF := Vundef;
LSF := Vundef;
LOF := Vundef;
LXMM0 := rs XMM0;
LXMM1 := rs XMM1;
LXMM2 := rs XMM2;
LXMM3 := rs XMM3;
LXMM4 := rs XMM4;
LXMM5 := rs XMM5;
LXMM6 := rs XMM6;
LXMM7 := rs XMM7 |};
DeviceStateDataType.tf_trapno := curr_intr_num labd;
DeviceStateDataType.tf_err := 0;
DeviceStateDataType.tf_esp := Vptr b0 Int.zero |} :: nil) HEX3); intro tmp.
apply tmp.
Lregset_simpl_tac.
lift_trivial.
intros. inv H4.
rewrite Hnextblock3; assumption.
discriminate.
discriminate.
Lregset_simpl_tac.
change (Int.add
(Int.add
(Int.add
(Int.add (Int.add Int.zero Int.one) Int.one)
Int.one) Int.one) Int.one) with (Int.repr 5).
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
unfold exec_storeex.
unfold LoadStoreSem1.exec_storeex1.
unfold AddrMake.
simpl.
rewrite symofs.
rewrite HIK1, HIH1.
unfold Asm.exec_store.
Lregset_simpl_tac.
rewrite symofs.
change (Int.add (Int.add Int.zero Int.zero) Int.zero) with (Int.zero).
unfold Mem.storev.
change (Int.unsigned Int.zero) with 0.
lift_trivial.
unfold lift.
simpl.
rewrite HST´.
reflexivity.
one_step_forward´.
unfold symbol_offset. unfold fundef.
rewrite Hrestore_context_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_prim_call _ b_restore_context); eauto 1; trivial.
econstructor.
refine_split´; eauto.
econstructor; eauto 1. simpl.
econstructor.
unfold restore_context_spec.
Lregset_simpl_tac.
simpl.
case_eq (tf labd ++
{|
DeviceStateDataType.tf_regs := Lregset_fold
{|
LPC := Vptr b_save_context Int.zero;
LRA := Vptr b (Int.repr 4);
LEAX := rs EAX;
LEBX := rs EBX;
LECX := rs ECX;
LEDX := rs EDX;
LESI := rs ESI;
LEDI := rs EDI;
LEBP := rs EBP;
LESP := Vptr b0 Int.zero;
LST0 := rs ST0;
LZF := Vundef;
LCF := Vundef;
LPF := Vundef;
LSF := Vundef;
LOF := Vundef;
LXMM0 := rs XMM0;
LXMM1 := rs XMM1;
LXMM2 := rs XMM2;
LXMM3 := rs XMM3;
LXMM4 := rs XMM4;
LXMM5 := rs XMM5;
LXMM6 := rs XMM6;
LXMM7 := rs XMM7 |};
DeviceStateDataType.tf_trapno := curr_intr_num labd;
DeviceStateDataType.tf_err := 0;
DeviceStateDataType.tf_esp := Vptr b0 Int.zero |} :: nil); intros.
apply app_eq_nil in H4.
destruct H4.
inv H5.
rewrite <- H4.
repeat rewrite removelast_app.
repeat rewrite last_concat.
simpl.
reflexivity.
intro contra; inv contra.
intro contra; inv contra.
simpl.
generalize inv_reg_wt; intro tmp_wt.
unfold AsmX.wt_regset in ×.
intros.
specialize (inv_reg_wt r).
destruct r; simpl in *; eauto.
destruct i; simpl in *; eauto.
Lregset_simpl_tac.
destruct f; simpl in *; eauto.
destruct c; simpl in *; eauto.
Lregset_simpl_tac.
auto.
inv inv_inject_neutral.
intros.
rewrite Hnextblockmtmp´.
erewrite Mem.nextblock_alloc; eauto.
rewrite <- Hnextblocktmp.
Lregset_simpl_tac.
generalize (Mem.alloc_result _ _ _ _ _ HALC); intro nb0.
generalize (inv_reg_inject_neutral r); intro.
destruct r; simpl in ×.
econstructor.
unfold Mem.flat_inj.
destruct (plt b_save_context (Pos.succ (Mem.nextblock m0))).
reflexivity.
{
generalize n, Hbsave_contextltge, Hblock, Hnextblocktmp, Htmpm1. clearAll. intros.
assert (Pge b_save_context (Pos.succ (Mem.nextblock m0))) by xomega.
destruct Hblock. rewrite Hnextblocktmp in ×. rewrite <- Htmpm1 in ×.
xomega.
}
reflexivity.
destruct i; simpl in *; eauto;
try (eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega).
econstructor.
unfold Mem.flat_inj.
rewrite nb0.
rewrite <- Hnextblocktmp.
destruct (plt (Mem.nextblock m0) (Pos.succ (Mem.nextblock m0))).
reflexivity.
xomega.
reflexivity.
destruct f; simpl in *; eauto;
try (eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega).
eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega.
destruct c; simpl in *; eauto;
try (eapply inv_reg_le; eauto;
clearAll; lift_unfold; xomega).
econstructor.
unfold Mem.flat_inj.
destruct (plt b (Pos.succ (Mem.nextblock m0))).
reflexivity.
{
generalize n, Hbltge, Hblock, Hnextblocktmp, Htmpm1. clearAll. intros.
assert (Pge b (Pos.succ (Mem.nextblock m0))) by xomega.
destruct Hblock. rewrite Hnextblocktmp in ×. rewrite <- Htmpm1 in ×.
xomega.
}
reflexivity.
simpl.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
unfold set; simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
erewrite register_type_load_result.
rewrite HFree. reflexivity.
apply inv_reg_wt.
right. left. simpl. omega.
Lregset_simpl_tac.
rewrite register_type_load_result by (apply inv_reg_wt; eauto).
one_step_forward´.
simpl.
Lregset_simpl_tac.
rewrite app_nil_r.
assert (tf_eq: ∀ d tf1 tf2, d {tf: tf1} {tf: tf2} = d {tf: tf2}) by (intros; reflexivity).
rewrite tf_eq.
functional inversion HEX2; subst.
assert (tf labd´ = tf labd ++
{|
DeviceStateDataType.tf_regs := rs;
DeviceStateDataType.tf_trapno := curr_intr_num labd;
DeviceStateDataType.tf_err := 0;
DeviceStateDataType.tf_esp := rs ESP |} :: nil).
{
generalize HEX3. clearAll. intros.
remember (save_context_spec rs labd) as d1.
functional inversion Heqd1.
functional inversion HEX3.
functional inversion H6;
functional inversion H5; simpl; rewrite <- H; simpl; reflexivity.
}
rewrite H5 in H4.
symmetry in H4.
apply app_eq_nil in H4.
destruct H4.
inv H6.
assert (tf labd1 = tf labd ++
{|
DeviceStateDataType.tf_regs := rs;
DeviceStateDataType.tf_trapno := curr_intr_num labd;
DeviceStateDataType.tf_err := 0;
DeviceStateDataType.tf_esp := rs ESP |} :: nil).
{
generalize HEX3. clearAll. intros.
remember (save_context_spec rs labd) as d1.
functional inversion Heqd1.
functional inversion HEX3.
functional inversion H6;
functional inversion H5; simpl; rewrite <- H; simpl; reflexivity.
}
rewrite H4.
rewrite removelast_app.
simpl.
rewrite app_nil_r.
simpl.
unfold AsmX.wt_regset in inv_reg_wt.
instantiate (2:= (Lregset_fold
{|
LPC := rs RA;
LRA := Vundef;
LEAX := rs EAX;
LEBX := rs EBX;
LECX := rs ECX;
LEDX := rs EDX;
LESI := rs ESI;
LEDI := rs EDI;
LEBP := rs EBP;
LESP := rs ESP;
LST0 := rs ST0;
LZF := rs ZF;
LCF := rs CF;
LPF := rs PF;
LSF := rs SF;
LOF := rs OF;
LXMM0 := rs XMM0;
LXMM1 := rs XMM1;
LXMM2 := rs XMM2;
LXMM3 := rs XMM3;
LXMM4 := rs XMM4;
LXMM5 := rs XMM5;
LXMM6 := rs XMM6;
LXMM7 := rs XMM7 |})).
Lregset_simpl_tac.
eapply star_refl.
intro contra; inv contra.
reflexivity.
reflexivity.
assert (HFB: ∀ b1 delta, Mem.flat_inj (Mem.nextblock m0) b1 ≠ Some (b0, delta)).
{
intros. unfold Mem.flat_inj.
red; intros.
destruct (plt b1 (Mem.nextblock m0)). inv H4.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
rewrite Hnextblocktmp in p.
xomega.
inv H4.
}
rewrite Hnextblocktmp´´ in HFB.
eapply Mem.free_right_inject; eauto; [|intros; specialize (HFB b1 delta); apply HFB; trivial].
rewrite <- Hnextblocktmp´´.
rewrite Hnextblocktmp.
assert (b´plt: Plt b´ (Mem.nextblock m0)).
{
inv inv_inject_neutral.
eapply genv_symb_range in settfb.
generalize Hnextblocktmp, inv_mem_valid, settfb; clearAll.
lift_simpl.
unfold lift; simpl.
intros.
xomega.
}
assert (Mem.inject (Mem.flat_inj (Mem.nextblock mtmp)) mtmp m3).
{
rewrite <- Hnextblocktmp´´ in HFB.
rewrite Hnextblocktmp in HFB.
repeat (eapply Mem.store_outside_inject; [ | | eassumption]
; [|intros b1 delta; intros; specialize (HFB b1 delta); apply HFB; trivial]).
eapply Mem.alloc_right_inject; eauto.
inv inv_inject_neutral.
apply Mem.neutral_inject; trivial.
rewrite <- Hnextblocktmp.
eapply Mem.store_inject_neutral; eauto.
}
exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b´ 0 (Vint Int.zero) H4 settfrw1); eauto.
unfold Mem.flat_inj.
rewrite <- Hnextblocktmp.
destruct (plt b´ (Mem.nextblock m0)).
reflexivity.
xomega.
intros[n2 [store inject]].
simpl in store.
rewrite HST´ in store; inv store.
apply inject.
generalize (Mem.nextblock_free _ _ _ _ _ HFree); intro.
rewrite H4, <- Hnextblocktmp´´, Hnextblocktmp.
generalize (Mem.nextblock_alloc _ _ _ _ _ HALC); intro.
rewrite Hnextblockmtmp´.
rewrite H5.
xomega.
unfold Lregset_fold; simpl.
intros reg.
functional inversion HEX1; subst; simpl in ×.
generalize (serial_intr_handler_sw_spec_does_not_change_tf _ _ HEX3); intro.
functional inversion HEX2; subst; simpl in ×.
rewrite H6 in H4.
symmetry in H4.
apply app_eq_nil in H4.
destruct H4.
inv H5.
rewrite H4.
rewrite last_concat.
simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF; inv HF.
intro contra; inv contra.
Qed.
Lemma serial_intr_handler_asm_code_correct:
asm_spec_le (serial_intr_handler_asm ↦ serial_intr_handler_asm_spec_low)
(〚 serial_intr_handler_asm ↦ serial_intr_handler_asm_function 〛 dhandlersw).
Proof.
eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b =
Some (Internal serial_intr_handler_asm_function)).
{
assert (Hmodule:
get_module_function serial_intr_handler_asm (serial_intr_handler_asm ↦ serial_intr_handler_asm_function)
= OK (Some serial_intr_handler_asm_function)) by reflexivity.
assert (HInternal:
make_internal serial_intr_handler_asm_function
= OK (AST.Internal serial_intr_handler_asm_function)) by reflexivity.
eapply make_globalenv_get_module_function in H0; eauto.
destruct H0 as [?[Hsymbol´ ?]].
inv Hstencil_matches.
rewrite stencil_matches_symbols in Hsymbol´.
rewrite H6 in Hsymbol´. inv Hsymbol´.
assumption.
}
assert(Hnextblocktmp: Mem.nextblock m0 = Mem.nextblock mtmp).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ H3); trivial.
}
assert(Hnextblockm1: Mem.nextblock mtmp = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ H5); trivial.
}
exploit serial_intr_handler_asm_code_correct_aux; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).
split.
lift_simpl.
unfold lift; simpl.
rewrite Hnextblocktmp, Hnextblockm1.
xomega.
∃ f´, (m0´, labd´). esplit.
repeat split; try eassumption.
simpl; unfold lift; simpl.
exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
intros.
simpl.
generalize (Hlessdef l); intro.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
destruct l; simpl in *; try apply H.
assert (PC = PC) by reflexivity; contradiction.
assert (RA = RA) by reflexivity; contradiction.
Qed.
End WITHMEM.
End ASM_VERIFICATION.