Library mcertikos.multithread.flatmem.LoadStoreSemPHB
This file defines the load and store semantics for primitives at all layers
Require Import Coqlib.
Require Import Maps.
Require Import Globalenvs.
Require Import ASTExtra.
Require Import AsmX.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import LAsm.
Require Import AuxStateDataType.
Require Import Constant.
Require Import FlatMemory.
Require Import GlobIdent.
Require Import Integers.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import AsmImplLemma.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.ClightModules.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatClightSem.
Require Import liblayers.compcertx.MemWithData.
Require Import GlobalOracleProp.
Require Import AuxSingleAbstractDataType.
Require Import SingleAbstractDataType.
Require Import HostAccessPHB.
Require Import GuestAccessIntelPHB.
Require Export LoadStoreDefPHB.
Require Import SingleOracle.
Section Load_Store.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{threads_conf_ops: ThreadsConfigurationOps}.
Context `{HD: CompatData PData}.
Notation HDATAOps := (cdata (cdata_ops := data_ops) PData).
Context `{single_trap_inv: Single_TrapinfoSetInvariant (oracle_ops := oracle_ops) (big_ops := big_ops) (data_ops := data_ops)}.
Context `{single_flatmem_store: PData → memory_chunk → Z → val → option (cdata PData)}.
Section GE.
Context {F V} (ge: Genv.t F V).
Definition single_exec_loadex (chunk: memory_chunk) (m: mwd HDATAOps)
(a: addrmode) (rs: regset) (rd: preg) :=
let adt:= (snd m) in
match (eval_addrmode ge a rs) with
| Vptr b ofs ⇒
match (ikern (snd adt), ihost (snd adt)) with
| (true, true) ⇒ Asm.exec_load ge chunk m a rs rd
| _ ⇒ Stuck
end
| Vint adr ⇒
match (init (fst adt), ihost (snd adt), pg (fst adt), ikern (snd adt)) with
| (true, true, true, false) ⇒ single_exec_host_load ge adr chunk m rs rd
| (true, false, _, _) ⇒ single_exec_guest_intel_load adr chunk m rs rd
| _ ⇒ Stuck
end
| _ ⇒ Stuck
end.
Definition single_exec_storeex (chunk: memory_chunk) (m: mwd HDATAOps)
(a: addrmode) (rs: regset) (rd: preg) (destroyed: list preg) :=
let adt:= (snd m) in
match (eval_addrmode ge a rs) with
| Vptr b ofs ⇒
match (ikern (snd adt), ihost (snd adt)) with
| (true, true) ⇒ Asm.exec_store ge chunk m a rs rd destroyed
| _ ⇒ Stuck
end
| Vint adr ⇒
match (init (fst adt), ihost (snd adt), pg (fst adt), ikern (snd adt)) with
| (true, true, true, false)
⇒ single_exec_host_store (single_flatmem_store:= single_flatmem_store) ge adr chunk m rs rd destroyed
| (true, false, _, _)
⇒ single_exec_guest_intel_store (single_flatmem_store:= single_flatmem_store) adr chunk m rs rd destroyed
| _ ⇒ Stuck
end
| _ ⇒ Stuck
end.
Local Existing Instance Asm.mem_accessors_default.
Local Existing Instance AsmX.mem_accessors_default_invariant.
Lemma single_exec_loadex_high_level_invariant:
∀ adr chunk m rs rd rs´ m´,
single_exec_loadex chunk m adr rs rd = Next rs´ m´ →
high_level_invariant (snd m) →
high_level_invariant (snd m´).
Proof.
unfold single_exec_loadex.
intros until m´.
destruct (eval_addrmode ge adr rs); try discriminate.
- destruct (init (fst (snd m))); try discriminate.
destruct (ihost (snd (snd m))); try discriminate.
destruct (pg (fst (snd m))); destruct (ikern (snd (snd m))); try discriminate.
+ eapply single_exec_host_load_high_level_invariant; eauto.
+ eapply single_exec_guest_intel_load_high_level_invariant; eauto.
- destruct (ikern (snd (snd m))); try discriminate.
destruct (ihost (snd (snd m))); try discriminate.
unfold Asm.exec_load. destruct (Mem.loadv chunk m (eval_addrmode ge adr rs)); try discriminate.
congruence.
Qed.
Lemma single_exec_loadex_asm_invariant:
∀ chunk rd,
∀ TYP: subtype (type_of_chunk chunk) (typ_of_preg rd) = true,
∀ adr m rs rs´ m´,
single_exec_loadex chunk m adr rs rd = Next rs´ m´ →
AsmX.asm_invariant ge rs m →
AsmX.asm_invariant ge rs´ m´.
Proof.
unfold single_exec_loadex. intros until m´.
destruct (eval_addrmode ge adr rs); try discriminate.
- destruct (init (fst (snd m))); try discriminate.
destruct (ihost (snd (snd m))); try discriminate.
destruct (pg (fst (snd m))); destruct (ikern (snd (snd m))); try discriminate.
+ eapply single_exec_host_load_asm_invariant; eauto.
+ intros; eapply single_exec_guest_intel_load_asm_invariant; eauto.
- destruct (ikern (snd (snd m))); try discriminate.
destruct (ihost (snd (snd m))); try discriminate.
intros; eapply exec_load_invariant; eauto.
Qed.
Lemma single_exec_loadex_low_level_invariant:
∀ adr chunk m rs rd rs´ m´,
single_exec_loadex chunk m adr rs rd = Next rs´ m´ →
AsmX.asm_invariant ge rs m →
CompatData.low_level_invariant (Mem.nextblock m) (snd m) →
CompatData.low_level_invariant (Mem.nextblock m´) (snd m´).
Proof.
unfold single_exec_loadex.
intros until m´.
destruct (eval_addrmode ge adr rs); try discriminate.
- destruct (init (fst (snd m))); try discriminate.
destruct (ihost (snd (snd m))); try discriminate.
destruct (pg (fst (snd m))); destruct (ikern (snd (snd m))); try discriminate.
+ eapply single_exec_host_load_low_level_invariant; eauto.
+ intros; eapply single_exec_guest_intel_load_low_level_invariant; eauto.
- destruct (ikern (snd (snd m))); try discriminate.
destruct (ihost (snd (snd m))); try discriminate.
unfold Asm.exec_load.
destruct (Mem.loadv chunk m (eval_addrmode ge adr rs)); try discriminate.
congruence.
Qed.
Context {single_flat_inv: Single_FlatmemStoreInvariant (data_ops := data_ops)
(single_flatmem_store:= single_flatmem_store)}.
Lemma single_exec_storeex_high_level_invariant:
∀ adr chunk m rs rd des rs´ m´,
single_exec_storeex chunk m adr rs rd des = Next rs´ m´ →
high_level_invariant (snd m) →
high_level_invariant (snd m´).
Proof.
unfold single_exec_storeex.
intros until m´.
destruct (eval_addrmode ge adr rs); try discriminate.
- destruct (init (fst (snd m))); try discriminate.
destruct (ihost (snd (snd m))); try discriminate.
destruct (pg (fst (snd m))); destruct (ikern (snd (snd m))); try discriminate.
+ eapply single_exec_host_store_high_level_invariant; eauto.
+ eapply single_exec_guest_intel_store_high_level_invariant; eauto.
- destruct (ikern (snd (snd m))); try discriminate.
destruct (ihost (snd (snd m))); try discriminate.
unfold Asm.exec_store.
destruct (Mem.storev chunk m (eval_addrmode ge adr rs) (rs rd)) eqn:Heqo; try discriminate.
destruct (eval_addrmode ge adr rs); try discriminate.
lift_unfold.
destruct Heqo as [? DATA].
unfold π_data in DATA.
simpl in × |- ×.
congruence.
Qed.
Lemma single_exec_storeex_asm_invariant:
∀ chunk rd,
∀ adr m des rs rs´ m´,
single_exec_storeex chunk m adr rs rd des = Next rs´ m´ →
AsmX.asm_invariant ge rs m →
AsmX.asm_invariant ge rs´ m´.
Proof.
unfold single_exec_storeex.
intros until m´.
destruct (eval_addrmode ge adr rs); try discriminate.
- destruct (init (fst (snd m))); try discriminate.
destruct (ihost (snd (snd m))); try discriminate.
destruct (pg (fst (snd m))); destruct (ikern (snd (snd m))); try discriminate.
+ eapply single_exec_host_store_asm_invariant; eauto.
+ intros; eapply single_exec_guest_intel_store_asm_invariant; eauto.
- destruct (ikern (snd (snd m))); try discriminate.
destruct (ihost (snd (snd m))); try discriminate.
intros; eapply exec_store_invariant; eauto.
Qed.
Lemma single_exec_storeex_low_level_invariant:
∀ adr chunk m rs rd des rs´ m´,
single_exec_storeex chunk m adr rs rd des = Next rs´ m´ →
AsmX.asm_invariant ge rs m →
CompatData.low_level_invariant (Mem.nextblock m) (snd m) →
CompatData.low_level_invariant (Mem.nextblock m´) (snd m´).
Proof.
unfold single_exec_storeex.
intros until m´.
destruct (eval_addrmode ge adr rs); try discriminate.
- destruct (init (fst (snd m))); try discriminate.
destruct (ihost (snd (snd m))); try discriminate.
destruct (pg (fst (snd m))); destruct (ikern (snd (snd m))); try discriminate.
+ eapply single_exec_host_store_low_level_invariant; eauto.
+ intros; eapply single_exec_guest_intel_store_low_level_invariant; eauto.
- destruct (ikern (snd (snd m))); try discriminate.
destruct (ihost (snd (snd m))); try discriminate.
unfold Asm.exec_store.
destruct (Mem.storev chunk m (eval_addrmode ge adr rs) (rs rd)) eqn:Heqo; try discriminate.
destruct (eval_addrmode ge adr rs); try discriminate.
lift_unfold.
destruct Heqo as [? DATA].
unfold π_data in DATA.
simpl in × |- ×.
injection 1; intros; subst.
erewrite Mem.nextblock_store; eauto.
congruence.
Qed.
End GE.
Context `{Single_KernelModeImplies (oracle_ops:= oracle_ops) (big_ops:= big_ops) (data_ops:= data_ops)}.
Context {single_flat_inv: Single_FlatmemStoreInvariant (data_ops := data_ops)
(single_flatmem_store:= single_flatmem_store)}.
Global Instance single_load_accessor_prf:
LoadAccessor _ (@single_exec_loadex).
Proof.
constructor.
{
unfold single_exec_loadex; intros.
erewrite AsmX.eval_addrmode_symbols_preserved; eauto.
destruct (eval_addrmode ge1 a rs); try reflexivity.
- destruct (init (fst (snd m))); try reflexivity.
destruct (ihost (snd (snd m))); try reflexivity.
destruct (pg (fst (snd m))); destruct (ikern (snd (snd m))); try reflexivity.
+ unfold single_exec_host_load.
unfold single_exec_pagefault; rewrite SYMB; reflexivity.
- unfold Asm.exec_load.
erewrite AsmX.eval_addrmode_symbols_preserved; eauto.
}
{
intros.
apply single_kernel_mode_implies in H1.
destruct H1 as [IKERN IHOST].
unfold single_exec_loadex.
unfold Asm.exec_load in H0 |- ×.
destruct (eval_addrmode ge a rs); try discriminate.
unfold π_data in IKERN, IHOST.
rewrite IKERN.
rewrite IHOST.
assumption.
}
{
intros; eapply single_exec_loadex_asm_invariant; eauto.
}
{
intros; eapply single_exec_loadex_low_level_invariant; eauto.
}
{
intros; eapply single_exec_loadex_high_level_invariant; eauto.
}
Qed.
Global Instance single_store_accessor_prf:
StoreAccessor _ (@single_exec_storeex).
Proof.
constructor.
{
unfold single_exec_storeex; intros.
erewrite AsmX.eval_addrmode_symbols_preserved; eauto.
destruct (eval_addrmode ge1 a rs); try reflexivity.
- destruct (init (fst (snd m))); try reflexivity.
destruct (ihost (snd (snd m))); try reflexivity.
destruct (pg (fst (snd m))); destruct (ikern (snd (snd m))); try reflexivity.
+ unfold single_exec_host_store.
unfold single_exec_pagefault. rewrite SYMB. reflexivity.
- unfold Asm.exec_store.
erewrite AsmX.eval_addrmode_symbols_preserved; eauto.
}
{
intros.
apply single_kernel_mode_implies in H1.
destruct H1 as [IKERN IHOST].
unfold single_exec_storeex.
unfold Asm.exec_store in H0 |- ×.
destruct (eval_addrmode ge a rs); try discriminate.
unfold π_data in IKERN, IHOST.
rewrite IKERN. rewrite IHOST.
assumption.
}
{
intros; eapply single_exec_storeex_asm_invariant; eauto.
}
{
intros; eapply single_exec_storeex_low_level_invariant; eauto.
}
{
intros; eapply single_exec_storeex_high_level_invariant; eauto.
}
Qed.
End Load_Store.