1module Runtime.NativeSocketRoutine
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Runtime.NativePhysicalNative
6import Data.Bytes
7import Model.Word64
8import Std.Natural
9
10-- Linux x86-64 connected SOCK_STREAM transport. The caller owns a valid
11-- buffer of extent bytes and one endpoint for the duration of this call.
12-- ABI: rdi=fd, rsi=buffer, rdx=extent, rcx=poll timeout milliseconds,
13-- r8=maximum poll/IO attempts. Return extent or a negative Linux errno.
14-- A partial failure NEVER authorizes consumption or retry from the beginning:
15-- abandon this edge/session; the caller must discard partial destination data.
16--
17-- Each attempt consumes budget, including EINTR/EAGAIN and partial progress.
18-- Poll is bounded, and MSG_DONTWAIT prevents readiness races from blocking.
19-- This bounds syscall attempts/wait intervals, not scheduler delay or a global
20-- monotonic deadline. MSG_NOSIGNAL makes a broken send a returned error.
21-- Sources: Linux man-pages recv(2), send(2), poll(2) (man7.org, 2026-10-02);
22-- Linux x86-64 syscall ABI asm/unistd_64.h. No libc/vendor runtime is called.
23-- These are platform facts; a different host ABI needs its own realization.
24--
25-- Preserve all SysV callee-saved registers used by the enclosing native VM.
26-- Stack offsets belong to this layout; each follows the preceding field.
27def nativeSocketWordBytes =
28 (bytes-length (dataBytesWord64LE (modelWord64FromNaturalTruncated 0)))
29
30def nativeSocketSaveRBX : Nat =
31 0
32
33def nativeSocketSaveRBP : Nat =
34 (naturalAdd nativeSocketSaveRBX nativeSocketWordBytes)
35
36def nativeSocketSaveR12 : Nat =
37 (naturalAdd nativeSocketSaveRBP nativeSocketWordBytes)
38
39def nativeSocketSaveR13 : Nat =
40 (naturalAdd nativeSocketSaveR12 nativeSocketWordBytes)
41
42def nativeSocketSaveR14 : Nat =
43 (naturalAdd nativeSocketSaveR13 nativeSocketWordBytes)
44
45def nativeSocketSaveR15 : Nat =
46 (naturalAdd nativeSocketSaveR14 nativeSocketWordBytes)
47
48def nativeSocketPollSlot =
49 (naturalAdd nativeSocketSaveR15 nativeSocketWordBytes)
50
51def nativeSocketPollFdBytes : Nat =
52 4
53
54def nativeSocketPollEventsBytes : Nat =
55 2
56
57def nativeSocketPollReturnedBytes : Nat =
58 2
59
60def nativeSocketPollEventsSlot =
61 (naturalAdd nativeSocketPollSlot nativeSocketPollFdBytes)
62
63def nativeSocketStackBytes =
64 (naturalAdd
65 nativeSocketPollSlot
66 (naturalAdd
67 nativeSocketPollFdBytes
68 (naturalAdd nativeSocketPollEventsBytes nativeSocketPollReturnedBytes)))
69
70def nativeSocketImmediate =
71 x86NativeImmediate32FromNatural
72
73def nativeSocketDisplacement =
74 x86NativeDisplacement32FromNatural
75
76def nativeSocketEntry =
77 (lambda unrestricted tail : (family X86NativeAssembly) .
78 (nativePhysicalNativeEmit
79 (nativePhysicalNativeAddImmediate
80 (constructor X86NativeRegister64 X86NativeRSP)
81 (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 nativeSocketStackBytes)))
82 (nativePhysicalNativeEmit
83 (nativePhysicalNativeStore64
84 (constructor X86NativeRegister64 X86NativeRSP)
85 (nativeSocketDisplacement nativeSocketSaveRBX)
86 (constructor X86NativeRegister64 X86NativeRBX))
87 (nativePhysicalNativeEmit
88 (nativePhysicalNativeStore64
89 (constructor X86NativeRegister64 X86NativeRSP)
90 (nativeSocketDisplacement nativeSocketSaveRBP)
91 (constructor X86NativeRegister64 X86NativeRBP))
92 (nativePhysicalNativeEmit
93 (nativePhysicalNativeStore64
94 (constructor X86NativeRegister64 X86NativeRSP)
95 (nativeSocketDisplacement nativeSocketSaveR12)
96 (constructor X86NativeRegister64 X86NativeR12))
97 (nativePhysicalNativeEmit
98 (nativePhysicalNativeStore64
99 (constructor X86NativeRegister64 X86NativeRSP)
100 (nativeSocketDisplacement nativeSocketSaveR13)
101 (constructor X86NativeRegister64 X86NativeR13))
102 (nativePhysicalNativeEmit
103 (nativePhysicalNativeStore64
104 (constructor X86NativeRegister64 X86NativeRSP)
105 (nativeSocketDisplacement nativeSocketSaveR14)
106 (constructor X86NativeRegister64 X86NativeR14))
107 (nativePhysicalNativeEmit
108 (nativePhysicalNativeStore64
109 (constructor X86NativeRegister64 X86NativeRSP)
110 (nativeSocketDisplacement nativeSocketSaveR15)
111 (constructor X86NativeRegister64 X86NativeR15))
112 (nativePhysicalNativeEmit
113 (nativePhysicalNativeMove
114 (constructor X86NativeRegister64 X86NativeRDI)
115 (constructor X86NativeRegister64 X86NativeRBX))
116 (nativePhysicalNativeEmit
117 (nativePhysicalNativeMove
118 (constructor X86NativeRegister64 X86NativeRSI)
119 (constructor X86NativeRegister64 X86NativeR12))
120 (nativePhysicalNativeEmit
121 (nativePhysicalNativeMove
122 (constructor X86NativeRegister64 X86NativeRDX)
123 (constructor X86NativeRegister64 X86NativeR13))
124 (nativePhysicalNativeEmit
125 (nativePhysicalNativeMove
126 (constructor X86NativeRegister64 X86NativeRDX)
127 (constructor X86NativeRegister64 X86NativeRBP))
128 (nativePhysicalNativeEmit
129 (nativePhysicalNativeMove
130 (constructor X86NativeRegister64 X86NativeRCX)
131 (constructor X86NativeRegister64 X86NativeR14))
132 (nativePhysicalNativeEmit
133 (nativePhysicalNativeMove
134 (constructor X86NativeRegister64 X86NativeR8)
135 (constructor X86NativeRegister64 X86NativeR15))
136 (nativePhysicalNativeEmit
137 (nativePhysicalNativeCompareImmediate
138 (constructor X86NativeRegister64 X86NativeRBX)
139 (nativeSocketImmediate 2147483647))
140 (nativePhysicalNativeJumpCondition
141 (constructor X86NativeCondition X86NativeConditionAbove)
142 b"socket-invalid"
143 (nativePhysicalNativeEmit
144 (nativePhysicalNativeCompareImmediate
145 (constructor X86NativeRegister64 X86NativeR14)
146 (nativeSocketImmediate 2147483647))
147 (nativePhysicalNativeJumpCondition
148 (constructor X86NativeCondition X86NativeConditionAbove)
149 b"socket-invalid"
150 (nativePhysicalNativeEmit
151 (nativePhysicalNativeTest
152 (constructor X86NativeRegister64 X86NativeR13)
153 (constructor X86NativeRegister64 X86NativeR13))
154 (nativePhysicalNativeJumpCondition
155 (constructor X86NativeCondition X86NativeConditionSign)
156 b"socket-invalid"
157 (nativePhysicalNativeEmit
158 (nativePhysicalNativeMove
159 (constructor X86NativeRegister64 X86NativeR12)
160 (constructor X86NativeRegister64 X86NativeRAX))
161 (nativePhysicalNativeEmit
162 (nativePhysicalNativeAdd
163 (constructor X86NativeRegister64 X86NativeR13)
164 (constructor X86NativeRegister64 X86NativeRAX))
165 (nativePhysicalNativeJumpCondition
166 (constructor X86NativeCondition X86NativeConditionBelow)
167 b"socket-invalid"
168 tail)))))))))))))))))))))))
169
170def nativeSocketPoll =
171 (lambda unrestricted events : Nat .
172 (lambda unrestricted tail : (family X86NativeAssembly) .
173 (nativePhysicalNativeLabel
174 b"socket-loop"
175 (nativePhysicalNativeEmit
176 (nativePhysicalNativeTest
177 (constructor X86NativeRegister64 X86NativeR13)
178 (constructor X86NativeRegister64 X86NativeR13))
179 (nativePhysicalNativeJumpCondition
180 (constructor X86NativeCondition X86NativeConditionZero)
181 b"socket-success"
182 (nativePhysicalNativeEmit
183 (nativePhysicalNativeTest
184 (constructor X86NativeRegister64 X86NativeR15)
185 (constructor X86NativeRegister64 X86NativeR15))
186 (nativePhysicalNativeJumpCondition
187 (constructor X86NativeCondition X86NativeConditionZero)
188 b"socket-timeout"
189 (nativePhysicalNativeEmit
190 (nativePhysicalNativeAddImmediate
191 (constructor X86NativeRegister64 X86NativeR15)
192 (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 1)))
193 (nativePhysicalNativeEmit
194 (nativePhysicalNativeStore64
195 (constructor X86NativeRegister64 X86NativeRSP)
196 (nativeSocketDisplacement nativeSocketPollSlot)
197 (constructor X86NativeRegister64 X86NativeRBX))
198 (nativePhysicalNativeEmit
199 (nativePhysicalNativeMoveImmediate32
200 (constructor X86NativeRegister64 X86NativeRAX)
201 (nativeSocketImmediate events))
202 (nativePhysicalNativeEmit
203 (nativePhysicalNativeStore8
204 (constructor X86NativeRegister64 X86NativeRSP)
205 (nativeSocketDisplacement nativeSocketPollEventsSlot)
206 (constructor X86NativeRegister64 X86NativeRAX))
207 (nativePhysicalNativeEmit
208 (nativePhysicalNativeMove
209 (constructor X86NativeRegister64 X86NativeRSP)
210 (constructor X86NativeRegister64 X86NativeRDI))
211 (nativePhysicalNativeEmit
212 (nativePhysicalNativeAddImmediate
213 (constructor X86NativeRegister64 X86NativeRDI)
214 (nativeSocketImmediate nativeSocketPollSlot))
215 (nativePhysicalNativeEmit
216 (nativePhysicalNativeMoveImmediate32
217 (constructor X86NativeRegister64 X86NativeRSI)
218 (nativeSocketImmediate 1))
219 (nativePhysicalNativeEmit
220 (nativePhysicalNativeMove
221 (constructor X86NativeRegister64 X86NativeR14)
222 (constructor X86NativeRegister64 X86NativeRDX))
223 (nativePhysicalNativeEmit
224 (nativePhysicalNativeMoveImmediate32
225 (constructor X86NativeRegister64 X86NativeRAX)
226 (nativeSocketImmediate 7))
227 (nativePhysicalNativeEmit
228 nativePhysicalNativeSystemCallInstruction
229 (nativePhysicalNativeEmit
230 (nativePhysicalNativeCompareImmediate
231 (constructor X86NativeRegister64 X86NativeRAX)
232 (nativeSocketImmediate
233 (naturalSaturatingSubtract 4294967296 4)))
234 (nativePhysicalNativeJumpCondition
235 (constructor X86NativeCondition X86NativeConditionZero)
236 b"socket-loop"
237 (nativePhysicalNativeEmit
238 (nativePhysicalNativeTest
239 (constructor X86NativeRegister64 X86NativeRAX)
240 (constructor X86NativeRegister64 X86NativeRAX))
241 (nativePhysicalNativeJumpCondition
242 (constructor X86NativeCondition X86NativeConditionSign)
243 b"socket-return"
244 (nativePhysicalNativeJumpCondition
245 (constructor X86NativeCondition X86NativeConditionZero)
246 b"socket-timeout"
247 tail))))))))))))))))))))))
248
249def nativeSocketIO =
250 (lambda unrestricted flags : Nat .
251 (lambda unrestricted syscallNumber : Nat .
252 (lambda unrestricted tail : (family X86NativeAssembly) .
253 (nativePhysicalNativeEmit
254 (nativePhysicalNativeMove
255 (constructor X86NativeRegister64 X86NativeRBX)
256 (constructor X86NativeRegister64 X86NativeRDI))
257 (nativePhysicalNativeEmit
258 (nativePhysicalNativeMove
259 (constructor X86NativeRegister64 X86NativeR12)
260 (constructor X86NativeRegister64 X86NativeRSI))
261 (nativePhysicalNativeEmit
262 (nativePhysicalNativeMove
263 (constructor X86NativeRegister64 X86NativeR13)
264 (constructor X86NativeRegister64 X86NativeRDX))
265 (nativePhysicalNativeEmit
266 (nativePhysicalNativeMoveImmediate32
267 (constructor X86NativeRegister64 X86NativeR10)
268 (nativeSocketImmediate flags))
269 (nativePhysicalNativeEmit
270 (constructor
271 X86NativeInstruction
272 X86NativeClear32
273 (constructor X86NativeRegister64 X86NativeR8))
274 (nativePhysicalNativeEmit
275 (constructor
276 X86NativeInstruction
277 X86NativeClear32
278 (constructor X86NativeRegister64 X86NativeR9))
279 (nativePhysicalNativeEmit
280 (nativePhysicalNativeMoveImmediate32
281 (constructor X86NativeRegister64 X86NativeRAX)
282 (nativeSocketImmediate syscallNumber))
283 (nativePhysicalNativeEmit
284 nativePhysicalNativeSystemCallInstruction
285 (nativePhysicalNativeEmit
286 (nativePhysicalNativeCompareImmediate
287 (constructor X86NativeRegister64 X86NativeRAX)
288 (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 4)))
289 (nativePhysicalNativeJumpCondition
290 (constructor X86NativeCondition X86NativeConditionZero)
291 b"socket-loop"
292 (nativePhysicalNativeEmit
293 (nativePhysicalNativeCompareImmediate
294 (constructor X86NativeRegister64 X86NativeRAX)
295 (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 11)))
296 (nativePhysicalNativeJumpCondition
297 (constructor X86NativeCondition X86NativeConditionZero)
298 b"socket-loop"
299 (nativePhysicalNativeEmit
300 (nativePhysicalNativeTest
301 (constructor X86NativeRegister64 X86NativeRAX)
302 (constructor X86NativeRegister64 X86NativeRAX))
303 (nativePhysicalNativeJumpCondition
304 (constructor X86NativeCondition X86NativeConditionSign)
305 b"socket-return"
306 (nativePhysicalNativeJumpCondition
307 (constructor X86NativeCondition X86NativeConditionZero)
308 b"socket-eof"
309 (nativePhysicalNativeEmit
310 (nativePhysicalNativeCompare
311 (constructor X86NativeRegister64 X86NativeR13)
312 (constructor X86NativeRegister64 X86NativeRAX))
313 (nativePhysicalNativeJumpCondition
314 (constructor X86NativeCondition X86NativeConditionAbove)
315 b"socket-invalid"
316 (nativePhysicalNativeEmit
317 (nativePhysicalNativeAdd
318 (constructor X86NativeRegister64 X86NativeRAX)
319 (constructor X86NativeRegister64 X86NativeR12))
320 (nativePhysicalNativeEmit
321 (nativePhysicalNativeSubtract
322 (constructor X86NativeRegister64 X86NativeRAX)
323 (constructor X86NativeRegister64 X86NativeR13))
324 (nativePhysicalNativeJump b"socket-loop" tail)))))))))))))))))))))))
325
326def nativeSocketReturn =
327 (lambda unrestricted tail : (family X86NativeAssembly) .
328 (nativePhysicalNativeLabel
329 b"socket-invalid"
330 (nativePhysicalNativeEmit
331 (constructor
332 X86NativeInstruction
333 X86NativeClear32
334 (constructor X86NativeRegister64 X86NativeRAX))
335 (nativePhysicalNativeEmit
336 (nativePhysicalNativeAddImmediate
337 (constructor X86NativeRegister64 X86NativeRAX)
338 (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 22)))
339 (nativePhysicalNativeJump
340 b"socket-return"
341 (nativePhysicalNativeLabel
342 b"socket-timeout"
343 (nativePhysicalNativeEmit
344 (constructor
345 X86NativeInstruction
346 X86NativeClear32
347 (constructor X86NativeRegister64 X86NativeRAX))
348 (nativePhysicalNativeEmit
349 (nativePhysicalNativeAddImmediate
350 (constructor X86NativeRegister64 X86NativeRAX)
351 (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 110)))
352 (nativePhysicalNativeJump
353 b"socket-return"
354 (nativePhysicalNativeLabel
355 b"socket-eof"
356 (nativePhysicalNativeEmit
357 (constructor
358 X86NativeInstruction
359 X86NativeClear32
360 (constructor X86NativeRegister64 X86NativeRAX))
361 (nativePhysicalNativeEmit
362 (nativePhysicalNativeAddImmediate
363 (constructor X86NativeRegister64 X86NativeRAX)
364 (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 61)))
365 (nativePhysicalNativeJump
366 b"socket-return"
367 (nativePhysicalNativeLabel
368 b"socket-success"
369 (nativePhysicalNativeEmit
370 (nativePhysicalNativeMove
371 (constructor X86NativeRegister64 X86NativeRBP)
372 (constructor X86NativeRegister64 X86NativeRAX))
373 (nativePhysicalNativeLabel
374 b"socket-return"
375 (nativePhysicalNativeEmit
376 (nativePhysicalNativeLoad64
377 (constructor X86NativeRegister64 X86NativeRBX)
378 (constructor X86NativeRegister64 X86NativeRSP)
379 (nativeSocketDisplacement nativeSocketSaveRBX))
380 (nativePhysicalNativeEmit
381 (nativePhysicalNativeLoad64
382 (constructor X86NativeRegister64 X86NativeRBP)
383 (constructor X86NativeRegister64 X86NativeRSP)
384 (nativeSocketDisplacement nativeSocketSaveRBP))
385 (nativePhysicalNativeEmit
386 (nativePhysicalNativeLoad64
387 (constructor X86NativeRegister64 X86NativeR12)
388 (constructor X86NativeRegister64 X86NativeRSP)
389 (nativeSocketDisplacement nativeSocketSaveR12))
390 (nativePhysicalNativeEmit
391 (nativePhysicalNativeLoad64
392 (constructor X86NativeRegister64 X86NativeR13)
393 (constructor X86NativeRegister64 X86NativeRSP)
394 (nativeSocketDisplacement nativeSocketSaveR13))
395 (nativePhysicalNativeEmit
396 (nativePhysicalNativeLoad64
397 (constructor X86NativeRegister64 X86NativeR14)
398 (constructor X86NativeRegister64 X86NativeRSP)
399 (nativeSocketDisplacement nativeSocketSaveR14))
400 (nativePhysicalNativeEmit
401 (nativePhysicalNativeLoad64
402 (constructor X86NativeRegister64 X86NativeR15)
403 (constructor X86NativeRegister64 X86NativeRSP)
404 (nativeSocketDisplacement nativeSocketSaveR15))
405 (nativePhysicalNativeEmit
406 (nativePhysicalNativeAddImmediate
407 (constructor X86NativeRegister64 X86NativeRSP)
408 (nativeSocketImmediate nativeSocketStackBytes))
409 (nativePhysicalNativeEmit
410 nativePhysicalNativeReturnInstruction
411 tail))))))))))))))))))))))))
412
413-- ADD's signed imm32 produces the full negative 64-bit errno; MOV r32 would
414-- zero-extend it and turn our synthetic failures into positive byte counts.
415def nativeSocketReadAssembly =
416 (nativeSocketEntry
417 (nativeSocketPoll
418 1
419 (nativeSocketIO
420 64
421 45
422 (nativeSocketReturn (constructor X86NativeAssembly X86NativeAssemblyEnd)))))
423
424def nativeSocketWriteAssembly =
425 (nativeSocketEntry
426 (nativeSocketPoll
427 4
428 (nativeSocketIO
429 (naturalAdd 64 16384)
430 44
431 (nativeSocketReturn (constructor X86NativeAssembly X86NativeAssemblyEnd)))))
432
433def nativeSocketReadCode =
434 (compiler-native-encode (family X86NativeAssembly) nativeSocketReadAssembly)
435
436def nativeSocketWriteCode =
437 (compiler-native-encode (family X86NativeAssembly) nativeSocketWriteAssembly)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.