From da28d9497415973afdf2b38297fbdfbff2148700 Mon Sep 17 00:00:00 2001 From: Pang Luo Date: Mon, 24 Apr 2017 10:02:53 +1000 Subject: [PATCH] VER-717: refactor tpidrurwRegister and fix corresponding proof --- proof/crefine/ARM/Tcb_C.thy | 14 +++++++++--- proof/refine/ARM/Tcb_R.thy | 19 ++++++++++------ spec/design/ARM/ArchTCB_H.thy | 5 +++++ spec/design/TCB_H.thy | 3 ++- spec/design/skel/TCB_H.thy | 1 + spec/design/version | 28 +++--------------------- spec/haskell/src/SEL4/Object/TCB.lhs | 2 +- spec/haskell/src/SEL4/Object/TCB/ARM.lhs | 8 ++++--- 8 files changed, 40 insertions(+), 40 deletions(-) diff --git a/proof/crefine/ARM/Tcb_C.thy b/proof/crefine/ARM/Tcb_C.thy index 22e579738..dcf6f6d6b 100644 --- a/proof/crefine/ARM/Tcb_C.thy +++ b/proof/crefine/ARM/Tcb_C.thy @@ -558,6 +558,16 @@ lemma cteInsert_cap_to'2: apply auto done +lemma archSetIPCBuffer_ccorres: + "ccorres dc xfdc \ (UNIV \ {s. thread_' s = tcb_ptr_to_ctcb_ptr target} \ {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 \ (\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: \ {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 diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy index d37ad2e18..9668351b0 100644 --- a/proof/refine/ARM/Tcb_R.thy +++ b/proof/refine/ARM/Tcb_R.thy @@ -1080,12 +1080,19 @@ definition valid_tcb_invocation :: "tcbinvocation \ bool" where ThreadControl _ _ _ mcp p _ _ _ \ valid_option_prio p \ valid_option_prio mcp | _ \ 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 \ g' = None | Some (vptr, g'') \ \g'''. g' = Some (vptr, g''') \ newroot_rel g'' g''')" and sl: "{e, f, option_map undefined g} \ {None} \ sl' = cte_map slot" + notes arch_tcb_set_ipc_buffer_def[simp del] shows "corres (intr \ op =) (einvs and simple_sched_action and tcb_at a and @@ -1214,7 +1221,7 @@ proof - (\ptr frame. doE cap_delete (a, tcb_cnode_index 4); do y \ thread_set (tcb_ipc_buffer_update (\_. ptr)) a; - y \ as_user a (set_register TPIDRURW ptr); + y \ arch_tcb_set_ipc_buffer a ptr; liftE $ case_option (return ()) (case_prod @@ -1231,7 +1238,7 @@ proof - do bufferSlot \ getThreadBufferSlot a; doE y \ cteDelete bufferSlot True; do y \ threadSet (tcbIPCBuffer_update (\_. ptr)) a; - y \ asUser a (setRegister ARM_H.tpidrurwRegister ptr); + y \ 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 diff --git a/spec/design/ARM/ArchTCB_H.thy b/spec/design/ARM/ArchTCB_H.thy index 02c51e6a9..efd98285f 100644 --- a/spec/design/ARM/ArchTCB_H.thy +++ b/spec/design/ARM/ArchTCB_H.thy @@ -38,6 +38,11 @@ getSanitiseRegisterInfo :: "machine_word \ bool kernel" where "getSanitiseRegisterInfo arg1 \ return False" +definition +setTCBIPCBuffer :: "vptr \ unit user_monad" +where +"setTCBIPCBuffer ptr \ setRegister tpidrurwRegister $ fromVPtr ptr" + definition diff --git a/spec/design/TCB_H.thy b/spec/design/TCB_H.thy index 3868117e0..79f5234c2 100644 --- a/spec/design/TCB_H.thy +++ b/spec/design/TCB_H.thy @@ -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 (\ t. t \tcbIPCBuffer := ptr\) target; - withoutPreemption $ asUser target $ setRegister tpidrurwRegister $ fromVPtr ptr; + withoutPreemption $ asUser target $ setTCBIPCBuffer ptr; withoutPreemption $ (case frame of Some (newCap, srcSlot) \ checkCapAt newCap srcSlot diff --git a/spec/design/skel/TCB_H.thy b/spec/design/skel/TCB_H.thy index 161c1bd24..014d17e2f 100644 --- a/spec/design/skel/TCB_H.thy +++ b/spec/design/skel/TCB_H.thy @@ -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 diff --git a/spec/design/version b/spec/design/version index d79b1ee0b..2d285c383 100644 --- a/spec/design/version +++ b/spec/design/version @@ -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 diff --git a/spec/haskell/src/SEL4/Object/TCB.lhs b/spec/haskell/src/SEL4/Object/TCB.lhs index ea00517df..9183cc87f 100644 --- a/spec/haskell/src/SEL4/Object/TCB.lhs +++ b/spec/haskell/src/SEL4/Object/TCB.lhs @@ -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 diff --git a/spec/haskell/src/SEL4/Object/TCB/ARM.lhs b/spec/haskell/src/SEL4/Object/TCB/ARM.lhs index 315769dd2..cb06be6e6 100644 --- a/spec/haskell/src/SEL4/Object/TCB/ARM.lhs +++ b/spec/haskell/src/SEL4/Object/TCB/ARM.lhs @@ -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 +