1(* ========================================================================= *) 2(* FILE : systemScript.sml *) 3(* DESCRIPTION : Model of a basic ARM system, with upto 16 coprocessors *) 4(* plus main memory. *) 5(* AUTHOR : Anthony Fox (with some contributions by Juliano Iyoda) *) 6(* University of Cambridge *) 7(* DATE : 2005 - 2006 *) 8(* ========================================================================= *) 9 10(* interactive use: 11 app load ["wordsLib", "wordsSyntax", "armTheory"]; 12*) 13 14open HolKernel boolLib bossLib Parse; 15open Q wordsTheory rich_listTheory updateTheory armTheory; 16 17val _ = new_theory "system"; 18 19(* -------------------------------------------------------------------------- *) 20(* In what follows, the term "cp" stands for "coprocessor". *) 21(* -------------------------------------------------------------------------- *) 22 23(* -------------------------------------------------------------------------- *) 24(* Memory + CP and bus output *) 25(* -------------------------------------------------------------------------- *) 26 27val _ = type_abbrev("mem", ``:word30->word32``); 28 29val _ = Hol_datatype` 30 cp_output = <| data : word32 option list; absent : bool |>`; 31 32val _ = Hol_datatype `bus = 33 <| data : word32 list; 34 memory : mem; 35 abort : num option; 36 cp_state : 'a 37 |>`; 38 39(* -------------------------------------------------------------------------- *) 40(* The system state *) 41(* -------------------------------------------------------------------------- *) 42 43val _ = Hol_datatype `arm_sys_state = 44 <| registers : registers; 45 psrs : psrs; 46 memory : mem; 47 undefined : bool; 48 cp_state : 'a 49 |>`; 50 51(* -------------------------------------------------------------------------- *) 52(* The model is paramaterised by a collection of coprocessor operations *) 53(* i.e. cdp, mrc, mcr, stc and ldc functions: *) 54(* *) 55(* absent: is_usr ireg => bool ... which instructions are accepted *) 56(* *) 57(* f_cdp : state is_usr ireg => state ... operation for CDP instruction *) 58(* *) 59(* f_mrc : state is_usr ireg => word32 ... output for MRC instruction *) 60(* *) 61(* f_mcr : state is_usr ireg data => state *) 62(* ... operation for MCR instruction *) 63(* *) 64(* f_stc : state is_usr ireg => word32 option list *) 65(* ... output for STC instruction *) 66(* *) 67(* f_ldc : state is_usr ireg data => state *) 68(* ... operation for LDC instruction *) 69(* *) 70(* n_ldc : state is_usr ireg => num ... number of words to load *) 71(* *) 72(* -------------------------------------------------------------------------- *) 73 74val _ = Hol_datatype `coproc = 75 <| absent : bool -> word32 -> bool; 76 f_cdp : 'a -> bool -> word32 -> 'a; 77 f_mrc : 'a -> bool -> word32 -> word32; 78 f_mcr : 'a -> bool -> word32 -> word32 -> 'a; 79 f_stc : 'a -> bool -> word32 -> word32 option list; 80 f_ldc : 'a -> bool -> word32 -> word32 list -> 'a; 81 n_ldc : 'a -> bool -> word32 -> num 82 |>`; 83 84(* -------------------------------------------------------------------------- *) 85(* ADD_COPROC *) 86(* Add a new coprocessor (cp1) to an existing specification (cp2) *) 87(* -------------------------------------------------------------------------- *) 88 89val ADD_COPROC = Define` 90 ADD_COPROC (cp1:'a coproc) (cp2:'b coproc) = 91 <| absent := \is_usr ireg. cp1.absent is_usr ireg /\ cp2.absent is_usr ireg; 92 f_cdp := \state is_usr ireg. 93 (if cp1.absent is_usr ireg then 94 FST state 95 else 96 cp1.f_cdp (FST state) is_usr ireg, 97 if cp2.absent is_usr ireg then 98 SND state 99 else 100 cp2.f_cdp (SND state) is_usr ireg); 101 f_mrc := \state is_usr ireg. 102 if cp1.absent is_usr ireg then 103 cp2.f_mrc (SND state) is_usr ireg 104 else 105 cp1.f_mrc (FST state) is_usr ireg; 106 f_mcr := \state is_usr ireg data. 107 (if cp1.absent is_usr ireg then 108 FST state 109 else 110 cp1.f_mcr (FST state) is_usr ireg data, 111 if cp2.absent is_usr ireg then 112 SND state 113 else 114 cp2.f_mcr (SND state) is_usr ireg data); 115 f_stc := \state is_usr ireg. 116 if cp1.absent is_usr ireg then 117 cp2.f_stc (SND state) is_usr ireg 118 else 119 cp1.f_stc (FST state) is_usr ireg; 120 f_ldc := \state is_usr ireg data. 121 (if cp1.absent is_usr ireg then 122 FST state 123 else 124 cp1.f_ldc (FST state) is_usr ireg data, 125 if cp2.absent is_usr ireg then 126 SND state 127 else 128 cp2.f_ldc (SND state) is_usr ireg data); 129 n_ldc := \state is_usr ireg. 130 if cp1.absent is_usr ireg then 131 cp2.n_ldc (SND state) is_usr ireg 132 else 133 cp1.n_ldc (FST state) is_usr ireg 134 |>`; 135 136(* -------------------------------------------------------------------------- *) 137(* CPN *) 138(* Returns the coprocessor number from the instruction *) 139(* -------------------------------------------------------------------------- *) 140 141val _ = wordsLib.guess_lengths(); 142 143val DECODE_CPN_def = Define `DECODE_CPN (w:word32) = (11 >< 8) w`; 144 145(* -------------------------------------------------------------------------- *) 146(* DECODE_CDP *) 147(* -------------------------------------------------------------------------- *) 148 149val DECODE_CDP_def = Define` 150 DECODE_CDP (w:word32) = 151 ((23 >< 20) w, (* Cop1 *) 152 (19 >< 16) w, (* CRn *) 153 (15 >< 12) w, (* CRd *) 154 (11 >< 8) w, (* CPN *) 155 (7 >< 5) w, (* Cop2 *) 156 (3 >< 0) w)`; (* CRm *) 157 158(* -------------------------------------------------------------------------- *) 159(* DECODE_CP *) 160(* Determines the instruction class ** for a coprocessor instruction ** *) 161(* -------------------------------------------------------------------------- *) 162 163val DECODE_CP_def = Define` 164 DECODE_CP (w:word32) = 165 if w ' 25 then 166 if w ' 4 /\ w ' 27 then 167 if w ' 20 then 168 mrc 169 else 170 mcr 171 else 172 cdp_und 173 else 174 ldc_stc`; 175 176(* -------------------------------------------------------------------------- *) 177(* OUT_CP *) 178(* It is assumed that only one coprocessor (i.e. "CP ireg") can accept the *) 179(* instruction but in general this need not be the case *) 180(* -------------------------------------------------------------------------- *) 181 182val OUT_CP_def = Define` 183 OUT_CP cp state ireg arm_out = 184 let is_usr = arm_out.user in 185 if arm_out.cpi /\ ireg ' 27 /\ ~cp.absent is_usr ireg then 186 <| data := 187 let ic = DECODE_CP ireg in 188 if ic = mrc then 189 [SOME (cp.f_mrc state is_usr ireg) ; NONE ] 190 else if (ic = ldc_stc) /\ ~(ireg ' 20) then 191 cp.f_stc state is_usr ireg 192 else 193 GENLIST (K NONE) (cp.n_ldc state is_usr ireg); 194 absent := F |> 195 else 196 <| data := []; absent := T |>`; 197 198(* -------------------------------------------------------------------------- *) 199(* RUN_CP *) 200(* Takes a CP state and the input (word32 list) and returns the next state *) 201(* -------------------------------------------------------------------------- *) 202 203val RUN_CP_def = Define` 204 RUN_CP cp state absent is_usr ireg data = 205 if ~absent then 206 let ic = DECODE_CP ireg in 207 if ic = mcr then 208 cp.f_mcr state is_usr ireg (HD data) 209 else if (ic = ldc_stc) /\ ireg ' 20 then 210 cp.f_ldc state is_usr ireg data 211 else if ic = cdp_und then 212 cp.f_cdp state is_usr ireg 213 else 214 state 215 else 216 state`; 217 218(* -------------------------------------------------------------------------- *) 219(* NEXT_ARM_SYS and STATE_ARM_SYS *) 220(* NB. Assumes that there are no prefetch aborts or hardware *) 221(* interrupts (fiq, irq) *) 222(* -------------------------------------------------------------------------- *) 223 224val addr30_def = Define `addr30 (x:word32) = (31 >< 2) x`; 225 226val NEXT_ARM_SYS_def = Define` 227 NEXT_ARM_SYS bus_op (cp:'a coproc) (state:'a arm_sys_state) = 228 let ireg = state.memory (addr30 (FETCH_PC state.registers)) in 229 let s = <| regs := <| reg := state.registers; psr := state.psrs |>; 230 ireg := ireg; 231 exception := if state.undefined then undefined else software |> 232 in 233 let arm_out = OUT_ARM s 234 in 235 let cp_out = OUT_CP cp state.cp_state ireg arm_out 236 in 237 let b = bus_op arm_out state.cp_state cp_out.data state.memory 238 in 239 let r = RUN_ARM s (if IS_SOME b.abort then 240 SOME (THE b.abort) 241 else 242 NONE) 243 b.data cp_out.absent 244 and p = RUN_CP cp b.cp_state cp_out.absent arm_out.user ireg b.data 245 in 246 <| registers := r.reg; psrs := r.psr; memory := b.memory; 247 undefined := (~state.undefined /\ arm_out.cpi /\ cp_out.absent); 248 cp_state := p |>`; 249 250val STATE_ARM_SYS_def = Define` 251 (STATE_ARM_SYS bus_op cp 0 s = s) /\ 252 (STATE_ARM_SYS bus_op cp (SUC t) s = 253 NEXT_ARM_SYS bus_op cp (STATE_ARM_SYS bus_op cp t s))`; 254 255(* -------------------------------------------------------------------------- *) 256(* An Idealistic Memory Model *) 257(* -------------------------------------------------------------------------- *) 258 259val SET_BYTE_def = Define` 260 SET_BYTE (oareg:word2) (b:word8) (w:word32) = 261 word_modify (\i x. 262 (i < 8) /\ (if oareg = 0w then b ' i else x) \/ 263 (8 <= i /\ i < 16) /\ (if oareg = 1w then b ' (i - 8) else x) \/ 264 (16 <= i /\ i < 24) /\ (if oareg = 2w then b ' (i - 16) else x) \/ 265 (24 <= i /\ i < 32) /\ (if oareg = 3w then b ' (i - 24) else x)) w`; 266 267val SET_HALF_def = Define` 268 SET_HALF (oareg:bool) (hw:word16) (w:word32) = 269 word_modify (\i x. 270 (i < 16) /\ (if ~oareg then hw ' i else x) \/ 271 (16 <= i /\ i < 32) /\ (if oareg then hw ' (i - 16) else x)) w`; 272 273val MEM_WRITE_BYTE_def = Define` 274 MEM_WRITE_BYTE (mem:mem) addr (word:word8) = 275 let a30 = addr30 addr in 276 (a30 =+ SET_BYTE ((1 >< 0) addr) word (mem a30)) mem`; 277 278val MEM_WRITE_HALF_def = Define` 279 MEM_WRITE_HALF (mem:mem) addr (word:word16) = 280 let a30 = addr30 addr in 281 (a30 =+ SET_HALF (addr ' 1) word (mem a30)) mem`; 282 283val MEM_WRITE_WORD_def = Define` 284 MEM_WRITE_WORD (mem:mem) addr word = (addr30 addr =+ word) mem`; 285 286val MEM_WRITE_def = Define` 287 MEM_WRITE mem addr d = 288 case d of 289 Byte b => MEM_WRITE_BYTE mem addr b 290 | Half hw => MEM_WRITE_HALF mem addr hw 291 | Word w => MEM_WRITE_WORD mem addr w`; 292 293val TRANSFER_def = Define` 294 TRANSFER cpi (cp_data,data,mem) t = 295 case t of 296 MemRead a => 297 if cpi then 298 let (f, b) = SPLITP IS_SOME cp_data in 299 (b, data ++ 300 MAP (\addr. mem (addr30 addr)) (ADDRESS_LIST a (LENGTH f)), mem) 301 else 302 (cp_data, data ++ [mem (addr30 a)], mem) 303 | MemWrite a d => 304 if cpi then 305 let (f, b) = SPLITP IS_NONE cp_data in 306 (b, data, 307 FOLDL (\m (addr,cpd). MEM_WRITE mem addr (Word (THE cpd))) 308 mem (ZIP (ADDRESS_LIST a (LENGTH f), f))) 309 else 310 (cp_data, data, MEM_WRITE mem a d) 311 | CPWrite w => 312 (cp_data, if cpi then data ++ [w] else data, mem)`; 313 314val TRANSFERS_def = Define` 315 TRANSFERS arm_out cp_state cp_data mem = 316 let (data, mem) = 317 if arm_out.cpi /\ NULL arm_out.transfers then 318 (MAP THE cp_data, mem) 319 else 320 SND (FOLDL (TRANSFER arm_out.cpi) (cp_data, [], mem) arm_out.transfers) 321 in 322 <| data := data; memory := mem; 323 abort := NONE; cp_state := cp_state |>`; 324 325(* -------------------------------------------------------------------------- *) 326(* NEXT_ARM_MMU *) 327(* -------------------------------------------------------------------------- *) 328 329val NEXT_ARM_MMU_def = Define `NEXT_ARM_MMU = NEXT_ARM_SYS TRANSFERS`; 330 331infix \\ << >> 332 333val op \\ = op THEN; 334val op << = op THENL; 335val op >> = op THEN1; 336 337val TRANSFERS = prove( 338 `(!arm_out p15_reg data mem. 339 (TRANSFERS arm_out cp_state data mem).abort = NONE) /\ 340 (!arm_out p15_reg data mem. 341 (TRANSFERS arm_out cp_state data mem).cp_state = cp_state)`, 342 SRW_TAC [] [TRANSFERS_def] \\ FULL_SIMP_TAC (srw_ss()) []); 343 344val NEXT_ARM_MMU = store_thm("NEXT_ARM_MMU", 345 `NEXT_ARM_MMU cp state = 346 let ireg = state.memory (addr30 (FETCH_PC state.registers)) in 347 let s = <| regs := <| reg := state.registers; psr := state.psrs |>; 348 ireg := ireg; 349 exception := if state.undefined then undefined else software |> 350 in 351 let arm_out = OUT_ARM s 352 in 353 let cp_out = OUT_CP cp state.cp_state ireg arm_out 354 in 355 let b = TRANSFERS arm_out state.cp_state cp_out.data state.memory 356 in 357 let r = RUN_ARM s NONE b.data cp_out.absent 358 and p = RUN_CP cp state.cp_state cp_out.absent arm_out.user ireg b.data 359 in 360 <| registers := r.reg; psrs := r.psr; memory := b.memory; 361 undefined := (~state.undefined /\ arm_out.cpi /\ cp_out.absent); 362 cp_state := p |>`, 363 SRW_TAC [boolSimps.LET_ss] [NEXT_ARM_SYS_def,NEXT_ARM_MMU_def,TRANSFERS]); 364 365val STATE_ARM_MMU_def = Define` 366 (STATE_ARM_MMU cp 0 s = s) /\ 367 (STATE_ARM_MMU cp (SUC t) s = NEXT_ARM_MMU cp (STATE_ARM_MMU cp t s))`; 368 369(* -------------------------------------------------------------------------- *) 370(* NEXT_ARM_MEM and STATE_ARM_MEM *) 371(* -------------------------------------------------------------------------- *) 372 373val NO_CP_def = Define `NO_CP = <| absent := \u i. T |> : 'a coproc`; 374 375val OUT_CP_NO_CPS = 376 SIMP_CONV (srw_ss()++boolSimps.LET_ss) [OUT_CP_def,NO_CP_def] 377 ``OUT_CP NO_CP state ireg arm_out``; 378 379val RUN_CP_NO_CPS = 380 SIMP_CONV (srw_ss()++boolSimps.LET_ss) [RUN_CP_def,NO_CP_def] 381 ``RUN_CP NO_CP state T is_usr ireg data``; 382 383val NEXT_ARM_MEM_def = Define `NEXT_ARM_MEM = NEXT_ARM_MMU NO_CP`; 384val STATE_ARM_MEM_def = Define `STATE_ARM_MEM = STATE_ARM_MMU NO_CP`; 385 386val NEXT_ARM_MEM = store_thm("NEXT_ARM_MEM", 387 `NEXT_ARM_MEM state = 388 let ireg = state.memory (addr30 (FETCH_PC state.registers)) in 389 let s = <| regs := <| reg := state.registers; psr := state.psrs |>; 390 ireg := ireg; 391 exception := if state.undefined then undefined else software |> 392 in 393 let arm_out = OUT_ARM s in 394 let mmu_out = TRANSFERS arm_out state.cp_state [] state.memory 395 in 396 let r = RUN_ARM s NONE mmu_out.data T 397 in 398 <| registers := r.reg; psrs := r.psr; memory := mmu_out.memory; 399 undefined := (~state.undefined /\ arm_out.cpi); 400 cp_state := state.cp_state |>`, 401 SRW_TAC [boolSimps.LET_ss] 402 [NEXT_ARM_MEM_def,NEXT_ARM_MMU,RUN_CP_NO_CPS,OUT_CP_NO_CPS]); 403 404(* ------------------------------------------------------------------------- *) 405(* Export ML versions of functions *) 406(*---------------------------------------------------------------------------*) 407 408val mem_read_def = Define`mem_read (m: mem, a) = m a`; 409val mem_write_def = Define`mem_write (m:mem) a d = (a =+ d) m`; 410val mem_write_block_def = Define`mem_write_block (m:mem) a cr = (a |: cr) m`; 411val mem_items_def = Define`mem_items (m:mem) = []:(word30 # word32) list`; 412val empty_memory_def = Define`empty_memory = (\a. 0xE6000010w):mem`; 413val empty_registers_def = Define`empty_registers = (\n. 0w):registers`; 414val empty_psrs_def = Define`empty_psrs = (\x. SET_IFMODE F F usr 0w):psrs`; 415 416(* ------------------------------------------------------------------------- *) 417 418open arithmeticTheory numeralTheory bitTheory; 419 420val std_ss = std_ss ++ boolSimps.LET_ss; 421val arith_ss = arith_ss ++ boolSimps.LET_ss; 422 423val word_ss = arith_ss++fcpLib.FCP_ss++wordsLib.SIZES_ss++ 424 rewrites [n2w_def,word_extract_def,word_bits_n2w,w2w, 425 BIT_def,BITS_THM,DIVMOD_2EXP_def,DIV_2EXP_def,DIV_1, 426 DIV2_def,ODD_MOD2_LEM,DIV_DIV_DIV_MULT,MOD_2EXP_def] 427 428val MOD_DIMINDEX_32 = (SIMP_RULE (std_ss++wordsLib.SIZES_ss) [] o 429 Thm.INST_TYPE [alpha |-> ``:32``]) MOD_DIMINDEX; 430 431val DECODE_TAC = SIMP_TAC std_ss [DECODE_PSR_def,DECODE_BRANCH_def, 432 DECODE_DATAP_def,DECODE_MRS_def,DECODE_MSR_def,DECODE_LDR_STR_def, 433 DECODE_LDRH_STRH_def,DECODE_MLA_MUL_def,DECODE_LDM_STM_def, 434 DECODE_SWP_def,DECODE_LDC_STC_def,DECODE_CDP_def,DECODE_MRC_MCR_def, 435 SHIFT_IMMEDIATE_def,SHIFT_REGISTER_def, 436 CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV rich_listTheory.GENLIST, 437 NZCV_def,REGISTER_LIST_def,rich_listTheory.SNOC,word_extract_def] 438 \\ SIMP_TAC word_ss []; 439 440val DECODE_PSR_THM = store_thm("DECODE_PSR_THM", 441 `!n. DECODE_PSR (n2w n) = 442 let (q0,m) = DIVMOD_2EXP 5 n in 443 let (q1,i) = DIVMOD_2EXP 1 (DIV2 q0) in 444 let (q2,f) = DIVMOD_2EXP 1 q1 in 445 let (q3,V) = DIVMOD_2EXP 1 (DIV_2EXP 20 q2) in 446 let (q4,C) = DIVMOD_2EXP 1 q3 in 447 let (q5,Z) = DIVMOD_2EXP 1 q4 in 448 ((ODD q5,Z=1,C=1,V=1),f = 1,i = 1,n2w m)`, DECODE_TAC); 449 450val DECODE_BRANCH_THM = store_thm("DECODE_BRANCH_THM", 451 `!n. DECODE_BRANCH (n2w n) = 452 let (L,offset) = DIVMOD_2EXP 24 n in (ODD L,n2w offset)`, DECODE_TAC); 453 454val DECODE_DATAP_THM = store_thm("DECODE_DATAP_THM", 455 `!n. DECODE_DATAP (n2w n) = 456 let (q0,opnd2) = DIVMOD_2EXP 12 n in 457 let (q1,Rd) = DIVMOD_2EXP 4 q0 in 458 let (q2,Rn) = DIVMOD_2EXP 4 q1 in 459 let (q3,S) = DIVMOD_2EXP 1 q2 in 460 let (q4,opcode) = DIVMOD_2EXP 4 q3 in 461 (ODD q4,n2w opcode,S = 1,n2w Rn,n2w Rd,n2w opnd2)`, DECODE_TAC); 462 463val DECODE_MRS_THM = store_thm("DECODE_MRS_THM", 464 `!n. DECODE_MRS (n2w n) = 465 let (q,Rd) = DIVMOD_2EXP 4 (DIV_2EXP 12 n) in 466 (ODD (DIV_2EXP 6 q),n2w Rd)`, DECODE_TAC); 467 468val DECODE_MSR_THM = store_thm("DECODE_MSR_THM", 469 `!n. DECODE_MSR (n2w n) = 470 let (q0,opnd) = DIVMOD_2EXP 12 n in 471 let (q1,bit16) = DIVMOD_2EXP 1 (DIV_2EXP 4 q0) in 472 let (q2,bit19) = DIVMOD_2EXP 1 (DIV_2EXP 2 q1) in 473 let (q3,R) = DIVMOD_2EXP 1 (DIV_2EXP 2 q2) in 474 (ODD (DIV_2EXP 2 q3),R = 1,bit19 = 1,bit16 = 1, 475 n2w (MOD_2EXP 4 opnd),n2w opnd)`, 476 DECODE_TAC \\ `4096 = 16 * 256n` by numLib.ARITH_TAC 477 \\ ASM_REWRITE_TAC [] \\ SIMP_TAC arith_ss [MOD_MULT_MOD]); 478 479val DECODE_LDR_STR_THM = store_thm("DECODE_LDR_STR_THM", 480 `!n. DECODE_LDR_STR (n2w n) = 481 let (q0,offset) = DIVMOD_2EXP 12 n in 482 let (q1,Rd) = DIVMOD_2EXP 4 q0 in 483 let (q2,Rn) = DIVMOD_2EXP 4 q1 in 484 let (q3,L) = DIVMOD_2EXP 1 q2 in 485 let (q4,W) = DIVMOD_2EXP 1 q3 in 486 let (q5,B) = DIVMOD_2EXP 1 q4 in 487 let (q6,U) = DIVMOD_2EXP 1 q5 in 488 let (q7,P) = DIVMOD_2EXP 1 q6 in 489 (ODD q7,P = 1,U = 1,B = 1,W = 1,L = 1,n2w Rn,n2w Rd,n2w offset)`, 490 DECODE_TAC); 491 492val DECODE_LDRH_STRH_THM = store_thm("DECODE_LDRH_STRH_THM", 493 `!n. DECODE_LDRH_STRH (n2w n) = 494 let (q0,offsetL) = DIVMOD_2EXP 4 n in 495 let (q1,H) = DIVMOD_2EXP 1 (DIV2 q0) in 496 let (q2,S) = DIVMOD_2EXP 1 q1 in 497 let (q3,offsetH) = DIVMOD_2EXP 4 (DIV2 q2) in 498 let (q4,Rd) = DIVMOD_2EXP 4 q3 in 499 let (q5,Rn) = DIVMOD_2EXP 4 q4 in 500 let (q6,L) = DIVMOD_2EXP 1 q5 in 501 let (q7,W) = DIVMOD_2EXP 1 q6 in 502 let (q8,I) = DIVMOD_2EXP 1 q7 in 503 let (q9,U) = DIVMOD_2EXP 1 q8 in 504 (ODD q9,U = 1,I = 1,W = 1,L = 1,n2w Rn,n2w Rd, 505 n2w offsetH,S = 1,H = 1,n2w offsetL)`, 506 DECODE_TAC); 507 508val DECODE_MLA_MUL_THM = store_thm("DECODE_MLA_MUL_THM", 509 `!n. DECODE_MLA_MUL (n2w n) = 510 let (q0,Rm) = DIVMOD_2EXP 4 n in 511 let (q1,Rs) = DIVMOD_2EXP 4 (DIV_2EXP 4 q0) in 512 let (q2,Rn) = DIVMOD_2EXP 4 q1 in 513 let (q3,Rd) = DIVMOD_2EXP 4 q2 in 514 let (q4,S) = DIVMOD_2EXP 1 q3 in 515 let (q5,A) = DIVMOD_2EXP 1 q4 in 516 let (q6,Sgn) = DIVMOD_2EXP 1 q5 in 517 (ODD q6,Sgn = 1,A = 1,S = 1,n2w Rd,n2w Rn,n2w Rs,n2w Rm)`, DECODE_TAC); 518 519val DECODE_LDM_STM_THM = store_thm("DECODE_LDM_STM_THM", 520 `!n. DECODE_LDM_STM (n2w n) = 521 let (q0,list) = DIVMOD_2EXP 16 n in 522 let (q1,Rn) = DIVMOD_2EXP 4 q0 in 523 let (q2,L) = DIVMOD_2EXP 1 q1 in 524 let (q3,W) = DIVMOD_2EXP 1 q2 in 525 let (q4,S) = DIVMOD_2EXP 1 q3 in 526 let (q5,U) = DIVMOD_2EXP 1 q4 in 527 (ODD q5, U = 1, S = 1, W = 1, L = 1,n2w Rn,n2w list)`, DECODE_TAC); 528 529val DECODE_SWP_THM = store_thm("DECODE_SWP_THM", 530 `!n. DECODE_SWP (n2w n) = 531 let (q0,Rm) = DIVMOD_2EXP 4 n in 532 let (q1,Rd) = DIVMOD_2EXP 4 (DIV_2EXP 8 q0) in 533 let (q2,Rn) = DIVMOD_2EXP 4 q1 in 534 (ODD (DIV_2EXP 2 q2),n2w Rn,n2w Rd,n2w Rm)`, DECODE_TAC); 535 536val DECODE_LDC_STC_THM = store_thm("DECODE_LDC_STC_THM", 537 `!n. DECODE_LDC_STC (n2w n) = 538 let (q0,offset) = DIVMOD_2EXP 8 n in 539 let (q1,CPN) = DIVMOD_2EXP 4 q0 in 540 let (q2,CRd) = DIVMOD_2EXP 4 q1 in 541 let (q3,Rn) = DIVMOD_2EXP 4 q2 in 542 let (q4,L) = DIVMOD_2EXP 1 q3 in 543 let (q5,W) = DIVMOD_2EXP 1 q4 in 544 let (q6,N) = DIVMOD_2EXP 1 q5 in 545 let (q7,U) = DIVMOD_2EXP 1 q6 in 546 (ODD q7,U = 1,N = 1,W = 1,L = 1,n2w Rn,n2w CRd,n2w CPN,n2w offset)`, 547 DECODE_TAC); 548 549val DECODE_CDP_THM = store_thm("DECODE_CDP_THM", 550 `!n. DECODE_CDP (n2w n) = 551 let (q0,CRm) = DIVMOD_2EXP 4 n in 552 let (q1,Cop2) = DIVMOD_2EXP 3 (DIV2 q0) in 553 let (q2,CPN) = DIVMOD_2EXP 4 q1 in 554 let (q3,CRd) = DIVMOD_2EXP 4 q2 in 555 let (q4,CRn) = DIVMOD_2EXP 4 q3 in 556 (n2w (MOD_2EXP 4 q4),n2w CRn,n2w CRd,n2w CPN,n2w Cop2,n2w CRm)`, 557 DECODE_TAC); 558 559val DECODE_MRC_MCR_THM = store_thm("DECODE_MRC_MCR_THM", 560 `!n. DECODE_MRC_MCR (n2w n) = 561 let (q0,CRm) = DIVMOD_2EXP 4 n in 562 let (q1,Cop2) = DIVMOD_2EXP 3 (DIV2 q0) in 563 let (q2,CPN) = DIVMOD_2EXP 4 q1 in 564 let (q3,CRd) = DIVMOD_2EXP 4 q2 in 565 let (q4,CRn) = DIVMOD_2EXP 4 q3 in 566 (n2w (MOD_2EXP 3 (DIV2 q4)),n2w CRn,n2w CRd,n2w CPN,n2w Cop2,n2w CRm)`, 567 DECODE_TAC); 568 569(* ------------------------------------------------------------------------- *) 570 571fun w2w_n2w_sizes a b = (GSYM o SIMP_RULE (std_ss++wordsLib.SIZES_ss) [] o 572 Thm.INST_TYPE [alpha |-> a, beta |-> b]) w2w_n2w; 573 574val SHIFT_IMMEDIATE_THM = store_thm("SHIFT_IMMEDIATE_THM", 575 `!reg mode C opnd2. 576 SHIFT_IMMEDIATE reg mode C (n2w opnd2) = 577 let (q0,Rm) = DIVMOD_2EXP 4 opnd2 in 578 let (q1,Sh) = DIVMOD_2EXP 2 (DIV2 q0) in 579 let shift = MOD_2EXP 5 q1 in 580 let rm = REG_READ reg mode (n2w Rm) in 581 SHIFT_IMMEDIATE2 (n2w shift) (n2w Sh) rm C`, 582 ONCE_REWRITE_TAC (map (w2w_n2w_sizes ``:12``) [``:8``, ``:4``, ``:2``]) 583 \\ DECODE_TAC); 584 585val SHIFT_REGISTER_THM = store_thm("SHIFT_REGISTER_THM", 586 `!reg mode C opnd2. 587 SHIFT_REGISTER reg mode C (n2w opnd2) = 588 let (q0,Rm) = DIVMOD_2EXP 4 opnd2 in 589 let (q1,Sh) = DIVMOD_2EXP 2 (DIV2 q0) in 590 let Rs = MOD_2EXP 4 (DIV2 q1) in 591 let shift = MOD_2EXP 8 (w2n (REG_READ reg mode (n2w Rs))) 592 and rm = REG_READ (INC_PC reg) mode (n2w Rm) in 593 SHIFT_REGISTER2 (n2w shift) (n2w Sh) rm C`, 594 ONCE_REWRITE_TAC [w2w_n2w_sizes ``:32`` ``:8``] 595 \\ ONCE_REWRITE_TAC (map (w2w_n2w_sizes ``:12``) [``:8``, ``:4``, ``:2``]) 596 \\ SIMP_TAC std_ss [SHIFT_REGISTER_def,word_extract_def, 597 (GSYM o SIMP_RULE (std_ss++wordsLib.SIZES_ss) [n2w_w2n,BITS_THM,DIV_1, 598 (GSYM o SIMP_RULE std_ss [] o SPEC `8`) MOD_2EXP_def] o 599 SPECL [`7`,`0`,`w2n (a:word32)`] o 600 Thm.INST_TYPE [alpha |-> ``:32``]) word_bits_n2w] 601 \\ SIMP_TAC word_ss []); 602 603(* ------------------------------------------------------------------------- *) 604 605val REGISTER_LIST_THM = store_thm("REGISTER_LIST_THM", 606 `!n. REGISTER_LIST (n2w n) = 607 let (q0,b0) = DIVMOD_2EXP 1 n in 608 let (q1,b1) = DIVMOD_2EXP 1 q0 in 609 let (q2,b2) = DIVMOD_2EXP 1 q1 in 610 let (q3,b3) = DIVMOD_2EXP 1 q2 in 611 let (q4,b4) = DIVMOD_2EXP 1 q3 in 612 let (q5,b5) = DIVMOD_2EXP 1 q4 in 613 let (q6,b6) = DIVMOD_2EXP 1 q5 in 614 let (q7,b7) = DIVMOD_2EXP 1 q6 in 615 let (q8,b8) = DIVMOD_2EXP 1 q7 in 616 let (q9,b9) = DIVMOD_2EXP 1 q8 in 617 let (q10,b10) = DIVMOD_2EXP 1 q9 in 618 let (q11,b11) = DIVMOD_2EXP 1 q10 in 619 let (q12,b12) = DIVMOD_2EXP 1 q11 in 620 let (q13,b13) = DIVMOD_2EXP 1 q12 in 621 let (q14,b14) = DIVMOD_2EXP 1 q13 in 622 MAP SND (FILTER FST 623 [(b0 = 1,0w); (b1 = 1,1w); (b2 = 1,2w); (b3 = 1,3w); 624 (b4 = 1,4w); (b5 = 1,5w); (b6 = 1,6w); (b7 = 1,7w); 625 (b8 = 1,8w); (b9 = 1,9w); (b10 = 1,10w); (b11 = 1,11w); 626 (b12 = 1,12w); (b13 = 1,13w); (b14 = 1,14w); (ODD q14,15w)])`, 627 DECODE_TAC); 628 629(* ------------------------------------------------------------------------- *) 630 631val DECODE_ARM_THM = store_thm("DECODE_ARM_THM", 632 `!ireg. DECODE_ARM (ireg : word32) = 633 let b n = ireg ' n in 634 if b 27 then 635 if b 26 then 636 if b 25 then 637 if b 24 then (* (T,T,T,T,...) *) 638 swi_ex 639 else (* (T,T,T,F,...) *) 640 if b 4 then 641 if b 20 then mrc else mcr 642 else 643 cdp_und 644 else (* (T,T,F,...) *) 645 ldc_stc 646 else (* (T,F,...) *) 647 if b 25 then br else ldm_stm 648 else 649 if b 26 then (* (F,T,...) *) 650 if b 25 then 651 if b 4 then cdp_und else ldr_str 652 else 653 ldr_str 654 else 655 if b 25 then (* (F,F,T,...) *) 656 if b 24 /\ ~b 23 /\ ~b 20 then 657 if b 21 then 658 msr 659 else 660 cdp_und 661 else 662 data_proc 663 else 664 if b 24 then (* (F,F,F,T,...) *) 665 if b 7 then 666 if b 4 then 667 if b 20 then 668 if b 6 then 669 ldrh_strh 670 else 671 if b 5 then 672 ldrh_strh 673 else 674 cdp_und 675 else 676 if b 6 then 677 cdp_und 678 else 679 if b 5 then 680 ldrh_strh 681 else 682 if ~b 23 /\ ~b 21 then 683 swp 684 else 685 cdp_und 686 else 687 data_proc 688 else 689 if b 4 then 690 data_proc 691 else 692 if ~b 23 /\ ~b 20 /\ ~b 6 /\ ~b 5 then 693 if b 21 then msr else mrs 694 else 695 data_proc 696 else (* (F,F,F,F,...) *) 697 if b 7 then 698 if b 4 then 699 if b 6 \/ b 5 then 700 if b 20 /\ b 6 then 701 ldrh_strh 702 else 703 if ~b 6 /\ b 5 then 704 ldrh_strh 705 else 706 cdp_und 707 else 708 if b 23 \/ ~b 22 then mla_mul else cdp_und 709 else 710 data_proc 711 else 712 if b 4 then data_proc else data_proc`, 713 SRW_TAC [boolSimps.LET_ss] [DECODE_ARM_def] 714 \\ FULL_SIMP_TAC (srw_ss()) [bool_case_ID]); 715 716(* -------------------------------------------------------------------------- *) 717 718val _ = export_theory(); 719