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

x64 crefine: update for seL4 bugfix [GITHUB PR 107] 

Always invalidate TLB during unmapPage.
This commit is contained in:
Victor Phan 2019-11-14 18:05:24 +11:00
parent 831d3b4f70
commit 9fda73732a
1 changed files with 5 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
proof/crefine/X64/VSpace_C.thy
View File

@ -1971,22 +1971,12 @@ lemma unmapPage_ccorres:
apply (rule ccorres_name_ksCurThread)
apply (rule_tac val="tcb_ptr_to_ctcb_ptr rv" and xf'="\<lambda>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=\<top> 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)