provide TCB argument for sanitiseRegister
Other platforms such as arm-hyp will need to look into additional TCB state such as VCPU in sanitiseRegister. This commit provides the scaffolding for that.
This commit is contained in:
Gerwin Klein
parent
3607dfabbf
commit
520921351a
|
|
@ -287,6 +287,30 @@ lemma asUser_threadGet_tcbFault_comm:
|
|||
apply assumption
|
||||
done
|
||||
|
||||
lemma asUser_getRegister_threadGet_comm:
|
||||
"do
|
||||
ra \<leftarrow> asUser a (getRegister r);
|
||||
rb \<leftarrow> threadGet fb b;
|
||||
c ra rb
|
||||
od = do
|
||||
rb \<leftarrow> threadGet fb b;
|
||||
ra \<leftarrow> asUser a (getRegister r);
|
||||
c ra rb
|
||||
od"
|
||||
by (rule bind_inv_inv_comm, auto; wp)
|
||||
|
||||
lemma asUser_mapMloadWordUser_threadGet_comm:
|
||||
"do
|
||||
ra \<leftarrow> mapM loadWordUser xs;
|
||||
rb \<leftarrow> threadGet fb b;
|
||||
c ra rb
|
||||
od = do
|
||||
rb \<leftarrow> threadGet fb b;
|
||||
ra \<leftarrow> mapM loadWordUser xs;
|
||||
c ra rb
|
||||
od"
|
||||
by (rule bind_inv_inv_comm, auto; wp mapM_wp')
|
||||
|
||||
lemma threadGet_tcbFault_doMachineOp_comm:
|
||||
"\<lbrakk> empty_fail m' \<rbrakk> \<Longrightarrow>
|
||||
do x \<leftarrow> threadGet tcbFault t; y \<leftarrow> doMachineOp m'; n x y od =
|
||||
|
|
@ -477,26 +501,30 @@ definition
|
|||
CapFault _ _ _ \<Rightarrow> return True
|
||||
| ArchFault af \<Rightarrow> handleArchFaultReply' af sender receiver tag
|
||||
| UnknownSyscallException _ \<Rightarrow> do
|
||||
t \<leftarrow> threadGet id receiver;
|
||||
regs \<leftarrow> return $ take (unat mlen) syscallMessage;
|
||||
zipWithM_x (\<lambda>rs rd. do
|
||||
v \<leftarrow> asUser sender $ getRegister rs;
|
||||
asUser receiver $ setRegister rd $ sanitiseRegister rd v
|
||||
asUser receiver $ setRegister rd $ sanitiseRegister t rd v
|
||||
od) msgRegisters regs;
|
||||
sendBuf \<leftarrow> lookupIPCBuffer False sender;
|
||||
case sendBuf of
|
||||
None \<Rightarrow> return ()
|
||||
| Some bufferPtr \<Rightarrow>
|
||||
| Some bufferPtr \<Rightarrow> do
|
||||
t \<leftarrow> threadGet id receiver;
|
||||
zipWithM_x (\<lambda>i rd. do
|
||||
v \<leftarrow> loadWordUser (bufferPtr + PPtr (i * 4));
|
||||
asUser receiver $ setRegister rd $ sanitiseRegister rd v
|
||||
od) [(scast n_msgRegisters :: word32) + 1.e. scast n_syscallMessage] (drop (unat (scast n_msgRegisters :: word32)) regs);
|
||||
asUser receiver $ setRegister rd $ sanitiseRegister t rd v
|
||||
od) [(scast n_msgRegisters :: word32) + 1.e. scast n_syscallMessage] (drop (unat (scast n_msgRegisters :: word32)) regs)
|
||||
od;
|
||||
return (label = 0)
|
||||
od
|
||||
| UserException _ _ \<Rightarrow> do
|
||||
t \<leftarrow> threadGet id receiver;
|
||||
regs \<leftarrow> return $ take (unat mlen) exceptionMessage;
|
||||
zipWithM_x (\<lambda>rs rd. do
|
||||
v \<leftarrow> asUser sender $ getRegister rs;
|
||||
asUser receiver $ setRegister rd $ sanitiseRegister rd v
|
||||
asUser receiver $ setRegister rd $ sanitiseRegister t rd v
|
||||
od) msgRegisters regs;
|
||||
return (label = 0)
|
||||
od
|
||||
|
|
@ -568,34 +596,76 @@ lemma mapM_x_zip_take_Cons_append:
|
|||
by (cases n, simp_all add: mapM_x_Cons)
|
||||
|
||||
lemma monadic_rewrite_do_flip:
|
||||
"monadic_rewrite E F P (do a \<leftarrow> f; b \<leftarrow> g; return (a, b) od)
|
||||
(do b \<leftarrow> g; a \<leftarrow> f; return (a, b) od)
|
||||
\<Longrightarrow> monadic_rewrite E F P (do a \<leftarrow> f; b \<leftarrow> g; h a b od)
|
||||
(do b \<leftarrow> g; a \<leftarrow> f; h a b od)"
|
||||
"monadic_rewrite E F P (do c \<leftarrow> j; a \<leftarrow> f c; b \<leftarrow> g c; return (a, b) od)
|
||||
(do c \<leftarrow> j; b \<leftarrow> g c; a \<leftarrow> f c; return (a, b) od)
|
||||
\<Longrightarrow> monadic_rewrite E F P (do c \<leftarrow> j; a \<leftarrow> f c; b \<leftarrow> g c; h a b od)
|
||||
(do c \<leftarrow> j; b \<leftarrow> g c; a \<leftarrow> f c; h a b od)"
|
||||
apply (drule_tac h="\<lambda>(a, b). h a b" in monadic_rewrite_bind_head)
|
||||
apply (simp add: bind_assoc)
|
||||
done
|
||||
|
||||
lemma threadGet_lookupIPCBuffer_comm:
|
||||
"do
|
||||
a \<leftarrow> lookupIPCBuffer x y;
|
||||
t \<leftarrow> threadGet id r;
|
||||
c a t
|
||||
od = do
|
||||
t \<leftarrow> threadGet id r;
|
||||
a \<leftarrow> lookupIPCBuffer x y;
|
||||
c a t
|
||||
od"
|
||||
by (rule bind_inv_inv_comm; wp?; auto)
|
||||
|
||||
lemma threadGet_moreMapM_comm:
|
||||
"do
|
||||
a \<leftarrow>
|
||||
case sb of None \<Rightarrow> return []
|
||||
| Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser;
|
||||
t \<leftarrow> threadGet id r;
|
||||
c a t
|
||||
od = do
|
||||
t \<leftarrow> threadGet id r;
|
||||
a \<leftarrow>
|
||||
case sb of None \<Rightarrow> return []
|
||||
| Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser;
|
||||
c a t
|
||||
od"
|
||||
apply (rule bind_inv_inv_comm)
|
||||
apply (rule hoare_pre, wpc; (wp mapM_wp')?)
|
||||
apply simp
|
||||
apply wp
|
||||
apply (auto split: option.splits)
|
||||
done
|
||||
|
||||
|
||||
lemma monadic_rewrite_symb_exec_r':
|
||||
"\<lbrakk> \<And>s. \<lbrace>op = s\<rbrace> m \<lbrace>\<lambda>r. op = s\<rbrace>; no_fail P m;
|
||||
\<And>rv. monadic_rewrite F False (Q rv) x (y rv);
|
||||
\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace> \<rbrakk>
|
||||
\<Longrightarrow> monadic_rewrite F False P x (m >>= y)"
|
||||
apply (rule monadic_rewrite_imp)
|
||||
apply (rule monadic_rewrite_symb_exec_r; assumption)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma monadic_rewrite_threadGet_return:
|
||||
"monadic_rewrite True False (tcb_at' r) (return x) (do t \<leftarrow> threadGet f r; return x od)"
|
||||
apply (rule monadic_rewrite_symb_exec_r')
|
||||
apply wp+
|
||||
apply (rule monadic_rewrite_refl)
|
||||
apply wp
|
||||
done
|
||||
|
||||
lemma monadic_rewrite_inst: "monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E P f g"
|
||||
by simp
|
||||
|
||||
context kernel_m begin interpretation Arch .
|
||||
|
||||
lemma lookupIPCBuffer_isolatable:
|
||||
"thread_actions_isolatable idx (lookupIPCBuffer w t)"
|
||||
apply (simp add: lookupIPCBuffer_def)
|
||||
apply (rule thread_actions_isolatable_bind)
|
||||
apply (clarsimp simp: put_tcb_state_regs_tcb_def threadGet_isolatable
|
||||
getThreadBufferSlot_def locateSlot_conv getSlotCap_def
|
||||
split: tcb_state_regs.split)+
|
||||
apply (rule thread_actions_isolatable_bind)
|
||||
apply (clarsimp simp: thread_actions_isolatable_return
|
||||
getCTE_isolatable
|
||||
assert_isolatable
|
||||
split: capability.split arch_capability.split bool.split)+
|
||||
apply (rule thread_actions_isolatable_if)
|
||||
apply (rule thread_actions_isolatable_bind)
|
||||
apply (simp add: assert_isolatable thread_actions_isolatable_return | wp)+
|
||||
lemma threadGet_discarded:
|
||||
"(threadGet f t >>= (\<lambda>_. n)) = stateAssert (tcb_at' t) [] >>= (\<lambda>_. n)"
|
||||
apply (simp add: threadGet_def getObject_get_assert liftM_def bind_assoc stateAssert_def)
|
||||
apply (rule ext)
|
||||
apply (simp add: bind_def simpler_gets_def get_def)
|
||||
done
|
||||
|
||||
lemma handleFaultReply':
|
||||
|
|
@ -611,13 +681,11 @@ lemma handleFaultReply':
|
|||
bit_def msgLengthBits_def msgRegisters_unfold
|
||||
fromIntegral_simp1 fromIntegral_simp2
|
||||
shiftL_word)
|
||||
apply (simp add: bind_assoc del: take_append)
|
||||
apply (simp add: bind_assoc)
|
||||
apply (rule monadic_rewrite_bind_tail)
|
||||
apply (clarsimp simp: mapM_def sequence_def bind_assoc asUser_bind_distrib
|
||||
asUser_return submonad_asUser.fn_stateAssert
|
||||
del: take_append)
|
||||
apply (case_tac f, simp_all add: handleFaultReply_def zipWithM_x_mapM_x zip_take
|
||||
del: take_append)
|
||||
asUser_return submonad_asUser.fn_stateAssert)
|
||||
apply (case_tac f, simp_all add: handleFaultReply_def zipWithM_x_mapM_x zip_take)
|
||||
(* UserException *)
|
||||
apply (clarsimp simp: handleFaultReply_def zipWithM_x_mapM_x
|
||||
zip_Cons ARM_H.exceptionMessage_def
|
||||
|
|
@ -629,15 +697,15 @@ lemma handleFaultReply':
|
|||
(erule disjE[OF word_less_cases],
|
||||
( clarsimp simp: n_msgRegisters_def asUser_bind_distrib
|
||||
mapM_x_Cons mapM_x_Nil bind_assoc
|
||||
asUser_getRegister_discarded
|
||||
asUser_comm[OF neq]
|
||||
asUser_getRegister_discarded asUser_mapMloadWordUser_threadGet_comm
|
||||
asUser_comm[OF neq] asUser_getRegister_threadGet_comm
|
||||
bind_comm_mapM_comm [OF asUser_loadWordUser_comm, symmetric]
|
||||
word_le_nat_alt[of 4, simplified linorder_not_less[symmetric, of 4]]
|
||||
asUser_return submonad_asUser.fn_stateAssert
|
||||
| rule monadic_rewrite_bind_tail monadic_rewrite_refl
|
||||
monadic_rewrite_symb_exec_l[OF stateAssert_inv]
|
||||
monadic_rewrite_symb_exec_l[OF mapM_x_mapM_valid[OF mapM_x_wp']]
|
||||
| wp asUser_tcb_at' lookupIPCBuffer_inv')+)+))
|
||||
| wp asUser_tcb_at' lookupIPCBuffer_inv' )+)+))
|
||||
apply wp
|
||||
(* capFault *)
|
||||
apply (rule monadic_rewrite_symb_exec_l, (wp empty_fail_asUser)+)+
|
||||
|
|
@ -648,31 +716,34 @@ lemma handleFaultReply':
|
|||
| wp mapM_x_mapM_valid[OF mapM_x_wp'[OF loadWordUser_inv]]
|
||||
empty_fail_loadWordUser)+
|
||||
(* UnknownSyscallExceptio *)
|
||||
apply (simp add: zip_append2 mapM_x_append asUser_bind_distrib split_def
|
||||
bind_assoc)
|
||||
apply (simp add: zip_append2 mapM_x_append asUser_bind_distrib split_def bind_assoc)
|
||||
apply (rule monadic_rewrite_imp)
|
||||
apply (rule monadic_rewrite_trans[rotated])
|
||||
apply (rule monadic_rewrite_do_flip)
|
||||
apply (rule_tac P="inj (case_bool s r)" in monadic_rewrite_gen_asm)
|
||||
apply (rule monadic_rewrite_trans[OF _ monadic_rewrite_transverse])
|
||||
apply (rule monadic_rewrite_weaken[where F=False and E=True], simp)
|
||||
apply (rule isolate_thread_actions_rewrite_bind
|
||||
bool.simps setRegister_simple
|
||||
zipWithM_setRegister_simple
|
||||
thread_actions_isolatable_bind lookupIPCBuffer_isolatable
|
||||
lookupIPCBuffer_isolatable[THEN thread_actions_isolatableD]
|
||||
copy_registers_isolate_general thread_actions_isolatable_return
|
||||
thread_actions_isolatable_return[THEN thread_actions_isolatableD]
|
||||
| assumption
|
||||
| wp assert_inv)+
|
||||
apply (rule monadic_rewrite_isolate_final[where P="\<top>"])
|
||||
apply simp+
|
||||
apply (rule monadic_rewrite_bind_tail)
|
||||
apply (rule_tac P="inj (case_bool s r)" in monadic_rewrite_gen_asm)
|
||||
apply (rule monadic_rewrite_trans[OF _ monadic_rewrite_transverse])
|
||||
apply (rule monadic_rewrite_weaken[where F=False and E=True], simp)
|
||||
apply (rule isolate_thread_actions_rewrite_bind
|
||||
bool.simps setRegister_simple
|
||||
zipWithM_setRegister_simple
|
||||
thread_actions_isolatable_bind lookupIPCBuffer_isolatable
|
||||
lookupIPCBuffer_isolatable[THEN thread_actions_isolatableD]
|
||||
copy_registers_isolate_general thread_actions_isolatable_return
|
||||
thread_actions_isolatable_return[THEN thread_actions_isolatableD]
|
||||
| assumption
|
||||
| wp assert_inv)+
|
||||
apply (rule monadic_rewrite_isolate_final[where P="\<top>"])
|
||||
apply simp+
|
||||
apply wp
|
||||
(* swap ends *)
|
||||
apply (clarsimp simp: handleFaultReply_def zipWithM_x_mapM_x
|
||||
zip_Cons syscallMessage_unfold
|
||||
n_syscallMessage_def
|
||||
upto_enum_word mapM_x_Cons mapM_x_Nil)
|
||||
apply (simp add: threadGet_moreMapM_comm asUser_getRegister_threadGet_comm threadGet_lookupIPCBuffer_comm)
|
||||
apply (rule monadic_rewrite_bind_tail)
|
||||
apply (rule monadic_rewrite_bind_tail [where Q="\<lambda>_. tcb_at' r"])
|
||||
apply (case_tac sb)
|
||||
apply (case_tac "msgLength tag < scast n_msgRegisters")
|
||||
apply (erule disjE[OF word_less_cases],
|
||||
|
|
@ -697,7 +768,8 @@ lemma handleFaultReply':
|
|||
| rule monadic_rewrite_bind_tail monadic_rewrite_refl
|
||||
monadic_rewrite_symb_exec_l[OF mapM_x_mapM_valid[OF mapM_x_wp']]
|
||||
monadic_rewrite_symb_exec_l[OF stateAssert_inv]
|
||||
| wp asUser_tcb_at')+)+
|
||||
monadic_rewrite_threadGet_return
|
||||
| wp asUser_tcb_at' mapM_wp')+)+
|
||||
apply (simp add: n_msgRegisters_def word_le_nat_alt n_syscallMessage_def
|
||||
linorder_not_less syscallMessage_unfold)
|
||||
apply (clarsimp | frule neq0_conv[THEN iffD2, THEN not0_implies_Suc,
|
||||
|
|
@ -707,8 +779,8 @@ lemma handleFaultReply':
|
|||
@ [scast n_syscallMessage + 1 .e. msgMaxLength]")
|
||||
apply (simp only: upto_enum_word[where y="scast n_syscallMessage :: word32"]
|
||||
upto_enum_word[where y="scast n_syscallMessage + 1 :: word32"])
|
||||
apply (clarsimp simp: bind_assoc asUser_bind_distrib
|
||||
mapM_x_Cons mapM_x_Nil
|
||||
apply (clarsimp simp: bind_assoc asUser_bind_distrib asUser_getRegister_threadGet_comm
|
||||
mapM_x_Cons mapM_x_Nil threadGet_discarded
|
||||
asUser_comm [OF neq] asUser_getRegister_discarded
|
||||
submonad_asUser.fn_stateAssert take_zip
|
||||
bind_subst_lift [OF submonad_asUser.stateAssert_fn]
|
||||
|
|
@ -742,7 +814,7 @@ lemma handleFaultReply':
|
|||
msgLengthBits_def shiftL_nat
|
||||
del: upt.simps upt_rec_numeral)
|
||||
apply (simp add: upto_enum_word cong: if_weak_cong)
|
||||
apply wp
|
||||
apply wp+
|
||||
(* ArchFault *)
|
||||
apply (simp add: neq inj_case_bool split: bool.split)
|
||||
apply (rule monadic_rewrite_imp)
|
||||
|
|
@ -3696,6 +3768,7 @@ lemma length_exceptionMessage:
|
|||
lemma copyMRsFaultReply_ccorres_exception:
|
||||
"ccorres dc xfdc
|
||||
(valid_pspace' and tcb_at' s
|
||||
and ko_at' t r
|
||||
and obj_at' (\<lambda>t. tcbFault t = Some f) r
|
||||
and K (r \<noteq> s)
|
||||
and K (len \<le> unat n_exceptionMessage))
|
||||
|
|
@ -3704,7 +3777,7 @@ lemma copyMRsFaultReply_ccorres_exception:
|
|||
\<inter> \<lbrace>\<acute>id___anonymous_enum = MessageID_Exception \<rbrace>
|
||||
\<inter> \<lbrace>\<acute>length___unsigned_long = of_nat len \<rbrace>) hs
|
||||
(zipWithM_x (\<lambda>rs rd. do v \<leftarrow> asUser s (getRegister rs);
|
||||
asUser r (setRegister rd (ARM_H.sanitiseRegister rd v))
|
||||
asUser r (setRegister rd (ARM_H.sanitiseRegister t rd v))
|
||||
od)
|
||||
ARM_H.msgRegisters (take len ARM_H.exceptionMessage))
|
||||
(Call copyMRsFaultReply_'proc)"
|
||||
|
|
@ -3738,7 +3811,7 @@ proof -
|
|||
ARM.exceptionMessage_def word_of_nat_less)
|
||||
apply (simp add: msgRegisters_ccorres n_msgRegisters_def length_msgRegisters
|
||||
unat_of_nat exceptionMessage_ccorres[symmetric,simplified MessageID_Exception_def,simplified]
|
||||
n_exceptionMessage_def length_exceptionMessage)
|
||||
n_exceptionMessage_def length_exceptionMessage sanitiseRegister_def)
|
||||
apply (simp add: word_less_nat_alt unat_of_nat)
|
||||
apply (rule conseqPre, vcg)
|
||||
apply (clarsimp simp: word_of_nat_less ARM_H.exceptionMessage_def
|
||||
|
|
@ -3790,6 +3863,7 @@ lemma copyMRsFaultReply_ccorres_syscall:
|
|||
fixes word_size :: "'a::len"
|
||||
shows "ccorres dc xfdc
|
||||
(valid_pspace' and tcb_at' s
|
||||
and ko_at' t r
|
||||
and obj_at' (\<lambda>t. tcbFault t = Some f) r
|
||||
and K (r \<noteq> s)
|
||||
and K (len \<le> unat n_syscallMessage))
|
||||
|
|
@ -3798,18 +3872,20 @@ lemma copyMRsFaultReply_ccorres_syscall:
|
|||
\<inter> \<lbrace>\<acute>id___anonymous_enum = MessageID_Syscall \<rbrace>
|
||||
\<inter> \<lbrace>\<acute>length___unsigned_long = of_nat len \<rbrace>) hs
|
||||
(do a \<leftarrow> zipWithM_x (\<lambda>rs rd. do v \<leftarrow> asUser s (getRegister rs);
|
||||
asUser r (setRegister rd (ARM_H.sanitiseRegister rd v))
|
||||
asUser r (setRegister rd (ARM_H.sanitiseRegister t rd v))
|
||||
od)
|
||||
ARM_H.msgRegisters (take len ARM_H.syscallMessage);
|
||||
sendBuf \<leftarrow> lookupIPCBuffer False s;
|
||||
case sendBuf of None \<Rightarrow> return ()
|
||||
| Some bufferPtr \<Rightarrow>
|
||||
| Some bufferPtr \<Rightarrow> do
|
||||
t \<leftarrow> threadGet id r;
|
||||
zipWithM_x (\<lambda>i rd. do v \<leftarrow> loadWordUser (bufferPtr + i * 4);
|
||||
asUser r (setRegister rd (ARM_H.sanitiseRegister rd v))
|
||||
asUser r (setRegister rd (ARM_H.sanitiseRegister t rd v))
|
||||
od)
|
||||
[scast n_msgRegisters + 1.e.scast n_syscallMessage]
|
||||
(drop (unat (scast n_msgRegisters :: word32))
|
||||
(take len ARM_H.syscallMessage))
|
||||
od
|
||||
od)
|
||||
(Call copyMRsFaultReply_'proc)"
|
||||
proof -
|
||||
|
|
@ -3846,7 +3922,7 @@ lemma copyMRsFaultReply_ccorres_syscall:
|
|||
length_msgRegisters)
|
||||
apply (simp add: msgRegisters_ccorres n_msgRegisters_def length_msgRegisters unat_of_nat
|
||||
syscallMessage_ccorres[symmetric,simplified MessageID_Syscall_def,simplified]
|
||||
n_syscallMessage_def length_syscallMessage)
|
||||
n_syscallMessage_def length_syscallMessage sanitiseRegister_def)
|
||||
apply (simp add: word_less_nat_alt unat_of_nat)
|
||||
apply (rule conseqPre, vcg)
|
||||
apply (clarsimp simp: word_of_nat_less syscallMessage_unfold length_msgRegisters
|
||||
|
|
@ -3880,87 +3956,91 @@ lemma copyMRsFaultReply_ccorres_syscall:
|
|||
apply wpc
|
||||
apply (simp add: option_to_0_def ccorres_cond_iffs option_to_ptr_def)
|
||||
apply (rule ccorres_return_Skip')
|
||||
apply (rule_tac P="sb \<noteq> Some 0" in ccorres_gen_asm)
|
||||
apply (rule_tac P="case_option True (\<lambda>x. is_aligned x msg_align_bits) sb"
|
||||
in ccorres_gen_asm)
|
||||
apply (simp add: option_to_0_def option_to_ptr_def)
|
||||
apply (subgoal_tac "sb'\<noteq> NULL") prefer 2
|
||||
apply clarsimp
|
||||
apply (simp add: ccorres_cond_iffs)
|
||||
apply (subst ccorres_seq_skip' [symmetric])
|
||||
apply (rule_tac r'="\<lambda>rv rv'. rv' = of_nat (unat n_msgRegisters) + _" in ccorres_rel_imp)
|
||||
apply (drule_tac s="sb" in sym)
|
||||
apply (simp only: zipWithM_x_mapM_x)
|
||||
apply ccorres_rewrite
|
||||
apply (rule_tac F="\<lambda>_. valid_pspace'
|
||||
and (case sb of None \<Rightarrow> \<top>
|
||||
| Some x \<Rightarrow> valid_ipc_buffer_ptr' x)
|
||||
and tcb_at' r"
|
||||
in ccorres_mapM_x_while')
|
||||
apply clarsimp
|
||||
apply (rule ccorres_guard_imp2)
|
||||
apply (rule ccorres_pre_loadWordUser)
|
||||
apply (intro ccorres_rhs_assoc)
|
||||
apply (rule ccorres_symb_exec_r)
|
||||
apply (rule ccorres_move_array_assertion_ipc_buffer
|
||||
ccorres_Guard_Seq[where S="{s. h_t_valid (htd s) c_guard (ptr s)}" for ptr htd])+
|
||||
apply (rule ccorres_symb_exec_r)
|
||||
apply (rule ccorres_move_c_guard_tcb)
|
||||
apply (rule ccorres_symb_exec_r)
|
||||
apply ctac
|
||||
apply vcg
|
||||
apply (rule conseqPre, vcg)
|
||||
apply fastforce
|
||||
apply vcg
|
||||
apply (rule conseqPre, vcg)
|
||||
apply (rule ccorres_symb_exec_l)
|
||||
apply (rule_tac P="sb \<noteq> Some 0" in ccorres_gen_asm)
|
||||
apply (rule_tac P="case_option True (\<lambda>x. is_aligned x msg_align_bits) sb"
|
||||
in ccorres_gen_asm)
|
||||
apply (simp add: option_to_0_def option_to_ptr_def)
|
||||
apply (subgoal_tac "sb'\<noteq> NULL") prefer 2
|
||||
apply clarsimp
|
||||
apply (simp add: ccorres_cond_iffs)
|
||||
apply (subst ccorres_seq_skip' [symmetric])
|
||||
apply (rule_tac r'="\<lambda>rv rv'. rv' = of_nat (unat n_msgRegisters) + _" in ccorres_rel_imp)
|
||||
apply (drule_tac s="sb" in sym)
|
||||
apply (simp only: zipWithM_x_mapM_x)
|
||||
apply ccorres_rewrite
|
||||
apply (rule_tac F="\<lambda>_. valid_pspace'
|
||||
and (case sb of None \<Rightarrow> \<top>
|
||||
| Some x \<Rightarrow> valid_ipc_buffer_ptr' x)
|
||||
and tcb_at' r"
|
||||
in ccorres_mapM_x_while')
|
||||
apply clarsimp
|
||||
apply vcg
|
||||
apply (rule conseqPre, vcg)
|
||||
apply (rule ccorres_guard_imp2)
|
||||
apply (rule ccorres_pre_loadWordUser)
|
||||
apply (intro ccorres_rhs_assoc)
|
||||
apply (rule ccorres_symb_exec_r)
|
||||
apply (rule ccorres_move_array_assertion_ipc_buffer
|
||||
ccorres_Guard_Seq[where S="{s. h_t_valid (htd s) c_guard (ptr s)}" for ptr htd])+
|
||||
apply (rule ccorres_symb_exec_r)
|
||||
apply (rule ccorres_move_c_guard_tcb)
|
||||
apply (rule ccorres_symb_exec_r)
|
||||
apply ctac
|
||||
apply vcg
|
||||
apply (rule conseqPre, vcg)
|
||||
apply fastforce
|
||||
apply vcg
|
||||
apply (rule conseqPre, vcg)
|
||||
apply clarsimp
|
||||
apply vcg
|
||||
apply (rule conseqPre, vcg)
|
||||
apply clarsimp
|
||||
apply clarsimp
|
||||
apply (subst aligned_add_aligned, assumption)
|
||||
apply (rule is_aligned_mult_triv2[where n=2, simplified])
|
||||
apply (simp add: msg_align_bits)
|
||||
apply (simp add: of_nat_unat[simplified comp_def])
|
||||
apply (simp only: n_msgRegisters_def)
|
||||
apply (clarsimp simp: n_syscallMessage_def n_msgRegisters_def
|
||||
word_unat.Rep_inverse[of "scast _ :: 'a word"]
|
||||
msgRegisters_ccorres[symmetric]
|
||||
length_msgRegisters[symmetric]
|
||||
syscallMessage_ccorres[symmetric]
|
||||
length_msgRegisters length_syscallMessage
|
||||
syscallMessage_ccorres[symmetric, simplified MessageID_Syscall_def, simplified]
|
||||
unat_of_nat32 word_bits_def
|
||||
MessageID_Syscall_def
|
||||
min_def message_info_to_H_def
|
||||
upto_enum_def typ_heap_simps'
|
||||
unat_add_lem[THEN iffD1]
|
||||
msg_align_bits sanitiseRegister_def
|
||||
simp del: upt_rec_numeral,
|
||||
simp_all add: word_less_nat_alt unat_add_lem[THEN iffD1] unat_of_nat)[1]
|
||||
apply (clarsimp simp: n_syscallMessage_def n_msgRegisters_def
|
||||
msgRegisters_ccorres
|
||||
syscallMessage_ccorres
|
||||
length_syscallMessage length_msgRegisters
|
||||
message_info_to_H_def min_def
|
||||
split: if_split)
|
||||
apply (fastforce dest!: le_antisym)
|
||||
apply (vcg spec=TrueI)
|
||||
apply clarsimp
|
||||
apply clarsimp
|
||||
apply (subst aligned_add_aligned, assumption)
|
||||
apply (rule is_aligned_mult_triv2[where n=2, simplified])
|
||||
apply (simp add: msg_align_bits)
|
||||
apply (simp add: of_nat_unat[simplified comp_def])
|
||||
apply (simp only: n_msgRegisters_def)
|
||||
apply (clarsimp simp: n_syscallMessage_def n_msgRegisters_def
|
||||
word_unat.Rep_inverse[of "scast _ :: 'a word"]
|
||||
msgRegisters_ccorres[symmetric]
|
||||
length_msgRegisters[symmetric]
|
||||
syscallMessage_ccorres[symmetric]
|
||||
length_msgRegisters length_syscallMessage
|
||||
syscallMessage_ccorres[symmetric, simplified MessageID_Syscall_def, simplified]
|
||||
unat_of_nat32 word_bits_def
|
||||
MessageID_Syscall_def
|
||||
min_def message_info_to_H_def
|
||||
upto_enum_def typ_heap_simps'
|
||||
unat_add_lem[THEN iffD1]
|
||||
msg_align_bits
|
||||
simp del: upt_rec_numeral,
|
||||
simp_all add: word_less_nat_alt unat_add_lem[THEN iffD1] unat_of_nat)[1]
|
||||
apply (clarsimp simp: n_syscallMessage_def n_msgRegisters_def
|
||||
msgRegisters_ccorres
|
||||
syscallMessage_ccorres
|
||||
length_syscallMessage length_msgRegisters
|
||||
message_info_to_H_def min_def
|
||||
split: if_split)
|
||||
apply (fastforce dest!: le_antisym)
|
||||
apply (vcg spec=TrueI)
|
||||
apply clarsimp
|
||||
apply (simp add: split_def)
|
||||
apply (wp hoare_case_option_wp)
|
||||
apply (fastforce elim: aligned_add_aligned
|
||||
intro: is_aligned_mult_triv2 [where n=2,
|
||||
simplified]
|
||||
simp: word_bits_def msg_align_bits)
|
||||
apply (clarsimp simp: msgRegisters_unfold
|
||||
n_msgRegisters_def
|
||||
word_bits_def not_less)
|
||||
apply (simp add: n_syscallMessage_def)
|
||||
apply simp
|
||||
apply (simp add: split_def)
|
||||
apply (wp hoare_case_option_wp)
|
||||
apply (fastforce elim: aligned_add_aligned
|
||||
intro: is_aligned_mult_triv2 [where n=2,simplified]
|
||||
simp: word_bits_def msg_align_bits)
|
||||
apply (clarsimp simp: msgRegisters_unfold
|
||||
n_msgRegisters_def
|
||||
word_bits_def not_less)
|
||||
apply (simp add: n_syscallMessage_def)
|
||||
apply simp
|
||||
apply wp
|
||||
apply (wpsimp wp: threadGet_wp)
|
||||
apply simp
|
||||
apply (subst option.split[symmetric,where P=id, simplified])
|
||||
apply (rule valid_drop_case)
|
||||
apply (wp lookupIPCBuffer_aligned[simplified K_def] lookupIPCBuffer_not_Some_0[simplified K_def])
|
||||
apply (wp hoare_drop_imps hoare_vcg_all_lift lookupIPCBuffer_aligned[simplified K_def]
|
||||
lookupIPCBuffer_not_Some_0[simplified K_def])
|
||||
apply (simp add: length_syscallMessage
|
||||
length_msgRegisters
|
||||
n_syscallMessage_def
|
||||
|
|
@ -3973,8 +4053,11 @@ lemma copyMRsFaultReply_ccorres_syscall:
|
|||
apply (rule ccorres_symb_exec_l)
|
||||
apply (case_tac rv ; clarsimp)
|
||||
apply (rule ccorres_return_Skip[simplified dc_def])+
|
||||
apply (wp mapM_x_wp_inv user_getreg_inv'
|
||||
| clarsimp simp: zipWithM_x_mapM_x split: prod.split)+
|
||||
apply (rule ccorres_guard_imp)
|
||||
apply (rule ccorres_symb_exec_l)
|
||||
apply (rule ccorres_return_Skip[simplified dc_def])+
|
||||
apply (wp mapM_x_wp_inv user_getreg_inv'
|
||||
| clarsimp simp: zipWithM_x_mapM_x split: prod.split)+
|
||||
apply (cases "4 < len")
|
||||
apply (fastforce simp: guard_is_UNIV_def
|
||||
msgRegisters_unfold
|
||||
|
|
@ -4088,11 +4171,13 @@ lemma handleFaultReply_ccorres [corres]:
|
|||
apply (rename_tac number code)
|
||||
apply (clarsimp simp: bind_assoc seL4_Fault_tag_defs ccorres_cond_iffs
|
||||
split del: if_split)
|
||||
apply (subst take_min_len[symmetric,where n="unat (msgLength _)"])
|
||||
apply (ctac add: copyMRsFaultReply_ccorres_exception)
|
||||
apply (ctac add: ccorres_return_C)
|
||||
apply wp
|
||||
apply (vcg exspec=copyMRsFaultReply_modifies)
|
||||
apply (rule ccorres_symb_exec_l)
|
||||
apply (subst take_min_len[symmetric,where n="unat (msgLength _)"])
|
||||
apply (ctac add: copyMRsFaultReply_ccorres_exception)
|
||||
apply (ctac add: ccorres_return_C)
|
||||
apply wp
|
||||
apply (vcg exspec=copyMRsFaultReply_modifies)
|
||||
apply (wpsimp wp: threadGet_wp)+
|
||||
(* CapFault *)
|
||||
apply (clarsimp simp: bind_assoc seL4_Fault_tag_defs ccorres_cond_iffs
|
||||
split del: if_split)
|
||||
|
|
@ -4101,13 +4186,16 @@ lemma handleFaultReply_ccorres [corres]:
|
|||
apply (rename_tac number)
|
||||
apply (clarsimp simp: seL4_Fault_tag_defs ccorres_cond_iffs
|
||||
split del: if_split)
|
||||
apply (subst take_min_len[symmetric,where n="unat (msgLength _)"])
|
||||
apply (subst take_min_len[symmetric,where n="unat (msgLength _)"])
|
||||
apply (fold bind_assoc)
|
||||
apply (ctac add: copyMRsFaultReply_ccorres_syscall[simplified bind_assoc[symmetric]])
|
||||
apply (ctac add: ccorres_return_C)
|
||||
apply wp
|
||||
apply (vcg exspec=copyMRsFaultReply_modifies)
|
||||
apply (rule ccorres_symb_exec_l)
|
||||
apply (subst take_min_len[symmetric,where n="unat (msgLength _)"])
|
||||
apply (subst take_min_len[symmetric,where n="unat (msgLength _)"])
|
||||
apply (fold bind_assoc id_def)
|
||||
apply (ctac add: copyMRsFaultReply_ccorres_syscall[simplified bind_assoc[symmetric]])
|
||||
apply (ctac add: ccorres_return_C)
|
||||
apply wp
|
||||
apply (vcg exspec=copyMRsFaultReply_modifies)
|
||||
apply (wpsimp wp: threadGet_wp)+
|
||||
|
||||
(* ArchFault *)
|
||||
apply (rule ccorres_cond_false)
|
||||
apply (rule ccorres_cond_false)
|
||||
|
|
|
|||
|
|
@ -117,12 +117,7 @@ lemma isolate_thread_actions_bind:
|
|||
apply (simp add: exec_gets exec_modify)
|
||||
done
|
||||
|
||||
lemma setEndpoint_obj_at_tcb':
|
||||
"\<lbrace>obj_at' (P :: tcb \<Rightarrow> bool) p\<rbrace> setEndpoint p' val \<lbrace>\<lambda>rv. obj_at' P p\<rbrace>"
|
||||
apply (simp add: setEndpoint_def)
|
||||
apply (rule obj_at_setObject2)
|
||||
apply (clarsimp simp: updateObject_default_def in_monad)
|
||||
done
|
||||
lemmas setEndpoint_obj_at_tcb' = setEndpoint_obj_at'_tcb
|
||||
|
||||
lemma tcbSchedEnqueue_obj_at_unchangedT:
|
||||
assumes y: "\<And>f. \<forall>tcb. P (tcbQueued_update f tcb) = P tcb"
|
||||
|
|
@ -184,14 +179,7 @@ lemmas setThreadState_obj_at_unchanged
|
|||
lemmas setBoundNotification_obj_at_unchanged
|
||||
= setBoundNotification_obj_at_unchangedT[OF all_tcbI]
|
||||
|
||||
lemma setNotification_tcb:
|
||||
"\<lbrace>obj_at' (\<lambda>tcb::tcb. P tcb) t\<rbrace>
|
||||
setNotification ntfn e
|
||||
\<lbrace>\<lambda>_. obj_at' P t\<rbrace>"
|
||||
apply (simp add: setNotification_def)
|
||||
apply (rule obj_at_setObject2)
|
||||
apply (clarsimp simp: updateObject_default_def in_monad)
|
||||
done
|
||||
lemmas setNotification_tcb = set_ntfn_tcb_obj_at'
|
||||
|
||||
(* FIXME: move *)
|
||||
lemmas threadSet_obj_at' = threadSet_obj_at'_strongish
|
||||
|
|
|
|||
|
|
@ -208,13 +208,12 @@ lemma is_aligned_tcb_ptr_to_ctcb_ptr:
|
|||
done
|
||||
|
||||
lemma sanitiseRegister_spec:
|
||||
"\<forall>s v r. \<Gamma> \<turnstile> ({s} \<inter> \<lbrace>\<acute>v___unsigned_long = v\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H r\<rbrace>)
|
||||
Call sanitiseRegister_'proc
|
||||
\<lbrace>\<acute>ret__unsigned_long = sanitiseRegister r v\<rbrace>"
|
||||
"\<forall>s t v r. \<Gamma> \<turnstile> ({s} \<inter> \<lbrace>\<acute>v___unsigned_long = v\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H r\<rbrace>)
|
||||
Call sanitiseRegister_'proc
|
||||
\<lbrace>\<acute>ret__unsigned_long = sanitiseRegister t r v\<rbrace>"
|
||||
apply vcg
|
||||
apply (auto simp: C_register_defs ARM_H.sanitiseRegister_def
|
||||
ARM.sanitiseRegister_def word_0_sle_from_less
|
||||
split: register.split)
|
||||
apply (auto simp: C_register_defs sanitiseRegister_def word_0_sle_from_less
|
||||
split: register.split)
|
||||
done
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1127,24 +1127,16 @@ lemma invokeTCB_CopyRegisters_ccorres:
|
|||
done
|
||||
|
||||
(* FIXME: move *)
|
||||
lemma mapM_x_append:
|
||||
"mapM_x f (xs @ ys) = do mapM_x f xs; mapM_x f ys od"
|
||||
apply (simp add: mapM_x_def sequence_x_def)
|
||||
apply (induct xs)
|
||||
apply simp
|
||||
apply (simp add: bind_assoc)
|
||||
done
|
||||
lemmas mapM_x_append = mapM_x_append2
|
||||
|
||||
(* ARMHYP note: this works on ARM for all t since the that argument of sanitiseRegister is
|
||||
discarded. On arm-hyp, the argument is used, needing changes to arch-common code in higher-level
|
||||
specs. *)
|
||||
lemma invokeTCB_WriteRegisters_ccorres_helper:
|
||||
"\<lbrakk> unat (f (of_nat n)) = incn
|
||||
\<and> g (of_nat n) = register_from_H reg \<and> n'=incn
|
||||
\<and> of_nat n < bnd \<and> of_nat n < bnd2 \<rbrakk> \<Longrightarrow>
|
||||
ccorres dc xfdc (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) \<lbrace>\<acute>i = of_nat n\<rbrace> hs
|
||||
ccorres dc xfdc (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P)
|
||||
(\<lbrace>\<acute>i = of_nat n\<rbrace>) hs
|
||||
(asUser dst (setRegister reg
|
||||
(sanitiseRegister reg (args ! incn))))
|
||||
(sanitiseRegister tcb reg (args ! incn))))
|
||||
(\<acute>ret__unsigned_long :== CALL getSyscallArg(f (\<acute>i),option_to_ptr buffer);;
|
||||
Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace>
|
||||
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr dst}
|
||||
|
|
@ -1162,7 +1154,7 @@ lemma invokeTCB_WriteRegisters_ccorres_helper:
|
|||
apply wp
|
||||
apply simp
|
||||
apply (vcg exspec=getSyscallArg_modifies)
|
||||
apply (clarsimp simp: tcb_at_h_t_valid)
|
||||
apply (fastforce simp: tcb_at_h_t_valid)
|
||||
done
|
||||
|
||||
lemma doMachineOp_context:
|
||||
|
|
@ -1393,6 +1385,19 @@ lemma asUser_sysargs_rel:
|
|||
apply (wp asUser_getMRs_rel hoare_valid_ipc_buffer_ptr_typ_at'|simp)+
|
||||
done
|
||||
|
||||
lemma threadSet_same:
|
||||
"\<lbrace>\<lambda>s. \<exists>tcb'. ko_at' tcb' t s \<and> tcb = f tcb'\<rbrace> threadSet f t \<lbrace>\<lambda>rv. ko_at' tcb t\<rbrace>"
|
||||
unfolding threadSet_def
|
||||
by (wpsimp wp: setObject_tcb_strongest getObject_tcb_wp) fastforce
|
||||
|
||||
lemma asUser_setRegister_ko_at':
|
||||
"\<lbrace>obj_at' (\<lambda>tcb'. tcb = tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch tcb'))(r := v)) (tcbArch tcb')) tcb') dst\<rbrace>
|
||||
asUser dst (setRegister r v) \<lbrace>\<lambda>rv. ko_at' (tcb::tcb) dst\<rbrace>"
|
||||
unfolding asUser_def
|
||||
apply (wpsimp wp: threadSet_same threadGet_wp)
|
||||
apply (clarsimp simp: setRegister_def simpler_modify_def obj_at'_def)
|
||||
done
|
||||
|
||||
lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]:
|
||||
notes static_imp_wp [wp]
|
||||
shows
|
||||
|
|
@ -1429,108 +1434,104 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]:
|
|||
apply (rule_tac P'="{s. n_' s = n}" in ccorres_from_vcg[where P=\<top>])
|
||||
apply (rule allI, rule conseqPre, vcg)
|
||||
apply (clarsimp simp: return_def min_def)
|
||||
apply (simp add: linorder_not_less[symmetric]
|
||||
n_gpRegisters_def n_frameRegisters_def)
|
||||
apply (simp add: linorder_not_less[symmetric] n_gpRegisters_def n_frameRegisters_def)
|
||||
apply ceqv
|
||||
apply (simp add: zipWithM_mapM split_def zip_append1
|
||||
mapM_discarded mapM_x_append
|
||||
del: Collect_const)
|
||||
apply (simp add: asUser_bind_distrib getRestartPC_def setNextPC_def
|
||||
bind_assoc del: Collect_const)
|
||||
apply (simp only: getRestartPC_def[symmetric] setNextPC_def[symmetric])
|
||||
apply (simp add: asUser_mapM_x bind_assoc)
|
||||
apply (rule ccorres_stateAssert)
|
||||
apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg)
|
||||
apply (rule_tac F="\<lambda>n. sysargs_rel args buffer and sysargs_rel_n args buffer (n + 2)
|
||||
apply (rule ccorres_symb_exec_l)
|
||||
apply (simp add: zipWithM_mapM split_def zip_append1 mapM_discarded mapM_x_append
|
||||
del: Collect_const)
|
||||
apply (simp add: asUser_bind_distrib getRestartPC_def setNextPC_def bind_assoc
|
||||
del: Collect_const)
|
||||
apply (simp only: getRestartPC_def[symmetric] setNextPC_def[symmetric])
|
||||
apply (simp add: asUser_mapM_x bind_assoc)
|
||||
apply (rule ccorres_stateAssert)
|
||||
apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg)
|
||||
apply (rule_tac F="\<lambda>n. sysargs_rel args buffer and sysargs_rel_n args buffer (n + 2)
|
||||
and tcb_at' dst and (\<lambda>s. dst \<noteq> ksCurThread s)"
|
||||
and Q=UNIV
|
||||
in ccorres_mapM_x_whileQ)
|
||||
apply clarsimp
|
||||
apply (rule_tac invokeTCB_WriteRegisters_ccorres_helper
|
||||
[where args=args])
|
||||
apply (simp add: unat_word_ariths frame_gp_registers_convs
|
||||
n_frameRegisters_def unat_of_nat32 word_bits_def
|
||||
word_of_nat_less)
|
||||
apply (simp add: n_frameRegisters_def n_gpRegisters_def
|
||||
frame_gp_registers_convs word_less_nat_alt)
|
||||
apply (simp add: unat_of_nat32 word_bits_def)
|
||||
apply arith
|
||||
apply clarsimp
|
||||
apply (vcg exspec=setRegister_modifies exspec=getSyscallArg_modifies
|
||||
exspec=sanitiseRegister_modifies)
|
||||
apply clarsimp
|
||||
apply (simp add: sysargs_rel_n_def)
|
||||
apply (rule hoare_pre, wp asUser_sysargs_rel)
|
||||
apply (clarsimp simp: n_msgRegisters_def sysargs_rel_def)
|
||||
apply (simp add: frame_gp_registers_convs n_frameRegisters_def
|
||||
word_bits_def)
|
||||
apply simp
|
||||
apply (rule ceqv_refl)
|
||||
apply (rule ccorres_stateAssert)
|
||||
apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg)
|
||||
apply (rule_tac F="\<lambda>n. sysargs_rel args buffer
|
||||
and sysargs_rel_n args buffer (n + length ARM_H.frameRegisters + 2)
|
||||
and tcb_at' dst
|
||||
and (\<lambda>s. dst \<noteq> ksCurThread s)"
|
||||
and Q=UNIV
|
||||
in ccorres_mapM_x_whileQ)
|
||||
and Q=UNIV in ccorres_mapM_x_whileQ)
|
||||
apply clarsimp
|
||||
apply (rule invokeTCB_WriteRegisters_ccorres_helper
|
||||
[where args=args])
|
||||
apply (simp add: n_gpRegisters_def unat_word_ariths
|
||||
frame_gp_registers_convs unat_of_nat32
|
||||
word_bits_def n_frameRegisters_def
|
||||
word_of_nat_less)
|
||||
apply (rule_tac invokeTCB_WriteRegisters_ccorres_helper [where args=args])
|
||||
apply (simp add: unat_word_ariths frame_gp_registers_convs n_frameRegisters_def
|
||||
unat_of_nat32 word_bits_def word_of_nat_less)
|
||||
apply (simp add: n_frameRegisters_def n_gpRegisters_def
|
||||
frame_gp_registers_convs unat_of_nat32
|
||||
word_less_nat_alt word_bits_def
|
||||
less_diff_conv)
|
||||
apply (simp add: unat_word_ariths cong: conj_cong)
|
||||
frame_gp_registers_convs word_less_nat_alt)
|
||||
apply (simp add: unat_of_nat32 word_bits_def)
|
||||
apply arith
|
||||
apply clarsimp
|
||||
apply (vcg exspec=setRegister_modifies exspec=getSyscallArg_modifies
|
||||
exspec=sanitiseRegister_modifies)
|
||||
apply clarsimp
|
||||
apply (simp add: sysargs_rel_n_def)
|
||||
apply (rule hoare_pre, wp asUser_sysargs_rel)
|
||||
apply (clarsimp simp: n_msgRegisters_def frame_gp_registers_convs
|
||||
n_frameRegisters_def)
|
||||
apply arith
|
||||
apply (simp add: ARM_H.gpRegisters_def word_bits_def
|
||||
ARM.gpRegisters_def)
|
||||
apply (clarsimp simp: n_msgRegisters_def sysargs_rel_def)
|
||||
apply (simp add: frame_gp_registers_convs n_frameRegisters_def word_bits_def)
|
||||
apply simp
|
||||
apply (rule ceqv_refl)
|
||||
apply (ctac(no_vcg) add: getRestartPC_ccorres)
|
||||
apply simp
|
||||
apply (ctac(no_vcg) add: setNextPC_ccorres)
|
||||
apply (rule ccorres_split_nothrow_novcg)
|
||||
apply (rule ccorres_when[where R=\<top>])
|
||||
apply (simp add: from_bool_0 Collect_const_mem)
|
||||
apply (rule_tac xf'="\<lambda>_. 0" in ccorres_call)
|
||||
apply (rule restart_ccorres)
|
||||
apply simp
|
||||
apply (simp add: xfdc_def)
|
||||
apply simp
|
||||
apply (rule ceqv_refl)
|
||||
apply (unfold return_returnOk)[1]
|
||||
apply (rule ccorres_return_CE, simp+)[1]
|
||||
apply wp
|
||||
apply (simp add: guard_is_UNIV_def)
|
||||
apply wp+
|
||||
apply simp
|
||||
apply (rule mapM_x_wp')
|
||||
apply (rule hoare_pre, wp)
|
||||
apply clarsimp
|
||||
apply simp
|
||||
apply wp
|
||||
apply (simp add: guard_is_UNIV_def)
|
||||
apply (rule hoare_drop_imps)
|
||||
apply (simp add: sysargs_rel_n_def)
|
||||
apply (wp mapM_x_wp')
|
||||
apply (rule hoare_pre, wp asUser_sysargs_rel)
|
||||
apply clarsimp
|
||||
apply wpsimp
|
||||
apply (simp add: guard_is_UNIV_def)
|
||||
apply (wp)
|
||||
apply (rule ceqv_refl)
|
||||
apply (rule ccorres_stateAssert)
|
||||
apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg)
|
||||
apply (rule_tac F="\<lambda>n. sysargs_rel args buffer
|
||||
and sysargs_rel_n args buffer (n + length ARM_H.frameRegisters + 2)
|
||||
and tcb_at' dst
|
||||
and (\<lambda>s. dst \<noteq> ksCurThread s)"
|
||||
and Q=UNIV in ccorres_mapM_x_whileQ)
|
||||
apply clarsimp
|
||||
apply (rule invokeTCB_WriteRegisters_ccorres_helper [where args=args])
|
||||
apply (simp add: n_gpRegisters_def unat_word_ariths
|
||||
frame_gp_registers_convs unat_of_nat32
|
||||
word_bits_def n_frameRegisters_def
|
||||
word_of_nat_less)
|
||||
apply (simp add: n_frameRegisters_def n_gpRegisters_def
|
||||
frame_gp_registers_convs unat_of_nat32
|
||||
word_less_nat_alt word_bits_def
|
||||
less_diff_conv)
|
||||
apply (simp add: unat_word_ariths cong: conj_cong)
|
||||
apply clarsimp
|
||||
apply (vcg exspec=setRegister_modifies exspec=getSyscallArg_modifies
|
||||
exspec=sanitiseRegister_modifies)
|
||||
apply clarsimp
|
||||
apply (simp add: sysargs_rel_n_def)
|
||||
apply (rule hoare_pre, wp asUser_sysargs_rel)
|
||||
apply (clarsimp simp: n_msgRegisters_def frame_gp_registers_convs
|
||||
n_frameRegisters_def)
|
||||
apply arith
|
||||
apply (simp add: ARM_H.gpRegisters_def word_bits_def
|
||||
ARM.gpRegisters_def)
|
||||
apply simp
|
||||
apply (rule ceqv_refl)
|
||||
apply (ctac(no_vcg) add: getRestartPC_ccorres)
|
||||
apply simp
|
||||
apply (ctac(no_vcg) add: setNextPC_ccorres)
|
||||
apply (rule ccorres_split_nothrow_novcg)
|
||||
apply (rule ccorres_when[where R=\<top>])
|
||||
apply (simp add: from_bool_0 Collect_const_mem)
|
||||
apply (rule_tac xf'="\<lambda>_. 0" in ccorres_call)
|
||||
apply (rule restart_ccorres)
|
||||
apply simp
|
||||
apply (simp add: xfdc_def)
|
||||
apply simp
|
||||
apply (rule ceqv_refl)
|
||||
apply (unfold return_returnOk)[1]
|
||||
apply (rule ccorres_return_CE, simp+)[1]
|
||||
apply wp
|
||||
apply (simp add: guard_is_UNIV_def)
|
||||
apply wp+
|
||||
apply simp
|
||||
apply (rule mapM_x_wp')
|
||||
apply (rule hoare_pre, wp)
|
||||
apply clarsimp
|
||||
apply simp
|
||||
apply wp
|
||||
apply (simp add: guard_is_UNIV_def)
|
||||
apply (rule hoare_drop_imps)
|
||||
apply (simp add: sysargs_rel_n_def)
|
||||
apply (wp mapM_x_wp')
|
||||
apply (rule hoare_pre, wp asUser_sysargs_rel)
|
||||
apply clarsimp
|
||||
apply wpsimp
|
||||
apply (simp add: guard_is_UNIV_def)
|
||||
apply (wp)
|
||||
apply (wp threadGet_wp)
|
||||
apply simp
|
||||
apply wp
|
||||
apply vcg
|
||||
apply (rule ccorres_inst[where P=\<top> and P'=UNIV])
|
||||
apply simp
|
||||
|
|
@ -4156,8 +4157,7 @@ lemma decodeSetSpace_ccorres:
|
|||
apply (frule interpret_excaps_eq[rule_format, where n=1], simp)
|
||||
apply (clarsimp simp: mask_def[where n=4] ccap_rights_relation_def
|
||||
rightsFromWord_wordFromRights
|
||||
capTCBPtr_eq tcb_ptr_to_ctcb_ptr_mask
|
||||
tcb_cnode_index_defs size_of_def
|
||||
capTCBPtr_eq tcb_cnode_index_defs size_of_def
|
||||
option_to_0_def rf_sr_ksCurThread
|
||||
"StrictC'_thread_state_defs" mask_eq_iff_w2p word_size)
|
||||
apply (simp add: word_sle_def cap_get_tag_isCap)
|
||||
|
|
|
|||
|
|
@ -2114,16 +2114,18 @@ lemma dcorres_handle_fault_reply:
|
|||
(corrupt_tcb_intent y)
|
||||
(handle_fault_reply a y mi mrs)"
|
||||
apply (case_tac a)
|
||||
apply (simp_all)
|
||||
apply (rule dummy_corrupt_tcb_intent_corres)+
|
||||
apply (simp_all)
|
||||
apply (rule dummy_corrupt_tcb_intent_corres)+
|
||||
apply (rule corres_dummy_return_l)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split[OF corres_trivial[OF corres_free_return] corrupt_tcb_intent_as_user_corres])
|
||||
apply (wp|clarsimp)+
|
||||
apply (rule corres_dummy_return_l)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split[OF corres_trivial[OF corres_free_return] corrupt_tcb_intent_as_user_corres])
|
||||
apply (wp|clarsimp)+
|
||||
apply (rule corres_symb_exec_r)
|
||||
apply (rule corres_split[OF corres_trivial[OF corres_free_return] corrupt_tcb_intent_as_user_corres])
|
||||
apply (wp|clarsimp)+
|
||||
apply (rule corres_dummy_return_l)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_symb_exec_r)
|
||||
apply (rule corres_split[OF corres_trivial[OF corres_free_return] corrupt_tcb_intent_as_user_corres])
|
||||
apply (wp|clarsimp)+
|
||||
apply (rule dcorres_handle_arch_fault_reply)
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -636,15 +636,16 @@ lemma invoke_tcb_corres_write_regs:
|
|||
dcorres (dc \<oplus> dc) \<top> (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')"
|
||||
apply (clarsimp simp: Tcb_D.invoke_tcb_def translate_tcb_invocation_def)
|
||||
apply (rule corres_symb_exec_r)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split [where r'=dc])
|
||||
apply (rule corres_cases [where R=resume])
|
||||
apply (clarsimp simp: when_def)
|
||||
apply (rule corres_bind_return_r)
|
||||
apply (clarsimp simp: dc_def, rule restart_corres [unfolded dc_def])
|
||||
apply (clarsimp simp: when_def)
|
||||
apply (rule corrupt_tcb_intent_as_user_corres)
|
||||
apply (wp wp_post_taut | simp add:invs_def valid_state_def | fastforce)+
|
||||
apply (rule corres_symb_exec_r)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split [where r'=dc])
|
||||
apply (rule corres_cases [where R=resume])
|
||||
apply (clarsimp simp: when_def)
|
||||
apply (rule corres_bind_return_r)
|
||||
apply (clarsimp simp: dc_def, rule restart_corres [unfolded dc_def])
|
||||
apply (clarsimp simp: when_def)
|
||||
apply (rule corrupt_tcb_intent_as_user_corres)
|
||||
apply (wp wp_post_taut | simp add:invs_def valid_state_def | fastforce)+
|
||||
done
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
|
|
|
|||
|
|
@ -1998,11 +1998,9 @@ lemma handle_arch_fault_reply_reads_respects:
|
|||
lemma handle_fault_reply_reads_respects:
|
||||
"reads_respects aag l (K (is_subject aag thread)) (handle_fault_reply fault thread x y)"
|
||||
apply(case_tac fault)
|
||||
apply (wp as_user_reads_respects
|
||||
det_zipWithM_x
|
||||
set_register_det
|
||||
handle_arch_fault_reply_reads_respects[simplified K_def]
|
||||
| simp add: reads_lrefl)+
|
||||
apply (wp as_user_reads_respects thread_get_reads_respects
|
||||
thread_get_wp' handle_arch_fault_reply_reads_respects[simplified K_def]
|
||||
| simp add: reads_lrefl det_zipWithM_x set_register_det)+
|
||||
done
|
||||
|
||||
lemma lookup_ipc_buffer_has_read_auth':
|
||||
|
|
|
|||
|
|
@ -654,6 +654,8 @@ lemma bind_notification_reads_respects:
|
|||
apply (clarsimp dest!: reads_ep)
|
||||
done
|
||||
|
||||
lemmas thread_get_reads_respects_f = reads_respects_f[OF thread_get_reads_respects, where Q="\<top>", simplified, OF thread_get_silc_inv]
|
||||
|
||||
lemma invoke_tcb_reads_respects_f:
|
||||
notes validE_valid[wp del]
|
||||
static_imp_wp [wp]
|
||||
|
|
@ -661,7 +663,7 @@ lemma invoke_tcb_reads_respects_f:
|
|||
"reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and Tcb_AI.tcb_inv_wf ti and (\<lambda>s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)"
|
||||
including no_pre
|
||||
apply(case_tac ti)
|
||||
apply(wp when_ev restart_reads_respects_f as_user_reads_respects_f static_imp_wp | simp)+
|
||||
apply(wp thread_get_reads_respects_f when_ev restart_reads_respects_f as_user_reads_respects_f static_imp_wp thread_get_wp'| simp)+
|
||||
apply(auto intro: requiv_cur_thread_eq intro!: det_zipWithM simp: det_setRegister det_getRestartPC det_setNextPC authorised_tcb_inv_def simp: reads_equiv_f_def)[1]
|
||||
apply(wp as_user_reads_respects_f suspend_silc_inv when_ev suspend_reads_respects_f[where st=st] | simp | elim conjE, assumption)+
|
||||
apply(auto simp: authorised_tcb_inv_def intro!: det_mapM[OF _ subset_refl] simp: det_getRegister simp: reads_equiv_f_def)[1]
|
||||
|
|
|
|||
|
|
@ -274,10 +274,10 @@ lemma (in Systemcall_AI_Pre) handle_fault_reply_cte_wp_at:
|
|||
apply (case_tac f)
|
||||
apply (clarsimp)+
|
||||
apply (clarsimp simp add: as_user_def)
|
||||
apply (wp set_object_cte_wp_at2 | simp add: split_def)+
|
||||
apply (wp set_object_cte_wp_at2 thread_get_wp' | simp add: split_def)+
|
||||
apply (clarsimp simp add: NC)
|
||||
apply (clarsimp simp add: as_user_def)
|
||||
apply (wp set_object_cte_wp_at2 | simp add: split_def)+
|
||||
apply (wp set_object_cte_wp_at2 thread_get_wp' | simp add: split_def)+
|
||||
apply (clarsimp simp add: NC)
|
||||
apply simp
|
||||
apply wp
|
||||
|
|
|
|||
|
|
@ -793,7 +793,7 @@ lemma bind_notification_invs:
|
|||
apply (wp valid_irq_node_typ set_ntfn_valid_objs set_notification_obj_at
|
||||
| clarsimp simp:idle_no_ex_cap)+
|
||||
apply (clarsimp simp: obj_at_def is_ntfn)
|
||||
apply (wp | clarsimp)+
|
||||
apply (wp | clarsimp)+
|
||||
apply (rule conjI, rule impI)
|
||||
apply (clarsimp simp: obj_at_def pred_tcb_at_def2)
|
||||
apply (rule impI, erule delta_sym_refs)
|
||||
|
|
|
|||
|
|
@ -2011,24 +2011,27 @@ crunch nosch[wp]: doIPCTransfer "\<lambda>s. P (ksSchedulerAction s)"
|
|||
|
||||
lemma handle_fault_reply_registers_corres:
|
||||
"corres (op =) (tcb_at t) (tcb_at' t)
|
||||
(do y \<leftarrow> as_user t
|
||||
(do t' \<leftarrow> thread_get id t;
|
||||
y \<leftarrow> as_user t
|
||||
(zipWithM_x
|
||||
(\<lambda>r v. set_register r
|
||||
(ARM.sanitiseRegister r v))
|
||||
(sanitise_register t' r v))
|
||||
msg_template msg);
|
||||
return (label = 0)
|
||||
od)
|
||||
(do y \<leftarrow> asUser t
|
||||
(do t' \<leftarrow> threadGet id t;
|
||||
y \<leftarrow> asUser t
|
||||
(zipWithM_x
|
||||
(\<lambda>r v. setRegister r (ARM_H.sanitiseRegister r v))
|
||||
(\<lambda>r v. setRegister r (sanitiseRegister t' r v))
|
||||
msg_template msg);
|
||||
return (label = 0)
|
||||
od)"
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split)
|
||||
apply (rule corres_split [OF _ threadget_corres, where r'=tcb_relation])
|
||||
apply (rule corres_split)
|
||||
apply (rule corres_trivial, simp)
|
||||
apply (rule corres_as_user')
|
||||
apply(simp add: set_register_def setRegister_def
|
||||
apply(simp add: set_register_def setRegister_def sanitise_register_def
|
||||
sanitiseRegister_def syscallMessage_def)
|
||||
apply(subst zipWithM_x_modify)+
|
||||
apply(rule corres_modify')
|
||||
|
|
|
|||
|
|
@ -2637,10 +2637,8 @@ lemma schedule_corres:
|
|||
apply (rule_tac P="tcb_at cur" in corres_symb_exec_l')
|
||||
apply (rule_tac corres_symb_exec_l')
|
||||
apply simp
|
||||
apply (rule corres_assert_ret)
|
||||
apply (wp gets_exs_valid | simp)+
|
||||
apply (rule thread_get_wp')
|
||||
apply simp
|
||||
apply (rule corres_assert_ret)
|
||||
apply (wpsimp wp: thread_get_wp' gets_exs_valid)+
|
||||
apply (rule corres_split[OF _ thread_get_isRunnable_corres])
|
||||
apply (rule corres_split[OF _ corres_when])
|
||||
apply (rule corres_split[OF _ guarded_switch_to_corres])
|
||||
|
|
@ -2659,28 +2657,23 @@ lemma schedule_corres:
|
|||
apply (simp_all only: cong: if_cong Deterministic_A.scheduler_action.case_cong
|
||||
Structures_H.scheduler_action.case_cong)
|
||||
apply ((wp thread_get_wp' hoare_vcg_conj_lift hoare_drop_imps | clarsimp)+)
|
||||
thm tcbSchedEnqueue_invs'
|
||||
apply (rule conjI,simp)
|
||||
apply (clarsimp split:Deterministic_A.scheduler_action.splits
|
||||
simp: invs_psp_aligned invs_distinct invs_valid_objs
|
||||
invs_arch_state invs_arch_objs)
|
||||
apply (intro impI conjI allI tcb_at_invs | (fastforce
|
||||
simp: invs_def cur_tcb_def valid_arch_caps_def
|
||||
valid_sched_def valid_sched_action_def
|
||||
is_activatable_def st_tcb_at_def obj_at_def
|
||||
valid_state_def only_idle_def valid_etcbs_def
|
||||
weak_valid_sched_action_def
|
||||
not_cur_thread_def tcb_at_invs
|
||||
))+
|
||||
apply (clarsimp split: Deterministic_A.scheduler_action.splits
|
||||
simp: invs_psp_aligned invs_distinct invs_valid_objs invs_arch_state invs_arch_objs)
|
||||
apply (intro impI conjI allI tcb_at_invs |
|
||||
(fastforce simp: invs_def cur_tcb_def valid_arch_caps_def valid_etcbs_def
|
||||
valid_sched_def valid_sched_action_def is_activatable_def
|
||||
st_tcb_at_def obj_at_def valid_state_def only_idle_def
|
||||
weak_valid_sched_action_def not_cur_thread_def tcb_at_invs))+
|
||||
apply (cut_tac s = s in valid_blocked_valid_blocked_except)
|
||||
prefer 2
|
||||
apply (simp add:valid_sched_def)
|
||||
apply (simp add:valid_sched_def)
|
||||
apply simp
|
||||
by (fastforce simp: invs'_def cur_tcb'_def valid_state'_def st_tcb_at'_def
|
||||
sch_act_wf_def valid_pspace'_def valid_objs'_maxDomain
|
||||
valid_objs'_maxPriority comp_def
|
||||
split: scheduler_action.splits)
|
||||
sch_act_wf_def valid_pspace'_def valid_objs'_maxDomain
|
||||
valid_objs'_maxPriority comp_def
|
||||
split: scheduler_action.splits)
|
||||
|
||||
lemma ssa_all_invs_but_ct_not_inQ':
|
||||
"\<lbrace>all_invs_but_ct_not_inQ' and sch_act_wf sa and
|
||||
|
|
|
|||
|
|
@ -327,24 +327,25 @@ lemma writereg_corres:
|
|||
(invokeTCB (tcbinvocation.WriteRegisters dest resume values arch'))"
|
||||
apply (simp add: invokeTCB_def performTransfer_def
|
||||
frameRegisters_def gpRegisters_def
|
||||
sanitiseRegister_def)
|
||||
sanitiseRegister_def sanitise_register_def)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split [OF _ gct_corres])
|
||||
apply (rule corres_split_nor)
|
||||
prefer 2
|
||||
apply (rule corres_as_user)
|
||||
apply (simp add: zipWithM_mapM getRestartPC_def setNextPC_def)
|
||||
apply (rule corres_Id, simp+)
|
||||
apply (rule no_fail_pre, wp no_fail_mapM)
|
||||
apply clarsimp
|
||||
apply (wp no_fail_setRegister | simp)+
|
||||
apply (rule corres_split_nor)
|
||||
apply (rule_tac P=\<top> and P'=\<top> in corres_inst)
|
||||
apply simp
|
||||
apply (rule corres_when [OF refl])
|
||||
apply (rule restart_corres)
|
||||
apply (wp static_imp_wp | clarsimp simp: invs'_def valid_state'_def
|
||||
dest!: global'_no_ex_cap)+
|
||||
apply (rule corres_split [OF _ threadget_corres, where r'=tcb_relation])
|
||||
apply (rule corres_split_nor)
|
||||
prefer 2
|
||||
apply (rule corres_as_user)
|
||||
apply (simp add: zipWithM_mapM getRestartPC_def setNextPC_def)
|
||||
apply (rule corres_Id, simp+)
|
||||
apply (rule no_fail_pre, wp no_fail_mapM)
|
||||
apply clarsimp
|
||||
apply (wp no_fail_setRegister | simp)+
|
||||
apply (rule corres_split_nor)
|
||||
apply (rule_tac P=\<top> and P'=\<top> in corres_inst)
|
||||
apply simp
|
||||
apply (rule corres_when [OF refl])
|
||||
apply (rule restart_corres)
|
||||
apply (wp static_imp_wp | clarsimp simp: invs'_def valid_state'_def
|
||||
dest!: global'_no_ex_cap)+
|
||||
done
|
||||
|
||||
crunch it[wp]: suspend "\<lambda>s. P (ksIdleThread s)"
|
||||
|
|
|
|||
|
|
@ -25,5 +25,12 @@ definition
|
|||
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"
|
||||
where
|
||||
"sanitise_register t r v \<equiv> case r of
|
||||
CPSR \<Rightarrow> (v && 0xf8000000) || 0x150
|
||||
| _ \<Rightarrow> v"
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
|||
|
|
@ -171,14 +171,16 @@ fun
|
|||
where
|
||||
"handle_fault_reply (CapFault cptr rp lf) thread x y = return True"
|
||||
| "handle_fault_reply (UnknownSyscallException n) thread label msg = do
|
||||
t \<leftarrow> thread_get id thread;
|
||||
as_user thread $ zipWithM_x
|
||||
(\<lambda>r v. set_register r $ sanitiseRegister r v)
|
||||
(\<lambda>r v. set_register r $ sanitise_register t r v)
|
||||
syscallMessage msg;
|
||||
return (label = 0)
|
||||
od"
|
||||
| "handle_fault_reply (UserException exception code) thread label msg = do
|
||||
t \<leftarrow> thread_get id thread;
|
||||
as_user thread $ zipWithM_x
|
||||
(\<lambda>r v. set_register r $ sanitiseRegister r v)
|
||||
(\<lambda>r v. set_register r $ sanitise_register t r v)
|
||||
exceptionMessage msg;
|
||||
return (label = 0)
|
||||
od"
|
||||
|
|
|
|||
|
|
@ -23,6 +23,7 @@ context begin interpretation Arch .
|
|||
requalify_consts
|
||||
arch_activate_idle_thread
|
||||
arch_tcb_set_ipc_buffer
|
||||
sanitise_register
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -219,8 +220,9 @@ where
|
|||
| "invoke_tcb (WriteRegisters dest resume_target values arch) =
|
||||
(liftE $ do
|
||||
self \<leftarrow> gets cur_thread;
|
||||
t \<leftarrow> thread_get id dest;
|
||||
as_user dest $ do
|
||||
zipWithM (\<lambda>r v. setRegister r (sanitiseRegister r v))
|
||||
zipWithM (\<lambda>r v. setRegister r (sanitise_register t r v))
|
||||
(frameRegisters @ gpRegisters) values;
|
||||
pc \<leftarrow> getRestartPC;
|
||||
setNextPC pc
|
||||
|
|
|
|||
|
|
@ -25,6 +25,14 @@ performTransfer :: "copy_register_sets \<Rightarrow> machine_word \<Rightarrow>
|
|||
where
|
||||
"performTransfer arg1 arg2 arg3 \<equiv> return ()"
|
||||
|
||||
definition
|
||||
sanitiseRegister :: "tcb \<Rightarrow> register \<Rightarrow> machine_word \<Rightarrow> machine_word"
|
||||
where
|
||||
"sanitiseRegister x0 x1 v\<equiv> (case x1 of
|
||||
CPSR \<Rightarrow> (v && 0xf8000000) || 0x150
|
||||
| _ \<Rightarrow> v
|
||||
)"
|
||||
|
||||
|
||||
|
||||
definition
|
||||
|
|
|
|||
|
|
@ -105,13 +105,6 @@ tpidrurwRegister :: "register"
|
|||
where
|
||||
"tpidrurwRegister \<equiv> Register ARM.tpidrurwRegister"
|
||||
|
||||
definition
|
||||
sanitiseRegister :: "register \<Rightarrow> machine_word \<Rightarrow> machine_word"
|
||||
where
|
||||
"sanitiseRegister x0 x1\<equiv> (case (x0, x1) of
|
||||
(((* Register *) r), ((* Word *) w)) \<Rightarrow> Word $ ARM.sanitiseRegister r w
|
||||
)"
|
||||
|
||||
|
||||
definition
|
||||
PPtr :: "machine_word \<Rightarrow> machine_word"
|
||||
|
|
|
|||
|
|
@ -89,14 +89,16 @@ defs handleFaultReply_def:
|
|||
"handleFaultReply x0 thread label msg\<equiv> (case x0 of
|
||||
(CapFault _ _ _) \<Rightarrow> return True
|
||||
| (UnknownSyscallException _) \<Rightarrow> (do
|
||||
t \<leftarrow> threadGet id thread;
|
||||
asUser thread $ zipWithM_x
|
||||
(\<lambda> r v. setRegister r $ sanitiseRegister r v)
|
||||
(\<lambda> r v. setRegister r $ sanitiseRegister t r v)
|
||||
syscallMessage msg;
|
||||
return (label = 0)
|
||||
od)
|
||||
| (UserException _ _) \<Rightarrow> (do
|
||||
t \<leftarrow> threadGet id thread;
|
||||
asUser thread $ zipWithM_x
|
||||
(\<lambda> r v. setRegister r $ sanitiseRegister r v)
|
||||
(\<lambda> r v. setRegister r $ sanitiseRegister t r v)
|
||||
exceptionMessage msg;
|
||||
return (label = 0)
|
||||
od)
|
||||
|
|
|
|||
|
|
@ -129,5 +129,8 @@ threadSet :: "(tcb \<Rightarrow> tcb) \<Rightarrow> machine_word \<Rightarrow> u
|
|||
consts'
|
||||
asUser :: "machine_word \<Rightarrow> 'a user_monad \<Rightarrow> 'a kernel"
|
||||
|
||||
consts'
|
||||
sanitiseRegister :: "tcb \<Rightarrow> register \<Rightarrow> machine_word \<Rightarrow> machine_word"
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -374,8 +374,9 @@ defs invokeTCB_def:
|
|||
withoutPreemption $ (do
|
||||
self \<leftarrow> getCurThread;
|
||||
performTransfer arch self dest;
|
||||
t \<leftarrow> threadGet id dest;
|
||||
asUser dest $ (do
|
||||
zipWithM (\<lambda> r v. setRegister r (sanitiseRegister r v))
|
||||
zipWithM (\<lambda> r v. setRegister r (sanitiseRegister t r v))
|
||||
(frameRegisters @ gpRegisters) values;
|
||||
pc \<leftarrow> getRestartPC;
|
||||
setNextPC pc
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ requalify_consts
|
|||
fromVPtr
|
||||
end
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Object/TCB.lhs Arch= bodies_only NOT liftFnMaybe assertDerived archThreadGet archThreadSet asUser
|
||||
#INCLUDE_HASKELL SEL4/Object/TCB.lhs Arch= bodies_only NOT liftFnMaybe assertDerived archThreadGet archThreadSet asUser sanitiseRegister
|
||||
|
||||
defs asUser_def:
|
||||
"asUser tptr f\<equiv> (do
|
||||
|
|
|
|||
|
|
@ -1,9 +1,8 @@
|
|||
Built from git repo at /Users/kleing/verification/l4v/spec/haskell by kleing
|
||||
|
||||
Generated from changeset:
|
||||
d08ee04 haskell: update documentation for building the Haskell kernel
|
||||
697758d provide TCB argument for sanitiseRegister
|
||||
|
||||
|
||||
Warning - uncomitted changes used:
|
||||
M ../design/version
|
||||
M src/SEL4.lhs
|
||||
|
|
|
|||
|
|
@ -32,7 +32,6 @@ This is the top-level module; it defines the interface between the kernel and th
|
|||
> import SEL4.Object.TCB(asUser)
|
||||
> import SEL4.Object.Interrupt(handleInterrupt)
|
||||
> import Control.Monad.Error
|
||||
> import Control.Monad.State
|
||||
> import Data.Maybe
|
||||
|
||||
\subsection{Kernel Entry Point}
|
||||
|
|
@ -50,3 +49,4 @@ faults, and system calls; the set of possible events is defined in
|
|||
> when (isJust irq) $ handleInterrupt (fromJust irq))
|
||||
> schedule
|
||||
> activateThread
|
||||
|
||||
|
|
|
|||
|
|
@ -64,14 +64,16 @@ This function returns "True" if the faulting thread should be restarted after th
|
|||
> handleFaultReply (CapFault {}) _ _ _ = return True
|
||||
>
|
||||
> handleFaultReply (UnknownSyscallException _) thread label msg = do
|
||||
> t <- threadGet id thread
|
||||
> asUser thread $ zipWithM_
|
||||
> (\r v -> setRegister r $ sanitiseRegister r v)
|
||||
> (\r v -> setRegister r $ sanitiseRegister t r v)
|
||||
> syscallMessage msg
|
||||
> return (label == 0)
|
||||
|
||||
> handleFaultReply (UserException _ _) thread label msg = do
|
||||
> t <- threadGet id thread
|
||||
> asUser thread $ zipWithM_
|
||||
> (\r v -> setRegister r $ sanitiseRegister r v)
|
||||
> (\r v -> setRegister r $ sanitiseRegister t r v)
|
||||
> exceptionMessage msg
|
||||
> return (label == 0)
|
||||
|
||||
|
|
|
|||
|
|
@ -160,11 +160,6 @@ Functions are provided to get and set a single register.
|
|||
> setRegister :: Register -> Word -> UserMonad ()
|
||||
> setRegister r v = modify $ UC . (//[(r, v)]) . fromUC
|
||||
|
||||
On some architectures, the thread context may include registers that may be modified by user level code, but cannot safely be given arbitrary values. For example, some of the bits in the ARM architecture's CPSR are used for conditional execution, and others enable kernel mode. This function is used to filter out any bits that should not be modified by user level programs.
|
||||
|
||||
> sanitiseRegister :: Register -> Word -> Word
|
||||
> sanitiseRegister (Register r) (Word w) = Word $ Arch.sanitiseRegister r w
|
||||
|
||||
\subsubsection{Miscellaneous}
|
||||
|
||||
The "mask" function is a trivial function which, given a number of bits, returns a word with that number of low-order bits set.
|
||||
|
|
|
|||
|
|
@ -16,7 +16,6 @@ This module defines the ARM register set.
|
|||
|
||||
> import qualified Data.Word
|
||||
> import Data.Array
|
||||
> import Data.Bits
|
||||
|
||||
\end{impdetails}
|
||||
|
||||
|
|
@ -40,8 +39,4 @@ This module defines the ARM register set.
|
|||
> initContext :: [(Register, Word)]
|
||||
> initContext = [(CPSR,0x150)] -- User mode
|
||||
|
||||
> sanitiseRegister :: Register -> Word -> Word
|
||||
> sanitiseRegister CPSR v = (v .&. 0xf8000000) .|. 0x150
|
||||
> sanitiseRegister _ v = v
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ This module uses the C preprocessor to select a target architecture.
|
|||
\end{impdetails}
|
||||
|
||||
> module SEL4.Object.TCB (
|
||||
> threadGet, threadSet, asUser,
|
||||
> threadGet, threadSet, asUser, sanitiseRegister,
|
||||
> getThreadCSpaceRoot, getThreadVSpaceRoot,
|
||||
> getThreadReplySlot, getThreadCallerSlot,
|
||||
> getThreadBufferSlot,
|
||||
|
|
@ -466,8 +466,9 @@ The "ReadRegisters" and "WriteRegisters" functions are similar to "CopyRegisters
|
|||
> withoutPreemption $ do
|
||||
> self <- getCurThread
|
||||
> Arch.performTransfer arch self dest
|
||||
> t <- threadGet id dest
|
||||
> asUser dest $ do
|
||||
> zipWithM (\r v -> setRegister r (sanitiseRegister r v))
|
||||
> zipWithM (\r v -> setRegister r (sanitiseRegister t r v))
|
||||
> (frameRegisters ++ gpRegisters) values
|
||||
> pc <- getRestartPC
|
||||
> setNextPC pc
|
||||
|
|
@ -757,3 +758,8 @@ identified by "tcbPtr".
|
|||
> threadSet (\tcb -> tcb { tcbArch = atcbContextSet uc' (tcbArch tcb) }) tptr
|
||||
> return a
|
||||
|
||||
On some architectures, the thread context may include registers that may be modified by user level code, but cannot safely be given arbitrary values. For example, some of the bits in the ARM architecture's CPSR are used for conditional execution, and others enable kernel mode. This function is used to filter out any bits that should not be modified by user level programs.
|
||||
|
||||
> sanitiseRegister :: TCB -> Register -> Word -> Word
|
||||
> sanitiseRegister t (Register r) (Word w) = Word $ Arch.sanitiseRegister t r w
|
||||
|
||||
|
|
|
|||
|
|
@ -16,11 +16,14 @@ There are presently no ARM-specific register subsets defined, but in future this
|
|||
|
||||
\begin{impdetails}
|
||||
|
||||
> import SEL4.Machine
|
||||
> import SEL4.Machine(PPtr)
|
||||
> import SEL4.Model
|
||||
> import SEL4.Object.Structures
|
||||
> import SEL4.API.Failures
|
||||
> import SEL4.API.Invocation.ARM
|
||||
> import SEL4.Machine.RegisterSet.ARM
|
||||
> import Data.Bits
|
||||
|
||||
|
||||
> import Data.Word(Word8)
|
||||
|
||||
|
|
@ -32,3 +35,7 @@ There are presently no ARM-specific register subsets defined, but in future this
|
|||
> performTransfer :: CopyRegisterSets -> PPtr TCB -> PPtr TCB -> Kernel ()
|
||||
> performTransfer _ _ _ = return ()
|
||||
|
||||
> sanitiseRegister :: TCB -> Register -> Word -> Word
|
||||
> sanitiseRegister _ CPSR v = (v .&. 0xf8000000) .|. 0x150
|
||||
> sanitiseRegister _ _ v = v
|
||||
|
||||
|
|
|
|||
|
|
@ -54,9 +54,6 @@ type_synonym machine_word = "word32"
|
|||
consts'
|
||||
initContext :: "(register * machine_word) list"
|
||||
|
||||
consts'
|
||||
sanitiseRegister :: "register \<Rightarrow> machine_word \<Rightarrow> machine_word"
|
||||
|
||||
(*<*)
|
||||
|
||||
section "Machine Words"
|
||||
|
|
@ -171,12 +168,6 @@ definition
|
|||
defs initContext_def:
|
||||
"initContext\<equiv> [(CPSR,0x150)]"
|
||||
|
||||
defs sanitiseRegister_def:
|
||||
"sanitiseRegister x0 v\<equiv> (case x0 of
|
||||
CPSR \<Rightarrow> (v && 0xf8000000) || 0x150
|
||||
| _ \<Rightarrow> v
|
||||
)"
|
||||
|
||||
|
||||
section "Machine State"
|
||||
|
||||
|
|
|
|||
|
|
@ -35,7 +35,6 @@ requalify_consts
|
|||
getRestartPC
|
||||
setRegister
|
||||
getRegister
|
||||
sanitiseRegister
|
||||
initContext
|
||||
exceptionMessage
|
||||
syscallMessage
|
||||
|
|
|
|||
Loading…
Reference in New Issue