1module Platform.AArch64.SocketRoutine
2
3import Compiler.MachineAArch64
4import Compiler.MachineAArch64Assembly
5import Platform.AArch64.RoutineEmitter
6import Runtime.NativeSocketEndpoint
7import Model.Word64
8import Data.Bytes
9import Std.List
10import Std.Natural
11
12-- Linux AArch64 realization of Runtime.NativeSocketRoutine's bounded connected
13-- stream contract and Runtime.NativeSocketEndpoint's connect/accept contract.
14-- x0 fd, x1 admitted buffer (or address), x2 count (or address extent), x3
15-- timeout milliseconds, x4 attempt budget. Stream IO returns the exact count;
16-- connect returns zero; accept returns an owned nonblocking close-on-exec
17-- descriptor. Every failure is a negative Linux errno. Partial failure
18-- requires abandoning the stream and discarding the destination; a failed
19-- connect never retries the indeterminate socket.
20--
21-- The routines share one structure with the x86-64 owners, piece by piece:
22-- entry validation, an optional nonblocking check, the bounded readiness
23-- loop, the operation-specific ready step, and one return block. Keeping the
24-- pieces in that order is what lets each routine be read against its x86-64
25-- twin; the operation semantics, errno classification and attempt budget are
26-- the same contract on both hosts, only the instructions and ABI differ.
27--
28-- Each poll/IO attempt consumes budget, including EINTR/EAGAIN and partial
29-- progress. ppoll uses a fresh timespec on every attempt because the raw Linux
30-- syscall can modify it. MSG_DONTWAIT avoids blocking after a readiness race;
31-- MSG_NOSIGNAL converts a broken send into an error. The bound is on waits and
32-- attempts, not elapsed scheduler delay or a global monotonic deadline.
33--
34-- Platform facts: Linux asm-generic/unistd.h (fcntl 25, ppoll 73, connect 203,
35-- sendto 206, recvfrom 207, getsockopt 209, accept4 242), asm-generic/fcntl.h
36-- (F_GETFL 3, O_NONBLOCK 0x800, O_CLOEXEC 0x80000 -- the values x86-64 also
37-- uses), asm-generic/socket.h (SOL_SOCKET 1, SO_ERROR 4), asm-generic/errno.h
38-- (the errno numbers are shared with x86-64), Linux pollfd/timespec UAPI and
39-- the AAPCS64 register/stack convention.
40-- https://github.com/torvalds/linux/blob/master/include/uapi/asm-generic/unistd.h
41-- https://man7.org/linux/man-pages/man2/poll.2.html
42-- https://man7.org/linux/man-pages/man2/recv.2.html
43-- https://man7.org/linux/man-pages/man2/send.2.html
44-- https://man7.org/linux/man-pages/man2/connect.2.html
45-- https://man7.org/linux/man-pages/man2/accept.2.html
46-- Persistent state uses x9-x15, preserved by Linux syscall return; x18 and
47-- callee-saved x19-x29 are untouched. The VM saves its volatile x12-x15 at
48-- the shared routine-call boundary. No BL is used, so x30 remains the caller's
49-- return address. The private frame stays aligned to the AAPCS64 16-byte rule.
50-- Register roles: x9 fd, x10 buffer cursor, x11 remaining count, x12 original
51-- count, x13 timeout (then its nanoseconds), x14 timeout seconds, x15 attempts;
52-- x6 is scratch, x16/x17 belong to Platform.AArch64.RoutineEmitter.
53def aarch64SocketWordBytes =
54 (bytes-length (dataBytesWord64LE (modelWord64FromNaturalTruncated 0)))
55
56def aarch64SocketPollAt : Nat =
57 0
58
59def aarch64SocketPollFdBytes : Nat =
60 4
61
62def aarch64SocketPollEventsBytes : Nat =
63 2
64
65def aarch64SocketPollReturnedBytes : Nat =
66 2
67
68def aarch64SocketEventsAt =
69 (naturalAdd aarch64SocketPollAt aarch64SocketPollFdBytes)
70
71def aarch64SocketTimeAt =
72 (naturalAdd
73 aarch64SocketEventsAt
74 (naturalAdd aarch64SocketPollEventsBytes aarch64SocketPollReturnedBytes))
75
76def aarch64SocketNanosAt =
77 (naturalAdd aarch64SocketTimeAt aarch64SocketWordBytes)
78
79def aarch64SocketStackBytes =
80 (naturalMultiply
81 16
82 (naturalDivideUnchecked
83 (naturalAdd 15 (naturalAdd aarch64SocketNanosAt aarch64SocketWordBytes))
84 16))
85
86-- After readiness the pollfd storage is no longer live. Connect reuses it as
87-- SO_ERROR (int, at the pollfd's fd field) followed by its socklen_t (at the
88-- events/revents pair): both views occupy exactly the eight pollfd bytes, as
89-- on x86-64.
90def aarch64SocketErrorAt =
91 aarch64SocketPollAt
92
93def aarch64SocketErrorLengthAt =
94 aarch64SocketEventsAt
95
96-- A negative errno compared as the sign-extended 32-bit immediate the
97-- emitter's ahrCmpImm materializes.
98def aarch64SocketNegated =
99 (lambda unrestricted errno : Nat . (naturalSaturatingSubtract 4294967296 errno))
100
101def aarch64SocketReturnIfNegative =
102 (lambda unrestricted tail : (family AArch64Assembly) .
103 (ahrCmpImm ahrX0 0 (ahrBranchIf (constructor AArch64Condition AArch64Minus) b"return" tail)))
104
105def aarch64SocketRetryOn =
106 (lambda unrestricted errno : Nat .
107 (lambda unrestricted tail : (family AArch64Assembly) .
108 (ahrCmpImm
109 ahrX0
110 (aarch64SocketNegated errno)
111 (ahrBranchIf (constructor AArch64Condition AArch64Equal) b"loop" tail))))
112
113def aarch64SocketSystemCall =
114 (lambda unrestricted number : Nat .
115 (lambda unrestricted tail : (family AArch64Assembly) .
116 (ahrMovImm ahrX8 number (ahrEmit (constructor AArch64Instruction AArch64SupervisorCall) tail))))
117
118def aarch64SocketStackAddress =
119 (lambda unrestricted destination : (family AArch64Register) .
120 (lambda unrestricted at : Nat .
121 (ahrEmit (constructor AArch64Instruction AArch64AddImmediateFromStackPointer destination at))))
122
123-- Validate the caller's operands before any system call: fd and timeout fit
124-- a Linux int, the count is not negative and buffer+count does not wrap. The
125-- timeout is converted once into the timespec ppoll needs on every attempt.
126def aarch64SocketEntry =
127 (lambda unrestricted tail : (family AArch64Assembly) .
128 (ahrEmit
129 (constructor
130 AArch64Instruction
131 AArch64SubtractStackPointer
132 aarch64SocketStackBytes
133 (constructor AArch64ImmediateShift AArch64Unshifted))
134 (ahrMov
135 ahrX9
136 ahrX0
137 (ahrMov
138 ahrX10
139 ahrX1
140 (ahrMov
141 ahrX11
142 ahrX2
143 (ahrMov
144 ahrX12
145 ahrX2
146 (ahrMov
147 ahrX13
148 ahrX3
149 (ahrMov
150 ahrX15
151 ahrX4
152 (ahrCmpImm
153 ahrX9
154 2147483647
155 (ahrBranchIf
156 (constructor AArch64Condition AArch64UnsignedHigher)
157 b"invalid"
158 (ahrCmpImm
159 ahrX13
160 2147483647
161 (ahrBranchIf
162 (constructor AArch64Condition AArch64UnsignedHigher)
163 b"invalid"
164 (ahrCmpImm
165 ahrX11
166 0
167 (ahrBranchIf
168 (constructor AArch64Condition AArch64Minus)
169 b"invalid"
170 (ahrEmit
171 (constructor
172 AArch64Instruction
173 AArch64AddRegister
174 ahrX6
175 ahrX10
176 ahrX11)
177 (ahrEmit
178 (constructor
179 AArch64Instruction
180 AArch64CompareRegister
181 ahrX6
182 ahrX10)
183 (ahrBranchIf
184 (constructor AArch64Condition AArch64CarryClear)
185 b"invalid"
186 (ahrMovImm
187 ahrX6
188 1000
189 (ahrEmit
190 (constructor
191 AArch64Instruction
192 AArch64DivideRegisterUnsigned
193 ahrX14
194 ahrX13
195 ahrX6)
196 (ahrEmit
197 (constructor
198 AArch64Instruction
199 AArch64MultiplyRegister
200 ahrX6
201 ahrX14
202 ahrX6)
203 (ahrEmit
204 (constructor
205 AArch64Instruction
206 AArch64SubtractRegister
207 ahrX13
208 ahrX13
209 ahrX6)
210 (ahrMovImm
211 ahrX6
212 1000000
213 (ahrEmit
214 (constructor
215 AArch64Instruction
216 AArch64MultiplyRegister
217 ahrX13
218 ahrX13
219 ahrX6)
220 tail)))))))))))))))))))))))
221
222-- The bounded readiness loop. A zero remaining count is success, an exhausted
223-- budget or a ppoll timeout is ETIMEDOUT, EINTR consumes an attempt and polls
224-- again, and any other failure returns. Readiness falls through to tail.
225def aarch64SocketPoll =
226 (lambda unrestricted events : Nat .
227 (lambda unrestricted tail : (family AArch64Assembly) .
228 (ahrLabel
229 b"loop"
230 (ahrCmpImm
231 ahrX11
232 0
233 (ahrBranchIf
234 (constructor AArch64Condition AArch64Equal)
235 b"success"
236 (ahrCmpImm
237 ahrX15
238 0
239 (ahrBranchIf
240 (constructor AArch64Condition AArch64Equal)
241 b"timeout"
242 (ahrEmit
243 (constructor AArch64Instruction AArch64SubtractImmediate ahrX15 ahrX15 1)
244 (ahrEmit
245 (constructor
246 AArch64Instruction
247 AArch64StoreMemory64ToStack
248 aarch64SocketPollAt
249 ahrX9)
250 (ahrMovImm
251 ahrX6
252 events
253 (ahrEmit
254 (constructor
255 AArch64Instruction
256 AArch64StoreMemory8ToStack
257 aarch64SocketEventsAt
258 ahrX6)
259 (ahrEmit
260 (constructor
261 AArch64Instruction
262 AArch64StoreMemory64ToStack
263 aarch64SocketTimeAt
264 ahrX14)
265 (ahrEmit
266 (constructor
267 AArch64Instruction
268 AArch64StoreMemory64ToStack
269 aarch64SocketNanosAt
270 ahrX13)
271 (aarch64SocketStackAddress
272 ahrX0
273 aarch64SocketPollAt
274 (ahrMovImm
275 ahrX1
276 1
277 (aarch64SocketStackAddress
278 ahrX2
279 aarch64SocketTimeAt
280 (ahrMovImm
281 ahrX3
282 0
283 (ahrMovImm
284 ahrX4
285 0
286 (aarch64SocketSystemCall
287 73
288 (aarch64SocketRetryOn
289 4
290 (aarch64SocketReturnIfNegative
291 (ahrBranchIf
292 (constructor AArch64Condition AArch64Equal)
293 b"timeout"
294 tail))))))))))))))))))))))
295
296-- One stream transfer after readiness. EINTR/EAGAIN retry through the loop;
297-- zero is end-of-stream; a count above the remainder is refused.
298def aarch64SocketIO =
299 (lambda unrestricted flags : Nat .
300 (lambda unrestricted syscallNumber : Nat .
301 (lambda unrestricted tail : (family AArch64Assembly) .
302 (ahrMov
303 ahrX0
304 ahrX9
305 (ahrMov
306 ahrX1
307 ahrX10
308 (ahrMov
309 ahrX2
310 ahrX11
311 (ahrMovImm
312 ahrX3
313 flags
314 (ahrMovImm
315 ahrX4
316 0
317 (ahrMovImm
318 ahrX5
319 0
320 (aarch64SocketSystemCall
321 syscallNumber
322 (aarch64SocketRetryOn
323 4
324 (aarch64SocketRetryOn
325 11
326 (aarch64SocketReturnIfNegative
327 (ahrBranchIf
328 (constructor AArch64Condition AArch64Equal)
329 b"eof"
330 (ahrEmit
331 (constructor AArch64Instruction AArch64CompareRegister ahrX0 ahrX11)
332 (ahrBranchIf
333 (constructor AArch64Condition AArch64UnsignedHigher)
334 b"invalid"
335 (ahrEmit
336 (constructor
337 AArch64Instruction
338 AArch64AddRegister
339 ahrX10
340 ahrX10
341 ahrX0)
342 (ahrEmit
343 (constructor
344 AArch64Instruction
345 AArch64SubtractRegister
346 ahrX11
347 ahrX11
348 ahrX0)
349 (ahrBranch b"loop" tail)))))))))))))))))))
350
351-- Endpoint operations require a nonblocking descriptor before anything that
352-- could otherwise block: F_GETFL must succeed and report O_NONBLOCK.
353def aarch64SocketRequireNonblocking =
354 (lambda unrestricted tail : (family AArch64Assembly) .
355 (ahrMov
356 ahrX0
357 ahrX9
358 (ahrMovImm
359 ahrX1
360 3
361 (aarch64SocketSystemCall
362 25
363 (aarch64SocketReturnIfNegative
364 (ahrAndImm
365 ahrX0
366 nativeSocketNonblock
367 (ahrCmpImm
368 ahrX0
369 0
370 (ahrBranchIf (constructor AArch64Condition AArch64Equal) b"invalid" tail))))))))
371
372def aarch64SocketRetryOnInProgress =
373 (lambda unrestricted tail : (family AArch64Assembly) .
374 (ahrCmpImm
375 ahrX0
376 (aarch64SocketNegated 115)
377 (ahrBranchIf (constructor AArch64Condition AArch64Equal) b"loop" tail)))
378
379-- Initiate once; only EINPROGRESS waits for writability. Immediate success
380-- returns zero and every other result returns unchanged.
381def aarch64SocketConnectStart =
382 (lambda unrestricted tail : (family AArch64Assembly) .
383 (ahrMov
384 ahrX0
385 ahrX9
386 (ahrMov
387 ahrX1
388 ahrX10
389 (ahrMov
390 ahrX2
391 ahrX11
392 (aarch64SocketSystemCall
393 203
394 (ahrCmpImm
395 ahrX0
396 0
397 (ahrBranchIf
398 (constructor AArch64Condition AArch64Equal)
399 b"return"
400 (aarch64SocketRetryOnInProgress (ahrBranch b"return" tail)))))))))
401
402-- Writability includes refusal. Read the full int SO_ERROR with its length,
403-- refuse an unexpected length, and return the negated socket error (zero when
404-- the connection was established).
405def aarch64SocketReadConnectStatus =
406 (lambda unrestricted tail : (family AArch64Assembly) .
407 (ahrMovImm
408 ahrX6
409 0
410 (aarch64SocketStackAddress
411 ahrX16
412 aarch64SocketErrorAt
413 (ahrEmit
414 (constructor AArch64Instruction AArch64StoreMemory32 ahrX16 0 ahrX6)
415 (ahrMovImm
416 ahrX6
417 aarch64SocketPollFdBytes
418 (aarch64SocketStackAddress
419 ahrX16
420 aarch64SocketErrorLengthAt
421 (ahrEmit
422 (constructor AArch64Instruction AArch64StoreMemory32 ahrX16 0 ahrX6)
423 (ahrMov
424 ahrX0
425 ahrX9
426 (ahrMovImm
427 ahrX1
428 1
429 (ahrMovImm
430 ahrX2
431 4
432 (aarch64SocketStackAddress
433 ahrX3
434 aarch64SocketErrorAt
435 (aarch64SocketStackAddress
436 ahrX4
437 aarch64SocketErrorLengthAt
438 (aarch64SocketSystemCall
439 209
440 (aarch64SocketRetryOn
441 4
442 (aarch64SocketReturnIfNegative
443 (aarch64SocketStackAddress
444 ahrX16
445 aarch64SocketErrorLengthAt
446 (ahrEmit
447 (constructor
448 AArch64Instruction
449 AArch64LoadMemory32ZeroExtend
450 ahrX6
451 ahrX16
452 0)
453 (ahrCmpImm
454 ahrX6
455 aarch64SocketPollFdBytes
456 (ahrBranchIf
457 (constructor AArch64Condition AArch64NotEqual)
458 b"invalid"
459 (aarch64SocketStackAddress
460 ahrX16
461 aarch64SocketErrorAt
462 (ahrEmit
463 (constructor
464 AArch64Instruction
465 AArch64LoadMemory32ZeroExtend
466 ahrX6
467 ahrX16
468 0)
469 (ahrMovImm
470 ahrX0
471 0
472 (ahrEmit
473 (constructor
474 AArch64Instruction
475 AArch64SubtractRegister
476 ahrX0
477 ahrX0
478 ahrX6)
479 (ahrBranch b"return" tail))))))))))))))))))))))))
480
481-- accept4 after readiness. The transient classes the x86-64 owner retries
482-- (Runtime.NativeSocketEndpoint.nativeSocketAcceptTransientErrors) retry here
483-- in the same order; everything else, including a new descriptor, returns.
484def aarch64SocketAcceptReady =
485 (lambda unrestricted tail : (family AArch64Assembly) .
486 (ahrMov
487 ahrX0
488 ahrX9
489 (ahrMovImm
490 ahrX1
491 0
492 (ahrMovImm
493 ahrX2
494 0
495 (ahrMovImm
496 ahrX3
497 nativeSocketEndpointFlags
498 (aarch64SocketSystemCall
499 242
500 (stdListFold
501 Nat
502 (family AArch64Assembly)
503 aarch64SocketRetryOn
504 (ahrBranch b"return" tail)
505 nativeSocketAcceptTransientErrors)))))))
506
507def aarch64SocketReturn : (family AArch64Assembly) =
508 (ahrLabel
509 b"invalid"
510 (ahrSignedImm
511 ahrX0
512 (aarch64SocketNegated 22)
513 (ahrBranch
514 b"return"
515 (ahrLabel
516 b"timeout"
517 (ahrSignedImm
518 ahrX0
519 (aarch64SocketNegated 110)
520 (ahrBranch
521 b"return"
522 (ahrLabel
523 b"eof"
524 (ahrSignedImm
525 ahrX0
526 (aarch64SocketNegated 61)
527 (ahrBranch
528 b"return"
529 (ahrLabel
530 b"success"
531 (ahrMov
532 ahrX0
533 ahrX12
534 (ahrLabel
535 b"return"
536 (ahrEmit
537 (constructor
538 AArch64Instruction
539 AArch64AddStackPointer
540 aarch64SocketStackBytes
541 (constructor AArch64ImmediateShift AArch64Unshifted))
542 (ahrReturn ahrEnd))))))))))))))
543
544def aarch64SocketStreamAssembly =
545 (lambda unrestricted events : Nat .
546 (lambda unrestricted flags : Nat .
547 (lambda unrestricted syscallNumber : Nat .
548 (aarch64SocketEntry
549 (aarch64SocketPoll events (aarch64SocketIO flags syscallNumber aarch64SocketReturn))))))
550
551def aarch64SocketReadCode =
552 (aarch64RoutineBytes (aarch64SocketStreamAssembly 1 64 207))
553
554def aarch64SocketWriteCode =
555 (aarch64RoutineBytes (aarch64SocketStreamAssembly 4 (naturalAdd 64 16384) 206))
556
557def aarch64SocketConnectAssembly =
558 (aarch64SocketEntry
559 (aarch64SocketRequireNonblocking
560 (aarch64SocketConnectStart
561 (aarch64SocketPoll 4 (aarch64SocketReadConnectStatus aarch64SocketReturn)))))
562
563def aarch64SocketAcceptAssembly =
564 (aarch64SocketEntry
565 (aarch64SocketRequireNonblocking
566 (aarch64SocketPoll 1 (aarch64SocketAcceptReady aarch64SocketReturn))))
567
568def aarch64SocketConnectCode =
569 (aarch64RoutineBytes aarch64SocketConnectAssembly)
570
571def aarch64SocketAcceptCode =
572 (aarch64RoutineBytes aarch64SocketAcceptAssembly)The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.