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 VMPower.Spec.
Require Import AbsMachine.Spec.
Require Import SmmuAux.Spec.
Require Import MmioSPTWalk.Spec.
Require Import RData.
Require Import BootOps.Spec.
Require Import Constants.
Require Import HypsecCommLib.
Require Import MmioSPTOps.Spec.
Require Import SmmuAux.Layer.
Require Import NPTWalk.Spec.
Require Import MmioSPTWalk.Spec.
Local Open Scope Z_scope.
Section SmmuOpsSpec.
Definition emulate_mmio_spec (addr: Z64) (hsr: Z) (adt: RData) : option (RData * Z) :=
match addr with
| VZ64 addr =>
let fault_ipa := Z.lor addr (Z.land (far_el2 (ctxt_regs (regs adt))) 4095) in
let len := host_dabt_get_as' hsr in
let is_write := host_dabt_is_write' hsr in
let rt := host_dabt_get_rd' hsr in
let vcpuid := cur_vcpuid adt in
rely is_addr addr; rely is_int hsr;
rely is_addr fault_ipa; rely is_int len; rely is_int is_write;
rely is_int rt; rely is_vcpu vcpuid;
if halt adt then Some (adt, 0) else
let cpu := curid adt in
match SMMU_ID @ (lock adt), SMMU_ID @ (oracle adt), SMMU_ID @ (log adt) with
| LockFalse, sorc, sl0 =>
match H_CalLock (sorc cpu sl0 ++ sl0) with
| Some (_, EMPTY, None) =>
let smmu := CalSMMU (smmu_vmid (shared adt)) (sorc cpu sl0) in
let sl := TEVENT cpu (TSHARED (OPULL SMMU_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (sorc cpu sl0) ++ sl0 in
let sl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OSMMU smmu)) :: sl in
let conf := smmu_conf adt in
let num := smmu_num conf in
rely is_smmu num;
match is_smmu_range_loop (Z.to_nat num) addr 0 INVALID conf with
| Some (idx, res) =>
rely is_int res;
if res =? INVALID then
Some (adt {tstate: 1} {shared: (shared adt) {smmu_vmid: smmu}}
{log: (log adt) # SMMU_ID == sl'} {lock: (lock adt) # SMMU_ID == LockFalse},
INVALID)
else
rely is_smmu res;
let logn := HOSTVISOR @ (data_log adt) in
let ctxt := (ctxt_id HOSTVISOR vcpuid) @ (shadow_ctxts adt) in
match
handle_host_mmio_specx res fault_ipa len is_write rt (ctxt_regs ctxt) (ctxt_states ctxt) (ctxt_regs (regs adt)) (doracle adt) logn smmu
with
| Some (halt', logn', cregs', cstates', rcregs') =>
if halt' then
Some (adt {halt: true} {tstate: 0} {shared: (shared adt) {smmu_vmid: smmu}}
{data_log : if logn =? logn' then data_log adt else (data_log adt) # HOSTVISOR == logn'}
{regs : (regs adt) {ctxt_regs : rcregs'}}
{log: (log adt) # SMMU_ID == sl} {lock: (lock adt) # SMMU_ID == (LockOwn true)},
0)
else
Some (adt {tstate: 1} {shared: (shared adt) {smmu_vmid: smmu}}
{data_log : if logn =? logn' then data_log adt else (data_log adt) # HOSTVISOR == logn'}
{shadow_ctxts: if (is_write =? 0)
then (shadow_ctxts adt) # (ctxt_id HOSTVISOR vcpuid) == ((ctxt {ctxt_regs : cregs'}) {ctxt_states : cstates'})
else (shadow_ctxts adt)}
{regs : (regs adt) {ctxt_regs : rcregs'}}
{log: (log adt) # SMMU_ID == sl'} {lock: (lock adt) # SMMU_ID == LockFalse},
res)
| _ => None
end
| _ => None
end
| _ => None
end
| _, _, _ => None
end
end.
Definition el2_free_smmu_pgd_spec (cbndx: Z) (index: Z) (adt: RData) : option RData :=
rely is_smmu index; rely is_smmu_cfg cbndx;
if halt adt then Some adt else
let cpu := curid adt in
match SMMU_ID @ (lock adt), SMMU_ID @ (oracle adt), SMMU_ID @ (log adt) with
| LockFalse, sorc, sl0 =>
match H_CalLock (sorc cpu sl0 ++ sl0) with
| Some (_, EMPTY, None) =>
let smmu := CalSMMU (smmu_vmid (shared adt)) (sorc cpu sl0) in
let sl := TEVENT cpu (TSHARED (OPULL SMMU_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (sorc cpu sl0) ++ sl0 in
let vmid := (smmu_id index cbndx) @ smmu in
if vmid =? INVALID then
let sl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OSMMU smmu)) :: sl in
Some adt {tstate: 1} {shared: (shared adt) {smmu_vmid: smmu}}
{log: (log adt) # SMMU_ID == sl'} {lock: (lock adt) # SMMU_ID == LockFalse}
else
rely is_vmid vmid;
let id := INFO_ID + vmid in
match id @ (lock adt), id @ (oracle adt), id @ (log adt) with
| LockFalse, orac, l0 =>
match H_CalLock ((orac cpu l0) ++ l0) with
| Some (_, LEMPTY, None) =>
let info := CalVMInfo (vmid @ (vminfos (shared adt))) (orac cpu l0) in
rely is_int (vm_state (VS info));
let l' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OVMINFO info)) ::
TEVENT cpu (TSHARED (OPULL id)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) ::
(orac cpu l0) ++ l0 in
if vm_state (VS info) =? POWEROFF then
let smmu' := smmu # (smmu_id index cbndx) == INVALID in
let sl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OSMMU smmu')) :: sl in
Some adt {tstate: 1} {shared: (shared adt) {smmu_vmid: smmu'} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: ((log adt) # SMMU_ID == sl') # id == l'} {lock: ((lock adt) # SMMU_ID == LockFalse) # id == LockFalse}
else
Some adt {halt: true} {tstate: 1} {shared: (shared adt) {smmu_vmid: smmu} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: ((log adt) # SMMU_ID == sl) # id == l'} {lock: ((lock adt) # SMMU_ID == (LockOwn true)) # id == LockFalse}
| _ => None
end
| _, _, _ => None
end
| _ => None
end
| _, _, _ => None
end.
Definition el2_alloc_smmu_pgd_spec (cbndx: Z) (vmid: Z) (index: Z) (adt: RData) : option RData :=
rely is_vmid vmid; rely is_smmu index; rely is_smmu_cfg cbndx;
if halt adt then Some adt else
let cpu := curid adt in
let num := index @ (smmu_dev_context_banks (smmu_conf adt)) in
rely is_int num;
match SMMU_ID @ (lock adt), SMMU_ID @ (oracle adt), SMMU_ID @ (log adt) with
| LockFalse, sorc, sl0 =>
match H_CalLock (sorc cpu sl0 ++ sl0) with
| Some (_, EMPTY, None) =>
let smmu := CalSMMU (smmu_vmid (shared adt)) (sorc cpu sl0) in
let sl := TEVENT cpu (TSHARED (OPULL SMMU_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (sorc cpu sl0) ++ sl0 in
if cbndx <? num then
let target := (smmu_id index cbndx) @ smmu in
rely is_int target;
if target =? INVALID then
let smmu' := smmu # (smmu_id index cbndx) == vmid in
let sl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OSMMU smmu')) :: sl in
match SPT_ID @ (lock adt), SPT_ID @ (oracle adt), SPT_ID @ (log adt) with
| LockFalse, pto, ptl0 =>
match H_CalLock (pto cpu ptl0 ++ ptl0) with
| Some (_, EMPTY, None) =>
let spt := CalSPT (spts (shared adt)) (pto cpu ptl0) in
let ttbr := SMMU_TTBR index cbndx in
let spt' := spt {spt_pt: (spt_pt spt) # ttbr == (ZMap.init (0, 0))}
{spt_pgd_t: (spt_pgd_t spt) # ttbr == (ZMap.init false)}
{spt_pmd_t: (spt_pmd_t spt) # ttbr == (ZMap.init (ZMap.init false))} in
let ptl' := (TEVENT cpu (TTICKET REL_LOCK)) :: (TEVENT cpu (TSHARED (OSPT spt'))) ::
TEVENT cpu (TSHARED (OPULL SPT_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (pto cpu ptl0) ++ ptl0 in
Some adt {tstate: 1} {shared: (shared adt) {smmu_vmid: smmu'} {spts: spt'}}
{log: ((log adt) # SMMU_ID == sl') # SPT_ID == ptl'} {lock: ((lock adt) # SMMU_ID == LockFalse) # SPT_ID == LockFalse}
| _ => None
end
| _, _, _ => None
end
else
let sl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OSMMU smmu)) :: sl in
Some adt {tstate: 1} {shared: (shared adt) {smmu_vmid: smmu}}
{log: (log adt) # SMMU_ID == sl'} {lock: (lock adt) # SMMU_ID == LockFalse}
else
Some adt {halt: true} {tstate: 0} {shared: (shared adt) {smmu_vmid: smmu}}
{log: (log adt) # SMMU_ID == sl} {lock: (lock adt) # SMMU_ID == (LockOwn true)}
| _ => None
end
| _, _, _ => None
end.
Definition smmu_assign_page_spec (cbndx: Z) (index: Z) (pfn: Z64) (gfn: Z64) (adt: RData) : option RData :=
match pfn, gfn with
| VZ64 pfn, VZ64 gfn =>
rely is_smmu index; rely is_smmu_cfg cbndx; rely is_gfn gfn; rely is_pfn pfn;
if halt adt then Some adt else
let cpu := curid adt in
match SMMU_ID @ (lock adt), SMMU_ID @ (oracle adt), SMMU_ID @ (log adt) with
| LockFalse, sorc, sl0 =>
match H_CalLock (sorc cpu sl0 ++ sl0) with
| Some (_, EMPTY, None) =>
let smmu := CalSMMU (smmu_vmid (shared adt)) (sorc cpu sl0) in
let sl := TEVENT cpu (TSHARED (OPULL SMMU_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (sorc cpu sl0) ++ sl0 in
let sl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OSMMU smmu)) :: sl in
let vmid := (smmu_id index cbndx) @ smmu in
if vmid =? INVALID then
Some adt {tstate: 1} {shared: (shared adt) {smmu_vmid: smmu}}
{log: (log adt) # SMMU_ID == sl'} {lock: (lock adt) # SMMU_ID == LockFalse}
else
rely is_vmid vmid;
let id := INFO_ID + vmid in
let ptid := NPT_ID in
let cpu := curid adt in
match id @ (lock adt), id @ (oracle adt), id @ (log adt),
S2PAGE_ID @ (lock adt), S2PAGE_ID @ (log adt), S2PAGE_ID @ (oracle adt),
ptid @ (lock adt), ptid @ (log adt), ptid @ (oracle adt),
FLATMEM_ID @ (log adt), FLATMEM_ID @ (oracle adt) with
| LockFalse, vmo, vml0, LockFalse, spl0, spo, LockFalse, ptl0, pto, fml0, fmo =>
match H_CalLock ((vmo cpu vml0) ++ vml0), H_CalLock ((spo cpu spl0) ++ spl0), H_CalLock ((pto cpu ptl0) ++ ptl0) with
| Some (_, LEMPTY, None), Some (_, LEMPTY, None), Some (_, LEMPTY, None) =>
let info := CalVMInfo (vmid @ (vminfos (shared adt))) (vmo cpu vml0) in
let s2p := CalS2Page (s2page (shared adt)) (spo cpu spl0) in
let npt := CalNPT (HOSTVISOR @ (npts (shared adt))) (pto cpu ptl0) in
let fmem := CalFlatmem (flatmem (shared adt)) (fmo cpu fml0) in
let spl := TEVENT cpu (TSHARED (OPULL S2PAGE_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (spo cpu spl0) ++ spl0 in
let ptl := TEVENT cpu (TSHARED (OPULL ptid)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (pto cpu ptl0) ++ ptl0 in
let vml := TEVENT cpu (TSHARED (OPULL id)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: ((vmo cpu vml0) ++ vml0) in
let vml' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OVMINFO info)) :: vml in
let state := vm_state (VS info) in
rely is_int state;
if (HOSTVISOR <? vmid) && (vmid <? COREVISOR) then
if state =? VERIFIED then
let page := pfn @ s2p in
rely is_int (s2_owner page); rely is_int (s2_count page); rely is_int64 (s2_gfn page);
if s2_owner page =? HOSTVISOR then
if s2_count page =? 0 then
let s2p' := s2p # pfn == (mkS2Page vmid INVALID gfn) in
let logn := vmid @ (data_log adt) in
let fmem' := fmem # pfn == ((doracle adt) vmid logn) in
match pfn @ (pt npt) with
| (_, level, pte) =>
rely is_int level;
match (if (if phys_page pte =? 0 then 0 else level) =? 0 then Some (false, npt)
else local_mmap HOSTVISOR (pfn * PAGE_SIZE) 3 PAGE_GUEST npt) with
| Some (halt', npt') =>
let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p')) :: spl in
let ptl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (ONPT npt')) :: ptl in
let fml' := TEVENT cpu (TSHARED (OFLATMEM fmem')) :: (fmo cpu fml0) ++ fml0 in
if halt' then
Some adt {halt: true} {tstate: 0}
{shared: (shared adt) {npts: (npts (shared adt)) # HOSTVISOR == npt'} {smmu_vmid: smmu}
{s2page: s2p} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: (((((log adt) # SMMU_ID == sl) # id == vml)# S2PAGE_ID == spl) # ptid == ptl)}
{lock: ((((lock adt) # SMMU_ID == (LockOwn true)) # id == (LockOwn true)) # S2PAGE_ID == (LockOwn true)) # ptid == (LockOwn true)}
else
Some adt {tstate: 1} {data_log: (data_log adt) # vmid == (logn + 1)}
{shared: (shared adt) {npts: (npts (shared adt)) # HOSTVISOR == npt'} {smmu_vmid: smmu}
{s2page: s2p'} {flatmem: fmem'} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: (((((log adt) # SMMU_ID == sl') # id == vml')# S2PAGE_ID == spl') # ptid == ptl') # FLATMEM_ID == fml'}
{lock: ((((lock adt) # SMMU_ID == LockFalse) # id == LockFalse) # S2PAGE_ID == LockFalse) # ptid == LockFalse}
| _ => None
end
end
else
Some adt {halt: true} {tstate: 0} {shared: (shared adt) {s2page: s2p} {smmu_vmid: smmu} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: (((log adt) # SMMU_ID == sl) # id == vml) # S2PAGE_ID == spl} {lock: (((lock adt) # SMMU_ID == (LockOwn true)) # id == (LockOwn true)) # S2PAGE_ID == (LockOwn true)}
else
if s2_owner page =? vmid then
let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p)) :: spl in
Some adt {tstate: 1} {shared: (shared adt) {s2page: s2p} {smmu_vmid: smmu} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: (((log adt) # SMMU_ID == sl') # id == vml') # S2PAGE_ID == spl'} {lock: (((lock adt) # SMMU_ID == LockFalse) # id == LockFalse) # S2PAGE_ID == LockFalse}
else
Some adt {halt: true} {tstate: 0} {shared: (shared adt) {s2page: s2p} {smmu_vmid: smmu} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: (((log adt) # SMMU_ID == sl) # id == vml) # S2PAGE_ID == spl} {lock: (((lock adt) # SMMU_ID == (LockOwn true)) # id == (LockOwn true)) # S2PAGE_ID == (LockOwn true)}
else
Some (adt {halt: true} {tstate: 0} {shared: (shared adt) {smmu_vmid: smmu} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: ((log adt) # SMMU_ID == sl) # id == vml} {lock: ((lock adt) # SMMU_ID == (LockOwn true)) # id == (LockOwn true)})
else
Some adt {tstate: 1} {shared: (shared adt) {smmu_vmid: smmu} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: ((log adt) # SMMU_ID == sl') # id == vml'} {lock: ((lock adt) # SMMU_ID == LockFalse) # id == LockFalse}
| _, _, _ => None
end
| _, _, _, _, _, _, _, _, _, _, _ => None
end
| _ => None
end
| _, _, _ => None
end
end.
Definition smmu_map_page_spec (cbndx: Z) (index: Z) (iova: Z64) (pte: Z64) (adt: RData) : option RData :=
match iova, pte with
| VZ64 iova, VZ64 pte =>
rely is_smmu index; rely is_smmu_cfg cbndx; rely is_smmu_addr iova; rely is_int64 pte;
if halt adt then Some adt else
let cpu := curid adt in
match SMMU_ID @ (lock adt), SMMU_ID @ (oracle adt), SMMU_ID @ (log adt) with
| LockFalse, sorc, sl0 =>
match H_CalLock (sorc cpu sl0 ++ sl0) with
| Some (_, EMPTY, None) =>
let smmu := CalSMMU (smmu_vmid (shared adt)) (sorc cpu sl0) in
let sl := TEVENT cpu (TSHARED (OPULL SMMU_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (sorc cpu sl0) ++ sl0 in
let sl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OSMMU smmu)) :: sl in
let vmid := (smmu_id index cbndx) @ smmu in
if vmid =? INVALID then
Some adt {tstate: 1} {shared: (shared adt) {smmu_vmid: smmu}}
{log: (log adt) # SMMU_ID == sl'} {lock: (lock adt) # SMMU_ID == LockFalse}
else
rely is_vmid vmid;
let id := INFO_ID + vmid in
match id @ (lock adt), id @ (oracle adt), id @ (log adt),
S2PAGE_ID @ (lock adt), S2PAGE_ID @ (log adt), S2PAGE_ID @ (oracle adt),
SPT_ID @ (lock adt), SPT_ID @ (log adt), SPT_ID @ (oracle adt) with
| LockFalse, vmo, vml0, LockFalse, spl0, spo, LockFalse, ptl0, pto =>
match H_CalLock ((vmo cpu vml0) ++ vml0), H_CalLock ((spo cpu spl0) ++ spl0), H_CalLock ((pto cpu ptl0) ++ ptl0) with
| Some (_, LEMPTY, None), Some (_, LEMPTY, None), Some (_, LEMPTY, None) =>
let info := CalVMInfo (vmid @ (vminfos (shared adt))) (vmo cpu vml0) in
let s2p := CalS2Page (s2page (shared adt)) (spo cpu spl0) in
let spt := CalSPT (spts (shared adt)) (pto cpu ptl0) in
let spl := TEVENT cpu (TSHARED (OPULL S2PAGE_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (spo cpu spl0) ++ spl0 in
let ptl := TEVENT cpu (TSHARED (OPULL SPT_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (pto cpu ptl0) ++ ptl0 in
let vml := TEVENT cpu (TSHARED (OPULL id)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: ((vmo cpu vml0) ++ vml0) in
let vml' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OVMINFO info)) :: vml in
let state := vm_state (VS info) in
rely is_int state;
if (HOSTVISOR <? vmid) && (vmid <? COREVISOR) && (state =? VERIFIED) then
Some (adt {halt: true} {tstate: 0} {shared: (shared adt) {smmu_vmid: smmu} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: ((log adt) # SMMU_ID == sl) # id == vml} {lock: ((lock adt) # SMMU_ID == (LockOwn true)) # id == (LockOwn true)})
else
let pfn := phys_page pte / PAGE_SIZE in
let gfn := iova / PAGE_SIZE in
let page := pfn @ s2p in
rely is_int (s2_owner page); rely is_int (s2_count page); rely is_int64 (s2_gfn page);
if (vmid =? s2_owner page) && (gfn =? s2_gfn page) then
match local_spt_map cbndx index iova pte spt with
| Some (halt', spt') =>
if halt' then
Some adt {halt: true} {tstate: 0}
{shared: (shared adt) {spts: spt'} {s2page: s2p} {smmu_vmid: smmu} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: (((((log adt) # SMMU_ID == sl) # id == vml)# S2PAGE_ID == spl) # SPT_ID == ptl)}
{lock: ((((lock adt) # SMMU_ID == (LockOwn true)) # id == (LockOwn true)) # S2PAGE_ID == (LockOwn true)) # SPT_ID == (LockOwn true)}
else
let s2p' := (if (s2_owner page =? HOSTVISOR) && (s2_count page <? EL2_SMMU_CFG_SIZE)
then s2p # pfn == (page {s2_count: (s2_count page) + 1}) else s2p) in
let ptl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OSPT spt')) :: ptl in
let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p')) :: spl in
Some adt {tstate: 1} {shared: (shared adt) {spts: spt'} {s2page: s2p'} {smmu_vmid: smmu} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: (((((log adt) # SMMU_ID == sl') # id == vml') # S2PAGE_ID == spl') # SPT_ID == ptl')}
{lock: ((((lock adt) # SMMU_ID == LockFalse) # id == LockFalse) # S2PAGE_ID == LockFalse) # SPT_ID == LockFalse}
| _ => None
end
else
Some adt {halt: true} {tstate: 0} {shared: (shared adt) {s2page: s2p} {smmu_vmid: smmu} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: (((log adt) # SMMU_ID == sl) # id == vml) # S2PAGE_ID == spl}
{lock: (((lock adt) # SMMU_ID == (LockOwn true)) # id == (LockOwn true)) # S2PAGE_ID == (LockOwn true)}
| _, _, _ => None
end
| _, _, _, _, _, _, _, _, _ => None
end
| _ => None
end
| _, _, _ => None
end
end.
Definition el2_arm_lpae_iova_to_phys_spec (iova: Z64) (cbndx: Z) (index: Z) (adt: RData) : option (RData * Z64) :=
match iova with
| VZ64 iova =>
rely is_smmu index; rely is_smmu_cfg cbndx; rely is_smmu_addr iova;
if halt adt then Some (adt, VZ64 0) else
let cpu := curid adt in
match SPT_ID @ (lock adt), SPT_ID @ (oracle adt), SPT_ID @ (log adt) with
| LockFalse, pto, ptl0 =>
match H_CalLock (pto cpu ptl0 ++ ptl0) with
| Some (_, EMPTY, None) =>
let spt := CalSPT (spts (shared adt)) (pto cpu ptl0) in
let ttbr := SMMU_TTBR index cbndx in
let pt := ttbr @ (spt_pt spt) in
let gfn := iova / PAGE_SIZE in
match gfn @ pt with
| (pfn, pte) =>
rely is_int64 pte;
let ptl' := (TEVENT cpu (TTICKET REL_LOCK)) :: (TEVENT cpu (TSHARED (OSPT spt))) ::
TEVENT cpu (TSHARED (OPULL SPT_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (pto cpu ptl0) ++ ptl0 in
Some (adt {tstate: 1} {shared: (shared adt) {spts: spt}}
{log: (log adt) # SPT_ID == ptl'} {lock: (lock adt) # SPT_ID == LockFalse},
VZ64 (phys_page pte + (Z.land iova 4095)))
end
| _ => None
end
| _, _, _ => None
end
end.
Definition el2_arm_lpae_clear_spec (iova: Z64) (cbndx: Z) (index: Z) (adt: RData) : option RData :=
match iova with
| VZ64 iova =>
rely is_smmu index; rely is_smmu_cfg cbndx; rely is_smmu_addr iova;
if halt adt then Some adt else
let cpu := curid adt in
match SMMU_ID @ (lock adt), SMMU_ID @ (oracle adt), SMMU_ID @ (log adt) with
| LockFalse, sorc, sl0 =>
match H_CalLock (sorc cpu sl0 ++ sl0) with
| Some (_, EMPTY, None) =>
let smmu := CalSMMU (smmu_vmid (shared adt)) (sorc cpu sl0) in
let sl := TEVENT cpu (TSHARED (OPULL SMMU_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (sorc cpu sl0) ++ sl0 in
let sl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OSMMU smmu)) :: sl in
let vmid := (smmu_id index cbndx) @ smmu in
if vmid =? INVALID then
Some adt {tstate: 1} {shared: (shared adt) {smmu_vmid: smmu}}
{log: (log adt) # SMMU_ID == sl'} {lock: (lock adt) # SMMU_ID == LockFalse}
else
rely is_vmid vmid;
let id := INFO_ID + vmid in
match id @ (lock adt), id @ (oracle adt), id @ (log adt),
S2PAGE_ID @ (lock adt), S2PAGE_ID @ (log adt), S2PAGE_ID @ (oracle adt),
SPT_ID @ (lock adt), SPT_ID @ (log adt), SPT_ID @ (oracle adt) with
| LockFalse, vmo, vml0, LockFalse, spl0, spo, LockFalse, ptl0, pto =>
match H_CalLock ((vmo cpu vml0) ++ vml0), H_CalLock ((spo cpu spl0) ++ spl0), H_CalLock ((pto cpu ptl0) ++ ptl0) with
| Some (_, LEMPTY, None), Some (_, LEMPTY, None), Some (_, LEMPTY, None) =>
let info := CalVMInfo (vmid @ (vminfos (shared adt))) (vmo cpu vml0) in
let s2p := CalS2Page (s2page (shared adt)) (spo cpu spl0) in
let spt := CalSPT (spts (shared adt)) (pto cpu ptl0) in
let spl := TEVENT cpu (TSHARED (OPULL S2PAGE_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (spo cpu spl0) ++ spl0 in
let ptl := TEVENT cpu (TSHARED (OPULL SPT_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (pto cpu ptl0) ++ ptl0 in
let vml := TEVENT cpu (TSHARED (OPULL id)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: ((vmo cpu vml0) ++ vml0) in
let vml' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OVMINFO info)) :: vml in
let state := vm_state (VS info) in
rely is_int state;
if (HOSTVISOR <? vmid) && (vmid <? COREVISOR) && (state =? VERIFIED) then
Some (adt {halt: true} {tstate: 0} {shared: (shared adt) {smmu_vmid: smmu} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: ((log adt) # SMMU_ID == sl) # id == vml} {lock: ((lock adt) # SMMU_ID == (LockOwn true)) # id == (LockOwn true)})
else
let ttbr := SMMU_TTBR index cbndx in
let pt := ttbr @ (spt_pt spt) in
let gfn := iova / PAGE_SIZE in
let (_, pte) := gfn @ pt in
rely is_int64 pte;
match (if pte =? 0 then Some (false, spt) else local_spt_map cbndx index iova 0 spt) with
| Some (halt', spt') =>
if halt' then
Some adt {halt: true} {tstate: 0} {shared: (shared adt) {spts: spt'} {smmu_vmid: smmu} {s2page: s2p} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: ((((log adt) # SMMU_ID == sl) # id == vml) # S2PAGE_ID == spl) # SPT_ID == ptl}
{lock: ((((lock adt) # SMMU_ID == (LockOwn true)) # id == (LockOwn true)) # S2PAGE_ID == (LockOwn true)) # SPT_ID == (LockOwn true)}
else
let pfn := phys_page pte / PAGE_SIZE in
let page := pfn @ s2p in
rely is_int (s2_owner page); rely is_int (s2_count page);
let s2p' := (if (s2_owner page =? HOSTVISOR) && (s2_count page >? 0)
then s2p # pfn == (page {s2_count: (s2_count page) - 1}) else s2p) in
let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p')) :: spl in
let ptl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OSPT spt')) :: ptl in
Some adt {tstate: 1} {shared: (shared adt) {spts: spt'} {smmu_vmid: smmu} {s2page: s2p'} {vminfos: (vminfos (shared adt)) # vmid == info}}
{log: (((((log adt) # SMMU_ID == sl') # id == vml') # S2PAGE_ID == spl') # SPT_ID == ptl')}
{lock: ((((lock adt) # SMMU_ID == LockFalse) # id == LockFalse) # S2PAGE_ID == LockFalse) # SPT_ID == LockFalse}
| _ => None
end
| _, _, _ => None
end
| _, _, _, _, _, _, _, _, _ => None
end
| _ => None
end
| _, _, _ => None
end
end.
End SmmuOpsSpec.
Section SmmuOpsSpecLow.
Context `{real_params: RealParams}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := SmmuAux_ops) LDATA).
Definition emulate_mmio_spec0 (addr: Z64) (hsr: Z) (adt: RData) : option (RData * Z) :=
match addr with
| VZ64 addr =>
when adt' == acquire_lock_smmu_spec adt;
when res == is_smmu_range_spec (VZ64 addr) adt';
rely is_int res;
if res =? INVALID then
when adt'' == release_lock_smmu_spec adt';
when ret == check_spec res adt'';
Some (adt'', ret)
else
when adt'' == handle_host_mmio_spec (VZ64 addr) res hsr adt';
when adt3 == release_lock_smmu_spec adt'';
when ret == check_spec res adt3;
Some (adt3, ret)
end.
Definition el2_free_smmu_pgd_spec0 (cbndx: Z) (index: Z) (adt: RData) : option RData :=
when adt' == acquire_lock_smmu_spec adt;
when vmid == get_smmu_cfg_vmid_spec cbndx index adt';
rely is_int vmid;
if vmid =? INVALID then
release_lock_smmu_spec adt'
else
when power, adt2 == get_vm_poweron_spec vmid adt';
rely is_int power;
if power =? 0 then
when adt'' == set_smmu_cfg_vmid_spec cbndx index INVALID adt2;
release_lock_smmu_spec adt''
else
when adt'' == panic_spec adt2;
release_lock_smmu_spec adt''.
Definition el2_alloc_smmu_pgd_spec0 (cbndx: Z) (vmid: Z) (index: Z) (adt: RData) : option RData :=
when adt' == acquire_lock_smmu_spec adt;
when num == get_smmu_num_context_banks_spec index adt';
rely is_int num;
if cbndx <? num then
when target == get_smmu_cfg_vmid_spec cbndx index adt';
rely is_int target;
if target =? INVALID then
when adt2 == set_smmu_cfg_vmid_spec cbndx index vmid adt';
when adt3 == init_spt_spec cbndx index adt2;
release_lock_smmu_spec adt3
else
release_lock_smmu_spec adt'
else
when adt2 == panic_spec adt';
release_lock_smmu_spec adt2.
Definition smmu_assign_page_spec0 (cbndx: Z) (index: Z) (pfn: Z64) (gfn: Z64) (adt: RData) : option RData :=
when adt1 == acquire_lock_smmu_spec adt;
when vmid == get_smmu_cfg_vmid_spec cbndx index adt1;
rely is_int vmid;
if vmid =? INVALID then
release_lock_smmu_spec adt1
else
when adt2 == assign_smmu_spec vmid pfn gfn adt1;
release_lock_smmu_spec adt2.
Definition smmu_map_page_spec0 (cbndx: Z) (index: Z) (iova: Z64) (pte: Z64) (adt: RData) : option RData :=
when adt1 == acquire_lock_smmu_spec adt;
when vmid == get_smmu_cfg_vmid_spec cbndx index adt1;
rely is_int vmid;
if vmid =? INVALID then
release_lock_smmu_spec adt1
else
when adt2 == map_smmu_spec vmid cbndx index iova pte adt1;
release_lock_smmu_spec adt2.
Definition el2_arm_lpae_iova_to_phys_spec0 (iova: Z64) (cbndx: Z) (index: Z) (adt: RData) : option (RData * Z64) :=
match iova with
| VZ64 iova =>
when' pte, adt' == walk_spt_spec cbndx index (VZ64 iova) adt;
rely is_int64 pte;
let res := phys_page pte + (Z.land iova 4095) in
when' ret == check64_spec (VZ64 res) adt';
Some (adt', VZ64 ret)
end.
Definition el2_arm_lpae_clear_spec0 (iova: Z64) (cbndx: Z) (index: Z) (adt: RData) : option RData :=
when adt1 == acquire_lock_smmu_spec adt;
when vmid == get_smmu_cfg_vmid_spec cbndx index adt1;
rely is_int vmid;
if vmid =? INVALID then
release_lock_smmu_spec adt1
else
when adt2 == clear_smmu_spec vmid cbndx index iova adt1;
release_lock_smmu_spec adt2.
Inductive emulate_mmio_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| emulate_mmio_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' addr hsr res
(Hinv: high_level_invariant labd)
(Hspec: emulate_mmio_spec0 (VZ64 (Int64.unsigned addr)) (Int.unsigned hsr) labd = Some (labd', (Int.unsigned res))):
emulate_mmio_spec_low_step s WB ((Vlong addr)::(Vint hsr)::nil) (m'0, labd) (Vint res) (m'0, labd').
Inductive el2_free_smmu_pgd_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| el2_free_smmu_pgd_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' cbndx index
(Hinv: high_level_invariant labd)
(Hspec: el2_free_smmu_pgd_spec0 (Int.unsigned cbndx) (Int.unsigned index) labd = Some labd'):
el2_free_smmu_pgd_spec_low_step s WB ((Vint cbndx)::(Vint index)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive el2_alloc_smmu_pgd_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| el2_alloc_smmu_pgd_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' cbndx vmid index
(Hinv: high_level_invariant labd)
(Hspec: el2_alloc_smmu_pgd_spec0 (Int.unsigned cbndx) (Int.unsigned vmid) (Int.unsigned index) labd = Some labd'):
el2_alloc_smmu_pgd_spec_low_step s WB ((Vint cbndx)::(Vint vmid)::(Vint index)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive smmu_assign_page_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| smmu_assign_page_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' cbndx index pfn gfn
(Hinv: high_level_invariant labd)
(Hspec: smmu_assign_page_spec0 (Int.unsigned cbndx) (Int.unsigned index) (VZ64 (Int64.unsigned pfn)) (VZ64 (Int64.unsigned gfn)) labd = Some labd'):
smmu_assign_page_spec_low_step s WB ((Vint cbndx)::(Vint index)::(Vlong pfn)::(Vlong gfn)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive smmu_map_page_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| smmu_map_page_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' cbndx index iova pte
(Hinv: high_level_invariant labd)
(Hspec: smmu_map_page_spec0 (Int.unsigned cbndx) (Int.unsigned index) (VZ64 (Int64.unsigned iova)) (VZ64 (Int64.unsigned pte)) labd = Some labd'):
smmu_map_page_spec_low_step s WB ((Vint cbndx)::(Vint index)::(Vlong iova)::(Vlong pte)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive el2_arm_lpae_iova_to_phys_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| el2_arm_lpae_iova_to_phys_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' iova cbndx index res
(Hinv: high_level_invariant labd)
(Hspec: el2_arm_lpae_iova_to_phys_spec0 (VZ64 (Int64.unsigned iova)) (Int.unsigned cbndx) (Int.unsigned index) labd = Some (labd', (VZ64 (Int64.unsigned res)))):
el2_arm_lpae_iova_to_phys_spec_low_step s WB ((Vlong iova)::(Vint cbndx)::(Vint index)::nil) (m'0, labd) (Vlong res) (m'0, labd').
Inductive el2_arm_lpae_clear_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| el2_arm_lpae_clear_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' iova cbndx index
(Hinv: high_level_invariant labd)
(Hspec: el2_arm_lpae_clear_spec0 (VZ64 (Int64.unsigned iova)) (Int.unsigned cbndx) (Int.unsigned index) labd = Some labd'):
el2_arm_lpae_clear_spec_low_step s WB ((Vlong iova)::(Vint cbndx)::(Vint index)::nil) (m'0, labd) Vundef (m'0, labd').
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Definition emulate_mmio_spec_low: compatsem LDATAOps :=
csem emulate_mmio_spec_low_step (type_of_list_type (Tint64::Tint32::nil)) Tint32.
Definition el2_free_smmu_pgd_spec_low: compatsem LDATAOps :=
csem el2_free_smmu_pgd_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.
Definition el2_alloc_smmu_pgd_spec_low: compatsem LDATAOps :=
csem el2_alloc_smmu_pgd_spec_low_step (type_of_list_type (Tint32::Tint32::Tint32::nil)) Tvoid.
Definition smmu_assign_page_spec_low: compatsem LDATAOps :=
csem smmu_assign_page_spec_low_step (type_of_list_type (Tint32::Tint32::Tint64::Tint64::nil)) Tvoid.
Definition smmu_map_page_spec_low: compatsem LDATAOps :=
csem smmu_map_page_spec_low_step (type_of_list_type (Tint32::Tint32::Tint64::Tint64::nil)) Tvoid.
Definition el2_arm_lpae_iova_to_phys_spec_low: compatsem LDATAOps :=
csem el2_arm_lpae_iova_to_phys_spec_low_step (type_of_list_type (Tint64::Tint32::Tint32::nil)) Tint64.
Definition el2_arm_lpae_clear_spec_low: compatsem LDATAOps :=
csem el2_arm_lpae_clear_spec_low_step (type_of_list_type (Tint64::Tint32::Tint32::nil)) Tvoid.
End WITHMEM.
End SmmuOpsSpecLow.