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
136def nativeMemoryRoutineTelemetrySuccess =
137 (lambda unrestricted code : Bytes .
138 (lambda unrestricted digest : Bytes .
139 (constructor
140 NativeMemoryRoutineTelemetry
141 NativeMemoryRoutineTelemetryValue
142 nativeMemoryCopyInstructionCount
143 (bytes-length code)
144 zero
145 zero
146 digest
147 b"")))
148
149def nativeMemoryRoutineTelemetryFailure =
150 (lambda unrestricted error : (family NativeMemoryRoutineErrorCode) .
151 (constructor
152 NativeMemoryRoutineTelemetry
153 NativeMemoryRoutineTelemetryValue
154 nativeMemoryCopyInstructionCount
155 zero
156 (succ zero)
157 zero
158 b""
159 (nativeMemoryRoutineErrorCodeBytes error)))
160
161def nativeMemoryRoutineFail =
162 (lambda unrestricted error : (family NativeMemoryRoutineErrorCode) .
163 (constructor
164 NativeMemoryRoutineResult
165 NativeMemoryRoutineGenerationFailed
166 error
167 (nativeMemoryRoutineTelemetryFailure error)))
168
169-- Generation remains pure and byte-identical, but is requested by the
170-- actual lowering consumer rather than performed when this module is loaded.
171def nativeMemoryGenerateCopyRoutine :
172 (pi unrestricted request : Nat . (family NativeMemoryRoutineResult)) =
173 (lambda unrestricted request : Nat .
174 (eliminate
175 X86NativeAssemblyResult
176 (lambda unrestricted current : (family X86NativeAssemblyResult) .
177 (family NativeMemoryRoutineResult))
178 (x86NativeAssemble nativeMemoryCopyAssembly)
179 (branch
180 X86NativeAssemblyEncoded
181 code
182 .
183 (app
184 (lambda unrestricted digest : Bytes .
185 (app
186 (lambda unrestricted telemetry : (family NativeMemoryRoutineTelemetry) .
187 (constructor
188 NativeMemoryRoutineResult
189 NativeMemoryRoutineGenerated
190 (constructor
191 NativeMemoryRoutine
192 NativeMemoryRoutineValue
193 code
194 digest
195 nativeMemoryCopyInstructionCount
196 telemetry)
197 telemetry))
198 (nativeMemoryRoutineTelemetrySuccess code digest)))
199 (sha256HexBytesOrEmpty (sha256Hex code))))
200 (branch
201 X86NativeAssemblyEncodeDuplicateLabel
202 duplicateName
203 .
204 (nativeMemoryRoutineFail
205 (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineDuplicateLabel duplicateName)))
206 (branch
207 X86NativeAssemblyEncodeOffsetOverflow
208 .
209 (nativeMemoryRoutineFail
210 (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineOffsetOverflow)))
211 (branch
212 X86NativeAssemblyMissingLabel
213 missingName
214 .
215 (nativeMemoryRoutineFail
216 (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineMissingLabel missingName)))
217 (branch
218 X86NativeAssemblyDisplacementOutOfRange
219 distantName
220 .
221 (nativeMemoryRoutineFail
222 (constructor
223 NativeMemoryRoutineErrorCode
224 NativeMemoryRoutineDisplacementOutOfRange
225 distantName)))))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.