1(* ========================================================================= *) 2(* FILE : armScript.sml *) 3(* DESCRIPTION : Model of the ARM instruction set architecture *) 4(* *) 5(* AUTHOR : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2001 - 2007 *) 7(* ========================================================================= *) 8 9(* interactive use: 10 app load ["wordsLib", "wordsSyntax", "rich_listTheory", "updateTheory"]; 11*) 12 13open HolKernel boolLib bossLib Parse; 14open Q wordsTheory rich_listTheory updateTheory; 15 16val _ = new_theory "arm"; 17 18(* ------------------------------------------------------------------------- *) 19(* The ARM State Space *) 20(* ------------------------------------------------------------------------- *) 21 22val _ = Hol_datatype `state_inp = <| state : 'a; inp : num -> 'b |>`; 23val _ = Hol_datatype `state_out = <| state : 'a; out : 'b |>`; 24 25val _ = Hol_datatype `register = 26 r0 | r1 | r2 | r3 | r4 | r5 | r6 | r7 | 27 r8 | r9 | r10 | r11 | r12 | r13 | r14 | r15 | 28 r8_fiq | r9_fiq | r10_fiq | r11_fiq | r12_fiq | r13_fiq | r14_fiq | 29 r13_irq | r14_irq | 30 r13_svc | r14_svc | 31 r13_abt | r14_abt | 32 r13_und | r14_und`; 33 34val _ = Hol_datatype 35 `psr = CPSR | SPSR_fiq | SPSR_irq | SPSR_svc | SPSR_abt | SPSR_und`; 36 37val _ = Hol_datatype 38 `exceptions = reset | undefined | software | pabort | 39 dabort | address |interrupt | fast`; 40 41val _ = type_abbrev("registers", ``:register->word32``); 42val _ = type_abbrev("psrs", ``:psr->word32``); 43 44val _ = Hol_datatype `regs = <| reg : registers; psr : psrs |>`; 45 46val _ = Hol_datatype 47 `arm_state = <| regs : regs; ireg : word32; exception : exceptions |>`; 48 49(* ......................................................................... *) 50 51val _ = Hol_datatype 52 `formats = SignedByte | UnsignedByte | SignedHalfWord | 53 UnsignedHalfWord | UnsignedWord`; 54 55val _ = Hol_datatype `data = Byte of word8 | Half of word16 | Word of word32`; 56 57val _ = Hol_datatype` 58 memop = MemRead of word32 | MemWrite of word32=>data | CPWrite of word32`; 59 60val _ = Hol_datatype` 61 interrupt = Reset of regs | Undef | Prefetch | Dabort of num | Fiq | Irq`; 62 63val _ = Hol_datatype` 64 arm_input = <| ireg : word32; data : word32 list; 65 interrupt : interrupt option; no_cp : bool |>`; 66 67val _ = Hol_datatype `mode = usr | fiq | irq | svc | abt | und | sys | safe`; 68 69val _ = Hol_datatype 70 `condition = EQ | CS | MI | VS | HI | GE | GT | AL | 71 NE | CC | PL | VC | LS | LT | LE | NV`; 72 73val _ = Hol_datatype 74 `iclass = swp | mrs | msr | data_proc | mla_mul | 75 ldr_str | ldrh_strh | ldm_stm | br | swi_ex | cdp_und | 76 mcr | mrc | ldc_stc | unexec`; 77 78val _ = Hol_datatype` 79 arm_output = <| transfers : memop list; cpi : bool; user : bool |>`; 80 81(* ------------------------------------------------------------------------- *) 82(* Memory operations *) 83(* ------------------------------------------------------------------------- *) 84 85val _ = wordsLib.guess_lengths(); 86 87val GET_BYTE_def = Define` 88 GET_BYTE (oareg:word2) (data:word32) = 89 case oareg of 90 0w => (7 >< 0) data 91 | 1w => (15 >< 8) data 92 | 2w => (23 >< 16) data 93 | _ => (31 >< 24) data`; 94 95val GET_HALF_def = Define` 96 GET_HALF (oareg:word2) (data:word32) = 97 if oareg ' 1 then 98 (31 >< 16) data 99 else 100 (15 >< 0) data`; 101 102val FORMAT_def = Define` 103 FORMAT fmt oareg data = 104 case fmt of 105 SignedByte => sw2sw (GET_BYTE oareg data) 106 | UnsignedByte => w2w (GET_BYTE oareg data) 107 | SignedHalfWord => sw2sw (GET_HALF oareg data) 108 | UnsignedHalfWord => w2w (GET_HALF oareg data) 109 | UnsignedWord => data #>> (8 * w2n oareg)`; 110 111(* ------------------------------------------------------------------------- *) 112(* General Purpose Register operations *) 113(* ------------------------------------------------------------------------- *) 114 115val USER_def = Define `USER m = (m = usr) \/ (m = sys) \/ (m = safe)`; 116 117val mode_reg2num_def = Define` 118 mode_reg2num m (w:word4) = let n = w2n w in 119 (if (n = 15) \/ USER m \/ (m = fiq) /\ n < 8 \/ ~(m = fiq) /\ n < 13 then 120 n 121 else case m of 122 fiq => n + 8 123 | irq => n + 10 124 | svc => n + 12 125 | abt => n + 14 126 | und => n + 16 127 | _ => ARB)`; 128 129val REG_READ_def = Define` 130 REG_READ (reg:registers) m n = 131 if n = 15w then 132 reg r15 + 8w 133 else 134 reg (num2register (mode_reg2num m n))`; 135 136val REG_WRITE_def = Define` 137 REG_WRITE (reg:registers) m n d = 138 (num2register (mode_reg2num m n) =+ d) reg`; 139 140val INC_PC_def = Define `INC_PC (reg:registers) = (r15 =+ reg r15 + 4w) reg`; 141val FETCH_PC_def = Define `FETCH_PC (reg:registers) = reg r15`; 142 143(* FETCH_PC is needed because (REG_READ reg usr 15w) gives PC + 8. *) 144 145(* ------------------------------------------------------------------------- *) 146(* Program Status Register operations *) 147(* ------------------------------------------------------------------------- *) 148 149val SET_NZCV_def = Define` 150 SET_NZCV (N,Z,C,V) w:word32 = 151 word_modify (\i b. (i = 31) /\ N \/ (i = 30) /\ Z \/ 152 (i = 29) /\ C \/ (i = 28) /\ V \/ 153 (i < 28) /\ b) w`; 154 155val SET_NZC_def = Define `SET_NZC (N,Z,C) w = SET_NZCV (N,Z,C,w ' 28) w`; 156val SET_NZ_def = Define `SET_NZ (N,Z) w = SET_NZC (N,Z,w ' 29) w`; 157 158val mode_num_def = Define` 159 mode_num mode = 160 case mode of 161 usr => 16w 162 | fiq => 17w 163 | irq => 18w 164 | svc => 19w 165 | abt => 23w 166 | und => 27w 167 | sys => 31w 168 | _ => 0w:word5`; 169 170val SET_IFMODE_def = Define` 171 SET_IFMODE irq' fiq' mode w:word32 = 172 word_modify (\i b. (7 < i \/ (i = 5)) /\ b \/ 173 (i = 7) /\ irq' \/ (i = 6) /\ fiq' \/ 174 (i < 5) /\ (mode_num mode) ' i) w`; 175 176val DECODE_MODE_def = Define` 177 DECODE_MODE (m:word5) = 178 case m of 179 16w => usr 180 | 17w => fiq 181 | 18w => irq 182 | 19w => svc 183 | 23w => abt 184 | 27w => und 185 | 31w => sys 186 | _ => safe`; 187 188val NZCV_def = Define `NZCV (w:word32) = (w ' 31, w ' 30, w ' 29, w ' 28)`; 189 190val DECODE_PSR_def = Define` 191 DECODE_PSR (cpsr:word32) = (NZCV cpsr, cpsr ' 7, cpsr ' 6, (4 >< 0) cpsr)`; 192 193val CARRY_def = Define `CARRY (n,z,c,v) = c`; 194 195val mode2psr_def = Define` 196 mode2psr mode = 197 case mode of 198 usr => CPSR 199 | fiq => SPSR_fiq 200 | irq => SPSR_irq 201 | svc => SPSR_svc 202 | abt => SPSR_abt 203 | und => SPSR_und 204 | _ => CPSR`; 205 206val SPSR_READ_def = Define `SPSR_READ (psr:psrs) mode = psr (mode2psr mode)`; 207val CPSR_READ_def = Define `CPSR_READ (psr:psrs) = psr CPSR`; 208 209val CPSR_WRITE_def = Define` 210 CPSR_WRITE (psr:psrs) cpsr = (CPSR =+ cpsr) psr`; 211 212val SPSR_WRITE_def = Define` 213 SPSR_WRITE (psr:psrs) mode spsr = 214 if USER mode then psr else (mode2psr mode =+ spsr) psr`; 215 216(* ------------------------------------------------------------------------- *) 217(* The Sofware Interrupt/Exception instruction class (swi_ex) *) 218(* ------------------------------------------------------------------------- *) 219 220val exception2mode_def = Define` 221 exception2mode e = 222 case e of 223 reset => svc 224 | undefined => und 225 | software => svc 226 | address => svc 227 | pabort => abt 228 | dabort => abt 229 | interrupt => irq 230 | fast => fiq`; 231 232val EXCEPTION_def = Define` 233 EXCEPTION r type = 234 let cpsr = CPSR_READ r.psr in 235 let fiq' = ((type = reset) \/ (type = fast)) \/ cpsr ' 6 236 and mode' = exception2mode type 237 and pc = n2w (4 * exceptions2num type):word32 in 238 let reg' = REG_WRITE r.reg mode' 14w (FETCH_PC r.reg + 4w) in 239 <| reg := REG_WRITE reg' usr 15w pc; 240 psr := CPSR_WRITE (SPSR_WRITE r.psr mode' cpsr) 241 (SET_IFMODE T fiq' mode' cpsr) |>`; 242 243(* ------------------------------------------------------------------------- *) 244(* The Branch instruction class (br) *) 245(* ------------------------------------------------------------------------- *) 246 247val DECODE_BRANCH_def = Define` 248 DECODE_BRANCH (w:word32) = (w ' 24, (23 >< 0) w)`; 249 250val BRANCH_def = Define` 251 BRANCH r mode ireg = 252 let (L,offset) = DECODE_BRANCH ireg 253 and pc = REG_READ r.reg usr 15w in 254 let br_addr = pc + sw2sw offset << 2 in 255 let pc_reg = REG_WRITE r.reg usr 15w br_addr in 256 <| reg := if L then 257 REG_WRITE pc_reg mode 14w (FETCH_PC r.reg + 4w) 258 else 259 pc_reg; 260 psr := r.psr |>`; 261 262(* ------------------------------------------------------------------------- *) 263(* The Data Processing instruction class (data_proc) *) 264(* ------------------------------------------------------------------------- *) 265 266val LSL_def = Define` 267 LSL (m:word32) (n:word8) c = 268 if n = 0w then (c, m) else 269 (n <=+ 32w /\ m ' (32 - w2n n), m << w2n n)`; 270 271val LSR_def = Define` 272 LSR (m:word32) (n:word8) c = 273 if n = 0w then LSL m 0w c else 274 (n <=+ 32w /\ m ' (w2n n - 1), m >>> w2n n)`; 275 276val ASR_def = Define` 277 ASR (m:word32) (n:word8) c = 278 if n = 0w then LSL m 0w c else 279 (m ' (MIN 31 (w2n n - 1)), m >> w2n n)`; 280 281val ROR_def = Define` 282 ROR (m:word32) (n:word8) c = 283 if n = 0w then LSL m 0w c else 284 (m ' (w2n ((w2w n):word5) - 1), m #>> w2n n)`; 285 286val IMMEDIATE_def = Define` 287 IMMEDIATE C (opnd2:word12) = 288 let rot = (11 >< 8) opnd2 289 and imm = (7 >< 0) opnd2 290 in 291 ROR imm (2w * rot) C`; 292 293val SHIFT_IMMEDIATE2_def = Define` 294 SHIFT_IMMEDIATE2 shift (sh:word2) rm c = 295 case sh of 296 0w => LSL rm shift c 297 | 1w => LSR rm (if shift = 0w then 32w else shift) c 298 | 2w => ASR rm (if shift = 0w then 32w else shift) c 299 | _ => if shift = 0w then word_rrx (c,rm) else ROR rm shift c`; 300 301val SHIFT_REGISTER2_def = Define` 302 SHIFT_REGISTER2 shift (sh:word2) rm c = 303 case sh of 304 0w => LSL rm shift c 305 | 1w => LSR rm shift c 306 | 2w => ASR rm shift c 307 | _ => ROR rm shift c`; 308 309val SHIFT_IMMEDIATE_def = Define` 310 SHIFT_IMMEDIATE reg mode C (opnd2:word12) = 311 let Rm = (3 >< 0) opnd2 in 312 let rm = REG_READ reg mode Rm 313 and sh = (6 >< 5) opnd2 314 and shift = (11 >< 7) opnd2 315 in 316 SHIFT_IMMEDIATE2 shift sh rm C`; 317 318val SHIFT_REGISTER_def = Define` 319 SHIFT_REGISTER reg mode C (opnd2:word12) = 320 let Rs = (11 >< 8) opnd2 321 and Rm = (3 >< 0) opnd2 in 322 let sh = (6 >< 5) opnd2 323 and rm = REG_READ (INC_PC reg) mode Rm 324 and shift = (7 >< 0) (REG_READ reg mode Rs) in 325 SHIFT_REGISTER2 shift sh rm C`; 326 327val ADDR_MODE1_def = Define` 328 ADDR_MODE1 reg mode C Im opnd2 = 329 if Im then 330 IMMEDIATE C opnd2 331 else if opnd2 ' 4 then 332 SHIFT_REGISTER reg mode C opnd2 333 else 334 SHIFT_IMMEDIATE reg mode C opnd2`; 335 336(* ......................................................................... *) 337 338val ALU_arith_def = Define` 339 ALU_arith op (rn:word32) (op2:word32) = 340 let sign = word_msb rn 341 and (q,r) = DIVMOD_2EXP 32 (op (w2n rn) (w2n op2)) in 342 let res = (n2w r):word32 in 343 ((word_msb res,r = 0,ODD q, 344 (word_msb op2 = sign) /\ ~(word_msb res = sign)),res)`; 345 346val ALU_logic_def = Define` 347 ALU_logic (res:word32) = ((word_msb res,res = 0w,F,F),res)`; 348 349val ADD_def = Define` 350 ADD a b c = ALU_arith (\x y.x+y+(if c then 1 else 0)) a b`; 351 352val SUB_def = Define`SUB a b c = ADD a (~b) c`; 353val AND_def = Define`AND a b = ALU_logic (a && b)`; 354val EOR_def = Define`EOR a b = ALU_logic (a ?? b)`; 355val ORR_def = Define`ORR a b = ALU_logic (a || b)`; 356 357val ALU_def = Define` 358 ALU (opc:word4) rn op2 c = 359 case opc of 360 0w => AND rn op2 361 | 1w => EOR rn op2 362 | 2w => SUB rn op2 T 363 | 4w => ADD rn op2 F 364 | 3w => SUB op2 rn T 365 | 5w => ADD rn op2 c 366 | 6w => SUB rn op2 c 367 | 7w => SUB op2 rn c 368 | 8w => AND rn op2 369 | 9w => EOR rn op2 370 | 10w => SUB rn op2 T 371 | 11w => ADD rn op2 F 372 | 12w => ORR rn op2 373 | 13w => ALU_logic op2 374 | 14w => AND rn (~op2) 375 | _ => ALU_logic (~op2)`; 376 377(* ......................................................................... *) 378 379val ARITHMETIC_def = Define` 380 ARITHMETIC (opcode:word4) = 381 (opcode ' 2 \/ opcode ' 1) /\ (~(opcode ' 3) \/ ~(opcode ' 2))`; 382 383val TEST_OR_COMP_def = Define` 384 TEST_OR_COMP (opcode:word4) = ((3 -- 2 ) opcode = 2w)`; 385 386val DECODE_DATAP_def = Define` 387 DECODE_DATAP (w:word32) = 388 (w ' 25,(24 >< 21) w,w ' 20,(19 >< 16) w,(15 >< 12) w,(11 >< 0) w)`; 389 390val DATA_PROCESSING_def = Define` 391 DATA_PROCESSING r C mode ireg = 392 let (I,opcode,S,Rn,Rd,opnd2) = DECODE_DATAP ireg in 393 let (C_s,op2) = ADDR_MODE1 r.reg mode C I opnd2 394 and pc_reg = INC_PC r.reg in 395 let rn = REG_READ (if ~I /\ (opnd2 ' 4) then pc_reg else r.reg) mode Rn in 396 let ((N,Z,C_alu,V),res) = ALU opcode rn op2 C 397 and tc = TEST_OR_COMP opcode in 398 <| reg := if tc then pc_reg else REG_WRITE pc_reg mode Rd res; 399 psr := if S then 400 CPSR_WRITE r.psr 401 (if (Rd = 15w) /\ ~tc then SPSR_READ r.psr mode 402 else (if ARITHMETIC opcode 403 then SET_NZCV (N,Z,C_alu,V) 404 else SET_NZC (N,Z,C_s)) (CPSR_READ r.psr)) 405 else r.psr |>`; 406 407(* ------------------------------------------------------------------------- *) 408(* The PSR Transfer instruction class (mrs and msr) *) 409(* ------------------------------------------------------------------------- *) 410 411val DECODE_MRS_def = Define `DECODE_MRS (w:word32) = (w ' 22,(15 >< 12) w)`; 412 413val MRS_def = Define` 414 MRS r mode ireg = 415 let (R,Rd) = DECODE_MRS ireg in 416 let word = if R then SPSR_READ r.psr mode else CPSR_READ r.psr in 417 <| reg := REG_WRITE (INC_PC r.reg) mode Rd word; psr := r.psr |>`; 418 419(* ......................................................................... *) 420 421val DECODE_MSR_def = Define` 422 DECODE_MSR (w:word32) = 423 (w ' 25,w ' 22,w ' 19,w ' 16,(3 >< 0) w,(11 >< 0) w)`; 424 425val MSR_def = Define` 426 MSR r mode ireg = 427 let (I,R,bit19,bit16,Rm,opnd) = DECODE_MSR ireg in 428 if (USER mode /\ (R \/ (~bit19 /\ bit16))) \/ (~bit19 /\ ~bit16) then 429 <| reg := INC_PC r.reg; psr := r.psr |> 430 else 431 let psrd = if R then SPSR_READ r.psr mode else CPSR_READ r.psr 432 and src = if I then SND (IMMEDIATE F opnd) else REG_READ r.reg mode Rm in 433 let psrd' = word_modify 434 (\i b. (28 <= i) /\ (if bit19 then src ' i else b) \/ 435 (8 <= i) /\ (i <= 27) /\ b \/ 436 (i <= 7) /\ (if bit16 /\ ~USER mode then src ' i else b)) 437 psrd 438 in 439 <| reg := INC_PC r.reg; 440 psr := if R then 441 SPSR_WRITE r.psr mode psrd' 442 else 443 CPSR_WRITE r.psr psrd' |>`; 444 445(* ------------------------------------------------------------------------- *) 446(* The Multiply instruction class (mla_mul) *) 447(* ------------------------------------------------------------------------- *) 448 449val ALU_multiply_def = Define` 450 ALU_multiply L Sgn A rd rn rs rm = 451 let res = (if A then 452 if L then rd @@ rn else w2w rn 453 else 454 0w:word64) + 455 (if L /\ Sgn then 456 sw2sw rm * sw2sw rs 457 else 458 w2w rm * w2w rs) in 459 let resHi = (63 >< 32) res 460 and resLo = (31 >< 0) res in 461 if L then 462 (word_msb res,res = 0w,resHi,resLo) 463 else 464 (word_msb resLo,resLo = 0w,rd,resLo)`; 465 466val DECODE_MLA_MUL_def = Define` 467 DECODE_MLA_MUL (w:word32) = (w ' 23,w ' 22,w ' 21,w ' 20, 468 (19 >< 16) w,(15 >< 12) w,(11 >< 8) w,(3 >< 0) w)`; 469 470val MLA_MUL_def = Define` 471 MLA_MUL r mode ireg = 472 let (L,Sgn,A,S,Rd,Rn,Rs,Rm) = DECODE_MLA_MUL ireg in 473 let pc_reg = INC_PC r.reg in 474 let rd = REG_READ r.reg mode Rd 475 and rn = REG_READ r.reg mode Rn 476 and rs = REG_READ r.reg mode Rs 477 and rm = REG_READ r.reg mode Rm in 478 let (N,Z,resHi,resLo) = ALU_multiply L Sgn A rd rn rs rm in 479 if (Rd = 15w) \/ (Rd = Rm) \/ 480 L /\ ((Rn = 15w) \/ (Rn = Rm) \/ (Rd = Rn)) then 481 <| reg := pc_reg; psr := r.psr |> 482 else 483 <| reg := if L then 484 REG_WRITE (REG_WRITE pc_reg mode Rn resLo) mode Rd resHi 485 else 486 REG_WRITE pc_reg mode Rd resLo; 487 psr := if S then 488 CPSR_WRITE r.psr (SET_NZ (N,Z) (CPSR_READ r.psr)) 489 else 490 r.psr |>`; 491 492(* ------------------------------------------------------------------------- *) 493(* The Single Data Transfer instruction class (ldr_str) *) 494(* ------------------------------------------------------------------------- *) 495 496val UP_DOWN_def = Define`UP_DOWN u = if u then $word_add else $word_sub`; 497 498val ADDR_MODE2_def = Define` 499 ADDR_MODE2 reg mode C Im P U Rn offset = 500 let addr = REG_READ reg mode Rn in 501 let wb_addr = UP_DOWN U addr 502 (if Im then SND (SHIFT_IMMEDIATE reg mode C offset) 503 else w2w offset) in 504 (if P then wb_addr else addr,wb_addr)`; 505 506val DECODE_LDR_STR_def = Define` 507 DECODE_LDR_STR (w:word32) = 508 (w ' 25,w ' 24,w ' 23,w ' 22,w ' 21,w ' 20, 509 (19 >< 16) w,(15 >< 12) w,(11 >< 0) w)`; 510 511val LDR_STR_def = Define` 512 LDR_STR r C mode ireg input = 513 let (I,P,U,B,W,L,Rn,Rd,offset) = DECODE_LDR_STR ireg in 514 let (addr,wb_addr) = ADDR_MODE2 r.reg mode C I P U Rn offset in 515 let pc_reg = INC_PC r.reg in 516 case input of 517 NONE => INL 518 [if L then 519 MemRead addr 520 else 521 let w = REG_READ pc_reg mode Rd in 522 MemWrite addr (if B then Byte ((7 >< 0) w) else Word w)] 523 | SOME (isdabort, data) => 524 let wb_reg = if P ==> W then 525 REG_WRITE pc_reg mode Rn wb_addr 526 else 527 pc_reg 528 in INR 529 <| reg := 530 if L ==> isdabort then 531 wb_reg 532 else let fmt = if B then UnsignedByte else UnsignedWord in 533 REG_WRITE wb_reg mode Rd 534 (FORMAT fmt ((1 >< 0) addr) (HD data)); 535 psr := r.psr |>`; 536 537(* ------------------------------------------------------------------------- *) 538(* Half Word Single Data Transfer instruction class (ldrh_strh) *) 539(* ------------------------------------------------------------------------- *) 540 541val ADDR_MODE3_def = Define` 542 ADDR_MODE3 reg mode Im P U Rn offsetH offsetL = 543 let addr = REG_READ reg mode Rn in 544 let wb_addr = UP_DOWN U addr 545 (if Im then offsetH @@ offsetL 546 else REG_READ reg mode offsetL) in 547 (if P then wb_addr else addr,wb_addr)`; 548 549val DECODE_LDRH_STRH_def = Define` 550 DECODE_LDRH_STRH (w:word32) = 551 (w ' 24,w ' 23,w ' 22,w ' 21,w ' 20, 552 (19 >< 16) w,(15 >< 12) w,(11 >< 8) w,w ' 6,w ' 5,(3 >< 0) w)`; 553 554val LDRH_STRH_def = Define` 555 LDRH_STRH r mode ireg input = 556 let (P,U,I,W,L,Rn,Rd,offsetH,S,H,offsetL) = DECODE_LDRH_STRH ireg in 557 let (addr,wb_addr) = ADDR_MODE3 r.reg mode I P U Rn offsetH offsetL in 558 let pc_reg = INC_PC r.reg in 559 case input of 560 NONE => INL 561 [if L then 562 MemRead addr 563 else 564 MemWrite addr (Half ((15 >< 0) (REG_READ pc_reg mode Rd)))] 565 | SOME (isdabort, data) => 566 let wb_reg = if P ==> W then 567 REG_WRITE pc_reg mode Rn wb_addr 568 else 569 pc_reg 570 in INR 571 <| reg := 572 if L ==> isdabort then 573 wb_reg 574 else 575 let fmt = case (S, H) of 576 (F,T) => UnsignedHalfWord 577 | (T,F) => SignedByte 578 | (T,T) => SignedHalfWord 579 | _ => ARB 580 in 581 REG_WRITE wb_reg mode Rd 582 (FORMAT fmt ((1 >< 0) addr) (HD data)); 583 psr := r.psr |>`; 584 585(* ------------------------------------------------------------------------- *) 586(* The Block Data Transfer instruction class (ldm_stm) *) 587(* ------------------------------------------------------------------------- *) 588 589val REGISTER_LIST_def = Define` 590 REGISTER_LIST (list:word16) = 591 (MAP SND o FILTER FST) (GENLIST (\i. (list ' i,(n2w i):word4)) 16)`; 592 593val ADDRESS_LIST_def = Define` 594 ADDRESS_LIST (start:word32) n = GENLIST (\i. start + 4w * n2w i) n`; 595 596val WB_ADDRESS_def = Define` 597 WB_ADDRESS U base len = UP_DOWN U base (n2w (4 * len):word32)`; 598 599val FIRST_ADDRESS_def = Define` 600 FIRST_ADDRESS P U (base:word32) wb = 601 if U then if P then base + 4w else base 602 else if P then wb else wb + 4w`; 603 604val ADDR_MODE4_def = Define` 605 ADDR_MODE4 P U base (list:word16) = 606 let rp_list = REGISTER_LIST list in 607 let len = LENGTH rp_list in 608 let wb = WB_ADDRESS U base len in 609 let addr_list = ADDRESS_LIST (FIRST_ADDRESS P U base wb) len in 610 (rp_list,addr_list,wb)`; 611 612val LDM_LIST_def = Define` 613 LDM_LIST reg mode rp_list data = 614 FOLDL (\reg' (rp,rd). REG_WRITE reg' mode rp rd) reg (ZIP (rp_list,data))`; 615 616val STM_LIST_def = Define` 617 STM_LIST reg mode bl_list = 618 MAP (\(rp,addr). MemWrite addr (Word (REG_READ reg mode rp))) bl_list`; 619 620val DECODE_LDM_STM_def = Define` 621 DECODE_LDM_STM (w:word32) = 622 (w ' 24,w ' 23,w ' 22,w ' 21,w ' 20,(19 >< 16) w,(15 >< 0) w)`; 623 624val LDM_STM_def = Define` 625 LDM_STM r mode ireg input = 626 let (P,U,S,W,L,Rn,list) = DECODE_LDM_STM ireg in 627 let pc_in_list = list ' 15 628 and rn = REG_READ r.reg mode Rn in 629 let (rp_list,addr_list,rn') = ADDR_MODE4 P U rn list 630 and mode' = if S /\ (L ==> ~pc_in_list) then usr else mode 631 and pc_reg = INC_PC r.reg in 632 let wb_reg = if W /\ ~(Rn = 15w) then 633 REG_WRITE pc_reg (if L then mode else mode') Rn rn' 634 else 635 pc_reg 636 in 637 case input of 638 NONE => INL 639 (if L then 640 MAP MemRead addr_list 641 else 642 STM_LIST (if HD rp_list = Rn then pc_reg else wb_reg) mode' 643 (ZIP (rp_list,addr_list))) 644 | SOME (dabort_t, data) => INR 645 (if L then 646 <| reg := 647 let t = if IS_SOME dabort_t then 648 THE dabort_t 649 else 650 LENGTH rp_list in 651 let ldm_reg = LDM_LIST wb_reg mode' (FIRSTN t rp_list) 652 (FIRSTN t data) in 653 if IS_SOME dabort_t /\ ~(Rn = 15w) then 654 REG_WRITE ldm_reg mode' Rn (REG_READ wb_reg mode' Rn) 655 else ldm_reg; 656 psr := if S /\ pc_in_list /\ IS_NONE dabort_t then 657 CPSR_WRITE r.psr (SPSR_READ r.psr mode) 658 else r.psr |> 659 else <| reg := wb_reg; psr := r.psr |>)`; 660 661(* ------------------------------------------------------------------------- *) 662(* The Single Data Swap instruction class (swp) *) 663(* ------------------------------------------------------------------------- *) 664 665val DECODE_SWP_def = Define` 666 DECODE_SWP (w:word32) = (w ' 22,(19 >< 16) w,(15 >< 12) w,(3 >< 0) w)`; 667 668val SWP_def = Define` 669 SWP r mode ireg input = 670 let (B,Rn,Rd,Rm) = DECODE_SWP ireg in 671 let rn = REG_READ r.reg mode Rn 672 and pc_reg = INC_PC r.reg in 673 let rm = REG_READ pc_reg mode Rm in 674 case input of 675 NONE => INL 676 [MemRead rn; 677 MemWrite rn (if B then Byte ((7 >< 0) rm) else Word rm)] 678 | SOME (isdabort, data) => INR 679 <| reg := 680 if isdabort then 681 pc_reg 682 else let fmt = if B then UnsignedByte else UnsignedWord in 683 REG_WRITE pc_reg mode Rd 684 (FORMAT fmt ((1 >< 0) rn) (HD data)); 685 psr := r.psr |>`; 686 687(* ------------------------------------------------------------------------- *) 688(* Coprocessor Register Transfer (mrc, mcr) *) 689(* ------------------------------------------------------------------------- *) 690 691val DECODE_MRC_MCR_def = Define` 692 DECODE_MRC_MCR (w:word32) = 693 ((23 >< 21) w,(19 >< 16) w,(15 >< 12) w, 694 (11 >< 8) w, (7 >< 5) w,(3 >< 0) w)`; 695 696val MRC_def = Define` 697 MRC r mode data ireg = 698 let Rd = (15 >< 12) ireg 699 and pc_reg = INC_PC r.reg in 700 if Rd = 15w then 701 <| reg := pc_reg; 702 psr := CPSR_WRITE r.psr (SET_NZCV (NZCV data) (CPSR_READ r.psr)) |> 703 else 704 <| reg := REG_WRITE pc_reg mode Rd data; psr := r.psr |>`; 705 706val MCR_OUT_def = Define` 707 MCR_OUT reg mode ireg = 708 let Rd = (15 >< 12) ireg in 709 [CPWrite (REG_READ (INC_PC reg) mode Rd)]`; 710 711(* ------------------------------------------------------------------------- *) 712(* Coprocessor Data Transfers (ldc_stc) *) 713(* ------------------------------------------------------------------------- *) 714 715val DECODE_LDC_STC_def = Define` 716 DECODE_LDC_STC (w:word32) = 717 (w ' 24,w ' 23,w ' 22,w ' 21,w ' 20, 718 (19 >< 16) w,(15 >< 12) w,(11 >< 8) w,(7 >< 0) w)`; 719 720val ADDR_MODE5_def = Define` 721 ADDR_MODE5 reg mode P U Rn (offset:word8) = 722 let addr = REG_READ reg mode Rn in 723 let wb_addr = UP_DOWN U addr (w2w offset << 2) in 724 (if P then wb_addr else addr,wb_addr)`; 725 726val LDC_STC_def = Define` 727 LDC_STC r mode ireg input = 728 let (P,U,N,W,L,Rn,CRd,CPN,offset) = DECODE_LDC_STC ireg in 729 let (addr,wb_addr) = ADDR_MODE5 r.reg mode P U Rn offset in 730 if input then 731 let pc_reg = INC_PC r.reg in 732 let wb_reg = if W /\ ~(Rn = 15w) then 733 REG_WRITE pc_reg mode Rn wb_addr 734 else 735 pc_reg 736 in 737 INR <| reg := wb_reg; psr := r.psr |> 738 else 739 INL [if L then MemRead addr else MemWrite addr ARB]`; 740 741(* ------------------------------------------------------------------------- *) 742(* Predicate for conditional execution *) 743(* ------------------------------------------------------------------------- *) 744 745val CONDITION_PASSED2_def = Define` 746 CONDITION_PASSED2 (N,Z,C,V) cond = 747 case cond of 748 EQ => Z 749 | NE => ~Z 750 | CS => C 751 | CC => ~C 752 | MI => N 753 | PL => ~N 754 | VS => V 755 | VC => ~V 756 | HI => C /\ ~Z 757 | LS => ~C \/ Z 758 | GE => N = V 759 | LT => ~(N = V) 760 | GT => ~Z /\ (N = V) 761 | LE => Z \/ ~(N = V) 762 | AL => T 763 | NV => F`; 764 765val CONDITION_PASSED_def = Define` 766 CONDITION_PASSED flags (ireg:word32) = 767 let pass = CONDITION_PASSED2 flags (num2condition (w2n ((31 -- 29) ireg))) 768 in 769 if ireg ' 28 then ~pass else pass`; 770 771(* ------------------------------------------------------------------------- *) 772(* Top-level decode and run functions *) 773(* ------------------------------------------------------------------------- *) 774 775val DECODE_ARM_def = Define` 776 DECODE_ARM (ireg : word32) = 777 let b n = ireg ' n in 778 case (b 27,b 26,b 25,b 24,b 23,b 22,b 21,b 20,b 7,b 6,b 5,b 4) of 779 (F,F,F,T,F,_,F,F,F,F,F,F) => mrs 780 | (F,F,F,T,F,_,T,F,F,F,F,F) => msr 781 | (F,F,F,_,_,_,_,_,_,_,_,F) => data_proc 782 | (F,F,F,_,_,_,_,_,F,_,_,T) => data_proc 783 | (F,F,F,F,F,F,_,_,T,F,F,T) => mla_mul 784 | (F,F,F,F,T,_,_,_,T,F,F,T) => mla_mul 785 | (F,F,F,T,F,_,F,F,T,F,F,T) => swp 786 | (F,F,F,_,_,_,_,_,T,F,T,T) => ldrh_strh 787 | (F,F,F,_,_,_,_,T,T,T,_,T) => ldrh_strh 788 | (F,F,T,T,F,_,F,F,_,_,_,_) => cdp_und 789 | (F,F,T,T,F,_,T,F,_,_,_,_) => msr 790 | (F,F,T,_,_,_,_,_,_,_,_,_) => data_proc 791 | (F,T,F,_,_,_,_,_,_,_,_,_) => ldr_str 792 | (F,T,T,_,_,_,_,_,_,_,_,F) => ldr_str 793 | (T,F,F,_,_,_,_,_,_,_,_,_) => ldm_stm 794 | (T,F,T,_,_,_,_,_,_,_,_,_) => br 795 | (T,T,F,_,_,_,_,_,_,_,_,_) => ldc_stc 796 | (T,T,T,F,_,_,_,T,_,_,_,T) => mrc 797 | (T,T,T,F,_,_,_,F,_,_,_,T) => mcr 798 | (T,T,T,T,_,_,_,_,_,_,_,_) => swi_ex 799 | _ => cdp_und`; 800 801val RUN_ARM_def = Define` 802 RUN_ARM state (dabt:num option) data no_cp = 803 let ireg = state.ireg and r = state.regs 804 and inc_pc x = <| reg := INC_PC x.reg; psr := x.psr |> 805 in 806 if ~(state.exception = software) then 807 EXCEPTION r state.exception 808 else let (nzcv,i,f,m) = DECODE_PSR (CPSR_READ r.psr) in 809 if ~CONDITION_PASSED nzcv ireg then 810 inc_pc r 811 else let mode = DECODE_MODE m 812 and coproc f = if no_cp then r else f r 813 in 814 case DECODE_ARM ireg of 815 data_proc => DATA_PROCESSING r (CARRY nzcv) mode ireg 816 | mla_mul => MLA_MUL r mode ireg 817 | swi_ex => EXCEPTION r software 818 | br => BRANCH r mode ireg 819 | msr => MSR r mode ireg 820 | mrs => MRS r mode ireg 821 | swp => OUTR (SWP r mode ireg (SOME (IS_SOME dabt, data))) 822 | ldm_stm => OUTR (LDM_STM r mode ireg (SOME (dabt, data))) 823 | ldr_str => OUTR 824 (LDR_STR r (CARRY nzcv) mode ireg (SOME (IS_SOME dabt, data))) 825 | ldrh_strh => OUTR 826 (LDRH_STRH r mode ireg (SOME (IS_SOME dabt, data))) 827 | ldc_stc => coproc (\x. (OUTR (LDC_STC x mode ireg T))) 828 | mrc => coproc (\x. MRC x mode (ELL 1 data) ireg) 829 | mcr => coproc inc_pc 830 | cdp_und => coproc inc_pc 831 | _ => r`; 832 833(* ------------------------------------------------------------------------- *) 834(* Exception operations *) 835(* ------------------------------------------------------------------------- *) 836 837val IS_Reset_def = Define` 838 (IS_Reset (SOME (Reset x)) = T) /\ (IS_Reset _ = F)`; 839 840val PROJ_Reset_def = Define` 841 PROJ_Reset (SOME (Reset x)) = x`; 842 843val PROJ_Dabort_def = Define` 844 (PROJ_Dabort (SOME (Dabort x)) = SOME x) /\ 845 (PROJ_Dabort _ = NONE)`; 846 847val interrupt2exception_def = Define` 848 interrupt2exception state (i',f') irpt = 849 let ireg = state.ireg in 850 let (flags,i,f,m) = DECODE_PSR (CPSR_READ state.regs.psr) in 851 let pass = (state.exception = software) /\ CONDITION_PASSED flags ireg 852 and ic = DECODE_ARM ireg in 853 let old_flags = pass /\ ((ic = mrs) \/ (ic = msr)) in 854 (case irpt of 855 NONE => software 856 | SOME (Reset x) => reset 857 | SOME Prefetch => pabort 858 | SOME (Dabort t) => dabort 859 | SOME Undef => if pass /\ ic IN {cdp_und; mrc; mcr; ldc_stc} then 860 undefined 861 else 862 software 863 | SOME Fiq => if (if old_flags then f else f') then 864 software 865 else 866 fast 867 | SOME Irq => if (if old_flags then i else i') then 868 software 869 else 870 interrupt)`; 871 872val PROJ_IF_FLAGS_def = Define` 873 PROJ_IF_FLAGS psr = 874 let (flags,i,f,m) = DECODE_PSR (CPSR_READ psr) in (i,f)`; 875 876(* ------------------------------------------------------------------------- *) 877(* The next state, output and state functions *) 878(* ------------------------------------------------------------------------- *) 879 880val NEXT_ARM_def = Define` 881 NEXT_ARM state inp = 882 let r = if IS_Reset inp.interrupt then 883 PROJ_Reset inp.interrupt 884 else 885 RUN_ARM state (PROJ_Dabort inp.interrupt) inp.data inp.no_cp 886 in 887 <| regs := r; ireg := inp.ireg; 888 exception := 889 interrupt2exception state (PROJ_IF_FLAGS r.psr) inp.interrupt |>`; 890 891val OUT_ARM_def = Define` 892 OUT_ARM state = 893 let ireg = state.ireg and r = state.regs in 894 let (nzcv,i,f,m) = DECODE_PSR (CPSR_READ r.psr) in 895 let mode = DECODE_MODE m in 896 if (state.exception = software) /\ CONDITION_PASSED nzcv ireg then 897 let ic = DECODE_ARM ireg in 898 <| transfers := 899 (case ic of 900 ldr_str => OUTL (LDR_STR r (CARRY nzcv) mode ireg NONE) 901 | ldrh_strh => OUTL (LDRH_STRH r mode ireg NONE) 902 | ldm_stm => OUTL (LDM_STM r mode ireg NONE) 903 | swp => OUTL (SWP r mode ireg NONE) 904 | ldc_stc => OUTL (LDC_STC r mode ireg F) 905 | mcr => MCR_OUT r.reg mode ireg 906 | _ => []); 907 cpi := (ic IN {cdp_und; mcr; mrc; ldc_stc}); 908 user := USER mode 909 |> 910 else 911 <| transfers := []; cpi := F; user := USER mode |>`; 912 913val STATE_ARM_def = Define` 914 (STATE_ARM 0 x = x.state) /\ 915 (STATE_ARM (SUC t) x = NEXT_ARM (STATE_ARM t x) (x.inp t))`; 916 917val ARM_SPEC_def = Define` 918 ARM_SPEC t x = let s = STATE_ARM t x in <| state := s; out := OUT_ARM s |>`; 919 920(* ------------------------------------------------------------------------- *) 921 922val _ = computeLib.add_persistent_funs 923 (["pred_set.IN_INSERT", 924 "pred_set.NOT_IN_EMPTY"] @ 925 ["register_EQ_register","num2register_thm","register2num_thm", "mode_EQ_mode", 926 "mode2num_thm", "psr_EQ_psr", "psr2num_thm", "iclass_EQ_iclass", 927 "iclass2num_thm", "num2condition_thm", "condition2num_thm", 928 "exceptions_EQ_exceptions", "num2exceptions_thm", "exceptions2num_thm"]) 929 930val _ = export_theory(); 931