Runtime.NativeWordArithmetic

1module Runtime.NativeWordArithmetic
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Runtime.NativePhysicalProgram
6import Runtime.NativeLaunchRecipeLoad
7
8-- System V: RDI destination, RSI left, RDX right. Unsigned addition returns
9-- zero and stores the sum, or one on overflow without touching destination.
10-- No pointer or counter is truncated to a signed immediate. The carry branch
11-- must precede the store: recovery and frame versions cannot wrap into reuse.
12def nativeCheckedWordAddAssembly : (family X86NativeAssembly) =
13  (constructor
14    X86NativeAssembly
15    X86NativeAssemblyEmit
16    (constructor
17      X86NativeInstruction
18      X86NativeAddRegister64
19      (constructor X86NativeRegister64 X86NativeRDX)
20      (constructor X86NativeRegister64 X86NativeRSI))
21    (constructor
22      X86NativeAssembly
23      X86NativeAssemblyJumpCondition
24      (constructor X86NativeCondition X86NativeConditionBelow)
25      b"overflow"
26      (constructor
27        X86NativeAssembly
28        X86NativeAssemblyEmit
29        (constructor
30          X86NativeInstruction
31          X86NativeStoreMemory64
32          (constructor X86NativeRegister64 X86NativeRDI)
33          (x86NativeDisplacement32FromNatural 0)
34          (constructor X86NativeRegister64 X86NativeRSI))
35        (constructor
36          X86NativeAssembly
37          X86NativeAssemblyEmit
38          (constructor
39            X86NativeInstruction
40            X86NativeClear32
41            (constructor X86NativeRegister64 X86NativeRAX))
42          (constructor
43            X86NativeAssembly
44            X86NativeAssemblyEmit
45            (constructor X86NativeInstruction X86NativeReturn)
46            (constructor
47              X86NativeAssembly
48              X86NativeAssemblyLabel
49              b"overflow"
50              (constructor
51                X86NativeAssembly
52                X86NativeAssemblyEmit
53                (constructor
54                  X86NativeInstruction
55                  X86NativeMoveImmediate32
56                  (constructor X86NativeRegister64 X86NativeRAX)
57                  (x86NativeImmediate32FromNatural 1))
58                (constructor
59                  X86NativeAssembly
60                  X86NativeAssemblyEmit
61                  (constructor X86NativeInstruction X86NativeReturn)
62                  (constructor X86NativeAssembly X86NativeAssemblyEnd)))))))))
63
64def nativeCheckedWordAddCode : Bytes =
65  (compiler-native-encode (family X86NativeAssembly) nativeCheckedWordAddAssembly)
66
67def nativeCheckedWordAdd =
68  (lambda unrestricted destination : (family NativePhysicalOperand) .
69    (lambda unrestricted left : (family NativePhysicalOperand) .
70      (lambda unrestricted right : (family NativePhysicalOperand) .
71        (lambda unrestricted slot : Nat .
72          (lambda unrestricted error : Bytes .
73            (lambda unrestricted tail : (family NativePhysicalCommands) .
74              (nativeLaunchRecipeCommand
75                (constructor
76                  NativePhysicalOperation
77                  NativePhysicalMachineRoutine
78                  nativeCheckedWordAddCode
79                  (nativeLaunchRecipeArguments
80                    destination
81                    left
82                    right
83                    (nativeLaunchRecipeImmediate 0))
84                  (nativeLaunchRecipeStore slot))
85                error
86                (nativeLaunchRecipeAssertEqual
87                  (nativeLaunchRecipeSlotValue slot)
88                  (nativeLaunchRecipeImmediate 0)
89                  error
90                  tail))))))))