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