edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-03 02:03:20 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'network-lib' of https://github.com/abailly/Idris2 into abailly-network-lib

Browse Source
This commit is contained in:
Edwin Brady 2019-08-01 11:11:45 +01:00
commit 89eb495d97
14 changed files with 1344 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Makefile
View File

@ -26,7 +26,11 @@ prelude:
base: prelude
make -C libs/base IDRIS2=../../idris2
libs : prelude base
network: prelude
make -C libs/network IDRIS2=../../idris2
make -C libs/network test IDRIS2=../../idris2
libs : prelude base network
clean: clean-libs
make -C src clean
@ -37,6 +41,7 @@ clean: clean-libs
clean-libs:
make -C libs/prelude clean
make -C libs/base clean
make -C libs/network clean
test:
idris --build tests.ipkg
@ -58,3 +63,4 @@ install-exec: idris2
install-libs: libs
make -C libs/prelude install IDRIS2=../../idris2
make -C libs/base install IDRIS2=../../idris2
make -C libs/network install IDRIS2=../../idris2

47
libs/base/Data/List.idr
View File

@ -40,11 +40,28 @@ dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
public export
filter : (p : a -> Bool) -> List a -> List a
filter p [] = []
filter p (x :: xs)
filter p (x :: xs)
= if p x
then x :: filter p xs
else filter p xs
||| Find associated information in a list using a custom comparison.
public export
lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
lookupBy p e [] = Nothing
lookupBy p e (x::xs) =
let (l, r) = x in
if p e l then
Just r
else
lookupBy p e xs
||| Find associated information in a list using Boolean equality.
public export
lookup : Eq a => a -> List (a, b) -> Maybe b
lookup = lookupBy (==)
public export
span : (a -> Bool) -> List a -> (List a, List a)
span p [] = ([], [])
@ -70,7 +87,7 @@ public export
splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
splitAt Z xs = ([], xs)
splitAt (S k) [] = ([], [])
splitAt (S k) (x :: xs)
splitAt (S k) (x :: xs)
= let (tk, dr) = splitAt k xs in
(x :: tk, dr)
@ -115,6 +132,22 @@ export
toList : Foldable t => t a -> List a
toList = foldr (::) []
||| Insert some separator between the elements of a list.
|||
||| ````idris example
||| with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])
||| ````
|||
export
intersperse : a -> List a -> List a
intersperse sep [] = []
intersperse sep (x::xs) = x :: intersperse' sep xs
where
intersperse' : a -> List a -> List a
intersperse' sep [] = []
intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
--------------------------------------------------------------------------------
-- Sorting
--------------------------------------------------------------------------------
@ -181,17 +214,17 @@ Uninhabited ([] = Prelude.(::) x xs) where
export
Uninhabited (Prelude.(::) x xs = []) where
uninhabited Refl impossible
--
--
-- ||| (::) is injective
-- consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
-- (x :: xs) = (y :: ys) -> (x = y, xs = ys)
-- consInjective Refl = (Refl, Refl)
--
--
-- ||| Two lists are equal, if their heads are equal and their tails are equal.
-- consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
-- x = y -> xs = ys -> x :: xs = y :: ys
-- consCong2 Refl Refl = Refl
--
--
-- ||| Appending pairwise equal lists gives equal lists
-- appendCong2 : {x1 : List a} -> {x2 : List a} ->
-- {y1 : List b} -> {y2 : List b} ->
@ -203,13 +236,13 @@ Uninhabited (Prelude.(::) x xs = []) where
-- consCong2
-- (fst $ consInjective eq1)
-- (appendCong2 (snd $ consInjective eq1) eq2)
--
--
-- ||| List.map is distributive over appending.
-- mapAppendDistributive : (f : a -> b) -> (x : List a) -> (y : List a) ->
-- map f (x ++ y) = map f x ++ map f y
-- mapAppendDistributive _ [] _ = Refl
-- mapAppendDistributive f (_ :: xs) y = cong $ mapAppendDistributive f xs y
--
--
||| The empty list is a right identity for append.
export
appendNilRightNeutral : (l : List a) ->

11
libs/base/Data/Strings.idr
View File

@ -72,6 +72,17 @@ public export
break : (Char -> Bool) -> String -> (String, String)
break p = span (not . p)
||| Splits the string into parts with the predicate
||| indicating separator characters.
|||
||| ```idris example
||| split (== '.') ".AB.C..D"
||| ```
public export
split : (Char -> Bool) -> String -> List String
split p xs = map pack (split p (unpack xs))
export
stringToNatOrZ : String -> Nat
stringToNatOrZ = fromInteger . prim__cast_StringInteger

57
libs/network/Echo.idr Normal file
View File

@ -0,0 +1,57 @@
module Main
import System
import Network.Socket
import Network.Socket.Data
import Network.Socket.Raw
%cg chez libidris_net.so
runServer : IO (Either String (Port, ThreadID))
runServer = do
Right sock <- socket AF_INET Stream 0
| Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
res <- bind sock (Just (Hostname "localhost")) 0
if res /= 0
then pure (Left $ "Failed to bind socket with error: " ++ show res)
else do
port <- getSockPort sock
res <- listen sock
if res /= 0
then pure (Left $ "Failed to listen on socket with error: " ++ show res)
else do
forked <- fork (serve port sock)
pure $ Right (port, forked)
where
serve : Port -> Socket -> IO ()
serve port sock = do
Right (s, _) <- accept sock
| Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
Right (str, _) <- recv s 1024
| Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
putStrLn ("Received: " ++ str)
Right n <- send s ("echo: " ++ str)
| Left err => putStrLn ("Server failed to send data with error: " ++ show err)
putStrLn ("Server sent " ++ show n ++ " bytes")
runClient : Port -> IO ()
runClient serverPort = do
Right sock <- socket AF_INET Stream 0
| Left fail => putStrLn ("Failed to open socket: " ++ show fail)
res <- connect sock (Hostname "localhost") serverPort
if res /= 0
then putStrLn ("Failed to connect client to port " ++ show serverPort ++ ": " ++ show res)
else do
Right n <- send sock ("hello world!")
| Left err => putStrLn ("Client failed to send data with error: " ++ show err)
putStrLn ("Client sent " ++ show n ++ " bytes")
Right (str, _) <- recv sock 1024
| Left err => putStrLn ("Client failed to receive on socket with error: " ++ show err)
putStrLn ("Received: " ++ str)
main : IO ()
main = do
Right (serverPort, tid) <- runServer
| Left err => putStrLn $ "[server] " ++ err
runClient serverPort

61
libs/network/Makefile Normal file
View File

@ -0,0 +1,61 @@
RANLIB ?=ranlib
AR ?=ar
MACHINE := $(shell $(CC) -dumpmachine)
ifneq (, $(findstring darwin, $(MACHINE)))
OS :=darwin
else ifneq (, $(findstring cygwin, $(MACHINE)))
OS :=windows
else ifneq (, $(findstring mingw, $(MACHINE)))
OS :=windows
else ifneq (, $(findstring windows, $(MACHINE)))
OS :=windows
else
OS :=unix
endif
SHLIB_SUFFIX :=.so
LIBNAME=idris_net
OBJS = $(LIBNAME).o
HDRS = $(LIBNAME).h
CFLAGS := $(CFLAGS)
IDRIS_SRCS = Network/Socket.idr Network/Socket/Data.idr Network/Socket/Raw.idr
ifneq ($(OS), windows)
CFLAGS += -fPIC
endif
DYLIBTARGET = $(LIBNAME)$(SHLIB_SUFFIX)
LIBTARGET = $(LIBNAME).a
TARGET=${HOME}/.idris2
build: $(DYLIBTARGET) $(IDRIS_SRCS)
@if ! [ -d build ]; then echo "creating 'build' directory"; mkdir build ; else echo "directory 'build' exists"; fi
@if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi
${IDRIS2} --build network.ipkg
$(DYLIBTARGET) : $(OBJS)
$(CC) -o $(DYLIBTARGET) $(LIBFLAGS) -shared $(OBJS)
install:
@if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi
${IDRIS2} --install network.ipkg
@if ! [ -d $(TARGET)/idris2/network/lib ]; then mkdir $(TARGET)/idris2/network/lib; fi
install $(DYLIBTARGET) $(HDRS) $(TARGET)/idris2/network/lib
clean :
rm -rf $(OBJS) $(LIBTARGET) $(DYLIBTARGET) build
test: build test.c
cp $(DYLIBTARGET) lib$(DYLIBTARGET) # to make C linker happy
$(CC) -o network-tests -L. -I. test.c -l$(LIBNAME)
LD_LIBRARY_PATH=. ./network-tests
./lib-tests
$(OBJS): $(HDRS)
all: $(DYLIBTARGET) $(LIBTARGET)
${IDRIS2} --build network.ipkg
.PHONY: install clean

223
libs/network/Network/Socket.idr Normal file
View File

@ -0,0 +1,223 @@
||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
|||
||| Original (C) SimonJF, MIT Licensed, 2014
||| Modified (C) The Idris Community, 2015, 2016, 2019
module Network.Socket
import public Network.Socket.Data
import Network.Socket.Raw
import Data.List
-- ----------------------------------------------------- [ Network Socket API. ]
||| Creates a UNIX socket with the given family, socket type and protocol
||| number. Returns either a socket or an error.
socket : (fam : SocketFamily)
-> (ty : SocketType)
-> (pnum : ProtocolNumber)
-> IO (Either SocketError Socket)
socket sf st pn = do
socket_res <- cCall Int "idrnet_socket" [toCode sf, toCode st, pn]
if socket_res == -1
then map Left getErrno
else pure $ Right (MkSocket socket_res sf st pn)
||| Close a socket
close : Socket -> IO ()
close sock = cCall () "close" [descriptor sock]
||| Binds a socket to the given socket address and port.
||| Returns 0 on success, an error code otherwise.
bind : (sock : Socket)
-> (addr : Maybe SocketAddress)
-> (port : Port)
-> IO Int
bind sock addr port = do
bind_res <- cCall Int "idrnet_bind"
[ descriptor sock, toCode $ family sock
, toCode $ socketType sock, saString addr, port
]
if bind_res == (-1)
then getErrno
else pure 0
where
saString : Maybe SocketAddress -> String
saString (Just sa) = show sa
saString Nothing = ""
||| Connects to a given address and port.
||| Returns 0 on success, and an error number on error.
connect : (sock : Socket)
-> (addr : SocketAddress)
-> (port : Port)
-> IO ResultCode
connect sock addr port = do
conn_res <- cCall Int "idrnet_connect"
[ descriptor sock, toCode $ family sock, toCode $ socketType sock, show addr, port]
if conn_res == (-1)
then getErrno
else pure 0
||| Listens on a bound socket.
|||
||| @sock The socket to listen on.
listen : (sock : Socket) -> IO Int
listen sock = do
listen_res <- cCall Int "listen" [ descriptor sock, BACKLOG ]
if listen_res == (-1)
then getErrno
else pure 0
||| Accept a connection on the provided socket.
|||
||| Returns on failure a `SocketError`
||| Returns on success a pairing of:
||| + `Socket` :: The socket representing the connection.
||| + `SocketAddress` :: The
|||
||| @sock The socket used to establish connection.
accept : (sock : Socket)
-> IO (Either SocketError (Socket, SocketAddress))
accept sock = do
-- We need a pointer to a sockaddr structure. This is then passed into
-- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
sockaddr_ptr <- cCall Ptr "idrnet_create_sockaddr" []
accept_res <- cCall Int "idrnet_accept" [ descriptor sock, sockaddr_ptr ]
if accept_res == (-1)
then map Left getErrno
else do
let (MkSocket _ fam ty p_num) = sock
sockaddr <- getSockAddr (SAPtr sockaddr_ptr)
sockaddr_free (SAPtr sockaddr_ptr)
pure $ Right ((MkSocket accept_res fam ty p_num), sockaddr)
||| Send data on the specified socket.
|||
||| Returns on failure a `SocketError`.
||| Returns on success the `ResultCode`.
|||
||| @sock The socket on which to send the message.
||| @msg The data to send.
send : (sock : Socket)
-> (msg : String)
-> IO (Either SocketError ResultCode)
send sock dat = do
send_res <- cCall Int "idrnet_send" [ descriptor sock, dat ]
if send_res == (-1)
then map Left getErrno
else pure $ Right send_res
||| Receive data on the specified socket.
|||
||| Returns on failure a `SocketError`
||| Returns on success a pairing of:
||| + `String` :: The payload.
||| + `ResultCode` :: The result of the underlying function.
|||
||| @sock The socket on which to receive the message.
||| @len How much of the data to receive.
recv : (sock : Socket)
-> (len : ByteLength)
-> IO (Either SocketError (String, ResultCode))
recv sock len = do
-- Firstly make the request, get some kind of recv structure which
-- contains the result of the recv and possibly the retrieved payload
recv_struct_ptr <- cCall Ptr "idrnet_recv" [ descriptor sock, len]
recv_res <- cCall Int "idrnet_get_recv_res" [ recv_struct_ptr ]
if recv_res == (-1)
then do
errno <- getErrno
freeRecvStruct (RSPtr recv_struct_ptr)
pure $ Left errno
else
if recv_res == 0
then do
freeRecvStruct (RSPtr recv_struct_ptr)
pure $ Left 0
else do
payload <- cCall String "idrnet_get_recv_payload" [ recv_struct_ptr ]
freeRecvStruct (RSPtr recv_struct_ptr)
pure $ Right (payload, recv_res)
||| Receive all the remaining data on the specified socket.
|||
||| Returns on failure a `SocketError`
||| Returns on success the payload `String`
|||
||| @sock The socket on which to receive the message.
partial
recvAll : (sock : Socket) -> IO (Either SocketError String)
recvAll sock = recvRec sock [] 64
where
partial
recvRec : Socket -> List String -> ByteLength -> IO (Either SocketError String)
recvRec sock acc n = do res <- recv sock n
case res of
Left 0 => pure (Right $ concat $ reverse acc)
Left c => pure (Left c)
Right (str, _) => let n' = min (n * 2) 65536 in
recvRec sock (str :: acc) n'
||| Send a message.
|||
||| Returns on failure a `SocketError`
||| Returns on success the `ResultCode`
|||
||| @sock The socket on which to send the message.
||| @addr Address of the recipient.
||| @port The port on which to send the message.
||| @msg The message to send.
sendTo : (sock : Socket)
-> (addr : SocketAddress)
-> (port : Port)
-> (msg : String)
-> IO (Either SocketError ByteLength)
sendTo sock addr p dat = do
sendto_res <- cCall Int "idrnet_sendto"
[ descriptor sock, dat, show addr, p ,toCode $ family sock ]
if sendto_res == (-1)
then map Left getErrno
else pure $ Right sendto_res
||| Receive a message.
|||
||| Returns on failure a `SocketError`.
||| Returns on success a triple of
||| + `UDPAddrInfo` :: The address of the sender.
||| + `String` :: The payload.
||| + `Int` :: Result value from underlying function.
|||
||| @sock The channel on which to receive.
||| @len Size of the expected message.
|||
recvFrom : (sock : Socket)
-> (len : ByteLength)
-> IO (Either SocketError (UDPAddrInfo, String, ResultCode))
recvFrom sock bl = do
recv_ptr <- cCall Ptr "idrnet_recvfrom"
[ descriptor sock, bl ]
let recv_ptr' = RFPtr recv_ptr
isNull <- (nullPtr recv_ptr)
if isNull
then map Left getErrno
else do
result <- cCall Int "idrnet_get_recvfrom_res" [ recv_ptr ]
if result == -1
then do
freeRecvfromStruct recv_ptr'
map Left getErrno
else do
payload <- foreignGetRecvfromPayload recv_ptr'
port <- foreignGetRecvfromPort recv_ptr'
addr <- foreignGetRecvfromAddr recv_ptr'
freeRecvfromStruct recv_ptr'
pure $ Right (MkUDPAddrInfo addr port, payload, result)

214
libs/network/Network/Socket/Data.idr Normal file
View File

@ -0,0 +1,214 @@
||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
||| Types used by Network.Socket.Raw and Network.Socket.
|||
||| Original (C) SimonJF, MIT Licensed, 2014
||| Modified (C) The Idris Community, 2015, 2016, 2019
module Network.Socket.Data
import Data.List
import Data.Strings
-- ------------------------------------------------------------ [ Type Aliases ]
-- FIXME should be generic name with OS-dependent suffix
%cg chez "libidris_net.so"
public export
ByteLength : Type
ByteLength = Int
public export
ResultCode : Type
ResultCode = Int
||| Protocol Number.
|||
||| Generally good enough to just set it to 0.
public export
ProtocolNumber : Type
ProtocolNumber = Int
||| SocketError: Error thrown by a socket operation
public export
SocketError : Type
SocketError = Int
||| SocketDescriptor: Native C Socket Descriptor
public export
SocketDescriptor : Type
SocketDescriptor = Int
public export
Port : Type
Port = Int
-- --------------------------------------------------------------- [ Constants ]
||| Backlog used within listen() call -- number of incoming calls
export
BACKLOG : Int
BACKLOG = 20
export
EAGAIN : Int
EAGAIN =
-- I'm sorry
-- maybe
unsafePerformIO $ cCall Int "idrnet_geteagain" []
-- ---------------------------------------------------------------- [ Error Code ]
export
getErrno : IO SocketError
getErrno = cCall Int "idrnet_errno" []
export
nullPtr : Ptr -> IO Bool
nullPtr p = cCall Bool "isNull" [p]
-- -------------------------------------------------------------- [ Interfaces ]
public export
interface ToCode a where
toCode : a -> Int
-- --------------------------------------------------------- [ Socket Families ]
||| Socket Families
|||
||| The ones that people might actually use. We're not going to need US
||| Government proprietary ones.
public export
data SocketFamily : Type where
||| Unspecified
AF_UNSPEC : SocketFamily
||| Unix type sockets
AF_UNIX : SocketFamily
||| IP / UDP etc. IPv4
AF_INET : SocketFamily
||| IP / UDP etc. IPv6
AF_INET6 : SocketFamily
Show SocketFamily where
show AF_UNSPEC = "AF_UNSPEC"
show AF_UNIX = "AF_UNIX"
show AF_INET = "AF_INET"
show AF_INET6 = "AF_INET6"
export
ToCode SocketFamily where
-- Don't know how to read a constant value from C code in idris2...
-- gotta to hardcode those for now
toCode AF_UNSPEC = 0 -- unsafePerformIO (cMacro "#AF_UNSPEC" Int)
toCode AF_UNIX = 1
toCode AF_INET = 2
toCode AF_INET6 = 10
export
getSocketFamily : Int -> Maybe SocketFamily
getSocketFamily i =
lookup i [ (toCode AF_UNSPEC, AF_UNSPEC)
, (toCode AF_UNIX, AF_UNIX)
, (toCode AF_INET, AF_INET)
, (toCode AF_INET6, AF_INET6)
]
-- ------------------------------------------------------------ [ Socket Types ]
||| Socket Types.
public export
data SocketType : Type where
||| Not a socket, used in certain operations
NotASocket : SocketType
||| TCP
Stream : SocketType
||| UDP
Datagram : SocketType
||| Raw sockets
RawSocket : SocketType
export
Show SocketType where
show NotASocket = "Not a socket"
show Stream = "Stream"
show Datagram = "Datagram"
show RawSocket = "Raw"
export
ToCode SocketType where
toCode NotASocket = 0
toCode Stream = 1
toCode Datagram = 2
toCode RawSocket = 3
-- --------------------------------------------------------------- [ Addresses ]
||| Network Addresses
public export
data SocketAddress : Type where
IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
||| Not implemented (yet)
IPv6Addr : SocketAddress
Hostname : String -> SocketAddress
||| Used when there's a parse error
InvalidAddress : SocketAddress
export
Show SocketAddress where
show (IPv4Addr i1 i2 i3 i4) = concat $ intersperse "." (map show [i1, i2, i3, i4])
show IPv6Addr = "NOT IMPLEMENTED YET"
show (Hostname host) = host
show InvalidAddress = "Invalid"
||| Parses a textual representation of an IPv4 address into a SocketAddress
export
parseIPv4 : String -> SocketAddress
parseIPv4 str =
case splitted of
(i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
otherwise => InvalidAddress
where
toInt' : String -> Integer
toInt' = cast
toInt : String -> Int
toInt s = fromInteger $ toInt' s
splitted : List Int
splitted = map toInt (split (\c => c == '.') str)
-- --------------------------------------------------------- [ UDP Information ]
-- TODO: Expand to non-string payloads
public export
record UDPRecvData where
constructor MkUDPRecvData
remote_addr : SocketAddress
remote_port : Port
recv_data : String
data_len : Int
public export
record UDPAddrInfo where
constructor MkUDPAddrInfo
remote_addr : SocketAddress
remote_port : Port
-- ----------------------------------------------------------------- [ Sockets ]
||| The metadata about a socket
public export
record Socket where
constructor MkSocket
descriptor : SocketDescriptor
family : SocketFamily
socketType : SocketType
protocolNumber : ProtocolNumber

190
libs/network/Network/Socket/Raw.idr Normal file
View File

@ -0,0 +1,190 @@
||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
||| Type-unsafe parts. Use Network.Socket for a safe variant.
|||
||| Original (C) SimonJF, MIT Licensed, 2014
||| Modified (C) The Idris Community, 2015, 2016
module Network.Socket.Raw
import public Network.Socket.Data
-- ---------------------------------------------------------------- [ Pointers ]
public export
data RecvStructPtr = RSPtr Ptr
public export
data RecvfromStructPtr = RFPtr Ptr
public export
data BufPtr = BPtr Ptr
public export
data SockaddrPtr = SAPtr Ptr
-- ---------------------------------------------------------- [ Socket Utilies ]
||| Frees a given pointer
sock_free : BufPtr -> IO ()
sock_free (BPtr ptr) = cCall () "idrnet_free" [ptr]
export
sockaddr_free : SockaddrPtr -> IO ()
sockaddr_free (SAPtr ptr) = cCall () "idrnet_free" [ptr]
||| Allocates an amount of memory given by the ByteLength parameter.
|||
||| Used to allocate a mutable pointer to be given to the Recv functions.
sock_alloc : ByteLength -> IO BufPtr
sock_alloc bl = map BPtr $ cCall Ptr "idrnet_malloc" [bl]
||| Retrieves the port the given socket is bound to
export
getSockPort : Socket -> IO Port
getSockPort sock = cCall Int "idrnet_sockaddr_port" [descriptor sock]
||| Retrieves a socket address from a sockaddr pointer
export
getSockAddr : SockaddrPtr -> IO SocketAddress
getSockAddr (SAPtr ptr) = do
addr_family_int <- cCall Int "idrnet_sockaddr_family" [ptr]
-- ASSUMPTION: Foreign call returns a valid int
assert_total (case getSocketFamily addr_family_int of
Just AF_INET => do
ipv4_addr <- cCall String "idrnet_sockaddr_ipv4" [ptr]
pure $ parseIPv4 ipv4_addr
Just AF_INET6 => pure IPv6Addr
Just AF_UNSPEC => pure InvalidAddress)
export
freeRecvStruct : RecvStructPtr -> IO ()
freeRecvStruct (RSPtr p) = cCall () "idrnet_free_recv_struct" [p]
||| Utility to extract data.
export
freeRecvfromStruct : RecvfromStructPtr -> IO ()
freeRecvfromStruct (RFPtr p) = cCall () "idrnet_free_recvfrom_struct" [p]
||| Sends the data in a given memory location
|||
||| Returns on failure a `SocketError`
||| Returns on success the `ResultCode`
|||
||| @sock The socket on which to send the message.
||| @ptr The location containing the data to send.
||| @len How much of the data to send.
export
sendBuf : (sock : Socket)
-> (ptr : BufPtr)
-> (len : ByteLength)
-> IO (Either SocketError ResultCode)
sendBuf sock (BPtr ptr) len = do
send_res <- cCall Int "idrnet_send_buf" [ descriptor sock, ptr, len]
if send_res == (-1)
then map Left getErrno
else pure $ Right send_res
||| Receive data from a given memory location.
|||
||| Returns on failure a `SocketError`
||| Returns on success the `ResultCode`
|||
||| @sock The socket on which to receive the message.
||| @ptr The location containing the data to receive.
||| @len How much of the data to receive.
export
recvBuf : (sock : Socket)
-> (ptr : BufPtr)
-> (len : ByteLength)
-> IO (Either SocketError ResultCode)
recvBuf sock (BPtr ptr) len = do
recv_res <- cCall Int "idrnet_recv_buf" [ descriptor sock, ptr, len ]
if (recv_res == (-1))
then map Left getErrno
else pure $ Right recv_res
||| Send a message stored in some buffer.
|||
||| Returns on failure a `SocketError`
||| Returns on success the `ResultCode`
|||
||| @sock The socket on which to send the message.
||| @addr Address of the recipient.
||| @port The port on which to send the message.
||| @ptr A Pointer to the buffer containing the message.
||| @len The size of the message.
export
sendToBuf : (sock : Socket)
-> (addr : SocketAddress)
-> (port : Port)
-> (ptr : BufPtr)
-> (len : ByteLength)
-> IO (Either SocketError ResultCode)
sendToBuf sock addr p (BPtr dat) len = do
sendto_res <- cCall Int "idrnet_sendto_buf"
[ descriptor sock, dat, len, show addr, p, toCode $ family sock ]
if sendto_res == (-1)
then map Left getErrno
else pure $ Right sendto_res
||| Utility function to get the payload of the sent message as a `String`.
export
foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
foreignGetRecvfromPayload (RFPtr p) = cCall String "idrnet_get_recvfrom_payload" [ p ]
||| Utility function to return senders socket address.
export
foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
foreignGetRecvfromAddr (RFPtr p) = do
sockaddr_ptr <- map SAPtr $ cCall Ptr "idrnet_get_recvfrom_sockaddr" [p]
getSockAddr sockaddr_ptr
||| Utility function to return sender's IPV4 port.
export
foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
foreignGetRecvfromPort (RFPtr p) = do
sockaddr_ptr <- cCall Ptr "idrnet_get_recvfrom_sockaddr" [p]
port <- cCall Int "idrnet_sockaddr_ipv4_port" [sockaddr_ptr]
pure port
||| Receive a message placed on a 'known' buffer.
|||
||| Returns on failure a `SocketError`.
||| Returns on success a pair of
||| + `UDPAddrInfo` :: The address of the sender.
||| + `Int` :: Result value from underlying function.
|||
||| @sock The channel on which to receive.
||| @ptr Pointer to the buffer to place the message.
||| @len Size of the expected message.
|||
export
recvFromBuf : (sock : Socket)
-> (ptr : BufPtr)
-> (len : ByteLength)
-> IO (Either SocketError (UDPAddrInfo, ResultCode))
recvFromBuf sock (BPtr ptr) bl = do
recv_ptr <- cCall Ptr "idrnet_recvfrom_buf" [ descriptor sock, ptr, bl]
let recv_ptr' = RFPtr recv_ptr
isnull <- nullPtr recv_ptr
if isnull
then map Left getErrno
else do
result <- cCall Int "idrnet_get_recvfrom_res" [recv_ptr]
if result == -1
then do
freeRecvfromStruct recv_ptr'
map Left getErrno
else do
port <- foreignGetRecvfromPort recv_ptr'
addr <- foreignGetRecvfromAddr recv_ptr'
freeRecvfromStruct recv_ptr'
pure $ Right (MkUDPAddrInfo addr port, result + 1)

4
libs/network/expected Normal file
View File

@ -0,0 +1,4 @@
Client sent 12 bytes
Received: hello world!
Server sent 18 bytes
Received: echo: hello world!

383
libs/network/idris_net.c Normal file
View File

@ -0,0 +1,383 @@
// C-Side of the Idris network library
// (C) Simon Fowler, 2014
// MIT Licensed. Have fun!
#include "idris_net.h"
#include <errno.h>
#include <stdbool.h>
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#ifndef _WIN32
#include <netinet/in.h>
#include <arpa/inet.h>
#else
static int socket_inited = 0;
static WSADATA wsa_data;
static void clean_sockets(void) {
WSACleanup();
}
static int check_init(void) {
if (!socket_inited) {
int result = WSAStartup(MAKEWORD(2, 2), &wsa_data);
if (result == NO_ERROR) {
socket_inited = 1;
atexit(clean_sockets);
}
}
return socket_inited;
}
#endif
void buf_htonl(void* buf, int len) {
int* buf_i = (int*) buf;
int i;
for (i = 0; i < (len / sizeof(int)) + 1; i++) {
buf_i[i] = htonl(buf_i[i]);
}
}
void buf_ntohl(void* buf, int len) {
int* buf_i = (int*) buf;
int i;
for (i = 0; i < (len / sizeof(int)) + 1; i++) {
buf_i[i] = ntohl(buf_i[i]);
}
}
void* idrnet_malloc(int size) {
return malloc(size);
}
void idrnet_free(void* ptr) {
free(ptr);
}
int idrnet_socket(int domain, int type, int protocol) {
#ifdef _WIN32
if (!check_init()) {
return -1;
}
#endif
return socket(domain, type, protocol);
}
// We call this from quite a few functions. Given a textual host and an int port,
// populates a struct addrinfo.
int idrnet_getaddrinfo(struct addrinfo** address_res, char* host, int port,
int family, int socket_type) {
struct addrinfo hints;
// Convert port into string
char str_port[8];
sprintf(str_port, "%d", port);
// Set up hints structure
memset(&hints, 0, sizeof(hints)); // zero out hints
hints.ai_family = family;
hints.ai_socktype = socket_type;
// If the length of the hostname is 0 (i.e, it was set to Nothing in Idris)
// then we want to instruct the C library to fill in the IP automatically
if (strlen(host) == 0) {
hints.ai_flags = AI_PASSIVE; // fill in IP automatically
return getaddrinfo(NULL, str_port, &hints, address_res);
}
return getaddrinfo(host, str_port, &hints, address_res);
}
int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) {
struct addrinfo *address_res;
int addr_res = idrnet_getaddrinfo(&address_res, host, port, family, socket_type);
if (addr_res != 0) {
//printf("Lib err: bind getaddrinfo\n");
return -1;
}
int bind_res = bind(sockfd, address_res->ai_addr, address_res->ai_addrlen);
if (bind_res == -1) {
//freeaddrinfo(address_res);
//printf("Lib err: bind\n");
return -1;
}
return 0;
}
// to retrieve information about a socket bound to port 0
int idrnet_getsockname(int sockfd, void *address, void *len) {
int res = getsockname(sockfd, address, len);
if(res != 0) {
return -1;
}
return 0;
}
int idrnet_sockaddr_port(int sockfd) {
struct sockaddr address;
socklen_t addrlen = sizeof(struct sockaddr);
int res = getsockname(sockfd, &address, &addrlen);
if(res < 0) {
return -1;
}
switch(address.sa_family) {
case AF_INET:
return ntohs(((struct sockaddr_in*)&address)->sin_port);
case AF_INET6:
return ntohs(((struct sockaddr_in6*)&address)->sin6_port);
default:
return -1;
}
}
int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port) {
struct addrinfo* remote_host;
int addr_res = idrnet_getaddrinfo(&remote_host, host, port, family, socket_type);
if (addr_res != 0) {
return -1;
}
int connect_res = connect(sockfd, remote_host->ai_addr, remote_host->ai_addrlen);
if (connect_res == -1) {
freeaddrinfo(remote_host);
return -1;
}
freeaddrinfo(remote_host);
return 0;
}
int idrnet_sockaddr_family(void* sockaddr) {
struct sockaddr* addr = (struct sockaddr*) sockaddr;
return (int) addr->sa_family;
}
char* idrnet_sockaddr_ipv4(void* sockaddr) {
struct sockaddr_in* addr = (struct sockaddr_in*) sockaddr;
char* ip_addr = (char*) malloc(sizeof(char) * INET_ADDRSTRLEN);
inet_ntop(AF_INET, &(addr->sin_addr), ip_addr, INET_ADDRSTRLEN);
//printf("Lib: ip_addr: %s\n", ip_addr);
return ip_addr;
}
int idrnet_sockaddr_ipv4_port(void* sockaddr) {
struct sockaddr_in* addr = (struct sockaddr_in*) sockaddr;
return ((int) ntohs(addr->sin_port));
}
void* idrnet_create_sockaddr() {
return malloc(sizeof(struct sockaddr_storage));
}
int idrnet_accept(int sockfd, void* sockaddr) {
struct sockaddr* addr = (struct sockaddr*) sockaddr;
socklen_t addr_size = sizeof(struct sockaddr_storage);
return accept(sockfd, addr, &addr_size);
}
int idrnet_send(int sockfd, char* data) {
int len = strlen(data); // For now.
return send(sockfd, (void*) data, len, 0);
}
int idrnet_send_buf(int sockfd, void* data, int len) {
void* buf_cpy = malloc(len);
memset(buf_cpy, 0, len);
memcpy(buf_cpy, data, len);
buf_htonl(buf_cpy, len);
int res = send(sockfd, buf_cpy, len, 0);
free(buf_cpy);
return res;
}
void* idrnet_recv(int sockfd, int len) {
idrnet_recv_result* res_struct =
(idrnet_recv_result*) malloc(sizeof(idrnet_recv_result));
char* buf = malloc(len + 1);
memset(buf, 0, len + 1);
int recv_res = recv(sockfd, buf, len, 0);
res_struct->result = recv_res;
if (recv_res > 0) { // Data was received
buf[recv_res + 1] = 0x00; // Null-term, so Idris can interpret it
}
res_struct->payload = buf;
return (void*) res_struct;
}
int idrnet_recv_buf(int sockfd, void* buf, int len) {
int recv_res = recv(sockfd, buf, len, 0);
if (recv_res != -1) {
buf_ntohl(buf, len);
}
return recv_res;
}
int idrnet_get_recv_res(void* res_struct) {
return (((idrnet_recv_result*) res_struct)->result);
}
char* idrnet_get_recv_payload(void* res_struct) {
return (((idrnet_recv_result*) res_struct)->payload);
}
void idrnet_free_recv_struct(void* res_struct) {
idrnet_recv_result* i_res_struct =
(idrnet_recv_result*) res_struct;
if (i_res_struct->payload != NULL) {
free(i_res_struct->payload);
}
free(res_struct);
}
int idrnet_errno() {
return errno;
}
int idrnet_sendto(int sockfd, char* data, char* host, int port, int family) {
struct addrinfo* remote_host;
int addr_res = idrnet_getaddrinfo(&remote_host, host, port, family, SOCK_DGRAM);
if (addr_res != 0) {
return -1;
}
int send_res = sendto(sockfd, data, strlen(data), 0,
remote_host->ai_addr, remote_host->ai_addrlen);
freeaddrinfo(remote_host);
return send_res;
}
int idrnet_sendto_buf(int sockfd, void* buf, int buf_len, char* host, int port, int family) {
struct addrinfo* remote_host;
int addr_res = idrnet_getaddrinfo(&remote_host, host, port, family, SOCK_DGRAM);
if (addr_res != 0) {
//printf("lib err: sendto getaddrinfo \n");
return -1;
}
buf_htonl(buf, buf_len);
int send_res = sendto(sockfd, buf, buf_len, 0,
remote_host->ai_addr, remote_host->ai_addrlen);
if (send_res == -1) {
perror("lib err: sendto \n");
}
//freeaddrinfo(remote_host);
return send_res;
}
void* idrnet_recvfrom(int sockfd, int len) {
/*
* int recvfrom(int sockfd, void *buf, int len, unsigned int flags,
struct sockaddr *from, int *fromlen);
*/
// Allocate the required structures, and nuke them
struct sockaddr_storage* remote_addr =
(struct sockaddr_storage*) malloc(sizeof(struct sockaddr_storage));
char* buf = (char*) malloc(len + 1);
idrnet_recvfrom_result* ret =
(idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));
memset(remote_addr, 0, sizeof(struct sockaddr_storage));
memset(buf, 0, len + 1);
memset(ret, 0, sizeof(idrnet_recvfrom_result));
socklen_t fromlen = sizeof(struct sockaddr_storage);
int recv_res = recvfrom(sockfd, buf, len, 0, (struct sockaddr*) remote_addr, &fromlen);
ret->result = recv_res;
// Check for failure...
if (recv_res == -1) {
free(buf);
free(remote_addr);
} else {
// If data was received, process and populate
ret->result = recv_res;
ret->remote_addr = remote_addr;
// Ensure the last byte is NULL, since in this mode we're sending strings
buf[len] = 0x00;
ret->payload = (void*) buf;
}
return ret;
}
void* idrnet_recvfrom_buf(int sockfd, void* buf, int len) {
// Allocate the required structures, and nuke them
struct sockaddr_storage* remote_addr =
(struct sockaddr_storage*) malloc(sizeof(struct sockaddr_storage));
idrnet_recvfrom_result* ret =
(idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));
memset(remote_addr, 0, sizeof(struct sockaddr_storage));
memset(ret, 0, sizeof(idrnet_recvfrom_result));
socklen_t fromlen = 0;
int recv_res = recvfrom(sockfd, buf, len, 0, (struct sockaddr*) remote_addr, &fromlen);
// Check for failure... But don't free the buffer! Not our job.
ret->result = recv_res;
if (recv_res == -1) {
free(remote_addr);
}
// Payload will be NULL -- since it's been put into the user-specified buffer. We
// still need the return struct to get our hands on the remote address, though.
if (recv_res > 0) {
buf_ntohl(buf, len);
ret->payload = NULL;
ret->remote_addr = remote_addr;
}
return ret;
}
int idrnet_get_recvfrom_res(void* res_struct) {
return (((idrnet_recvfrom_result*) res_struct)->result);
}
char* idrnet_get_recvfrom_payload(void* res_struct) {
return (((idrnet_recvfrom_result*) res_struct)->payload);
}
void* idrnet_get_recvfrom_sockaddr(void* res_struct) {
idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;
return recv_struct->remote_addr;
}
int idrnet_get_recvfrom_port(void* res_struct) {
idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;
if (recv_struct->remote_addr != NULL) {
struct sockaddr_in* remote_addr_in =
(struct sockaddr_in*) recv_struct->remote_addr;
return ((int) ntohs(remote_addr_in->sin_port));
}
return -1;
}
void idrnet_free_recvfrom_struct(void* res_struct) {
idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;
if (recv_struct != NULL) {
if (recv_struct->payload != NULL) {
free(recv_struct->payload);
}
if (recv_struct->remote_addr != NULL) {
free(recv_struct->remote_addr);
}
}
}
int idrnet_geteagain() {
return EAGAIN;
}
int isNull(void* ptr) {
return ptr==NULL;
}

98
libs/network/idris_net.h Normal file
View File

@ -0,0 +1,98 @@
#ifndef IDRISNET_H
#define IDRISNET_H
// Includes used by the idris-file.
#ifdef _WIN32
#include <winsock2.h>
#include <Ws2tcpip.h>
#else
#include <netdb.h>
#include <unistd.h>
#include <sys/types.h>
#include <sys/socket.h>
#endif
struct sockaddr_storage;
struct addrinfo;
typedef struct idrnet_recv_result {
int result;
void* payload;
} idrnet_recv_result;
// Same type of thing as idrnet_recv_result, but for UDP, so stores some
// address information
typedef struct idrnet_recvfrom_result {
int result;
void* payload;
struct sockaddr_storage* remote_addr;
} idrnet_recvfrom_result;
// Memory management functions
void* idrnet_malloc(int size);
void idrnet_free(void* ptr);
// Gets value of errno
int idrnet_errno();
int idrnet_socket(int domain, int type, int protocol);
// Bind
int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port);
// Retrieve information about socket
int idrnet_getsockname(int sockfd, void *address, void *len);
// Connect
int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port);
// Accessor functions for struct_sockaddr
int idrnet_sockaddr_family(void* sockaddr);
char* idrnet_sockaddr_ipv4(void* sockaddr);
int idrnet_sockaddr_ipv4_port(void* sockaddr);
void* idrnet_create_sockaddr();
int idrnet_sockaddr_port(int sockfd);
// Accept
int idrnet_accept(int sockfd, void* sockaddr);
// Send
int idrnet_send(int sockfd, char* data);
int idrnet_send_buf(int sockfd, void* data, int len);
// Receive
// Creates a result structure containing result and payload
void* idrnet_recv(int sockfd, int len);
// Receives directly into a buffer
int idrnet_recv_buf(int sockfd, void* buf, int len);
// UDP Send
int idrnet_sendto(int sockfd, char* data, char* host, int port, int family);
int idrnet_sendto_buf(int sockfd, void* buf, int buf_len, char* host, int port, int family);
// UDP Receive
void* idrnet_recvfrom(int sockfd, int len);
void* idrnet_recvfrom_buf(int sockfd, void* buf, int len);
// Receive structure accessors
int idrnet_get_recv_res(void* res_struct);
char* idrnet_get_recv_payload(void* res_struct);
void idrnet_free_recv_struct(void* res_struct);
// Recvfrom structure accessors
int idrnet_get_recvfrom_res(void* res_struct);
char* idrnet_get_recvfrom_payload(void* res_struct);
void* idrnet_get_recvfrom_sockaddr(void* res_struct);
void idrnet_free_recvfrom_struct(void* res_struct);
int idrnet_getaddrinfo(struct addrinfo** address_res, char* host,
int port, int family, int socket_type);
int idrnet_geteagain();
int isNull(void* ptr);
#endif

10
libs/network/lib-tests Executable file
View File

@ -0,0 +1,10 @@
#!/bin/sh
${IDRIS2} --exec main Echo.idr > build/output
if ! [ -z "$(diff build/output expected)" ]; then
echo "TEST FAILURE: unexpected build/output"
exit 2
else
echo "TEST SUCCESS"
fi

5
libs/network/network.ipkg Normal file
View File

@ -0,0 +1,5 @@
package network
modules = Network.Socket,
Network.Socket.Data,
Network.Socket.Raw

41
libs/network/test.c Normal file
View File

@ -0,0 +1,41 @@
#include <assert.h>
#include <stdio.h>
#include <netinet/in.h>
#include <arpa/inet.h>
#include "idris_net.h"
void test_sockaddr_port_returns_random_port_when_bind_port_is_0() {
int sock = idrnet_socket(AF_INET, 1, 0);
assert(sock > 0);
int res = idrnet_bind(sock, AF_INET, 1, "127.0.0.1", 0);
assert(res == 0);
res = idrnet_sockaddr_port(sock);
assert(res > 0);
close(sock);
}
void test_sockaddr_port_returns_explicitly_assigned_port() {
int sock = idrnet_socket(AF_INET, 1, 0);
assert(sock > 0);
int res = idrnet_bind(sock, AF_INET, 1, "127.0.0.1", 34567);
assert(res == 0);
res = idrnet_sockaddr_port(sock);
assert(res == 34567);
close(sock);
}
int main(int argc, char**argv) {
test_sockaddr_port_returns_explicitly_assigned_port();
test_sockaddr_port_returns_random_port_when_bind_port_is_0();
printf("network library tests SUCCESS\n");
return 0;
}