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