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

ARM refine: proof update for user_context refactor

This commit is contained in:
Gerwin Klein 2018-03-01 08:56:28 +11:00
parent 8601dce656
commit 2d9de5b9a6
4 changed files with 20 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
proof/refine/ARM/Bits_R.thy
View File

@ -48,8 +48,7 @@ end
crunch_ignore (add:
storeWordVM loadWord setRegister getRegister getRestartPC
debugPrint set_register get_register
setNextPC maskInterrupt clearMemory throw_on_false)
debugPrint setNextPC maskInterrupt clearMemory throw_on_false)
crunch_ignore (add: unifyFailure ignoreFailure)

4
proof/refine/ARM/Ipc_R.thy
View File

@ -2014,7 +2014,7 @@ lemma handle_fault_reply_registers_corres:
(do t' \<leftarrow> arch_get_sanitise_register_info t;
y \<leftarrow> as_user t
(zipWithM_x
(\<lambda>r v. set_register r
(\<lambda>r v. setRegister r
(sanitise_register t' r v))
msg_template msg);
return (label = 0)
@ -2031,7 +2031,7 @@ lemma handle_fault_reply_registers_corres:
apply (rule corres_split)
apply (rule corres_trivial, simp)
apply (rule corres_as_user')
apply(simp add: set_register_def setRegister_def sanitise_register_def
apply(simp add: setRegister_def sanitise_register_def
sanitiseRegister_def syscallMessage_def)
apply(subst zipWithM_x_modify)+
apply(rule corres_modify')

17
proof/refine/ARM/TcbAcc_R.thy
View File

@ -1576,9 +1576,9 @@ qed
lemma user_getreg_corres:
"corres op = (tcb_at t) (tcb_at' t)
(as_user t (get_register r)) (asUser t (getRegister r))"
(as_user t (getRegister r)) (asUser t (getRegister r))"
apply (rule corres_as_user')
apply (clarsimp simp: get_register_def getRegister_def)
apply (clarsimp simp: getRegister_def)
done
lemma user_getreg_inv'[wp]:
@ -1741,9 +1741,9 @@ lemma no_fail_asUser [wp]:
lemma user_setreg_corres:
"corres dc (tcb_at t)
(tcb_at' t)
(as_user t (set_register r v))
(as_user t (setRegister r v))
(asUser t (setRegister r v))"
apply (simp add: set_register_def setRegister_def)
apply (simp add: setRegister_def)
apply (rule corres_as_user')
apply (rule corres_modify'; simp)
done
@ -3708,7 +3708,8 @@ lemma get_mrs_corres:
have S: "get = gets id"
by (simp add: gets_def)
have T: "corres (\<lambda>con regs. regs = map con msg_registers) (tcb_at t) (tcb_at' t)
(thread_get (arch_tcb_context_get o tcb_arch) t) (asUser t (mapM getRegister ARM_H.msgRegisters))"
(thread_get (arch_tcb_get_registers o tcb_arch) t) (asUser t (mapM getRegister ARM_H.msgRegisters))"
unfolding arch_tcb_get_registers_def
apply (subst thread_get_as_user)
apply (rule corres_as_user')
apply (subst mapM_gets)
@ -3827,7 +3828,7 @@ proof -
show ?thesis using m
unfolding setMRs_def set_mrs_def
apply (clarsimp cong: option.case_cong split del: if_split)
apply (clarsimp simp: arch_tcb_set_registers_def arch_tcb_get_registers_def cong: option.case_cong split del: if_split)
apply (subst bind_assoc[symmetric])
apply (fold thread_set_def[simplified])
apply (subst thread_set_as_user[where f="\<lambda>context. \<lambda>reg.
@ -3886,8 +3887,8 @@ proof -
have as_user_bit:
"\<And>v :: word32. corres dc (tcb_at s and tcb_at r) (tcb_at' s and tcb_at' r)
(mapM
(\<lambda>ra. do v \<leftarrow> as_user s (get_register ra);
as_user r (set_register ra v)
(\<lambda>ra. do v \<leftarrow> as_user s (getRegister ra);
as_user r (setRegister ra v)
od)
(take (unat n) msg_registers))
(mapM

19
proof/refine/ARM/Tcb_R.thy
View File

@ -402,8 +402,8 @@ proof -
have Q: "\<And>src src' des des' r r'. \<lbrakk> src = src'; des = des' \<rbrakk> \<Longrightarrow>
corres dc (tcb_at src and tcb_at des and invs)
(tcb_at' src' and tcb_at' des' and invs')
(do v \<leftarrow> as_user src (get_register r);
as_user des (set_register r' v)
(do v \<leftarrow> as_user src (getRegister r);
as_user des (setRegister r' v)
od)
(do v \<leftarrow> asUser src' (getRegister r);
asUser des' (setRegister r' v)
@ -411,7 +411,7 @@ proof -
apply clarsimp
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (simp add: set_register_def setRegister_def)
apply (simp add: setRegister_def)
apply (rule corres_as_user)
apply (rule corres_modify')
apply simp
@ -422,8 +422,8 @@ proof -
have R: "\<And>src src' des des' xs ys. \<lbrakk> src = src'; des = des'; xs = ys \<rbrakk> \<Longrightarrow>
corres dc (tcb_at src and tcb_at des and invs)
(tcb_at' src' and tcb_at' des' and invs')
(mapM_x (\<lambda>r. do v \<leftarrow> as_user src (get_register r);
as_user des (set_register r v)
(mapM_x (\<lambda>r. do v \<leftarrow> as_user src (getRegister r);
as_user des (setRegister r v)
od) xs)
(mapM_x (\<lambda>r'. do v \<leftarrow> asUser src' (getRegister r');
asUser des' (setRegister r' v)
@ -433,9 +433,6 @@ proof -
apply (rule Q)
apply (clarsimp simp: set_zip_same | wp)+
done
have S: "get_register = getRegister" "set_register = setRegister"
by (rule ext | simp add: get_register_def getRegister_def
set_register_def setRegister_def)+
have U: "\<And>t. corres dc (tcb_at t and invs) (tcb_at' t and invs')
(do pc \<leftarrow> as_user t getRestartPC; as_user t (setNextPC pc) od)
(do pc \<leftarrow> asUser t getRestartPC; asUser t (setNextPC pc) od)"
@ -459,7 +456,7 @@ proof -
apply simp
apply (wp static_imp_wp)+
apply (rule corres_when[OF refl])
apply (rule R[unfolded S, OF refl refl])
apply (rule R[OF refl refl])
apply (simp add: gpRegisters_def)
apply (rule_tac Q="\<lambda>_. einvs and tcb_at dest" in hoare_strengthen_post[rotated])
apply (clarsimp simp: invs_def valid_sched_weak_strg valid_sched_def)
@ -470,8 +467,8 @@ proof -
apply (rule corres_when[OF refl])
apply (rule corres_split_nor)
apply (simp add: getRestartPC_def setNextPC_def dc_def[symmetric])
apply (rule Q[unfolded S, OF refl refl])
apply (rule R[unfolded S, OF refl refl])
apply (rule Q[OF refl refl])
apply (rule R[OF refl refl])
apply (simp add: frame_registers_def frameRegisters_def)
apply ((wp mapM_x_wp' static_imp_wp, simp+)+)[2]
apply (wp mapM_x_wp' static_imp_wp, simp+)