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

x64: spec: fix up definition of decodeX64FrameInvocation to match C

This commit is contained in:
Joel Beeren 2018-06-29 12:11:47 +10:00
parent 5ed7bb16be
commit e6ca6883ad
3 changed files with 16 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
spec/abstract/X64/ArchDecode_A.thy
View File

@ -346,7 +346,7 @@ where
| _ \<Rightarrow> throwError $ InvalidCapability 1);
vspace' \<leftarrow> lookup_error_on_failure False $ find_vspace_for_asid asid;
whenE (vspace' \<noteq> vspace) $ throwError $ InvalidCapability 1;
vtop \<leftarrow> returnOk $ vaddr + mask (pageBitsForSize pgsz);
vtop \<leftarrow> returnOk $ vaddr + bit (pageBitsForSize pgsz);
whenE (vtop > user_vtop) $ throwError $ InvalidArgument 0;
vm_rights \<leftarrow> 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 \<noteq> VMVSpaceMap) $ throwError IllegalOperation;
(vspace,asid) \<leftarrow> (case vspace_cap of
ArchObjectCap (PML4Cap pm (Some asid)) \<Rightarrow>
returnOk (pm, asid)
@ -372,12 +371,13 @@ where
(asid',vaddr) \<leftarrow> (case mapped_address of
Some a \<Rightarrow> returnOk a
| _ \<Rightarrow> throwError $ InvalidCapability 0);
vspace' \<leftarrow> lookup_error_on_failure False $ find_vspace_for_asid asid;
vspace' \<leftarrow> lookup_error_on_failure False $ find_vspace_for_asid asid';
whenE (vspace' \<noteq> vspace \<or> asid \<noteq> asid') $ throwError $ InvalidCapability 1;
vm_rights \<leftarrow> returnOk $ mask_vm_rights R $ data_to_rights rights_mask;
check_vp_alignment pgsz vaddr;
entries \<leftarrow> 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

10
spec/abstract/X64/ArchVSpace_A.thy
View File

@ -65,19 +65,14 @@ where
|
"ensure_safe_mapping (VMPDPTE InvalidPDPTE, _) = returnOk ()"
|
"ensure_safe_mapping (VMPTE (SmallPagePTE _ _ _), pt_slot) =
doE
pte \<leftarrow> liftE $ get_pte pt_slot;
(case pte of
InvalidPTE \<Rightarrow> returnOk ()
| _ \<Rightarrow> throwError DeleteFirst)
odE"
"ensure_safe_mapping (VMPTE (SmallPagePTE _ _ _), pt_slot) = returnOk ()"
|
"ensure_safe_mapping (VMPDE (LargePagePDE _ _ _), pd_slot) =
doE
pde \<leftarrow> liftE $ get_pde pd_slot;
(case pde of
InvalidPDE \<Rightarrow> returnOk ()
| LargePagePDE _ _ _ \<Rightarrow> returnOk ()
| _ \<Rightarrow> throwError DeleteFirst)
odE"
|
@ -86,6 +81,7 @@ where
pdpt \<leftarrow> liftE $ get_pdpte pdpt_slot;
(case pdpt of
InvalidPDPTE \<Rightarrow> returnOk ()
| HugePagePDPTE _ _ _ \<Rightarrow> returnOk ()
| _ \<Rightarrow> throwError DeleteFirst)
odE"
|

22
spec/haskell/src/SEL4/Kernel/VSpace/X64.lhs
View File

@ -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,