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

SELFOUR-444: Adjust Haskell, new ghost data. 

The new ghost data is saved in the design spec when Untyped caps
are modified and will be used by CRefine.
This commit is contained in:
Thomas Sewell 2016-05-30 23:12:15 +10:00
parent a96346e308
commit 6ad456ca03
16 changed files with 142 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
lib/DataMap.thy
View File

@ -50,4 +50,13 @@ where
None \<Rightarrow> None
| Some y \<Rightarrow> if f x y then Some y else None"
abbreviation(input)
"data_set_empty \<equiv> {}"
abbreviation(input)
"data_set_insert \<equiv> insert"
abbreviation(input)
"data_set_delete x S \<equiv> S - {x}"
end

3
spec/design/ARM/ArchVSpace_H.thy
View File

@ -17,6 +17,7 @@
theory ArchVSpace_H
imports
"../CNode_H"
"../Untyped_H"
"../KI_Decls_H"
ArchVSpaceDecls_H
begin
@ -1396,7 +1397,7 @@ defs performASIDControlInvocation_def:
(MakePool frame slot parent base) \<Rightarrow> (do
deleteObjects frame pageBits;
pcap \<leftarrow> getSlotCap parent;
updateCap parent (pcap \<lparr>capFreeIndex := maxFreeIndex (capBlockSize pcap) \<rparr>);
updateFreeIndex parent (maxFreeIndex (capBlockSize pcap));
placeNewObject frame (makeObject ::asidpool) 0;
poolPtr \<leftarrow> return ( PPtr $ fromPPtr frame);
cteInsert (ArchObjectCap $ ASIDPoolCap poolPtr base) parent slot;

1
spec/design/KernelInit_H.thy
View File

@ -316,6 +316,7 @@ newKernelState_def:
ksPSpace= newPSpace,
gsUserPages= (\<lambda>x. None),
gsCNodes= (\<lambda>x. None),
gsUntypedZeroRanges= {},
gsMaxObjectSize = card (UNIV :: machine_word set),
ksDomScheduleIdx = newKSDomScheduleIdx,
ksDomSchedule = newKSDomSchedule,

1
spec/design/KernelStateData_H.thy
View File

@ -49,6 +49,7 @@ record kernel_state =
ksPSpace :: pspace
gsUserPages :: "machine_word \<Rightarrow> vmpage_size option"
gsCNodes :: "machine_word \<Rightarrow> nat option"
gsUntypedZeroRanges :: "(machine_word \<times> machine_word) set"
gsMaxObjectSize :: nat
ksDomScheduleIdx :: nat
ksDomSchedule :: "(domain \<times> machine_word) list"

44
spec/design/Untyped_H.thy
View File

@ -111,6 +111,40 @@ where
else IllegalOperation
)"
definition
untypedZeroRange :: "capability \<Rightarrow> (machine_word * machine_word) option"
where
"untypedZeroRange x0\<equiv> (let cap = x0 in
if isUntypedCap cap
then
let
empty = capFreeIndex cap = maxFreeIndex (capBlockSize cap);
startPtr = getFreeRef (capPtr cap) (capFreeIndex cap);
endPtr = capPtr cap + PPtr (2 ^ capBlockSize cap) - 1
in
if empty then Nothing
else Just (fromPPtr startPtr, fromPPtr endPtr)
else Nothing
)"
definition
updateFreeIndex :: "machine_word \<Rightarrow> nat \<Rightarrow> unit kernel"
where
"updateFreeIndex slot idx\<equiv> (do
cap \<leftarrow> getSlotCap slot;
modify (\<lambda> ks. (case untypedZeroRange (cap \<lparr>capFreeIndex := idx\<rparr>) of
None \<Rightarrow> ks
| Some r \<Rightarrow> ks \<lparr>gsUntypedZeroRanges := data_set_insert
r (gsUntypedZeroRanges ks)\<rparr>)
);
updateCap slot (cap \<lparr>capFreeIndex := idx\<rparr>);
modify (\<lambda> ks. (case untypedZeroRange cap of
None \<Rightarrow> ks
| Some r \<Rightarrow> ks \<lparr>gsUntypedZeroRanges := data_set_delete
r (gsUntypedZeroRanges ks)\<rparr>)
)
od)"
definition
resetUntypedCap :: "machine_word \<Rightarrow> unit kernel_p"
where
@ -122,7 +156,7 @@ where
then withoutPreemption $ (do
unless (capIsDevice cap) $ doMachineOp $
clearMemory (PPtr (fromPPtr (capPtr cap))) (1 `~shiftL~` sz);
updateCap slot (cap \<lparr>capFreeIndex := 0\<rparr>)
updateFreeIndex slot 0
od)
else (
forME_x (reverse [capPtr cap, capPtr cap + (1 `~shiftL~` resetChunkBits) .e.
@ -130,8 +164,8 @@ where
(\<lambda> addr. (doE
withoutPreemption $ doMachineOp $ clearMemory
(PPtr (fromPPtr addr)) (1 `~shiftL~` resetChunkBits);
withoutPreemption $ updateCap slot (cap \<lparr>capFreeIndex
:= getFreeIndex (capPtr cap) addr\<rparr>);
withoutPreemption $ updateFreeIndex slot
(getFreeIndex (capPtr cap) addr);
preemptionPoint
odE))
)
@ -144,15 +178,13 @@ where
(Retype srcSlot reset base retypeBase newType userSize destSlots isDev) \<Rightarrow> (doE
whenE reset $ resetUntypedCap srcSlot;
withoutPreemption $ (do
cap \<leftarrow> getSlotCap srcSlot;
totalObjectSize \<leftarrow> return ( (length destSlots) `~shiftL~` (getObjectSize newType userSize));
stateAssert (\<lambda> x. Not (cNodeOverlap (gsCNodes x)
(\<lambda> x. fromPPtr retypeBase \<le> x
\<and> x \<le> fromPPtr retypeBase + fromIntegral totalObjectSize - 1)))
[];
freeRef \<leftarrow> return ( retypeBase + PPtr (fromIntegral totalObjectSize));
updateCap srcSlot
(cap \<lparr>capFreeIndex := getFreeIndex base freeRef\<rparr>);
updateFreeIndex srcSlot (getFreeIndex base freeRef);
createNewObjects newType srcSlot destSlots retypeBase userSize isDev
od)
odE)

1
spec/design/skel/ARM/ArchVSpace_H.thy
View File

@ -15,6 +15,7 @@
theory ArchVSpace_H
imports
"../CNode_H"
"../Untyped_H"
"../KI_Decls_H"
ArchVSpaceDecls_H
begin

1
spec/design/skel/KernelInit_H.thy
View File

@ -63,6 +63,7 @@ newKernelState_def:
ksPSpace= newPSpace,
gsUserPages= (\<lambda>x. None),
gsCNodes= (\<lambda>x. None),
gsUntypedZeroRanges= {},
gsMaxObjectSize = card (UNIV :: machine_word set),
ksDomScheduleIdx = newKSDomScheduleIdx,
ksDomSchedule = newKSDomSchedule,

1
spec/design/skel/KernelStateData_H.thy
View File

@ -47,6 +47,7 @@ record kernel_state =
ksPSpace :: pspace
gsUserPages :: "machine_word \<Rightarrow> vmpage_size option"
gsCNodes :: "machine_word \<Rightarrow> nat option"
gsUntypedZeroRanges :: "(machine_word \<times> machine_word) set"
gsMaxObjectSize :: nat
ksDomScheduleIdx :: nat
ksDomSchedule :: "(domain \<times> machine_word) list"

6
spec/haskell/src/SEL4/Kernel/Init.lhs
View File

@ -25,6 +25,7 @@ This module contains functions that create a new kernel state and set up the add
> import SEL4.API.Failures
> import SEL4.Model
> import SEL4.Object
> import SEL4.Object.Structures
> import SEL4.Machine
> import SEL4.Kernel.Thread
> import SEL4.Kernel.VSpace
@ -369,11 +370,12 @@ Specific allocRegion for convenience, since most allocations are frame-sized.
> bifUntypedObjSizeBits = untypedObjs' ++ [sizeBits],
> bifUntypedObjIsDeviceList = untypedDevices ++ [isDevice] }
> noInitFailure $ modify (\st -> st { initBootInfo = bootInfo' })
> let size = fromIntegral sizeBits
> provideCap rootCNodeCap $ UntypedCap {
> capIsDevice = isDevice,
> capPtr = ptrFromPAddr pptr,
> capBlockSize = fromIntegral sizeBits,
> capFreeIndex = 0 }
> capBlockSize = size,
> capFreeIndex = maxFreeIndex size }
\subsection{Helper Functions}

2
spec/haskell/src/SEL4/Kernel/VSpace/ARM.lhs
View File

@ -1447,7 +1447,7 @@ the PT/PD is consistent.
> performASIDControlInvocation (MakePool frame slot parent base) = do
> deleteObjects frame pageBits
> pcap <- getSlotCap parent
> updateCap parent (pcap {capFreeIndex = maxFreeIndex (capBlockSize pcap) })
> updateFreeIndex parent (maxFreeIndex (capBlockSize pcap))
> placeNewObject frame (makeObject :: ASIDPool) 0
> let poolPtr = PPtr $ fromPPtr frame
> cteInsert (ArchObjectCap $ ASIDPoolCap poolPtr base) parent slot

3
spec/haskell/src/SEL4/Model/StateData.lhs
View File

@ -39,6 +39,7 @@ The architecture-specific definitions are imported qualified with the "Arch" pre
> import SEL4.Machine.Hardware.TARGET (VMPageSize)
> import Data.Array
> import qualified Data.Set
> import Data.Helpers
> import Control.Monad
> import Control.Monad.State
@ -62,6 +63,7 @@ The top-level kernel state structure is called "KernelState". It contains:
> gsUserPages :: Word -> (Maybe VMPageSize),
> gsCNodes :: Word -> (Maybe Int),
> gsUntypedZeroRanges :: Data.Set.Set (Word, Word),
\item the cyclic domain schedule;
@ -219,6 +221,7 @@ A new kernel state structure contains an empty physical address space, a set of
> ksPSpace = newPSpace,
> gsUserPages = (\_ -> Nothing),
> gsCNodes = (\_ -> Nothing),
> gsUntypedZeroRanges = Data.Set.empty,
> ksDomScheduleIdx = 0,
> ksDomSchedule = [(0, 15), (2, 42), (1, 73)],
> ksCurDomain = 0,

45
spec/haskell/src/SEL4/Object/CNode.lhs
View File

@ -20,13 +20,14 @@ creating the "Capability" objects used at higher levels of the kernel.
> getSlotCap, locateSlotTCB, locateSlotCNode, locateSlotCap,
> locateSlotBasic, getReceiveSlots, getCTE, setupReplyMaster,
> insertInitCap, decodeCNodeInvocation, invokeCNode,
> updateCap, isFinalCapability, createNewObjects
> updateCap, isFinalCapability, createNewObjects,
> updateFreeIndex
> ) where
\begin{impdetails}
> {-# BOOT-IMPORTS: SEL4.Machine SEL4.API.Types SEL4.API.Failures SEL4.Model SEL4.Object.Structures SEL4.API.Invocation #-}
> {-# BOOT-EXPORTS: ensureNoChildren getSlotCap locateSlotTCB locateSlotCNode locateSlotCap locateSlotBasic ensureEmptySlot insertInitCap cteInsert cteDelete cteDeleteOne decodeCNodeInvocation invokeCNode getCTE updateCap isFinalCapability createNewObjects #-}
> {-# BOOT-EXPORTS: ensureNoChildren getSlotCap locateSlotTCB locateSlotCNode locateSlotCap locateSlotBasic ensureEmptySlot insertInitCap cteInsert cteDelete cteDeleteOne decodeCNodeInvocation invokeCNode getCTE updateCap isFinalCapability createNewObjects updateFreeIndex #-}
> import SEL4.API.Types
> import SEL4.API.Failures
@ -42,6 +43,7 @@ creating the "Capability" objects used at higher levels of the kernel.
> import {-# SOURCE #-} SEL4.Kernel.CSpace
> import Data.Bits
> import qualified Data.Set
\end{impdetails}
@ -391,6 +393,7 @@ the bitmask bit that will allow the reissue of an IRQHandlerCap to this IRQ.
> emptySlot :: PPtr CTE -> Maybe IRQ -> Kernel ()
> emptySlot slot irq = do
> clearUntypedFreeIndex slot
> newCTE <- getCTE slot
> let mdbNode = cteMDBNode newCTE
> let prev = mdbPrev mdbNode
@ -580,6 +583,7 @@ The following function inserts a new revocable cap as a child of another.
> setCTE slot $ CTE cap (MDB next parent True True)
> updateMDB next $ (\m -> m { mdbPrev = slot })
> updateMDB parent $ (\m -> m { mdbNext = slot })
> updateNewFreeIndex slot
The following function is used by the bootstrap code to create the initial set of capabilities.
@ -614,6 +618,43 @@ This function is used in the assertion above; it returns "True" if no reply capa
> noReplyCapsFor :: PPtr TCB -> KernelState -> Bool
> noReplyCapsFor _ _ = True
These functions concern the free indices of untyped caps. For verification reasons we also track the free ranges in a ghost variable, which must be updated appropriately when untyped caps might be changed.
> updateTrackedFreeIndex :: PPtr CTE -> Int -> Kernel ()
> updateTrackedFreeIndex slot idx = do
> cap <- getSlotCap slot
> modify (\ks -> ks {gsUntypedZeroRanges =
> case untypedZeroRange cap of
> Nothing -> gsUntypedZeroRanges ks
> Just r -> Data.Set.delete r (gsUntypedZeroRanges ks)
> })
> modify (\ks -> ks {gsUntypedZeroRanges =
> case untypedZeroRange (cap {capFreeIndex = idx}) of
> Nothing -> gsUntypedZeroRanges ks
> Just r -> Data.Set.insert r (gsUntypedZeroRanges ks)
> })
> updateFreeIndex :: PPtr CTE -> Int -> Kernel ()
> updateFreeIndex slot idx = do
> updateTrackedFreeIndex slot idx
> cap <- getSlotCap slot
> updateCap slot (cap {capFreeIndex = idx})
> clearUntypedFreeIndex :: PPtr CTE -> Kernel ()
> clearUntypedFreeIndex slot = do
> cap <- getSlotCap slot
> case cap of
> UntypedCap {} -> updateTrackedFreeIndex slot
> (maxFreeIndex (capBlockSize cap))
> _ -> return ()
> updateNewFreeIndex :: PPtr CTE -> Kernel ()
> updateNewFreeIndex slot = do
> cap <- getSlotCap slot
> case cap of
> UntypedCap {} -> updateTrackedFreeIndex slot (capFreeIndex cap)
> _ -> return ()
\subsection{MDB Operations}
\label{sec:object.cnode.mdb}

19
spec/haskell/src/SEL4/Object/Structures.lhs
View File

@ -465,9 +465,26 @@ This type is used to represent a frame in the user's address space.
> data UserDataDevice = UserDataDevice
\subsubsection{The max free index of a UntypedCap}
\subsubsection{The Untyped free index}
Various operations on the free index of an Untyped cap.
> maxFreeIndex :: Int -> Int
> maxFreeIndex sizeBits = bit sizeBits
> getFreeRef :: PPtr () -> Int -> PPtr ()
> getFreeRef base freeIndex = base + (fromIntegral freeIndex)
> getFreeIndex :: PPtr () -> PPtr () -> Int
> getFreeIndex base free = fromIntegral $ fromPPtr (free - base)
> untypedZeroRange :: Capability -> Maybe (Word, Word)
> untypedZeroRange (cap@UntypedCap {}) = if empty then Nothing
> else Just (fromPPtr startPtr, fromPPtr endPtr)
> where
> empty = capFreeIndex cap == maxFreeIndex (capBlockSize cap)
> startPtr = getFreeRef (capPtr cap) (capFreeIndex cap)
> endPtr = capPtr cap + PPtr (2 ^ capBlockSize cap) - 1
> untypedZeroRange _ = Nothing

34
spec/haskell/src/SEL4/Object/Untyped.lhs
View File

@ -26,19 +26,12 @@ This module defines the behavior of untyped objects.
> import SEL4.Object.Structures
> import SEL4.Object.Instances()
> import {-# SOURCE #-} SEL4.Object.CNode
> import {-# SOURCE #-} SEL4.Kernel.CSpace
> import Data.Bits
\end{impdetails}
> getFreeRef :: PPtr () -> Int -> PPtr ()
> getFreeRef base freeIndex = base + (fromIntegral freeIndex)
> getFreeIndex :: PPtr () -> PPtr () -> Int
> getFreeIndex base free = fromIntegral $ fromPPtr (free - base)
\subsection{Invocation}
Invocation of an untyped object retypes the memory region, possibly creating
@ -180,27 +173,27 @@ A Retype operation may begin with a reset of an Untyped cap. This returns the fr
> resetUntypedCap slot = do
> cap <- withoutPreemption $ getSlotCap slot
> let sz = capBlockSize cap
> unless (capFreeIndex cap == 0) $ do
\begin{impdetails}
The objects in the Haskell model are removed at this time. This operation is specific to the Haskell physical memory model, in which memory objects are typed; it is not necessary (or possible) when running on real hardware.
> withoutPreemption $ deleteObjects (capPtr cap) sz
> withoutPreemption $ deleteObjects (capPtr cap) sz
\end{impdetails}
> if (capIsDevice cap || sz < resetChunkBits)
> then withoutPreemption $ do
> unless (capIsDevice cap) $ doMachineOp $
> clearMemory (PPtr (fromPPtr (capPtr cap))) (1 `shiftL` sz)
> updateCap slot (cap {capFreeIndex = 0})
> else do
> forM_ (reverse [capPtr cap, capPtr cap + (1 `shiftL` resetChunkBits) ..
> getFreeRef (capPtr cap) (capFreeIndex cap) - 1])
> if (capIsDevice cap || sz < resetChunkBits)
> then withoutPreemption $ do
> unless (capIsDevice cap) $ doMachineOp $
> clearMemory (PPtr (fromPPtr (capPtr cap))) (1 `shiftL` sz)
> updateFreeIndex slot 0
> else forM_ (reverse [capPtr cap, capPtr cap + (1 `shiftL` resetChunkBits) ..
> getFreeRef (capPtr cap) (capFreeIndex cap) - 1])
> $ \addr -> do
> withoutPreemption $ doMachineOp $ clearMemory
> (PPtr (fromPPtr addr)) (1 `shiftL` resetChunkBits)
> withoutPreemption $ updateCap slot (cap {capFreeIndex
> = getFreeIndex (capPtr cap) addr})
> withoutPreemption $ updateFreeIndex slot
> (getFreeIndex (capPtr cap) addr)
> preemptionPoint
> invokeUntyped :: UntypedInvocation -> KernelP ()
@ -208,7 +201,6 @@ The objects in the Haskell model are removed at this time. This operation is spe
> when reset $ resetUntypedCap srcSlot
> withoutPreemption $ do
> cap <- getSlotCap srcSlot
For verification purposes a check is made that the region the objects are created in does not overlap with any existing CNodes.
@ -218,8 +210,7 @@ For verification purposes a check is made that the region the objects are create
> && x <= fromPPtr retypeBase + fromIntegral totalObjectSize - 1)))
> "CNodes present in region to be retyped."
> let freeRef = retypeBase + PPtr (fromIntegral totalObjectSize)
> updateCap srcSlot
> (cap {capFreeIndex = getFreeIndex base freeRef})
> updateFreeIndex srcSlot (getFreeIndex base freeRef)
Create the new objects and insert caps to these objects into the destination slots.
@ -230,3 +221,4 @@ This function performs the check that CNodes do not overlap with the retyping re
> cNodeOverlap :: (Word -> Maybe Int) -> (Word -> Bool) -> Bool
> cNodeOverlap _ _ = False

5
tools/haskell-translator/caseconvs
View File

@ -1612,3 +1612,8 @@ case \x of (ArchInvocationLabel X64PDPTMap, vaddr':attr:_, (vspaceCap,_):_) -> (
case \x of ArchObjectCap (frame@PageCap {capVPIsDevice = False}) -> _ -> ---X>
case \x of (cap@UntypedCap {}) -> _ -> ---> let cap = \x in
if isUntypedCap cap
then ->1
else ->2

1
tools/haskell-translator/lhs_pars.py
View File

@ -2137,6 +2137,7 @@ regexes = [
(re.compile(r"\.\|\."), '||'),
(re.compile(r"Data\.Word\.Word"), r"word"),
(re.compile(r"Data\.Map\."), r"data_map_"),
(re.compile(r"Data\.Set\."), r"data_set_"),
(re.compile(r"BinaryTree\."), 'bt_'),
(re.compile("mapM_"), "mapM_x"),
(re.compile("forM_"), "forM_x"),