on 78c76fe help sign in
370 lines 12 kB history raw
1-- Time to do this properly.
2-- Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
3-- (C) SimonJF, MIT Licensed, 2014
4module IdrisNet.Socket
6%include C "idris_net.h"
7%include C "sys/types.h"
8%include C "sys/socket.h"
9%include C "netdb.h"
11%access public
13ByteLength : Type
14ByteLength = Int
16class ToCode a where
17 toCode : a -> Int
19||| Socket Families
20|||
21||| The ones that people might actually use. We're not going to need US
22||| Government proprietary ones.
23data SocketFamily =
24 ||| Unspecified
25 AF_UNSPEC |
26 ||| IP / UDP etc. IPv4
27 AF_INET |
28 ||| IP / UDP etc. IPv6
29 AF_INET6
31instance Show SocketFamily where
32 show AF_UNSPEC = "AF_UNSPEC"
33 show AF_INET = "AF_INET"
34 show AF_INET6 = "AF_INET6"
36instance ToCode SocketFamily where
37 toCode AF_UNSPEC = 0
38 toCode AF_INET = 2
39 toCode AF_INET6 = 10
41getSocketFamily : Int -> Maybe SocketFamily
42getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
44||| Socket Types.
45data SocketType =
46 ||| Not a socket, used in certain operations
47 NotASocket |
48 ||| TCP
49 Stream |
50 ||| UDP
51 Datagram |
52 ||| Raw sockets
53 RawSocket
55instance Show SocketType where
56 show NotASocket = "Not a socket"
57 show Stream = "Stream"
58 show Datagram = "Datagram"
59 show RawSocket = "Raw"
61instance ToCode SocketType where
62 toCode NotASocket = 0
63 toCode Stream = 1
64 toCode Datagram = 2
65 toCode RawSocket = 3
68data RecvStructPtr = RSPtr Ptr
69data RecvfromStructPtr = RFPtr Ptr
70data BufPtr = BPtr Ptr
71data SockaddrPtr = SAPtr Ptr
73||| Protocol Number.
74|||
75||| Generally good enough to just set it to 0.
76ProtocolNumber : Type
77ProtocolNumber = Int
79||| SocketError: Error thrown by a socket operation
80SocketError : Type
81SocketError = Int
83||| SocketDescriptor: Native C Socket Descriptor
84SocketDescriptor : Type
85SocketDescriptor = Int
87data SocketAddress = IPv4Addr Int Int Int Int
88 | IPv6Addr -- Not implemented (yet)
89 | Hostname String
90 | InvalidAddress -- Used when there's a parse error
92instance Show SocketAddress where
93 show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
94 show IPv6Addr = "NOT IMPLEMENTED YET"
95 show (Hostname host) = host
96 show InvalidAddress = "Invalid"
98Port : Type
99Port = Int
101||| Backlog used within listen() call -- number of incoming calls
102BACKLOG : Int
103BACKLOG = 20
105-- FIXME: This *must* be pulled in from C
106EAGAIN : Int
107EAGAIN = 11
109-- TODO: Expand to non-string payloads
110record UDPRecvData : Type where
111 MkUDPRecvData :
112 (remote_addr : SocketAddress) ->
113 (remote_port : Port) ->
114 (recv_data : String) ->
115 (data_len : Int) ->
116 UDPRecvData
118record UDPAddrInfo : Type where
119 MkUDPAddrInfo :
120 (remote_addr : SocketAddress) ->
121 (remote_port : Port) ->
122 UDPAddrInfo
124||| Frees a given pointer
125public
126sock_free : BufPtr -> IO ()
127sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
129public
130sockaddr_free : SockaddrPtr -> IO ()
131sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
133||| Allocates an amount of memory given by the ByteLength parameter.
134|||
135||| Used to allocate a mutable pointer to be given to the Recv functions.
136public
137sock_alloc : ByteLength -> IO BufPtr
138sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
140||| The metadata about a socket
141record Socket : Type where
142 MkSocket : (descriptor : SocketDescriptor) ->
143 (family : SocketFamily) ->
144 (socketType : SocketType) ->
145 (protocolNumber : ProtocolNumber) ->
146 Socket
148||| Get the C error number
149getErrno : IO Int
150getErrno = foreign FFI_C "idrnet_errno" (IO Int)
152||| Creates a UNIX socket with the given family, socket type and protocol
153||| number. Returns either a socket or an error.
154socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
155socket sf st pn = do
156 socket_res <- foreign FFI_C "socket" (Int -> Int -> Int -> IO Int) (toCode sf) (toCode st) pn
157 if socket_res == -1 then -- error
158 map Left getErrno
159 else
160 return $ Right (MkSocket socket_res sf st pn)
162||| Close a socket
163close : Socket -> IO ()
164close sock = foreign FFI_C "close" (Int -> IO ()) (descriptor sock)
166private
167saString : (Maybe SocketAddress) -> String
168saString (Just sa) = show sa
169saString Nothing = ""
171||| Binds a socket to the given socket address and port.
172||| Returns 0 on success, an error code otherwise.
173bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
174bind sock addr port = do
175 bind_res <- foreign FFI_C "idrnet_bind"
176 (Int -> Int -> Int -> String -> Int -> IO Int)
177 (descriptor sock) (toCode $ family sock)
178 (toCode $ socketType sock) (saString addr) port
179 if bind_res == (-1) then -- error
180 getErrno
181 else return 0 -- Success
183||| Connects to a given address and port.
184||| Returns 0 on success, and an error number on error.
185connect : Socket -> SocketAddress -> Port -> IO Int
186connect sock addr port = do
187 conn_res <- foreign FFI_C "idrnet_connect"
188 (Int -> Int -> Int -> String -> Int -> IO Int)
189 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port
190 if conn_res == (-1) then
191 getErrno
192 else return 0
194||| Listens on a bound socket.
195listen : Socket -> IO Int
196listen sock = do
197 listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int)
198 (descriptor sock) BACKLOG
199 if listen_res == (-1) then
200 getErrno
201 else return 0
203||| Parses a textual representation of an IPv4 address into a SocketAddress
204parseIPv4 : String -> SocketAddress
205parseIPv4 str = case splitted of
206 (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
207 _ => InvalidAddress
208 where toInt' : String -> Integer
209 toInt' = cast
210 toInt : String -> Int
211 toInt s = fromInteger $ toInt' s
212 splitted : List Int
213 splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
216||| Retrieves a socket address from a sockaddr pointer
217getSockAddr : SockaddrPtr -> IO SocketAddress
218getSockAddr (SAPtr ptr) = do
219 addr_family_int <- foreign FFI_C "idrnet_sockaddr_family" (Ptr -> IO Int) ptr
220 -- putStrLn $ "Addr family int: " ++ (show addr_family_int)
221 -- ASSUMPTION: Foreign call returns a valid int
222 assert_total (case getSocketFamily addr_family_int of
223 Just AF_INET => do
224 ipv4_addr <- foreign FFI_C "idrnet_sockaddr_ipv4" (Ptr -> IO String) ptr
225 return $ parseIPv4 ipv4_addr
226 Just AF_INET6 => return IPv6Addr
227 Just AF_UNSPEC => return InvalidAddress)
229accept : Socket -> IO (Either SocketError (Socket, SocketAddress))
230accept sock = do
231 -- We need a pointer to a sockaddr structure. This is then passed into
232 -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
233 sockaddr_ptr <- foreign FFI_C "idrnet_create_sockaddr" (IO Ptr)
234 accept_res <- foreign FFI_C "idrnet_accept" (Int -> Ptr -> IO Int) (descriptor sock) sockaddr_ptr
235 if accept_res == (-1) then
236 map Left getErrno
237 else do
238 let (MkSocket _ fam ty p_num) = sock
239 sockaddr <- getSockAddr (SAPtr sockaddr_ptr)
240 sockaddr_free (SAPtr sockaddr_ptr)
241 return $ Right ((MkSocket accept_res fam ty p_num), sockaddr)
243send : Socket -> String -> IO (Either SocketError ByteLength)
244send sock dat = do
245 send_res <- foreign FFI_C "idrnet_send" (Int -> String -> IO Int) (descriptor sock) dat
246 if send_res == (-1) then
247 map Left getErrno
248 else
249 return $ Right send_res
252freeRecvStruct : RecvStructPtr -> IO ()
253freeRecvStruct (RSPtr p) = foreign FFI_C "idrnet_free_recv_struct" (Ptr -> IO ()) p
255freeRecvfromStruct : RecvfromStructPtr -> IO ()
256freeRecvfromStruct (RFPtr p) = foreign FFI_C "idrnet_free_recvfrom_struct" (Ptr -> IO ()) p
258recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))
259recv sock len = do
260 -- Firstly make the request, get some kind of recv structure which
261 -- contains the result of the recv and possibly the retrieved payload
262 recv_struct_ptr <- foreign FFI_C "idrnet_recv" (Int -> Int -> IO Ptr) (descriptor sock) len
263 recv_res <- foreign FFI_C "idrnet_get_recv_res" (Ptr -> IO Int) recv_struct_ptr
264 if recv_res == (-1) then do
265 errno <- getErrno
266 freeRecvStruct (RSPtr recv_struct_ptr)
267 return $ Left errno
268 else
269 if recv_res == 0 then do
270 freeRecvStruct (RSPtr recv_struct_ptr)
271 return $ Left 0
272 else do
273 payload <- foreign FFI_C "idrnet_get_recv_payload" (Ptr -> IO String) recv_struct_ptr
274 freeRecvStruct (RSPtr recv_struct_ptr)
275 return $ Right (payload, recv_res)
278||| Sends the data in a given memory location
279sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
280sendBuf sock (BPtr ptr) len = do
281 send_res <- foreign FFI_C "idrnet_send_buf" (Int -> Ptr -> Int -> IO Int) (descriptor sock) ptr len
282 if send_res == (-1) then
283 map Left getErrno
284 else
285 return $ Right send_res
287recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
288recvBuf sock (BPtr ptr) len = do
289 recv_res <- foreign FFI_C "idrnet_recv_buf" (Int -> Ptr -> Int -> IO Int) (descriptor sock) ptr len
290 if (recv_res == (-1)) then
291 map Left getErrno
292 else
293 return $ Right recv_res
295sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength)
296sendTo sock addr p dat = do
297 sendto_res <- foreign FFI_C "idrnet_sendto"
298 (Int -> String -> String -> Int -> Int -> IO Int)
299 (descriptor sock) dat (show addr) p (toCode $ family sock)
300 if sendto_res == (-1) then
301 map Left getErrno
302 else
303 return $ Right sendto_res
306sendToBuf : Socket -> SocketAddress -> Port -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
307sendToBuf sock addr p (BPtr dat) len = do
308 sendto_res <- foreign FFI_C "idrnet_sendto_buf"
309 (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)
310 (descriptor sock) dat len (show addr) p (toCode $ family sock)
311 if sendto_res == (-1) then
312 map Left getErrno
313 else
314 return $ Right sendto_res
317foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
318foreignGetRecvfromPayload (RFPtr p)
319 = foreign FFI_C "idrnet_get_recvfrom_payload" (Ptr -> IO String) p
321foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
322foreignGetRecvfromAddr (RFPtr p) = do
323 sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr" (Ptr -> IO Ptr) p
324 getSockAddr sockaddr_ptr
327foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
328foreignGetRecvfromPort (RFPtr p) = do
329 sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr" (Ptr -> IO Ptr) p
330 port <- foreign FFI_C "idrnet_sockaddr_ipv4_port" (Ptr -> IO Int) sockaddr_ptr
331 return port
333recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength))
334recvFrom sock bl = do
335 recv_ptr <- foreign FFI_C "idrnet_recvfrom" (Int -> Int -> IO Ptr)
336 (descriptor sock) bl
337 let recv_ptr' = RFPtr recv_ptr
338 if !(nullPtr recv_ptr) then
339 map Left getErrno
340 else do
341 result <- foreign FFI_C "idrnet_get_recvfrom_res" (Ptr -> IO Int) recv_ptr
342 if result == -1 then do
343 freeRecvfromStruct recv_ptr'
344 map Left getErrno
345 else do
346 payload <- foreignGetRecvfromPayload recv_ptr'
347 port <- foreignGetRecvfromPort recv_ptr'
348 addr <- foreignGetRecvfromAddr recv_ptr'
349 freeRecvfromStruct recv_ptr'
350 return $ Right (MkUDPAddrInfo addr port, payload, result)
353recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrInfo, ByteLength))
354recvFromBuf sock (BPtr ptr) bl = do
355 recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf" (Int -> Ptr -> Int -> IO Ptr) (descriptor sock) ptr bl
356 let recv_ptr' = RFPtr recv_ptr
357 if !(nullPtr recv_ptr) then
358 map Left getErrno
359 else do
360 result <- foreign FFI_C "idrnet_get_recvfrom_res" (Ptr -> IO Int) recv_ptr
361 if result == -1 then do
362 freeRecvfromStruct recv_ptr'
363 map Left getErrno
364 else do
365 port <- foreignGetRecvfromPort recv_ptr'
366 addr <- foreignGetRecvfromAddr recv_ptr'
367 freeRecvfromStruct recv_ptr'
368 return $ Right (MkUDPAddrInfo addr port, result + 1)