From a6789a73ffeeb80d6570312919e30d0e2e1caaa5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 9 Jan 2025 10:33:03 +0100 Subject: [PATCH] feat: `Std.Net.Addr` (#6563) This PR implements `Std.Net.Addr` which contains structures around IP and socket addresses. While we could implement our own parser instead of going through the `addr_in`/`addr_in6` route we will need to implement these conversions to make proper system calls anyway. Hence this is likely the approach with the least amount of non trivial code overall. The only thing I am uncertain about is whether `ofString` should return `Option` or `Except`, unfortunately `libuv` doesn't hand out error messages on IP parsing. --- src/Std.lean | 1 + src/Std/Net.lean | 7 ++ src/Std/Net/Addr.lean | 197 +++++++++++++++++++++++++++++++++++ src/runtime/CMakeLists.txt | 2 +- src/runtime/uv/net_addr.cpp | 131 +++++++++++++++++++++++ src/runtime/uv/net_addr.h | 28 +++++ tests/lean/run/net_addr.lean | 39 +++++++ 7 files changed, 404 insertions(+), 1 deletion(-) create mode 100644 src/Std/Net.lean create mode 100644 src/Std/Net/Addr.lean create mode 100644 src/runtime/uv/net_addr.cpp create mode 100644 src/runtime/uv/net_addr.h create mode 100644 tests/lean/run/net_addr.lean diff --git a/src/Std.lean b/src/Std.lean index 0a2f53c641..f427d00b8a 100644 --- a/src/Std.lean +++ b/src/Std.lean @@ -10,3 +10,4 @@ import Std.Sync import Std.Time import Std.Tactic import Std.Internal +import Std.Net diff --git a/src/Std/Net.lean b/src/Std/Net.lean new file mode 100644 index 0000000000..3d96dac348 --- /dev/null +++ b/src/Std/Net.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +prelude +import Std.Net.Addr diff --git a/src/Std/Net/Addr.lean b/src/Std/Net/Addr.lean new file mode 100644 index 0000000000..dffa107465 --- /dev/null +++ b/src/Std/Net/Addr.lean @@ -0,0 +1,197 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +prelude +import Init.Data.Vector.Basic + +/-! +This module contains Lean representations of IP and socket addresses: +- `IPv4Addr`: Representing IPv4 addresses. +- `SocketAddressV4`: Representing a pair of IPv4 address and port. +- `IPv6Addr`: Representing IPv6 addresses. +- `SocketAddressV6`: Representing a pair of IPv6 address and port. +- `IPAddr`: Can either be an `IPv4Addr` or an `IPv6Addr`. +- `SocketAddress`: Can either be a `SocketAddressV4` or `SocketAddressV6`. +-/ + +namespace Std +namespace Net + +/-- +Representation of an IPv4 address. +-/ +structure IPv4Addr where + /-- + This structure represents the address: `octets[0].octets[1].octets[2].octets[3]`. + -/ + octets : Vector UInt8 4 + deriving Inhabited, DecidableEq + +/-- +A pair of an `IPv4Addr` and a port. +-/ +structure SocketAddressV4 where + addr : IPv4Addr + port : UInt16 + deriving Inhabited, DecidableEq + +/-- +Representation of an IPv6 address. +-/ +structure IPv6Addr where + /-- + This structure represents the address: `segments[0]:segments[1]:...`. + -/ + segments : Vector UInt16 8 + deriving Inhabited, DecidableEq + +/-- +A pair of an `IPv6Addr` and a port. +-/ +structure SocketAddressV6 where + addr : IPv6Addr + port : UInt16 + deriving Inhabited, DecidableEq + +/-- +An IP address, either IPv4 or IPv6. +-/ +inductive IPAddr where + | v4 (addr : IPv4Addr) + | v6 (addr : IPv6Addr) + deriving Inhabited, DecidableEq + +/-- +Either a `SocketAddressV4` or `SocketAddressV6`. +-/ +inductive SocketAddress where + | v4 (addr : SocketAddressV4) + | v6 (addr : SocketAddressV6) + deriving Inhabited, DecidableEq + +/-- +The kinds of address families supported by Lean, currently only IP variants. +-/ +inductive AddressFamily where + | ipv4 + | ipv6 + deriving Inhabited, DecidableEq + +namespace IPv4Addr + +/-- +Build the IPv4 address `a.b.c.d`. +-/ +def ofParts (a b c d : UInt8) : IPv4Addr := + { octets := #v[a, b, c, d] } + +/-- +Try to parse `s` as an IPv4 address, returning `none` on failure. +-/ +@[extern "lean_uv_pton_v4"] +opaque ofString (s : @&String) : Option IPv4Addr + +/-- +Turn `addr` into a `String` in the usual IPv4 format. +-/ +@[extern "lean_uv_ntop_v4"] +opaque toString (addr : @&IPv4Addr) : String + +instance : ToString IPv4Addr where + toString := toString + +instance : Coe IPv4Addr IPAddr where + coe addr := .v4 addr + +end IPv4Addr + +namespace SocketAddressV4 + +instance : Coe SocketAddressV4 SocketAddress where + coe addr := .v4 addr + +end SocketAddressV4 + +namespace IPv6Addr + +/-- +Build the IPv6 address `a:b:c:d:e:f:g:h`. +-/ +def ofParts (a b c d e f g h : UInt16) : IPv6Addr := + { segments := #v[a, b, c, d, e, f, g, h] } + +/-- +Try to parse `s` as an IPv6 address according to +[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373), returning `none` on failure. +-/ +@[extern "lean_uv_pton_v6"] +opaque ofString (s : @&String) : Option IPv6Addr + +/-- +Turn `addr` into a `String` in the IPv6 format described in +[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373). +-/ +@[extern "lean_uv_ntop_v6"] +opaque toString (addr : @&IPv6Addr) : String + +instance : ToString IPv6Addr where + toString := toString + +instance : Coe IPv6Addr IPAddr where + coe addr := .v6 addr + +end IPv6Addr + +namespace SocketAddressV6 + +instance : Coe SocketAddressV6 SocketAddress where + coe addr := .v6 addr + +end SocketAddressV6 + +namespace IPAddr + +/-- +Obtain the `AddressFamily` associated with an `IPAddr`. +-/ +def family : IPAddr → AddressFamily + | .v4 .. => .ipv4 + | .v6 .. => .ipv6 + +def toString : IPAddr → String + | .v4 addr => addr.toString + | .v6 addr => addr.toString + +instance : ToString IPAddr where + toString := toString + +end IPAddr + +namespace SocketAddress + +/-- +Obtain the `AddressFamily` associated with a `SocketAddress`. +-/ +def family : SocketAddress → AddressFamily + | .v4 .. => .ipv4 + | .v6 .. => .ipv6 + +/-- +Obtain the `IPAddr` contained in a `SocketAddress`. +-/ +def ipAddr : SocketAddress → IPAddr + | .v4 sa => .v4 sa.addr + | .v6 sa => .v6 sa.addr + +/-- +Obtain the port contained in a `SocketAddress`. +-/ +def port : SocketAddress → UInt16 + | .v4 sa | .v6 sa => sa.port + +end SocketAddress + +end Net +end Std diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt index 367c7c2980..d6d8b50b39 100644 --- a/src/runtime/CMakeLists.txt +++ b/src/runtime/CMakeLists.txt @@ -2,7 +2,7 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp 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) +process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp) add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS}) set_target_properties(leanrt_initial-exec PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}) diff --git a/src/runtime/uv/net_addr.cpp b/src/runtime/uv/net_addr.cpp new file mode 100644 index 0000000000..f06a078f68 --- /dev/null +++ b/src/runtime/uv/net_addr.cpp @@ -0,0 +1,131 @@ +/* +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Henrik Böving +*/ + +#include "runtime/uv/net_addr.h" +#include + +namespace lean { + +#ifndef LEAN_EMSCRIPTEN + +void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, in_addr* out) { + out->s_addr = 0; + for (int i = 0; i < 4; i++) { + uint32_t octet = (uint32_t)(uint8_t)lean_unbox(array_uget(ipv4_addr, i)); + out->s_addr |= octet << (3 - i) * 8; + } + out->s_addr = htonl(out->s_addr); +} + +void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, in6_addr* out) { + for (int i = 0; i < 8; i++) { + uint16_t segment = htons((uint16_t)lean_unbox(array_uget(ipv6_addr, i))); + out->s6_addr[2 * i] = (uint8_t)segment; + out->s6_addr[2 * i + 1] = (uint8_t)(segment >> 8); + } +} + +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); + + for (int i = 0; i < 4; i++) { + uint8_t octet = (uint8_t)(hostaddr >> (3 - i) * 8); + array_push(ret, lean_box(octet)); + } + + lean_assert(array_size(ret) == 4); + return ret; +} + +lean_obj_res lean_in6_addr_to_ipv6_addr(const in6_addr* ipv6_addr) { + obj_res ret = alloc_array(0, 8); + + for (int i = 0; i < 16; i += 2) { + uint16_t part1 = (uint16_t)ipv6_addr->s6_addr[i]; + uint16_t part2 = (uint16_t)ipv6_addr->s6_addr[i + 1]; + uint16_t segment = ntohs((part2 << 8) | part1); + array_push(ret, lean_box(segment)); + } + + lean_assert(array_size(ret) == 8); + return ret; +} + +/* 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); + in_addr internal; + if (uv_inet_pton(AF_INET, str, &internal) == 0) { + return mk_option_some(lean_in_addr_to_ipv4_addr(&internal)); + } else { + return mk_option_none(); + } +} + +/* Std.Net.IPV4Addr.toString (addr : @&IPV4Addr) : String */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr) { + in_addr internal; + lean_ipv4_addr_to_in_addr(ipv4_addr, &internal); + char dst[INET_ADDRSTRLEN]; + int ret = uv_inet_ntop(AF_INET, &internal, dst, sizeof(dst)); + lean_always_assert(ret == 0); + return lean_mk_string(dst); +} + +/* Std.Net.IPV6Addr.ofString (s : @&String) : Option IPV6Addr */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj) { + const char* str = string_cstr(str_obj); + in6_addr internal; + if (uv_inet_pton(AF_INET6, str, &internal) == 0) { + return mk_option_some(lean_in6_addr_to_ipv6_addr(&internal)); + } else { + return mk_option_none(); + } +} + +/* Std.Net.IPV6Addr.toString (addr : @&IPV6Addr) : String */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) { + in6_addr internal; + lean_ipv6_addr_to_in6_addr(ipv6_addr, &internal); + char dst[INET6_ADDRSTRLEN]; + int ret = uv_inet_ntop(AF_INET6, &internal, dst, sizeof(dst)); + lean_always_assert(ret == 0); + return lean_mk_string(dst); +} + +#else + +/* Std.Net.IPV4Addr.ofString (s : @&String) : Option IPV4Addr */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +/* Std.Net.IPV4Addr.toString (addr : @&IPV4Addr) : String */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +/* Std.Net.IPV6Addr.ofString (s : @&String) : Option IPV6Addr */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +/* Std.Net.IPV6Addr.toString (addr : @&IPV6Addr) : String */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +#endif +} diff --git a/src/runtime/uv/net_addr.h b/src/runtime/uv/net_addr.h new file mode 100644 index 0000000000..2d6783beb5 --- /dev/null +++ b/src/runtime/uv/net_addr.h @@ -0,0 +1,28 @@ +/* +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Henrik Böving +*/ +#pragma once +#include +#include "runtime/object.h" + + +namespace lean { + +#ifndef LEAN_EMSCRIPTEN +#include + +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); +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); + +#endif + +extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr); + +} diff --git a/tests/lean/run/net_addr.lean b/tests/lean/run/net_addr.lean new file mode 100644 index 0000000000..5503e88031 --- /dev/null +++ b/tests/lean/run/net_addr.lean @@ -0,0 +1,39 @@ +import Std.Net.Addr + +open Std.Net + +/-- info: true -/ +#guard_msgs in +#eval (IPv4Addr.ofParts 192 168 178 120).toString == "192.168.178.120" + +/-- info: true -/ +#guard_msgs in +#eval (IPv4Addr.ofParts 1 2 3 4).toString == "1.2.3.4" + +/-- info: true -/ +#guard_msgs in +#eval (IPv6Addr.ofParts 0xdead 0xbeef 0 0 0 0 0 0).toString == "dead:beef::" + +/-- info: true -/ +#guard_msgs in +#eval (IPv6Addr.ofParts 0x1234 0x5678 0x9abc 0xdef1 0x4321 0x8765 0xcba9 0x1fed).toString == "1234:5678:9abc:def1:4321:8765:cba9:1fed" + +/-- info: true -/ +#guard_msgs in +#eval IPv4Addr.ofString "1.2.3.4" == some (IPv4Addr.ofParts 1 2 3 4) + +/-- info: true -/ +#guard_msgs in +#eval IPv4Addr.ofString "192.168.300.120" |>.isNone + +/-- info: true -/ +#guard_msgs in +#eval IPv6Addr.ofString "dead:beef::" == some (IPv6Addr.ofParts 0xdead 0xbeef 0 0 0 0 0 0) + +/-- info: true -/ +#guard_msgs in +#eval IPv6Addr.ofString "1234:5678:9abc:def1:4321:8765:cba9:1fed" == some (IPv6Addr.ofParts 0x1234 0x5678 0x9abc 0xdef1 0x4321 0x8765 0xcba9 0x1fed) + +/-- info: true -/ +#guard_msgs in +#eval IPv6Addr.ofString "dead:beef::badaddress" |>.isNone