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