Platform.AArch64.WordDigest

1module Platform.AArch64.WordDigest
2
3import Compiler.MachineAArch64
4import Compiler.MachineAArch64Assembly
5import Model.Config
6import Platform.AArch64.RoutineEmitter
7import Runtime.WordDigest
8import Std.Natural
9
10-- AAPCS64 emitter for shared word digest and ALPHATEL sealing. Arguments occupy
11-- x0..x5; all other values fit in caller-saved x6..x14. x16 is exclusively an
12-- address scratch and x17 an immediate scratch; x18 and callee-saved registers
13-- are untouched. The interpreter also retains image state in x12..x14 across
14-- inline calls. The shared algorithm saves/restores those registers through
15-- its R13/R14/R15 roles; this custom runtime requirement is stronger than
16-- AAPCS64 and those saves must not be removed as redundant.
17-- Form addresses before loads/stores so the clock field at byte 13 is handled
18-- as an unaligned access, without truncating an A64 scaled displacement.
19def digestAArch64JumpIf =
20  (lambda unrestricted condition : (family WordDigestCondition) .
21    (lambda unrestricted name : Bytes .
22      (lambda unrestricted rest : (family AArch64Assembly) .
23        (constructor
24          AArch64Assembly
25          AArch64AssemblyBranchIf
26          (eliminate
27            WordDigestCondition
28            (lambda unrestricted current : (family WordDigestCondition) . (family AArch64Condition))
29            condition
30            (branch WordDigestBelow . (constructor AArch64Condition AArch64CarryClear))
31            (branch WordDigestNotZero . (constructor AArch64Condition AArch64NotEqual))
32            (branch WordDigestZero . (constructor AArch64Condition AArch64Equal))
33            (branch WordDigestNegative . (constructor AArch64Condition AArch64Minus)))
34          name
35          rest))))
36
37def aarch64WordDigestBackendFor =
38  (lambda unrestricted return : (pi unrestricted tail : (family AArch64Assembly) . (family AArch64Assembly)) .
39    (constructor
40      WordDigestBackend
41      WordDigestBackendValue
42      (family AArch64Assembly)
43      (family AArch64Register)
44      ahrLoad32
45      ahrLoad64
46      ahrLoad8
47      ahrStore32
48      ahrStore64
49      ahrStore8
50      ahrMov
51      ahrAdd
52      ahrAnd
53      ahrOr
54      ahrXor
55      ahrShl
56      ahrShr
57      ahrMovImm
58      ahrAddImm
59      ahrAndImm
60      ahrCmpImm
61      ahrMulImm
62      ahrLabel
63      digestAArch64JumpIf
64      return
65      ahrEnd
66      ahrX6
67      ahrX7
68      ahrX3
69      ahrX2
70      ahrX1
71      ahrX0
72      ahrX8
73      ahrX4
74      ahrX5
75      ahrX9
76      ahrX10
77      ahrX11
78      ahrX12
79      ahrX13
80      ahrX14))
81
82-- The existing seal has a void result, so keep its emission unchanged. Raw
83-- digest returns a byte count: the abstract RAX lives in x6, whereas AAPCS64
84-- and NativePhysicalRuntime consume the return value in x0.
85def aarch64WordDigestBackend =
86  (aarch64WordDigestBackendFor ahrReturn)
87
88def aarch64WordDigestReturn =
89  (lambda unrestricted tail : (family AArch64Assembly) . (ahrMov ahrX0 ahrX6 (ahrReturn tail)))
90
91def aarch64WordDigestAssembly : (family AArch64Assembly) =
92  (wordDigestAssemblyFor
93    (family AArch64Assembly)
94    (family AArch64Register)
95    (aarch64WordDigestBackendFor aarch64WordDigestReturn))
96
97def aarch64WordDigestRoutine : Bytes =
98  (aarch64RoutineBytes aarch64WordDigestAssembly)
99
100-- Select the same byte-padding algorithm with AAPCS64 register assignments.
101-- Refusal returns directly in x0; successful padding retains x0/x2/x5 for
102-- block compression and never touches the interpreter's x12..x14 state.
103def aarch64ByteDigestAssembly : (family AArch64Assembly) =
104  (constructor
105    AArch64Assembly
106    AArch64AssemblyBranch
107    b"byte-digest-entry"
108    (ahrLabel
109      b"byte-digest-refused"
110      (ahrMovImm
111        ahrX0
112        0
113        (ahrReturn
114          (ahrLabel
115            b"byte-digest-entry"
116            (wordDigestBytePaddingFor
117              (family AArch64Assembly)
118              (family AArch64Register)
119              (aarch64WordDigestBackendFor aarch64WordDigestReturn)
120              ahrX1
121              aarch64WordDigestAssembly))))))
122
123def aarch64ByteDigestRoutine : Bytes =
124  (aarch64RoutineBytes aarch64ByteDigestAssembly)
125
126def aarch64WordDigestContinueAssembly =
127  (wordDigestContinueAssemblyFor
128    (family AArch64Assembly)
129    (family AArch64Register)
130    (aarch64WordDigestBackendFor aarch64WordDigestReturn))
131
132def aarch64WordDigestContinueRoutine : Bytes =
133  (aarch64RoutineBytes aarch64WordDigestContinueAssembly)
134
135def aarch64ByteDigestStreamStartAssembly =
136  (wordDigestStreamStartFor
137    (family AArch64Assembly)
138    (family AArch64Register)
139    (aarch64WordDigestBackendFor aarch64WordDigestReturn))
140
141def aarch64ByteDigestStreamStartRoutine : Bytes =
142  (aarch64RoutineBytes aarch64ByteDigestStreamStartAssembly)
143
144def aarch64ByteDigestStreamFinishAssembly =
145  (constructor
146    AArch64Assembly
147    AArch64AssemblyBranch
148    b"byte-digest-entry"
149    (ahrLabel
150      b"byte-digest-refused"
151      (ahrMovImm
152        ahrX0
153        0
154        (ahrReturn
155          (ahrLabel
156            b"byte-digest-entry"
157            (wordDigestStreamFinishFor
158              (family AArch64Assembly)
159              (family AArch64Register)
160              (aarch64WordDigestBackendFor aarch64WordDigestReturn)))))))
161
162def aarch64ByteDigestStreamFinishRoutine : Bytes =
163  (aarch64RoutineBytes aarch64ByteDigestStreamFinishAssembly)