Runtime.NativeTelemetryValue

1module Runtime.NativeTelemetryValue
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Observe.Value
6import Runtime.NativeTelemetrySeal
7import Runtime.TelemetryCapture
8import Runtime.TelemetryValue
9import Std.Natural
10import Runtime.TelemetryValueRoutine
11import Runtime.NativeWordDigest
12
13-- System V realization of the shared formatter algorithm. The original
14-- register assignment and instruction encodings are intentionally preserved.
15def valueX86Compare =
16  (lambda unrestricted left : (family X86NativeRegister64) .
17    (lambda unrestricted right : (family X86NativeRegister64) .
18      (digestEmit (constructor X86NativeInstruction X86NativeCompareRegister64 right left))))
19
20def valueX86Subtract =
21  (lambda unrestricted left : (family X86NativeRegister64) .
22    (lambda unrestricted right : (family X86NativeRegister64) .
23      (digestEmit (constructor X86NativeInstruction X86NativeSubtractRegister64 right left))))
24
25def valueX86Divide =
26  (lambda unrestricted divisor : (family X86NativeRegister64) .
27    (digestEmit (constructor X86NativeInstruction X86NativeDivideRegister64Unsigned divisor)))
28
29def valueX86JumpIf =
30  (lambda unrestricted condition : (family TelemetryValueCondition) .
31    (digestJumpIf
32      (eliminate
33        TelemetryValueCondition
34        (lambda unrestricted current : (family TelemetryValueCondition) .
35          (family X86NativeCondition))
36        condition
37        (branch TelemetryValueZero . (constructor X86NativeCondition X86NativeConditionZero))
38        (branch TelemetryValueNotZero . (constructor X86NativeCondition X86NativeConditionNotZero))
39        (branch TelemetryValueBelow . (constructor X86NativeCondition X86NativeConditionBelow))
40        (branch TelemetryValueAbove . (constructor X86NativeCondition X86NativeConditionAbove)))))
41
42def valueX86Jump =
43  (lambda unrestricted name : Bytes .
44    (lambda unrestricted tail : (family X86NativeAssembly) .
45      (constructor X86NativeAssembly X86NativeAssemblyJump name tail)))
46
47def valueX86Backend =
48  (constructor
49    TelemetryValueBackend
50    TelemetryValueBackendValue
51    (family X86NativeAssembly)
52    (family X86NativeRegister64)
53    digestLoad64
54    digestLoad8
55    digestStore8
56    digestMov
57    digestMovImm
58    digestCmpImm
59    valueX86Compare
60    digestAdd
61    digestAddImm
62    valueX86Subtract
63    digestShr
64    digestAndImm
65    valueX86Divide
66    valueX86JumpIf
67    valueX86Jump
68    digestLabel
69    digestReturn
70    digestEnd
71    digestRAX
72    digestRDI
73    digestRSI
74    digestRDX
75    digestRCX
76    digestR8
77    digestR9
78    digestR10
79    digestR11)
80
81def nativeTelemetryDecimalCellRoutine =
82  (lambda unrestricted signed : Nat .
83    (aosChoose
84      Bytes
85      (naturalLessOrEqual signed 1)
86      (compiler-native-encode
87        (family X86NativeAssembly)
88        (telemetryValueAssemblyFor
89          (family X86NativeAssembly)
90          (family X86NativeRegister64)
91          valueX86Backend
92          (constructor TelemetryValueRoutineKind TelemetryValueDecimalRoutine signed)))
93      b""))
94
95def nativeTelemetryHexCellRoutine =
96  (lambda unrestricted width : Nat .
97    (lambda unrestricted reverse : Nat .
98      (aosChoose
99        Bytes
100        (naturalAnd
101          (naturalNonzero width)
102          (naturalAnd
103            (naturalLessOrEqual width telemetryHexSourceMaximumBytes)
104            (naturalLessOrEqual reverse 1)))
105        (compiler-native-encode
106          (family X86NativeAssembly)
107          (telemetryValueAssemblyFor
108            (family X86NativeAssembly)
109            (family X86NativeRegister64)
110            valueX86Backend
111            (constructor TelemetryValueRoutineKind TelemetryValueHexRoutine width reverse)))
112        b"")))
113
114def nativeTelemetryDecimalWordCellRoutine =
115  (lambda unrestricted signed : Nat .
116    (lambda unrestricted offset : Nat .
117      (aosChoose
118        Bytes
119        (naturalAnd
120          (naturalLessOrEqual signed 1)
121          (naturalLessOrEqual (naturalAdd offset captureWordBytes) captureRecordBytes))
122        (compiler-native-encode
123          (family X86NativeAssembly)
124          (telemetryValueAssemblyFor
125            (family X86NativeAssembly)
126            (family X86NativeRegister64)
127            valueX86Backend
128            (constructor TelemetryValueRoutineKind TelemetryValueWordRoutine signed offset)))
129        b"")))
130
131def nativeTelemetryHexSliceCellRoutine =
132  (lambda unrestricted width : Nat .
133    (lambda unrestricted reverse : Nat .
134      (lambda unrestricted offset : Nat .
135        (aosChoose
136          Bytes
137          (naturalAnd
138            (naturalNonzero width)
139            (naturalAnd
140              (naturalLessOrEqual width telemetryHexSourceMaximumBytes)
141              (naturalAnd
142                (naturalLessOrEqual reverse 1)
143                (naturalLessOrEqual (naturalAdd offset width) captureRecordBytes))))
144          (compiler-native-encode
145            (family X86NativeAssembly)
146            (telemetryValueAssemblyFor
147              (family X86NativeAssembly)
148              (family X86NativeRegister64)
149              valueX86Backend
150              (constructor
151                TelemetryValueRoutineKind
152                TelemetryValueSliceRoutine
153                width
154                reverse
155                offset)))
156          b""))))