Library mcertikos.conlib.conmtlib.EAsm
This file provide the semantics for the Asm instructions. Since we introduce paging mechanisms, the semantics of memory load and store are different from Compcert Asm
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import AuxLemma.
Require Import CommonTactic.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import Decision.
Require Import LAsm.
Require Import GlobIdent.
Require Export EAsmCommon.
Require Import SingleConfiguration.
Section ESemantics.
Context `{conf : SingleConfiguration}.
Context `{Hmwd: UseMemWithData mem}.
Context `{data_prf : CompatData PData}.
Context `{Hstencil: Stencil}.
Context `{L: compatlayer (cdata PData)}.
Context `{ass_def: !AccessorsDefined L}.
Local Instance ec_ops: ExternalCallsOps (mwd (cdata PData)) := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance lcfg_ops: LayerConfigurationOps := compatlayer_configuration_ops L.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import AuxLemma.
Require Import CommonTactic.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import Decision.
Require Import LAsm.
Require Import GlobIdent.
Require Export EAsmCommon.
Require Import SingleConfiguration.
Section ESemantics.
Context `{conf : SingleConfiguration}.
Context `{Hmwd: UseMemWithData mem}.
Context `{data_prf : CompatData PData}.
Context `{Hstencil: Stencil}.
Context `{L: compatlayer (cdata PData)}.
Context `{ass_def: !AccessorsDefined L}.
Local Instance ec_ops: ExternalCallsOps (mwd (cdata PData)) := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance lcfg_ops: LayerConfigurationOps := compatlayer_configuration_ops L.
EAsm threads can be in one of three states: environment,
available, or running. Environment threads can only take oracle
steps and will never change states. Available threads have not
been run yet, but may be "yielded back" to, at which time they
become running threads. Running threads have a current register
state and take normal steps.
Inductive estate: Type :=
| EState: Z → ZMap.t ThreadState → mem → EData → Log → estate.
Inductive estep (ge: genv) : estate → trace → estate → Prop :=
| eexec_step_internal:
∀ b ofs f i (rs: regset) m m´ dp d d´ ds´ rs´ curid rsm l,
ZMap.get curid rsm = Running rs →
proc_id (uRData l) = curid →
rs PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
find_instr (Int.unsigned ofs) f.(fn_code) = Some i →
lastEvType l ≠ Some LogYieldTy →
exec_instr ge f i rs (m, (uRData l,d)) = Next rs´ (m´, (ds´,d´)) →
∀ (Hget_dp: ZMap.get curid dp = Some d),
estep ge (EState curid rsm m dp l) E0
(EState curid (ZMap.set curid (Running rs´) rsm) m´ (ZMap.set curid (Some d´) dp) l)
| eexec_step_builtin:
∀ b ofs f ef args res (rs: regset) m m´ dp d d´ ds´ t vl rs´ curid rsm l,
ZMap.get curid rsm = Running rs →
proc_id (uRData l) = curid →
rs PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
find_instr (Int.unsigned ofs) f.(fn_code) = Some (asm_instruction (Pbuiltin ef args res)) →
lastEvType l ≠ Some LogYieldTy →
external_call´ (mem:= mwd (cdata PData)) (fun _ ⇒ True) ef ge (map rs args) (m, (uRData l,d)) t vl (m´, (ds´, d´)) →
rs´ = nextinstr_nf
(set_regs res vl
(undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) →
∀ BUILTIN_ENABLED: match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end,
∀ BUILTIN_WT:
subtype_list (proj_sig_res´ (ef_sig ef)) (map typ_of_preg res) = true,
∀ (Hget_dp: ZMap.get curid dp = Some d),
estep ge (EState curid rsm m dp l) t
(EState curid (ZMap.set curid (Running rs´) rsm) m´ (ZMap.set curid (Some d´) dp) l)
| eexec_step_annot:
∀ b ofs f ef args (rs: regset) m m´ dp d d´ ds´ vargs t v curid rsm l,
ZMap.get curid rsm = Running rs →
proc_id (uRData l) = curid →
rs PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
find_instr (Int.unsigned ofs) f.(fn_code) = Some (asm_instruction (Pannot ef args)) →
annot_arguments rs m args vargs →
lastEvType l ≠ Some LogYieldTy →
external_call´ (mem:= mwd (cdata PData)) (fun _ ⇒ True) ef ge vargs (m, (uRData l, d)) t v (m´, (ds´, d´)) →
∀ BUILTIN_ENABLED:
match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end,
∀ (Hget_dp: ZMap.get curid dp = Some d),
estep ge (EState curid rsm m dp l) t
(EState curid (ZMap.set curid (Running (nextinstr rs)) rsm) m´ (ZMap.set curid (Some d´) dp) l)
| eexec_step_external:
∀ b ef args res (rs: regset) m m´ dp d d´ ds´ t rs´ curid rsm l l´,
ZMap.get curid rsm = Running rs →
proc_id (uRData l) = curid →
rs PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
extcall_arguments rs m (ef_sig ef) args →
lastEvType l ≠ Some LogYieldTy →
external_call´ (mem:= mwd (cdata PData)) (fun _ ⇒ True) ef ge args (m, (uRData l, d)) t res (m´, (ds´,d´)) →
rs´ = (set_regs (loc_external_result (ef_sig ef)) res
(undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs)))
#PC <- (rs RA) #RA <- Vundef →
∀ NON_YIELD: match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else
if has_event id then
∃ largs choice,
val2Lval_list args largs ∧
choice_check id largs (uRData l) d = choice ∧
l´ = (LEvent curid (LogPrim id largs choice (snap_func d)) :: l)
else
l´ = l
| _ ⇒ l´ = l
end,
∀ STACK:
∀ b o, rs ESP = Vptr b o →
(Ple (Genv.genv_next ge) b ∧ Plt b (Mem.nextblock m)),
∀ SP_NOT_VUNDEF: rs ESP ≠ Vundef,
∀ RA_NOT_VUNDEF: rs RA ≠ Vundef,
∀ (Hget_dp: ZMap.get curid dp = Some d),
estep ge (EState curid rsm m dp l) t
(EState curid (ZMap.set curid (Running rs´) rsm) m´ (ZMap.set curid (Some d´) dp) l´)
| eexec_step_prim_call:
∀ b ef (rs: regset) m m´ dp d d´ ds´ t rs´ curid rsm l l´,
ZMap.get curid rsm = Running rs →
proc_id (uRData l) = curid →
rs PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
lastEvType l ≠ Some LogYieldTy →
primitive_call (mem:= mwd (cdata PData)) ef ge rs (m, (uRData l, d)) t rs´ (m´, (ds´, d´)) →
∀ NON_YIELD: match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else
if has_event id then
l´ = (LEvent curid (LogPrim id nil 0 (snap_func d)) :: l)
else
l´ = l
| _ ⇒ l´ = l
end,
∀ (Hget_dp: ZMap.get curid dp = Some d),
estep ge (EState curid rsm m dp l) t
(EState curid (ZMap.set curid (Running rs´) rsm) m´ (ZMap.set curid (Some d´) dp) l´)
| eexec_step_external_yield:
∀ b ef (rs: regset) (m: mem) curid curid´ rsm s l l´ dp d,
ZMap.get curid rsm = Running rs →
ZMap.get curid dp = Some d →
proc_id (uRData l) = curid →
rs PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
stencil_matches s ge →
l´ = (LEvent curid (LogYield (Mem.nextblock m))::l) →
lastEvType l ≠ Some LogYieldTy →
state_checks thread_yield nil l dp →
curid´ = proc_id (uRData l´) →
∀ (NON_YIELD: match ef with
| EF_external id _ ⇒
if peq id thread_yield then True
else False
| _ ⇒ False
end),
estep ge (EState curid rsm m dp l) E0
(EState curid´ rsm m dp l´)
| eexec_step_external_sleep:
∀ b ef (rs: regset) (m: mem) curid curid´ rsm s l l´ dp d i,
ZMap.get curid rsm = Running rs →
ZMap.get curid dp = Some d →
proc_id (uRData l) = curid →
rs PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
stencil_matches s ge →
l´ = (LEvent curid (LogSleep (Int.unsigned i) (Mem.nextblock m)
(sync_chpool_check thread_sleep ((Lint i)::nil) (uRData l) d))::l) →
lastEvType l ≠ Some LogYieldTy →
state_checks thread_sleep (Lint i::nil) l dp →
curid´ = proc_id (uRData l´) →
∀
(Hargs: extcall_arguments rs m (mksignature (Tint:: nil) None cc_default) (Vint i:: nil))
(NON_YIELD: match ef with
| EF_external id _ ⇒
if peq id thread_sleep then True
else False
| _ ⇒ False
end),
estep ge (EState curid rsm m dp l) E0
(EState curid´ rsm m dp l´)
Environment step
| eexec_step_external_empty:
∀ m curid curid´ rsm dp l l´,
ZMap.get curid rsm = Environment →
ZMap.get curid dp = None →
proc_id (uRData l) = curid →
l´ = (Single_Oracle l::l) →
curid´ = proc_id (uRData l´) →
estep ge (EState curid rsm m dp l) E0
(EState curid´ rsm m dp l´)
| eexec_step_external_yield_back:
∀ (rs´ rs0: regset) (m m´: mem) curid rsm l l´ nb dp d e,
(ZMap.get curid rsm = Available ∧ initial_thread_kctxt ge curid l = Some rs0) ∨
ZMap.get curid rsm = Running rs0 →
ZMap.get curid dp = Some d →
proc_id (uRData l) = curid →
last_op l = Some e →
l´ = (LEvent curid LogYieldBack::l) →
rs´ = (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs0))
# EAX <- Vundef #PC <- (rs0 RA) #RA <- Vundef →
∀
(Hnextblock: getLogEventNB (e) = Some nb)
(LIFT_NEXTBLOCK: mem_lift_nextblock m (Pos.to_nat (nb) - Pos.to_nat (Mem.nextblock m) % nat) = m´),
estep ge (EState curid rsm m dp l) E0
(EState curid (ZMap.set curid (Running rs´) rsm) m´ dp l´).
Context (active_threads : list Z).
∀ m curid curid´ rsm dp l l´,
ZMap.get curid rsm = Environment →
ZMap.get curid dp = None →
proc_id (uRData l) = curid →
l´ = (Single_Oracle l::l) →
curid´ = proc_id (uRData l´) →
estep ge (EState curid rsm m dp l) E0
(EState curid´ rsm m dp l´)
| eexec_step_external_yield_back:
∀ (rs´ rs0: regset) (m m´: mem) curid rsm l l´ nb dp d e,
(ZMap.get curid rsm = Available ∧ initial_thread_kctxt ge curid l = Some rs0) ∨
ZMap.get curid rsm = Running rs0 →
ZMap.get curid dp = Some d →
proc_id (uRData l) = curid →
last_op l = Some e →
l´ = (LEvent curid LogYieldBack::l) →
rs´ = (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs0))
# EAX <- Vundef #PC <- (rs0 RA) #RA <- Vundef →
∀
(Hnextblock: getLogEventNB (e) = Some nb)
(LIFT_NEXTBLOCK: mem_lift_nextblock m (Pos.to_nat (nb) - Pos.to_nat (Mem.nextblock m) % nat) = m´),
estep ge (EState curid rsm m dp l) E0
(EState curid (ZMap.set curid (Running rs´) rsm) m´ dp l´).
Context (active_threads : list Z).
An active main thread is initialized as usual, other active
threads start out in the Available state, and non-active threads
are assigned to be Environment threads.
Inductive einitial_state {F V} (p: AST.program F V): estate → Prop :=
| einitial_state_intro:
∀ m0,
Genv.init_mem p = Some m0 →
let rsm := initial_map Environment (init_regset (Genv.globalenv p)) active_threads in
let dm := initial_map None (fun i ⇒ Some (thread_init_dproc i)) active_threads in
einitial_state p (EState main_thread rsm m0 dm nil).
Definition efinal_state: estate → int → Prop :=
fun _ _ ⇒ False.
Definition esemantics (p: program) :=
Smallstep.Semantics estep (einitial_state p) efinal_state (Genv.globalenv p).
Section Properties.
Context `{extcallsx: !ExternalCallsXDefined L}.
Context `{norepet: CompCertBuiltins.BuiltinIdentsNorepet}.
Instance externalcall_prf:
ExternalCalls (mwd (cdata PData)) (external_calls_ops:= ec_ops).
Proof.
eapply compatlayer_extcall_strong; assumption.
Defined.
Lemma easm_semantics_single_events:
∀ p, single_events (esemantics p).
Proof.
intros p s t s´ Hstep; inv Hstep; auto.
- inv H5; eapply external_call_trace_length; eauto.
- inv H6; eapply external_call_trace_length; eauto.
- inv H5; eapply external_call_trace_length; eauto.
- destruct H4 as [? [? [? [? [? Hsem]]]]]; inv Hsem; auto.
Qed.
Lemma easm_semantics_receptive:
∀ p, receptive (esemantics p).
Proof.
intros; constructor.
- inversion 1; subst; try solve [inversion 1; subst; eauto].
+ intros. inv H6.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. econstructor; eauto. econstructor; eauto.
+ intros. inv H7.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. eapply eexec_step_annot; eauto. econstructor; eauto.
+ intros. inv H6.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. eapply eexec_step_external; eauto. econstructor; eauto.
+ intros. inv H5.
destruct H6 as [?[?[?[? Hsem]]]]; subst.
inv Hsem. inv H1. eauto.
- apply easm_semantics_single_events.
Qed.
Inductive sprimitive_call : stencil → regset → mwd (cdata PData) →
regset → mwd (cdata PData) → Prop :=
| sprim_intro:
∀ s rs m rs´ m´ ef ge t,
stencil_matches s ge →
primitive_call ef ge rs m t rs´ m´ →
sprimitive_call s rs m rs´ m´.
Context `{primcall_props: !PrimcallProperties sprimitive_call}.
Lemma prim_call_determ:
∀ ef ge rs m t1 t2 rs1´ rs2´ m1´ m2´,
primitive_call ef ge rs m t1 rs1´ m1´ →
primitive_call ef ge rs m t2 rs2´ m2´ →
t1 = E0 ∧ t2 = E0 ∧ rs1´ = rs2´ ∧ m1´ = m2´.
Proof.
intros until m2´; intros Hp1 Hp2.
assert (Hp1´:=Hp1).
destruct Hp1´ as [? [? [? [? [? Hp1´]]]]]; destruct Hp1´.
edestruct primitive_call_determ.
{ econstructor; [eauto | eapply Hp1]. }
{ econstructor; [eauto | eapply Hp2]. }
destruct Hp1 as [? [? [? [? [? Hp1]]]]]; inv Hp1.
destruct Hp2 as [? [? [? [? [? Hp2]]]]]; inv Hp2; auto.
Qed.
Lemma val2Lval_determ:
∀ v v1 v2,
val2Lval v v1 → val2Lval v v2 → v1 = v2.
Proof.
destruct v; inversion 1; inversion 1; auto.
Qed.
Lemma val2Lval_list_determ:
∀ l l1 l2,
val2Lval_list l l1 → val2Lval_list l l2 → l1 = l2.
Proof.
induction l; simpl; inversion 1; inversion 1; subst; auto.
assert (v´ = v´0) by (eapply val2Lval_determ; eauto).
assert (l´ = l´0) by (eapply IHl; eauto); subst; auto.
Qed.
Lemma external_call´_primitive_call:
∀ WB ef ge m rs1 rs2 t1 t2 rs1´ rs2´ m1´ m2´,
external_call´ WB ef ge rs1 m t1 rs1´ m1´ →
primitive_call ef ge rs2 m t2 rs2´ m2´ → False.
Proof.
intros until m2´; intros Hx Hp.
destruct Hp as [? [? [? [? [? Hp]]]]]; subst.
destruct Hx as [? Hx].
destruct Hx as [? [? Hx]]; rewrite_inv.
destruct Hx as [? [? [? [? [? ?]]]]]; subst; inv Hp.
Qed.
Import Events.
Lemma easm_semantics_determinate:
∀ p, determinate (esemantics p).
Proof.
intros; constructor.
- intros s t1 s1 t2 s2 Hstep1 Hstep2.
inv Hstep1.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
split; auto; constructor.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
destruct H5 as [? Hx1]; destruct H18 as [? Hx2].
destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2) as [? Heq]; split; auto.
intro Ht; destruct (Heq Ht); congruence.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
destruct H6 as [? Hx1]; destruct H20 as [? Hx2].
assert (vargs = vargs0) by (eapply annot_arguments_determ; eauto); subst.
destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2) as [? Heq]; split; auto.
intro Ht; destruct (Heq Ht); congruence.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
× destruct H5 as [? Hx1]; destruct H18 as [? Hx2].
assert (args = args0) by (eapply extcall_arguments_determ; eauto); subst.
subdestruct; try (destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2) as [? Heq]; split; auto;
assert (l´ = l´0) by (subdestruct; try contradiction; subst; auto); subst;
intro Ht; destruct (Heq Ht); subst; congruence; fail).
destruct NON_YIELD as (largs & choice & H1 & H2 & H5).
destruct NON_YIELD0 as (largs0 & choice0 & H1´ & H2´ & H5´).
assert (largs = largs0) by (eapply val2Lval_list_determ; eauto); subst.
destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2) as [? Heq]; split; auto.
intro Ht; destruct (Heq Ht); congruence.
× assert False by (eapply external_call´_primitive_call; eauto); contradiction.
× subdestruct; contradiction.
× subdestruct; contradiction.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
× assert False by (eapply external_call´_primitive_call; eauto); contradiction.
× destruct (prim_call_determ _ _ _ _ _ _ _ _ _ _ H4 H16) as [? [? [? Heq]]]; inv Heq.
assert (l´ = l´0) by (subdestruct; try contradiction; subst; auto); subst.
split; auto; constructor.
× subdestruct; contradiction.
× subdestruct; contradiction.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
× subdestruct; contradiction.
× subdestruct; contradiction.
× split; auto.
{ constructor. }
× subdestruct; try contradiction.
subst; discriminate.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
× subdestruct; contradiction.
× subdestruct; contradiction.
× subdestruct; try contradiction.
subst; discriminate.
× assert (i = i0).
{
exploit extcall_arguments_determ; [eapply Hargs | eapply Hargs0 |..].
inversion 1; auto.
}
subst; split; auto; constructor.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
× split; auto; constructor.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
× destruct H as [[? ?] | ?]; try congruence.
{ split; [constructor | intros _].
destruct H7 as [[? ?] | ?]; try congruence. }
{ split; [constructor | intros _].
destruct H7 as [[? ?] | ?]; try congruence. }
- apply easm_semantics_single_events.
- simpl; intros s1 s2 Hs1 Hs2.
inv Hs1; inv Hs2.
subst rsm rsm0.
subst dm dm0.
congruence.
- simpl; intros s r Hf t s´ Hstep; inv Hf.
- simpl; intros s r1 r2 Hr1 Hr2; inv Hr1; inv Hr2.
Qed.
End Properties.
End ESemantics.