Runtime.NativeFloatPlan

1module Runtime.NativeFloatPlan
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Runtime.NativePhysicalProgram
6import Runtime.NativeLaunchRecipeLoad
7import Runtime.NativeMemoryPlan
8import Std.Numeric.Profile
9
10-- Numerical semantics of the guarded host commands below. This names a command
11-- contract, not a new measurement of any device. Each host executor owes the
12-- declared nearest-even, preserved-subnormal behavior; qualification checks
13-- its rounding and tiny-value cases separately. No device operation inherits
14-- this profile by falling back to host arithmetic.
15def nativeFiniteFloat64Profile : (family StdNumericProfile) =
16  (constructor
17    StdNumericProfile
18    StdNumericProfileOf
19    (constructor
20      StdNumericProfileIdentity
21      StdProfileIdentityNamed
22      b"native-f64-finite-separate-rne-v1")
23    (constructor StdNumericFormat StdFormatBinary64)
24    (constructor StdNumericFormat StdFormatBinary64)
25    (constructor StdRounding StdRoundNearestEven)
26    (constructor StdContraction StdContractionForbidden)
27    (constructor StdReductionOrder StdReductionDeclaredTree)
28    (constructor StdSubnormalHandling StdSubnormalsPreserved)
29    (constructor StdExceptionalValues StdExceptionalFiniteOrRefuse)
30    (stdTableCons
31      (stdEntry stdOpAdd stdExact)
32      (stdTableCons
33        (stdEntry stdOpSubtract stdExact)
34        (stdTableCons
35          (stdEntry stdOpMultiply stdExact)
36          (stdTableCons
37            (stdEntry stdOpDivide stdExact)
38            (stdTableCons (stdEntry stdOpSquareRoot stdExact) stdTableEmpty))))))
39
40-- Explicit host arithmetic commands. No device operation selects this path as
41-- a fallback. The caller owns scalar representation and state arena bounds.
42def nativeFloat64 =
43  (lambda unrestricted error : Bytes .
44    (lambda unrestricted op : (family NativePhysicalFloat64Operation) .
45      (lambda unrestricted destination : Nat .
46        (lambda unrestricted left : (family NativePhysicalOperand) .
47          (lambda unrestricted right : (family NativePhysicalOperand) .
48            (nativeLaunchRecipeCommand
49              (constructor
50                NativePhysicalOperation
51                NativePhysicalFloat64
52                op
53                (nativeMemoryState destination)
54                left
55                right)
56              error))))))
57
58def nativeFloat64Natural =
59  (lambda unrestricted error : Bytes .
60    (lambda unrestricted destination : Nat .
61      (lambda unrestricted value : Nat .
62        (nativeFloat64
63          error
64          (constructor NativePhysicalFloat64Operation NativePhysicalFloat64FromNatural)
65          destination
66          (nativeLaunchRecipeImmediate value)
67          (nativeLaunchRecipeImmediate 0)))))
68
69def nativeFloat64Binary =
70  (lambda unrestricted error : Bytes .
71    (lambda unrestricted op : (family NativePhysicalFloat64Operation) .
72      (lambda unrestricted destination : Nat .
73        (lambda unrestricted left : Nat .
74          (lambda unrestricted right : Nat .
75            (nativeFloat64 error op destination (nativeMemoryLoad left) (nativeMemoryLoad right)))))))
76
77-- One typed format boundary, realized by the maintained host float commands.
78-- Values occupy admitted word slots; binary32 words use the low half. Identity
79-- copies bits. Narrowing is visible in the source program and is never inserted
80-- by framing. The enclosing planner checks the producer/consumer endpoints.
81def nativeNumericConvert =
82  (lambda unrestricted error : Bytes .
83    (lambda unrestricted conversion : (family StdNumericConversion) .
84      (lambda unrestricted destination : Nat .
85        (lambda unrestricted source : (family NativePhysicalOperand) .
86          (eliminate
87            StdNumericConversion
88            (lambda unrestricted current : (family StdNumericConversion) .
89              (pi unrestricted tail : (family NativePhysicalCommands) .
90                (family NativePhysicalCommands)))
91            conversion
92            (branch
93              StdNumericKeepFormat
94              format
95              .
96              (nativeMemoryStoreWord64 error destination source))
97            (branch
98              StdNumericWidenBinary32
99              .
100              (nativeFloat64
101                error
102                (constructor NativePhysicalFloat64Operation NativePhysicalFloat64FromBinary32)
103                destination
104                source
105                (nativeLaunchRecipeImmediate 0)))
106            (branch
107              StdNumericRoundBinary64
108              .
109              (nativeFloat64
110                error
111                (constructor NativePhysicalFloat64Operation NativePhysicalFloat64ToBinary32)
112                destination
113                source
114                (nativeLaunchRecipeImmediate 0))))))))
115
116-- Binary64 is finite iff its eleven exponent bits are not all ones.
117-- RDI is a value, not an address. Only caller-saved RAX is modified; signed
118-- zeros and subnormals are accepted. Platform.AArch64.FloatRoutine supplies
119-- the admitted twin; an unknown host lowering still refuses.
120def nativeFloat64FiniteAssembly : (family X86NativeAssembly) =
121  (constructor
122    X86NativeAssembly
123    X86NativeAssemblyEmit
124    (constructor
125      X86NativeInstruction
126      X86NativeMoveRegister64
127      (constructor X86NativeRegister64 X86NativeRDI)
128      (constructor X86NativeRegister64 X86NativeRAX))
129    (constructor
130      X86NativeAssembly
131      X86NativeAssemblyEmit
132      (constructor
133        X86NativeInstruction
134        X86NativeShiftRightImmediate64
135        (constructor X86NativeRegister64 X86NativeRAX)
136        (constructor X86NativeImmediate8 X86NativeImmediate8Value (nat-to-byte 52)))
137      (constructor
138        X86NativeAssembly
139        X86NativeAssemblyEmit
140        (constructor
141          X86NativeInstruction
142          X86NativeAndImmediate64
143          (constructor X86NativeRegister64 X86NativeRAX)
144          (x86NativeImmediate32FromNatural 2047))
145        (constructor
146          X86NativeAssembly
147          X86NativeAssemblyEmit
148          (constructor
149            X86NativeInstruction
150            X86NativeCompareImmediate64
151            (constructor X86NativeRegister64 X86NativeRAX)
152            (x86NativeImmediate32FromNatural 2047))
153          (constructor
154            X86NativeAssembly
155            X86NativeAssemblyJumpCondition
156            (constructor X86NativeCondition X86NativeConditionNotZero)
157            b"finite"
158            (constructor
159              X86NativeAssembly
160              X86NativeAssemblyEmit
161              (constructor
162                X86NativeInstruction
163                X86NativeMoveImmediate32
164                (constructor X86NativeRegister64 X86NativeRAX)
165                (x86NativeImmediate32FromNatural 1))
166              (constructor
167                X86NativeAssembly
168                X86NativeAssemblyEmit
169                (constructor X86NativeInstruction X86NativeReturn)
170                (constructor
171                  X86NativeAssembly
172                  X86NativeAssemblyLabel
173                  b"finite"
174                  (constructor
175                    X86NativeAssembly
176                    X86NativeAssemblyEmit
177                    (constructor
178                      X86NativeInstruction
179                      X86NativeClear32
180                      (constructor X86NativeRegister64 X86NativeRAX))
181                    (constructor
182                      X86NativeAssembly
183                      X86NativeAssemblyEmit
184                      (constructor X86NativeInstruction X86NativeReturn)
185                      (constructor X86NativeAssembly X86NativeAssemblyEnd)))))))))))
186
187def nativeFloat64FiniteCode : Bytes =
188  (compiler-native-encode (family X86NativeAssembly) nativeFloat64FiniteAssembly)
189
190def nativeFloat64RequireFinite =
191  (lambda unrestricted value : (family NativePhysicalOperand) .
192    (lambda unrestricted slot : Nat .
193      (lambda unrestricted error : Bytes .
194        (lambda unrestricted tail : (family NativePhysicalCommands) .
195          (nativeLaunchRecipeCommand
196            (constructor
197              NativePhysicalOperation
198              NativePhysicalMachineRoutine
199              nativeFloat64FiniteCode
200              (nativeLaunchRecipeArguments
201                value
202                (nativeLaunchRecipeImmediate 0)
203                (nativeLaunchRecipeImmediate 0)
204                (nativeLaunchRecipeImmediate 0))
205              (nativeLaunchRecipeStore slot))
206            error
207            (nativeLaunchRecipeAssertEqual
208              (nativeLaunchRecipeSlotValue slot)
209              (nativeLaunchRecipeImmediate 0)
210              error
211              tail))))))
212
213-- Finite-domain arithmetic has an explicit refusal outcome. This avoids making
214-- cross-host equality depend on unspecified NaN payload/default bits. Input
215-- and output checks remain in the emitted program, including after overflow.
216def nativeFiniteFloat64Binary =
217  (lambda unrestricted error : Bytes .
218    (lambda unrestricted slot : Nat .
219      (lambda unrestricted operation : (family NativePhysicalFloat64Operation) .
220        (lambda unrestricted destination : Nat .
221          (lambda unrestricted left : Nat .
222            (lambda unrestricted right : Nat .
223              (lambda unrestricted tail : (family NativePhysicalCommands) .
224                (nativeFloat64RequireFinite
225                  (nativeMemoryLoad left)
226                  slot
227                  error
228                  (nativeFloat64RequireFinite
229                    (nativeMemoryLoad right)
230                    slot
231                    error
232                    (nativeFloat64Binary
233                      error
234                      operation
235                      destination
236                      left
237                      right
238                      (nativeFloat64RequireFinite (nativeMemoryLoad destination) slot error tail)))))))))))