1% Copyright 2014, General Dynamics C4 Systems
2%
3% This software may be distributed and modified according to the terms of
4% the GNU General Public License version 2. Note that NO WARRANTY is provided.
5% See "LICENSE_GPLv2.txt" for details.
6%
7% @TAG(GD_GPL)
8%
9
10This module defines IO port routines, specific to x64.
11
12> module SEL4.Object.IOPort.X64 where
13
14\begin{impdetails}
15
16> {-# BOOT-IMPORTS: SEL4.Machine SEL4.Model SEL4.Object.Structures SEL4.Object.Instances() SEL4.API.Failures SEL4.API.Invocation.X64%ArchInv #-}
17> {-# BOOT-EXPORTS: performX64PortInvocation decodeX64PortInvocation #-}
18
19> import Prelude hiding (Word)
20> import SEL4.Machine
21> import SEL4.API.Types
22> import SEL4.API.Failures
23> import SEL4.Machine.Hardware.X64
24> import SEL4.Model
25> import SEL4.Model.StateData.X64
26> import SEL4.Object.Structures
27> import SEL4.Object.TCB
28> import SEL4.Object.ObjectType.X64
29> import SEL4.API.Invocation.X64 as ArchInv
30> import SEL4.API.InvocationLabels
31> import SEL4.API.InvocationLabels.X64
32> import SEL4.Object.CNode
33> import SEL4.Kernel.CSpace
34
35> import Data.Bool
36> import Data.Array
37> import Data.Word(Word32)
38
39\end{impdetails}
40
41> ensurePortOperationAllowed :: ArchCapability -> Word32 -> Int ->
42>     KernelF SyscallError ()
43> ensurePortOperationAllowed (IOPortCap { capIOPortFirstPort = first_allowed, capIOPortLastPort = last_allowed }) start_port size = do
44>     let end_port = start_port + fromIntegral size - 1
45>     assert (first_allowed <= last_allowed) "first allowed must be less than last allowed"
46>     assert (start_port <= end_port) "first requested must be less than last requested"
47>     when ((start_port < fromIntegral first_allowed) || (end_port > fromIntegral last_allowed)) $
48>         throw IllegalOperation
49> ensurePortOperationAllowed _ _ _ = fail "Unreachable"
50
51> isIOPortRangeFree :: IOPort -> IOPort -> Kernel Bool
52> isIOPortRangeFree f l = do
53>     ports <- gets (x64KSAllocatedIOPorts . ksArchState)
54>     return $ not $ foldl (\x y -> x || ports ! y) False [f..l]
55
56%FIXME port+output data packing in C, see SELFOUR-360
57
58%FIXME downcast to 16-bit port from 64-bit arg happens before range check, which
59%      is likely incorrect
60
61> decodeX64PortInvocation :: Word -> [Word] -> PPtr CTE ->
62>         ArchCapability -> [Capability] -> KernelF SyscallError ArchInv.Invocation
63> decodeX64PortInvocation label args _ cap@(IOPortCap {}) _  = do
64>     case (invocationType label, args) of
65>         (ArchInvocationLabel X64IOPortIn8, port':_) -> do
66>             let port = (fromIntegral port') :: IOPort
67>             ensurePortOperationAllowed cap (fromIntegral port) 1
68>             return $ InvokeIOPort $ IOPortInvocation port $ IOPortIn8
69>         (ArchInvocationLabel X64IOPortIn8, _) -> throw TruncatedMessage
70>         (ArchInvocationLabel X64IOPortIn16, port':_) -> do
71>             let port = (fromIntegral port') :: IOPort
72>             ensurePortOperationAllowed cap (fromIntegral port) 2
73>             return $ InvokeIOPort $ IOPortInvocation port $ IOPortIn16
74>         (ArchInvocationLabel X64IOPortIn16, _) -> throw TruncatedMessage
75>         (ArchInvocationLabel X64IOPortIn32, port':_) -> do
76>             let port = (fromIntegral port') :: IOPort
77>             ensurePortOperationAllowed cap (fromIntegral port) 4
78>             return $ InvokeIOPort $ IOPortInvocation port $ IOPortIn32
79>         (ArchInvocationLabel X64IOPortIn32, _) -> throw TruncatedMessage
80>         (ArchInvocationLabel X64IOPortOut8, port':out:_) -> do
81>             let port = (fromIntegral port') :: IOPort
82>             ensurePortOperationAllowed cap (fromIntegral port) 1
83>             let output_data = fromIntegral out
84>             return $ InvokeIOPort $ IOPortInvocation port $ IOPortOut8 output_data
85>         (ArchInvocationLabel X64IOPortOut8, _) -> throw TruncatedMessage
86>         (ArchInvocationLabel X64IOPortOut16, port':out:_)-> do
87>             let port = (fromIntegral port') :: IOPort
88>             ensurePortOperationAllowed cap (fromIntegral port) 2
89>             let output_data = fromIntegral out
90>             return $ InvokeIOPort $ IOPortInvocation port $ IOPortOut16 output_data
91>         (ArchInvocationLabel X64IOPortOut16, _) -> throw TruncatedMessage
92>         (ArchInvocationLabel X64IOPortOut32, port':out:_) -> do
93>             let port = (fromIntegral port') :: IOPort
94>             ensurePortOperationAllowed cap (fromIntegral port) 4
95>             let output_data = fromIntegral out
96>             return $ InvokeIOPort $ IOPortInvocation port $ IOPortOut32 output_data
97>         (ArchInvocationLabel X64IOPortOut32, _) -> throw TruncatedMessage
98>         (_, _) -> throw IllegalOperation
99
100> decodeX64PortInvocation label args slot IOPortControlCap extraCaps = do
101>     case (invocationType label, args, extraCaps) of
102>         (ArchInvocationLabel X64IOPortControlIssue, f:l:index:depth:_, cnode:_) -> do
103>             let firstPort = (fromIntegral f) :: IOPort
104>             let lastPort = (fromIntegral l) :: IOPort
105>
106>             when (firstPort > lastPort) $ throw $ InvalidArgument 1
107>             check <- withoutFailure $ isIOPortRangeFree firstPort lastPort
108>             unless check $ throw RevokeFirst
109>
110>             destSlot <- lookupTargetSlot cnode (CPtr index) (fromIntegral depth)
111>             ensureEmptySlot destSlot
112>             return $ InvokeIOPortControl $ IOPortControlIssue firstPort lastPort destSlot slot
113>         (ArchInvocationLabel X64IOPortControlIssue, _, _) -> throw TruncatedMessage
114>         _ -> throw IllegalOperation
115
116> decodeX64PortInvocation _ _ _ _ _ = fail "Unreachable"
117
118> portIn f = do
119>       res <- doMachineOp $ f
120>       return [res]
121
122> portOut f w = do
123>        doMachineOp $ f w
124>        return []
125
126>
127> performX64PortInvocation :: ArchInv.Invocation -> KernelP [Word]
128> performX64PortInvocation (InvokeIOPort (IOPortInvocation port port_data)) = withoutPreemption $
129>     case port_data of
130>         ArchInv.IOPortIn8 -> portIn $ in8 port
131>         ArchInv.IOPortIn16 -> portIn $ in16 port
132>         ArchInv.IOPortIn32 -> portIn $ in32 port
133>         ArchInv.IOPortOut8 w -> portOut (out8 port) w
134>         ArchInv.IOPortOut16 w -> portOut (out16 port) w
135>         ArchInv.IOPortOut32 w -> portOut (out32 port) w
136
137> performX64PortInvocation (InvokeIOPortControl (IOPortControlIssue f l destSlot srcSlot)) =
138>   withoutPreemption $ do
139>     setIOPortMask f l True
140>     cteInsert (ArchObjectCap (IOPortCap f l)) srcSlot destSlot
141>     return []
142
143> performX64PortInvocation _ = fail "Unreachable"
144
145