module Platform.AArch64.SocketRoutine import Compiler.MachineAArch64 import Compiler.MachineAArch64Assembly import Platform.AArch64.RoutineEmitter import Runtime.NativeSocketEndpoint import Model.Word64 import Data.Bytes import Std.List import Std.Natural -- Linux AArch64 realization of Runtime.NativeSocketRoutine's bounded connected -- stream contract and Runtime.NativeSocketEndpoint's connect/accept contract. -- x0 fd, x1 admitted buffer (or address), x2 count (or address extent), x3 -- timeout milliseconds, x4 attempt budget. Stream IO returns the exact count; -- connect returns zero; accept returns an owned nonblocking close-on-exec -- descriptor. Every failure is a negative Linux errno. Partial failure -- requires abandoning the stream and discarding the destination; a failed -- connect never retries the indeterminate socket. -- -- The routines share one structure with the x86-64 owners, piece by piece: -- entry validation, an optional nonblocking check, the bounded readiness -- loop, the operation-specific ready step, and one return block. Keeping the -- pieces in that order is what lets each routine be read against its x86-64 -- twin; the operation semantics, errno classification and attempt budget are -- the same contract on both hosts, only the instructions and ABI differ. -- -- Each poll/IO attempt consumes budget, including EINTR/EAGAIN and partial -- progress. ppoll uses a fresh timespec on every attempt because the raw Linux -- syscall can modify it. MSG_DONTWAIT avoids blocking after a readiness race; -- MSG_NOSIGNAL converts a broken send into an error. The bound is on waits and -- attempts, not elapsed scheduler delay or a global monotonic deadline. -- -- Platform facts: Linux asm-generic/unistd.h (fcntl 25, ppoll 73, connect 203, -- sendto 206, recvfrom 207, getsockopt 209, accept4 242), asm-generic/fcntl.h -- (F_GETFL 3, O_NONBLOCK 0x800, O_CLOEXEC 0x80000 -- the values x86-64 also -- uses), asm-generic/socket.h (SOL_SOCKET 1, SO_ERROR 4), asm-generic/errno.h -- (the errno numbers are shared with x86-64), Linux pollfd/timespec UAPI and -- the AAPCS64 register/stack convention. -- https://github.com/torvalds/linux/blob/master/include/uapi/asm-generic/unistd.h -- https://man7.org/linux/man-pages/man2/poll.2.html -- https://man7.org/linux/man-pages/man2/recv.2.html -- https://man7.org/linux/man-pages/man2/send.2.html -- https://man7.org/linux/man-pages/man2/connect.2.html -- https://man7.org/linux/man-pages/man2/accept.2.html -- Persistent state uses x9-x15, preserved by Linux syscall return; x18 and -- callee-saved x19-x29 are untouched. The VM saves its volatile x12-x15 at -- the shared routine-call boundary. No BL is used, so x30 remains the caller's -- return address. The private frame stays aligned to the AAPCS64 16-byte rule. -- Register roles: x9 fd, x10 buffer cursor, x11 remaining count, x12 original -- count, x13 timeout (then its nanoseconds), x14 timeout seconds, x15 attempts; -- x6 is scratch, x16/x17 belong to Platform.AArch64.RoutineEmitter. def aarch64SocketWordBytes = (bytes-length (dataBytesWord64LE (modelWord64FromNaturalTruncated 0))) def aarch64SocketPollAt : Nat = 0 def aarch64SocketPollFdBytes : Nat = 4 def aarch64SocketPollEventsBytes : Nat = 2 def aarch64SocketPollReturnedBytes : Nat = 2 def aarch64SocketEventsAt = (naturalAdd aarch64SocketPollAt aarch64SocketPollFdBytes) def aarch64SocketTimeAt = (naturalAdd aarch64SocketEventsAt (naturalAdd aarch64SocketPollEventsBytes aarch64SocketPollReturnedBytes)) def aarch64SocketNanosAt = (naturalAdd aarch64SocketTimeAt aarch64SocketWordBytes) def aarch64SocketStackBytes = (naturalMultiply 16 (naturalDivideUnchecked (naturalAdd 15 (naturalAdd aarch64SocketNanosAt aarch64SocketWordBytes)) 16)) -- After readiness the pollfd storage is no longer live. Connect reuses it as -- SO_ERROR (int, at the pollfd's fd field) followed by its socklen_t (at the -- events/revents pair): both views occupy exactly the eight pollfd bytes, as -- on x86-64. def aarch64SocketErrorAt = aarch64SocketPollAt def aarch64SocketErrorLengthAt = aarch64SocketEventsAt -- A negative errno compared as the sign-extended 32-bit immediate the -- emitter's ahrCmpImm materializes. def aarch64SocketNegated = (lambda unrestricted errno : Nat . (naturalSaturatingSubtract 4294967296 errno)) def aarch64SocketReturnIfNegative = (lambda unrestricted tail : (family AArch64Assembly) . (ahrCmpImm ahrX0 0 (ahrBranchIf (constructor AArch64Condition AArch64Minus) b"return" tail))) def aarch64SocketRetryOn = (lambda unrestricted errno : Nat . (lambda unrestricted tail : (family AArch64Assembly) . (ahrCmpImm ahrX0 (aarch64SocketNegated errno) (ahrBranchIf (constructor AArch64Condition AArch64Equal) b"loop" tail)))) def aarch64SocketSystemCall = (lambda unrestricted number : Nat . (lambda unrestricted tail : (family AArch64Assembly) . (ahrMovImm ahrX8 number (ahrEmit (constructor AArch64Instruction AArch64SupervisorCall) tail)))) def aarch64SocketStackAddress = (lambda unrestricted destination : (family AArch64Register) . (lambda unrestricted at : Nat . (ahrEmit (constructor AArch64Instruction AArch64AddImmediateFromStackPointer destination at)))) -- Validate the caller's operands before any system call: fd and timeout fit -- a Linux int, the count is not negative and buffer+count does not wrap. The -- timeout is converted once into the timespec ppoll needs on every attempt. def aarch64SocketEntry = (lambda unrestricted tail : (family AArch64Assembly) . (ahrEmit (constructor AArch64Instruction AArch64SubtractStackPointer aarch64SocketStackBytes (constructor AArch64ImmediateShift AArch64Unshifted)) (ahrMov ahrX9 ahrX0 (ahrMov ahrX10 ahrX1 (ahrMov ahrX11 ahrX2 (ahrMov ahrX12 ahrX2 (ahrMov ahrX13 ahrX3 (ahrMov ahrX15 ahrX4 (ahrCmpImm ahrX9 2147483647 (ahrBranchIf (constructor AArch64Condition AArch64UnsignedHigher) b"invalid" (ahrCmpImm ahrX13 2147483647 (ahrBranchIf (constructor AArch64Condition AArch64UnsignedHigher) b"invalid" (ahrCmpImm ahrX11 0 (ahrBranchIf (constructor AArch64Condition AArch64Minus) b"invalid" (ahrEmit (constructor AArch64Instruction AArch64AddRegister ahrX6 ahrX10 ahrX11) (ahrEmit (constructor AArch64Instruction AArch64CompareRegister ahrX6 ahrX10) (ahrBranchIf (constructor AArch64Condition AArch64CarryClear) b"invalid" (ahrMovImm ahrX6 1000 (ahrEmit (constructor AArch64Instruction AArch64DivideRegisterUnsigned ahrX14 ahrX13 ahrX6) (ahrEmit (constructor AArch64Instruction AArch64MultiplyRegister ahrX6 ahrX14 ahrX6) (ahrEmit (constructor AArch64Instruction AArch64SubtractRegister ahrX13 ahrX13 ahrX6) (ahrMovImm ahrX6 1000000 (ahrEmit (constructor AArch64Instruction AArch64MultiplyRegister ahrX13 ahrX13 ahrX6) tail))))))))))))))))))))))) -- The bounded readiness loop. A zero remaining count is success, an exhausted -- budget or a ppoll timeout is ETIMEDOUT, EINTR consumes an attempt and polls -- again, and any other failure returns. Readiness falls through to tail. def aarch64SocketPoll = (lambda unrestricted events : Nat . (lambda unrestricted tail : (family AArch64Assembly) . (ahrLabel b"loop" (ahrCmpImm ahrX11 0 (ahrBranchIf (constructor AArch64Condition AArch64Equal) b"success" (ahrCmpImm ahrX15 0 (ahrBranchIf (constructor AArch64Condition AArch64Equal) b"timeout" (ahrEmit (constructor AArch64Instruction AArch64SubtractImmediate ahrX15 ahrX15 1) (ahrEmit (constructor AArch64Instruction AArch64StoreMemory64ToStack aarch64SocketPollAt ahrX9) (ahrMovImm ahrX6 events (ahrEmit (constructor AArch64Instruction AArch64StoreMemory8ToStack aarch64SocketEventsAt ahrX6) (ahrEmit (constructor AArch64Instruction AArch64StoreMemory64ToStack aarch64SocketTimeAt ahrX14) (ahrEmit (constructor AArch64Instruction AArch64StoreMemory64ToStack aarch64SocketNanosAt ahrX13) (aarch64SocketStackAddress ahrX0 aarch64SocketPollAt (ahrMovImm ahrX1 1 (aarch64SocketStackAddress ahrX2 aarch64SocketTimeAt (ahrMovImm ahrX3 0 (ahrMovImm ahrX4 0 (aarch64SocketSystemCall 73 (aarch64SocketRetryOn 4 (aarch64SocketReturnIfNegative (ahrBranchIf (constructor AArch64Condition AArch64Equal) b"timeout" tail)))))))))))))))))))))) -- One stream transfer after readiness. EINTR/EAGAIN retry through the loop; -- zero is end-of-stream; a count above the remainder is refused. def aarch64SocketIO = (lambda unrestricted flags : Nat . (lambda unrestricted syscallNumber : Nat . (lambda unrestricted tail : (family AArch64Assembly) . (ahrMov ahrX0 ahrX9 (ahrMov ahrX1 ahrX10 (ahrMov ahrX2 ahrX11 (ahrMovImm ahrX3 flags (ahrMovImm ahrX4 0 (ahrMovImm ahrX5 0 (aarch64SocketSystemCall syscallNumber (aarch64SocketRetryOn 4 (aarch64SocketRetryOn 11 (aarch64SocketReturnIfNegative (ahrBranchIf (constructor AArch64Condition AArch64Equal) b"eof" (ahrEmit (constructor AArch64Instruction AArch64CompareRegister ahrX0 ahrX11) (ahrBranchIf (constructor AArch64Condition AArch64UnsignedHigher) b"invalid" (ahrEmit (constructor AArch64Instruction AArch64AddRegister ahrX10 ahrX10 ahrX0) (ahrEmit (constructor AArch64Instruction AArch64SubtractRegister ahrX11 ahrX11 ahrX0) (ahrBranch b"loop" tail))))))))))))))))))) -- Endpoint operations require a nonblocking descriptor before anything that -- could otherwise block: F_GETFL must succeed and report O_NONBLOCK. def aarch64SocketRequireNonblocking = (lambda unrestricted tail : (family AArch64Assembly) . (ahrMov ahrX0 ahrX9 (ahrMovImm ahrX1 3 (aarch64SocketSystemCall 25 (aarch64SocketReturnIfNegative (ahrAndImm ahrX0 nativeSocketNonblock (ahrCmpImm ahrX0 0 (ahrBranchIf (constructor AArch64Condition AArch64Equal) b"invalid" tail)))))))) def aarch64SocketRetryOnInProgress = (lambda unrestricted tail : (family AArch64Assembly) . (ahrCmpImm ahrX0 (aarch64SocketNegated 115) (ahrBranchIf (constructor AArch64Condition AArch64Equal) b"loop" tail))) -- Initiate once; only EINPROGRESS waits for writability. Immediate success -- returns zero and every other result returns unchanged. def aarch64SocketConnectStart = (lambda unrestricted tail : (family AArch64Assembly) . (ahrMov ahrX0 ahrX9 (ahrMov ahrX1 ahrX10 (ahrMov ahrX2 ahrX11 (aarch64SocketSystemCall 203 (ahrCmpImm ahrX0 0 (ahrBranchIf (constructor AArch64Condition AArch64Equal) b"return" (aarch64SocketRetryOnInProgress (ahrBranch b"return" tail))))))))) -- Writability includes refusal. Read the full int SO_ERROR with its length, -- refuse an unexpected length, and return the negated socket error (zero when -- the connection was established). def aarch64SocketReadConnectStatus = (lambda unrestricted tail : (family AArch64Assembly) . (ahrMovImm ahrX6 0 (aarch64SocketStackAddress ahrX16 aarch64SocketErrorAt (ahrEmit (constructor AArch64Instruction AArch64StoreMemory32 ahrX16 0 ahrX6) (ahrMovImm ahrX6 aarch64SocketPollFdBytes (aarch64SocketStackAddress ahrX16 aarch64SocketErrorLengthAt (ahrEmit (constructor AArch64Instruction AArch64StoreMemory32 ahrX16 0 ahrX6) (ahrMov ahrX0 ahrX9 (ahrMovImm ahrX1 1 (ahrMovImm ahrX2 4 (aarch64SocketStackAddress ahrX3 aarch64SocketErrorAt (aarch64SocketStackAddress ahrX4 aarch64SocketErrorLengthAt (aarch64SocketSystemCall 209 (aarch64SocketRetryOn 4 (aarch64SocketReturnIfNegative (aarch64SocketStackAddress ahrX16 aarch64SocketErrorLengthAt (ahrEmit (constructor AArch64Instruction AArch64LoadMemory32ZeroExtend ahrX6 ahrX16 0) (ahrCmpImm ahrX6 aarch64SocketPollFdBytes (ahrBranchIf (constructor AArch64Condition AArch64NotEqual) b"invalid" (aarch64SocketStackAddress ahrX16 aarch64SocketErrorAt (ahrEmit (constructor AArch64Instruction AArch64LoadMemory32ZeroExtend ahrX6 ahrX16 0) (ahrMovImm ahrX0 0 (ahrEmit (constructor AArch64Instruction AArch64SubtractRegister ahrX0 ahrX0 ahrX6) (ahrBranch b"return" tail)))))))))))))))))))))))) -- accept4 after readiness. The transient classes the x86-64 owner retries -- (Runtime.NativeSocketEndpoint.nativeSocketAcceptTransientErrors) retry here -- in the same order; everything else, including a new descriptor, returns. def aarch64SocketAcceptReady = (lambda unrestricted tail : (family AArch64Assembly) . (ahrMov ahrX0 ahrX9 (ahrMovImm ahrX1 0 (ahrMovImm ahrX2 0 (ahrMovImm ahrX3 nativeSocketEndpointFlags (aarch64SocketSystemCall 242 (stdListFold Nat (family AArch64Assembly) aarch64SocketRetryOn (ahrBranch b"return" tail) nativeSocketAcceptTransientErrors))))))) def aarch64SocketReturn : (family AArch64Assembly) = (ahrLabel b"invalid" (ahrSignedImm ahrX0 (aarch64SocketNegated 22) (ahrBranch b"return" (ahrLabel b"timeout" (ahrSignedImm ahrX0 (aarch64SocketNegated 110) (ahrBranch b"return" (ahrLabel b"eof" (ahrSignedImm ahrX0 (aarch64SocketNegated 61) (ahrBranch b"return" (ahrLabel b"success" (ahrMov ahrX0 ahrX12 (ahrLabel b"return" (ahrEmit (constructor AArch64Instruction AArch64AddStackPointer aarch64SocketStackBytes (constructor AArch64ImmediateShift AArch64Unshifted)) (ahrReturn ahrEnd)))))))))))))) def aarch64SocketStreamAssembly = (lambda unrestricted events : Nat . (lambda unrestricted flags : Nat . (lambda unrestricted syscallNumber : Nat . (aarch64SocketEntry (aarch64SocketPoll events (aarch64SocketIO flags syscallNumber aarch64SocketReturn)))))) def aarch64SocketReadCode = (aarch64RoutineBytes (aarch64SocketStreamAssembly 1 64 207)) def aarch64SocketWriteCode = (aarch64RoutineBytes (aarch64SocketStreamAssembly 4 (naturalAdd 64 16384) 206)) def aarch64SocketConnectAssembly = (aarch64SocketEntry (aarch64SocketRequireNonblocking (aarch64SocketConnectStart (aarch64SocketPoll 4 (aarch64SocketReadConnectStatus aarch64SocketReturn))))) def aarch64SocketAcceptAssembly = (aarch64SocketEntry (aarch64SocketRequireNonblocking (aarch64SocketPoll 1 (aarch64SocketAcceptReady aarch64SocketReturn)))) def aarch64SocketConnectCode = (aarch64RoutineBytes aarch64SocketConnectAssembly) def aarch64SocketAcceptCode = (aarch64RoutineBytes aarch64SocketAcceptAssembly)