Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: TCP socket support using LibUV #6683

Open
wants to merge 44 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 16 commits
Commits
Show all changes
44 commits
Select commit Hold shift + click to select a range
b875f26
feat: implement the basic libuv event loop
algebraic-dev Jan 2, 2025
7528056
doc: the event loop
hargoniX Jan 2, 2025
50cc599
fix: make the cond var safe and document it
hargoniX Jan 2, 2025
cd71bf0
feat: add async timer primitives based on libuv (#6219)
algebraic-dev Jan 6, 2025
f1e506a
feat: asynchronous timer API (#6306)
hargoniX Jan 10, 2025
c18310d
feat: start of the uv tc
algebraic-dev Jan 10, 2025
5726fcd
feat: basic tcp structure
algebraic-dev Jan 10, 2025
f376f93
Merge branch 'ft-async' of github.com:leanprover/lean4 into tcp-socket
algebraic-dev Jan 10, 2025
da8919a
feat: progress on connection
algebraic-dev Jan 14, 2025
04621bb
feat: three functions
algebraic-dev Jan 14, 2025
7a1c978
merge branch 'master' of github.com:leanprover/lean4 into tcp-socket
algebraic-dev Jan 17, 2025
260d5cb
chore: remove useless comment
algebraic-dev Jan 18, 2025
8e2fe1c
chore: remove useless modifications
algebraic-dev Jan 18, 2025
9c2e66b
feat: impl all functions
algebraic-dev Jan 23, 2025
c08d70b
fix: namespace brace
algebraic-dev Jan 23, 2025
889f9cb
fix: memory leak in accept
algebraic-dev Jan 23, 2025
cc2baa4
chore: stylistic changes
algebraic-dev Jan 23, 2025
28fe474
chore: small changes
algebraic-dev Jan 23, 2025
6e6016e
chore: remove useless print
algebraic-dev Jan 23, 2025
abf70f8
chore: comments and messages
algebraic-dev Jan 28, 2025
128aec9
chore: move things around
algebraic-dev Jan 28, 2025
4ec0f5f
Merge branch 'libuv-move' of github.com:algebraic-dev/lean4 into tcp-…
algebraic-dev Jan 29, 2025
fdd5599
fix: behavior of loop configure function
algebraic-dev Jan 29, 2025
9e39fbd
Merge branch 'libuv-move' of github.com:algebraic-dev/lean4 into tcp-…
algebraic-dev Jan 29, 2025
989f4f6
feat: high level interface and fix some memory leaks
algebraic-dev Jan 29, 2025
21f3829
feat: opt in client accept and fix some lean_dec and lean_inc
algebraic-dev Jan 30, 2025
65e3165
feat: move namespace
algebraic-dev Jan 30, 2025
05dc16a
feat: add shutdown and warning
algebraic-dev Jan 30, 2025
cefb9f0
fix: replace new with malloc
algebraic-dev Jan 30, 2025
20f04e8
chore: remove useless file
algebraic-dev Jan 30, 2025
f2a514d
feat: add buffer_size
algebraic-dev Feb 4, 2025
67800fd
fix: bug in getsockaddr
algebraic-dev Feb 4, 2025
e52e3a2
chore: add test
algebraic-dev Feb 4, 2025
e6e3ec8
fix: parametre in the timer.lean
algebraic-dev Feb 4, 2025
400d2a2
Merge branch 'libuv-move' of github.com:algebraic-dev/lean4 into tcp-…
algebraic-dev Feb 4, 2025
e55f9f0
refactor: use async monad, just to show the example
algebraic-dev Feb 4, 2025
cc8ae03
fix: lean_always_assert
algebraic-dev Feb 5, 2025
27a55f1
Merge branch 'libuv-move' of github.com:algebraic-dev/lean4 into tcp-…
algebraic-dev Feb 5, 2025
1a5dcde
fix: documentation and function signature
algebraic-dev Feb 7, 2025
061c218
fix: remove user io error
algebraic-dev Feb 7, 2025
2419b54
feat: improve async tcp interface
algebraic-dev Feb 7, 2025
ccdcda2
Merge branch 'master' of github.com:leanprover/lean4 into tcp-socket
algebraic-dev Feb 7, 2025
ff1921a
fix: remove Tcp.lean files that MacOS don't detect because of the cas…
algebraic-dev Feb 7, 2025
a577e78
fix: deprecation
algebraic-dev Feb 7, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
99 changes: 99 additions & 0 deletions src/Std/Internal/UV/Tcp.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
algebraic-dev marked this conversation as resolved.
Show resolved Hide resolved
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Boving, Sofia Rodrigues
-/
prelude
import Init.System.IO
import Init.System.Promise
import Std.Net

namespace Std
namespace Internal
namespace UV
namespace Tcp
algebraic-dev marked this conversation as resolved.
Show resolved Hide resolved

open Std.Net

private opaque SocketImpl : NonemptyType.{0}

/--
Represents a TCP socket.
-/
def Socket : Type := SocketImpl.type

instance : Nonempty Socket := SocketImpl.property

namespace Socket

/--
Creates a new TCP socket.
-/
@[extern "lean_uv_tcp_new"]
opaque new : IO Socket

/--
Connect a TCP socket to the specified address.
-/
@[extern "lean_uv_tcp_connect"]
opaque connect (socket : @& Socket) (addr : SocketAddress) : IO (IO.Promise (Except IO.Error Unit))

/--
Send data through a TCP socket.
-/
@[extern "lean_uv_tcp_send"]
opaque send (socket : @& Socket) (data : ByteArray) : IO (IO.Promise (Except IO.Error Unit))

/--
Receive data from a TCP socket.
-/
@[extern "lean_uv_tcp_recv"]
opaque recv (socket : @& Socket) : IO (IO.Promise (Except IO.Error ByteArray))

/--
Bind a TCP socket to a specific address.
-/
@[extern "lean_uv_tcp_bind"]
opaque bind (socket : @& Socket) (addr : SocketAddress) : IO Unit

/--
Start listening for incoming connections on a TCP socket.
-/
@[extern "lean_uv_tcp_listen"]
opaque listen (socket : @& Socket) (backlog : Int32) : IO Unit

/--
Accept an incoming connection on a listening TCP socket.
-/
@[extern "lean_uv_tcp_accept"]
opaque accept (socket : @& Socket) : IO (IO.Promise (Except IO.Error Socket))

/--
Get the remote address of a connected TCP socket.
-/
@[extern "lean_uv_tcp_getpeername"]
opaque getpeername (socket : @& Socket) : IO SocketAddress

/--
Get the local address of a bound TCP socket.
-/
@[extern "lean_uv_tcp_getsockname"]
opaque getsockname (socket : @& Socket) : IO SocketAddress

/--
Enable or disable the Nagle algorithm for a TCP socket.
-/
@[extern "lean_uv_tcp_nodelay"]
opaque nodelay (socket : @& Socket) : IO Unit

/--
Enable or disable TCP keep-alive for a socket.
-/
@[extern "lean_uv_tcp_keepalive"]
opaque keepalive (socket : @& Socket) (enable : Int32) (delay : UInt32) : IO Unit

end Socket
end Tcp
end UV
end Internal
end Std
2 changes: 1 addition & 1 deletion src/runtime/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp uv/event_loop.cpp
uv/timer.cpp)
uv/timer.cpp uv/tcp.cpp)
add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
set_target_properties(leanrt_initial-exec PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})
Expand Down
1 change: 1 addition & 0 deletions src/runtime/libuv.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ namespace lean {

extern "C" void initialize_libuv() {
initialize_libuv_timer();
initialize_libuv_tcp_socket();
initialize_libuv_loop();

lthread([]() { event_loop_run_loop(&global_ev); });
Expand Down
3 changes: 2 additions & 1 deletion src/runtime/libuv.h
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@ Author: Markus Himmel, Sofia Rodrigues
#pragma once
#include <lean/lean.h>
#include "runtime/uv/event_loop.h"
#include "runtime/uv/timer.h"
#include "runtime/uv/timer.h"
#include "runtime/uv/tcp.h"
#include "runtime/alloc.h"
#include "runtime/io.h"
#include "runtime/utf8.h"
Expand Down
53 changes: 53 additions & 0 deletions src/runtime/uv/net_addr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,24 @@ void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, in6_addr* out) {
}
}

extern "C" void lean_socket_addr_to_sockaddr(b_obj_arg ip_addr, struct sockaddr* out) {
lean_object * socket_addr_obj = lean_ctor_get(ip_addr, 0);
lean_object * ip_addr_obj = lean_ctor_get(socket_addr_obj, 0);
uint16_t port_obj = lean_ctor_get_uint16(socket_addr_obj, sizeof(void*)*1);

if (lean_ptr_tag(ip_addr) == 0) {
struct sockaddr_in * cast = (struct sockaddr_in*)out;
lean_ipv4_addr_to_in_addr(ip_addr_obj, &cast->sin_addr);
cast->sin_family = AF_INET;
cast->sin_port = htons(port_obj);
} else {
struct sockaddr_in6 * cast = (struct sockaddr_in6*)out;
lean_ipv6_addr_to_in6_addr(ip_addr_obj, (in6_addr*)&cast->sin6_addr);
cast->sin6_family = AF_INET6;
cast->sin6_port = htons(port_obj);
}
}

lean_obj_res lean_in_addr_to_ipv4_addr(const in_addr* ipv4_addr) {
obj_res ret = alloc_array(0, 4);
uint32_t hostaddr = ntohl(ipv4_addr->s_addr);
Expand Down Expand Up @@ -55,6 +73,41 @@ lean_obj_res lean_in6_addr_to_ipv6_addr(const in6_addr* ipv6_addr) {
return ret;
}

lean_obj_res lean_mk_socketaddress(lean_obj_res ip_addr, lean_obj_res port) {
lean_obj_res socket_addr = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(socket_addr, 0, ip_addr);
lean_ctor_set(socket_addr, 1, port);
return socket_addr;
}

lean_obj_res lean_sockaddr_to_socketaddress(const struct sockaddr* sockaddr) {
lean_object* part;
int tag;

if (sockaddr->sa_family == AF_INET) {
const struct sockaddr_in* addr_in = (const struct sockaddr_in*)sockaddr;
const in_addr* ipv4_addr = &addr_in->sin_addr;

lean_obj_res lean_ipv4 = lean_in_addr_to_ipv4_addr(ipv4_addr);
uint16_t port = ntohs(addr_in->sin_port);
part = lean_mk_socketaddress(lean_ipv4, lean_box(port));
tag = 0;
} else if (sockaddr->sa_family == AF_INET6) {
const struct sockaddr_in6* addr_in6 = (const struct sockaddr_in6*)sockaddr;
const in6_addr* ipv6_addr = &addr_in6->sin6_addr;
lean_obj_res lean_ipv6 = lean_in6_addr_to_ipv6_addr(ipv6_addr);
uint16_t port = ntohs(addr_in6->sin6_port);
part = lean_mk_socketaddress(lean_ipv6, lean_box(port));
tag = 1;
}

lean_object* ctor = lean_alloc_ctor(tag, 1, 0);
lean_ctor_set(ctor, 0, part);

return ctor;
}


/* Std.Net.IPV4Addr.ofString (s : @&String) : Option IPV4Addr */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj) {
const char* str = string_cstr(str_obj);
Expand Down
2 changes: 2 additions & 0 deletions src/runtime/uv/net_addr.h
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,10 @@ namespace lean {

void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, struct in_addr* out);
void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, struct in6_addr* out);
extern "C" void lean_socket_addr_to_sockaddr(b_obj_arg ip_addr, struct sockaddr* out);
lean_obj_res lean_in_addr_to_ipv4_addr(const struct in_addr* ipv4_addr);
lean_obj_res lean_in6_addr_to_ipv6_addr(const struct in6_addr* ipv6_addr);
lean_obj_res lean_sockaddr_to_socketaddress(const struct sockaddr* sockaddr);

#endif

Expand Down
Loading
Loading