arm_hyp: proof updates for seL4 commit 93ab2543d9d8
The seL4 commit factors out special treatment of specific VCPU registers, and this commit updates the ARM_HYP proofs accordingly. Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein
Gerwin Klein
parent
3cc7a1c6b7
commit
8f992b2350
|
|
@ -4237,6 +4237,17 @@ lemma decodeARMMMUInvocation_ccorres:
|
|||
elim!: ccap_relationE split: if_split_asm)
|
||||
done
|
||||
|
||||
lemma vcpu_reg_saved_when_disabled_spec:
|
||||
"\<forall>s. \<Gamma> \<turnstile> {s}
|
||||
Call vcpu_reg_saved_when_disabled_'proc
|
||||
\<lbrace> \<acute>ret__unsigned_long = from_bool (\<^bsup>s\<^esup>field = scast seL4_VCPUReg_SCTLR) \<rbrace>"
|
||||
by vcg clarsimp
|
||||
|
||||
|
||||
lemma vcpuRegSavedWhenDisabled_spec[simp]:
|
||||
"vcpuRegSavedWhenDisabled reg = (reg = VCPURegSCTLR)"
|
||||
by (simp add: vcpuRegSavedWhenDisabled_def split: vcpureg.splits)
|
||||
|
||||
lemma writeVCPUReg_ccorres:
|
||||
notes Collect_const[simp del] dc_simp[simp del]
|
||||
shows
|
||||
|
|
@ -4253,34 +4264,31 @@ lemma writeVCPUReg_ccorres:
|
|||
apply (rule_tac C'="{s. cvcpuopt \<noteq> None \<and> (cvcpuopt \<noteq> None \<longrightarrow> fst (the cvcpuopt) = vcpuptr) }"
|
||||
and Q="\<lambda>s. vcpuptr \<noteq> 0 \<and> (armHSCurVCPU \<circ> ksArchState) s = cvcpuopt"
|
||||
and Q'=UNIV in ccorres_rewrite_cond_sr)
|
||||
subgoal by (fastforce dest: rf_sr_ksArchState_armHSCurVCPU simp: cur_vcpu_relation_def
|
||||
split: option.splits)
|
||||
apply (clarsimp simp: vcpureg_eq_use_types) \<comment> \<open>C register comparison into reg comparison\<close>
|
||||
subgoal by (fastforce dest: rf_sr_ksArchState_armHSCurVCPU simp: cur_vcpu_relation_def
|
||||
split: option.splits)
|
||||
apply (rule ccorres_Cond_rhs)
|
||||
|
||||
\<comment> \<open>vcpuptr is current vcpu\<close>
|
||||
apply clarsimp
|
||||
apply (rename_tac curvcpuactive)
|
||||
apply (rule ccorres_Cond_rhs ; clarsimp)
|
||||
apply (rule_tac C'="{s. curvcpuactive }"
|
||||
apply csymbr
|
||||
apply (rule_tac C'="{s. reg = VCPURegSCTLR \<and> \<not>curvcpuactive }"
|
||||
and Q="\<lambda>s. (armHSCurVCPU \<circ> ksArchState) s = Some (vcpuptr, curvcpuactive)"
|
||||
and Q'=UNIV in ccorres_rewrite_cond_sr)
|
||||
subgoal by (clarsimp dest!: rf_sr_ksArchState_armHSCurVCPU simp: cur_vcpu_relation_def
|
||||
split: option.splits)
|
||||
subgoal by (clarsimp dest!: rf_sr_ksArchState_armHSCurVCPU
|
||||
simp: cur_vcpu_relation_def from_bool_0 vcpureg_eq_use_types(1)
|
||||
split: option.splits)
|
||||
(* unification choking on schematics with pairs *)
|
||||
apply (rule_tac A="vcpu_at' vcpuptr" and A'=UNIV in ccorres_guard_imp)
|
||||
apply (rule ccorres_Cond_rhs ; clarsimp)
|
||||
apply (ctac (no_vcg) add: setSCTLR_ccorres)
|
||||
apply (rule_tac A="vcpu_at' vcpuptr" and A'=UNIV in ccorres_guard_imp)
|
||||
apply (rule ccorres_Cond_rhs, clarsimp)
|
||||
apply (ctac (no_vcg) add: vcpu_write_reg_ccorres)
|
||||
apply fastforce
|
||||
apply (simp (no_asm_simp))
|
||||
apply (ctac (no_vcg) add: vcpu_hw_write_reg_ccorres)
|
||||
apply fastforce
|
||||
apply (ctac (no_vcg) add: vcpu_hw_write_reg_ccorres)
|
||||
apply fastforce
|
||||
\<comment> \<open>no current vcpu\<close>
|
||||
apply clarsimp
|
||||
apply wpc
|
||||
apply (subgoal_tac "\<not> x1")
|
||||
prefer 2
|
||||
apply fastforce
|
||||
apply (rename_tac cur b, prop_tac "\<not>cur", fastforce)
|
||||
apply simp
|
||||
apply (ctac (no_vcg) add: vcpu_write_reg_ccorres)
|
||||
apply fastforce
|
||||
|
|
@ -4300,53 +4308,46 @@ lemma readVCPUReg_ccorres:
|
|||
apply (rule_tac C'="{s. cvcpuopt \<noteq> None \<and> (cvcpuopt \<noteq> None \<longrightarrow> fst (the cvcpuopt) = vcpuptr) }"
|
||||
and Q="\<lambda>s. vcpuptr \<noteq> 0 \<and> (armHSCurVCPU \<circ> ksArchState) s = cvcpuopt"
|
||||
and Q'=UNIV in ccorres_rewrite_cond_sr)
|
||||
subgoal by (fastforce dest: rf_sr_ksArchState_armHSCurVCPU simp: cur_vcpu_relation_def
|
||||
subgoal by (fastforce dest: rf_sr_ksArchState_armHSCurVCPU simp: cur_vcpu_relation_def
|
||||
split: option.splits)
|
||||
apply (clarsimp simp: vcpureg_eq_use_types) \<comment> \<open>C register comparison into reg comparison\<close>
|
||||
apply (rule ccorres_Cond_rhs)
|
||||
\<comment> \<open>vcpuptr is current vcpu\<close>
|
||||
apply clarsimp
|
||||
apply (rename_tac curvcpuactive)
|
||||
apply (rule ccorres_Cond_rhs ; clarsimp)
|
||||
apply (rule_tac C'="{s. curvcpuactive }"
|
||||
apply csymbr
|
||||
apply (rule_tac C'="{s. reg = VCPURegSCTLR \<and> \<not>curvcpuactive }"
|
||||
and Q="\<lambda>s. (armHSCurVCPU \<circ> ksArchState) s = Some (vcpuptr, curvcpuactive)"
|
||||
and Q'=UNIV in ccorres_rewrite_cond_sr)
|
||||
subgoal by (clarsimp dest!: rf_sr_ksArchState_armHSCurVCPU simp: cur_vcpu_relation_def
|
||||
split: option.splits)
|
||||
(* unification choking on schematics with pairs *)
|
||||
apply (rule_tac A=\<top> and A'=UNIV in ccorres_guard_imp)
|
||||
apply (rule ccorres_Cond_rhs ; clarsimp)
|
||||
\<comment> \<open>SCTLR\<close>
|
||||
apply (rule ccorres_add_return2)
|
||||
apply (ctac (no_vcg) add: getSCTLR_ccorres)
|
||||
apply (fastforce intro!: ccorres_return_C)
|
||||
apply simp
|
||||
apply (rule hoare_post_taut[of \<top>])
|
||||
subgoal by (clarsimp dest!: rf_sr_ksArchState_armHSCurVCPU
|
||||
simp: cur_vcpu_relation_def from_bool_0 vcpureg_eq_use_types(1)
|
||||
split: option.splits)
|
||||
(* unification choking on schematics with pairs *)
|
||||
apply (rule_tac A="vcpu_at' vcpuptr" and A'=UNIV in ccorres_guard_imp)
|
||||
apply (rule ccorres_Cond_rhs, clarsimp)
|
||||
apply (rule ccorres_add_return2)
|
||||
apply (ctac (no_vcg) add: vcpu_read_reg_ccorres)
|
||||
apply (fastforce intro!: ccorres_return_C)
|
||||
apply wpsimp
|
||||
(* re-unify with ccorres_guard_imp *)
|
||||
apply fastforce
|
||||
apply wp
|
||||
apply (simp (no_asm_simp))
|
||||
apply (rule ccorres_add_return2)
|
||||
apply (ctac (no_vcg) add: vcpu_hw_read_reg_ccorres)
|
||||
apply (fastforce intro!: ccorres_return_C)
|
||||
apply wp
|
||||
apply fastforce
|
||||
\<comment> \<open>any other hyp register\<close>
|
||||
apply (rule ccorres_add_return2)
|
||||
apply (ctac (no_vcg) add: vcpu_hw_read_reg_ccorres)
|
||||
apply (fastforce intro!: ccorres_return_C)
|
||||
apply wpsimp
|
||||
apply fastforce
|
||||
\<comment> \<open>no current vcpu\<close>
|
||||
apply clarsimp
|
||||
apply wpc
|
||||
apply (subgoal_tac "\<not> x1")
|
||||
prefer 2
|
||||
apply fastforce
|
||||
apply (rename_tac cur b, prop_tac "\<not>cur", fastforce)
|
||||
apply simp
|
||||
apply (rule ccorres_add_return2)
|
||||
apply (ctac (no_vcg) add: vcpu_read_reg_ccorres)
|
||||
apply (fastforce intro!: ccorres_return_C)
|
||||
apply wpsimp
|
||||
apply wp
|
||||
apply fastforce
|
||||
done
|
||||
|
||||
|
||||
lemma invokeVCPUReadReg_ccorres: (* styled after invokeTCB_ReadRegisters_ccorres *)
|
||||
notes Collect_const[simp del] dc_simp[simp del]
|
||||
shows
|
||||
|
|
|
|||
|
|
@ -67,9 +67,8 @@ where
|
|||
| _ \<Rightarrow> (False, False));
|
||||
|
||||
if on_cur_vcpu
|
||||
then if reg = VCPURegSCTLR
|
||||
then if active then do_machine_op getSCTLR
|
||||
else vcpu_read_reg vcpu_ptr VCPURegSCTLR
|
||||
then if vcpuRegSavedWhenDisabled reg \<and> \<not>active
|
||||
then vcpu_read_reg vcpu_ptr reg
|
||||
else do_machine_op $ readVCPUHardwareReg reg
|
||||
else vcpu_read_reg vcpu_ptr reg
|
||||
od"
|
||||
|
|
@ -85,9 +84,8 @@ where
|
|||
| _ \<Rightarrow> (False, False));
|
||||
|
||||
if on_cur_vcpu
|
||||
then if reg = VCPURegSCTLR
|
||||
then if active then do_machine_op $ setSCTLR val
|
||||
else vcpu_write_reg vcpu_ptr reg val
|
||||
then if vcpuRegSavedWhenDisabled reg \<and> \<not>active
|
||||
then vcpu_write_reg vcpu_ptr reg val
|
||||
else do_machine_op $ writeVCPUHardwareReg reg val
|
||||
else vcpu_write_reg vcpu_ptr reg val
|
||||
od"
|
||||
|
|
|
|||
|
|
@ -96,6 +96,10 @@ This module defines the ARM register set.
|
|||
> vcpuRegNum :: Int
|
||||
> vcpuRegNum = fromEnum (maxBound :: VCPUReg)
|
||||
|
||||
> vcpuRegSavedWhenDisabled :: VCPUReg -> Bool
|
||||
> vcpuRegSavedWhenDisabled VCPURegSCTLR = True
|
||||
> vcpuRegSavedWhenDisabled _ = False
|
||||
|
||||
#endif
|
||||
|
||||
> initContext :: [(Register, Word)]
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ hypervisor extensions on ARM.
|
|||
> import SEL4.API.InvocationLabels.ARM
|
||||
> import SEL4.API.Invocation
|
||||
> import SEL4.API.Invocation.ARM as ArchInv
|
||||
> import SEL4.Machine.RegisterSet.ARM (Register(..), VCPUReg(..), vcpuRegNum)
|
||||
> import SEL4.Machine.RegisterSet.ARM (Register(..), VCPUReg(..), vcpuRegNum, vcpuRegSavedWhenDisabled)
|
||||
> import SEL4.API.Types
|
||||
> import SEL4.API.InvocationLabels
|
||||
> import SEL4.API.Failures.TARGET
|
||||
|
|
@ -172,9 +172,8 @@ Currently, there is only one VCPU register available for reading/writing by the
|
|||
> _ -> (False, False)
|
||||
>
|
||||
> if onCurVCPU
|
||||
> then if reg == VCPURegSCTLR
|
||||
> then if active then doMachineOp getSCTLR
|
||||
> else vcpuReadReg vcpuPtr VCPURegSCTLR
|
||||
> then if vcpuRegSavedWhenDisabled reg && not active
|
||||
> then vcpuReadReg vcpuPtr reg
|
||||
> else doMachineOp $ readVCPUHardwareReg reg
|
||||
> else vcpuReadReg vcpuPtr reg
|
||||
|
||||
|
|
@ -186,9 +185,8 @@ Currently, there is only one VCPU register available for reading/writing by the
|
|||
> _ -> (False, False)
|
||||
>
|
||||
> if onCurVCPU
|
||||
> then if reg == VCPURegSCTLR
|
||||
> then if active then doMachineOp $ setSCTLR val
|
||||
> else vcpuWriteReg vcpuPtr reg val
|
||||
> then if vcpuRegSavedWhenDisabled reg && not active
|
||||
> then vcpuWriteReg vcpuPtr reg val
|
||||
> else doMachineOp $ writeVCPUHardwareReg reg val
|
||||
> else vcpuWriteReg vcpuPtr reg val
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue