From 9fda73732a95d96a2cd0ea6b5394c10e3c64e77f Mon Sep 17 00:00:00 2001 From: Victor Phan Date: Thu, 14 Nov 2019 18:05:24 +1100 Subject: [PATCH] x64 crefine: update for seL4 bugfix [GITHUB PR 107] Always invalidate TLB during unmapPage. --- proof/crefine/X64/VSpace_C.thy | 20 +++++--------------- 1 file changed, 5 insertions(+), 15 deletions(-) diff --git a/proof/crefine/X64/VSpace_C.thy b/proof/crefine/X64/VSpace_C.thy index 1265f7769..4cfb9228a 100644 --- a/proof/crefine/X64/VSpace_C.thy +++ b/proof/crefine/X64/VSpace_C.thy @@ -1971,22 +1971,12 @@ lemma unmapPage_ccorres: apply (rule ccorres_name_ksCurThread) apply (rule_tac val="tcb_ptr_to_ctcb_ptr rv" and xf'="\s. ksCurThread_' (globals s)" in ccorres_abstract_known, ceqv) - apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_move_c_guard_tcb_ctes)+ - apply (rule ccorres_symb_exec_r) - apply (rule ccorres_rhs_assoc2) - apply (rule ccorres_symb_exec_r_known_rv[where R=\ and R'=UNIV and xf'=ret__int_' and val=1]) - apply vcg - apply clarsimp - apply ceqv - apply ccorres_rewrite - apply (clarsimp simp: liftE_liftM) - apply (ctac add: invalidateTranslationSingleASID_ccorres[simplified dc_def]) - apply vcg - apply clarsimp - apply vcg - apply (rule conseqPre, vcg) apply clarsimp - apply (wpsimp simp: cur_tcb'_def[symmetric]) + apply ccorres_rewrite + apply (clarsimp simp: liftE_liftM) + apply (ctac add: invalidateTranslationSingleASID_ccorres[simplified dc_def]) + apply clarsimp + apply clarsimp apply (clarsimp simp: guard_is_UNIV_def conj_comms tcb_cnode_index_defs) apply (simp add: throwError_def) apply (rule ccorres_split_throws)