1module Runtime.NativeMemoryRoutine
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Data.SHA256Digest
6import Runtime.NativePhysicalNative
7
8family NativeMemoryRoutineErrorCode : Type 0
9constructor NativeMemoryRoutineDuplicateLabel
10field unrestricted nativeMemoryRoutineDuplicateLabelName : Bytes
11constructor NativeMemoryRoutineOffsetOverflow
12constructor NativeMemoryRoutineMissingLabel
13field unrestricted nativeMemoryRoutineMissingLabelName : Bytes
14constructor NativeMemoryRoutineDisplacementOutOfRange
15field unrestricted nativeMemoryRoutineDistantLabelName : Bytes
16
17end-family
18
19family NativeMemoryRoutineTelemetry : Type 0
20constructor NativeMemoryRoutineTelemetryValue
21field unrestricted nativeMemoryRoutineTelemetryInstructions : Nat
22field unrestricted nativeMemoryRoutineTelemetryCodeBytes : Nat
23field unrestricted nativeMemoryRoutineTelemetryFailures : Nat
24field unrestricted nativeMemoryRoutineTelemetryFallbacks : Nat
25field unrestricted nativeMemoryRoutineTelemetryCodeSHA256 : Bytes
26field unrestricted nativeMemoryRoutineTelemetryLastError : Bytes
27
28end-family
29
30family NativeMemoryRoutine : Type 0
31constructor NativeMemoryRoutineValue
32field unrestricted nativeMemoryRoutineCode : Bytes
33field unrestricted nativeMemoryRoutineCodeSHA256 : Bytes
34field unrestricted nativeMemoryRoutineInstructionCount : Nat
35field unrestricted nativeMemoryRoutineTelemetry : (family NativeMemoryRoutineTelemetry)
36
37end-family
38
39family NativeMemoryRoutineResult : Type 0
40constructor NativeMemoryRoutineGenerated
41field unrestricted nativeMemoryGeneratedRoutine : (family NativeMemoryRoutine)
42field unrestricted nativeMemoryRoutineSuccessTelemetry : (family NativeMemoryRoutineTelemetry)
43constructor NativeMemoryRoutineGenerationFailed
44field unrestricted nativeMemoryRoutineGenerationError : (family NativeMemoryRoutineErrorCode)
45field unrestricted nativeMemoryRoutineFailureTelemetry : (family NativeMemoryRoutineTelemetry)
46
47end-family
48
49def nativeMemoryRoutineErrorCodeBytes =
50 (lambda unrestricted code : (family NativeMemoryRoutineErrorCode) .
51 (eliminate
52 NativeMemoryRoutineErrorCode
53 (lambda unrestricted current : (family NativeMemoryRoutineErrorCode) . Bytes)
54 code
55 (branch
56 NativeMemoryRoutineDuplicateLabel
57 labelName
58 .
59 (bytes-append b"ALPHA-MEM-001-" labelName))
60 (branch NativeMemoryRoutineOffsetOverflow . b"ALPHA-MEM-002")
61 (branch
62 NativeMemoryRoutineMissingLabel
63 labelName
64 .
65 (bytes-append b"ALPHA-MEM-003-" labelName))
66 (branch
67 NativeMemoryRoutineDisplacementOutOfRange
68 labelName
69 .
70 (bytes-append b"ALPHA-MEM-004-" labelName))))
71
72def nativeMemoryRoutineLabelEntry : Bytes =
73 b"mem-entry"
74
75def nativeMemoryRoutineLabelLoop : Bytes =
76 b"mem-loop"
77
78def nativeMemoryRoutineLabelDone : Bytes =
79 b"mem-done"
80
81def nativeMemoryCopyInstructionCount : Nat =
82 (byte-to-nat (byte 11))
83
84def nativeMemoryCopyAssembly : (family X86NativeAssembly) =
85 (nativePhysicalNativeLabel
86 nativeMemoryRoutineLabelEntry
87 (nativePhysicalNativeEmit
88 (nativePhysicalNativeTest
89 (constructor X86NativeRegister64 X86NativeRDX)
90 (constructor X86NativeRegister64 X86NativeRDX))
91 (nativePhysicalNativeJumpCondition
92 (constructor X86NativeCondition X86NativeConditionZero)
93 nativeMemoryRoutineLabelDone
94 (nativePhysicalNativeLabel
95 nativeMemoryRoutineLabelLoop
96 (nativePhysicalNativeEmit
97 (nativePhysicalNativeLoad8
98 (constructor X86NativeRegister64 X86NativeRAX)
99 (constructor X86NativeRegister64 X86NativeRSI)
100 nativePhysicalNativeD0)
101 (nativePhysicalNativeEmit
102 (nativePhysicalNativeStore8
103 (constructor X86NativeRegister64 X86NativeRDI)
104 nativePhysicalNativeD0
105 (constructor X86NativeRegister64 X86NativeRAX))
106 (nativePhysicalNativeEmit
107 (nativePhysicalNativeAddImmediate
108 (constructor X86NativeRegister64 X86NativeRSI)
109 (nativePhysicalNativeI32Byte (byte 1)))
110 (nativePhysicalNativeEmit
111 (nativePhysicalNativeAddImmediate
112 (constructor X86NativeRegister64 X86NativeRDI)
113 (nativePhysicalNativeI32Byte (byte 1)))
114 (nativePhysicalNativeEmit
115 (nativePhysicalNativeAddImmediate
116 (constructor X86NativeRegister64 X86NativeRDX)
117 nativePhysicalNativeI32NegativeOne)
118 (nativePhysicalNativeEmit
119 (nativePhysicalNativeTest
120 (constructor X86NativeRegister64 X86NativeRDX)
121 (constructor X86NativeRegister64 X86NativeRDX))
122 (nativePhysicalNativeJumpCondition
123 (constructor X86NativeCondition X86NativeConditionNotZero)
124 nativeMemoryRoutineLabelLoop
125 (nativePhysicalNativeLabel
126 nativeMemoryRoutineLabelDone
127 (nativePhysicalNativeEmit
128 (constructor
129 X86NativeInstruction
130 X86NativeClear32
131 (constructor X86NativeRegister64 X86NativeRAX))
132 (nativePhysicalNativeEmit
133 nativePhysicalNativeReturnInstruction
134 (constructor X86NativeAssembly X86NativeAssemblyEnd)))))))))))))))
135
136-- The shared forward copy returns zero, including for an empty region.
137-- Callers admit disjoint regions (or identical addresses), not memmove overlap.
138def nativeMemoryCopyCode : Bytes =
139 (compiler-native-encode (family X86NativeAssembly) nativeMemoryCopyAssembly)
140
141def nativeMemoryRoutineTelemetrySuccess =
142 (lambda unrestricted code : Bytes .
143 (lambda unrestricted digest : Bytes .
144 (constructor
145 NativeMemoryRoutineTelemetry
146 NativeMemoryRoutineTelemetryValue
147 nativeMemoryCopyInstructionCount
148 (bytes-length code)
149 zero
150 zero
151 digest
152 b"")))
153
154def nativeMemoryRoutineTelemetryFailure =
155 (lambda unrestricted error : (family NativeMemoryRoutineErrorCode) .
156 (constructor
157 NativeMemoryRoutineTelemetry
158 NativeMemoryRoutineTelemetryValue
159 nativeMemoryCopyInstructionCount
160 zero
161 (succ zero)
162 zero
163 b""
164 (nativeMemoryRoutineErrorCodeBytes error)))
165
166def nativeMemoryRoutineFail =
167 (lambda unrestricted error : (family NativeMemoryRoutineErrorCode) .
168 (constructor
169 NativeMemoryRoutineResult
170 NativeMemoryRoutineGenerationFailed
171 error
172 (nativeMemoryRoutineTelemetryFailure error)))
173
174-- Generation remains pure and byte-identical, but is requested by the
175-- actual lowering consumer rather than performed when this module is loaded.
176def nativeMemoryGenerateCopyRoutine :
177 (pi unrestricted request : Nat . (family NativeMemoryRoutineResult)) =
178 (lambda unrestricted request : Nat .
179 (eliminate
180 X86NativeAssemblyResult
181 (lambda unrestricted current : (family X86NativeAssemblyResult) .
182 (family NativeMemoryRoutineResult))
183 (x86NativeAssemble nativeMemoryCopyAssembly)
184 (branch
185 X86NativeAssemblyEncoded
186 code
187 .
188 (app
189 (lambda unrestricted digest : Bytes .
190 (app
191 (lambda unrestricted telemetry : (family NativeMemoryRoutineTelemetry) .
192 (constructor
193 NativeMemoryRoutineResult
194 NativeMemoryRoutineGenerated
195 (constructor
196 NativeMemoryRoutine
197 NativeMemoryRoutineValue
198 code
199 digest
200 nativeMemoryCopyInstructionCount
201 telemetry)
202 telemetry))
203 (nativeMemoryRoutineTelemetrySuccess code digest)))
204 (sha256HexBytesOrEmpty (sha256Hex code))))
205 (branch
206 X86NativeAssemblyEncodeDuplicateLabel
207 duplicateName
208 .
209 (nativeMemoryRoutineFail
210 (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineDuplicateLabel duplicateName)))
211 (branch
212 X86NativeAssemblyEncodeOffsetOverflow
213 .
214 (nativeMemoryRoutineFail
215 (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineOffsetOverflow)))
216 (branch
217 X86NativeAssemblyMissingLabel
218 missingName
219 .
220 (nativeMemoryRoutineFail
221 (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineMissingLabel missingName)))
222 (branch
223 X86NativeAssemblyDisplacementOutOfRange
224 distantName
225 .
226 (nativeMemoryRoutineFail
227 (constructor
228 NativeMemoryRoutineErrorCode
229 NativeMemoryRoutineDisplacementOutOfRange
230 distantName)))))
231
232-- Compare exactly rdx bytes at rdi/rsi, including empty buffers. Return 1 or
233-- 0, preserve callee-saved registers, and never read beyond the admitted views.
234-- This is integrity/header comparison, not a constant-time secret comparison.
235def nativeMemoryEqualAssembly : (family X86NativeAssembly) =
236 (nativePhysicalNativeEmit
237 (nativePhysicalNativeTest
238 (constructor X86NativeRegister64 X86NativeRDX)
239 (constructor X86NativeRegister64 X86NativeRDX))
240 (nativePhysicalNativeJumpCondition
241 (constructor X86NativeCondition X86NativeConditionZero)
242 b"memory-equal"
243 (nativePhysicalNativeLabel
244 b"memory-compare"
245 (nativePhysicalNativeEmit
246 (nativePhysicalNativeLoad8
247 (constructor X86NativeRegister64 X86NativeRAX)
248 (constructor X86NativeRegister64 X86NativeRDI)
249 nativePhysicalNativeD0)
250 (nativePhysicalNativeEmit
251 (nativePhysicalNativeLoad8
252 (constructor X86NativeRegister64 X86NativeRCX)
253 (constructor X86NativeRegister64 X86NativeRSI)
254 nativePhysicalNativeD0)
255 (nativePhysicalNativeEmit
256 (nativePhysicalNativeCompare
257 (constructor X86NativeRegister64 X86NativeRAX)
258 (constructor X86NativeRegister64 X86NativeRCX))
259 (nativePhysicalNativeJumpCondition
260 (constructor X86NativeCondition X86NativeConditionNotZero)
261 b"memory-different"
262 (nativePhysicalNativeEmit
263 (nativePhysicalNativeAddImmediate
264 (constructor X86NativeRegister64 X86NativeRDI)
265 (nativePhysicalNativeI32Byte (byte 1)))
266 (nativePhysicalNativeEmit
267 (nativePhysicalNativeAddImmediate
268 (constructor X86NativeRegister64 X86NativeRSI)
269 (nativePhysicalNativeI32Byte (byte 1)))
270 (nativePhysicalNativeEmit
271 (nativePhysicalNativeAddImmediate
272 (constructor X86NativeRegister64 X86NativeRDX)
273 nativePhysicalNativeI32NegativeOne)
274 (nativePhysicalNativeJumpCondition
275 (constructor X86NativeCondition X86NativeConditionNotZero)
276 b"memory-compare"
277 (nativePhysicalNativeLabel
278 b"memory-equal"
279 (nativePhysicalNativeEmit
280 (nativePhysicalNativeMoveImmediate32
281 (constructor X86NativeRegister64 X86NativeRAX)
282 (nativePhysicalNativeI32Byte (byte 1)))
283 (nativePhysicalNativeEmit
284 nativePhysicalNativeReturnInstruction
285 (nativePhysicalNativeLabel
286 b"memory-different"
287 (nativePhysicalNativeEmit
288 (constructor
289 X86NativeInstruction
290 X86NativeClear32
291 (constructor X86NativeRegister64 X86NativeRAX))
292 (nativePhysicalNativeEmit
293 nativePhysicalNativeReturnInstruction
294 (constructor X86NativeAssembly X86NativeAssemblyEnd))))))))))))))))))
295
296def nativeMemoryEqualCode =
297 (compiler-native-encode (family X86NativeAssembly) nativeMemoryEqualAssembly)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.