Library mcertikos.multithread.flatmem.GuestAccessIntelPHB
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 Export FlatLoadStoreSemPHB.
Require Import LoadStoreDefPHB.
Require Export GuestAccessIntelDefPHB.
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).
Section GE.
Context {F V} (ge: Genv.t F V).
Section Load_StorePHB.
Open Scope Z_scope.
Definition single_load_accessor (n: Z) (ofs: Z) (chunk: memory_chunk) (m: mwd HDATAOps) (rs: regset) (rd: preg) :=
let adr´ := (EPTADDR (n / PgSize) ofs) in
if (zle (ofs mod PgSize) (PgSize - size_chunk chunk)) then
if (Zdivide_dec (align_chunk chunk) (ofs mod PgSize) (align_chunk_pos chunk)) then
match ZMap.get (PageI (EPTADDR (n / PgSize) ofs)) (pperm (snd (snd m))) with
| PGAlloc ⇒ single_exec_flatmem_load chunk m adr´ rs rd
| _ ⇒ Stuck
end
else Stuck
else Stuck.
Definition single_exec_guest_intel_load (adr: int) (chunk: memory_chunk) (m: mwd HDATAOps) (rs: regset) (rd: preg) :=
single_exec_guest_intel_accessor single_load_accessor adr chunk m rs rd.
Lemma single_exec_guest_intel_load_high_level_invariant:
∀ adr chunk m rs rd rs´ m´,
single_exec_guest_intel_load adr chunk m rs rd = Next rs´ m´ →
high_level_invariant (snd m) →
high_level_invariant (snd m´).
Proof.
unfold single_exec_guest_intel_load. intros.
eapply single_exec_guest_intel_accessor_high_level_invariant; eauto.
unfold single_load_accessor. intros.
subdestruct.
eapply single_exec_flatmem_load_mem in H1; eauto. inv H1. assumption.
Qed.
Lemma single_exec_guest_intel_load_asm_invariant:
∀ chunk rd,
∀ TYP: subtype (type_of_chunk chunk) (typ_of_preg rd) = true,
∀ adr m rs rs´ m´,
single_exec_guest_intel_load adr chunk m rs rd = Next rs´ m´ →
AsmX.asm_invariant ge rs m →
AsmX.asm_invariant ge rs´ m´.
Proof.
unfold single_exec_guest_intel_load. intros.
eapply single_exec_guest_intel_accessor_asm_invariant; eauto.
unfold single_load_accessor. intros. subdestruct.
eapply single_exec_flatmem_load_asm_invariant; eauto.
Qed.
Lemma single_exec_guest_intel_load_low_level_invariant:
∀ adr chunk m rs rd rs´ m´,
single_exec_guest_intel_load adr chunk m rs rd = Next rs´ m´ →
CompatData.low_level_invariant (Mem.nextblock m) (snd m) →
CompatData.low_level_invariant (Mem.nextblock m´) (snd m´).
Proof.
unfold single_exec_guest_intel_load. intros.
eapply single_exec_guest_intel_accessor_low_level_invariant; eauto.
unfold single_load_accessor. intros.
subdestruct.
eapply single_exec_flatmem_load_mem in H1; eauto. inv H1. assumption.
Qed.
Context `{single_flatmem_store: PData → memory_chunk → Z → val → option (cdata PData)}.
Definition single_store_accessor (destroyed: list preg) (n: Z) (ofs: Z)
(chunk: memory_chunk) (m: mwd HDATAOps) (rs: regset) (rd: preg) :=
let adr´ := (EPTADDR (n / PgSize) ofs) in
if (zle (ofs mod PgSize) (PgSize - size_chunk chunk)) then
if (Zdivide_dec (align_chunk chunk) (ofs mod PgSize) (align_chunk_pos chunk)) then
single_exec_flatmem_store (single_flatmem_store:= single_flatmem_store) chunk m adr´ rs rd destroyed
else Stuck
else Stuck.
Definition single_exec_guest_intel_store (adr: int) (chunk: memory_chunk) (m: mwd HDATAOps)
(rs: regset) (rd: preg) (destroyed: list preg) :=
single_exec_guest_intel_accessor (single_store_accessor destroyed) adr chunk m rs rd.
Context {single_flat_inv: Single_FlatmemStoreInvariant
(data_ops := data_ops)
(single_flatmem_store:= single_flatmem_store)}.
Lemma PTADDR_mod_lt:
∀ adr n,
(adr mod PgSize ≤ PgSize - n)%Z →
∀ i,
(PTADDR i adr mod PgSize ≤ PgSize - n)%Z.
Proof.
unfold PTADDR. intros. rewrite Zplus_comm.
rewrite Z_mod_plus_full. rewrite Zmod_mod.
assumption.
Qed.
Lemma single_exec_guest_intel_store_high_level_invariant:
∀ adr chunk m rs rd rs´ ds m´,
single_exec_guest_intel_store adr chunk m rs rd ds = Next rs´ m´ →
high_level_invariant (snd m) →
high_level_invariant (snd m´).
Proof.
unfold single_exec_guest_intel_store. intros.
eapply single_exec_guest_intel_accessor_high_level_invariant; eauto.
unfold single_store_accessor. intros. subdestruct.
eapply single_exec_flatmem_store_high_level_invariant; eauto 1.
eapply PTADDR_mod_lt; assumption.
Qed.
Lemma single_exec_guest_intel_store_asm_invariant:
∀ chunk rd,
∀ adr m rs rs´ ds m´,
single_exec_guest_intel_store adr chunk m rs rd ds = Next rs´ m´ →
AsmX.asm_invariant ge rs m →
AsmX.asm_invariant ge rs´ m´.
Proof.
unfold single_exec_guest_intel_store. intros.
eapply single_exec_guest_intel_accessor_asm_invariant; eauto.
unfold single_store_accessor. intros. subdestruct.
eapply single_exec_flatmem_store_asm_invariant; eauto.
Qed.
Lemma single_exec_guest_intel_store_low_level_invariant:
∀ adr chunk m rs rd rs´ ds m´,
single_exec_guest_intel_store adr chunk m rs rd ds = Next rs´ m´ →
CompatData.low_level_invariant (Mem.nextblock m) (snd m) →
CompatData.low_level_invariant (Mem.nextblock m´) (snd m´).
Proof.
unfold single_exec_guest_intel_store. intros.
eapply single_exec_guest_intel_accessor_low_level_invariant; eauto.
unfold single_store_accessor. intros. subdestruct.
eapply single_exec_flatmem_store_low_level_invariant in H1; eauto.
Qed.
End Load_StorePHB.
End GE.
End Load_Store.