@@ -4,210 +4,20 @@
44||| Modified (C) The Idris Community, 2015, 2016
55module Network.Socket
66
7+import public Network.Socket.Data
8+import Network.Socket.Raw
9+
710%include C "idris_net.h"
811%include C "sys/types.h"
912%include C "sys/socket.h"
1013%include C "netdb.h"
1114
12−-- ------------------------------------------------------------ [ Type Aliases ]
13−
14−public export
15−ByteLength : Type
16−ByteLength = Int
17−
18−public export
19−ResultCode : Type
20−ResultCode = Int
21−
22−||| Protocol Number.
23−|||
24−||| Generally good enough to just set it to 0.
25−public export
26−ProtocolNumber : Type
27−ProtocolNumber = Int
28−
29−||| SocketError: Error thrown by a socket operation
30−public export
31−SocketError : Type
32−SocketError = Int
33−
34−||| SocketDescriptor: Native C Socket Descriptor
35−public export
36−SocketDescriptor : Type
37−SocketDescriptor = Int
38−
39−public export
40−Port : Type
41−Port = Int
42−
43−-- --------------------------------------------------------------- [ Constants ]
44−
45−||| Backlog used within listen() call -- number of incoming calls
46−public export
47−BACKLOG : Int
48−BACKLOG = 20
49−
50−-- FIXME: This *must* be pulled in from C
51−public export
52−EAGAIN : Int
53−EAGAIN = 11
54−
55−-- -------------------------------------------------------------- [ Interfaces ]
56−
57−export
58−interface ToCode a where
59− toCode : a -> Int
60−
61−-- --------------------------------------------------------- [ Socket Families ]
62−
63−||| Socket Families
64−|||
65−||| The ones that people might actually use. We're not going to need US
66−||| Government proprietary ones.
67−public export
68−data SocketFamily : Type where
69− ||| Unspecified
70− AF_UNSPEC : SocketFamily
71−
72− ||| IP / UDP etc. IPv4
73− AF_INET : SocketFamily
74−
75− ||| IP / UDP etc. IPv6
76− AF_INET6 : SocketFamily
77−
78−export
79−Show SocketFamily where
80− show AF_UNSPEC = "AF_UNSPEC"
81− show AF_INET = "AF_INET"
82− show AF_INET6 = "AF_INET6"
83−
84−export
85−ToCode SocketFamily where
86− toCode AF_UNSPEC = 0
87− toCode AF_INET = 2
88− toCode AF_INET6 = 10
89−
90−getSocketFamily : Int -> Maybe SocketFamily
91−getSocketFamily i =
92− Prelude.List.lookup i [ (0, AF_UNSPEC)
93− , (2, AF_INET)
94− , (10, AF_INET6)
95− ]
96−
97−-- ------------------------------------------------------------ [ Socket Types ]
98−||| Socket Types.
99−public export
100−data SocketType : Type where
101− ||| Not a socket, used in certain operations
102− NotASocket : SocketType
103−
104− ||| TCP
105− Stream : SocketType
106−
107− ||| UDP
108− Datagram : SocketType
109−
110− ||| Raw sockets
111− RawSocket : SocketType
112−
113−export
114−Show SocketType where
115− show NotASocket = "Not a socket"
116− show Stream = "Stream"
117− show Datagram = "Datagram"
118− show RawSocket = "Raw"
119−
120−export
121−ToCode SocketType where
122− toCode NotASocket = 0
123− toCode Stream = 1
124− toCode Datagram = 2
125− toCode RawSocket = 3
126−
127−-- ---------------------------------------------------------------- [ Pointers ]
128−
129−data RecvStructPtr = RSPtr Ptr
130−data RecvfromStructPtr = RFPtr Ptr
131−
132−export
133−data BufPtr = BPtr Ptr
134−
135−export
136−data SockaddrPtr = SAPtr Ptr
137−
138−-- --------------------------------------------------------------- [ Addresses ]
139−
140−||| Network Addresses
141−public export
142−data SocketAddress : Type where
143− IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
144−
145− ||| Not implemented (yet)
146− IPv6Addr : SocketAddress
147−
148− Hostname : String -> SocketAddress
149−
150− ||| Used when there's a parse error
151− InvalidAddress : SocketAddress
152−
153−export
154−Show SocketAddress where
155− show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
156− show IPv6Addr = "NOT IMPLEMENTED YET"
157− show (Hostname host) = host
158− show InvalidAddress = "Invalid"
159−
160−-- --------------------------------------------------------- [ UDP Information ]
161−
162−-- TODO: Expand to non-string payloads
163−export
164−record UDPRecvData where
165− constructor MkUDPRecvData
166− remote_addr : SocketAddress
167− remote_port : Port
168− recv_data : String
169− data_len : Int
170−
171−export
172−record UDPAddrInfo where
173− constructor MkUDPAddrInfo
174− remote_addr : SocketAddress
175− remote_port : Port
176−
177−-- ---------------------------------------------------------- [ Socket Utilies ]
178−
179−||| Frees a given pointer
180−export
181−sock_free : BufPtr -> IO ()
182−sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
183−
184−export
185−sockaddr_free : SockaddrPtr -> IO ()
186−sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
187−
188−||| Allocates an amount of memory given by the ByteLength parameter.
189−|||
190−||| Used to allocate a mutable pointer to be given to the Recv functions.
191−export
192−sock_alloc : ByteLength -> IO BufPtr
193−sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
194−
195−-- ----------------------------------------------------------------- [ Sockets ]
196−||| The metadata about a socket
197−export
198−record Socket where
199− constructor MkSocket
200− descriptor : SocketDescriptor
201− family : SocketFamily
202− socketType : SocketType
203− protocolNumber : ProtocolNumber
204−
15+%access export
20516
20617-- ----------------------------------------------------- [ Network Socket API. ]
20718
20819||| Creates a UNIX socket with the given family, socket type and protocol
20920||| number. Returns either a socket or an error.
210−export
21121socket : (fam : SocketFamily)
21222 -> (ty : SocketType)
21323 -> (pnum : ProtocolNumber)
@@ -222,34 +32,30 @@ socket sf st pn = do
22232 else pure $ Right (MkSocket socket_res sf st pn)
22333
22434||| Close a socket
225−export
22635close : Socket -> IO ()
22736close sock = foreign FFI_C "close" (Int -> IO ()) (descriptor sock)
22837
229−private
230−saString : (Maybe SocketAddress) -> String
231−saString (Just sa) = show sa
232−saString Nothing = ""
233−
23438||| Binds a socket to the given socket address and port.
23539||| Returns 0 on success, an error code otherwise.
236−export
23740bind : (sock : Socket)
23841 -> (addr : Maybe SocketAddress)
23942 -> (port : Port)
24043 -> IO Int
24144bind sock addr port = do
242− bind_res <- foreign FFI_C "idrnet_bind"
243− (Int -> Int -> Int -> String -> Int -> IO Int)
244− (descriptor sock) (toCode $ family sock)
245− (toCode $ socketType sock) (saString addr) port
246− if bind_res == (-1)
247− then getErrno
248− else pure 0
45+ bind_res <- foreign FFI_C "idrnet_bind"
46+ (Int -> Int -> Int -> String -> Int -> IO Int)
47+ (descriptor sock) (toCode $ family sock)
48+ (toCode $ socketType sock) (saString addr) port
49+ if bind_res == (-1)
50+ then getErrno
51+ else pure 0
52+ where
53+ saString : Maybe SocketAddress -> String
54+ saString (Just sa) = show sa
55+ saString Nothing = ""
24956
25057||| Connects to a given address and port.
25158||| Returns 0 on success, and an error number on error.
252−export
25359connect : (sock : Socket)
25460 -> (addr : SocketAddress)
25561 -> (port : Port)
@@ -266,7 +72,6 @@ connect sock addr port = do
26672||| Listens on a bound socket.
26773|||
26874||| @sock The socket to listen on.
269−export
27075listen : (sock : Socket) -> IO Int
27176listen sock = do
27277 listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int)
@@ -275,40 +80,6 @@ listen sock = do
27580 then getErrno
27681 else pure 0
27782
278−||| Parses a textual representation of an IPv4 address into a SocketAddress
279−parseIPv4 : String -> SocketAddress
280−parseIPv4 str =
281− case splitted of
282− (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
283− otherwise => InvalidAddress
284− where
285− toInt' : String -> Integer
286− toInt' = cast
287−
288− toInt : String -> Int
289− toInt s = fromInteger $ toInt' s
290−
291− splitted : List Int
292− splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
293−
294−||| Retrieves a socket address from a sockaddr pointer
295−getSockAddr : SockaddrPtr -> IO SocketAddress
296−getSockAddr (SAPtr ptr) = do
297− addr_family_int <- foreign FFI_C "idrnet_sockaddr_family"
298− (Ptr -> IO Int)
299− ptr
300−
301− -- ASSUMPTION: Foreign call returns a valid int
302− assert_total (case getSocketFamily addr_family_int of
303− Just AF_INET => do
304− ipv4_addr <- foreign FFI_C "idrnet_sockaddr_ipv4"
305− (Ptr -> IO String)
306− ptr
307−
308− pure $ parseIPv4 ipv4_addr
309− Just AF_INET6 => pure IPv6Addr
310− Just AF_UNSPEC => pure InvalidAddress)
311−
31283||| Accept a connection on the provided socket.
31384|||
31485||| Returns on failure a `SocketError`
@@ -317,7 +88,6 @@ getSockAddr (SAPtr ptr) = do
31788||| + `SocketAddress` :: The
31889|||
31990||| @sock The socket used to establish connection.
320−export
32191accept : (sock : Socket)
32292 -> IO (Either SocketError (Socket, SocketAddress))
32393accept sock = do
@@ -346,7 +116,6 @@ accept sock = do
346116|||
347117||| @sock The socket on which to send the message.
348118||| @msg The data to send.
349−export
350119send : (sock : Socket)
351120 -> (msg : String)
352121 -> IO (Either SocketError ResultCode)
@@ -359,20 +128,6 @@ send sock dat = do
359128 then map Left getErrno
360129 else pure $ Right send_res
361130
362−freeRecvStruct : RecvStructPtr -> IO ()
363−freeRecvStruct (RSPtr p) =
364− foreign FFI_C "idrnet_free_recv_struct"
365− (Ptr -> IO ())
366− p
367−
368−||| Utility to extract data.
369−freeRecvfromStruct : RecvfromStructPtr -> IO ()
370−freeRecvfromStruct (RFPtr p) =
371− foreign FFI_C "idrnet_free_recvfrom_struct"
372− (Ptr -> IO ())
373− p
374−
375−
376131||| Receive data on the specified socket.
377132|||
378133||| Returns on failure a `SocketError`
@@ -382,7 +137,6 @@ freeRecvfromStruct (RFPtr p) =
382137|||
383138||| @sock The socket on which to receive the message.
384139||| @len How much of the data to send.
385−export
386140recv : (sock : Socket)
387141 -> (len : ByteLength)
388142 -> IO (Either SocketError (String, ResultCode))
@@ -413,48 +167,6 @@ recv sock len = do
413167 freeRecvStruct (RSPtr recv_struct_ptr)
414168 pure $ Right (payload, recv_res)
415169
416−||| Sends the data in a given memory location
417−|||
418−||| Returns on failure a `SocketError`
419−||| Returns on success the `ResultCode`
420−|||
421−||| @sock The socket on which to send the message.
422−||| @ptr The location containing the data to send.
423−||| @len How much of the data to send.
424−sendBuf : (sock : Socket)
425− -> (ptr : BufPtr)
426− -> (len : ByteLength)
427− -> IO (Either SocketError ResultCode)
428−sendBuf sock (BPtr ptr) len = do
429− send_res <- foreign FFI_C "idrnet_send_buf"
430− (Int -> Ptr -> Int -> IO Int)
431− (descriptor sock) ptr len
432−
433− if send_res == (-1)
434− then map Left getErrno
435− else pure $ Right send_res
436−
437−||| Receive data from a given memory location.
438−|||
439−||| Returns on failure a `SocketError`
440−||| Returns on success the `ResultCode`
441−|||
442−||| @sock The socket on which to receive the message.
443−||| @ptr The location containing the data to receive.
444−||| @len How much of the data to receive.
445−recvBuf : (sock : Socket)
446− -> (ptr : BufPtr)
447− -> (len : ByteLength)
448− -> IO (Either SocketError ResultCode)
449−recvBuf sock (BPtr ptr) len = do
450− recv_res <- foreign FFI_C "idrnet_recv_buf"
451− (Int -> Ptr -> Int -> IO Int)
452− (descriptor sock) ptr len
453−
454− if (recv_res == (-1))
455− then map Left getErrno
456− else pure $ Right recv_res
457−
458170||| Send a message.
459171|||
460172||| Returns on failure a `SocketError`
@@ -464,7 +176,6 @@ recvBuf sock (BPtr ptr) len = do
464176||| @addr Address of the recipient.
465177||| @port The port on which to send the message.
466178||| @msg The message to send.
467−export
468179sendTo : (sock : Socket)
469180 -> (addr : SocketAddress)
470181 -> (port : Port)
@@ -479,58 +190,6 @@ sendTo sock addr p dat = do
479190 then map Left getErrno
480191 else pure $ Right sendto_res
481192
482−||| Send a message stored in some buffer.
483−|||
484−||| Returns on failure a `SocketError`
485−||| Returns on success the `ResultCode`
486−|||
487−||| @sock The socket on which to send the message.
488−||| @addr Address of the recipient.
489−||| @port The port on which to send the message.
490−||| @ptr A Pointer to the buffer containing the message.
491−||| @len The size of the message.
492−sendToBuf : (sock : Socket)
493− -> (addr : SocketAddress)
494− -> (port : Port)
495− -> (ptr : BufPtr)
496− -> (len : ByteLength)
497− -> IO (Either SocketError ResultCode)
498−sendToBuf sock addr p (BPtr dat) len = do
499− sendto_res <- foreign FFI_C "idrnet_sendto_buf"
500− (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)
501− (descriptor sock) dat len (show addr) p (toCode $ family sock)
502−
503− if sendto_res == (-1)
504− then map Left getErrno
505− else pure $ Right sendto_res
506−
507−||| Utility function to get the payload of the sent message as a `String`.
508−foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
509−foreignGetRecvfromPayload (RFPtr p) =
510− foreign FFI_C "idrnet_get_recvfrom_payload"
511− (Ptr -> IO String)
512− p
513−
514−||| Utility function to return senders socket address.
515−foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
516−foreignGetRecvfromAddr (RFPtr p) = do
517− sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr"
518− (Ptr -> IO Ptr)
519− p
520− getSockAddr sockaddr_ptr
521−
522−||| Utility function to return sender's IPV4 port.
523−foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
524−foreignGetRecvfromPort (RFPtr p) = do
525− sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr"
526− (Ptr -> IO Ptr)
527− p
528− port <- foreign FFI_C "idrnet_sockaddr_ipv4_port"
529− (Ptr -> IO Int)
530− sockaddr_ptr
531− pure port
532−
533−
534193||| Receive a message.
535194|||
536195||| Returns on failure a `SocketError`.
@@ -542,7 +201,6 @@ foreignGetRecvfromPort (RFPtr p) = do
542201||| @sock The channel on which to receive.
543202||| @len Size of the expected message.
544203|||
545−export
546204recvFrom : (sock : Socket)
547205 -> (len : ByteLength)
548206 -> IO (Either SocketError (UDPAddrInfo, String, ResultCode))
@@ -570,42 +228,3 @@ recvFrom sock bl = do
570228 freeRecvfromStruct recv_ptr'
571229 pure $ Right (MkUDPAddrInfo addr port, payload, result)
572230
573−||| Receive a message placed on a 'known' buffer.
574−|||
575−||| Returns on failure a `SocketError`.
576−||| Returns on success a pair of
577−||| + `UDPAddrInfo` :: The address of the sender.
578−||| + `Int` :: Result value from underlying function.
579−|||
580−||| @sock The channel on which to receive.
581−||| @ptr Pointer to the buffer to place the message.
582−||| @len Size of the expected message.
583−|||
584−recvFromBuf : (sock : Socket)
585− -> (ptr : BufPtr)
586− -> (len : ByteLength)
587− -> IO (Either SocketError (UDPAddrInfo, ResultCode))
588−recvFromBuf sock (BPtr ptr) bl = do
589− recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf"
590− (Int -> Ptr -> Int -> IO Ptr)
591− (descriptor sock) ptr bl
592−
593− let recv_ptr' = RFPtr recv_ptr
594−
595− if !(nullPtr recv_ptr)
596− then map Left getErrno
597− else do
598− result <- foreign FFI_C "idrnet_get_recvfrom_res"
599− (Ptr -> IO Int)
600− recv_ptr
601− if result == -1
602− then do
603− freeRecvfromStruct recv_ptr'
604− map Left getErrno
605− else do
606− port <- foreignGetRecvfromPort recv_ptr'
607− addr <- foreignGetRecvfromAddr recv_ptr'
608− freeRecvfromStruct recv_ptr'
609− pure $ Right (MkUDPAddrInfo addr port, result + 1)
610−
611−-- --------------------------------------------------------------------- [ EOF ]