From 18d83420da924d7f4198120fb841b517dfdfc6ae Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Mon, 22 Jul 2019 17:21:38 +0200 Subject: [PATCH 01/16] initial import of idris 1 network lib --- Makefile | 7 +- libs/network/Makefile | 61 +++++ libs/network/Network/Cgi.idr | 146 +++++++++++ libs/network/Network/Socket.idr | 245 +++++++++++++++++++ libs/network/Network/Socket/Data.idr | 178 ++++++++++++++ libs/network/Network/Socket/Raw.idr | 199 +++++++++++++++ libs/network/idris_net.c | 350 +++++++++++++++++++++++++++ libs/network/idris_net.h | 91 +++++++ libs/network/network.ipkg | 6 + 9 files changed, 1282 insertions(+), 1 deletion(-) create mode 100644 libs/network/Makefile create mode 100644 libs/network/Network/Cgi.idr create mode 100644 libs/network/Network/Socket.idr create mode 100644 libs/network/Network/Socket/Data.idr create mode 100644 libs/network/Network/Socket/Raw.idr create mode 100644 libs/network/idris_net.c create mode 100644 libs/network/idris_net.h create mode 100644 libs/network/network.ipkg diff --git a/Makefile b/Makefile index 4125f0a..4055de9 100644 --- a/Makefile +++ b/Makefile @@ -20,7 +20,10 @@ prelude: base: prelude make -C libs/base IDRIS2=../../idris2 -libs : prelude base +network: prelude + make -C libs/network IDRIS2=../../idris2 + +libs : prelude base network clean: clean-libs make -C src clean @@ -31,6 +34,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 @@ -51,3 +55,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 diff --git a/libs/network/Makefile b/libs/network/Makefile new file mode 100644 index 0000000..0ba969f --- /dev/null +++ b/libs/network/Makefile @@ -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 + +ifeq ($(OS),darwin) + SHLIB_SUFFIX :=.dylib + LIBFLAGS :=-dynamiclib +else ifeq ($(OS),windows) + SHLIB_SUFFIX :=.DLL + LIBFLAGS :=-shared +else + SHLIB_SUFFIX :=.so + LIBFLAGS :=-shared +endif + +OBJS = idris_net.o +HDRS = idris_net.h +CFLAGS := $(CFLAGS) + +ifneq ($(OS), windows) + CFLAGS += -fPIC +endif + +DYLIBTARGET = idrnet$(SHLIB_SUFFIX) +LIBTARGET = idrnet.a +TARGET=${HOME}/.idris2 + +build: $(LIBTARGET) $(DYLIBTARGET) + +$(LIBTARGET) : $(OBJS) + $(AR) rc $(LIBTARGET) $(OBJS) + $(RANLIB) $(LIBTARGET) + +$(DYLIBTARGET) : $(OBJS) + $(CC) -o $(DYLIBTARGET) $(LIBFLAGS) -shared $(OBJS) + +install: build + install $(LIBTARGET) $(HDRS) $(TARGET) + ${IDRIS2} --install network.ipkg + +clean : + rm -rf $(OBJS) $(LIBTARGET) $(DYLIBTARGET) build + +$(OBJS): $(HDRS) + +all: $(DYLIBTARGET) $(LIBTARGET) + ${IDRIS2} --build network1.ipkg + +.PHONY: build install clean diff --git a/libs/network/Network/Cgi.idr b/libs/network/Network/Cgi.idr new file mode 100644 index 0000000..48d9499 --- /dev/null +++ b/libs/network/Network/Cgi.idr @@ -0,0 +1,146 @@ +module Network.Cgi + +import System + +%default total + +public export +Vars : Type +Vars = List (String, String) + +record CGIInfo where + constructor CGISt + GET : Vars + POST : Vars + Cookies : Vars + UserAgent : String + Headers : String + Output : String + +add_Headers : String -> CGIInfo -> CGIInfo +add_Headers str st = record { Headers = Headers st ++ str } st + +add_Output : String -> CGIInfo -> CGIInfo +add_Output str st = record { Output = Output st ++ str } st + +export +data CGI : Type -> Type where + MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a + +getAction : CGI a -> CGIInfo -> IO (a, CGIInfo) +getAction (MkCGI act) = act + +export +implementation Functor CGI where + map f (MkCGI c) = MkCGI (\s => do (a, i) <- c s + pure (f a, i)) + +export +implementation Applicative CGI where + pure v = MkCGI (\s => pure (v, s)) + + (MkCGI a) <*> (MkCGI b) = MkCGI (\s => do (f, i) <- a s + (c, j) <- b i + pure (f c, j)) + +export +implementation Monad CGI where + (>>=) (MkCGI f) k = MkCGI (\s => do v <- f s + getAction (k (fst v)) (snd v)) + +setInfo : CGIInfo -> CGI () +setInfo i = MkCGI (\s => pure ((), i)) + +getInfo : CGI CGIInfo +getInfo = MkCGI (\s => pure (s, s)) + +export +lift : IO a -> CGI a +lift op = MkCGI (\st => do { x <- op + pure (x, st) } ) + +export +output : String -> CGI () +output s = do i <- getInfo + setInfo (add_Output s i) + +export +queryVars : CGI Vars +queryVars = do i <- getInfo + pure (GET i) + +export +postVars : CGI Vars +postVars = do i <- getInfo + pure (POST i) + +export +cookieVars : CGI Vars +cookieVars = do i <- getInfo + pure (Cookies i) + +export +queryVar : String -> CGI (Maybe String) +queryVar x = do vs <- queryVars + pure (lookup x vs) + +getOutput : CGI String +getOutput = do i <- getInfo + pure (Output i) + +getHeaders : CGI String +getHeaders = do i <- getInfo + pure (Headers i) + +export +flushHeaders : CGI () +flushHeaders = do o <- getHeaders + lift (putStrLn o) + +export +flush : CGI () +flush = do o <- getOutput + lift (putStr o) + +getVars : List Char -> String -> List (String, String) +getVars seps query = mapMaybe readVar (split (\x => elem x seps) query) + where + readVar : String -> Maybe (String, String) + readVar xs with (split (\x => x == '=') xs) + | [k, v] = Just (trim k, trim v) + | _ = Nothing + +getContent : Int -> IO String +getContent x = getC (cast x) "" where + getC : Nat -> String -> IO String + getC Z acc = pure $ reverse acc + getC (S k) acc = do x <- getChar + getC k (strCons x acc) + +getCgiEnv : String -> IO String +getCgiEnv key = do + val <- getEnv key + pure $ maybe "" id val + +export +runCGI : CGI a -> IO a +runCGI prog = do + clen_in <- getCgiEnv "CONTENT_LENGTH" + let clen = prim__fromStrInt clen_in + content <- getContent clen + query <- getCgiEnv "QUERY_STRING" + cookie <- getCgiEnv "HTTP_COOKIE" + agent <- getCgiEnv "HTTP_USER_AGENT" + + let get_vars = getVars ['&',';'] query + let post_vars = getVars ['&'] content + let cookies = getVars [';'] cookie + + (v, st) <- getAction prog (CGISt get_vars post_vars cookies agent + "Content-type: text/html\n" + "") + putStrLn (Headers st) + putStr (Output st) + pure v + + diff --git a/libs/network/Network/Socket.idr b/libs/network/Network/Socket.idr new file mode 100644 index 0000000..f5638c6 --- /dev/null +++ b/libs/network/Network/Socket.idr @@ -0,0 +1,245 @@ +||| 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 + +%include C "idris_net.h" + +%access export + +-- ----------------------------------------------------- [ 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 <- foreign FFI_C "idrnet_socket" + (Int -> Int -> Int -> IO Int) + (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 = foreign FFI_C "close" (Int -> IO ()) (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 <- foreign FFI_C "idrnet_bind" + (Int -> Int -> Int -> String -> Int -> IO Int) + (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 <- foreign FFI_C "idrnet_connect" + (Int -> Int -> Int -> String -> Int -> IO Int) + (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 <- foreign FFI_C "listen" (Int -> Int -> IO Int) + (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 <- foreign FFI_C "idrnet_create_sockaddr" + (IO Ptr) + + accept_res <- foreign FFI_C "idrnet_accept" + (Int -> Ptr -> IO Int) + (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 <- foreign FFI_C "idrnet_send" + (Int -> String -> IO Int) + (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 <- foreign FFI_C "idrnet_recv" + (Int -> Int -> IO Ptr) + (descriptor sock) len + recv_res <- foreign FFI_C "idrnet_get_recv_res" + (Ptr -> IO Int) + 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 <- foreign FFI_C "idrnet_get_recv_payload" + (Ptr -> IO String) + 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 <- foreign FFI_C "idrnet_sendto" + (Int -> String -> String -> Int -> Int -> IO Int) + (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 <- foreign FFI_C "idrnet_recvfrom" + (Int -> Int -> IO Ptr) + (descriptor sock) bl + + let recv_ptr' = RFPtr recv_ptr + + if !(nullPtr recv_ptr) + then map Left getErrno + else do + result <- foreign FFI_C "idrnet_get_recvfrom_res" + (Ptr -> IO Int) + 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) diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr new file mode 100644 index 0000000..83a46f3 --- /dev/null +++ b/libs/network/Network/Socket/Data.idr @@ -0,0 +1,178 @@ +||| 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 + +-- ------------------------------------------------------------ [ Type Aliases ] + +-- FIXME should be generic name with OS-dependent suffix +%cg chez "./libidrnet.dylib" + +export +ByteLength : Type +ByteLength = Int + +export +ResultCode : Type +ResultCode = Int + +||| Protocol Number. +||| +||| Generally good enough to just set it to 0. +export +ProtocolNumber : Type +ProtocolNumber = Int + +||| SocketError: Error thrown by a socket operation +export +SocketError : Type +SocketError = Int + +||| SocketDescriptor: Native C Socket Descriptor +export +SocketDescriptor : Type +SocketDescriptor = Int + +export +Port : Type +Port = Int + +-- --------------------------------------------------------------- [ Constants ] + +||| Backlog used within listen() call -- number of incoming calls +BACKLOG : Int +BACKLOG = 20 + +EAGAIN : Int +EAGAIN = + -- I'm sorry + -- maybe + unsafePerformIO $ foreign FFI_C "idrnet_geteagain" (() -> IO Int) () + +-- -------------------------------------------------------------- [ Interfaces ] + +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. +data SocketFamily : Type where + ||| Unspecified + AF_UNSPEC : 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_INET = "AF_INET" + show AF_INET6 = "AF_INET6" + +ToCode SocketFamily where + toCode AF_UNSPEC = unsafePerformIO (foreign FFI_C "#AF_UNSPEC" (IO Int)) + toCode AF_INET = unsafePerformIO (foreign FFI_C "#AF_INET" (IO Int)) + toCode AF_INET6 = unsafePerformIO (foreign FFI_C "#AF_INET6" (IO Int)) + +getSocketFamily : Int -> Maybe SocketFamily +getSocketFamily i = + Prelude.List.lookup i [ (toCode AF_UNSPEC, AF_UNSPEC) + , (toCode AF_INET, AF_INET) + , (toCode AF_INET6, AF_INET6) + ] + +-- ------------------------------------------------------------ [ Socket Types ] + +||| Socket Types. +data SocketType : Type where + ||| Not a socket, used in certain operations + NotASocket : SocketType + + ||| TCP + Stream : SocketType + + ||| UDP + Datagram : SocketType + + ||| Raw sockets + RawSocket : SocketType + +Show SocketType where + show NotASocket = "Not a socket" + show Stream = "Stream" + show Datagram = "Datagram" + show RawSocket = "Raw" + +ToCode SocketType where + toCode NotASocket = 0 + toCode Stream = 1 + toCode Datagram = 2 + toCode RawSocket = 3 + +-- --------------------------------------------------------------- [ Addresses ] + +||| Network Addresses +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 + +Show SocketAddress where + show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.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 +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 (Prelude.Strings.split (\c => c == '.') str) + +-- --------------------------------------------------------- [ UDP Information ] + +-- TODO: Expand to non-string payloads +record UDPRecvData where + constructor MkUDPRecvData + remote_addr : SocketAddress + remote_port : Port + recv_data : String + data_len : Int + +record UDPAddrInfo where + constructor MkUDPAddrInfo + remote_addr : SocketAddress + remote_port : Port + +-- ----------------------------------------------------------------- [ Sockets ] +||| The metadata about a socket +record Socket where + constructor MkSocket + descriptor : SocketDescriptor + family : SocketFamily + socketType : SocketType + protocolNumber : ProtocolNumber diff --git a/libs/network/Network/Socket/Raw.idr b/libs/network/Network/Socket/Raw.idr new file mode 100644 index 0000000..b3e1a57 --- /dev/null +++ b/libs/network/Network/Socket/Raw.idr @@ -0,0 +1,199 @@ +||| 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 + +%include C "idris_net.h" + +%access public export + +-- ---------------------------------------------------------------- [ Pointers ] + +data RecvStructPtr = RSPtr Ptr +data RecvfromStructPtr = RFPtr Ptr + +data BufPtr = BPtr Ptr + +data SockaddrPtr = SAPtr Ptr + +-- ---------------------------------------------------------- [ Socket Utilies ] + +||| Frees a given pointer +sock_free : BufPtr -> IO () +sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr + +sockaddr_free : SockaddrPtr -> IO () +sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) 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 $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl + +||| Retrieves a socket address from a sockaddr pointer +getSockAddr : SockaddrPtr -> IO SocketAddress +getSockAddr (SAPtr ptr) = do + addr_family_int <- foreign FFI_C "idrnet_sockaddr_family" + (Ptr -> IO Int) + ptr + + -- ASSUMPTION: Foreign call returns a valid int + assert_total (case getSocketFamily addr_family_int of + Just AF_INET => do + ipv4_addr <- foreign FFI_C "idrnet_sockaddr_ipv4" + (Ptr -> IO String) + ptr + + pure $ parseIPv4 ipv4_addr + Just AF_INET6 => pure IPv6Addr + Just AF_UNSPEC => pure InvalidAddress) + +freeRecvStruct : RecvStructPtr -> IO () +freeRecvStruct (RSPtr p) = + foreign FFI_C "idrnet_free_recv_struct" + (Ptr -> IO ()) + p + +||| Utility to extract data. +freeRecvfromStruct : RecvfromStructPtr -> IO () +freeRecvfromStruct (RFPtr p) = + foreign FFI_C "idrnet_free_recvfrom_struct" + (Ptr -> IO ()) + 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. +sendBuf : (sock : Socket) + -> (ptr : BufPtr) + -> (len : ByteLength) + -> IO (Either SocketError ResultCode) +sendBuf sock (BPtr ptr) len = do + send_res <- foreign FFI_C "idrnet_send_buf" + (Int -> Ptr -> Int -> IO Int) + (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. +recvBuf : (sock : Socket) + -> (ptr : BufPtr) + -> (len : ByteLength) + -> IO (Either SocketError ResultCode) +recvBuf sock (BPtr ptr) len = do + recv_res <- foreign FFI_C "idrnet_recv_buf" + (Int -> Ptr -> Int -> IO Int) + (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. +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 <- foreign FFI_C "idrnet_sendto_buf" + (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int) + (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`. +foreignGetRecvfromPayload : RecvfromStructPtr -> IO String +foreignGetRecvfromPayload (RFPtr p) = + foreign FFI_C "idrnet_get_recvfrom_payload" + (Ptr -> IO String) + p + +||| Utility function to return senders socket address. +foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress +foreignGetRecvfromAddr (RFPtr p) = do + sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr" + (Ptr -> IO Ptr) + p + getSockAddr sockaddr_ptr + +||| Utility function to return sender's IPV4 port. +foreignGetRecvfromPort : RecvfromStructPtr -> IO Port +foreignGetRecvfromPort (RFPtr p) = do + sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr" + (Ptr -> IO Ptr) + p + port <- foreign FFI_C "idrnet_sockaddr_ipv4_port" + (Ptr -> IO Int) + 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. +||| +recvFromBuf : (sock : Socket) + -> (ptr : BufPtr) + -> (len : ByteLength) + -> IO (Either SocketError (UDPAddrInfo, ResultCode)) +recvFromBuf sock (BPtr ptr) bl = do + recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf" + (Int -> Ptr -> Int -> IO Ptr) + (descriptor sock) ptr bl + + let recv_ptr' = RFPtr recv_ptr + + if !(nullPtr recv_ptr) + then map Left getErrno + else do + result <- foreign FFI_C "idrnet_get_recvfrom_res" + (Ptr -> IO Int) + 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) + diff --git a/libs/network/idris_net.c b/libs/network/idris_net.c new file mode 100644 index 0000000..e1b7465 --- /dev/null +++ b/libs/network/idris_net.c @@ -0,0 +1,350 @@ +// C-Side of the Idris network library +// (C) Simon Fowler, 2014 +// MIT Licensed. Have fun! +#include "idris_net.h" +#include +#include +#include +#include +#include + +#ifndef _WIN32 +#include +#include +#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; +} + +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; +} diff --git a/libs/network/idris_net.h b/libs/network/idris_net.h new file mode 100644 index 0000000..8558f03 --- /dev/null +++ b/libs/network/idris_net.h @@ -0,0 +1,91 @@ +#ifndef IDRISNET_H +#define IDRISNET_H + +// Includes used by the idris-file. +#ifdef _WIN32 +#include +#include +#else +#include +#include +#include +#include +#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); + +// 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(); + +// 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(); + +#endif diff --git a/libs/network/network.ipkg b/libs/network/network.ipkg new file mode 100644 index 0000000..6a4edbf --- /dev/null +++ b/libs/network/network.ipkg @@ -0,0 +1,6 @@ +package network + +modules = Network.Socket, + Network.Socket.Data, + Network.Socket.Raw, + Network.Cgi From 7f53d0d54decffdcb0965219e9506fc885bbd058 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Tue, 23 Jul 2019 09:37:48 +0200 Subject: [PATCH 02/16] add 'missing' functions into base libraries --- libs/base/Data/List.idr | 51 ++++++++++++++++++++++++++++++-------- libs/base/Data/Strings.idr | 11 ++++++++ 2 files changed, 52 insertions(+), 10 deletions(-) diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr index 4e42eba..2a06532 100644 --- a/libs/base/Data/List.idr +++ b/libs/base/Data/List.idr @@ -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) @@ -105,6 +122,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 -------------------------------------------------------------------------------- @@ -166,20 +199,20 @@ sort = sortBy compare -- Uninhabited ([] = _ :: _) where -- uninhabited Refl impossible --- +-- -- Uninhabited (_ :: _ = []) 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} -> @@ -191,13 +224,13 @@ sort = sortBy compare -- 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) -> @@ -215,5 +248,3 @@ appendAssociative [] c r = Refl appendAssociative (x::xs) c r = let inductiveHypothesis = appendAssociative xs c r in rewrite inductiveHypothesis in Refl - - diff --git a/libs/base/Data/Strings.idr b/libs/base/Data/Strings.idr index 64e0168..583dc39 100644 --- a/libs/base/Data/Strings.idr +++ b/libs/base/Data/Strings.idr @@ -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 From 2b11b7cc32b5b60f69131083f68a1d940af99d4e Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Tue, 23 Jul 2019 09:38:28 +0200 Subject: [PATCH 03/16] add test target and basic test 'harness' test harness is a grand word for just a basic C main file that uses plain macro to run tests --- libs/network/Makefile | 28 ++++++++++++++++------------ libs/network/test.c | 12 ++++++++++++ 2 files changed, 28 insertions(+), 12 deletions(-) create mode 100644 libs/network/test.c diff --git a/libs/network/Makefile b/libs/network/Makefile index 0ba969f..6c040fd 100644 --- a/libs/network/Makefile +++ b/libs/network/Makefile @@ -25,37 +25,41 @@ else LIBFLAGS :=-shared endif -OBJS = idris_net.o -HDRS = idris_net.h +LIBNAME=idris_net +OBJS = $(LIBNAME).o +HDRS = $(LIBNAME).h CFLAGS := $(CFLAGS) ifneq ($(OS), windows) CFLAGS += -fPIC endif -DYLIBTARGET = idrnet$(SHLIB_SUFFIX) -LIBTARGET = idrnet.a +DYLIBTARGET = lib$(LIBNAME)$(SHLIB_SUFFIX) +LIBTARGET = $(LIBNAME).a TARGET=${HOME}/.idris2 -build: $(LIBTARGET) $(DYLIBTARGET) - -$(LIBTARGET) : $(OBJS) - $(AR) rc $(LIBTARGET) $(OBJS) - $(RANLIB) $(LIBTARGET) +build: $(DYLIBTARGET) + @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: build - install $(LIBTARGET) $(HDRS) $(TARGET) +install: + install $(DYLIBTARGET) $(HDRS) $(TARGET) ${IDRIS2} --install network.ipkg clean : rm -rf $(OBJS) $(LIBTARGET) $(DYLIBTARGET) build +test: $(DYLIBTARGET) + $(CC) -o network-tests -L. -I. -l$(LIBNAME) test.c + ./network-tests + $(OBJS): $(HDRS) all: $(DYLIBTARGET) $(LIBTARGET) - ${IDRIS2} --build network1.ipkg + ${IDRIS2} --build network.ipkg .PHONY: build install clean diff --git a/libs/network/test.c b/libs/network/test.c new file mode 100644 index 0000000..4de6c4e --- /dev/null +++ b/libs/network/test.c @@ -0,0 +1,12 @@ +#include +#include +#include "idris_net.h" + + +int main(int argc, char**argv) { + int eagain = idrnet_geteagain(); + assert(eagain == 35); + + printf("network library tests SUCCESS\n"); + return 0; +} From 7c1b1bc98d1ad81f5ab5a9444dda24a47b94ab3e Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Tue, 23 Jul 2019 22:39:54 +0200 Subject: [PATCH 04/16] got code to compile * removed Cgi * add a couple of utility functions to the C source * converted all foreign calls to use cCall --- libs/network/Network/Cgi.idr | 146 --------------------------- libs/network/Network/Socket.idr | 68 +++++-------- libs/network/Network/Socket/Data.idr | 70 +++++++++---- libs/network/Network/Socket/Raw.idr | 87 +++++++--------- libs/network/idris_net.c | 4 + libs/network/idris_net.h | 2 + libs/network/network.ipkg | 3 +- 7 files changed, 119 insertions(+), 261 deletions(-) delete mode 100644 libs/network/Network/Cgi.idr diff --git a/libs/network/Network/Cgi.idr b/libs/network/Network/Cgi.idr deleted file mode 100644 index 48d9499..0000000 --- a/libs/network/Network/Cgi.idr +++ /dev/null @@ -1,146 +0,0 @@ -module Network.Cgi - -import System - -%default total - -public export -Vars : Type -Vars = List (String, String) - -record CGIInfo where - constructor CGISt - GET : Vars - POST : Vars - Cookies : Vars - UserAgent : String - Headers : String - Output : String - -add_Headers : String -> CGIInfo -> CGIInfo -add_Headers str st = record { Headers = Headers st ++ str } st - -add_Output : String -> CGIInfo -> CGIInfo -add_Output str st = record { Output = Output st ++ str } st - -export -data CGI : Type -> Type where - MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a - -getAction : CGI a -> CGIInfo -> IO (a, CGIInfo) -getAction (MkCGI act) = act - -export -implementation Functor CGI where - map f (MkCGI c) = MkCGI (\s => do (a, i) <- c s - pure (f a, i)) - -export -implementation Applicative CGI where - pure v = MkCGI (\s => pure (v, s)) - - (MkCGI a) <*> (MkCGI b) = MkCGI (\s => do (f, i) <- a s - (c, j) <- b i - pure (f c, j)) - -export -implementation Monad CGI where - (>>=) (MkCGI f) k = MkCGI (\s => do v <- f s - getAction (k (fst v)) (snd v)) - -setInfo : CGIInfo -> CGI () -setInfo i = MkCGI (\s => pure ((), i)) - -getInfo : CGI CGIInfo -getInfo = MkCGI (\s => pure (s, s)) - -export -lift : IO a -> CGI a -lift op = MkCGI (\st => do { x <- op - pure (x, st) } ) - -export -output : String -> CGI () -output s = do i <- getInfo - setInfo (add_Output s i) - -export -queryVars : CGI Vars -queryVars = do i <- getInfo - pure (GET i) - -export -postVars : CGI Vars -postVars = do i <- getInfo - pure (POST i) - -export -cookieVars : CGI Vars -cookieVars = do i <- getInfo - pure (Cookies i) - -export -queryVar : String -> CGI (Maybe String) -queryVar x = do vs <- queryVars - pure (lookup x vs) - -getOutput : CGI String -getOutput = do i <- getInfo - pure (Output i) - -getHeaders : CGI String -getHeaders = do i <- getInfo - pure (Headers i) - -export -flushHeaders : CGI () -flushHeaders = do o <- getHeaders - lift (putStrLn o) - -export -flush : CGI () -flush = do o <- getOutput - lift (putStr o) - -getVars : List Char -> String -> List (String, String) -getVars seps query = mapMaybe readVar (split (\x => elem x seps) query) - where - readVar : String -> Maybe (String, String) - readVar xs with (split (\x => x == '=') xs) - | [k, v] = Just (trim k, trim v) - | _ = Nothing - -getContent : Int -> IO String -getContent x = getC (cast x) "" where - getC : Nat -> String -> IO String - getC Z acc = pure $ reverse acc - getC (S k) acc = do x <- getChar - getC k (strCons x acc) - -getCgiEnv : String -> IO String -getCgiEnv key = do - val <- getEnv key - pure $ maybe "" id val - -export -runCGI : CGI a -> IO a -runCGI prog = do - clen_in <- getCgiEnv "CONTENT_LENGTH" - let clen = prim__fromStrInt clen_in - content <- getContent clen - query <- getCgiEnv "QUERY_STRING" - cookie <- getCgiEnv "HTTP_COOKIE" - agent <- getCgiEnv "HTTP_USER_AGENT" - - let get_vars = getVars ['&',';'] query - let post_vars = getVars ['&'] content - let cookies = getVars [';'] cookie - - (v, st) <- getAction prog (CGISt get_vars post_vars cookies agent - "Content-type: text/html\n" - "") - putStrLn (Headers st) - putStr (Output st) - pure v - - diff --git a/libs/network/Network/Socket.idr b/libs/network/Network/Socket.idr index f5638c6..e255f58 100644 --- a/libs/network/Network/Socket.idr +++ b/libs/network/Network/Socket.idr @@ -6,10 +6,7 @@ module Network.Socket import public Network.Socket.Data import Network.Socket.Raw - -%include C "idris_net.h" - -%access export +import Data.List -- ----------------------------------------------------- [ Network Socket API. ] @@ -20,9 +17,7 @@ socket : (fam : SocketFamily) -> (pnum : ProtocolNumber) -> IO (Either SocketError Socket) socket sf st pn = do - socket_res <- foreign FFI_C "idrnet_socket" - (Int -> Int -> Int -> IO Int) - (toCode sf) (toCode st) pn + socket_res <- cCall Int "idrnet_socket" [toCode sf, toCode st, pn] if socket_res == -1 then map Left getErrno @@ -30,7 +25,7 @@ socket sf st pn = do ||| Close a socket close : Socket -> IO () -close sock = foreign FFI_C "close" (Int -> IO ()) (descriptor sock) +close sock = cCall () "close" [descriptor sock] ||| Binds a socket to the given socket address and port. ||| Returns 0 on success, an error code otherwise. @@ -39,10 +34,10 @@ bind : (sock : Socket) -> (port : Port) -> IO Int bind sock addr port = do - bind_res <- foreign FFI_C "idrnet_bind" - (Int -> Int -> Int -> String -> Int -> IO Int) - (descriptor sock) (toCode $ family sock) - (toCode $ socketType sock) (saString addr) port + 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 @@ -58,9 +53,8 @@ connect : (sock : Socket) -> (port : Port) -> IO ResultCode connect sock addr port = do - conn_res <- foreign FFI_C "idrnet_connect" - (Int -> Int -> Int -> String -> Int -> IO Int) - (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port + conn_res <- cCall Int "idrnet_connect" + [ descriptor sock, toCode $ family sock, toCode $ socketType sock, show addr, port] if conn_res == (-1) then getErrno @@ -71,8 +65,7 @@ connect sock addr port = do ||| @sock The socket to listen on. listen : (sock : Socket) -> IO Int listen sock = do - listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int) - (descriptor sock) BACKLOG + listen_res <- cCall Int "listen" [ descriptor sock, BACKLOG ] if listen_res == (-1) then getErrno else pure 0 @@ -92,12 +85,9 @@ 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 <- foreign FFI_C "idrnet_create_sockaddr" - (IO Ptr) + sockaddr_ptr <- cCall Ptr "idrnet_create_sockaddr" [] - accept_res <- foreign FFI_C "idrnet_accept" - (Int -> Ptr -> IO Int) - (descriptor sock) sockaddr_ptr + accept_res <- cCall Int "idrnet_accept" [ descriptor sock, sockaddr_ptr ] if accept_res == (-1) then map Left getErrno else do @@ -117,9 +107,7 @@ send : (sock : Socket) -> (msg : String) -> IO (Either SocketError ResultCode) send sock dat = do - send_res <- foreign FFI_C "idrnet_send" - (Int -> String -> IO Int) - (descriptor sock) dat + send_res <- cCall Int "idrnet_send" [ descriptor sock, dat ] if send_res == (-1) then map Left getErrno @@ -140,12 +128,8 @@ recv : (sock : Socket) 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 <- foreign FFI_C "idrnet_recv" - (Int -> Int -> IO Ptr) - (descriptor sock) len - recv_res <- foreign FFI_C "idrnet_get_recv_res" - (Ptr -> IO Int) - recv_struct_ptr + 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 @@ -158,9 +142,7 @@ recv sock len = do freeRecvStruct (RSPtr recv_struct_ptr) pure $ Left 0 else do - payload <- foreign FFI_C "idrnet_get_recv_payload" - (Ptr -> IO String) - recv_struct_ptr + payload <- cCall String "idrnet_get_recv_payload" [ recv_struct_ptr ] freeRecvStruct (RSPtr recv_struct_ptr) pure $ Right (payload, recv_res) @@ -198,9 +180,8 @@ sendTo : (sock : Socket) -> (msg : String) -> IO (Either SocketError ByteLength) sendTo sock addr p dat = do - sendto_res <- foreign FFI_C "idrnet_sendto" - (Int -> String -> String -> Int -> Int -> IO Int) - (descriptor sock) dat (show addr) p (toCode $ family sock) + sendto_res <- cCall Int "idrnet_sendto" + [ descriptor sock, dat, show addr, p ,toCode $ family sock ] if sendto_res == (-1) then map Left getErrno @@ -221,18 +202,15 @@ recvFrom : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError (UDPAddrInfo, String, ResultCode)) recvFrom sock bl = do - recv_ptr <- foreign FFI_C "idrnet_recvfrom" - (Int -> Int -> IO Ptr) - (descriptor sock) bl + recv_ptr <- cCall Ptr "idrnet_recvfrom" + [ descriptor sock, bl ] let recv_ptr' = RFPtr recv_ptr - - if !(nullPtr recv_ptr) + isNull <- (nullPtr recv_ptr) + if isNull then map Left getErrno else do - result <- foreign FFI_C "idrnet_get_recvfrom_res" - (Ptr -> IO Int) - recv_ptr + result <- cCall Int "idrnet_get_recvfrom_res" [ recv_ptr ] if result == -1 then do freeRecvfromStruct recv_ptr' diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr index 83a46f3..b4f8874 100644 --- a/libs/network/Network/Socket/Data.idr +++ b/libs/network/Network/Socket/Data.idr @@ -5,54 +5,70 @@ ||| 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 "./libidrnet.dylib" +%cg chez "libidris_net.dylib" -export +public export ByteLength : Type ByteLength = Int -export +public export ResultCode : Type ResultCode = Int ||| Protocol Number. ||| ||| Generally good enough to just set it to 0. -export +public export ProtocolNumber : Type ProtocolNumber = Int ||| SocketError: Error thrown by a socket operation -export +public export SocketError : Type SocketError = Int ||| SocketDescriptor: Native C Socket Descriptor -export +public export SocketDescriptor : Type SocketDescriptor = Int -export +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 $ foreign FFI_C "idrnet_geteagain" (() -> IO Int) () + unsafePerformIO $ cCall Int "idrnet_geteagain" [] + +-- ---------------------------------------------------------------- [ Error Code ] + +export +getErrno : IO SocketError +getErrno = cCall SocketError "idrnet_errno" [] + +export +nullPtr : Ptr -> IO Bool +nullPtr p = cCall Bool "isNull" [p] -- -------------------------------------------------------------- [ Interfaces ] +public export interface ToCode a where toCode : a -> Int @@ -62,10 +78,14 @@ interface ToCode a where ||| ||| 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 @@ -74,24 +94,32 @@ data SocketFamily : Type where 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 - toCode AF_UNSPEC = unsafePerformIO (foreign FFI_C "#AF_UNSPEC" (IO Int)) - toCode AF_INET = unsafePerformIO (foreign FFI_C "#AF_INET" (IO Int)) - toCode AF_INET6 = unsafePerformIO (foreign FFI_C "#AF_INET6" (IO Int)) + -- 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 = - Prelude.List.lookup i [ (toCode AF_UNSPEC, AF_UNSPEC) - , (toCode AF_INET, AF_INET) - , (toCode AF_INET6, AF_INET6) - ] + 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 @@ -105,12 +133,14 @@ data SocketType : Type where ||| 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 @@ -120,6 +150,7 @@ ToCode SocketType where -- --------------------------------------------------------------- [ Addresses ] ||| Network Addresses +public export data SocketAddress : Type where IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress @@ -131,13 +162,15 @@ data SocketAddress : Type where ||| Used when there's a parse error InvalidAddress : SocketAddress +export Show SocketAddress where - show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4]) + 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 @@ -151,11 +184,12 @@ parseIPv4 str = toInt s = fromInteger $ toInt' s splitted : List Int - splitted = map toInt (Prelude.Strings.split (\c => c == '.') str) + 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 @@ -163,6 +197,7 @@ record UDPRecvData where recv_data : String data_len : Int +public export record UDPAddrInfo where constructor MkUDPAddrInfo remote_addr : SocketAddress @@ -170,6 +205,7 @@ record UDPAddrInfo where -- ----------------------------------------------------------------- [ Sockets ] ||| The metadata about a socket +public export record Socket where constructor MkSocket descriptor : SocketDescriptor diff --git a/libs/network/Network/Socket/Raw.idr b/libs/network/Network/Socket/Raw.idr index b3e1a57..9f03e3e 100644 --- a/libs/network/Network/Socket/Raw.idr +++ b/libs/network/Network/Socket/Raw.idr @@ -7,64 +7,59 @@ module Network.Socket.Raw import public Network.Socket.Data -%include C "idris_net.h" - -%access public export - -- ---------------------------------------------------------------- [ 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) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr +sock_free (BPtr ptr) = cCall () "idrnet_free" [ptr] +export sockaddr_free : SockaddrPtr -> IO () -sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr +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 $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl +sock_alloc bl = map BPtr $ cCall Ptr "idrnet_malloc" [bl] ||| Retrieves a socket address from a sockaddr pointer +export getSockAddr : SockaddrPtr -> IO SocketAddress getSockAddr (SAPtr ptr) = do - addr_family_int <- foreign FFI_C "idrnet_sockaddr_family" - (Ptr -> IO Int) - ptr + 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 <- foreign FFI_C "idrnet_sockaddr_ipv4" - (Ptr -> IO String) - ptr + 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) = - foreign FFI_C "idrnet_free_recv_struct" - (Ptr -> IO ()) - p +freeRecvStruct (RSPtr p) = cCall () "idrnet_free_recv_struct" [p] ||| Utility to extract data. +export freeRecvfromStruct : RecvfromStructPtr -> IO () -freeRecvfromStruct (RFPtr p) = - foreign FFI_C "idrnet_free_recvfrom_struct" - (Ptr -> IO ()) - p +freeRecvfromStruct (RFPtr p) = cCall () "idrnet_free_recvfrom_struct" [p] ||| Sends the data in a given memory location ||| @@ -74,14 +69,13 @@ freeRecvfromStruct (RFPtr p) = ||| @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 <- foreign FFI_C "idrnet_send_buf" - (Int -> Ptr -> Int -> IO Int) - (descriptor sock) ptr len + send_res <- cCall Int "idrnet_send_buf" [ descriptor sock, ptr, len] if send_res == (-1) then map Left getErrno @@ -95,14 +89,13 @@ sendBuf sock (BPtr ptr) len = do ||| @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 <- foreign FFI_C "idrnet_recv_buf" - (Int -> Ptr -> Int -> IO Int) - (descriptor sock) ptr len + recv_res <- cCall ResultCode "idrnet_recv_buf" [ descriptor sock, ptr, len ] if (recv_res == (-1)) then map Left getErrno @@ -118,6 +111,7 @@ recvBuf sock (BPtr ptr) len = do ||| @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) @@ -125,38 +119,31 @@ sendToBuf : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError ResultCode) sendToBuf sock addr p (BPtr dat) len = do - sendto_res <- foreign FFI_C "idrnet_sendto_buf" - (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int) - (descriptor sock) dat len (show addr) p (toCode $ family sock) + sendto_res <- cCall ResultCode "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) = - foreign FFI_C "idrnet_get_recvfrom_payload" - (Ptr -> IO String) - p +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 $ foreign FFI_C "idrnet_get_recvfrom_sockaddr" - (Ptr -> IO Ptr) - p + 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 <- foreign FFI_C "idrnet_get_recvfrom_sockaddr" - (Ptr -> IO Ptr) - p - port <- foreign FFI_C "idrnet_sockaddr_ipv4_port" - (Ptr -> IO Int) - sockaddr_ptr + 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. @@ -170,23 +157,22 @@ foreignGetRecvfromPort (RFPtr p) = do ||| @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 <- foreign FFI_C "idrnet_recvfrom_buf" - (Int -> Ptr -> Int -> IO Ptr) - (descriptor sock) ptr bl + recv_ptr <- cCall Ptr "idrnet_recvfrom_buf" [ descriptor sock, ptr, bl] let recv_ptr' = RFPtr recv_ptr - if !(nullPtr recv_ptr) + isnull <- nullPtr recv_ptr + + if isnull then map Left getErrno else do - result <- foreign FFI_C "idrnet_get_recvfrom_res" - (Ptr -> IO Int) - recv_ptr + result <- cCall Int "idrnet_get_recvfrom_res" [recv_ptr] if result == -1 then do freeRecvfromStruct recv_ptr' @@ -196,4 +182,3 @@ recvFromBuf sock (BPtr ptr) bl = do addr <- foreignGetRecvfromAddr recv_ptr' freeRecvfromStruct recv_ptr' pure $ Right (MkUDPAddrInfo addr port, result + 1) - diff --git a/libs/network/idris_net.c b/libs/network/idris_net.c index e1b7465..1916b7b 100644 --- a/libs/network/idris_net.c +++ b/libs/network/idris_net.c @@ -348,3 +348,7 @@ void idrnet_free_recvfrom_struct(void* res_struct) { int idrnet_geteagain() { return EAGAIN; } + +int isNull(void* ptr) { + return ptr==NULL; +} diff --git a/libs/network/idris_net.h b/libs/network/idris_net.h index 8558f03..275d987 100644 --- a/libs/network/idris_net.h +++ b/libs/network/idris_net.h @@ -88,4 +88,6 @@ int idrnet_getaddrinfo(struct addrinfo** address_res, char* host, int idrnet_geteagain(); +int isNull(void* ptr); + #endif diff --git a/libs/network/network.ipkg b/libs/network/network.ipkg index 6a4edbf..968728c 100644 --- a/libs/network/network.ipkg +++ b/libs/network/network.ipkg @@ -2,5 +2,4 @@ package network modules = Network.Socket, Network.Socket.Data, - Network.Socket.Raw, - Network.Cgi + Network.Socket.Raw From dc219a07ec60bb19668dfe3a37be51a2f2727a07 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Wed, 24 Jul 2019 09:17:29 +0200 Subject: [PATCH 05/16] provide a way to retrieve port of (server) socket bound to 0 --- libs/network/Network/Socket/Raw.idr | 6 ++++++ libs/network/idris_net.c | 29 +++++++++++++++++++++++++++++ libs/network/idris_net.h | 5 +++++ libs/network/test.c | 29 +++++++++++++++++++++++++++-- 4 files changed, 67 insertions(+), 2 deletions(-) diff --git a/libs/network/Network/Socket/Raw.idr b/libs/network/Network/Socket/Raw.idr index 9f03e3e..90edd5e 100644 --- a/libs/network/Network/Socket/Raw.idr +++ b/libs/network/Network/Socket/Raw.idr @@ -37,6 +37,12 @@ sockaddr_free (SAPtr ptr) = cCall () "idrnet_free" [ptr] 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 Port "idrnet_sockaddr_port" [descriptor sock] + + ||| Retrieves a socket address from a sockaddr pointer export getSockAddr : SockaddrPtr -> IO SocketAddress diff --git a/libs/network/idris_net.c b/libs/network/idris_net.c index 1916b7b..f11089d 100644 --- a/libs/network/idris_net.c +++ b/libs/network/idris_net.c @@ -108,6 +108,35 @@ int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) { 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 ((struct sockaddr_in*)&address)->sin_port; + case AF_INET6: + return ((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); diff --git a/libs/network/idris_net.h b/libs/network/idris_net.h index 275d987..5f4ebe2 100644 --- a/libs/network/idris_net.h +++ b/libs/network/idris_net.h @@ -40,6 +40,9 @@ 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); @@ -49,6 +52,8 @@ 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); diff --git a/libs/network/test.c b/libs/network/test.c index 4de6c4e..81392bb 100644 --- a/libs/network/test.c +++ b/libs/network/test.c @@ -1,11 +1,36 @@ #include #include +#include +#include + #include "idris_net.h" +void test_eagain() { + int eagain = idrnet_geteagain(); + assert(eagain == 35); +} + + +void test_bind_to_0_assigns_random_port() { + struct sockaddr_in address; + socklen_t addrlen = sizeof(struct sockaddr); + 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); + + printf("socket bound to %d\n",res); + close(sock); +} + int main(int argc, char**argv) { - int eagain = idrnet_geteagain(); - assert(eagain == 35); + test_eagain(); + test_bind_to_0_assigns_random_port(); printf("network library tests SUCCESS\n"); return 0; From b5cc727f3bb74226fd3a0c702a14e3e53bd6f0ab Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Wed, 24 Jul 2019 10:08:59 +0200 Subject: [PATCH 06/16] [wip] test basic server --- libs/network/Echo.idr | 77 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) create mode 100644 libs/network/Echo.idr diff --git a/libs/network/Echo.idr b/libs/network/Echo.idr new file mode 100644 index 0000000..f3a1b2f --- /dev/null +++ b/libs/network/Echo.idr @@ -0,0 +1,77 @@ +module Main + +import Network.Socket +import Network.Socket.Data +import Network.Socket.Raw + +runServer : IO (Either String (Port, Maybe ThreadID)) +runServer = do + osock <- socket AF_INET Stream 0 + case osock of + Left fail => pure (Left $ "Failed to open socket: " ++ show fail) + Right sock => do + putStrLn "success" + pure $ Right (0,Nothing) + -- do + -- 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 sock) + -- pure $ Right (port, forked) + + -- where + -- serve : Socket -> IO () + -- serve sock = do + -- res <- accept sock + -- case res of + -- Left err => do + -- putStrLn ("Failed to accept on socket with error: " ++ show err) + -- Right (s, _) => do + -- received <- recv s 1024 + -- case received of + -- Left err => do + -- putStrLn ("Failed to accept on socket with error: " ++ show err) + -- Right (str, _) => do + -- putStrLn ("Received: " ++ str) + -- sent <- send s ("echo: " ++ str) + -- case sent of + -- Left err => do + -- putStrLn ("Server failed to send data with error: " ++ show err) + -- Right n => + -- putStrLn ("Server sent " ++ show n ++ " bytes") + +runClient : Port -> IO () +runClient serverPort = do + osock <- socket AF_INET Stream 0 + case osock of + Left fail => putStrLn ("Failed to open socket: " ++ show fail) + Right sock => do + res <- connect sock (Hostname "localhost") serverPort + if res /= 0 + then putStrLn ("Failed to connect client to port " ++ show serverPort) + else do + sent <- send sock ("hello world!") + case sent of + Left err => do + putStrLn ("Client failed to send data with error: " ++ show err) + Right n => do + putStrLn ("Client sent " ++ show n ++ " bytes") + received <- recv sock 1024 + case received of + Left err => do + putStrLn ("Client failed to receive on socket with error: " ++ show err) + Right (str, _) => do + putStrLn ("Received: " ++ str) + +-- main : IO () +-- main = do +-- server <- runServer +-- case server of +-- Left err => putStrLn $ "[server] " ++ err +-- Right (serverPort, tid) => runClient serverPort From 055a5f24490d65382348629ee0279079881c5935 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Thu, 25 Jul 2019 09:43:33 +0200 Subject: [PATCH 07/16] got a first basic test passing --- libs/network/Echo.idr | 85 ++++++++++++++-------------- libs/network/Makefile | 11 ++-- libs/network/Network/Socket/Data.idr | 2 +- libs/network/Network/Socket/Raw.idr | 6 +- libs/network/expected | 4 ++ libs/network/idris_net.c | 6 +- libs/network/test.c | 21 +++++-- 7 files changed, 77 insertions(+), 58 deletions(-) create mode 100644 libs/network/expected diff --git a/libs/network/Echo.idr b/libs/network/Echo.idr index f3a1b2f..4eeb883 100644 --- a/libs/network/Echo.idr +++ b/libs/network/Echo.idr @@ -1,50 +1,50 @@ module Main +import System import Network.Socket import Network.Socket.Data import Network.Socket.Raw -runServer : IO (Either String (Port, Maybe ThreadID)) +%cg chez libidris_net.dylib + +runServer : IO (Either String (Port, ThreadID)) runServer = do osock <- socket AF_INET Stream 0 case osock of Left fail => pure (Left $ "Failed to open socket: " ++ show fail) Right sock => do - putStrLn "success" - pure $ Right (0,Nothing) - -- do - -- 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 sock) - -- pure $ Right (port, forked) + 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 : Socket -> IO () - -- serve sock = do - -- res <- accept sock - -- case res of - -- Left err => do - -- putStrLn ("Failed to accept on socket with error: " ++ show err) - -- Right (s, _) => do - -- received <- recv s 1024 - -- case received of - -- Left err => do - -- putStrLn ("Failed to accept on socket with error: " ++ show err) - -- Right (str, _) => do - -- putStrLn ("Received: " ++ str) - -- sent <- send s ("echo: " ++ str) - -- case sent of - -- Left err => do - -- putStrLn ("Server failed to send data with error: " ++ show err) - -- Right n => - -- putStrLn ("Server sent " ++ show n ++ " bytes") + where + serve : Port -> Socket -> IO () + serve port sock = do + res <- accept sock + case res of + Left err => do + putStrLn ("Failed to accept on socket with error: " ++ show err) + Right (s, _) => do + received <- recv s 1024 + case received of + Left err => do + putStrLn ("Failed to accept on socket with error: " ++ show err) + Right (str, _) => do + putStrLn ("Received: " ++ str) + sent <- send s ("echo: " ++ str) + case sent of + Left err => do + putStrLn ("Server failed to send data with error: " ++ show err) + Right n => + putStrLn ("Server sent " ++ show n ++ " bytes") runClient : Port -> IO () runClient serverPort = do @@ -54,7 +54,7 @@ runClient serverPort = do Right sock => do res <- connect sock (Hostname "localhost") serverPort if res /= 0 - then putStrLn ("Failed to connect client to port " ++ show serverPort) + then putStrLn ("Failed to connect client to port " ++ show serverPort ++ ": " ++ show res) else do sent <- send sock ("hello world!") case sent of @@ -69,9 +69,10 @@ runClient serverPort = do Right (str, _) => do putStrLn ("Received: " ++ str) --- main : IO () --- main = do --- server <- runServer --- case server of --- Left err => putStrLn $ "[server] " ++ err --- Right (serverPort, tid) => runClient serverPort +main : IO () +main = do + server <- runServer + case server of + Left err => putStrLn $ "[server] " ++ err + Right (serverPort, tid) => do + runClient serverPort diff --git a/libs/network/Makefile b/libs/network/Makefile index 6c040fd..4d2b59c 100644 --- a/libs/network/Makefile +++ b/libs/network/Makefile @@ -29,16 +29,17 @@ 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 = lib$(LIBNAME)$(SHLIB_SUFFIX) +DYLIBTARGET = $(LIBNAME)$(SHLIB_SUFFIX) LIBTARGET = $(LIBNAME).a TARGET=${HOME}/.idris2 -build: $(DYLIBTARGET) +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 @@ -53,13 +54,15 @@ install: clean : rm -rf $(OBJS) $(LIBTARGET) $(DYLIBTARGET) build -test: $(DYLIBTARGET) +test: build test.c $(CC) -o network-tests -L. -I. -l$(LIBNAME) test.c ./network-tests + ${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 $(OBJS): $(HDRS) all: $(DYLIBTARGET) $(LIBTARGET) ${IDRIS2} --build network.ipkg -.PHONY: build install clean +.PHONY: install clean diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr index b4f8874..4070f83 100644 --- a/libs/network/Network/Socket/Data.idr +++ b/libs/network/Network/Socket/Data.idr @@ -60,7 +60,7 @@ EAGAIN = export getErrno : IO SocketError -getErrno = cCall SocketError "idrnet_errno" [] +getErrno = cCall Int "idrnet_errno" [] export nullPtr : Ptr -> IO Bool diff --git a/libs/network/Network/Socket/Raw.idr b/libs/network/Network/Socket/Raw.idr index 90edd5e..41515f3 100644 --- a/libs/network/Network/Socket/Raw.idr +++ b/libs/network/Network/Socket/Raw.idr @@ -40,7 +40,7 @@ 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 Port "idrnet_sockaddr_port" [descriptor sock] +getSockPort sock = cCall Int "idrnet_sockaddr_port" [descriptor sock] ||| Retrieves a socket address from a sockaddr pointer @@ -101,7 +101,7 @@ recvBuf : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError ResultCode) recvBuf sock (BPtr ptr) len = do - recv_res <- cCall ResultCode "idrnet_recv_buf" [ descriptor sock, ptr, len ] + recv_res <- cCall Int "idrnet_recv_buf" [ descriptor sock, ptr, len ] if (recv_res == (-1)) then map Left getErrno @@ -125,7 +125,7 @@ sendToBuf : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError ResultCode) sendToBuf sock addr p (BPtr dat) len = do - sendto_res <- cCall ResultCode "idrnet_sendto_buf" + sendto_res <- cCall Int "idrnet_sendto_buf" [ descriptor sock, dat, len, show addr, p, toCode $ family sock ] if sendto_res == (-1) diff --git a/libs/network/expected b/libs/network/expected new file mode 100644 index 0000000..bf70af7 --- /dev/null +++ b/libs/network/expected @@ -0,0 +1,4 @@ +Client sent 12 bytes +Received: hello world! +Server sent 18 bytes +Received: echo: hello world! diff --git a/libs/network/idris_net.c b/libs/network/idris_net.c index f11089d..84505f7 100644 --- a/libs/network/idris_net.c +++ b/libs/network/idris_net.c @@ -92,7 +92,7 @@ int idrnet_getaddrinfo(struct addrinfo** address_res, char* host, int port, } int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) { - struct addrinfo* address_res; + 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"); @@ -128,9 +128,9 @@ int idrnet_sockaddr_port(int sockfd) { switch(address.sa_family) { case AF_INET: - return ((struct sockaddr_in*)&address)->sin_port; + return ntohs(((struct sockaddr_in*)&address)->sin_port); case AF_INET6: - return ((struct sockaddr_in6*)&address)->sin6_port; + return ntohs(((struct sockaddr_in6*)&address)->sin6_port); default: return -1; } diff --git a/libs/network/test.c b/libs/network/test.c index 81392bb..80e94ef 100644 --- a/libs/network/test.c +++ b/libs/network/test.c @@ -11,9 +11,7 @@ void test_eagain() { } -void test_bind_to_0_assigns_random_port() { - struct sockaddr_in address; - socklen_t addrlen = sizeof(struct sockaddr); +void test_sockaddr_port_returns_random_port_when_bind_port_is_0() { int sock = idrnet_socket(AF_INET, 1, 0); assert(sock > 0); @@ -23,14 +21,27 @@ void test_bind_to_0_assigns_random_port() { res = idrnet_sockaddr_port(sock); assert(res > 0); - printf("socket bound to %d\n",res); + 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_eagain(); - test_bind_to_0_assigns_random_port(); + 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; From 87b754de4555e2c248271988016879c43170b52f Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Thu, 25 Jul 2019 19:49:15 +0200 Subject: [PATCH 08/16] fix execution of tests to actually fail if there's an error --- libs/network/Makefile | 7 +++---- libs/network/lib-tests | 10 ++++++++++ 2 files changed, 13 insertions(+), 4 deletions(-) create mode 100755 libs/network/lib-tests diff --git a/libs/network/Makefile b/libs/network/Makefile index 4d2b59c..ccd7cf4 100644 --- a/libs/network/Makefile +++ b/libs/network/Makefile @@ -35,7 +35,7 @@ ifneq ($(OS), windows) CFLAGS += -fPIC endif -DYLIBTARGET = $(LIBNAME)$(SHLIB_SUFFIX) +DYLIBTARGET = lib$(LIBNAME)$(SHLIB_SUFFIX) LIBTARGET = $(LIBNAME).a TARGET=${HOME}/.idris2 @@ -48,7 +48,7 @@ $(DYLIBTARGET) : $(OBJS) $(CC) -o $(DYLIBTARGET) $(LIBFLAGS) -shared $(OBJS) install: - install $(DYLIBTARGET) $(HDRS) $(TARGET) + install $(DYLIBTARGET) $(HDRS) $(TARGET)/idris2/network ${IDRIS2} --install network.ipkg clean : @@ -57,8 +57,7 @@ clean : test: build test.c $(CC) -o network-tests -L. -I. -l$(LIBNAME) test.c ./network-tests - ${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 + ./lib-tests $(OBJS): $(HDRS) diff --git a/libs/network/lib-tests b/libs/network/lib-tests new file mode 100755 index 0000000..67f84a0 --- /dev/null +++ b/libs/network/lib-tests @@ -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 From a87639d53a304a67f4ebdf543454d44980ef252b Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Fri, 26 Jul 2019 09:51:36 +0200 Subject: [PATCH 09/16] refactor code to be more compact uses alternative branches for failed pattern matches in do-notation --- Makefile | 1 + libs/network/Echo.idr | 93 +++++++++++++++++-------------------------- libs/network/Makefile | 2 +- 3 files changed, 38 insertions(+), 58 deletions(-) diff --git a/Makefile b/Makefile index 4055de9..08be133 100644 --- a/Makefile +++ b/Makefile @@ -22,6 +22,7 @@ base: prelude network: prelude make -C libs/network IDRIS2=../../idris2 + make -C libs/network test IDRIS2=../../idris2 libs : prelude base network diff --git a/libs/network/Echo.idr b/libs/network/Echo.idr index 4eeb883..c9a4965 100644 --- a/libs/network/Echo.idr +++ b/libs/network/Echo.idr @@ -9,70 +9,49 @@ import Network.Socket.Raw runServer : IO (Either String (Port, ThreadID)) runServer = do - osock <- socket AF_INET Stream 0 - case osock of - Left fail => pure (Left $ "Failed to open socket: " ++ show fail) - Right sock => do - 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) + 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 - res <- accept sock - case res of - Left err => do - putStrLn ("Failed to accept on socket with error: " ++ show err) - Right (s, _) => do - received <- recv s 1024 - case received of - Left err => do - putStrLn ("Failed to accept on socket with error: " ++ show err) - Right (str, _) => do - putStrLn ("Received: " ++ str) - sent <- send s ("echo: " ++ str) - case sent of - Left err => do - putStrLn ("Server failed to send data with error: " ++ show err) - Right n => - putStrLn ("Server sent " ++ show n ++ " bytes") + 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 - osock <- socket AF_INET Stream 0 - case osock of - Left fail => putStrLn ("Failed to open socket: " ++ show fail) - Right sock => do - res <- connect sock (Hostname "localhost") serverPort - if res /= 0 - then putStrLn ("Failed to connect client to port " ++ show serverPort ++ ": " ++ show res) - else do - sent <- send sock ("hello world!") - case sent of - Left err => do - putStrLn ("Client failed to send data with error: " ++ show err) - Right n => do - putStrLn ("Client sent " ++ show n ++ " bytes") - received <- recv sock 1024 - case received of - Left err => do - putStrLn ("Client failed to receive on socket with error: " ++ show err) - Right (str, _) => do - putStrLn ("Received: " ++ str) + 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 - server <- runServer - case server of - Left err => putStrLn $ "[server] " ++ err - Right (serverPort, tid) => do - runClient serverPort + Right (serverPort, tid) <- runServer + | Left err => putStrLn $ "[server] " ++ err + runClient serverPort diff --git a/libs/network/Makefile b/libs/network/Makefile index ccd7cf4..80770b3 100644 --- a/libs/network/Makefile +++ b/libs/network/Makefile @@ -48,8 +48,8 @@ $(DYLIBTARGET) : $(OBJS) $(CC) -o $(DYLIBTARGET) $(LIBFLAGS) -shared $(OBJS) install: - install $(DYLIBTARGET) $(HDRS) $(TARGET)/idris2/network ${IDRIS2} --install network.ipkg + install $(DYLIBTARGET) $(HDRS) $(TARGET)/idris2/network clean : rm -rf $(OBJS) $(LIBTARGET) $(DYLIBTARGET) build From f6b746e7ac702f0dabfdf8d51b87300b0ebe3f07 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sun, 28 Jul 2019 09:53:33 +0200 Subject: [PATCH 10/16] set LD_LIBRARY_PATH for network tests to run --- libs/network/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/network/Makefile b/libs/network/Makefile index 80770b3..348c8ca 100644 --- a/libs/network/Makefile +++ b/libs/network/Makefile @@ -55,7 +55,7 @@ clean : rm -rf $(OBJS) $(LIBTARGET) $(DYLIBTARGET) build test: build test.c - $(CC) -o network-tests -L. -I. -l$(LIBNAME) test.c + LD_LIBRARY_PATH=. $(CC) -o network-tests -L. -I. -l$(LIBNAME) test.c ./network-tests ./lib-tests From 75459e7fca921fc1b3fd1d1d9abf1a8de2f2daa5 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sun, 28 Jul 2019 22:23:26 +0200 Subject: [PATCH 11/16] fix execution of network test to correctly load library --- libs/network/Echo.idr | 2 +- libs/network/Makefile | 6 +++--- libs/network/test.c | 7 ------- 3 files changed, 4 insertions(+), 11 deletions(-) diff --git a/libs/network/Echo.idr b/libs/network/Echo.idr index c9a4965..d2bafc7 100644 --- a/libs/network/Echo.idr +++ b/libs/network/Echo.idr @@ -5,7 +5,7 @@ import Network.Socket import Network.Socket.Data import Network.Socket.Raw -%cg chez libidris_net.dylib +%cg chez libidris_net runServer : IO (Either String (Port, ThreadID)) runServer = do diff --git a/libs/network/Makefile b/libs/network/Makefile index 348c8ca..9ed11cc 100644 --- a/libs/network/Makefile +++ b/libs/network/Makefile @@ -55,9 +55,9 @@ clean : rm -rf $(OBJS) $(LIBTARGET) $(DYLIBTARGET) build test: build test.c - LD_LIBRARY_PATH=. $(CC) -o network-tests -L. -I. -l$(LIBNAME) test.c - ./network-tests - ./lib-tests + $(CC) -o network-tests -L. -I. -l$(LIBNAME) test.c + LD_LIBRARY_PATH=. ./network-tests + LD_LIBRARY_PATH=. ./lib-tests $(OBJS): $(HDRS) diff --git a/libs/network/test.c b/libs/network/test.c index 80e94ef..2504345 100644 --- a/libs/network/test.c +++ b/libs/network/test.c @@ -5,12 +5,6 @@ #include "idris_net.h" -void test_eagain() { - int eagain = idrnet_geteagain(); - assert(eagain == 35); -} - - void test_sockaddr_port_returns_random_port_when_bind_port_is_0() { int sock = idrnet_socket(AF_INET, 1, 0); assert(sock > 0); @@ -39,7 +33,6 @@ void test_sockaddr_port_returns_explicitly_assigned_port() { int main(int argc, char**argv) { - test_eagain(); test_sockaddr_port_returns_explicitly_assigned_port(); test_sockaddr_port_returns_random_port_when_bind_port_is_0(); From 9e7d79cb65640c95a6a226a4fc88558cda866be0 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sun, 28 Jul 2019 16:47:26 +0200 Subject: [PATCH 12/16] load library using OS-dependent names --- src/Compiler/Scheme/Chez.idr | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 91d83bb..e404bc2 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -40,6 +40,28 @@ findLibs = mapMaybe (isLib . trim) then Just (trim (substr 3 (length d) d)) else Nothing +||| Generate the correct dynamic library loading code depending on the target machine +loadSharedLibs : List String -> String +loadSharedLibs [] = "" +loadSharedLibs libs = + "(case (machine-type)\n" ++ + " [(i3le ti3le a6le ta6le) " ++ load asLinux ++ "]\n" ++ + " [(i3osx ti3osx a6osx ta6osx) " ++ load asMac ++ "]\n" ++ + " [(i3nt ti3nt a6nt ta6nt) " ++ load asWin ++ "]\n" ++ + " [else " ++ load asLinux ++ "])" + where + load : (String -> String) -> String + load fmt = "(begin\n" ++ showSep "\n" (map (\ s => "(load-shared-object \"" ++ fmt s ++ "\")") libs) ++ ")\n" + + asLinux : String -> String + asLinux s = "lib" ++ s ++ ".so" + + asMac : String -> String + asMac s = "lib" ++ s ++ ".dylib" + + asWin : String -> String + asWin s = s ++ ".dll" + escapeQuotes : String -> String escapeQuotes s = pack $ foldr escape [] $ unpack s where @@ -56,7 +78,7 @@ schHeader chez libs " [(i3osx ti3osx a6osx ta6osx) (load-shared-object \"libc.dylib\")]\n" ++ " [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")]\n" ++ " [else (load-shared-object \"libc.so\")])\n\n" ++ - showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeQuotes x ++ "\")") libs) ++ "\n\n" ++ + loadSharedLibs libs ++ "\n\n" ++ "(let ()\n" schFooter : String @@ -159,4 +181,3 @@ executeExpr c tm export codegenChez : Codegen codegenChez = MkCG compileExpr executeExpr - From fbfa74d48df4d12b2950c9f1206dab74db8bf11a Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sun, 28 Jul 2019 23:00:29 +0200 Subject: [PATCH 13/16] Revert "load library using OS-dependent names" This reverts commit 9e7d79cb65640c95a6a226a4fc88558cda866be0. --- src/Compiler/Scheme/Chez.idr | 25 ++----------------------- 1 file changed, 2 insertions(+), 23 deletions(-) diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 24f1fdb..8c894f7 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -57,28 +57,6 @@ findLibs ds then Just (trim (substr 3 (length d) d)) else Nothing -||| Generate the correct dynamic library loading code depending on the target machine -loadSharedLibs : List String -> String -loadSharedLibs [] = "" -loadSharedLibs libs = - "(case (machine-type)\n" ++ - " [(i3le ti3le a6le ta6le) " ++ load asLinux ++ "]\n" ++ - " [(i3osx ti3osx a6osx ta6osx) " ++ load asMac ++ "]\n" ++ - " [(i3nt ti3nt a6nt ta6nt) " ++ load asWin ++ "]\n" ++ - " [else " ++ load asLinux ++ "])" - where - load : (String -> String) -> String - load fmt = "(begin\n" ++ showSep "\n" (map (\ s => "(load-shared-object \"" ++ fmt s ++ "\")") libs) ++ ")\n" - - asLinux : String -> String - asLinux s = "lib" ++ s ++ ".so" - - asMac : String -> String - asMac s = "lib" ++ s ++ ".dylib" - - asWin : String -> String - asWin s = s ++ ".dll" - escapeQuotes : String -> String escapeQuotes s = pack $ foldr escape [] $ unpack s where @@ -95,7 +73,7 @@ schHeader chez libs " [(i3osx ti3osx a6osx ta6osx) (load-shared-object \"libc.dylib\")]\n" ++ " [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")]\n" ++ " [else (load-shared-object \"libc.so\")])\n\n" ++ - loadSharedLibs libs ++ "\n\n" ++ + showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeQuotes x ++ "\")") libs) ++ "\n\n" ++ "(let ()\n" schFooter : String @@ -199,3 +177,4 @@ executeExpr c tm export codegenChez : Codegen codegenChez = MkCG compileExpr executeExpr + From ec402c3c4a991f564907ad3892a9b18fcc0c9e24 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Mon, 29 Jul 2019 12:45:38 +0200 Subject: [PATCH 14/16] reference idris_net library as idris_net.so for all OSes --- libs/network/Makefile | 20 +++++++------------- libs/network/Network/Socket/Data.idr | 2 +- 2 files changed, 8 insertions(+), 14 deletions(-) diff --git a/libs/network/Makefile b/libs/network/Makefile index 9ed11cc..33e1b6a 100644 --- a/libs/network/Makefile +++ b/libs/network/Makefile @@ -14,16 +14,7 @@ else OS :=unix endif -ifeq ($(OS),darwin) - SHLIB_SUFFIX :=.dylib - LIBFLAGS :=-dynamiclib -else ifeq ($(OS),windows) - SHLIB_SUFFIX :=.DLL - LIBFLAGS :=-shared -else - SHLIB_SUFFIX :=.so - LIBFLAGS :=-shared -endif +SHLIB_SUFFIX :=.so LIBNAME=idris_net OBJS = $(LIBNAME).o @@ -35,7 +26,7 @@ ifneq ($(OS), windows) CFLAGS += -fPIC endif -DYLIBTARGET = lib$(LIBNAME)$(SHLIB_SUFFIX) +DYLIBTARGET = $(LIBNAME)$(SHLIB_SUFFIX) LIBTARGET = $(LIBNAME).a TARGET=${HOME}/.idris2 @@ -48,16 +39,19 @@ $(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 - install $(DYLIBTARGET) $(HDRS) $(TARGET)/idris2/network + @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. -l$(LIBNAME) test.c LD_LIBRARY_PATH=. ./network-tests - LD_LIBRARY_PATH=. ./lib-tests + ./lib-tests $(OBJS): $(HDRS) diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr index 4070f83..70c4f1f 100644 --- a/libs/network/Network/Socket/Data.idr +++ b/libs/network/Network/Socket/Data.idr @@ -11,7 +11,7 @@ import Data.Strings -- ------------------------------------------------------------ [ Type Aliases ] -- FIXME should be generic name with OS-dependent suffix -%cg chez "libidris_net.dylib" +%cg chez "libidris_net.so" public export ByteLength : Type From d600a3980cb143a8bb28f227ada8ee681c395f65 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Mon, 29 Jul 2019 13:15:52 +0200 Subject: [PATCH 15/16] added back missing file extension --- libs/network/Echo.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/network/Echo.idr b/libs/network/Echo.idr index d2bafc7..775385a 100644 --- a/libs/network/Echo.idr +++ b/libs/network/Echo.idr @@ -5,7 +5,7 @@ import Network.Socket import Network.Socket.Data import Network.Socket.Raw -%cg chez libidris_net +%cg chez libidris_net.so runServer : IO (Either String (Port, ThreadID)) runServer = do From f66d68189338500aac119e042b974eb2dfacfab7 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Wed, 31 Jul 2019 14:13:32 +0200 Subject: [PATCH 16/16] linked libraries should be after the source file referencing them http://gcc.gnu.org/onlinedocs/gcc/Link-Options.html --- libs/network/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/network/Makefile b/libs/network/Makefile index 33e1b6a..b63547e 100644 --- a/libs/network/Makefile +++ b/libs/network/Makefile @@ -49,7 +49,7 @@ clean : test: build test.c cp $(DYLIBTARGET) lib$(DYLIBTARGET) # to make C linker happy - $(CC) -o network-tests -L. -I. -l$(LIBNAME) test.c + $(CC) -o network-tests -L. -I. test.c -l$(LIBNAME) LD_LIBRARY_PATH=. ./network-tests ./lib-tests