adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

always use `addrFromKPPtr` for kernel addresses 

This verifies a C kernel patch (seL4/seL4#409) which consolidates
translation between virtual and physical addresses, and makes it
consistent across architectures. In particular, we always use
`addrFromKPPtr`, even on architectures that don't use a distinct region
to map the kernel ELF. This will facilitate future improvements which
move the ELF mapping into a distinct virtual address region.

Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
This commit is contained in:
Matthew Brecknell 2021-06-24 16:20:03 +10:00 committed by Matthew Brecknell
parent 2aadbf9589
commit fd01872121
12 changed files with 77 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
proof/crefine/ARM/VSpace_C.thy
View File

@ -705,24 +705,29 @@ lemma pde_case_isPageTablePDE:
by (cases pde, simp_all add: isPageTablePDE_def)
lemma ptrFromPAddr_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
Call ptrFromPAddr_'proc
\<lbrace> \<acute>ret__ptr_to_void = Ptr (ptrFromPAddr (paddr_' s) ) \<rbrace>"
"\<forall>s. \<Gamma> \<turnstile> {s}
Call ptrFromPAddr_'proc
\<lbrace>\<acute>ret__ptr_to_void = Ptr (ptrFromPAddr (paddr_' s))\<rbrace>"
apply vcg
apply (simp add: ARM.ptrFromPAddr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM.physBase_def)
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def)
done
lemma addrFromPPtr_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
Call addrFromPPtr_'proc
\<lbrace> \<acute>ret__unsigned_long = (addrFromPPtr (ptr_val (pptr_' s)) ) \<rbrace>"
"\<forall>s. \<Gamma> \<turnstile> {s}
Call addrFromPPtr_'proc
\<lbrace>\<acute>ret__unsigned_long = addrFromPPtr (ptr_val (pptr_' s))\<rbrace>"
apply vcg
apply (simp add: addrFromPPtr_def
ARM.addrFromPPtr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM.physBase_def)
apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def physBase_def)
done
lemma addrFromKPPtr_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
Call addrFromKPPtr_'proc
\<lbrace>\<acute>ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\<rbrace>"
apply vcg
apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def kernelELFPAddrBase_def
kernelELFBase_def physBase_def pptrBase_def mask_def)
done
abbreviation
"lookupPTSlot_xf \<equiv> liftxf errstate lookupPTSlot_ret_C.status_C lookupPTSlot_ret_C.ptSlot_C ret__struct_lookupPTSlot_ret_C_'"

27
proof/crefine/ARM_HYP/VSpace_C.thy
View File

@ -777,24 +777,29 @@ lemma pde_case_isPageTablePDE:
by (cases pde, simp_all add: isPageTablePDE_def)
lemma ptrFromPAddr_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
Call ptrFromPAddr_'proc
\<lbrace> \<acute>ret__ptr_to_void = Ptr (ptrFromPAddr (paddr_' s) ) \<rbrace>"
"\<forall>s. \<Gamma> \<turnstile> {s}
Call ptrFromPAddr_'proc
\<lbrace>\<acute>ret__ptr_to_void = Ptr (ptrFromPAddr (paddr_' s))\<rbrace>"
apply vcg
apply (simp add: ARM_HYP.ptrFromPAddr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM_HYP.physBase_def)
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def)
done
lemma addrFromPPtr_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
Call addrFromPPtr_'proc
\<lbrace> \<acute>ret__unsigned_long = (addrFromPPtr (ptr_val (pptr_' s)) ) \<rbrace>"
"\<forall>s. \<Gamma> \<turnstile> {s}
Call addrFromPPtr_'proc
\<lbrace>\<acute>ret__unsigned_long = addrFromPPtr (ptr_val (pptr_' s))\<rbrace>"
apply vcg
apply (simp add: addrFromPPtr_def
ARM_HYP.addrFromPPtr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM_HYP.physBase_def)
apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def physBase_def)
done
lemma addrFromKPPtr_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
Call addrFromKPPtr_'proc
\<lbrace>\<acute>ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\<rbrace>"
apply vcg
apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def kernelELFPAddrBase_def
kernelELFBase_def physBase_def pptrBase_def mask_def)
done
abbreviation
"lookupPTSlot_xf \<equiv> liftxf errstate lookupPTSlot_ret_C.status_C lookupPTSlot_ret_C.ptSlot_C ret__struct_lookupPTSlot_ret_C_'"

13
proof/crefine/RISCV64/VSpace_C.thy
View File

@ -877,14 +877,13 @@ lemma ccorres_name_pre_C:
apply simp
done
lemma kpptr_to_paddr_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
Call kpptr_to_paddr_'proc
\<lbrace> \<acute>ret__unsigned_long = RISCV64.addrFromKPPtr (ptr_val (pptr_' s)) \<rbrace>"
lemma addrFromKPPtr_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
Call addrFromKPPtr_'proc
\<lbrace>\<acute>ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\<rbrace>"
apply vcg
apply (simp add: RISCV64.addrFromKPPtr_def RISCV64.addrFromKPPtr_def pptrBaseOffset_def
RISCV64.kernelELFBase_def RISCV64.kernelELFPAddrBase_def
RISCV64.kernelELFBaseOffset_def)
apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def
kernelELFBase_def kernelELFPAddrBase_def)
done
lemma isValidVTableRoot_def2:

11
proof/crefine/X64/VSpace_C.thy
View File

@ -1101,13 +1101,12 @@ lemma ccorres_name_pre_C:
apply simp
done
lemma kpptr_to_paddr_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
Call kpptr_to_paddr_'proc
\<lbrace> \<acute>ret__unsigned_long = X64.addrFromKPPtr (ptr_val (pptr_' s)) \<rbrace>"
lemma addrFromKPPtr_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
Call addrFromKPPtr_'proc
\<lbrace>\<acute>ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\<rbrace>"
apply vcg
apply (simp add: X64.addrFromKPPtr_def X64.addrFromKPPtr_def
X64.kernelELFBaseOffset_def)
apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def)
done
(* A version of ccr3_relation in which the most significant bit is cleared.

2
proof/drefine/Finalise_DR.thy
View File

@ -585,7 +585,7 @@ lemma invalidate_hw_asid_entry_dwp[wp]:
done
lemma set_current_pd_dwp[wp]:
" \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> set_current_pd (addrFromPPtr x) \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
" \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> set_current_pd paddr \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
by (clarsimp simp:set_current_pd_def writeTTBR0_def isb_def dsb_def,wp)
lemma set_hardware_asid_dwp[wp]:

8
proof/refine/ARM/VSpace_R.thy
View File

@ -665,10 +665,10 @@ lemma setVMRoot_corres:
proof -
have P: "corres dc \<top> \<top>
(do global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromPPtr global_pd))
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od)
(do globalPD \<leftarrow> gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromPPtr globalPD))
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)"
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
@ -680,11 +680,11 @@ proof -
have Q: "\<And>P P'. corres dc P P'
(throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch>
(\<lambda>_ . do global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromPPtr global_pd
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od))
(throwError Fault_H.lookup_failure.InvalidRoot <catch>
(\<lambda>_ . do globalPD \<leftarrow> gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromPPtr globalPD
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))"
apply (rule corres_guard_imp)
apply (rule corres_split_catch [where f=lfr])

4
proof/refine/ARM_HYP/VSpace_R.thy
View File

@ -1166,11 +1166,11 @@ proof -
have Q: "\<And>P P'. corres dc P P'
(throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch>
(\<lambda>_. do global_us_pd \<leftarrow> gets (arm_us_global_pd \<circ> arch_state);
do_machine_op $ set_current_pd $ addrFromPPtr global_us_pd
do_machine_op $ set_current_pd $ addrFromKPPtr global_us_pd
od))
(throwError Fault_H.lookup_failure.InvalidRoot <catch>
(\<lambda>_ . do globalPD \<leftarrow> gets (armUSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromPPtr globalPD
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))"
apply (rule corres_guard_imp)
apply (rule corres_split_catch [where f=lfr])

2
spec/abstract/ARM/ArchVSpace_A.thy
View File

@ -325,7 +325,7 @@ definition
| _ \<Rightarrow> throwError InvalidRoot) <catch>
(\<lambda>_. do
global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
do_machine_op $ set_current_pd $ addrFromPPtr global_pd
do_machine_op $ set_current_pd $ addrFromKPPtr global_pd
od)
od"

2
spec/abstract/ARM_HYP/ArchVSpace_A.thy
View File

@ -643,7 +643,7 @@ definition
| _ \<Rightarrow> throwError InvalidRoot) <catch>
(\<lambda>_. do
global_us_pd \<leftarrow> gets (arm_us_global_pd o arch_state);
do_machine_op $ set_current_pd $ addrFromPPtr global_us_pd
do_machine_op $ set_current_pd $ addrFromKPPtr global_us_pd
od)
od"

2
spec/haskell/src/SEL4/Kernel/VSpace/ARM.lhs
View File

@ -937,7 +937,7 @@ If the current thread has no page directory, or if it has an invalid ASID, the h
#else
> globalPD <- gets (armKSGlobalPD . ksArchState)
#endif
> doMachineOp $ setCurrentPD $ addrFromPPtr globalPD)
> doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD)
When cleaning the cache by user virtual address on ARM11, the active address space must be the one that contains the mappings being cleaned. The following function is used to temporarily switch to a given page directory and ASID, in order to clean the cache. It returns "True" if the address space was not the same as the current one, in which case the caller must switch back to the current address space once the cache is clean.

12
spec/machine/ARM/Platform.thy
View File

@ -48,12 +48,24 @@ definition physBase :: word32 where
definition pptrBaseOffset :: word32 where
"pptrBaseOffset \<equiv> pptrBase - physBase"
definition kernelELFBase :: word32 where
"kernelELFBase \<equiv> pptrBase + (physBase && mask 22)"
definition kernelELFPAddrBase :: word32 where
"kernelELFPAddrBase \<equiv> 0x10000000"
definition kernelELFBaseOffset :: word32 where
"kernelELFBaseOffset \<equiv> kernelELFBase - kernelELFPAddrBase"
definition ptrFromPAddr :: "paddr \<Rightarrow> word32" where
"ptrFromPAddr paddr \<equiv> paddr + pptrBaseOffset"
definition addrFromPPtr :: "word32 \<Rightarrow> paddr" where
"addrFromPPtr pptr \<equiv> pptr - pptrBaseOffset"
definition addrFromKPPtr :: "word32 \<Rightarrow> paddr" where
"addrFromKPPtr kpptr \<equiv> kpptr - kernelELFBaseOffset"
definition minIRQ :: "irq" where
"minIRQ \<equiv> 0"

12
spec/machine/ARM_HYP/Platform.thy
View File

@ -56,12 +56,24 @@ definition paddrTop :: "32 word" where
definition pptrBaseOffset :: word32 where
"pptrBaseOffset \<equiv> pptrBase - physBase"
definition kernelELFBase :: word32 where
"kernelELFBase \<equiv> pptrBase + (physBase && mask 22)"
definition kernelELFPAddrBase :: word32 where
"kernelELFPAddrBase \<equiv> 0x80000000"
definition kernelELFBaseOffset :: word32 where
"kernelELFBaseOffset \<equiv> kernelELFBase - kernelELFPAddrBase"
definition ptrFromPAddr :: "paddr \<Rightarrow> word32" where
"ptrFromPAddr paddr \<equiv> paddr + pptrBaseOffset"
definition addrFromPPtr :: "word32 \<Rightarrow> paddr" where
"addrFromPPtr pptr \<equiv> pptr - pptrBaseOffset"
definition addrFromKPPtr :: "word32 \<Rightarrow> paddr" where
"addrFromKPPtr kpptr \<equiv> kpptr - kernelELFBaseOffset"
definition minIRQ :: "irq" where
"minIRQ \<equiv> 0"