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)))))))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.