From e6ca6883ad9c879552df360b2827a399cc2c9154 Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Fri, 29 Jun 2018 12:11:47 +1000 Subject: [PATCH] x64: spec: fix up definition of decodeX64FrameInvocation to match C --- spec/abstract/X64/ArchDecode_A.thy | 8 ++++---- spec/abstract/X64/ArchVSpace_A.thy | 10 +++------- spec/haskell/src/SEL4/Kernel/VSpace/X64.lhs | 22 +++++++++------------ 3 files changed, 16 insertions(+), 24 deletions(-) diff --git a/spec/abstract/X64/ArchDecode_A.thy b/spec/abstract/X64/ArchDecode_A.thy index 63da752c9..50c66d509 100644 --- a/spec/abstract/X64/ArchDecode_A.thy +++ b/spec/abstract/X64/ArchDecode_A.thy @@ -346,7 +346,7 @@ where | _ \ throwError $ InvalidCapability 1); vspace' \ lookup_error_on_failure False $ find_vspace_for_asid asid; whenE (vspace' \ vspace) $ throwError $ InvalidCapability 1; - vtop \ returnOk $ vaddr + mask (pageBitsForSize pgsz); + vtop \ returnOk $ vaddr + bit (pageBitsForSize pgsz); whenE (vtop > user_vtop) $ throwError $ InvalidArgument 0; vm_rights \ returnOk $ mask_vm_rights R (data_to_rights rights_mask); check_vp_alignment pgsz vaddr; @@ -363,8 +363,7 @@ where attr = args ! 1; vspace_cap = fst (extra_caps ! 0) in doE - (* FIXME x64-vtd: *) - (* whenE (map_type = VMIOSpaceMap) $ throwError IllegalOperation; *) + whenE (map_type \ VMVSpaceMap) $ throwError IllegalOperation; (vspace,asid) \ (case vspace_cap of ArchObjectCap (PML4Cap pm (Some asid)) \ returnOk (pm, asid) @@ -372,12 +371,13 @@ where (asid',vaddr) \ (case mapped_address of Some a \ returnOk a | _ \ throwError $ InvalidCapability 0); - vspace' \ lookup_error_on_failure False $ find_vspace_for_asid asid; + vspace' \ lookup_error_on_failure False $ find_vspace_for_asid asid'; whenE (vspace' \ vspace \ asid \ asid') $ throwError $ InvalidCapability 1; vm_rights \ returnOk $ mask_vm_rights R $ data_to_rights rights_mask; check_vp_alignment pgsz vaddr; entries \ create_mapping_entries (addrFromPPtr p) vaddr pgsz vm_rights (attribs_from_word attr) vspace; + ensure_safe_mapping entries; returnOk $ InvokePage $ PageRemap entries asid vspace odE else throwError TruncatedMessage diff --git a/spec/abstract/X64/ArchVSpace_A.thy b/spec/abstract/X64/ArchVSpace_A.thy index 02b540d33..95af80ee4 100644 --- a/spec/abstract/X64/ArchVSpace_A.thy +++ b/spec/abstract/X64/ArchVSpace_A.thy @@ -65,19 +65,14 @@ where | "ensure_safe_mapping (VMPDPTE InvalidPDPTE, _) = returnOk ()" | -"ensure_safe_mapping (VMPTE (SmallPagePTE _ _ _), pt_slot) = - doE - pte \ liftE $ get_pte pt_slot; - (case pte of - InvalidPTE \ returnOk () - | _ \ throwError DeleteFirst) - odE" +"ensure_safe_mapping (VMPTE (SmallPagePTE _ _ _), pt_slot) = returnOk ()" | "ensure_safe_mapping (VMPDE (LargePagePDE _ _ _), pd_slot) = doE pde \ liftE $ get_pde pd_slot; (case pde of InvalidPDE \ returnOk () + | LargePagePDE _ _ _ \ returnOk () | _ \ throwError DeleteFirst) odE" | @@ -86,6 +81,7 @@ where pdpt \ liftE $ get_pdpte pdpt_slot; (case pdpt of InvalidPDPTE \ returnOk () + | HugePagePDPTE _ _ _ \ returnOk () | _ \ throwError DeleteFirst) odE" | diff --git a/spec/haskell/src/SEL4/Kernel/VSpace/X64.lhs b/spec/haskell/src/SEL4/Kernel/VSpace/X64.lhs index 333dff09f..95ce78ccf 100644 --- a/spec/haskell/src/SEL4/Kernel/VSpace/X64.lhs +++ b/spec/haskell/src/SEL4/Kernel/VSpace/X64.lhs @@ -123,22 +123,20 @@ The following function is called before creating or modifying mappings in a page > ensureSafeMapping (VMPDE InvalidPDE, _) = return () > ensureSafeMapping (VMPDPTE InvalidPDPTE, _) = return () > -> ensureSafeMapping (VMPTE (SmallPagePTE {}), VMPTEPtr slot) = do -> pte <- withoutFailure $ getObject slot -> case pte of -> InvalidPTE -> return () -> _ -> throw DeleteFirst +> ensureSafeMapping (VMPTE (SmallPagePTE {}), VMPTEPtr slot) = return () > > ensureSafeMapping (VMPDE (LargePagePDE {}), VMPDEPtr slot) = do > pde <- withoutFailure $ getObject slot > case pde of > InvalidPDE -> return () +> LargePagePDE {} -> return () > _ -> throw DeleteFirst > > ensureSafeMapping (VMPDPTE (HugePagePDPTE {}), VMPDPTEPtr slot) = do > pdpte <- withoutFailure $ getObject slot > case pdpte of > InvalidPDPTE -> return () +> HugePagePDPTE {} -> return () > _ -> throw DeleteFirst > > ensureSafeMapping _ = fail "This should never happen" @@ -539,7 +537,7 @@ Note that implementations with separate high and low memory regions may also wis > vspaceCheck <- lookupErrorOnFailure False $ findVSpaceForASID asid > when (vspaceCheck /= vspace) $ throw $ InvalidCapability 1 > let vaddr' = vaddr .&. userVTop -> let vtop = vaddr' + (bit (pageBitsForSize $ capVPSize cap) - 1) +> let vtop = vaddr' + bit (pageBitsForSize $ capVPSize cap) > when (VPtr vtop > VPtr userVTop) $ > throw $ InvalidArgument 0 > let vmRights = maskVMRights (capVPRights cap) $ @@ -556,26 +554,24 @@ Note that implementations with separate high and low memory regions may also wis > pageMapVSpace = vspace } > (ArchInvocationLabel X64PageMap, _, _) -> throw TruncatedMessage > (ArchInvocationLabel X64PageRemap, rightsMask:attr:_, (vspaceCap,_):_) -> do ->-- FIXME x64-vtd: ->-- when (capVPMapType cap == VMIOSpaceMap) $ throw IllegalOperation +> when (capVPMapType cap /= VMVSpaceMap) $ throw IllegalOperation > (vspace,asid) <- case vspaceCap of > ArchObjectCap (PML4Cap { > capPML4MappedASID = Just asid, > capPML4BasePtr = vspace }) > -> return (vspace,asid) > _ -> throw $ InvalidCapability 1 -> (asid',vaddr) <- case capVPMappedAddress cap of +> (asidCheck, vaddr) <- case capVPMappedAddress cap of > Just v -> return v > _ -> throw $ InvalidCapability 0 -> vspaceCheck <- lookupErrorOnFailure False $ findVSpaceForASID asid -> when (vspaceCheck /= vspace || asid /= asid') $ throw $ InvalidCapability 1 -> -- asidCheck not required because ASIDs and HWASIDs are the same on x86 +> vspaceCheck <- lookupErrorOnFailure False $ findVSpaceForASID asidCheck +> when (vspaceCheck /= vspace || asid /= asidCheck) $ throw $ InvalidCapability 1 > let vmRights = maskVMRights (capVPRights cap) $ > rightsFromWord rightsMask > checkVPAlignment (capVPSize cap) vaddr > entries <- createMappingEntries (addrFromPPtr $ capVPBasePtr cap) > vaddr (capVPSize cap) vmRights (attribsFromWord attr) vspace -> -- x64 allows arbitrary remapping, so no need to call ensureSafeMapping +> ensureSafeMapping entries > return $ InvokePage $ PageRemap { > pageRemapEntries = entries, > pageRemapASID = asid,