From 2d9de5b9a61965b93fe0181972004bee90ca9fc1 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 1 Mar 2018 08:56:28 +1100 Subject: [PATCH] ARM refine: proof update for user_context refactor --- proof/refine/ARM/Bits_R.thy | 3 +-- proof/refine/ARM/Ipc_R.thy | 4 ++-- proof/refine/ARM/TcbAcc_R.thy | 17 +++++++++-------- proof/refine/ARM/Tcb_R.thy | 19 ++++++++----------- 4 files changed, 20 insertions(+), 23 deletions(-) diff --git a/proof/refine/ARM/Bits_R.thy b/proof/refine/ARM/Bits_R.thy index 2b949b7c9..9656eff3f 100644 --- a/proof/refine/ARM/Bits_R.thy +++ b/proof/refine/ARM/Bits_R.thy @@ -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) diff --git a/proof/refine/ARM/Ipc_R.thy b/proof/refine/ARM/Ipc_R.thy index f5a9a7ec1..5d1ae3f5b 100644 --- a/proof/refine/ARM/Ipc_R.thy +++ b/proof/refine/ARM/Ipc_R.thy @@ -2014,7 +2014,7 @@ lemma handle_fault_reply_registers_corres: (do t' \ arch_get_sanitise_register_info t; y \ as_user t (zipWithM_x - (\r v. set_register r + (\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') diff --git a/proof/refine/ARM/TcbAcc_R.thy b/proof/refine/ARM/TcbAcc_R.thy index f2d3bd194..6f6ce68fb 100644 --- a/proof/refine/ARM/TcbAcc_R.thy +++ b/proof/refine/ARM/TcbAcc_R.thy @@ -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 (\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="\context. \reg. @@ -3886,8 +3887,8 @@ proof - have as_user_bit: "\v :: word32. corres dc (tcb_at s and tcb_at r) (tcb_at' s and tcb_at' r) (mapM - (\ra. do v \ as_user s (get_register ra); - as_user r (set_register ra v) + (\ra. do v \ as_user s (getRegister ra); + as_user r (setRegister ra v) od) (take (unat n) msg_registers)) (mapM diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy index e09abcee7..0ab45b505 100644 --- a/proof/refine/ARM/Tcb_R.thy +++ b/proof/refine/ARM/Tcb_R.thy @@ -402,8 +402,8 @@ proof - have Q: "\src src' des des' r r'. \ src = src'; des = des' \ \ corres dc (tcb_at src and tcb_at des and invs) (tcb_at' src' and tcb_at' des' and invs') - (do v \ as_user src (get_register r); - as_user des (set_register r' v) + (do v \ as_user src (getRegister r); + as_user des (setRegister r' v) od) (do v \ 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: "\src src' des des' xs ys. \ src = src'; des = des'; xs = ys \ \ corres dc (tcb_at src and tcb_at des and invs) (tcb_at' src' and tcb_at' des' and invs') - (mapM_x (\r. do v \ as_user src (get_register r); - as_user des (set_register r v) + (mapM_x (\r. do v \ as_user src (getRegister r); + as_user des (setRegister r v) od) xs) (mapM_x (\r'. do v \ 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: "\t. corres dc (tcb_at t and invs) (tcb_at' t and invs') (do pc \ as_user t getRestartPC; as_user t (setNextPC pc) od) (do pc \ 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="\_. 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+)