1module Compiler.MachineX86
2
3family X86ValueClass : Type 0
4constructor X86UndefinedValue
5constructor X86Word64Value
6constructor X86AddressValue
7
8end-family
9
10family X86MachineState : Type 0
11constructor X86MachineStateValue
12field erased x86StateRAX : (family X86ValueClass)
13field erased x86StateRDI : (family X86ValueClass)
14field erased x86StateRSI : (family X86ValueClass)
15field erased x86StateRDX : (family X86ValueClass)
16
17end-family
18
19family X86EffectTrace : Type 0
20constructor X86NoEffects
21constructor X86SystemCallEffect
22recursive erased x86RemainingEffects
23
24end-family
25
26family X86Immediate32 : Type 0
27constructor X86Immediate32Value
28field unrestricted x86ImmediateByte0 : Byte
29field unrestricted x86ImmediateByte1 : Byte
30field unrestricted x86ImmediateByte2 : Byte
31field unrestricted x86ImmediateByte3 : Byte
32
33end-family
34
35family X86Instruction : Type 0
36index erased x86InstructionInput : (family X86MachineState)
37index erased x86InstructionOutput : (family X86MachineState)
38index erased x86InstructionEffects : (family X86EffectTrace)
39constructor X86ZeroEDI32
40field erased x86ZeroInputRAX : (family X86ValueClass)
41field erased x86ZeroInputRDI : (family X86ValueClass)
42field erased x86ZeroInputRSI : (family X86ValueClass)
43field erased x86ZeroInputRDX : (family X86ValueClass)
44result (constructor X86MachineState X86MachineStateValue x86ZeroInputRAX x86ZeroInputRDI x86ZeroInputRSI x86ZeroInputRDX)
45result (constructor X86MachineState X86MachineStateValue x86ZeroInputRAX (constructor X86ValueClass X86Word64Value) x86ZeroInputRSI x86ZeroInputRDX)
46result (constructor X86EffectTrace X86NoEffects)
47constructor X86IncrementRDI64
48field erased x86IncrementInputRAX : (family X86ValueClass)
49field erased x86IncrementInputRSI : (family X86ValueClass)
50field erased x86IncrementInputRDX : (family X86ValueClass)
51result (constructor X86MachineState X86MachineStateValue x86IncrementInputRAX (constructor X86ValueClass X86Word64Value) x86IncrementInputRSI x86IncrementInputRDX)
52result (constructor X86MachineState X86MachineStateValue x86IncrementInputRAX (constructor X86ValueClass X86Word64Value) x86IncrementInputRSI x86IncrementInputRDX)
53result (constructor X86EffectTrace X86NoEffects)
54constructor X86MoveEAXImmediate32
55field erased x86MoveEAXInputRAX : (family X86ValueClass)
56field erased x86MoveEAXInputRDI : (family X86ValueClass)
57field erased x86MoveEAXInputRSI : (family X86ValueClass)
58field erased x86MoveEAXInputRDX : (family X86ValueClass)
59field unrestricted x86MoveEAXImmediate : (family X86Immediate32)
60result (constructor X86MachineState X86MachineStateValue x86MoveEAXInputRAX x86MoveEAXInputRDI x86MoveEAXInputRSI x86MoveEAXInputRDX)
61result (constructor X86MachineState X86MachineStateValue (constructor X86ValueClass X86Word64Value) x86MoveEAXInputRDI x86MoveEAXInputRSI x86MoveEAXInputRDX)
62result (constructor X86EffectTrace X86NoEffects)
63constructor X86MoveEDIImmediate32
64field erased x86MoveEDIInputRAX : (family X86ValueClass)
65field erased x86MoveEDIInputRDI : (family X86ValueClass)
66field erased x86MoveEDIInputRSI : (family X86ValueClass)
67field erased x86MoveEDIInputRDX : (family X86ValueClass)
68field unrestricted x86MoveEDIImmediate : (family X86Immediate32)
69result (constructor X86MachineState X86MachineStateValue x86MoveEDIInputRAX x86MoveEDIInputRDI x86MoveEDIInputRSI x86MoveEDIInputRDX)
70result (constructor X86MachineState X86MachineStateValue x86MoveEDIInputRAX (constructor X86ValueClass X86Word64Value) x86MoveEDIInputRSI x86MoveEDIInputRDX)
71result (constructor X86EffectTrace X86NoEffects)
72constructor X86MoveEDXImmediate32
73field erased x86MoveEDXInputRAX : (family X86ValueClass)
74field erased x86MoveEDXInputRDI : (family X86ValueClass)
75field erased x86MoveEDXInputRSI : (family X86ValueClass)
76field erased x86MoveEDXInputRDX : (family X86ValueClass)
77field unrestricted x86MoveEDXImmediate : (family X86Immediate32)
78result (constructor X86MachineState X86MachineStateValue x86MoveEDXInputRAX x86MoveEDXInputRDI x86MoveEDXInputRSI x86MoveEDXInputRDX)
79result (constructor X86MachineState X86MachineStateValue x86MoveEDXInputRAX x86MoveEDXInputRDI x86MoveEDXInputRSI (constructor X86ValueClass X86Word64Value))
80result (constructor X86EffectTrace X86NoEffects)
81constructor X86LoadRSIRIPRelative
82field erased x86LoadRSIInputRAX : (family X86ValueClass)
83field erased x86LoadRSIInputRDI : (family X86ValueClass)
84field erased x86LoadRSIInputRSI : (family X86ValueClass)
85field erased x86LoadRSIInputRDX : (family X86ValueClass)
86field unrestricted x86LoadRSIDisplacement : (family X86Immediate32)
87result (constructor X86MachineState X86MachineStateValue x86LoadRSIInputRAX x86LoadRSIInputRDI x86LoadRSIInputRSI x86LoadRSIInputRDX)
88result (constructor X86MachineState X86MachineStateValue x86LoadRSIInputRAX x86LoadRSIInputRDI (constructor X86ValueClass X86AddressValue) x86LoadRSIInputRDX)
89result (constructor X86EffectTrace X86NoEffects)
90constructor X86SystemCall
91field erased x86SystemCallInputRDI : (family X86ValueClass)
92field erased x86SystemCallInputRSI : (family X86ValueClass)
93field erased x86SystemCallInputRDX : (family X86ValueClass)
94result (constructor X86MachineState X86MachineStateValue (constructor X86ValueClass X86Word64Value) x86SystemCallInputRDI x86SystemCallInputRSI x86SystemCallInputRDX)
95result (constructor X86MachineState X86MachineStateValue (constructor X86ValueClass X86Word64Value) x86SystemCallInputRDI x86SystemCallInputRSI x86SystemCallInputRDX)
96result (constructor X86EffectTrace X86SystemCallEffect (constructor X86EffectTrace X86NoEffects))
97
98end-family
99
100family X86Program : Type 0
101index erased x86ProgramInput : (family X86MachineState)
102index erased x86ProgramOutput : (family X86MachineState)
103index erased x86ProgramEffects : (family X86EffectTrace)
104constructor X86ProgramEnd
105field erased x86ProgramEndState : (family X86MachineState)
106result x86ProgramEndState
107result x86ProgramEndState
108result (constructor X86EffectTrace X86NoEffects)
109constructor X86ProgramPureNext
110field erased x86ProgramStartState : (family X86MachineState)
111field erased x86ProgramMiddleState : (family X86MachineState)
112field erased x86ProgramFinishState : (family X86MachineState)
113field erased x86ProgramTailEffects : (family X86EffectTrace)
114field unrestricted x86ProgramHead : (family X86Instruction x86ProgramStartState x86ProgramMiddleState (constructor X86EffectTrace X86NoEffects))
115recursive unrestricted x86ProgramTail
116recursive-index x86ProgramMiddleState
117recursive-index x86ProgramFinishState
118recursive-index x86ProgramTailEffects
119result x86ProgramStartState
120result x86ProgramFinishState
121result x86ProgramTailEffects
122constructor X86ProgramSystemCallNext
123field erased x86SystemCallProgramStartState : (family X86MachineState)
124field erased x86SystemCallProgramMiddleState : (family X86MachineState)
125field erased x86SystemCallProgramFinishState : (family X86MachineState)
126field erased x86SystemCallProgramTailEffects : (family X86EffectTrace)
127field unrestricted x86SystemCallProgramHead : (family X86Instruction x86SystemCallProgramStartState x86SystemCallProgramMiddleState (constructor X86EffectTrace X86SystemCallEffect (constructor X86EffectTrace X86NoEffects)))
128recursive unrestricted x86SystemCallProgramTail
129recursive-index x86SystemCallProgramMiddleState
130recursive-index x86SystemCallProgramFinishState
131recursive-index x86SystemCallProgramTailEffects
132result x86SystemCallProgramStartState
133result x86SystemCallProgramFinishState
134result (constructor X86EffectTrace X86SystemCallEffect x86SystemCallProgramTailEffects)
135
136end-family
137
138def x86Immediate32 =
139 (lambda unrestricted lowByte : Byte .
140 (constructor X86Immediate32 X86Immediate32Value lowByte (byte 0) (byte 0) (byte 0)))
141
142def x86EncodeImmediate32 =
143 (lambda unrestricted immediate : (family X86Immediate32) .
144 (eliminate
145 X86Immediate32
146 (lambda unrestricted value : (family X86Immediate32) . Bytes)
147 immediate
148 (branch
149 X86Immediate32Value
150 byte0
151 byte1
152 byte2
153 byte3
154 .
155 (bytes-cons byte0 (bytes-cons byte1 (bytes-cons byte2 (bytes-cons byte3 b"")))))))
156
157def x86EncodeInstruction =
158 (lambda erased input : (family X86MachineState) .
159 (lambda erased output : (family X86MachineState) .
160 (lambda erased effects : (family X86EffectTrace) .
161 (lambda unrestricted instruction : (family X86Instruction input output effects) .
162 (eliminate
163 X86Instruction
164 (lambda erased motiveInput : (family X86MachineState) .
165 (lambda erased motiveOutput : (family X86MachineState) .
166 (lambda erased motiveEffects : (family X86EffectTrace) .
167 (lambda unrestricted value : (family X86Instruction motiveInput motiveOutput motiveEffects) .
168 Bytes))))
169 instruction
170 (branch X86ZeroEDI32 inputRAX inputRDI inputRSI inputRDX . (bytes 49 255))
171 (branch X86IncrementRDI64 inputRAX inputRSI inputRDX . (bytes 72 255 199))
172 (branch
173 X86MoveEAXImmediate32
174 inputRAX
175 inputRDI
176 inputRSI
177 inputRDX
178 immediate
179 .
180 (bytes-append (bytes 184) (x86EncodeImmediate32 immediate)))
181 (branch
182 X86MoveEDIImmediate32
183 inputRAX
184 inputRDI
185 inputRSI
186 inputRDX
187 immediate
188 .
189 (bytes-append (bytes 191) (x86EncodeImmediate32 immediate)))
190 (branch
191 X86MoveEDXImmediate32
192 inputRAX
193 inputRDI
194 inputRSI
195 inputRDX
196 immediate
197 .
198 (bytes-append (bytes 186) (x86EncodeImmediate32 immediate)))
199 (branch
200 X86LoadRSIRIPRelative
201 inputRAX
202 inputRDI
203 inputRSI
204 inputRDX
205 displacement
206 .
207 (bytes-append (bytes 72 141 53) (x86EncodeImmediate32 displacement)))
208 (branch X86SystemCall inputRDI inputRSI inputRDX . (bytes 15 5)))))))
209
210def x86EncodeProgramBuilder =
211 (lambda erased input : (family X86MachineState) .
212 (lambda erased output : (family X86MachineState) .
213 (lambda erased effects : (family X86EffectTrace) .
214 (lambda unrestricted program : (family X86Program input output effects) .
215 (eliminate
216 X86Program
217 (lambda erased motiveInput : (family X86MachineState) .
218 (lambda erased motiveOutput : (family X86MachineState) .
219 (lambda erased motiveEffects : (family X86EffectTrace) .
220 (lambda unrestricted value : (family X86Program motiveInput motiveOutput motiveEffects) .
221 BytesBuilder))))
222 program
223 (branch X86ProgramEnd state . (bytes-builder-empty))
224 (branch
225 X86ProgramPureNext
226 start
227 middle
228 finish
229 tailEffects
230 head
231 tail
232 ih_tail
233 .
234 (bytes-builder-append
235 (bytes-builder-chunk
236 (x86EncodeInstruction start middle (constructor X86EffectTrace X86NoEffects) head))
237 ih_tail))
238 (branch
239 X86ProgramSystemCallNext
240 start
241 middle
242 finish
243 tailEffects
244 head
245 tail
246 ih_tail
247 .
248 (bytes-builder-append
249 (bytes-builder-chunk
250 (x86EncodeInstruction
251 start
252 middle
253 (constructor
254 X86EffectTrace
255 X86SystemCallEffect
256 (constructor X86EffectTrace X86NoEffects))
257 head))
258 ih_tail)))))))
259
260def x86EncodeProgram =
261 (lambda erased input : (family X86MachineState) .
262 (lambda erased output : (family X86MachineState) .
263 (lambda erased effects : (family X86EffectTrace) .
264 (lambda unrestricted program : (family X86Program input output effects) .
265 (bytes-builder-build (x86EncodeProgramBuilder input output effects program))))))
266
267def x86UndefinedClass : (family X86ValueClass) =
268 (constructor X86ValueClass X86UndefinedValue)
269
270def x86Word64Class : (family X86ValueClass) =
271 (constructor X86ValueClass X86Word64Value)
272
273def x86AddressClass : (family X86ValueClass) =
274 (constructor X86ValueClass X86AddressValue)
275
276def x86NoEffects : (family X86EffectTrace) =
277 (constructor X86EffectTrace X86NoEffects)
278
279def x86OneSystemCall : (family X86EffectTrace) =
280 (constructor X86EffectTrace X86SystemCallEffect x86NoEffects)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.