1(* arm - generated by L3 - Wed Jan 31 15:06:54 2018 *)
2
3signature arm =
4sig
5
6structure Map : Map
7
8(* -------------------------------------------------------------------------
9   Types
10   ------------------------------------------------------------------------- *)
11
12datatype Architecture
13  = ARMv4 | ARMv4T | ARMv5T | ARMv5TE | ARMv6 | ARMv6K | ARMv6T2 | ARMv7_A
14  | ARMv7_R
15
16datatype Extensions
17  = Extension_ThumbEE | Extension_Security | Extension_Multiprocessing
18  | Extension_Virtualization | Extension_AdvanvedSIMD
19
20type PSR =
21  { A: bool, C: bool, E: bool, F: bool, GE: BitsN.nbit, I: bool,
22    IT: BitsN.nbit, J: bool, M: BitsN.nbit, N: bool, Q: bool, T: bool,
23    V: bool, Z: bool, psr'rst: BitsN.nbit }
24
25type CP14 = { TEEHBR: BitsN.nbit }
26
27type SCTLR =
28  { A: bool, B: bool, BR: bool, C: bool, DZ: bool, EE: bool, FI: bool,
29    I: bool, IE: bool, M: bool, NMFI: bool, RR: bool, SW: bool, TE: bool,
30    U: bool, V: bool, VE: bool, Z: bool, sctlr'rst: BitsN.nbit }
31
32type HSCTLR =
33  { A: bool, C: bool, CP15BEN: bool, EE: bool, FI: bool, I: bool, M: bool,
34    TE: bool, WXN: bool, hsctlr'rst: BitsN.nbit }
35
36type HSR = { EC: BitsN.nbit, IL: bool, ISS: BitsN.nbit }
37
38type SCR =
39  { AW: bool, EA: bool, FIQ: bool, FW: bool, HCE: bool, IRQ: bool,
40    NS: bool, SCD: bool, SIF: bool, nET: bool, scr'rst: BitsN.nbit }
41
42type NSACR =
43  { NSASEDIS: bool, NSD32DIS: bool, NSTRCDIS: bool, RFR: bool,
44    cp: BitsN.nbit, nsacr'rst: BitsN.nbit }
45
46type HCR =
47  { AMO: bool, BSU: BitsN.nbit, DC: bool, FB: bool, FMO: bool, IMO: bool,
48    PTW: bool, SWIO: bool, TAC: bool, TGE: bool, TID: BitsN.nbit,
49    TIDCP: bool, TPC: bool, TPU: bool, TSC: bool, TSW: bool, TTLB: bool,
50    TVM: bool, TWE: bool, TWI: bool, VA: bool, VF: bool, VI: bool,
51    VM: bool, hcr'rst: BitsN.nbit }
52
53type CP15 =
54  { HCR: HCR, HSCTLR: HSCTLR, HSR: HSR, MVBAR: BitsN.nbit, NSACR: NSACR,
55    SCR: SCR, SCTLR: SCTLR, VBAR: BitsN.nbit }
56
57datatype InstrSet
58  = InstrSet_ARM | InstrSet_Thumb | InstrSet_Jazelle | InstrSet_ThumbEE
59
60datatype Encoding = Encoding_Thumb | Encoding_Thumb2 | Encoding_ARM
61
62datatype RName
63  = RName_0usr | RName_1usr | RName_2usr | RName_3usr | RName_4usr
64  | RName_5usr | RName_6usr | RName_7usr | RName_8usr | RName_8fiq
65  | RName_9usr | RName_9fiq | RName_10usr | RName_10fiq | RName_11usr
66  | RName_11fiq | RName_12usr | RName_12fiq | RName_SPusr | RName_SPfiq
67  | RName_SPirq | RName_SPsvc | RName_SPabt | RName_SPund | RName_SPmon
68  | RName_SPhyp | RName_LRusr | RName_LRfiq | RName_LRirq | RName_LRsvc
69  | RName_LRabt | RName_LRund | RName_LRmon | RName_PC
70
71datatype SRType
72  = SRType_LSL | SRType_LSR | SRType_ASR | SRType_ROR | SRType_RRX
73
74datatype offset1
75  = immediate_form1 of BitsN.nbit
76  | register_form1 of BitsN.nbit * (SRType * Nat.nat)
77
78datatype offset2
79  = immediate_form2 of BitsN.nbit | register_form2 of BitsN.nbit
80
81datatype VFPExtension = NoVFP | VFPv2 | VFPv3 | VFPv4
82
83type FPSCR =
84  { AHP: bool, C: bool, DN: bool, DZC: bool, DZE: bool, FZ: bool,
85    IDC: bool, IDE: bool, IOC: bool, IOE: bool, IXC: bool, IXE: bool,
86    N: bool, OFC: bool, OFE: bool, QC: bool, RMode: BitsN.nbit, UFC: bool,
87    UFE: bool, V: bool, Z: bool, fpscr'rst: BitsN.nbit }
88
89type FP = { FPSCR: FPSCR, REG: BitsN.nbit Map.map }
90
91datatype VFPNegMul = VFPNegMul_VNMLA | VFPNegMul_VNMLS | VFPNegMul_VNMUL
92
93datatype VFP
94  = vabs of bool * (BitsN.nbit * BitsN.nbit)
95  | vadd of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
96  | vcmp of bool * (BitsN.nbit * (BitsN.nbit option))
97  | vcvt_float of bool * (BitsN.nbit * BitsN.nbit)
98  | vcvt_from_integer of bool * (bool * (BitsN.nbit * BitsN.nbit))
99  | vcvt_to_integer of bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))
100  | vdiv of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
101  | vfma_vfms of bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
102  | vfnma_vfnms of
103      bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
104  | vldm of
105      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
106  | vldr of bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
107  | vmla_vmls of bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
108  | vmov of bool * (BitsN.nbit * BitsN.nbit)
109  | vmov_double of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
110  | vmov_imm of bool * (BitsN.nbit * BitsN.nbit)
111  | vmov_single of bool * (BitsN.nbit * BitsN.nbit)
112  | vmov_two_singles of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
113  | vmrs of BitsN.nbit
114  | vmsr of BitsN.nbit
115  | vmul of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
116  | vneg of bool * (BitsN.nbit * BitsN.nbit)
117  | vneg_mul of
118      bool * (VFPNegMul * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
119  | vsqrt of bool * (BitsN.nbit * BitsN.nbit)
120  | vstm of
121      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
122  | vstr of bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
123  | vsub of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
124
125datatype Hint
126  = Breakpoint of BitsN.nbit
127  | DataMemoryBarrier of BitsN.nbit
128  | DataSynchronizationBarrier of BitsN.nbit
129  | Debug of BitsN.nbit
130  | InstructionSynchronizationBarrier of BitsN.nbit
131  | PreloadData of bool * (bool * (BitsN.nbit * offset1))
132  | PreloadDataLiteral of bool * BitsN.nbit
133  | PreloadInstruction of bool * (BitsN.nbit * offset1)
134  | SendEvent
135  | WaitForEvent
136  | WaitForInterrupt
137  | Yield
138
139datatype System
140  = ChangeProcessorState of
141      bool * (bool * (bool * (bool * (bool * (BitsN.nbit option)))))
142  | EnterxLeavex of bool
143  | ExceptionReturn
144  | HypervisorCall of BitsN.nbit
145  | MoveToBankedOrSpecialRegister of bool * (BitsN.nbit * BitsN.nbit)
146  | MoveToRegisterFromBankedOrSpecial of bool * (BitsN.nbit * BitsN.nbit)
147  | MoveToRegisterFromSpecial of bool * BitsN.nbit
148  | MoveToSpecialFromImmediate of bool * (BitsN.nbit * BitsN.nbit)
149  | MoveToSpecialFromRegister of bool * (BitsN.nbit * BitsN.nbit)
150  | ReturnFromException of bool * (bool * (bool * BitsN.nbit))
151  | SecureMonitorCall of BitsN.nbit
152  | Setend of bool
153  | StoreReturnState of bool * (bool * (bool * BitsN.nbit))
154  | SupervisorCall of BitsN.nbit
155
156datatype Store
157  = StoreByte of
158      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))
159  | StoreByteUnprivileged of
160      bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))
161  | StoreDual of
162      bool *
163      (bool *
164       (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * offset2)))))
165  | StoreExclusive of
166      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
167  | StoreExclusiveByte of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
168  | StoreExclusiveDoubleword of
169      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
170  | StoreExclusiveHalf of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
171  | StoreHalf of
172      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))
173  | StoreHalfUnprivileged of
174      bool * (bool * (BitsN.nbit * (BitsN.nbit * offset2)))
175  | StoreMultiple of bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))
176  | StoreMultipleUserRegisters of
177      bool * (bool * (BitsN.nbit * BitsN.nbit))
178  | StoreUnprivileged of
179      bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))
180  | StoreWord of
181      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))
182
183datatype Load
184  = LoadByte of
185      bool *
186      (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))))
187  | LoadByteLiteral of bool * (bool * (BitsN.nbit * BitsN.nbit))
188  | LoadByteUnprivileged of
189      bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))
190  | LoadDual of
191      bool *
192      (bool *
193       (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * offset2)))))
194  | LoadDualLiteral of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
195  | LoadExclusive of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
196  | LoadExclusiveByte of BitsN.nbit * BitsN.nbit
197  | LoadExclusiveDoubleword of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
198  | LoadExclusiveHalf of BitsN.nbit * BitsN.nbit
199  | LoadHalf of
200      bool *
201      (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))))
202  | LoadHalfLiteral of bool * (bool * (BitsN.nbit * BitsN.nbit))
203  | LoadHalfUnprivileged of
204      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset2))))
205  | LoadLiteral of bool * (BitsN.nbit * BitsN.nbit)
206  | LoadMultiple of bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))
207  | LoadMultipleExceptionReturn of
208      bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))
209  | LoadMultipleUserRegisters of bool * (bool * (BitsN.nbit * BitsN.nbit))
210  | LoadSignedByteUnprivileged of
211      bool * (bool * (BitsN.nbit * (BitsN.nbit * offset2)))
212  | LoadUnprivileged of
213      bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))
214  | LoadWord of
215      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))
216
217datatype Media
218  = BitFieldClearOrInsert of
219      BitsN.nbit * (BitsN.nbit * (Nat.nat * Nat.nat))
220  | BitFieldExtract of
221      bool * (BitsN.nbit * (BitsN.nbit * (Nat.nat * Nat.nat)))
222  | ByteReverse of BitsN.nbit * BitsN.nbit
223  | ByteReversePackedHalfword of BitsN.nbit * BitsN.nbit
224  | ByteReverseSignedHalfword of BitsN.nbit * BitsN.nbit
225  | ExtendByte of
226      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat)))
227  | ExtendByte16 of
228      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat)))
229  | ExtendHalfword of
230      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat)))
231  | PackHalfword of
232      SRType *
233      (Nat.nat * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
234  | ReverseBits of BitsN.nbit * BitsN.nbit
235  | Saturate of
236      SRType * (Nat.nat * (Nat.nat * (bool * (BitsN.nbit * BitsN.nbit))))
237  | Saturate16 of Nat.nat * (bool * (BitsN.nbit * BitsN.nbit))
238  | SaturatingAddSubtract of
239      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
240  | SelectBytes of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
241
242datatype SIMD
243  = SignedAddSub16 of
244      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
245  | SignedAddSub8 of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
246  | SignedHalvingAddSub16 of
247      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
248  | SignedHalvingAddSub8 of
249      bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
250  | SignedSaturatingAddSub16 of
251      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
252  | SignedSaturatingAddSub8 of
253      bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
254  | UnsignedAddSub16 of
255      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
256  | UnsignedAddSub8 of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
257  | UnsignedHalvingAddSub16 of
258      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
259  | UnsignedHalvingAddSub8 of
260      bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
261  | UnsignedSaturatingAddSub16 of
262      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
263  | UnsignedSaturatingAddSub8 of
264      bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
265  | UnsignedSumAbsoluteDifferences of
266      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
267
268datatype Multiply
269  = Multiply32 of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
270  | MultiplyAccumulate of
271      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
272  | MultiplyAccumulateAccumulate of
273      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
274  | MultiplyLong of
275      bool *
276      (bool *
277       (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))
278  | MultiplySubtract of
279      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
280  | Signed16Multiply32Accumulate of
281      bool *
282      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
283  | Signed16Multiply32Result of
284      bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
285  | Signed16Multiply64Accumulate of
286      bool *
287      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
288  | Signed16x32Multiply32Accumulate of
289      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
290  | Signed16x32Multiply32Result of
291      bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
292  | SignedMostSignificantMultiply of
293      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
294  | SignedMostSignificantMultiplySubtract of
295      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
296  | SignedMultiplyDual of
297      bool *
298      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
299  | SignedMultiplyLongDual of
300      bool *
301      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
302
303datatype Data
304  = AddSub of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
305  | ArithLogicImmediate of
306      BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
307  | CountLeadingZeroes of BitsN.nbit * BitsN.nbit
308  | Move of bool * (bool * (BitsN.nbit * BitsN.nbit))
309  | MoveHalfword of bool * (BitsN.nbit * BitsN.nbit)
310  | Register of
311      BitsN.nbit *
312      (bool *
313       (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))))
314  | RegisterShiftedRegister of
315      BitsN.nbit *
316      (bool *
317       (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit)))))
318  | ShiftImmediate of
319      bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat))))
320  | ShiftRegister of
321      bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit))))
322  | TestCompareImmediate of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
323  | TestCompareRegister of
324      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))
325
326datatype Branch
327  = BranchExchange of BitsN.nbit
328  | BranchLinkExchangeImmediate of InstrSet * BitsN.nbit
329  | BranchLinkExchangeRegister of BitsN.nbit
330  | BranchTarget of BitsN.nbit
331  | CheckArray of BitsN.nbit * BitsN.nbit
332  | CompareBranch of bool * (BitsN.nbit * BitsN.nbit)
333  | HandlerBranchLink of bool * BitsN.nbit
334  | HandlerBranchLinkParameter of BitsN.nbit * BitsN.nbit
335  | HandlerBranchParameter of BitsN.nbit * BitsN.nbit
336  | TableBranchByte of bool * (BitsN.nbit * BitsN.nbit)
337
338datatype instruction
339  = Branch of Branch
340  | ClearExclusive
341  | Data of Data
342  | Divide of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
343  | Hint of Hint
344  | IfThen of BitsN.nbit * BitsN.nbit
345  | Load of Load
346  | Media of Media
347  | Multiply of Multiply
348  | NoOperation
349  | SIMD of SIMD
350  | Store of Store
351  | Swap of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
352  | System of System
353  | Undefined of BitsN.nbit
354  | VFP of VFP
355
356datatype MachineCode
357  = ARM of BitsN.nbit
358  | BadCode of string
359  | Thumb of BitsN.nbit
360  | Thumb2 of BitsN.nbit * BitsN.nbit
361  | ThumbEE of BitsN.nbit
362
363datatype enc = Enc_ARM | Enc_Thumb | Enc_Narrow | Enc_Wide
364
365datatype maybe_instruction
366  = FAIL of string
367  | OK of (BitsN.nbit * string) * instruction
368  | PENDING of string * ((BitsN.nbit * string) * instruction)
369  | WORD of BitsN.nbit
370
371datatype nat_or_reg = NAT of Nat.nat | REGISTER of BitsN.nbit
372
373(* -------------------------------------------------------------------------
374   Exceptions
375   ------------------------------------------------------------------------- *)
376
377exception ASSERT of string
378
379exception AlignmentFault of BitsN.nbit
380
381exception IMPLEMENTATION_DEFINED of string
382
383exception UNPREDICTABLE of string
384
385exception VFP_EXCEPTION of string
386
387(* -------------------------------------------------------------------------
388   Functions
389   ------------------------------------------------------------------------- *)
390
391structure Cast:
392sig
393
394val natToArchitecture: Nat.nat -> Architecture
395val ArchitectureToNat: Architecture -> Nat.nat
396val stringToArchitecture: string -> Architecture
397val ArchitectureToString: Architecture -> string
398val natToExtensions: Nat.nat -> Extensions
399val ExtensionsToNat: Extensions -> Nat.nat
400val stringToExtensions: string -> Extensions
401val ExtensionsToString: Extensions -> string
402val natToInstrSet: Nat.nat -> InstrSet
403val InstrSetToNat: InstrSet -> Nat.nat
404val stringToInstrSet: string -> InstrSet
405val InstrSetToString: InstrSet -> string
406val natToEncoding: Nat.nat -> Encoding
407val EncodingToNat: Encoding -> Nat.nat
408val stringToEncoding: string -> Encoding
409val EncodingToString: Encoding -> string
410val natToRName: Nat.nat -> RName
411val RNameToNat: RName -> Nat.nat
412val stringToRName: string -> RName
413val RNameToString: RName -> string
414val natToSRType: Nat.nat -> SRType
415val SRTypeToNat: SRType -> Nat.nat
416val stringToSRType: string -> SRType
417val SRTypeToString: SRType -> string
418val natToVFPExtension: Nat.nat -> VFPExtension
419val VFPExtensionToNat: VFPExtension -> Nat.nat
420val stringToVFPExtension: string -> VFPExtension
421val VFPExtensionToString: VFPExtension -> string
422val natToVFPNegMul: Nat.nat -> VFPNegMul
423val VFPNegMulToNat: VFPNegMul -> Nat.nat
424val stringToVFPNegMul: string -> VFPNegMul
425val VFPNegMulToString: VFPNegMul -> string
426val natToenc: Nat.nat -> enc
427val encToNat: enc -> Nat.nat
428val stringToenc: string -> enc
429val encToString: enc -> string
430
431end
432
433val Architecture: Architecture ref
434val CP14: CP14 ref
435val CP15: CP15 ref
436val CPSR: PSR ref
437val CurrentCondition: BitsN.nbit ref
438val ELR_hyp: BitsN.nbit ref
439val Encoding: Encoding ref
440val Extensions: (Extensions list) ref
441val FP: FP ref
442val MEM: (BitsN.nbit Map.map) ref
443val REG: (BitsN.nbit Map.map) ref
444val SPSR_abt: PSR ref
445val SPSR_fiq: PSR ref
446val SPSR_hyp: PSR ref
447val SPSR_irq: PSR ref
448val SPSR_mon: PSR ref
449val SPSR_svc: PSR ref
450val SPSR_und: PSR ref
451val VFPExtension: VFPExtension ref
452val undefined: bool ref
453val PSR_A_rupd: PSR * bool -> PSR
454val PSR_C_rupd: PSR * bool -> PSR
455val PSR_E_rupd: PSR * bool -> PSR
456val PSR_F_rupd: PSR * bool -> PSR
457val PSR_GE_rupd: PSR * BitsN.nbit -> PSR
458val PSR_I_rupd: PSR * bool -> PSR
459val PSR_IT_rupd: PSR * BitsN.nbit -> PSR
460val PSR_J_rupd: PSR * bool -> PSR
461val PSR_M_rupd: PSR * BitsN.nbit -> PSR
462val PSR_N_rupd: PSR * bool -> PSR
463val PSR_Q_rupd: PSR * bool -> PSR
464val PSR_T_rupd: PSR * bool -> PSR
465val PSR_V_rupd: PSR * bool -> PSR
466val PSR_Z_rupd: PSR * bool -> PSR
467val PSR_psr'rst_rupd: PSR * BitsN.nbit -> PSR
468val CP14_TEEHBR_rupd: CP14 * BitsN.nbit -> CP14
469val SCTLR_A_rupd: SCTLR * bool -> SCTLR
470val SCTLR_B_rupd: SCTLR * bool -> SCTLR
471val SCTLR_BR_rupd: SCTLR * bool -> SCTLR
472val SCTLR_C_rupd: SCTLR * bool -> SCTLR
473val SCTLR_DZ_rupd: SCTLR * bool -> SCTLR
474val SCTLR_EE_rupd: SCTLR * bool -> SCTLR
475val SCTLR_FI_rupd: SCTLR * bool -> SCTLR
476val SCTLR_I_rupd: SCTLR * bool -> SCTLR
477val SCTLR_IE_rupd: SCTLR * bool -> SCTLR
478val SCTLR_M_rupd: SCTLR * bool -> SCTLR
479val SCTLR_NMFI_rupd: SCTLR * bool -> SCTLR
480val SCTLR_RR_rupd: SCTLR * bool -> SCTLR
481val SCTLR_SW_rupd: SCTLR * bool -> SCTLR
482val SCTLR_TE_rupd: SCTLR * bool -> SCTLR
483val SCTLR_U_rupd: SCTLR * bool -> SCTLR
484val SCTLR_V_rupd: SCTLR * bool -> SCTLR
485val SCTLR_VE_rupd: SCTLR * bool -> SCTLR
486val SCTLR_Z_rupd: SCTLR * bool -> SCTLR
487val SCTLR_sctlr'rst_rupd: SCTLR * BitsN.nbit -> SCTLR
488val HSCTLR_A_rupd: HSCTLR * bool -> HSCTLR
489val HSCTLR_C_rupd: HSCTLR * bool -> HSCTLR
490val HSCTLR_CP15BEN_rupd: HSCTLR * bool -> HSCTLR
491val HSCTLR_EE_rupd: HSCTLR * bool -> HSCTLR
492val HSCTLR_FI_rupd: HSCTLR * bool -> HSCTLR
493val HSCTLR_I_rupd: HSCTLR * bool -> HSCTLR
494val HSCTLR_M_rupd: HSCTLR * bool -> HSCTLR
495val HSCTLR_TE_rupd: HSCTLR * bool -> HSCTLR
496val HSCTLR_WXN_rupd: HSCTLR * bool -> HSCTLR
497val HSCTLR_hsctlr'rst_rupd: HSCTLR * BitsN.nbit -> HSCTLR
498val HSR_EC_rupd: HSR * BitsN.nbit -> HSR
499val HSR_IL_rupd: HSR * bool -> HSR
500val HSR_ISS_rupd: HSR * BitsN.nbit -> HSR
501val SCR_AW_rupd: SCR * bool -> SCR
502val SCR_EA_rupd: SCR * bool -> SCR
503val SCR_FIQ_rupd: SCR * bool -> SCR
504val SCR_FW_rupd: SCR * bool -> SCR
505val SCR_HCE_rupd: SCR * bool -> SCR
506val SCR_IRQ_rupd: SCR * bool -> SCR
507val SCR_NS_rupd: SCR * bool -> SCR
508val SCR_SCD_rupd: SCR * bool -> SCR
509val SCR_SIF_rupd: SCR * bool -> SCR
510val SCR_nET_rupd: SCR * bool -> SCR
511val SCR_scr'rst_rupd: SCR * BitsN.nbit -> SCR
512val NSACR_NSASEDIS_rupd: NSACR * bool -> NSACR
513val NSACR_NSD32DIS_rupd: NSACR * bool -> NSACR
514val NSACR_NSTRCDIS_rupd: NSACR * bool -> NSACR
515val NSACR_RFR_rupd: NSACR * bool -> NSACR
516val NSACR_cp_rupd: NSACR * BitsN.nbit -> NSACR
517val NSACR_nsacr'rst_rupd: NSACR * BitsN.nbit -> NSACR
518val HCR_AMO_rupd: HCR * bool -> HCR
519val HCR_BSU_rupd: HCR * BitsN.nbit -> HCR
520val HCR_DC_rupd: HCR * bool -> HCR
521val HCR_FB_rupd: HCR * bool -> HCR
522val HCR_FMO_rupd: HCR * bool -> HCR
523val HCR_IMO_rupd: HCR * bool -> HCR
524val HCR_PTW_rupd: HCR * bool -> HCR
525val HCR_SWIO_rupd: HCR * bool -> HCR
526val HCR_TAC_rupd: HCR * bool -> HCR
527val HCR_TGE_rupd: HCR * bool -> HCR
528val HCR_TID_rupd: HCR * BitsN.nbit -> HCR
529val HCR_TIDCP_rupd: HCR * bool -> HCR
530val HCR_TPC_rupd: HCR * bool -> HCR
531val HCR_TPU_rupd: HCR * bool -> HCR
532val HCR_TSC_rupd: HCR * bool -> HCR
533val HCR_TSW_rupd: HCR * bool -> HCR
534val HCR_TTLB_rupd: HCR * bool -> HCR
535val HCR_TVM_rupd: HCR * bool -> HCR
536val HCR_TWE_rupd: HCR * bool -> HCR
537val HCR_TWI_rupd: HCR * bool -> HCR
538val HCR_VA_rupd: HCR * bool -> HCR
539val HCR_VF_rupd: HCR * bool -> HCR
540val HCR_VI_rupd: HCR * bool -> HCR
541val HCR_VM_rupd: HCR * bool -> HCR
542val HCR_hcr'rst_rupd: HCR * BitsN.nbit -> HCR
543val CP15_HCR_rupd: CP15 * HCR -> CP15
544val CP15_HSCTLR_rupd: CP15 * HSCTLR -> CP15
545val CP15_HSR_rupd: CP15 * HSR -> CP15
546val CP15_MVBAR_rupd: CP15 * BitsN.nbit -> CP15
547val CP15_NSACR_rupd: CP15 * NSACR -> CP15
548val CP15_SCR_rupd: CP15 * SCR -> CP15
549val CP15_SCTLR_rupd: CP15 * SCTLR -> CP15
550val CP15_VBAR_rupd: CP15 * BitsN.nbit -> CP15
551val FPSCR_AHP_rupd: FPSCR * bool -> FPSCR
552val FPSCR_C_rupd: FPSCR * bool -> FPSCR
553val FPSCR_DN_rupd: FPSCR * bool -> FPSCR
554val FPSCR_DZC_rupd: FPSCR * bool -> FPSCR
555val FPSCR_DZE_rupd: FPSCR * bool -> FPSCR
556val FPSCR_FZ_rupd: FPSCR * bool -> FPSCR
557val FPSCR_IDC_rupd: FPSCR * bool -> FPSCR
558val FPSCR_IDE_rupd: FPSCR * bool -> FPSCR
559val FPSCR_IOC_rupd: FPSCR * bool -> FPSCR
560val FPSCR_IOE_rupd: FPSCR * bool -> FPSCR
561val FPSCR_IXC_rupd: FPSCR * bool -> FPSCR
562val FPSCR_IXE_rupd: FPSCR * bool -> FPSCR
563val FPSCR_N_rupd: FPSCR * bool -> FPSCR
564val FPSCR_OFC_rupd: FPSCR * bool -> FPSCR
565val FPSCR_OFE_rupd: FPSCR * bool -> FPSCR
566val FPSCR_QC_rupd: FPSCR * bool -> FPSCR
567val FPSCR_RMode_rupd: FPSCR * BitsN.nbit -> FPSCR
568val FPSCR_UFC_rupd: FPSCR * bool -> FPSCR
569val FPSCR_UFE_rupd: FPSCR * bool -> FPSCR
570val FPSCR_V_rupd: FPSCR * bool -> FPSCR
571val FPSCR_Z_rupd: FPSCR * bool -> FPSCR
572val FPSCR_fpscr'rst_rupd: FPSCR * BitsN.nbit -> FPSCR
573val FP_FPSCR_rupd: FP * FPSCR -> FP
574val FP_REG_rupd: FP * (BitsN.nbit Map.map) -> FP
575val boolify'5: BitsN.nbit -> bool * (bool * (bool * (bool * bool)))
576val boolify'16:
577  BitsN.nbit ->
578  bool *
579  (bool *
580   (bool *
581    (bool *
582     (bool *
583      (bool *
584       (bool *
585        (bool *
586         (bool *
587          (bool * (bool * (bool * (bool * (bool * (bool * bool))))))))))))))
588val boolify'4: BitsN.nbit -> bool * (bool * (bool * bool))
589val boolify'28:
590  BitsN.nbit ->
591  bool *
592  (bool *
593   (bool *
594    (bool *
595     (bool *
596      (bool *
597       (bool *
598        (bool *
599         (bool *
600          (bool *
601           (bool *
602            (bool *
603             (bool *
604              (bool *
605               (bool *
606                (bool *
607                 (bool *
608                  (bool *
609                   (bool *
610                    (bool *
611                     (bool *
612                      (bool *
613                       (bool * (bool * (bool * (bool * (bool * bool))))))))))))))))))))))))))
614val boolify'3: BitsN.nbit -> bool * (bool * bool)
615val boolify'8:
616  BitsN.nbit ->
617  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
618val ArchVersion: unit -> Nat.nat
619val HaveDSPSupport: unit -> bool
620val HaveThumb2: unit -> bool
621val HaveThumbEE: unit -> bool
622val HaveMPExt: unit -> bool
623val HaveSecurityExt: unit -> bool
624val HaveVirtExt: unit -> bool
625val rec'PSR: BitsN.nbit -> PSR
626val reg'PSR: PSR -> BitsN.nbit
627val write'rec'PSR: (BitsN.nbit * PSR) -> BitsN.nbit
628val write'reg'PSR: (PSR * BitsN.nbit) -> PSR
629val rec'SCTLR: BitsN.nbit -> SCTLR
630val reg'SCTLR: SCTLR -> BitsN.nbit
631val write'rec'SCTLR: (BitsN.nbit * SCTLR) -> BitsN.nbit
632val write'reg'SCTLR: (SCTLR * BitsN.nbit) -> SCTLR
633val rec'HSCTLR: BitsN.nbit -> HSCTLR
634val reg'HSCTLR: HSCTLR -> BitsN.nbit
635val write'rec'HSCTLR: (BitsN.nbit * HSCTLR) -> BitsN.nbit
636val write'reg'HSCTLR: (HSCTLR * BitsN.nbit) -> HSCTLR
637val rec'HSR: BitsN.nbit -> HSR
638val reg'HSR: HSR -> BitsN.nbit
639val write'rec'HSR: (BitsN.nbit * HSR) -> BitsN.nbit
640val write'reg'HSR: (HSR * BitsN.nbit) -> HSR
641val rec'SCR: BitsN.nbit -> SCR
642val reg'SCR: SCR -> BitsN.nbit
643val write'rec'SCR: (BitsN.nbit * SCR) -> BitsN.nbit
644val write'reg'SCR: (SCR * BitsN.nbit) -> SCR
645val rec'NSACR: BitsN.nbit -> NSACR
646val reg'NSACR: NSACR -> BitsN.nbit
647val write'rec'NSACR: (BitsN.nbit * NSACR) -> BitsN.nbit
648val write'reg'NSACR: (NSACR * BitsN.nbit) -> NSACR
649val rec'HCR: BitsN.nbit -> HCR
650val reg'HCR: HCR -> BitsN.nbit
651val write'rec'HCR: (BitsN.nbit * HCR) -> BitsN.nbit
652val write'reg'HCR: (HCR * BitsN.nbit) -> HCR
653val ProcessorID: unit -> IntInf.int
654val IsExternalAbort: unit -> bool
655val IsSecure: unit -> bool
656val UnalignedSupport: unit -> bool
657val BadMode: BitsN.nbit -> bool
658val CurrentModeIsNotUser: unit -> bool
659val CurrentModeIsUserOrSystem: unit -> bool
660val CurrentModeIsHyp: unit -> bool
661val IntegerZeroDivideTrappingEnabled: unit -> bool
662val ISETSTATE: unit -> BitsN.nbit
663val write'ISETSTATE: BitsN.nbit -> unit
664val CurrentInstrSet: unit -> InstrSet
665val SelectInstrSet: InstrSet -> unit
666val ITSTATE: unit -> BitsN.nbit
667val write'ITSTATE: BitsN.nbit -> unit
668val ITAdvance: unit -> unit
669val InITBlock: unit -> bool
670val LastInITBlock: unit -> bool
671val ThumbCondition: unit -> BitsN.nbit
672val BigEndian: unit -> bool
673val SetExclusiveMonitors: (BitsN.nbit * Nat.nat) -> unit
674val ExclusiveMonitorsPass: (BitsN.nbit * Nat.nat) -> bool
675val ClearExclusiveLocal: IntInf.int -> unit
676val CurrentCond: unit -> BitsN.nbit
677val ConditionPassed: unit -> bool
678val SPSR: unit -> PSR
679val write'SPSR: PSR -> unit
680val CPSRWriteByInstr: (BitsN.nbit * (BitsN.nbit * bool)) -> unit
681val SPSRWriteByInstr: (BitsN.nbit * BitsN.nbit) -> unit
682val RBankSelect:
683  (BitsN.nbit *
684   (RName *
685    (RName * (RName * (RName * (RName * (RName * (RName * RName)))))))) ->
686  RName
687val RfiqBankSelect: (BitsN.nbit * (RName * RName)) -> RName
688val LookUpRName: (BitsN.nbit * BitsN.nbit) -> RName
689val Rmode: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
690val write'Rmode: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
691val R: BitsN.nbit -> BitsN.nbit
692val write'R: (BitsN.nbit * BitsN.nbit) -> unit
693val SP: unit -> BitsN.nbit
694val write'SP: BitsN.nbit -> unit
695val LR: unit -> BitsN.nbit
696val write'LR: BitsN.nbit -> unit
697val PC: unit -> BitsN.nbit
698val BranchTo: BitsN.nbit -> unit
699val PCStoreValue: unit -> BitsN.nbit
700val BranchWritePC: BitsN.nbit -> unit
701val BXWritePC: BitsN.nbit -> unit
702val LoadWritePC: BitsN.nbit -> unit
703val ALUWritePC: BitsN.nbit -> unit
704val ThisInstrLength: unit -> Nat.nat
705val IncPC: unit -> unit
706val mem1: BitsN.nbit -> (bool list)
707val mem: (BitsN.nbit * Nat.nat) -> (bool list)
708val write'mem: ((bool list) * (BitsN.nbit * Nat.nat)) -> unit
709val BigEndianReverse: ((bool list) * Nat.nat) -> (bool list)
710val Align: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
711val Aligned: Nat.nat -> (BitsN.nbit * Nat.nat) -> bool
712val MemA_with_priv: Nat.nat ->
713  (BitsN.nbit * (Nat.nat * bool)) -> BitsN.nbit
714val write'MemA_with_priv: Nat.nat ->
715  (BitsN.nbit * (BitsN.nbit * (Nat.nat * bool))) -> unit
716val MemA_unpriv: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
717val write'MemA_unpriv: Nat.nat ->
718  (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit
719val MemA: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
720val write'MemA: Nat.nat -> (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit
721val MemU_with_priv: Nat.nat ->
722  (BitsN.nbit * (Nat.nat * bool)) -> BitsN.nbit
723val write'MemU_with_priv: Nat.nat ->
724  (BitsN.nbit * (BitsN.nbit * (Nat.nat * bool))) -> unit
725val MemU_unpriv: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
726val write'MemU_unpriv: Nat.nat ->
727  (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit
728val MemU: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
729val write'MemU: Nat.nat -> (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit
730val NullCheckIfThumbEE: BitsN.nbit -> bool
731val HighestSetBit: Nat.nat -> BitsN.nbit -> IntInf.int
732val CountLeadingZeroBits: Nat.nat -> BitsN.nbit -> Nat.nat
733val LowestSetBit: Nat.nat -> BitsN.nbit -> Nat.nat
734val BitCount: Nat.nat -> BitsN.nbit -> Nat.nat
735val SignExtendFrom: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
736val Extend: Nat.nat * Nat.nat -> (bool * BitsN.nbit) -> BitsN.nbit
737val UInt: Nat.nat -> BitsN.nbit -> IntInf.int
738val SignedSatQ: Nat.nat -> (IntInf.int * Nat.nat) -> (BitsN.nbit * bool)
739val UnsignedSatQ: Nat.nat -> (IntInf.int * Nat.nat) -> (BitsN.nbit * bool)
740val SatQ: Nat.nat ->
741  (IntInf.int * (Nat.nat * bool)) -> (BitsN.nbit * bool)
742val SignedSat: Nat.nat -> (IntInf.int * Nat.nat) -> BitsN.nbit
743val UnsignedSat: Nat.nat -> (IntInf.int * Nat.nat) -> BitsN.nbit
744val LSL_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool)
745val LSL: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
746val LSR_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool)
747val LSR: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
748val ASR_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool)
749val ASR: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
750val ROR_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool)
751val ROR: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
752val RRX_C: Nat.nat -> (BitsN.nbit * bool) -> (BitsN.nbit * bool)
753val RRX: Nat.nat -> (BitsN.nbit * bool) -> BitsN.nbit
754val DecodeImmShift: (BitsN.nbit * BitsN.nbit) -> (SRType * Nat.nat)
755val DecodeRegShift: BitsN.nbit -> SRType
756val Shift_C: Nat.nat ->
757  (BitsN.nbit * (SRType * (Nat.nat * bool))) -> (BitsN.nbit * bool)
758val Shift: Nat.nat ->
759  (BitsN.nbit * (SRType * (Nat.nat * bool))) -> BitsN.nbit
760val ARMExpandImm_C: (BitsN.nbit * bool) -> (BitsN.nbit * bool)
761val ARMExpandImm: BitsN.nbit -> BitsN.nbit
762val ThumbExpandImm_C: (BitsN.nbit * bool) -> (BitsN.nbit * bool)
763val ExpandImm_C: (BitsN.nbit * bool) -> (BitsN.nbit * bool)
764val AddWithCarry: Nat.nat ->
765  (BitsN.nbit * (BitsN.nbit * bool)) -> (BitsN.nbit * (bool * bool))
766val DataProcessingALU:
767  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))) ->
768  (BitsN.nbit * (bool * bool))
769val ArithmeticOpcode: BitsN.nbit -> bool
770val ExcVectorBase: unit -> BitsN.nbit
771val EnterMonitorMode: (PSR * (BitsN.nbit * BitsN.nbit)) -> unit
772val EnterHypMode: (PSR * (BitsN.nbit * BitsN.nbit)) -> unit
773val TakeReset: unit -> unit
774val TakeUndefInstrException: unit -> unit
775val TakeSVCException: unit -> unit
776val TakeSMCException: unit -> unit
777val TakeHVCException: unit -> unit
778val TakeDataAbortException: unit -> unit
779val TakePrefetchAbortException: unit -> unit
780val TakePhysicalIRQException: unit -> unit
781val TakeVirtualIRQException: unit -> unit
782val TakePhysicalFIQException: unit -> unit
783val TakeVirtualFIQException: unit -> unit
784val TakeHypTrapException: unit -> unit
785val WriteHSR: (BitsN.nbit * BitsN.nbit) -> unit
786val CallSupervisor: BitsN.nbit -> unit
787val CallHypervisor: BitsN.nbit -> unit
788val BankedRegisterAccessValid: (BitsN.nbit * BitsN.nbit) -> unit
789val SPSRAccessValid: (BitsN.nbit * BitsN.nbit) -> unit
790val dfn'BranchTarget: BitsN.nbit -> unit
791val dfn'BranchExchange: BitsN.nbit -> unit
792val dfn'BranchLinkExchangeImmediate: (InstrSet * BitsN.nbit) -> unit
793val dfn'BranchLinkExchangeRegister: BitsN.nbit -> unit
794val dfn'CompareBranch: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
795val dfn'TableBranchByte: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
796val dfn'CheckArray: (BitsN.nbit * BitsN.nbit) -> unit
797val dfn'HandlerBranchLink: (bool * BitsN.nbit) -> unit
798val dfn'HandlerBranchLinkParameter: (BitsN.nbit * BitsN.nbit) -> unit
799val dfn'HandlerBranchParameter: (BitsN.nbit * BitsN.nbit) -> unit
800val dfn'EnterxLeavex: bool -> unit
801val dfn'IfThen: (BitsN.nbit * BitsN.nbit) -> unit
802val dfn'CountLeadingZeroes: (BitsN.nbit * BitsN.nbit) -> unit
803val dfn'MoveHalfword: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
804val DataProcessing:
805  (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))))) ->
806  unit
807val DataProcessingPC:
808  (BitsN.nbit * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
809val dfn'Move: (bool * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
810val dfn'TestCompareImmediate:
811  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
812val dfn'ArithLogicImmediate:
813  (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
814val doRegister:
815  (BitsN.nbit *
816   (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))))) ->
817  unit
818val dfn'Register:
819  (BitsN.nbit *
820   (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))))) ->
821  unit
822val dfn'TestCompareRegister:
823  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))) -> unit
824val dfn'ShiftImmediate:
825  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat))))) ->
826  unit
827val doRegisterShiftedRegister:
828  (BitsN.nbit *
829   (bool *
830    (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit)))))) ->
831  unit
832val dfn'RegisterShiftedRegister:
833  (BitsN.nbit *
834   (bool *
835    (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit)))))) ->
836  unit
837val dfn'ShiftRegister:
838  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit))))) ->
839  unit
840val dfn'AddSub: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
841val dfn'SaturatingAddSubtract:
842  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
843val dfn'Multiply32:
844  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
845val dfn'MultiplyAccumulate:
846  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
847val dfn'MultiplyLong:
848  (bool *
849   (bool *
850    (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))) ->
851  unit
852val dfn'MultiplyAccumulateAccumulate:
853  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
854val dfn'MultiplySubtract:
855  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
856val dfn'Signed16Multiply32Accumulate:
857  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
858  unit
859val dfn'Signed16Multiply32Result:
860  (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
861val dfn'Signed16x32Multiply32Accumulate:
862  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
863val dfn'Signed16x32Multiply32Result:
864  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
865val dfn'Signed16Multiply64Accumulate:
866  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
867  unit
868val dfn'SignedMultiplyDual:
869  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
870  unit
871val dfn'SignedMultiplyLongDual:
872  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
873  unit
874val dfn'SignedMostSignificantMultiply:
875  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
876val dfn'SignedMostSignificantMultiplySubtract:
877  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
878val SignedParallelAddSub16:
879  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> (IntInf.int * IntInf.int)
880val dfn'SignedAddSub16:
881  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
882val dfn'SignedSaturatingAddSub16:
883  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
884val dfn'SignedHalvingAddSub16:
885  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
886val SignedParallelAddSub8:
887  (bool * (BitsN.nbit * BitsN.nbit)) ->
888  (IntInf.int * (IntInf.int * (IntInf.int * IntInf.int)))
889val dfn'SignedAddSub8:
890  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
891val dfn'SignedSaturatingAddSub8:
892  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
893val dfn'SignedHalvingAddSub8:
894  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
895val UnsignedParallelAddSub16:
896  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> (IntInf.int * IntInf.int)
897val dfn'UnsignedAddSub16:
898  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
899val dfn'UnsignedSaturatingAddSub16:
900  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
901val dfn'UnsignedHalvingAddSub16:
902  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
903val UnsignedParallelAddSub8:
904  (bool * (BitsN.nbit * BitsN.nbit)) ->
905  (IntInf.int * (IntInf.int * (IntInf.int * IntInf.int)))
906val dfn'UnsignedAddSub8:
907  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
908val dfn'UnsignedSaturatingAddSub8:
909  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
910val dfn'UnsignedHalvingAddSub8:
911  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
912val dfn'UnsignedSumAbsoluteDifferences:
913  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
914val GenerateIntegerZeroDivide: unit -> unit
915val dfn'Divide: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
916val dfn'PackHalfword:
917  (SRType * (Nat.nat * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
918  unit
919val dfn'Saturate:
920  (SRType * (Nat.nat * (Nat.nat * (bool * (BitsN.nbit * BitsN.nbit))))) ->
921  unit
922val dfn'Saturate16: (Nat.nat * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
923val dfn'ExtendByte:
924  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat)))) -> unit
925val dfn'ExtendByte16:
926  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat)))) -> unit
927val dfn'ExtendHalfword:
928  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat)))) -> unit
929val dfn'SelectBytes: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
930val dfn'ByteReverse: (BitsN.nbit * BitsN.nbit) -> unit
931val dfn'ByteReversePackedHalfword: (BitsN.nbit * BitsN.nbit) -> unit
932val dfn'ByteReverseSignedHalfword: (BitsN.nbit * BitsN.nbit) -> unit
933val dfn'ReverseBits: (BitsN.nbit * BitsN.nbit) -> unit
934val dfn'BitFieldExtract:
935  (bool * (BitsN.nbit * (BitsN.nbit * (Nat.nat * Nat.nat)))) -> unit
936val dfn'BitFieldClearOrInsert:
937  (BitsN.nbit * (BitsN.nbit * (Nat.nat * Nat.nat))) -> unit
938val dfn'LoadWord:
939  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))) -> unit
940val dfn'LoadLiteral: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
941val dfn'LoadUnprivileged:
942  (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))) -> unit
943val dfn'LoadByte:
944  (bool * (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))))) ->
945  unit
946val dfn'LoadByteLiteral:
947  (bool * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
948val dfn'LoadByteUnprivileged:
949  (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))) -> unit
950val dfn'LoadSignedByteUnprivileged:
951  (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset2)))) -> unit
952val dfn'LoadHalf:
953  (bool * (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))))) ->
954  unit
955val dfn'LoadHalfLiteral:
956  (bool * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
957val dfn'LoadHalfUnprivileged:
958  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset2))))) -> unit
959val dfn'LoadMultiple:
960  (bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))) -> unit
961val dfn'LoadMultipleExceptionReturn:
962  (bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))) -> unit
963val dfn'LoadMultipleUserRegisters:
964  (bool * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
965val dfn'LoadDual:
966  (bool *
967   (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * offset2)))))) ->
968  unit
969val dfn'LoadDualLiteral:
970  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
971val dfn'LoadExclusive: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
972val dfn'LoadExclusiveByte: (BitsN.nbit * BitsN.nbit) -> unit
973val dfn'LoadExclusiveHalf: (BitsN.nbit * BitsN.nbit) -> unit
974val dfn'LoadExclusiveDoubleword:
975  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
976val dfn'StoreWord:
977  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))) -> unit
978val dfn'StoreUnprivileged:
979  (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))) -> unit
980val dfn'StoreByte:
981  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))) -> unit
982val dfn'StoreByteUnprivileged:
983  (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))) -> unit
984val dfn'StoreHalf:
985  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))) -> unit
986val dfn'StoreHalfUnprivileged:
987  (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset2)))) -> unit
988val dfn'StoreMultiple:
989  (bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))) -> unit
990val dfn'StoreMultipleUserRegisters:
991  (bool * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
992val dfn'StoreDual:
993  (bool *
994   (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * offset2)))))) ->
995  unit
996val dfn'StoreExclusive:
997  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
998val dfn'StoreExclusiveByte:
999  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
1000val dfn'StoreExclusiveHalf:
1001  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
1002val dfn'StoreExclusiveDoubleword:
1003  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
1004val dfn'ClearExclusive: unit -> unit
1005val dfn'Swap: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
1006val dfn'ChangeProcessorState:
1007  (bool * (bool * (bool * (bool * (bool * (BitsN.nbit option)))))) -> unit
1008val dfn'ExceptionReturn: unit -> unit
1009val dfn'HypervisorCall: BitsN.nbit -> unit
1010val dfn'MoveToRegisterFromSpecial: (bool * BitsN.nbit) -> unit
1011val dfn'MoveToRegisterFromBankedOrSpecial:
1012  (bool * (BitsN.nbit * BitsN.nbit)) -> unit
1013val dfn'MoveToSpecialFromImmediate:
1014  (bool * (BitsN.nbit * BitsN.nbit)) -> unit
1015val dfn'MoveToSpecialFromRegister:
1016  (bool * (BitsN.nbit * BitsN.nbit)) -> unit
1017val dfn'MoveToBankedOrSpecialRegister:
1018  (bool * (BitsN.nbit * BitsN.nbit)) -> unit
1019val dfn'ReturnFromException: (bool * (bool * (bool * BitsN.nbit))) -> unit
1020val dfn'SecureMonitorCall: BitsN.nbit -> unit
1021val dfn'SupervisorCall: BitsN.nbit -> unit
1022val dfn'StoreReturnState: (bool * (bool * (bool * BitsN.nbit))) -> unit
1023val dfn'Setend: bool -> unit
1024val dfn'Undefined: BitsN.nbit -> unit
1025val dfn'NoOperation: unit -> unit
1026val dfn'Breakpoint: BitsN.nbit -> unit
1027val dfn'Debug: BitsN.nbit -> unit
1028val dfn'DataMemoryBarrier: BitsN.nbit -> unit
1029val dfn'DataSynchronizationBarrier: BitsN.nbit -> unit
1030val dfn'InstructionSynchronizationBarrier: BitsN.nbit -> unit
1031val dfn'PreloadData: (bool * (bool * (BitsN.nbit * offset1))) -> unit
1032val dfn'PreloadDataLiteral: (bool * BitsN.nbit) -> unit
1033val dfn'PreloadInstruction: (bool * (BitsN.nbit * offset1)) -> unit
1034val dfn'SendEvent: unit -> unit
1035val dfn'WaitForEvent: unit -> unit
1036val dfn'WaitForInterrupt: unit -> unit
1037val dfn'Yield: unit -> unit
1038val rec'FPSCR: BitsN.nbit -> FPSCR
1039val reg'FPSCR: FPSCR -> BitsN.nbit
1040val write'rec'FPSCR: (BitsN.nbit * FPSCR) -> BitsN.nbit
1041val write'reg'FPSCR: (FPSCR * BitsN.nbit) -> FPSCR
1042val RoundingMode: unit -> IEEEReal.rounding_mode
1043val FPAdd32: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
1044val FPSub32: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
1045val FPMul32: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
1046val FPAdd64: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
1047val FPSub64: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
1048val FPMul64: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
1049val FPToFixed32: (BitsN.nbit * (bool * bool)) -> BitsN.nbit
1050val FPToFixed64: (BitsN.nbit * (bool * bool)) -> BitsN.nbit
1051val FixedToFP32: (BitsN.nbit * (bool * bool)) -> BitsN.nbit
1052val FixedToFP64: (BitsN.nbit * (bool * bool)) -> BitsN.nbit
1053val D: BitsN.nbit -> BitsN.nbit
1054val write'D: (BitsN.nbit * BitsN.nbit) -> unit
1055val S: BitsN.nbit -> BitsN.nbit
1056val write'S: (BitsN.nbit * BitsN.nbit) -> unit
1057val VFPExpandImm: (BitsN.nbit * bool) -> BitsN.nbit
1058val FPCompare32: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
1059val FPCompare64: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
1060val FPZero32: BitsN.nbit -> BitsN.nbit
1061val FPZero64: BitsN.nbit -> BitsN.nbit
1062val dfn'vmov_imm: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
1063val dfn'vmov: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
1064val dfn'vmov_single: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
1065val dfn'vmov_two_singles:
1066  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
1067val dfn'vmov_double:
1068  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
1069val dfn'vabs: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
1070val dfn'vneg: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
1071val dfn'vsqrt: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
1072val dfn'vcvt_float: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
1073val dfn'vcvt_to_integer:
1074  (bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))) -> unit
1075val dfn'vcvt_from_integer:
1076  (bool * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
1077val dfn'vcmp: (bool * (BitsN.nbit * (BitsN.nbit option))) -> unit
1078val dfn'vmsr: BitsN.nbit -> unit
1079val dfn'vmrs: BitsN.nbit -> unit
1080val dfn'vadd: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
1081val dfn'vsub: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
1082val dfn'vmul: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
1083val dfn'vdiv: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
1084val dfn'vmla_vmls:
1085  (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
1086val dfn'vfma_vfms:
1087  (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
1088val dfn'vfnma_vfnms:
1089  (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
1090val dfn'vneg_mul:
1091  (bool * (VFPNegMul * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
1092val dfn'vldr:
1093  (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
1094val dfn'vstr:
1095  (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
1096val dfn'vldm:
1097  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
1098  unit
1099val dfn'vstm:
1100  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
1101  unit
1102val Run: instruction -> unit
1103val Fetch: unit -> MachineCode
1104val Do: (BitsN.nbit * bool) -> bool
1105val Skip: unit -> instruction
1106val UndefinedARM: BitsN.nbit -> instruction
1107val UndefinedThumb: unit -> instruction
1108val DECODE_UNPREDICTABLE: (MachineCode * string) -> unit
1109val DecodeHint: (BitsN.nbit * BitsN.nbit) -> instruction
1110val DecodeParallelAdditionSubtraction:
1111  (BitsN.nbit *
1112   (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
1113  instruction
1114val DecodeVFP: BitsN.nbit -> (bool * (string * instruction))
1115val DecodeARM: BitsN.nbit -> instruction
1116val DecodeThumb: BitsN.nbit -> instruction
1117val DecodeThumbEE: BitsN.nbit -> instruction
1118val DecodeThumb2: (BitsN.nbit * BitsN.nbit) -> instruction
1119val Decode: MachineCode -> instruction
1120val Next: unit -> unit
1121val EncodeThumbImmediate: BitsN.nbit -> (BitsN.nbit option)
1122val EncodeARMImmediate_aux:
1123  (BitsN.nbit * BitsN.nbit) -> (BitsN.nbit option)
1124val EncodeARMImmediate: BitsN.nbit -> (BitsN.nbit option)
1125val EncodeImmShift: (SRType * Nat.nat) -> (BitsN.nbit * BitsN.nbit)
1126val EncodeRegShift: SRType -> BitsN.nbit
1127val EncodeAddSubOpc: BitsN.nbit -> BitsN.nbit
1128val EncodeVFPImmediate: (BitsN.nbit * bool) -> (BitsN.nbit option)
1129val EncodeVFPReg: (BitsN.nbit * bool) -> (BitsN.nbit * BitsN.nbit)
1130val e_branch: (BitsN.nbit * (Branch * enc)) -> MachineCode
1131val e_vfp: (BitsN.nbit * (VFP * enc)) -> MachineCode
1132val e_data: (BitsN.nbit * (Data * enc)) -> MachineCode
1133val e_media: (BitsN.nbit * (Media * enc)) -> MachineCode
1134val e_hint: (BitsN.nbit * (Hint * enc)) -> MachineCode
1135val e_system: (BitsN.nbit * (System * enc)) -> MachineCode
1136val e_multiply: (BitsN.nbit * (Multiply * enc)) -> MachineCode
1137val e_simd: (BitsN.nbit * (SIMD * enc)) -> MachineCode
1138val e_load: (BitsN.nbit * (Load * enc)) -> MachineCode
1139val e_store: (BitsN.nbit * (Store * enc)) -> MachineCode
1140val instructionEncode: (BitsN.nbit * (instruction * enc)) -> MachineCode
1141val SetPassCondition: BitsN.nbit -> unit
1142val Encode: (BitsN.nbit * (instruction * enc)) -> MachineCode
1143val al: BitsN.nbit * string
1144val stripSpaces: string -> string
1145val p_number: string -> (Nat.nat option)
1146val p_signed_number: (bool * string) -> ((bool * Nat.nat) option)
1147val p_encode_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option)
1148val p_encode_signed_immediate: Nat.nat ->
1149  (bool * string) -> ((bool * (bool * BitsN.nbit)) option)
1150val p_encode_signed_immediate_offset: Nat.nat ->
1151  (bool * string) -> ((bool * (bool * BitsN.nbit)) option)
1152val p_encode_signed_offset: Nat.nat ->
1153  (bool * string) -> ((bool * BitsN.nbit) option)
1154val p_unbounded_immediate: string -> (Nat.nat option)
1155val p_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option)
1156val p_immediate_number: Nat.nat -> string -> ((bool * BitsN.nbit) option)
1157val p_signed_immediate: Nat.nat ->
1158  string -> ((bool * (bool * BitsN.nbit)) option)
1159val p_signed_offset: Nat.nat ->
1160  string -> ((bool * (bool * BitsN.nbit)) option)
1161val p_offset: Nat.nat -> string -> ((bool * BitsN.nbit) option)
1162val p_arm_immediate: string -> ((string * BitsN.nbit) option)
1163val p_arm_fp_immediate: (bool * string) -> ((string * BitsN.nbit) option)
1164val p_range_imm: (Nat.nat * (Nat.nat * string)) -> (string * Nat.nat)
1165val p_label: string -> (string option)
1166val p_cond: string -> (BitsN.nbit option)
1167val p_suffix: string -> ((BitsN.nbit * string) option)
1168val p_suffix2: string -> ((BitsN.nbit * (string * string)) option)
1169val p_register: string -> (BitsN.nbit option)
1170val p_register1: (string list) -> (BitsN.nbit option)
1171val p_register2: (string list) -> ((BitsN.nbit * BitsN.nbit) option)
1172val p_register3:
1173  (string list) -> ((BitsN.nbit * (BitsN.nbit * BitsN.nbit)) option)
1174val p_register4:
1175  (string list) ->
1176  ((BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) option)
1177val p_reg_offset: (bool * string) -> ((bool * BitsN.nbit) option)
1178val p_register_offset: string -> ((bool * BitsN.nbit) option)
1179val p_fp_register: (bool * string) -> (BitsN.nbit option)
1180val p_any_fp_register: (string * string) -> ((bool * BitsN.nbit) option)
1181val p_fp_register3:
1182  (bool * (string list)) ->
1183  ((BitsN.nbit * (BitsN.nbit * BitsN.nbit)) option)
1184val closingRegList: string -> ((bool * string) option)
1185val p_reg_list: (BitsN.nbit * string) -> (BitsN.nbit option)
1186val p_registers_loop:
1187  (BitsN.nbit * (string list)) -> ((bool * BitsN.nbit) option)
1188val p_registers: (string list) -> ((bool * BitsN.nbit) option)
1189val p_fp_reg_list: (bool * (BitsN.nbit * string)) -> (BitsN.nbit option)
1190val p_fp_registers_loop:
1191  (bool * (BitsN.nbit * (string list))) -> (BitsN.nbit option)
1192val fp_reg_list:
1193  (bool * BitsN.nbit) -> ((bool * (BitsN.nbit * BitsN.nbit)) option)
1194val p_fp_registers:
1195  (string list) -> ((bool * (BitsN.nbit * BitsN.nbit)) option)
1196val p_shift_amount:
1197  (SRType * (char * string)) -> (string * (SRType * nat_or_reg))
1198val p_shift_imm_or_reg: string -> (string * (SRType * nat_or_reg))
1199val p_rotation: string -> (string * Nat.nat)
1200val p_arith_logic_full:
1201  (string * (BitsN.nbit * (bool * (string list)))) -> maybe_instruction
1202val p_arith_logic:
1203  (string * (BitsN.nbit * (bool * (string list)))) -> maybe_instruction
1204val p_test_compare:
1205  (string * (BitsN.nbit * (string list))) -> maybe_instruction
1206val p_mov_mvn:
1207  (string * (bool * (bool * (string list)))) -> maybe_instruction
1208val p_shift_full:
1209  (string * (SRType * (bool * (string list)))) -> maybe_instruction
1210val p_shift:
1211  (string * (SRType * (bool * (string list)))) -> maybe_instruction
1212val p_rrx: (string * (bool * (string list))) -> maybe_instruction
1213val p_adr: (string * (string list)) -> maybe_instruction
1214val p_bx: (string * (string list)) -> maybe_instruction
1215val p_bl: (string * (string list)) -> maybe_instruction
1216val p_b: (string * (string list)) -> maybe_instruction
1217val p_blx: (string * (string list)) -> maybe_instruction
1218val p_clz: (string * (string list)) -> maybe_instruction
1219val p_movt_movw: (string * (bool * (string list))) -> maybe_instruction
1220val p_addw_subw: (string * (bool * (string list))) -> maybe_instruction
1221val p_mul: (string * (bool * (string list))) -> maybe_instruction
1222val p_mla: (string * (bool * (string list))) -> maybe_instruction
1223val p_umull_etc:
1224  (string * (bool * (bool * (bool * (string list))))) -> maybe_instruction
1225val p_umaal: (string * (string list)) -> maybe_instruction
1226val p_mls: (string * (string list)) -> maybe_instruction
1227val p_smla:
1228  (string * (bool * (bool * (string list)))) -> maybe_instruction
1229val p_smul:
1230  (string * (bool * (bool * (string list)))) -> maybe_instruction
1231val p_smlaw: (string * (bool * (string list))) -> maybe_instruction
1232val p_smulw: (string * (bool * (string list))) -> maybe_instruction
1233val p_smlal:
1234  (string * (bool * (bool * (string list)))) -> maybe_instruction
1235val p_smuad_smusd:
1236  (string * (bool * (bool * (string list)))) -> maybe_instruction
1237val p_smlad_smlsd:
1238  (string * (bool * (bool * (string list)))) -> maybe_instruction
1239val p_smlald_smlsld:
1240  (string * (bool * (bool * (string list)))) -> maybe_instruction
1241val p_smmul: (string * (bool * (string list))) -> maybe_instruction
1242val p_smmla: (string * (bool * (string list))) -> maybe_instruction
1243val p_smmls: (string * (bool * (string list))) -> maybe_instruction
1244val p_qadd_etc:
1245  (string * (BitsN.nbit * (string list))) -> maybe_instruction
1246val p_sadd16_etc:
1247  (string * (BitsN.nbit * (string list))) -> maybe_instruction
1248val p_qadd16_etc:
1249  (string * (BitsN.nbit * (string list))) -> maybe_instruction
1250val p_shadd16_etc:
1251  (string * (BitsN.nbit * (string list))) -> maybe_instruction
1252val p_sadd8_etc: (string * (bool * (string list))) -> maybe_instruction
1253val p_qadd8_etc: (string * (bool * (string list))) -> maybe_instruction
1254val p_shadd8_etc: (string * (bool * (string list))) -> maybe_instruction
1255val p_uadd16_etc:
1256  (string * (BitsN.nbit * (string list))) -> maybe_instruction
1257val p_uqadd16_etc:
1258  (string * (BitsN.nbit * (string list))) -> maybe_instruction
1259val p_uhadd16_etc:
1260  (string * (BitsN.nbit * (string list))) -> maybe_instruction
1261val p_uadd8_etc: (string * (bool * (string list))) -> maybe_instruction
1262val p_uqadd8_etc: (string * (bool * (string list))) -> maybe_instruction
1263val p_uhadd8_etc: (string * (bool * (string list))) -> maybe_instruction
1264val p_usad8: (string * (string list)) -> maybe_instruction
1265val p_usada8: (string * (string list)) -> maybe_instruction
1266val p_pkhbt_pkhtb: (string * (bool * (string list))) -> maybe_instruction
1267val p_sat: (string * (bool * (string list))) -> maybe_instruction
1268val p_sat16: (string * (bool * (string list))) -> maybe_instruction
1269val pick_sxtb:
1270  (Nat.nat * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat))))) ->
1271  instruction
1272val p_sxtb_etc:
1273  (string * (Nat.nat * (bool * (string list)))) -> maybe_instruction
1274val p_sxtab_etc:
1275  (string * (Nat.nat * (bool * (string list)))) -> maybe_instruction
1276val p_sel: (string * (string list)) -> maybe_instruction
1277val p_rev: (string * (string list)) -> maybe_instruction
1278val p_rev16: (string * (string list)) -> maybe_instruction
1279val p_revsh: (string * (string list)) -> maybe_instruction
1280val p_rbit: (string * (string list)) -> maybe_instruction
1281val p_sbfx_ubfx: (string * (bool * (string list))) -> maybe_instruction
1282val p_bfc: (string * (string list)) -> maybe_instruction
1283val p_bfi: (string * (string list)) -> maybe_instruction
1284val closingAddress: string -> ((bool * string) option)
1285val p_address_mode1:
1286  (string list) ->
1287  (string * ((bool * (bool * (bool * (BitsN.nbit * offset1)))) option))
1288val p_address_mode2:
1289  (string list) ->
1290  (string * ((bool * (bool * (bool * (BitsN.nbit * offset2)))) option))
1291val p_address_mode3:
1292  (string list) -> (string * ((BitsN.nbit * (BitsN.nbit option)) option))
1293val pick_ldr_str:
1294  (Nat.nat *
1295   (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))))) ->
1296  instruction
1297val p_ldr_str: (string * (Nat.nat * (string list))) -> maybe_instruction
1298val pick_ldrb_ldrh:
1299  (bool *
1300   (bool *
1301    (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))))) ->
1302  instruction
1303val p_ldrb_ldrh:
1304  (string * (bool * (bool * (string list)))) -> maybe_instruction
1305val pick_ldrd_strd:
1306  (bool *
1307   (bool *
1308    (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * offset2))))))) ->
1309  instruction
1310val p_ldrd_strd: (string * (bool * (string list))) -> maybe_instruction
1311val p_ldrt_strt1:
1312  (string * (Nat.nat * (string list))) -> maybe_instruction
1313val p_ldrt_strt2:
1314  (string * (Nat.nat * (string list))) -> maybe_instruction
1315val p_pld: (string * (bool * (string list))) -> maybe_instruction
1316val p_pli: (string * (string list)) -> maybe_instruction
1317val p_ldrex: (string * (string list)) -> maybe_instruction
1318val p_ldrexb_ldrexh:
1319  (string * (bool * (string list))) -> maybe_instruction
1320val p_ldrexd: (string * (string list)) -> maybe_instruction
1321val p_strex: (string * (string list)) -> maybe_instruction
1322val p_strexb_strexh:
1323  (string * (bool * (string list))) -> maybe_instruction
1324val p_strexd: (string * (string list)) -> maybe_instruction
1325val p_swp: (string * (bool * (string list))) -> maybe_instruction
1326val p_pop_push: (string * (bool * (string list))) -> maybe_instruction
1327val p_vpop_vpush: (string * (bool * (string list))) -> maybe_instruction
1328val p_ldm_stm:
1329  (string * (bool * (bool * (bool * (string list))))) -> maybe_instruction
1330val p_vldm_vstm:
1331  (string * (bool * (bool * (string list)))) -> maybe_instruction
1332val p_setend: (string list) -> maybe_instruction
1333val p_aif:
1334  (bool * (bool * (bool * string))) -> ((bool * (bool * bool)) option)
1335val p_cps: (bool * (bool * (string list))) -> maybe_instruction
1336val p_mode: string -> (BitsN.nbit option)
1337val banked_register: (BitsN.nbit * string) -> (BitsN.nbit option)
1338val p_banked_register: string -> (BitsN.nbit option)
1339val p_mrs: (string * (string list)) -> maybe_instruction
1340val p_cxsf: (BitsN.nbit * string) -> (BitsN.nbit option)
1341val p_spec_reg: string -> ((bool * BitsN.nbit) option)
1342val p_msr: (string * (string list)) -> maybe_instruction
1343val p_rfe: (string * (bool * (bool * (string list)))) -> maybe_instruction
1344val p_srs: (string * (bool * (bool * (string list)))) -> maybe_instruction
1345val p_call: (string * (Nat.nat * (string list))) -> maybe_instruction
1346val p_barrier_option: (string list) -> (BitsN.nbit option)
1347val p_dmb_dsb: (string * (bool * (string list))) -> maybe_instruction
1348val p_isb: (string * (string list)) -> maybe_instruction
1349val p_vcmpe: (string * (string list)) -> maybe_instruction
1350val p_vmrs_register: string -> (BitsN.nbit option)
1351val p_vmrs: (string * (string list)) -> maybe_instruction
1352val p_vmsr: (string * (string list)) -> maybe_instruction
1353val p_vcvt: (string * (bool * (string list))) -> maybe_instruction
1354val p_fp2: (string * (Nat.nat * (string list))) -> maybe_instruction
1355val p_fp3: (string * (Nat.nat * (string list))) -> maybe_instruction
1356val p_vldr_vstr: (string * (bool * (string list))) -> maybe_instruction
1357val p_noarg: (string * instruction) -> maybe_instruction
1358val p_tokens: string -> (string list)
1359val instructionFromString: string -> maybe_instruction
1360val s_cond: BitsN.nbit -> string
1361val s_reg: BitsN.nbit -> string
1362val s_reg2: (BitsN.nbit * BitsN.nbit) -> string
1363val s_reg3: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> string
1364val s_reg4:
1365  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string
1366val s_vfp_reg: (bool * BitsN.nbit) -> string
1367val s_any_reg: ((bool option) * Nat.nat) -> string
1368val contiguous:
1369  (((Nat.nat * Nat.nat) list) * (Nat.nat * (bool list))) ->
1370  ((Nat.nat * Nat.nat) list)
1371val s_registers_from_contiguous:
1372  ((bool option) * (string * ((Nat.nat * Nat.nat) list))) -> string
1373val s_registers: Nat.nat -> ((bool option) * BitsN.nbit) -> string
1374val s_arm_registers: Nat.nat -> BitsN.nbit -> string
1375val s_fp_registers: Nat.nat -> (bool * BitsN.nbit) -> string
1376val s_hex: Nat.nat -> BitsN.nbit -> string
1377val s_offset: BitsN.nbit -> string
1378val s_add_sub_offset: (bool * BitsN.nbit) -> string
1379val s_branch: (BitsN.nbit * Branch) -> (string * string)
1380val s_vfp_suffix: (BitsN.nbit * bool) -> string
1381val s_vfp: (BitsN.nbit * VFP) -> (string * string)
1382val s_test_compare: BitsN.nbit -> string
1383val s_arith_logic: BitsN.nbit -> string
1384val s_shift: SRType -> string
1385val s_shift_n: (SRType * Nat.nat) -> string
1386val s_shift_r: (bool * (BitsN.nbit * (SRType * Nat.nat))) -> string
1387val s_expand_imm: BitsN.nbit -> string
1388val s_data: (BitsN.nbit * Data) -> (string * string)
1389val s_multiply: (BitsN.nbit * Multiply) -> (string * string)
1390val s_imm_form:
1391  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
1392  string
1393val s_reg_form:
1394  (bool *
1395   (bool *
1396    (bool *
1397     (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat))))))) ->
1398  string
1399val s_stack: (bool * bool) -> string
1400val s_load: (BitsN.nbit * Load) -> (string * string)
1401val s_store: (BitsN.nbit * Store) -> (string * string)
1402val s_barrier_option: BitsN.nbit -> string
1403val s_hint: (BitsN.nbit * Hint) -> (string * string)
1404val s_add_sub16:
1405  (string *
1406   (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
1407  (string * string)
1408val s_add_sub8:
1409  (string *
1410   (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
1411  (string * string)
1412val s_simd: (BitsN.nbit * SIMD) -> (string * string)
1413val s_xt_rotation:
1414  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat))) -> string
1415val s_media: (BitsN.nbit * Media) -> (string * string)
1416val s_psr: (bool * BitsN.nbit) -> string
1417val s_special: (bool * BitsN.nbit) -> string
1418val s_system: (BitsN.nbit * System) -> (string * string)
1419val s_it_mask: (bool * BitsN.nbit) -> string
1420val instructionToString: (BitsN.nbit * instruction) -> (string * string)
1421
1422end