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

access-control, capDL-api, drefine, infoflow, sep-capDL, capDL: update for Isabelle2019

This commit is contained in:
Michael McInerney 2019-05-27 18:32:17 +10:00 committed by Matthew Brecknell
parent c0a2d54c15
commit 356e91c9fa
20 changed files with 238 additions and 232 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
proof/access-control/Dpolicy.thy
View File

@ -1008,6 +1008,7 @@ lemma transform_asid_low_bits_of:
lemma cap_asid'_transform:
"\<lbrakk> invs s; caps_of_state s ptr = Some cap \<rbrakk> \<Longrightarrow> cap_asid' cap = cdl_cap_asid' (transform_cap cap)"
supply image_cong_simp [cong del]
apply (case_tac cap; simp)
apply (drule caps_of_state_valid, simp)
apply (rename_tac arch_cap)

60
proof/capDL-api/CNode_DP.thy
View File

@ -81,20 +81,20 @@ lemma seL4_CNode_Mint_sep:
\<guillemotleft>root_tcb_id \<mapsto>f tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(* Root CNode. *)
\<comment> \<open>Root CNode.\<close>
cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
(* Client cnode. *)
\<comment> \<open>Client cnode.\<close>
dest_id \<mapsto>f CNode (empty_cnode dest_size) \<and>*
(* Cap to the root CNode. *)
\<comment> \<open>Cap to the root CNode.\<close>
(root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
(* Cap to the client CNode. *)
\<comment> \<open>Cap to the client CNode.\<close>
(cnode_id, dest_root_slot) \<mapsto>c dest_root_cap \<and>*
(* Cap that the root task has to it's own CNode. *)
\<comment> \<open>Cap that the root task has to its own CNode.\<close>
(cnode_id, cnode_cap_slot) \<mapsto>c cnode_cap' \<and>*
(* Cap to be copied, in the root CNode. *)
\<comment> \<open>Cap to be copied, in the root CNode.\<close>
(cnode_id, src_slot) \<mapsto>c src_cap \<and>*
(* Where to copy the cap (in the client CNode). *)
\<comment> \<open>Where to copy the cap (in the client CNode).\<close>
(dest_id, dest_slot) \<mapsto>c NullCap \<and>*
R\<guillemotright> s \<and>
@ -103,7 +103,7 @@ lemma seL4_CNode_Mint_sep:
one_lvl_lookup cnode_cap' (unat src_depth) root_size \<and>
one_lvl_lookup dest_root_cap (unat dest_depth) dest_size \<and>
(* We need some word invariants *)
\<comment> \<open>We need some word invariants\<close>
unat src_depth \<le> word_bits \<and>
0 < unat src_depth \<and>
unat dest_depth \<le> word_bits \<and>
@ -118,12 +118,12 @@ lemma seL4_CNode_Mint_sep:
guard_equal cnode_cap dest_root word_bits \<and>
(* Caps point to the right objects. *)
\<comment> \<open>Caps point to the right objects.\<close>
cap_object cnode_cap = cnode_id \<and>
cap_object cnode_cap' = cnode_id \<and>
cap_object dest_root_cap = dest_id \<and>
(* Cap slots match their cptrs. *)
\<comment> \<open>Cap slots match their cptrs.\<close>
dest_root_slot = offset dest_root root_size \<and>
cnode_cap_slot = offset src_root root_size \<and>
src_slot = offset src_index root_size \<and>
@ -261,20 +261,20 @@ lemma seL4_CNode_Mutate_sep:
root_tcb_id \<mapsto>f tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>*
(* Root CNode. *)
\<comment> \<open>Root CNode.\<close>
cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
(* Client cnode. *)
\<comment> \<open>Client cnode.\<close>
dest_id \<mapsto>f CNode (empty_cnode dest_size) \<and>*
(* Cap to the root CNode. *)
\<comment> \<open>Cap to the root CNode.\<close>
(root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
(* Cap to the client CNode. *)
\<comment> \<open>Cap to the client CNode.\<close>
(cnode_id, dest_root_slot) \<mapsto>c dest_root_cap \<and>*
(* Cap that the root task has to it's own CNode. *)
\<comment> \<open>Cap that the root task has to its own CNode.\<close>
(cnode_id, cnode_cap_slot) \<mapsto>c cnode_cap' \<and>*
(* Cap to be copied, in the root CNode. *)
\<comment> \<open>Cap to be copied, in the root CNode.\<close>
(cnode_id, src_slot) \<mapsto>c src_cap \<and>*
(* Where to copy the cap (in the client CNode). *)
\<comment> \<open>Where to copy the cap (in the client CNode).\<close>
(dest_id, dest_slot) \<mapsto>c NullCap \<and>*
R\<guillemotright> s \<and>
@ -282,7 +282,7 @@ lemma seL4_CNode_Mutate_sep:
one_lvl_lookup cnode_cap' (unat src_depth) root_size \<and>
one_lvl_lookup dest_root_cap (unat dest_depth) dest_size \<and>
(* We need some word invariants *)
\<comment> \<open>We need some word invariants\<close>
unat src_depth \<le> word_bits \<and>
0 < unat src_depth \<and>
unat dest_depth \<le> word_bits \<and>
@ -297,12 +297,12 @@ lemma seL4_CNode_Mutate_sep:
guard_equal dest_root_cap dest_index (unat dest_depth ) \<and>
guard_equal cnode_cap src_root word_bits \<and>
guard_equal cnode_cap dest_root word_bits \<and>
(* Caps point to the right objects. *)
\<comment> \<open>Caps point to the right objects.\<close>
cap_object cnode_cap = cnode_id \<and>
cap_object cnode_cap' = cnode_id \<and>
cap_object dest_root_cap = dest_id \<and>
(* Cap slots match their cptrs. *)
\<comment> \<open>Cap slots match their cptrs.\<close>
dest_root_slot = offset dest_root root_size \<and>
cnode_cap_slot = offset src_root root_size \<and>
src_slot = offset src_index root_size \<and>
@ -426,20 +426,20 @@ lemma seL4_CNode_Move_sep:
root_tcb_id \<mapsto>f tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>*
(* Root CNode. *)
\<comment> \<open>Root CNode.\<close>
cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
(* Client cnode. *)
\<comment> \<open>Client cnode.\<close>
dest_id \<mapsto>f CNode (empty_cnode dest_size) \<and>*
(* Cap to the root CNode. *)
\<comment> \<open>Cap to the root CNode.\<close>
(root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
(* Cap to the client CNode. *)
\<comment> \<open>Cap to the client CNode.\<close>
(cnode_id, dest_root_slot) \<mapsto>c dest_root_cap \<and>*
(* Cap that the root task has to it's own CNode. *)
\<comment> \<open>Cap that the root task has to its own CNode.\<close>
(cnode_id, cnode_cap_slot) \<mapsto>c cnode_cap' \<and>*
(* Cap to be copied, in the root CNode. *)
\<comment> \<open>Cap to be copied, in the root CNode.\<close>
(cnode_id, src_slot) \<mapsto>c src_cap \<and>*
(* Where to copy the cap (in the client CNode). *)
\<comment> \<open>Where to copy the cap (in the client CNode).\<close>
(dest_id, dest_slot) \<mapsto>c NullCap \<and>*
R\<guillemotright> s \<and>
@ -447,7 +447,7 @@ lemma seL4_CNode_Move_sep:
one_lvl_lookup cnode_cap' (unat src_depth) root_size \<and>
one_lvl_lookup dest_root_cap (unat dest_depth) dest_size \<and>
(* We need some word invariants *)
\<comment> \<open>We need some word invariants\<close>
unat src_depth \<le> word_bits \<and>
0 < unat src_depth \<and>
unat dest_depth \<le> word_bits \<and>
@ -463,12 +463,12 @@ lemma seL4_CNode_Move_sep:
guard_equal cnode_cap src_root word_bits \<and>
guard_equal cnode_cap dest_root word_bits \<and>
(* Caps point to the right objects. *)
\<comment> \<open>Caps point to the right objects.\<close>
cap_object cnode_cap = cnode_id \<and>
cap_object cnode_cap' = cnode_id \<and>
cap_object dest_root_cap = dest_id \<and>
(* Cap slots match their cptrs. *)
\<comment> \<open>Cap slots match their cptrs.\<close>
dest_root_slot = offset dest_root root_size \<and>
cnode_cap_slot = offset src_root root_size \<and>
src_slot = offset src_index root_size \<and>

20
proof/capDL-api/IRQ_DP.thy
View File

@ -175,9 +175,9 @@ shows "\<lbrace>\<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>* (root_t
seL4_IRQControl_Get control_cap irq croot node_index node_depth
\<lbrace>\<lambda>fail s. \<guillemotleft> root_tcb_id \<mapsto>f root_tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(* Root CNode. *)
\<comment> \<open>Root CNode.\<close>
cap_object root_cap \<mapsto>f CNode (empty_cnode root_size) \<and>*
(* Cap to the root CNode. *)
\<comment> \<open>Cap to the root CNode.\<close>
(root_tcb_id, tcb_cspace_slot) \<mapsto>c root_cap \<and>*
irq \<mapsto>irq obj \<and>* control_ptr \<mapsto>c c_cap \<and>* target_ptr \<mapsto>c irq_cap \<and>* root_ptr \<mapsto>c root_cap \<and>* R\<guillemotright> s\<rbrace>"
apply (simp add: seL4_IRQControl_Get_def sep_state_projection2_def)
@ -282,10 +282,10 @@ lemma seL4_IRQHandler_IRQControl_Get:
\<lbrace>\<lambda>fail.
\<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(* Cap to the root CNode. *)
\<comment> \<open>Cap to the root CNode.\<close>
(root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
irq \<mapsto>irq irq_id \<and>*
(* Root CNode. *)
\<comment> \<open>Root CNode.\<close>
cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
(cnode_id, control_index) \<mapsto>c IrqControlCap \<and>*
(cnode_id, root_index) \<mapsto>c cnode_cap \<and>*
@ -321,9 +321,9 @@ shows "\<lbrace>\<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>* (root_t
\<lbrace>\<lambda>fail s. \<guillemotleft> root_tcb_id \<mapsto>f root_tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(* Root CNode. *)
\<comment> \<open>Root CNode.\<close>
cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
(* Cap to the root CNode. *)
\<comment> \<open>Cap to the root CNode.\<close>
(root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
(endpoint_ptr) \<mapsto>c endpoint_cap \<and>*
irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c endpoint_cap \<and>* irq_ptr \<mapsto>c irq_cap \<and>* R\<guillemotright> s\<rbrace>"
@ -406,9 +406,9 @@ lemma obj_tcb_simps [simp]:
lemma seL4_IRQHandler_SetEndpoint_wp:
"\<lbrace>\<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(* Root CNode. *)
\<comment> \<open>Root CNode.\<close>
cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
(* Cap to the root CNode. *)
\<comment> \<open>Cap to the root CNode.\<close>
(root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
(cnode_id, endpoint_slot) \<mapsto>c endpoint_cap \<and>*
irq \<mapsto>irq irq_id \<and>*
@ -431,9 +431,9 @@ lemma seL4_IRQHandler_SetEndpoint_wp:
seL4_IRQHandler_SetEndpoint irq_handler_cptr endpoint_cptr
\<lbrace>\<lambda>fail. \<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(* Root CNode. *)
\<comment> \<open>Root CNode.\<close>
cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
(* Cap to the root CNode. *)
\<comment> \<open>Cap to the root CNode.\<close>
(root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
(cnode_id, endpoint_slot) \<mapsto>c endpoint_cap \<and>*
irq \<mapsto>irq irq_id \<and>*

4
proof/capDL-api/Kernel_DP.thy
View File

@ -66,7 +66,7 @@ definition
call_kernel_loop :: "event \<Rightarrow> unit k_monad"
where
"call_kernel_loop ev = do
(* Deal with the event. *)
\<comment> \<open>Deal with the event.\<close>
whileLoop (\<lambda>rv s. isLeft rv)
(\<lambda>_. handle_event ev
<handle> (\<lambda> _. do handle_pending_interrupts; throwError PreemptError od)
@ -96,7 +96,7 @@ where
ndomain \<leftarrow> gets cdl_current_domain;
assert (minBound = ndomain);
has_error \<leftarrow> thread_has_error thread_ptr;
(* capDL will need to be extended to support return types. *)
\<comment> \<open>capDL will need to be extended to support return types.\<close>
when (check_error) (assert (\<not> has_error));
return has_error
od"

30
proof/capDL-api/TCB_DP.thy
View File

@ -930,7 +930,7 @@ shows
is_cnode_cap cnode_cap;
buffer_addr \<noteq> 0;
cap_has_object tcb_cap;
(* Caps point to the right objects. *)
\<comment> \<open>Caps point to the right objects.\<close>
one_lvl_lookup cnode_cap word_bits root_size;
guard_equal cnode_cap tcb_root word_bits;
guard_equal cnode_cap cspace_root word_bits;
@ -952,23 +952,23 @@ shows
\<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(* Root CNode. *)
\<comment> \<open>Root CNode.\<close>
cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
(* Cap to the root CNode. *)
\<comment> \<open>Cap to the root CNode.\<close>
(root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
(* Cap that the root task has to it's own CNode. *)
\<comment> \<open>Cap that the root task has to its own CNode.\<close>
(cnode_id, cnode_cap_slot) \<mapsto>c cnode_cap' \<and>*
(* TCB's stuff *)
\<comment> \<open>TCB's stuff\<close>
tcb_id \<mapsto>f Tcb tcb \<and>*
(* Where to copy the cap from (in the client CNode). *)
\<comment> \<open>Where to copy the cap from (in the client CNode).\<close>
(cnode_id, tcb_cap_slot) \<mapsto>c tcb_cap \<and>*
(cnode_id, cspace_slot) \<mapsto>c cspace_cap \<and>*
(cnode_id, vspace_slot) \<mapsto>c vspace_cap \<and>*
(cnode_id, buffer_frame_slot) \<mapsto>c buffer_frame_cap \<and>*
(* Cap to the TCB. *)
\<comment> \<open>Cap to the TCB.\<close>
(tcb_id, tcb_cspace_slot) \<mapsto>c NullCap \<and>*
(tcb_id, tcb_vspace_slot) \<mapsto>c NullCap \<and>*
(tcb_id, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>*
@ -989,23 +989,23 @@ shows
\<lbrace>\<lambda>rv s. \<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>*
(root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
(* Root CNode. *)
\<comment> \<open>Root CNode.\<close>
cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
(* Cap to the root CNode. *)
\<comment> \<open>Cap to the root CNode.\<close>
(root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
(* Cap that the root task has to it's own CNode. *)
\<comment> \<open>Cap that the root task has to its own CNode.\<close>
(cnode_id, cnode_cap_slot) \<mapsto>c cnode_cap' \<and>*
(* TCB's stuff *)
\<comment> \<open>TCB's stuff\<close>
tcb_id \<mapsto>f Tcb new_tcb_fields \<and>*
(* Where to copy the cap from (in the client CNode). *)
\<comment> \<open>Where to copy the cap from (in the client CNode).\<close>
(cnode_id, tcb_cap_slot) \<mapsto>c tcb_cap \<and>*
(cnode_id, cspace_slot) \<mapsto>c cspace_cap \<and>*
(cnode_id, vspace_slot) \<mapsto>c vspace_cap \<and>*
(cnode_id, buffer_frame_slot) \<mapsto>c buffer_frame_cap \<and>*
(* Cap to the TCB. *)
\<comment> \<open>Cap to the TCB.\<close>
(tcb_id, tcb_cspace_slot) \<mapsto>c (cdl_update_cnode_cap_data cspace_cap cspace_root_data)\<and>*
(tcb_id, tcb_vspace_slot) \<mapsto>c vspace_cap \<and>*
(tcb_id, tcb_ipcbuffer_slot) \<mapsto>c buffer_frame_cap \<and>*
@ -1200,7 +1200,7 @@ lemma restart_cdl_current_thread:
lemma seL4_TCB_WriteRegisters_wp:
"\<lbrakk> is_cnode_cap cnode_cap;
(* Caps point to the right objects. *)
\<comment> \<open>Caps point to the right objects.\<close>
one_lvl_lookup cnode_cap word_bits root_size;
guard_equal cnode_cap tcb_ref word_bits;
is_tcb root_tcb;
@ -1282,7 +1282,7 @@ done
lemma seL4_TCB_Resume_wp:
"\<lbrakk> is_cnode_cap cnode_cap;
(* Caps point to the right objects. *)
\<comment> \<open>Caps point to the right objects.\<close>
one_lvl_lookup cnode_cap word_bits root_size;
guard_equal cnode_cap tcb_ref word_bits;
is_tcb root_tcb;

2
proof/drefine/Ipc_DR.thy
View File

@ -1952,7 +1952,7 @@ lemma corres_complete_ipc_transfer:
(valid_objs and pspace_aligned and valid_global_refs and pspace_distinct and valid_mdb
and (\<lambda>s. not_idle_thread (cur_thread s) s) and valid_irq_node
and valid_idle and not_idle_thread recv and not_idle_thread send and valid_etcbs)
(Endpoint_D.do_ipc_transfer ep' send recv can_grant) (* FIXME argument order *)
(Endpoint_D.do_ipc_transfer ep' send recv can_grant) \<comment> \<open>FIXME argument order\<close>
(Ipc_A.do_ipc_transfer send ep badge can_grant recv)"
apply (clarsimp simp: Endpoint_D.do_ipc_transfer_def Ipc_A.do_ipc_transfer_def)
apply (rule dcorres_expand_pfx)

2
proof/drefine/Untyped_DR.thy
View File

@ -1082,7 +1082,7 @@ lemma retype_addrs_range_subset_strong:
shows "\<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk>
\<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1}"
apply (clarsimp simp: retype_addrs_def ptr_add_def)
apply (drule_tac p = pa in range_cover_subset)
apply (drule_tac p = x in range_cover_subset)
apply clarsimp+
apply blast
done

36
proof/infoflow/ADT_IF.thy
View File

@ -355,14 +355,16 @@ begin
lemma enabled:
"enabled_system A s0"
supply image_cong_simp [cong del]
supply ex_image_cong_iff [simp del]
apply (clarsimp simp: enabled_system_def)
apply (rename_tac jsa, induct_tac jsa rule: rev_induct)
apply (clarsimp simp: execution_def steps_def)
apply (clarsimp simp: execution_def steps_def)
apply (fold steps_def)
apply (rule_tac x="Fin A x" in exI)
apply (rule_tac x="Fin A x" in exI)
apply (rule imageI)
apply (rule Init_Fin)
apply (rule set_mp)
apply (rule set_mp)
apply (rule inv_holds_steps[OF I])
apply (rule s0_I)
apply simp
@ -467,6 +469,8 @@ begin
lemma enabled:
"enabled_system A s0"
supply image_cong_simp [cong del]
supply ex_image_cong_iff [simp del]
apply (clarsimp simp: enabled_system_def)
apply (induct_tac jsa rule: rev_induct)
apply (clarsimp simp: execution_def steps_def)
@ -735,43 +739,43 @@ definition global_automaton_if
where
"global_automaton_if get_active_irqf do_user_opf kernel_callf
preemptionf schedulef kernel_exitf \<equiv>
(* Kernel entry with preemption during event handling
NOTE: kernel cannot be preempted while servicing an interrupt *)
\<comment> \<open>Kernel entry with preemption during event handling
NOTE: kernel cannot be preempted while servicing an interrupt\<close>
{ ( (s, KernelEntry e),
(s', KernelPreempted) ) |s s' e. (s, True, s') \<in> kernel_callf e \<and>
e \<noteq> Interrupt} \<union>
(* kernel entry without preemption during event handling *)
\<comment> \<open>kernel entry without preemption during event handling\<close>
{ ( (s, KernelEntry e),
(s', KernelSchedule (e = Interrupt)) ) |s s' e. (s, False, s') \<in> kernel_callf e } \<union>
(* handle in-kernel preemption *)
\<comment> \<open>handle in-kernel preemption\<close>
{ ( (s, KernelPreempted),
(s', KernelSchedule True) ) |s s'. (s, (), s') \<in> preemptionf } \<union>
(* schedule *)
\<comment> \<open>schedule\<close>
{ ( (s, KernelSchedule b),
(s', KernelExit) ) |s s' b. (s, (), s') \<in> schedulef } \<union>
(* kernel exit *)
\<comment> \<open>kernel exit\<close>
{ ( (s, KernelExit),
(s', m) ) |s s' m. (s, m, s') \<in> kernel_exitf } \<union>
(* User runs, causes exception *)
\<comment> \<open>User runs, causes exception\<close>
{ ( (s, InUserMode),
(s', KernelEntry e ) ) |s s_aux s' e.
(s, None, s_aux) \<in> get_active_irqf \<and>
(s_aux, Some e, s') \<in> do_user_opf \<and>
e \<noteq> Interrupt} \<union>
(* User runs, no exception happens *)
\<comment> \<open>User runs, no exception happens\<close>
{ ( (s, InUserMode),
(s', InUserMode) ) |s s_aux s'.
(s, None, s_aux) \<in> get_active_irqf \<and>
(s_aux, None, s') \<in> do_user_opf} \<union>
(* Interrupt while in user mode *)
\<comment> \<open>Interrupt while in user mode\<close>
{ ( (s, InUserMode),
(s', KernelEntry Interrupt) ) |s s' i.
(s, Some i, s') \<in> get_active_irqf} \<union>
(* Interrupt while in idle mode *)
\<comment> \<open>Interrupt while in idle mode\<close>
{ ( (s, InIdleMode),
(s', KernelEntry Interrupt) ) |s s' i.
(s, Some i, s') \<in> get_active_irqf} \<union>
(* No interrupt while in idle mode *)
\<comment> \<open>No interrupt while in idle mode\<close>
{ ( (s, InIdleMode),
(s', InIdleMode) ) |s s'. (s, None, s') \<in> get_active_irqf}"
@ -3881,7 +3885,7 @@ lemma LI_sub_big_steps:
apply (clarsimp simp: LI_def)
apply (erule_tac x=e in allE)
apply (clarsimp simp: rel_semi_def)
apply (drule_tac x="(t', ta)" in set_mp)
apply (drule_tac c="(t', ta)" in set_mp)
apply (rule_tac b=s' in relcompI)
apply simp
apply (rule sub_big_steps_I_holds)
@ -3921,7 +3925,7 @@ lemma LI_big_steps:
apply (clarsimp simp: LI_def)
apply (erule_tac x=a in allE)
apply (clarsimp simp: rel_semi_def)
apply (drule_tac x="(t', s')" in set_mp)
apply (drule_tac c="(t', s')" in set_mp)
apply (rule_tac b="s'a" in relcompI)
apply simp
apply simp

2
proof/infoflow/Retype_IF.thy
View File

@ -671,7 +671,7 @@ lemma retype_region_globals_equiv:
apply(clarsimp simp: pspace_no_overlap_def)
apply(drule_tac x="arm_global_pd (arch_state sa)" in spec)
apply(clarsimp simp: invs_def valid_state_def valid_global_objs_def valid_vso_at_def obj_at_def ptr_add_def)
apply(frule_tac p=p in range_cover_subset)
apply(frule_tac p=x in range_cover_subset)
apply(simp add: blah)
apply simp
apply(frule range_cover_subset')

28
proof/infoflow/UserOp_IF.thy
View File

@ -56,47 +56,47 @@ definition do_user_op_if
where
"do_user_op_if uop tc =
do
(* Get the page rights of each address (ReadOnly, ReadWrite, None, etc). *)
\<comment> \<open>Get the page rights of each address (ReadOnly, ReadWrite, None, etc).\<close>
pr \<leftarrow> gets ptable_rights_s;
(* Fetch the 'execute never' bits of the current thread's page mappings. *)
\<comment> \<open>Fetch the 'execute never' bits of the current thread's page mappings.\<close>
pxn \<leftarrow> gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s s x);
(* Get the mapping from virtual to physical addresses. *)
\<comment> \<open>Get the mapping from virtual to physical addresses.\<close>
pl \<leftarrow> gets (\<lambda>s. restrict_map (ptable_lift_s s) {x. pr x \<noteq> {}});
allow_read \<leftarrow> return {y. EX x. pl x = Some y \<and> AllowRead \<in> pr x};
allow_write \<leftarrow> return {y. EX x. pl x = Some y \<and> AllowWrite \<in> pr x};
(* Get the current thread. *)
\<comment> \<open>Get the current thread.\<close>
t \<leftarrow> gets cur_thread;
(* Generate user memory by throwing away anything from global
* memory that the user doesn't have access to. (The user must
* have both (1) a mapping to the page; (2) that mapping has the
* AllowRead right. *)
\<comment> \<open>Generate user memory by throwing away anything from global
memory that the user doesn't have access to. (The user must
have both (1) a mapping to the page; (2) that mapping has the
AllowRead right.\<close>
um \<leftarrow> gets (\<lambda>s. (user_mem s) \<circ> ptrFromPAddr);
dm \<leftarrow> gets (\<lambda>s. (device_mem s) \<circ> ptrFromPAddr);
ds \<leftarrow> gets (device_state \<circ> machine_state);
es \<leftarrow> do_machine_op getExMonitor;
(* Non-deterministically execute one of the user's operations. *)
\<comment> \<open>Non-deterministically execute one of the user's operations.\<close>
u \<leftarrow> return (uop t pl pr pxn (tc, um|`allow_read, (ds \<circ> ptrFromPAddr)|` allow_read, es));
assert (u \<noteq> {});
(e,(tc',um',ds',es')) \<leftarrow> select u;
(* Update the changes the user made to memory into our model.
* We ignore changes that took place where they didn't have
* write permissions. (uop shouldn't be doing that --- if it is,
* uop isn't correctly modelling real hardware.) *)
\<comment> \<open>Update the changes the user made to memory into our model.
We ignore changes that took place where they didn't have
write permissions. (uop shouldn't be doing that --- if it is,
uop isn't correctly modelling real hardware.)\<close>
do_machine_op (user_memory_update
(((um' |` allow_write) \<circ> addrFromPPtr) |` (-(dom ds))));
do_machine_op (device_memory_update
(((ds' |` allow_write) \<circ> addrFromPPtr) |` (dom ds)));
(* Update exclusive monitor state used by the thread. *)
\<comment> \<open>Update exclusive monitor state used by the thread.\<close>
do_machine_op (setExMonitor es');
return (e,tc')

6
proof/sep-capDL/Lookups_D.thy
View File

@ -32,7 +32,7 @@ where
"resolve_cap cnode_cap cap_ptr remaining_size =
(if is_cnode_cap cnode_cap
then DO
(* Fetch the next level CNode. *)
\<comment> \<open>Fetch the next level CNode.\<close>
cnode \<leftarrow> opt_cnode $ cap_object cnode_cap;
radix_size \<leftarrow> oreturn $ cdl_cnode_size_bits cnode;
guard_size \<leftarrow> oreturn $ cap_guard_size cnode_cap;
@ -40,13 +40,13 @@ where
level_size \<leftarrow> oreturn (radix_size + guard_size);
oassert (level_size \<noteq> 0);
(* Ensure the guard matches up. *)
\<comment> \<open>Ensure the guard matches up.\<close>
guard \<leftarrow> oreturn $ (cap_ptr >> (remaining_size-guard_size)) && (mask guard_size);
if \<not>(guard_size \<le> remaining_size \<and> guard = cap_guard) \<or>
level_size > remaining_size
then othrow FaultError
else DO
(* Find the next slot. *)
\<comment> \<open>Find the next slot.\<close>
offset \<leftarrow> oreturn $ (cap_ptr >> (remaining_size-level_size)) && (mask radix_size);
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (remaining_size - level_size);

14
spec/capDL/Asid_D.thy
View File

@ -28,14 +28,14 @@ where
doE
base \<leftarrow> liftE $ select {x. x < 2 ^ asid_high_bits};
(* Fetch the untyped item, and ensure it is valid. *)
\<comment> \<open>Fetch the untyped item, and ensure it is valid.\<close>
(untyped_cap, untyped_cap_ref) \<leftarrow> throw_on_none $ get_index caps 0;
(case untyped_cap of
UntypedCap _ s _ \<Rightarrow> returnOk ()
| _ \<Rightarrow> throw);
ensure_no_children untyped_cap_ref;
(* Fetch the slot we plan to put the generated cap into. *)
\<comment> \<open>Fetch the slot we plan to put the generated cap into.\<close>
(cspace_cap, _) \<leftarrow> throw_on_none $ get_index caps 1;
target_slot \<leftarrow> lookup_slot_for_cnode_op cspace_cap index (unat depth);
ensure_empty target_slot;
@ -70,21 +70,21 @@ where
case params of
MakePool untyped_cap untyped_cap_ref untyped_covers target_slot base \<Rightarrow>
do
(* Untype the region. A choice may be made about whether to detype
objects with Untyped addresses. *)
\<comment> \<open>Untype the region. A choice may be made about whether to detype
objects with Untyped addresses.\<close>
modify (detype untyped_covers);
set_cap untyped_cap_ref untyped_cap;
targets \<leftarrow> generate_object_ids 1 AsidPoolType untyped_covers;
(* Retype the region. *)
\<comment> \<open>Retype the region.\<close>
retype_region 0 AsidPoolType targets;
assert (targets \<noteq> []);
(* Insert the cap. *)
\<comment> \<open>Insert the cap.\<close>
frame \<leftarrow> return $ pick (hd targets);
insert_cap_child (AsidPoolCap frame base) untyped_cap_ref target_slot;
(* Update the asid table. *)
\<comment> \<open>Update the asid table.\<close>
asid_table \<leftarrow> gets cdl_asid_table;
asid_table' \<leftarrow> return $ asid_table (base \<mapsto> AsidPoolCap frame 0);
modify (\<lambda>s. s \<lparr>cdl_asid_table := asid_table'\<rparr>)

36
spec/capDL/CNode_D.thy
View File

@ -42,7 +42,7 @@ where
returnOk $ InsertCall cap src_slot dest_slot
odE
(* Copy a cap to another capslot, possibly modifying the cap. *)
\<comment> \<open>Copy a cap to another capslot, possibly modifying the cap.\<close>
| CNodeMintIntent dest_index dest_depth src_index src_depth rights badge \<Rightarrow>
doE
(src_root, _) \<leftarrow> throw_on_none $ get_index caps 0;
@ -51,7 +51,7 @@ where
src_slot \<leftarrow> lookup_slot_for_cnode_op src_root src_index (unat src_depth);
src_cap \<leftarrow> liftE $ get_cap src_slot;
(* Munge the caps rights/data. *)
\<comment> \<open>Munge the caps rights/data.\<close>
new_cap \<leftarrow> returnOk $ update_cap_rights (cap_rights src_cap \<inter> rights) src_cap;
new_cap' \<leftarrow> liftE $ update_cap_data False badge new_cap;
@ -61,7 +61,7 @@ where
returnOk $ InsertCall cap src_slot dest_slot
odE
(* Move a cap to another capslot, without modifying the cap. *)
\<comment> \<open>Move a cap to another capslot, without modifying the cap.\<close>
| CNodeMoveIntent dest_index dest_depth src_index src_depth \<Rightarrow>
doE
(src_root, _) \<leftarrow> throw_on_none $ get_index caps 0;
@ -73,7 +73,7 @@ where
returnOk $ MoveCall src_cap src_slot dest_slot
odE
(* Move a cap to another capslot, possibly modifying the cap. *)
\<comment> \<open>Move a cap to another capslot, possibly modifying the cap.\<close>
| CNodeMutateIntent dest_index dest_depth src_index src_depth badge \<Rightarrow>
doE
(src_root, _) \<leftarrow> throw_on_none $ get_index caps 0;
@ -82,28 +82,28 @@ where
src_slot \<leftarrow> lookup_slot_for_cnode_op src_root src_index (unat src_depth);
src_cap \<leftarrow> liftE $ get_cap src_slot;
(* Munge the caps rights/data. *)
\<comment> \<open>Munge the caps rights/data.\<close>
cap \<leftarrow> liftE $ update_cap_data True badge src_cap;
whenE (cap = NullCap) throw;
returnOk $ MoveCall cap src_slot dest_slot
odE
(* Revoke all CDT children of the given cap. *)
\<comment> \<open>Revoke all CDT children of the given cap.\<close>
| CNodeRevokeIntent index depth \<Rightarrow>
doE
target_slot \<leftarrow> lookup_slot_for_cnode_op target index (unat depth);
returnOk $ RevokeCall target_slot
odE
(* Delete the given cap, but not its children. *)
\<comment> \<open>Delete the given cap, but not its children.\<close>
| CNodeDeleteIntent index depth \<Rightarrow>
doE
target_slot \<leftarrow> lookup_slot_for_cnode_op target index (unat depth);
returnOk $ DeleteCall target_slot
odE
(* Save the current thread's reply cap into the target slot. *)
\<comment> \<open>Save the current thread's reply cap into the target slot.\<close>
| CNodeSaveCallerIntent index depth \<Rightarrow>
doE
target_slot \<leftarrow> lookup_slot_for_cnode_op target index (unat depth);
@ -111,7 +111,7 @@ where
returnOk $ SaveCall target_slot
odE
(* Recycle the target cap. *)
\<comment> \<open>Recycle the target cap.\<close>
| CNodeCancelBadgedSendsIntent index depth \<Rightarrow>
doE
target_slot \<leftarrow> lookup_slot_for_cnode_op target index (unat depth);
@ -120,7 +120,7 @@ where
returnOk $ CancelBadgedSendsCall cap
odE
(* Atomically move several caps. *)
\<comment> \<open>Atomically move several caps.\<close>
| CNodeRotateIntent dest_index dest_depth pivot_index pivot_depth pivot_badge src_index src_depth src_badge \<Rightarrow>
doE
pivot_root \<leftarrow> throw_on_none $ get_index caps 0;
@ -144,7 +144,7 @@ where
pivot_cap \<leftarrow> liftE $ get_cap pivot_slot;
whenE (pivot_cap = NullCap) throw;
(* Munge caps. *)
\<comment> \<open>Munge caps.\<close>
new_src \<leftarrow> liftE $ update_cap_data True src_badge src_cap;
new_pivot \<leftarrow> liftE $ update_cap_data True pivot_badge pivot_cap;
@ -159,26 +159,26 @@ definition
invoke_cnode :: "cdl_cnode_invocation \<Rightarrow> unit preempt_monad"
where
"invoke_cnode params \<equiv> case params of
(* Insert a new cap. *)
\<comment> \<open>Insert a new cap.\<close>
InsertCall cap src_slot dest_slot \<Rightarrow>
liftE $
insert_cap_sibling cap src_slot dest_slot
\<sqinter>
insert_cap_child cap src_slot dest_slot
(* Move a cap, possibly modifying it in the process. *)
\<comment> \<open>Move a cap, possibly modifying it in the process.\<close>
| MoveCall cap src_slot dest_slot \<Rightarrow>
liftE $ move_cap cap src_slot dest_slot
(* Revoke a cap. *)
\<comment> \<open>Revoke a cap.\<close>
| RevokeCall src_slot \<Rightarrow>
revoke_cap src_slot
(* Delete a cap. *)
\<comment> \<open>Delete a cap.\<close>
| DeleteCall src_slot \<Rightarrow>
delete_cap src_slot
(* Atomically move two capabilities. *)
\<comment> \<open>Atomically move two capabilities.\<close>
| RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow>
liftE $ if slot1 = slot3 then
swap_cap cap1 slot1 cap2 slot2
@ -188,7 +188,7 @@ where
move_cap cap1 slot1 slot2
od
(* Save a reply cap from the caller's TCB into this CNode. *)
\<comment> \<open>Save a reply cap from the caller's TCB into this CNode.\<close>
| SaveCall dest_slot \<Rightarrow>
liftE $ do
current \<leftarrow> gets_the cdl_current_thread;
@ -197,7 +197,7 @@ where
$ move_cap replycap (current, tcb_caller_slot) dest_slot
od
(* Reset an object into its original state. *)
\<comment> \<open>Reset an object into its original state.\<close>
| CancelBadgedSendsCall (EndpointCap ep b _) \<Rightarrow> liftE $ when (b \<noteq> 0) $ cancel_badged_sends ep b
| CancelBadgedSendsCall _ \<Rightarrow> fail
"

28
spec/capDL/Decode_D.thy
View File

@ -116,8 +116,8 @@ definition
where
"decode_invocation invoked_cap invoked_cap_ref caps intent \<equiv>
case invoked_cap of
(* For endpoint-like caps, we always perform an operation,
* regardless of the user's actual intent. *)
\<comment> \<open>For endpoint-like caps, we always perform an operation,
regardless of the user's actual intent.\<close>
EndpointCap o_id badge rights \<Rightarrow>
(if Write \<in> rights then
returnOk $ InvokeEndpoint (SyncMessage badge (Grant \<in> rights) (GrantReply \<in> rights) o_id)
@ -131,17 +131,17 @@ where
| ReplyCap o_id rights \<Rightarrow>
returnOk $ InvokeReply (ReplyMessage o_id invoked_cap_ref (Grant \<in> rights))
(*
* For other operations, we only perform the user's intent
* if it matches up with the cap.
*
* Note that this does not currently match the current
* implementation: instead, the user's message will be
* decoded into a new (undefined) intent for what the
* cap happened to be. I propose modifying labels used to
* avoid overlaps between different items so that we can
* recognise when the user is invoking the wrong item.
*)
\<comment> \<open>
For other operations, we only perform the user's intent
if it matches up with the cap.
Note that this does not currently match the current
implementation: instead, the user's message will be
decoded into a new (undefined) intent for what the
cap happened to be. I propose modifying labels used to
avoid overlaps between different items so that we can
recognise when the user is invoking the wrong item.
\<close>
| CNodeCap _ _ _ _ \<Rightarrow>
doE
cnode_intent \<leftarrow> throw_opt undefined $ get_cnode_intent intent;
@ -206,7 +206,7 @@ where
liftME InvokeDomain $ decode_domain_invocation caps domain_intent
odE
(* Don't support operations on other types of caps. *)
\<comment> \<open>Don't support operations on other types of caps.\<close>
| _ \<Rightarrow> throw"
end

36
spec/capDL/Endpoint_D.thy
View File

@ -51,11 +51,11 @@ where
return None
| Some (croot, index, depth) \<Rightarrow>
doE
(* Lookup the slot. *)
\<comment> \<open>Lookup the slot.\<close>
cspace_root \<leftarrow> unify_failure $ lookup_cap thread croot;
result \<leftarrow> unify_failure $ lookup_slot_for_cnode_op cspace_root index depth;
(* Ensure nothing is already in it. *)
\<comment> \<open>Ensure nothing is already in it.\<close>
cap \<leftarrow> liftE $ get_cap result;
whenE (cap \<noteq> NullCap) throw;
@ -110,29 +110,29 @@ fun
where
"transfer_caps_loop ep receiver [] dest = return ()"
| "transfer_caps_loop ep receiver ((cap,slot)#caps) dest =
(* Transfer badge, transfer cap, or abort early if more than
one cap to transfer *)
\<comment> \<open>Transfer badge, transfer cap, or abort early if more than
one cap to transfer\<close>
(if is_ep_cap cap \<and> ep = Some (cap_object cap)
then do
(* transfer badge *)
\<comment> \<open>transfer badge\<close>
corrupt_ipc_buffer receiver True;
(* transfer rest of badges or cap *)
\<comment> \<open>transfer rest of badges or cap\<close>
transfer_caps_loop ep receiver caps dest
od
else if dest \<noteq> None then doE
(* Possibly diminish rights (if diminish flag was set on endpoint) *)
\<comment> \<open>Possibly diminish rights (if diminish flag was set on endpoint)\<close>
new_cap \<leftarrow> returnOk (update_cap_rights (cap_rights cap - {Write}) cap) \<sqinter>
returnOk cap;
(* Target cap is derived. This may abort transfer early. *)
\<comment> \<open>Target cap is derived. This may abort transfer early.\<close>
target_cap \<leftarrow> derive_cap slot new_cap;
whenE (target_cap = NullCap) throw;
(* Copy the cap across as either a child or sibling. *)
\<comment> \<open>Copy the cap across as either a child or sibling.\<close>
liftE (insert_cap_child target_cap slot (the dest)
\<sqinter> insert_cap_sibling target_cap slot (the dest));
(* Transfer rest of badges *)
\<comment> \<open>Transfer rest of badges\<close>
liftE $ transfer_caps_loop ep receiver caps None
odE <catch> (\<lambda>_. return ())
else
@ -246,20 +246,20 @@ definition
do_ipc_transfer :: "cdl_object_id option \<Rightarrow> cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> bool \<Rightarrow> unit k_monad"
where
"do_ipc_transfer ep_id sender_id receiver_id can_grant \<equiv> do
(* look up cap transfer *)
\<comment> \<open>look up cap transfer\<close>
src_slots \<leftarrow> get_send_slots sender_id;
do (* do normal transfer *)
do \<comment> \<open>do normal transfer\<close>
caps \<leftarrow> if can_grant then
lookup_extra_caps sender_id src_slots <catch> (\<lambda>_. return [])
else
return [];
(* copy registers, transfer message or fault *)
\<comment> \<open>copy registers, transfer message or fault\<close>
corrupt_ipc_buffer receiver_id True;
(* transfer caps if no fault occured *)
\<comment> \<open>transfer caps if no fault occured\<close>
transfer_caps ep_id caps sender_id receiver_id
od \<sqinter> (* fault transfer *)
od \<sqinter> \<comment> \<open>fault transfer\<close>
corrupt_ipc_buffer receiver_id True;
(* set message info *)
\<comment> \<open>set message info\<close>
corrupt_tcb_intent receiver_id
od"
@ -279,7 +279,7 @@ where
do
has_fault \<leftarrow> get_thread_fault receiver_id;
when (\<not> has_fault) $ do_ipc_transfer None sender_id receiver_id can_grant;
(* Clear out any pending operation caps. *)
\<comment> \<open>Clear out any pending operation caps.\<close>
delete_cap_simple reply_cap_slot;
when (has_fault) $ (do corrupt_tcb_intent receiver_id;
update_thread_fault receiver_id (\<lambda>_. False) od );
@ -447,7 +447,7 @@ definition
where
"send_fault_ipc tcb_id \<equiv>
doE
(* Lookup where we should send the fault IPC to. *)
\<comment> \<open>Lookup where we should send the fault IPC to.\<close>
tcb \<leftarrow> liftE $ get_thread tcb_id;
target_ep_cptr \<leftarrow> returnOk $ cdl_tcb_fault_endpoint tcb;
handler_cap \<leftarrow> lookup_cap tcb_id target_ep_cptr;

20
spec/capDL/Interrupt_D.thy
View File

@ -53,8 +53,8 @@ definition
cdl_irq_control_intent \<Rightarrow> cdl_irq_control_invocation except_monad"
where
"decode_irq_control_invocation target target_ref caps intent \<equiv> case intent of
(* Create an IRQ handler cap for the given IRQ, placing it
* in the specified CNode slot. *)
\<comment> \<open>Create an IRQ handler cap for the given IRQ, placing it
in the specified CNode slot.\<close>
IrqControlIssueIrqHandlerIntent irq index depth \<Rightarrow>
doE
root \<leftarrow> throw_on_none $ get_index caps 0;
@ -69,21 +69,21 @@ definition
cdl_irq_handler_intent \<Rightarrow> cdl_irq_handler_invocation except_monad"
where
"decode_irq_handler_invocation target target_ref caps intent \<equiv> case intent of
(* Acknowledge an IRQ. *)
\<comment> \<open>Acknowledge an IRQ.\<close>
IrqHandlerAckIntent \<Rightarrow>
doE
irq \<leftarrow> liftE $ assert_opt $ cdl_cap_irq target;
returnOk $ AckIrq irq
odE \<sqinter> throw
(* Modify the IRQ so that it no longer sends to an endpoint. *)
\<comment> \<open>Modify the IRQ so that it no longer sends to an endpoint.\<close>
| IrqHandlerClearIntent \<Rightarrow>
doE
irq \<leftarrow> liftE $ assert_opt $ cdl_cap_irq target;
returnOk $ ClearIrqHandler irq
odE \<sqinter> throw
(* Setup an IRQ to cause an endpoint to be sent to. *)
\<comment> \<open>Setup an IRQ to cause an endpoint to be sent to.\<close>
| IrqHandlerSetEndpointIntent \<Rightarrow>
doE
endpoint \<leftarrow> throw_on_none $ get_index caps 0;
@ -101,7 +101,7 @@ definition
arch_invoke_irq_control :: "arch_cdl_irq_control_invocation \<Rightarrow> unit k_monad"
where
"arch_invoke_irq_control params \<equiv> case params of
(* Create a new IRQ handler cap. *)
\<comment> \<open>Create a new IRQ handler cap.\<close>
ARMIssueIrqHandler irq control_slot dest_slot trigger \<Rightarrow>
insert_cap_child (IrqHandlerCap irq) control_slot dest_slot
"
@ -110,7 +110,7 @@ definition
invoke_irq_control :: "cdl_irq_control_invocation \<Rightarrow> unit k_monad"
where
"invoke_irq_control params \<equiv> case params of
(* Create a new IRQ handler cap. *)
\<comment> \<open>Create a new IRQ handler cap.\<close>
IssueIrqHandler irq control_slot dest_slot \<Rightarrow>
insert_cap_child (IrqHandlerCap irq) control_slot dest_slot
| ArchIssueIrqHandler arch_inv \<Rightarrow>
@ -120,10 +120,10 @@ definition
invoke_irq_handler :: "cdl_irq_handler_invocation \<Rightarrow> unit k_monad"
where
"invoke_irq_handler params \<equiv> case params of
(* Acknowledge and unmask an IRQ. *)
\<comment> \<open>Acknowledge and unmask an IRQ.\<close>
AckIrq irq \<Rightarrow> return ()
(* Attach an IRQ handler to write to an endpoint. *)
\<comment> \<open>Attach an IRQ handler to write to an endpoint.\<close>
| SetIrqHandler irq cap slot \<Rightarrow>
do
irqslot \<leftarrow> gets (get_irq_slot irq);
@ -131,7 +131,7 @@ where
insert_cap_child cap slot irqslot \<sqinter> insert_cap_sibling cap slot irqslot
od
(* Deassociate this handler with all endpoints. *)
\<comment> \<open>Deassociate this handler with all endpoints.\<close>
| ClearIrqHandler irq \<Rightarrow>
do
irqslot \<leftarrow> gets (get_irq_slot irq);

66
spec/capDL/PageTable_D.thy
View File

@ -40,18 +40,18 @@ definition
cdl_page_table_intent \<Rightarrow> cdl_page_table_invocation except_monad"
where
"decode_page_table_invocation target target_ref caps intent \<equiv> case intent of
(*
* Map the given PageTable into the given PageDirectory at the given
* virtual address.
*
* The concrete implementation only allows a PageTable to be mapped
* once at any point in time, but we don't enforce that here.
*)
\<comment> \<open>
Map the given PageTable into the given PageDirectory at the given
virtual address.
The concrete implementation only allows a PageTable to be mapped
once at any point in time, but we don't enforce that here.
\<close>
PageTableMapIntent vaddr attr \<Rightarrow>
doE
case cdl_get_pt_mapped_addr target of Some a \<Rightarrow> throw
| None \<Rightarrow> returnOk ();
(* Ensure that a PD was passed in. *)
\<comment> \<open>Ensure that a PD was passed in.\<close>
pd \<leftarrow> throw_on_none $ get_index caps 0;
(pd_object_id, asid) \<leftarrow>
case (fst pd) of
@ -63,7 +63,7 @@ where
returnOk $ PageTableMap (PageTableCap (cap_object target) Real (Some (asid,vaddr && ~~ mask 20)))
(PageTableCap (cap_object target) Fake None) target_ref target_slot
odE \<sqinter> throw
(* Unmap this PageTable. *)
\<comment> \<open>Unmap this PageTable.\<close>
| PageTableUnmapIntent \<Rightarrow> (
case target of PageTableCap pid ctype maddr \<Rightarrow>
(returnOk $ PageTableUnmap maddr pid target_ref)
@ -92,36 +92,36 @@ definition
cdl_page_intent \<Rightarrow> cdl_page_invocation except_monad"
where
"decode_page_invocation target target_ref caps intent \<equiv> case intent of
(*
* Map the given Page into the given PageDirectory or PageTable at
* the given virtual address.
*
* The concrete implementation only allows a Page to be mapped
* once at any point in time, but we don't enforce that here.
*)
\<comment> \<open>
Map the given Page into the given PageDirectory or PageTable at
the given virtual address.
The concrete implementation only allows a Page to be mapped
once at any point in time, but we don't enforce that here.
\<close>
PageMapIntent vaddr rights attr \<Rightarrow>
doE
(* Ensure that a PD was passed in. *)
\<comment> \<open>Ensure that a PD was passed in.\<close>
pd \<leftarrow> throw_on_none $ get_index caps 0;
(pd_object_id, asid) \<leftarrow>
case (fst pd) of
PageDirectoryCap x _ (Some asid) \<Rightarrow> returnOk (x, asid)
| _ \<Rightarrow> throw;
(* Collect mapping from target cap. *)
\<comment> \<open>Collect mapping from target cap.\<close>
(frame, sz,dev) \<leftarrow> returnOk $ (case target of FrameCap dev p R sz m mp \<Rightarrow> (p,sz,dev));
target_slots \<leftarrow> cdl_page_mapping_entries vaddr sz pd_object_id;
(* Calculate rights. *)
\<comment> \<open>Calculate rights.\<close>
new_rights \<leftarrow> returnOk $ validate_vm_rights $ cap_rights target \<inter> rights;
(* Return the map intent. *)
\<comment> \<open>Return the map intent.\<close>
returnOk $ PageMap (FrameCap dev frame (cap_rights target) sz Real (Some (asid,vaddr)))
(FrameCap False frame new_rights sz Fake None) target_ref target_slots
odE \<sqinter> throw
(* Unmap this PageTable. *)
\<comment> \<open>Unmap this PageTable.\<close>
| PageUnmapIntent \<Rightarrow> doE
(frame, asid, sz) \<leftarrow> (case target of
FrameCap _ p R sz m mp \<Rightarrow> returnOk (p, mp , sz)
@ -129,10 +129,10 @@ where
(returnOk $ PageUnmap asid frame target_ref sz) \<sqinter> throw
odE
(* Change the rights on a given mapping. *)
\<comment> \<open>Change the rights on a given mapping.\<close>
| PageRemapIntent rights attrs \<Rightarrow>
doE
(* Ensure user has a right to the PD. *)
\<comment> \<open>Ensure user has a right to the PD.\<close>
pd \<leftarrow> throw_on_none $ get_index caps 0;
pd_object_id \<leftarrow>
case (fst pd) of
@ -141,20 +141,20 @@ where
pd_object \<leftarrow> liftE $ get_object pd_object_id;
(* Find all of our children caps. *)
\<comment> \<open>Find all of our children caps.\<close>
pd_slots \<leftarrow> liftE $ gets $ all_pd_pt_slots pd_object pd_object_id;
target_slots \<leftarrow> liftE $ select {M. set M \<subseteq> pd_slots \<and> distinct M};
(* Calculate rights. *)
\<comment> \<open>Calculate rights.\<close>
new_rights \<leftarrow> returnOk $ validate_vm_rights $ cap_rights target \<inter> rights;
(* Collect mapping from target cap. *)
\<comment> \<open>Collect mapping from target cap.\<close>
(frame, sz, dev) \<leftarrow> returnOk $ (case target of FrameCap dev p R sz m mp \<Rightarrow> (p,sz,dev));
returnOk $ PageRemap (FrameCap False frame new_rights sz Fake None) target_slots
odE \<sqinter> throw
(* Flush the caches associated with this page. *)
\<comment> \<open>Flush the caches associated with this page.\<close>
| PageFlushCachesIntent \<Rightarrow>
(returnOk $ PageFlushCaches Unify) \<sqinter> (returnOk $ PageFlushCaches Clean) \<sqinter>
(returnOk $ PageFlushCaches CleanInvalidate ) \<sqinter> (returnOk $ PageFlushCaches Invalidate)
@ -182,11 +182,11 @@ where
"invoke_page_table params \<equiv> case params of
PageTableMap real_pt_cap pt_cap pt_cap_ref pd_target_slot \<Rightarrow>
do set_cap pt_cap_ref real_pt_cap;
(*
* We install the Page Table into the Page Directory. The
* concrete kernel uses hardware-defined PDEs (Page Directory
* Entries). Our abstract spec just uses caps.
*)
\<comment> \<open>
We install the Page Table into the Page Directory. The
concrete kernel uses hardware-defined PDEs (Page Directory
Entries). Our abstract spec just uses caps.
\<close>
insert_cap_orphan pt_cap pd_target_slot
od
| PageTableUnmap mapped_addr pt_id pt_cap_ref \<Rightarrow> do
@ -207,7 +207,7 @@ definition
where
"invoke_page params \<equiv> case params of
PageMap frame_cap pseudo_frame_cap frame_cap_ref target_slots \<Rightarrow>
(* Clear out the target slots. *)
\<comment> \<open>Clear out the target slots.\<close>
do
set_cap frame_cap_ref frame_cap;
mapM_x (swp set_cap pseudo_frame_cap) target_slots

16
spec/capDL/Syscall_D.thy
View File

@ -109,16 +109,16 @@ where
extra_cap_cptrs \<leftarrow> returnOk $ cdl_intent_extras full_intent;
syscall
(* Lookup all caps presented. *)
\<comment> \<open>Lookup all caps presented.\<close>
(doE
(cap, cap_ref) \<leftarrow> lookup_cap_and_slot thread_ptr invoked_cptr;
extra_caps \<leftarrow> lookup_extra_caps thread_ptr extra_cap_cptrs;
returnOk (cap, cap_ref, extra_caps)
odE)
(* If that failed, send off a fault IPC (if we did a blocking operation). *)
\<comment> \<open>If that failed, send off a fault IPC (if we did a blocking operation).\<close>
(when can_block $ handle_fault)
(* Decode the user's intent. *)
\<comment> \<open>Decode the user's intent.\<close>
(\<lambda> (cap, cap_ref, extra_caps).
case intent of
None \<Rightarrow> (if ep_related_cap cap then
@ -127,12 +127,12 @@ where
| Some intent' \<Rightarrow>
decode_invocation cap cap_ref extra_caps intent')
(* If that stuffed up, we do nothing more than corrupt the frames. *)
\<comment> \<open>If that stuffed up, we do nothing more than corrupt the frames.\<close>
(do corrupt_ipc_buffer thread_ptr True;
when is_call (mark_tcb_intent_error thread_ptr True)
od)
(* Invoke the system call. *)
\<comment> \<open>Invoke the system call.\<close>
(\<lambda> inv. doE
liftE $ set_cap (thread_ptr,tcb_pending_op_slot) RestartCap;
perform_invocation is_call can_block inv;
@ -151,10 +151,10 @@ definition
where
"handle_recv \<equiv>
do
(* Get the current thread. *)
\<comment> \<open>Get the current thread.\<close>
tcb_id \<leftarrow> gets_the cdl_current_thread;
tcb \<leftarrow> get_thread tcb_id;
(* Get the endpoint it is trying to receive from. *)
\<comment> \<open>Get the endpoint it is trying to receive from.\<close>
(doE
ep_cptr \<leftarrow> returnOk $ cdl_intent_cap (cdl_tcb_intent tcb);
ep_cap \<leftarrow> lookup_cap tcb_id ep_cptr;
@ -232,7 +232,7 @@ definition
where
"call_kernel ev \<equiv>
do
(* Deal with the event. *)
\<comment> \<open>Deal with the event.\<close>
handle_event ev
<handle> (\<lambda> _. liftE handle_pending_interrupts);
schedule;

40
spec/capDL/Tcb_D.thy
View File

@ -50,15 +50,15 @@ definition
cdl_tcb_intent \<Rightarrow> cdl_tcb_invocation except_monad"
where
"decode_tcb_invocation target slot caps intent \<equiv> case intent of
(* Read another thread's registers. *)
\<comment> \<open>Read another thread's registers.\<close>
TcbReadRegistersIntent suspend flags count \<Rightarrow>
returnOk (ReadRegisters (cap_object target) suspend 0 0) \<sqinter> throw
(* Write another thread's registers. *)
\<comment> \<open>Write another thread's registers.\<close>
| TcbWriteRegistersIntent resume flags count regs \<Rightarrow>
returnOk (WriteRegisters (cap_object target) resume [0] 0) \<sqinter> throw
(* Copy registers from one thread to another. *)
\<comment> \<open>Copy registers from one thread to another.\<close>
| TcbCopyRegistersIntent suspend_source resume_target f1 f2 f3 \<Rightarrow>
doE
(source_cap, _) \<leftarrow> throw_on_none $ get_index caps 0;
@ -70,15 +70,15 @@ where
returnOk (CopyRegisters target_tcb source_tcb suspend_source resume_target f1 f2 0)
odE \<sqinter> throw
(* Suspend the target thread. *)
\<comment> \<open>Suspend the target thread.\<close>
| TcbSuspendIntent \<Rightarrow>
returnOk (Suspend (cap_object target)) \<sqinter> throw
(* Resume the target thread. *)
\<comment> \<open>Resume the target thread.\<close>
| TcbResumeIntent \<Rightarrow>
returnOk (Resume (cap_object target)) \<sqinter> throw
(* Configure: target, fault_ep, mcp, priority, cspace_root_data, vspace_root_data, buffer *)
\<comment> \<open>Configure: target, fault_ep, mcp, priority, cspace_root_data, vspace_root_data, buffer\<close>
| TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer \<Rightarrow>
doE
cspace_root \<leftarrow> throw_on_none $ get_index caps 0;
@ -91,28 +91,28 @@ where
(Some cspace_root_cap_ref) (Some vspace_root_cap_ref) (buffer_frame_opt))
odE \<sqinter> throw
(* Modify a thread's maximum control priority. *)
\<comment> \<open>Modify a thread's maximum control priority.\<close>
| TcbSetMCPriorityIntent mcp \<Rightarrow>
doE
auth_cap \<leftarrow> throw_on_none $ get_index caps 0;
returnOk (ThreadControl (cap_object target) slot None None None None)
odE \<sqinter> throw
(* Modify a thread's priority. *)
\<comment> \<open>Modify a thread's priority.\<close>
| TcbSetPriorityIntent priority \<Rightarrow>
doE
auth_cap \<leftarrow> throw_on_none $ get_index caps 0;
returnOk (ThreadControl (cap_object target) slot None None None None)
odE \<sqinter> throw
(* Modify a thread's mcp and priority at the same time. *)
\<comment> \<open>Modify a thread's mcp and priority at the same time.\<close>
| TcbSetSchedParamsIntent mcp priority \<Rightarrow>
doE
auth_cap \<leftarrow> throw_on_none $ get_index caps 0;
returnOk (ThreadControl (cap_object target) slot None None None None)
odE \<sqinter> throw
(* Modify a thread's IPC buffer. *)
\<comment> \<open>Modify a thread's IPC buffer.\<close>
| TcbSetIPCBufferIntent buffer \<Rightarrow>
doE
buffer_frame \<leftarrow> throw_on_none $ get_index caps 0;
@ -120,7 +120,7 @@ where
returnOk (ThreadControl (cap_object target) slot None None None buffer_frame_opt)
odE \<sqinter> throw
(* Update the various spaces (CSpace/VSpace) of a thread. *)
\<comment> \<open>Update the various spaces (CSpace/VSpace) of a thread.\<close>
| TcbSetSpaceIntent fault_ep cspace_root_data vspace_root_data \<Rightarrow>
doE
cspace_root \<leftarrow> throw_on_none $ get_index caps 0;
@ -244,7 +244,7 @@ definition
invoke_tcb :: "cdl_tcb_invocation \<Rightarrow> unit preempt_monad"
where
"invoke_tcb params \<equiv> case params of
(* Modify a thread's registers. *)
\<comment> \<open>Modify a thread's registers.\<close>
WriteRegisters target_tcb resume _ _ \<Rightarrow>
liftE $
do
@ -252,11 +252,11 @@ where
when resume $ restart target_tcb
od
(* Read a thread's registers. *)
\<comment> \<open>Read a thread's registers.\<close>
| ReadRegisters src_tcb _ _ _ \<Rightarrow>
liftE $ suspend src_tcb \<sqinter> return ()
(* Copy registers from one thread to another *)
\<comment> \<open>Copy registers from one thread to another\<close>
| CopyRegisters target_tcb source_tcb _ _ _ _ _ \<Rightarrow>
liftE $
do
@ -265,32 +265,32 @@ where
corrupt_tcb_intent target_tcb
od
(* Suspend this thread. *)
\<comment> \<open>Suspend this thread.\<close>
| Suspend target_tcb \<Rightarrow>
liftE $ suspend target_tcb \<sqinter> return ()
(* Resume this thread. *)
\<comment> \<open>Resume this thread.\<close>
| Resume target_tcb \<Rightarrow>
liftE $ restart target_tcb
(* Update a thread's options. *)
\<comment> \<open>Update a thread's options.\<close>
| ThreadControl target_tcb tcb_cap_slot faultep croot vroot ipc_buffer \<Rightarrow>
doE
case faultep of
Some x \<Rightarrow> liftE $ update_thread target_tcb (\<lambda>tcb. tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)
| None \<Rightarrow> returnOk ();
(* Possibly update CSpace *)
\<comment> \<open>Possibly update CSpace\<close>
case croot of
Some x \<Rightarrow> tcb_update_cspace_root target_tcb tcb_cap_slot x
| None \<Rightarrow> returnOk ();
(* Possibly update VSpace *)
\<comment> \<open>Possibly update VSpace\<close>
case vroot of
Some x \<Rightarrow> tcb_update_vspace_root target_tcb tcb_cap_slot x
| None \<Rightarrow> returnOk ();
(* Possibly update Ipc Buffer *)
\<comment> \<open>Possibly update Ipc Buffer\<close>
case ipc_buffer of
Some x \<Rightarrow> tcb_update_ipc_buffer target_tcb tcb_cap_slot x
| None \<Rightarrow> (returnOk () \<sqinter> (doE tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot;

23
spec/capDL/Untyped_D.thy
View File

@ -25,7 +25,7 @@ where
doE
(root_cap, root_slot) \<leftarrow> throw_on_none $ get_index caps 0;
(* Lookup the destination slots. *)
\<comment> \<open>Lookup the destination slots.\<close>
target_node \<leftarrow> if node_depth = 0 then
returnOk root_cap
else
@ -34,15 +34,15 @@ where
liftE $ get_cap target_slot
odE;
(* Ensure it is a CNode cap. *)
\<comment> \<open>Ensure it is a CNode cap.\<close>
unlessE (is_cnode_cap target_node) throw;
(* Find our target slots. *)
\<comment> \<open>Find our target slots.\<close>
slots \<leftarrow> returnOk $ map (\<lambda>n. (cap_object target_node, n))
[unat node_offset ..< unat node_offset + unat node_window];
mapME_x ensure_empty slots;
(* Work out what names are available. If we haven't haven't already been typed into something we can reuse our names. *)
\<comment> \<open>Work out what names are available. If we haven't haven't already been typed into something we can reuse our names.\<close>
s \<leftarrow> liftE $ get;
has_kids \<leftarrow> returnOk $ has_children untyped_ref s;
@ -115,8 +115,8 @@ definition
where
"retype_region target_bits target_type target_object_ids \<equiv>
do
(* Get a list of target locations. We are happy with any unused name
within the target range. *)
\<comment> \<open>Get a list of target locations. We are happy with any unused name
within the target range.\<close>
if (target_type \<noteq> UntypedType) then
do
@ -125,7 +125,8 @@ where
od
else return ();
(* Return the list of new objects. *)
\<comment> \<open>Get a list of target locations. We are happy with any unused name
within the target range.\<close>
return target_object_ids
od"
@ -166,14 +167,14 @@ where
update_available_range new_range (map (\<lambda>s. pick s) new_obj_refs) untyped_ref untyped_cap;
(* Construct new objects within the covered range. *)
\<comment> \<open>Construct new objects within the covered range.\<close>
retype_region type_size new_type new_obj_refs;
(* Construct caps for the new objects. *)
\<comment> \<open>Construct caps for the new objects.\<close>
mapM_x (create_cap new_type type_size untyped_ref (untyped_is_device untyped_cap)) (zip target_slots new_obj_refs);
(* Ideally, we should return back to the user how many
* objects were created. *)
\<comment> \<open>Ideally, we should return back to the user how many
objects were created.\<close>
return ()
od