0 | ||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
  1 | |||
  2 | ||| Original (C) SimonJF, MIT Licensed, 2014
  3 | ||| Modified (C) The Idris Community, 2015, 2016, 2019
  4 | module Network.Socket
  5 |
  6 | import public Network.Socket.Data
  7 | import Network.Socket.Raw
  8 | import Network.FFI
  9 | import Data.Buffer
 10 | import Data.List
 11 | import Data.SnocList
 12 |
 13 | -- ----------------------------------------------------- [ Network Socket API. ]
 14 |
 15 | ||| Creates a UNIX socket with the given family, socket type and protocol
 16 | ||| number. Returns either a socket or an error.
 17 | export
 18 | socket : HasIO io
 19 |       => (fam  : SocketFamily)
 20 |       -> (ty   : SocketType)
 21 |       -> (pnum : ProtocolNumber)
 22 |       -> io (Either SocketError Socket)
 23 | socket sf st pn = do
 24 |   socket_res <- primIO $ prim__idrnet_socket (toCode sf) (toCode st) pn
 25 |
 26 |   if socket_res == -1
 27 |     then map Left getErrno
 28 |     else pure $ Right (MkSocket socket_res sf st pn)
 29 |
 30 | ||| Close a socket
 31 | export
 32 | close : HasIO io => Socket -> io ()
 33 | close sock = do _ <- primIO $ prim__idrnet_close $ descriptor sock
 34 |                 pure ()
 35 |
 36 | ||| Binds a socket to the given socket address and port.
 37 | ||| Returns 0 on success, an error code otherwise.
 38 | export
 39 | bind : HasIO io
 40 |     => (sock : Socket)
 41 |     -> (addr : Maybe SocketAddress)
 42 |     -> (port : Port)
 43 |     -> io Int
 44 | bind sock addr port = do
 45 |     bind_res <- primIO $ prim__idrnet_bind
 46 |                   (descriptor sock)
 47 |                   (toCode $ family sock)
 48 |                   (toCode $ socketType sock)
 49 |                   (saString addr)
 50 |                   port
 51 |
 52 |     if bind_res == (-1)
 53 |       then getErrno
 54 |       else pure 0
 55 |   where
 56 |     saString : Maybe SocketAddress -> String
 57 |     saString (Just sa) = show sa
 58 |     saString Nothing   = ""
 59 |
 60 | ||| Connects to a given address and port.
 61 | ||| Returns 0 on success, and an error number on error.
 62 | export
 63 | connect : HasIO io
 64 |        => (sock : Socket)
 65 |        -> (addr : SocketAddress)
 66 |        -> (port : Port)
 67 |        -> io ResultCode
 68 | connect sock addr port = do
 69 |   conn_res <- primIO $ prim__idrnet_connect
 70 |               (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port
 71 |
 72 |   if conn_res == (-1)
 73 |     then getErrno
 74 |     else pure 0
 75 |
 76 | ||| Listens on a bound socket.
 77 | |||
 78 | ||| @sock The socket to listen on.
 79 | export
 80 | listen : HasIO io => (sock : Socket) -> io Int
 81 | listen sock = do
 82 |   listen_res <- primIO $ prim__idrnet_listen (descriptor sock) BACKLOG
 83 |   if listen_res == (-1)
 84 |     then getErrno
 85 |     else pure 0
 86 |
 87 | ||| Accept a connection on the provided socket.
 88 | |||
 89 | ||| Returns on failure a `SocketError`
 90 | ||| Returns on success a pairing of:
 91 | ||| + `Socket`        :: The socket representing the connection.
 92 | ||| + `SocketAddress` :: The
 93 | |||
 94 | ||| @sock The socket used to establish connection.
 95 | export
 96 | accept : HasIO io
 97 |       => (sock : Socket)
 98 |       -> io (Either SocketError (Socket, SocketAddress))
 99 | accept sock = do
100 |
101 |   -- We need a pointer to a sockaddr structure. This is then passed into
102 |   -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
103 |
104 |   sockaddr_ptr <- primIO prim__idrnet_create_sockaddr
105 |
106 |   accept_res <- primIO $ prim__idrnet_accept (descriptor sock) sockaddr_ptr
107 |   if accept_res == (-1)
108 |     then map Left getErrno
109 |     else do
110 |       let (MkSocket _ fam ty p_num) = sock
111 |       sockaddr <- getSockAddr (SAPtr sockaddr_ptr)
112 |       sockaddr_free (SAPtr sockaddr_ptr)
113 |       pure $ Right ((MkSocket accept_res fam ty p_num), sockaddr)
114 |
115 | ||| Send data on the specified socket.
116 | |||
117 | ||| Returns on failure a `SocketError`.
118 | ||| Returns on success the `ResultCode`.
119 | |||
120 | ||| @sock The socket on which to send the message.
121 | ||| @msg  The data to send.
122 | export
123 | send : HasIO io
124 |     => (sock : Socket)
125 |     -> (msg  : String)
126 |     -> io (Either SocketError ResultCode)
127 | send sock dat = do
128 |   send_res <- primIO $ prim__idrnet_send (descriptor sock) dat
129 |
130 |   if send_res == (-1)
131 |     then map Left getErrno
132 |     else pure $ Right send_res
133 |
134 | ||| Receive data on the specified socket.
135 | |||
136 | ||| Returns on failure a `SocketError`
137 | ||| Returns on success a pairing of:
138 | ||| + `String`     :: The payload.
139 | ||| + `ResultCode` :: The result of the underlying function.
140 | |||
141 | ||| @sock The socket on which to receive the message.
142 | ||| @len  How much of the data to receive.
143 | export
144 | recv : HasIO io
145 |     => (sock : Socket)
146 |     -> (len : ByteLength)
147 |     -> io (Either SocketError (String, ResultCode))
148 | recv sock len = do
149 |   -- Firstly make the request, get some kind of recv structure which
150 |   -- contains the result of the recv and possibly the retrieved payload
151 |   recv_struct_ptr <- primIO $ prim__idrnet_recv (descriptor sock) len
152 |   recv_res <- primIO $ prim__idrnet_get_recv_res recv_struct_ptr
153 |
154 |   if recv_res == (-1)
155 |     then do
156 |       errno <- getErrno
157 |       freeRecvStruct (RSPtr recv_struct_ptr)
158 |       pure $ Left errno
159 |     else
160 |       if recv_res == 0
161 |         then do
162 |            freeRecvStruct (RSPtr recv_struct_ptr)
163 |            pure $ Left 0
164 |         else do
165 |            payload <- primIO $ prim__idrnet_get_recv_payload recv_struct_ptr
166 |            freeRecvStruct (RSPtr recv_struct_ptr)
167 |            pure $ Right (payload, recv_res)
168 |
169 | recvAllRec : (Monoid a, HasIO io) => io (Either SocketError a) -> SnocList a -> io (Either SocketError a)
170 | recvAllRec recv_from_socket acc = case !recv_from_socket of
171 |   Left 0 => pure (Right $ concat acc)
172 |   Left c => pure (Left c)
173 |   Right str => recvAllRec recv_from_socket (acc :< str)
174 |
175 | ||| Receive all the remaining data on the specified socket.
176 | |||
177 | ||| Returns on failure a `SocketError`
178 | ||| Returns on success the payload `String`
179 | |||
180 | ||| @sock The socket on which to receive the message.
181 | export
182 | recvAll : HasIO io => (sock : Socket) -> io (Either SocketError String)
183 | recvAll sock = recvAllRec {a=String} (mapSnd fst <$> recv sock 65536) [<]
184 |
185 | ||| Send a message.
186 | |||
187 | ||| Returns on failure a `SocketError`
188 | ||| Returns on success the `ResultCode`
189 | |||
190 | ||| @sock The socket on which to send the message.
191 | ||| @addr Address of the recipient.
192 | ||| @port The port on which to send the message.
193 | ||| @msg  The message to send.
194 | export
195 | sendTo : HasIO io
196 |       => (sock : Socket)
197 |       -> (addr : SocketAddress)
198 |       -> (port : Port)
199 |       -> (msg  : String)
200 |       -> io (Either SocketError ByteLength)
201 | sendTo sock addr p dat = do
202 |   sendto_res <- primIO $ prim__idrnet_sendto
203 |                 (descriptor sock) dat (show addr) p (toCode $ family sock)
204 |
205 |   if sendto_res == (-1)
206 |     then map Left getErrno
207 |     else pure $ Right sendto_res
208 |
209 | ||| Receive a message.
210 | |||
211 | ||| Returns on failure a `SocketError`.
212 | ||| Returns on success a triple of
213 | ||| + `UDPAddrInfo` :: The address of the sender.
214 | ||| + `String`      :: The payload.
215 | ||| + `Int`         :: Result value from underlying function.
216 | |||
217 | ||| @sock The channel on which to receive.
218 | ||| @len  Size of the expected message.
219 | |||
220 | export
221 | recvFrom : HasIO io
222 |         => (sock : Socket)
223 |         -> (len  : ByteLength)
224 |         -> io (Either SocketError (UDPAddrInfo, String, ResultCode))
225 | recvFrom sock bl = do
226 |   recv_ptr <- primIO $ prim__idrnet_recvfrom
227 |                        (descriptor sock) bl
228 |
229 |   let recv_ptr' = RFPtr recv_ptr
230 |   isNull <- (nullPtr recv_ptr)
231 |   if isNull
232 |     then map Left getErrno
233 |     else do
234 |       result <- primIO $ prim__idrnet_get_recvfrom_res recv_ptr
235 |       if result == -1
236 |         then do
237 |           freeRecvfromStruct recv_ptr'
238 |           map Left getErrno
239 |         else do
240 |           payload <- foreignGetRecvfromPayload recv_ptr'
241 |           port <- foreignGetRecvfromPort recv_ptr'
242 |           addr <- foreignGetRecvfromAddr recv_ptr'
243 |           freeRecvfromStruct recv_ptr'
244 |           pure $ Right (MkUDPAddrInfo addr port, payload, result)
245 |
246 | ||| Send data on the specified socket.
247 | |||
248 | ||| Returns on failure a `SocketError`.
249 | ||| Returns on success the number of bytes sent.
250 | |||
251 | ||| @sock   The socket on which to send the message.
252 | ||| @bytes  The data to send.
253 | export
254 | sendBytes : HasIO m => Socket -> List Bits8 -> m (Either SocketError Int)
255 | sendBytes sock bytes = do
256 |   let len' = cast $ length bytes
257 |   Just buffer <- newBuffer len'
258 |   | Nothing => assert_total $ idris_crash "INTERNAL ERROR: sendBytes -> somehow newBuffer failed"
259 |   traverse_ (uncurry (setBits8 buffer)) (zip [0..len'] bytes)
260 |   ret <- primIO $ prim__idrnet_send_bytes sock.descriptor buffer len' 0
261 |   case ret < 0 of
262 |     True => pure $ Left ret
263 |     False => pure $ Right ret
264 |
265 | ||| Receive data on the specified socket.
266 | |||
267 | ||| Returns on failure a `SocketError`
268 | ||| Returns on success a pairing of:
269 | ||| + `List Bits8` :: The payload.
270 | ||| + `ResultCode` :: The result of the underlying function.
271 | |||
272 | ||| @sock     The socket on which to receive the message.
273 | ||| @max_size How much of the data to receive at most.
274 | export
275 | recvBytes : HasIO m => Socket -> (max_size : ByteLength) -> m (Either SocketError (List Bits8))
276 | recvBytes sock max_size = do
277 |   Just buffer <- newBuffer max_size
278 |   | Nothing => pure $ Left (-1)
279 |   ret <- primIO $ prim__idrnet_recv_bytes sock.descriptor buffer max_size 0
280 |   case ret > 0 of
281 |     False => do
282 |       pure $ Left ret
283 |     True => do
284 |       bytes <- traverse (getBits8 buffer) [0..((cast ret)-1)]
285 |       pure $ Right $ toList bytes
286 |
287 |
288 | ||| Receive all the remaining data on the specified socket.
289 | |||
290 | ||| Returns on failure a `SocketError`
291 | ||| Returns on success the payload `List Bits8`
292 | |||
293 | ||| @sock The socket on which to receive the message.
294 | export
295 | recvAllBytes : HasIO io => (sock : Socket) -> io (Either SocketError (List Bits8))
296 | recvAllBytes sock = recvAllRec {a=List Bits8} (recvBytes sock 65536) [<]
297 |