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 SmmuRaw.Layer.
Require Import AbsMachine.Spec.
Require Import RData.
Require Import SmmuRaw.Spec.
Require Import Constants.
Require Import HypsecCommLib.
Local Open Scope Z_scope.
Section SmmuCoreAuxSpec.
Definition handle_smmu_global_access_spec (hsr: Z) (offset: Z64) (smmu_index: Z) (adt: RData) : option Z :=
match offset with
| VZ64 offset =>
rely is_int hsr;
if halt adt then Some 0 else
match SMMU_ID @ (lock adt) with
| LockOwn true =>
let vcpuid := cur_vcpuid adt in
rely is_vcpu vcpuid;
let rt := host_dabt_get_rd' hsr in
rely is_int rt;
when' data == get_shadow_ctxt_spec HOSTVISOR vcpuid rt adt;
rely is_int64 data;
if (offset >=? 0) && (offset <=? ARM_SMMU_GR1_BASE) then
if offset =? ARM_SMMU_GR0_sCR0 then
let smmu_enable := Z.land (Z.shiftr data sCR0_SMCFCFG_SHIFT) 1 in
if smmu_enable =? 0 then Some 0 else Some 1
else if offset =? ARM_SMMU_GR0_sCR2 then
if (Z.land data 255) =? 0 then Some 1 else Some 0
else Some 1
else if (offset >=? ARM_SMMU_GR1_BASE) && (offset <? ARM_SMMU_GR1_END) then
let n := (offset - ARM_SMMU_GR1_BASE) / 4 in
rely is_smmu smmu_index; rely is_smmu_cfg n;
let vmid := (smmu_id smmu_index n) @ (smmu_vmid (shared adt)) in
rely is_vmid vmid;
let type := Z.shiftr data CBAR_TYPE_SHIFT in
let t_vmid := Z.land data CBAR_VMID_MASK in
if vmid =? 0 then Some 1
else
if (type =? CBAR_TYPE_S2_TRANS) && (vmid =? t_vmid) then Some 1 else Some 0
else Some 1
| _ => None
end
end.
Definition handle_smmu_cb_access_spec (offset: Z64) (adt: RData) : option Z :=
match offset with
| VZ64 offset =>
rely (offset >=? SMMU_GLOBAL_BASE);
if halt adt then Some 0 else
let off' := offset - SMMU_GLOBAL_BASE in
let cb_offset := Z.land off' ARM_SMMU_PGSHIFT_MASK in
if cb_offset =? ARM_SMMU_CB_TTBR0 then Some 2
else if cb_offset =? ARM_SMMU_CB_CONTEXTIDR then Some 0 else Some 1
end.
Definition __handle_smmu_write_spec (hsr: Z) (fault_ipa: Z64) (len: Z) (val: Z64) (write_val: Z) (adt: RData) : option RData :=
match fault_ipa, val with
| VZ64 fault_ipa, VZ64 val =>
rely is_int hsr;
if halt adt then Some adt else
if len =? 8 then
if write_val =? 0 then
let vcpuid := cur_vcpuid adt in
rely is_vcpu vcpuid;
let rt := host_dabt_get_rd' hsr in
rely is_int rt;
when' data == get_shadow_ctxt_spec HOSTVISOR vcpuid rt adt;
rely is_int64 data;
Some adt
else
Some adt
else
if len =? 4 then
Some adt
else
Some adt {halt: true}
end.
Definition __handle_smmu_read_spec (hsr: Z) (fault_ipa: Z64) (len: Z) (adt: RData) : option RData :=
match fault_ipa with
| VZ64 fault_ipa =>
rely is_int hsr;
if halt adt then Some adt else
let vcpuid := cur_vcpuid adt in
rely is_vcpu vcpuid;
let rt := host_dabt_get_rd' hsr in
rely is_int rt;
let n := HOSTVISOR @ (data_log adt) in
let data := (doracle adt) HOSTVISOR n in
rely is_int64 data;
let dlog' := (data_log adt) # HOSTVISOR == (n + 1) in
if len =? 8 then
set_shadow_ctxt_spec HOSTVISOR vcpuid rt (VZ64 data) (adt {data_log: dlog'})
else if len =? 4 then
set_shadow_ctxt_spec HOSTVISOR vcpuid rt (VZ64 (Z.land data INVALID)) (adt {data_log: dlog'})
else
Some adt {halt: true}
end.
End SmmuCoreAuxSpec.
Section SmmuCoreAuxSpecLow.
Context `{real_params: RealParams}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := SmmuRaw_ops) LDATA).
Definition handle_smmu_global_access_spec0 (hsr: Z) (offset: Z64) (smmu_index: Z) (adt: RData) : option Z :=
match offset with
| VZ64 offset =>
when' data == host_get_mmio_data_spec hsr adt;
rely is_int64 data;
if (offset >=? 0) && (offset <=? ARM_SMMU_GR1_BASE) then
if offset =? ARM_SMMU_GR0_sCR0 then
let smmu_enable := Z.land (Z.shiftr data sCR0_SMCFCFG_SHIFT) 1 in
if smmu_enable =? 0 then
check_spec 0 adt
else
check_spec 1 adt
else if offset =? ARM_SMMU_GR0_sCR2 then
if (Z.land data 255) =? 0 then
check_spec 1 adt
else
check_spec 0 adt
else
check_spec 1 adt
else if (offset >=? ARM_SMMU_GR1_BASE) && (offset <? ARM_SMMU_GR1_END) then
let n := (offset - ARM_SMMU_GR1_BASE) / 4 in
when vmid == get_smmu_cfg_vmid_spec n smmu_index adt;
rely is_vmid vmid;
let type := Z.shiftr data CBAR_TYPE_SHIFT in
let t_vmid := Z.land data CBAR_VMID_MASK in
if vmid =? 0 then
check_spec 1 adt
else
if (type =? CBAR_TYPE_S2_TRANS) && (vmid =? t_vmid) then
check_spec 1 adt
else
check_spec 0 adt
else
check_spec 1 adt
end.
Definition handle_smmu_cb_access_spec0 (offset: Z64) (adt: RData) : option Z :=
match offset with
| VZ64 offset =>
rely (offset >=? SMMU_GLOBAL_BASE);
let off' := offset - SMMU_GLOBAL_BASE in
let cb_offset := Z.land off' ARM_SMMU_PGSHIFT_MASK in
if cb_offset =? ARM_SMMU_CB_TTBR0 then
check_spec 2 adt
else if cb_offset =? ARM_SMMU_CB_CONTEXTIDR then
check_spec 0 adt
else
check_spec 1 adt
end.
Definition __handle_smmu_write_spec0 (hsr: Z) (fault_ipa: Z64) (len: Z) (val: Z64) (write_val: Z) (adt: RData) : option RData :=
match fault_ipa, val with
| VZ64 fault_ipa, VZ64 val =>
if len =? 8 then
if write_val =? 0 then
when' data == host_get_mmio_data_spec hsr adt;
rely is_int64 data;
writeq_relaxed_spec (VZ64 data) (VZ64 fault_ipa) adt
else
writeq_relaxed_spec (VZ64 val) (VZ64 fault_ipa) adt
else
if len =? 4 then
writel_relaxed_spec (VZ64 val) (VZ64 fault_ipa) adt
else
panic_spec adt
end.
Definition __handle_smmu_read_spec0 (hsr: Z) (fault_ipa: Z64) (len: Z) (adt: RData) : option RData :=
match fault_ipa with
| VZ64 fault_ipa =>
when rt == host_dabt_get_rd_spec hsr adt;
rely is_int rt;
when vcpuid == get_cur_vcpuid_spec adt;
rely is_vcpu vcpuid;
if len =? 8 then
when' data, adt' == readq_relaxed_spec (VZ64 fault_ipa) adt;
rely is_int64 data;
set_shadow_ctxt_spec HOSTVISOR vcpuid rt (VZ64 data) adt'
else if len =? 4 then
when' data, adt' == readl_relaxed_spec (VZ64 fault_ipa) adt;
rely is_int64 data;
set_shadow_ctxt_spec HOSTVISOR vcpuid rt (VZ64 data) adt'
else
panic_spec adt
end.
Inductive handle_smmu_global_access_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| handle_smmu_global_access_spec_low_intro s (WB: _ -> Prop) m'0 labd hsr offset smmu_index res
(Hinv: high_level_invariant labd)
(Hspec: handle_smmu_global_access_spec0 (Int.unsigned hsr) (VZ64 (Int64.unsigned offset)) (Int.unsigned smmu_index) labd = Some (Int.unsigned res)):
handle_smmu_global_access_spec_low_step s WB ((Vint hsr)::(Vlong offset)::(Vint smmu_index)::nil) (m'0, labd) (Vint res) (m'0, labd).
Inductive handle_smmu_cb_access_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| handle_smmu_cb_access_spec_low_intro s (WB: _ -> Prop) m'0 labd offset res
(Hinv: high_level_invariant labd)
(Hspec: handle_smmu_cb_access_spec0 (VZ64 (Int64.unsigned offset)) labd = Some (Int.unsigned res)):
handle_smmu_cb_access_spec_low_step s WB ((Vlong offset)::nil) (m'0, labd) (Vint res) (m'0, labd).
Inductive __handle_smmu_write_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| __handle_smmu_write_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' hsr fault_ipa len val write_val
(Hinv: high_level_invariant labd)
(Hspec: __handle_smmu_write_spec0 (Int.unsigned hsr) (VZ64 (Int64.unsigned fault_ipa)) (Int.unsigned len) (VZ64 (Int64.unsigned val)) (Int.unsigned write_val) labd = Some labd'):
__handle_smmu_write_spec_low_step s WB ((Vint hsr)::(Vlong fault_ipa)::(Vint len)::(Vlong val)::(Vint write_val)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive __handle_smmu_read_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| __handle_smmu_read_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' hsr fault_ipa len
(Hinv: high_level_invariant labd)
(Hspec: __handle_smmu_read_spec0 (Int.unsigned hsr) (VZ64 (Int64.unsigned fault_ipa)) (Int.unsigned len) labd = Some labd'):
__handle_smmu_read_spec_low_step s WB ((Vint hsr)::(Vlong fault_ipa)::(Vint len)::nil) (m'0, labd) Vundef (m'0, labd').
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Definition handle_smmu_global_access_spec_low: compatsem LDATAOps :=
csem handle_smmu_global_access_spec_low_step (type_of_list_type (Tint32::Tint64::Tint32::nil)) Tint32.
Definition handle_smmu_cb_access_spec_low: compatsem LDATAOps :=
csem handle_smmu_cb_access_spec_low_step (type_of_list_type (Tint64::nil)) Tint32.
Definition __handle_smmu_write_spec_low: compatsem LDATAOps :=
csem __handle_smmu_write_spec_low_step (type_of_list_type (Tint32::Tint64::Tint32::Tint64::Tint32::nil)) Tvoid.
Definition __handle_smmu_read_spec_low: compatsem LDATAOps :=
csem __handle_smmu_read_spec_low_step (type_of_list_type (Tint32::Tint64::Tint32::nil)) Tvoid.
End WITHMEM.
End SmmuCoreAuxSpecLow.