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