1(* ------------------------------------------------------------------------ *) 2(* ARM Machine Code Semantics (A and R profiles) *) 3(* ============================================= *) 4(* Operational semantics for ARM *) 5(* ------------------------------------------------------------------------ *) 6 7(* interactive use: 8 app load 9 ["arm_seq_monadTheory", "wordsLib", "intLib", "integer_wordTheory", 10 "stringSimps", "parmonadsyntax"]; 11*) 12 13open HolKernel boolLib bossLib Parse; 14open wordsTheory wordsLib integer_wordTheory; 15 16open arm_coretypesTheory arm_seq_monadTheory; 17 18val _ = new_theory "arm_opsem"; 19val _ = ParseExtras.temp_loose_equality() 20 21(* ------------------------------------------------------------------------ *) 22 23val _ = numLib.prefer_num(); 24val _ = wordsLib.prefer_word(); 25 26val _ = set_fixity ">>=" (Infixr 660); 27val _ = set_fixity "|||" (Infixr 90); 28val _ = overload_on(">>=", ``seqT``); 29val _ = overload_on("|||", ``parT``); 30 31val _ = temp_overload_on (parmonadsyntax.monad_bind, ``seqT``); 32val _ = temp_overload_on (parmonadsyntax.monad_par, ``parT``); 33val _ = temp_overload_on ("return", ``constT``); 34 35val _ = overload_on("UNKNOWN", ``ARB:bool``); 36val _ = overload_on("UNKNOWN", ``ARB:word32``); 37val _ = overload_on("BITS16_UNKNOWN", ``[ARB;ARB] : word8 list``); 38val _ = overload_on("BITS32_UNKNOWN", ``[ARB;ARB;ARB;ARB] : word8 list``); 39 40val _ = app temp_overload_on 41 [("unit2", ``\(u1:unit,u2:unit). constT ()``), 42 ("unit3", ``\(u1:unit,u2:unit,u3:unit). constT ()``), 43 ("unit4", ``\(u1:unit,u2:unit,u3:unit,u4:unit). constT ()``)]; 44 45val _ = temp_overload_on 46 ("ALL", ``(UNIV CROSS UNIV) : (ARMarch # ARMextensions set) set``); 47 48val _ = temp_overload_on 49 ("ARCH", ``\s. (s CROSS UNIV) : (ARMarch # ARMextensions set) set``); 50 51val _ = temp_overload_on("BadReg", ``\n:word4. (n = 13w) \/ (n = 15w)``); 52 53val _ = temp_overload_on("extend", ``\u. if u then w2w else sw2sw``); 54 55val _ = temp_overload_on 56 ("ARCH2", 57 ``\enc a. ARCH (if enc = Encoding_Thumb2 then thumb2_support else a)``); 58 59(* ------------------------------------------------------------------------ *) 60 61val unaligned_support_def = Define` 62 unaligned_support ii = 63 read_info ii >>= (\info. constT (info.unaligned_support))`; 64 65val dsp_support_def = Define` 66 dsp_support = COMPL {ARMv4; ARMv4T; ARMv5T}`; 67 68val kernel_support_def = Define` 69 kernel_support = {a | (a = ARMv6K) \/ version_number a >= 7}`; 70 71val arch_version_def = Define` 72 arch_version ii = seqT (read_arch ii) (constT o version_number)`; 73 74val read_reg_literal_def = Define` 75 read_reg_literal ii n = 76 if n = 15w then 77 read_reg ii 15w >>= (\pc. constT (align(pc,4))) 78 else 79 read_reg ii n`; 80 81val read_flags_def = Define` 82 read_flags ii = 83 read_cpsr ii >>= (\cpsr. constT (cpsr.N,cpsr.Z,cpsr.C,cpsr.V))`; 84 85val write_flags_def = Define` 86 write_flags ii (n,z,c,v) = 87 read_cpsr ii >>= 88 (\cpsr. write_cpsr ii (cpsr with <| N := n; Z := z; C := c; V := v |>))`; 89 90val read_cflag_def = Define` 91 read_cflag ii = read_flags ii >>= (\(n,z,c,v). constT c)`; 92 93val set_q_def = Define` 94 set_q ii = 95 read_cpsr ii >>= (\cpsr. write_cpsr ii (cpsr with Q := T))`; 96 97val read_ge_def = Define` 98 read_ge ii = read_cpsr ii >>= (\cpsr. constT (cpsr.GE))`; 99 100val write_ge_def = Define` 101 write_ge ii ge = 102 read_cpsr ii >>= (\cpsr. write_cpsr ii (cpsr with GE := ge))`; 103 104val write_e_def = Define` 105 write_e ii e = 106 read_cpsr ii >>= (\cpsr. write_cpsr ii (cpsr with E := e))`; 107 108val IT_advance_def = Define` 109 IT_advance ii = 110 read_arch ii >>= 111 (\arch. 112 condT (arch IN thumb2_support) 113 (read_cpsr ii >>= 114 (\cpsr. 115 if (cpsr.IT = 0w) \/ cpsr.T then 116 write_cpsr ii (cpsr with IT := ITAdvance cpsr.IT) 117 else 118 errorT "IT_advance: unpredictable")))`; 119 120val cpsr_write_by_instr_def = zDefine` 121 cpsr_write_by_instr ii (value:word32, bytemask:word4, affect_execstate:bool) = 122 let value_mode = (4 >< 0) value in 123 (current_mode_is_priviledged ii ||| is_secure ii ||| read_nsacr ii ||| 124 bad_mode ii value_mode) >>= 125 (\(priviledged,is_secure,nsacr,badmode). 126 if bytemask ' 0 /\ priviledged /\ 127 (badmode \/ 128 ~is_secure /\ (value_mode = 0b10110w) \/ 129 ~is_secure /\ (value_mode = 0b10001w) /\ nsacr.RFR) 130 then 131 errorT "cpsr_write_by_instr: unpredictable" 132 else 133 (read_sctlr ii ||| read_scr ii ||| read_cpsr ii) >>= 134 (\(sctlr,scr,cpsr). 135 let cpsr = word_modify (\i b. 136 if 27 <= i /\ i <= 31 /\ bytemask ' 3 \/ 137 24 <= i /\ i <= 26 /\ bytemask ' 3 /\ 138 affect_execstate \/ 139 16 <= i /\ i <= 19 /\ bytemask ' 2 \/ 140 10 <= i /\ i <= 15 /\ bytemask ' 1 /\ 141 affect_execstate \/ 142 (i = 9) /\ bytemask ' 1 \/ 143 (i = 8) /\ bytemask ' 1 /\ 144 priviledged /\ 145 (is_secure \/ scr.AW) \/ 146 (i = 7) /\ bytemask ' 0 /\ priviledged \/ 147 (i = 6) /\ bytemask ' 0 /\ 148 priviledged /\ 149 (is_secure \/ scr.FW) /\ 150 (~sctlr.NMFI \/ ~(value ' 6)) \/ 151 (i = 5) /\ bytemask ' 0 /\ 152 affect_execstate \/ 153 (i < 5) /\ bytemask ' 0 /\ 154 priviledged 155 then value ' i else b) (encode_psr cpsr) 156 in 157 write_cpsr ii (decode_psr cpsr)))`; 158 159val spsr_write_by_instr_def = zDefine` 160 spsr_write_by_instr ii (value:word32, bytemask:word4) = 161 (current_mode_is_user_or_system ii ||| bad_mode ii ((4 >< 0) value)) >>= 162 (\(user_or_system,badmode). 163 if user_or_system \/ bytemask ' 0 /\ badmode then 164 errorT "spsr_write_by_instr: unpredictable" 165 else 166 read_spsr ii >>= 167 (\spsr. 168 let spsr = word_modify (\i b. 169 if 24 <= i /\ i <= 31 /\ bytemask ' 3 \/ 170 16 <= i /\ i <= 19 /\ bytemask ' 2 \/ 171 8 <= i /\ i <= 15 /\ bytemask ' 1 \/ 172 i <= 7 /\ bytemask ' 0 173 then value ' i else b) (encode_psr spsr) 174 in 175 write_spsr ii (decode_psr spsr)))`; 176 177val integer_zero_divide_trapping_enabled_def = Define` 178 integer_zero_divide_trapping_enabled ii = 179 read_sctlr ii >>= (\sctlr. constT sctlr.DZ)`; 180 181(* ------------------------------------------------------------------------ *) 182 183val branch_write_pc_def = Define` 184 branch_write_pc ii (address:word32) = 185 current_instr_set ii >>= 186 (\iset. 187 if iset = InstrSet_ARM then 188 arch_version ii >>= 189 (\version. 190 if version < 6 /\ ((1 >< 0) address <> 0w:word2) 191 then 192 errorT "branch_write_pc: unpredictable" 193 else 194 branch_to ii ((31 '' 2) address)) 195 else 196 branch_to ii ((31 '' 1) address))`; 197 198val bx_write_pc_def = Define` 199 bx_write_pc ii (address:word32) = 200 current_instr_set ii >>= 201 (\iset. 202 if iset = InstrSet_ThumbEE then 203 if address ' 0 then 204 branch_to ii ((31 '' 1) address) 205 else 206 errorT "bx_write_pc: unpredictable" 207 else 208 if address ' 0 then 209 select_instr_set ii InstrSet_Thumb >>= 210 (\u. branch_to ii ((31 '' 1) address)) 211 else if ~(address ' 1) then 212 select_instr_set ii InstrSet_ARM >>= 213 (\u. branch_to ii address) 214 else (* address<1:0> = '10' *) 215 errorT "bx_write_pc: unpredictable")`; 216 217val load_write_pc_def = Define` 218 load_write_pc ii (address:word32) = 219 arch_version ii >>= 220 (\version. 221 if version >= 5 then 222 bx_write_pc ii address 223 else 224 branch_write_pc ii address)`; 225 226val alu_write_pc_def = Define` 227 alu_write_pc ii (address:word32) = 228 (arch_version ii ||| current_instr_set ii) >>= 229 (\(version,iset). 230 if version >= 7 /\ (iset = InstrSet_ARM) then 231 bx_write_pc ii address 232 else 233 branch_write_pc ii address)`; 234 235(* ------------------------------------------------------------------------ *) 236 237val decode_imm_shift_def = Define` 238 decode_imm_shift (type:word2, imm5:word5) = 239 case type 240 of 0b00w => (SRType_LSL, w2n imm5) 241 | 0b01w => (SRType_LSR, if imm5 = 0w then 32 else w2n imm5) 242 | 0b10w => (SRType_ASR, if imm5 = 0w then 32 else w2n imm5) 243 | 0b11w => if imm5 = 0w then 244 (SRType_RRX, 1) 245 else 246 (SRType_ROR, w2n imm5)`; 247 248val decode_reg_shift_def = Define` 249 decode_reg_shift (type:word2) = 250 case type 251 of 0b00w => SRType_LSL 252 | 0b01w => SRType_LSR 253 | 0b10w => SRType_ASR 254 | 0b11w => SRType_ROR`; 255 256val shift_c_def = Define` 257 shift_c (value:'a word, type:SRType, amount:num, carry_in:bool) = 258 if (type = SRType_RRX) /\ (amount <> 1) then 259 errorT "shift_c: RRX amount not 1" 260 else 261 constT 262 (if amount = 0 then 263 (value, carry_in) 264 else 265 (case type 266 of SRType_LSL => LSL_C (value, amount) 267 | SRType_LSR => LSR_C (value, amount) 268 | SRType_ASR => ASR_C (value, amount) 269 | SRType_ROR => ROR_C (value, amount) 270 | SRType_RRX => RRX_C (value, carry_in)))`; 271 272val shift_def = Define` 273 shift (value:'a word, type:SRType, amount:num, carry_in:bool) = 274 (shift_c (value, type, amount, carry_in)) >>= 275 (\r. constT (FST r))`; 276 277val arm_expand_imm_c_def = Define` 278 arm_expand_imm_c (imm12:word12, carry_in:bool) = 279 shift_c 280 ((7 >< 0) imm12 : word32, SRType_ROR, 281 2 * w2n ((11 -- 8) imm12), carry_in)`; 282 283val arm_expand_imm_def = Define` 284 arm_expand_imm ii (imm12:word12) = 285 read_cflag ii >>= 286 (\c. 287 arm_expand_imm_c (imm12,c) >>= 288 (\(imm32,c). constT imm32))`; 289 290val thumb_expand_imm_c_def = Define` 291 thumb_expand_imm_c (imm12:word12, carry_in:bool) : (word32 # bool) M = 292 if (11 -- 10) imm12 = 0b00w then 293 let imm8 = (7 >< 0) imm12 : word8 in 294 case (9 >< 8) imm12 : word2 295 of 0b00w => 296 constT (w2w imm8, carry_in) 297 | 0b01w => 298 if imm8 = 0w then 299 errorT "thumb_expand_imm_c: unpredictable" 300 else 301 constT (word32 [imm8; 0b00000000w; imm8; 0b00000000w], carry_in) 302 | 0b10w => 303 if imm8 = 0w then 304 errorT "thumb_expand_imm_c: unpredictable" 305 else 306 constT (word32 [0b00000000w; imm8; 0b00000000w; imm8], carry_in) 307 | 0b11w => 308 if imm8 = 0w then 309 errorT "thumb_expand_imm_c: unpredictable" 310 else 311 constT (word32 [imm8; imm8; imm8; imm8], carry_in) 312 else 313 let unrotated_value = (7 :+ T) ((6 >< 0) imm12) in 314 constT (ROR_C (unrotated_value, w2n ((11 -- 7) imm12)))`; 315 316(* 317val thumb_expand_imm_def = Define` 318 thumb_expand_imm ii (imm12:word12) = 319 read_cflag ii >>= 320 (\c. 321 thumb_expand_imm_c (imm12,c) >>= 322 (\(imm32,c). constT imm32))`; 323*) 324 325(* ------------------------------------------------------------------------ *) 326 327val address_mode1_def = Define` 328 (address_mode1 ii thumb2 (Mode1_immediate imm12) = 329 read_cflag ii >>= 330 (\c. 331 if thumb2 then 332 thumb_expand_imm_c (imm12,c) 333 else 334 arm_expand_imm_c (imm12,c))) /\ 335 (address_mode1 ii thumb2 (Mode1_register imm5 type rm) = 336 (read_reg ii rm ||| read_cflag ii) >>= 337 (\(rm,c). 338 let (shift_t,shift_n) = decode_imm_shift (type,imm5) in 339 shift_c (rm, shift_t, shift_n, c))) /\ 340 (address_mode1 ii thumb2 (Mode1_register_shifted_register rs type rm) = 341 (read_reg ii rm ||| read_reg ii rs ||| read_cflag ii) >>= 342 (\(rm,rs,c). 343 let shift_t = decode_reg_shift type 344 and shift_n = w2n ((7 -- 0) rs) in 345 shift_c (rm, shift_t, shift_n, c)))`; 346 347val address_mode2_def = Define` 348 (address_mode2 ii indx add rn (Mode2_immediate imm12) = 349 let imm32 = w2w imm12 in 350 let offset_addr = if add then rn + imm32 else rn - imm32 in 351 constT (offset_addr, if indx then offset_addr else rn)) /\ 352 (address_mode2 ii indx add rn (Mode2_register imm5 type rm) = 353 (read_reg ii rm ||| read_cflag ii) >>= 354 (\(rm,c). 355 let (shift_t,shift_n) = decode_imm_shift (type,imm5) in 356 shift (rm, shift_t, shift_n, c) >>= 357 (\imm32. 358 let offset_addr = if add then rn + imm32 else rn - imm32 in 359 constT (offset_addr, if indx then offset_addr else rn))))`; 360 361val address_mode3_def = Define` 362 (address_mode3 ii indx add rn (Mode3_immediate imm12) = 363 let imm32 = w2w imm12 in 364 let offset_addr = if add then rn + imm32 else rn - imm32 in 365 constT (offset_addr, if indx then offset_addr else rn)) /\ 366 (address_mode3 ii indx add rn (Mode3_register imm2 rm) = 367 (read_reg ii rm ||| read_cflag ii) >>= 368 (\(rm,c). 369 shift (rm, SRType_LSL, w2n imm2, c) >>= 370 (\imm32. 371 let offset_addr = if add then rn + imm32 else rn - imm32 in 372 constT (offset_addr, if indx then offset_addr else rn))))`; 373 374val address_mode5_def = Define` 375 address_mode5 indx add rn (imm8:word8) = 376 let imm32 : word32 = (w2w imm8) << 2 in 377 let offset_addr = if add then rn + imm32 else rn - imm32 in 378 constT (offset_addr, if indx then offset_addr else rn)`; 379 380(* ------------------------------------------------------------------------ *) 381 382val data_processing_alu_def = Define` 383 data_processing_alu (opc:word4) (a:word32) b c = 384 case opc 385 of 0b0000w => ( a && b , ARB, ARB) (* AND *) 386 | 0b0001w => ( a ?? b , ARB, ARB) (* EOR *) 387 | 0b0010w => add_with_carry( a,~b, T) (* SUB *) 388 | 0b0011w => add_with_carry(~a, b, T) (* RSB *) 389 | 0b0100w => add_with_carry( a, b, F) (* ADD *) 390 | 0b0101w => add_with_carry( a, b, c) (* ADC *) 391 | 0b0110w => add_with_carry( a,~b, c) (* SBC *) 392 | 0b0111w => add_with_carry(~a, b, c) (* RSC *) 393 | 0b1000w => ( a && b , ARB , ARB) (* TST *) 394 | 0b1001w => ( a ?? b , ARB , ARB) (* TEQ *) 395 | 0b1010w => add_with_carry( a,~b, T) (* CMP *) 396 | 0b1011w => add_with_carry( a, b, F) (* CMN *) 397 | 0b1100w => ( a || b , ARB , ARB) (* ORR *) 398 | 0b1101w => ( b , ARB , ARB) (* MOV *) 399 | 0b1110w => ( a && ~b , ARB , ARB) (* BIC *) 400 | _ => ( a || ~b , ARB , ARB)`; (* MVN/ORN *) 401 402val data_processing_thumb2_unpredictable_def = Define` 403 (data_processing_thumb2_unpredictable 404 (Data_Processing opc setflags n d (Mode1_immediate imm12)) = 405 case opc 406 of 0b0000w => (* AND *) 407 (d = 13w) \/ (d = 15w) /\ ~setflags \/ BadReg n 408 | 0b0001w => (* EOR *) 409 (d = 13w) \/ (d = 15w) /\ ~setflags \/ BadReg n 410 | 0b0010w => (* SUB *) 411 (if n = 13w then 412 (d = 15w) /\ ~setflags 413 else 414 (d = 13w) \/ (d = 15w) /\ ~setflags \/ (n = 15w)) 415 | 0b0100w => (* ADD *) 416 if n = 13w then 417 (d = 15w) /\ ~setflags 418 else 419 (d = 13w) \/ (d = 15w) /\ ~setflags \/ (n = 15w) 420 | 0b0111w => T (* RSC *) 421 | 0b1000w => BadReg n (* TST *) 422 | 0b1001w => BadReg n (* TEQ *) 423 | 0b1010w => n = 15w (* CMP *) 424 | 0b1011w => n = 15w (* CMN *) 425 | 0b1101w => BadReg d (* MOV *) 426 | 0b1111w => BadReg d \/ (n = 13w) (* MVN/ORN *) 427 | _ => (* RSB,ADC,SBC,ORR,BIC *) 428 BadReg d \/ BadReg n) /\ 429 (data_processing_thumb2_unpredictable 430 (Data_Processing opc setflags n d (Mode1_register imm5 typ m)) = 431 case opc 432 of 0b0000w => (* AND *) 433 (d = 13w) \/ (d = 15w) /\ ~setflags \/ BadReg n 434 | 0b0001w => (* EOR *) 435 (d = 13w) \/ (d = 15w) /\ ~setflags \/ BadReg n 436 | 0b0010w => (* SUB *) 437 if n = 13w then 438 (d = 13w) /\ (typ <> 0w \/ w2n imm5 > 3) \/ 439 (d = 15w) \/ BadReg m 440 else 441 (d = 13w) \/ (d = 15w) /\ ~setflags \/ (n = 15w) \/ BadReg m 442 | 0b0100w => (* ADD *) 443 if n = 13w then 444 (d = 13w) /\ (typ <> 0w \/ w2n imm5 > 3) \/ 445 (d = 15w) \/ BadReg m 446 else 447 (d = 13w) \/ (d = 15w) /\ ~setflags \/ (n = 15w) \/ BadReg m 448 | 0b0111w => T (* RSC *) 449 | 0b1000w => BadReg n \/ BadReg m (* TST *) 450 | 0b1001w => BadReg n \/ BadReg m (* TEQ *) 451 | 0b1010w => (n = 15w) \/ BadReg m (* CMP *) 452 | 0b1011w => (n = 15w) \/ BadReg m (* CMN *) 453 | 0b1101w => (* MOV *) 454 if setflags then 455 BadReg d \/ BadReg m 456 else 457 (d = 15w) \/ (m = 15w) \/ (d = 13w) /\ (m = 13w) 458 | 0b1111w => BadReg d \/ (n = 13w) \/ BadReg m (* MVN/ORN *) 459 | _ => (* RSB,ADC,SBC,ORR,BIC *) 460 BadReg d \/ BadReg n \/ BadReg m) /\ 461 (data_processing_thumb2_unpredictable 462 (Data_Processing opc setflags n d 463 (Mode1_register_shifted_register s typ m)) = 464 opc <> 0b1101w \/ BadReg d \/ BadReg s \/ BadReg m)`; 465 466val _ = temp_overload_on ("top_half", ``( 31 >< 16 ) : word32 -> word16``); 467val _ = temp_overload_on ("bot_half", ``( 15 >< 0 ) : word32 -> word16``); 468 469val signed_parallel_add_sub_16_def = Define` 470 signed_parallel_add_sub_16 op2 rn rm = 471 let bn = SInt (bot_half rn) and bm = SInt (bot_half rm) 472 and tn = SInt (top_half rn) and tm = SInt (top_half rm) 473 in 474 case op2 475 of Parallel_add_16 => (bn + bm, tn + tm) 476 | Parallel_add_sub_exchange => (bn - tm, tn + bm) 477 | Parallel_sub_add_exchange => (bn + tm, tn - bm) 478 | Parallel_sub_16 => (bn - bm, tn - tm)`; 479 480val signed_normal_add_sub_16_def = Define` 481 signed_normal_add_sub_16 op2 rn rm : word32 # word4 option = 482 let (r1,r2) = signed_parallel_add_sub_16 op2 rn rm in 483 let ge1 = if r1 >= 0i then 0b11w else 0b00w : word2 484 and ge2 = if r2 >= 0i then 0b11w else 0b00w : word2 485 in 486 ((i2w r2 : word16) @@ (i2w r1 : word16), SOME (ge2 @@ ge1))`; 487 488val signed_saturating_add_sub_16_def = Define` 489 signed_saturating_add_sub_16 op2 rn rm : word32 # word4 option = 490 let (r1,r2) = signed_parallel_add_sub_16 op2 rn rm in 491 ((signed_sat (r2,16) : word16) @@ (signed_sat (r1,16) : word16), NONE)`; 492 493val signed_halving_add_sub_16_def = Define` 494 signed_halving_add_sub_16 op2 rn rm : word32 # word4 option = 495 let (r1,r2) = signed_parallel_add_sub_16 op2 rn rm in 496 ((i2w (r2 / 2) : word16) @@ (i2w (r1 / 2) : word16), NONE)`; 497 498val signed_parallel_add_sub_8_def = Define` 499 signed_parallel_add_sub_8 op2 rn rm = 500 let n = MAP SInt (bytes (rn,4)) 501 and m = MAP SInt (bytes (rm,4)) 502 in 503 case op2 of Parallel_add_8 => MAP (UNCURRY $+) (ZIP (n,m)) 504 | Parallel_sub_8 => MAP (UNCURRY $-) (ZIP (n,m))`; 505 506val signed_normal_add_sub_8_def = Define` 507 signed_normal_add_sub_8 op2 rn rm : word32 # word4 option = 508 let r = signed_parallel_add_sub_8 op2 rn rm in 509 let ge = FCP i. EL i r >= 0i in 510 (word32 (MAP i2w r), SOME ge)`; 511 512val signed_saturating_add_sub_8_def = Define` 513 signed_saturating_add_sub_8 op2 rn rm : word32 # word4 option = 514 (word32 (MAP (\i. signed_sat (i,8)) (signed_parallel_add_sub_8 op2 rn rm)), 515 NONE)`; 516 517val signed_halving_add_sub_8_def = Define` 518 signed_halving_add_sub_8 op2 rn rm : word32 # word4 option = 519 (word32 (MAP (\i. i2w (i / 2)) 520 (signed_parallel_add_sub_8 op2 rn rm)), NONE)`; 521 522val unsigned_parallel_add_sub_16_def = Define` 523 unsigned_parallel_add_sub_16 op2 rn rm = 524 let bn = UInt (bot_half rn) and bm = UInt (bot_half rm) 525 and tn = UInt (top_half rn) and tm = UInt (top_half rm) 526 in 527 case op2 528 of Parallel_add_16 => (bn + bm, tn + tm) 529 | Parallel_add_sub_exchange => (bn - tm, tn + bm) 530 | Parallel_sub_add_exchange => (bn + tm, tn - bm) 531 | Parallel_sub_16 => (bn - bm, tn - tm)`; 532 533val unsigned_normal_add_sub_16_def = Define` 534 unsigned_normal_add_sub_16 op2 rn rm : word32 # word4 option = 535 let (r1,r2) = unsigned_parallel_add_sub_16 op2 rn rm in 536 let (ge1:word2,ge2:word2) = 537 case op2 538 of Parallel_add_16 => 539 (if r1 >= 0x10000i then 0b11w else 0b00w, 540 if r2 >= 0x10000i then 0b11w else 0b00w) 541 | Parallel_add_sub_exchange => 542 (if r1 >= 0i then 0b11w else 0b00w, 543 if r2 >= 0x10000i then 0b11w else 0b00w) 544 | Parallel_sub_add_exchange => 545 (if r1 >= 0x10000i then 0b11w else 0b00w, 546 if r2 >= 0i then 0b11w else 0b00w) 547 | Parallel_sub_16 => 548 (if r1 >= 0i then 0b11w else 0b00w, 549 if r2 >= 0i then 0b11w else 0b00w) 550 in 551 ((i2w r2 : word16) @@ (i2w r1 : word16), SOME (ge2 @@ ge1))`; 552 553val unsigned_saturating_add_sub_16_def = Define` 554 unsigned_saturating_add_sub_16 op2 rn rm : word32 # word4 option = 555 let (r1,r2) = unsigned_parallel_add_sub_16 op2 rn rm in 556 ((unsigned_sat (r2,16) : word16) @@ (unsigned_sat (r1,16) : word16), 557 NONE)`; 558 559val unsigned_halving_add_sub_16_def = Define` 560 unsigned_halving_add_sub_16 op2 rn rm : word32 # word4 option = 561 let (r1,r2) = unsigned_parallel_add_sub_16 op2 rn rm in 562 ((i2w (r2 / 2) : word16) @@ (i2w (r1 / 2) : word16), NONE)`; 563 564val unsigned_parallel_add_sub_8_def = Define` 565 unsigned_parallel_add_sub_8 op2 rn rm = 566 let n = MAP UInt (bytes (rn,4)) 567 and m = MAP UInt (bytes (rm,4)) 568 in 569 case op2 of Parallel_add_8 => MAP (UNCURRY $+) (ZIP (n,m)) 570 | Parallel_sub_8 => MAP (UNCURRY $-) (ZIP (n,m))`; 571 572val unsigned_normal_add_sub_8_def = Define` 573 unsigned_normal_add_sub_8 op2 rn rm : word32 # word4 option = 574 let r = unsigned_parallel_add_sub_8 op2 rn rm 575 and ge_lim = case op2 of Parallel_add_8 => 0x100i 576 | Parallel_sub_8 => 0i 577 in 578 let ge:word4 = FCP i. EL i r >= ge_lim in 579 (word32 (MAP i2w r), SOME ge)`; 580 581val unsigned_saturating_add_sub_8_def = Define` 582 unsigned_saturating_add_sub_8 op2 rn rm : word32 # word4 option = 583 (word32 584 (MAP (\i. unsigned_sat (i,8)) 585 (unsigned_parallel_add_sub_8 op2 rn rm)), NONE)`; 586 587val unsigned_halving_add_sub_8_def = Define` 588 unsigned_halving_add_sub_8 op2 rn rm : word32 # word4 option = 589 (word32 (MAP (\i. i2w (i / 2)) (unsigned_parallel_add_sub_8 op2 rn rm)), 590 NONE)`; 591 592val parallel_add_sub_def = Define` 593 parallel_add_sub u (op1,op2) rn rm = 594 case (u,op1,op2) 595 of (F,Parallel_normal,Parallel_add_8) => 596 signed_normal_add_sub_8 op2 rn rm 597 | (F,Parallel_normal,Parallel_sub_8) => 598 signed_normal_add_sub_8 op2 rn rm 599 | (F,Parallel_normal,_) => 600 signed_normal_add_sub_16 op2 rn rm 601 | (F,Parallel_saturating,Parallel_add_8) => 602 signed_saturating_add_sub_8 op2 rn rm 603 | (F,Parallel_saturating,Parallel_sub_8) => 604 signed_saturating_add_sub_8 op2 rn rm 605 | (F,Parallel_saturating,_) => 606 signed_saturating_add_sub_16 op2 rn rm 607 | (F,Parallel_halving,Parallel_add_8) => 608 signed_halving_add_sub_8 op2 rn rm 609 | (F,Parallel_halving,Parallel_sub_8) => 610 signed_halving_add_sub_8 op2 rn rm 611 | (F,Parallel_halving,_) => 612 signed_halving_add_sub_16 op2 rn rm 613 | (T,Parallel_normal,Parallel_add_8) => 614 unsigned_normal_add_sub_8 op2 rn rm 615 | (T,Parallel_normal,Parallel_sub_8) => 616 unsigned_normal_add_sub_8 op2 rn rm 617 | (T,Parallel_normal,_) => 618 unsigned_normal_add_sub_16 op2 rn rm 619 | (T,Parallel_saturating,Parallel_add_8) => 620 unsigned_saturating_add_sub_8 op2 rn rm 621 | (T,Parallel_saturating,Parallel_sub_8) => 622 unsigned_saturating_add_sub_8 op2 rn rm 623 | (T,Parallel_saturating,_) => 624 unsigned_saturating_add_sub_16 op2 rn rm 625 | (T,Parallel_halving,Parallel_add_8) => 626 unsigned_halving_add_sub_8 op2 rn rm 627 | (T,Parallel_halving,Parallel_sub_8) => 628 unsigned_halving_add_sub_8 op2 rn rm 629 | (T,Parallel_halving,_) => 630 unsigned_halving_add_sub_16 op2 rn rm`; 631 632(* ------------------------------------------------------------------------ *) 633 634val barrier_option_def = Define` 635 barrier_option (option:word4) = 636 case option 637 of 0b0010w => (MBReqDomain_OuterShareable, MBReqTypes_Writes) 638 | 0b0011w => (MBReqDomain_OuterShareable, MBReqTypes_All) 639 | 0b0110w => (MBReqDomain_Nonshareable, MBReqTypes_Writes) 640 | 0b0111w => (MBReqDomain_Nonshareable, MBReqTypes_All) 641 | 0b1010w => (MBReqDomain_InnerShareable, MBReqTypes_Writes) 642 | 0b1011w => (MBReqDomain_InnerShareable, MBReqTypes_All) 643 | 0b1110w => (MBReqDomain_FullSystem, MBReqTypes_Writes) 644 | _ => (MBReqDomain_FullSystem, MBReqTypes_All)`; 645 646(* ------------------------------------------------------------------------ *) 647 648val exc_vector_base_def = Define` 649 exc_vector_base ii : word32 M = 650 read_sctlr ii >>= 651 (\sctlr. 652 if sctlr.V then 653 constT 0xFFFF0000w 654 else 655 (have_security_ext ii >>= 656 (\have_security_exta. 657 if have_security_exta then 658 read_vbar ii 659 else 660 constT 0w)))`; 661 662val take_reset_def = Define` 663 take_reset ii = 664 (exc_vector_base ii ||| have_security_ext ii ||| 665 read_cpsr ii ||| read_scr ii ||| read_sctlr ii) >>= 666 (\(ExcVectorBase,have_security_exta,cpsr,scr,sctlr). 667 (condT (cpsr.M = 0b10110w) 668 (write_scr ii (scr with NS := F)) ||| 669 write_cpsr ii (cpsr with M := 0b10011w)) >>= 670 (\(u1:unit,u2:unit). 671 ((read_cpsr ii >>= 672 (\cpsr. 673 write_cpsr ii (cpsr with 674 <| I := T; 675 IT := 0b00000000w; 676 J := F; T := sctlr.TE; 677 E := sctlr.EE |>))) ||| 678 branch_to ii (ExcVectorBase + 0w)) >>= unit2))`; 679 680val take_undef_instr_exception_def = Define` 681 take_undef_instr_exception ii = 682 (read_reg ii 15w ||| exc_vector_base ii ||| 683 read_cpsr ii ||| read_scr ii ||| read_sctlr ii) >>= 684 (\(pc,ExcVectorBase,cpsr,scr,sctlr). 685 (condT (cpsr.M = 0b10110w) 686 (write_scr ii (scr with NS := F)) ||| 687 write_cpsr ii (cpsr with M := 0b11011w)) >>= 688 (\(u1:unit,u2:unit). 689 (write_spsr ii cpsr ||| 690 write_reg ii 14w (if cpsr.T then pc - 2w else pc - 4w) ||| 691 (read_cpsr ii >>= 692 (\cpsr. 693 write_cpsr ii (cpsr with 694 <| I := T; 695 IT := 0b00000000w; 696 J := F; T := sctlr.TE; 697 E := sctlr.EE |>))) ||| 698 branch_to ii (ExcVectorBase + 4w)) >>= unit4))`; 699 700val take_svc_exception_def = Define` 701 take_svc_exception ii = 702 IT_advance ii >>= 703 (\u:unit. 704 (read_reg ii 15w ||| exc_vector_base ii ||| 705 read_cpsr ii ||| read_scr ii ||| read_sctlr ii) >>= 706 (\(pc,ExcVectorBase,cpsr,scr,sctlr). 707 (condT (cpsr.M = 0b10110w) 708 (write_scr ii (scr with NS := F)) ||| 709 write_cpsr ii (cpsr with M := 0b10011w)) >>= 710 (\(u1:unit,u2:unit). 711 (write_spsr ii cpsr ||| 712 write_reg ii 14w (if cpsr.T then pc - 2w else pc - 4w) ||| 713 (read_cpsr ii >>= 714 (\cpsr. 715 write_cpsr ii (cpsr with 716 <| I := T; 717 IT := 0b00000000w; 718 J := F; T := sctlr.TE; 719 E := sctlr.EE |>))) ||| 720 branch_to ii (ExcVectorBase + 8w)) >>= unit4)))`; 721 722val take_smc_exception_def = Define` 723 take_smc_exception ii = 724 IT_advance ii >>= 725 (\u:unit. 726 (read_reg ii 15w ||| read_mvbar ii ||| 727 read_cpsr ii ||| read_scr ii ||| read_sctlr ii) >>= 728 (\(pc,mvbar,cpsr,scr,sctlr). 729 (condT (cpsr.M = 0b10110w) 730 (write_scr ii (scr with NS := F)) ||| 731 write_cpsr ii (cpsr with M := 0b10110w)) >>= 732 (\(u1:unit,u2:unit). 733 (write_spsr ii cpsr ||| 734 write_reg ii 14w (if cpsr.T then pc else pc - 4w) ||| 735 (read_cpsr ii >>= 736 (\cpsr. 737 write_cpsr ii (cpsr with 738 <| I := T; F := T; A := T; 739 IT := 0b00000000w; 740 J := F; T := sctlr.TE; 741 E := sctlr.EE |>))) ||| 742 branch_to ii (mvbar + 8w)) >>= unit4)))`; 743 744(* For now assume trap_to_monitor is false, i.e. no external aborts *) 745val take_prefetch_abort_exception_def = Define` 746 take_prefetch_abort_exception ii = 747 (read_reg ii 15w ||| exc_vector_base ii ||| have_security_ext ii ||| 748 read_cpsr ii ||| read_scr ii ||| read_sctlr ii) >>= 749 (\(pc,ExcVectorBase,have_security_exta,cpsr,scr,sctlr). 750 (condT (cpsr.M = 0b10110w) 751 (write_scr ii (scr with NS := F)) ||| 752 write_cpsr ii (cpsr with M := 0b10111w)) >>= 753 (\(u1:unit,u2:unit). 754 (write_spsr ii cpsr ||| 755 write_reg ii 14w (if cpsr.T then pc else pc - 4w) ||| 756 (read_cpsr ii >>= 757 (\cpsr. 758 write_cpsr ii (cpsr with 759 <| I := T; 760 A := ((~have_security_exta \/ ~scr.NS \/ scr.AW) \/ cpsr.A); 761 IT := 0b00000000w; 762 J := F; T := sctlr.TE; 763 E := sctlr.EE |>))) ||| 764 branch_to ii (ExcVectorBase + 12w)) >>= unit4))`; 765 766 767val take_data_abort_exception_def = Define` 768 take_data_abort_exception ii = 769 (read_reg ii 15w ||| exc_vector_base ii ||| have_security_ext ii ||| 770 read_cpsr ii ||| read_scr ii ||| read_sctlr ii) >>= 771 (\(pc,ExcVectorBase,have_security_exta,cpsr,scr,sctlr). 772 (condT (cpsr.M = 0b10110w) 773 (write_scr ii (scr with NS := F)) ||| 774 write_cpsr ii (cpsr with M := 0b10111w)) >>= 775 (\(u1:unit,u2:unit). 776 (write_spsr ii cpsr ||| 777 write_reg ii 14w (if cpsr.T then pc else pc - 4w) ||| 778 (read_cpsr ii >>= 779 (\cpsr. 780 write_cpsr ii (cpsr with 781 <| I := T; 782 A := ((~have_security_exta \/ ~scr.NS \/ scr.AW) \/ cpsr.A); 783 IT := 0b00000000w; 784 J := F; T := sctlr.TE; 785 E := sctlr.EE |>))) ||| 786 branch_to ii (ExcVectorBase + 16w)) >>= unit4))`; 787 788 789val take_irq_exception_def = Define` 790 take_irq_exception ii = 791 (read_reg ii 15w ||| exc_vector_base ii ||| have_security_ext ii ||| 792 read_cpsr ii ||| read_scr ii ||| read_sctlr ii) >>= 793 (\(pc,ExcVectorBase,have_security_exta,cpsr,scr,sctlr). 794 (condT (cpsr.M = 0b10110w) 795 (write_scr ii (scr with NS := F)) ||| 796 write_cpsr ii (cpsr with M := 0b10010w)) >>= 797 (\(u1:unit,u2:unit). 798 (write_spsr ii cpsr ||| 799 write_reg ii 14w (if cpsr.T then pc else pc - 4w) ||| 800 (read_cpsr ii >>= 801 (\cpsr. 802 write_cpsr ii (cpsr with 803 <| I := T; 804 A := ((~have_security_exta \/ ~scr.NS \/ scr.AW) \/ cpsr.A); 805 IT := 0b00000000w; 806 J := F; T := sctlr.TE; 807 E := sctlr.EE |>))) ||| 808 branch_to ii (ExcVectorBase + 24w)) >>= unit4))`; 809 810val take_fiq_exception_def = Define` 811 take_fiq_exception ii = 812 (read_reg ii 15w ||| exc_vector_base ii ||| have_security_ext ii ||| 813 read_cpsr ii ||| read_scr ii ||| read_sctlr ii) >>= 814 (\(pc,ExcVectorBase,have_security_exta,cpsr,scr,sctlr). 815 (condT (cpsr.M = 0b10110w) 816 (write_scr ii (scr with NS := F)) ||| 817 write_cpsr ii (cpsr with M := 0b10001w)) >>= 818 (\(u1:unit,u2:unit). 819 (write_spsr ii cpsr ||| 820 write_reg ii 14w (if cpsr.T then pc else pc - 4w) ||| 821 (read_cpsr ii >>= 822 (\cpsr. 823 write_cpsr ii (cpsr with 824 <| I := T; 825 F := ((~have_security_exta \/ ~scr.NS \/ scr.AW) \/ cpsr.F); 826 A := ((~have_security_exta \/ ~scr.NS \/ scr.AW) \/ cpsr.A); 827 IT := 0b00000000w; 828 J := F; T := sctlr.TE; 829 E := sctlr.EE |>))) ||| 830 branch_to ii (ExcVectorBase + 28w)) >>= unit4))`; 831 832(* ------------------------------------------------------------------------ *) 833 834val null_check_if_thumbee_def = Define` 835 null_check_if_thumbEE ii n (f:unit M) = 836 current_instr_set ii >>= 837 (\iset. 838 if iset = InstrSet_ThumbEE then 839 read_reg ii n >>= 840 (\rn. 841 if n = 15w then 842 if align (rn, 4) = 0w then 843 errorT ("null_check_if_thumbEE PC: unpredictable") 844 else 845 f 846 else if n = 13w then 847 if rn = 0w then 848 errorT ("null_check_if_thumbEE SP: unpredictable") 849 else 850 f 851 else if rn = 0w then 852 (read_reg ii 15w ||| read_cpsr ii ||| read_teehbr ii) >>= 853 (\(pc,cpsr,teehbr). 854 (write_reg ii 14w ((0 :+ T) pc) ||| 855 write_cpsr ii (cpsr with IT := 0w)) >>= 856 (\(u1:unit, u2:unit). 857 branch_write_pc ii (teehbr - 4w))) 858 else 859 f) 860 else 861 f)`; 862 863val run_instruction_def = Define` 864 run_instruction ii s n defined unpredictable c = 865 read_info ii >>= 866 (\info. 867 if (info.arch,info.extensions) NOTIN defined then 868 take_undef_instr_exception ii 869 else if unpredictable (version_number info.arch) then 870 errorT (s ++ ": unpredictable") 871 else if IS_SOME n then 872 null_check_if_thumbEE ii (THE n) c 873 else 874 c)`; 875 876val null_check_instruction_def = Define` 877 null_check_instruction ii s n defined unpredictable c = 878 run_instruction ii s (SOME n) defined unpredictable c`; 879 880val instruction_def = Define` 881 instruction ii s defined unpredictable c = 882 run_instruction ii s NONE defined unpredictable c`; 883 884val instructions = ref ([] : (string * thm) list); 885 886fun iDefine t = 887let 888 val thm = zDefine t 889 val name = (fst o dest_const o fst o strip_comb o lhs o concl o SPEC_ALL) thm 890 val _ = instructions := (name,thm) :: !instructions 891in 892 thm 893end; 894 895(* ........................................................................ 896 T,A: B<c> <label> 897 T2: B<c>.W <label> 898 ```````````````````````````````````````````````````````````````````````` *) 899val branch_target_instr_def = iDefine` 900 branch_target_instr ii enc (Branch_Target imm24) = 901 instruction ii "branch_target" ALL {} 902 (read_reg ii 15w >>= 903 (\pc. 904 let imm32 = sw2sw imm24 << (if enc = Encoding_ARM then 2 else 1) in 905 branch_write_pc ii (pc + imm32)))`; 906 907(* ........................................................................ 908 T,A: BX<c> <Rm> 909 ```````````````````````````````````````````````````````````````````````` *) 910val branch_exchange_instr_def = iDefine` 911 branch_exchange_instr ii (Branch_Exchange m) = 912 instruction ii "branch_exchange" (ARCH {a | a <> ARMv4}) {} 913 (read_reg ii m >>= (\rm. bx_write_pc ii rm))`; 914 915(* ........................................................................ 916 T,A: BL<c> <label> 917 T,A: BLX<c> <label> 918 ```````````````````````````````````````````````````````````````````````` *) 919(* If toARM = F then Unpredictable for ARMv4*. *) 920val branch_link_exchange_imm_instr_def = iDefine` 921 branch_link_exchange_imm_instr ii enc 922 (Branch_Link_Exchange_Immediate H toARM imm24) = 923 instruction ii "branch_link_exchange_imm" 924 (if (enc = Encoding_Thumb2) /\ toARM \/ 925 (enc = Encoding_ARM) /\ ~toARM 926 then 927 ARCH {a | version_number a >= 5} 928 else 929 ALL) {} 930 (current_instr_set ii >>= 931 (\CurrentInstrSet. 932 if toARM /\ (CurrentInstrSet = InstrSet_ThumbEE) then 933 take_undef_instr_exception ii 934 else 935 let targetInstrSet = 936 if toARM then 937 InstrSet_ARM 938 else if enc = Encoding_ARM then 939 InstrSet_Thumb 940 else 941 CurrentInstrSet 942 and imm32 = sw2sw imm24 << 2 in 943 let imm32 = if toARM then imm32 else (1 :+ H) imm32 944 in 945 read_reg ii 15w >>= 946 (\pc. 947 (if CurrentInstrSet = InstrSet_ARM then 948 write_reg ii 14w (pc - 4w) 949 else 950 write_reg ii 14w ((0 :+ T) pc)) >>= 951 (\u. let targetAddress = if targetInstrSet = InstrSet_ARM then 952 align(pc,4) + imm32 953 else 954 pc + imm32 955 in 956 select_instr_set ii targetInstrSet >>= 957 (\u. branch_write_pc ii targetAddress)))))`; 958 959(* ........................................................................ 960 T,A: BLX<c> <Rm> 961 ```````````````````````````````````````````````````````````````````````` *) 962val branch_link_exchange_reg_instr_def = iDefine` 963 branch_link_exchange_reg_instr ii (Branch_Link_Exchange_Register m) = 964 instruction ii "branch_link_exchange_reg" 965 (ARCH {a | version_number a >= 5}) {} 966 ((read_reg ii 15w ||| read_reg ii m ||| current_instr_set ii) >>= 967 (\(pc,rm,iset). 968 let next_instr_addr = 969 if iset = InstrSet_ARM 970 then pc - 4w 971 else pc - 2w 972 in 973 (if iset = InstrSet_ARM then 974 write_reg ii 14w next_instr_addr 975 else 976 write_reg ii 14w ((0 :+ T) next_instr_addr)) >>= 977 (\u. bx_write_pc ii rm)))`; 978 979(* ........................................................................ 980 T: CB{N}Z <Rn>,<label> 981 ```````````````````````````````````````````````````````````````````````` *) 982val compare_branch_instr_def = iDefine` 983 compare_branch_instr ii (Compare_Branch nonzero imm6 n) = 984 instruction ii "compare_branch" (ARCH thumb2_support) {} 985 (read_reg ii (w2w n) >>= 986 (\rn. 987 if nonzero <=/=> (rn = 0w) then 988 read_reg ii 15w >>= 989 (\pc. 990 let imm32 = w2w imm6 << 1 in 991 branch_write_pc ii (pc + imm32)) 992 else 993 increment_pc ii Encoding_Thumb))`; 994 995(* ........................................................................ 996 T2: TBB<c> [<Rn>,<Rm>] 997 T2: TBH<c> [<Rn>,<Rm>,LSL #1] 998 ```````````````````````````````````````````````````````````````````````` *) 999val table_branch_byte_instr_def = iDefine` 1000 table_branch_byte_instr ii (Table_Branch_Byte n is_tbh m) = 1001 null_check_instruction ii "table_branch_byte" n (ARCH thumb2_support) 1002 (\v. (n = 13w) \/ BadReg m) 1003 ((read_reg ii 15w ||| read_reg ii n ||| read_reg ii m) >>= 1004 (\(pc,rn,rm). 1005 (if is_tbh then 1006 read_memU ii (rn + LSL(rm,1), 2) 1007 else 1008 read_memU ii (rn + rm, 1)) >>= 1009 (\halfwords. 1010 branch_write_pc ii (pc + 2w * zero_extend32 halfwords))))`; 1011 1012(* ........................................................................ 1013 TX: CHKA<c> <Rn>,<Rm> 1014 ```````````````````````````````````````````````````````````````````````` *) 1015val check_array_instr_def = iDefine` 1016 check_array_instr ii (Check_Array n m) = 1017 instruction ii "check_array" thumbee_support 1018 (\v. (n = 15w) \/ BadReg m) 1019 ((read_reg ii 15w ||| read_reg ii n ||| read_reg ii m ||| 1020 read_cpsr ii ||| read_teehbr ii) >>= 1021 (\(pc,rn,rm,cpsr,teehbr). 1022 if rn <=+ rm then 1023 ((write_reg ii 14w ((0 :+ T) pc) ||| 1024 write_cpsr ii (cpsr with IT := 0w)) >>= 1025 (\(u1:unit,u2:unit). 1026 branch_write_pc ii (teehbr - 8w))) 1027 else 1028 increment_pc ii Encoding_ThumbEE))`; 1029 1030(* ........................................................................ 1031 TX: HB{L}<c> #<HandlerID> 1032 ```````````````````````````````````````````````````````````````````````` *) 1033val handler_branch_link_instr_def = iDefine` 1034 handler_branch_link_instr ii (Handler_Branch_Link generate_link handler) = 1035 instruction ii "handler_branch_link" thumbee_support {} 1036 ((read_reg ii 15w ||| read_teehbr ii) >>= 1037 (\(pc,teehbr). 1038 let handler_offset = w2w handler << 5 in 1039 condT (generate_link) 1040 (let next_instr_addr = pc - 2w in 1041 write_reg ii 14w ((0 :+ T) next_instr_addr)) >>= 1042 (\u:unit. 1043 branch_write_pc ii (teehbr + handler_offset))))`; 1044 1045(* ........................................................................ 1046 TX: HBLP<c> #<imm>,#<HandlerID> 1047 ```````````````````````````````````````````````````````````````````````` *) 1048val handler_branch_link_parameter_instr_def = iDefine` 1049 handler_branch_link_parameter_instr ii 1050 (Handler_Branch_Link_Parameter imm5 handler) = 1051 instruction ii "handler_branch_link_parameter" thumbee_support {} 1052 ((read_reg ii 15w ||| read_teehbr ii) >>= 1053 (\(pc,teehbr). 1054 let next_instr_addr = pc - 2w 1055 and handler_offset = w2w handler << 5 1056 in 1057 (write_reg ii 8w (w2w imm5) ||| 1058 write_reg ii 14w ((0 :+ T) next_instr_addr)) >>= 1059 (\(u1:unit,u2:unit). 1060 branch_write_pc ii (teehbr + handler_offset))))`; 1061 1062(* ........................................................................ 1063 TX: HBP<c> #<imm>,#<HandlerID> 1064 ```````````````````````````````````````````````````````````````````````` *) 1065val handler_branch_parameter_instr_def = iDefine` 1066 handler_branch_parameter_instr ii (Handler_Branch_Parameter imm3 handler) = 1067 instruction ii "handler_branch_link_parameter" thumbee_support {} 1068 (read_teehbr ii >>= 1069 (\teehbr. 1070 let handler_offset = w2w handler << 5 in 1071 write_reg ii 8w (w2w imm3) >>= 1072 (\u:unit. 1073 branch_write_pc ii (teehbr + handler_offset))))`; 1074 1075(* ........................................................................ 1076 T2: ENTERX 1077 T2: LEAVEX 1078 ```````````````````````````````````````````````````````````````````````` *) 1079val enterx_leavex_def = iDefine` 1080 enterx_leavex_instr ii is_enterx = 1081 instruction ii "enterx_leavex" thumbee_support {} 1082 ((if is_enterx then 1083 select_instr_set ii InstrSet_ThumbEE 1084 else 1085 select_instr_set ii InstrSet_Thumb) >>= 1086 (\u:unit. increment_pc ii Encoding_Thumb2))`; 1087 1088(* ........................................................................ 1089 T: IT{<x>{<y>{<z>}}} <firstcond> 1090 where <x>, <y> and <z> are T or E. 1091 ```````````````````````````````````````````````````````````````````````` *) 1092val if_then_instr_def = iDefine` 1093 if_then_instr ii (If_Then firstcond mask) = 1094 instruction ii "if_then" (ARCH thumb2_support) 1095 (\v. (mask = 0w) \/ (firstcond = 0b1111w) \/ 1096 (firstcond = 0b1110w) /\ (bit_count mask <> 1)) 1097 (read_cpsr ii >>= 1098 (\cpsr. 1099 (increment_pc ii Encoding_Thumb ||| 1100 write_cpsr ii (cpsr with IT := (firstcond @@ mask))) >>= unit2))`; 1101 1102(* ........................................................................ 1103 T2,A: CLZ<c> <Rd>,<Rm> 1104 ```````````````````````````````````````````````````````````````````````` *) 1105val count_leading_zeroes_instr_def = iDefine` 1106 count_leading_zeroes_instr ii enc (Count_Leading_Zeroes d m) = 1107 instruction ii "count_leading_zeroes" 1108 (ARCH2 enc {a | version_number a >= 5}) 1109 (\v. if enc = Encoding_Thumb2 then 1110 BadReg d \/ BadReg m 1111 else 1112 (d = 15w) \/ (m = 15w)) 1113 (read_reg ii m >>= 1114 (\rm. 1115 (increment_pc ii enc ||| 1116 write_reg ii d (n2w (count_leading_zeroes rm))) >>= 1117 unit2))`; 1118 1119(* ........................................................................ 1120 T2,A: MOVW<c> <Rd>,#<imm16> 1121 T2,A: MOVT<c> <Rd>,#<imm16> 1122 ```````````````````````````````````````````````````````````````````````` *) 1123val move_halfword_instr_def = iDefine` 1124 move_halfword_instr ii enc (Move_Halfword high d imm16) = 1125 instruction ii "move_halfword" (ARCH thumb2_support) 1126 (\v. if enc = Encoding_Thumb2 then BadReg d else d = 15w) 1127 ((if high then 1128 read_reg ii d >>= (\rd. constT (imm16 @@ bot_half rd)) 1129 else 1130 constT (w2w imm16)) >>= 1131 (\result. 1132 (increment_pc ii enc ||| write_reg ii d result) >>= unit2))`; 1133 1134(* ........................................................................ 1135 T,A: ADR<c> <Rd>,<label> 1136 T2: ADR<c>.W <Rd>,<label> 1137 T,T2,A: ADD<c><q> <Rd>, PC, #<const> 1138 T2,A : SUB<c><q> <Rd>, PC, #<const> 1139 T2 : ADDW<c> <Rd>, <Rn>, #<imm12> 1140 T2 : SUBW<c> <Rd>, <Rn>, #<imm12> 1141 ```````````````````````````````````````````````````````````````````````` *) 1142val add_sub_instr_def = iDefine` 1143 add_sub_instr ii enc (Add_Sub add n d imm12) = 1144 instruction ii "add_sub" 1145 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 1146 (\v. (enc = Encoding_Thumb2) /\ if n = 13w then d = 15w else BadReg d) 1147 ((read_reg_literal ii n ||| 1148 (if enc = Encoding_ARM then 1149 arm_expand_imm ii imm12 1150 else 1151 constT (w2w imm12))) >>= 1152 (\(rn,imm32). 1153 let result = if add then rn + imm32 else rn - imm32 in 1154 if d = 15w then 1155 alu_write_pc ii result 1156 else 1157 (increment_pc ii enc ||| write_reg ii d result) >>= unit2))`; 1158 1159(* ........................................................................ 1160 For opc in {AND,EOR,ADC,SBC,ORR,BIC} 1161 T2,A: <opc>{S}<c> <Rd>,<Rn>,#<const> 1162 T: <opc>S <Rd>,<Rm> (Outside IT block) 1163 T: <opc><c> <Rd>,<Rm> (Inside IT block) 1164 T2: <opc>{S}<c>.W <Rd>,<Rn>,<Rm>{,<shift>} 1165 A: <opc>{S}<c> <Rd>,<Rn>,<Rm>{,<shift>} 1166 A: <opc>{S}<c> <Rd>,<Rn>,<Rm>,<type> <Rs> 1167 1168 T: ADDS <Rd>,<Rn>,#<imm3> (Outside IT block) 1169 T: ADD<c> <Rd>,<Rn>,#<imm3> (Inside IT block) 1170 T: ADDS <Rdn>,#<imm8> (Outside IT block) 1171 T: ADD<c> <Rdn>,#<imm8> (Inside IT block) 1172 T2: ADD{S}<c>.W <Rd>,<Rn>,#<const> 1173 A: ADD{S}<c> <Rd>,<Rn>,#<const> 1174 T: ADDS <Rd>,<Rn>,<Rm> (Outside IT block) 1175 T: ADD<c> <Rd>,<Rn>,<Rm> (Inside IT block) 1176 T: ADD<c> <Rdn>,<Rm> 1177 T2: ADD{S}<c>.W <Rd>,<Rn>,<Rm>{,<shift>} 1178 A: ADD{S}<c> <Rd>,<Rn>,<Rm>{,<shift>} 1179 A: ADD{S}<c> <Rd>,<Rn>,<Rm>,<type> <Rs> 1180 1181 T: SUBS <Rd>,<Rn>,#<imm3> (Outside IT block) 1182 T: SUB<c> <Rd>,<Rn>,#<imm3> (Inside IT block) 1183 T: SUBS <Rdn>,#<imm8> (Outside IT block) 1184 T: SUB<c> <Rdn>,#<imm8> (Inside IT block) 1185 T2: SUB{S}<c>.W <Rd>,<Rn>,#<const> 1186 A: SUB{S}<c> <Rd>,<Rn>,#<const> 1187 T: SUBS <Rd>,<Rn>,<Rm> (Outside IT block) 1188 T: SUB<c> <Rd>,<Rn>,<Rm> (Inside IT block) 1189 T2: SUB{S}<c>.W <Rd>,<Rn>,<Rm>{,<shift>} 1190 A: SUB{S}<c> <Rd>,<Rn>,<Rm>{,<shift>} 1191 A: SUB{S}<c> <Rd>,<Rn>,<Rm>,<type> <Rs> 1192 1193 T: RSBS <Rd>,<Rn>,#0 (Outside IT block) 1194 T: RSB<c> <Rd>,<Rn>,#0 (Inside IT block) 1195 T2: RSB{S}<c>.W <Rd>,<Rn>,#<const> 1196 A: RSB{S}<c> <Rd>,<Rn>,#<const> 1197 T2,A: RSB{S}<c>.W <Rd>,<Rn>,<Rm>{,<shift>} 1198 A: RSB{S}<c> <Rd>,<Rn>,<Rm>,<type> <Rs> 1199 1200 A: RSC{S}<c> <Rd>,<Rn>,#<const> 1201 A: RSC{S}<c> <Rd>,<Rn>,<Rm>{,<shift>} 1202 A: RSC{S}<c> <Rd>,<Rn>,<Rm>,<type> <Rs> 1203 1204 T2,A: TST<c> <Rn>,#<const> 1205 T: TST<c> <Rn>,<Rm> 1206 T2: TST<c>.W <Rn>,<Rm>{,<shift>} 1207 A: TST<c> <Rn>,<Rm>{,<shift>} 1208 A: TST<c> <Rn>,<Rm>,<type> <Rs> 1209 1210 T2,A: CMN<c> <Rn>,#<const> 1211 T: CMN<c> <Rn>,<Rm> 1212 T2: CMN<c>.W <Rn>,<Rm>{,<shift>} 1213 A: CMN<c> <Rn>,<Rm>{,<shift>} 1214 A: CMN<c> <Rn>,<Rm>,<type> <Rs> 1215 1216 T2,A: TEQ<c> <Rn>,#<const> 1217 T2: TEQ<c> <Rn>,<Rm>{,<shift>} 1218 A: TEQ<c> <Rn>,<Rm>{,<shift>} 1219 A: TEQ<c> <Rn>,<Rm>,<type> <Rs> 1220 1221 T: CMP<c> <Rn>,#<imm8> 1222 T2: CMP<c>.W <Rn>,#<const> 1223 A: CMP<c> <Rn>,#<const> 1224 T: CMP<c> <Rn>,<Rm> 1225 T2: CMP<c>.W <Rn>,<Rm>{,<shift>} 1226 A: CMP<c> <Rn>,<Rm>{,<shift>} 1227 A: CMP<c> <Rn>,<Rm>,<type> <Rs> 1228 1229 T: MOVS <Rd>,#<imm8> (Outside IT block) 1230 T: MOV<c> <Rd>,#<imm8> (Inside IT block) 1231 T2: MOV{S}<c>.W <Rd>,#<const> 1232 A: MOV{S}<c> <Rd>,#<const> 1233 T: MOV <Rd>,<Rm> (Outside IT block) 1234 T: MOV<c> <Rd>,<Rm> (Inside IT block) 1235 T: MOVS <Rd>,<Rm> (Outside IT block) 1236 T2: MOV{S}<c>.W <Rd>,<Rm>{,<shift>} (Covers LSL etc.) 1237 A: MOV{S}<c> <Rd>,<Rm>{,<shift>} (Covers LSL etc.) 1238 A: MOV{S}<c> <Rd>,<Rm>,<type> <Rs> (Covers LSL etc.) 1239 1240 T2,A: MVN{S}<c> <Rd>,#<const> 1241 T: MVNS <Rd>,<Rm> (Outside IT block) 1242 T: MVN<c> <Rd>,<Rm> (Inside IT block) 1243 T2: MVN{S}<c>.W <Rn>,<Rm>{,<shift>} 1244 A: MVN<c> <Rn>,<Rm>{,<shift>} 1245 A: MVN<c> <Rn>,<Rm>,<type> <Rs> 1246 1247 T2: ORN{S}<c> <Rd>,<Rn>,#<const> 1248 T2: ORN{S}<c> <Rn>,<Rn>,<Rm>{,<shift>} 1249 1250 For opc in {LSL,LSR,ASR} 1251 T: <opc>S <Rd>,<Rm>,#<imm5> (Outside IT block) 1252 T: <opc><c> <Rd>,<Rm>,#<imm5> (Inside IT block) 1253 T2: <opc>{S}<c>.W <Rd>,<Rm>,#<imm5> 1254 A: <opc>{S}<c> <Rd>,<Rm>,#<imm5> 1255 T: <opc>S <Rdn>,<Rm> (Outside IT block) 1256 T: <opc><c> <Rdn>,<Rm> (Inside IT block) 1257 T2: <opc>{S}<c>.W <Rd>,<Rn>,<Rm> 1258 A: <opc>{S}<c> <Rd>,<Rn>,<Rm> 1259 T2,A: ROR{S}<c> <Rd>,<Rm>,#<imm5> 1260 T: RORS <Rdn>,<Rm> (Outside IT block) 1261 T: ROR<c> <Rdn>,<Rm> (Inside IT block) 1262 T2: ROR{S}<c>.W <Rd>,<Rn>,<Rm> 1263 A: ROR{S}<c> <Rd>,<Rn>,<Rm> 1264 T2,A: RRX{S}<c> <Rd>,<Rm> 1265 ```````````````````````````````````````````````````````````````````````` *) 1266val data_processing_instr_def = iDefine` 1267 data_processing_instr ii enc (Data_Processing opc setflags n d mode1) = 1268 let test_or_compare = ((3 -- 2 ) opc = 2w) in 1269 instruction ii "data_processing" 1270 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 1271 (\v. (enc = Encoding_Thumb2) /\ 1272 data_processing_thumb2_unpredictable 1273 (Data_Processing opc setflags n d mode1) \/ 1274 (case mode1 1275 of Mode1_register_shifted_register s type m => 1276 (d = 15w) \/ (n = 15w) \/ (m = 15w) \/ (s = 15w) 1277 | Mode1_immediate imm12 => 1278 opc IN {0b0010w; 0b0100w} /\ (n = 15w) /\ ~setflags 1279 | _ => F)) 1280 (((if (opc = 0b1101w) \/ 1281 (opc = 0b1111w) /\ (enc <> Encoding_Thumb2 \/ (n = 15w)) 1282 then 1283 constT 0w 1284 else 1285 read_reg ii n) ||| 1286 address_mode1 ii (enc = Encoding_Thumb2) mode1 ||| 1287 read_flags ii) >>= 1288 (\(rn,(shifted,C_shift),(N,Z,C,V)). 1289 let (result,C_alu,V_alu) = data_processing_alu opc rn shifted C in 1290 ((if test_or_compare then 1291 increment_pc ii enc 1292 else if d = 15w then 1293 if setflags then 1294 read_spsr ii >>= 1295 (\spsr. 1296 cpsr_write_by_instr ii (encode_psr spsr,0b1111w,T) >>= 1297 (\u. branch_write_pc ii result)) 1298 else 1299 alu_write_pc ii result 1300 else 1301 (increment_pc ii enc ||| write_reg ii d result) >>= unit2) ||| 1302 condT (setflags /\ ((d <> 15w) \/ test_or_compare)) 1303 (if (opc ' 2 \/ opc ' 1) /\ (~opc ' 3 \/ ~opc ' 2) 1304 then 1305 write_flags ii (word_msb result,result = 0w,C_alu,V_alu) 1306 else 1307 write_flags ii (word_msb result,result = 0w,C_shift,V))) >>= 1308 unit2))`; 1309 1310(* ........................................................................ 1311 T: MULS <Rdm>,<Rn>,<Rdm> (Outside IT block) 1312 T: MUL<c> <Rdm>,<Rn>,<Rdm> (Inside IT block) 1313 T2: MUL<c> <Rd>,<Rn>,<Rm> 1314 A: MUL{S}<c> <Rd>,<Rn>,<Rm> 1315 T2: MLA<c> <Rd>,<Rn>,<Rm>,<Ra> 1316 A: MLA{S}<c> <Rd>,<Rn>,<Rm>,<Ra> 1317 ```````````````````````````````````````````````````````````````````````` *) 1318val multiply_instr_def = iDefine` 1319 multiply_instr ii enc (Multiply acc setflags d a m n) = 1320 instruction ii "multiply" 1321 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 1322 (\version. 1323 if enc = Encoding_Thumb2 then 1324 BadReg d \/ BadReg n \/ BadReg m \/ acc /\ (a = 13w) 1325 else 1326 (d = 15w) \/ (n = 15w) \/ (m = 15w) \/ acc /\ (a = 15w) \/ 1327 version < 6 /\ (d = n)) 1328 ((read_reg ii a ||| 1329 read_reg ii m ||| 1330 read_reg ii n ||| 1331 arch_version ii) >>= 1332 (\(ra,rm,rn,version). 1333 (let result = rn * rm + (if acc then ra else 0w) in 1334 (increment_pc ii enc ||| 1335 write_reg ii d result ||| 1336 condT setflags (read_flags ii >>= 1337 (\(N,Z,C,V). 1338 let C_flag = if version = 4 then UNKNOWN else C in 1339 write_flags ii (word_msb result,result = 0w,C_flag,V)))) >>= 1340 unit3)))`; 1341 1342(* ........................................................................ 1343 T2: UMULL<c> <RdLo>,<RdHi>,<Rn>,<Rm> 1344 A: UMULL{S}<c> <RdLo>,<RdHi>,<Rn>,<Rm> 1345 T2: UMLAL<c> <RdLo>,<RdHi>,<Rn>,<Rm> 1346 A: UMLAL{S}<c> <RdLo>,<RdHi>,<Rn>,<Rm> 1347 T2: SMULL<c> <RdLo>,<RdHi>,<Rn>,<Rm> 1348 A: SMULL{S}<c> <RdLo>,<RdHi>,<Rn>,<Rm> 1349 T2: SMLAL<c> <RdLo>,<RdHi>,<Rn>,<Rm> 1350 A: SMLAL{S}<c> <RdLo>,<RdHi>,<Rn>,<Rm> 1351 ```````````````````````````````````````````````````````````````````````` *) 1352val multiply_long_instr_def = iDefine` 1353 multiply_long_instr ii enc (Multiply_Long signed acc setflags dhi dlo m n) = 1354 instruction ii "multiply_long" 1355 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 1356 (\version. 1357 (if enc = Encoding_Thumb2 then 1358 BadReg dlo \/ BadReg dhi \/ BadReg n \/ BadReg m 1359 else 1360 (dlo = 15w) \/ (dhi = 15w) \/ (n = 15w) \/ (m = 15w) \/ 1361 version < 6 /\ ((dhi = n) \/ (dlo = n))) \/ 1362 (dhi = dlo)) 1363 ((read_reg ii dhi ||| 1364 read_reg ii dlo ||| 1365 read_reg ii m ||| 1366 read_reg ii n ||| 1367 arch_version ii) >>= 1368 (\(rdhi,rdlo,rm,rn,version). 1369 (let result : word64 = 1370 (if signed then sw2sw rn * sw2sw rm else w2w rn * w2w rm) + 1371 (if acc then rdhi @@ rdlo else 0w) 1372 in 1373 (increment_pc ii enc ||| 1374 write_reg ii dhi (( 63 >< 32 ) result) ||| 1375 write_reg ii dlo (( 31 >< 0 ) result) ||| 1376 condT setflags (read_flags ii >>= 1377 (\(N,Z,C,V). 1378 let (C_flag,V_flag) = if version = 4 then (UNKNOWN,UNKNOWN) 1379 else (C,V) 1380 in 1381 write_flags ii 1382 (word_msb result,result = 0w,C_flag,V_flag)))) >>= 1383 unit4)))`; 1384 1385(* ........................................................................ 1386 T2,A: UMAAL<c> <RdLo>,<RdHi>,<Rn>,<Rm> 1387 ```````````````````````````````````````````````````````````````````````` *) 1388val multiply_accumulate_accumulate_instr_def = iDefine` 1389 multiply_accumulate_accumulate_instr ii enc 1390 (Multiply_Accumulate_Accumulate dhi dlo m n) = 1391 instruction ii "multiply_accumulate_accumulate" 1392 (ARCH2 enc {a | version_number a >= 6}) 1393 (\v. (if enc = Encoding_Thumb2 then 1394 BadReg dlo \/ BadReg dhi \/ BadReg n \/ BadReg m 1395 else 1396 (dlo = 15w) \/ (dhi = 15w) \/ (n = 15w) \/ (m = 15w)) \/ 1397 (dhi = dlo)) 1398 ((read_reg ii dhi ||| 1399 read_reg ii dlo ||| 1400 read_reg ii m ||| 1401 read_reg ii n) >>= 1402 (\(rdhi,rdlo,rm,rn). 1403 (let result : word64 = w2w rn * w2w rm + w2w rdhi + w2w rdlo in 1404 (increment_pc ii enc ||| 1405 write_reg ii dhi (( 63 >< 32 ) result) ||| 1406 write_reg ii dlo (( 31 >< 0 ) result)) >>= 1407 unit3)))`; 1408 1409(* ........................................................................ 1410 T2,A: MLS<c> <Rd>,<Rn>,<Rm>,<Ra> 1411 ```````````````````````````````````````````````````````````````````````` *) 1412val multiply_subtract_instr_def = iDefine` 1413 multiply_subtract_instr ii enc (Multiply_Subtract d a m n) = 1414 instruction ii "multiply_subtract" (ARCH thumb2_support) 1415 (\v. if enc = Encoding_Thumb2 then 1416 BadReg d \/ BadReg n \/ BadReg m \/ BadReg a 1417 else 1418 (d = 15w) \/ (n = 15w) \/ (m = 15w) \/ (a = 15w)) 1419 ((read_reg ii n ||| read_reg ii m ||| read_reg ii a) >>= 1420 (\(rn,rm,ra). let result = ra - rn * rm in 1421 (increment_pc ii enc ||| write_reg ii d result) >>= unit2))`; 1422 1423(* ........................................................................ 1424 T2,A: QADD<c> <Rd>,<Rm>,<Rn> 1425 T2,A: QSUB<c> <Rd>,<Rm>,<Rn> 1426 T2,A: QDADD<c> <Rd>,<Rm>,<Rn> 1427 T2,A: QDSUB<c> <Rd>,<Rm>,<Rn> 1428 ```````````````````````````````````````````````````````````````````````` *) 1429val saturating_add_subtract_instr_def = iDefine` 1430 saturating_add_subtract_instr ii enc (Saturating_Add_Subtract opc n d m) = 1431 instruction ii "saturating_add_subtract" (ARCH2 enc dsp_support) 1432 (\v. if enc = Encoding_Thumb2 then 1433 BadReg d \/ BadReg n \/ BadReg m 1434 else 1435 (d = 15w) \/ (n = 15w) \/ (m = 15w)) 1436 ((read_reg ii m ||| read_reg ii n) >>= 1437 (\(rm,rn). 1438 let (result,sat) = 1439 case opc 1440 of 0b00w => signed_sat_q (SInt rm + SInt rn,32) 1441 | 0b01w => signed_sat_q (SInt rm - SInt rn,32) 1442 | 0b10w => 1443 (let (doubled:word32,sat1) = 1444 signed_sat_q (2 * SInt rn,32) in 1445 let (result,sat2) = 1446 signed_sat_q (SInt rm + SInt doubled,32) 1447 in 1448 (result,sat1 \/ sat2)) 1449 | 0b11w => 1450 (let (doubled:word32,sat1) = 1451 signed_sat_q (2 * SInt rn,32) in 1452 let (result,sat2) = 1453 signed_sat_q (SInt rm - SInt doubled,32) 1454 in 1455 (result,sat1 \/ sat2)) 1456 in 1457 (increment_pc ii enc ||| 1458 write_reg ii d result ||| 1459 condT sat (set_q ii)) >>= 1460 unit3))`; 1461 1462(* ........................................................................ 1463 T2,A: SMLA<x><y><c> <Rd>,<Rn>,<Rm>,<Ra> 1464 where <x> and <y> are T (top) or B (bottom) 1465 ```````````````````````````````````````````````````````````````````````` *) 1466val signed_16_multiply_32_accumulate_instr_def = iDefine` 1467 signed_16_multiply_32_accumulate_instr ii enc 1468 (Signed_Halfword_Multiply opc m_high n_high d a m n) = 1469 instruction ii "signed_16_multiply_32_accumulate" (ARCH2 enc dsp_support) 1470 (\v. (opc <> 0w) \/ 1471 (if enc = Encoding_Thumb2 then 1472 BadReg d \/ BadReg n \/ BadReg m \/ BadReg a 1473 else 1474 (d = 15w) \/ (n = 15w) \/ (m = 15w) \/ (a = 15w))) 1475 ((read_reg ii m ||| read_reg ii n ||| read_reg ii a) >>= 1476 (\(rm,rn,ra). 1477 let operand1 = if n_high then top_half rn else bot_half rn 1478 and operand2 = if m_high then top_half rm else bot_half rm 1479 in 1480 let result = SInt operand1 * SInt operand2 + SInt ra in 1481 let result32 = i2w result 1482 in 1483 (increment_pc ii enc ||| 1484 write_reg ii d result32 ||| 1485 condT (result <> SInt result32) (set_q ii)) >>= 1486 unit3))`; 1487 1488(* ........................................................................ 1489 T2,A: SMUL<x><y><c> <Rd>,<Rn>,<Rm> 1490 where <x> and <y> are T (top) or B (bottom) 1491 ```````````````````````````````````````````````````````````````````````` *) 1492val signed_16_multiply_32_result_instr_def = iDefine` 1493 signed_16_multiply_32_result_instr ii enc 1494 (Signed_Halfword_Multiply opc m_high n_high d sbz m n) = 1495 instruction ii "signed_16_multiply_32_result" (ARCH2 enc dsp_support) 1496 (\v. (opc <> 3w) \/ 1497 (if enc = Encoding_Thumb2 then 1498 BadReg d \/ BadReg n \/ BadReg m 1499 else 1500 (d = 15w) \/ (n = 15w) \/ (m = 15w))) 1501 ((read_reg ii m ||| read_reg ii n) >>= 1502 (\(rm,rn). 1503 let operand1 = if n_high then top_half rn else bot_half rn 1504 and operand2 = if m_high then top_half rm else bot_half rm 1505 in 1506 let result = SInt operand1 * SInt operand2 1507 in 1508 (increment_pc ii enc ||| 1509 write_reg ii d (i2w result)) >>= unit2))`; 1510 1511(* ........................................................................ 1512 T2,A: SMLAW<y><c> <Rd>,<Rn>,<Rm>,<Ra> 1513 where <y> is T (top) or B (bottom) 1514 ```````````````````````````````````````````````````````````````````````` *) 1515val signed_16x32_multiply_32_accumulate_instr_def = iDefine` 1516 signed_16x32_multiply_32_accumulate_instr ii enc 1517 (Signed_Halfword_Multiply opc m_high n_high d a m n) = 1518 instruction ii "signed_16x32_multiply_32_accumulate" (ARCH2 enc dsp_support) 1519 (\v. (opc <> 1w) \/ n_high \/ 1520 (if enc = Encoding_Thumb2 then 1521 BadReg d \/ BadReg n \/ BadReg m \/ BadReg a 1522 else 1523 (d = 15w) \/ (n = 15w) \/ (m = 15w) \/ (a = 15w))) 1524 ((read_reg ii m ||| read_reg ii n ||| read_reg ii a) >>= 1525 (\(rm,rn,ra). 1526 let operand2 = if m_high then top_half rm else bot_half rm 1527 and sh16 = 2i ** 16 1528 in 1529 let result = (SInt rn * SInt operand2 + (SInt ra * sh16)) / sh16 1530 in 1531 let result32 = i2w result 1532 in 1533 (increment_pc ii enc ||| 1534 write_reg ii d result32 ||| 1535 condT (result <> SInt result32) (set_q ii)) >>= 1536 unit3))`; 1537 1538(* ........................................................................ 1539 T2,A: SMULW<y><c> <Rd>,<Rn>,<Rm> 1540 where <y> is T (top) or B (bottom) 1541 ```````````````````````````````````````````````````````````````````````` *) 1542val signed_16x32_multiply_32_result_instr_def = iDefine` 1543 signed_16x32_multiply_32_result_instr ii enc 1544 (Signed_Halfword_Multiply opc m_high n_high d sbz m n) = 1545 instruction ii "signed_16x32_multiply_32_result" (ARCH2 enc dsp_support) 1546 (\v. (opc <> 1w) \/ ~n_high \/ 1547 (if enc = Encoding_Thumb2 then 1548 BadReg d \/ BadReg n \/ BadReg m 1549 else 1550 (d = 15w) \/ (n = 15w) \/ (m = 15w))) 1551 ((read_reg ii m ||| read_reg ii n) >>= 1552 (\(rm,rn). 1553 let operand2 = if m_high then top_half rm else bot_half rm 1554 in 1555 let result = (SInt rn * SInt operand2) / 2 ** 16 1556 in 1557 (increment_pc ii enc ||| 1558 write_reg ii d (i2w result)) >>= unit2))`; 1559 1560(* ........................................................................ 1561 T2,A: SMLAL<x><y><c> <RdLo>,RdHi>,<Rn>,<Rm> 1562 where <x> and <y> are T (top) or B (bottom) 1563 ```````````````````````````````````````````````````````````````````````` *) 1564val signed_16_multiply_64_accumulate_instr_def = iDefine` 1565 signed_16_multiply_64_accumulate_instr ii enc 1566 (Signed_Halfword_Multiply opc m_high n_high dhi dlo m n) = 1567 instruction ii "signed_16_multiply_64_accumulate" (ARCH2 enc dsp_support) 1568 (\v. (opc <> 2w) \/ 1569 (if enc = Encoding_Thumb2 then 1570 BadReg dlo \/ BadReg dhi \/ BadReg n \/ BadReg m 1571 else 1572 (dlo = 15w) \/ (dhi = 15w) \/ (n = 15w) \/ (m = 15w)) \/ 1573 (dhi = dlo)) 1574 ((read_reg ii m ||| read_reg ii n ||| 1575 read_reg ii dhi ||| read_reg ii dlo) >>= 1576 (\(rm,rn,rdhi,rdlo). 1577 let operand1 = if n_high then top_half rn else bot_half rn 1578 and operand2 = if m_high then top_half rm else bot_half rm 1579 in 1580 let result = (SInt operand1 * SInt operand2) + 1581 (SInt ((rdhi @@ rdlo) : word64)) 1582 in 1583 (increment_pc ii enc ||| 1584 write_reg ii dlo (i2w result) ||| 1585 write_reg ii dhi (i2w (result / 2 ** 32))) >>= 1586 unit3))`; 1587 1588(* ........................................................................ 1589 T2,A: SMUAD{X}<c> <Rd>,<Rn>,<Rm> 1590 T2,A: SMUSD{X}<c> <Rd>,<Rn>,<Rm> 1591 T2,A: SMLAD{X}<c> <Rd>,<Rn>,<Rm>,<Ra> 1592 T2,A: SMLSD{X}<c> <Rd>,<Rn>,<Rm>,<Ra> 1593 ```````````````````````````````````````````````````````````````````````` *) 1594val signed_multiply_dual_instr_def = iDefine` 1595 signed_multiply_dual_instr ii enc (Signed_Multiply_Dual d a m sub m_swap n) = 1596 instruction ii "signed_multiply_dual" 1597 (ARCH2 enc {a | version_number a >= 6}) 1598 (\v. if enc = Encoding_Thumb2 then 1599 BadReg d \/ BadReg n \/ BadReg m \/ (a = 13w) 1600 else 1601 (d = 15w) \/ (n = 15w) \/ (m = 15w)) 1602 ((read_reg ii m ||| read_reg ii n ||| 1603 (if a = 15w then constT 0w else read_reg ii a)) >>= 1604 (\(rm,rn,ra). 1605 let operand2 = if m_swap then ROR (rm,16) else rm in 1606 let product1 = SInt (bot_half rn) * SInt (bot_half operand2) 1607 and product2 = SInt (top_half rn) * SInt (top_half operand2) 1608 in 1609 let result = if sub then product1 - product2 + SInt ra 1610 else product1 + product2 + SInt ra 1611 in 1612 let result32 = i2w result 1613 in 1614 (increment_pc ii enc ||| 1615 write_reg ii d result32 ||| 1616 condT (result <> SInt result32) (set_q ii)) >>= unit3))`; 1617 1618(* ........................................................................ 1619 T2,A: SMLALD{X}<c> <RdLo>,<RdHi>,<Rn>,<Rm> 1620 T2,A: SMLSLD{X}<c> <RdLo>,<RdHi>,<Rn>,<Rm> 1621 ```````````````````````````````````````````````````````````````````````` *) 1622val signed_multiply_long_dual_instr_def = iDefine` 1623 signed_multiply_long_dual_instr ii enc 1624 (Signed_Multiply_Long_Dual dhi dlo m sub m_swap n) = 1625 instruction ii "signed_multiply_long_dual" 1626 (ARCH2 enc {a | version_number a >= 6}) 1627 (\v. (if enc = Encoding_Thumb2 then 1628 BadReg dlo \/ BadReg dhi \/ BadReg n /\ BadReg m 1629 else 1630 (dlo = 15w) \/ (dhi = 15w) \/ (n = 15w) \/ (m = 15w)) \/ 1631 (dhi = dlo)) 1632 ((read_reg ii m ||| 1633 read_reg ii n ||| 1634 read_reg ii dhi ||| 1635 read_reg ii dlo) >>= 1636 (\(rm,rn,rdhi,rdlo). 1637 let operand2 = if m_swap then ROR (rm,16) else rm in 1638 let product1 = SInt (bot_half rn) * SInt (bot_half operand2) 1639 and product2 = SInt (top_half rn) * SInt (top_half operand2) 1640 and rd = (rdhi @@ rdlo) : word64 1641 in 1642 let result = if sub then product1 - product2 + SInt rd 1643 else product1 + product2 + SInt rd 1644 in 1645 let result64 : word64 = i2w result 1646 in 1647 (increment_pc ii enc ||| 1648 write_reg ii dhi (( 63 >< 32 ) result64) ||| 1649 write_reg ii dlo (( 31 >< 0 ) result64)) >>= unit3))`; 1650 1651(* ........................................................................ 1652 T2,A: SMMUL{R}<c> <Rd>,<Rn>,<Rm> 1653 T2,A: SMMLA{R}<c> <Rd>,<Rn>,<Rm>,<Ra> 1654 ```````````````````````````````````````````````````````````````````````` *) 1655val signed_most_significant_multiply_instr_def = iDefine` 1656 signed_most_significant_multiply_instr ii enc 1657 (Signed_Most_Significant_Multiply d a m round n) = 1658 instruction ii "signed_most_significant_multiply" 1659 (ARCH2 enc {a | version_number a >= 6}) 1660 (\v. if enc = Encoding_Thumb2 then 1661 BadReg d \/ BadReg n \/ BadReg m \/ (a = 13w) 1662 else 1663 (d = 15w) \/ (n = 15w) \/ (m = 15w)) 1664 ((read_reg ii m ||| read_reg ii n ||| 1665 (if a = 15w then constT 0w else read_reg ii a)) >>= 1666 (\(rm,rn,ra). 1667 let result = SInt ((w2w ra : word64) << 32) + SInt rn * SInt rm in 1668 let result = i2w (if round then result + 0x80000000 else result) 1669 in 1670 (increment_pc ii enc ||| 1671 write_reg ii d ((63 >< 32) (result:word64))) >>= unit2))`; 1672 1673(* ........................................................................ 1674 T2,A: SMMLS{R}<c> <Rd>,<Rn>,<Rm>,<Ra> 1675 ```````````````````````````````````````````````````````````````````````` *) 1676val signed_most_significant_multiply_subtract_instr_def = iDefine` 1677 signed_most_significant_multiply_subtract_instr ii enc 1678 (Signed_Most_Significant_Multiply_Subtract d a m round n) = 1679 instruction ii "signed_most_significant_multiply_subtract" 1680 (ARCH2 enc {a | version_number a >= 6}) 1681 (\v. if enc = Encoding_Thumb2 then 1682 BadReg d \/ BadReg n \/ BadReg m \/ BadReg a 1683 else 1684 (d = 15w) \/ (n = 15w) \/ (m = 15w) \/ (a = 15w)) 1685 ((read_reg ii m ||| read_reg ii n ||| read_reg ii a) >>= 1686 (\(rm,rn,ra). 1687 let result = SInt ((w2w ra :word64) << 32) - SInt rn * SInt rm in 1688 let result = i2w (if round then result + 0x80000000 else result) 1689 in 1690 (increment_pc ii enc ||| 1691 write_reg ii d ((63 >< 32) (result:word64))) >>= unit2))`; 1692 1693(* ........................................................................ 1694 T2,A: SADD16<c> <Rd>,<Rn>,<Rm> 1695 T2,A: SASX<c> <Rd>,<Rn>,<Rm> 1696 T2,A: SSAX<c> <Rd>,<Rn>,<Rm> 1697 T2,A: SSUB16<c> <Rd>,<Rn>,<Rm> 1698 T2,A: SADD8<c> <Rd>,<Rn>,<Rm> 1699 T2,A: SSUB8<c> <Rd>,<Rn>,<Rm> 1700 1701 T2,A: QADD16<c> <Rd>,<Rn>,<Rm> 1702 T2,A: QASX<c> <Rd>,<Rn>,<Rm> 1703 T2,A: QSAX<c> <Rd>,<Rn>,<Rm> 1704 T2,A: QSUB16<c> <Rd>,<Rn>,<Rm> 1705 T2,A: QADD8<c> <Rd>,<Rn>,<Rm> 1706 T2,A: QSUB8<c> <Rd>,<Rn>,<Rm> 1707 1708 T2,A: SHADD16<c> <Rd>,<Rn>,<Rm> 1709 T2,A: SHASX<c> <Rd>,<Rn>,<Rm> 1710 T2,A: SHSAX<c> <Rd>,<Rn>,<Rm> 1711 T2,A: SHSUB16<c> <Rd>,<Rn>,<Rm> 1712 T2,A: SHADD8<c> <Rd>,<Rn>,<Rm> 1713 T2,A: SHSUB8<c> <Rd>,<Rn>,<Rm> 1714 1715 T2,A: UADD16<c> <Rd>,<Rn>,<Rm> 1716 T2,A: UASX<c> <Rd>,<Rn>,<Rm> 1717 T2,A: USAX<c> <Rd>,<Rn>,<Rm> 1718 T2,A: USUB16<c> <Rd>,<Rn>,<Rm> 1719 T2,A: UADD8<c> <Rd>,<Rn>,<Rm> 1720 T2,A: USUB8<c> <Rd>,<Rn>,<Rm> 1721 1722 T2,A: UQADD16<c> <Rd>,<Rn>,<Rm> 1723 T2,A: UQASX<c> <Rd>,<Rn>,<Rm> 1724 T2,A: UQSAX<c> <Rd>,<Rn>,<Rm> 1725 T2,A: UQSUB16<c> <Rd>,<Rn>,<Rm> 1726 T2,A: UQADD8<c> <Rd>,<Rn>,<Rm> 1727 T2,A: UQSUB8<c> <Rd>,<Rn>,<Rm> 1728 1729 T2,A: UHADD16<c> <Rd>,<Rn>,<Rm> 1730 T2,A: UHASX<c> <Rd>,<Rn>,<Rm> 1731 T2,A: UHSAX<c> <Rd>,<Rn>,<Rm> 1732 T2,A: UHSUB16<c> <Rd>,<Rn>,<Rm> 1733 T2,A: UHADD8<c> <Rd>,<Rn>,<Rm> 1734 T2,A: UHSUB8<c> <Rd>,<Rn>,<Rm> 1735 ```````````````````````````````````````````````````````````````````````` *) 1736val parallel_add_subtract_instr_def = iDefine` 1737 parallel_add_subtract_instr ii enc (Parallel_Add_Subtract u op n d m) = 1738 instruction ii "parallel_add_subtract" 1739 (ARCH2 enc {a | version_number a >= 6}) 1740 (\v. if enc = Encoding_Thumb2 then 1741 BadReg d \/ BadReg n \/ BadReg m 1742 else 1743 (d = 15w) \/ (n = 15w) \/ (m = 15w)) 1744 ((read_reg ii n ||| read_reg ii m) >>= 1745 (\(rn,rm). 1746 let (result,ge) = parallel_add_sub u op rn rm in 1747 (increment_pc ii enc ||| 1748 write_reg ii d result ||| 1749 condT (IS_SOME ge) (write_ge ii (THE ge))) >>= unit3))`; 1750 1751(* ........................................................................ 1752 T2: SDIV<c> <Rd>,<Rn>,<Rm> 1753 T2: UDIV<c> <Rd>,<Rn>,<Rm> 1754 ```````````````````````````````````````````````````````````````````````` *) 1755val divide_instr_def = iDefine` 1756 divide_instr ii (Divide unsigned n d m) = 1757 instruction ii "divide" (ARCH {ARMv7_R}) 1758 (\v. BadReg d \/ BadReg n \/ BadReg m) 1759 (read_reg ii m >>= 1760 (\rm. 1761 if rm = 0w then 1762 integer_zero_divide_trapping_enabled ii >>= 1763 (\trap. 1764 if trap then 1765 take_undef_instr_exception ii 1766 else 1767 (increment_pc ii Encoding_Thumb2 ||| write_reg ii d 0w) >>= 1768 unit2) 1769 else 1770 read_reg ii n >>= 1771 (\rn. 1772 (increment_pc ii Encoding_Thumb2 ||| 1773 write_reg ii d (if unsigned then rn // rm else rn / rm)) >>= 1774 unit2)))`; 1775 1776(* ........................................................................ 1777 T2,A: PKHBT<c> <Rd>,<Rn>,<Rm>{,LSL #<imm>} 1778 T2,A: PKHTB<c> <Rd>,<Rn>,<Rm>{,ASR #<imm>} 1779 ```````````````````````````````````````````````````````````````````````` *) 1780val pack_halfword_instr_def = iDefine` 1781 pack_halfword_instr ii enc (Pack_Halfword n d imm5 tbform m) = 1782 instruction ii "pack_halfword" (ARCH2 enc {a | version_number a >= 6}) 1783 (\v. if enc = Encoding_Thumb2 then 1784 BadReg d \/ BadReg n \/ BadReg m 1785 else 1786 (d = 15w) \/ (n = 15w) \/ (m = 15w)) 1787 ((read_reg ii n ||| read_reg ii m ||| read_cflag ii) >>= 1788 (\(rn,rm,c). 1789 let (shift_t,shift_n) = decode_imm_shift ((1 :+ tbform) 0w, imm5) in 1790 shift (rm, shift_t, shift_n, c) >>= 1791 (\operand2. 1792 let r1 = if tbform then bot_half operand2 else bot_half rn 1793 and r2 = if tbform then top_half rn else top_half operand2 1794 in 1795 (increment_pc ii enc ||| 1796 write_reg ii d (r2 @@ r1)) >>= unit2)))`; 1797 1798(* ........................................................................ 1799 T2,A: SSAT<c> <Rd>,#<imm>, <Rn>{,<shift>} 1800 T2,A: USAT<c> <Rd>,#<imm5>,<Rn>{,<shift>} 1801 ```````````````````````````````````````````````````````````````````````` *) 1802val saturate_instr_def = iDefine` 1803 saturate_instr ii enc (Saturate unsigned sat_imm d imm5 sh n) = 1804 instruction ii "saturate" (ARCH2 enc {a | version_number a >= 6}) 1805 (\v. if enc = Encoding_Thumb2 then 1806 BadReg d \/ BadReg n 1807 else 1808 (d = 15w) \/ (n = 15w)) 1809 ((read_reg ii n ||| read_cflag ii) >>= 1810 (\(rn,c). 1811 let (shift_t,shift_n) = decode_imm_shift ((1 :+ sh) 0w, imm5) in 1812 shift (rn, shift_t, shift_n, c) >>= 1813 (\operand. 1814 let (result,sat) = 1815 if unsigned then 1816 unsigned_sat_q (SInt operand, w2n sat_imm) 1817 else let saturate_to = w2n sat_imm + 1 in 1818 (word_sign_extend saturate_to ## I) 1819 (signed_sat_q (SInt operand, saturate_to)) 1820 in 1821 (increment_pc ii enc ||| 1822 write_reg ii d result ||| 1823 condT sat (set_q ii)) >>= unit3)))`; 1824 1825(* ........................................................................ 1826 T2,A: SXTB16<c> <Rd>,<Rm>{,<rotation>} 1827 T2,A: UXTB16<c> <Rd>,<Rm>{,<rotation>} 1828 T2,A: SXTAB16<c> <Rd>,<Rn>,<Rm>{,<rotation>} 1829 T2,A: UXTAB16<c> <Rd>,<Rn>,<Rm>{,<rotation>} 1830 ```````````````````````````````````````````````````````````````````````` *) 1831val extend_byte_16_instr_def = iDefine` 1832 extend_byte_16_instr ii enc (Extend_Byte_16 unsigned n d rotate m) = 1833 instruction ii "extend_byte_16" (ARCH2 enc {a | version_number a >= 6}) 1834 (\v. if enc = Encoding_Thumb2 then 1835 BadReg d \/ (n = 13w) \/ BadReg m 1836 else 1837 (d = 15w) \/ (m = 15w)) 1838 (((if n = 15w then constT 0w else read_reg ii n) ||| 1839 read_reg ii m) >>= 1840 (\(rn,rm). 1841 let rotated = ROR (rm, w2n rotate * 8) in 1842 let r1 = bot_half rn + extend unsigned (( 7 >< 0 ) rotated : word8) 1843 and r2 = top_half rn + extend unsigned (( 23 >< 16 ) rotated : word8) 1844 in 1845 (increment_pc ii enc ||| 1846 write_reg ii d (r2 @@ r1)) >>= unit2))`; 1847 1848(* ........................................................................ 1849 T2,A: SEL<c> <Rd>,<Rn>,<Rm> 1850 ```````````````````````````````````````````````````````````````````````` *) 1851val select_bytes_instr_def = iDefine` 1852 select_bytes_instr ii enc (Select_Bytes n d m) = 1853 instruction ii "select_bytes" (ARCH2 enc {a | version_number a >= 6}) 1854 (\v. if enc = Encoding_Thumb2 then 1855 BadReg d \/ BadReg n \/ BadReg m 1856 else 1857 (d = 15w) \/ (n = 15w) \/ (m = 15w)) 1858 ((read_reg ii n ||| read_reg ii m ||| read_ge ii) >>= 1859 (\(rn,rm,ge). 1860 let r1 = if ge ' 0 then ( 7 >< 0 ) rn else ( 7 >< 0 ) rm 1861 and r2 = if ge ' 1 then ( 15 >< 8 ) rn else ( 15 >< 8 ) rm 1862 and r3 = if ge ' 2 then ( 23 >< 16 ) rn else ( 23 >< 16 ) rm 1863 and r4 = if ge ' 3 then ( 31 >< 24 ) rn else ( 31 >< 24 ) rm 1864 in 1865 (increment_pc ii enc ||| 1866 write_reg ii d (word32 [r1;r2;r3;r4])) >>= unit2))`; 1867 1868(* ........................................................................ 1869 T2,A: SSAT16<c> <Rd>,#<imm>,<Rn> 1870 T2,A: USAT16<c> <Rd>,#<imm>,<Rn> 1871 ```````````````````````````````````````````````````````````````````````` *) 1872val saturate_16_instr_def = iDefine` 1873 saturate_16_instr ii enc (Saturate_16 unsigned sat_imm d n) = 1874 instruction ii "saturate_16" (ARCH2 enc {a | version_number a >= 6}) 1875 (\v. if enc = Encoding_Thumb2 then 1876 BadReg d \/ BadReg n 1877 else 1878 (d = 15w) \/ (n = 15w)) 1879 (read_reg ii n >>= 1880 (\rn. 1881 let ((result1:word16,sat1),(result2:word16,sat2)) = 1882 if unsigned then 1883 let saturate_to = w2n sat_imm in 1884 unsigned_sat_q (SInt (bot_half rn), saturate_to), 1885 unsigned_sat_q (SInt (top_half rn), saturate_to) 1886 else 1887 let saturate_to = w2n sat_imm + 1 in 1888 (word_sign_extend saturate_to ## I) 1889 (signed_sat_q (SInt (bot_half rn), saturate_to)), 1890 (word_sign_extend saturate_to ## I) 1891 (signed_sat_q (SInt (top_half rn), saturate_to)) 1892 in 1893 (increment_pc ii enc ||| 1894 write_reg ii d (result2 @@ result1) ||| 1895 condT (sat1 \/ sat2) (set_q ii)) >>= unit3))`; 1896 1897(* ........................................................................ 1898 T: SXTB<c> <Rd>,<Rm> 1899 T: UXTB<c> <Rd>,<Rm> 1900 T2: SXTB<c>.W <Rd>,<Rm>{,<rotation>} 1901 T2: UXTB<c>.W <Rd>,<Rm>{,<rotation>} 1902 A: SXTB<c> <Rd>,<Rm>{,<rotation>} 1903 A: UXTB<c> <Rd>,<Rm>{,<rotation>} 1904 T2,A: SXTAB<c> <Rd>,<Rn>,<Rm>{,<rotation>} 1905 T2,A: UXTAB<c> <Rd>,<Rn>,<Rm>{,<rotation>} 1906 ```````````````````````````````````````````````````````````````````````` *) 1907val extend_byte_instr_def = iDefine` 1908 extend_byte_instr ii enc (Extend_Byte unsigned n d rotate m) = 1909 instruction ii "extend_byte" (ARCH2 enc {a | version_number a >= 6}) 1910 (\v. if enc = Encoding_Thumb2 then 1911 BadReg d \/ (n = 13w) \/ BadReg m 1912 else 1913 (d = 15w) \/ (m = 15w)) 1914 (((if n = 15w then constT 0w else read_reg ii n) ||| 1915 read_reg ii m) >>= 1916 (\(rn,rm). 1917 let rotated = ROR (rm, w2n rotate * 8) in 1918 let r = rn + extend unsigned (( 7 >< 0 ) rotated : word8) 1919 in 1920 (increment_pc ii enc ||| 1921 write_reg ii d r) >>= unit2))`; 1922 1923(* ........................................................................ 1924 T,A: REV<c> <Rd>,<Rm> 1925 T2: REV<c>.W <Rd>,<Rm> 1926 ```````````````````````````````````````````````````````````````````````` *) 1927val byte_reverse_word_instr_def = iDefine` 1928 byte_reverse_word_instr ii enc (Byte_Reverse_Word d m) = 1929 instruction ii "byte_reverse_word" (ARCH2 enc {a | version_number a >= 6}) 1930 (\v. if enc = Encoding_Thumb2 then 1931 BadReg d \/ BadReg m 1932 else 1933 (d = 15w) \/ (m = 15w)) 1934 (read_reg ii m >>= 1935 (\rm. 1936 (increment_pc ii enc ||| 1937 write_reg ii d (word32 (REVERSE (bytes (rm, 4))))) >>= unit2))`; 1938 1939(* ........................................................................ 1940 T: SXTH<c> <Rd>,<Rm> 1941 T: UXTH<c> <Rd>,<Rm> 1942 T2: SXTH<c>.W <Rd>,<Rm>{,<rotation>} 1943 T2: UXTH<c>.W <Rd>,<Rm>{,<rotation>} 1944 A: SXTH<c> <Rd>,<Rm>{,<rotation>} 1945 A: UXTH<c> <Rd>,<Rm>{,<rotation>} 1946 T2,A: SXTAH<c> <Rd>,<Rn>,<Rm>{,<rotation>} 1947 T2,A: UXTAH<c> <Rd>,<Rn>,<Rm>{,<rotation>} 1948 ```````````````````````````````````````````````````````````````````````` *) 1949val extend_halfword_instr_def = iDefine` 1950 extend_halfword_instr ii enc (Extend_Halfword unsigned n d rotate m) = 1951 instruction ii "extend_halfword" (ARCH2 enc {a | version_number a >= 6}) 1952 (\v. if enc = Encoding_Thumb2 then 1953 BadReg d \/ (n = 13w) \/ BadReg m 1954 else 1955 (d = 15w) \/ (m = 15w)) 1956 (((if n = 15w then constT 0w else read_reg ii n) ||| 1957 read_reg ii m) >>= 1958 (\(rn,rm). 1959 let rotated = ROR (rm, w2n rotate * 8) in 1960 let r = rn + extend unsigned (( 15 >< 0 ) rotated : word16) 1961 in 1962 (increment_pc ii enc ||| 1963 write_reg ii d r) >>= unit2))`; 1964 1965(* ........................................................................ 1966 T,A: REV16<c> <Rd>,<Rm> 1967 T2: REV16<c>.W <Rd>,<Rm> 1968 ```````````````````````````````````````````````````````````````````````` *) 1969val byte_reverse_packed_halfword_instr_def = iDefine` 1970 byte_reverse_packed_halfword_instr ii enc (Byte_Reverse_Packed_Halfword d m) = 1971 instruction ii "byte_reverse_packed_halfword" 1972 (ARCH2 enc {a | version_number a >= 6}) 1973 (\v. if enc = Encoding_Thumb2 then 1974 BadReg d \/ BadReg m 1975 else 1976 (d = 15w) \/ (m = 15w)) 1977 (read_reg ii m >>= 1978 (\rm. 1979 (increment_pc ii enc ||| 1980 write_reg ii d 1981 (let w = bytes (rm, 4) in 1982 word32 [EL 1 w; EL 0 w; EL 3 w; EL 2 w])) >>= 1983 unit2))`; 1984 1985(* ........................................................................ 1986 T2,A: RBIT<c> <Rd>,<Rm> 1987 ```````````````````````````````````````````````````````````````````````` *) 1988val reverse_bits_instr_def = iDefine` 1989 reverse_bits_instr ii enc (Reverse_Bits d m) = 1990 instruction ii "reverse_bits" (ARCH2 enc {a | version_number a >= 6}) 1991 (\v. if enc = Encoding_Thumb2 then 1992 BadReg d \/ BadReg m 1993 else 1994 (d = 15w) \/ (m = 15w)) 1995 (read_reg ii m >>= 1996 (\rm. 1997 (increment_pc ii enc ||| 1998 write_reg ii d (word_reverse rm)) >>= unit2))`; 1999 2000(* ........................................................................ 2001 T,A: REVSH<c> <Rd>,<Rm> 2002 T2: REVSH<c>.W <Rd>,<Rm> 2003 ```````````````````````````````````````````````````````````````````````` *) 2004val byte_reverse_signed_halfword_instr_def = iDefine` 2005 byte_reverse_signed_halfword_instr ii enc (Byte_Reverse_Signed_Halfword d m) = 2006 instruction ii "byte_reverse_signed_halfword" 2007 (ARCH2 enc {a | version_number a >= 6}) 2008 (\v. if enc = Encoding_Thumb2 then 2009 BadReg d \/ BadReg m 2010 else 2011 (d = 15w) \/ (m = 15w)) 2012 (read_reg ii m >>= 2013 (\rm. 2014 let r1 = sw2sw (( 7 >< 0 ) rm : word8) : word24 2015 and r2 = ( 15 >< 8 ) rm : word8 2016 in 2017 (increment_pc ii enc ||| 2018 write_reg ii d (r1 @@ r2)) >>= unit2))`; 2019 2020(* ........................................................................ 2021 T2,A: USAD8<c> <Rd>,<Rn>,<Rm> 2022 T2,A: USADA8<c> <Rd>,<Rn>,<Rm>,<Ra> 2023 ```````````````````````````````````````````````````````````````````````` *) 2024val unsigned_sum_absolute_differences_instr_def = iDefine` 2025 unsigned_sum_absolute_differences_instr ii enc 2026 (Unsigned_Sum_Absolute_Differences d a m n) = 2027 instruction ii "unsigned_sum_absolute_differences" 2028 (ARCH2 enc {a | version_number a >= 6}) 2029 (\v. if enc = Encoding_Thumb2 then 2030 BadReg d \/ BadReg n \/ BadReg m \/ (a = 13w) 2031 else 2032 (d = 15w) \/ (n = 15w) \/ (m = 15w)) 2033 ((read_reg ii m ||| read_reg ii n ||| 2034 (if a = 15w then constT 0w else read_reg ii a)) >>= 2035 (\(rm,rn,ra). 2036 let absdiff1 = ABS (UInt (( 7 -- 0 ) rn) - UInt (( 7 -- 0 ) rm)) 2037 and absdiff2 = ABS (UInt (( 15 -- 8 ) rn) - UInt (( 15 -- 8 ) rm)) 2038 and absdiff3 = ABS (UInt (( 23 -- 16 ) rn) - UInt (( 23 -- 16 ) rm)) 2039 and absdiff4 = ABS (UInt (( 31 -- 24 ) rn) - UInt (( 31 -- 24 ) rm)) 2040 in 2041 let result = UInt ra + absdiff1 + absdiff2 + absdiff3 + absdiff4 2042 in 2043 (increment_pc ii enc ||| 2044 write_reg ii d (i2w result)) >>= unit2))`; 2045 2046(* ........................................................................ 2047 T2,A: SBFX<c> <Rd>,<Rn>,#<lsb>,#<width> 2048 T2,A: UBFX<c> <Rd>,<Rn>,#<lsb>,#<width> 2049 ```````````````````````````````````````````````````````````````````````` *) 2050val bit_field_extract_instr_def = iDefine` 2051 bit_field_extract_instr ii enc (Bit_Field_Extract unsigned widthm1 d lsb n) = 2052 let lsbit = w2n lsb and widthm1 = w2n widthm1 in 2053 let msbit = lsbit + widthm1 2054 in 2055 instruction ii "bit_field_extract" (ARCH thumb2_support) 2056 (\v. (if enc = Encoding_Thumb2 then 2057 BadReg d \/ BadReg n 2058 else 2059 (d = 15w) \/ (n = 15w)) \/ ~(msbit <= 31)) 2060 (read_reg ii n >>= 2061 (\rn. 2062 let result = 2063 if unsigned then 2064 (msbit -- lsbit) rn 2065 else 2066 (msbit --- lsbit) rn 2067 in 2068 (increment_pc ii enc ||| 2069 write_reg ii d result) >>= unit2))`; 2070 2071(* ........................................................................ 2072 T2,A: BFC<c> <Rd>,#<lsb>,#<width> 2073 T2,A: BFI<c> <Rd>,<Rn>,#<lsb>,#<width> 2074 ```````````````````````````````````````````````````````````````````````` *) 2075val bit_field_clear_insert_instr_def = iDefine` 2076 bit_field_clear_insert_instr ii enc (Bit_Field_Clear_Insert msb d lsb n) = 2077 let lsbit = w2n lsb and msbit = w2n msb in 2078 instruction ii "bit_field_clear_insert" (ARCH thumb2_support) 2079 (\v. (if enc = Encoding_Thumb2 then 2080 BadReg d \/ (n = 13w) 2081 else 2082 (d = 15w)) \/ msbit < lsbit) 2083 ((read_reg ii d ||| 2084 (if n = 15w then constT 0w else read_reg ii n)) >>= 2085 (\(rd,rn). 2086 (increment_pc ii enc ||| 2087 write_reg ii d (bit_field_insert msbit lsbit rn rd)) >>= unit2))`; 2088 2089(* ........................................................................ 2090 T2: PLD{W}<c> [<Rn>,#<imm12>] 2091 T2: PLD{W}<c> [<Rn>,#-<imm8>] 2092 A: PLD{W} [<Rn>,#+/-<imm12>] 2093 T2: PLD<c> <label> 2094 A: PLD <label> 2095 T2: PLD{W}<c> [<Rn>,<Rm>{,LSL #<imm2>}] 2096 A: PLD{W} [<Rn>,+/-<Rm>{,<shift>}] 2097 ```````````````````````````````````````````````````````````````````````` *) 2098(* Unpredictable for ARMv4*. *) 2099val preload_data_instr_def = iDefine` 2100 preload_data_instr ii enc (Preload_Data add is_pldw n mode2) = 2101 instruction ii "preload_data" 2102 {(a,e) | (if enc = Encoding_Thumb2 then 2103 a IN thumb2_support 2104 else 2105 a IN dsp_support) /\ 2106 (is_pldw ==> 2107 Extension_Multiprocessing IN e /\ version_number a >= 7)} 2108 (\v. case mode2 2109 of Mode2_register imm5 type m => 2110 if enc = Encoding_Thumb2 then 2111 BadReg m 2112 else 2113 (m = 15w) \/ (n = 15w) /\ is_pldw 2114 | Mode2_immediate imm12 => F) 2115 ((if is_mode2_immediate mode2 then 2116 read_reg_literal ii n 2117 else 2118 read_reg ii n) >>= 2119 (\base. 2120 address_mode2 ii T add base mode2 >>= 2121 (\(offset_addr,address). 2122 (increment_pc ii enc ||| 2123 if is_pldw then 2124 hint_preload_data_for_write ii address 2125 else 2126 hint_preload_data ii address) >>= unit2)))`; 2127 2128(* ........................................................................ 2129 T2: PLI<c> [<Rn>,#<imm12>] 2130 T2: PLI<c> [<Rn>,#-<imm8>] 2131 A: PLI [<Rn>,#+/-<imm12>] 2132 T2: PLI<c> <label> 2133 A: PLI <label> 2134 T2: PLI<c> [<Rn>,<Rm>{,LSL #<imm2>}] 2135 A: PLI [<Rn>,+/-<Rm>{,<shift>}] 2136 ```````````````````````````````````````````````````````````````````````` *) 2137(* Unpredictable for ARMv4*. *) 2138val preload_instruction_instr_def = iDefine` 2139 preload_instruction_instr ii enc (Preload_Instruction add n mode2) = 2140 instruction ii "preload_instruction" (ARCH {a | version_number a >= 7}) 2141 (\v. case mode2 2142 of Mode2_register imm5 type m => 2143 if enc = Encoding_Thumb2 then BadReg m else m = 15w 2144 | Mode2_immediate imm12 => F) 2145 ((if is_mode2_immediate mode2 then 2146 read_reg_literal ii n 2147 else 2148 read_reg ii n) >>= 2149 (\base. 2150 address_mode2 ii T add base mode2 >>= 2151 (\(offset_addr,address). 2152 (increment_pc ii enc ||| 2153 hint_preload_instr ii address) >>= unit2)))`; 2154 2155(* ........................................................................ 2156 T: LDR{B}<c> <Rt>,[<Rn>{,#<imm>}] 2157 T: LDR<c> <Rt>,[SP{,#<imm>}] 2158 T2: LDR{B}<c>.W <Rt>,[<Rn>{,#<imm12>}] 2159 T2: LDR{B}<c> <Rt>,[<Rn>{,#-<imm8>}] 2160 T2: LDR{B}<c> <Rt>,[<Rn>],#+/-<imm8> 2161 T2: LDR{B}<c> <Rt>,[<Rn>,#+/-<imm8>]! 2162 A: LDR{B}<c> <Rt>,[<Rn>{,#+/-<imm12>}] 2163 A: LDR{B}<c> <Rt>,[<Rn>],#+/-<imm12> 2164 A: LDR{B}<c> <Rt>,[<Rn>,#+/-<imm12>]! 2165 T: LDR<c> <Rt>,<label> 2166 T2: LDR<c>.W <Rt>,<label> 2167 T2: LDRB<c> <Rt>,<label> 2168 A: LDR{B}<c> <Rt>,<label> 2169 T: LDR{B}<c> <Rt>,[<Rn>,<Rm>] 2170 T2: LDR{B}<c>.W <Rt>,[<Rn>,<Rm>{,LSL #<imm2>}] 2171 A: LDR{B}<c> <Rt>,[<Rn>,+/-<Rm>{,<shift>}]{!} 2172 A: LDR{B}<c> <Rt>,[<Rn>],+/-<Rm>{,<shift>} 2173 Unprivileged: 2174 T2: LDR{B}T<c> <Rt>,[<Rn>{,#<imm8>}] 2175 A: LDR{B}T<c> <Rt>,[<Rn>]{,#+/-<imm12>} 2176 A: LDR{B}T<c> <Rt>,[<Rn>],+/-<Rm>{,<shift>} 2177 ```````````````````````````````````````````````````````````````````````` *) 2178val load_instr_def = iDefine` 2179 load_instr ii enc (Load indx add load_byte w unpriv n t mode2) = 2180 let wback = ~indx \/ w in 2181 null_check_instruction ii "load" n 2182 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 2183 (\version. 2184 unpriv /\ (if enc = Encoding_Thumb2 then 2185 ~indx \/ ~add \/ w 2186 else 2187 indx \/ ~w) \/ 2188 (load_byte \/ unpriv) /\ 2189 (if enc = Encoding_Thumb2 then BadReg t else t = 15w) \/ 2190 wback /\ ((n = 15w) \/ (n = t)) \/ 2191 (case mode2 2192 of Mode2_register imm5 type m => 2193 if enc = Encoding_Thumb2 then 2194 BadReg m 2195 else 2196 (m = 15w) \/ wback /\ version < 6 /\ (m = n) 2197 | Mode2_immediate imm12 => F)) 2198 ((if is_mode2_immediate mode2 then 2199 read_reg_literal ii n 2200 else 2201 read_reg ii n) >>= 2202 (\base. 2203 address_mode2 ii indx add base mode2 >>= 2204 (\(offset_addr,address). 2205 (condT wback (write_reg ii n offset_addr) ||| 2206 (if load_byte then 2207 (if unpriv then 2208 read_memU_unpriv ii (address,1) 2209 else 2210 read_memU ii (address,1)) >>= 2211 (\data. 2212 (increment_pc ii enc ||| 2213 write_reg ii t (zero_extend32 data)) >>= unit2) 2214 else 2215 (if unpriv then 2216 read_memU_unpriv ii (address,4) 2217 else 2218 read_memU ii (address,4)) >>= 2219 (\data. 2220 let data = word32 data in 2221 if t = 15w then 2222 if aligned(address,4) then 2223 load_write_pc ii data 2224 else 2225 errorT "load: unpredictable" 2226 else 2227 (increment_pc ii enc ||| 2228 (unaligned_support ii >>= 2229 (\has_unaligned_support. 2230 if has_unaligned_support \/ aligned(address,4) then 2231 write_reg ii t data 2232 else 2233 write_reg ii t 2234 (ROR (data, 8 * w2n ((1 -- 0) address)))))) >>= 2235 unit2))) >>= 2236 unit2)))`; 2237 2238(* ........................................................................ 2239 T: STR{B}<c> <Rt>,[<Rn>{,#<imm>}] 2240 T: STR<c> <Rt>,[SP{,#<imm>}] 2241 T2: STR{B}<c>.W <Rt>,[<Rn>{,#<imm12>}] 2242 T2: STR{B}<c> <Rt>,[<Rn>{,#-<imm8>}] 2243 T2: STR{B}<c> <Rt>,[<Rn>],#+/-<imm8> 2244 T2: STR{B}<c> <Rt>,[<Rn>,#+/-<imm8>]! 2245 A: STR{B}<c> <Rt>,[<Rn>{,#+/-<imm12>}] 2246 A: STR{B}<c> <Rt>,[<Rn>],#+/-<imm12> 2247 A: STR{B}<c> <Rt>,[<Rn>,#+/-<imm12>]! 2248 T: STR{B}<c> <Rt>,[<Rn>,<Rm>] 2249 T2: STR{B}<c>.W <Rt>,[<Rn>,<Rm>{,LSL #<imm2>}] 2250 A: STR{B}<c> <Rt>,[<Rn>,+/-<Rm>{,<shift>}]{!} 2251 A: STR{B}<c> <Rt>,[<Rn>],+/-<Rm>{,<shift>} 2252 Unprivileged: 2253 T2: STR{B}T<c> <Rt>,[<Rn>{,#<imm8>}] 2254 A: STR{B}T<c> <Rt>,[<Rn>]{,#+/-<imm12>} 2255 A: STR{B}T<c> <Rt>,[<Rn>],+/-<Rm>{,<shift>} 2256 ```````````````````````````````````````````````````````````````````````` *) 2257val store_instr_def = iDefine` 2258 store_instr ii enc (Store indx add store_byte w unpriv n t mode2) = 2259 let wback = ~indx \/ w in 2260 null_check_instruction ii "store" n 2261 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 2262 (\version. 2263 unpriv /\ (if enc = Encoding_Thumb2 then 2264 ~indx \/ ~add \/ w 2265 else 2266 indx \/ ~w) \/ 2267 (if enc = Encoding_Thumb2 then 2268 store_byte /\ (t = 13w) \/ (t = 15w) 2269 else 2270 store_byte /\ (t = 15w)) \/ 2271 wback /\ ((n = 15w) \/ (n = t)) \/ 2272 (case mode2 2273 of Mode2_register imm5 type m => 2274 if enc = Encoding_Thumb2 then 2275 BadReg m 2276 else 2277 (m = 15w) \/ wback /\ version < 6 /\ (m = n) 2278 | Mode2_immediate imm12 => F)) 2279 ((read_reg ii n ||| 2280 (if t = 15w then pc_store_value ii else read_reg ii t)) >>= 2281 (\(base,data). 2282 address_mode2 ii indx add base mode2 >>= 2283 (\(offset_addr,address). 2284 ((if store_byte then 2285 if unpriv then 2286 write_memU_unpriv ii (address,1) (bytes(data,1)) 2287 else 2288 write_memU ii (address,1) (bytes(data,1)) 2289 else 2290 unaligned_support ii >>= 2291 (\has_unaligned_support. 2292 let data = if has_unaligned_support \/ aligned(address,4) 2293 then bytes(data,4) 2294 else BITS32_UNKNOWN 2295 in 2296 (if unpriv then 2297 write_memU_unpriv ii (address,4) data 2298 else 2299 write_memU ii (address,4) data))) ||| 2300 increment_pc ii enc ||| 2301 condT wback (write_reg ii n offset_addr)) >>= 2302 unit3)))`; 2303 2304(* ........................................................................ 2305 T: LDR{S}H<c> <Rt>,[<Rn>{,#<imm>}] 2306 T2: LDR{S}H<c>.W <Rt>,[<Rn>{,#<imm12>}] 2307 T2: LDR{S}H<c> <Rt>,[<Rn>{,#-<imm8>}] 2308 A: LDR{S}H<c> <Rt>,[<Rn>{,#+/-<imm8>}] 2309 T2,A: LDR{S}H<c> <Rt>,[<Rn>],#+/-<imm8> 2310 T2,A: LDR{S}H<c> <Rt>,[<Rn>,#+/-<imm8>]! 2311 T2: LDR{S}H<c> <Rt>,<label> 2312 A: LDR{S}H<c> <Rt>,<label> 2313 T: LDR{S}H<c> <Rt>,[<Rn>,<Rm>] 2314 T2: LDR{S}H<c>.W <Rt>,[<Rn>,<Rm>{,LSL #<imm2>}] 2315 A: LDR{S}H<c> <Rt>,[<Rn>,+/-<Rm>]{!} 2316 A: LDR{S}H<c> <Rt>,[<Rn>],+/-<Rm> 2317 Unprivileged: 2318 T2: LDR{S}HT<c> <Rt>,[<Rn>{,#<imm8>}] 2319 A: LDR{S}HT<c> <Rt>,[<Rn>]{,#+/-<imm8>} 2320 A: LDR{S}HT<c> <Rt>,[<Rn>],+/-<Rm> 2321 2322 T2: LDRSB<c> <Rt>,[<Rn>{,#<imm12>}] 2323 T2: LDRSB<c> <Rt>,[<Rn>{,#-<imm8>}] 2324 A: LDRSB<c> <Rt>,[<Rn>{,#+/-<imm8>}] 2325 T2,A: LDRSB<c> <Rt>,[<Rn>],#+/-<imm8> 2326 T2,A: LDRSB<c> <Rt>,[<Rn>,#+/-<imm8>]! 2327 T2,A: LDRSB<c> <Rt>,<label> 2328 T: LDRSB<c> <Rt>,[<Rn>,<Rm>] 2329 T2: LDRSB<c>.W <Rt>,[<Rn>,<Rm>{,LSL #<imm2>}] 2330 A: LDRSB<c> <Rt>,[<Rn>,+/-<Rm>]{!} 2331 A: LDRSB<c> <Rt>,[<Rn>],+/-<Rm> 2332 Unprivileged: 2333 T2: LDRSBT<c> <Rt>,[<Rn>{,#<imm8>}] 2334 A: LDRSBT<c> <Rt>,[<Rn>]{,#+/-<imm8>} 2335 A: LDRSBT<c> <Rt>,[<Rn>],+/-<Rm> 2336 ```````````````````````````````````````````````````````````````````````` *) 2337(* The decoder should guarantee: signed \/ half *) 2338val load_halfword_instr_def = iDefine` 2339 load_halfword_instr ii enc 2340 (Load_Halfword indx add w signed half unpriv n t mode3) = 2341 let wback = ~indx \/ w in 2342 null_check_instruction ii "load_halfword" n 2343 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 2344 (\version. 2345 unpriv /\ (if enc = Encoding_Thumb2 then 2346 ~indx \/ ~add \/ w 2347 else 2348 indx \/ ~w) \/ 2349 ~signed /\ ~half \/ 2350 (if enc = Encoding_Thumb2 then BadReg t else t = 15w) \/ 2351 wback /\ ((n = 15w) \/ (n = t)) \/ 2352 (case mode3 2353 of Mode3_register imm2 m => 2354 if enc = Encoding_Thumb2 then 2355 BadReg m 2356 else 2357 (m = 15w) \/ wback /\ version < 6 /\ (m = n) 2358 | Mode3_immediate imm12 => F)) 2359 ((if is_mode3_immediate mode3 then 2360 read_reg_literal ii n 2361 else 2362 read_reg ii n) >>= 2363 (\base. 2364 address_mode3 ii indx add base mode3 >>= 2365 (\(offset_addr,address). 2366 (increment_pc ii enc ||| 2367 condT wback (write_reg ii n offset_addr) ||| 2368 (if half then 2369 (if unpriv then 2370 read_memU_unpriv ii (address,2) 2371 else 2372 read_memU ii (address,2)) >>= 2373 (\data. 2374 (unaligned_support ii >>= 2375 (\has_unaligned_support. 2376 if has_unaligned_support \/ aligned(address,2) then 2377 if signed then 2378 write_reg ii t (sign_extend32 data) 2379 else 2380 write_reg ii t (zero_extend32 data) 2381 else 2382 write_reg ii t UNKNOWN))) 2383 else 2384 (if unpriv then 2385 read_memU_unpriv ii (address,1) 2386 else 2387 read_memU ii (address,1)) >>= 2388 (\data. 2389 write_reg ii t (sign_extend32 data)))) >>= 2390 unit3)))`; 2391 2392(* ........................................................................ 2393 T: STRH<c> <Rt>,[<Rn>{,#<imm>}] 2394 T2: STRH<c>.W <Rt>,[<Rn>{,#<imm12>}] 2395 T2: STRH<c> <Rt>,[<Rn>{,#-<imm8>}] 2396 A: STRH<c> <Rt>,[<Rn>{,#+/-<imm8>}] 2397 T2,A: STRH<c> <Rt>,[<Rn>],#+/-<imm8> 2398 T2,A: STRH<c> <Rt>,[<Rn>,#+/-<imm8>]! 2399 T: STRH<c> <Rt>,[<Rn>,<Rm>] 2400 T2: STRH<c>.W <Rt>,[<Rn>,<Rm>{,LSL #<imm2>}] 2401 A: STRH<c> <Rt>,[<Rn>,+/-<Rm>]{!} 2402 A: STRH<c> <Rt>,[<Rn>],+/-<Rm> 2403 Unprivileged: 2404 T2: STRHT<c> <Rt>,[<Rn>{,#<imm8>}] 2405 A: STRHT<c> <Rt>,[<Rn>]{,#+/-<imm8>} 2406 A: STRHT<c> <Rt>,[<Rn>],+/-<Rm> 2407 ```````````````````````````````````````````````````````````````````````` *) 2408val store_halfword_instr_def = iDefine` 2409 store_halfword_instr ii enc (Store_Halfword indx add w unpriv n t mode3) = 2410 let wback = ~indx \/ w in 2411 null_check_instruction ii "store_halfword" n 2412 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 2413 (\version. 2414 unpriv /\ (if enc = Encoding_Thumb2 then 2415 ~indx \/ ~add \/ w 2416 else 2417 indx \/ ~w) \/ 2418 (if enc = Encoding_Thumb2 then BadReg t else t = 15w) \/ 2419 wback /\ ((n = 15w) \/ (n = t)) \/ 2420 (case mode3 2421 of Mode3_register imm2 m => 2422 if enc = Encoding_Thumb2 then 2423 BadReg m 2424 else 2425 (m = 15w) \/ wback /\ version < 6 /\ (m = n) 2426 | Mode3_immediate imm12 => F)) 2427 ((read_reg ii n ||| read_reg ii t) >>= 2428 (\(base,rt). 2429 address_mode3 ii indx add base mode3 >>= 2430 (\(offset_addr,address). 2431 ((unaligned_support ii >>= 2432 (\has_unaligned_support. 2433 let data = if has_unaligned_support \/ aligned(address,2) 2434 then bytes(rt,2) 2435 else BITS16_UNKNOWN 2436 in 2437 (if unpriv then 2438 write_memU_unpriv ii (address,2) data 2439 else 2440 write_memU ii (address,2) data))) ||| 2441 increment_pc ii enc ||| 2442 condT wback (write_reg ii n offset_addr)) >>= 2443 unit3)))`; 2444 2445(* ........................................................................ 2446 T,A: POP<c> <registers> 2447 T2: POP<c>.W <registers> 2448 T: LDM<c> <Rn>!,<registers> (<Rn> not included in <registers>) 2449 T: LDM<c> <Rn>,<registers> (<Rn> included in <registers>) 2450 T2: LDM<c>.W <Rn>{!},<registers> 2451 A: LDM<c> <Rn>{!},<registers> 2452 A: LDMDA<c> <Rn>{!},<registers> 2453 T2,A: LDMDB<c> <Rn>{!},<registers> 2454 A: LDMIB<c> <Rn>{!},<registers> 2455 Exception return: 2456 A: LDM{<amode>}<c> <Rn>{!},<registers_with_pc>^ 2457 User registers: 2458 A: LDM{<amode>}<c> <Rn>,<registers_without_pc>^ 2459 where <amode> is DA, DB, IA or IB. 2460 ```````````````````````````````````````````````````````````````````````` *) 2461val load_multiple_instr_def = iDefine` 2462 load_multiple_instr ii enc (Load_Multiple indx add system wback n registers) = 2463 null_check_instruction ii "load_multiple" n 2464 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 2465 (\version. 2466 (n = 15w) \/ bit_count registers < 1 \/ 2467 (enc = Encoding_Thumb2) /\ 2468 (system \/ bit_count registers < 2 \/ 2469 registers ' 15 /\ registers ' 14 \/ registers ' 13) \/ 2470 system /\ wback /\ ~(registers ' 15) \/ 2471 wback /\ registers ' (w2n n) /\ 2472 ((enc = Encoding_Thumb2) \/ version >= 7)) 2473 ((read_reg ii n ||| read_cpsr ii) >>= 2474 (\(base,cpsr). 2475 let mode = if system /\ ~(registers ' 15) then 0b10000w else cpsr.M 2476 and length = n2w (4 * bit_count registers) in 2477 let base_address = if add then base else base - length in 2478 let start_address = if indx = add then base_address + 4w 2479 else base_address 2480 in 2481 let address i = start_address + 2482 n2w (4 * (bit_count_upto (i + 1) registers - 1)) 2483 in 2484 forT 0 14 2485 (\i. condT (registers ' i) 2486 (read_memA ii (address i,4) >>= 2487 (\d. write_reg_mode ii (n2w i,mode) (word32 d)))) >>= 2488 (\unit_list:unit list. 2489 condT wback 2490 (if ~(registers ' (w2n n)) then 2491 if add then 2492 write_reg ii n (base + length) 2493 else 2494 write_reg ii n (base - length) 2495 else 2496 write_reg ii n UNKNOWN) >>= 2497 (\u:unit. 2498 if registers ' 15 then 2499 read_memA ii (address 15,4) >>= 2500 (\d. 2501 if system then 2502 current_mode_is_user_or_system ii >>= 2503 (\is_user_or_system. 2504 if is_user_or_system then 2505 errorT "load_multiple_instr: unpredictable" 2506 else 2507 read_spsr ii >>= 2508 (\spsr. 2509 cpsr_write_by_instr ii (encode_psr spsr, 0b1111w, T) 2510 >>= (\u. branch_write_pc ii (word32 d)))) 2511 else 2512 load_write_pc ii (word32 d)) 2513 else 2514 increment_pc ii enc))))`; 2515 2516 2517(* ........................................................................ 2518 T,A: PUSH<c> <registers> 2519 T2: PUSH<c>.W <registers> 2520 T: STM<c> <Rn>!,<registers> 2521 T2: STM<c>.W <Rn>{!},<registers> 2522 A: STM<c> <Rn>{!},<registers> 2523 A: STMDA<c> <Rn>{!},<registers> 2524 T2,A: STMDB<c> <Rn>{!},<registers> 2525 A: STMIB<c> <Rn>{!},<registers> 2526 User registers: 2527 A: STM{<amode>}<c> <Rn>,<registers>^ 2528 where <amode> is DA, DB, IA or IB. 2529 ```````````````````````````````````````````````````````````````````````` *) 2530val store_multiple_instr_def = iDefine` 2531 store_multiple_instr ii enc 2532 (Store_Multiple indx add system wback n registers) = 2533 null_check_instruction ii "store_multiple" n 2534 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 2535 (\v. (n = 15w) \/ bit_count registers < 1 \/ 2536 (enc = Encoding_Thumb2) /\ 2537 (bit_count registers < 2 \/ 2538 registers ' 15 \/ registers ' 13 \/ 2539 wback /\ registers ' (w2n n)) \/ 2540 system /\ wback) 2541 (current_mode_is_user_or_system ii >>= 2542 (\is_user_or_system. 2543 if system /\ is_user_or_system then 2544 errorT "store_multiple_instr: unpredictable" 2545 else 2546 (read_reg ii n ||| read_cpsr ii) >>= 2547 (\(base,cpsr). 2548 let mode = if system then 0b10000w else cpsr.M 2549 and length = n2w (4 * bit_count registers) 2550 and lowest = lowest_set_bit registers 2551 in 2552 let base_address = if add then base else base - length in 2553 let start_address = if indx = add then base_address + 4w 2554 else base_address 2555 in 2556 let address i = start_address + 2557 n2w (4 * (bit_count_upto (i + 1) registers - 1)) 2558 in 2559 forT 0 14 2560 (\i. condT (registers ' i) 2561 (if (i = w2n n) /\ wback /\ (i <> lowest) then 2562 write_memA ii (address i,4) BITS32_UNKNOWN 2563 else 2564 read_reg_mode ii (n2w i,mode) >>= 2565 (\d. write_memA ii (address i,4) (bytes(d,4))))) >>= 2566 (\unit_list:unit list. 2567 (condT (registers ' 15) 2568 (pc_store_value ii >>= 2569 (\pc. write_memA ii (address 15,4) (bytes(pc,4)))) ||| 2570 increment_pc ii enc ||| 2571 condT wback 2572 (if add then 2573 write_reg ii n (base + length) 2574 else 2575 write_reg ii n (base - length))) >>= 2576 unit3))))`; 2577 2578(* ........................................................................ 2579 T2: LDRD<c> <Rt>,<Rt2>,[<Rn>{,#+/-<imm>}] 2580 T2: LDRD<c> <Rt>,<Rt2>,[<Rn>],#+/-<imm> 2581 T2: LDRD<c> <Rt>,<Rt2>,[<Rn>,#+/-<imm>]! 2582 A: LDRD<c> <Rt>,<Rt2>,[<Rn>{,#+/-<imm8>}] 2583 A: LDRD<c> <Rt>,<Rt2>,[<Rn>],#+/-<imm8> 2584 A: LDRD<c> <Rt>,<Rt2>,[<Rn>,#+/-<imm8>]! 2585 T2,A: LDRD<c> <Rt>,<Rt2>,<label> 2586 A: LDRD<c> <Rt>,<Rt2>,[<Rn>,#+/-<Rm>]{!} 2587 A: LDRD<c> <Rt>,<Rt2>,[<Rn>],#+/-<Rm> 2588 ```````````````````````````````````````````````````````````````````````` *) 2589val load_dual_instr_def = iDefine` 2590 load_dual_instr ii enc (Load_Dual indx add w n t t2 mode3) = 2591 let wback = ~indx \/ w in 2592 null_check_instruction ii "load_dual" n (ARCH2 enc {a | a IN dsp_support}) 2593 (\version. 2594 (if enc = Encoding_Thumb2 then 2595 BadReg t \/ BadReg t2 \/ (t = t2) 2596 else 2597 ~indx /\ w \/ t ' 0 \/ t2 <> t + 1w \/ (t2 = 15w)) \/ 2598 (case mode3 2599 of Mode3_register imm2 m => 2600 (imm2 <> 0w) \/ (m = 15w) \/ (m = t) \/ (m = t2) \/ 2601 version < 6 /\ wback /\ (m = n) 2602 | Mode3_immediate imm12 => F) \/ 2603 wback /\ ((n = 15w) \/ (n = t) \/ (n = t2))) 2604 ((if is_mode3_immediate mode3 then 2605 read_reg_literal ii n 2606 else 2607 read_reg ii n) >>= 2608 (\base. 2609 address_mode3 ii indx add base mode3 >>= 2610 (\(offset_addr,address). 2611 (increment_pc ii enc ||| 2612 condT wback (write_reg ii n offset_addr) ||| 2613 read_memA ii (address,4) >>= 2614 (\data. write_reg ii t (word32 data)) ||| 2615 read_memA ii (address + 4w,4) >>= 2616 (\data. write_reg ii t2 (word32 data))) >>= 2617 unit4)))`; 2618 2619(* ........................................................................ 2620 T2: STRD<c> <Rt>,<Rt2>,[<Rn>{,#+/-<imm>}] 2621 T2: STRD<c> <Rt>,<Rt2>,[<Rn>],#+/-<imm> 2622 T2: STRD<c> <Rt>,<Rt2>,[<Rn>,#+/-<imm>]! 2623 A: STRD<c> <Rt>,<Rt2>,[<Rn>{,#+/-<imm8>}] 2624 A: STRD<c> <Rt>,<Rt2>,[<Rn>],#+/-<imm8> 2625 A: STRD<c> <Rt>,<Rt2>,[<Rn>,#+/-<imm8>]! 2626 A: STRD<c> <Rt>,<Rt2>,[<Rn>,#+/-<Rm>]{!} 2627 A: STRD<c> <Rt>,<Rt2>,[<Rn>],#+/-<Rm> 2628 ```````````````````````````````````````````````````````````````````````` *) 2629val store_dual_instr_def = iDefine` 2630 store_dual_instr ii enc (Store_Dual indx add w n t t2 mode3) = 2631 let wback = ~indx \/ w in 2632 null_check_instruction ii "store_dual" n 2633 (ARCH2 enc {a | a IN dsp_support}) 2634 (\version. 2635 (if enc = Encoding_Thumb2 then 2636 (n = 15w) \/ BadReg t \/ BadReg t2 2637 else 2638 ~indx /\ w \/ t ' 0 \/ t2 <> t + 1w \/ (t2 = 15w)) \/ 2639 (case mode3 2640 of Mode3_register imm2 m => 2641 (imm2 <> 0w) \/ (m = 15w) \/ version < 6 /\ wback /\ (m = n) 2642 | Mode3_immediate imm12 => 2643 F) \/ 2644 wback /\ ((n = 15w) \/ (n = t) \/ (n = t2))) 2645 ((read_reg ii n ||| read_reg ii t ||| read_reg ii t2) >>= 2646 (\(base,rt,rt2). 2647 address_mode3 ii indx add base mode3 >>= 2648 (\(offset_addr,address). 2649 (increment_pc ii enc ||| 2650 condT wback (write_reg ii n offset_addr) ||| 2651 write_memA ii (address,4) (bytes(rt,4)) ||| 2652 write_memA ii (address + 4w,4) (bytes(rt2,4))) >>= 2653 unit4)))`; 2654 2655(* ........................................................................ 2656 T2: LDREX<c> <Rt>,[<Rn>{,#<imm>}] 2657 A: LDREX<c> <Rt>,[<Rn>] 2658 ```````````````````````````````````````````````````````````````````````` *) 2659val load_exclusive_instr_def = iDefine` 2660 load_exclusive_instr ii enc (Load_Exclusive n t imm8) = 2661 null_check_instruction ii "load_exclusive" n 2662 (ARCH2 enc {a | version_number a >= 6}) 2663 (\v. (if enc = Encoding_Thumb2 then BadReg t else t = 15w) \/ (n = 15w)) 2664 ((increment_pc ii enc ||| 2665 read_reg ii n >>= 2666 (\rn. let address = rn + (w2w imm8) << 2 in 2667 set_exclusive_monitors ii (address,4) >>= 2668 (\u:unit. read_memA ii (address,4) >>= 2669 (\d. write_reg ii t (word32 d))))) >>= 2670 unit2)`; 2671 2672(* ........................................................................ 2673 T2: STREX<c> <Rd>,<Rt>,[<Rn>{,#<imm>}] 2674 A: STREX<c> <Rd>,<Rt>,[<Rn>] 2675 ```````````````````````````````````````````````````````````````````````` *) 2676val store_exclusive_instr_def = iDefine` 2677 store_exclusive_instr ii enc (Store_Exclusive n d t imm8) = 2678 null_check_instruction ii "store_exclusive" n 2679 (ARCH2 enc {a | version_number a >= 6}) 2680 (\v. (if enc = Encoding_Thumb2 then 2681 BadReg d \/ BadReg t 2682 else 2683 (d = 15w) \/ (t = 15w) \/ (imm8 <> 0w)) \/ 2684 (n = 15w) \/ (d = n) \/ (d = t)) 2685 ((increment_pc ii enc ||| 2686 read_reg ii n >>= 2687 (\rn. let address = rn + (w2w imm8) << 2 in 2688 (exclusive_monitors_pass ii (address,4) >>= 2689 (\pass. 2690 if pass then 2691 read_reg ii t >>= 2692 (\rt. 2693 (write_memA ii (address,4) (bytes(rt,4)) ||| 2694 write_reg ii d 0w) >>= 2695 unit2) 2696 else 2697 write_reg ii d 1w)))) >>= 2698 unit2)`; 2699 2700(* ........................................................................ 2701 T2,A: LDREXD<c> <Rt>,<Rt2>,[<Rn>] 2702 ```````````````````````````````````````````````````````````````````````` *) 2703val load_exclusive_doubleword_instr_def = iDefine` 2704 load_exclusive_doubleword_instr ii enc (Load_Exclusive_Doubleword n t t2) = 2705 null_check_instruction ii "load_exclusive_doubleword" n 2706 (ARCH (if enc = Encoding_Thumb2 then 2707 {a | version_number a >= 7} 2708 else 2709 kernel_support)) 2710 (\v. (if enc = Encoding_Thumb2 then 2711 BadReg t \/ BadReg t2 \/ (t = t2) 2712 else 2713 t ' 0 \/ (t = 0b1110w)) \/ (n = 15w)) 2714 ((increment_pc ii enc ||| 2715 read_reg ii n >>= 2716 (\address. 2717 set_exclusive_monitors ii (address,8) >>= 2718 (\u:unit. (read_memA ii (address,8) ||| big_endian ii) >>= 2719 (\(d,E). let value = word64 d in 2720 write_reg ii t 2721 (if E then (63 >< 32) value else (31 >< 0) value) ||| 2722 write_reg ii (t + 1w) 2723 (if E then (31 >< 0) value else (63 >< 32) value))))) >>= 2724 (\(u1:unit,u2:unit # unit). constT ()))`; 2725 2726(* ........................................................................ 2727 T2,A: STREXD<c> <Rd>,<Rt>,<Rt2>,[<Rn>] 2728 ```````````````````````````````````````````````````````````````````````` *) 2729val store_exclusive_doubleword_instr_def = iDefine` 2730 store_exclusive_doubleword_instr ii enc 2731 (Store_Exclusive_Doubleword n d t t2) = 2732 null_check_instruction ii "store_exclusive_doubleword" n 2733 (ARCH (if enc = Encoding_Thumb2 then 2734 {a | version_number a >= 7} 2735 else 2736 kernel_support)) 2737 (\v. (if enc = Encoding_Thumb2 then 2738 BadReg d \/ BadReg t \/ BadReg t2 2739 else 2740 (d = 15w) \/ t ' 0 \/ (t = 0b1110w)) \/ 2741 (n = 15w) \/ (d = n) \/ (d = t) \/ (d = t2)) 2742 ((increment_pc ii enc ||| 2743 read_reg ii n >>= 2744 (\address. 2745 exclusive_monitors_pass ii (address,8) >>= 2746 (\pass. 2747 if pass then 2748 (read_reg ii t ||| read_reg ii t2 ||| big_endian ii) >>= 2749 (\(rt,rt2,E). 2750 let value = if E then bytes(rt,4) ++ bytes(rt2,4) 2751 else bytes(rt2,4) ++ bytes(rt,4) 2752 in 2753 (write_memA ii (address,8) value ||| 2754 write_reg ii d 0w) >>= 2755 unit2) 2756 else 2757 write_reg ii d 1w))) >>= 2758 unit2)`; 2759 2760(* ........................................................................ 2761 T2,A: LDREXB<c> <Rt>,[<Rn>] 2762 ```````````````````````````````````````````````````````````````````````` *) 2763val load_exclusive_byte_instr_def = iDefine` 2764 load_exclusive_byte_instr ii enc (Load_Exclusive_Byte n t) = 2765 null_check_instruction ii "load_exclusive_byte" n 2766 (ARCH (if enc = Encoding_Thumb2 then 2767 {a | version_number a >= 7} 2768 else 2769 kernel_support)) 2770 (\v. (if enc = Encoding_Thumb2 then BadReg t else t = 15w) \/ (n = 15w)) 2771 ((increment_pc ii enc ||| 2772 read_reg ii n >>= 2773 (\address. 2774 set_exclusive_monitors ii (address,1) >>= 2775 (\u:unit. read_memA ii (address,1) >>= 2776 (\d. write_reg ii t (zero_extend32 d))))) >>= 2777 unit2)`; 2778 2779(* ........................................................................ 2780 T2,A: STREXB<c> <Rd>,<Rt>,[<Rn>] 2781 ```````````````````````````````````````````````````````````````````````` *) 2782val store_exclusive_byte_instr_def = iDefine` 2783 store_exclusive_byte_instr ii enc (Store_Exclusive_Byte n d t) = 2784 null_check_instruction ii "store_exclusive_byte" n 2785 (ARCH (if enc = Encoding_Thumb2 then 2786 {a | version_number a >= 7} 2787 else 2788 kernel_support)) 2789 (\v. (if enc = Encoding_Thumb2 then 2790 BadReg d \/ BadReg t 2791 else 2792 (d = 15w) \/ (t = 15w)) \/ 2793 (n = 15w) \/ (d = n) \/ (d = t)) 2794 ((increment_pc ii enc ||| 2795 read_reg ii n >>= 2796 (\address. 2797 exclusive_monitors_pass ii (address,1) >>= 2798 (\pass. 2799 if pass then 2800 read_reg ii t >>= 2801 (\rt. 2802 (write_memA ii (address,1) (bytes(rt,1)) ||| 2803 write_reg ii d 0w) >>= 2804 unit2) 2805 else 2806 write_reg ii d 1w))) >>= 2807 unit2)`; 2808 2809(* ........................................................................ 2810 T2,A: LDREXH<c> <Rt>,[<Rn>] 2811 ```````````````````````````````````````````````````````````````````````` *) 2812val load_exclusive_halfword_instr_def = iDefine` 2813 load_exclusive_halfword_instr ii enc (Load_Exclusive_Halfword n t) = 2814 null_check_instruction ii "load_exclusive_halfword" n 2815 (ARCH (if enc = Encoding_Thumb2 then 2816 {a | version_number a >= 7} 2817 else 2818 kernel_support)) 2819 (\v. (if enc = Encoding_Thumb2 then BadReg t else t = 15w) \/ (n = 15w)) 2820 ((increment_pc ii enc ||| 2821 read_reg ii n >>= 2822 (\address. 2823 set_exclusive_monitors ii (address,2) >>= 2824 (\u:unit. read_memA ii (address,2) >>= 2825 (\d. write_reg ii t (zero_extend32 d))))) >>= 2826 unit2)`; 2827 2828(* ........................................................................ 2829 T2,A: STREXH<c> <Rd>,<Rt>,[<Rn>] 2830 ```````````````````````````````````````````````````````````````````````` *) 2831val store_exclusive_halfword_instr_def = iDefine` 2832 store_exclusive_halfword_instr ii enc (Store_Exclusive_Halfword n d t) = 2833 null_check_instruction ii "store_exclusive_halfword" n 2834 (ARCH (if enc = Encoding_Thumb2 then 2835 {a | version_number a >= 7} 2836 else 2837 kernel_support)) 2838 (\v. (if enc = Encoding_Thumb2 then 2839 BadReg d \/ BadReg t 2840 else 2841 (d = 15w) \/ (t = 15w)) \/ 2842 (n = 15w) \/ (d = n) \/ (d = t)) 2843 ((increment_pc ii enc ||| 2844 read_reg ii n >>= 2845 (\address. 2846 exclusive_monitors_pass ii (address,2) >>= 2847 (\pass. 2848 if pass then 2849 read_reg ii t >>= 2850 (\rt. 2851 (write_memA ii (address,2) (bytes(rt,2)) ||| 2852 write_reg ii d 0w) >>= 2853 unit2) 2854 else 2855 write_reg ii d 1w))) >>= 2856 unit2)`; 2857 2858(* ........................................................................ 2859 T2: CLREX<c> 2860 A: CLREX 2861 ```````````````````````````````````````````````````````````````````````` *) 2862(* Unpredictable for ARMv4*. *) 2863val clear_exclusive_instr_def = iDefine` 2864 clear_exclusive_instr ii enc = 2865 instruction ii "clear_exclusive" 2866 (ARCH (if enc = Encoding_Thumb2 then 2867 {a | version_number a >= 7} 2868 else 2869 kernel_support)) {} 2870 ((increment_pc ii enc ||| clear_exclusive_local ii) >>= unit2)`; 2871 2872(* ........................................................................ 2873 A: SWP{B}<c> <Rt>,<Rt2>,[<Rn>] (deprecated for version >= 6) 2874 ```````````````````````````````````````````````````````````````````````` *) 2875val swap_instr_def = iDefine` 2876 swap_instr ii (Swap swap_byte n t t2) = 2877 instruction ii "swap" ALL 2878 (\v. (t = 15w) \/ (t2 = 15w) \/ (n = 15w) \/ (n = t) \/ (n = t2)) 2879 (lockT 2880 ((read_reg ii n ||| read_reg ii t2) >>= 2881 (\(address,rt2). 2882 (if swap_byte then 2883 read_memA ii (address,1) ||| 2884 write_memA ii (address,1) (bytes(rt2,1)) 2885 else 2886 read_memA ii (address,4) ||| 2887 write_memA ii (address,4) (bytes(rt2,4))) >>= 2888 (\(d,u:unit). 2889 (increment_pc ii Encoding_ARM ||| 2890 (if swap_byte then 2891 write_reg ii t (zero_extend32 d) 2892 else 2893 write_reg ii t 2894 (ROR (word32 d, 8 * w2n ((1 -- 0) address))))) >>= 2895 unit2))))`; 2896 2897(* ........................................................................ 2898 T2: SRSDB<c> SP{!},#<mode> 2899 T2: SRS{IA}<c> SP{!},#<mode> 2900 A: SRS{<amode>} SP{!},#<mode> 2901 where <amode> is DA, DB, IA or IB. 2902 ```````````````````````````````````````````````````````````````````````` *) 2903(* Unpredictable for ARMv4*. *) 2904val store_return_state_instr_def = iDefine` 2905 store_return_state_instr ii enc (Store_Return_State P inc wback mode) = 2906 (is_secure ii ||| read_nsacr ii) >>= 2907 (\(is_secure,nsacr). 2908 instruction ii "store_return_state" 2909 (ARCH2 enc {a | version_number a >= 6}) 2910 (\v. ~is_secure /\ 2911 ((mode = 0b10110w) \/ (mode = 0b10001w) /\ nsacr.RFR)) 2912 ((current_mode_is_user_or_system ii ||| current_instr_set ii) >>= 2913 (\(is_user_or_system,iset). 2914 if is_user_or_system \/ (iset = InstrSet_ThumbEE) then 2915 errorT "store_return_state_instr: unpredictable" 2916 else 2917 (read_reg_mode ii (13w,mode) ||| read_reg ii 14w ||| 2918 read_spsr ii) >>= 2919 (\(base,lr,spsr). 2920 let wordhigher = (P = inc) 2921 and address = if inc then base else base - 8w 2922 in 2923 let address = if wordhigher then address + 4w else address 2924 in 2925 (increment_pc ii enc ||| 2926 write_memA ii (address,4) (bytes (lr,4)) ||| 2927 write_memA ii (address + 4w,4) (bytes (encode_psr spsr,4)) ||| 2928 condT wback 2929 (write_reg_mode ii (13w,mode) 2930 (if inc then base + 8w else base - 8w))) >>= unit4))))`; 2931 2932(* ........................................................................ 2933 T2: RFEDB<c> <Rn>{!} 2934 T2: RFE{IA}<c> <Rn>{!} 2935 A: RFE{<amode>} <Rn>{!} 2936 where <amode> is DA, DB, IA or IB. 2937 ```````````````````````````````````````````````````````````````````````` *) 2938(* Unpredictable for ARMv4*. *) 2939val return_from_exception_instr_def = iDefine` 2940 return_from_exception_instr ii enc (Return_From_Exception P inc wback n) = 2941 instruction ii "return_from_exception" 2942 (ARCH2 enc {a | version_number a >= 6}) {} 2943 ((current_mode_is_user_or_system ii ||| current_instr_set ii) >>= 2944 (\(is_user_or_system,iset). 2945 if is_user_or_system \/ (iset = InstrSet_ThumbEE) then 2946 errorT "return_from_exception_instr: unpredictable" 2947 else 2948 read_reg ii n >>= 2949 (\base. 2950 let wordhigher = (P = inc) 2951 and address = if inc then base else base - 8w 2952 in 2953 let address = if wordhigher then address + 4w else address 2954 in 2955 (read_memA ii (address + 4w,4) ||| 2956 read_memA ii (address,4)) >>= 2957 (\(d1,d2). 2958 (cpsr_write_by_instr ii (word32 d1, 0b1111w, T) ||| 2959 branch_write_pc ii (word32 d2) ||| 2960 condT wback 2961 (write_reg ii n (if inc then base + 8w else base - 8w))) >>= 2962 unit3))))`; 2963 2964(* ........................................................................ 2965 T2,A: MRS<c> <Rd>,<spec_reg> 2966 where <spec_reg> is APSR, CPSR or SPSR. 2967 ```````````````````````````````````````````````````````````````````````` *) 2968val status_to_register_instr_def = iDefine` 2969 status_to_register_instr ii enc (Status_to_Register readspsr d) = 2970 instruction ii "status_to_register" 2971 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 2972 (\v. if enc = Encoding_Thumb2 then BadReg d else (d = 15w)) 2973 ((increment_pc ii enc ||| 2974 (if readspsr then 2975 current_mode_is_user_or_system ii >>= 2976 (\is_user_or_system_mode. 2977 if is_user_or_system_mode then 2978 errorT "status_to_register_instr: unpredictable" 2979 else 2980 read_spsr ii >>= (\spsr. write_reg ii d (encode_psr spsr))) 2981 else 2982 read_cpsr ii >>= (\cpsr. write_reg ii d 2983 (encode_psr cpsr && 0b11111000_11111111_00000011_11011111w)))) >>= 2984 unit2)`; 2985 2986(* ........................................................................ 2987 A: MSR<c> <spec_reg>,#<const> 2988 where <spec_reg> is APSR_<bits>, CPSR_<fields> or SPSR_<fields> 2989 <bits> is nzcvq, g, or nzcvqg 2990 <fields> is one or more of c, x, s and f. 2991 ```````````````````````````````````````````````````````````````````````` *) 2992val immediate_to_status_instr_def = iDefine` 2993 immediate_to_status_instr ii (Immediate_to_Status writespsr mask imm12) = 2994 instruction ii "immidiate_to_status" ALL (\v. mask = 0w) 2995 (arm_expand_imm ii imm12 >>= 2996 (\imm32. 2997 (increment_pc ii Encoding_ARM ||| 2998 if writespsr then 2999 spsr_write_by_instr ii (imm32,mask) 3000 else 3001 cpsr_write_by_instr ii (imm32,mask,F)) >>= 3002 unit2))`; 3003 3004(* ........................................................................ 3005 T2,A: MSR<c> <spec_reg>,<Rn> 3006 where <spec_reg> is APSR_<bits>, CPSR_<fields> or SPSR_<fields> 3007 <bits> is nzcvq, g, or nzcvqg 3008 <fields> is one or more of c, x, s and f. 3009 ```````````````````````````````````````````````````````````````````````` *) 3010val register_to_status_instr_def = iDefine` 3011 register_to_status_instr ii enc (Register_to_Status writespsr mask n) = 3012 instruction ii "register_to_status" 3013 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 3014 (\v. (mask = 0w) \/ (n = 15w)) 3015 (read_reg ii n >>= 3016 (\rn. 3017 (increment_pc ii enc ||| 3018 if writespsr then 3019 spsr_write_by_instr ii (rn,mask) 3020 else 3021 cpsr_write_by_instr ii (rn,mask,F)) >>= 3022 unit2))`; 3023 3024(* ........................................................................ 3025 T: CPS<effect> <iflags> 3026 T2: CPS<effect>.W <iflags>{,#<mode>} 3027 A: CPS<effect> <iflags>{,#<mode>} 3028 T2,A: CPS #<mode> 3029 where <effect> is IE or ID 3030 <iflags> is one or more of a, i and f. 3031 ```````````````````````````````````````````````````````````````````````` *) 3032(* Unpredictable for ARMv4*. *) 3033val change_processor_state_instr_def = iDefine` 3034 change_processor_state_instr ii enc 3035 (Change_Processor_State imod affectA affectI affectF mode) = 3036 instruction ii "change_processor_state" 3037 (ARCH2 enc {a | version_number a >= 6}) 3038 (\v. ((imod = 0b00w) /\ IS_NONE mode) \/ 3039 (imod ' 1 <=> ~affectA /\ ~affectI /\ ~affectF) \/ 3040 (imod = 0b01w)) 3041 (current_mode_is_priviledged ii >>= 3042 (\current_mode_is_priviledged. 3043 if current_mode_is_priviledged then 3044 read_cpsr ii >>= 3045 (\cpsr. 3046 let enable = (imod = 0b10w) 3047 and disable = (imod = 0b11w) 3048 in 3049 let cpsr_val = word_modify (\i b. 3050 if (i = 8) /\ affectA \/ 3051 (i = 7) /\ affectI \/ 3052 (i = 6) /\ affectF 3053 then 3054 ~enable /\ (disable \/ b) 3055 else if i < 5 /\ IS_SOME mode then 3056 (THE mode) ' i 3057 else 3058 b) (encode_psr cpsr) 3059 in 3060 (cpsr_write_by_instr ii (cpsr_val, 0b1111w, T) ||| 3061 increment_pc ii enc) >>= unit2) 3062 else 3063 increment_pc ii enc))`; 3064 3065(* ........................................................................ 3066 T,A: SETEND <endian_specifier> 3067 where <endian_specifier> is BE or LE. 3068 ```````````````````````````````````````````````````````````````````````` *) 3069(* Unpredictable for ARMv4*. *) 3070val set_endianness_instr_def = iDefine` 3071 set_endianness_instr ii enc (Set_Endianness set_bigend) = 3072 instruction ii "set_endianness" (ARCH {a | version_number a >= 6}) {} 3073 ((write_e ii set_bigend ||| increment_pc ii enc) >>= unit2)`; 3074 3075(* ........................................................................ 3076 T2,A: SMC<c> #<imm4> (previously SMI) 3077 ```````````````````````````````````````````````````````````````````````` *) 3078val secure_monitor_call_instr_def = iDefine` 3079 secure_monitor_call_instr ii = 3080 instruction ii "secure_monitor_call" security_support {} 3081 (current_mode_is_priviledged ii >>= 3082 (\current_mode_is_priviledged. 3083 if current_mode_is_priviledged then 3084 take_smc_exception ii 3085 else 3086 take_undef_instr_exception ii))`; 3087 3088(* ........................................................................ 3089 T: BKPT #<imm8> 3090 A: BKPT #<imm16> 3091 ```````````````````````````````````````````````````````````````````````` *) 3092val breakpoint_instr_def = iDefine` 3093 breakpoint_instr ii = 3094 instruction ii "breakpoint" (ARCH {a | version_number a >= 5}) {} 3095 (take_prefetch_abort_exception ii)`; 3096 3097(* ........................................................................ 3098 T2: DMB<c> <option> 3099 A: DMB <option> 3100 where <option> is SY, ST, ISH, ISHST, NSH, NSHST, OSH or OSHST. 3101 ```````````````````````````````````````````````````````````````````````` *) 3102(* Unpredictable for ARMv4*. *) 3103val data_memory_barrier_instr_def = iDefine` 3104 data_memory_barrier_instr ii enc (Data_Memory_Barrier option) = 3105 instruction ii "data_memory_barrier" (ARCH {a | version_number a >= 7}) {} 3106 ((increment_pc ii enc ||| 3107 data_memory_barrier ii (barrier_option option)) >>= unit2)`; 3108 3109(* ........................................................................ 3110 T2: DSB<c> <option> 3111 A: DSB <option> 3112 where <option> is SY, ST, ISH, ISHST, NSH, NSHST, OSH or OSHST. 3113 ```````````````````````````````````````````````````````````````````````` *) 3114(* Unpredictable for ARMv4*. *) 3115val data_synchronization_barrier_instr_def = iDefine` 3116 data_synchronization_barrier_instr ii enc 3117 (Data_Synchronization_Barrier option) = 3118 instruction ii "data_synchronization_barrier" 3119 (ARCH {a | version_number a >= 7}) {} 3120 ((increment_pc ii enc ||| 3121 data_synchronization_barrier ii (barrier_option option)) >>= unit2)`; 3122 3123(* ........................................................................ 3124 T2: ISB<c> <option> 3125 A: ISB <option> 3126 where <option> is optionally SY. 3127 ```````````````````````````````````````````````````````````````````````` *) 3128(* Unpredictable for ARMv4*. *) 3129val instruction_synchronization_barrier_instr_def = iDefine` 3130 instruction_synchronization_barrier_instr ii enc 3131 (Instruction_Synchronization_Barrier option) = 3132 instruction ii "instruction_synchronization_barrier" 3133 (ARCH {a | version_number a >= 7}) {} 3134 ((increment_pc ii enc ||| 3135 instruction_synchronization_barrier ii) >>= unit2)`; 3136 3137(* ........................................................................ 3138 T2,A: CDP{2}<c> <coproc>,#<opc1>,<CRd>,<CRn>,<CRm>{,#<opc2>} 3139 ```````````````````````````````````````````````````````````````````````` *) 3140(* If cond = 15w then Unpredictable for ARMv4*. *) 3141val coprocessor_data_processing_instr_def = iDefine` 3142 coprocessor_data_processing_instr ii enc cond 3143 (Coprocessor_Data_Processing opc1 crn crd coproc opc2 crm) = 3144 instruction ii "coprocessor_data_processing" 3145 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) {} 3146 (let ThisInstr = 3147 (cond,Coprocessor_Data_Processing opc1 crn crd coproc opc2 crm) 3148 in 3149 coproc_accepted ii (coproc,ThisInstr) >>= 3150 (\accepted. 3151 if ~accepted then 3152 take_undef_instr_exception ii 3153 else 3154 (increment_pc ii enc ||| 3155 coproc_internal_operation ii (coproc,ThisInstr)) >>= 3156 unit2))`; 3157 3158(* ........................................................................ 3159 T2,A: LDC{2}{L}<c> <coproc>,<CRd>,[<Rn>{,#+/-<imm>}] 3160 T2,A: LDC{2}{L}<c> <coproc>,<CRd>,[<Rn>,#+/-<imm>]! 3161 T2,A: LDC{2}{L}<c> <coproc>,<CRd>,[<Rn>],#+/-<imm> 3162 T2,A: LDC{2}{L}<c> <coproc>,<CRd>,[<Rn>],<option> 3163 ```````````````````````````````````````````````````````````````````````` *) 3164(* If cond = 15w then Unpredictable for ARMv4*. *) 3165val coprocessor_load_instr_def = iDefine` 3166 coprocessor_load_instr ii enc cond 3167 (Coprocessor_Load p u d w rn crd coproc mode5) = 3168 current_instr_set ii >>= 3169 (\iset. 3170 instruction ii "coprocessor_load" 3171 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 3172 (\v. (rn = 15w) /\ (w \/ (~p /\ (iset <> InstrSet_ARM)))) 3173 (let ThisInstr = (cond,Coprocessor_Load p u d w rn crd coproc mode5) 3174 in 3175 coproc_accepted ii (coproc,ThisInstr) >>= 3176 (\accepted. 3177 if ~accepted then 3178 take_undef_instr_exception ii 3179 else 3180 read_reg_literal ii rn >>= 3181 (\base. 3182 address_mode5 p u base mode5 >>= 3183 (\(offset_addr,address). 3184 let readm i = 3185 (read_memA ii (address + n2w (4 * i),4)) >>= 3186 (\data. constT (word32 data)) 3187 in 3188 (coproc_send_loaded_words ii 3189 (readm,coproc,ThisInstr) ||| 3190 increment_pc ii enc ||| 3191 condT w (write_reg ii rn offset_addr)) >>= 3192 unit3)))))`; 3193 3194(* ........................................................................ 3195 T2,A: STC{2}{L}<c> <coproc>,<CRd>,[<Rn>{,#+/-<imm>}] 3196 T2,A: STC{2}{L}<c> <coproc>,<CRd>,[<Rn>,#+/-<imm>]! 3197 T2,A: STC{2}{L}<c> <coproc>,<CRd>,[<Rn>],#+/-<imm> 3198 T2,A: STC{2}{L}<c> <coproc>,<CRd>,[<Rn>],<option> 3199 ```````````````````````````````````````````````````````````````````````` *) 3200(* If cond = 15w then Unpredictable for ARMv4*. *) 3201val coprocessor_store_instr_def = iDefine` 3202 coprocessor_store_instr ii enc cond 3203 (Coprocessor_Store p u d w rn crd coproc mode5) = 3204 current_instr_set ii >>= 3205 (\iset. 3206 instruction ii "coprocessor_store" 3207 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 3208 (\v. (rn = 15w) /\ (w \/ (iset <> InstrSet_ARM))) 3209 (let ThisInstr = (cond,Coprocessor_Store p u d w rn crd coproc mode5) 3210 in 3211 coproc_accepted ii (coproc,ThisInstr) >>= 3212 (\accepted. 3213 if ~accepted then 3214 take_undef_instr_exception ii 3215 else 3216 read_reg ii rn >>= 3217 (\base. 3218 (coproc_get_words_to_store ii (coproc,ThisInstr) ||| 3219 address_mode5 p u base mode5) >>= 3220 (\(data,offset_addr,start_address). 3221 let address i = start_address + n2w (4 * i) in 3222 (forT 0 (LENGTH data - 1) 3223 (\i. write_memA ii (address i,4) 3224 (bytes(EL i data,4))) ||| 3225 increment_pc ii enc ||| 3226 condT w (write_reg ii rn offset_addr)) >>= 3227 (\(unit_list:unit list,u2:unit,u3:unit). constT ()))))))`; 3228 3229(* ........................................................................ 3230 T2,A: MRC{2}<c> <coproc>,#<opc1>,<Rt>,<CRn>,<CRm>{,#<opc2>} 3231 ```````````````````````````````````````````````````````````````````````` *) 3232(* If cond = 15w then Unpredictable for ARMv4*. *) 3233val coprocessor_register_to_arm_instr_def = iDefine` 3234 coprocessor_register_to_arm_instr ii enc cond 3235 (Coprocessor_Transfer opc1 T crn rt coproc opc2 crm) = 3236 current_instr_set ii >>= 3237 (\iset. 3238 instruction ii "coprocessor_register_to_arm" 3239 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 3240 (\v. (rt = 13w) /\ (iset <> InstrSet_ARM)) 3241 (let ThisInstr = 3242 (cond,Coprocessor_Transfer opc1 T crn rt coproc opc2 crm) 3243 in 3244 coproc_accepted ii (coproc,ThisInstr) >>= 3245 (\accepted. 3246 if ~accepted then 3247 take_undef_instr_exception ii 3248 else 3249 coproc_get_one_word ii (coproc,ThisInstr) >>= 3250 (\value. 3251 (increment_pc ii enc ||| 3252 if rt <> 15w then 3253 write_reg ii rt value 3254 else 3255 write_flags ii 3256 (value ' 31,value ' 30,value ' 29,value ' 28)) >>= 3257 unit2))))`; 3258 3259(* ........................................................................ 3260 T2,A: MCR{2}<c> <coproc>,#<opc1>,<Rt>,<CRn>,<CRm>{,#<opc2>} 3261 ```````````````````````````````````````````````````````````````````````` *) 3262(* If cond = 15w then Unpredictable for ARMv4*. *) 3263val arm_register_to_coprocessor_instr_def = iDefine` 3264 arm_register_to_coprocessor_instr ii enc cond 3265 (Coprocessor_Transfer opc1 F crn rt coproc opc2 crm) = 3266 current_instr_set ii >>= 3267 (\iset. 3268 instruction ii "arm_register_to_coprocessor" 3269 (if enc = Encoding_Thumb2 then ARCH thumb2_support else ALL) 3270 (\v. (rt = 15w) \/ (rt = 13w) /\ (iset <> InstrSet_ARM)) 3271 (let ThisInstr = 3272 (cond,Coprocessor_Transfer opc1 F crn rt coproc opc2 crm) 3273 in 3274 coproc_accepted ii (coproc,ThisInstr) >>= 3275 (\accepted. 3276 if ~accepted then 3277 take_undef_instr_exception ii 3278 else 3279 read_reg ii rt >>= 3280 (\value. 3281 (increment_pc ii enc ||| 3282 coproc_send_one_word ii (value,coproc,ThisInstr)) >>= 3283 unit2))))`; 3284 3285(* ........................................................................ 3286 T2,A: MRRC{2}<c> <coproc>,#<opc1>,<Rt>,<Rt2>,<CRm> 3287 ```````````````````````````````````````````````````````````````````````` *) 3288(* If cond = 15w then Unpredictable for ARMv4*. *) 3289val coprocessor_register_to_arm_two_instr_def = iDefine` 3290 coprocessor_register_to_arm_two_instr ii enc cond 3291 (Coprocessor_Transfer_Two T rt2 rt coproc opc1 crm) = 3292 current_instr_set ii >>= 3293 (\iset. 3294 instruction ii "coprocessor_register_to_arm_two" 3295 (ARCH {a | if enc = Encoding_Thumb2 then 3296 a IN thumb2_support 3297 else if cond = 15w then 3298 version_number a >= 6 3299 else 3300 a IN dsp_support}) 3301 (\v. (rt = 15w) \/ (rt2 = 15w) \/ (rt = rt2) \/ 3302 ((rt = 13w) \/ (rt2 = 13w)) /\ (iset <> InstrSet_ARM)) 3303 (let ThisInstr = 3304 (cond,Coprocessor_Transfer_Two T rt2 rt coproc opc1 crm) 3305 in 3306 coproc_accepted ii (coproc,ThisInstr) >>= 3307 (\accepted. 3308 if ~accepted then 3309 take_undef_instr_exception ii 3310 else 3311 coproc_get_two_words ii (coproc,ThisInstr) >>= 3312 (\(data1,data2). 3313 (increment_pc ii enc ||| 3314 write_reg ii rt data1 ||| 3315 write_reg ii rt2 data2) >>= 3316 unit3))))`; 3317 3318(* ........................................................................ 3319 T2,A: MCRR{2}<c> <coproc>,#<opc1>,<Rt>,<Rt2>,<CRm> 3320 ```````````````````````````````````````````````````````````````````````` *) 3321(* If cond = 15w then Unpredictable for ARMv4*. *) 3322val arm_register_to_coprocessor_two_instr_def = iDefine` 3323 arm_register_to_coprocessor_two_instr ii enc cond 3324 (Coprocessor_Transfer_Two F rt2 rt coproc opc1 crm) = 3325 current_instr_set ii >>= 3326 (\iset. 3327 instruction ii "arm_register_to_coprocessor_two" 3328 (ARCH {a | if enc = Encoding_Thumb2 then 3329 a IN thumb2_support 3330 else if cond = 15w then 3331 version_number a >= 6 3332 else 3333 a IN dsp_support}) 3334 (\v. (rt = 15w) \/ (rt2 = 15w) \/ 3335 ((rt = 13w) \/ (rt2 = 13w)) /\ (iset <> InstrSet_ARM)) 3336 (let ThisInstr = 3337 (cond,Coprocessor_Transfer_Two F rt2 rt coproc opc1 crm) 3338 in 3339 coproc_accepted ii (coproc,ThisInstr) >>= 3340 (\accepted. 3341 if ~accepted then 3342 take_undef_instr_exception ii 3343 else 3344 (read_reg ii rt ||| read_reg ii rt2) >>= 3345 (\data. 3346 (increment_pc ii enc ||| 3347 coproc_send_two_words ii (data,coproc,ThisInstr)) >>= 3348 unit2))))`; 3349 3350(* ........................................................................ 3351 T,A: NOP<c> 3352 T2: NOP<c>.W 3353 ```````````````````````````````````````````````````````````````````````` *) 3354val no_operation_instr_def = iDefine` 3355 no_operation_instr ii enc = 3356 instruction ii "no_operation" 3357 (ARCH {a | a IN thumb2_support \/ (enc = Encoding_ARM) /\ (a = ARMv6K)}) 3358 {} (increment_pc ii enc)`; 3359 3360(* ........................................................................ 3361 T,A: YIELD<c> 3362 T2: YIELD<c>.W 3363 ```````````````````````````````````````````````````````````````````````` *) 3364val yield_instr_def = iDefine` 3365 yield_instr ii enc = 3366 read_arch ii >>= 3367 (\arch. 3368 if arch = ARMv6T2 then 3369 no_operation_instr ii enc 3370 else 3371 instruction ii "yield" 3372 (ARCH (if enc = Encoding_ARM then 3373 kernel_support 3374 else 3375 {a | version_number a >= 7})) {} 3376 ((increment_pc ii enc ||| hint_yield ii) >>= unit2))`; 3377 3378(* ........................................................................ 3379 T,A: WFE<c> 3380 T2: WFE<c>.W 3381 ```````````````````````````````````````````````````````````````````````` *) 3382val wait_for_event_instr_def = iDefine` 3383 wait_for_event_instr ii enc = 3384 read_arch ii >>= 3385 (\arch. 3386 if arch = ARMv6T2 then 3387 no_operation_instr ii enc 3388 else 3389 instruction ii "wait_for_event" 3390 (ARCH (if enc = Encoding_ARM then 3391 kernel_support 3392 else 3393 {a | version_number a >= 7})) {} 3394 ((increment_pc ii enc ||| 3395 event_registered ii >>= 3396 (\registered. 3397 if registered then 3398 clear_event_register ii 3399 else 3400 wait_for_event ii)) >>= unit2))`; 3401 3402(* ........................................................................ 3403 T,A: SEV<c> 3404 T2: SEV<c>.W 3405 ```````````````````````````````````````````````````````````````````````` *) 3406val send_event_instr_def = iDefine` 3407 send_event_instr ii enc = 3408 read_arch ii >>= 3409 (\arch. 3410 if arch = ARMv6T2 then 3411 no_operation_instr ii enc 3412 else 3413 instruction ii "send_event" 3414 (ARCH (if enc = Encoding_ARM then 3415 kernel_support 3416 else 3417 {a | version_number a >= 7})) {} 3418 ((increment_pc ii enc ||| send_event ii) >>= unit2))`; 3419 3420(* ........................................................................ 3421 T,A: WFI<c> 3422 T2: WFI<c>.W 3423 ```````````````````````````````````````````````````````````````````````` *) 3424val wait_for_interrupt_instr_def = iDefine` 3425 wait_for_interrupt_instr ii enc = 3426 read_arch ii >>= 3427 (\arch. 3428 if arch = ARMv6T2 then 3429 no_operation_instr ii enc 3430 else 3431 instruction ii "wait_for_interrupt" 3432 (ARCH (if enc = Encoding_ARM then 3433 kernel_support 3434 else 3435 {a | version_number a >= 7})) {} 3436 ((increment_pc ii enc ||| wait_for_interrupt ii) >>= unit2))`; 3437 3438(* ........................................................................ 3439 T2,A: DBG<c> #<option> 3440 ```````````````````````````````````````````````````````````````````````` *) 3441val debug_instr_def = iDefine` 3442 debug_instr ii enc option = 3443 read_arch ii >>= 3444 (\arch. 3445 if (arch = ARMv6T2) \/ (enc = Encoding_ARM) /\ (arch = ARMv6K) then 3446 no_operation_instr ii enc 3447 else 3448 instruction ii "debug" (ARCH {a | version_number a >= 7}) {} 3449 ((increment_pc ii enc ||| hint_debug ii option) >>= unit2))`; 3450 3451(* ------------------------------------------------------------------------ *) 3452 3453val condition_passed_def = Define` 3454 condition_passed ii (cond:word4) = 3455 read_flags ii >>= 3456 (\(n,z,c,v). 3457 let result = 3458 (case (3 >< 1) cond : word3 3459 of 0b000w => z (* EQ or NE *) 3460 | 0b001w => c (* CS or CC *) 3461 | 0b010w => n (* MI or PL *) 3462 | 0b011w => v (* VS or VC *) 3463 | 0b100w => c /\ ~z (* HI or LS *) 3464 | 0b101w => n = v (* GE or LT *) 3465 | 0b110w => (n = v) /\ ~z (* GT or LE *) 3466 | 0b111w => T) (* AL *) 3467 in 3468 if cond ' 0 /\ (cond <> 15w) then 3469 constT (~result) 3470 else 3471 constT result)`; 3472 3473val branch_instruction_def = Define` 3474 branch_instruction ii (enc,inst) = 3475 case inst 3476 of Branch_Target imm24 => 3477 branch_target_instr ii enc inst 3478 | Branch_Exchange rm => 3479 branch_exchange_instr ii inst 3480 | Branch_Link_Exchange_Immediate H toARM imm24 => 3481 branch_link_exchange_imm_instr ii enc inst 3482 | Branch_Link_Exchange_Register rm => 3483 branch_link_exchange_reg_instr ii inst 3484 | Compare_Branch nonzero imm6 rn => 3485 compare_branch_instr ii inst 3486 | Table_Branch_Byte rn h rm => 3487 table_branch_byte_instr ii inst 3488 | Check_Array rn rm => 3489 check_array_instr ii inst 3490 | Handler_Branch_Link l handler => 3491 handler_branch_link_instr ii inst 3492 | Handler_Branch_Link_Parameter imm5 handler => 3493 handler_branch_link_parameter_instr ii inst 3494 | Handler_Branch_Parameter imm3 handler => 3495 handler_branch_parameter_instr ii inst`; 3496 3497val data_processing_instruction_def = Define` 3498 data_processing_instruction ii (enc,inst) = 3499 case inst 3500 of Data_Processing opc s rn rd mode1 => 3501 data_processing_instr ii enc inst 3502 | Move_Halfword high rd imm16 => 3503 move_halfword_instr ii enc inst 3504 | Add_Sub add n d imm12 => 3505 add_sub_instr ii enc inst 3506 | Multiply a s rd ra rm rn => 3507 multiply_instr ii enc inst 3508 | Multiply_Subtract rd ra rm rn => 3509 multiply_subtract_instr ii enc inst 3510 | Signed_Halfword_Multiply 0w m n rd ra rm rn => 3511 signed_16_multiply_32_accumulate_instr ii enc inst 3512 | Signed_Halfword_Multiply 1w m F rd ra rm rn => 3513 signed_16x32_multiply_32_accumulate_instr ii enc inst 3514 | Signed_Halfword_Multiply 1w m T rd ra rm rn => 3515 signed_16x32_multiply_32_result_instr ii enc inst 3516 | Signed_Halfword_Multiply 2w m n rd ra rm rn => 3517 signed_16_multiply_64_accumulate_instr ii enc inst 3518 | Signed_Halfword_Multiply opc m n rd ra rm rn => 3519 signed_16_multiply_32_result_instr ii enc inst 3520 | Signed_Multiply_Dual rd ra rm sub m_swap rn => 3521 signed_multiply_dual_instr ii enc inst 3522 | Signed_Multiply_Long_Dual rdhi rdlo rm sub m_swap rn => 3523 signed_multiply_long_dual_instr ii enc inst 3524 | Signed_Most_Significant_Multiply rd ra rm round rn => 3525 signed_most_significant_multiply_instr ii enc inst 3526 | Signed_Most_Significant_Multiply_Subtract rd ra rm round rn => 3527 signed_most_significant_multiply_subtract_instr ii enc inst 3528 | Multiply_Long u a s rdhi rdlo rm rn => 3529 multiply_long_instr ii enc inst 3530 | Multiply_Accumulate_Accumulate rdhi rdlo rm rn => 3531 multiply_accumulate_accumulate_instr ii enc inst 3532 | Saturate u sat_imm5 rd imm5 sh rn => 3533 saturate_instr ii enc inst 3534 | Saturate_16 u sat_imm4 rd rn => 3535 saturate_16_instr ii enc inst 3536 | Saturating_Add_Subtract opc rn rd rm => 3537 saturating_add_subtract_instr ii enc inst 3538 | Pack_Halfword rn rd imm5 tbform rm => 3539 pack_halfword_instr ii enc inst 3540 | Extend_Byte u rn rd rotate rm => 3541 extend_byte_instr ii enc inst 3542 | Extend_Byte_16 u rn rd rotate rm => 3543 extend_byte_16_instr ii enc inst 3544 | Extend_Halfword u rn rd rotate rm => 3545 extend_halfword_instr ii enc inst 3546 | Bit_Field_Clear_Insert msb rd lsb rn => 3547 bit_field_clear_insert_instr ii enc inst 3548 | Count_Leading_Zeroes rd rm => 3549 count_leading_zeroes_instr ii enc inst 3550 | Reverse_Bits rd rm => 3551 reverse_bits_instr ii enc inst 3552 | Byte_Reverse_Word rd rm => 3553 byte_reverse_word_instr ii enc inst 3554 | Byte_Reverse_Packed_Halfword rd rm => 3555 byte_reverse_packed_halfword_instr ii enc inst 3556 | Byte_Reverse_Signed_Halfword rd rm => 3557 byte_reverse_signed_halfword_instr ii enc inst 3558 | Bit_Field_Extract u widthm1 rd lsb rn => 3559 bit_field_extract_instr ii enc inst 3560 | Select_Bytes rn rd rm => 3561 select_bytes_instr ii enc inst 3562 | Unsigned_Sum_Absolute_Differences rd ra rm rn => 3563 unsigned_sum_absolute_differences_instr ii enc inst 3564 | Parallel_Add_Subtract u op rn rd rm => 3565 parallel_add_subtract_instr ii enc inst 3566 | Divide u rn rd rm => 3567 divide_instr ii inst`; 3568 3569val status_access_instruction_def = Define` 3570 status_access_instruction ii (enc,inst) = 3571 case inst 3572 of Status_to_Register r rd => 3573 status_to_register_instr ii enc inst 3574 | Immediate_to_Status r mask imm12 => 3575 immediate_to_status_instr ii inst 3576 | Register_to_Status r mask rn => 3577 register_to_status_instr ii enc inst 3578 | Change_Processor_State imod affectA affectI affectF mode => 3579 change_processor_state_instr ii enc inst 3580 | Set_Endianness set_bigend => 3581 set_endianness_instr ii enc inst`; 3582 3583val load_store_instruction_def = Define` 3584 load_store_instruction ii (enc,inst) = 3585 case inst 3586 of Load p u b w unpriv rn rt mode2 => 3587 load_instr ii enc inst 3588 | Store p u b w unpriv rn rt mode2 => 3589 store_instr ii enc inst 3590 | Load_Halfword p u w s h unpriv rn rt mode3 => 3591 load_halfword_instr ii enc inst 3592 | Store_Halfword p u w unpriv rn rt mode3 => 3593 store_halfword_instr ii enc inst 3594 | Load_Dual p u w rn rt rt2 mode3 => 3595 load_dual_instr ii enc inst 3596 | Store_Dual p u w rn rt rt2 mode3 => 3597 store_dual_instr ii enc inst 3598 | Load_Multiple p u s w rn registers => 3599 load_multiple_instr ii enc inst 3600 | Store_Multiple p u s w rn registers => 3601 store_multiple_instr ii enc inst 3602 | Load_Exclusive rn rt imm8 => 3603 load_exclusive_instr ii enc inst 3604 | Store_Exclusive rn rd rt imm8 => 3605 store_exclusive_instr ii enc inst 3606 | Load_Exclusive_Doubleword rn rt rt2 => 3607 load_exclusive_doubleword_instr ii enc inst 3608 | Store_Exclusive_Doubleword rn rd rt rt2 => 3609 store_exclusive_doubleword_instr ii enc inst 3610 | Load_Exclusive_Halfword rn rt => 3611 load_exclusive_halfword_instr ii enc inst 3612 | Store_Exclusive_Halfword rn rd rt => 3613 store_exclusive_halfword_instr ii enc inst 3614 | Load_Exclusive_Byte rn rt => 3615 load_exclusive_byte_instr ii enc inst 3616 | Store_Exclusive_Byte rn rd rt => 3617 store_exclusive_byte_instr ii enc inst 3618 | Store_Return_State p u w mode => 3619 store_return_state_instr ii enc inst 3620 | Return_From_Exception p u w rn => 3621 return_from_exception_instr ii enc inst`; 3622 3623val miscellaneous_instruction_def = Define` 3624 miscellaneous_instruction ii (enc,inst) = 3625 case inst 3626 of Hint Hint_nop => 3627 no_operation_instr ii enc 3628 | Hint Hint_yield => 3629 yield_instr ii enc 3630 | Hint Hint_wait_for_event => 3631 wait_for_event_instr ii enc 3632 | Hint Hint_send_event => 3633 send_event_instr ii enc 3634 | Hint Hint_wait_for_interrupt => 3635 wait_for_interrupt_instr ii enc 3636 | Hint (Hint_debug option) => 3637 debug_instr ii enc option 3638 | Breakpoint imm16 => 3639 breakpoint_instr ii 3640 | Data_Memory_Barrier option => 3641 data_memory_barrier_instr ii enc inst 3642 | Data_Synchronization_Barrier option => 3643 data_synchronization_barrier_instr ii enc inst 3644 | Instruction_Synchronization_Barrier option => 3645 instruction_synchronization_barrier_instr ii enc inst 3646 | Swap b rn rt rt2 => 3647 swap_instr ii inst 3648 | Preload_Data u r rn mode2 => 3649 preload_data_instr ii enc inst 3650 | Preload_Instruction u rn mode2 => 3651 preload_instruction_instr ii enc inst 3652 | Supervisor_Call imm24 => 3653 take_svc_exception ii 3654 | Secure_Monitor_Call imm4 => 3655 secure_monitor_call_instr ii 3656 | Enterx_Leavex is_enterx => 3657 enterx_leavex_instr ii is_enterx 3658 | Clear_Exclusive => 3659 clear_exclusive_instr ii enc 3660 | If_Then firstcond mask => 3661 if_then_instr ii inst`; 3662 3663val coprocessor_instruction_def = Define` 3664 coprocessor_instruction ii (enc,cond,inst) = 3665 case inst 3666 of Coprocessor_Load p u d w rn crd coproc mode5 => 3667 coprocessor_load_instr ii enc cond inst 3668 | Coprocessor_Store p u d w rn crd coproc mode5 => 3669 coprocessor_store_instr ii enc cond inst 3670 | Coprocessor_Data_Processing opc1 crn crd coproc opc2 crm => 3671 coprocessor_data_processing_instr ii enc cond inst 3672 | Coprocessor_Transfer opc1_1 F crn rt coproc opc2 crm => 3673 arm_register_to_coprocessor_instr ii enc cond inst 3674 | Coprocessor_Transfer opc1_1 T crn rt coproc opc2 crm => 3675 coprocessor_register_to_arm_instr ii enc cond inst 3676 | Coprocessor_Transfer_Two F rt2 rt coproc opc1 crm => 3677 arm_register_to_coprocessor_two_instr ii enc cond inst 3678 | Coprocessor_Transfer_Two T rt2 rt coproc opc1 crm => 3679 coprocessor_register_to_arm_two_instr ii enc cond inst`; 3680 3681val arm_instr_def = Define` 3682 arm_instr ii (enc,cond,inst) = 3683 (condition_passed ii cond >>= 3684 (\pass. 3685 if pass then 3686 case inst 3687 of Branch b => 3688 branch_instruction ii (enc,b) 3689 | DataProcessing d => 3690 data_processing_instruction ii (enc,d) 3691 | StatusAccess s => 3692 status_access_instruction ii (enc,s) 3693 | LoadStore l => 3694 load_store_instruction ii (enc,l) 3695 | Miscellaneous m => 3696 miscellaneous_instruction ii (enc,m) 3697 | Coprocessor c => 3698 coprocessor_instruction ii (enc,cond,c) 3699 | Undefined => 3700 take_undef_instr_exception ii 3701 | _ => 3702 errorT "decode: unpredictable" 3703 else 3704 increment_pc ii enc)) >>= 3705 (\u:unit. 3706 condT (case inst 3707 of Miscellaneous (If_Then _ _) => F 3708 | _ => T) 3709 (IT_advance ii))`; 3710 3711(* ======================================================================== *) 3712 3713infix \\ << 3714 3715val op \\ = op THEN; 3716val op << = op THENL; 3717 3718val _ = wordsLib.guess_lengths(); 3719 3720val extract_modify = 3721 (GEN_ALL o SIMP_CONV (arith_ss++fcpLib.FCP_ss++boolSimps.CONJ_ss) 3722 [word_modify_def, word_extract_def, word_bits_def, w2w]) 3723 ``(h >< l) (word_modify P w) = value``; 3724 3725val CONCAT62_EQ = Q.prove( 3726 `(!a b c d. 3727 ((a:word6) @@ (b:word2) = (c:word6) @@ (d:word2)) = (a = c) /\ (b = d)) /\ 3728 (!a b c. 3729 ((a:word6) @@ (b:word2) = c) = (a = (7 >< 2) c) /\ (b = (1 >< 0) c))`, 3730 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [] 3731 \\ DECIDE_TAC); 3732 3733val LESS_THM = 3734 CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV prim_recTheory.LESS_THM; 3735 3736val cpsr_write_by_instr_thm = Q.prove( 3737 `!cpsr value:word32 bytemask:word4 affect_execstate priviledged secure 3738 aw fw nmfi. 3739 decode_psr (word_modify (\i b. 3740 if 27 <= i /\ i <= 31 /\ bytemask ' 3 \/ 3741 24 <= i /\ i <= 26 /\ bytemask ' 3 /\ affect_execstate \/ 3742 16 <= i /\ i <= 19 /\ bytemask ' 2 \/ 3743 10 <= i /\ i <= 15 /\ bytemask ' 1 /\ affect_execstate \/ 3744 (i = 9) /\ bytemask ' 1 \/ 3745 (i = 8) /\ bytemask ' 1 /\ 3746 priviledged /\ (secure \/ aw) \/ 3747 (i = 7) /\ bytemask ' 0 /\ priviledged \/ 3748 (i = 6) /\ bytemask ' 0 /\ 3749 priviledged /\ (secure \/ fw) /\ 3750 (~nmfi \/ ~(value ' 6)) \/ 3751 (i = 5) /\ bytemask ' 0 /\ affect_execstate \/ 3752 (i < 5) /\ bytemask ' 0 /\ priviledged 3753 then value ' i else b) (encode_psr cpsr)) = 3754 cpsr with 3755 <| N := if bytemask ' 3 then value ' 31 else cpsr.N; 3756 Z := if bytemask ' 3 then value ' 30 else cpsr.Z; 3757 C := if bytemask ' 3 then value ' 29 else cpsr.C; 3758 V := if bytemask ' 3 then value ' 28 else cpsr.V; 3759 Q := if bytemask ' 3 then value ' 27 else cpsr.Q; 3760 IT := if affect_execstate then 3761 if bytemask ' 3 then 3762 if bytemask ' 1 then 3763 (15 >< 10) value @@ (26 >< 25) value 3764 else 3765 (7 >< 2) cpsr.IT @@ (26 >< 25) value 3766 else 3767 if bytemask ' 1 then 3768 (15 >< 10) value @@ (1 >< 0) cpsr.IT 3769 else 3770 cpsr.IT 3771 else 3772 cpsr.IT; 3773 J := if bytemask ' 3 /\ affect_execstate then value ' 24 else cpsr.J; 3774 GE := if bytemask ' 2 then (19 >< 16) value else cpsr.GE; 3775 E := if bytemask ' 1 then value ' 9 else cpsr.E; 3776 A := if bytemask ' 1 /\ priviledged /\ (secure \/ aw) 3777 then value ' 8 3778 else cpsr.A; 3779 I := if bytemask ' 0 /\ priviledged then value ' 7 else cpsr.I; 3780 F := if bytemask ' 0 /\ priviledged /\ (secure \/ fw) /\ 3781 (~nmfi \/ ~(value ' 6)) 3782 then value ' 6 3783 else cpsr.F; 3784 T := if bytemask ' 0 /\ affect_execstate then value ' 5 else cpsr.T; 3785 M := if bytemask ' 0 /\ priviledged then (4 >< 0) value else cpsr.M 3786 |>`, 3787 STRIP_TAC 3788 \\ SIMP_TAC (srw_ss()++ARITH_ss) [ARMpsr_component_equality, 3789 WORD_MODIFY_BIT, decode_psr_def, encode_psr_bit, encode_psr_bits, 3790 extract_modify] 3791 \\ REPEAT STRIP_TAC 3792 << [ 3793 SRW_TAC [ARITH_ss] [CONCAT62_EQ, extract_modify] 3794 \\ ASM_SIMP_TAC (arith_ss++wordsLib.WORD_BIT_EQ_ss) [] 3795 \\ FULL_SIMP_TAC std_ss [LESS_THM, encode_psr_bit], 3796 FULL_SIMP_TAC std_ss [LESS_THM, encode_psr_bit], 3797 SRW_TAC [fcpLib.FCP_ss,ARITH_ss] [word_extract_def, w2w, word_bits_def] 3798 \\ FULL_SIMP_TAC std_ss [LESS_THM, encode_psr_bit], 3799 SRW_TAC [fcpLib.FCP_ss,ARITH_ss] [word_extract_def, w2w, word_bits_def] 3800 \\ FULL_SIMP_TAC std_ss [LESS_THM, encode_psr_bit]]); 3801 3802val spsr_write_by_instr_thm = Q.prove( 3803 `!spsr value:word32 bytemask:word4. 3804 decode_psr (word_modify (\i b. 3805 if 24 <= i /\ i <= 31 /\ bytemask ' 3 \/ 3806 16 <= i /\ i <= 19 /\ bytemask ' 2 \/ 3807 8 <= i /\ i <= 15 /\ bytemask ' 1 \/ 3808 i <= 7 /\ bytemask ' 0 3809 then value ' i else b) (encode_psr spsr)) = 3810 spsr with 3811 <| N := if bytemask ' 3 then value ' 31 else spsr.N; 3812 Z := if bytemask ' 3 then value ' 30 else spsr.Z; 3813 C := if bytemask ' 3 then value ' 29 else spsr.C; 3814 V := if bytemask ' 3 then value ' 28 else spsr.V; 3815 Q := if bytemask ' 3 then value ' 27 else spsr.Q; 3816 IT := if bytemask ' 3 then 3817 if bytemask ' 1 then 3818 (15 >< 10) value @@ (26 >< 25) value 3819 else 3820 (7 >< 2) spsr.IT @@ (26 >< 25) value 3821 else 3822 if bytemask ' 1 then 3823 (15 >< 10) value @@ (1 >< 0) spsr.IT 3824 else 3825 spsr.IT; 3826 J := if bytemask ' 3 then value ' 24 else spsr.J; 3827 GE := if bytemask ' 2 then (19 >< 16) value else spsr.GE; 3828 E := if bytemask ' 1 then value ' 9 else spsr.E; 3829 A := if bytemask ' 1 then value ' 8 else spsr.A; 3830 I := if bytemask ' 0 then value ' 7 else spsr.I; 3831 F := if bytemask ' 0 then value ' 6 else spsr.F; 3832 T := if bytemask ' 0 then value ' 5 else spsr.T; 3833 M := if bytemask ' 0 then (4 >< 0) value else spsr.M 3834 |>`, 3835 STRIP_TAC 3836 \\ SIMP_TAC (srw_ss()++ARITH_ss) [ARMpsr_component_equality, 3837 WORD_MODIFY_BIT, decode_psr_def, encode_psr_bit, encode_psr_bits, 3838 extract_modify] 3839 \\ REPEAT STRIP_TAC 3840 << [ 3841 SRW_TAC [ARITH_ss] [CONCAT62_EQ, extract_modify] 3842 \\ ASM_SIMP_TAC (arith_ss++wordsLib.WORD_BIT_EQ_ss) [] 3843 \\ FULL_SIMP_TAC std_ss [LESS_THM, encode_psr_bit], 3844 FULL_SIMP_TAC std_ss [LESS_THM, encode_psr_bit], 3845 SRW_TAC [fcpLib.FCP_ss,ARITH_ss] [word_extract_def, w2w, word_bits_def] 3846 \\ FULL_SIMP_TAC std_ss [LESS_THM, encode_psr_bit], 3847 SRW_TAC [fcpLib.FCP_ss,ARITH_ss] [word_extract_def, w2w, word_bits_def] 3848 \\ FULL_SIMP_TAC std_ss [LESS_THM, encode_psr_bit]]); 3849 3850val change_processor_state_thm = Q.prove( 3851 `!cpsr affectA affectI affectF enable disable mode. 3852 word_modify (\i b. 3853 if (i = 8) /\ affectA \/ 3854 (i = 7) /\ affectI \/ 3855 (i = 6) /\ affectF 3856 then 3857 ~enable /\ (disable \/ b) 3858 else if i < 5 /\ IS_SOME mode then 3859 (THE mode) ' i 3860 else 3861 b) (encode_psr cpsr) = 3862 encode_psr (cpsr with 3863 <| A := if affectA then ~enable /\ (disable \/ cpsr.A) else cpsr.A; 3864 I := if affectI then ~enable /\ (disable \/ cpsr.I) else cpsr.I; 3865 F := if affectF then ~enable /\ (disable \/ cpsr.F) else cpsr.F; 3866 M := if IS_SOME mode then THE mode else cpsr.M 3867 |>)`, 3868 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [encode_psr_bit]); 3869 3870val cpsr_write_by_instr = 3871 SIMP_RULE (std_ss++boolSimps.LET_ss) [cpsr_write_by_instr_thm] 3872 cpsr_write_by_instr_def; 3873 3874val spsr_write_by_instr = 3875 SIMP_RULE (std_ss++boolSimps.LET_ss) [spsr_write_by_instr_thm] 3876 spsr_write_by_instr_def; 3877 3878(* ------------------------------------------------------------------------ *) 3879 3880val eval_ss = 3881 std_ss++boolSimps.CONJ_ss++pred_setSimps.PRED_SET_ss++listSimps.LIST_ss; 3882 3883val instruction_rule = SIMP_RULE eval_ss 3884 [(GEN_ALL o SIMP_RULE std_ss [] o Q.ISPEC `\x. a NOTIN x`) COND_RAND, 3885 DECIDE ``~(a >= b) = a < b:num``, condT_def, 3886 arm_coretypesTheory.NOT_IN_EMPTY_SPECIFICATION, 3887 instruction_def, run_instruction_def, null_check_instruction_def, 3888 dsp_support_def, kernel_support_def, change_processor_state_thm, 3889 arm_coretypesTheory.thumb2_support_def, 3890 arm_coretypesTheory.security_support_def, 3891 arm_coretypesTheory.thumbee_support_def]; 3892 3893val instructions = 3894 [("cpsr_write_by_instr", cpsr_write_by_instr), 3895 ("spsr_write_by_instr", spsr_write_by_instr)] @ 3896 map (I ## instruction_rule) (!instructions); 3897 3898val _ = map save_thm instructions; 3899val _ = computeLib.add_persistent_funs (map fst instructions); 3900 3901val instructions = map fst (List.drop (instructions,2)); 3902 3903val instructions_list = 3904 "val instruction_list =\n [" ^ 3905 foldl (fn (t,s) => quote t ^ ",\n " ^ s) 3906 (quote (hd instructions) ^ "]\n") (tl instructions); 3907 3908val _ = adjoin_to_theory 3909 {sig_ps = SOME (fn _ => 3910 PP.add_string "val instruction_list : string list"), 3911 struct_ps = SOME (fn _ => PP.add_string instructions_list)}; 3912 3913(* ------------------------------------------------------------------------ *) 3914 3915val _ = export_theory (); 3916