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

ainvs (arm_hyp + generic): 'getActiveIRQ in_kernel' proof updates

This commit is contained in:
Gerwin Klein 2017-03-15 18:18:15 +11:00 committed by Alejandro Gomez-Londono
parent 4ee422a392
commit 91b723903e
6 changed files with 28 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/invariant-abstract/ADT_AI.thy
View File

@ -183,7 +183,7 @@ definition
check_active_irq :: "(bool,'z :: state_ext) s_monad"
where
"check_active_irq \<equiv> do
irq \<leftarrow> do_machine_op getActiveIRQ;
irq \<leftarrow> do_machine_op $ getActiveIRQ False;
return (irq \<noteq> None)
od"

2
proof/invariant-abstract/ARM_HYP/ArchCSpace_AI.thy
View File

@ -23,7 +23,7 @@ named_theorems CSpace_AI_assms
(* FIXME: move? *)
lemma getActiveIRQ_wp [CSpace_AI_assms]:
"irq_state_independent_A P \<Longrightarrow>
valid P (do_machine_op getActiveIRQ) (\<lambda>_. P)"
valid P (do_machine_op (getActiveIRQ in_kernel)) (\<lambda>_. P)"
apply (simp add: getActiveIRQ_def do_machine_op_def split_def exec_gets
select_f_select[simplified liftM_def]
select_modify_comm gets_machine_state_modify)

26
proof/invariant-abstract/ARM_HYP/Machine_AI.thy
View File

@ -328,7 +328,7 @@ lemma no_fail_freeMemory[simp, wp]:
lemma no_fail_getActiveIRQ[wp]:
"no_fail \<top> getActiveIRQ"
"no_fail \<top> (getActiveIRQ in_kernel)"
apply (simp add: getActiveIRQ_def)
apply (rule no_fail_pre)
apply (wp non_fail_select)
@ -338,7 +338,7 @@ lemma no_fail_getActiveIRQ[wp]:
definition "irq_state_independent P \<equiv> \<forall>f s. P s \<longrightarrow> P (irq_state_update f s)"
lemma getActiveIRQ_inv [wp]:
"\<lbrakk>irq_state_independent P\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> getActiveIRQ \<lbrace>\<lambda>rv. P\<rbrace>"
"\<lbrakk>irq_state_independent P\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: getActiveIRQ_def)
apply (wp alternative_wp select_wp)
apply (simp add: irq_state_independent_def)
@ -529,7 +529,7 @@ lemma no_irq_loadWord: "no_irq (loadWord x)"
done
lemma no_irq_getActiveIRQ: "no_irq getActiveIRQ"
lemma no_irq_getActiveIRQ: "no_irq (getActiveIRQ in_kernel)"
apply (clarsimp simp: no_irq_def)
apply (rule getActiveIRQ_inv)
apply (simp add: irq_state_independent_def)
@ -671,7 +671,7 @@ lemma no_irq_clearMemory: "no_irq (clearMemory a b)"
done
lemma getActiveIRQ_le_maxIRQ':
"\<lbrace>\<lambda>s. \<forall>irq > maxIRQ. irq_masks s irq\<rbrace> getActiveIRQ \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>"
"\<lbrace>\<lambda>s. \<forall>irq > maxIRQ. irq_masks s irq\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>"
apply (simp add: getActiveIRQ_def)
apply (wp alternative_wp select_wp)
apply clarsimp
@ -681,12 +681,28 @@ lemma getActiveIRQ_le_maxIRQ':
(* FIXME: follows already from getActiveIRQ_le_maxIRQ *)
lemma getActiveIRQ_neq_Some0xFF':
"\<lbrace>\<top>\<rbrace> getActiveIRQ \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>"
"\<lbrace>\<top>\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>"
apply (simp add: getActiveIRQ_def)
apply (wp alternative_wp select_wp)
apply simp
done
lemma getActiveIRQ_neq_non_kernel:
"\<lbrace>\<top>\<rbrace> getActiveIRQ True \<lbrace>\<lambda>rv s. rv \<notin> Some ` non_kernel_IRQs \<rbrace>"
apply (simp add: getActiveIRQ_def)
apply (wp alternative_wp select_wp)
apply auto
done
lemma dmo_getActiveIRQ_non_kernel[wp]:
"\<lbrace>\<top>\<rbrace> do_machine_op (getActiveIRQ True)
\<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> irq \<in> non_kernel_IRQs \<longrightarrow> P irq s\<rbrace>"
unfolding do_machine_op_def
apply wpsimp
apply (drule use_valid, rule getActiveIRQ_neq_non_kernel, rule TrueI)
apply clarsimp
done
lemma empty_fail_isb: "empty_fail isb"
by (simp add: isb_def)

2
proof/invariant-abstract/CSpace_AI.thy
View File

@ -114,7 +114,7 @@ locale CSpace_AI_getActiveIRQ_wp =
fixes state_ext_t :: "'state_ext::state_ext itself"
assumes getActiveIRQ_wp[wp]:
"\<And>P :: 'state_ext state \<Rightarrow> bool.
irq_state_independent_A P \<Longrightarrow> valid P (do_machine_op getActiveIRQ) (\<lambda>_. P)"
irq_state_independent_A P \<Longrightarrow> valid P (do_machine_op (getActiveIRQ in_kernel)) (\<lambda>_. P)"
lemma OR_choiceE_weak_wp:

2
proof/invariant-abstract/EmptyFail_AI.thy
View File

@ -450,7 +450,7 @@ locale EmptyFail_AI_call_kernel = EmptyFail_AI_schedule state_ext_t
assumes activate_thread_empty_fail[wp]:
"empty_fail (activate_thread :: (unit, 'state_ext) s_monad)"
assumes getActiveIRQ_empty_fail[wp]:
"empty_fail getActiveIRQ"
"empty_fail (getActiveIRQ in_kernel)"
assumes handle_event_empty_fail[wp]:
"\<And>event. empty_fail (handle_event event :: (unit, 'state_ext) p_monad)"
assumes handle_interrupt_empty_fail[wp]:

3
proof/invariant-abstract/KHeap_AI.thy
View File

@ -57,6 +57,9 @@ requalify_facts
wellformed_arch_obj_same_type
default_arch_object_not_live
default_tcb_not_live
getActiveIRQ_neq_non_kernel
dmo_getActiveIRQ_non_kernel
end
lemmas cap_is_device_obj_is_device[simp] = cap_is_device_obj_is_device