Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import GenSem.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import RealParams.
Require Import GenSem.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import PrimSemantics.
Require Import CompatClightSem.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import AbsMachine.Spec.
Require Import PageIndex.Layer.
Require Import PageIndex.Spec.
Require Import RData.
Require Import Constants.
Require Import HypsecCommLib.
Local Open Scope Z_scope.
Section PageMgmtSpec.
Definition get_pfn_owner_spec (pfn: Z64) (adt: RData) : option Z :=
match pfn with
| VZ64 pfn =>
rely is_gfn pfn;
if halt adt then Some 0 else
let id := S2PAGE_ID in
match ZMap.get id (lock adt) with
| LockOwn true =>
let page := pfn @ (s2page (shared adt)) in
rely is_int (s2_owner page);
Some (s2_owner page)
| _ => None
end
end.
Definition set_pfn_owner_spec (pfn: Z64) (vmid: Z) (adt: RData) : option RData :=
match pfn with
| VZ64 pfn =>
rely is_gfn pfn;
if halt adt then Some adt else
let id := S2PAGE_ID in
match ZMap.get id (lock adt) with
| LockOwn true =>
let page := pfn @ (s2page (shared adt)) in
if s2_owner page =? INVALID then
Some adt
else
Some adt {shared: (shared adt) {s2page: (s2page (shared adt)) # pfn == (page {s2_owner: vmid})}}
| _ => None
end
end.
Definition get_pfn_count_spec (pfn: Z64) (adt: RData) : option Z :=
match pfn with
| VZ64 pfn =>
rely is_gfn pfn;
if halt adt then Some 0 else
let id := S2PAGE_ID in
match ZMap.get id (lock adt) with
| LockOwn true =>
let page := pfn @ (s2page (shared adt)) in
rely is_int (s2_count page);
Some (s2_count page)
| _ => None
end
end.
Definition set_pfn_count_spec (pfn: Z64) (count: Z) (adt: RData) : option RData :=
match pfn with
| VZ64 pfn =>
rely is_gfn pfn;
if halt adt then Some adt else
let id := S2PAGE_ID in
match ZMap.get id (lock adt) with
| LockOwn true =>
let page := pfn @ (s2page (shared adt)) in
if s2_owner page =? INVALID then
Some adt
else
Some adt {shared: (shared adt) {s2page: (s2page (shared adt)) # pfn == (page {s2_count: count})}}
| _ => None
end
end.
Definition get_pfn_map_spec (pfn: Z64) (adt: RData) : option Z64 :=
match pfn with
| VZ64 pfn =>
rely is_gfn pfn;
if halt adt then Some (VZ64 0) else
let id := S2PAGE_ID in
match ZMap.get id (lock adt) with
| LockOwn true =>
let page := pfn @ (s2page (shared adt)) in
rely is_int (s2_count page);
Some (VZ64 (s2_gfn page))
| _ => None
end
end.
Definition set_pfn_map_spec (pfn: Z64) (gfn: Z64) (adt: RData) : option RData :=
match pfn, gfn with
| VZ64 pfn, VZ64 gfn =>
rely is_gfn pfn;
if halt adt then Some adt else
let id := S2PAGE_ID in
match ZMap.get id (lock adt) with
| LockOwn true =>
let page := pfn @ (s2page (shared adt)) in
if s2_owner page =? INVALID then
Some adt
else
Some adt {shared: (shared adt) {s2page: (s2page (shared adt)) # pfn == (page {s2_gfn: gfn})}}
| _ => None
end
end.
Definition mem_load_check_spec (gfn: Z64) (reg: Z) (bypass: Z) (adt: RData) : option RData :=
match gfn, icore adt with
| VZ64 gfn, false =>
let vmid := cur_vmid adt in
match gfn @ (pt (vmid @ (npts (shared adt)))) with
| (pfn, level, pte) =>
if pfn =? 0 then None
else
if bypass =? 0 then
let (valc, labelc) := (pfn @ (cache (shared adt))) in
if (labelc =? -1) then
let (valm, labelm) := (pfn @ (flatmem (shared adt))) in
if (labelm =? -2) || (labelm =? vmid) then
let cache' := ((cache (shared adt)) # pfn == (valm, labelm)) in
let adt' := adt {shared: (shared adt) {cache: cache'}} in
Some adt'
else
None
else
if (labelc =? vmid) ||(labelc =? -2) then
Some adt
else
None
(* cache bypass *)
else
let (valm, labelm) := (pfn @ (flatmem (shared adt))) in
if (labelm =? -2) || (labelm =? vmid) then
Some adt
else
None
end
| _, _ => None
end.
Definition mem_store_check_spec (gfn: Z64) (reg: Z) (bypass: Z) (adt: RData) : option RData :=
match gfn, icore adt with
| VZ64 gfn, false =>
let vmid := cur_vmid adt in
match gfn @ (pt (vmid @ (npts (shared adt)))) with
| (pfn, level, pte) =>
if pfn =? 0 then None
else
let new_label := (
if (s2_owner (pfn @ (s2page (shared adt))) =? INVALID) ||
(s2_count (pfn @ (s2page (shared adt))) >? 0) then
-2
else
vmid
) in
if bypass =? 0 then
let (valc, label) := (pfn @ (cache (shared adt))) in
if (label =? -1) then
let fm' := ((flatmem (shared adt)) # pfn == (val, new_label)) in
let cache' := ((cache (shared adt)) # pfn == (val, new_label)) in
let adt' := adt {shared: (shared adt) {flatmem: fm'} {cache: cache'}} in
Some adt'
else
(* if cache hit --> (label = vmid) *)
if (label =? vmid) || (label =? -2) then
let cache' := ((cache (shared adt)) # pfn == (val, new_label)) in
let adt' := adt {shared: (shared adt) {cache: cache'}} in
Some adt'
else
None
(* cache bypass *)
else
let (valm, labelm) := (pfn @ (flatmem (shared adt))) in
if (labelm =? -2) || (labelm =? vmid) then
let fm' := ((flatmem (shared adt)) # pfn == (val, new_label)) in
let adt' := adt {shared: (shared adt) {flatmem: fm'}} in
Some adt'
else
None
end
| _, _ => None
end.
End PageMgmtSpec.
Section PageMgmtSpecLow.
Context `{real_params: RealParams}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := PageIndex_ops) LDATA).
Definition get_pfn_owner_spec0 (pfn: Z64) (adt: RData) : option Z :=
match pfn with
| VZ64 pfn =>
rely is_pfn pfn;
when' index == get_s2_page_index_spec (VZ64 (pfn * PAGE_SIZE)) adt;
rely is_int64 index;
if index =? INVALID64 then
check_spec INVALID adt
else
rely is_s2page index;
when ret == get_s2_page_vmid_spec (VZ64 index) adt;
rely is_vmid ret;
check_spec ret adt
end.
Definition set_pfn_owner_spec0 (pfn: Z64) (vmid: Z) (adt: RData) : option RData :=
match pfn with
| VZ64 pfn =>
rely is_pfn pfn;
when' index == get_s2_page_index_spec (VZ64 (pfn * PAGE_SIZE)) adt;
rely is_int64 index;
if index =? INVALID64 then
Some adt
else
rely is_s2page index;
set_s2_page_vmid_spec (VZ64 index) vmid adt
end.
Definition get_pfn_count_spec0 (pfn: Z64) (adt: RData) : option Z :=
match pfn with
| VZ64 pfn =>
rely is_pfn pfn;
when' index == get_s2_page_index_spec (VZ64 (pfn * PAGE_SIZE)) adt;
rely is_int64 index;
if index =? INVALID64 then
check_spec INVALID adt
else
rely is_s2page index;
when ret == get_s2_page_count_spec (VZ64 index) adt;
rely is_count ret;
check_spec ret adt
end.
Definition set_pfn_count_spec0 (pfn: Z64) (count: Z) (adt: RData) : option RData :=
match pfn with
| VZ64 pfn =>
rely is_pfn pfn;
when' index == get_s2_page_index_spec (VZ64 (pfn * PAGE_SIZE)) adt;
rely is_int64 index;
if index =? INVALID64 then
Some adt
else
rely is_s2page index;
set_s2_page_count_spec (VZ64 index) count adt
end.
Definition get_pfn_map_spec0 (pfn: Z64) (adt: RData) : option Z64 :=
match pfn with
| VZ64 pfn =>
rely is_pfn pfn;
when' index == get_s2_page_index_spec (VZ64 (pfn * PAGE_SIZE)) adt;
rely is_int64 index;
if index =? INVALID64 then
check64_spec (VZ64 INVALID64) adt
else
rely is_s2page index;
when' ret == get_s2_page_gfn_spec (VZ64 index) adt;
rely is_gfn ret;
check64_spec (VZ64 ret) adt
end.
Definition set_pfn_map_spec0 (pfn: Z64) (gfn: Z64) (adt: RData) : option RData :=
match pfn, gfn with
| VZ64 pfn, VZ64 gfn =>
rely is_pfn pfn;
when' index == get_s2_page_index_spec (VZ64 (pfn * PAGE_SIZE)) adt;
rely is_int64 index;
if index =? INVALID64 then
Some adt
else
rely is_s2page index;
set_s2_page_gfn_spec (VZ64 index) (VZ64 gfn) adt
end.
Definition mem_load_check_spec0 (gfn: Z64) (reg: Z) (bypass: Z) (adt: RData) : option RData :=
mem_load_no_tlb_spec gfn reg bypass adt.
Definition mem_store_check_spec0 (gfn: Z64) (reg: Z) (bypass: Z) (adt: RData) : option RData :=
mem_store_no_tlb_spec gfn reg bypass adt.
Inductive get_pfn_owner_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| get_pfn_owner_spec_low_intro s (WB: _ -> Prop) m'0 labd pfn res
(Hinv: high_level_invariant labd)
(Hspec: get_pfn_owner_spec0 (VZ64 (Int64.unsigned pfn)) labd = Some (Int.unsigned res)):
get_pfn_owner_spec_low_step s WB ((Vlong pfn)::nil) (m'0, labd) (Vint res) (m'0, labd).
Inductive set_pfn_owner_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| set_pfn_owner_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' pfn vmid
(Hinv: high_level_invariant labd)
(Hspec: set_pfn_owner_spec0 (VZ64 (Int64.unsigned pfn)) (Int.unsigned vmid) labd = Some labd'):
set_pfn_owner_spec_low_step s WB ((Vlong pfn)::(Vint vmid)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive get_pfn_count_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| get_pfn_count_spec_low_intro s (WB: _ -> Prop) m'0 labd pfn res
(Hinv: high_level_invariant labd)
(Hspec: get_pfn_count_spec0 (VZ64 (Int64.unsigned pfn)) labd = Some (Int.unsigned res)):
get_pfn_count_spec_low_step s WB ((Vlong pfn)::nil) (m'0, labd) (Vint res) (m'0, labd).
Inductive set_pfn_count_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| set_pfn_count_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' pfn count
(Hinv: high_level_invariant labd)
(Hspec: set_pfn_count_spec0 (VZ64 (Int64.unsigned pfn)) (Int.unsigned count) labd = Some labd'):
set_pfn_count_spec_low_step s WB ((Vlong pfn)::(Vint count)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive get_pfn_map_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| get_pfn_map_spec_low_intro s (WB: _ -> Prop) m'0 labd pfn res
(Hinv: high_level_invariant labd)
(Hspec: get_pfn_map_spec0 (VZ64 (Int64.unsigned pfn)) labd = Some (VZ64 (Int64.unsigned res))):
get_pfn_map_spec_low_step s WB ((Vlong pfn)::nil) (m'0, labd) (Vlong res) (m'0, labd).
Inductive set_pfn_map_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| set_pfn_map_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' pfn gfn
(Hinv: high_level_invariant labd)
(Hspec: set_pfn_map_spec0 (VZ64 (Int64.unsigned pfn)) (VZ64 (Int64.unsigned gfn)) labd = Some labd'):
set_pfn_map_spec_low_step s WB ((Vlong pfn)::(Vlong gfn)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive mem_load_check_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| mem_load_check_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' gfn reg bypass
(Hinv: high_level_invariant labd)
(Hspec: mem_load_check_spec0 (VZ64 (Int64.unsigned gfn)) (Int.unsigned reg) (Int.unsigned bypass) labd = Some labd'):
mem_load_check_spec_low_step s WB ((Vlong gfn)::(Vint reg)::(Vint bypass)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive mem_store_check_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| mem_store_check_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' gfn reg bypass
(Hinv: high_level_invariant labd)
(Hspec: mem_store_check_spec0 (VZ64 (Int64.unsigned gfn)) (Int.unsigned reg) (Int.unsigned bypass) labd = Some labd'):
mem_store_check_spec_low_step s WB ((Vlong gfn)::(Vint reg)::(Vint bypass)::nil) (m'0, labd) Vundef (m'0, labd').
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Definition get_pfn_owner_spec_low: compatsem LDATAOps :=
csem get_pfn_owner_spec_low_step (type_of_list_type (Tint64::nil)) Tint32.
Definition set_pfn_owner_spec_low: compatsem LDATAOps :=
csem set_pfn_owner_spec_low_step (type_of_list_type (Tint64::Tint32::nil)) Tvoid.
Definition get_pfn_count_spec_low: compatsem LDATAOps :=
csem get_pfn_count_spec_low_step (type_of_list_type (Tint64::nil)) Tint32.
Definition set_pfn_count_spec_low: compatsem LDATAOps :=
csem set_pfn_count_spec_low_step (type_of_list_type (Tint64::Tint32::nil)) Tvoid.
Definition get_pfn_map_spec_low: compatsem LDATAOps :=
csem get_pfn_map_spec_low_step (type_of_list_type (Tint64::nil)) Tint64.
Definition set_pfn_map_spec_low: compatsem LDATAOps :=
csem set_pfn_map_spec_low_step (type_of_list_type (Tint64::Tint64::nil)) Tvoid.
Definition mem_load_check_spec_low: compatsem LDATAOps :=
csem mem_load_check_spec_low_step (type_of_list_type (Tint64::Tint32::Tint32::nil)) Tvoid.
Definition mem_store_check_spec_low: compatsem LDATAOps :=
csem mem_store_check_spec_low_step (type_of_list_type (Tint64::Tint32::Tint32::nil)) Tvoid.
End WITHMEM.
End PageMgmtSpecLow.