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