1(* m0 - generated by L3 - Thu Jun 22 15:54:54 2017 *) 2 3structure m0 :> m0 = 4struct 5 6structure Map = MutableMap 7 8(* ------------------------------------------------------------------------- 9 Type declarations 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 Casting maps (for enumerated types) 146 ------------------------------------------------------------------------- *) 147 148structure Cast = 149struct 150fun natToMode x = 151 case Nat.toInt x of 152 0 => Mode_Thread | 1 => Mode_Handler | _ => raise Fail "natToMode" 153 154fun natToRName x = 155 case Nat.toInt x of 156 0 => RName_0 157 | 1 => RName_1 158 | 2 => RName_2 159 | 3 => RName_3 160 | 4 => RName_4 161 | 5 => RName_5 162 | 6 => RName_6 163 | 7 => RName_7 164 | 8 => RName_8 165 | 9 => RName_9 166 | 10 => RName_10 167 | 11 => RName_11 168 | 12 => RName_12 169 | 13 => RName_SP_main 170 | 14 => RName_SP_process 171 | 15 => RName_LR 172 | 16 => RName_PC 173 | _ => raise Fail "natToRName" 174 175fun natToSRType x = 176 case Nat.toInt x of 177 0 => SRType_LSL 178 | 1 => SRType_LSR 179 | 2 => SRType_ASR 180 | 3 => SRType_ROR 181 | 4 => SRType_RRX 182 | _ => raise Fail "natToSRType" 183 184fun natToenc x = 185 case Nat.toInt x of 186 0 => Enc_Thumb 187 | 1 => Enc_Narrow 188 | 2 => Enc_Wide 189 | _ => raise Fail "natToenc" 190 191fun ModeToNat x = 192 case x of 193 Mode_Thread => 0 | Mode_Handler => 1 194 195fun RNameToNat x = 196 case x of 197 RName_0 => 0 198 | RName_1 => 1 199 | RName_2 => 2 200 | RName_3 => 3 201 | RName_4 => 4 202 | RName_5 => 5 203 | RName_6 => 6 204 | RName_7 => 7 205 | RName_8 => 8 206 | RName_9 => 9 207 | RName_10 => 10 208 | RName_11 => 11 209 | RName_12 => 12 210 | RName_SP_main => 13 211 | RName_SP_process => 14 212 | RName_LR => 15 213 | RName_PC => 16 214 215fun SRTypeToNat x = 216 case x of 217 SRType_LSL => 0 218 | SRType_LSR => 1 219 | SRType_ASR => 2 220 | SRType_ROR => 3 221 | SRType_RRX => 4 222 223fun encToNat x = 224 case x of 225 Enc_Thumb => 0 | Enc_Narrow => 1 | Enc_Wide => 2 226 227fun ModeToString x = 228 case x of 229 Mode_Thread => "Mode_Thread" | Mode_Handler => "Mode_Handler" 230 231fun RNameToString x = 232 case x of 233 RName_0 => "RName_0" 234 | RName_1 => "RName_1" 235 | RName_2 => "RName_2" 236 | RName_3 => "RName_3" 237 | RName_4 => "RName_4" 238 | RName_5 => "RName_5" 239 | RName_6 => "RName_6" 240 | RName_7 => "RName_7" 241 | RName_8 => "RName_8" 242 | RName_9 => "RName_9" 243 | RName_10 => "RName_10" 244 | RName_11 => "RName_11" 245 | RName_12 => "RName_12" 246 | RName_SP_main => "RName_SP_main" 247 | RName_SP_process => "RName_SP_process" 248 | RName_LR => "RName_LR" 249 | RName_PC => "RName_PC" 250 251fun SRTypeToString x = 252 case x of 253 SRType_LSL => "SRType_LSL" 254 | SRType_LSR => "SRType_LSR" 255 | SRType_ASR => "SRType_ASR" 256 | SRType_ROR => "SRType_ROR" 257 | SRType_RRX => "SRType_RRX" 258 259fun encToString x = 260 case x of 261 Enc_Thumb => "Enc_Thumb" 262 | Enc_Narrow => "Enc_Narrow" 263 | Enc_Wide => "Enc_Wide" 264 265fun stringToMode x = 266 case x of 267 "Mode_Thread" => Mode_Thread 268 | "Mode_Handler" => Mode_Handler 269 | _ => raise Fail "stringToMode" 270 271fun stringToRName x = 272 case x of 273 "RName_0" => RName_0 274 | "RName_1" => RName_1 275 | "RName_2" => RName_2 276 | "RName_3" => RName_3 277 | "RName_4" => RName_4 278 | "RName_5" => RName_5 279 | "RName_6" => RName_6 280 | "RName_7" => RName_7 281 | "RName_8" => RName_8 282 | "RName_9" => RName_9 283 | "RName_10" => RName_10 284 | "RName_11" => RName_11 285 | "RName_12" => RName_12 286 | "RName_SP_main" => RName_SP_main 287 | "RName_SP_process" => RName_SP_process 288 | "RName_LR" => RName_LR 289 | "RName_PC" => RName_PC 290 | _ => raise Fail "stringToRName" 291 292fun stringToSRType x = 293 case x of 294 "SRType_LSL" => SRType_LSL 295 | "SRType_LSR" => SRType_LSR 296 | "SRType_ASR" => SRType_ASR 297 | "SRType_ROR" => SRType_ROR 298 | "SRType_RRX" => SRType_RRX 299 | _ => raise Fail "stringToSRType" 300 301fun stringToenc x = 302 case x of 303 "Enc_Thumb" => Enc_Thumb 304 | "Enc_Narrow" => Enc_Narrow 305 | "Enc_Wide" => Enc_Wide 306 | _ => raise Fail "stringToenc" 307end 308 309(* ------------------------------------------------------------------------- 310 Record update functions 311 ------------------------------------------------------------------------- *) 312 313fun PRIMASK_PM_rupd ({PM, primask'rst}: PRIMASK, x') = 314 {PM = x', primask'rst = primask'rst}: PRIMASK 315 316fun PRIMASK_primask'rst_rupd ({PM, primask'rst}: PRIMASK, x') = 317 {PM = PM, primask'rst = x'}: PRIMASK 318 319fun PSR_C_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst}: PSR, x') = 320 {C = x', ExceptionNumber = ExceptionNumber, N = N, T = T, V = V, Z = Z, 321 psr'rst = psr'rst}: PSR 322 323fun PSR_ExceptionNumber_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst} 324 : PSR, x') = 325 {C = C, ExceptionNumber = x', N = N, T = T, V = V, Z = Z, 326 psr'rst = psr'rst}: PSR 327 328fun PSR_N_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst}: PSR, x') = 329 {C = C, ExceptionNumber = ExceptionNumber, N = x', T = T, V = V, Z = Z, 330 psr'rst = psr'rst}: PSR 331 332fun PSR_T_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst}: PSR, x') = 333 {C = C, ExceptionNumber = ExceptionNumber, N = N, T = x', V = V, Z = Z, 334 psr'rst = psr'rst}: PSR 335 336fun PSR_V_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst}: PSR, x') = 337 {C = C, ExceptionNumber = ExceptionNumber, N = N, T = T, V = x', Z = Z, 338 psr'rst = psr'rst}: PSR 339 340fun PSR_Z_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst}: PSR, x') = 341 {C = C, ExceptionNumber = ExceptionNumber, N = N, T = T, V = V, Z = x', 342 psr'rst = psr'rst}: PSR 343 344fun PSR_psr'rst_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst} 345 : PSR, x') = 346 {C = C, ExceptionNumber = ExceptionNumber, N = N, T = T, V = V, Z = Z, 347 psr'rst = x'}: PSR 348 349fun CONTROL_SPSEL_rupd ({SPSEL, control'rst, nPRIV}: CONTROL, x') = 350 {SPSEL = x', control'rst = control'rst, nPRIV = nPRIV}: CONTROL 351 352fun CONTROL_control'rst_rupd ({SPSEL, control'rst, nPRIV}: CONTROL, x') = 353 {SPSEL = SPSEL, control'rst = x', nPRIV = nPRIV}: CONTROL 354 355fun CONTROL_nPRIV_rupd ({SPSEL, control'rst, nPRIV}: CONTROL, x') = 356 {SPSEL = SPSEL, control'rst = control'rst, nPRIV = x'}: CONTROL 357 358fun AIRCR_ENDIANNESS_rupd ({ENDIANNESS, SYSRESETREQ, VECTCLRACTIVE, 359 VECTKEY, aircr'rst}: AIRCR, x') = 360 {ENDIANNESS = x', SYSRESETREQ = SYSRESETREQ, 361 VECTCLRACTIVE = VECTCLRACTIVE, VECTKEY = VECTKEY, aircr'rst = aircr'rst} 362 : AIRCR 363 364fun AIRCR_SYSRESETREQ_rupd ({ENDIANNESS, SYSRESETREQ, VECTCLRACTIVE, 365 VECTKEY, aircr'rst}: AIRCR, x') = 366 {ENDIANNESS = ENDIANNESS, SYSRESETREQ = x', 367 VECTCLRACTIVE = VECTCLRACTIVE, VECTKEY = VECTKEY, aircr'rst = aircr'rst} 368 : AIRCR 369 370fun AIRCR_VECTCLRACTIVE_rupd ({ENDIANNESS, SYSRESETREQ, VECTCLRACTIVE, 371 VECTKEY, aircr'rst}: AIRCR, x') = 372 {ENDIANNESS = ENDIANNESS, SYSRESETREQ = SYSRESETREQ, VECTCLRACTIVE = x', 373 VECTKEY = VECTKEY, aircr'rst = aircr'rst}: AIRCR 374 375fun AIRCR_VECTKEY_rupd ({ENDIANNESS, SYSRESETREQ, VECTCLRACTIVE, VECTKEY, 376 aircr'rst}: AIRCR, x') = 377 {ENDIANNESS = ENDIANNESS, SYSRESETREQ = SYSRESETREQ, 378 VECTCLRACTIVE = VECTCLRACTIVE, VECTKEY = x', aircr'rst = aircr'rst} 379 : AIRCR 380 381fun AIRCR_aircr'rst_rupd ({ENDIANNESS, SYSRESETREQ, VECTCLRACTIVE, 382 VECTKEY, aircr'rst}: AIRCR, x') = 383 {ENDIANNESS = ENDIANNESS, SYSRESETREQ = SYSRESETREQ, 384 VECTCLRACTIVE = VECTCLRACTIVE, VECTKEY = VECTKEY, aircr'rst = x'} 385 : AIRCR 386 387fun CCR_STKALIGN_rupd ({STKALIGN, UNALIGN_TRP, ccr'rst}: CCR, x') = 388 {STKALIGN = x', UNALIGN_TRP = UNALIGN_TRP, ccr'rst = ccr'rst}: CCR 389 390fun CCR_UNALIGN_TRP_rupd ({STKALIGN, UNALIGN_TRP, ccr'rst}: CCR, x') = 391 {STKALIGN = STKALIGN, UNALIGN_TRP = x', ccr'rst = ccr'rst}: CCR 392 393fun CCR_ccr'rst_rupd ({STKALIGN, UNALIGN_TRP, ccr'rst}: CCR, x') = 394 {STKALIGN = STKALIGN, UNALIGN_TRP = UNALIGN_TRP, ccr'rst = x'}: CCR 395 396fun SHPR2_PRI_11_rupd ({PRI_11, shpr2'rst}: SHPR2, x') = 397 {PRI_11 = x', shpr2'rst = shpr2'rst}: SHPR2 398 399fun SHPR2_shpr2'rst_rupd ({PRI_11, shpr2'rst}: SHPR2, x') = 400 {PRI_11 = PRI_11, shpr2'rst = x'}: SHPR2 401 402fun SHPR3_PRI_14_rupd ({PRI_14, PRI_15, shpr3'rst}: SHPR3, x') = 403 {PRI_14 = x', PRI_15 = PRI_15, shpr3'rst = shpr3'rst}: SHPR3 404 405fun SHPR3_PRI_15_rupd ({PRI_14, PRI_15, shpr3'rst}: SHPR3, x') = 406 {PRI_14 = PRI_14, PRI_15 = x', shpr3'rst = shpr3'rst}: SHPR3 407 408fun SHPR3_shpr3'rst_rupd ({PRI_14, PRI_15, shpr3'rst}: SHPR3, x') = 409 {PRI_14 = PRI_14, PRI_15 = PRI_15, shpr3'rst = x'}: SHPR3 410 411fun IPR_PRI_N0_rupd ({PRI_N0, PRI_N1, PRI_N2, PRI_N3, ipr'rst}: IPR, x') = 412 {PRI_N0 = x', PRI_N1 = PRI_N1, PRI_N2 = PRI_N2, PRI_N3 = PRI_N3, 413 ipr'rst = ipr'rst}: IPR 414 415fun IPR_PRI_N1_rupd ({PRI_N0, PRI_N1, PRI_N2, PRI_N3, ipr'rst}: IPR, x') = 416 {PRI_N0 = PRI_N0, PRI_N1 = x', PRI_N2 = PRI_N2, PRI_N3 = PRI_N3, 417 ipr'rst = ipr'rst}: IPR 418 419fun IPR_PRI_N2_rupd ({PRI_N0, PRI_N1, PRI_N2, PRI_N3, ipr'rst}: IPR, x') = 420 {PRI_N0 = PRI_N0, PRI_N1 = PRI_N1, PRI_N2 = x', PRI_N3 = PRI_N3, 421 ipr'rst = ipr'rst}: IPR 422 423fun IPR_PRI_N3_rupd ({PRI_N0, PRI_N1, PRI_N2, PRI_N3, ipr'rst}: IPR, x') = 424 {PRI_N0 = PRI_N0, PRI_N1 = PRI_N1, PRI_N2 = PRI_N2, PRI_N3 = x', 425 ipr'rst = ipr'rst}: IPR 426 427fun IPR_ipr'rst_rupd ({PRI_N0, PRI_N1, PRI_N2, PRI_N3, ipr'rst} 428 : IPR, x') = 429 {PRI_N0 = PRI_N0, PRI_N1 = PRI_N1, PRI_N2 = PRI_N2, PRI_N3 = PRI_N3, 430 ipr'rst = x'}: IPR 431 432(* ------------------------------------------------------------------------- 433 Exceptions 434 ------------------------------------------------------------------------- *) 435 436exception ASSERT of string 437 438exception UNPREDICTABLE of string 439 440(* ------------------------------------------------------------------------- 441 Global variables (state) 442 ------------------------------------------------------------------------- *) 443 444val AIRCR = ref 445 ({ENDIANNESS = false, SYSRESETREQ = false, VECTCLRACTIVE = false, 446 VECTKEY = BitsN.B(0x0,16), aircr'rst = BitsN.B(0x0,13)}): AIRCR ref 447 448val CCR = ref 449 ({STKALIGN = false, UNALIGN_TRP = false, ccr'rst = BitsN.B(0x0,30)}) 450 : CCR ref 451 452val CONTROL = ref ({SPSEL = false, control'rst = false, nPRIV = false}) 453 : CONTROL ref 454 455val CurrentMode = ref (Mode_Handler): Mode ref 456 457val ExceptionActive = ref (Map.mkMap(SOME 64,false)): (bool Map.map) ref 458 459val MEM = ref (Map.mkMap(SOME 4294967296,BitsN.B(0x0,8))) 460 : (BitsN.nbit Map.map) ref 461 462val NVIC_IPR = ref 463 (Map.mkMap 464 (SOME 8, 465 {PRI_N0 = BitsN.B(0x0,2), PRI_N1 = BitsN.B(0x0,2), 466 PRI_N2 = BitsN.B(0x0,2), PRI_N3 = BitsN.B(0x0,2), 467 ipr'rst = BitsN.B(0x0,24)})): (IPR Map.map) ref 468 469val PRIMASK = ref ({PM = false, primask'rst = BitsN.B(0x0,31)}) 470 : PRIMASK ref 471 472val PSR = ref 473 ({C = false, ExceptionNumber = BitsN.B(0x0,6), N = false, T = false, 474 V = false, Z = false, psr'rst = BitsN.B(0x0,21)}): PSR ref 475 476val REG = ref (Map.mkMap(SOME 17,BitsN.B(0x0,32))) 477 : (BitsN.nbit Map.map) ref 478 479val SHPR2 = ref ({PRI_11 = BitsN.B(0x0,2), shpr2'rst = BitsN.B(0x0,30)}) 480 : SHPR2 ref 481 482val SHPR3 = ref 483 ({PRI_14 = BitsN.B(0x0,2), PRI_15 = BitsN.B(0x0,2), 484 shpr3'rst = BitsN.B(0x0,28)}): SHPR3 ref 485 486val VTOR = ref (BitsN.B(0x0,32)): BitsN.nbit ref 487 488val count = ref (0): Nat.nat ref 489 490val pcinc = ref (BitsN.B(0x0,32)): BitsN.nbit ref 491 492val pending = ref (NONE): (ARM_Exception option) ref 493 494(* ------------------------------------------------------------------------- 495 Main specification 496 ------------------------------------------------------------------------- *) 497 498local 499 fun tuple'16 [t0,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] = 500 (t0, 501 (t1, 502 (t2, 503 (t3,(t4,(t5,(t6,(t7,(t8,(t9,(t10,(t11,(t12,(t13,(t14,t15))))))))))))))) 504 | tuple'16 (_: bool list) = raise Fail "tuple'16" 505in 506 val boolify'16 = tuple'16 o BitsN.toList 507end 508 509local 510 fun tuple'4 [t0,t1,t2,t3] = (t0,(t1,(t2,t3))) 511 | tuple'4 (_: bool list) = raise Fail "tuple'4" 512in 513 val boolify'4 = tuple'4 o BitsN.toList 514end 515 516fun rec'PRIMASK x = 517 {PM = BitsN.bit(x,0), primask'rst = BitsN.bits(31,1) x}; 518 519fun reg'PRIMASK x = 520 case x of 521 {PM = PM, primask'rst = primask'rst} => 522 BitsN.@@(primask'rst,BitsN.fromBit PM); 523 524fun write'rec'PRIMASK (_,x) = reg'PRIMASK x; 525 526fun write'reg'PRIMASK (_,x) = rec'PRIMASK x; 527 528fun rec'PSR x = 529 {C = BitsN.bit(x,29), ExceptionNumber = BitsN.bits(5,0) x, 530 N = BitsN.bit(x,31), T = BitsN.bit(x,24), V = BitsN.bit(x,28), 531 Z = BitsN.bit(x,30), 532 psr'rst = BitsN.@@(BitsN.bits(23,6) x,BitsN.bits(27,25) x)}; 533 534fun reg'PSR x = 535 case x of 536 {C = C, ExceptionNumber = ExceptionNumber, N = N, T = T, V = V, 537 Z = Z, psr'rst = psr'rst} => 538 BitsN.concat 539 [BitsN.fromBit N,BitsN.fromBit Z,BitsN.fromBit C,BitsN.fromBit V, 540 BitsN.bits(2,0) psr'rst,BitsN.fromBit T, 541 BitsN.bits(20,3) psr'rst,ExceptionNumber]; 542 543fun write'rec'PSR (_,x) = reg'PSR x; 544 545fun write'reg'PSR (_,x) = rec'PSR x; 546 547fun rec'CONTROL x = 548 {SPSEL = BitsN.bit(x,1), control'rst = BitsN.bit(x,2), 549 nPRIV = BitsN.bit(x,0)}; 550 551fun reg'CONTROL x = 552 case x of 553 {SPSEL = SPSEL, control'rst = control'rst, nPRIV = nPRIV} => 554 BitsN.concat 555 [BitsN.fromBit control'rst,BitsN.fromBit SPSEL, 556 BitsN.fromBit nPRIV]; 557 558fun write'rec'CONTROL (_,x) = reg'CONTROL x; 559 560fun write'reg'CONTROL (_,x) = rec'CONTROL x; 561 562fun rec'AIRCR x = 563 {ENDIANNESS = BitsN.bit(x,15), SYSRESETREQ = BitsN.bit(x,2), 564 VECTCLRACTIVE = BitsN.bit(x,1), VECTKEY = BitsN.bits(31,16) x, 565 aircr'rst = BitsN.@@(BitsN.bits(0,0) x,BitsN.bits(14,3) x)}; 566 567fun reg'AIRCR x = 568 case x of 569 {ENDIANNESS = ENDIANNESS, SYSRESETREQ = SYSRESETREQ, 570 VECTCLRACTIVE = VECTCLRACTIVE, VECTKEY = VECTKEY, 571 aircr'rst = aircr'rst} => 572 BitsN.concat 573 [VECTKEY,BitsN.fromBit ENDIANNESS,BitsN.bits(11,0) aircr'rst, 574 BitsN.fromBit SYSRESETREQ,BitsN.fromBit VECTCLRACTIVE, 575 BitsN.bits(12,12) aircr'rst]; 576 577fun write'rec'AIRCR (_,x) = reg'AIRCR x; 578 579fun write'reg'AIRCR (_,x) = rec'AIRCR x; 580 581fun rec'CCR x = 582 {STKALIGN = BitsN.bit(x,9), UNALIGN_TRP = BitsN.bit(x,3), 583 ccr'rst = 584 BitsN.concat[BitsN.bits(2,0) x,BitsN.bits(8,4) x,BitsN.bits(31,10) x]}; 585 586fun reg'CCR x = 587 case x of 588 {STKALIGN = STKALIGN, UNALIGN_TRP = UNALIGN_TRP, ccr'rst = ccr'rst} => 589 BitsN.concat 590 [BitsN.bits(21,0) ccr'rst,BitsN.fromBit STKALIGN, 591 BitsN.bits(26,22) ccr'rst,BitsN.fromBit UNALIGN_TRP, 592 BitsN.bits(29,27) ccr'rst]; 593 594fun write'rec'CCR (_,x) = reg'CCR x; 595 596fun write'reg'CCR (_,x) = rec'CCR x; 597 598fun rec'SHPR2 x = 599 {PRI_11 = BitsN.bits(31,30) x, shpr2'rst = BitsN.bits(29,0) x}; 600 601fun reg'SHPR2 x = 602 case x of 603 {PRI_11 = PRI_11, shpr2'rst = shpr2'rst} => 604 BitsN.@@(PRI_11,shpr2'rst); 605 606fun write'rec'SHPR2 (_,x) = reg'SHPR2 x; 607 608fun write'reg'SHPR2 (_,x) = rec'SHPR2 x; 609 610fun rec'SHPR3 x = 611 {PRI_14 = BitsN.bits(23,22) x, PRI_15 = BitsN.bits(31,30) x, 612 shpr3'rst = BitsN.@@(BitsN.bits(21,0) x,BitsN.bits(29,24) x)}; 613 614fun reg'SHPR3 x = 615 case x of 616 {PRI_14 = PRI_14, PRI_15 = PRI_15, shpr3'rst = shpr3'rst} => 617 BitsN.concat 618 [PRI_15,BitsN.bits(5,0) shpr3'rst,PRI_14, 619 BitsN.bits(27,6) shpr3'rst]; 620 621fun write'rec'SHPR3 (_,x) = reg'SHPR3 x; 622 623fun write'reg'SHPR3 (_,x) = rec'SHPR3 x; 624 625fun rec'IPR x = 626 {PRI_N0 = BitsN.bits(7,6) x, PRI_N1 = BitsN.bits(15,14) x, 627 PRI_N2 = BitsN.bits(23,22) x, PRI_N3 = BitsN.bits(31,30) x, 628 ipr'rst = 629 BitsN.concat 630 [BitsN.bits(5,0) x,BitsN.bits(13,8) x,BitsN.bits(21,16) x, 631 BitsN.bits(29,24) x]}; 632 633fun reg'IPR x = 634 case x of 635 {PRI_N0 = PRI_N0, PRI_N1 = PRI_N1, PRI_N2 = PRI_N2, PRI_N3 = PRI_N3, 636 ipr'rst = ipr'rst} => 637 BitsN.concat 638 [PRI_N3,BitsN.bits(5,0) ipr'rst,PRI_N2,BitsN.bits(11,6) ipr'rst, 639 PRI_N1,BitsN.bits(17,12) ipr'rst,PRI_N0, 640 BitsN.bits(23,18) ipr'rst]; 641 642fun write'rec'IPR (_,x) = reg'IPR x; 643 644fun write'reg'IPR (_,x) = rec'IPR x; 645 646fun ProcessorID () = 0; 647 648fun ConditionPassed cond = 649 let 650 val result = 651 case BitsN.bits(3,1) cond of 652 BitsN.B(0x0,_) => #Z((!PSR) : PSR) 653 | BitsN.B(0x1,_) => #C((!PSR) : PSR) 654 | BitsN.B(0x2,_) => #N((!PSR) : PSR) 655 | BitsN.B(0x3,_) => #V((!PSR) : PSR) 656 | BitsN.B(0x4,_) => 657 (#C((!PSR) : PSR)) andalso (not(#Z((!PSR) : PSR))) 658 | BitsN.B(0x5,_) => (#N((!PSR) : PSR)) = (#V((!PSR) : PSR)) 659 | BitsN.B(0x6,_) => 660 ((#N((!PSR) : PSR)) = (#V((!PSR) : PSR))) andalso 661 (not(#Z((!PSR) : PSR))) 662 | BitsN.B(0x7,_) => true 663 | _ => raise General.Bind 664 in 665 if (BitsN.bit(cond,0)) andalso (not(cond = (BitsN.B(0xF,4)))) 666 then not result 667 else result 668 end; 669 670fun Raise e = pending := (Option.SOME e); 671 672fun CurrentModeIsPrivileged () = 673 ((!CurrentMode) = Mode_Handler) orelse 674 (not(#nPRIV((!CONTROL) : CONTROL))); 675 676fun LookUpSP () = 677 if #SPSEL((!CONTROL) : CONTROL) then RName_SP_process else RName_SP_main; 678 679fun R n = 680 if n = (BitsN.B(0xF,4)) 681 then BitsN.+ 682 (Map.lookup((!REG),Cast.RNameToNat RName_PC),BitsN.B(0x4,32)) 683 else if n = (BitsN.B(0xE,4)) 684 then Map.lookup((!REG),Cast.RNameToNat RName_LR) 685 else if n = (BitsN.B(0xD,4)) 686 then Map.lookup((!REG),Cast.RNameToNat(LookUpSP ())) 687 else Map.lookup 688 ((!REG),Cast.RNameToNat((Cast.natToRName o BitsN.toNat) n)); 689 690fun write'R (value,n) = 691 if n = (BitsN.B(0xF,4)) 692 then raise ASSERT "n >= 0 and n <= 14" 693 else if n = (BitsN.B(0xE,4)) 694 then REG := (Map.update((!REG),Cast.RNameToNat RName_LR,value)) 695 else if n = (BitsN.B(0xD,4)) 696 then let 697 val x = LookUpSP () 698 in 699 REG := 700 (Map.update 701 ((!REG),Cast.RNameToNat x, 702 BitsN.@@(BitsN.bits(31,2) value,BitsN.B(0x0,2)))) 703 end 704 else let 705 val x = (Cast.natToRName o BitsN.toNat) n 706 in 707 REG := (Map.update((!REG),Cast.RNameToNat x,value)) 708 end; 709 710fun SP_main () = Map.lookup((!REG),Cast.RNameToNat RName_SP_main); 711 712fun write'SP_main value = 713 REG := (Map.update((!REG),Cast.RNameToNat RName_SP_main,value)); 714 715fun SP_process () = Map.lookup((!REG),Cast.RNameToNat RName_SP_process); 716 717fun write'SP_process value = 718 REG := (Map.update((!REG),Cast.RNameToNat RName_SP_process,value)); 719 720fun SP () = R(BitsN.B(0xD,4)); 721 722fun write'SP value = write'R(value,BitsN.B(0xD,4)); 723 724fun LR () = R(BitsN.B(0xE,4)); 725 726fun write'LR value = write'R(value,BitsN.B(0xE,4)); 727 728fun PC () = R(BitsN.B(0xF,4)); 729 730fun write'PC value = 731 REG := (Map.update((!REG),Cast.RNameToNat RName_PC,value)); 732 733fun mem1 address = 734 BitsN.toBitstring(Map.lookup((!MEM),BitsN.toNat address)); 735 736fun mem (address,size) = 737 case size of 738 1 => Bitstring.bits(7,0) (mem1(BitsN.+(address,BitsN.B(0x0,32)))) 739 | 2 => 740 Bitstring.bits(15,0) 741 ((mem1(BitsN.+(address,BitsN.B(0x1,32)))) 742 @ 743 (mem1(BitsN.+(address,BitsN.B(0x0,32))))) 744 | 4 => 745 Bitstring.bits(31,0) 746 (List.concat 747 [mem1(BitsN.+(address,BitsN.B(0x3,32))), 748 mem1(BitsN.+(address,BitsN.B(0x2,32))), 749 mem1(BitsN.+(address,BitsN.B(0x1,32))), 750 mem1(BitsN.+(address,BitsN.B(0x0,32)))]) 751 | _ => raise ASSERT "mem: size in {1, 2, 4}"; 752 753fun write'mem (value,(address,size)) = 754 case size of 755 1 => 756 let 757 val x = BitsN.+(address,BitsN.B(0x0,32)) 758 in 759 MEM := 760 (Map.update 761 ((!MEM),BitsN.toNat x, 762 BitsN.fromBitstring(Bitstring.bits(7,0) value,8))) 763 end 764 | 2 => 765 ( let 766 val x = BitsN.+(address,BitsN.B(0x0,32)) 767 in 768 MEM := 769 (Map.update 770 ((!MEM),BitsN.toNat x, 771 BitsN.fromBitstring(Bitstring.bits(7,0) value,8))) 772 end 773 ; let 774 val x = BitsN.+(address,BitsN.B(0x1,32)) 775 in 776 MEM := 777 (Map.update 778 ((!MEM),BitsN.toNat x, 779 BitsN.fromBitstring(Bitstring.bits(15,8) value,8))) 780 end 781 ) 782 | 4 => 783 ( let 784 val x = BitsN.+(address,BitsN.B(0x0,32)) 785 in 786 MEM := 787 (Map.update 788 ((!MEM),BitsN.toNat x, 789 BitsN.fromBitstring(Bitstring.bits(7,0) value,8))) 790 end 791 ; let 792 val x = BitsN.+(address,BitsN.B(0x1,32)) 793 in 794 MEM := 795 (Map.update 796 ((!MEM),BitsN.toNat x, 797 BitsN.fromBitstring(Bitstring.bits(15,8) value,8))) 798 end 799 ; let 800 val x = BitsN.+(address,BitsN.B(0x2,32)) 801 in 802 MEM := 803 (Map.update 804 ((!MEM),BitsN.toNat x, 805 BitsN.fromBitstring(Bitstring.bits(23,16) value,8))) 806 end 807 ; let 808 val x = BitsN.+(address,BitsN.B(0x3,32)) 809 in 810 MEM := 811 (Map.update 812 ((!MEM),BitsN.toNat x, 813 BitsN.fromBitstring(Bitstring.bits(31,24) value,8))) 814 end 815 ) 816 | _ => raise ASSERT "mem: size in {1, 2, 4}"; 817 818fun BigEndianReverse (value,n) = 819 case n of 820 1 => Bitstring.bits(7,0) value 821 | 2 => (Bitstring.bits(7,0) value) @ (Bitstring.bits(15,8) value) 822 | 4 => 823 List.concat 824 [Bitstring.bits(7,0) value,Bitstring.bits(15,8) value, 825 Bitstring.bits(23,16) value,Bitstring.bits(31,24) value] 826 | _ => raise ASSERT "BigEndianReverse: n in {1, 2, 4}"; 827 828fun Align N (w,n) = BitsN.fromNat(Nat.*(n,Nat.div(BitsN.toNat w,n)),N); 829 830fun Aligned N (w,n) = w = (Align N (w,n)); 831 832fun MemA N (address,size) = 833 if not(Aligned 32 (address,size)) 834 then ( Raise HardFault; BitsN.fromNat(0,N) ) 835 else let 836 val value = mem(address,size) 837 in 838 BitsN.fromBitstring 839 (if #ENDIANNESS((!AIRCR) : AIRCR) 840 then BigEndianReverse(value,size) 841 else value,N) 842 end; 843 844fun write'MemA N (value,(address,size)) = 845 if not(Aligned 32 (address,size)) 846 then Raise HardFault 847 else let 848 val x = (address,size) 849 in 850 write'mem 851 (if #ENDIANNESS((!AIRCR) : AIRCR) 852 then BigEndianReverse(BitsN.toBitstring value,size) 853 else BitsN.toBitstring value,x) 854 end; 855 856fun MemU N (address,size) = MemA N (address,size); 857 858fun write'MemU N (value,(address,size)) = 859 let val x = (address,size) in write'MemA N (value,x) end; 860 861fun ExcNumber e = 862 case e of 863 Reset => BitsN.B(0x1,6) 864 | NMI => BitsN.B(0x2,6) 865 | HardFault => BitsN.B(0x3,6) 866 | SVCall => BitsN.B(0xB,6) 867 | PendSV => BitsN.B(0xE,6) 868 | SysTick => BitsN.B(0xF,6) 869 | ExternalInterrupt n => BitsN.+(BitsN.B(0x10,6),n); 870 871fun TakeReset () = 872 let 873 val vectortable = (!VTOR) 874 in 875 ( L3.for 876 (0,12, 877 fn i => 878 let 879 val x = BitsN.fromNat(i,4) 880 in 881 write'R(BitsN.B(0x0,32),x) 882 end) 883 ; write'SP_main(MemA 32 (vectortable,4)) 884 ; write'SP_process(BitsN.@@(BitsN.B(0x0,30),BitsN.B(0x0,2))) 885 ; write'LR(BitsN.B(0x0,32)) 886 ; write'PC(MemA 32 (BitsN.+(vectortable,BitsN.B(0x4,32)),4)) 887 ; CurrentMode := Mode_Thread 888 ; PSR := 889 {C = false, ExceptionNumber = BitsN.B(0x0,6), N = false, T = false, 890 V = false, Z = false, psr'rst = BitsN.B(0x0,21)} 891 ; PSR := (PSR_ExceptionNumber_rupd((!PSR),BitsN.B(0x0,6))) 892 ; PRIMASK := (PRIMASK_PM_rupd((!PRIMASK),false)) 893 ; CONTROL := (CONTROL_SPSEL_rupd((!CONTROL),false)) 894 ; CONTROL := (CONTROL_nPRIV_rupd((!CONTROL),false)) 895 ; L3.for 896 (0,63, 897 fn i => 898 let 899 val x = BitsN.fromNat(i,6) 900 in 901 ExceptionActive := 902 (Map.update((!ExceptionActive),BitsN.toNat x,false)) 903 end) 904 ) 905 end; 906 907fun ExceptionPriority n = 908 if n = 2 909 then IntInf.~ 2 910 else if n = 1 911 then IntInf.~ 1 912 else if n = 11 913 then BitsN.toInt(#PRI_11((!SHPR2) : SHPR2)) 914 else if n = 14 915 then BitsN.toInt(#PRI_14((!SHPR3) : SHPR3)) 916 else if n = 15 917 then BitsN.toInt(#PRI_15((!SHPR3) : SHPR3)) 918 else if Nat.>=(n,16) 919 then let 920 val r = 921 Map.lookup 922 ((!NVIC_IPR), 923 BitsN.toNat(BitsN.fromNat(Nat.div(Nat.-(n,16),4),3))) 924 in 925 case BitsN.fromNat(Nat.mod(n,4),2) of 926 BitsN.B(0x0,_) => BitsN.toInt(#PRI_N0(r : IPR)) 927 | BitsN.B(0x1,_) => BitsN.toInt(#PRI_N1(r : IPR)) 928 | BitsN.B(0x2,_) => BitsN.toInt(#PRI_N2(r : IPR)) 929 | BitsN.B(0x3,_) => BitsN.toInt(#PRI_N3(r : IPR)) 930 | _ => raise General.Bind 931 end 932 else 4; 933 934fun ExecutionPriority () = 935 let 936 val highestpri = ref 4 937 in 938 let 939 val boostedpri = ref 4 940 in 941 ( L3.for 942 (2,48, 943 fn i => 944 if Map.lookup 945 ((!ExceptionActive),BitsN.toNat(BitsN.fromNat(i,6))) 946 then let 947 val p = ExceptionPriority i 948 in 949 if IntInf.<(p,(!highestpri)) 950 then highestpri := p 951 else () 952 end 953 else ()) 954 ; if #PM((!PRIMASK) : PRIMASK) then boostedpri := 0 else () 955 ; IntInf.min((!boostedpri),(!highestpri)) 956 ) 957 end 958 end; 959 960fun ReturnAddress () = PC (); 961 962fun PushStack () = 963 let 964 val frameptralign = ref (BitsN.B(0x0,1)) 965 in 966 let 967 val frameptr = ref (BitsN.B(0x0,32)) 968 in 969 ( if (#SPSEL((!CONTROL) : CONTROL)) andalso 970 ((!CurrentMode) = Mode_Thread) 971 then ( frameptralign := (BitsN.bits(2,2) (SP_process ())) 972 ; write'SP_process 973 (BitsN.&& 974 (BitsN.-(SP_process (),BitsN.B(0x20,32)), 975 BitsN.~(BitsN.zeroExtend 32 (BitsN.B(0x4,3))))) 976 ; frameptr := (SP_process ()) 977 ) 978 else ( frameptralign := (BitsN.bits(2,2) (SP_main ())) 979 ; write'SP_process 980 (BitsN.&& 981 (BitsN.-(SP_main (),BitsN.B(0x20,32)), 982 BitsN.~(BitsN.zeroExtend 32 (BitsN.B(0x4,3))))) 983 ; frameptr := (SP_main ()) 984 ) 985 ; let 986 val x = ((!frameptr),4) 987 in 988 write'MemA 32 (R(BitsN.B(0x0,4)),x) 989 end 990 ; let 991 val x = (BitsN.+((!frameptr),BitsN.B(0x4,32)),4) 992 in 993 write'MemA 32 (R(BitsN.B(0x1,4)),x) 994 end 995 ; let 996 val x = (BitsN.+((!frameptr),BitsN.B(0x8,32)),4) 997 in 998 write'MemA 32 (R(BitsN.B(0x2,4)),x) 999 end 1000 ; let 1001 val x = (BitsN.+((!frameptr),BitsN.B(0xC,32)),4) 1002 in 1003 write'MemA 32 (R(BitsN.B(0x3,4)),x) 1004 end 1005 ; let 1006 val x = (BitsN.+((!frameptr),BitsN.B(0x10,32)),4) 1007 in 1008 write'MemA 32 (R(BitsN.B(0xC,4)),x) 1009 end 1010 ; let 1011 val x = (BitsN.+((!frameptr),BitsN.B(0x14,32)),4) 1012 in 1013 write'MemA 32 (LR (),x) 1014 end 1015 ; let 1016 val x = (BitsN.+((!frameptr),BitsN.B(0x14,32)),4) 1017 in 1018 write'MemA 32 (ReturnAddress (),x) 1019 end 1020 ; let 1021 val x = (BitsN.+((!frameptr),BitsN.B(0x1C,32)),4) 1022 in 1023 write'MemA 32 1024 (BitsN.concat 1025 [BitsN.bits(31,10) (reg'PSR (!PSR)),(!frameptralign), 1026 BitsN.bits(8,0) (reg'PSR (!PSR))],x) 1027 end 1028 ; if (!CurrentMode) = Mode_Handler 1029 then write'LR(BitsN.B(0xFFFFFFF1,32)) 1030 else if not(#SPSEL((!CONTROL) : CONTROL)) 1031 then write'LR(BitsN.B(0xFFFFFFF9,32)) 1032 else write'LR(BitsN.B(0xFFFFFFFD,32)) 1033 ) 1034 end 1035 end; 1036 1037fun ExceptionTaken ExceptionNumber = 1038 let 1039 val vectortable = (!VTOR) 1040 in 1041 ( L3.for 1042 (0,3, 1043 fn i => 1044 let 1045 val x = BitsN.fromNat(i,4) 1046 in 1047 write'R(BitsN.B(0x0,32),x) 1048 end) 1049 ; write'R(BitsN.B(0x0,32),BitsN.B(0xC,4)) 1050 ; write'PC 1051 (MemA 32 1052 (BitsN.+ 1053 (vectortable, 1054 BitsN.* 1055 (BitsN.B(0x4,32), 1056 BitsN.fromNat(BitsN.toNat ExceptionNumber,32))),4)) 1057 ; PSR := 1058 {C = false, ExceptionNumber = BitsN.B(0x0,6), N = false, T = false, 1059 V = false, Z = false, psr'rst = BitsN.B(0x0,21)} 1060 ; CurrentMode := Mode_Handler 1061 ; PSR := (PSR_ExceptionNumber_rupd((!PSR),ExceptionNumber)) 1062 ; CONTROL := (CONTROL_SPSEL_rupd((!CONTROL),false)) 1063 ; ExceptionActive := 1064 (Map.update((!ExceptionActive),BitsN.toNat ExceptionNumber,true)) 1065 ) 1066 end; 1067 1068fun ExceptionEntry () = 1069 case (!pending) of 1070 Option.SOME e => ( PushStack (); ExceptionTaken(ExcNumber e) ) 1071 | NONE => (); 1072 1073fun PopStack (frameptr,EXC_RETURN) = 1074 ( write'R(MemA 32 (frameptr,4),BitsN.B(0x0,4)) 1075 ; write'R(MemA 32 (BitsN.+(frameptr,BitsN.B(0x4,32)),4),BitsN.B(0x1,4)) 1076 ; write'R(MemA 32 (BitsN.+(frameptr,BitsN.B(0x8,32)),4),BitsN.B(0x2,4)) 1077 ; write'R(MemA 32 (BitsN.+(frameptr,BitsN.B(0xC,32)),4),BitsN.B(0x3,4)) 1078 ; write'R(MemA 32 (BitsN.+(frameptr,BitsN.B(0x10,32)),4),BitsN.B(0xC,4)) 1079 ; write'LR(MemA 32 (BitsN.+(frameptr,BitsN.B(0x14,32)),4)) 1080 ; write'PC(MemA 32 (BitsN.+(frameptr,BitsN.B(0x18,32)),4)) 1081 ; let 1082 val psr = MemA 32 (BitsN.+(frameptr,BitsN.B(0x1C,32)),4) 1083 val spmask = 1084 BitsN.zeroExtend 32 (BitsN.@@(BitsN.bits(9,9) psr,BitsN.B(0x0,2))) 1085 in 1086 ( case boolify'4(BitsN.bits(3,0) EXC_RETURN) of 1087 (_,(false,(false,true))) => 1088 write'SP_main 1089 (BitsN.||(BitsN.+(SP_main (),BitsN.B(0x20,32)),spmask)) 1090 | (true,(true,(false,true))) => 1091 write'SP_process 1092 (BitsN.||(BitsN.+(SP_process (),BitsN.B(0x20,32)),spmask)) 1093 | _ => () 1094 ; let 1095 val w = reg'PSR (!PSR) 1096 in 1097 PSR := 1098 (write'reg'PSR 1099 ((!PSR),BitsN.bitFieldInsert(31,27) (w,BitsN.bits(31,27) psr))) 1100 end 1101 ; let 1102 val w = reg'PSR (!PSR) 1103 in 1104 PSR := 1105 (write'reg'PSR 1106 ((!PSR), 1107 BitsN.bitFieldInsert(24,24) 1108 (w,BitsN.fromBit(BitsN.bit(psr,24))))) 1109 end 1110 ; let 1111 val w = reg'PSR (!PSR) 1112 in 1113 PSR := 1114 (write'reg'PSR 1115 ((!PSR),BitsN.bitFieldInsert(5,0) (w,BitsN.bits(5,0) psr))) 1116 end 1117 ) 1118 end 1119 ); 1120 1121fun DeActivate ReturningExceptionNumber = 1122 ExceptionActive := 1123 (Map.update 1124 ((!ExceptionActive),BitsN.toNat ReturningExceptionNumber,false)); 1125 1126fun IsOnes N w = w = (BitsN.neg(BitsN.BV(0x1,N))); 1127 1128fun ExceptionActiveBitCount () = 1129 let 1130 val count = ref 0 1131 in 1132 ( L3.for 1133 (0,63, 1134 fn i => 1135 if Map.lookup 1136 ((!ExceptionActive),BitsN.toNat(BitsN.fromNat(i,6))) 1137 then count := (Nat.+((!count),1)) 1138 else ()) 1139 ; (!count) 1140 ) 1141 end; 1142 1143fun ExceptionReturn EXC_RETURN = 1144 ( if not((!CurrentMode) = Mode_Handler) 1145 then raise ASSERT "CurrentMode == Mode_Handler" 1146 else () 1147 ; if not(IsOnes 24 (BitsN.bits(27,4) EXC_RETURN)) 1148 then raise UNPREDICTABLE "ExceptionReturn" 1149 else () 1150 ; let 1151 val ReturningExceptionNumber = #ExceptionNumber((!PSR) : PSR) 1152 val NestedActivation = ExceptionActiveBitCount () 1153 in 1154 if not(Map.lookup 1155 ((!ExceptionActive),BitsN.toNat ReturningExceptionNumber)) 1156 then raise UNPREDICTABLE "ExceptionReturn" 1157 else let 1158 val frameptr = ref (BitsN.B(0x0,32)) 1159 in 1160 ( case BitsN.bits(3,0) EXC_RETURN of 1161 BitsN.B(0x1,_) => 1162 if NestedActivation = 1 1163 then raise UNPREDICTABLE "ExceptionReturn" 1164 else ( frameptr := (SP_main ()) 1165 ; CurrentMode := Mode_Handler 1166 ; CONTROL := 1167 (CONTROL_SPSEL_rupd((!CONTROL),false)) 1168 ) 1169 | BitsN.B(0x9,_) => 1170 if not(NestedActivation = 1) 1171 then raise UNPREDICTABLE "ExceptionReturn" 1172 else ( frameptr := (SP_main ()) 1173 ; CurrentMode := Mode_Thread 1174 ; CONTROL := (CONTROL_SPSEL_rupd((!CONTROL),false)) 1175 ) 1176 | BitsN.B(0xD,_) => 1177 if not(NestedActivation = 1) 1178 then raise UNPREDICTABLE "ExceptionReturn" 1179 else ( frameptr := (SP_process ()) 1180 ; CurrentMode := Mode_Thread 1181 ; CONTROL := (CONTROL_SPSEL_rupd((!CONTROL),true)) 1182 ) 1183 | _ => raise UNPREDICTABLE "ExceptionReturn" 1184 ; DeActivate ReturningExceptionNumber 1185 ; PopStack((!frameptr),EXC_RETURN) 1186 ; if (!CurrentMode) = Mode_Handler 1187 then if (#ExceptionNumber((!PSR) : PSR)) = 1188 (BitsN.B(0x0,6)) 1189 then raise UNPREDICTABLE "ExceptionReturn" 1190 else () 1191 else if not((#ExceptionNumber((!PSR) : PSR)) = 1192 (BitsN.B(0x0,6))) 1193 then raise UNPREDICTABLE "ExceptionReturn" 1194 else () 1195 ) 1196 end 1197 end 1198 ); 1199 1200fun CallSupervisor () = Raise SVCall; 1201 1202fun BranchTo address = write'PC address; 1203 1204fun BranchWritePC address = 1205 BranchTo(BitsN.@@(BitsN.bits(31,1) address,BitsN.B(0x0,1))); 1206 1207fun BXWritePC address = 1208 if ((!CurrentMode) = Mode_Handler) andalso 1209 ((BitsN.bits(31,28) address) = (BitsN.B(0xF,4))) 1210 then ExceptionReturn(BitsN.bits(27,0) address) 1211 else ( if not(BitsN.bit(address,0)) then Raise HardFault else () 1212 ; BranchTo(BitsN.@@(BitsN.bits(31,1) address,BitsN.B(0x0,1))) 1213 ); 1214 1215fun BLXWritePC address = 1216 ( if not(BitsN.bit(address,0)) then Raise HardFault else () 1217 ; BranchTo(BitsN.@@(BitsN.bits(31,1) address,BitsN.B(0x0,1))) 1218 ); 1219 1220fun LoadWritePC address = BXWritePC address; 1221 1222fun ALUWritePC address = BranchWritePC address; 1223 1224fun IncPC () = 1225 BranchTo(BitsN.+(Map.lookup((!REG),Cast.RNameToNat RName_PC),(!pcinc))); 1226 1227fun HighestSetBit N w = 1228 if w = (BitsN.BV(0x0,N)) then IntInf.~ 1 else BitsN.toInt(BitsN.log2 w); 1229 1230fun CountLeadingZeroBits N w = 1231 Nat.fromInt 1232 (IntInf.- 1233 (IntInf.-(Nat.toInt(BitsN.size(BitsN.BV(0x0,N))),1), 1234 HighestSetBit N w)); 1235 1236fun LowestSetBit N w = CountLeadingZeroBits N (BitsN.reverse w); 1237 1238fun BitCount N w = 1239 let 1240 val result = ref 0 1241 in 1242 ( L3.for 1243 (0,Nat.-(BitsN.size(BitsN.BV(0x0,N)),1), 1244 fn i => 1245 if BitsN.bit(w,i) then result := (Nat.+((!result),1)) else ()) 1246 ; (!result) 1247 ) 1248 end; 1249 1250fun SignExtendFrom N (w,p) = 1251 let 1252 val s = Nat.-(BitsN.size(BitsN.BV(0x0,N)),p) 1253 in 1254 BitsN.>>(BitsN.<<(w,s),s) 1255 end; 1256 1257fun Extend (M,N) (unsigned,w) = 1258 if unsigned then BitsN.zeroExtend N w else BitsN.signExtend N w; 1259 1260fun UInt N w = Nat.toInt(BitsN.toNat w); 1261 1262fun LSL_C N (x,shift) = 1263 ( if shift = 0 then raise ASSERT "LSL_C" else () 1264 ; let 1265 val extended_x = 1266 (BitsN.toBitstring x) @ (Bitstring.replicate([false],shift)) 1267 in 1268 (BitsN.<<(x,shift), 1269 Bitstring.bit(extended_x,BitsN.size(BitsN.BV(0x0,N)))) 1270 end 1271 ); 1272 1273fun LSL N (x,shift) = if shift = 0 then x else L3.fst(LSL_C N (x,shift)); 1274 1275fun LSR_C N (x,shift) = 1276 ( if shift = 0 then raise ASSERT "LSR_C" else () 1277 ; (BitsN.>>+(x,shift), 1278 (Nat.<=(shift,BitsN.size(BitsN.BV(0x0,N)))) andalso 1279 (BitsN.bit(x,Nat.-(shift,1)))) 1280 ); 1281 1282fun LSR N (x,shift) = if shift = 0 then x else L3.fst(LSR_C N (x,shift)); 1283 1284fun ASR_C N (x,shift) = 1285 ( if shift = 0 then raise ASSERT "ASR_C" else () 1286 ; (BitsN.>>(x,shift), 1287 BitsN.bit(x,Nat.-(Nat.min(BitsN.size(BitsN.BV(0x0,N)),shift),1))) 1288 ); 1289 1290fun ASR N (x,shift) = if shift = 0 then x else L3.fst(ASR_C N (x,shift)); 1291 1292fun ROR_C N (x,shift) = 1293 ( if shift = 0 then raise ASSERT "ROR_C" else () 1294 ; let val result = BitsN.#>>(x,shift) in (result,BitsN.msb result) end 1295 ); 1296 1297fun ROR N (x,shift) = if shift = 0 then x else L3.fst(ROR_C N (x,shift)); 1298 1299fun RRX_C N (x,carry_in) = 1300 let 1301 val result = 1302 BitsN.fromBitstring 1303 ((Bitstring.fromBool carry_in) 1304 @ 1305 (Bitstring.bits(Nat.-(BitsN.size(BitsN.BV(0x0,N)),1),1) 1306 (BitsN.toBitstring x)),N) 1307 in 1308 (result,BitsN.bit(x,0)) 1309 end; 1310 1311fun RRX N (x,carry_in) = L3.fst(RRX_C N (x,carry_in)); 1312 1313fun DecodeImmShift (typ,imm5) = 1314 case typ of 1315 BitsN.B(0x0,_) => (SRType_LSL,BitsN.toNat imm5) 1316 | BitsN.B(0x1,_) => 1317 (SRType_LSR,if imm5 = (BitsN.B(0x0,5)) then 32 else BitsN.toNat imm5) 1318 | BitsN.B(0x2,_) => 1319 (SRType_ASR,if imm5 = (BitsN.B(0x0,5)) then 32 else BitsN.toNat imm5) 1320 | BitsN.B(0x3,_) => 1321 if imm5 = (BitsN.B(0x0,5)) 1322 then (SRType_RRX,1) 1323 else (SRType_ROR,BitsN.toNat imm5) 1324 | _ => raise General.Bind; 1325 1326fun DecodeRegShift typ = 1327 case typ of 1328 BitsN.B(0x0,_) => SRType_LSL 1329 | BitsN.B(0x1,_) => SRType_LSR 1330 | BitsN.B(0x2,_) => SRType_ASR 1331 | BitsN.B(0x3,_) => SRType_ROR 1332 | _ => raise General.Bind; 1333 1334fun Shift_C N (value,(typ,(amount,carry_in))) = 1335 if amount = 0 1336 then (value,carry_in) 1337 else case typ of 1338 SRType_LSL => LSL_C N (value,amount) 1339 | SRType_LSR => LSR_C N (value,amount) 1340 | SRType_ASR => ASR_C N (value,amount) 1341 | SRType_ROR => ROR_C N (value,amount) 1342 | SRType_RRX => RRX_C N (value,carry_in); 1343 1344fun Shift N (value,(typ,(amount,carry_in))) = 1345 L3.fst(Shift_C N (value,(typ,(amount,carry_in)))); 1346 1347fun AddWithCarry N (x,(y,carry_in)) = 1348 let 1349 val unsigned_sum = 1350 Nat.+(Nat.+(BitsN.toNat x,BitsN.toNat y),Nat.fromBool carry_in) 1351 val signed_sum = 1352 IntInf.+ 1353 (IntInf.+(BitsN.toInt x,BitsN.toInt y),IntExtra.fromBool carry_in) 1354 val result = BitsN.fromNat(unsigned_sum,N) 1355 val carry_out = not((BitsN.toNat result) = unsigned_sum) 1356 val overflow = not((BitsN.toInt result) = signed_sum) 1357 in 1358 (result,(carry_out,overflow)) 1359 end; 1360 1361fun DataProcessingALU (opc,(a,(b,c))) = 1362 case opc of 1363 BitsN.B(0x0,_) => (BitsN.&&(a,b),(c,false)) 1364 | BitsN.B(0x8,_) => (BitsN.&&(a,b),(c,false)) 1365 | BitsN.B(0x1,_) => (BitsN.??(a,b),(c,false)) 1366 | BitsN.B(0x9,_) => (BitsN.??(a,b),(c,false)) 1367 | BitsN.B(0x2,_) => AddWithCarry 32 (a,(BitsN.~ b,true)) 1368 | BitsN.B(0xA,_) => AddWithCarry 32 (a,(BitsN.~ b,true)) 1369 | BitsN.B(0x3,_) => AddWithCarry 32 (BitsN.~ a,(b,true)) 1370 | BitsN.B(0x4,_) => AddWithCarry 32 (a,(b,false)) 1371 | BitsN.B(0xB,_) => AddWithCarry 32 (a,(b,false)) 1372 | BitsN.B(0x5,_) => AddWithCarry 32 (a,(b,c)) 1373 | BitsN.B(0x6,_) => AddWithCarry 32 (a,(BitsN.~ b,c)) 1374 | BitsN.B(0x7,_) => AddWithCarry 32 (BitsN.~ a,(b,c)) 1375 | BitsN.B(0xC,_) => (BitsN.||(a,b),(c,false)) 1376 | BitsN.B(0xD,_) => (b,(c,false)) 1377 | BitsN.B(0xE,_) => (BitsN.&&(a,BitsN.~ b),(c,false)) 1378 | BitsN.B(0xF,_) => (BitsN.~ b,(c,false)) 1379 | _ => raise General.Bind; 1380 1381fun ArithmeticOpcode opc = 1382 ((BitsN.bit(opc,2)) orelse (BitsN.bit(opc,1))) andalso 1383 (not((BitsN.bit(opc,3)) andalso (BitsN.bit(opc,2)))); 1384 1385fun dfn'BranchTarget imm32 = 1386 ( BranchWritePC(BitsN.+(PC (),imm32)); count := (Nat.+((!count),3)) ); 1387 1388fun dfn'BranchExchange m = 1389 ( BXWritePC(R m); count := (Nat.+((!count),3)) ); 1390 1391fun dfn'BranchLinkImmediate imm32 = 1392 let 1393 val next_instr_addr = PC () 1394 in 1395 ( write'LR(BitsN.@@(BitsN.bits(31,1) next_instr_addr,BitsN.B(0x1,1))) 1396 ; BranchWritePC(BitsN.+(PC (),imm32)) 1397 ; count := (Nat.+((!count),4)) 1398 ) 1399 end; 1400 1401fun dfn'BranchLinkExchangeRegister m = 1402 let 1403 val target = R m 1404 val next_instr_addr = BitsN.-(PC (),BitsN.B(0x2,32)) 1405 in 1406 ( write'LR(BitsN.@@(BitsN.bits(31,1) next_instr_addr,BitsN.B(0x1,1))) 1407 ; BLXWritePC target 1408 ; count := (Nat.+((!count),3)) 1409 ) 1410 end; 1411 1412fun DataProcessing (opc,(setflags,(d,(n,(imm32,C))))) = 1413 let 1414 val rn = 1415 if (opc = (BitsN.B(0xD,4))) orelse (opc = (BitsN.B(0xF,4))) 1416 then BitsN.B(0x0,32) 1417 else if (Set.mem(opc,[BitsN.B(0x4,4),BitsN.B(0x2,4)])) andalso 1418 ((n = (BitsN.B(0xF,4))) andalso (not setflags)) 1419 then Align 32 (PC (),4) 1420 else R n 1421 val (result,(carry,overflow)) = DataProcessingALU(opc,(rn,(imm32,C))) 1422 in 1423 ( if not((BitsN.bits(3,2) opc) = (BitsN.B(0x2,2))) 1424 then write'R(result,d) 1425 else () 1426 ; if setflags 1427 then ( PSR := (PSR_N_rupd((!PSR),BitsN.bit(result,31))) 1428 ; PSR := (PSR_Z_rupd((!PSR),result = (BitsN.B(0x0,32)))) 1429 ; PSR := (PSR_C_rupd((!PSR),carry)) 1430 ; if ArithmeticOpcode opc 1431 then PSR := (PSR_V_rupd((!PSR),overflow)) 1432 else () 1433 ) 1434 else () 1435 ; IncPC () 1436 ; count := (Nat.+((!count),1)) 1437 ) 1438 end; 1439 1440fun DataProcessingPC (opc,(n,(imm32,C))) = 1441 let 1442 val rn = 1443 if opc = (BitsN.B(0xD,4)) 1444 then BitsN.B(0x0,32) 1445 else if n = (BitsN.B(0xF,4)) then PC () else R n 1446 val (result,_) = DataProcessingALU(opc,(rn,(imm32,C))) 1447 in 1448 ( ALUWritePC result; count := (Nat.+((!count),3)) ) 1449 end; 1450 1451fun dfn'Move (d,imm32) = 1452 DataProcessing 1453 (BitsN.B(0xD,4),(true,(d,(BitsN.B(0xF,4),(imm32,#C((!PSR) : PSR)))))); 1454 1455fun dfn'CompareImmediate (n,imm32) = 1456 DataProcessing 1457 (BitsN.B(0xA,4),(true,(BitsN.B(0x0,4),(n,(imm32,#C((!PSR) : PSR)))))); 1458 1459fun dfn'ArithLogicImmediate (opc,(setflags,(d,(n,imm32)))) = 1460 DataProcessing(opc,(setflags,(d,(n,(imm32,#C((!PSR) : PSR)))))); 1461 1462fun doRegister (opc,(setflags,(d,(n,(m,(shift_t,shift_n)))))) = 1463 let 1464 val (shifted,carry) = 1465 Shift_C 32 (R m,(shift_t,(shift_n,#C((!PSR) : PSR)))) 1466 val carry = if ArithmeticOpcode opc then #C((!PSR) : PSR) else carry 1467 in 1468 if d = (BitsN.B(0xF,4)) 1469 then DataProcessingPC(opc,(n,(shifted,carry))) 1470 else DataProcessing(opc,(setflags,(d,(n,(shifted,carry))))) 1471 end; 1472 1473fun dfn'Register (opc,(setflags,(d,(n,m)))) = 1474 doRegister(opc,(setflags,(d,(n,(m,(SRType_LSL,0)))))); 1475 1476fun dfn'TestCompareRegister (opc,(n,m)) = 1477 doRegister 1478 (BitsN.@@(BitsN.B(0x2,2),opc), 1479 (true,(BitsN.B(0x0,4),(n,(m,(SRType_LSL,0)))))); 1480 1481fun dfn'ShiftImmediate (negate,(setflags,(d,(m,(shift_t,shift_n))))) = 1482 if negate 1483 then doRegister 1484 (BitsN.B(0xF,4), 1485 (setflags,(d,(BitsN.B(0xF,4),(m,(shift_t,shift_n)))))) 1486 else doRegister 1487 (BitsN.B(0xD,4), 1488 (setflags,(d,(BitsN.B(0x0,4),(m,(shift_t,shift_n)))))); 1489 1490fun dfn'ShiftRegister (d,(n,(shift_t,m))) = 1491 let 1492 val shift_n = BitsN.toNat(BitsN.bits(7,0) (R m)) 1493 val (shifted,carry) = 1494 Shift_C 32 (R n,(shift_t,(shift_n,#C((!PSR) : PSR)))) 1495 in 1496 DataProcessing 1497 (BitsN.B(0xD,4),(true,(d,(BitsN.B(0x0,4),(shifted,carry))))) 1498 end; 1499 1500fun dfn'Multiply32 (d,(n,m)) = 1501 let 1502 val result = BitsN.*(R n,R m) 1503 in 1504 ( write'R(result,d) 1505 ; PSR := (PSR_N_rupd((!PSR),BitsN.bit(result,31))) 1506 ; PSR := (PSR_Z_rupd((!PSR),result = (BitsN.B(0x0,32)))) 1507 ; IncPC () 1508 ; count := (Nat.+((!count),1)) 1509 ) 1510 end; 1511 1512fun dfn'ExtendByte (unsigned,(d,m)) = 1513 ( write'R(Extend (8,32) (unsigned,BitsN.bits(7,0) (R m)),d) 1514 ; IncPC () 1515 ; count := (Nat.+((!count),1)) 1516 ); 1517 1518fun dfn'ExtendHalfword (unsigned,(d,m)) = 1519 ( write'R(Extend (16,32) (unsigned,BitsN.bits(15,0) (R m)),d) 1520 ; IncPC () 1521 ; count := (Nat.+((!count),1)) 1522 ); 1523 1524fun dfn'ByteReverse (d,m) = 1525 let 1526 val Rm = R m 1527 in 1528 ( write'R 1529 (BitsN.concat 1530 [BitsN.bits(7,0) Rm,BitsN.bits(15,8) Rm,BitsN.bits(23,16) Rm, 1531 BitsN.bits(31,24) Rm],d) 1532 ; IncPC () 1533 ; count := (Nat.+((!count),1)) 1534 ) 1535 end; 1536 1537fun dfn'ByteReversePackedHalfword (d,m) = 1538 let 1539 val Rm = R m 1540 in 1541 ( write'R 1542 (BitsN.concat 1543 [BitsN.bits(23,16) Rm,BitsN.bits(31,24) Rm,BitsN.bits(7,0) Rm, 1544 BitsN.bits(15,8) Rm],d) 1545 ; IncPC () 1546 ; count := (Nat.+((!count),1)) 1547 ) 1548 end; 1549 1550fun dfn'ByteReverseSignedHalfword (d,m) = 1551 let 1552 val Rm = R m 1553 in 1554 ( write'R 1555 (BitsN.@@ 1556 (BitsN.signExtend 24 (BitsN.bits(7,0) Rm),BitsN.bits(15,8) Rm), 1557 d) 1558 ; IncPC () 1559 ; count := (Nat.+((!count),1)) 1560 ) 1561 end; 1562 1563fun dfn'LoadWord (t,(n,m)) = 1564 let 1565 val offset = 1566 case m of 1567 register_form m => 1568 Shift 32 (R m,(SRType_LSL,(0,#C((!PSR) : PSR)))) 1569 | immediate_form imm32 => imm32 1570 val address = BitsN.+(R n,offset) 1571 val data = MemU 32 (address,4) 1572 in 1573 ( write'R(data,t); IncPC (); count := (Nat.+((!count),2)) ) 1574 end; 1575 1576fun dfn'LoadLiteral (t,imm32) = 1577 let 1578 val base = Align 32 (PC (),4) 1579 val address = BitsN.+(base,imm32) 1580 in 1581 ( write'R(MemU 32 (address,4),t) 1582 ; IncPC () 1583 ; count := (Nat.+((!count),2)) 1584 ) 1585 end; 1586 1587fun dfn'LoadByte (unsigned,(t,(n,m))) = 1588 let 1589 val offset = 1590 case m of 1591 register_form m => 1592 Shift 32 (R m,(SRType_LSL,(0,#C((!PSR) : PSR)))) 1593 | immediate_form imm32 => imm32 1594 val address = BitsN.+(R n,offset) 1595 val data = MemU 8 (address,1) 1596 in 1597 ( write'R(Extend (8,32) (unsigned,data),t) 1598 ; IncPC () 1599 ; count := (Nat.+((!count),2)) 1600 ) 1601 end; 1602 1603fun dfn'LoadHalf (unsigned,(t,(n,m))) = 1604 let 1605 val offset = 1606 case m of 1607 register_form m => 1608 Shift 32 (R m,(SRType_LSL,(0,#C((!PSR) : PSR)))) 1609 | immediate_form imm32 => imm32 1610 val address = BitsN.+(R n,offset) 1611 val data = MemU 16 (address,2) 1612 in 1613 ( write'R(Extend (16,32) (unsigned,data),t) 1614 ; IncPC () 1615 ; count := (Nat.+((!count),2)) 1616 ) 1617 end; 1618 1619fun dfn'LoadMultiple (wback,(n,registers)) = 1620 let 1621 val Rn = R n 1622 val bitcount = BitCount 9 registers 1623 in 1624 let 1625 val address = ref Rn 1626 in 1627 ( L3.for 1628 (0,7, 1629 fn i => 1630 if BitsN.bit(registers,i) 1631 then ( let 1632 val x = BitsN.fromNat(i,4) 1633 in 1634 write'R(MemA 32 ((!address),4),x) 1635 end 1636 ; address := (BitsN.+((!address),BitsN.B(0x4,32))) 1637 ) 1638 else ()) 1639 ; if BitsN.bit(registers,8) 1640 then ( LoadWritePC(MemA 32 ((!address),4)) 1641 ; count := (Nat.+(Nat.+((!count),bitcount),4)) 1642 ) 1643 else ( IncPC (); count := (Nat.+(Nat.+((!count),bitcount),1)) ) 1644 ; if wback andalso (not(BitsN.bit(registers,BitsN.toNat n))) 1645 then write'R 1646 (BitsN.+ 1647 (Rn, 1648 BitsN.*(BitsN.B(0x4,32),BitsN.fromNat(bitcount,32))), 1649 n) 1650 else () 1651 ) 1652 end 1653 end; 1654 1655fun dfn'StoreWord (t,(n,m)) = 1656 let 1657 val offset = 1658 case m of 1659 register_form m => 1660 Shift 32 (R m,(SRType_LSL,(0,#C((!PSR) : PSR)))) 1661 | immediate_form imm32 => imm32 1662 val address = BitsN.+(R n,offset) 1663 in 1664 ( let val x = (address,4) in write'MemU 32 (R t,x) end 1665 ; IncPC () 1666 ; count := (Nat.+((!count),2)) 1667 ) 1668 end; 1669 1670fun dfn'StoreByte (t,(n,m)) = 1671 let 1672 val offset = 1673 case m of 1674 register_form m => 1675 Shift 32 (R m,(SRType_LSL,(0,#C((!PSR) : PSR)))) 1676 | immediate_form imm32 => imm32 1677 val address = BitsN.+(R n,offset) 1678 in 1679 ( let 1680 val x = (address,1) 1681 in 1682 write'MemU 8 (BitsN.bits(7,0) (R t),x) 1683 end 1684 ; IncPC () 1685 ; count := (Nat.+((!count),2)) 1686 ) 1687 end; 1688 1689fun dfn'StoreHalf (t,(n,m)) = 1690 let 1691 val offset = 1692 case m of 1693 register_form m => 1694 Shift 32 (R m,(SRType_LSL,(0,#C((!PSR) : PSR)))) 1695 | immediate_form imm32 => imm32 1696 val address = BitsN.+(R n,offset) 1697 in 1698 ( let 1699 val x = (address,2) 1700 in 1701 write'MemU 16 (BitsN.bits(15,0) (R t),x) 1702 end 1703 ; IncPC () 1704 ; count := (Nat.+((!count),2)) 1705 ) 1706 end; 1707 1708fun dfn'StoreMultiple (n,registers) = 1709 let 1710 val Rn = R n 1711 val bitcount = BitCount 8 registers 1712 val lowest = LowestSetBit 8 registers 1713 in 1714 let 1715 val address = ref Rn 1716 in 1717 ( L3.for 1718 (0,7, 1719 fn i => 1720 if BitsN.bit(registers,i) 1721 then ( if ((BitsN.fromNat(i,4)) = n) andalso 1722 (not(i = lowest)) 1723 then let 1724 val x = ((!address),4) 1725 in 1726 write'MemA 32 (BitsN.B(0x0,32),x) 1727 end 1728 else let 1729 val x = ((!address),4) 1730 in 1731 write'MemA 32 (R(BitsN.fromNat(i,4)),x) 1732 end 1733 ; address := (BitsN.+((!address),BitsN.B(0x4,32))) 1734 ) 1735 else ()) 1736 ; write'R 1737 (BitsN.+(Rn,BitsN.*(BitsN.B(0x4,32),BitsN.fromNat(bitcount,32))), 1738 n) 1739 ; IncPC () 1740 ; count := (Nat.+(Nat.+((!count),bitcount),1)) 1741 ) 1742 end 1743 end; 1744 1745fun dfn'Push registers = 1746 let 1747 val sp = SP () 1748 val bitcount = BitCount 9 registers 1749 val length = BitsN.*(BitsN.B(0x4,32),BitsN.fromNat(bitcount,32)) 1750 in 1751 let 1752 val address = ref (BitsN.-(sp,length)) 1753 in 1754 ( L3.for 1755 (0,8, 1756 fn i => 1757 if BitsN.bit(registers,i) 1758 then ( let 1759 val x = ((!address),4) 1760 in 1761 write'MemA 32 1762 (if i = 8 then LR () else R(BitsN.fromNat(i,4)), 1763 x) 1764 end 1765 ; address := (BitsN.+((!address),BitsN.B(0x4,32))) 1766 ) 1767 else ()) 1768 ; write'SP(BitsN.-(sp,length)) 1769 ; IncPC () 1770 ; count := (Nat.+(Nat.+((!count),bitcount),1)) 1771 ) 1772 end 1773 end; 1774 1775fun dfn'SupervisorCall imm32 = 1776 ( CallSupervisor (); count := (Nat.+((!count),0)) ); 1777 1778fun dfn'ChangeProcessorState im = 1779 ( if CurrentModeIsPrivileged () 1780 then PRIMASK := (PRIMASK_PM_rupd((!PRIMASK),im)) 1781 else () 1782 ; IncPC () 1783 ; count := (Nat.+((!count),1)) 1784 ); 1785 1786fun dfn'MoveToRegisterFromSpecial (SYSm,d) = 1787 ( write'R(BitsN.B(0x0,32),d) 1788 ; case BitsN.bits(7,3) SYSm of 1789 BitsN.B(0x0,_) => 1790 ( if BitsN.bit(SYSm,0) 1791 then let 1792 val w = R d 1793 in 1794 write'R 1795 (BitsN.bitFieldInsert(8,0) 1796 (w,BitsN.bits(8,0) (reg'PSR (!PSR))),d) 1797 end 1798 else () 1799 ; if BitsN.bit(SYSm,1) 1800 then let 1801 val w = R d 1802 in 1803 write'R 1804 (BitsN.bitFieldInsert(24,24) (w,BitsN.fromBit false), 1805 d) 1806 end 1807 else () 1808 ; if not(BitsN.bit(SYSm,2)) 1809 then let 1810 val w = R d 1811 in 1812 write'R 1813 (BitsN.bitFieldInsert(31,27) 1814 (w,BitsN.bits(31,27) (reg'PSR (!PSR))),d) 1815 end 1816 else () 1817 ) 1818 | BitsN.B(0x1,_) => 1819 (case BitsN.bits(2,0) SYSm of 1820 BitsN.B(0x0,_) => write'R(SP_main (),d) 1821 | BitsN.B(0x1,_) => write'R(SP_process (),d) 1822 | _ => ()) 1823 | BitsN.B(0x2,_) => 1824 (case BitsN.bits(2,0) SYSm of 1825 BitsN.B(0x0,_) => 1826 let 1827 val w = R d 1828 in 1829 write'R 1830 (BitsN.bitFieldInsert(0,0) 1831 (w,BitsN.fromBit(#PM((!PRIMASK) : PRIMASK))),d) 1832 end 1833 | BitsN.B(0x4,_) => 1834 let 1835 val w = R d 1836 in 1837 write'R 1838 (BitsN.bitFieldInsert(1,0) 1839 (w,BitsN.bits(1,0) (reg'CONTROL (!CONTROL))),d) 1840 end 1841 | _ => ()) 1842 | _ => () 1843 ; IncPC () 1844 ; count := (Nat.+((!count),4)) 1845 ); 1846 1847fun dfn'MoveToSpecialRegister (SYSm,n) = 1848 let 1849 val Rn = R n 1850 in 1851 ( case BitsN.bits(7,3) SYSm of 1852 BitsN.B(0x0,_) => 1853 if not(BitsN.bit(SYSm,2)) 1854 then let 1855 val w = reg'PSR (!PSR) 1856 in 1857 PSR := 1858 (write'reg'PSR 1859 ((!PSR), 1860 BitsN.bitFieldInsert(31,27) 1861 (w,BitsN.bits(31,27) Rn))) 1862 end 1863 else () 1864 | BitsN.B(0x1,_) => 1865 if CurrentModeIsPrivileged () 1866 then case BitsN.bits(2,0) SYSm of 1867 BitsN.B(0x0,_) => 1868 write'SP_main 1869 (BitsN.@@(BitsN.bits(31,2) Rn,BitsN.B(0x0,2))) 1870 | BitsN.B(0x1,_) => 1871 write'SP_process 1872 (BitsN.@@(BitsN.bits(31,2) Rn,BitsN.B(0x0,2))) 1873 | _ => () 1874 else () 1875 | BitsN.B(0x2,_) => 1876 if CurrentModeIsPrivileged () 1877 then case BitsN.bits(2,0) SYSm of 1878 BitsN.B(0x0,_) => 1879 PRIMASK := 1880 (PRIMASK_PM_rupd((!PRIMASK),BitsN.bit(Rn,0))) 1881 | BitsN.B(0x4,_) => 1882 if (!CurrentMode) = Mode_Thread 1883 then ( CONTROL := 1884 (CONTROL_SPSEL_rupd 1885 ((!CONTROL),BitsN.bit(Rn,1))) 1886 ; CONTROL := 1887 (CONTROL_nPRIV_rupd 1888 ((!CONTROL),BitsN.bit(Rn,0))) 1889 ) 1890 else () 1891 | _ => () 1892 else () 1893 | _ => () 1894 ; IncPC () 1895 ; count := (Nat.+((!count),4)) 1896 ) 1897 end; 1898 1899fun dfn'Undefined imm32 = Raise HardFault; 1900 1901fun dfn'NoOperation () = ( IncPC (); count := (Nat.+((!count),1)) ); 1902 1903fun dfn'Breakpoint imm32 = ( IncPC (); count := (Nat.+((!count),0)) ); 1904 1905fun dfn'DataMemoryBarrier option = 1906 ( IncPC (); count := (Nat.+((!count),4)) ); 1907 1908fun dfn'DataSynchronizationBarrier option = 1909 ( IncPC (); count := (Nat.+((!count),4)) ); 1910 1911fun dfn'InstructionSynchronizationBarrier option = 1912 ( IncPC (); count := (Nat.+((!count),4)) ); 1913 1914fun dfn'SendEvent () = ( IncPC (); count := (Nat.+((!count),1)) ); 1915 1916fun dfn'WaitForEvent () = ( IncPC (); count := (Nat.+((!count),2)) ); 1917 1918fun dfn'WaitForInterrupt () = ( IncPC (); count := (Nat.+((!count),2)) ); 1919 1920fun dfn'Yield () = ( IncPC (); count := (Nat.+((!count),1)) ); 1921 1922fun Run v0 = 1923 case v0 of 1924 NoOperation () => dfn'NoOperation () 1925 | Undefined v49 => dfn'Undefined v49 1926 | Branch v1 => 1927 (case v1 of 1928 BranchExchange v2 => dfn'BranchExchange v2 1929 | BranchLinkExchangeRegister v3 => 1930 dfn'BranchLinkExchangeRegister v3 1931 | BranchLinkImmediate v4 => dfn'BranchLinkImmediate v4 1932 | BranchTarget v5 => dfn'BranchTarget v5) 1933 | Data v6 => 1934 (case v6 of 1935 ArithLogicImmediate v7 => dfn'ArithLogicImmediate v7 1936 | CompareImmediate v8 => dfn'CompareImmediate v8 1937 | Move v9 => dfn'Move v9 1938 | Register v10 => dfn'Register v10 1939 | ShiftImmediate v11 => dfn'ShiftImmediate v11 1940 | ShiftRegister v12 => dfn'ShiftRegister v12 1941 | TestCompareRegister v13 => dfn'TestCompareRegister v13) 1942 | Hint v14 => 1943 (case v14 of 1944 Breakpoint v15 => dfn'Breakpoint v15 1945 | DataMemoryBarrier v16 => dfn'DataMemoryBarrier v16 1946 | DataSynchronizationBarrier v17 => 1947 dfn'DataSynchronizationBarrier v17 1948 | InstructionSynchronizationBarrier v18 => 1949 dfn'InstructionSynchronizationBarrier v18 1950 | SendEvent () => dfn'SendEvent () 1951 | WaitForEvent () => dfn'WaitForEvent () 1952 | WaitForInterrupt () => dfn'WaitForInterrupt () 1953 | Yield () => dfn'Yield ()) 1954 | Load v23 => 1955 (case v23 of 1956 LoadByte v24 => dfn'LoadByte v24 1957 | LoadHalf v25 => dfn'LoadHalf v25 1958 | LoadLiteral v26 => dfn'LoadLiteral v26 1959 | LoadMultiple v27 => dfn'LoadMultiple v27 1960 | LoadWord v28 => dfn'LoadWord v28) 1961 | Media v29 => 1962 (case v29 of 1963 ByteReverse v30 => dfn'ByteReverse v30 1964 | ByteReversePackedHalfword v31 => 1965 dfn'ByteReversePackedHalfword v31 1966 | ByteReverseSignedHalfword v32 => 1967 dfn'ByteReverseSignedHalfword v32 1968 | ExtendByte v33 => dfn'ExtendByte v33 1969 | ExtendHalfword v34 => dfn'ExtendHalfword v34) 1970 | Multiply v35 => (case v35 of Multiply32 v36 => dfn'Multiply32 v36) 1971 | Store v37 => 1972 (case v37 of 1973 Push v38 => dfn'Push v38 1974 | StoreByte v39 => dfn'StoreByte v39 1975 | StoreHalf v40 => dfn'StoreHalf v40 1976 | StoreMultiple v41 => dfn'StoreMultiple v41 1977 | StoreWord v42 => dfn'StoreWord v42) 1978 | System v43 => 1979 (case v43 of 1980 ChangeProcessorState v44 => dfn'ChangeProcessorState v44 1981 | MoveToRegisterFromSpecial v45 => 1982 dfn'MoveToRegisterFromSpecial v45 1983 | MoveToSpecialRegister v46 => dfn'MoveToSpecialRegister v46 1984 | SupervisorCall v47 => dfn'SupervisorCall v47); 1985 1986fun Fetch () = 1987 let 1988 val fpc = Map.lookup((!REG),Cast.RNameToNat RName_PC) 1989 val ireg = MemA 16 (fpc,2) 1990 in 1991 if ((BitsN.bits(15,13) ireg) = (BitsN.B(0x7,3))) andalso 1992 (not((BitsN.bits(12,11) ireg) = (BitsN.B(0x0,2)))) 1993 then Thumb2(ireg,MemA 16 (BitsN.+(fpc,BitsN.B(0x2,32)),2)) 1994 else Thumb ireg 1995 end; 1996 1997fun DECODE_UNPREDICTABLE (mc,s) = 1998 raise UNPREDICTABLE 1999 (String.concat 2000 ["Decode ", 2001 case mc of 2002 Thumb opc => 2003 (Bitstring.toBinString(BitsN.toBitstring opc)) ^ "; Thumb; " 2004 | Thumb2(opc1,opc2) => 2005 String.concat 2006 [Bitstring.toBinString(BitsN.toBitstring opc1),", ", 2007 Bitstring.toBinString(BitsN.toBitstring opc2),"; Thumb2; "], 2008 s]); 2009 2010fun DecodeThumb h = 2011 let 2012 val mc = Thumb h 2013 in 2014 case boolify'16 h of 2015 (false, 2016 (false, 2017 (false, 2018 (true, 2019 (true, 2020 (false, 2021 (S'0, 2022 (Rm'2,(Rm'1,(Rm'0,(Rn'2,(Rn'1,(Rn'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) => 2023 let 2024 val d = 2025 BitsN.fromNat 2026 (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4) 2027 val n = 2028 BitsN.fromNat 2029 (BitsN.toNat(BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)),4) 2030 val m = 2031 BitsN.fromNat 2032 (BitsN.toNat(BitsN.fromBitstring([Rm'2,Rm'1,Rm'0],3)),4) 2033 val setflags = true 2034 val opc = 2035 if (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x1,1)) 2036 then BitsN.B(0x2,4) 2037 else BitsN.B(0x4,4) 2038 in 2039 Data(Register(opc,(setflags,(d,(n,m))))) 2040 end 2041 | (false, 2042 (false, 2043 (false, 2044 (true, 2045 (true, 2046 (true, 2047 (S'0, 2048 (imm3'2, 2049 (imm3'1,(imm3'0,(Rn'2,(Rn'1,(Rn'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) => 2050 let 2051 val d = 2052 BitsN.fromNat 2053 (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4) 2054 val n = 2055 BitsN.fromNat 2056 (BitsN.toNat(BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)),4) 2057 val setflags = true 2058 val imm32 = 2059 BitsN.zeroExtend 32 2060 (BitsN.fromBitstring([imm3'2,imm3'1,imm3'0],3)) 2061 val opc = 2062 if (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x1,1)) 2063 then BitsN.B(0x2,4) 2064 else BitsN.B(0x4,4) 2065 in 2066 Data(ArithLogicImmediate(opc,(setflags,(d,(n,imm32))))) 2067 end 2068 | (false, 2069 (false, 2070 (false, 2071 (opc'1, 2072 (opc'0, 2073 (imm5'4, 2074 (imm5'3, 2075 (imm5'2, 2076 (imm5'1,(imm5'0,(Rm'2,(Rm'1,(Rm'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) => 2077 let 2078 val d = 2079 BitsN.fromNat 2080 (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4) 2081 val m = 2082 BitsN.fromNat 2083 (BitsN.toNat(BitsN.fromBitstring([Rm'2,Rm'1,Rm'0],3)),4) 2084 val setflags = true 2085 val (shift_t,shift_n) = 2086 DecodeImmShift 2087 (BitsN.fromBitstring([opc'1,opc'0],2), 2088 BitsN.fromBitstring([imm5'4,imm5'3,imm5'2,imm5'1,imm5'0],5)) 2089 in 2090 Data(ShiftImmediate(false,(setflags,(d,(m,(shift_t,shift_n)))))) 2091 end 2092 | (false, 2093 (false, 2094 (true, 2095 (false, 2096 (false, 2097 (Rd'2, 2098 (Rd'1, 2099 (Rd'0, 2100 (imm8'7, 2101 (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) => 2102 let 2103 val d = 2104 BitsN.fromNat 2105 (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4) 2106 val imm32 = 2107 BitsN.zeroExtend 32 2108 (BitsN.fromBitstring 2109 ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,imm8'0], 2110 8)) 2111 in 2112 Data(Move(d,imm32)) 2113 end 2114 | (false, 2115 (false, 2116 (true, 2117 (false, 2118 (true, 2119 (Rn'2, 2120 (Rn'1, 2121 (Rn'0, 2122 (imm8'7, 2123 (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) => 2124 let 2125 val n = 2126 BitsN.fromNat 2127 (BitsN.toNat(BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)),4) 2128 val imm32 = 2129 BitsN.zeroExtend 32 2130 (BitsN.fromBitstring 2131 ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,imm8'0], 2132 8)) 2133 in 2134 Data(CompareImmediate(n,imm32)) 2135 end 2136 | (false, 2137 (false, 2138 (true, 2139 (true, 2140 (S'0, 2141 (Rdn'2, 2142 (Rdn'1, 2143 (Rdn'0, 2144 (imm8'7, 2145 (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) => 2146 let 2147 val d = 2148 BitsN.fromNat 2149 (BitsN.toNat(BitsN.fromBitstring([Rdn'2,Rdn'1,Rdn'0],3)),4) 2150 val n = d 2151 val setflags = true 2152 val imm32 = 2153 BitsN.zeroExtend 32 2154 (BitsN.fromBitstring 2155 ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,imm8'0], 2156 8)) 2157 val opc = 2158 if (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x1,1)) 2159 then BitsN.B(0x2,4) 2160 else BitsN.B(0x4,4) 2161 in 2162 Data(ArithLogicImmediate(opc,(setflags,(d,(n,imm32))))) 2163 end 2164 | (false, 2165 (true, 2166 (false, 2167 (false, 2168 (false, 2169 (false, 2170 (opc'3, 2171 (opc'2,(opc'1,(opc'0,(Rx'2,(Rx'1,(Rx'0,(Ry'2,(Ry'1,Ry'0))))))))))))))) => 2172 let 2173 val Ry = BitsN.fromBitstring([Ry'2,Ry'1,Ry'0],3) 2174 val Rx = BitsN.fromBitstring([Rx'2,Rx'1,Rx'0],3) 2175 val opc = BitsN.fromBitstring([opc'3,opc'2,opc'1,opc'0],4) 2176 in 2177 case opc of 2178 BitsN.B(0x0,_) => 2179 let 2180 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2181 val n = d 2182 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2183 val setflags = true 2184 in 2185 Data(Register(opc,(setflags,(d,(n,m))))) 2186 end 2187 | BitsN.B(0x1,_) => 2188 let 2189 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2190 val n = d 2191 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2192 val setflags = true 2193 in 2194 Data(Register(opc,(setflags,(d,(n,m))))) 2195 end 2196 | BitsN.B(0x5,_) => 2197 let 2198 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2199 val n = d 2200 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2201 val setflags = true 2202 in 2203 Data(Register(opc,(setflags,(d,(n,m))))) 2204 end 2205 | BitsN.B(0x6,_) => 2206 let 2207 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2208 val n = d 2209 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2210 val setflags = true 2211 in 2212 Data(Register(opc,(setflags,(d,(n,m))))) 2213 end 2214 | BitsN.B(0xC,_) => 2215 let 2216 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2217 val n = d 2218 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2219 val setflags = true 2220 in 2221 Data(Register(opc,(setflags,(d,(n,m))))) 2222 end 2223 | BitsN.B(0xE,_) => 2224 let 2225 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2226 val n = d 2227 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2228 val setflags = true 2229 in 2230 Data(Register(opc,(setflags,(d,(n,m))))) 2231 end 2232 | BitsN.B(0x2,_) => 2233 let 2234 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2235 val n = d 2236 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2237 val shift_t = 2238 DecodeRegShift 2239 (BitsN.fromNat 2240 (BitsN.toNat(BitsN.-(opc,BitsN.B(0x2,4))),2)) 2241 in 2242 Data(ShiftRegister(d,(n,(shift_t,m)))) 2243 end 2244 | BitsN.B(0x3,_) => 2245 let 2246 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2247 val n = d 2248 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2249 val shift_t = 2250 DecodeRegShift 2251 (BitsN.fromNat 2252 (BitsN.toNat(BitsN.-(opc,BitsN.B(0x2,4))),2)) 2253 in 2254 Data(ShiftRegister(d,(n,(shift_t,m)))) 2255 end 2256 | BitsN.B(0x4,_) => 2257 let 2258 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2259 val n = d 2260 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2261 val shift_t = 2262 DecodeRegShift 2263 (BitsN.fromNat 2264 (BitsN.toNat(BitsN.-(opc,BitsN.B(0x2,4))),2)) 2265 in 2266 Data(ShiftRegister(d,(n,(shift_t,m)))) 2267 end 2268 | BitsN.B(0x7,_) => 2269 let 2270 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2271 val n = d 2272 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2273 in 2274 Data(ShiftRegister(d,(n,(SRType_ROR,m)))) 2275 end 2276 | BitsN.B(0x8,_) => 2277 let 2278 val n = BitsN.fromNat(BitsN.toNat Ry,4) 2279 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2280 in 2281 Data(TestCompareRegister(BitsN.bits(1,0) opc,(n,m))) 2282 end 2283 | BitsN.B(0xA,_) => 2284 let 2285 val n = BitsN.fromNat(BitsN.toNat Ry,4) 2286 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2287 in 2288 Data(TestCompareRegister(BitsN.bits(1,0) opc,(n,m))) 2289 end 2290 | BitsN.B(0xB,_) => 2291 let 2292 val n = BitsN.fromNat(BitsN.toNat Ry,4) 2293 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2294 in 2295 Data(TestCompareRegister(BitsN.bits(1,0) opc,(n,m))) 2296 end 2297 | BitsN.B(0x9,_) => 2298 let 2299 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2300 val n = BitsN.fromNat(BitsN.toNat Rx,4) 2301 val setflags = true 2302 in 2303 Data 2304 (ArithLogicImmediate 2305 (BitsN.B(0x3,4),(setflags,(d,(n,BitsN.B(0x0,32)))))) 2306 end 2307 | BitsN.B(0xD,_) => 2308 let 2309 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2310 val n = BitsN.fromNat(BitsN.toNat Rx,4) 2311 val m = d 2312 in 2313 Multiply(Multiply32(d,(n,m))) 2314 end 2315 | BitsN.B(0xF,_) => 2316 let 2317 val d = BitsN.fromNat(BitsN.toNat Ry,4) 2318 val m = BitsN.fromNat(BitsN.toNat Rx,4) 2319 val setflags = true 2320 val (shift_t,shift_n) = (SRType_LSL,0) 2321 in 2322 Data 2323 (ShiftImmediate(true,(setflags,(d,(m,(shift_t,shift_n)))))) 2324 end 2325 | _ => raise General.Bind 2326 end 2327 | (false, 2328 (true, 2329 (false, 2330 (false, 2331 (false, 2332 (true, 2333 (false, 2334 (false, 2335 (DN'0,(Rm'3,(Rm'2,(Rm'1,(Rm'0,(Rdn'2,(Rdn'1,Rdn'0))))))))))))))) => 2336 let 2337 val Rm = BitsN.fromBitstring([Rm'3,Rm'2,Rm'1,Rm'0],4) 2338 val d = 2339 BitsN.@@ 2340 (BitsN.fromBitstring([DN'0],1), 2341 BitsN.fromBitstring([Rdn'2,Rdn'1,Rdn'0],3)) 2342 val n = d 2343 in 2344 ( if (n = (BitsN.B(0xF,4))) andalso (Rm = (BitsN.B(0xF,4))) 2345 then DECODE_UNPREDICTABLE(mc,"ADD") 2346 else () 2347 ; let 2348 val setflags = false 2349 in 2350 Data(Register(BitsN.B(0x4,4),(setflags,(d,(n,Rm))))) 2351 end 2352 ) 2353 end 2354 | (false, 2355 (true, 2356 (false, 2357 (false, 2358 (false, 2359 (true, 2360 (false, 2361 (true,(N'0,(Rm'3,(Rm'2,(Rm'1,(Rm'0,(Rn'2,(Rn'1,Rn'0))))))))))))))) => 2362 let 2363 val Rm = BitsN.fromBitstring([Rm'3,Rm'2,Rm'1,Rm'0],4) 2364 val n = 2365 BitsN.@@ 2366 (BitsN.fromBitstring([N'0],1), 2367 BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)) 2368 in 2369 ( if ((BitsN.<+(n,BitsN.B(0x8,4))) andalso 2370 (BitsN.<+(Rm,BitsN.B(0x8,4)))) orelse 2371 ((n = (BitsN.B(0xF,4))) orelse (Rm = (BitsN.B(0xF,4)))) 2372 then DECODE_UNPREDICTABLE(mc,"CMP") 2373 else () 2374 ; Data(TestCompareRegister(BitsN.B(0x2,2),(n,Rm))) 2375 ) 2376 end 2377 | (false, 2378 (true, 2379 (false, 2380 (false, 2381 (false, 2382 (true, 2383 (true, 2384 (false,(D'0,(Rm'3,(Rm'2,(Rm'1,(Rm'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) => 2385 let 2386 val d = 2387 BitsN.@@ 2388 (BitsN.fromBitstring([D'0],1), 2389 BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)) 2390 val setflags = false 2391 val (shift_t,shift_n) = (SRType_LSL,0) 2392 in 2393 Data 2394 (ShiftImmediate 2395 (false, 2396 (setflags, 2397 (d, 2398 (BitsN.fromBitstring([Rm'3,Rm'2,Rm'1,Rm'0],4), 2399 (shift_t,shift_n)))))) 2400 end 2401 | (false, 2402 (true, 2403 (false, 2404 (false, 2405 (false,(true,(true,(true,(false,(Rm'3,(Rm'2,(Rm'1,(Rm'0,_))))))))))))) => 2406 Branch 2407 (BranchExchange(BitsN.fromBitstring([Rm'3,Rm'2,Rm'1,Rm'0],4))) 2408 | (false, 2409 (true, 2410 (false, 2411 (false, 2412 (false,(true,(true,(true,(true,(Rm'3,(Rm'2,(Rm'1,(Rm'0,_))))))))))))) => 2413 Branch 2414 (BranchLinkExchangeRegister 2415 (BitsN.fromBitstring([Rm'3,Rm'2,Rm'1,Rm'0],4))) 2416 | (false, 2417 (true, 2418 (false, 2419 (false, 2420 (true, 2421 (Rt'2, 2422 (Rt'1, 2423 (Rt'0, 2424 (imm8'7, 2425 (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) => 2426 let 2427 val imm32 = 2428 BitsN.zeroExtend 32 2429 (BitsN.@@ 2430 (BitsN.fromBitstring 2431 ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1, 2432 imm8'0],8),BitsN.B(0x0,2))) 2433 in 2434 Load 2435 (LoadLiteral 2436 (BitsN.fromNat 2437 (BitsN.toNat(BitsN.fromBitstring([Rt'2,Rt'1,Rt'0],3)),4), 2438 imm32)) 2439 end 2440 | (false, 2441 (true, 2442 (false, 2443 (true, 2444 (opc'2, 2445 (opc'1, 2446 (opc'0, 2447 (Rm'2,(Rm'1,(Rm'0,(Rn'2,(Rn'1,(Rn'0,(Rt'2,(Rt'1,Rt'0))))))))))))))) => 2448 let 2449 val Rt = BitsN.fromBitstring([Rt'2,Rt'1,Rt'0],3) 2450 val Rn = BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3) 2451 val m = 2452 register_form 2453 (BitsN.fromNat 2454 (BitsN.toNat(BitsN.fromBitstring([Rm'2,Rm'1,Rm'0],3)),4)) 2455 in 2456 case BitsN.fromBitstring([opc'2,opc'1,opc'0],3) of 2457 BitsN.B(0x0,_) => 2458 Store 2459 (StoreWord 2460 (BitsN.fromNat(BitsN.toNat Rt,4), 2461 (BitsN.fromNat(BitsN.toNat Rn,4),m))) 2462 | BitsN.B(0x1,_) => 2463 Store 2464 (StoreHalf 2465 (BitsN.fromNat(BitsN.toNat Rt,4), 2466 (BitsN.fromNat(BitsN.toNat Rn,4),m))) 2467 | BitsN.B(0x2,_) => 2468 Store 2469 (StoreByte 2470 (BitsN.fromNat(BitsN.toNat Rt,4), 2471 (BitsN.fromNat(BitsN.toNat Rn,4),m))) 2472 | BitsN.B(0x3,_) => 2473 Load 2474 (LoadByte 2475 (false, 2476 (BitsN.fromNat(BitsN.toNat Rt,4), 2477 (BitsN.fromNat(BitsN.toNat Rn,4),m)))) 2478 | BitsN.B(0x4,_) => 2479 Load 2480 (LoadWord 2481 (BitsN.fromNat(BitsN.toNat Rt,4), 2482 (BitsN.fromNat(BitsN.toNat Rn,4),m))) 2483 | BitsN.B(0x5,_) => 2484 Load 2485 (LoadHalf 2486 (true, 2487 (BitsN.fromNat(BitsN.toNat Rt,4), 2488 (BitsN.fromNat(BitsN.toNat Rn,4),m)))) 2489 | BitsN.B(0x6,_) => 2490 Load 2491 (LoadByte 2492 (true, 2493 (BitsN.fromNat(BitsN.toNat Rt,4), 2494 (BitsN.fromNat(BitsN.toNat Rn,4),m)))) 2495 | BitsN.B(0x7,_) => 2496 Load 2497 (LoadHalf 2498 (false, 2499 (BitsN.fromNat(BitsN.toNat Rt,4), 2500 (BitsN.fromNat(BitsN.toNat Rn,4),m)))) 2501 | _ => raise General.Bind 2502 end 2503 | (false, 2504 (true, 2505 (true, 2506 (false, 2507 (L'0, 2508 (imm5'4, 2509 (imm5'3, 2510 (imm5'2, 2511 (imm5'1,(imm5'0,(Rn'2,(Rn'1,(Rn'0,(Rt'2,(Rt'1,Rt'0))))))))))))))) => 2512 let 2513 val Rt = BitsN.fromBitstring([Rt'2,Rt'1,Rt'0],3) 2514 val Rn = BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3) 2515 val imm32 = 2516 BitsN.zeroExtend 32 2517 (BitsN.@@ 2518 (BitsN.fromBitstring 2519 ([imm5'4,imm5'3,imm5'2,imm5'1,imm5'0],5),BitsN.B(0x0,2))) 2520 val m = immediate_form imm32 2521 in 2522 if (BitsN.fromBitstring([L'0],1)) = (BitsN.B(0x1,1)) 2523 then Load 2524 (LoadWord 2525 (BitsN.fromNat(BitsN.toNat Rt,4), 2526 (BitsN.fromNat(BitsN.toNat Rn,4),m))) 2527 else Store 2528 (StoreWord 2529 (BitsN.fromNat(BitsN.toNat Rt,4), 2530 (BitsN.fromNat(BitsN.toNat Rn,4),m))) 2531 end 2532 | (false, 2533 (true, 2534 (true, 2535 (true, 2536 (L'0, 2537 (imm5'4, 2538 (imm5'3, 2539 (imm5'2, 2540 (imm5'1,(imm5'0,(Rn'2,(Rn'1,(Rn'0,(Rt'2,(Rt'1,Rt'0))))))))))))))) => 2541 let 2542 val Rt = BitsN.fromBitstring([Rt'2,Rt'1,Rt'0],3) 2543 val Rn = BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3) 2544 val imm32 = 2545 BitsN.zeroExtend 32 2546 (BitsN.fromBitstring([imm5'4,imm5'3,imm5'2,imm5'1,imm5'0],5)) 2547 val m = immediate_form imm32 2548 in 2549 if (BitsN.fromBitstring([L'0],1)) = (BitsN.B(0x1,1)) 2550 then Load 2551 (LoadByte 2552 (true, 2553 (BitsN.fromNat(BitsN.toNat Rt,4), 2554 (BitsN.fromNat(BitsN.toNat Rn,4),m)))) 2555 else Store 2556 (StoreByte 2557 (BitsN.fromNat(BitsN.toNat Rt,4), 2558 (BitsN.fromNat(BitsN.toNat Rn,4),m))) 2559 end 2560 | (true, 2561 (false, 2562 (false, 2563 (false, 2564 (L'0, 2565 (imm5'4, 2566 (imm5'3, 2567 (imm5'2, 2568 (imm5'1,(imm5'0,(Rn'2,(Rn'1,(Rn'0,(Rt'2,(Rt'1,Rt'0))))))))))))))) => 2569 let 2570 val Rt = BitsN.fromBitstring([Rt'2,Rt'1,Rt'0],3) 2571 val Rn = BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3) 2572 val imm32 = 2573 BitsN.zeroExtend 32 2574 (BitsN.@@ 2575 (BitsN.fromBitstring 2576 ([imm5'4,imm5'3,imm5'2,imm5'1,imm5'0],5),BitsN.B(0x0,1))) 2577 val m = immediate_form imm32 2578 in 2579 if (BitsN.fromBitstring([L'0],1)) = (BitsN.B(0x1,1)) 2580 then Load 2581 (LoadHalf 2582 (true, 2583 (BitsN.fromNat(BitsN.toNat Rt,4), 2584 (BitsN.fromNat(BitsN.toNat Rn,4),m)))) 2585 else Store 2586 (StoreHalf 2587 (BitsN.fromNat(BitsN.toNat Rt,4), 2588 (BitsN.fromNat(BitsN.toNat Rn,4),m))) 2589 end 2590 | (true, 2591 (false, 2592 (false, 2593 (true, 2594 (L'0, 2595 (Rt'2, 2596 (Rt'1, 2597 (Rt'0, 2598 (imm8'7, 2599 (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) => 2600 let 2601 val Rt = BitsN.fromBitstring([Rt'2,Rt'1,Rt'0],3) 2602 val imm32 = 2603 BitsN.zeroExtend 32 2604 (BitsN.@@ 2605 (BitsN.fromBitstring 2606 ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1, 2607 imm8'0],8),BitsN.B(0x0,2))) 2608 val m = immediate_form imm32 2609 in 2610 if (BitsN.fromBitstring([L'0],1)) = (BitsN.B(0x1,1)) 2611 then Load 2612 (LoadWord 2613 (BitsN.fromNat(BitsN.toNat Rt,4),(BitsN.B(0xD,4),m))) 2614 else Store 2615 (StoreWord 2616 (BitsN.fromNat(BitsN.toNat Rt,4),(BitsN.B(0xD,4),m))) 2617 end 2618 | (true, 2619 (false, 2620 (true, 2621 (false, 2622 (S'0, 2623 (Rd'2, 2624 (Rd'1, 2625 (Rd'0, 2626 (imm8'7, 2627 (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) => 2628 let 2629 val imm32 = 2630 BitsN.zeroExtend 32 2631 (BitsN.@@ 2632 (BitsN.fromBitstring 2633 ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1, 2634 imm8'0],8),BitsN.B(0x0,2))) 2635 val Rn = 2636 if (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x1,1)) 2637 then BitsN.B(0xD,4) 2638 else BitsN.B(0xF,4) 2639 in 2640 Data 2641 (ArithLogicImmediate 2642 (BitsN.B(0x4,4), 2643 (false, 2644 (BitsN.fromNat 2645 (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4), 2646 (Rn,imm32))))) 2647 end 2648 | (true, 2649 (false, 2650 (true, 2651 (true, 2652 (false, 2653 (false, 2654 (false, 2655 (false, 2656 (S'0, 2657 (imm7'6,(imm7'5,(imm7'4,(imm7'3,(imm7'2,(imm7'1,imm7'0))))))))))))))) => 2658 let 2659 val imm32 = 2660 BitsN.zeroExtend 32 2661 (BitsN.@@ 2662 (BitsN.fromBitstring 2663 ([imm7'6,imm7'5,imm7'4,imm7'3,imm7'2,imm7'1,imm7'0],7), 2664 BitsN.B(0x0,2))) 2665 val opc = 2666 if (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x1,1)) 2667 then BitsN.B(0x2,4) 2668 else BitsN.B(0x4,4) 2669 in 2670 Data 2671 (ArithLogicImmediate 2672 (opc,(false,(BitsN.B(0xD,4),(BitsN.B(0xD,4),imm32))))) 2673 end 2674 | (true, 2675 (false, 2676 (true, 2677 (true, 2678 (false, 2679 (false, 2680 (true, 2681 (false,(U'0,(false,(Rm'2,(Rm'1,(Rm'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) => 2682 let 2683 val unsigned = (BitsN.fromBitstring([U'0],1)) = (BitsN.B(0x1,1)) 2684 in 2685 Media 2686 (ExtendHalfword 2687 (unsigned, 2688 (BitsN.fromNat 2689 (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4), 2690 BitsN.fromNat 2691 (BitsN.toNat(BitsN.fromBitstring([Rm'2,Rm'1,Rm'0],3)),4)))) 2692 end 2693 | (true, 2694 (false, 2695 (true, 2696 (true, 2697 (false, 2698 (false, 2699 (true, 2700 (false,(U'0,(true,(Rm'2,(Rm'1,(Rm'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) => 2701 let 2702 val unsigned = (BitsN.fromBitstring([U'0],1)) = (BitsN.B(0x1,1)) 2703 in 2704 Media 2705 (ExtendByte 2706 (unsigned, 2707 (BitsN.fromNat 2708 (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4), 2709 BitsN.fromNat 2710 (BitsN.toNat(BitsN.fromBitstring([Rm'2,Rm'1,Rm'0],3)),4)))) 2711 end 2712 | (true, 2713 (false, 2714 (true, 2715 (true, 2716 (false, 2717 (true, 2718 (false, 2719 (registers'8, 2720 (registers'7, 2721 (registers'6, 2722 (registers'5, 2723 (registers'4, 2724 (registers'3,(registers'2,(registers'1,registers'0))))))))))))))) => 2725 let 2726 val registers = 2727 BitsN.fromBitstring 2728 ([registers'8,registers'7,registers'6,registers'5, 2729 registers'4,registers'3,registers'2,registers'1,registers'0], 2730 9) 2731 in 2732 ( if Nat.<(BitCount 9 registers,1) 2733 then DECODE_UNPREDICTABLE(mc,"Push") 2734 else () 2735 ; Store(Push registers) 2736 ) 2737 end 2738 | (true, 2739 (false, 2740 (true, 2741 (true,(false,(true,(true,(false,(false,(true,(true,(im'0,_)))))))))))) => 2742 System 2743 (ChangeProcessorState 2744 ((not o L3.equal (BitsN.zero (1))) 2745 (BitsN.fromBitstring([im'0],1)))) 2746 | (true, 2747 (false, 2748 (true, 2749 (true, 2750 (true, 2751 (false, 2752 (true, 2753 (false,(opc'1,(opc'0,(Rm'2,(Rm'1,(Rm'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) => 2754 let 2755 val Rd = BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3) 2756 val Rm = BitsN.fromBitstring([Rm'2,Rm'1,Rm'0],3) 2757 in 2758 case BitsN.fromBitstring([opc'1,opc'0],2) of 2759 BitsN.B(0x0,_) => 2760 Media 2761 (ByteReverse 2762 (BitsN.fromNat(BitsN.toNat Rd,4), 2763 BitsN.fromNat(BitsN.toNat Rm,4))) 2764 | BitsN.B(0x1,_) => 2765 Media 2766 (ByteReversePackedHalfword 2767 (BitsN.fromNat(BitsN.toNat Rd,4), 2768 BitsN.fromNat(BitsN.toNat Rm,4))) 2769 | BitsN.B(0x3,_) => 2770 Media 2771 (ByteReverseSignedHalfword 2772 (BitsN.fromNat(BitsN.toNat Rd,4), 2773 BitsN.fromNat(BitsN.toNat Rm,4))) 2774 | _ => Undefined(BitsN.B(0x0,32)) 2775 end 2776 | (true, 2777 (false, 2778 (true, 2779 (true, 2780 (true, 2781 (true, 2782 (false, 2783 (registers'8, 2784 (registers'7, 2785 (registers'6, 2786 (registers'5, 2787 (registers'4, 2788 (registers'3,(registers'2,(registers'1,registers'0))))))))))))))) => 2789 let 2790 val registers = 2791 BitsN.fromBitstring 2792 ([registers'8,registers'7,registers'6,registers'5, 2793 registers'4,registers'3,registers'2,registers'1,registers'0], 2794 9) 2795 in 2796 ( if Nat.<(BitCount 9 registers,1) 2797 then DECODE_UNPREDICTABLE(mc,"POP") 2798 else () 2799 ; let 2800 val wback = true 2801 in 2802 Load(LoadMultiple(wback,(BitsN.B(0xD,4),registers))) 2803 end 2804 ) 2805 end 2806 | (true, 2807 (false, 2808 (true, 2809 (true, 2810 (true, 2811 (true, 2812 (true, 2813 (false, 2814 (imm8'7, 2815 (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) => 2816 let 2817 val imm32 = 2818 BitsN.zeroExtend 32 2819 (BitsN.fromBitstring 2820 ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,imm8'0], 2821 8)) 2822 in 2823 Hint(Breakpoint imm32) 2824 end 2825 | (true, 2826 (false, 2827 (true, 2828 (true, 2829 (true, 2830 (true, 2831 (true, 2832 (true, 2833 (op'3,(op'2,(op'1,(op'0,(false,(false,(false,false))))))))))))))) => 2834 (case BitsN.fromBitstring([op'3,op'2,op'1,op'0],4) of 2835 BitsN.B(0x1,_) => Hint(Yield ()) 2836 | BitsN.B(0x2,_) => Hint(WaitForEvent ()) 2837 | BitsN.B(0x3,_) => Hint(WaitForInterrupt ()) 2838 | BitsN.B(0x4,_) => Hint(SendEvent ()) 2839 | _ => NoOperation ()) 2840 | (true, 2841 (true, 2842 (false, 2843 (false, 2844 (false, 2845 (Rn'2, 2846 (Rn'1, 2847 (Rn'0, 2848 (registers'7, 2849 (registers'6, 2850 (registers'5, 2851 (registers'4, 2852 (registers'3,(registers'2,(registers'1,registers'0))))))))))))))) => 2853 let 2854 val registers = 2855 BitsN.fromBitstring 2856 ([registers'7,registers'6,registers'5,registers'4, 2857 registers'3,registers'2,registers'1,registers'0],8) 2858 in 2859 ( if Nat.<(BitCount 8 registers,1) 2860 then DECODE_UNPREDICTABLE(mc,"StoreMultiple") 2861 else () 2862 ; Store 2863 (StoreMultiple 2864 (BitsN.fromNat 2865 (BitsN.toNat(BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)),4), 2866 registers)) 2867 ) 2868 end 2869 | (true, 2870 (true, 2871 (false, 2872 (false, 2873 (true, 2874 (Rn'2, 2875 (Rn'1, 2876 (Rn'0, 2877 (register_list'7, 2878 (register_list'6, 2879 (register_list'5, 2880 (register_list'4, 2881 (register_list'3, 2882 (register_list'2,(register_list'1,register_list'0))))))))))))))) => 2883 let 2884 val Rn = BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3) 2885 val registers = 2886 BitsN.fromNat 2887 (BitsN.toNat 2888 (BitsN.fromBitstring 2889 ([register_list'7,register_list'6,register_list'5, 2890 register_list'4,register_list'3,register_list'2, 2891 register_list'1,register_list'0],8)),9) 2892 in 2893 ( if Nat.<(BitCount 9 registers,1) 2894 then DECODE_UNPREDICTABLE(mc,"LoadMultiple") 2895 else () 2896 ; let 2897 val wback = not(BitsN.bit(registers,BitsN.toNat Rn)) 2898 in 2899 Load 2900 (LoadMultiple 2901 (wback,(BitsN.fromNat(BitsN.toNat Rn,4),registers))) 2902 end 2903 ) 2904 end 2905 | (true, 2906 (true, 2907 (false, 2908 (true, 2909 (true, 2910 (true, 2911 (true, 2912 (false, 2913 (imm8'7, 2914 (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) => 2915 let 2916 val imm32 = 2917 BitsN.zeroExtend 32 2918 (BitsN.fromBitstring 2919 ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,imm8'0], 2920 8)) 2921 in 2922 Undefined imm32 2923 end 2924 | (true, 2925 (true, 2926 (false, 2927 (true, 2928 (true, 2929 (true, 2930 (true, 2931 (true, 2932 (imm8'7, 2933 (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) => 2934 System 2935 (SupervisorCall 2936 (BitsN.zeroExtend 32 2937 (BitsN.fromBitstring 2938 ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1, 2939 imm8'0],8)))) 2940 | (true, 2941 (true, 2942 (false, 2943 (true, 2944 (cond'3, 2945 (cond'2, 2946 (cond'1, 2947 (cond'0, 2948 (imm8'7, 2949 (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) => 2950 (if ConditionPassed 2951 (BitsN.fromBitstring([cond'3,cond'2,cond'1,cond'0],4)) 2952 then let 2953 val imm32 = 2954 BitsN.signExtend 32 2955 (BitsN.@@ 2956 (BitsN.fromBitstring 2957 ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2, 2958 imm8'1,imm8'0],8),BitsN.B(0x0,1))) 2959 in 2960 Branch(BranchTarget imm32) 2961 end 2962 else NoOperation ()) 2963 | (true, 2964 (true, 2965 (true, 2966 (false, 2967 (false, 2968 (imm11'10, 2969 (imm11'9, 2970 (imm11'8, 2971 (imm11'7, 2972 (imm11'6, 2973 (imm11'5,(imm11'4,(imm11'3,(imm11'2,(imm11'1,imm11'0))))))))))))))) => 2974 let 2975 val imm32 = 2976 BitsN.signExtend 32 2977 (BitsN.@@ 2978 (BitsN.fromBitstring 2979 ([imm11'10,imm11'9,imm11'8,imm11'7,imm11'6,imm11'5, 2980 imm11'4,imm11'3,imm11'2,imm11'1,imm11'0],11), 2981 BitsN.B(0x0,1))) 2982 in 2983 Branch(BranchTarget imm32) 2984 end 2985 | _ => Undefined(BitsN.B(0x0,32)) 2986 end; 2987 2988fun DecodeThumb2 h = 2989 let 2990 val mc = Thumb2 h 2991 in 2992 case (boolify'16(L3.fst h),boolify'16(L3.snd h)) of 2993 ((true, 2994 (true, 2995 (true, 2996 (true, 2997 (false, 2998 (false, 2999 (true, 3000 (true,(true,(false,(false,(_,(Rn'3,(Rn'2,(Rn'1,Rn'0))))))))))))))), 3001 (true, 3002 (false, 3003 (_, 3004 (false, 3005 (_, 3006 (_, 3007 (_, 3008 (_, 3009 (SYSm'7, 3010 (SYSm'6, 3011 (SYSm'5,(SYSm'4,(SYSm'3,(SYSm'2,(SYSm'1,SYSm'0)))))))))))))))) => 3012 let 3013 val Rn = BitsN.fromBitstring([Rn'3,Rn'2,Rn'1,Rn'0],4) 3014 val SYSm = 3015 BitsN.fromBitstring 3016 ([SYSm'7,SYSm'6,SYSm'5,SYSm'4,SYSm'3,SYSm'2,SYSm'1,SYSm'0], 3017 8) 3018 in 3019 ( if (Set.mem(Rn,[BitsN.B(0xD,4),BitsN.B(0xF,4)])) orelse 3020 (not(Set.mem 3021 (SYSm, 3022 [BitsN.B(0x0,8),BitsN.B(0x1,8),BitsN.B(0x2,8), 3023 BitsN.B(0x3,8),BitsN.B(0x5,8),BitsN.B(0x6,8), 3024 BitsN.B(0x7,8),BitsN.B(0x8,8),BitsN.B(0x9,8), 3025 BitsN.B(0x10,8),BitsN.B(0x11,8),BitsN.B(0x12,8), 3026 BitsN.B(0x13,8),BitsN.B(0x14,8)]))) 3027 then DECODE_UNPREDICTABLE(mc,"MoveToSpecialRegister") 3028 else () 3029 ; System(MoveToSpecialRegister(SYSm,Rn)) 3030 ) 3031 end 3032 | ((true, 3033 (true, 3034 (true, 3035 (true, 3036 (false,(false,(true,(true,(true,(false,(true,(true,_)))))))))))), 3037 (true, 3038 (false, 3039 (_, 3040 (false, 3041 (_, 3042 (_, 3043 (_, 3044 (_, 3045 (op'3, 3046 (op'2, 3047 (op'1,(op'0,(option'3,(option'2,(option'1,option'0)))))))))))))))) => 3048 let 3049 val option = 3050 BitsN.fromBitstring([option'3,option'2,option'1,option'0],4) 3051 in 3052 case BitsN.fromBitstring([op'3,op'2,op'1,op'0],4) of 3053 BitsN.B(0x4,_) => Hint(DataSynchronizationBarrier option) 3054 | BitsN.B(0x5,_) => Hint(DataMemoryBarrier option) 3055 | BitsN.B(0x6,_) => 3056 Hint(InstructionSynchronizationBarrier option) 3057 | _ => Undefined(BitsN.B(0x0,32)) 3058 end 3059 | ((true, 3060 (true, 3061 (true,(true,(false,(false,(true,(true,(true,(true,(true,_))))))))))), 3062 (true, 3063 (false, 3064 (_, 3065 (false, 3066 (Rd'3, 3067 (Rd'2, 3068 (Rd'1, 3069 (Rd'0, 3070 (SYSm'7, 3071 (SYSm'6,(SYSm'5,(SYSm'4,(SYSm'3,(SYSm'2,(SYSm'1,SYSm'0)))))))))))))))) => 3072 let 3073 val SYSm = 3074 BitsN.fromBitstring 3075 ([SYSm'7,SYSm'6,SYSm'5,SYSm'4,SYSm'3,SYSm'2,SYSm'1,SYSm'0],8) 3076 val Rd = BitsN.fromBitstring([Rd'3,Rd'2,Rd'1,Rd'0],4) 3077 in 3078 ( if (Set.mem(Rd,[BitsN.B(0xD,4),BitsN.B(0xF,4)])) orelse 3079 (not(Set.mem 3080 (SYSm, 3081 [BitsN.B(0x0,8),BitsN.B(0x1,8),BitsN.B(0x2,8), 3082 BitsN.B(0x3,8),BitsN.B(0x5,8),BitsN.B(0x6,8), 3083 BitsN.B(0x7,8),BitsN.B(0x8,8),BitsN.B(0x9,8), 3084 BitsN.B(0x10,8),BitsN.B(0x11,8),BitsN.B(0x12,8), 3085 BitsN.B(0x13,8),BitsN.B(0x14,8)]))) 3086 then DECODE_UNPREDICTABLE(mc,"MoveToRegisterFromSpecial") 3087 else () 3088 ; System(MoveToRegisterFromSpecial(SYSm,Rd)) 3089 ) 3090 end 3091 | ((true, 3092 (true, 3093 (true, 3094 (true, 3095 (false, 3096 (true, 3097 (true, 3098 (true, 3099 (true,(true,(true,(true,(imm4'3,(imm4'2,(imm4'1,imm4'0))))))))))))))), 3100 (true, 3101 (false, 3102 (true, 3103 (false, 3104 (imm12'11, 3105 (imm12'10, 3106 (imm12'9, 3107 (imm12'8, 3108 (imm12'7, 3109 (imm12'6, 3110 (imm12'5,(imm12'4,(imm12'3,(imm12'2,(imm12'1,imm12'0)))))))))))))))) => 3111 let 3112 val imm32 = 3113 BitsN.zeroExtend 32 3114 (BitsN.@@ 3115 (BitsN.fromBitstring([imm4'3,imm4'2,imm4'1,imm4'0],4), 3116 BitsN.fromBitstring 3117 ([imm12'11,imm12'10,imm12'9,imm12'8,imm12'7,imm12'6, 3118 imm12'5,imm12'4,imm12'3,imm12'2,imm12'1,imm12'0],12))) 3119 in 3120 Undefined imm32 3121 end 3122 | ((true, 3123 (true, 3124 (true, 3125 (true, 3126 (false, 3127 (S'0, 3128 (imm10'9, 3129 (imm10'8, 3130 (imm10'7, 3131 (imm10'6, 3132 (imm10'5,(imm10'4,(imm10'3,(imm10'2,(imm10'1,imm10'0))))))))))))))), 3133 (true, 3134 (true, 3135 (J1'0, 3136 (true, 3137 (J2'0, 3138 (imm11'10, 3139 (imm11'9, 3140 (imm11'8, 3141 (imm11'7, 3142 (imm11'6, 3143 (imm11'5,(imm11'4,(imm11'3,(imm11'2,(imm11'1,imm11'0)))))))))))))))) => 3144 let 3145 val S = BitsN.fromBitstring([S'0],1) 3146 val I1 = BitsN.~(BitsN.??(BitsN.fromBitstring([J1'0],1),S)) 3147 val I2 = BitsN.~(BitsN.??(BitsN.fromBitstring([J2'0],1),S)) 3148 val imm32 = 3149 BitsN.signExtend 32 3150 (BitsN.concat 3151 [S,I1,I2, 3152 BitsN.fromBitstring 3153 ([imm10'9,imm10'8,imm10'7,imm10'6,imm10'5,imm10'4, 3154 imm10'3,imm10'2,imm10'1,imm10'0],10), 3155 BitsN.fromBitstring 3156 ([imm11'10,imm11'9,imm11'8,imm11'7,imm11'6,imm11'5, 3157 imm11'4,imm11'3,imm11'2,imm11'1,imm11'0],11), 3158 BitsN.B(0x0,1)]) 3159 in 3160 Branch(BranchLinkImmediate imm32) 3161 end 3162 | _ => Undefined(BitsN.B(0x0,32)) 3163 end; 3164 3165fun Decode mc = 3166 case mc of 3167 Thumb h => ( pcinc := (BitsN.B(0x2,32)); DecodeThumb h ) 3168 | Thumb2 hs => ( pcinc := (BitsN.B(0x4,32)); DecodeThumb2 hs ); 3169 3170fun Next () = Run(Decode(Fetch ())); 3171 3172fun EncodeImmShift (shift_t,shift_n) = 3173 case shift_t of 3174 SRType_LSL => (BitsN.B(0x0,2),BitsN.fromNat(shift_n,5)) 3175 | SRType_LSR => 3176 (BitsN.B(0x1,2), 3177 if shift_n = 32 then BitsN.B(0x0,5) else BitsN.fromNat(shift_n,5)) 3178 | SRType_ASR => 3179 (BitsN.B(0x2,2), 3180 if shift_n = 32 then BitsN.B(0x0,5) else BitsN.fromNat(shift_n,5)) 3181 | SRType_ROR => (BitsN.B(0x3,2),BitsN.fromNat(shift_n,5)) 3182 | SRType_RRX => (BitsN.B(0x3,2),BitsN.B(0x0,5)); 3183 3184fun e_branch (c,(ast,e)) = 3185 case ast of 3186 BranchTarget imm32 => 3187 (if Set.mem(c,[BitsN.B(0xE,4),BitsN.B(0xF,4)]) 3188 then if (BitsN.<=(BitsN.neg(BitsN.B(0x800,32)),imm32)) andalso 3189 ((BitsN.<=(imm32,BitsN.B(0x7FE,32))) andalso 3190 (not(e = Enc_Wide))) 3191 then Thumb16 3192 (BitsN.@@(BitsN.B(0x1C,5),BitsN.bits(11,1) imm32)) 3193 else let 3194 val S = BitsN.bits(24,24) imm32 3195 val I1 = BitsN.bits(23,23) imm32 3196 val I2 = BitsN.bits(22,22) imm32 3197 val J1 = BitsN.fromBit(I1 = S) 3198 val J2 = BitsN.fromBit(I2 = S) 3199 val imm10 = BitsN.bits(21,12) imm32 3200 val imm11 = BitsN.bits(11,1) imm32 3201 in 3202 Thumb32 3203 (BitsN.concat[BitsN.B(0x1E,5),S,imm10], 3204 BitsN.concat 3205 [BitsN.B(0x2,2),J1,BitsN.B(0x1,1),J2,imm11]) 3206 end 3207 else if (BitsN.<=(BitsN.neg(BitsN.B(0x100,32)),imm32)) andalso 3208 ((BitsN.<=(imm32,BitsN.B(0xFE,32))) andalso (not(e = Enc_Wide))) 3209 then Thumb16 3210 (BitsN.concat[BitsN.B(0xD,4),c,BitsN.bits(8,1) imm32]) 3211 else BadCode "BranchTarget") 3212 | BranchExchange Rm => 3213 Thumb16(BitsN.concat[BitsN.B(0x8E,9),Rm,BitsN.B(0x0,3)]) 3214 | BranchLinkExchangeRegister Rm => 3215 Thumb16(BitsN.concat[BitsN.B(0x8F,9),Rm,BitsN.B(0x0,3)]) 3216 | BranchLinkImmediate imm32 => 3217 let 3218 val S = BitsN.bits(24,24) imm32 3219 val I1 = BitsN.bits(23,23) imm32 3220 val I2 = BitsN.bits(22,22) imm32 3221 val J1 = BitsN.fromBit(I1 = S) 3222 val J2 = BitsN.fromBit(I2 = S) 3223 val imm10 = BitsN.bits(21,12) imm32 3224 val imm11 = BitsN.bits(11,1) imm32 3225 in 3226 Thumb32 3227 (BitsN.concat[BitsN.B(0x1E,5),S,imm10], 3228 BitsN.concat[BitsN.B(0x3,2),J1,BitsN.B(0x1,1),J2,imm11]) 3229 end; 3230 3231fun e_data ast = 3232 case ast of 3233 Move(d,imm32) => 3234 Thumb16 3235 (BitsN.concat 3236 [BitsN.B(0x4,5),BitsN.bits(2,0) d,BitsN.bits(7,0) imm32]) 3237 | ArithLogicImmediate(opc,(setflags,(d,(n,imm32)))) => 3238 (if (Set.mem(opc,[BitsN.B(0x4,4),BitsN.B(0x2,4)])) andalso 3239 ((BitsN.<=+(imm32,BitsN.B(0x7,32))) andalso 3240 (setflags andalso 3241 (not((BitsN.bit(d,3)) orelse (BitsN.bit(n,3)))))) 3242 then let 3243 val Rd = BitsN.bits(2,0) d 3244 val Rn = BitsN.bits(2,0) n 3245 val imm3 = BitsN.bits(2,0) imm32 3246 val S = BitsN.bits(1,1) opc 3247 in 3248 Thumb16(BitsN.concat[BitsN.B(0x7,6),S,imm3,Rn,Rd]) 3249 end 3250 else if (Set.mem(opc,[BitsN.B(0x4,4),BitsN.B(0x2,4)])) andalso 3251 ((d = n) andalso 3252 ((BitsN.<=+(imm32,BitsN.B(0xFF,32))) andalso 3253 (setflags andalso (not(BitsN.bit(d,3)))))) 3254 then let 3255 val Rdn = BitsN.bits(2,0) d 3256 val imm8 = BitsN.bits(7,0) imm32 3257 val S = BitsN.bits(1,1) opc 3258 in 3259 Thumb16(BitsN.concat[BitsN.B(0x3,4),S,Rdn,imm8]) 3260 end 3261 else if (opc = (BitsN.B(0x3,4))) andalso 3262 ((imm32 = (BitsN.B(0x0,32))) andalso 3263 (setflags andalso 3264 (not((BitsN.bit(d,3)) orelse (BitsN.bit(n,3)))))) 3265 then let 3266 val Rd = BitsN.bits(2,0) d 3267 val Rn = BitsN.bits(2,0) n 3268 in 3269 Thumb16(BitsN.concat[BitsN.B(0x109,10),Rn,Rd]) 3270 end 3271 else if (opc = (BitsN.B(0x4,4))) andalso 3272 ((not setflags) andalso 3273 ((Set.mem(n,[BitsN.B(0xD,4),BitsN.B(0xF,4)])) andalso 3274 ((not setflags) andalso 3275 (((BitsN.&&(imm32,BitsN.B(0xFFFFFC03,32))) = (BitsN.B(0x0,32))) andalso 3276 (not(BitsN.bit(d,3))))))) 3277 then let 3278 val Rd = BitsN.bits(2,0) d 3279 val imm8 = BitsN.bits(9,2) imm32 3280 val S = BitsN.fromBit(n = (BitsN.B(0xD,4))) 3281 in 3282 Thumb16(BitsN.concat[BitsN.B(0xA,4),S,Rd,imm8]) 3283 end 3284 else if (Set.mem(opc,[BitsN.B(0x4,4),BitsN.B(0x2,4)])) andalso 3285 ((d = (BitsN.B(0xD,4))) andalso 3286 ((n = (BitsN.B(0xD,4))) andalso 3287 ((not setflags) andalso 3288 (((BitsN.&&(imm32,BitsN.B(0xFFFFFE03,32))) = (BitsN.B(0x0,32))) andalso 3289 (not setflags))))) 3290 then let 3291 val imm7 = BitsN.bits(8,2) imm32 3292 val S = BitsN.bits(1,1) opc 3293 in 3294 Thumb16(BitsN.concat[BitsN.B(0xB0,8),S,imm7]) 3295 end 3296 else BadCode "ArithLogicImmediate") 3297 | Register(opc,(setflags,(d,(n,m)))) => 3298 (if (Set.mem(opc,[BitsN.B(0x2,4),BitsN.B(0x4,4)])) andalso 3299 (setflags andalso 3300 (not((BitsN.bit(d,3)) orelse 3301 ((BitsN.bit(n,3)) orelse (BitsN.bit(m,3)))))) 3302 then let 3303 val Rn = BitsN.bits(2,0) n 3304 val Rd = BitsN.bits(2,0) d 3305 val Rm = BitsN.bits(2,0) m 3306 val S = BitsN.fromBit(opc = (BitsN.B(0x2,4))) 3307 in 3308 Thumb16(BitsN.concat[BitsN.B(0x6,6),S,Rm,Rn,Rd]) 3309 end 3310 else if (Set.mem 3311 (opc, 3312 [BitsN.B(0x0,4),BitsN.B(0x1,4),BitsN.B(0x5,4),BitsN.B(0x6,4), 3313 BitsN.B(0xC,4),BitsN.B(0xE,4)])) andalso 3314 (setflags andalso 3315 ((d = n) andalso (not((BitsN.bit(d,3)) orelse (BitsN.bit(m,3)))))) 3316 then let 3317 val Rdn = BitsN.bits(2,0) d 3318 val Rm = BitsN.bits(2,0) m 3319 in 3320 Thumb16(BitsN.concat[BitsN.B(0x10,6),opc,Rm,Rdn]) 3321 end 3322 else if (opc = (BitsN.B(0x4,4))) andalso 3323 ((d = n) andalso (not setflags)) 3324 then let 3325 val DN = BitsN.bits(3,3) d 3326 val Rdn = BitsN.bits(2,0) d 3327 val Rm = m 3328 in 3329 Thumb16(BitsN.concat[BitsN.B(0x44,8),DN,Rm,Rdn]) 3330 end 3331 else BadCode "Register") 3332 | TestCompareRegister(opc,(n,m)) => 3333 (if not((opc = (BitsN.B(0x1,2))) orelse 3334 ((BitsN.bit(n,3)) orelse (BitsN.bit(m,3)))) 3335 then let 3336 val Rn = BitsN.bits(2,0) n 3337 val Rm = BitsN.bits(2,0) m 3338 in 3339 Thumb16(BitsN.concat[BitsN.B(0x42,8),opc,Rm,Rn]) 3340 end 3341 else if opc = (BitsN.B(0x2,2)) 3342 then let 3343 val N = BitsN.bits(3,3) n 3344 val Rn = BitsN.bits(2,0) n 3345 val Rm = m 3346 in 3347 Thumb16(BitsN.concat[BitsN.B(0x45,8),N,Rm,Rn]) 3348 end 3349 else BadCode "TestCompareRegister") 3350 | CompareImmediate(n,imm32) => 3351 Thumb16 3352 (BitsN.concat 3353 [BitsN.B(0x5,5),BitsN.bits(2,0) n,BitsN.bits(7,0) imm32]) 3354 | ShiftImmediate(negate,(setflags,(d,(m,(shift_t,shift_n))))) => 3355 (if negate andalso 3356 ((shift_t = SRType_LSL) andalso 3357 ((shift_n = 0) andalso 3358 (setflags andalso 3359 (not((BitsN.bit(m,3)) orelse (BitsN.bit(d,3))))))) 3360 then let 3361 val Rm = BitsN.bits(2,0) m 3362 val Rd = BitsN.bits(2,0) d 3363 in 3364 Thumb16(BitsN.concat[BitsN.B(0x10F,10),Rm,Rd]) 3365 end 3366 else if (Set.mem(shift_t,[SRType_LSL,SRType_LSR,SRType_ASR])) andalso 3367 (setflags andalso 3368 (not(negate orelse ((BitsN.bit(m,3)) orelse (BitsN.bit(d,3)))))) 3369 then let 3370 val Rm = BitsN.bits(2,0) m 3371 val Rd = BitsN.bits(2,0) d 3372 val (typ,imm5) = EncodeImmShift(shift_t,shift_n) 3373 in 3374 Thumb16(BitsN.concat[BitsN.B(0x0,3),typ,imm5,Rm,Rd]) 3375 end 3376 else if (shift_t = SRType_LSL) andalso 3377 ((shift_n = 0) andalso (not(negate orelse setflags))) 3378 then let 3379 val D = BitsN.bits(3,3) d 3380 val Rd = BitsN.bits(2,0) d 3381 val Rm = m 3382 in 3383 Thumb16(BitsN.concat[BitsN.B(0x46,8),D,Rm,Rd]) 3384 end 3385 else BadCode "ShiftImmediate") 3386 | ShiftRegister(_,(_,(SRType_RRX,_))) => BadCode "ShiftRegister: rrx" 3387 | ShiftRegister(d,(n,(shift_t,m))) => 3388 let 3389 val Rm = BitsN.bits(2,0) m 3390 val Rdn = BitsN.bits(2,0) d 3391 val opc = 3392 case shift_t of 3393 SRType_LSL => BitsN.B(0x2,3) 3394 | SRType_LSR => BitsN.B(0x3,3) 3395 | SRType_ASR => BitsN.B(0x4,3) 3396 | SRType_ROR => BitsN.B(0x7,3) 3397 | _ => BitsN.B(0x0,3) 3398 in 3399 Thumb16(BitsN.concat[BitsN.B(0x20,7),opc,Rm,Rdn]) 3400 end; 3401 3402fun e_media ast = 3403 case ast of 3404 ExtendByte(unsigned,(d,m)) => 3405 let 3406 val U = BitsN.fromBit unsigned 3407 val Rd = BitsN.bits(2,0) d 3408 val Rm = BitsN.bits(2,0) m 3409 in 3410 Thumb16(BitsN.concat[BitsN.B(0xB2,8),U,BitsN.B(0x1,1),Rm,Rd]) 3411 end 3412 | ExtendHalfword(unsigned,(d,m)) => 3413 let 3414 val U = BitsN.fromBit unsigned 3415 val Rd = BitsN.bits(2,0) d 3416 val Rm = BitsN.bits(2,0) m 3417 in 3418 Thumb16(BitsN.concat[BitsN.B(0xB2,8),U,BitsN.B(0x0,1),Rm,Rd]) 3419 end 3420 | ByteReverse(d,m) => 3421 Thumb16 3422 (BitsN.concat 3423 [BitsN.B(0x2E8,10),BitsN.bits(2,0) m,BitsN.bits(2,0) d]) 3424 | ByteReversePackedHalfword(d,m) => 3425 Thumb16 3426 (BitsN.concat 3427 [BitsN.B(0x2E9,10),BitsN.bits(2,0) m,BitsN.bits(2,0) d]) 3428 | ByteReverseSignedHalfword(d,m) => 3429 Thumb16 3430 (BitsN.concat 3431 [BitsN.B(0x2EB,10),BitsN.bits(2,0) m,BitsN.bits(2,0) d]); 3432 3433fun e_hint (ast,e) = 3434 case ast of 3435 Breakpoint imm32 => 3436 Thumb16(BitsN.@@(BitsN.B(0xBE,8),BitsN.bits(7,0) imm32)) 3437 | DataMemoryBarrier option => 3438 Thumb32(BitsN.B(0xF3BF,16),BitsN.@@(BitsN.B(0x8F5,12),option)) 3439 | DataSynchronizationBarrier option => 3440 Thumb32(BitsN.B(0xF3BF,16),BitsN.@@(BitsN.B(0x8F4,12),option)) 3441 | InstructionSynchronizationBarrier option => 3442 Thumb32(BitsN.B(0xF3BF,16),BitsN.@@(BitsN.B(0x8F6,12),option)) 3443 | SendEvent () => 3444 if e = Enc_Wide 3445 then Thumb32(BitsN.B(0xF3AF,16),BitsN.B(0x8004,16)) 3446 else Thumb16(BitsN.B(0xBF40,16)) 3447 | WaitForEvent () => 3448 if e = Enc_Wide 3449 then Thumb32(BitsN.B(0xF3AF,16),BitsN.B(0x8002,16)) 3450 else Thumb16(BitsN.B(0xBF20,16)) 3451 | WaitForInterrupt () => 3452 if e = Enc_Wide 3453 then Thumb32(BitsN.B(0xF3AF,16),BitsN.B(0x8003,16)) 3454 else Thumb16(BitsN.B(0xBF30,16)) 3455 | Yield () => 3456 if e = Enc_Wide 3457 then Thumb32(BitsN.B(0xF3AF,16),BitsN.B(0x8001,16)) 3458 else Thumb16(BitsN.B(0xBF10,16)); 3459 3460fun e_system ast = 3461 case ast of 3462 ChangeProcessorState enable => 3463 Thumb16 3464 (BitsN.concat 3465 [BitsN.B(0x5B3,11),BitsN.fromBit(not enable),BitsN.B(0x2,4)]) 3466 | MoveToRegisterFromSpecial(SYSm,Rd) => 3467 Thumb32(BitsN.B(0xF3EF,16),BitsN.concat[BitsN.B(0x8,4),Rd,SYSm]) 3468 | MoveToSpecialRegister(SYSm,Rn) => 3469 Thumb32 3470 (BitsN.@@(BitsN.B(0xF38,12),Rn),BitsN.@@(BitsN.B(0x88,8),SYSm)) 3471 | SupervisorCall imm32 => 3472 Thumb16(BitsN.@@(BitsN.B(0xDF,8),BitsN.bits(7,0) imm32)); 3473 3474fun e_multiply ast = 3475 case ast of 3476 Multiply32(d,(n,m)) => 3477 (if d = m 3478 then let 3479 val Rn = BitsN.bits(2,0) n 3480 val Rdm = BitsN.bits(2,0) d 3481 in 3482 Thumb16(BitsN.concat[BitsN.B(0x10D,10),Rn,Rdm]) 3483 end 3484 else BadCode "Multiply32"); 3485 3486fun e_load ast = 3487 case ast of 3488 LoadWord(t,(n,immediate_form imm32)) => 3489 (if n = (BitsN.B(0xD,4)) 3490 then Thumb16 3491 (BitsN.concat 3492 [BitsN.B(0x13,5),BitsN.bits(2,0) t, 3493 BitsN.bits(9,2) imm32]) 3494 else Thumb16 3495 (BitsN.concat 3496 [BitsN.B(0xD,5),BitsN.bits(6,2) imm32,BitsN.bits(2,0) n, 3497 BitsN.bits(2,0) t])) 3498 | LoadWord(t,(n,register_form m)) => 3499 Thumb16 3500 (BitsN.concat 3501 [BitsN.B(0x2C,7),BitsN.bits(2,0) m,BitsN.bits(2,0) n, 3502 BitsN.bits(2,0) t]) 3503 | LoadLiteral(t,imm32) => 3504 Thumb16 3505 (BitsN.concat 3506 [BitsN.B(0x9,5),BitsN.bits(2,0) t,BitsN.bits(9,2) imm32]) 3507 | LoadByte(unsigned,(t,(n,immediate_form imm32))) => 3508 Thumb16 3509 (BitsN.concat 3510 [BitsN.B(0xF,5),BitsN.bits(4,0) imm32,BitsN.bits(2,0) n, 3511 BitsN.bits(2,0) t]) 3512 | LoadByte(unsigned,(t,(n,register_form m))) => 3513 let 3514 val Rm = BitsN.bits(2,0) m 3515 val Rn = BitsN.bits(2,0) n 3516 val Rt = BitsN.bits(2,0) t 3517 val U = BitsN.fromBit unsigned 3518 val S = BitsN.~ U 3519 in 3520 Thumb16(BitsN.concat[BitsN.B(0x5,4),U,BitsN.B(0x1,1),S,Rm,Rn,Rt]) 3521 end 3522 | LoadHalf(unsigned,(t,(n,immediate_form imm32))) => 3523 Thumb16 3524 (BitsN.concat 3525 [BitsN.B(0x11,5),BitsN.bits(5,1) imm32,BitsN.bits(2,0) n, 3526 BitsN.bits(2,0) t]) 3527 | LoadHalf(unsigned,(t,(n,register_form m))) => 3528 Thumb16 3529 (BitsN.concat 3530 [BitsN.B(0xB,5),BitsN.fromBit(not unsigned),BitsN.B(0x1,1), 3531 BitsN.bits(2,0) m,BitsN.bits(2,0) n,BitsN.bits(2,0) t]) 3532 | LoadMultiple(wback,(n,registers)) => 3533 (if n = (BitsN.B(0xD,4)) 3534 then Thumb16(BitsN.@@(BitsN.B(0x5E,7),registers)) 3535 else Thumb16 3536 (BitsN.concat 3537 [BitsN.B(0x19,5),BitsN.bits(2,0) n, 3538 BitsN.bits(7,0) registers])); 3539 3540fun e_store ast = 3541 case ast of 3542 StoreWord(t,(n,immediate_form imm32)) => 3543 (if n = (BitsN.B(0xD,4)) 3544 then Thumb16 3545 (BitsN.concat 3546 [BitsN.B(0x12,5),BitsN.bits(2,0) t, 3547 BitsN.bits(9,2) imm32]) 3548 else Thumb16 3549 (BitsN.concat 3550 [BitsN.B(0xC,5),BitsN.bits(6,2) imm32,BitsN.bits(2,0) n, 3551 BitsN.bits(2,0) t])) 3552 | StoreWord(t,(n,register_form m)) => 3553 Thumb16 3554 (BitsN.concat 3555 [BitsN.B(0x28,7),BitsN.bits(2,0) m,BitsN.bits(2,0) n, 3556 BitsN.bits(2,0) t]) 3557 | StoreByte(t,(n,immediate_form imm32)) => 3558 Thumb16 3559 (BitsN.concat 3560 [BitsN.B(0xE,5),BitsN.bits(4,0) imm32,BitsN.bits(2,0) n, 3561 BitsN.bits(2,0) t]) 3562 | StoreByte(t,(n,register_form m)) => 3563 Thumb16 3564 (BitsN.concat 3565 [BitsN.B(0x2A,7),BitsN.bits(2,0) m,BitsN.bits(2,0) n, 3566 BitsN.bits(2,0) t]) 3567 | StoreHalf(t,(n,immediate_form imm32)) => 3568 Thumb16 3569 (BitsN.concat 3570 [BitsN.B(0x10,5),BitsN.bits(5,1) imm32,BitsN.bits(2,0) n, 3571 BitsN.bits(2,0) t]) 3572 | StoreHalf(t,(n,register_form m)) => 3573 Thumb16 3574 (BitsN.concat 3575 [BitsN.B(0x29,7),BitsN.bits(2,0) m,BitsN.bits(2,0) n, 3576 BitsN.bits(2,0) t]) 3577 | Push registers => Thumb16(BitsN.@@(BitsN.B(0x5A,7),registers)) 3578 | StoreMultiple(n,registers) => 3579 Thumb16(BitsN.concat[BitsN.B(0x18,5),BitsN.bits(2,0) n,registers]); 3580 3581fun instructionEncode (c,(ast,e)) = 3582 case ast of 3583 Branch b => e_branch(c,(b,e)) 3584 | Data d => e_data d 3585 | Load l => e_load l 3586 | Store s => e_store s 3587 | Multiply m => e_multiply m 3588 | Media m => e_media m 3589 | System s => e_system s 3590 | Hint h => e_hint(h,e) 3591 | Undefined imm32 => 3592 (if (not(e = Enc_Wide)) andalso 3593 ((BitsN.bits(31,8) imm32) = (BitsN.B(0x0,24))) 3594 then let 3595 val imm8 = BitsN.bits(7,0) imm32 3596 in 3597 Thumb16(BitsN.@@(BitsN.B(0xDE,8),imm8)) 3598 end 3599 else if not(e = Enc_Narrow) 3600 then let 3601 val imm4 = BitsN.bits(15,12) imm32 3602 val imm12 = BitsN.bits(11,0) imm32 3603 in 3604 Thumb32 3605 (BitsN.@@(BitsN.B(0xF7F,12),imm4), 3606 BitsN.@@(BitsN.B(0xA,4),imm12)) 3607 end 3608 else BadCode "Undefined") 3609 | NoOperation () => 3610 if e = Enc_Wide 3611 then Thumb32(BitsN.B(0xF3AF,16),BitsN.B(0x8000,16)) 3612 else Thumb16(BitsN.B(0xBF00,16)); 3613 3614fun SetPassCondition c = 3615 case c of 3616 BitsN.B(0x0,_) => PSR := (PSR_Z_rupd((!PSR),true)) 3617 | BitsN.B(0x1,_) => PSR := (PSR_Z_rupd((!PSR),false)) 3618 | BitsN.B(0x2,_) => PSR := (PSR_C_rupd((!PSR),true)) 3619 | BitsN.B(0x3,_) => PSR := (PSR_C_rupd((!PSR),false)) 3620 | BitsN.B(0x4,_) => PSR := (PSR_N_rupd((!PSR),true)) 3621 | BitsN.B(0x5,_) => PSR := (PSR_N_rupd((!PSR),false)) 3622 | BitsN.B(0x6,_) => PSR := (PSR_V_rupd((!PSR),true)) 3623 | BitsN.B(0x7,_) => PSR := (PSR_V_rupd((!PSR),false)) 3624 | BitsN.B(0x8,_) => 3625 ( PSR := (PSR_C_rupd((!PSR),true)) 3626 ; PSR := (PSR_Z_rupd((!PSR),false)) 3627 ) 3628 | BitsN.B(0x9,_) => PSR := (PSR_C_rupd((!PSR),false)) 3629 | BitsN.B(0xA,_) => 3630 ( PSR := (PSR_N_rupd((!PSR),false)) 3631 ; PSR := (PSR_V_rupd((!PSR),false)) 3632 ) 3633 | BitsN.B(0xB,_) => 3634 ( PSR := (PSR_N_rupd((!PSR),false)) 3635 ; PSR := (PSR_V_rupd((!PSR),true)) 3636 ) 3637 | BitsN.B(0xC,_) => 3638 ( PSR := (PSR_N_rupd((!PSR),false)) 3639 ; PSR := (PSR_V_rupd((!PSR),false)) 3640 ; PSR := (PSR_Z_rupd((!PSR),false)) 3641 ) 3642 | BitsN.B(0xD,_) => 3643 ( PSR := (PSR_N_rupd((!PSR),false)) 3644 ; PSR := (PSR_V_rupd((!PSR),true)) 3645 ) 3646 | _ => (); 3647 3648fun Encode (c,(ast,enc)) = 3649 ( SetPassCondition c 3650 ; case instructionEncode(c,(ast,enc)) of 3651 Thumb16 a => 3652 (if (not(enc = Enc_Wide)) andalso ((Decode(Thumb a)) = ast) 3653 then Thumb16 a 3654 else BadCode "Failed to encode") 3655 | Thumb32 a => 3656 (if (not(enc = Enc_Narrow)) andalso ((Decode(Thumb2 a)) = ast) 3657 then Thumb32 a 3658 else BadCode "Failed to encode") 3659 | mmc => mmc 3660 ); 3661 3662val al = (BitsN.B(0xE,4),"") 3663 3664fun stripSpaces s = 3665 L3.fst 3666 (L3.splitr 3667 (fn c => Char.isSpace c,L3.snd(L3.splitl(fn c => Char.isSpace c,s)))); 3668 3669fun p_number s = 3670 case String.explode(stripSpaces s) of 3671 #"0" :: (#"b" :: t) => Nat.fromBinString(String.implode t) 3672 | #"0" :: (#"x" :: t) => Nat.fromHexString(String.implode t) 3673 | _ => Nat.fromString s; 3674 3675fun p_signed_number (b,s) = 3676 case p_number s of Option.SOME n => Option.SOME(b,n) | NONE => NONE; 3677 3678fun p_encode_immediate N s = 3679 case p_number s of 3680 Option.SOME n => 3681 let 3682 val r = BitsN.fromNat(n,N) 3683 in 3684 Option.SOME(n = (BitsN.toNat r),r) 3685 end 3686 | NONE => NONE; 3687 3688fun p_encode_signed_immediate N x = 3689 case p_signed_number x of 3690 Option.SOME(sub,n) => 3691 let 3692 val r = BitsN.fromNat(n,N) 3693 in 3694 Option.SOME(sub,(n = (BitsN.toNat r),r)) 3695 end 3696 | NONE => NONE; 3697 3698fun p_encode_signed_offset N x = 3699 case p_signed_number x of 3700 Option.SOME(sub,n) => 3701 let 3702 val i = 3703 IntInf.-(if sub then IntInf.~(Nat.toInt n) else Nat.toInt n,4) 3704 val r = BitsN.fromInt(i,N) 3705 in 3706 Option.SOME(i = (BitsN.toInt r),r) 3707 end 3708 | NONE => NONE; 3709 3710fun p_unbounded_immediate s = 3711 case String.explode(stripSpaces s) of 3712 #"#" :: t => p_number(String.implode t) 3713 | _ => NONE; 3714 3715fun p_immediate N s = 3716 case String.explode(stripSpaces s) of 3717 #"#" :: t => p_encode_immediate N (String.implode t) 3718 | _ => NONE; 3719 3720fun p_immediate_number N s = 3721 case String.explode(stripSpaces s) of 3722 #"#" :: t => p_encode_immediate N (String.implode t) 3723 | t => p_encode_immediate N (String.implode t); 3724 3725fun p_signed_immediate N s = 3726 case String.explode(stripSpaces s) of 3727 #"#" :: (#"-" :: t) => 3728 p_encode_signed_immediate N (true,String.implode t) 3729 | #"#" :: (#"+" :: t) => 3730 p_encode_signed_immediate N (false,String.implode t) 3731 | #"#" :: t => p_encode_signed_immediate N (false,String.implode t) 3732 | _ => NONE; 3733 3734fun p_signed_offset N s = 3735 case String.explode(stripSpaces s) of 3736 #"+" :: (#"#" :: t) => 3737 (case p_encode_signed_immediate N (false,String.implode t) of 3738 Option.SOME(false,(true,n)) => 3739 Option.SOME 3740 (BitsN.<=+(BitsN.BV(0x4,N),n),BitsN.-(n,BitsN.BV(0x4,N))) 3741 | Option.SOME(_,(_,n)) => Option.SOME(false,n) 3742 | NONE => NONE) 3743 | _ => NONE; 3744 3745fun p_offset N s = 3746 case String.explode(stripSpaces s) of 3747 #"-" :: (#"#" :: t) => 3748 p_encode_signed_offset N (true,String.implode t) 3749 | #"+" :: (#"#" :: t) => 3750 p_encode_signed_offset N (false,String.implode t) 3751 | _ => NONE; 3752 3753fun p_label s = 3754 case L3.uncurry String.tokens (fn c => Char.isSpace c,s) of 3755 [t] => 3756 let 3757 val (l,r) = 3758 L3.splitl 3759 (fn c => (Char.isAlphaNum c) orelse (Set.mem(c,[#"_",#"."])), 3760 t) 3761 in 3762 if (r = "") andalso 3763 ((not(l = "")) andalso (not(Char.isDigit(L3.strHd l)))) 3764 then Option.SOME l 3765 else NONE 3766 end 3767 | _ => NONE; 3768 3769fun p_cond s = 3770 case s of 3771 "eq" => Option.SOME(BitsN.B(0x0,4)) 3772 | "ne" => Option.SOME(BitsN.B(0x1,4)) 3773 | "cs" => Option.SOME(BitsN.B(0x2,4)) 3774 | "hs" => Option.SOME(BitsN.B(0x2,4)) 3775 | "cc" => Option.SOME(BitsN.B(0x3,4)) 3776 | "lo" => Option.SOME(BitsN.B(0x3,4)) 3777 | "mi" => Option.SOME(BitsN.B(0x4,4)) 3778 | "pl" => Option.SOME(BitsN.B(0x5,4)) 3779 | "vs" => Option.SOME(BitsN.B(0x6,4)) 3780 | "vc" => Option.SOME(BitsN.B(0x7,4)) 3781 | "hi" => Option.SOME(BitsN.B(0x8,4)) 3782 | "ls" => Option.SOME(BitsN.B(0x9,4)) 3783 | "ge" => Option.SOME(BitsN.B(0xA,4)) 3784 | "lt" => Option.SOME(BitsN.B(0xB,4)) 3785 | "gt" => Option.SOME(BitsN.B(0xC,4)) 3786 | "le" => Option.SOME(BitsN.B(0xD,4)) 3787 | "al" => Option.SOME(BitsN.B(0xE,4)) 3788 | "" => Option.SOME(BitsN.B(0xE,4)) 3789 | _ => NONE; 3790 3791fun p_suffix s = 3792 case L3.uncurry String.fields (fn c => c = #".",s) of 3793 [cond,s] => 3794 (case (p_cond cond,Set.mem(s,["w","n"])) of 3795 (Option.SOME c,true) => Option.SOME(c,s) 3796 | _ => NONE) 3797 | [cond] => 3798 (case p_cond cond of 3799 Option.SOME c => Option.SOME(c,"") 3800 | NONE => NONE) 3801 | _ => NONE; 3802 3803fun p_al_suffix s = 3804 case p_suffix s of 3805 Option.SOME(BitsN.B(0xE,_),c) => Option.SOME(BitsN.B(0xE,4),c) 3806 | _ => NONE; 3807 3808fun p_special_register s = 3809 case stripSpaces s of 3810 "apsr" => Option.SOME(BitsN.B(0x0,8)) 3811 | "iapsr" => Option.SOME(BitsN.B(0x1,8)) 3812 | "eapsr" => Option.SOME(BitsN.B(0x2,8)) 3813 | "xpsr" => Option.SOME(BitsN.B(0x3,8)) 3814 | "ipsr" => Option.SOME(BitsN.B(0x5,8)) 3815 | "epsr" => Option.SOME(BitsN.B(0x6,8)) 3816 | "iepsr" => Option.SOME(BitsN.B(0x7,8)) 3817 | "msp" => Option.SOME(BitsN.B(0x8,8)) 3818 | "psp" => Option.SOME(BitsN.B(0x9,8)) 3819 | "primask" => Option.SOME(BitsN.B(0x10,8)) 3820 | "control" => Option.SOME(BitsN.B(0x14,8)) 3821 | n => 3822 (case p_encode_immediate 8 n of 3823 Option.SOME(true,imm8) => Option.SOME imm8 3824 | _ => NONE); 3825 3826fun p_register s = 3827 case stripSpaces s of 3828 "r0" => Option.SOME(BitsN.B(0x0,4)) 3829 | "r1" => Option.SOME(BitsN.B(0x1,4)) 3830 | "r2" => Option.SOME(BitsN.B(0x2,4)) 3831 | "r3" => Option.SOME(BitsN.B(0x3,4)) 3832 | "r4" => Option.SOME(BitsN.B(0x4,4)) 3833 | "r5" => Option.SOME(BitsN.B(0x5,4)) 3834 | "r6" => Option.SOME(BitsN.B(0x6,4)) 3835 | "r7" => Option.SOME(BitsN.B(0x7,4)) 3836 | "r8" => Option.SOME(BitsN.B(0x8,4)) 3837 | "r9" => Option.SOME(BitsN.B(0x9,4)) 3838 | "r10" => Option.SOME(BitsN.B(0xA,4)) 3839 | "r11" => Option.SOME(BitsN.B(0xB,4)) 3840 | "r12" => Option.SOME(BitsN.B(0xC,4)) 3841 | "r13" => Option.SOME(BitsN.B(0xD,4)) 3842 | "r14" => Option.SOME(BitsN.B(0xE,4)) 3843 | "r15" => Option.SOME(BitsN.B(0xF,4)) 3844 | "sp" => Option.SOME(BitsN.B(0xD,4)) 3845 | "lr" => Option.SOME(BitsN.B(0xE,4)) 3846 | "pc" => Option.SOME(BitsN.B(0xF,4)) 3847 | _ => NONE; 3848 3849fun p_register1 l = case l of [r1] => p_register r1 | _ => NONE; 3850 3851fun p_register2 l = 3852 case l of 3853 [r1,r2] => 3854 (case (p_register r1,p_register r2) of 3855 (Option.SOME v1,Option.SOME v2) => Option.SOME(v1,v2) 3856 | _ => NONE) 3857 | _ => NONE; 3858 3859fun p_register3 l = 3860 case l of 3861 [r1,r2,r3] => 3862 (case (p_register r1,(p_register r2,p_register r3)) of 3863 (Option.SOME v1,(Option.SOME v2,Option.SOME v3)) => 3864 Option.SOME(v1,(v2,v3)) 3865 | _ => NONE) 3866 | _ => NONE; 3867 3868fun p_shift_amount (typ,(h,s)) = 3869 if Char.isSpace h 3870 then case p_unbounded_immediate s of 3871 Option.SOME n => 3872 (if (Nat.<(n,32)) orelse 3873 ((n = 32) andalso (Set.mem(typ,[SRType_LSR,SRType_ASR]))) 3874 then ("",(typ,NAT n)) 3875 else ("shift amount too large",(SRType_LSL,NAT 0))) 3876 | NONE => 3877 (case p_register s of 3878 Option.SOME rs => ("",(typ,REGISTER rs)) 3879 | NONE => ("syntax error",(SRType_LSL,NAT 0))) 3880 else ("syntax error",(SRType_LSL,NAT 0)); 3881 3882fun p_shift_imm_or_reg s = 3883 case String.explode(stripSpaces s) of 3884 #"l" :: (#"s" :: (#"l" :: (h :: t))) => 3885 p_shift_amount(SRType_LSL,(h,String.implode t)) 3886 | #"l" :: (#"s" :: (#"r" :: (h :: t))) => 3887 p_shift_amount(SRType_LSR,(h,String.implode t)) 3888 | #"a" :: (#"s" :: (#"r" :: (h :: t))) => 3889 p_shift_amount(SRType_ASR,(h,String.implode t)) 3890 | #"r" :: (#"o" :: (#"r" :: (h :: t))) => 3891 p_shift_amount(SRType_ROR,(h,String.implode t)) 3892 | _ => ("syntax error",(SRType_LSL,NAT 0)); 3893 3894fun p_arith_logic_full (c,(opc,(setflags,l))) = 3895 case (p_al_suffix c,l) of 3896 (Option.SOME c,[r1,r2,x]) => 3897 (case p_register2[r1,r2] of 3898 Option.SOME(rd,rn) => 3899 (case p_register x of 3900 Option.SOME rm => 3901 OK(c,Data(Register(opc,(setflags,(rd,(rn,rm)))))) 3902 | NONE => 3903 (case p_immediate 32 x of 3904 Option.SOME(true,imm32) => 3905 OK(c, 3906 Data 3907 (ArithLogicImmediate 3908 (opc,(setflags,(rd,(rn,imm32)))))) 3909 | Option.SOME _ => FAIL "immediate too large" 3910 | NONE => FAIL "syntax error")) 3911 | NONE => FAIL "syntax error") 3912 | _ => FAIL "syntax error"; 3913 3914fun p_arith_logic (c,(opc,(setflags,l))) = 3915 case l of 3916 h :: _ => 3917 (case p_arith_logic_full(c,(opc,(setflags,l))) of 3918 FAIL "syntax error" => 3919 p_arith_logic_full(c,(opc,(setflags,h :: l))) 3920 | r => r) 3921 | [] => FAIL "syntax error"; 3922 3923fun p_test_compare (c,(opc,l)) = 3924 case (p_al_suffix c,l) of 3925 (Option.SOME c,[r1,x]) => 3926 (case p_register r1 of 3927 Option.SOME rn => 3928 (case p_register x of 3929 Option.SOME rm => 3930 OK(c,Data(TestCompareRegister(opc,(rn,rm)))) 3931 | NONE => 3932 (case (opc,p_immediate 32 x) of 3933 (BitsN.B(0x2,_),Option.SOME(true,imm32)) => 3934 OK(c,Data(CompareImmediate(rn,imm32))) 3935 | (BitsN.B(0x2,_),Option.SOME _) => 3936 FAIL "immediate too large" 3937 | _ => FAIL "syntax error")) 3938 | NONE => FAIL "syntax error") 3939 | _ => FAIL "syntax error"; 3940 3941fun p_mov_mvn (c,(negate,(setflags,l))) = 3942 case (p_al_suffix c,l) of 3943 (Option.SOME c,[r1,x]) => 3944 (case p_register r1 of 3945 Option.SOME rd => 3946 (case p_register x of 3947 Option.SOME rm => 3948 OK(c, 3949 Data 3950 (ShiftImmediate 3951 (negate,(setflags,(rd,(rm,(SRType_LSL,0))))))) 3952 | NONE => 3953 (case (negate,p_immediate 32 x) of 3954 (false,Option.SOME(true,imm32)) => 3955 OK(c,Data(Move(rd,imm32))) 3956 | (false,Option.SOME _) => FAIL "immediate too large" 3957 | _ => FAIL "syntax error")) 3958 | NONE => FAIL "syntax error") 3959 | (Option.SOME c,[r1,r2,sh]) => 3960 (case (negate,(setflags,(p_register2[r1,r2],p_shift_imm_or_reg sh))) of 3961 (false,(true,(Option.SOME(rd,rm),("",(typ,NAT n))))) => 3962 OK(c,Data(ShiftImmediate(negate,(setflags,(rd,(rm,(typ,n))))))) 3963 | (false,(true,(Option.SOME(rd,rm),("",(typ,REGISTER rs))))) => 3964 OK(c,Data(ShiftRegister(rd,(rm,(typ,rs))))) 3965 | (false,(true,(Option.SOME _,(err,_)))) => FAIL err 3966 | _ => FAIL "syntax error") 3967 | _ => FAIL "syntax error"; 3968 3969fun p_shift_full (c,(typ,l)) = 3970 case (p_al_suffix c,l) of 3971 (Option.SOME c,[r1,r2,s]) => 3972 (case p_register2[r1,r2] of 3973 Option.SOME(rd,rn) => 3974 (case p_register s of 3975 Option.SOME rm => 3976 OK(c,Data(ShiftRegister(rd,(rn,(typ,rm))))) 3977 | NONE => 3978 (case p_unbounded_immediate s of 3979 Option.SOME n => 3980 (if (Nat.<(n,32)) orelse 3981 ((n = 32) andalso 3982 (Set.mem(typ,[SRType_LSR,SRType_ASR]))) 3983 then OK(c, 3984 Data 3985 (ShiftImmediate 3986 (false,(true,(rd,(rn,(typ,n))))))) 3987 else FAIL "shift amount too large") 3988 | NONE => FAIL "syntax error")) 3989 | NONE => FAIL "syntax error") 3990 | _ => FAIL "syntax error"; 3991 3992fun p_shift (c,(typ,l)) = 3993 case l of 3994 h :: _ => 3995 (case p_shift_full(c,(typ,l)) of 3996 FAIL "syntax error" => p_shift_full(c,(typ,h :: l)) 3997 | r => r) 3998 | [] => FAIL "syntax error"; 3999 4000fun p_adr (c,l) = 4001 case (p_al_suffix c,l) of 4002 (Option.SOME c,[r,n]) => 4003 (case p_register r of 4004 Option.SOME d => 4005 (case p_signed_offset 10 n of 4006 Option.SOME(true,imm10) => 4007 OK(c, 4008 Data 4009 (ArithLogicImmediate 4010 (BitsN.B(0x4,4), 4011 (false, 4012 (d, 4013 (BitsN.B(0xF,4), 4014 BitsN.fromNat(BitsN.toNat imm10,32))))))) 4015 | Option.SOME _ => FAIL "bad offset" 4016 | NONE => 4017 (case p_label n of 4018 Option.SOME s => 4019 PENDING 4020 (s, 4021 (c, 4022 Data 4023 (ArithLogicImmediate 4024 (BitsN.B(0x4,4), 4025 (false, 4026 (d,(BitsN.B(0xF,4),BitsN.B(0x0,32)))))))) 4027 | NONE => FAIL "syntax error")) 4028 | NONE => FAIL "syntax error") 4029 | _ => FAIL "syntax error"; 4030 4031fun p_bx (c,l) = 4032 case (p_al_suffix c,p_register1 l) of 4033 (Option.SOME c,Option.SOME rm) => OK(c,Branch(BranchExchange rm)) 4034 | _ => FAIL "syntax error"; 4035 4036fun p_bl (c,l) = 4037 case (p_al_suffix c,l) of 4038 (Option.SOME c,[a]) => 4039 (case p_offset 32 a of 4040 Option.SOME(true,offset) => 4041 OK(c,Branch(BranchLinkImmediate offset)) 4042 | Option.SOME(false,_) => FAIL "offset too large" 4043 | NONE => 4044 (case p_label a of 4045 Option.SOME label => 4046 PENDING 4047 (label,(c,Branch(BranchLinkImmediate(BitsN.B(0x0,32))))) 4048 | NONE => FAIL "syntax error")) 4049 | _ => FAIL "syntax error"; 4050 4051fun p_b (c,l) = 4052 case (p_suffix c,l) of 4053 (Option.SOME c,[a]) => 4054 (case p_offset 32 a of 4055 Option.SOME(true,offset) => OK(c,Branch(BranchTarget offset)) 4056 | Option.SOME(false,_) => FAIL "offset too large" 4057 | NONE => 4058 (case p_label a of 4059 Option.SOME label => 4060 PENDING(label,(c,Branch(BranchTarget(BitsN.B(0x0,32))))) 4061 | NONE => FAIL "syntax error")) 4062 | _ => FAIL "syntax error"; 4063 4064fun p_blx (c,l) = 4065 case (p_al_suffix c,p_register1 l) of 4066 (Option.SOME c,Option.SOME rm) => 4067 OK(c,Branch(BranchLinkExchangeRegister rm)) 4068 | _ => FAIL "syntax error"; 4069 4070fun p_mul (c,l) = 4071 case (p_al_suffix c,l) of 4072 (Option.SOME c,[_,_,_]) => 4073 (case p_register3 l of 4074 Option.SOME(rd,(rn,rm)) => 4075 OK(c,Multiply(Multiply32(rd,(rn,rm)))) 4076 | NONE => FAIL "syntax error") 4077 | (Option.SOME c,[_,_]) => 4078 (case p_register2 l of 4079 Option.SOME(rn,rm) => OK(c,Multiply(Multiply32(rn,(rm,rn)))) 4080 | NONE => FAIL "syntax error") 4081 | _ => FAIL "syntax error"; 4082 4083fun p_sxtb_etc (c,(half,(unsigned,l))) = 4084 case (p_al_suffix c,l) of 4085 (Option.SOME c,[r1,r2]) => 4086 (case p_register2[r1,r2] of 4087 Option.SOME(rd,rm) => 4088 let 4089 val a = (unsigned,(rd,rm)) 4090 in 4091 OK(c,Media(if half then ExtendHalfword a else ExtendByte a)) 4092 end 4093 | NONE => FAIL "syntax error") 4094 | _ => FAIL "syntax error"; 4095 4096fun p_rev (c,l) = 4097 case (p_al_suffix c,p_register2 l) of 4098 (Option.SOME c,Option.SOME(rd,rm)) => OK(c,Media(ByteReverse(rd,rm))) 4099 | _ => FAIL "syntax error"; 4100 4101fun p_rev16 (c,l) = 4102 case (p_al_suffix c,p_register2 l) of 4103 (Option.SOME c,Option.SOME(rd,rm)) => 4104 OK(c,Media(ByteReversePackedHalfword(rd,rm))) 4105 | _ => FAIL "syntax error"; 4106 4107fun p_revsh (c,l) = 4108 case (p_al_suffix c,p_register2 l) of 4109 (Option.SOME c,Option.SOME(rd,rm)) => 4110 OK(c,Media(ByteReverseSignedHalfword(rd,rm))) 4111 | _ => FAIL "syntax error"; 4112 4113fun closingRegList s = 4114 case L3.splitr(fn c => c = #"}",stripSpaces s) of 4115 (l,"}") => Option.SOME l 4116 | _ => NONE; 4117 4118fun p_reg_list (w,s) = 4119 case p_register s of 4120 Option.SOME r => 4121 let 4122 val n = BitsN.toNat r 4123 in 4124 if BitsN.bit(w,n) 4125 then NONE 4126 else Option.SOME(BitsN.||(w,BitsN.<<(BitsN.B(0x1,16),n))) 4127 end 4128 | NONE => 4129 (case L3.uncurry String.fields (fn c => c = #"-",s) of 4130 [r1,r2] => 4131 (case p_register2[r1,r2] of 4132 Option.SOME(rlo,rhi) => 4133 let 4134 val lo = BitsN.toNat rlo 4135 val hi = BitsN.toNat rhi 4136 val mask = 4137 BitsN.- 4138 (BitsN.<<(BitsN.B(0x1,16),Nat.+(hi,1)), 4139 BitsN.<<(BitsN.B(0x1,16),lo)) 4140 in 4141 if (Nat.<(lo,hi)) andalso 4142 ((BitsN.&&(w,mask)) = (BitsN.B(0x0,16))) 4143 then Option.SOME(BitsN.||(w,mask)) 4144 else NONE 4145 end 4146 | NONE => NONE) 4147 | _ => NONE); 4148 4149fun p_registers_loop (w,l) = 4150 case l of 4151 [s] => 4152 (case closingRegList s of 4153 Option.SOME h => 4154 (case p_reg_list(w,h) of 4155 Option.SOME r => Option.SOME r 4156 | NONE => NONE) 4157 | NONE => NONE) 4158 | h :: t => 4159 (case p_reg_list(w,h) of 4160 Option.SOME r => p_registers_loop(r,t) 4161 | NONE => NONE) 4162 | [] => NONE; 4163 4164fun p_registers l = 4165 case l of 4166 h :: t => 4167 (case String.explode(stripSpaces h) of 4168 #"{" :: r => 4169 let 4170 val r = stripSpaces(String.implode r) 4171 in 4172 p_registers_loop 4173 (BitsN.B(0x0,16),if r = "" then t else r :: t) 4174 end 4175 | _ => NONE) 4176 | _ => NONE; 4177 4178fun closingAddress l = 4179 case l of 4180 [s] => 4181 (case L3.splitr(fn c => c = #"]",stripSpaces s) of 4182 (l,"]") => Option.SOME l 4183 | _ => NONE) 4184 | _ => NONE; 4185 4186fun p_address_mode l = 4187 case l of 4188 h1 :: t1 => 4189 (case String.explode(stripSpaces h1) of 4190 #"[" :: r1 => 4191 let 4192 val r1 = String.implode r1 4193 in 4194 case p_register r1 of 4195 Option.SOME rn => 4196 (case closingAddress t1 of 4197 Option.SOME offset => 4198 (case p_signed_immediate 32 offset of 4199 Option.SOME(false,(true,imm32)) => 4200 ("",Option.SOME(rn,immediate_form imm32)) 4201 | Option.SOME(true,_) => 4202 ("negative offset",NONE) 4203 | Option.SOME(_,(false,_)) => 4204 ("immediate too large",NONE) 4205 | NONE => 4206 (case p_register offset of 4207 Option.SOME rm => 4208 ("",Option.SOME(rn,register_form rm)) 4209 | NONE => ("syntax error",NONE))) 4210 | NONE => ("syntax error",NONE)) 4211 | NONE => 4212 (case closingAddress(r1 :: t1) of 4213 Option.SOME r2 => 4214 (case p_register r2 of 4215 Option.SOME rn => 4216 ("", 4217 Option.SOME 4218 (rn,immediate_form(BitsN.B(0x0,32)))) 4219 | NONE => ("syntax error",NONE)) 4220 | _ => ("syntax error",NONE)) 4221 end 4222 | _ => 4223 (case (p_signed_offset 32 h1,t1) of 4224 (Option.SOME(true,imm32),[]) => 4225 ("",Option.SOME(BitsN.B(0xF,4),immediate_form imm32)) 4226 | (Option.SOME(false,_),[]) => ("bad offset",NONE) 4227 | _ => ("syntax error",NONE))) 4228 | _ => ("syntax error",NONE); 4229 4230fun pick_ldr_str (opc,(rt,(rn,offset))) = 4231 let 4232 val r = (rt,(rn,offset)) 4233 in 4234 case opc of 4235 0 => 4236 (case (rn,offset) of 4237 (BitsN.B(0xF,_),immediate_form imm32) => 4238 Load(LoadLiteral(rt,imm32)) 4239 | _ => Load(LoadWord r)) 4240 | 1 => Store(StoreByte r) 4241 | 2 => Store(StoreHalf r) 4242 | _ => Store(StoreWord r) 4243 end; 4244 4245fun p_ldr_str (c,(opc,l)) = 4246 case (p_al_suffix c,l) of 4247 (Option.SOME c,h :: t) => 4248 (case p_register h of 4249 Option.SOME rt => 4250 (case p_address_mode t of 4251 ("",Option.SOME(rn,offset)) => 4252 OK(c,pick_ldr_str(opc,(rt,(rn,offset)))) 4253 | (err,_) => 4254 (case t of 4255 [l] => 4256 (case p_label l of 4257 Option.SOME s => 4258 PENDING 4259 (s, 4260 (c, 4261 pick_ldr_str 4262 (opc, 4263 (rt, 4264 (BitsN.B(0xF,4), 4265 immediate_form(BitsN.B(0x0,32))))))) 4266 | NONE => FAIL err) 4267 | _ => FAIL err)) 4268 | NONE => FAIL "syntax error") 4269 | _ => FAIL "syntax error"; 4270 4271fun p_ldrb_ldrh (c,(unsigned,(byte,l))) = 4272 case (p_al_suffix c,l) of 4273 (Option.SOME c,h :: t) => 4274 (case p_register h of 4275 Option.SOME rt => 4276 (case p_address_mode t of 4277 ("",Option.SOME(rn,offset)) => 4278 let 4279 val r = (unsigned,(rt,(rn,offset))) 4280 in 4281 OK(c,Load(if byte then LoadByte r else LoadHalf r)) 4282 end 4283 | (err,_) => 4284 (case t of 4285 [l] => 4286 (case p_label l of 4287 Option.SOME s => 4288 let 4289 val r = 4290 (unsigned, 4291 (rt, 4292 (BitsN.B(0xF,4), 4293 immediate_form(BitsN.B(0x0,32))))) 4294 val a = 4295 if byte then LoadByte r else LoadHalf r 4296 in 4297 PENDING(s,(c,Load a)) 4298 end 4299 | NONE => FAIL err) 4300 | _ => FAIL err)) 4301 | NONE => FAIL "syntax error") 4302 | _ => FAIL "syntax error"; 4303 4304fun p_pop_push (c,(pop,l)) = 4305 case (p_al_suffix c,p_registers l) of 4306 (Option.SOME c,Option.SOME w) => 4307 (if pop 4308 then if (BitsN.&&(w,BitsN.B(0x7F00,16))) = (BitsN.B(0x0,16)) 4309 then OK(c, 4310 Load 4311 (LoadMultiple 4312 (true, 4313 (BitsN.B(0xD,4), 4314 BitsN.@@ 4315 (BitsN.bits(15,15) w,BitsN.bits(7,0) w))))) 4316 else FAIL "bad register list" 4317 else if (BitsN.&&(w,BitsN.B(0xBF00,16))) = (BitsN.B(0x0,16)) 4318 then OK(c, 4319 Store 4320 (Push(BitsN.@@(BitsN.bits(14,14) w,BitsN.bits(7,0) w)))) 4321 else FAIL "bad register list") 4322 | (NONE,_) => FAIL "syntax error" 4323 | _ => FAIL "bad register list"; 4324 4325fun p_ldm_stm (c,(load,l)) = 4326 case (p_al_suffix c,l) of 4327 (Option.SOME c,h :: t) => 4328 let 4329 val (r,wb) = L3.splitr(fn c => c = #"!",stripSpaces h) 4330 in 4331 case (p_register r,(p_registers t,Set.mem(wb,["","!"]))) of 4332 (Option.SOME rn,(Option.SOME w,true)) => 4333 (if (BitsN.bits(15,8) w) = (BitsN.B(0x0,8)) 4334 then let 4335 val wback = wb = "!" 4336 in 4337 if load 4338 then OK(c, 4339 Load 4340 (LoadMultiple 4341 (wback,(rn,BitsN.bits(8,0) w)))) 4342 else if wback 4343 then if (rn = (BitsN.B(0xD,4))) andalso 4344 ((BitsN.&&(w,BitsN.B(0xBF00,16))) = 4345 (BitsN.B(0x0,16))) 4346 then OK(c, 4347 Store 4348 (Push 4349 (BitsN.@@ 4350 (BitsN.bits(14,14) w, 4351 BitsN.bits(7,0) w)))) 4352 else OK(c, 4353 Store 4354 (StoreMultiple 4355 (rn,BitsN.bits(7,0) w))) 4356 else FAIL "syntax error" 4357 end 4358 else FAIL "bad register list") 4359 | (Option.SOME _,(NONE,true)) => FAIL "bad register list" 4360 | _ => FAIL "syntax error" 4361 end 4362 | _ => FAIL "syntax error"; 4363 4364fun p_cps (enable,l) = 4365 case l of 4366 [i] => 4367 (if (stripSpaces i) = "i" 4368 then OK(al,System(ChangeProcessorState enable)) 4369 else FAIL "syntax error") 4370 | _ => FAIL "syntax error"; 4371 4372fun p_mrs (c,l) = 4373 case (p_al_suffix c,l) of 4374 (Option.SOME c,[r,s]) => 4375 (case (p_register r,p_special_register s) of 4376 (Option.SOME rd,Option.SOME SYSm) => 4377 OK(c,System(MoveToRegisterFromSpecial(SYSm,rd))) 4378 | _ => FAIL "syntax error") 4379 | _ => FAIL "syntax error"; 4380 4381fun p_msr (c,l) = 4382 case (p_al_suffix c,l) of 4383 (Option.SOME c,[s,r]) => 4384 (case (p_special_register s,p_register r) of 4385 (Option.SOME SYSm,Option.SOME rn) => 4386 OK(c,System(MoveToSpecialRegister(SYSm,rn))) 4387 | _ => FAIL "syntax error") 4388 | _ => FAIL "syntax error"; 4389 4390fun p_barrier_option l = 4391 case l of 4392 [] => Option.SOME(BitsN.B(0xF,4)) 4393 | [s] => 4394 (case stripSpaces s of 4395 "sy" => Option.SOME(BitsN.B(0xF,4)) 4396 | "st" => Option.SOME(BitsN.B(0xE,4)) 4397 | "ish" => Option.SOME(BitsN.B(0xB,4)) 4398 | "ishst" => Option.SOME(BitsN.B(0xA,4)) 4399 | "nsh" => Option.SOME(BitsN.B(0x7,4)) 4400 | "nshst" => Option.SOME(BitsN.B(0x6,4)) 4401 | "osh" => Option.SOME(BitsN.B(0x3,4)) 4402 | "oshst" => Option.SOME(BitsN.B(0x2,4)) 4403 | n => 4404 (case Nat.fromString n of 4405 Option.SOME v => Option.SOME(BitsN.fromNat(v,4)) 4406 | NONE => NONE)) 4407 | _ => NONE; 4408 4409fun p_dmb_dsb (c,(sync,l)) = 4410 case (p_suffix c,p_barrier_option l) of 4411 (Option.SOME c,Option.SOME option) => 4412 OK(c, 4413 Hint 4414 (if sync 4415 then DataSynchronizationBarrier option 4416 else DataMemoryBarrier option)) 4417 | _ => FAIL "syntax error"; 4418 4419fun p_isb (c,l) = 4420 case (p_suffix c,p_barrier_option l) of 4421 (Option.SOME c,Option.SOME(BitsN.B(0xF,_))) => 4422 OK(c,Hint(InstructionSynchronizationBarrier(BitsN.B(0xF,4)))) 4423 | _ => FAIL "syntax error"; 4424 4425fun p_call (c,(opc,l)) = 4426 case (p_al_suffix c,l) of 4427 (Option.SOME c,[imm]) => 4428 (case p_immediate_number 32 imm of 4429 Option.SOME(true,imm32) => 4430 let 4431 val ast = 4432 case opc of 4433 0 => Undefined imm32 4434 | 1 => System(SupervisorCall imm32) 4435 | _ => Hint(Breakpoint imm32) 4436 in 4437 OK(c,ast) 4438 end 4439 | Option.SOME(false,_) => FAIL "immediate too large" 4440 | _ => FAIL "syntax error") 4441 | _ => FAIL "syntax error"; 4442 4443fun p_noarg (c,i) = 4444 case p_al_suffix c of 4445 Option.SOME c => OK(c,i) 4446 | NONE => FAIL "syntax error"; 4447 4448fun p_tokens s = 4449 let 4450 val (l,r) = 4451 L3.splitl 4452 (fn c => not(Char.isSpace c), 4453 L3.lowercase(L3.snd(L3.splitl(fn c => Char.isSpace c,s)))) 4454 val r = L3.uncurry String.fields (fn c => c = #",",r) 4455 val r = 4456 if ((L3.length r) = 1) andalso ((stripSpaces(List.hd r)) = "") 4457 then [] 4458 else r 4459 in 4460 l :: r 4461 end; 4462 4463fun instructionFromString s = 4464 case p_tokens s of 4465 v'0 :: v'1 => 4466 (case (String.explode v'0,v'1) of 4467 (#"a" :: (#"d" :: (#"r" :: c)),l) => p_adr(String.implode c,l) 4468 | (#"a" :: (#"n" :: (#"d" :: (#"s" :: c))),l) => 4469 p_arith_logic(String.implode c,(BitsN.B(0x0,4),(true,l))) 4470 | (#"e" :: (#"o" :: (#"r" :: (#"s" :: c))),l) => 4471 p_arith_logic(String.implode c,(BitsN.B(0x1,4),(true,l))) 4472 | (#"s" :: (#"u" :: (#"b" :: (#"s" :: c))),l) => 4473 p_arith_logic(String.implode c,(BitsN.B(0x2,4),(true,l))) 4474 | (#"s" :: (#"u" :: (#"b" :: c)),l) => 4475 p_arith_logic(String.implode c,(BitsN.B(0x2,4),(false,l))) 4476 | (#"r" :: (#"s" :: (#"b" :: (#"s" :: c))),l) => 4477 p_arith_logic(String.implode c,(BitsN.B(0x3,4),(true,l))) 4478 | (#"a" :: (#"d" :: (#"d" :: (#"s" :: c))),l) => 4479 p_arith_logic(String.implode c,(BitsN.B(0x4,4),(true,l))) 4480 | (#"a" :: (#"d" :: (#"d" :: c)),l) => 4481 p_arith_logic(String.implode c,(BitsN.B(0x4,4),(false,l))) 4482 | (#"a" :: (#"d" :: (#"c" :: (#"s" :: c))),l) => 4483 p_arith_logic(String.implode c,(BitsN.B(0x5,4),(true,l))) 4484 | (#"s" :: (#"b" :: (#"c" :: (#"s" :: c))),l) => 4485 p_arith_logic(String.implode c,(BitsN.B(0x6,4),(true,l))) 4486 | (#"o" :: (#"r" :: (#"r" :: (#"s" :: c))),l) => 4487 p_arith_logic(String.implode c,(BitsN.B(0xC,4),(true,l))) 4488 | (#"b" :: (#"i" :: (#"c" :: (#"s" :: c))),l) => 4489 p_arith_logic(String.implode c,(BitsN.B(0xE,4),(true,l))) 4490 | (#"t" :: (#"s" :: (#"t" :: c)),l) => 4491 p_test_compare(String.implode c,(BitsN.B(0x0,2),l)) 4492 | (#"c" :: (#"m" :: (#"p" :: c)),l) => 4493 p_test_compare(String.implode c,(BitsN.B(0x2,2),l)) 4494 | (#"c" :: (#"m" :: (#"n" :: c)),l) => 4495 p_test_compare(String.implode c,(BitsN.B(0x3,2),l)) 4496 | (#"m" :: (#"o" :: (#"v" :: (#"s" :: c))),l) => 4497 p_mov_mvn(String.implode c,(false,(true,l))) 4498 | (#"m" :: (#"o" :: (#"v" :: c)),l) => 4499 p_mov_mvn(String.implode c,(false,(false,l))) 4500 | (#"m" :: (#"v" :: (#"n" :: (#"s" :: c))),l) => 4501 p_mov_mvn(String.implode c,(true,(true,l))) 4502 | (#"l" :: (#"s" :: (#"l" :: (#"s" :: c))),l) => 4503 p_shift(String.implode c,(SRType_LSL,l)) 4504 | (#"l" :: (#"s" :: (#"r" :: (#"s" :: c))),l) => 4505 p_shift(String.implode c,(SRType_LSR,l)) 4506 | (#"a" :: (#"s" :: (#"r" :: (#"s" :: c))),l) => 4507 p_shift(String.implode c,(SRType_ASR,l)) 4508 | (#"r" :: (#"o" :: (#"r" :: (#"s" :: c))),l) => 4509 p_shift(String.implode c,(SRType_ROR,l)) 4510 | (#"m" :: (#"u" :: (#"l" :: (#"s" :: c))),l) => 4511 p_mul(String.implode c,l) 4512 | (#"s" :: (#"x" :: (#"t" :: (#"b" :: c))),l) => 4513 p_sxtb_etc(String.implode c,(false,(false,l))) 4514 | (#"u" :: (#"x" :: (#"t" :: (#"b" :: c))),l) => 4515 p_sxtb_etc(String.implode c,(false,(true,l))) 4516 | (#"s" :: (#"x" :: (#"t" :: (#"h" :: c))),l) => 4517 p_sxtb_etc(String.implode c,(true,(false,l))) 4518 | (#"u" :: (#"x" :: (#"t" :: (#"h" :: c))),l) => 4519 p_sxtb_etc(String.implode c,(true,(true,l))) 4520 | (#"r" :: (#"e" :: (#"v" :: (#"1" :: (#"6" :: c)))),l) => 4521 p_rev16(String.implode c,l) 4522 | (#"r" :: (#"e" :: (#"v" :: (#"s" :: (#"h" :: c)))),l) => 4523 p_revsh(String.implode c,l) 4524 | (#"r" :: (#"e" :: (#"v" :: c)),l) => p_rev(String.implode c,l) 4525 | (#"l" :: (#"d" :: (#"r" :: (#"b" :: c))),l) => 4526 p_ldrb_ldrh(String.implode c,(true,(true,l))) 4527 | (#"l" :: (#"d" :: (#"r" :: (#"s" :: (#"b" :: c)))),l) => 4528 p_ldrb_ldrh(String.implode c,(false,(true,l))) 4529 | (#"l" :: (#"d" :: (#"r" :: (#"h" :: c))),l) => 4530 p_ldrb_ldrh(String.implode c,(true,(false,l))) 4531 | (#"l" :: (#"d" :: (#"r" :: (#"s" :: (#"h" :: c)))),l) => 4532 p_ldrb_ldrh(String.implode c,(false,(false,l))) 4533 | (#"l" :: (#"d" :: (#"r" :: c)),l) => 4534 p_ldr_str(String.implode c,(0,l)) 4535 | (#"s" :: (#"t" :: (#"r" :: (#"b" :: c))),l) => 4536 p_ldr_str(String.implode c,(1,l)) 4537 | (#"s" :: (#"t" :: (#"r" :: (#"h" :: c))),l) => 4538 p_ldr_str(String.implode c,(2,l)) 4539 | (#"s" :: (#"t" :: (#"r" :: c)),l) => 4540 p_ldr_str(String.implode c,(3,l)) 4541 | (#"p" :: (#"o" :: (#"p" :: c)),l) => 4542 p_pop_push(String.implode c,(true,l)) 4543 | (#"p" :: (#"u" :: (#"s" :: (#"h" :: c))),l) => 4544 p_pop_push(String.implode c,(false,l)) 4545 | (#"l" :: (#"d" :: (#"m" :: (#"i" :: (#"a" :: c)))),l) => 4546 p_ldm_stm(String.implode c,(true,l)) 4547 | (#"l" :: (#"d" :: (#"m" :: (#"f" :: (#"d" :: c)))),l) => 4548 p_ldm_stm(String.implode c,(true,l)) 4549 | (#"l" :: (#"d" :: (#"m" :: c)),l) => 4550 p_ldm_stm(String.implode c,(true,l)) 4551 | (#"s" :: (#"t" :: (#"m" :: (#"i" :: (#"a" :: c)))),l) => 4552 p_ldm_stm(String.implode c,(false,l)) 4553 | (#"s" :: (#"t" :: (#"m" :: (#"e" :: (#"a" :: c)))),l) => 4554 p_ldm_stm(String.implode c,(false,l)) 4555 | (#"s" :: (#"t" :: (#"m" :: c)),l) => 4556 p_ldm_stm(String.implode c,(false,l)) 4557 | ([#"c",#"p",#"s",#"i",#"e"],l) => p_cps(true,l) 4558 | ([#"c",#"p",#"s",#"i",#"d"],l) => p_cps(false,l) 4559 | (#"m" :: (#"r" :: (#"s" :: c)),l) => p_mrs(String.implode c,l) 4560 | (#"m" :: (#"s" :: (#"r" :: c)),l) => p_msr(String.implode c,l) 4561 | (#"u" :: (#"d" :: (#"f" :: c)),l) => 4562 p_call(String.implode c,(0,l)) 4563 | (#"s" :: (#"v" :: (#"c" :: c)),l) => 4564 p_call(String.implode c,(1,l)) 4565 | (#"b" :: (#"k" :: (#"p" :: (#"t" :: c))),l) => 4566 p_call(String.implode c,(2,l)) 4567 | (#"d" :: (#"m" :: (#"b" :: c)),l) => 4568 p_dmb_dsb(String.implode c,(false,l)) 4569 | (#"d" :: (#"s" :: (#"b" :: c)),l) => 4570 p_dmb_dsb(String.implode c,(true,l)) 4571 | (#"i" :: (#"s" :: (#"b" :: c)),l) => p_isb(String.implode c,l) 4572 | (#"n" :: (#"o" :: (#"p" :: c)),[]) => 4573 p_noarg(String.implode c,NoOperation ()) 4574 | (#"s" :: (#"e" :: (#"v" :: c)),[]) => 4575 p_noarg(String.implode c,Hint(SendEvent ())) 4576 | (#"w" :: (#"f" :: (#"e" :: c)),[]) => 4577 p_noarg(String.implode c,Hint(WaitForEvent ())) 4578 | (#"w" :: (#"f" :: (#"i" :: c)),[]) => 4579 p_noarg(String.implode c,Hint(WaitForInterrupt ())) 4580 | (#"y" :: (#"i" :: (#"e" :: (#"l" :: (#"d" :: c)))),[]) => 4581 p_noarg(String.implode c,Hint(Yield ())) 4582 | ([#"b",#"l",c1,c2,#".",e],l) => 4583 p_bl(String.implode[c1,c2,#".",e],l) 4584 | ([#"b",#"l",#".",e],l) => p_bl(String.implode[#".",e],l) 4585 | ([#"b",#"l"],l) => p_bl("",l) 4586 | (#"b" :: (#"x" :: c),l) => p_bx(String.implode c,l) 4587 | (#"b" :: (#"l" :: (#"x" :: c)),l) => p_blx(String.implode c,l) 4588 | (#"b" :: c,l) => p_b(String.implode c,l) 4589 | ([#"h",#"a",#"l",#"f"],[w]) => 4590 (case p_encode_immediate 16 w of 4591 Option.SOME(true,w) => HALFWORD w 4592 | Option.SOME _ => FAIL "immediate too large" 4593 | NONE => FAIL "syntax error") 4594 | _ => FAIL "Unrecognised op-code") 4595 | _ => FAIL "Unrecognised op-code"; 4596 4597fun halfString w = L3.padLeftString(#"0",(4,BitsN.toHexString w)); 4598 4599fun EncodeThumb s = 4600 case instructionFromString s of 4601 OK((c,e),ast) => 4602 let 4603 val enc = 4604 case e of "n" => Enc_Narrow | "w" => Enc_Wide | _ => Enc_Thumb 4605 in 4606 case instructionEncode(c,(ast,enc)) of 4607 Thumb16 w => ("",Option.SOME(halfString w)) 4608 | Thumb32(w1,w2) => 4609 ("", 4610 Option.SOME(String.concat[halfString w1," ",halfString w2])) 4611 | BadCode err => ("Encode error: " ^ err,NONE) 4612 end 4613 | HALFWORD w => ("",Option.SOME(halfString w)) 4614 | PENDING _ => ("Contains label",NONE) 4615 | FAIL err => ("Parse error: " ^ err,NONE); 4616 4617fun s_cond c = 4618 case c of 4619 BitsN.B(0x0,_) => "eq" 4620 | BitsN.B(0x1,_) => "ne" 4621 | BitsN.B(0x2,_) => "cs" 4622 | BitsN.B(0x3,_) => "cc" 4623 | BitsN.B(0x4,_) => "mi" 4624 | BitsN.B(0x5,_) => "pl" 4625 | BitsN.B(0x6,_) => "vs" 4626 | BitsN.B(0x7,_) => "vc" 4627 | BitsN.B(0x8,_) => "hi" 4628 | BitsN.B(0x9,_) => "ls" 4629 | BitsN.B(0xA,_) => "ge" 4630 | BitsN.B(0xB,_) => "lt" 4631 | BitsN.B(0xC,_) => "gt" 4632 | BitsN.B(0xD,_) => "le" 4633 | _ => ""; 4634 4635fun s_reg r = 4636 case r of 4637 BitsN.B(0xD,_) => "sp" 4638 | BitsN.B(0xE,_) => "lr" 4639 | BitsN.B(0xF,_) => "pc" 4640 | _ => "r" ^ (Nat.toString(BitsN.toNat r)); 4641 4642fun s_reg2 (r1,r2) = String.concat[s_reg r1,", ",s_reg r2]; 4643 4644fun s_reg3 (r1,(r2,r3)) = String.concat[s_reg2(r1,r2),", ",s_reg r3]; 4645 4646fun s_reg4 (r1,(r2,(r3,r4))) = 4647 String.concat[s_reg3(r1,(r2,r3)),", ",s_reg r4]; 4648 4649fun s_hex N v = 4650 if BitsN.<+(v,BitsN.BV(0x64,N)) 4651 then Nat.toString(BitsN.toNat v) 4652 else "0x" ^ (BitsN.toHexString v); 4653 4654fun s_offset imm32 = 4655 let 4656 val imm32 = BitsN.+(imm32,BitsN.B(0x4,32)) 4657 in 4658 if BitsN.<(imm32,BitsN.B(0x0,32)) 4659 then "-#" ^ (s_hex 32 (BitsN.neg imm32)) 4660 else "+#" ^ (s_hex 32 imm32) 4661 end; 4662 4663fun s_maybe_offset imm32 = 4664 if imm32 = (BitsN.B(0x0,32)) then "" else ", #" ^ (s_hex 32 imm32); 4665 4666fun s_special_reg SYSm = 4667 case SYSm of 4668 BitsN.B(0x0,_) => "apsr" 4669 | BitsN.B(0x1,_) => "iapsr" 4670 | BitsN.B(0x2,_) => "eapsr" 4671 | BitsN.B(0x3,_) => "xpsr" 4672 | BitsN.B(0x5,_) => "ipsr" 4673 | BitsN.B(0x6,_) => "epsr" 4674 | BitsN.B(0x7,_) => "iepsr" 4675 | BitsN.B(0x8,_) => "msp" 4676 | BitsN.B(0x9,_) => "psp" 4677 | BitsN.B(0x10,_) => "primask" 4678 | BitsN.B(0x14,_) => "control" 4679 | _ => Nat.toString(BitsN.toNat SYSm); 4680 4681fun s_barrier_option option = 4682 case option of 4683 BitsN.B(0x2,_) => "oshst" 4684 | BitsN.B(0x3,_) => "osh" 4685 | BitsN.B(0x6,_) => "nshst" 4686 | BitsN.B(0x7,_) => "nsh" 4687 | BitsN.B(0xA,_) => "ishst" 4688 | BitsN.B(0xB,_) => "ish" 4689 | BitsN.B(0xE,_) => "st" 4690 | BitsN.B(0xF,_) => "sy" 4691 | _ => Nat.toString(BitsN.toNat option); 4692 4693fun s_imm_form (t,(n,imm32)) = 4694 String.concat[s_reg t,", [",s_reg n,s_maybe_offset imm32,"]"]; 4695 4696fun s_reg_form (t,(n,m)) = String.concat[s_reg t,", [",s_reg2(n,m),"]"]; 4697 4698fun contiguous (a,(i,l)) = 4699 case l of 4700 [] => a 4701 | y :: x => 4702 contiguous 4703 (if y 4704 then case a of 4705 [] => [(i,i)] 4706 | (b,t) :: r => 4707 (if (Nat.+(i,1)) = b then (i,t) :: r else (i,i) :: a) 4708 else a,(Nat.-(i,1),x)); 4709 4710fun s_registers_from_contiguous (a,l) = 4711 case l of 4712 [] => a 4713 | (b,t) :: r => 4714 let 4715 val d = Nat.-(t,b) 4716 in 4717 s_registers_from_contiguous 4718 (if d = 0 4719 then String.concat[a,", ",s_reg(BitsN.fromNat(b,4))] 4720 else if d = 1 4721 then String.concat 4722 [a,", ",s_reg2(BitsN.fromNat(b,4),BitsN.fromNat(t,4))] 4723 else String.concat 4724 [a,", ",s_reg(BitsN.fromNat(b,4)),"-", 4725 s_reg(BitsN.fromNat(t,4))],r) 4726 end; 4727 4728fun s_registers N l = 4729 case String.explode 4730 (s_registers_from_contiguous 4731 ("", 4732 contiguous 4733 ([],(Nat.-(BitsN.size(BitsN.BV(0x0,N)),1),BitsN.toBitstring l)))) of 4734 [] => "{}" 4735 | #"," :: (#" " :: s) => String.concat["{",String.implode s,"}"] 4736 | _ => "???"; 4737 4738fun s_test_compare opc = 4739 case opc of 4740 BitsN.B(0x0,_) => "tst" 4741 | BitsN.B(0x1,_) => "teq" 4742 | BitsN.B(0x2,_) => "cmp" 4743 | BitsN.B(0x3,_) => "cmn" 4744 | _ => raise General.Bind; 4745 4746fun s_arith_logic opc = 4747 case opc of 4748 BitsN.B(0x0,_) => "and" 4749 | BitsN.B(0x1,_) => "eor" 4750 | BitsN.B(0x2,_) => "sub" 4751 | BitsN.B(0x3,_) => "rsb" 4752 | BitsN.B(0x4,_) => "add" 4753 | BitsN.B(0x5,_) => "adc" 4754 | BitsN.B(0x6,_) => "sbc" 4755 | BitsN.B(0x7,_) => "rsc" 4756 | BitsN.B(0x8,_) => "tst" 4757 | BitsN.B(0x9,_) => "teq" 4758 | BitsN.B(0xA,_) => "cmp" 4759 | BitsN.B(0xB,_) => "cmn" 4760 | BitsN.B(0xC,_) => "orr" 4761 | BitsN.B(0xD,_) => "mov" 4762 | BitsN.B(0xE,_) => "bic" 4763 | BitsN.B(0xF,_) => "mvn" 4764 | _ => raise General.Bind; 4765 4766fun s_shift shift_t = 4767 case shift_t of 4768 SRType_LSL => "lsl" 4769 | SRType_LSR => "lsr" 4770 | SRType_ASR => "asr" 4771 | SRType_ROR => "ror" 4772 | SRType_RRX => "rrx"; 4773 4774fun s_shift_n (shift_t,shift_n) = 4775 case (shift_t,shift_n) of 4776 (SRType_LSL,0) => "" 4777 | (SRType_RRX,1) => ", rrx" 4778 | _ => String.concat[", ",s_shift shift_t," #",Nat.toString shift_n]; 4779 4780fun s_shift_r (add,(r,(shift_t,shift_n))) = 4781 String.concat 4782 [", ",if add then "" else "-",s_reg r,s_shift_n(shift_t,shift_n)]; 4783 4784fun s_branch (c,ast) = 4785 case ast of 4786 BranchTarget imm32 => ("b" ^ (s_cond c),s_offset imm32) 4787 | BranchExchange m => ("bx",s_reg m) 4788 | BranchLinkImmediate imm32 => ("bl",s_offset imm32) 4789 | BranchLinkExchangeRegister m => ("blx",s_reg m); 4790 4791fun s_data ast = 4792 case ast of 4793 Move(d,imm12) => ("movs",String.concat[s_reg d,", #",s_hex 32 imm12]) 4794 | ArithLogicImmediate(opc,(setflags,(d,(n,imm12)))) => 4795 ((s_arith_logic opc) ^ (if setflags then "s" else ""), 4796 String.concat[s_reg2(d,n),", #",s_hex 32 imm12]) 4797 | Register(opc,(setflags,(d,(n,m)))) => 4798 ((s_arith_logic opc) ^ (if setflags then "s" else ""),s_reg3(d,(n,m))) 4799 | TestCompareRegister(opc,(n,m)) => (s_test_compare opc,s_reg2(n,m)) 4800 | CompareImmediate(n,imm32) => 4801 ("cmp",String.concat[s_reg n,", #",s_hex 32 imm32]) 4802 | ShiftImmediate(true,(setflags,(d,(m,(shift_t,shift_n))))) => 4803 ("mvn" ^ (if setflags then "s" else ""), 4804 (s_reg2(d,m)) ^ (s_shift_n(shift_t,shift_n))) 4805 | ShiftImmediate(false,(setflags,(d,(m,(SRType_LSL,0))))) => 4806 ("mov" ^ (if setflags then "s" else ""),s_reg2(d,m)) 4807 | ShiftImmediate(false,(setflags,(d,(m,(shift_t,shift_n))))) => 4808 ((s_shift shift_t) ^ (if setflags then "s" else ""), 4809 (s_reg2(d,m)) 4810 ^ 4811 (if (shift_t = SRType_RRX) andalso (shift_n = 1) 4812 then "" 4813 else ", #" ^ (Nat.toString shift_n))) 4814 | ShiftRegister(d,(n,(shift_t,m))) => 4815 ((s_shift shift_t) ^ "s",s_reg3(d,(n,m))); 4816 4817fun s_load ast = 4818 case ast of 4819 LoadWord(t,(n,immediate_form imm32)) => 4820 ("ldr",s_imm_form(t,(n,imm32))) 4821 | LoadWord(t,(n,register_form m)) => ("ldr",s_reg_form(t,(n,m))) 4822 | LoadLiteral(t,imm32) => 4823 ("ldr",String.concat[s_reg t,", [pc",s_maybe_offset imm32,"]"]) 4824 | LoadByte(unsigned,(t,(n,immediate_form imm32))) => 4825 ("ldr" ^ (if unsigned then "b" else "sb"),s_imm_form(t,(n,imm32))) 4826 | LoadByte(unsigned,(t,(n,register_form m))) => 4827 ("ldr" ^ (if unsigned then "b" else "sb"),s_reg_form(t,(n,m))) 4828 | LoadHalf(unsigned,(t,(n,immediate_form imm32))) => 4829 ("ldr" ^ (if unsigned then "h" else "sh"),s_imm_form(t,(n,imm32))) 4830 | LoadHalf(unsigned,(t,(n,register_form m))) => 4831 ("ldr" ^ (if unsigned then "h" else "sh"),s_reg_form(t,(n,m))) 4832 | LoadMultiple(true,(BitsN.B(0xD,4),registers)) => 4833 ("pop", 4834 s_registers 16 4835 (BitsN.concat 4836 [BitsN.bits(8,8) registers,BitsN.B(0x0,7), 4837 BitsN.bits(7,0) registers])) 4838 | LoadMultiple(wback,(n,registers)) => 4839 ("ldm", 4840 String.concat 4841 [s_reg n,if wback then "!" else "",", ", 4842 s_registers 16 4843 (BitsN.concat 4844 [BitsN.bits(8,8) registers,BitsN.B(0x0,7), 4845 BitsN.bits(7,0) registers])]); 4846 4847fun s_store ast = 4848 case ast of 4849 StoreWord(t,(n,immediate_form imm32)) => 4850 ("str",s_imm_form(t,(n,imm32))) 4851 | StoreWord(t,(n,register_form m)) => ("str",s_reg_form(t,(n,m))) 4852 | StoreByte(t,(n,immediate_form imm32)) => 4853 ("strb",s_imm_form(t,(n,imm32))) 4854 | StoreByte(t,(n,register_form m)) => ("strb",s_reg_form(t,(n,m))) 4855 | StoreHalf(t,(n,immediate_form imm32)) => 4856 ("strh",s_imm_form(t,(n,imm32))) 4857 | StoreHalf(t,(n,register_form m)) => ("strh",s_reg_form(t,(n,m))) 4858 | Push registers => 4859 ("push", 4860 s_registers 15 4861 (BitsN.concat 4862 [BitsN.bits(8,8) registers,BitsN.B(0x0,6), 4863 BitsN.bits(7,0) registers])) 4864 | StoreMultiple(n,registers) => 4865 ("stm",String.concat[s_reg n,"!, ",s_registers 8 registers]); 4866 4867fun s_hint ast = 4868 case ast of 4869 Breakpoint imm32 => ("bkpt","#" ^ (s_hex 32 imm32)) 4870 | DataMemoryBarrier option => ("dmb",s_barrier_option option) 4871 | DataSynchronizationBarrier option => ("dsb",s_barrier_option option) 4872 | InstructionSynchronizationBarrier option => 4873 ("isb",s_barrier_option option) 4874 | SendEvent () => ("sev","") 4875 | WaitForEvent () => ("wfe","") 4876 | WaitForInterrupt () => ("wfi","") 4877 | Yield () => ("yield",""); 4878 4879fun s_media ast = 4880 case ast of 4881 ExtendByte(unsigned,(d,m)) => 4882 ((if unsigned then "u" else "s") ^ "xtb",s_reg2(d,m)) 4883 | ExtendHalfword(unsigned,(d,m)) => 4884 ((if unsigned then "u" else "s") ^ "xth",s_reg2(d,m)) 4885 | ByteReverse(d,m) => ("rev",s_reg2(d,m)) 4886 | ByteReversePackedHalfword(d,m) => ("rev16",s_reg2(d,m)) 4887 | ByteReverseSignedHalfword(d,m) => ("revsh",s_reg2(d,m)); 4888 4889fun s_system ast = 4890 case ast of 4891 ChangeProcessorState enable => 4892 ("cps" ^ (if enable then "ie" else "id"),"i") 4893 | MoveToRegisterFromSpecial(SYSm,d) => 4894 ("mrs",String.concat[s_reg d,", ",s_special_reg SYSm]) 4895 | MoveToSpecialRegister(SYSm,n) => 4896 ("msr",String.concat[s_special_reg SYSm,", ",s_reg n]) 4897 | SupervisorCall imm32 => ("svc","#" ^ (s_hex 32 imm32)); 4898 4899fun instructionToString (c,ast) = 4900 case ast of 4901 Branch b => s_branch(c,b) 4902 | Data d => s_data d 4903 | Load l => s_load l 4904 | Store s => s_store s 4905 | Media m => s_media m 4906 | System s => s_system s 4907 | Hint h => s_hint h 4908 | Multiply(Multiply32(d,(n,m))) => ("muls",s_reg3(d,(n,m))) 4909 | Undefined imm32 => ("udf","#" ^ (s_hex 32 imm32)) 4910 | NoOperation () => ("nop",""); 4911 4912end