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

arm-hyp abstract: refactor sanitise_register to not take kernel_object

This commit is contained in:
Joel Beeren 2017-04-26 20:29:19 +10:00 committed by Alejandro Gomez-Londono
parent e33d4d3145
commit cd7820e026
2 changed files with 11 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
spec/abstract/ARM_HYP/ArchTcb_A.thy
View File

@ -26,16 +26,24 @@ where
"arch_tcb_set_ipc_buffer target ptr \<equiv> as_user target $ set_register TPIDRURW ptr"
definition
sanitise_register :: "tcb \<Rightarrow> register \<Rightarrow> machine_word \<Rightarrow> machine_word"
sanitise_register :: "bool \<Rightarrow> register \<Rightarrow> machine_word \<Rightarrow> machine_word"
where
"sanitise_register t r v \<equiv> case r of
CPSR \<Rightarrow>
if tcb_vcpu (tcb_arch t) \<noteq> None \<and>
if t \<and>
v && 0x1f \<in> {0x10, 0x11, 0x12, 0x13, 0x17, 0x1b, 0x1f}
(* PMODE_(USER/FIQ/IRQ/SUPERVISOR/ABORT/UNDEFINED/SYSTEM) *)
then v
else (v && 0xf8000000) || 0x150
| _ \<Rightarrow> v"
definition
arch_tcb_sanitise_condition :: "obj_ref \<Rightarrow> (bool, 'a::state_ext) s_monad"
where
"arch_tcb_sanitise_condition t \<equiv> do
vcpu \<leftarrow> arch_thread_get tcb_vcpu t;
return (vcpu \<noteq> None)
od"
end
end

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

@ -384,10 +384,9 @@ where "dissociate_vcpu_tcb vr t \<equiv> do
when (\<exists>a. cur_v = Some (vr,a)) vcpu_invalidate_active;
arch_thread_set (\<lambda>x. x \<lparr> tcb_vcpu := None \<rparr>) t;
set_vcpu vr (v\<lparr> vcpu_tcb := None \<rparr>);
tcb \<leftarrow> gets_the $ get_tcb t;
as_user t $ do
cpsr \<leftarrow> getRegister CPSR;
setRegister CPSR $ sanitise_register tcb CPSR cpsr
setRegister CPSR $ sanitise_register False CPSR cpsr
od
od"