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 RData.
Require Import Constants.
Require Import HypsecCommLib.
Require Import CalLock.
Local Open Scope Z_scope.
Section AbsMachineSpec.
Definition tlb_invalidate_spec (vmid: Z) (gfn: Z64) (adt: RData) : option RData :=
match gfn with
| VZ64 gfn =>
if halt adt then Some adt else
rely is_vmid vmid; rely is_gfn gfn;
let id := NPT_ID + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts (shared adt)) in
let tlb' := (tlb npt) # gfn == (ZMap.init (0, 0)) in
Some (adt {shared: (shared adt) {npts: (npts (shared adt)) # vmid == (npt {tlb: tlb'})}})
| _ => None
end
end.
Definition flush_cache_spec (pfn: Z) (adt: RData) : option RData :=
match pfn @ (cache (shared adt)) with
| None => Some adt
| Some (val, label) =>
let mem' := ((flatmem (shared adt)) # pfn == (val, label)) in
let cac' := ((cache (shared adt)) # pfn == None) in
Some adt {shared: (shared adt) {flatmem: mem'} {cache: cac'}}
end.
Definition load_phys_mem (pfn: Z) (bypass: Z) (mem: ZMap.t (Z * Z)) (cac: ZMap.t (option (Z * Z))) :=
if bypass =? 0 then
match pfn @ cac with
| Some (val, label) =>
(cac, val)
| None =>
let (val, label) := pfn @ mem in
let cac' := cac # pfn == (Some (val, label)) in
(cac', val)
end
else
let (val, label) := pfn @ mem in
(cac, val).
Definition store_phys_mem (pfn: Z) (val: Z) (label: Z) (bypass: Z) (mem: ZMap.t (Z * Z)) (cac: ZMap.t (option (Z * Z))) :=
if bypass =? 0 then
let cac' := cac # pfn == (Some (val, label)) in
(mem, cac')
else
let mem' := mem # pfn == (val, label) in
(mem', cac).
Definition mem_load_raw_spec (gfn: Z64) (reg: Z) (bypass: Z) (adt: RData) : option RData :=
match gfn with
| VZ64 gfn =>
if halt adt then Some adt else
let curid := curid adt in
let vmid := cur_vmid adt in
let vcpuid := cur_vcpuid adt in
let ctxtid := ctxt_id vmid vcpuid in
let ctxt := ctxtid @ (shadow_ctxts adt) in
let npt := vmid @ (npts (shared adt)) in
let addr := gfn * PAGE_SIZE in
(* match gfn @ (curid @ (tlb npt)) with *)
let pfn := tlb_look_up vmid curid gfn (tlb npt) in
(* | VZ64 pfn => *)
if pfn =? 0 then
let vttbr := pt_vttbr vmid in
let vttbr_pa := phys_page vttbr in
let pgd_idx := pgd_index addr in
let pgd_p := Z.lor vttbr_pa (pgd_idx * 8) in
let pgd := pgd_p @ (pt_vttbr_pool npt) in
if pgd =? 0 then None
else
let pgd_pa := phys_page pgd in
let pud_idx := pud_index addr in
let pud_p := Z.lor pgd_pa (pud_idx * 8) in
let pud := pud_p @ (pt_pgd_pool npt) in
if pud =? 0 then None
else
let pud_pa := phys_page pud in
let pmd_idx := pmd_index addr in
let pmd_p := Z.lor pud_pa (pmd_idx * 8) in
let pmd := pmd_p @ (pt_pud_pool npt) in
if pmd =? 0 then None
else
if pmd_table pmd =? PMD_TYPE_TABLE then
let pmd_pa := phys_page pmd in
let pte_idx := pte_index addr in
let pte_p := Z.lor pmd_pa (pte_idx * 8) in
let pte := pte_p @ (pt_pmd_pool npt) in
let pfn := phys_page pte / PAGE_SIZE in
if pfn =? 0 then None else
let (cac', val) := load_phys_mem pfn bypass (flatmem (shared adt)) (cache (shared adt)) in
match set_shadow_ctxt_specx reg val (ctxt_regs ctxt) (ctxt_states ctxt) with
| (cregs', cstates') =>
let ctxt' := ctxt {ctxt_regs: cregs'} {ctxt_states: cstates'} in
when adt' == reload_tlb vmid gfn pfn 3 adt;
Some adt' {shared: (shared adt') {cache: cac'}} {shadow_ctxts: (shadow_ctxts adt') # ctxtid == ctxt'}
end
else
(* pfn: 2mb base + offset *)
let gfn_b := gfn / PTRS_PER_PMD * PTRS_PER_PMD in
let offset := gfn - gfn_b in
let pfn := (phys_page pmd / PAGE_SIZE) in
if pfn =? 0 then None else
let pfn_offset := pfn + offset in
let (cac', val) := load_phys_mem pfn_offset bypass (flatmem (shared adt)) (cache (shared adt)) in
match set_shadow_ctxt_specx reg val (ctxt_regs ctxt) (ctxt_states ctxt) with
| (cregs', cstates') =>
let ctxt' := ctxt {ctxt_regs: cregs'} {ctxt_states: cstates'} in
let gfn_base := gfn - offset in
when adt' == reload_tlb vmid gfn_base pfn 2 adt;
Some adt' {shared: (shared adt') {cache: cac'}} {shadow_ctxts: (shadow_ctxts adt') # ctxtid == ctxt'}
end
else
let (cac', val) := load_phys_mem pfn bypass (flatmem (shared adt)) (cache (shared adt)) in
match set_shadow_ctxt_specx reg val (ctxt_regs ctxt) (ctxt_states ctxt) with
| (cregs', cstates') =>
let ctxt' := ctxt {ctxt_regs: cregs'} {ctxt_states: cstates'} in
Some adt {shared: (shared adt) {cache: cac'}} {shadow_ctxts: (shadow_ctxts adt) # ctxtid == ctxt'}
end
end.
Definition mem_store_raw_spec (gfn: Z64) (reg: Z) (bypass: Z) (adt: RData) : option RData :=
match gfn with
| VZ64 gfn =>
if halt adt then Some adt else
let curid := curid adt in
let vmid := cur_vmid adt in
let vcpuid := cur_vcpuid adt in
let ctxtid := ctxt_id vmid vcpuid in
let ctxt := ctxtid @ (shadow_ctxts adt) in
let npt := vmid @ (npts (shared adt)) in
let addr := gfn * PAGE_SIZE in
(* match gfn @ (curid @ (tlb npt)) with *)
let pfn := tlb_look_up vmid curid gfn (tlb npt) in
(* | VZ64 pfn => *)
if pfn =? 0 then
let vttbr := pt_vttbr vmid in
let vttbr_pa := phys_page vttbr in
let pgd_idx := pgd_index addr in
let pgd_p := Z.lor vttbr_pa (pgd_idx * 8) in
let pgd := pgd_p @ (pt_vttbr_pool npt) in
if pgd =? 0 then None
else
let pgd_pa := phys_page pgd in
let pud_idx := pud_index addr in
let pud_p := Z.lor pgd_pa (pud_idx * 8) in
let pud := pud_p @ (pt_pgd_pool npt) in
if pud =? 0 then None
else
let pud_pa := phys_page pud in
let pmd_idx := pmd_index addr in
let pmd_p := Z.lor pud_pa (pmd_idx * 8) in
let pmd := pmd_p @ (pt_pud_pool npt) in
if pmd =? 0 then None
else
if pmd_table pmd =? PMD_TYPE_TABLE then
let pmd_pa := phys_page pmd in
let pte_idx := pte_index addr in
let pte_p := Z.lor pmd_pa (pte_idx * 8) in
let pte := pte_p @ (pt_pmd_pool npt) in
let pfn := phys_page pte / PAGE_SIZE in
if pfn =? 0 then None else
let val := get_shadow_ctxt_specx reg (ctxt_regs ctxt) (ctxt_states ctxt) in
let (mem', cac') := store_phys_mem pfn val vmid bypass (flatmem (shared adt)) (cache (shared adt)) in
when adt' == reload_tlb vmid gfn pfn 3 adt;
Some adt' {shared: (shared adt') {flatmem: mem'} {cache: cac'}}
else
(* pfn: 2mb base + offset *)
let gfn_b := gfn / PTRS_PER_PMD * PTRS_PER_PMD in
let offset := gfn - gfn_b in
let pfn := (phys_page pmd / PAGE_SIZE) in
if pfn =? 0 then None else
let pfn_offset := pfn + offset in
let val := get_shadow_ctxt_specx reg (ctxt_regs ctxt) (ctxt_states ctxt) in
let (mem', cac') := store_phys_mem pfn_offset val vmid bypass (flatmem (shared adt)) (cache (shared adt)) in
when adt' == reload_tlb vmid gfn pfn 3 adt;
Some adt' {shared: (shared adt') {flatmem: mem'} {cache: cac'}}
else
let val := get_shadow_ctxt_specx reg (ctxt_regs ctxt) (ctxt_states ctxt) in
let (mem', cac') := store_phys_mem pfn val vmid bypass (flatmem (shared adt)) (cache (shared adt)) in
when adt' == reload_tlb vmid gfn pfn 3 adt;
Some adt' {shared: (shared adt') {flatmem: mem'} {cache: cac'}}
end.
Definition acquire_shared_spec (lk: Z) (adt: RData): option RData :=
match ZMap.get lk adt.(log), ZMap.get lk adt.(lock) with
| Some l, LockOwn false =>
let l' := TEVENT adt.(curid) (TSHARED (OPULL lk)) :: l in
match H_CalLock l', CalState lk l' adt.(shared) with
(* | Some _, Some sdt' => Some adt {log: ZMap.set lk (Some l') adt.(log)} *)
| Some _, sdt' => Some adt {log: ZMap.set lk (Some l') adt.(log)}
{lock: ZMap.set lk (LockOwn true) adt.(lock)}
{tstate: 0}
{shared: sdt'}
| _, _ => None
end
| _, _ => None
end
.
Definition release_shared_spec (e: SharedMemEvent) (lk: Z) (adt: RData): option RData :=
match ZMap.get lk adt.(log), ZMap.get lk adt.(lock) with
| Some l, LockOwn true =>
let l' := TEVENT adt.(curid) (TSHARED e) :: l in
match H_CalLock l' with
| Some _ => Some adt {log: ZMap.set lk (Some l') adt.(log)}
{lock: ZMap.set lk (LockOwn false) adt.(lock)}
{tstate: 1}
| _ => None
end
| _, _ => None
end
.
Definition release_shared_pt_spec (vmid: Z) (adt: RData) : option RData :=
let e := ONPT (ZMap.get vmid adt.(shared).(npts)) in
release_shared_spec e (lock_idx_pt vmid) adt.
Definition release_shared_spt_spec (adt: RData) : option RData :=
let e := OSPT adt.(shared).(spts) in
release_shared_spec e lock_idx_spt adt.
Definition release_shared_s2page_spec (adt: RData) : option RData :=
let e := OS2_PAGE adt.(shared).(s2page) in
release_shared_spec e lock_idx_s2page adt.
Definition release_shared_core_spec (adt: RData) : option RData :=
let e := OCORE_DATA adt.(shared).(core_data) in
release_shared_spec e lock_idx_core adt.
Definition release_shared_vm_spec (vmid: Z) (adt: RData) : option RData :=
let e := OVMINFO (ZMap.get vmid adt.(shared).(vminfos)) in
release_shared_spec e (lock_idx_vm vmid) adt.
Definition release_shared_smmu_spec (adt: RData) : option RData :=
let e := OSMMU adt.(shared).(smmu_vmid) in
release_shared_spec e lock_idx_smmu adt.
Definition get_now_spec (lk: Z) (adt: RData): option (RData * Z) :=
match ZMap.get lk adt.(log) with
| None => None
| Some l => let l' := TEVENT adt.(curid) (TTICKET GET_NOW) ::
(ZMap.get lk adt.(oracle)) adt.(curid) l ++
l in
match CalTicketLockWraparound l' with
| None => None
| Some (_, n, _) =>
let adt' := adt {log: ZMap.set lk (Some l') adt.(log)} in
Some (adt', n)
end
end.
Definition incr_now_spec (lk: Z) (adt: RData): option RData :=
match ZMap.get lk adt.(log) with
| None => None
| Some l => let l' := TEVENT adt.(curid) (TTICKET INC_NOW) ::
(* No need to query oracle when unlocking *)
(* (ZMap.get lk adt.(oracle)) adt.(curid) l ++ *)
l in
Some adt {log: ZMap.set lk (Some l') adt.(log)}
end.
Definition log_incr_spec (lk: Z) (adt: RData): option RData :=
match ZMap.get lk adt.(log) with
| None => None
| Some l => let l' := TEVENT adt.(curid) (TTICKET INC_NOW) ::
(* No need to query oracle when unlocking *)
(* (ZMap.get lk adt.(oracle)) adt.(curid) l ++ *)
l in
Some adt {log: ZMap.set lk (Some l') adt.(log)}
end.
Definition log_hold_spec (lk: Z) (adt: RData): option RData :=
match ZMap.get lk adt.(log) with
| None => None
| Some l => let l' := TEVENT adt.(curid) (TTICKET HOLD_LOCK) ::
l in
Some adt {log: ZMap.set lk (Some l') adt.(log)}
end.
Definition incr_ticket_spec (bound lk: Z) (adt: RData): option (RData * Z) :=
match ZMap.get lk adt.(log) with
| None => None
| Some l =>
let p := Z.to_nat bound in
let l' := (ZMap.get lk adt.(oracle)) adt.(curid) l ++ l in
match CalTicketLockWraparound l' with
| None => None
| Some (t, _, _) =>
let l'' := TEVENT adt.(curid) (TTICKET (INC_TICKET p)) :: l' in
let adt' := adt {log: ZMap.set lk (Some l'') adt.(log)} in
Some (adt', t)
end
end.
Parameter verify_img: Z -> Z64 -> Z.
Parameter reg_desc: Z -> Z.
Parameter exception_vector: Z64 -> Z.
Definition check_spec (n: Z) (adt: RData) : option Z :=
if halt adt then Some 0
else Some n.
Definition check64_spec (n: Z64) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0)
else Some n.
Definition panic_spec (adt: RData) : option RData :=
Some adt {halt: true}.
Definition get_shared_kvm_spec (vmid: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
rely is_vm vmid;
Some (VZ64 (shared_kvm vmid)).
Definition get_shared_vcpu_spec (vmid: Z) (vcpuid: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
rely is_vm vmid; rely is_vcpu vcpuid;
Some (VZ64 (shared_vcpu vmid vcpuid)).
Definition get_vgic_cpu_base_spec (adt: RData) : option Z64 :=
Some (VZ64 0).
Definition verify_image_spec (vmid: Z) (addr: Z64) (adt: RData) : option Z :=
match addr with
| VZ64 addr =>
if halt adt then Some 0 else
rely is_vm vmid; rely is_addr addr;
Some (verify_img vmid (VZ64 addr))
end.
Definition get_sys_reg_desc_val_spec (index: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
rely is_reg index;
Some (VZ64 (reg_desc index)).
Definition get_exception_vector_spec (pstate: Z64) (adt: RData) : option Z64 :=
Some (VZ64 (exception_vector pstate)).
Definition read_actlr_el1_spec (adt: RData) : option (RData * Z64) :=
if halt adt then Some (adt, VZ64 0) else
match query_data_oracle (cur_vmid adt) adt with
| (adt', val) => Some (adt', VZ64 val)
end.
Definition pool_start_spec (vmid: Z) (adt: RData) : option Z64 :=
Some (VZ64 (pool_start' vmid)).
Definition pool_end_spec (vmid: Z) (adt: RData) : option Z64 :=
Some (VZ64 (pool_end' vmid)).
Definition pgd_start_spec (vmid: Z) (adt: RData) : option Z64 :=
Some (VZ64 (pgd_start' vmid)).
Definition pud_start_spec (vmid: Z) (adt: RData) : option Z64 :=
Some (VZ64 (pud_start' vmid)).
Definition pmd_start_spec (vmid: Z) (adt: RData) : option Z64 :=
Some (VZ64 (pmd_start' vmid)).
Definition get_pgd_next_spec (vmid: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
rely is_vm vmid;
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
Some (VZ64 (pt_pgd_next npt))
| _ => None
end.
Definition set_pgd_next_spec (vmid: Z) (next: Z64) (adt: RData) : option RData :=
if halt adt then Some adt else
match next with
| VZ64 next' =>
rely is_vm vmid;
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
rely ((pgd_start' vmid <=? next') && (next' <=? pud_start' vmid));
let npt' := npt {pt_pgd_next: next'} in
Some adt {npts: (npts adt) # vmid == npt'}
| _ => None
end
end.
Definition get_pud_next_spec (vmid: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
rely is_vm vmid;
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
Some (VZ64 (pt_pud_next npt))
| _ => None
end.
Definition set_pud_next_spec (vmid: Z) (next: Z64) (adt: RData) : option RData :=
if halt adt then Some adt else
match next with
| VZ64 next' =>
rely is_vm vmid;
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
rely ((pud_start' vmid <=? next') && (next' <=? pmd_start' vmid));
let npt' := npt {pt_pud_next: next'} in
Some adt {npts: (npts adt) # vmid == npt'}
| _ => None
end
end.
Definition get_pmd_next_spec (vmid: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
rely is_vm vmid;
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
Some (VZ64 (pt_pmd_next npt))
| _ => None
end.
Definition set_pmd_next_spec (vmid: Z) (next: Z64) (adt: RData) : option RData :=
if halt adt then Some adt else
match next with
| VZ64 next' =>
rely is_vm vmid;
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
rely ((pmd_start' vmid <=? next') && (next' <=? pool_end' vmid));
let npt' := npt {pt_pmd_next: next'} in
Some adt {npts: (npts adt) # vmid == npt'}
| _ => None
end
end.
Definition vttbr_load_spec (vmid: Z) (addr: Z64) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
match addr with
| VZ64 addr =>
rely is_vm vmid;
rely ((pool_start' vmid <=? addr) && (addr <? pgd_start' vmid));
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
Some (VZ64 (addr @ (pt_vttbr_pool npt)))
| _ => None
end
end.
Definition vttbr_store_spec (vmid: Z) (addr: Z64) (value: Z64) (adt: RData) : option RData :=
if halt adt then Some adt else
match addr, value with
| VZ64 addr, VZ64 value' =>
rely is_vm vmid;
rely ((pool_start' vmid <=? addr) && (addr <? pgd_start' vmid));
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
let npt' := npt {pt_vttbr_pool: (pt_vttbr_pool npt) # addr == value'} in
Some adt {npts: (npts adt) # vmid == npt'}
| _ => None
end
end.
Definition pgd_load_spec (vmid: Z) (addr: Z64) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
match addr with
| VZ64 addr =>
rely is_vm vmid;
rely ((pgd_start' vmid <=? addr) && (addr <? pud_start' vmid));
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
Some (VZ64 (addr @ (pt_pgd_pool npt)))
| _ => None
end
end.
Definition pgd_store_spec (vmid: Z) (addr: Z64) (value: Z64) (adt: RData) : option RData :=
if halt adt then Some adt else
match addr, value with
| VZ64 addr, VZ64 value' =>
rely is_vm vmid;
rely ((pgd_start' vmid <=? addr) && (addr <? pud_start' vmid));
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
let npt' := npt {pt_pgd_pool: (pt_pgd_pool npt) # addr == value'} in
Some adt {npts: (npts adt) # vmid == npt'}
| _ => None
end
end.
Definition pud_load_spec (vmid: Z) (addr: Z64) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
match addr with
| VZ64 addr =>
rely is_vm vmid;
rely ((pud_start' vmid <=? addr) && (addr <? pmd_start' vmid));
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
Some (VZ64 (addr @ (pt_pud_pool npt)))
| _ => None
end
end.
Definition pud_store_spec (vmid: Z) (addr: Z64) (value: Z64) (adt: RData) : option RData :=
if halt adt then Some adt else
match addr, value with
| VZ64 addr, VZ64 value' =>
rely is_vm vmid;
rely ((pud_start' vmid <=? addr) && (addr <? pmd_start' vmid));
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
let npt' := npt {pt_pud_pool: (pt_pud_pool npt) # addr == value'} in
Some adt {npts: (npts adt) # vmid == npt'}
| _ => None
end
end.
Definition pmd_load_spec (vmid: Z) (addr: Z64) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
match addr with
| VZ64 addr =>
rely is_vm vmid;
rely ((pmd_start' vmid <=? addr) && (addr <? pool_end' vmid));
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
Some (VZ64 (addr @ (pt_pmd_pool npt)))
| _ => None
end
end.
Definition pmd_store_spec (vmid: Z) (addr: Z64) (value: Z64) (adt: RData) : option RData :=
if halt adt then Some adt else
match addr, value with
| VZ64 addr, VZ64 value' =>
rely is_vm vmid;
rely ((pmd_start' vmid <=? addr) && (addr <? pool_end' vmid));
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
let npt' := npt {pt_pmd_pool: (pt_pmd_pool npt) # addr == value'} in
Some adt {npts: (npts adt) # vmid == npt'}
| _ => None
end
end.
Definition get_pt_vttbr_spec (vmid: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
rely is_vm vmid;
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
Some (VZ64 (pt_vttbr npt))
| _ => None
end.
Definition set_pt_vttbr_spec (vmid: Z) (vttbr: Z64) (adt: RData) : option RData :=
if halt adt then Some adt else
match vttbr with
| VZ64 vttbr =>
rely is_vm vmid; rely is_pt_addr vttbr;
let id := 2 + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let npt := vmid @ (npts adt) in
let npt' := npt {pt_vttbr: vttbr} in
Some adt {npts: (npts adt) # vmid == npt'}
| _ => None
end
end.
Definition get_mem_region_cnt_spec (adt: RData) : option Z :=
Some (region_cnt adt).
Definition get_mem_region_base_spec (index: Z) (adt: RData) : option Z64 :=
match is_memblock index with
| true =>
let region := index @ (regions adt) in
Some (VZ64 (base region))
| _ => None
end.
Definition get_mem_region_size_spec (index: Z) (adt: RData) : option Z64 :=
match is_memblock index with
| true =>
let region := index @ (regions adt) in
Some (VZ64 (size region))
| _ => None
end.
Definition get_mem_region_index_spec (idx: Z) (adt: RData) : option Z64 :=
match is_memblock idx with
| true =>
let region := idx @ (regions adt) in
Some (VZ64 (index region))
| _ => None
end.
Definition get_mem_region_flag_spec (idx: Z) (adt: RData) : option Z64 :=
match is_memblock idx with
| true =>
let region := idx @ (regions adt) in
Some (VZ64 (flag region))
| _ => None
end.
Definition get_s2_page_vmid_spec (index: Z64) (adt: RData) : option Z :=
if halt adt then Some 0 else
match index with
| VZ64 idx =>
rely is_s2page idx;
let id := 1 in
match ZMap.get id (lock adt) with
| LockOwn true =>
Some (owner (idx @ (s2page adt)))
| _ => None
end
end.
Definition set_s2_page_vmid_spec (index: Z64) (vmid: Z) (adt: RData) : option RData :=
if halt adt then Some adt else
match index with
| VZ64 idx =>
rely is_s2page idx; rely is_vm vmid;
let id := 1 in
match ZMap.get id (lock adt) with
| LockOwn true =>
let s2p := idx @ (s2page adt) in
let s2p' := s2p {owner: vmid} in
Some adt {s2page: (s2page adt) # idx == s2p'}
| _ => None
end
end.
Definition get_s2_page_count_spec (index: Z64) (adt: RData) : option Z :=
if halt adt then Some 0 else
match index with
| VZ64 idx =>
rely is_s2page idx;
let id := 1 in
match ZMap.get id (lock adt) with
| LockOwn true =>
Some (count (idx @ (s2page adt)))
| _ => None
end
end.
Definition set_s2_page_count_spec (index: Z64) (count: Z) (adt: RData) : option RData :=
if halt adt then Some adt else
match index with
| VZ64 idx =>
rely is_s2page idx; rely is_count count;
let id := 1 in
match ZMap.get id (lock adt) with
| LockOwn true =>
let s2p := idx @ (s2page adt) in
let s2p' := s2p {count: count} in
Some adt {s2page: (s2page adt) # idx == s2p'}
| _ => None
end
end.
Definition get_vm_state_spec (vmid: Z) (adt: RData) : option Z :=
if halt adt then Some 0 else
rely is_vm vmid;
let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
Some (vm_state info)
| _ => None
end.
Definition set_vm_state_spec (vmid: Z) (state: Z) (adt: RData) : option RData :=
if halt adt then Some adt else
rely is_vm vmid;
let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
let info' := info {vm_state: state} in
Some adt {vminfos: (vminfos adt) # vmid == info'}
| _ => None
end.
Definition get_vcpu_state_spec (vmid: Z) (vcpuid: Z) (adt: RData) : option Z :=
if halt adt then Some 0 else
rely is_vm vmid; rely is_vcpu vcpuid;
let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
Some (vcpuid @ (vm_vcpu_state info))
| _ => None
end.
Definition set_vcpu_state_spec (vmid: Z) (vcpuid: Z) (state: Z) (adt: RData) : option RData :=
if halt adt then Some adt else
rely is_vm vmid; rely is_vcpu vcpuid;
let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
let vcpu_state' := (vm_vcpu_state info) # vcpuid == state in
let info' := info {vm_vcpu_state: vcpu_state'} in
Some adt {vminfos: (vminfos adt) # vmid == info'}
| _ => None
end.
Definition get_vm_power_spec (vmid: Z) (adt: RData) : option Z :=
if halt adt then Some 0 else
rely is_vm vmid;
let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
Some (vm_power info)
| _ => None
end.
Definition set_vm_power_spec (vmid: Z) (power: Z) (adt: RData) : option RData :=
if halt adt then Some adt else
rely is_vm vmid;
let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
let info' := info {vm_power: power} in
Some adt {vminfos: (vminfos adt) # vmid == info'}
| _ => None
end.
Definition get_vm_inc_exe_spec (vmid: Z) (adt: RData) : option Z :=
match is_vm vmid with
| true =>
if halt adt then Some 0
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
Some (vm_inc_exe info)
| _ => None
end
| _ => None
end.
Definition set_vm_inc_exe_spec (vmid: Z) (inc_exe: Z) (adt: RData) : option RData :=
match is_vm vmid with
| true =>
if halt adt then Some adt
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
let info' := info {vm_inc_exe: inc_exe} in
Some adt {vminfos: (vminfos adt) # vmid == info'}
| _ => None
end
| _ => None
end.
Definition get_vm_kvm_spec (vmid: Z) (adt: RData) : option Z64 :=
match is_vm vmid with
| true =>
if halt adt then Some (VZ64 0)
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
Some (VZ64 (vm_kvm info))
| _ => None
end
| _ => None
end.
Definition set_vm_kvm_spec (vmid: Z) (kvm: Z64) (adt: RData) : option RData :=
match kvm with
| VZ64 kvm =>
match is_vm vmid with
| true =>
if halt adt then Some adt
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
let info' := info {vm_kvm: kvm} in
Some adt {vminfos: (vminfos adt) # vmid == info'}
| _ => None
end
| _ => None
end
end.
Definition get_vm_vcpu_spec (vmid: Z) (vcpuid: Z) (adt: RData) : option Z64 :=
match is_vm vmid, is_vcpu vcpuid with
| true, true =>
if halt adt then Some (VZ64 0)
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
Some (VZ64 (vcpuid @ (vm_vcpu info)))
| _ => None
end
| _, _ => None
end.
Definition set_vm_vcpu_spec (vmid: Z) (vcpuid: Z) (vcpu: Z64) (adt: RData) : option RData :=
match vcpu with
| VZ64 vcpu =>
match is_vm vmid, is_vcpu vcpuid with
| true, true =>
if halt adt then Some adt
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
let vcpu' := (vm_vcpu info) # vcpuid == vcpu in
let info' := info {vm_vcpu: vcpu'} in
Some adt {vminfos: (vminfos adt) # vmid == info'}
| _ => None
end
| _, _ => None
end
end.
Definition get_vm_next_load_idx_spec (vmid: Z) (adt: RData) : option Z :=
match is_vm vmid with
| true =>
if halt adt then Some 0
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
Some (vm_next_load_info info)
| _ => None
end
| _ => None
end.
Definition set_vm_next_load_idx_spec (vmid: Z) (load_idx: Z) (adt: RData) : option RData :=
match is_vm vmid with
| true =>
if halt adt then Some adt
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
let info' := info {vm_next_load_info: load_idx} in
Some adt {vminfos: (vminfos adt) # vmid == info'}
| _ => None
end
| _ => None
end.
Definition get_vm_load_addr_spec (vmid: Z) (load_idx: Z) (adt: RData) : option Z64 :=
match is_vm vmid, is_load_idx load_idx with
| true, true =>
if halt adt then Some (VZ64 0)
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
Some (VZ64 (load_idx @ (vm_load_addr info)))
| _ => None
end
| _, _ => None
end.
Definition set_vm_load_addr_spec (vmid: Z) (load_idx: Z) (load_addr: Z64) (adt: RData) : option RData :=
match load_addr with
| VZ64 load_addr =>
match is_vm vmid, is_load_idx load_idx with
| true, true =>
if halt adt then Some adt
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
let load' := (vm_load_addr info) # load_idx == load_addr in
let info' := info {vm_load_addr: load'} in
Some adt {vminfos: (vminfos adt) # vmid == info'}
| _ => None
end
| _, _ => None
end
end.
Definition get_vm_load_size_spec (vmid: Z) (load_idx: Z) (adt: RData) : option Z64 :=
match is_vm vmid, is_load_idx load_idx with
| true, true =>
if halt adt then Some (VZ64 0)
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
Some (VZ64 (load_idx @ (vm_load_size info)))
| _ => None
end
| _, _ => None
end.
Definition set_vm_load_size_spec (vmid: Z) (load_idx: Z) (size: Z64) (adt: RData) : option RData :=
match size with
| VZ64 size =>
match is_vm vmid, is_load_idx load_idx with
| true, true =>
if halt adt then Some adt
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
let load' := (vm_load_size info) # load_idx == size in
let info' := info {vm_load_size: load'} in
Some adt {vminfos: (vminfos adt) # vmid == info'}
| _ => None
end
| _, _ => None
end
end.
Definition get_vm_remap_addr_spec (vmid: Z) (load_idx: Z) (adt: RData) : option Z64 :=
match is_vm vmid, is_load_idx load_idx with
| true, true =>
if halt adt then Some (VZ64 0)
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
Some (VZ64 (load_idx @ (vm_remap_addr info)))
| _ => None
end
| _, _ => None
end.
Definition set_vm_remap_addr_spec (vmid: Z) (load_idx: Z) (remap_addr: Z64) (adt: RData) : option RData :=
match remap_addr with
| VZ64 remap_addr =>
match is_vm vmid, is_load_idx load_idx with
| true, true =>
if halt adt then Some adt
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
let load' := (vm_remap_addr info) # load_idx == remap_addr in
let info' := info {vm_remap_addr: load'} in
Some adt {vminfos: (vminfos adt) # vmid == info'}
| _ => None
end
| _, _ => None
end
end.
Definition get_vm_mapped_pages_spec (vmid: Z) (load_idx: Z) (adt: RData) : option Z64 :=
match is_vm vmid, is_load_idx load_idx with
| true, true =>
if halt adt then Some (VZ64 0)
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
Some (VZ64 (load_idx @ (vm_mapped_pages info)))
| _ => None
end
| _, _ => None
end.
Definition set_vm_mapped_pages_spec (vmid: Z) (load_idx: Z) (mapped: Z64) (adt: RData) : option RData :=
match mapped with
| VZ64 mapped =>
match is_vm vmid, is_load_idx load_idx with
| true, true =>
if halt adt then Some adt
else let id := INFO_START + vmid in
match ZMap.get id (lock adt) with
| LockOwn true =>
let info := vmid @ (vminfos adt) in
let load' := (vm_mapped_pages info) # load_idx == mapped in
let info' := info {vm_mapped_pages: load'} in
Some adt {vminfos: (vminfos adt) # vmid == info'}
| _ => None
end
| _, _ => None
end
end.
Definition get_next_vmid_spec (adt: RData) : option Z :=
if halt adt then Some (next_vmid (core_data adt)) else
let id := 0 in
match ZMap.get id (lock adt) with
| LockOwn true =>
Some (next_vmid (core_data adt))
| _ => None
end.
Definition set_next_vmid_spec (vmid: Z) (adt: RData) : option RData :=
if halt adt then Some adt else
let id := 0 in
match ZMap.get id (lock adt) with
| LockOwn true =>
Some adt {core_data: (core_data adt) {next_vmid: vmid}}
| _ => None
end.
Definition get_next_remap_ptr_spec (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
let id := 0 in
match ZMap.get id (lock adt) with
| LockOwn true =>
Some (VZ64 (next_remap_ptr (core_data adt)))
| _ => None
end.
Definition set_next_remap_ptr_spec (remap: Z64) (adt: RData) : option RData :=
if halt adt then Some adt else
let id := 0 in
match remap with
| VZ64 remap =>
match ZMap.get id (lock adt) with
| LockOwn true =>
Some adt {core_data: (core_data adt) {next_remap_ptr: remap}}
| _ => None
end
end.
Definition get_shadow_ctxt_spec (vmid: Z) (vcpuid: Z) (index: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
rely is_vm vmid; rely is_vcpu vcpuid; rely is_reg index;
let ctxt := (ctxt_id vmid vcpuid) @ (shadow_ctxts adt) in
if index =? X0 then Some (VZ64 (x0 (ctxt_regs ctxt))) else
if index =? X1 then Some (VZ64 (x1 (ctxt_regs ctxt))) else
if index =? X2 then Some (VZ64 (x2 (ctxt_regs ctxt))) else
if index =? X3 then Some (VZ64 (x3 (ctxt_regs ctxt))) else
if index =? X4 then Some (VZ64 (x4 (ctxt_regs ctxt))) else
if index =? X5 then Some (VZ64 (x5 (ctxt_regs ctxt))) else
if index =? X6 then Some (VZ64 (x6 (ctxt_regs ctxt))) else
if index =? X7 then Some (VZ64 (x7 (ctxt_regs ctxt))) else
if index =? X8 then Some (VZ64 (x8 (ctxt_regs ctxt))) else
if index =? X9 then Some (VZ64 (x9 (ctxt_regs ctxt))) else
if index =? X10 then Some (VZ64 (x10 (ctxt_regs ctxt))) else
if index =? X11 then Some (VZ64 (x11 (ctxt_regs ctxt))) else
if index =? X12 then Some (VZ64 (x12 (ctxt_regs ctxt))) else
if index =? X13 then Some (VZ64 (x13 (ctxt_regs ctxt))) else
if index =? X14 then Some (VZ64 (x14 (ctxt_regs ctxt))) else
if index =? X15 then Some (VZ64 (x15 (ctxt_regs ctxt))) else
if index =? X16 then Some (VZ64 (x16 (ctxt_regs ctxt))) else
if index =? X17 then Some (VZ64 (x17 (ctxt_regs ctxt))) else
if index =? X18 then Some (VZ64 (x18 (ctxt_regs ctxt))) else
if index =? X19 then Some (VZ64 (x19 (ctxt_regs ctxt))) else
if index =? X20 then Some (VZ64 (x20 (ctxt_regs ctxt))) else
if index =? X21 then Some (VZ64 (x21 (ctxt_regs ctxt))) else
if index =? X22 then Some (VZ64 (x22 (ctxt_regs ctxt))) else
if index =? X23 then Some (VZ64 (x23 (ctxt_regs ctxt))) else
if index =? X24 then Some (VZ64 (x24 (ctxt_regs ctxt))) else
if index =? X25 then Some (VZ64 (x25 (ctxt_regs ctxt))) else
if index =? X26 then Some (VZ64 (x26 (ctxt_regs ctxt))) else
if index =? X27 then Some (VZ64 (x27 (ctxt_regs ctxt))) else
if index =? X28 then Some (VZ64 (x28 (ctxt_regs ctxt))) else
if index =? X29 then Some (VZ64 (x29 (ctxt_regs ctxt))) else
if index =? X30 then Some (VZ64 (x30 (ctxt_regs ctxt))) else
if index =? PC then Some (VZ64 (pc (ctxt_states ctxt))) else
if index =? PSTATE then Some (VZ64 (pstate (ctxt_states ctxt))) else
if index =? ELR_EL1 then Some (VZ64 (elr_el1 (ctxt_regs ctxt))) else
if index =? SPSR_EL1 then Some (VZ64 (spsr_el1 (ctxt_regs ctxt))) else
if index =? FAR_EL2 then Some (VZ64 (far_el2 (ctxt_regs ctxt))) else
if index =? HPFAR_EL2 then Some (VZ64 (hpfar_el2 (ctxt_regs ctxt))) else
if index =? HCR_EL2 then Some (VZ64 (hcr_el2 (ctxt_regs ctxt))) else
if index =? EC then Some (VZ64 (ec (ctxt_regs ctxt))) else
if index =? DIRTY then Some (VZ64 (dirty (ctxt_states ctxt))) else
if index =? FLAGS then Some (VZ64 (flags (ctxt_states ctxt))) else
if index =? MPIDR_EL1 then Some (VZ64 (mpidr_el1 (ctxt_regs ctxt))) else
if index =? CSSELR_EL1 then Some (VZ64 (csselr_el1 (ctxt_regs ctxt))) else
if index =? SCTLR_EL1 then Some (VZ64 (sctlr_el1 (ctxt_regs ctxt))) else
if index =? ACTLR_EL1 then Some (VZ64 (actlr_el1 (ctxt_regs ctxt))) else
if index =? CPACR_EL1 then Some (VZ64 (cpacr_el1 (ctxt_regs ctxt))) else
if index =? TTBR0_EL1 then Some (VZ64 (ttbr0_el1 (ctxt_regs ctxt))) else
if index =? TTBR1_EL1 then Some (VZ64 (ttbr1_el1 (ctxt_regs ctxt))) else
if index =? TCR_EL1 then Some (VZ64 (tcr_el1 (ctxt_regs ctxt))) else
if index =? ESR_EL1 then Some (VZ64 (esr_el1 (ctxt_states ctxt))) else
if index =? AFSR0_EL1 then Some (VZ64 (afsr0_el1 (ctxt_regs ctxt))) else
if index =? AFSR1_EL1 then Some (VZ64 (afsr1_el1 (ctxt_regs ctxt))) else
if index =? FAR_EL1 then Some (VZ64 (far_el1 (ctxt_regs ctxt))) else
if index =? MAIR_EL1 then Some (VZ64 (mair_el1 (ctxt_regs ctxt))) else
if index =? VBAR_EL1 then Some (VZ64 (vbar_el1 (ctxt_regs ctxt))) else
if index =? CONTEXTIDR_EL1 then Some (VZ64 (contextidr_el1 (ctxt_regs ctxt))) else
if index =? TPIDR_EL0 then Some (VZ64 (tpidr_el0 (ctxt_regs ctxt))) else
if index =? TPIDRRO_EL0 then Some (VZ64 (tpidrro_el0 (ctxt_regs ctxt))) else
if index =? TPIDR_EL1 then Some (VZ64 (tpidr_el1 (ctxt_regs ctxt))) else
if index =? AMAIR_EL1 then Some (VZ64 (amair_el1 (ctxt_regs ctxt))) else
if index =? CNTKCTL_EL1 then Some (VZ64 (cntkctl_el1 (ctxt_regs ctxt))) else
if index =? PAR_EL1 then Some (VZ64 (par_el1 (ctxt_regs ctxt))) else
if index =? MDSCR_EL1 then Some (VZ64 (mdscr_el1 (ctxt_regs ctxt))) else
if index =? MDCCINT_EL1 then Some (VZ64 0) else
if index =? ELR_EL2 then Some (VZ64 (elr_el2 (ctxt_regs ctxt))) else
if index =? SPSR_0 then Some (VZ64 (spsr_0 (ctxt_states ctxt))) else
if index =? ESR_EL2 then Some (VZ64 (esr_el2 (ctxt_regs ctxt))) else
None.
Definition set_shadow_ctxt_spec (vmid: Z) (vcpuid: Z) (index: Z) (value: Z64) (adt: RData) : option RData :=
if halt adt then Some adt else
rely is_vm vmid; rely is_vcpu vcpuid; rely is_reg index;
match value with
| VZ64 val =>
let ctxtid := ctxt_id vmid vcpuid in
let ctxt := ctxtid @ (shadow_ctxts adt) in
let cregs := ctxt_regs ctxt in
let cstats := ctxt_states ctxt in
if index =? X0 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x0: val}})} else
if index =? X1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x1: val}})} else
if index =? X2 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x2: val}})} else
if index =? X3 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x3: val}})} else
if index =? X4 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x4: val}})} else
if index =? X5 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x5: val}})} else
if index =? X6 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x6: val}})} else
if index =? X7 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x7: val}})} else
if index =? X8 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x8: val}})} else
if index =? X9 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x9: val}})} else
if index =? X10 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x10: val}})} else
if index =? X11 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x11: val}})} else
if index =? X12 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x12: val}})} else
if index =? X13 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x13: val}})} else
if index =? X14 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x14: val}})} else
if index =? X15 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x15: val}})} else
if index =? X16 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x16: val}})} else
if index =? X17 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x17: val}})} else
if index =? X18 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x18: val}})} else
if index =? X19 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x19: val}})} else
if index =? X20 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x20: val}})} else
if index =? X21 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x21: val}})} else
if index =? X22 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x22: val}})} else
if index =? X23 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x23: val}})} else
if index =? X24 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x24: val}})} else
if index =? X25 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x25: val}})} else
if index =? X26 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x26: val}})} else
if index =? X27 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x27: val}})} else
if index =? X28 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x28: val}})} else
if index =? X29 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x29: val}})} else
if index =? X30 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {x30: val}})} else
if index =? PC then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_states: cstats {pc: val}})} else
if index =? PSTATE then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_states: cstats {pstate: val}})} else
if index =? ELR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {elr_el1: val}})} else
if index =? SPSR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {spsr_el1: val}})} else
if index =? FAR_EL2 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {far_el2: val}})} else
if index =? HPFAR_EL2 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {hpfar_el2: val}})} else
if index =? HCR_EL2 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {hcr_el2: val}})} else
if index =? EC then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {ec: val}})} else
if index =? DIRTY then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_states: cstats {dirty: val}})} else
if index =? FLAGS then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_states: cstats {flags: val}})} else
if index =? MPIDR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {mpidr_el1: val}})} else
if index =? CSSELR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {csselr_el1: val}})} else
if index =? SCTLR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {sctlr_el1: val}})} else
if index =? ACTLR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {actlr_el1: val}})} else
if index =? CPACR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {cpacr_el1: val}})} else
if index =? TTBR0_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {ttbr0_el1: val}})} else
if index =? TTBR1_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {ttbr1_el1: val}})} else
if index =? TCR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {tcr_el1: val}})} else
if index =? ESR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_states: cstats {esr_el1: val}})} else
if index =? AFSR0_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {afsr0_el1: val}})} else
if index =? AFSR1_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {afsr1_el1: val}})} else
if index =? FAR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {far_el1: val}})} else
if index =? MAIR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {mair_el1: val}})} else
if index =? VBAR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {vbar_el1: val}})} else
if index =? CONTEXTIDR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {contextidr_el1: val}})} else
if index =? TPIDR_EL0 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {tpidr_el0: val}})} else
if index =? TPIDRRO_EL0 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {tpidrro_el0: val}})} else
if index =? TPIDR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {tpidr_el1: val}})} else
if index =? AMAIR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {amair_el1: val}})} else
if index =? CNTKCTL_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {cntkctl_el1: val}})} else
if index =? PAR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {par_el1: val}})} else
if index =? MDSCR_EL1 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {mdscr_el1: val}})} else
if index =? MDCCINT_EL1 then Some adt else
if index =? ELR_EL2 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {elr_el2: val}})} else
if index =? SPSR_0 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_states: cstats {spsr_0: val}})} else
if index =? ESR_EL2 then Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cregs {esr_el2: val}})} else
None
end.
Definition get_shadow_esr_spec (vmid: Z) (vcpuid: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
rely is_vm vmid; rely is_vcpu vcpuid;
let ctxtid := ctxt_id vmid vcpuid in
let ctxt := ctxtid @ (shadow_ctxts adt) in
Some (VZ64 (esr_el2 (ctxt_regs ctxt))).
Definition get_int_esr_spec (vmid: Z) (vcpuid: Z) (adt: RData) : option (RData * Z64) :=
if halt adt then Some (adt, VZ64 0)
else rely is_vm vmid; rely is_vcpu vcpuid;
match query_data_oracle (cur_vmid adt) adt with
| (adt', val) => Some (adt', VZ64 val)
end.
Definition get_int_gpr_spec (vmid: Z) (vcpuid: Z) (index: Z) (adt: RData) : option (RData * Z64) :=
if halt adt then Some (adt, VZ64 0)
else rely is_vm vmid; rely is_vcpu vcpuid; rely is_reg index;
match query_data_oracle (cur_vmid adt) adt with
| (adt', val) => Some (adt', VZ64 val)
end.
Definition get_int_pc_spec (vmid: Z) (vcpuid: Z) (adt: RData) : option (RData * Z64) :=
if halt adt then Some (adt, VZ64 0)
else rely is_vm vmid; rely is_vcpu vcpuid;
match query_data_oracle (cur_vmid adt) adt with
| (adt', val) => Some (adt', VZ64 val)
end.
Definition get_int_pstate_spec (vmid: Z) (vcpuid: Z) (adt: RData) : option (RData * Z64) :=
if halt adt then Some (adt, VZ64 0)
else rely is_vm vmid; rely is_vcpu vcpuid;
match query_data_oracle (cur_vmid adt) adt with
| (adt', val) => Some (adt', VZ64 val)
end.
Definition set_int_gpr_spec (vmid: Z) (vcpuid: Z) (index: Z) (value: Z64) (adt: RData) : option RData :=
rely is_vm vmid; rely is_vcpu vcpuid; rely is_reg index;
Some adt.
Definition clear_shadow_gp_regs_spec (vmid: Z) (vcpuid: Z) (adt: RData) : option RData :=
if halt adt then Some adt
else rely is_vm vmid; rely is_vcpu vcpuid;
let ctxtid := ctxt_id vmid vcpuid in
let ctxt := ctxtid @ (shadow_ctxts adt) in
let cr := (ctxt_regs ctxt) {x0: 0} {x1: 0} {x2: 0} {x3: 0}
{x4: 0} {x5: 0} {x6: 0} {x7: 0}
{x8: 0} {x9: 0} {x10: 0} {x11: 0}
{x12: 0} {x13: 0} {x14: 0} {x15: 0}
{x16: 0} {x17: 0} {x18: 0} {x19: 0}
{x20: 0} {x21: 0} {x22: 0} {x23: 0}
{x24: 0} {x25: 0} {x26: 0} {x27: 0}
{x28: 0} {x29: 0} {x30: 0}
in
Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cr})}.
Definition reset_fp_regs_spec (vmid: Z) (vcpuid: Z) (adt: RData) : option RData :=
if halt adt then Some adt
else rely is_vm vmid; rely is_vcpu vcpuid;
let ctxtid := ctxt_id vmid vcpuid in
let ctxt := ctxtid @ (shadow_ctxts adt) in
let cr := (ctxt_regs ctxt) {fp_q0: 0} {fp_q1: 0} {fp_q2: 0} {fp_q3: 0}
{fp_q4: 0} {fp_q5: 0} {fp_q6: 0} {fp_q7: 0}
{fp_q8: 0} {fp_q9: 0} {fp_q10: 0} {fp_q11: 0}
{fp_q12: 0} {fp_q13: 0} {fp_q14: 0} {fp_q15: 0}
{fp_q16: 0} {fp_q17: 0} {fp_q18: 0} {fp_q19: 0}
{fp_q20: 0} {fp_q21: 0} {fp_q22: 0} {fp_q23: 0}
{fp_q24: 0} {fp_q25: 0} {fp_q26: 0} {fp_q27: 0}
{fp_q28: 0} {fp_q29: 0} {fp_q30: 0}
{fp_q31: 0} {fp_fpsr: 0} {fp_fpcr: 0}
in
Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_regs: cr})}.
Definition get_shadow_dirty_bit_spec (vmid: Z) (vcpuid: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
rely is_vm vmid; rely is_vcpu vcpuid;
let ctxtid := ctxt_id vmid vcpuid in
let ctxt := ctxtid @ (shadow_ctxts adt) in
Some (VZ64 (dirty (ctxt_states ctxt))).
Definition set_shadow_dirty_bit_spec (vmid: Z) (vcpuid: Z) (value: Z64) (adt: RData) : option RData :=
match value with
| VZ64 val =>
if halt adt then Some adt else
rely is_vm vmid; rely is_vcpu vcpuid;
let ctxtid := ctxt_id vmid vcpuid in
let ctxt := ctxtid @ (shadow_ctxts adt) in
Some adt {shadow_ctxts: (shadow_ctxts adt) # ctxtid == (ctxt {ctxt_states: (ctxt_states ctxt) {dirty: val}})}
end.
Definition get_int_new_pte_spec (vmid: Z) (vcpuid: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0)
else Some (VZ64 (int_pte adt)).
Definition get_int_new_level_spec (vmid: Z) (vcpuid: Z) (adt: RData) : option Z :=
if halt adt then Some 0
else Some (int_level adt).
Definition get_cur_vmid_spec (adt: RData) : option Z :=
if halt adt then Some 0
else Some (cur_vmid adt).
Definition get_cur_vcpu_id_spec (adt: RData) : option Z :=
if halt adt then Some 0
else Some (cur_vcpuid adt).
Definition clear_phys_page_spec (pfn: Z64) (adt: RData) : option RData :=
match pfn with
| VZ64 pfn =>
if halt adt then Some adt else
rely is_flatmem pfn;
Some adt {flatmem: ZMap.set pfn 0 (flatmem adt)}
end.
Definition set_per_cpu_spec (vmid: Z) (vcpu_id: Z) (adt: RData) : option RData :=
match is_vm vmid, is_vcpu vcpu_id with
| true, true =>
if halt adt then Some adt else
if vmid =? HOSTVISOR then
Some adt {cur_vmid: HOSTVISOR} {cur_vcpuid: curid adt}
else if vmid =? COREVISOR then
Some adt {cur_vmid: COREVISOR} {cur_vcpuid: curid adt}
else Some adt {cur_vmid: vmid} {cur_vcpuid: vcpu_id}
| _, _ => None
end.
Definition get_int_run_vcpuid_spec (vmid: Z) (adt: RData) : option (RData * Z) :=
match is_vm vmid with
| true =>
if halt adt then Some (adt, 0) else
match query_data_oracle vmid adt with
| (adt', val) =>
Some (adt', val)
end
| _ => None
end.
Definition host_to_core_spec (adt: RData) : option RData :=
match ihost adt, icore adt with
| true, false =>
if halt adt then Some adt else
let adt1 := adt {ihost: false} {icore: true} in
match ZMap.get (host_ctxt + curid adt) (shadow_ctxts adt), regs adt with
| ctxt, regc =>
let gp := ctxt_regs ctxt in
let rgp := ctxt_regs regc in
let gp' := gp {x0: (x0 rgp)} {x1: (x1 rgp)} {x2: (x2 rgp)} {x3: (x3 rgp)}
{x4: (x4 rgp)} {x5: (x5 rgp)} {x6: (x6 rgp)} {x7: (x7 rgp)}
{x8: (x8 rgp)} {x9: (x9 rgp)} {x10: (x10 rgp)} {x11: (x11 rgp)}
{x12: (x12 rgp)} {x13: (x13 rgp)} {x14: (x14 rgp)} {x15: (x15 rgp)}
{x16: (x16 rgp)} {x17: (x17 rgp)} {x18: (x18 rgp)} {x19: (x19 rgp)}
{x20: (x20 rgp)} {x21: (x21 rgp)} {x22: (x22 rgp)} {x23: (x23 rgp)}
{x24: (x24 rgp)} {x25: (x25 rgp)} {x26: (x26 rgp)} {x27: (x27 rgp)}
{x28: (x28 rgp)} {x29: (x29 rgp)} {x30: (x30 rgp)}
in
Some (adt {shadow_ctxts: (shadow_ctxts adt) # (host_ctxt + curid adt) == (ctxt {ctxt_regs: gp'})})
end
| _, _ => None
end.
Definition vm_to_core_spec (adt: RData) : option RData :=
match ihost adt, icore adt with
| false, false =>
if halt adt then Some adt else
let adt1 := adt {icore: true} in
let vmid := cur_vmid adt in
let vcpuid := cur_vcpuid adt in
match ZMap.get (ctxt_id vmid vcpuid) (shadow_ctxts adt), regs adt with
| ctxt, regc =>
let gp := ctxt_regs ctxt in
let rgp := ctxt_regs regc in
let gp' := gp {x0: (x0 rgp)} {x1: (x1 rgp)} {x2: (x2 rgp)} {x3: (x3 rgp)}
{x4: (x4 rgp)} {x5: (x5 rgp)} {x6: (x6 rgp)} {x7: (x7 rgp)}
{x8: (x8 rgp)} {x9: (x9 rgp)} {x10: (x10 rgp)} {x11: (x11 rgp)}
{x12: (x12 rgp)} {x13: (x13 rgp)} {x14: (x14 rgp)} {x15: (x15 rgp)}
{x16: (x16 rgp)} {x17: (x17 rgp)} {x18: (x18 rgp)} {x19: (x19 rgp)}
{x20: (x20 rgp)} {x21: (x21 rgp)} {x22: (x22 rgp)} {x23: (x23 rgp)}
{x24: (x24 rgp)} {x25: (x25 rgp)} {x26: (x26 rgp)} {x27: (x27 rgp)}
{x28: (x28 rgp)} {x29: (x29 rgp)} {x30: (x30 rgp)}
in
Some adt {shadow_ctxts: (shadow_ctxts adt) # (ctxt_id vmid vcpuid) == (ctxt {ctxt_regs: gp'})}
end
| _, _ => None
end.
Definition core_to_host_spec (adt: RData) : option RData :=
match ihost adt, icore adt with
| false, true =>
if halt adt then Some adt else
match ZMap.get (host_ctxt + curid adt) (shadow_ctxts adt), regs adt with
| ctxt, regc =>
let rgp := ctxt_regs ctxt in
let gp := ctxt_regs regc in
let gp' := gp {x0: (x0 rgp)} {x1: (x1 rgp)} {x2: (x2 rgp)} {x3: (x3 rgp)}
{x4: (x4 rgp)} {x5: (x5 rgp)} {x6: (x6 rgp)} {x7: (x7 rgp)}
{x8: (x8 rgp)} {x9: (x9 rgp)} {x10: (x10 rgp)} {x11: (x11 rgp)}
{x12: (x12 rgp)} {x13: (x13 rgp)} {x14: (x14 rgp)} {x15: (x15 rgp)}
{x16: (x16 rgp)} {x17: (x17 rgp)} {x18: (x18 rgp)} {x19: (x19 rgp)}
{x20: (x20 rgp)} {x21: (x21 rgp)} {x22: (x22 rgp)} {x23: (x23 rgp)}
{x24: (x24 rgp)} {x25: (x25 rgp)} {x26: (x26 rgp)} {x27: (x27 rgp)}
{x28: (x28 rgp)} {x29: (x29 rgp)} {x30: (x30 rgp)}
in
Some adt {ihost: true} {icore: false} {regs: regc {ctxt_regs: gp'}}
end
| _, _ => None
end.
Definition core_to_vm_spec (adt: RData) : option RData :=
match ihost adt, icore adt with
| false, true =>
if halt adt then Some adt else
let vmid := cur_vmid adt in
let vcpuid := cur_vcpuid adt in
match ZMap.get (ctxt_id vmid vcpuid) (shadow_ctxts adt), regs adt with
| ctxt, regc =>
let rgp := ctxt_regs ctxt in
let gp := ctxt_regs regc in
let gp' := gp {x0: (x0 rgp)} {x1: (x1 rgp)} {x2: (x2 rgp)} {x3: (x3 rgp)}
{x4: (x4 rgp)} {x5: (x5 rgp)} {x6: (x6 rgp)} {x7: (x7 rgp)}
{x8: (x8 rgp)} {x9: (x9 rgp)} {x10: (x10 rgp)} {x11: (x11 rgp)}
{x12: (x12 rgp)} {x13: (x13 rgp)} {x14: (x14 rgp)} {x15: (x15 rgp)}
{x16: (x16 rgp)} {x17: (x17 rgp)} {x18: (x18 rgp)} {x19: (x19 rgp)}
{x20: (x20 rgp)} {x21: (x21 rgp)} {x22: (x22 rgp)} {x23: (x23 rgp)}
{x24: (x24 rgp)} {x25: (x25 rgp)} {x26: (x26 rgp)} {x27: (x27 rgp)}
{x28: (x28 rgp)} {x29: (x29 rgp)} {x30: (x30 rgp)}
in
Some adt {regs: regc {ctxt_regs: gp'}}
end
| _, _ => None
end.
Definition exit_populate_fault_spec (adt: RData) : option RData :=
if halt adt then Some adt else
let vmid := cur_vmid adt in
let vcpuid := cur_vcpuid adt in
match ZMap.get (ctxt_id vmid vcpuid) (shadow_ctxts adt), regs adt with
| ctxt, regc =>
let ctxt' := ctxt {ctxt_regs: (ctxt_regs ctxt) {esr_el2: esr_el2 (ctxt_regs regc)}
{ec: ec (ctxt_regs regc)}
{far_el2: far_el2 (ctxt_regs regc)}
{hpfar_el2: hpfar_el2 (ctxt_regs regc)}}
in
Some (adt {shadow_ctxts: ZMap.set (ctxt_id vmid vcpuid) ctxt' (shadow_ctxts adt)})
end.
Definition save_sysregs_spec (adt: RData) : option RData :=
if halt adt then Some adt else
let vmid := cur_vmid adt in
let vcpuid := cur_vcpuid adt in
match ZMap.get (ctxt_id vmid vcpuid) (shadow_ctxts adt), regs adt with
| ctxt, regc =>
let sys := ctxt_regs ctxt in
let rsys := ctxt_regs regc in
let sys' := sys
{csselr_el1: (csselr_el1 rsys)} {sctlr_el1: (sctlr_el1 rsys)}
{cpacr_el1: (cpacr_el1 rsys)} {ttbr0_el1: (ttbr0_el1 rsys)}
{ttbr1_el1: (ttbr1_el1 rsys)} {tcr_el1: (tcr_el1 rsys)}
{afsr0_el1: (afsr0_el1 rsys)} {afsr1_el1: (afsr1_el1 rsys)}
{far_el1: (far_el1 rsys)} {mair_el1: (mair_el1 rsys)}
{vbar_el1: (vbar_el1 rsys)} {contextidr_el1: (contextidr_el1 rsys)}
{amair_el1: (amair_el1 rsys)} {cntkctl_el1: (cntkctl_el1 rsys)}
{par_el1: (par_el1 rsys)} {tpidr_el1: (tpidr_el1 rsys)}
{spsr_el1: (spsr_el1 rsys)} {mdscr_el1: (mdscr_el1 rsys)}
{sp_el0: (sp_el0 rsys)} {tpidr_el0: (tpidr_el0 rsys)}
{tpidrro_el0: (tpidrro_el0 rsys)}
{mpidr_el1: (vmpidr_el2 rsys)} {actlr_el1: (actlr_el1 rsys)}
{sp_el1: (sp_el1 rsys)} {elr_el1: (elr_el1 rsys)}
in
let state' := (ctxt_states ctxt) {pstate: (spsr_el2 rsys)} in
Some (adt {shadow_ctxts: ZMap.set (ctxt_id vmid vcpuid) (ctxt {ctxt_regs: sys'} {ctxt_states: state'}) (shadow_ctxts adt)})
end.
Definition restore_sysregs_spec (adt: RData) : option RData :=
if halt adt then Some adt else
let vmid := cur_vmid adt in
let vcpuid := cur_vcpuid adt in
match ZMap.get (ctxt_id vmid vcpuid) (shadow_ctxts adt), regs adt with
| ctxt, regc =>
let sys := ctxt_regs regc in
let rsys := ctxt_regs ctxt in
let sys' := sys
{csselr_el1: (csselr_el1 rsys)} {sctlr_el1: (sctlr_el1 rsys)}
{cpacr_el1: (cpacr_el1 rsys)} {ttbr0_el1: (ttbr0_el1 rsys)}
{ttbr1_el1: (ttbr1_el1 rsys)} {tcr_el1: (tcr_el1 rsys)}
{afsr0_el1: (afsr0_el1 rsys)} {afsr1_el1: (afsr1_el1 rsys)}
{far_el1: (far_el1 rsys)} {mair_el1: (mair_el1 rsys)}
{vbar_el1: (vbar_el1 rsys)} {contextidr_el1: (contextidr_el1 rsys)}
{amair_el1: (amair_el1 rsys)} {cntkctl_el1: (cntkctl_el1 rsys)}
{par_el1: (par_el1 rsys)} {tpidr_el1: (tpidr_el1 rsys)}
{spsr_el1: (spsr_el1 rsys)} {mdscr_el1: (mdscr_el1 rsys)}
{sp_el0: (sp_el0 rsys)} {tpidr_el0: (tpidr_el0 rsys)}
{tpidrro_el0: (tpidrro_el0 rsys)} {spsr_el2: (pstate (ctxt_states ctxt))}
{vmpidr_el2: (mpidr_el1 rsys)} {mpidr_el1: (mpidr_el1 rsys)}
{actlr_el1: (actlr_el1 rsys)} {sp_el1: (sp_el1 rsys)}
{elr_el2: (pc (ctxt_states ctxt))} {elr_el1: (elr_el1 rsys)}
{esr_el2: (esr_el2 rsys)} {ec: (ec rsys)}
{far_el2: (far_el2 rsys)} {hpfar_el2: (hpfar_el2 rsys)}
in
Some (adt {regs: regc {ctxt_regs: sys'}})
end.
Definition fpsimd_save_state_spec (adt: RData) : option RData :=
if halt adt then Some adt else
let vmid := cur_vmid adt in
let vcpuid := cur_vcpuid adt in
match ZMap.get (ctxt_id vmid vcpuid) (shadow_ctxts adt), regs adt with
| ctxt, regc =>
let gp := ctxt_regs ctxt in
let rgp := ctxt_regs regc in
let gp' := gp {fp_q0: (fp_q0 rgp)} {fp_q1: (fp_q1 rgp)} {fp_q2: (fp_q2 rgp)}
{fp_q3: (fp_q3 rgp)} {fp_q4: (fp_q4 rgp)} {fp_q5: (fp_q5 rgp)}
{fp_q6: (fp_q6 rgp)} {fp_q7: (fp_q7 rgp)} {fp_q8: (fp_q8 rgp)}
{fp_q9: (fp_q9 rgp)} {fp_q10: (fp_q10 rgp)} {fp_q11: (fp_q11 rgp)}
{fp_q12: (fp_q12 rgp)} {fp_q13: (fp_q13 rgp)} {fp_q14: (fp_q14 rgp)}
{fp_q15: (fp_q15 rgp)} {fp_q16: (fp_q16 rgp)} {fp_q17: (fp_q17 rgp)}
{fp_q18: (fp_q18 rgp)} {fp_q19: (fp_q19 rgp)} {fp_q20: (fp_q20 rgp)}
{fp_q21: (fp_q21 rgp)} {fp_q22: (fp_q22 rgp)} {fp_q23: (fp_q23 rgp)}
{fp_q24: (fp_q24 rgp)} {fp_q25: (fp_q25 rgp)} {fp_q26: (fp_q26 rgp)}
{fp_q27: (fp_q27 rgp)} {fp_q28: (fp_q28 rgp)} {fp_q29: (fp_q29 rgp)}
{fp_q30: (fp_q30 rgp)} {fp_q31: (fp_q31 rgp)} {fp_fpsr: (fp_fpsr rgp)}
{fp_fpcr: (fp_fpcr rgp)}
in
Some (adt {shadow_ctxts: ZMap.set (ctxt_id vmid vcpuid) (ctxt {ctxt_regs: gp'}) (shadow_ctxts adt)})
end.
Definition fpsimd_restore_state_spec (adt: RData) : option RData :=
if halt adt then Some adt else
let vmid := cur_vmid adt in
let vcpuid := cur_vcpuid adt in
match ZMap.get (ctxt_id vmid vcpuid) (shadow_ctxts adt), regs adt with
| ctxt, regc =>
let gp := ctxt_regs regc in
let rgp := ctxt_regs ctxt in
let gp' := gp {fp_q0: (fp_q0 rgp)} {fp_q1: (fp_q1 rgp)} {fp_q2: (fp_q2 rgp)}
{fp_q3: (fp_q3 rgp)} {fp_q4: (fp_q4 rgp)} {fp_q5: (fp_q5 rgp)}
{fp_q6: (fp_q6 rgp)} {fp_q7: (fp_q7 rgp)} {fp_q8: (fp_q8 rgp)}
{fp_q9: (fp_q9 rgp)} {fp_q10: (fp_q10 rgp)} {fp_q11: (fp_q11 rgp)}
{fp_q12: (fp_q12 rgp)} {fp_q13: (fp_q13 rgp)} {fp_q14: (fp_q14 rgp)}
{fp_q15: (fp_q15 rgp)} {fp_q16: (fp_q16 rgp)} {fp_q17: (fp_q17 rgp)}
{fp_q18: (fp_q18 rgp)} {fp_q19: (fp_q19 rgp)} {fp_q20: (fp_q20 rgp)}
{fp_q21: (fp_q21 rgp)} {fp_q22: (fp_q22 rgp)} {fp_q23: (fp_q23 rgp)}
{fp_q24: (fp_q24 rgp)} {fp_q25: (fp_q25 rgp)} {fp_q26: (fp_q26 rgp)}
{fp_q27: (fp_q27 rgp)} {fp_q28: (fp_q28 rgp)} {fp_q29: (fp_q29 rgp)}
{fp_q30: (fp_q30 rgp)} {fp_q31: (fp_q31 rgp)} {fp_fpsr: (fp_fpsr rgp)}
{fp_fpcr: (fp_fpcr rgp)}
in
Some (adt {regs: regc {ctxt_regs: gp'}})
end.
Definition activate_traps_spec (adt: RData) : option RData :=
if halt adt then Some adt else
Some (adt {regs: (regs adt) {trap_regs: (trap_regs (regs adt)) {pmuselr_el0: 0} {pmuserenr_el0: ARMV8_PMU_USERENR_MASK}
{mdcr_el2: HYPSEC_MDCR_EL2_FLAG} {cptr_el2: CPTR_VM}}}).
Definition deactivate_traps_spec (adt: RData) : option RData :=
if halt adt then Some adt else
Some (adt {regs: (regs adt) {trap_regs: (trap_regs (regs adt)) {pmuserenr_el0: 0} {mdcr_el2: 0}
{cptr_el2: CPTR_EL2_DEFAULT }}}).
Definition timer_enable_traps_spec (adt: RData) : option RData :=
if halt adt then Some adt else
let v' := (cnthctl_el2 (trap_regs (regs adt))) - CNTHCTL_EL1PCEN + CNTHCTL_EL1PCTEN in
Some (adt {regs: (regs adt) {trap_regs: (trap_regs (regs adt)) {cnthctl_el2: v'}}}).
Definition core_handle_sys64_spec (adt: RData) : option RData :=
if halt adt then Some adt else
let pc := (elr_el2 (ctxt_regs (regs adt))) in
Some (adt {regs: (regs adt) {ctxt_regs: (ctxt_regs (regs adt)) {esr_el2: pc + 4}}}).
Definition timer_set_cntvoff_spec (adt: RData) : option RData :=
Some adt.
Definition vm_el2_restore_state_spec (adt: RData) : option RData :=
if halt adt then Some adt else
let vmid := cur_vmid adt in
let vcpuid := cur_vcpuid adt in
let ctxt := (ctxt_id vmid vcpuid) @ (shadow_ctxts adt) in
let vttbr := pt_vttbr (vmid @ (npts adt)) in
Some (adt {regs: (regs adt) {ctxt_regs: (ctxt_regs (regs adt)) {vttbr_el2: vttbr} {tpidr_el2: (tpidr_el2 (ctxt_regs ctxt))}
{hcr_el2: HCR_HYPSEC_VM_FLAGS}}}).
Definition host_el2_restore_state_spec (adt: RData) : option RData :=
if halt adt then Some adt else
let vttbr := (pt_vttbr (HOSTVISOR @ (npts adt))) in
Some (adt {regs: (regs adt) {ctxt_regs: (ctxt_regs (regs adt)) {vttbr_el2: vttbr} {hcr_el2: HCR_HOST_NVHE_FLAGS} {tpidr_el2: 0}}}).
Definition get_smmu_cfg_vmid_spec (cbndx: Z) (num: Z) (adt: RData) : option Z :=
if halt adt then Some 0 else
let smmu_dev := (num) @ (smmu_devices adt) in
let smmu_vmids := (smmu_vmid smmu_dev) in
Some (ZMap.get cbndx smmu_vmids).
Definition set_smmu_cfg_vmid_spec (cbndx: Z) (num: Z) (vmid: Z) (adt: RData) : option RData :=
if halt adt then Some adt else
let smmu_dev := (num) @ (smmu_devices adt) in
let smmu_vmids := (smmu_vmid smmu_dev) in
Some adt {smmu_devices: (smmu_devices adt) # num == (smmu_dev {smmu_vmid: ZMap.set cbndx vmid smmu_vmids})}.
Definition get_smmu_cfg_ttbr_spec (cbndx: Z) (num: Z) (adt: RData) : option Z :=
if halt adt then Some 0 else
let smmu_dev := (num) @ (smmu_devices adt) in
let smmu_ttbrs := (smmu_ttbr smmu_dev) in
Some (ZMap.get cbndx smmu_ttbrs).
Definition set_smmu_cfg_ttbr_spec (cbndx: Z) (num: Z) (ttbr: Z) (adt: RData) : option RData :=
if halt adt then Some adt else
let smmu_dev := (num) @ (smmu_devices adt) in
let smmu_ttbrs := (smmu_ttbr smmu_dev) in
Some adt {smmu_devices: (smmu_devices adt) # num == (smmu_dev {smmu_ttbr: ZMap.set cbndx ttbr smmu_ttbrs})}.
Definition get_smmu_cfg_hw_ttbr_spec (cbndx: Z) (num: Z) (adt: RData) : option Z :=
if halt adt then Some 0 else
let smmu_dev := (num) @ (smmu_devices adt) in
let smmu_hw_ttbrs := (smmu_hw_ttbr smmu_dev) in
Some (ZMap.get cbndx smmu_hw_ttbrs).
Definition set_smmu_cfg_hw_ttbr_spec (cbndx: Z) (num: Z) (hw_ttbr: Z) (adt: RData) : option RData :=
if halt adt then Some adt else
let smmu_dev := (num) @ (smmu_devices adt) in
let smmu_hw_ttbrs := (smmu_hw_ttbr smmu_dev) in
Some adt {smmu_devices: (smmu_devices adt) # num == (smmu_dev {smmu_hw_ttbr: ZMap.set cbndx hw_ttbr smmu_hw_ttbrs})}.
Definition get_smmu_num_context_banks_spec (num: Z) (adt: RData) : option Z :=
if halt adt then Some 0 else
let smmu_dev := (num) @ (smmu_devices adt) in
Some (smmu_num_context_banks smmu_dev).
Definition get_smmu_pgshift_spec (num: Z) (adt: RData) : option Z :=
if halt adt then Some 0 else
let smmu_dev := (num) @ (smmu_devices adt) in
Some (smmu_pgshift smmu_dev).
Definition get_smmu_num_spec (adt: RData) : option Z :=
if halt adt then Some 0 else
Some (smmu_num adt).
Definition get_smmu_size_spec (num: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
let smmu_dev := (num) @ (smmu_devices adt) in
Some (smmu_size smmu_dev).
Definition get_smmu_base_spec (num: Z) (adt: RData) : option Z64 :=
if halt adt then Some (VZ64 0) else
let smmu_dev := (num) @ (smmu_devices adt) in
Some (smmu_phys_base smmu_dev).
Definition set_per_cpu_host_regs_spec (hr: Z) (adt: RData) : option RData :=
Some adt.
(* We can use set_shadow_ctxt_spec passing HOSTVISOR as vmid *)
Definition set_host_regs_spec (hr: Z) (value: Z64) (adt: RData) : option RData :=
Some adt.
(* We can use get_shadow_ctxt_spec passing HOSTVISOR as vmid *)
Definition get_host_regs_spec (hr: Z) (adt: RData) : option Z64 :=
Some (VZ64 0).
Definition readq_relaxed_spec (addr: Z64) (adt: RData) : option Z64 :=
Some (VZ64 0).
Definition writeq_relaxed_spec (value: Z64) (addr: Z64) (adt: RData) : option RData :=
Some adt.
Definition readl_relaxed_spec (addr: Z64) (adt: RData) : option Z :=
Some (0).
Definition writel_relaxed_spec (value: Z) (addr: Z64) (adt: RData) : option RData :=
Some adt.
Definition host_skip_instr_spec (adt: RData) : option RData :=
let pc := (elr_el2 (ctxt_regs (regs adt))) in
Some (adt {regs: (regs adt) {ctxt_regs: (ctxt_regs (regs adt)) {esr_el2: pc + 4}}}).
Definition host_get_fault_ipa_spec (addr: Z64) (adt: RData) : option Z64 :=
match addr with
| VZ64 addr =>
let far_el2 := (far_el2 (ctxt_regs (regs adt))) in
let far_el2' := Z.land far_el2 4095 in
let addr' := Z.lor addr far_el2' in
Some (VZ64 addr')
end.
End AbsMachineSpec.