Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

arm-hyp+aarch64 haskell: add VCPURegVMPIDR(_EL2) #723

Merged
merged 3 commits into from
Mar 14, 2024
Merged

arm-hyp+aarch64 haskell: add VCPURegVMPIDR(_EL2) #723

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c852d4c
arm-hyp+aarch64 haskell: add VCPURegVMPIDR(_EL2)
lsf37 Feb 25, 2024
b887944
arm-hyp crefine: VCPUReg_VMPIDR updates
lsf37 Feb 25, 2024
a63d7ba
aarch64 crefine: VCPUReg_VMPIDR_EL2 updates
lsf37 Mar 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion proof/crefine/AARCH64/ArchMove_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -467,8 +467,9 @@ crunch pred_tcb_at'[wp]: readVCPUReg "\<lambda>s. P (pred_tcb_at' a b p s)" *)

crunch ksCurThread[wp]: readVCPUReg "\<lambda>s. P (ksCurThread s)"

(* schematic_goal leads to Suc (Suc ..) form only *)
lemma fromEnum_maxBound_vcpureg_def:
"fromEnum (maxBound :: vcpureg) = 22"
"fromEnum (maxBound :: vcpureg) = 23"
by (clarsimp simp: fromEnum_def maxBound_def enum_vcpureg)

lemma unat_of_nat_mword_fromEnum_vcpureg[simp]:
Expand Down
7 changes: 4 additions & 3 deletions proof/crefine/AARCH64/Retype_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5473,7 +5473,7 @@ lemma ptr_retyp_fromzeroVCPU:
assumes cor: "caps_overlap_reserved' {p ..+ 2 ^ vcpuBits} \<sigma>"
assumes ptr0: "p \<noteq> 0"
assumes kdr: "{p ..+ 2 ^ vcpuBits} \<inter> kernel_data_refs = {}"
assumes subr: "{p ..+ 736} \<subseteq> {p ..+ 2 ^ vcpuBits}"
assumes subr: "{p ..+ 752} \<subseteq> {p ..+ 2 ^ vcpuBits}" (is "{_ ..+ ?vcpusz} \<subseteq> _")
assumes act_bytes: "region_actually_is_bytes p (2 ^ vcpuBits) \<sigma>'"
assumes rep0: "heap_list (hrs_mem (t_hrs_' (globals \<sigma>'))) (2 ^ vcpuBits) p = replicate (2 ^ vcpuBits) 0"
assumes "\<not> snd (placeNewObject p vcpu0 0 \<sigma>)"
Expand All @@ -5490,7 +5490,8 @@ proof -
let ?htdret = "(hrs_htd_update (ptr_retyp (vcpu_Ptr p)) (t_hrs_' (globals \<sigma>')))"
let ?zeros = "from_bytes (replicate (size_of TYPE(vcpu_C)) 0) :: vcpu_C"

have "size_of TYPE(vcpu_C) = 736" (is "_ = ?vcpusz")
(* sanity check for the value of ?vcpusz *)
have "size_of TYPE(vcpu_C) = ?vcpusz"
by simp

have ptr_al:
Expand Down Expand Up @@ -5744,7 +5745,7 @@ lemma placeNewObject_vcpu_fromzero_ccorres:
apply (rule ccorres_from_vcg_nofail, clarsimp)
apply (rule conseqPre, vcg)
apply (clarsimp simp: rf_sr_htd_safe)
apply (subgoal_tac "{regionBase..+736} \<subseteq> {regionBase..+2^vcpuBits}")
apply (subgoal_tac "{regionBase..+752} \<subseteq> {regionBase..+2^vcpuBits}")
prefer 2
apply clarsimp
apply (drule intvlD, clarsimp)
Expand Down
1 change: 1 addition & 0 deletions proof/crefine/AARCH64/SR_lemmas_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2274,6 +2274,7 @@ lemmas seL4_VCPUReg_defs =
seL4_VCPUReg_ISR_def
seL4_VCPUReg_VBAR_def
seL4_VCPUReg_TPIDR_EL1_def
seL4_VCPUReg_VMPIDR_EL2_def
seL4_VCPUReg_SP_EL1_def
seL4_VCPUReg_ELR_EL1_def
seL4_VCPUReg_SPSR_EL1_def
Expand Down
10 changes: 3 additions & 7 deletions proof/crefine/AARCH64/Wellformed_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,15 +92,11 @@ abbreviation
abbreviation
vcpu_vppi_masked_C_Ptr :: "addr \<Rightarrow> (machine_word[1]) ptr" where "vcpu_vppi_masked_C_Ptr \<equiv> Ptr"

(* FIXME AARCH64 can't do this for either register or vcpureg due to missing code equations
value_type vcpuregs_count = "length enum_vcpureg"
if the above works, we could move it to the machine spec, at which point probably doing a rename
to register_count and vcpureg_count (singular) would make sense across the platforms *)

type_synonym vcpuregs_count = 23 (* length enum_vcpureg *)
declare seL4_VCPUReg_Num_def[code]
value_type num_vcpu_regs = seL4_VCPUReg_Num

abbreviation
vcpuregs_C_Ptr :: "addr \<Rightarrow> (machine_word[vcpuregs_count]) ptr" where "vcpuregs_C_Ptr \<equiv> Ptr"
vcpuregs_C_Ptr :: "addr \<Rightarrow> (machine_word[num_vcpu_regs]) ptr" where "vcpuregs_C_Ptr \<equiv> Ptr"

type_synonym tcb_cnode_array = "cte_C[5]"
type_synonym registers_count = 37 (* length enum_register *)
Expand Down
3 changes: 2 additions & 1 deletion proof/crefine/ARM_HYP/ArchMove_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -457,8 +457,9 @@ crunch pred_tcb_at'[wp]: readVCPUReg "\<lambda>s. P (pred_tcb_at' a b p s)"

crunch ksCurThread[wp]: readVCPUReg "\<lambda>s. P (ksCurThread s)"

(* schematic_goal leads to Suc (Suc ..) form only *)
lemma fromEnum_maxBound_vcpureg_def:
"fromEnum (maxBound :: vcpureg) = 41"
"fromEnum (maxBound :: vcpureg) = 42"
by (clarsimp simp: fromEnum_def maxBound_def enum_vcpureg)

lemma unat_of_nat_mword_fromEnum_vcpureg[simp]:
Expand Down
9 changes: 5 additions & 4 deletions proof/crefine/ARM_HYP/Retype_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5343,7 +5343,7 @@ lemma ptr_retyp_fromzeroVCPU:
assumes cor: "caps_overlap_reserved' {p ..+ 2 ^ vcpu_bits} \<sigma>"
assumes ptr0: "p \<noteq> 0"
assumes kdr: "{p ..+ 2 ^ vcpu_bits} \<inter> kernel_data_refs = {}"
assumes subr: "{p ..+ 456} \<subseteq> {p ..+ 2 ^ vcpu_bits}"
assumes subr: "{p ..+ 464} \<subseteq> {p ..+ 2 ^ vcpu_bits}" (is "{_ ..+ ?vcpusz} \<subseteq> _")
assumes act_bytes: "region_actually_is_bytes p (2 ^ vcpu_bits) \<sigma>'"
assumes rep0: "heap_list (hrs_mem (t_hrs_' (globals \<sigma>'))) (2 ^ vcpu_bits) p = replicate (2 ^ vcpu_bits) 0"
assumes "\<not> snd (placeNewObject p vcpu0 0 \<sigma>)"
Expand All @@ -5360,7 +5360,8 @@ proof -
let ?htdret = "(hrs_htd_update (ptr_retyp (vcpu_Ptr p)) (t_hrs_' (globals \<sigma>')))"
let ?zeros = "from_bytes (replicate (size_of TYPE(vcpu_C)) 0) :: vcpu_C"

have "size_of TYPE(vcpu_C) = 456" (is "_ = ?vcpusz")
(* sanity check for the value of ?vcpusz *)
have "size_of TYPE(vcpu_C) = ?vcpusz"
lsf37 marked this conversation as resolved.
Show resolved Hide resolved
by simp

have ptr_al:
Expand Down Expand Up @@ -5574,7 +5575,7 @@ proof -
apply (clarsimp simp: ko_vcpu_def vcpu0_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def
cmachine_state_relation_def Let_def h_t_valid_clift_Some_iff)
apply (subgoal_tac "region_is_bytes p 456 \<sigma>'")
apply (subgoal_tac "region_is_bytes p ?vcpusz \<sigma>'")
prefer 2
apply (fastforce simp: region_actually_is_bytes[OF act_bytes]
region_is_bytes_subset[OF _ subr])
Expand Down Expand Up @@ -5604,7 +5605,7 @@ lemma placeNewObject_vcpu_fromzero_ccorres:
apply (rule ccorres_from_vcg_nofail, clarsimp)
apply (rule conseqPre, vcg)
apply (clarsimp simp: rf_sr_htd_safe)
apply (subgoal_tac "{regionBase..+456} \<subseteq> {regionBase..+2^vcpu_bits}")
apply (subgoal_tac "{regionBase..+464} \<subseteq> {regionBase..+2^vcpu_bits}")
prefer 2
apply clarsimp
apply (drule intvlD, clarsimp)
Expand Down
1 change: 1 addition & 0 deletions proof/crefine/ARM_HYP/SR_lemmas_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2324,6 +2324,7 @@ lemmas seL4_VCPUReg_defs =
seL4_VCPUReg_R10fiq_def
seL4_VCPUReg_R11fiq_def
seL4_VCPUReg_R12fiq_def
seL4_VCPUReg_VMPIDR_def
seL4_VCPUReg_SPSRsvc_def
seL4_VCPUReg_SPSRabt_def
seL4_VCPUReg_SPSRund_def
Expand Down
7 changes: 6 additions & 1 deletion proof/crefine/ARM_HYP/Wellformed_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,13 @@ abbreviation
pt_Ptr :: "32 word \<Rightarrow> (pte_C[512]) ptr" where "pt_Ptr == Ptr"
abbreviation
pd_Ptr :: "32 word \<Rightarrow> (pde_C[2048]) ptr" where "pd_Ptr == Ptr"

declare seL4_VCPUReg_Num_def[code]
value_type num_vcpu_regs = seL4_VCPUReg_Num

abbreviation
regs_C_Ptr :: "addr \<Rightarrow> (machine_word_len word[42]) ptr" where "regs_C_Ptr \<equiv> Ptr"
regs_C_Ptr :: "addr \<Rightarrow> (machine_word[num_vcpu_regs]) ptr" where"regs_C_Ptr \<equiv> Ptr"

abbreviation
vgic_lr_C_Ptr :: "addr \<Rightarrow> (virq_C[64]) ptr" where "vgic_lr_C_Ptr \<equiv> Ptr"
abbreviation
Expand Down
1 change: 1 addition & 0 deletions spec/haskell/src/SEL4/Machine/RegisterSet/AARCH64.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,7 @@ data VCPUReg =
| VCPURegISR
| VCPURegVBAR
| VCPURegTPIDR_EL1
| VCPURegVMPIDR_EL2
| VCPURegSP_EL1
| VCPURegELR_EL1
| VCPURegSPSR_EL1
Expand Down
1 change: 1 addition & 0 deletions spec/haskell/src/SEL4/Machine/RegisterSet/ARM.lhs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,7 @@ This module defines the ARM register set.
> | VCPURegR10fiq
> | VCPURegR11fiq
> | VCPURegR12fiq
> | VCPURegVMPIDR
> | VCPURegSPSRsvc
> | VCPURegSPSRabt
> | VCPURegSPSRund
Expand Down
Loading