1(* m0 - generated by L3 - Mon Sep 18 10:36:51 2017 *) 2 3signature m0 = 4sig 5 6structure Map : Map 7 8(* ------------------------------------------------------------------------- 9 Types 10 ------------------------------------------------------------------------- *) 11 12type PRIMASK = { PM: bool, primask'rst: BitsN.nbit } 13 14type PSR = 15 { C: bool, ExceptionNumber: BitsN.nbit, N: bool, T: bool, V: bool, 16 Z: bool, psr'rst: BitsN.nbit } 17 18type CONTROL = { SPSEL: bool, control'rst: bool, nPRIV: bool } 19 20type AIRCR = 21 { ENDIANNESS: bool, SYSRESETREQ: bool, VECTCLRACTIVE: bool, 22 VECTKEY: BitsN.nbit, aircr'rst: BitsN.nbit } 23 24type CCR = { STKALIGN: bool, UNALIGN_TRP: bool, ccr'rst: BitsN.nbit } 25 26type SHPR2 = { PRI_11: BitsN.nbit, shpr2'rst: BitsN.nbit } 27 28type SHPR3 = 29 { PRI_14: BitsN.nbit, PRI_15: BitsN.nbit, shpr3'rst: BitsN.nbit } 30 31type IPR = 32 { PRI_N0: BitsN.nbit, PRI_N1: BitsN.nbit, PRI_N2: BitsN.nbit, 33 PRI_N3: BitsN.nbit, ipr'rst: BitsN.nbit } 34 35datatype Mode = Mode_Thread | Mode_Handler 36 37datatype ARM_Exception 38 = ExternalInterrupt of BitsN.nbit 39 | HardFault 40 | NMI 41 | PendSV 42 | Reset 43 | SVCall 44 | SysTick 45 46datatype RName 47 = RName_0 | RName_1 | RName_2 | RName_3 | RName_4 | RName_5 | RName_6 48 | RName_7 | RName_8 | RName_9 | RName_10 | RName_11 | RName_12 49 | RName_SP_main | RName_SP_process | RName_LR | RName_PC 50 51datatype SRType 52 = SRType_LSL | SRType_LSR | SRType_ASR | SRType_ROR | SRType_RRX 53 54datatype offset 55 = immediate_form of BitsN.nbit | register_form of BitsN.nbit 56 57datatype Hint 58 = Breakpoint of BitsN.nbit 59 | DataMemoryBarrier of BitsN.nbit 60 | DataSynchronizationBarrier of BitsN.nbit 61 | InstructionSynchronizationBarrier of BitsN.nbit 62 | SendEvent of unit 63 | WaitForEvent of unit 64 | WaitForInterrupt of unit 65 | Yield of unit 66 67datatype System 68 = ChangeProcessorState of bool 69 | MoveToRegisterFromSpecial of BitsN.nbit * BitsN.nbit 70 | MoveToSpecialRegister of BitsN.nbit * BitsN.nbit 71 | SupervisorCall of BitsN.nbit 72 73datatype Store 74 = Push of BitsN.nbit 75 | StoreByte of BitsN.nbit * (BitsN.nbit * offset) 76 | StoreHalf of BitsN.nbit * (BitsN.nbit * offset) 77 | StoreMultiple of BitsN.nbit * BitsN.nbit 78 | StoreWord of BitsN.nbit * (BitsN.nbit * offset) 79 80datatype Load 81 = LoadByte of bool * (BitsN.nbit * (BitsN.nbit * offset)) 82 | LoadHalf of bool * (BitsN.nbit * (BitsN.nbit * offset)) 83 | LoadLiteral of BitsN.nbit * BitsN.nbit 84 | LoadMultiple of bool * (BitsN.nbit * BitsN.nbit) 85 | LoadWord of BitsN.nbit * (BitsN.nbit * offset) 86 87datatype Media 88 = ByteReverse of BitsN.nbit * BitsN.nbit 89 | ByteReversePackedHalfword of BitsN.nbit * BitsN.nbit 90 | ByteReverseSignedHalfword of BitsN.nbit * BitsN.nbit 91 | ExtendByte of bool * (BitsN.nbit * BitsN.nbit) 92 | ExtendHalfword of bool * (BitsN.nbit * BitsN.nbit) 93 94datatype Multiply = Multiply32 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 95 96datatype Data 97 = ArithLogicImmediate of 98 BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 99 | CompareImmediate of BitsN.nbit * BitsN.nbit 100 | Move of BitsN.nbit * BitsN.nbit 101 | Register of 102 BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) 103 | ShiftImmediate of 104 bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))) 105 | ShiftRegister of BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit)) 106 | TestCompareRegister of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 107 108datatype Branch 109 = BranchExchange of BitsN.nbit 110 | BranchLinkExchangeRegister of BitsN.nbit 111 | BranchLinkImmediate of BitsN.nbit 112 | BranchTarget of BitsN.nbit 113 114datatype instruction 115 = Branch of Branch 116 | Data of Data 117 | Hint of Hint 118 | Load of Load 119 | Media of Media 120 | Multiply of Multiply 121 | NoOperation of unit 122 | Store of Store 123 | System of System 124 | Undefined of BitsN.nbit 125 126datatype MachineCode 127 = Thumb of BitsN.nbit | Thumb2 of BitsN.nbit * BitsN.nbit 128 129datatype enc = Enc_Thumb | Enc_Narrow | Enc_Wide 130 131datatype maybeMachineCode 132 = BadCode of string 133 | Thumb16 of BitsN.nbit 134 | Thumb32 of BitsN.nbit * BitsN.nbit 135 136datatype maybe_instruction 137 = FAIL of string 138 | HALFWORD of BitsN.nbit 139 | OK of (BitsN.nbit * string) * instruction 140 | PENDING of string * ((BitsN.nbit * string) * instruction) 141 142datatype nat_or_reg = NAT of Nat.nat | REGISTER of BitsN.nbit 143 144(* ------------------------------------------------------------------------- 145 Exceptions 146 ------------------------------------------------------------------------- *) 147 148exception ASSERT of string 149 150exception UNPREDICTABLE of string 151 152(* ------------------------------------------------------------------------- 153 Functions 154 ------------------------------------------------------------------------- *) 155 156structure Cast: 157sig 158 159val natToMode: Nat.nat -> Mode 160val ModeToNat: Mode -> Nat.nat 161val stringToMode: string -> Mode 162val ModeToString: Mode -> string 163val natToRName: Nat.nat -> RName 164val RNameToNat: RName -> Nat.nat 165val stringToRName: string -> RName 166val RNameToString: RName -> string 167val natToSRType: Nat.nat -> SRType 168val SRTypeToNat: SRType -> Nat.nat 169val stringToSRType: string -> SRType 170val SRTypeToString: SRType -> string 171val natToenc: Nat.nat -> enc 172val encToNat: enc -> Nat.nat 173val stringToenc: string -> enc 174val encToString: enc -> string 175 176end 177 178val AIRCR: AIRCR ref 179val CCR: CCR ref 180val CONTROL: CONTROL ref 181val CurrentMode: Mode ref 182val ExceptionActive: (bool Map.map) ref 183val MEM: (BitsN.nbit Map.map) ref 184val NVIC_IPR: (IPR Map.map) ref 185val PRIMASK: PRIMASK ref 186val PSR: PSR ref 187val REG: (BitsN.nbit Map.map) ref 188val SHPR2: SHPR2 ref 189val SHPR3: SHPR3 ref 190val VTOR: BitsN.nbit ref 191val count: Nat.nat ref 192val pcinc: BitsN.nbit ref 193val pending: (ARM_Exception option) ref 194val PRIMASK_PM_rupd: PRIMASK * bool -> PRIMASK 195val PRIMASK_primask'rst_rupd: PRIMASK * BitsN.nbit -> PRIMASK 196val PSR_C_rupd: PSR * bool -> PSR 197val PSR_ExceptionNumber_rupd: PSR * BitsN.nbit -> PSR 198val PSR_N_rupd: PSR * bool -> PSR 199val PSR_T_rupd: PSR * bool -> PSR 200val PSR_V_rupd: PSR * bool -> PSR 201val PSR_Z_rupd: PSR * bool -> PSR 202val PSR_psr'rst_rupd: PSR * BitsN.nbit -> PSR 203val CONTROL_SPSEL_rupd: CONTROL * bool -> CONTROL 204val CONTROL_control'rst_rupd: CONTROL * bool -> CONTROL 205val CONTROL_nPRIV_rupd: CONTROL * bool -> CONTROL 206val AIRCR_ENDIANNESS_rupd: AIRCR * bool -> AIRCR 207val AIRCR_SYSRESETREQ_rupd: AIRCR * bool -> AIRCR 208val AIRCR_VECTCLRACTIVE_rupd: AIRCR * bool -> AIRCR 209val AIRCR_VECTKEY_rupd: AIRCR * BitsN.nbit -> AIRCR 210val AIRCR_aircr'rst_rupd: AIRCR * BitsN.nbit -> AIRCR 211val CCR_STKALIGN_rupd: CCR * bool -> CCR 212val CCR_UNALIGN_TRP_rupd: CCR * bool -> CCR 213val CCR_ccr'rst_rupd: CCR * BitsN.nbit -> CCR 214val SHPR2_PRI_11_rupd: SHPR2 * BitsN.nbit -> SHPR2 215val SHPR2_shpr2'rst_rupd: SHPR2 * BitsN.nbit -> SHPR2 216val SHPR3_PRI_14_rupd: SHPR3 * BitsN.nbit -> SHPR3 217val SHPR3_PRI_15_rupd: SHPR3 * BitsN.nbit -> SHPR3 218val SHPR3_shpr3'rst_rupd: SHPR3 * BitsN.nbit -> SHPR3 219val IPR_PRI_N0_rupd: IPR * BitsN.nbit -> IPR 220val IPR_PRI_N1_rupd: IPR * BitsN.nbit -> IPR 221val IPR_PRI_N2_rupd: IPR * BitsN.nbit -> IPR 222val IPR_PRI_N3_rupd: IPR * BitsN.nbit -> IPR 223val IPR_ipr'rst_rupd: IPR * BitsN.nbit -> IPR 224val boolify'16: 225 BitsN.nbit -> 226 bool * 227 (bool * 228 (bool * 229 (bool * 230 (bool * 231 (bool * 232 (bool * 233 (bool * 234 (bool * 235 (bool * (bool * (bool * (bool * (bool * (bool * bool)))))))))))))) 236val boolify'4: BitsN.nbit -> bool * (bool * (bool * bool)) 237val rec'PRIMASK: BitsN.nbit -> PRIMASK 238val reg'PRIMASK: PRIMASK -> BitsN.nbit 239val write'rec'PRIMASK: (BitsN.nbit * PRIMASK) -> BitsN.nbit 240val write'reg'PRIMASK: (PRIMASK * BitsN.nbit) -> PRIMASK 241val rec'PSR: BitsN.nbit -> PSR 242val reg'PSR: PSR -> BitsN.nbit 243val write'rec'PSR: (BitsN.nbit * PSR) -> BitsN.nbit 244val write'reg'PSR: (PSR * BitsN.nbit) -> PSR 245val rec'CONTROL: BitsN.nbit -> CONTROL 246val reg'CONTROL: CONTROL -> BitsN.nbit 247val write'rec'CONTROL: (BitsN.nbit * CONTROL) -> BitsN.nbit 248val write'reg'CONTROL: (CONTROL * BitsN.nbit) -> CONTROL 249val rec'AIRCR: BitsN.nbit -> AIRCR 250val reg'AIRCR: AIRCR -> BitsN.nbit 251val write'rec'AIRCR: (BitsN.nbit * AIRCR) -> BitsN.nbit 252val write'reg'AIRCR: (AIRCR * BitsN.nbit) -> AIRCR 253val rec'CCR: BitsN.nbit -> CCR 254val reg'CCR: CCR -> BitsN.nbit 255val write'rec'CCR: (BitsN.nbit * CCR) -> BitsN.nbit 256val write'reg'CCR: (CCR * BitsN.nbit) -> CCR 257val rec'SHPR2: BitsN.nbit -> SHPR2 258val reg'SHPR2: SHPR2 -> BitsN.nbit 259val write'rec'SHPR2: (BitsN.nbit * SHPR2) -> BitsN.nbit 260val write'reg'SHPR2: (SHPR2 * BitsN.nbit) -> SHPR2 261val rec'SHPR3: BitsN.nbit -> SHPR3 262val reg'SHPR3: SHPR3 -> BitsN.nbit 263val write'rec'SHPR3: (BitsN.nbit * SHPR3) -> BitsN.nbit 264val write'reg'SHPR3: (SHPR3 * BitsN.nbit) -> SHPR3 265val rec'IPR: BitsN.nbit -> IPR 266val reg'IPR: IPR -> BitsN.nbit 267val write'rec'IPR: (BitsN.nbit * IPR) -> BitsN.nbit 268val write'reg'IPR: (IPR * BitsN.nbit) -> IPR 269val ProcessorID: unit -> IntInf.int 270val ConditionPassed: BitsN.nbit -> bool 271val Raise: ARM_Exception -> unit 272val CurrentModeIsPrivileged: unit -> bool 273val LookUpSP: unit -> RName 274val R: BitsN.nbit -> BitsN.nbit 275val write'R: (BitsN.nbit * BitsN.nbit) -> unit 276val SP_main: unit -> BitsN.nbit 277val write'SP_main: BitsN.nbit -> unit 278val SP_process: unit -> BitsN.nbit 279val write'SP_process: BitsN.nbit -> unit 280val SP: unit -> BitsN.nbit 281val write'SP: BitsN.nbit -> unit 282val LR: unit -> BitsN.nbit 283val write'LR: BitsN.nbit -> unit 284val PC: unit -> BitsN.nbit 285val write'PC: BitsN.nbit -> unit 286val mem1: BitsN.nbit -> (bool list) 287val mem: (BitsN.nbit * Nat.nat) -> (bool list) 288val write'mem: ((bool list) * (BitsN.nbit * Nat.nat)) -> unit 289val BigEndianReverse: ((bool list) * Nat.nat) -> (bool list) 290val Align: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit 291val Aligned: Nat.nat -> (BitsN.nbit * Nat.nat) -> bool 292val MemA: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit 293val write'MemA: Nat.nat -> (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit 294val MemU: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit 295val write'MemU: Nat.nat -> (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit 296val ExcNumber: ARM_Exception -> BitsN.nbit 297val TakeReset: unit -> unit 298val ExceptionPriority: Nat.nat -> IntInf.int 299val ExecutionPriority: unit -> IntInf.int 300val ReturnAddress: unit -> BitsN.nbit 301val PushStack: unit -> unit 302val ExceptionTaken: BitsN.nbit -> unit 303val ExceptionEntry: unit -> unit 304val PopStack: (BitsN.nbit * BitsN.nbit) -> unit 305val DeActivate: BitsN.nbit -> unit 306val IsOnes: Nat.nat -> BitsN.nbit -> bool 307val ExceptionActiveBitCount: unit -> Nat.nat 308val ExceptionReturn: BitsN.nbit -> unit 309val CallSupervisor: unit -> unit 310val BranchTo: BitsN.nbit -> unit 311val BranchWritePC: BitsN.nbit -> unit 312val BXWritePC: BitsN.nbit -> unit 313val BLXWritePC: BitsN.nbit -> unit 314val LoadWritePC: BitsN.nbit -> unit 315val ALUWritePC: BitsN.nbit -> unit 316val IncPC: unit -> unit 317val HighestSetBit: Nat.nat -> BitsN.nbit -> IntInf.int 318val CountLeadingZeroBits: Nat.nat -> BitsN.nbit -> Nat.nat 319val LowestSetBit: Nat.nat -> BitsN.nbit -> Nat.nat 320val BitCount: Nat.nat -> BitsN.nbit -> Nat.nat 321val SignExtendFrom: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit 322val Extend: Nat.nat * Nat.nat -> (bool * BitsN.nbit) -> BitsN.nbit 323val UInt: Nat.nat -> BitsN.nbit -> IntInf.int 324val LSL_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool) 325val LSL: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit 326val LSR_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool) 327val LSR: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit 328val ASR_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool) 329val ASR: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit 330val ROR_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool) 331val ROR: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit 332val RRX_C: Nat.nat -> (BitsN.nbit * bool) -> (BitsN.nbit * bool) 333val RRX: Nat.nat -> (BitsN.nbit * bool) -> BitsN.nbit 334val DecodeImmShift: (BitsN.nbit * BitsN.nbit) -> (SRType * Nat.nat) 335val DecodeRegShift: BitsN.nbit -> SRType 336val Shift_C: Nat.nat -> 337 (BitsN.nbit * (SRType * (Nat.nat * bool))) -> (BitsN.nbit * bool) 338val Shift: Nat.nat -> 339 (BitsN.nbit * (SRType * (Nat.nat * bool))) -> BitsN.nbit 340val AddWithCarry: Nat.nat -> 341 (BitsN.nbit * (BitsN.nbit * bool)) -> (BitsN.nbit * (bool * bool)) 342val DataProcessingALU: 343 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))) -> 344 (BitsN.nbit * (bool * bool)) 345val ArithmeticOpcode: BitsN.nbit -> bool 346val dfn'BranchTarget: BitsN.nbit -> unit 347val dfn'BranchExchange: BitsN.nbit -> unit 348val dfn'BranchLinkImmediate: BitsN.nbit -> unit 349val dfn'BranchLinkExchangeRegister: BitsN.nbit -> unit 350val DataProcessing: 351 (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))))) -> 352 unit 353val DataProcessingPC: 354 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))) -> unit 355val dfn'Move: (BitsN.nbit * BitsN.nbit) -> unit 356val dfn'CompareImmediate: (BitsN.nbit * BitsN.nbit) -> unit 357val dfn'ArithLogicImmediate: 358 (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit 359val doRegister: 360 (BitsN.nbit * 361 (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))))) -> 362 unit 363val dfn'Register: 364 (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit 365val dfn'TestCompareRegister: 366 (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 367val dfn'ShiftImmediate: 368 (bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat))))) -> 369 unit 370val dfn'ShiftRegister: 371 (BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit))) -> unit 372val dfn'Multiply32: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 373val dfn'ExtendByte: (bool * (BitsN.nbit * BitsN.nbit)) -> unit 374val dfn'ExtendHalfword: (bool * (BitsN.nbit * BitsN.nbit)) -> unit 375val dfn'ByteReverse: (BitsN.nbit * BitsN.nbit) -> unit 376val dfn'ByteReversePackedHalfword: (BitsN.nbit * BitsN.nbit) -> unit 377val dfn'ByteReverseSignedHalfword: (BitsN.nbit * BitsN.nbit) -> unit 378val dfn'LoadWord: (BitsN.nbit * (BitsN.nbit * offset)) -> unit 379val dfn'LoadLiteral: (BitsN.nbit * BitsN.nbit) -> unit 380val dfn'LoadByte: (bool * (BitsN.nbit * (BitsN.nbit * offset))) -> unit 381val dfn'LoadHalf: (bool * (BitsN.nbit * (BitsN.nbit * offset))) -> unit 382val dfn'LoadMultiple: (bool * (BitsN.nbit * BitsN.nbit)) -> unit 383val dfn'StoreWord: (BitsN.nbit * (BitsN.nbit * offset)) -> unit 384val dfn'StoreByte: (BitsN.nbit * (BitsN.nbit * offset)) -> unit 385val dfn'StoreHalf: (BitsN.nbit * (BitsN.nbit * offset)) -> unit 386val dfn'StoreMultiple: (BitsN.nbit * BitsN.nbit) -> unit 387val dfn'Push: BitsN.nbit -> unit 388val dfn'SupervisorCall: BitsN.nbit -> unit 389val dfn'ChangeProcessorState: bool -> unit 390val dfn'MoveToRegisterFromSpecial: (BitsN.nbit * BitsN.nbit) -> unit 391val dfn'MoveToSpecialRegister: (BitsN.nbit * BitsN.nbit) -> unit 392val dfn'Undefined: BitsN.nbit -> unit 393val dfn'NoOperation: unit -> unit 394val dfn'Breakpoint: BitsN.nbit -> unit 395val dfn'DataMemoryBarrier: BitsN.nbit -> unit 396val dfn'DataSynchronizationBarrier: BitsN.nbit -> unit 397val dfn'InstructionSynchronizationBarrier: BitsN.nbit -> unit 398val dfn'SendEvent: unit -> unit 399val dfn'WaitForEvent: unit -> unit 400val dfn'WaitForInterrupt: unit -> unit 401val dfn'Yield: unit -> unit 402val Run: instruction -> unit 403val Fetch: unit -> MachineCode 404val DECODE_UNPREDICTABLE: (MachineCode * string) -> unit 405val DecodeThumb: BitsN.nbit -> instruction 406val DecodeThumb2: (BitsN.nbit * BitsN.nbit) -> instruction 407val Decode: MachineCode -> instruction 408val Next: unit -> unit 409val EncodeImmShift: (SRType * Nat.nat) -> (BitsN.nbit * BitsN.nbit) 410val e_branch: (BitsN.nbit * (Branch * enc)) -> maybeMachineCode 411val e_data: Data -> maybeMachineCode 412val e_media: Media -> maybeMachineCode 413val e_hint: (Hint * enc) -> maybeMachineCode 414val e_system: System -> maybeMachineCode 415val e_multiply: Multiply -> maybeMachineCode 416val e_load: Load -> maybeMachineCode 417val e_store: Store -> maybeMachineCode 418val instructionEncode: 419 (BitsN.nbit * (instruction * enc)) -> maybeMachineCode 420val SetPassCondition: BitsN.nbit -> unit 421val Encode: (BitsN.nbit * (instruction * enc)) -> maybeMachineCode 422val al: BitsN.nbit * string 423val stripSpaces: string -> string 424val p_number: string -> (Nat.nat option) 425val p_signed_number: (bool * string) -> ((bool * Nat.nat) option) 426val p_encode_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option) 427val p_encode_signed_immediate: Nat.nat -> 428 (bool * string) -> ((bool * (bool * BitsN.nbit)) option) 429val p_encode_signed_offset: Nat.nat -> 430 (bool * string) -> ((bool * BitsN.nbit) option) 431val p_unbounded_immediate: string -> (Nat.nat option) 432val p_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option) 433val p_immediate_number: Nat.nat -> string -> ((bool * BitsN.nbit) option) 434val p_signed_immediate: Nat.nat -> 435 string -> ((bool * (bool * BitsN.nbit)) option) 436val p_signed_offset: Nat.nat -> string -> ((bool * BitsN.nbit) option) 437val p_offset: Nat.nat -> string -> ((bool * BitsN.nbit) option) 438val p_label: string -> (string option) 439val p_cond: string -> (BitsN.nbit option) 440val p_suffix: string -> ((BitsN.nbit * string) option) 441val p_al_suffix: string -> ((BitsN.nbit * string) option) 442val p_special_register: string -> (BitsN.nbit option) 443val p_register: string -> (BitsN.nbit option) 444val p_register1: (string list) -> (BitsN.nbit option) 445val p_register2: (string list) -> ((BitsN.nbit * BitsN.nbit) option) 446val p_register3: 447 (string list) -> ((BitsN.nbit * (BitsN.nbit * BitsN.nbit)) option) 448val p_shift_amount: 449 (SRType * (char * string)) -> (string * (SRType * nat_or_reg)) 450val p_shift_imm_or_reg: string -> (string * (SRType * nat_or_reg)) 451val p_arith_logic_full: 452 (string * (BitsN.nbit * (bool * (string list)))) -> maybe_instruction 453val p_arith_logic: 454 (string * (BitsN.nbit * (bool * (string list)))) -> maybe_instruction 455val p_test_compare: 456 (string * (BitsN.nbit * (string list))) -> maybe_instruction 457val p_mov_mvn: 458 (string * (bool * (bool * (string list)))) -> maybe_instruction 459val p_shift_full: (string * (SRType * (string list))) -> maybe_instruction 460val p_shift: (string * (SRType * (string list))) -> maybe_instruction 461val p_adr: (string * (string list)) -> maybe_instruction 462val p_bx: (string * (string list)) -> maybe_instruction 463val p_bl: (string * (string list)) -> maybe_instruction 464val p_b: (string * (string list)) -> maybe_instruction 465val p_blx: (string * (string list)) -> maybe_instruction 466val p_mul: (string * (string list)) -> maybe_instruction 467val p_sxtb_etc: 468 (string * (bool * (bool * (string list)))) -> maybe_instruction 469val p_rev: (string * (string list)) -> maybe_instruction 470val p_rev16: (string * (string list)) -> maybe_instruction 471val p_revsh: (string * (string list)) -> maybe_instruction 472val closingRegList: string -> (string option) 473val p_reg_list: (BitsN.nbit * string) -> (BitsN.nbit option) 474val p_registers_loop: (BitsN.nbit * (string list)) -> (BitsN.nbit option) 475val p_registers: (string list) -> (BitsN.nbit option) 476val closingAddress: (string list) -> (string option) 477val p_address_mode: 478 (string list) -> (string * ((BitsN.nbit * offset) option)) 479val pick_ldr_str: 480 (Nat.nat * (BitsN.nbit * (BitsN.nbit * offset))) -> instruction 481val p_ldr_str: (string * (Nat.nat * (string list))) -> maybe_instruction 482val p_ldrb_ldrh: 483 (string * (bool * (bool * (string list)))) -> maybe_instruction 484val p_pop_push: (string * (bool * (string list))) -> maybe_instruction 485val p_ldm_stm: (string * (bool * (string list))) -> maybe_instruction 486val p_cps: (bool * (string list)) -> maybe_instruction 487val p_mrs: (string * (string list)) -> maybe_instruction 488val p_msr: (string * (string list)) -> maybe_instruction 489val p_barrier_option: (string list) -> (BitsN.nbit option) 490val p_dmb_dsb: (string * (bool * (string list))) -> maybe_instruction 491val p_isb: (string * (string list)) -> maybe_instruction 492val p_call: (string * (Nat.nat * (string list))) -> maybe_instruction 493val p_noarg: (string * instruction) -> maybe_instruction 494val p_tokens: string -> (string list) 495val instructionFromString: string -> maybe_instruction 496val halfString: BitsN.nbit -> string 497val EncodeThumb: string -> (string * (string option)) 498val s_cond: BitsN.nbit -> string 499val s_reg: BitsN.nbit -> string 500val s_reg2: (BitsN.nbit * BitsN.nbit) -> string 501val s_reg3: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> string 502val s_reg4: 503 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 504val s_hex: Nat.nat -> BitsN.nbit -> string 505val s_offset: BitsN.nbit -> string 506val s_maybe_offset: BitsN.nbit -> string 507val s_special_reg: BitsN.nbit -> string 508val s_barrier_option: BitsN.nbit -> string 509val s_imm_form: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> string 510val s_reg_form: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> string 511val contiguous: 512 (((Nat.nat * Nat.nat) list) * (Nat.nat * (bool list))) -> 513 ((Nat.nat * Nat.nat) list) 514val s_registers_from_contiguous: 515 (string * ((Nat.nat * Nat.nat) list)) -> string 516val s_registers: Nat.nat -> BitsN.nbit -> string 517val s_test_compare: BitsN.nbit -> string 518val s_arith_logic: BitsN.nbit -> string 519val s_shift: SRType -> string 520val s_shift_n: (SRType * Nat.nat) -> string 521val s_shift_r: (bool * (BitsN.nbit * (SRType * Nat.nat))) -> string 522val s_branch: (BitsN.nbit * Branch) -> (string * string) 523val s_data: Data -> (string * string) 524val s_load: Load -> (string * string) 525val s_store: Store -> (string * string) 526val s_hint: Hint -> (string * string) 527val s_media: Media -> (string * string) 528val s_system: System -> (string * string) 529val instructionToString: (BitsN.nbit * instruction) -> (string * string) 530 531end