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

VER-717: refactor tpidrurwRegister and fix corresponding proof

This commit is contained in:
Pang Luo 2017-04-24 10:02:53 +10:00
parent 71e2db88a4
commit da28d94974
8 changed files with 40 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
proof/crefine/ARM/Tcb_C.thy
View File

@ -558,6 +558,16 @@ lemma cteInsert_cap_to'2:
apply auto
done
lemma archSetIPCBuffer_ccorres:
"ccorres dc xfdc \<top> (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr target} \<inter> {s. bufferAddr_' s = buf}) []
(asUser target $ setTCBIPCBuffer buf)
(Call Arch_setTCBIPCBuffer_'proc)"
apply (cinit lift: thread_' bufferAddr_')
apply (simp add: setTCBIPCBuffer_def)
apply (ctac add: setRegister_ccorres[simplified dc_def])
apply (clarsimp simp: ARM_H.tpidrurwRegister_def ARM.tpidrurwRegister_def)
done
lemma invokeTCB_ThreadControl_ccorres:
"ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and sch_act_simple
@ -659,7 +669,7 @@ lemma invokeTCB_ThreadControl_ccorres:
apply (rule ball_tcb_cte_casesI, simp+)
apply (clarsimp simp: ctcb_relation_def option_to_0_def)
apply (rule ceqv_refl)
apply (ctac)
apply (ctac(no_vcg) add: archSetIPCBuffer_ccorres[simplified])
apply csymbr
apply (simp add: ccorres_cond_iffs Collect_False split_def
del: Collect_const)
@ -709,7 +719,6 @@ lemma invokeTCB_ThreadControl_ccorres:
simp add: o_def)
apply (wp static_imp_wp )
apply (wp hoare_drop_imp)
apply vcg
apply (rule_tac P="is_aligned (fst (the buf)) msg_align_bits"
in hoare_gen_asm)
apply (wp threadSet_ipcbuffer_trivial static_imp_wp | simp )+
@ -3680,7 +3689,6 @@ lemma decodeBindNotification_ccorres:
\<inter> {s. excaps_' s = extraCaps'}) []
(decodeBindNotification cp extraCaps >>= invocationCatch thread isBlocking isCall InvokeTCB)
(Call decodeBindNotification_'proc)"
using [[goals_limit=1]]
apply (simp, rule ccorres_gen_asm)
apply (cinit lift: cap_' excaps_' simp: decodeBindNotification_def)
apply (simp add: bind_assoc whenE_def bind_bindE_assoc interpret_excaps_test_null

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

@ -1080,12 +1080,19 @@ definition valid_tcb_invocation :: "tcbinvocation \<Rightarrow> bool" where
ThreadControl _ _ _ mcp p _ _ _ \<Rightarrow> valid_option_prio p \<and> valid_option_prio mcp
| _ \<Rightarrow> True"
lemma arch_tcb_set_ipc_buffer_corres:
"corres dc (tcb_at target) (tcb_at' target) (arch_tcb_set_ipc_buffer target ptr) (asUser target $ setTCBIPCBuffer ptr)"
apply (simp add: setTCBIPCBuffer_def ARM_H.tpidrurwRegister_def ARM.tpidrurwRegister_def)
apply (rule user_setreg_corres)
done
lemma tc_corres:
assumes x: "newroot_rel e e'" and y: "newroot_rel f f'" and p: "p = p'" and mcp: "mcp = mcp'"
and z: "(case g of None \<Rightarrow> g' = None
| Some (vptr, g'') \<Rightarrow> \<exists>g'''. g' = Some (vptr, g''')
\<and> newroot_rel g'' g''')"
and sl: "{e, f, option_map undefined g} \<noteq> {None} \<longrightarrow> sl' = cte_map slot"
notes arch_tcb_set_ipc_buffer_def[simp del]
shows
"corres (intr \<oplus> op =)
(einvs and simple_sched_action and tcb_at a and
@ -1214,7 +1221,7 @@ proof -
(\<lambda>ptr frame.
doE cap_delete (a, tcb_cnode_index 4);
do y \<leftarrow> thread_set (tcb_ipc_buffer_update (\<lambda>_. ptr)) a;
y \<leftarrow> as_user a (set_register TPIDRURW ptr);
y \<leftarrow> arch_tcb_set_ipc_buffer a ptr;
liftE $
case_option (return ())
(case_prod
@ -1231,7 +1238,7 @@ proof -
do bufferSlot \<leftarrow> getThreadBufferSlot a;
doE y \<leftarrow> cteDelete bufferSlot True;
do y \<leftarrow> threadSet (tcbIPCBuffer_update (\<lambda>_. ptr)) a;
y \<leftarrow> asUser a (setRegister ARM_H.tpidrurwRegister ptr);
y \<leftarrow> asUser a $ setTCBIPCBuffer ptr;
liftE
(case_option (return ())
(case_prod
@ -1258,8 +1265,7 @@ proof -
apply (rule corres_split_norE)
apply (rule corres_split_nor)
apply (rule corres_split')
apply (simp add: ARM_H.tpidrurwRegister_def ARM.tpidrurwRegister_def)
apply (rule user_setreg_corres)
apply (rule arch_tcb_set_ipc_buffer_corres[simplified])
apply (rule corres_trivial)
apply simp
apply wp+
@ -1277,12 +1283,11 @@ proof -
in corres_gen_asm)
apply (rule corres_split_nor)
apply (rule corres_split[rotated])
apply (simp add: ARM_H.tpidrurwRegister_def ARM.tpidrurwRegister_def)
apply (rule user_setreg_corres)
apply (rule arch_tcb_set_ipc_buffer_corres[simplified])
prefer 3
apply simp
apply (erule checked_insert_corres)
apply wp+
apply (wp | simp add: arch_tcb_set_ipc_buffer_def)+
apply (rule threadset_corres,
simp add: tcb_relation_def, (simp add: exst_same_def)+)
apply (wp thread_set_tcb_ipc_buffer_cap_cleared_invs

5
spec/design/ARM/ArchTCB_H.thy
View File

@ -38,6 +38,11 @@ getSanitiseRegisterInfo :: "machine_word \<Rightarrow> bool kernel"
where
"getSanitiseRegisterInfo arg1 \<equiv> return False"
definition
setTCBIPCBuffer :: "vptr \<Rightarrow> unit user_monad"
where
"setTCBIPCBuffer ptr \<equiv> setRegister tpidrurwRegister $ fromVPtr ptr"
definition

3
spec/design/TCB_H.thy
View File

@ -37,6 +37,7 @@ requalify_consts
msgRegisters
tpidrurwRegister
fromVPtr
setTCBIPCBuffer
end
defs decodeTCBInvocation_def:
@ -325,7 +326,7 @@ defs invokeTCB_def:
cteDelete bufferSlot True;
withoutPreemption $ threadSet
(\<lambda> t. t \<lparr>tcbIPCBuffer := ptr\<rparr>) target;
withoutPreemption $ asUser target $ setRegister tpidrurwRegister $ fromVPtr ptr;
withoutPreemption $ asUser target $ setTCBIPCBuffer ptr;
withoutPreemption $ (case frame of
Some (newCap, srcSlot) \<Rightarrow>
checkCapAt newCap srcSlot

1
spec/design/skel/TCB_H.thy
View File

@ -35,6 +35,7 @@ requalify_consts
msgRegisters
tpidrurwRegister
fromVPtr
setTCBIPCBuffer
end
#INCLUDE_HASKELL SEL4/Object/TCB.lhs Arch= bodies_only NOT liftFnMaybe assertDerived archThreadGet archThreadSet asUser sanitiseRegister getSanitiseRegisterInfo

28
spec/design/version
View File

@ -1,37 +1,15 @@
Built from git repo at /home/joelb/work/bump/l4v/spec/haskell by joelb
Built from git repo at /home/pang/repos/v/l4v/spec/haskell by pang
Generated from changeset:
3e87113 arm crefine: fix breakages after sanitiseRegister change
71e2db88a arm: refactor sanitise_register to take a bool instead of a kernel_object
Warning - uncomitted changes used:
M ../../proof/crefine/ARM/Ipc_C.thy
M ../../proof/crefine/ARM/Tcb_C.thy
M ../../proof/invariant-abstract/ARM/ArchBCorres2_AI.thy
M ../../proof/invariant-abstract/ARM/ArchDetSchedDomainTime_AI.thy
M ../../proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy
M ../../proof/invariant-abstract/ARM/ArchDeterministic_AI.thy
M ../../proof/invariant-abstract/ARM/ArchIpc_AI.thy
M ../../proof/invariant-abstract/ARM/ArchSyscall_AI.thy
M ../../proof/invariant-abstract/ARM/ArchTcb_AI.thy
M ../../proof/invariant-abstract/BCorres2_AI.thy
M ../../proof/invariant-abstract/DetSchedDomainTime_AI.thy
M ../../proof/invariant-abstract/DetSchedSchedule_AI.thy
M ../../proof/invariant-abstract/Deterministic_AI.thy
M ../../proof/invariant-abstract/Ipc_AI.thy
M ../../proof/invariant-abstract/Syscall_AI.thy
M ../../proof/invariant-abstract/Tcb_AI.thy
M ../../proof/refine/ARM/Ipc_R.thy
M ../../proof/refine/ARM/Tcb_R.thy
M ../abstract/ARM/ArchTcb_A.thy
M ../abstract/Ipc_A.thy
M ../abstract/Tcb_A.thy
M ../design/ARM/ArchTCB_H.thy
M ../design/FaultHandler_H.thy
M ../design/TCBDecls_H.thy
M ../design/TCB_H.thy
M ../design/skel/TCB_H.thy
M ../design/version
M src/SEL4/API/Faults.lhs
UU ../design/version
M src/SEL4/Object/TCB.lhs
M src/SEL4/Object/TCB/ARM.lhs

2
spec/haskell/src/SEL4/Object/TCB.lhs
View File

@ -401,7 +401,7 @@ The use of "checkCapAt" addresses a corner case in which the only capability to
> cteDelete bufferSlot True
> withoutPreemption $ threadSet
> (\t -> t {tcbIPCBuffer = ptr}) target
> withoutPreemption $ asUser target $ setRegister tpidrurwRegister $ fromVPtr ptr
> withoutPreemption $ asUser target $ Arch.setTCBIPCBuffer ptr
> withoutPreemption $ case frame of
> Just (newCap, srcSlot) ->
> checkCapAt newCap srcSlot

8
spec/haskell/src/SEL4/Object/TCB/ARM.lhs
View File

@ -21,10 +21,9 @@ There are presently no ARM-specific register subsets defined, but in future this
> import SEL4.Object.Structures
> import SEL4.API.Failures
> import SEL4.API.Invocation.ARM
> import SEL4.Machine.RegisterSet.ARM
> import SEL4.Machine.RegisterSet(setRegister, tpidrurwRegister, UserMonad, VPtr(..))
> import SEL4.Machine.RegisterSet.ARM(Register(CPSR), Word)
> import Data.Bits
> import Data.Word(Word8)
\end{impdetails}
@ -42,3 +41,6 @@ There are presently no ARM-specific register subsets defined, but in future this
> getSanitiseRegisterInfo :: PPtr TCB -> Kernel Bool
> getSanitiseRegisterInfo _ = return False
> setTCBIPCBuffer :: VPtr -> UserMonad ()
> setTCBIPCBuffer ptr = setRegister tpidrurwRegister $ fromVPtr ptr