1module Runtime.NativeWordDigest
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Runtime.WordDigest
6import Std.Natural
7
8-- Shared x86-64 instruction selection for block hashing and its consumers.
9def digestImm32 =
10 x86NativeImmediate32FromNatural
11
12def digestDisp =
13 x86NativeDisplacement32FromNatural
14
15def digestImm8 =
16 (lambda unrestricted n : Nat .
17 (constructor X86NativeImmediate8 X86NativeImmediate8Value (nat-to-byte n)))
18
19def digestRAX =
20 (constructor X86NativeRegister64 X86NativeRAX)
21
22def digestRBX =
23 (constructor X86NativeRegister64 X86NativeRBX)
24
25def digestRCX =
26 (constructor X86NativeRegister64 X86NativeRCX)
27
28def digestRDX =
29 (constructor X86NativeRegister64 X86NativeRDX)
30
31def digestRSI =
32 (constructor X86NativeRegister64 X86NativeRSI)
33
34def digestRDI =
35 (constructor X86NativeRegister64 X86NativeRDI)
36
37def digestRBP =
38 (constructor X86NativeRegister64 X86NativeRBP)
39
40def digestR8 =
41 (constructor X86NativeRegister64 X86NativeR8)
42
43def digestR9 =
44 (constructor X86NativeRegister64 X86NativeR9)
45
46def digestR10 =
47 (constructor X86NativeRegister64 X86NativeR10)
48
49def digestR11 =
50 (constructor X86NativeRegister64 X86NativeR11)
51
52def digestR12 =
53 (constructor X86NativeRegister64 X86NativeR12)
54
55def digestR13 =
56 (constructor X86NativeRegister64 X86NativeR13)
57
58def digestR14 =
59 (constructor X86NativeRegister64 X86NativeR14)
60
61def digestR15 =
62 (constructor X86NativeRegister64 X86NativeR15)
63
64def digestEmit =
65 (lambda unrestricted instruction : (family X86NativeInstruction) .
66 (lambda unrestricted rest : (family X86NativeAssembly) .
67 (constructor X86NativeAssembly X86NativeAssemblyEmit instruction rest)))
68
69def digestLoad32 =
70 (lambda unrestricted d : (family X86NativeRegister64) .
71 (lambda unrestricted base : (family X86NativeRegister64) .
72 (lambda unrestricted at : Nat .
73 (digestEmit
74 (constructor
75 X86NativeInstruction
76 X86NativeLoadMemory32ZeroExtend64
77 d
78 base
79 (digestDisp at))))))
80
81def digestLoad64 =
82 (lambda unrestricted d : (family X86NativeRegister64) .
83 (lambda unrestricted base : (family X86NativeRegister64) .
84 (lambda unrestricted at : Nat .
85 (digestEmit (constructor X86NativeInstruction X86NativeLoadMemory64 d base (digestDisp at))))))
86
87def digestLoad8 =
88 (lambda unrestricted d : (family X86NativeRegister64) .
89 (lambda unrestricted base : (family X86NativeRegister64) .
90 (lambda unrestricted at : Nat .
91 (digestEmit
92 (constructor X86NativeInstruction X86NativeLoadMemory8ZeroExtend64 d base (digestDisp at))))))
93
94def digestStore32 =
95 (lambda unrestricted base : (family X86NativeRegister64) .
96 (lambda unrestricted at : Nat .
97 (lambda unrestricted s : (family X86NativeRegister64) .
98 (digestEmit
99 (constructor X86NativeInstruction X86NativeStoreMemory32 base (digestDisp at) s)))))
100
101def digestStore64 =
102 (lambda unrestricted base : (family X86NativeRegister64) .
103 (lambda unrestricted at : Nat .
104 (lambda unrestricted s : (family X86NativeRegister64) .
105 (digestEmit
106 (constructor X86NativeInstruction X86NativeStoreMemory64 base (digestDisp at) s)))))
107
108def digestStore8 =
109 (lambda unrestricted base : (family X86NativeRegister64) .
110 (lambda unrestricted at : Nat .
111 (lambda unrestricted s : (family X86NativeRegister64) .
112 (digestEmit (constructor X86NativeInstruction X86NativeStoreMemory8 base (digestDisp at) s)))))
113
114def digestMov =
115 (lambda unrestricted d : (family X86NativeRegister64) .
116 (lambda unrestricted s : (family X86NativeRegister64) .
117 (digestEmit (constructor X86NativeInstruction X86NativeMoveRegister64 s d))))
118
119def digestAdd =
120 (lambda unrestricted d : (family X86NativeRegister64) .
121 (lambda unrestricted s : (family X86NativeRegister64) .
122 (digestEmit (constructor X86NativeInstruction X86NativeAddRegister64 s d))))
123
124def digestAnd =
125 (lambda unrestricted d : (family X86NativeRegister64) .
126 (lambda unrestricted s : (family X86NativeRegister64) .
127 (digestEmit (constructor X86NativeInstruction X86NativeAndRegister64 s d))))
128
129def digestOr =
130 (lambda unrestricted d : (family X86NativeRegister64) .
131 (lambda unrestricted s : (family X86NativeRegister64) .
132 (digestEmit (constructor X86NativeInstruction X86NativeOrRegister64 s d))))
133
134def digestXor =
135 (lambda unrestricted d : (family X86NativeRegister64) .
136 (lambda unrestricted s : (family X86NativeRegister64) .
137 (digestEmit (constructor X86NativeInstruction X86NativeXorRegister64 s d))))
138
139def digestShl =
140 (lambda unrestricted d : (family X86NativeRegister64) .
141 (lambda unrestricted n : Nat .
142 (digestEmit (constructor X86NativeInstruction X86NativeShiftLeftImmediate64 d (digestImm8 n)))))
143
144def digestShr =
145 (lambda unrestricted d : (family X86NativeRegister64) .
146 (lambda unrestricted n : Nat .
147 (digestEmit
148 (constructor X86NativeInstruction X86NativeShiftRightImmediate64 d (digestImm8 n)))))
149
150def digestMovImm =
151 (lambda unrestricted d : (family X86NativeRegister64) .
152 (lambda unrestricted n : Nat .
153 (digestEmit (constructor X86NativeInstruction X86NativeMoveImmediate32 d (digestImm32 n)))))
154
155def digestAddImm =
156 (lambda unrestricted d : (family X86NativeRegister64) .
157 (lambda unrestricted n : Nat .
158 (digestEmit (constructor X86NativeInstruction X86NativeAddImmediate64 d (digestImm32 n)))))
159
160def digestAndImm =
161 (lambda unrestricted d : (family X86NativeRegister64) .
162 (lambda unrestricted n : Nat .
163 (digestEmit (constructor X86NativeInstruction X86NativeAndImmediate64 d (digestImm32 n)))))
164
165def digestCmpImm =
166 (lambda unrestricted d : (family X86NativeRegister64) .
167 (lambda unrestricted n : Nat .
168 (digestEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 d (digestImm32 n)))))
169
170def digestMulImm =
171 (lambda unrestricted d : (family X86NativeRegister64) .
172 (lambda unrestricted n : Nat .
173 (digestEmit (constructor X86NativeInstruction X86NativeMultiplyImmediate64 d (digestImm32 n)))))
174
175def digestLabel =
176 (lambda unrestricted name : Bytes .
177 (lambda unrestricted rest : (family X86NativeAssembly) .
178 (constructor X86NativeAssembly X86NativeAssemblyLabel name rest)))
179
180def digestJumpIf =
181 (lambda unrestricted condition : (family X86NativeCondition) .
182 (lambda unrestricted name : Bytes .
183 (lambda unrestricted rest : (family X86NativeAssembly) .
184 (constructor X86NativeAssembly X86NativeAssemblyJumpCondition condition name rest))))
185
186def digestReturn =
187 (lambda unrestricted rest : (family X86NativeAssembly) .
188 (digestEmit (constructor X86NativeInstruction X86NativeReturn) rest))
189
190def digestEnd : (family X86NativeAssembly) =
191 (constructor X86NativeAssembly X86NativeAssemblyEnd)
192
193def digestBackendJump =
194 (lambda unrestricted condition : (family WordDigestCondition) .
195 (eliminate
196 WordDigestCondition
197 (lambda unrestricted current : (family WordDigestCondition) .
198 (pi unrestricted name : Bytes .
199 (pi unrestricted rest : (family X86NativeAssembly) . (family X86NativeAssembly))))
200 condition
201 (branch
202 WordDigestBelow
203 .
204 (digestJumpIf (constructor X86NativeCondition X86NativeConditionBelow)))
205 (branch
206 WordDigestNotZero
207 .
208 (digestJumpIf (constructor X86NativeCondition X86NativeConditionNotZero)))
209 (branch
210 WordDigestZero
211 .
212 (digestJumpIf (constructor X86NativeCondition X86NativeConditionZero)))
213 (branch
214 WordDigestNegative
215 .
216 (digestJumpIf (constructor X86NativeCondition X86NativeConditionSign)))))
217
218def digestX86Backend :
219 (family WordDigestBackend (family X86NativeAssembly) (family X86NativeRegister64)) =
220 (constructor
221 WordDigestBackend
222 WordDigestBackendValue
223 (family X86NativeAssembly)
224 (family X86NativeRegister64)
225 digestLoad32
226 digestLoad64
227 digestLoad8
228 digestStore32
229 digestStore64
230 digestStore8
231 digestMov
232 digestAdd
233 digestAnd
234 digestOr
235 digestXor
236 digestShl
237 digestShr
238 digestMovImm
239 digestAddImm
240 digestAndImm
241 digestCmpImm
242 digestMulImm
243 digestLabel
244 digestBackendJump
245 digestReturn
246 digestEnd
247 digestRAX
248 digestRBX
249 digestRCX
250 digestRDX
251 digestRSI
252 digestRDI
253 digestRBP
254 digestR8
255 digestR9
256 digestR10
257 digestR11
258 digestR12
259 digestR13
260 digestR14
261 digestR15)
262
263def nativeWordDigestAssembly =
264 (wordDigestAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) digestX86Backend)
265
266def nativeWordDigestRoutine =
267 (compiler-native-encode (family X86NativeAssembly) nativeWordDigestAssembly)
268
269-- Hash a runtime-length byte string in an admitted writable buffer. RDI is
270-- the input followed by two writable SHA blocks; RSI is a u32 byte count;
271-- RDX and R9 retain the block routine's output and work-area arguments. Only
272-- the suffix is changed. Two blocks cover the longest SHA padding, including
273-- the length word. This entry point admits Linux user pointers, rejects error
274-- pointers and oversized lengths before touching memory, and returns zero on
275-- refusal. Allocation, extent and disjointness remain the caller's contract.
276-- Padding uses caller-saved R10: RBX belongs to the native host result-slot
277-- table and must reach the block routine unchanged so its save/restore works.
278-- The compression equations have one owner in WordDigest; this adds padding,
279-- never a second hash implementation or a dependency on kernel crypto policy.
280def nativeByteDigestPaddingBytes : Nat =
281 byteDigestPaddingBytes
282
283def nativeByteDigestPaddingAssembly =
284 (wordDigestBytePaddingFor
285 (family X86NativeAssembly)
286 (family X86NativeRegister64)
287 digestX86Backend
288 digestRSI
289 nativeWordDigestAssembly)
290
291-- The initial jump skips the refusal return. Both paths share one typed
292-- assembly, so label resolution still belongs to the compiler's encoder.
293def nativeByteDigestRoutine =
294 (compiler-native-encode
295 (family X86NativeAssembly)
296 (constructor
297 X86NativeAssembly
298 X86NativeAssemblyJump
299 b"byte-digest-entry"
300 (digestLabel
301 b"byte-digest-refused"
302 (digestMovImm
303 digestRAX
304 0
305 (digestReturn (digestLabel b"byte-digest-entry" nativeByteDigestPaddingAssembly))))))
306
307-- Streaming preserves the same caller-save boundary as the one-shot routine.
308def nativeWordDigestContinueRoutine =
309 (compiler-native-encode
310 (family X86NativeAssembly)
311 (wordDigestContinueAssemblyFor
312 (family X86NativeAssembly)
313 (family X86NativeRegister64)
314 digestX86Backend))
315
316def nativeByteDigestStreamStartRoutine =
317 (compiler-native-encode
318 (family X86NativeAssembly)
319 (wordDigestStreamStartFor
320 (family X86NativeAssembly)
321 (family X86NativeRegister64)
322 digestX86Backend))
323
324def nativeByteDigestStreamFinishRoutine =
325 (compiler-native-encode
326 (family X86NativeAssembly)
327 (constructor
328 X86NativeAssembly
329 X86NativeAssemblyJump
330 b"byte-digest-entry"
331 (digestLabel
332 b"byte-digest-refused"
333 (digestMovImm
334 digestRAX
335 0
336 (digestReturn
337 (digestLabel
338 b"byte-digest-entry"
339 (wordDigestStreamFinishFor
340 (family X86NativeAssembly)
341 (family X86NativeRegister64)
342 digestX86Backend)))))))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.