1(* arm8 - generated by L3 - Wed Oct 11 10:50:34 2017 *)
2
3signature arm8 =
4sig
5
6structure Map : Map
7
8(* -------------------------------------------------------------------------
9   Types
10   ------------------------------------------------------------------------- *)
11
12type ProcState =
13  { C: bool, EL: BitsN.nbit, N: bool, SPS: bool, V: bool, Z: bool }
14
15type TCR_EL1 = { TBI0: bool, TBI1: bool, tcr_el1'rst: BitsN.nbit }
16
17type TCR_EL2_EL3 = { TBI: bool, tcr_el2_el3'rst: BitsN.nbit }
18
19type SCTLRType =
20  { A: bool, E0E: bool, EE: bool, SA: bool, SA0: bool,
21    sctlrtype'rst: BitsN.nbit }
22
23datatype BranchType
24  = BranchType_CALL | BranchType_ERET | BranchType_DBGEXIT
25  | BranchType_RET | BranchType_JMP | BranchType_EXCEPTION
26  | BranchType_UNKNOWN
27
28datatype AccType
29  = AccType_NORMAL | AccType_VEC | AccType_STREAM | AccType_VECSTREAM
30  | AccType_ATOMIC | AccType_ORDERED | AccType_UNPRIV | AccType_IFETCH
31  | AccType_PTW | AccType_DC | AccType_IC | AccType_AT
32
33datatype ShiftType
34  = ShiftType_LSL | ShiftType_LSR | ShiftType_ASR | ShiftType_ROR
35
36datatype ExtendType
37  = ExtendType_UXTB | ExtendType_UXTH | ExtendType_UXTW | ExtendType_UXTX
38  | ExtendType_SXTB | ExtendType_SXTH | ExtendType_SXTW | ExtendType_SXTX
39
40datatype LogicalOp = LogicalOp_AND | LogicalOp_ORR | LogicalOp_EOR
41
42datatype MemOp = MemOp_LOAD | MemOp_STORE | MemOp_PREFETCH
43
44datatype MemBarrierOp
45  = MemBarrierOp_DSB | MemBarrierOp_DMB | MemBarrierOp_ISB
46
47datatype MoveWideOp = MoveWideOp_N | MoveWideOp_Z | MoveWideOp_K
48
49datatype RevOp = RevOp_RBIT | RevOp_REV16 | RevOp_REV32 | RevOp_REV64
50
51datatype SystemHintOp
52  = SystemHintOp_NOP | SystemHintOp_YIELD | SystemHintOp_WFE
53  | SystemHintOp_WFI | SystemHintOp_SEV | SystemHintOp_SEVL
54
55datatype PSTATEField
56  = PSTATEField_DAIFSet | PSTATEField_DAIFClr | PSTATEField_SP
57
58datatype System
59  = ExceptionReturn
60  | HypervisorCall of BitsN.nbit
61  | MoveImmediateProcState of PSTATEField * BitsN.nbit
62  | MoveSystemRegister of
63      bool *
64      (BitsN.nbit *
65       (BitsN.nbit *
66        (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))
67  | SecureMonitorCall of BitsN.nbit
68  | SupervisorCall of BitsN.nbit
69  | SystemInstruction of
70      BitsN.nbit *
71      (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (bool * BitsN.nbit))))
72
73datatype Debug
74  = Breakpoint of BitsN.nbit
75  | DebugRestore
76  | DebugSwitch of BitsN.nbit
77  | Halt of BitsN.nbit
78
79datatype LoadStore
80  = LoadLiteral''32 of
81      BitsN.nbit * (MemOp * (bool * (BitsN.nbit * BitsN.nbit)))
82  | LoadLiteral''64 of
83      BitsN.nbit * (MemOp * (bool * (BitsN.nbit * BitsN.nbit)))
84  | LoadStoreAcquire''16 of
85      BitsN.nbit *
86      (MemOp *
87       (AccType *
88        (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))
89  | LoadStoreAcquire''32 of
90      BitsN.nbit *
91      (MemOp *
92       (AccType *
93        (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))
94  | LoadStoreAcquire''64 of
95      BitsN.nbit *
96      (MemOp *
97       (AccType *
98        (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))
99  | LoadStoreAcquire''8 of
100      BitsN.nbit *
101      (MemOp *
102       (AccType *
103        (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))
104  | LoadStoreAcquirePair''128 of
105      BitsN.nbit *
106      (MemOp *
107       (AccType *
108        (bool *
109         (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))
110  | LoadStoreAcquirePair''64 of
111      BitsN.nbit *
112      (MemOp *
113       (AccType *
114        (bool *
115         (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))
116  | LoadStoreImmediate''16 of
117      BitsN.nbit *
118      (bool *
119       (MemOp *
120        (AccType *
121         (bool *
122          (bool *
123           (bool *
124            (bool *
125             (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))))))
126  | LoadStoreImmediate''32 of
127      BitsN.nbit *
128      (bool *
129       (MemOp *
130        (AccType *
131         (bool *
132          (bool *
133           (bool *
134            (bool *
135             (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))))))
136  | LoadStoreImmediate''64 of
137      BitsN.nbit *
138      (bool *
139       (MemOp *
140        (AccType *
141         (bool *
142          (bool *
143           (bool *
144            (bool *
145             (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))))))
146  | LoadStoreImmediate''8 of
147      BitsN.nbit *
148      (bool *
149       (MemOp *
150        (AccType *
151         (bool *
152          (bool *
153           (bool *
154            (bool *
155             (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))))))
156  | LoadStorePair''32 of
157      BitsN.nbit *
158      (MemOp *
159       (AccType *
160        (bool *
161         (bool *
162          (bool *
163           (bool *
164            (bool *
165             (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))))))))
166  | LoadStorePair''64 of
167      BitsN.nbit *
168      (MemOp *
169       (AccType *
170        (bool *
171         (bool *
172          (bool *
173           (bool *
174            (bool *
175             (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))))))))
176  | LoadStoreRegister''16 of
177      BitsN.nbit *
178      (bool *
179       (MemOp *
180        (bool *
181         (BitsN.nbit *
182          (ExtendType * (Nat.nat * (BitsN.nbit * BitsN.nbit)))))))
183  | LoadStoreRegister''32 of
184      BitsN.nbit *
185      (bool *
186       (MemOp *
187        (bool *
188         (BitsN.nbit *
189          (ExtendType * (Nat.nat * (BitsN.nbit * BitsN.nbit)))))))
190  | LoadStoreRegister''64 of
191      BitsN.nbit *
192      (bool *
193       (MemOp *
194        (bool *
195         (BitsN.nbit *
196          (ExtendType * (Nat.nat * (BitsN.nbit * BitsN.nbit)))))))
197  | LoadStoreRegister''8 of
198      BitsN.nbit *
199      (bool *
200       (MemOp *
201        (bool *
202         (BitsN.nbit *
203          (ExtendType * (Nat.nat * (BitsN.nbit * BitsN.nbit)))))))
204
205datatype Branch
206  = BranchConditional of BitsN.nbit * BitsN.nbit
207  | BranchImmediate of BitsN.nbit * BranchType
208  | BranchRegister of BitsN.nbit * BranchType
209  | CompareAndBranch''32 of
210      BitsN.nbit * (bool * (BitsN.nbit * BitsN.nbit))
211  | CompareAndBranch''64 of
212      BitsN.nbit * (bool * (BitsN.nbit * BitsN.nbit))
213  | TestBitAndBranch''32 of
214      BitsN.nbit * (BitsN.nbit * (bool * (BitsN.nbit * BitsN.nbit)))
215  | TestBitAndBranch''64 of
216      BitsN.nbit * (BitsN.nbit * (bool * (BitsN.nbit * BitsN.nbit)))
217
218datatype CRCExt
219  = CRC''16 of
220      BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
221  | CRC''32 of
222      BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
223  | CRC''64 of
224      BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
225  | CRC''8 of
226      BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
227
228datatype Data
229  = AddSubCarry''32 of
230      BitsN.nbit *
231      (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
232  | AddSubCarry''64 of
233      BitsN.nbit *
234      (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
235  | AddSubExtendRegister''32 of
236      BitsN.nbit *
237      (bool *
238       (bool *
239        (BitsN.nbit *
240         (ExtendType * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))))
241  | AddSubExtendRegister''64 of
242      BitsN.nbit *
243      (bool *
244       (bool *
245        (BitsN.nbit *
246         (ExtendType * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))))
247  | AddSubImmediate''32 of
248      BitsN.nbit *
249      (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
250  | AddSubImmediate''64 of
251      BitsN.nbit *
252      (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
253  | AddSubShiftedRegister''32 of
254      BitsN.nbit *
255      (bool *
256       (bool *
257        (ShiftType *
258         (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))))
259  | AddSubShiftedRegister''64 of
260      BitsN.nbit *
261      (bool *
262       (bool *
263        (ShiftType *
264         (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))))
265  | BitfieldMove''32 of
266      BitsN.nbit *
267      (bool *
268       (bool *
269        (BitsN.nbit *
270         (BitsN.nbit * (Nat.nat * (Nat.nat * (BitsN.nbit * BitsN.nbit)))))))
271  | BitfieldMove''64 of
272      BitsN.nbit *
273      (bool *
274       (bool *
275        (BitsN.nbit *
276         (BitsN.nbit * (Nat.nat * (Nat.nat * (BitsN.nbit * BitsN.nbit)))))))
277  | ConditionalCompareImmediate''32 of
278      BitsN.nbit *
279      (bool *
280       (BitsN.nbit *
281        (BitsN.nbit * ((bool * (bool * (bool * bool))) * BitsN.nbit))))
282  | ConditionalCompareImmediate''64 of
283      BitsN.nbit *
284      (bool *
285       (BitsN.nbit *
286        (BitsN.nbit * ((bool * (bool * (bool * bool))) * BitsN.nbit))))
287  | ConditionalCompareRegister''32 of
288      BitsN.nbit *
289      (bool *
290       (BitsN.nbit *
291        ((bool * (bool * (bool * bool))) * (BitsN.nbit * BitsN.nbit))))
292  | ConditionalCompareRegister''64 of
293      BitsN.nbit *
294      (bool *
295       (BitsN.nbit *
296        ((bool * (bool * (bool * bool))) * (BitsN.nbit * BitsN.nbit))))
297  | ConditionalSelect''32 of
298      BitsN.nbit *
299      (bool *
300       (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))
301  | ConditionalSelect''64 of
302      BitsN.nbit *
303      (bool *
304       (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))
305  | CountLeading''32 of BitsN.nbit * (bool * (BitsN.nbit * BitsN.nbit))
306  | CountLeading''64 of BitsN.nbit * (bool * (BitsN.nbit * BitsN.nbit))
307  | Division''32 of
308      BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
309  | Division''64 of
310      BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
311  | ExtractRegister''32 of
312      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
313  | ExtractRegister''64 of
314      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
315  | LogicalImmediate''32 of
316      BitsN.nbit *
317      (LogicalOp * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
318  | LogicalImmediate''64 of
319      BitsN.nbit *
320      (LogicalOp * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
321  | LogicalShiftedRegister''32 of
322      BitsN.nbit *
323      (LogicalOp *
324       (bool *
325        (bool *
326         (ShiftType * (Nat.nat * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))
327  | LogicalShiftedRegister''64 of
328      BitsN.nbit *
329      (LogicalOp *
330       (bool *
331        (bool *
332         (ShiftType * (Nat.nat * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))
333  | MoveWide''32 of
334      BitsN.nbit * (MoveWideOp * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
335  | MoveWide''64 of
336      BitsN.nbit * (MoveWideOp * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
337  | MultiplyAddSub''32 of
338      BitsN.nbit *
339      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
340  | MultiplyAddSub''64 of
341      BitsN.nbit *
342      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
343  | MultiplyAddSubLong of
344      bool *
345      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
346  | MultiplyHigh of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
347  | Reverse''32 of BitsN.nbit * (RevOp * (BitsN.nbit * BitsN.nbit))
348  | Reverse''64 of BitsN.nbit * (RevOp * (BitsN.nbit * BitsN.nbit))
349  | Shift''32 of
350      BitsN.nbit * (ShiftType * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
351  | Shift''64 of
352      BitsN.nbit * (ShiftType * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
353
354datatype instruction
355  = Address of bool * (BitsN.nbit * BitsN.nbit)
356  | Branch of Branch
357  | CRCExt of CRCExt
358  | ClearExclusive of BitsN.nbit
359  | Data of Data
360  | Debug of Debug
361  | Hint of SystemHintOp
362  | LoadStore of LoadStore
363  | MemoryBarrier of MemBarrierOp * BitsN.nbit
364  | Reserved
365  | System of System
366  | Unallocated
367
368datatype MachineCode = ARM8 of BitsN.nbit | BadCode of string
369
370datatype maybe_instruction
371  = FAIL of string
372  | OK of instruction
373  | PENDING of string * instruction
374  | WORD of BitsN.nbit
375
376(* -------------------------------------------------------------------------
377   Exceptions
378   ------------------------------------------------------------------------- *)
379
380exception ALIGNMENT_FAULT
381
382exception ASSERT of string
383
384exception UNDEFINED_FAULT of string
385
386(* -------------------------------------------------------------------------
387   Functions
388   ------------------------------------------------------------------------- *)
389
390structure Cast:
391sig
392
393val natToBranchType: Nat.nat -> BranchType
394val BranchTypeToNat: BranchType -> Nat.nat
395val stringToBranchType: string -> BranchType
396val BranchTypeToString: BranchType -> string
397val natToAccType: Nat.nat -> AccType
398val AccTypeToNat: AccType -> Nat.nat
399val stringToAccType: string -> AccType
400val AccTypeToString: AccType -> string
401val natToShiftType: Nat.nat -> ShiftType
402val ShiftTypeToNat: ShiftType -> Nat.nat
403val stringToShiftType: string -> ShiftType
404val ShiftTypeToString: ShiftType -> string
405val natToExtendType: Nat.nat -> ExtendType
406val ExtendTypeToNat: ExtendType -> Nat.nat
407val stringToExtendType: string -> ExtendType
408val ExtendTypeToString: ExtendType -> string
409val natToLogicalOp: Nat.nat -> LogicalOp
410val LogicalOpToNat: LogicalOp -> Nat.nat
411val stringToLogicalOp: string -> LogicalOp
412val LogicalOpToString: LogicalOp -> string
413val natToMemOp: Nat.nat -> MemOp
414val MemOpToNat: MemOp -> Nat.nat
415val stringToMemOp: string -> MemOp
416val MemOpToString: MemOp -> string
417val natToMemBarrierOp: Nat.nat -> MemBarrierOp
418val MemBarrierOpToNat: MemBarrierOp -> Nat.nat
419val stringToMemBarrierOp: string -> MemBarrierOp
420val MemBarrierOpToString: MemBarrierOp -> string
421val natToMoveWideOp: Nat.nat -> MoveWideOp
422val MoveWideOpToNat: MoveWideOp -> Nat.nat
423val stringToMoveWideOp: string -> MoveWideOp
424val MoveWideOpToString: MoveWideOp -> string
425val natToRevOp: Nat.nat -> RevOp
426val RevOpToNat: RevOp -> Nat.nat
427val stringToRevOp: string -> RevOp
428val RevOpToString: RevOp -> string
429val natToSystemHintOp: Nat.nat -> SystemHintOp
430val SystemHintOpToNat: SystemHintOp -> Nat.nat
431val stringToSystemHintOp: string -> SystemHintOp
432val SystemHintOpToString: SystemHintOp -> string
433val natToPSTATEField: Nat.nat -> PSTATEField
434val PSTATEFieldToNat: PSTATEField -> Nat.nat
435val stringToPSTATEField: string -> PSTATEField
436val PSTATEFieldToString: PSTATEField -> string
437
438end
439
440val MEM: (BitsN.nbit Map.map) ref
441val PC: BitsN.nbit ref
442val PSTATE: ProcState ref
443val REG: (BitsN.nbit Map.map) ref
444val SCTLR_EL1: SCTLRType ref
445val SCTLR_EL2: SCTLRType ref
446val SCTLR_EL3: SCTLRType ref
447val SP_EL0: BitsN.nbit ref
448val SP_EL1: BitsN.nbit ref
449val SP_EL2: BitsN.nbit ref
450val SP_EL3: BitsN.nbit ref
451val TCR_EL1: TCR_EL1 ref
452val TCR_EL2: TCR_EL2_EL3 ref
453val TCR_EL3: TCR_EL2_EL3 ref
454val branch_hint: (BranchType option) ref
455val ProcState_C_rupd: ProcState * bool -> ProcState
456val ProcState_EL_rupd: ProcState * BitsN.nbit -> ProcState
457val ProcState_N_rupd: ProcState * bool -> ProcState
458val ProcState_SPS_rupd: ProcState * bool -> ProcState
459val ProcState_V_rupd: ProcState * bool -> ProcState
460val ProcState_Z_rupd: ProcState * bool -> ProcState
461val TCR_EL1_TBI0_rupd: TCR_EL1 * bool -> TCR_EL1
462val TCR_EL1_TBI1_rupd: TCR_EL1 * bool -> TCR_EL1
463val TCR_EL1_tcr_el1'rst_rupd: TCR_EL1 * BitsN.nbit -> TCR_EL1
464val TCR_EL2_EL3_TBI_rupd: TCR_EL2_EL3 * bool -> TCR_EL2_EL3
465val TCR_EL2_EL3_tcr_el2_el3'rst_rupd:
466  TCR_EL2_EL3 * BitsN.nbit -> TCR_EL2_EL3
467val SCTLRType_A_rupd: SCTLRType * bool -> SCTLRType
468val SCTLRType_E0E_rupd: SCTLRType * bool -> SCTLRType
469val SCTLRType_EE_rupd: SCTLRType * bool -> SCTLRType
470val SCTLRType_SA_rupd: SCTLRType * bool -> SCTLRType
471val SCTLRType_SA0_rupd: SCTLRType * bool -> SCTLRType
472val SCTLRType_sctlrtype'rst_rupd: SCTLRType * BitsN.nbit -> SCTLRType
473val boolify'32:
474  BitsN.nbit ->
475  bool *
476  (bool *
477   (bool *
478    (bool *
479     (bool *
480      (bool *
481       (bool *
482        (bool *
483         (bool *
484          (bool *
485           (bool *
486            (bool *
487             (bool *
488              (bool *
489               (bool *
490                (bool *
491                 (bool *
492                  (bool *
493                   (bool *
494                    (bool *
495                     (bool *
496                      (bool *
497                       (bool *
498                        (bool *
499                         (bool *
500                          (bool *
501                           (bool *
502                            (bool * (bool * (bool * (bool * bool))))))))))))))))))))))))))))))
503val rec'TCR_EL1: BitsN.nbit -> TCR_EL1
504val reg'TCR_EL1: TCR_EL1 -> BitsN.nbit
505val write'rec'TCR_EL1: (BitsN.nbit * TCR_EL1) -> BitsN.nbit
506val write'reg'TCR_EL1: (TCR_EL1 * BitsN.nbit) -> TCR_EL1
507val rec'TCR_EL2_EL3: BitsN.nbit -> TCR_EL2_EL3
508val reg'TCR_EL2_EL3: TCR_EL2_EL3 -> BitsN.nbit
509val write'rec'TCR_EL2_EL3: (BitsN.nbit * TCR_EL2_EL3) -> BitsN.nbit
510val write'reg'TCR_EL2_EL3: (TCR_EL2_EL3 * BitsN.nbit) -> TCR_EL2_EL3
511val rec'SCTLRType: BitsN.nbit -> SCTLRType
512val reg'SCTLRType: SCTLRType -> BitsN.nbit
513val write'rec'SCTLRType: (BitsN.nbit * SCTLRType) -> BitsN.nbit
514val write'reg'SCTLRType: (SCTLRType * BitsN.nbit) -> SCTLRType
515val X: Nat.nat -> BitsN.nbit -> BitsN.nbit
516val write'X: Nat.nat -> (BitsN.nbit * BitsN.nbit) -> unit
517val SP: Nat.nat -> BitsN.nbit
518val write'SP: Nat.nat -> BitsN.nbit -> unit
519val TranslationRegime: unit -> BitsN.nbit
520val SCTLR: unit -> SCTLRType
521val Hint_Branch: BranchType -> unit
522val BranchTo: (BitsN.nbit * BranchType) -> unit
523val Align: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
524val Aligned: Nat.nat -> (BitsN.nbit * Nat.nat) -> bool
525val CheckSPAlignment: unit -> unit
526val CheckAlignment: (BitsN.nbit * (Nat.nat * (AccType * bool))) -> unit
527val BigEndian: unit -> bool
528val ByteList: (bool list) -> ((bool list) list)
529val BigEndianReverse: (bool list) -> (bool list)
530val Mem: Nat.nat -> (BitsN.nbit * (Nat.nat * AccType)) -> BitsN.nbit
531val write'Mem: Nat.nat ->
532  (BitsN.nbit * (BitsN.nbit * (Nat.nat * AccType))) -> unit
533val ConditionTest: (BitsN.nbit * (bool * (bool * (bool * bool)))) -> bool
534val ConditionHolds: BitsN.nbit -> bool
535val Ones: Nat.nat -> (bool list)
536val Zeros: Nat.nat -> (bool list)
537val Replicate: Nat.nat -> (bool list) -> BitsN.nbit
538val HighestSetBit: Nat.nat -> BitsN.nbit -> IntInf.int
539val CountLeadingZeroBits: Nat.nat -> BitsN.nbit -> Nat.nat
540val CountLeadingSignBits: Nat.nat -> BitsN.nbit -> Nat.nat
541val Poly32Mod2_loop:
542  (Nat.nat * ((bool list) * (bool list))) -> (bool list)
543val Poly32Mod2: ((bool list) * BitsN.nbit) -> BitsN.nbit
544val AddWithCarry: Nat.nat ->
545  (BitsN.nbit * (BitsN.nbit * bool)) ->
546  (BitsN.nbit * (bool * (bool * (bool * bool))))
547val SetTheFlags: (bool * (bool * (bool * (bool * bool)))) -> unit
548val DecodeShift: BitsN.nbit -> ShiftType
549val ShiftValue: Nat.nat ->
550  (BitsN.nbit * (ShiftType * Nat.nat)) -> BitsN.nbit
551val ShiftReg: Nat.nat ->
552  (BitsN.nbit * (ShiftType * Nat.nat)) -> BitsN.nbit
553val ExtendWord: Nat.nat * Nat.nat -> (BitsN.nbit * bool) -> BitsN.nbit
554val Extend: Nat.nat -> ((bool list) * bool) -> BitsN.nbit
555val DecodeRegExtend: BitsN.nbit -> ExtendType
556val ExtendValue: Nat.nat ->
557  (BitsN.nbit * (ExtendType * Nat.nat)) -> BitsN.nbit
558val ExtendReg: Nat.nat ->
559  (BitsN.nbit * (ExtendType * Nat.nat)) -> BitsN.nbit
560val DecodeBitMasks: Nat.nat ->
561  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))) ->
562  ((BitsN.nbit * BitsN.nbit) option)
563val dfn'Address: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
564val dfn'AddSubCarry: Nat.nat ->
565  (BitsN.nbit * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
566  unit
567val dfn'AddSubExtendRegister: Nat.nat ->
568  (BitsN.nbit *
569   (bool *
570    (bool *
571     (BitsN.nbit * (ExtendType * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))))) ->
572  unit
573val dfn'AddSubImmediate: Nat.nat ->
574  (BitsN.nbit * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
575  unit
576val dfn'AddSubShiftedRegister: Nat.nat ->
577  (BitsN.nbit *
578   (bool *
579    (bool *
580     (ShiftType * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))))) ->
581  unit
582val dfn'LogicalImmediate: Nat.nat ->
583  (BitsN.nbit *
584   (LogicalOp * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
585  unit
586val dfn'LogicalShiftedRegister: Nat.nat ->
587  (BitsN.nbit *
588   (LogicalOp *
589    (bool *
590     (bool *
591      (ShiftType * (Nat.nat * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))) ->
592  unit
593val dfn'Shift: Nat.nat ->
594  (BitsN.nbit * (ShiftType * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) ->
595  unit
596val dfn'MoveWide: Nat.nat ->
597  (BitsN.nbit * (MoveWideOp * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) ->
598  unit
599val dfn'BitfieldMove: Nat.nat ->
600  (BitsN.nbit *
601   (bool *
602    (bool *
603     (BitsN.nbit *
604      (BitsN.nbit * (Nat.nat * (Nat.nat * (BitsN.nbit * BitsN.nbit)))))))) ->
605  unit
606val dfn'ConditionalCompareImmediate: Nat.nat ->
607  (BitsN.nbit *
608   (bool *
609    (BitsN.nbit *
610     (BitsN.nbit * ((bool * (bool * (bool * bool))) * BitsN.nbit))))) ->
611  unit
612val dfn'ConditionalCompareRegister: Nat.nat ->
613  (BitsN.nbit *
614   (bool *
615    (BitsN.nbit *
616     ((bool * (bool * (bool * bool))) * (BitsN.nbit * BitsN.nbit))))) ->
617  unit
618val dfn'ConditionalSelect: Nat.nat ->
619  (BitsN.nbit *
620   (bool *
621    (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))) ->
622  unit
623val dfn'CountLeading: Nat.nat ->
624  (BitsN.nbit * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
625val dfn'ExtractRegister: Nat.nat ->
626  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) ->
627  unit
628val dfn'Division: Nat.nat ->
629  (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
630val dfn'MultiplyAddSub: Nat.nat ->
631  (BitsN.nbit *
632   (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
633  unit
634val dfn'MultiplyAddSubLong:
635  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
636  unit
637val dfn'MultiplyHigh:
638  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
639val dfn'Reverse: Nat.nat ->
640  (BitsN.nbit * (RevOp * (BitsN.nbit * BitsN.nbit))) -> unit
641val dfn'CRC: Nat.nat ->
642  (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
643val dfn'BranchConditional: (BitsN.nbit * BitsN.nbit) -> unit
644val dfn'BranchImmediate: (BitsN.nbit * BranchType) -> unit
645val dfn'BranchRegister: (BitsN.nbit * BranchType) -> unit
646val dfn'CompareAndBranch: Nat.nat ->
647  (BitsN.nbit * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
648val dfn'TestBitAndBranch: Nat.nat ->
649  (BitsN.nbit * (BitsN.nbit * (bool * (BitsN.nbit * BitsN.nbit)))) -> unit
650val LoadStoreSingle: Nat.nat ->
651  (BitsN.nbit *
652   (bool *
653    (MemOp *
654     (AccType *
655      (bool *
656       (bool *
657        (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))))))))) ->
658  unit
659val dfn'LoadStoreImmediate: Nat.nat ->
660  (BitsN.nbit *
661   (bool *
662    (MemOp *
663     (AccType *
664      (bool *
665       (bool *
666        (bool *
667         (bool *
668          (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))))))) ->
669  unit
670val dfn'LoadStoreRegister: Nat.nat ->
671  (BitsN.nbit *
672   (bool *
673    (MemOp *
674     (bool *
675      (BitsN.nbit * (ExtendType * (Nat.nat * (BitsN.nbit * BitsN.nbit)))))))) ->
676  unit
677val dfn'LoadStorePair: Nat.nat ->
678  (BitsN.nbit *
679   (MemOp *
680    (AccType *
681     (bool *
682      (bool *
683       (bool *
684        (bool *
685         (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))))))))) ->
686  unit
687val ExclusiveMonitorPass: (BitsN.nbit * Nat.nat) -> bool
688val SetExclusiveMonitors: (BitsN.nbit * Nat.nat) -> unit
689val ExclusiveMonitorStatus: BitsN.nbit
690val dfn'LoadStoreAcquire: Nat.nat ->
691  (BitsN.nbit *
692   (MemOp *
693    (AccType *
694     (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))) ->
695  unit
696val dfn'LoadStoreAcquirePair: Nat.nat ->
697  (BitsN.nbit *
698   (MemOp *
699    (AccType *
700     (bool *
701      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))) ->
702  unit
703val dfn'LoadLiteral: Nat.nat ->
704  (BitsN.nbit * (MemOp * (bool * (BitsN.nbit * BitsN.nbit)))) -> unit
705val dfn'MemoryBarrier: (MemBarrierOp * BitsN.nbit) -> unit
706val dfn'ClearExclusive: BitsN.nbit -> unit
707val dfn'Hint: SystemHintOp -> unit
708val dfn'Breakpoint: BitsN.nbit -> unit
709val dfn'DebugSwitch: BitsN.nbit -> unit
710val dfn'DebugRestore: unit -> unit
711val dfn'Halt: BitsN.nbit -> unit
712val dfn'SystemInstruction:
713  (BitsN.nbit *
714   (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (bool * BitsN.nbit))))) ->
715  unit
716val dfn'MoveSystemRegister:
717  (bool *
718   (BitsN.nbit *
719    (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))) ->
720  unit
721val dfn'MoveImmediateProcState: (PSTATEField * BitsN.nbit) -> unit
722val dfn'SupervisorCall: BitsN.nbit -> unit
723val dfn'HypervisorCall: BitsN.nbit -> unit
724val dfn'SecureMonitorCall: BitsN.nbit -> unit
725val dfn'ExceptionReturn: unit -> unit
726val dfn'Unallocated: unit -> unit
727val dfn'Reserved: unit -> unit
728val Run: instruction -> unit
729val DecodeLogicalOp: BitsN.nbit -> (LogicalOp * bool)
730val NoOperation: instruction
731val LoadStoreRegister:
732  (BitsN.nbit *
733   (bool *
734    (MemOp *
735     (bool *
736      (BitsN.nbit * (ExtendType * (Nat.nat * (BitsN.nbit * BitsN.nbit)))))))) ->
737  instruction
738val LoadStoreImmediateN:
739  (BitsN.nbit *
740   (bool *
741    (MemOp *
742     (AccType *
743      (bool *
744       (bool *
745        (bool *
746         (bool *
747          (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))))))) ->
748  instruction
749val LoadStoreImmediate:
750  (BitsN.nbit *
751   (BitsN.nbit *
752    (AccType *
753     (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))) ->
754  instruction
755val LoadStorePairN:
756  (BitsN.nbit *
757   (MemOp *
758    (AccType *
759     (bool *
760      (bool *
761       (bool *
762        (bool *
763         (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))))))))) ->
764  instruction
765val LoadStorePair:
766  (BitsN.nbit *
767   (MemOp *
768    (AccType *
769     (bool *
770      (bool *
771       (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))))))) ->
772  instruction
773val LoadStoreAcquireN:
774  (BitsN.nbit *
775   (MemOp *
776    (AccType *
777     (bool *
778      (bool *
779       (bool *
780        (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))))) ->
781  instruction
782val LoadStoreAcquire:
783  (BitsN.nbit *
784   (MemOp *
785    (AccType *
786     (bool *
787      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))) ->
788  instruction
789val Decode: BitsN.nbit -> instruction
790val Fetch: unit -> BitsN.nbit
791val Next: unit -> unit
792val CountTrailing: Nat.nat -> (bool * BitsN.nbit) -> Nat.nat
793val EncodeBitMaskAux: Nat.nat ->
794  BitsN.nbit -> (Nat.nat * (Nat.nat * Nat.nat))
795val EncodeBitMask: Nat.nat ->
796  BitsN.nbit -> ((BitsN.nbit * (BitsN.nbit * BitsN.nbit)) option)
797val e_sf: Nat.nat -> BitsN.nbit -> BitsN.nbit
798val EncodeLogicalOp: (LogicalOp * bool) -> (BitsN.nbit option)
799val e_data: Data -> MachineCode
800val e_debug: Debug -> BitsN.nbit
801val e_crc: CRCExt -> BitsN.nbit
802val e_branch: Branch -> MachineCode
803val e_system: System -> BitsN.nbit
804val e_LoadStoreImmediate:
805  (BitsN.nbit *
806   (bool *
807    (MemOp *
808     (AccType *
809      (bool *
810       (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))))))) ->
811  MachineCode
812val e_LoadStoreRegister:
813  (BitsN.nbit *
814   (bool *
815    (MemOp *
816     (bool *
817      (BitsN.nbit * (ExtendType * (Nat.nat * (BitsN.nbit * BitsN.nbit)))))))) ->
818  MachineCode
819val e_load_store: LoadStore -> MachineCode
820val Encode: instruction -> MachineCode
821val skipSpaces: string -> string
822val stripSpaces: string -> string
823val p_number: string -> (Nat.nat option)
824val p_encode_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option)
825val p_unbounded_immediate: string -> (Nat.nat option)
826val p_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option)
827val p_neg_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option)
828val p_pos_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option)
829val p_signed_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option)
830val p_offset: Nat.nat -> string -> ((bool * BitsN.nbit) option)
831val p_label: string -> (string option)
832val p_cond: string -> (BitsN.nbit option)
833val invert_cond: string -> string
834val p_w_x: string -> ((bool * string) option)
835val is_wide_reg: string -> bool
836val p_register: (bool * string) -> ((bool * BitsN.nbit) option)
837val p_register1: (bool * (string list)) -> ((bool * BitsN.nbit) option)
838val p_register2:
839  (bool * (bool * (string list))) ->
840  ((bool * (BitsN.nbit * BitsN.nbit)) option)
841val p_register3:
842  (bool * (bool * (bool * (string list)))) ->
843  ((bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) option)
844val p_register4:
845  (bool * (bool * (bool * (bool * (string list))))) ->
846  ((bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) option)
847val p_register2z:
848  (string list) -> ((bool * (BitsN.nbit * BitsN.nbit)) option)
849val p_register3z:
850  (string list) ->
851  ((bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) option)
852val p_extend_amount:
853  (ExtendType * (bool * string)) -> ((ExtendType * Nat.nat) option)
854val p_extend: string -> ((ExtendType * Nat.nat) option)
855val p_extend2:
856  (Nat.nat * (bool * string)) -> ((ExtendType * Nat.nat) option)
857val p_shift_amount: (ShiftType * string) -> ((ShiftType * Nat.nat) option)
858val p_shift_imm: string -> ((ShiftType * Nat.nat) option)
859val closingAddress: string -> ((bool * string) option)
860val p_address:
861  (string list) ->
862  (string * ((BitsN.nbit * (BitsN.nbit * (bool * bool))) option))
863val p_exclusive_address: (string list) -> (BitsN.nbit option)
864val p_opening_reg: string -> ((bool * BitsN.nbit) option)
865val p_reg_address:
866  (Nat.nat * (string list)) ->
867  ((BitsN.nbit * (BitsN.nbit * (ExtendType * Nat.nat))) option)
868val p_ldr_literal:
869  (Nat.nat *
870   (MemOp * (bool * (bool * (bool * (BitsN.nbit * (string list))))))) ->
871  maybe_instruction
872val p_ldr_str:
873  (Nat.nat * (MemOp * (AccType * (bool * (bool * (string list)))))) ->
874  maybe_instruction
875val p_ldar_stlr:
876  (Nat.nat * (MemOp * (AccType * (bool * (string list))))) ->
877  maybe_instruction
878val p_ldp_stp:
879  (MemOp * (AccType * (bool * (string list)))) -> maybe_instruction
880val p_ldxp: (AccType * (string list)) -> maybe_instruction
881val p_stxp: (AccType * (string list)) -> maybe_instruction
882val p_adr: (bool * (string list)) -> maybe_instruction
883val p_conditional_b: (BitsN.nbit * (string list)) -> maybe_instruction
884val p_b_bl: (BranchType * (string list)) -> maybe_instruction
885val p_br_etc: (BranchType * (string list)) -> maybe_instruction
886val p_cbz_cbnz: (bool * (string list)) -> maybe_instruction
887val p_tbz_tbnz: (bool * (string list)) -> maybe_instruction
888val p_extend_register:
889  (bool *
890   (bool *
891    (ExtendType * (Nat.nat * (bool * (string * (string * string))))))) ->
892  maybe_instruction
893val p_add_sub: (bool * (bool * (string list))) -> maybe_instruction
894val p_and_etc_fail: maybe_instruction
895val p_and_etc_imm_fail: maybe_instruction
896val p_and_etc:
897  (LogicalOp * (bool * (bool * (string list)))) -> maybe_instruction
898val p_movk_etc: (MoveWideOp * (string list)) -> maybe_instruction
899val p_adc_sbc: (bool * (bool * (string list))) -> maybe_instruction
900val p_asrv_etc: (ShiftType * (string list)) -> maybe_instruction
901val p_cls_clz: (bool * (string list)) -> maybe_instruction
902val p_sdiv_udiv: (bool * (string list)) -> maybe_instruction
903val p_madd_msub: (bool * (string list)) -> maybe_instruction
904val p_smaddl_etc: (bool * (bool * (string list))) -> maybe_instruction
905val p_smulh_umulh: (bool * (string list)) -> maybe_instruction
906val p_rbit_etc: (RevOp * (string list)) -> maybe_instruction
907val p_crc32b_etc: (Nat.nat * (bool * (string list))) -> maybe_instruction
908val p_crc32x: (bool * (string list)) -> maybe_instruction
909val p_bfm_etc: (bool * (bool * (string list))) -> maybe_instruction
910val p_ccmn_ccmp: (bool * (string list)) -> maybe_instruction
911val p_csel_etc: (bool * (bool * (string list))) -> maybe_instruction
912val p_extr: (string list) -> maybe_instruction
913val p_hint: (string list) -> maybe_instruction
914val p_call: (Nat.nat * (string list)) -> maybe_instruction
915val p_clrex: (string list) -> maybe_instruction
916val p_dmb_etc: (MemBarrierOp * (string list)) -> maybe_instruction
917val wzr_xzr: string -> string
918val convert_immediate: (bool * BitsN.nbit) -> (string list)
919val p_mov: (string list) -> maybe_instruction
920val p_shift: (ShiftType * (string list)) -> maybe_instruction
921val p_neg: (bool * (string list)) -> maybe_instruction
922val convert_bfxil_etc: (string list) -> (string list)
923val convert_bfi_etc: (string list) -> (string list)
924val convert_cinc_etc: (string list) -> (string list)
925val convert_cset_csetm: (string list) -> (string list)
926val convert_zr1: (string list) -> (string list)
927val convert_zr2: (string list) -> (string list)
928val convert_zr_end: (string list) -> (string list)
929val p_tokens: string -> (string list)
930val instructionFromString: string -> maybe_instruction
931val EncodeARM: string -> (string * (string option))
932val s_cond: BitsN.nbit -> string
933val s_regz: (bool * BitsN.nbit) -> string
934val s_regp: (bool * BitsN.nbit) -> string
935val s_reg2z: (bool * (BitsN.nbit * BitsN.nbit)) -> string
936val s_reg3z: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string
937val s_reg4z:
938  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) ->
939  string
940val s_nat: Nat.nat -> string
941val s_dec: Nat.nat -> BitsN.nbit -> string
942val s_hex: Nat.nat -> BitsN.nbit -> string
943val s_immn: Nat.nat -> string
944val s_imm: Nat.nat -> BitsN.nbit -> string
945val s_offset: BitsN.nbit -> string
946val s_signed_imm: BitsN.nbit -> string
947val s_shifted_imm: Nat.nat -> BitsN.nbit -> string
948val s_extend_type: ExtendType -> string
949val s_shift_type: ShiftType -> string
950val s_move_wide_op: MoveWideOp -> string
951val s_logical_op: LogicalOp -> string
952val s_invert_logical_op: LogicalOp -> string
953val s_rev_op: RevOp -> string
954val s_hint_op: SystemHintOp -> string
955val s_barrier_op: MemBarrierOp -> string
956val s_shift_amount: (ShiftType * Nat.nat) -> string
957val s_nzcv: (bool * (bool * (bool * bool))) -> string
958val s_data: Data -> (string * string)
959val s_crc: CRCExt -> (string * string)
960val s_branch: Branch -> (string * string)
961val s_debug: Debug -> (string * string)
962val s_system: System -> (string * string)
963val s_load_store: LoadStore -> (string * string)
964val instructionToString: instruction -> (string * string)
965val diss: string -> string
966
967end