From 8f992b23508c5c8f3fcc707569e0a6d31da33a97 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 18 Dec 2020 18:45:05 +1100 Subject: [PATCH] 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 --- proof/crefine/ARM_HYP/Arch_C.thy | 87 ++++++++++--------- spec/abstract/ARM_HYP/VCPU_A.thy | 10 +-- .../src/SEL4/Machine/RegisterSet/ARM.lhs | 4 + spec/haskell/src/SEL4/Object/VCPU/ARM.lhs | 12 ++- 4 files changed, 57 insertions(+), 56 deletions(-) diff --git a/proof/crefine/ARM_HYP/Arch_C.thy b/proof/crefine/ARM_HYP/Arch_C.thy index 01207aa82..a9cdc8016 100644 --- a/proof/crefine/ARM_HYP/Arch_C.thy +++ b/proof/crefine/ARM_HYP/Arch_C.thy @@ -4237,6 +4237,17 @@ lemma decodeARMMMUInvocation_ccorres: elim!: ccap_relationE split: if_split_asm) done +lemma vcpu_reg_saved_when_disabled_spec: + "\s. \ \ {s} + Call vcpu_reg_saved_when_disabled_'proc + \ \ret__unsigned_long = from_bool (\<^bsup>s\<^esup>field = scast seL4_VCPUReg_SCTLR) \" + 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 \ None \ (cvcpuopt \ None \ fst (the cvcpuopt) = vcpuptr) }" and Q="\s. vcpuptr \ 0 \ (armHSCurVCPU \ 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) \ \C register comparison into reg comparison\ + subgoal by (fastforce dest: rf_sr_ksArchState_armHSCurVCPU simp: cur_vcpu_relation_def + split: option.splits) apply (rule ccorres_Cond_rhs) - \ \vcpuptr is current vcpu\ 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 \ \curvcpuactive }" and Q="\s. (armHSCurVCPU \ 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 \ \no current vcpu\ apply clarsimp apply wpc - apply (subgoal_tac "\ x1") - prefer 2 - apply fastforce + apply (rename_tac cur b, prop_tac "\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 \ None \ (cvcpuopt \ None \ fst (the cvcpuopt) = vcpuptr) }" and Q="\s. vcpuptr \ 0 \ (armHSCurVCPU \ 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) \ \C register comparison into reg comparison\ apply (rule ccorres_Cond_rhs) \ \vcpuptr is current vcpu\ 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 \ \curvcpuactive }" and Q="\s. (armHSCurVCPU \ 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=\ and A'=UNIV in ccorres_guard_imp) - apply (rule ccorres_Cond_rhs ; clarsimp) - \ \SCTLR\ - 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 \]) + 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 - \ \any other hyp register\ - 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 + \ \no current vcpu\ apply clarsimp apply wpc - apply (subgoal_tac "\ x1") - prefer 2 - apply fastforce + apply (rename_tac cur b, prop_tac "\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 diff --git a/spec/abstract/ARM_HYP/VCPU_A.thy b/spec/abstract/ARM_HYP/VCPU_A.thy index fedcb4912..3869654af 100644 --- a/spec/abstract/ARM_HYP/VCPU_A.thy +++ b/spec/abstract/ARM_HYP/VCPU_A.thy @@ -67,9 +67,8 @@ where | _ \ (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 \ \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 | _ \ (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 \ \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" diff --git a/spec/haskell/src/SEL4/Machine/RegisterSet/ARM.lhs b/spec/haskell/src/SEL4/Machine/RegisterSet/ARM.lhs index e0cddafc5..8d589aca8 100644 --- a/spec/haskell/src/SEL4/Machine/RegisterSet/ARM.lhs +++ b/spec/haskell/src/SEL4/Machine/RegisterSet/ARM.lhs @@ -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)] diff --git a/spec/haskell/src/SEL4/Object/VCPU/ARM.lhs b/spec/haskell/src/SEL4/Object/VCPU/ARM.lhs index 908d2174f..c0c0f9596 100644 --- a/spec/haskell/src/SEL4/Object/VCPU/ARM.lhs +++ b/spec/haskell/src/SEL4/Object/VCPU/ARM.lhs @@ -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