1(* ------------------------------------------------------------------------ *) 2(* ARM Machine Code Semantics *) 3(* ========================== *) 4(* Decode from machine code to the AST data type *) 5(* ------------------------------------------------------------------------ *) 6 7(* interactive use: 8 app load ["arm_astTheory", "wordsLib"]; 9*) 10 11open HolKernel boolLib bossLib Parse; 12 13open arithmeticTheory bitTheory; 14open arm_astTheory; 15 16val _ = new_theory "arm_decoder"; 17 18(* ------------------------------------------------------------------------ *) 19 20val _ = numLib.prefer_num(); 21val _ = wordsLib.prefer_word(); 22 23(* ------------------------------------------------------------------------ *) 24 25val _ = type_abbrev ("word1", ``:1 word``); 26val _ = type_abbrev ("word10", ``:10 word``); 27val _ = type_abbrev ("word11", ``:11 word``); 28 29val _ = temp_overload_on("DP", 30 ``\opc setflags rn rd mode1. 31 DataProcessing (Data_Processing opc setflags rn rd mode1)``); 32val _ = temp_overload_on("IMM",``Mode1_immediate``); 33val _ = temp_overload_on("REG",``Mode1_register``); 34val _ = temp_overload_on("SHIFTED",``Mode1_register_shifted_register``); 35 36val hint_decode_def = Define` 37 hint_decode (w:word8) = 38 case w 39 of 0b000w => Hint_nop 40 | 0b001w => Hint_yield 41 | 0b010w => Hint_wait_for_event 42 | 0b011w => Hint_wait_for_interrupt 43 | 0b100w => Hint_send_event 44 | _ => if (7 -- 4) w = 0b1111w then 45 Hint_debug (w2w w) 46 else 47 Hint_nop`; 48 49val parallel_add_sub_decode_defs = TotalDefn.multiDefine` 50 (parallel_add_sub_op1 (0b01w :word2) = Parallel_normal) /\ 51 (parallel_add_sub_op1 (0b10w :word2) = Parallel_saturating) /\ 52 (parallel_add_sub_op1 (0b11w :word2) = Parallel_halving) /\ 53 (parallel_add_sub_op2 (0b000w:word3) = Parallel_add_16) /\ 54 (parallel_add_sub_op2 (0b001w:word3) = Parallel_add_sub_exchange) /\ 55 (parallel_add_sub_op2 (0b010w:word3) = Parallel_sub_add_exchange) /\ 56 (parallel_add_sub_op2 (0b011w:word3) = Parallel_sub_16) /\ 57 (parallel_add_sub_op2 (0b100w:word3) = Parallel_add_8) /\ 58 (parallel_add_sub_op2 (0b111w:word3) = Parallel_sub_8) /\ 59 (parallel_add_sub_thumb_op2 (0b001w:word3) = Parallel_add_16) /\ 60 (parallel_add_sub_thumb_op2 (0b010w:word3) = Parallel_add_sub_exchange) /\ 61 (parallel_add_sub_thumb_op2 (0b110w:word3) = Parallel_sub_add_exchange) /\ 62 (parallel_add_sub_thumb_op2 (0b101w:word3) = Parallel_sub_16) /\ 63 (parallel_add_sub_thumb_op2 (0b000w:word3) = Parallel_add_8) /\ 64 (parallel_add_sub_thumb_op2 (0b100w:word3) = Parallel_sub_8) /\ 65 (parallel_add_sub_decode (a,b) = 66 (parallel_add_sub_op1 a, parallel_add_sub_op2 b)) /\ 67 (parallel_add_sub_thumb_decode (a,b) = 68 (parallel_add_sub_op1 (a + 0b01w), parallel_add_sub_thumb_op2 b))`; 69 70val InITBlock_def = Define` 71 InITBlock (IT:word8) = (3 -- 0) IT <> 0w`; 72 73val LastInITBlock_def = Define` 74 LastInITBlock (IT:word8) = ((3 -- 0) IT = 0b1000w)`; 75 76(* ------------------------------------------------------------------------ *) 77 78val arm_decode_def = zDefine` 79 arm_decode v4 (ireg : word32) = 80 let b n = ireg ' n 81 and i2 n = ( n + 1 >< n ) ireg : word2 82 and i3 n = ( n + 2 >< n ) ireg : word3 83 and i4 n = ( n + 3 >< n ) ireg : word4 84 and i5 n = ( n + 4 >< n ) ireg : word5 85 and i8 n = ( n + 7 >< n ) ireg : word8 86 and i12 n = ( n + 11 >< n ) ireg : word12 87 and i16 n = ( n + 15 >< n ) ireg : word16 88 and i24 n = ( 23 >< 0 ) ireg : word24 in 89 let cond = i4 28 and r = i4 90 in 91 (cond, 92 if cond = 15w then 93 if v4 then 94 Unpredictable 95 else 96 case (b 27,b 26,b 25,b 24,b 23,b 22,b 21,b 20,b 7,b 6,b 5,b 4) 97 of (F, F , F , T , F , F , F , F,b7,b6, F,b4) => 98 (if b 16 then 99 if ~b7 /\ ~b6 /\ ~b4 then 100 StatusAccess (Set_Endianness (b 9)) 101 else 102 Undefined 103 else let m = b 17 and mode = i5 0 in 104 if ~m /\ (mode <> 0w) then 105 Unpredictable 106 else 107 StatusAccess 108 (Change_Processor_State (i2 18) (b 8) (b 7) 109 (b 6) (if m then SOME mode else NONE))) 110 | (F, T , F , F ,b23, T , F , T,_7,_6,_5,_4) => 111 Miscellaneous 112 (Preload_Instruction b23 (r 16) (Mode2_immediate (i12 0))) 113 | (F, T , T , F ,b23, T , F , T,_7,_6,_5,_4) => 114 Miscellaneous 115 (Preload_Instruction b23 (r 16) 116 (Mode2_register (i5 7) (i2 5) (r 0))) 117 | (F, T , F , T , F , T , T , T, F, F, F, T) => 118 Miscellaneous Clear_Exclusive 119 | (F, T , F , T , F , T , T , T, F, T, F, F) => 120 Miscellaneous (Data_Synchronization_Barrier (i4 0)) 121 | (F, T , F , T , F , T , T , T, F, T, F, T) => 122 Miscellaneous (Data_Memory_Barrier (i4 0)) 123 | (F, T , F , T , F , T , T , T, F, T, T, F) => 124 Miscellaneous (Instruction_Synchronization_Barrier (i4 0)) 125 | (F, T , F , T ,b23,b22, F , T,_7,_6,_5,_4) => 126 if ~b22 /\ (r 12 = 15w) then 127 Undefined 128 else 129 Miscellaneous 130 (Preload_Data b23 (~b22) (r 16) (Mode2_immediate (i12 0))) 131 | (F, T , T , T ,b23,b22, F , T,_7,_6,_5,_4) => 132 Miscellaneous 133 (Preload_Data b23 (~b22) (r 16) 134 (Mode2_register (i5 7) (i2 5) (r 0))) 135 | (F,_26,_25,_24,_23,_22,_21,_20,_7,_6,_5,_4) => Undefined 136 | (T, F , F ,b24,b23, T ,b21, F ,_7,_6,_5,_4) => 137 LoadStore (Store_Return_State b24 b23 b21 (i5 0)) 138 | (T, F , F ,b24,b23, F ,b21, T ,_7,_6,_5,_4) => 139 LoadStore (Return_From_Exception b24 b23 b21 (r 16)) 140 | (T, F , F ,_24,_23,_22,_21,_20,_7,_6,_5,_4) => Undefined 141 | (T, F , T ,b24,_23,_22,_21,_20,_7,_6,_5,_4) => 142 Branch (Branch_Link_Exchange_Immediate b24 F (i24 0)) 143 | (T,T,F, F , F , T , F ,b20,_7,_6,_5,_4) => 144 Coprocessor 145 (Coprocessor_Transfer_Two b20 (r 16) (r 12) (i4 8) (i4 4) (r 0)) 146 | (T, T , F ,b24,_23,_22,_21, F ,_7,_6,_5,_4) => 147 Coprocessor 148 (Coprocessor_Store b24 (b 23) (b 22) (b 21) (r 16) (r 12) 149 (i4 8) (i8 0)) 150 | (T, T , F ,b24,_23,_22,_21, T ,_7,_6,_5,_4) => 151 Coprocessor 152 (Coprocessor_Load b24 (b 23) (b 22) (b 21) (r 16) (r 12) (i4 8) 153 (i8 0)) 154 | (T, T , T , F ,_23,_22,_21,_20,_7,_6,_5, F) => 155 Coprocessor 156 (Coprocessor_Data_Processing (i4 20) (r 16) (r 12) (i4 8) 157 (i3 5) (r 0)) 158 | (T, T , T , F ,_23,_22,_21,_20,_7,_6,_5, T) => 159 Coprocessor 160 (Coprocessor_Transfer (i3 21) (b 20) (r 16) (r 12) (i4 8) 161 (i3 5) (r 0)) 162 | (T,T,T,T,_23,_22,_21,_20,_7,_6,_5,_4) => Undefined 163 else 164 case (b 27,b 26,b 25,b 24,b 23,b 22,b 21,b 20,b 7,b 6,b 5,b 4) 165 of (F,F,F, T , F ,b22, F , F , F, F, F, F) => 166 StatusAccess (Status_to_Register b22 (r 12)) 167 | (F,F,F, T , F ,b22, T , F , F, F, F, F) => 168 StatusAccess (Register_to_Status b22 (i4 16) (r 0)) 169 | (F,F,F, T , F , F , T , F , F, F, F, T) => 170 Branch (Branch_Exchange (r 0)) 171 | (F,F,F, T , F , T , T , F , F, F, F, T) => 172 DataProcessing (Count_Leading_Zeroes (r 12) (r 0)) 173 | (F,F,F, T , F , F , T , F , F, F, T, T) => 174 Branch (Branch_Link_Exchange_Register (r 0)) 175 | (F,F,F, T , F ,_22,_21, F , F, T, F, T) => 176 DataProcessing (Saturating_Add_Subtract (i2 21) (r 16) (r 12) (r 0)) 177 | (F,F,F, T , F , F , T , F , F, T, T, T) => 178 if cond = 14w then 179 Miscellaneous (Breakpoint (i12 8 @@ i4 0)) 180 else 181 Unpredictable 182 | (F,F,F, T , F , T , T , F , F, T, T, T) => 183 Miscellaneous (Secure_Monitor_Call (i4 0)) 184 | (F,F,F, T , F ,_22,_21, F , T,b6,b5, F) => 185 DataProcessing 186 (Signed_Halfword_Multiply (i2 21) b6 b5 (r 16) (r 12) (r 8) (r 0)) 187 | (F,F,F,_24,_23,_22,_21,b20,_7,_6,_5, F) => 188 DP (i4 21) b20 (r 16) (r 12) (REG (i5 7) (i2 5) (r 0)) 189 | (F,F,F,_24,_23,_22,_21,b20, F,_6,_5, T) => 190 DP (i4 21) b20 (r 16) (r 12) (SHIFTED (r 8) (i2 5) (r 0)) 191 | (F,F,F, F , F , F ,b21,b20, T, F, F, T) => 192 DataProcessing (Multiply b21 b20 (r 16) (r 12) (r 8) (r 0)) 193 | (F,F,F, F , F , T , F , F , T, F, F, T) => 194 DataProcessing 195 (Multiply_Accumulate_Accumulate (r 16) (r 12) (r 8) (r 0)) 196 | (F,F,F, F , F , T , T , F , T, F, F, T) => 197 DataProcessing (Multiply_Subtract (r 16) (r 12) (r 8) (r 0)) 198 | (F,F,F, F , T ,b22,b21,b20, T, F, F, T) => 199 DataProcessing (Multiply_Long b22 b21 b20 (r 16) (r 12) (r 8) (r 0)) 200 | (F,F,F, T , F ,b22, F , F , T, F, F, T) => 201 Miscellaneous (Swap b22 (r 16) (r 12) (r 0)) 202 | (F,F,F, T , T , F , F , F , T, F, F, T) => 203 LoadStore (Store_Exclusive (r 16) (r 12) (r 0) 0w) 204 | (F,F,F, T , T , F , F , T , T, F, F, T) => 205 LoadStore (Load_Exclusive (r 16) (r 12) 0w) 206 | (F,F,F, T , T , F , T , F , T, F, F, T) => 207 (let rt = r 0 in 208 LoadStore (Store_Exclusive_Doubleword (r 16) (r 12) rt (rt + 1w))) 209 | (F,F,F, T , T , F , T , T , T, F, F, T) => 210 (let rt = r 12 in 211 LoadStore (Load_Exclusive_Doubleword (r 16) rt (rt + 1w))) 212 | (F,F,F, T , T , T , F , F , T, F, F, T) => 213 LoadStore (Store_Exclusive_Byte (r 16) (r 12) (r 0)) 214 | (F,F,F, T , T , T , F , T , T, F, F, T) => 215 LoadStore (Load_Exclusive_Byte (r 16) (r 12)) 216 | (F,F,F, T , T , T , T , F , T, F, F, T) => 217 LoadStore (Store_Exclusive_Halfword (r 16) (r 12) (r 0)) 218 | (F,F,F, T , T , T , T , T , T, F, F, T) => 219 LoadStore (Load_Exclusive_Halfword (r 16) (r 12)) 220 | (F,F,F,b24,b23, F ,b21, F , T, F, T, T) => 221 LoadStore (Store_Halfword b24 b23 b21 (~b24 /\ b21) (r 16) (r 12) 222 (Mode3_register 0w (r 0))) 223 | (F,F,F,b24,b23, F ,b21, T , T, F, T, T) => 224 LoadStore (Load_Halfword b24 b23 b21 F T (~b24 /\ b21) (r 16) (r 12) 225 (Mode3_register 0w (r 0))) 226 | (F,F,F,b24,b23, T ,b21, F , T, F, T, T) => 227 LoadStore (Store_Halfword b24 b23 b21 (~b24 /\ b21) (r 16) (r 12) 228 (Mode3_immediate (i4 8 @@ i4 0))) 229 | (F,F,F,b24,b23, T ,b21, T , T, F, T, T) => 230 LoadStore (Load_Halfword b24 b23 b21 F T (~b24 /\ b21) (r 16) (r 12) 231 (Mode3_immediate (i4 8 @@ i4 0))) 232 | (F,F,F,b24,b23, F ,b21, F , T, T, F, T) => 233 (let rt = r 12 in 234 LoadStore (Load_Dual b24 b23 b21 (r 16) rt (rt + 1w) 235 (Mode3_register 0w (r 0)))) 236 | (F,F,F,b24,b23, F ,b21, F , T, T, T, T) => 237 (let rt = r 12 in 238 LoadStore (Store_Dual b24 b23 b21 (r 16) rt (rt + 1w) 239 (Mode3_register 0w (r 0)))) 240 | (F,F,F,b24,b23, F ,b21, T , T, T,b5, T) => 241 LoadStore (Load_Halfword b24 b23 b21 T b5 (~b24 /\ b21) (r 16) (r 12) 242 (Mode3_register 0w (r 0))) 243 | (F,F,F,b24,b23, T ,b21, F , T, T, F, T) => 244 (let rt = r 12 in 245 LoadStore (Load_Dual b24 b23 b21 (r 16) rt (rt + 1w) 246 (Mode3_immediate (i4 8 @@ i4 0)))) 247 | (F,F,F,b24,b23, T ,b21, F , T, T, T, T) => 248 (let rt = r 12 in 249 LoadStore (Store_Dual b24 b23 b21 (r 16) rt (rt + 1w) 250 (Mode3_immediate (i4 8 @@ i4 0)))) 251 | (F,F,F,b24,b23, T ,b21, T , T, T,b5, T) => 252 LoadStore (Load_Halfword b24 b23 b21 T b5 (~b24 /\ b21) (r 16) (r 12) 253 (Mode3_immediate (i4 8 @@ i4 0))) 254 | (F,F,T, F , F , T , F , F ,_7,_6,_5,_4) => 255 (let rn = r 16 in 256 if rn = 15w then 257 DataProcessing (Add_Sub F rn (r 12) (i12 0)) 258 else 259 DP 0b0010w F rn (r 12) (IMM (i12 0))) 260 | (F,F,T, F , T , F , F , F ,_7,_6,_5,_4) => 261 (let rn = r 16 in 262 if rn = 15w then 263 DataProcessing (Add_Sub T rn (r 12) (i12 0)) 264 else 265 DP 0b0100w F rn (r 12) (IMM (i12 0))) 266 | (F,F,T, T , F ,b22, F , F ,_7,_6,_5,_4) => 267 DataProcessing (Move_Halfword b22 (r 12) (i4 16 @@ i12 0)) 268 | (F,F,T, T , F ,b22, T , F ,_7,_6,_5,_4) => 269 if ~b22 /\ (r 16 = 0w) then 270 Miscellaneous (Hint (hint_decode (i8 0))) 271 else 272 StatusAccess (Immediate_to_Status b22 (i4 16) (i12 0)) 273 | (F,F,T, T , T , T , T ,b20,_7,_6,_5,_4) => 274 DP 0b1111w b20 0b1111w (r 12) (IMM (i12 0)) 275 | (F,F,T,_24,_23,_22,_21,b20,_7,_6,_5,_4) => 276 DP (i4 21) b20 (r 16) (r 12) (IMM (i12 0)) 277 | (F,T,F,b24,b23,b22,b21, F ,_7,_6,_5,_4) => 278 LoadStore (Store b24 b23 b22 b21 (~b24 /\ b21) (r 16) (r 12) 279 (Mode2_immediate (i12 0))) 280 | (F,T,F,b24,b23,b22,b21, T ,_7,_6,_5,_4) => 281 LoadStore (Load b24 b23 b22 b21 (~b24 /\ b21) (r 16) (r 12) 282 (Mode2_immediate (i12 0))) 283 | (F,T,T,b24,b23,b22,b21, F ,_7,_6,_5, F) => 284 LoadStore (Store b24 b23 b22 b21 (~b24 /\ b21) (r 16) (r 12) 285 (Mode2_register (i5 7) (i2 5) (r 0))) 286 | (F,T,T,b24,b23,b22,b21, T ,_7,_6,_5, F) => 287 LoadStore (Load b24 b23 b22 b21 (~b24 /\ b21) (r 16) (r 12) 288 (Mode2_register (i5 7) (i2 5) (r 0))) 289 | (F,T,T, F , F ,b22,_21,_20,_7,_6,_5, T) => 290 (let op1 = i2 20 and op2 = i3 5 in 291 if op1 <> 0w /\ (op2 <+ 5w \/ (op2 = 7w)) then 292 DataProcessing (Parallel_Add_Subtract b22 293 (parallel_add_sub_decode (op1,op2)) (r 16) (r 12) (r 0)) 294 else 295 Undefined) 296 | (F,T,T, F , T , F , F , F ,_7,b6, F, T) => 297 DataProcessing (Pack_Halfword (r 16) (r 12) (i5 7) b6 (r 0)) 298 | (F,T,T, F , T , F , F , F , T, F, T, T) => 299 DataProcessing (Select_Bytes (r 16) (r 12) (r 0)) 300 | (F,T,T, F , T ,b22, F , F , F, T, T, T) => 301 DataProcessing (Extend_Byte_16 b22 (r 16) (r 12) (i2 10) (r 0)) 302 | (F,T,T, F , T ,b22, T ,_20,_7,b6, F, T) => 303 DataProcessing (Saturate b22 (i5 16) (r 12) (i5 7) b6 (r 0)) 304 | (F,T,T, F , T ,b22, T , F , F, F, T, T) => 305 DataProcessing (Saturate_16 b22 (i4 16) (r 12) (r 0)) 306 | (F,T,T, F , T ,b22, T , F , F, T, T, T) => 307 DataProcessing (Extend_Byte b22 (r 16) (r 12) (i2 10) (r 0)) 308 | (F,T,T, F , T , F , T , T , F, F, T, T) => 309 DataProcessing (Byte_Reverse_Word (r 12) (r 0)) 310 | (F,T,T, F , T ,b22, T , T , F, T, T, T) => 311 DataProcessing (Extend_Halfword b22 (r 16) (r 12) (i2 10) (r 0)) 312 | (F,T,T, F , T , F , T , T , T, F, T, T) => 313 DataProcessing (Byte_Reverse_Packed_Halfword (r 12) (r 0)) 314 | (F,T,T, F , T , T , T , T , F, F, T, T) => 315 DataProcessing (Reverse_Bits (r 12) (r 0)) 316 | (F,T,T, F , T , T , T , T , T, F, T, T) => 317 DataProcessing (Byte_Reverse_Signed_Halfword (r 12) (r 0)) 318 | (F,T,T, T , F , F , F , F , F,b6,b5, T) => 319 DataProcessing (Signed_Multiply_Dual (r 16) (r 12) (r 8) b6 b5 (r 0)) 320 | (F,T,T, T , F , T , F , F , F,b6,b5, T) => 321 DataProcessing 322 (Signed_Multiply_Long_Dual (r 16) (r 12) (r 8) b6 b5 (r 0)) 323 | (F,T,T, T , F , T , F , T , F, F,b5, T) => 324 DataProcessing 325 (Signed_Most_Significant_Multiply (r 16) (r 12) (r 8) b5 (r 0)) 326 | (F,T,T, T , F , T , F , T , T, T,b5, T) => 327 DataProcessing (Signed_Most_Significant_Multiply_Subtract (r 16) 328 (r 12) (r 8) b5 (r 0)) 329 | (F,T,T, T , T , F , F , F , F, F, F, T) => 330 DataProcessing (Unsigned_Sum_Absolute_Differences (r 16) (r 12) 331 (r 8) (r 0)) 332 | (F,T,T, T , T ,b22, T ,b20,b7, T, F, T) => 333 DataProcessing (Bit_Field_Extract b22 (i5 16) (r 12) (i5 7) (r 0)) 334 | (F,T,T, T , T , T , F ,b20,b7, F, F, T) => 335 DataProcessing (Bit_Field_Clear_Insert (i5 16) (r 12) (i5 7) (r 0)) 336 | (F,T,T,_24,_23,_22,_21,_20,_7,_6,_5, T) => 337 Undefined 338 | (T,F,F,b24,b23,b22,b21, F ,_7,_6,_5,_4) => 339 LoadStore (Store_Multiple b24 b23 b22 b21 (r 16) (i16 0)) 340 | (T,F,F,b24,b23,b22,b21, T ,_7,_6,_5,_4) => 341 LoadStore (Load_Multiple b24 b23 b22 b21 (r 16) (i16 0)) 342 | (T,F,T, F ,_23,_22,_21,_20,_7,_6,_5,_4) => 343 Branch (Branch_Target (i24 0)) 344 | (T,F,T, T ,_23,_22,_21,_20,_7,_6,_5,_4) => 345 Branch (Branch_Link_Exchange_Immediate T T (i24 0)) 346 | (T,T,F, F , F , T , F ,b20,_7,_6,_5,_4) => 347 Coprocessor 348 (Coprocessor_Transfer_Two b20 (r 16) (r 12) (i4 8) (i4 4) (r 0)) 349 | (T,T,F,b24,b23,b22,b21, F ,_7,_6,_5,_4) => 350 Coprocessor (Coprocessor_Store b24 b23 b22 b21 (r 16) (r 12) (i4 8) 351 (i8 0)) 352 | (T,T,F,b24,b23,b22,b21, T ,_7,_6,_5,_4) => 353 Coprocessor (Coprocessor_Load b24 b23 b22 b21 (r 16) (r 12) (i4 8) 354 (i8 0)) 355 | (T,T,T, F ,_23,_22,_21,_20,_7,_6,_5, F) => 356 Coprocessor (Coprocessor_Data_Processing (i4 20) (r 16) (r 12) 357 (i4 8) (i3 5) (r 0)) 358 | (T,T,T, F ,_23,_22,_21,b20,_7,_6,_5, T) => 359 Coprocessor (Coprocessor_Transfer (i3 21) b20 (r 16) (r 12) (i4 8) 360 (i3 5) (r 0)) 361 | (T,T,T, T ,_23,_22,_21,_20,_7,_6,_5,_4) => 362 Miscellaneous (Supervisor_Call (i24 0)) 363 | __ => Undefined)`; 364 365(* ------------------------------------------------------------------------ *) 366 367val thumb_decode_def = zDefine` 368 thumb_decode arch IT (ireg : word16) = 369 let IT = if arch IN thumb2_support then IT else 0w in 370 let b n = ireg ' n 371 and r n = ( n + 2 >< n ) ireg : word4 372 and r4 n = ( n + 3 >< n ) ireg : word4 373 and InITBlock = InITBlock IT 374 and LastInITBlock = LastInITBlock IT 375 in 376 ((let cond = r4 8 in 377 if (15 >< 12) ireg <> (13w:word4) \/ cond IN {14w; 15w} then 378 if IT = 0w then 0b1110w else (7 >< 4) IT 379 else 380 cond), 381 case (b 15,b 14,b 13,b 12,b 11,b 10,b 9,b 8,b 7,b 6) 382 of (F,F,F, T , T , F , F,_8,_7,_6) => (* ADD(3) *) 383 DP 0b0100w (~InITBlock) (r 3) (r 0) (REG 0w 0w (r 6)) 384 | (F,F,F, T , T , F , T,_8,_7,_6) => (* SUB(3) *) 385 DP 0b0010w (~InITBlock) (r 3) (r 0) (REG 0w 0w (r 6)) 386 | (F,F,F, T , T , T , F,_8,_7,_6) => (* ADD(1) *) 387 DP 0b0100w (~InITBlock) (r 3) (r 0) (IMM ((8 >< 6) ireg)) 388 | (F,F,F, T , T , T , T,_8,_7,_6) => (* SUB(1) *) 389 DP 0b0010w (~InITBlock) (r 3) (r 0) (IMM ((8 >< 6) ireg)) 390 | (F,F,F,b12,b11,_10,_9,_8,_7,_6) => (* LSL(1), LSR(1), ASR(1) *) 391 DP 0b1101w (~InITBlock) 0w (r 0) 392 (REG ((10 >< 6) ireg) ((12 >< 11) ireg) (r 3)) 393 | (F,F,T, F , F ,_10,_9,_8,_7,_6) => (* MOV(1) *) 394 DP 0b1101w (~InITBlock) 0w (r 8) (IMM ((7 >< 0) ireg)) 395 | (F,F,T, F , T ,_10,_9,_8,_7,_6) => (* CMP(1) *) 396 DP 0b1010w T (r 8) 0w (IMM ((7 >< 0) ireg)) 397 | (F,F,T, T , F ,_10,_9,_8,_7,_6) => (* ADD(2) *) 398 DP 0b0100w (~InITBlock) (r 8) (r 8) (IMM ((7 >< 0) ireg)) 399 | (F,F,T, T , T ,_10,_9,_8,_7,_6) => (* SUB(2) *) 400 DP 0b0010w (~InITBlock) (r 8) (r 8) (IMM ((7 >< 0) ireg)) 401 | (F,T,F, F , F , F , F, F, F, F) => (* AND *) 402 DP 0b0000w (~InITBlock) (r 0) (r 0) (REG 0w 0w (r 3)) 403 | (F,T,F, F , F , F , F, F, F, T) => (* EOR *) 404 DP 0b0001w (~InITBlock) (r 0) (r 0) (REG 0w 0w (r 3)) 405 | (F,T,F, F , F , F , F, F, T, F) => (* LSL(2) *) 406 DP 0b1101w (~InITBlock) 0w (r 0) (SHIFTED (r 3) 0b00w (r 0)) 407 | (F,T,F, F , F , F , F, F, T, T) => (* LSR(2) *) 408 DP 0b1101w (~InITBlock) 0w (r 0) (SHIFTED (r 3) 0b01w (r 0)) 409 | (F,T,F, F , F , F , F, T, F, F) => (* ASR(2) *) 410 DP 0b1101w (~InITBlock) 0w (r 0) (SHIFTED (r 3) 0b10w (r 0)) 411 | (F,T,F, F , F , F , F, T, F, T) => (* ADC *) 412 DP 0b0101w (~InITBlock) (r 0) (r 0) (REG 0w 0w (r 3)) 413 | (F,T,F, F , F , F , F, T, T, F) => (* SBC *) 414 DP 0b0110w (~InITBlock) (r 0) (r 0) (REG 0w 0w (r 3)) 415 | (F,T,F, F , F , F , F, T, T, T) => (* ROR *) 416 DP 0b1101w (~InITBlock) 0w (r 0) (SHIFTED (r 3) 0b11w (r 0)) 417 | (F,T,F, F , F , F , T, F, F, F) => (* TST *) 418 DP 0b1000w T (r 0) 0w (REG 0w 0w (r 3)) 419 | (F,T,F, F , F , F , T, F, F, T) => (* RSB *) 420 DP 0b0011w (~InITBlock) (r 3) (r 0) (IMM 0w) 421 | (F,T,F, F , F , F , T, F, T, F) => (* CMP(2) *) 422 DP 0b1010w T (r 0) 0w (REG 0w 0w (r 3)) 423 | (F,T,F, F , F , F , T, F, T, T) => (* CMN *) 424 DP 0b1011w T (r 0) 0w (REG 0w 0w (r 3)) 425 | (F,T,F, F , F , F , T, T, F, F) => (* ORR *) 426 DP 0b1100w (~InITBlock) (r 0) (r 0) (REG 0w 0w (r 3)) 427 | (F,T,F, F , F , F , T, T, F, T) => (* MUL *) 428 DataProcessing (Multiply F (~InITBlock) (r 0) 0w (r 0) (r 3)) 429 | (F,T,F, F , F , F , T, T, T, F) => (* BIC *) 430 DP 0b1110w (~InITBlock) (r 0) (r 0) (REG 0w 0w (r 3)) 431 | (F,T,F, F , F , F , T, T, T, T) => (* MVN *) 432 DP 0b1111w (~InITBlock) 0w (r 0) (REG 0w 0w (r 3)) 433 | (F,T,F, F , F , T , F, F,b7,b6) => (* ADD(4) *) 434 (let rdn = (3 :+ b7) (r 0) and rm = r4 3 in 435 if ~b7 /\ ~b6 /\ arch NOTIN thumb2_support \/ 436 (rdn = 15w) /\ ((rm = 15w) \/ InITBlock /\ ~LastInITBlock) 437 then 438 Unpredictable 439 else 440 DP 0b0100w F rdn rdn (REG 0w 0w rm)) 441 | (F,T,F, F , F , T , F, T, F, F) => 442 Unpredictable 443 | (F,T,F, F , F , T , F, T,b7,_6) => (* CMP(3) *) 444 DP 0b1010w T ((3 :+ b7) (r 0)) 0w (REG 0w 0w (r4 3)) 445 | (F,T,F, F , F , T , T, F,b7,b6) => (* MOV(3) *) 446 (let rd = (3 :+ b7) (r 0) in 447 if ~b7 /\ ~b6 /\ version_number arch < 6 \/ 448 (rd = 15w) /\ InITBlock /\ ~LastInITBlock 449 then 450 Unpredictable 451 else 452 DP 0b1101w F 0w rd (REG 0w 0w (r4 3))) 453 | (F,T,F, F , F , T , T, T, F,_6) => (* BX *) 454 if InITBlock /\ ~LastInITBlock then 455 Unpredictable 456 else 457 Branch (Branch_Exchange (r4 3)) 458 | (F,T,F, F , F , T , T, T, T,_6) => (* BLX(2) *) 459 if InITBlock /\ ~LastInITBlock then 460 Unpredictable 461 else 462 Branch (Branch_Link_Exchange_Register (r4 3)) 463 | (F,T,F, F , T ,_10,_9,_8,_7,_6) => (* LDR(3) *) 464 LoadStore (Load T T F F F 15w (r 8) 465 (Mode2_immediate (((7 >< 0) ireg) << 2))) 466 | (F,T,F, T , F , F , F,_8,_7,_6) => (* STR(2) *) 467 LoadStore (Store T T F F F (r 3) (r 0) (Mode2_register 0w 0w (r 6))) 468 | (F,T,F, T , F , F , T,_8,_7,_6) => (* STRH(2) *) 469 LoadStore (Store_Halfword T T F F (r 3) (r 0) 470 (Mode3_register 0w (r 6))) 471 | (F,T,F, T , F , T , F,_8,_7,_6) => (* STRB(2) *) 472 LoadStore (Store T T T F F (r 3) (r 0) (Mode2_register 0w 0w (r 6))) 473 | (F,T,F, T , F , T , T,_8,_7,_6) => (* LDRSB *) 474 LoadStore (Load_Halfword T T F T F F (r 3) (r 0) 475 (Mode3_register 0w (r 6))) 476 | (F,T,F, T , T , F , F,_8,_7,_6) => (* LDR(2) *) 477 LoadStore (Load T T F F F (r 3) (r 0) (Mode2_register 0w 0w (r 6))) 478 | (F,T,F, T , T , F , T,_8,_7,_6) => (* LDRH(2) *) 479 LoadStore (Load_Halfword T T F F T F (r 3) (r 0) 480 (Mode3_register 0w (r 6))) 481 | (F,T,F, T , T , T , F,_8,_7,_6) => (* LDRB(2) *) 482 LoadStore (Load T T T F F (r 3) (r 0) (Mode2_register 0w 0w (r 6))) 483 | (F,T,F, T , T , T , T,_8,_7,_6) => (* LDRSH *) 484 LoadStore (Load_Halfword T T F T T F (r 3) (r 0) 485 (Mode3_register 0w (r 6))) 486 | (F,T,T, F , F ,_10,_9,_8,_7,_6) => (* STR(1) *) 487 LoadStore (Store T T F F F (r 3) (r 0) 488 (Mode2_immediate (((10 >< 6) ireg) << 2))) 489 | (F,T,T, F , T ,_10,_9,_8,_7,_6) => (* LDR(1) *) 490 LoadStore (Load T T F F F (r 3) (r 0) 491 (Mode2_immediate (((10 >< 6) ireg) << 2))) 492 | (F,T,T, T , F ,_10,_9,_8,_7,_6) => (* STRB(1) *) 493 LoadStore (Store T T T F F (r 3) (r 0) 494 (Mode2_immediate ((10 >< 6) ireg))) 495 | (F,T,T, T , T ,_10,_9,_8,_7,_6) => (* LDRB(1) *) 496 LoadStore (Load T T T F F (r 3) (r 0) 497 (Mode2_immediate ((10 >< 6) ireg))) 498 | (T,F,F, F , F ,_10,_9,_8,_7,_6) => (* STRH(1) *) 499 LoadStore (Store_Halfword T T F F (r 3) (r 0) 500 (Mode3_immediate (((10 >< 6) ireg) << 1))) 501 | (T,F,F, F , T ,_10,_9,_8,_7,_6) => (* LDRH(1) *) 502 LoadStore (Load_Halfword T T F F T F (r 3) (r 0) 503 (Mode3_immediate (((10 >< 6) ireg) << 1))) 504 | (T,F,F, T , F ,_10,_9,_8,_7,_6) => (* STR(3) *) 505 LoadStore (Store T T F F F 13w (r 8) 506 (Mode2_immediate (((7 >< 0) ireg) << 2))) 507 | (T,F,F, T , T ,_10,_9,_8,_7,_6) => (* LDR(4) *) 508 LoadStore (Load T T F F F 13w (r 8) 509 (Mode2_immediate (((7 >< 0) ireg) << 2))) 510 | (T,F,T, F , F ,_10,_9,_8,_7,_6) => (* ADD(5) *) 511 DataProcessing (Add_Sub T 15w (r 8) (((7 >< 0) ireg) << 2)) 512 | (T,F,T, F , T ,_10,_9,_8,_7,_6) => (* ADD(6) *) 513 DP 0b0100w F 13w (r 8) (IMM (0b1111_0000_0000w || ((7 >< 0) ireg))) 514 | (T,F,T, T , F , F , F, F, F,_6) => (* ADD(7) *) 515 DP 0b0100w F 13w 13w (IMM (0b1111_0000_0000w || ((6 >< 0) ireg))) 516 | (T,F,T, T , F , F , F, F, T,_6) => (* SUB(4) *) 517 DP 0b0010w F 13w 13w (IMM (0b1111_0000_0000w || ((6 >< 0) ireg))) 518 | (T,F,T, T ,b11, F ,b9, T,_7,_6) => 519 if InITBlock then 520 Unpredictable 521 else 522 Branch 523 (Compare_Branch b11 ((5 :+ b9) ((7 >< 3) ireg)) ((2 >< 0) ireg)) 524 | (T,F,T, T , F , F , T, F,b7, F) => 525 DataProcessing (Extend_Halfword b7 15w (r 0) 0w (r 3)) 526 | (T,F,T, T , F , F , T, F,b7, T) => 527 DataProcessing (Extend_Byte b7 15w (r 0) 0w (r 3)) 528 | (T,F,T, T , F , T , F,b8,_7,_6) => (* PUSH *) 529 LoadStore (Store_Multiple T F F T 13w ((14 :+ b8) ((7 >< 0) ireg))) 530 | (T,F,T, T , T , F , T, F, F, F) => 531 DataProcessing (Byte_Reverse_Word (r 0) (r 3)) 532 | (T,F,T, T , T , F , T, F, F, T) => 533 DataProcessing (Byte_Reverse_Packed_Halfword (r 0) (r 3)) 534 | (T,F,T, T , T , F , T, F, T, T) => 535 DataProcessing (Byte_Reverse_Signed_Halfword (r 0) (r 3)) 536 | (T,F,T, T , T , T , F,b8,_7,_6) => (* POP *) 537 if b8 /\ InITBlock /\ ~LastInITBlock then 538 Unpredictable 539 else 540 LoadStore (Load_Multiple F T F T 13w ((15 :+ b8) ((7 >< 0) ireg))) 541 | (T,F,T, T , F , T , T, F, F, T) => 542 if b 5 then 543 StatusAccess 544 (Change_Processor_State (if b 4 then 0b11w else 0b10w) 545 (b 2) (b 1) (b 0) NONE) 546 else 547 StatusAccess (Set_Endianness (b 3)) 548 | (T,F,T, T , T , T , T, F,_7,_6) => (* BKPT *) 549 Miscellaneous (Breakpoint ((7 >< 0) ireg)) 550 | (T,F,T, T , T , T , T, T,_7,_6) => 551 (let mask = r4 0 in 552 if mask = 0w then 553 Miscellaneous (Hint (hint_decode ((7 >< 4) ireg))) 554 else 555 Miscellaneous (If_Then (r4 4) mask)) 556 | (T,T,F, F , F ,b10,b9,b8,_7,_6) => (* STMIA *) 557 LoadStore (Store_Multiple F T F T (r 8) ((7 >< 0) ireg)) 558 | (T,T,F, F , T ,b10,b9,b8,b7,_6) => (* LDMIA *) 559 (let rn = r 8 in 560 let wback = ~(ireg ' (w2n rn)) in 561 LoadStore (Load_Multiple F T F wback rn ((7 >< 0) ireg))) 562 | (T,T,F, T , T , T , T, F,_7,_6) => 563 Undefined 564 | (T,T,F, T , T , T , T, T,_7,_6) => (* SVC *) 565 Miscellaneous (Supervisor_Call ((7 >< 0) ireg)) 566 | (T,T,F, T ,_11,_10,_9,_8,_7,_6) => (* B(1) *) 567 if InITBlock then 568 Unpredictable 569 else 570 Branch (Branch_Target (sw2sw ((7 >< 0) ireg : word8))) 571 | (T,T,T, F , F ,_10,_9,_8,_7,_6) => (* B(2) *) 572 if InITBlock /\ ~LastInITBlock then 573 Unpredictable 574 else 575 Branch (Branch_Target (sw2sw ((10 >< 0) ireg : word11))) 576 | _ => Undefined)`; 577 578val thumbee_decode_def = zDefine` 579 thumbee_decode arch IT (ireg : word16) = 580 let b n = ireg ' n 581 and r n = ( n + 2 >< n ) ireg : word4 582 and r4 n = ( n + 3 >< n ) ireg : word4 583 and cond = if IT = 0w then 0b1110w else (7 >< 4) IT 584 in 585 case (b 15,b 14,b 13,b 12,b 11,b 10,b 9,b 8) 586 of (F,T,F,T,F,F,F,_) => (* STR(2) *) 587 (Encoding_ThumbEE, cond, 588 LoadStore 589 (Store T T F F F (r 3) (r 0) (Mode2_register 2w 0w (r 6)))) 590 | (F,T,F,T,F,F,T,_) => (* STRH(2) *) 591 (Encoding_ThumbEE, cond, 592 LoadStore 593 (Store_Halfword T T F F (r 3) (r 0) (Mode3_register 1w (r 6)))) 594 | (F,T,F,T,T,F,F,_) => (* LDR(2) *) 595 (Encoding_ThumbEE, cond, 596 LoadStore (Load T T F F F (r 3) (r 0) (Mode2_register 2w 0w (r 6)))) 597 | (F,T,F,T,T,F,T,_) => (* LDRH(2) *) 598 (Encoding_ThumbEE, cond, 599 LoadStore 600 (Load_Halfword T T F F T F (r 3) (r 0) (Mode3_register 1w (r 6)))) 601 | (F,T,F,T,T,T,T,_) => (* LDRSH *) 602 (Encoding_ThumbEE, cond, 603 LoadStore 604 (Load_Halfword T T F T T F (r 3) (r 0) (Mode3_register 1w (r 6)))) 605 | (T,T,F,F,F,F,F,F) => 606 (Encoding_ThumbEE, cond, 607 if InITBlock IT /\ ~LastInITBlock IT then 608 Unpredictable 609 else 610 Branch (Handler_Branch_Parameter ((7 >< 5) ireg) ((4 >< 0) ireg))) 611 | (T,T,F,F,F,F,F,T) => 612 (Encoding_ThumbEE, cond, Undefined) 613 | (T,T,F,F,F,F,T,_) => 614 (Encoding_ThumbEE, cond, 615 if InITBlock IT /\ ~LastInITBlock IT then 616 Unpredictable 617 else 618 Branch (Handler_Branch_Link (b 8) ((7 >< 0) ireg))) 619 | (T,T,F,F,F,T,_,_) => 620 (Encoding_ThumbEE, cond, 621 if InITBlock IT /\ ~LastInITBlock IT then 622 Unpredictable 623 else 624 Branch 625 (Handler_Branch_Link_Parameter ((9 >< 5) ireg) ((4 >< 0) ireg))) 626 | (T,T,F,F,T,F,F,_) => 627 (Encoding_ThumbEE, cond, 628 LoadStore 629 (Load T F F F F (r 3) (r 0) 630 (Mode2_immediate (((8 >< 6) ireg) << 2)))) 631 | (T,T,F,F,T,F,T,F) => 632 (Encoding_ThumbEE, cond, 633 Branch (Check_Array ((3 :+ b 7) (r 0)) (r4 3))) 634 | (T,T,F,F,T,F,T,T) => 635 (Encoding_ThumbEE, cond, 636 LoadStore 637 (Load T T F F F 10w (r 0) 638 (Mode2_immediate (((7 >< 3) ireg) << 2)))) 639 | (T,T,F,F,T,T,F,_) => 640 (Encoding_ThumbEE, cond, 641 LoadStore 642 (Load T T F F F 9w (r 0) 643 (Mode2_immediate (((8 >< 3) ireg) << 2)))) 644 | (T,T,F,F,T,T,T,_) => 645 (Encoding_ThumbEE, cond, 646 LoadStore 647 (Store T T F F F 9w (r 0) 648 (Mode2_immediate (((8 >< 3) ireg) << 2)))) 649 | _ => (Encoding_Thumb, thumb_decode arch IT ireg)`; 650 651(* ------------------------------------------------------------------------ *) 652 653(* Load/store multiple, dual and exclusive, table branch *) 654val thumb2_decode_aux1_def = with_flag (priming, SOME "_") Define` 655 thumb2_decode_aux1 IT (ireg1 : word16, ireg2 : word16) = 656 let a n = ireg1 ' n 657 and b n = ireg2 ' n 658 and ra n = ( n + 3 >< n ) ireg1 : word4 659 and rb n = ( n + 3 >< n ) ireg2 : word4 660 in 661 case (a 8,a 7,a 6,a 5,a 4, b 7,b 6,b 5,b 4) 662 of (a8,a7, F,a5, F, b7,b6,b5,b4) => 663 (if a8 = a7 then 664 LoadStore (Store_Return_State (~a8) a8 a5 ((4 >< 0) ireg2)) 665 else 666 LoadStore (Store_Multiple a8 a7 F a5 (ra 0) ireg2)) 667 | (a8,a7, F,a5, T, b7,b6,b5,b4) => 668 (if a8 = a7 then 669 if InITBlock IT /\ ~LastInITBlock IT then 670 Unpredictable 671 else 672 LoadStore (Return_From_Exception (~a8) a8 a5 (ra 0)) 673 else 674 if b 15 /\ InITBlock IT /\ ~LastInITBlock IT then 675 Unpredictable 676 else 677 LoadStore (Load_Multiple a8 a7 F a5 (ra 0) ireg2)) 678 | ( F, F, T, F, F, b7,b6,b5,b4) => 679 LoadStore (Store_Exclusive (ra 0) (rb 8) (rb 12) ((7 >< 0) ireg2)) 680 | ( F, F, T, F, T, b7,b6,b5,b4) => 681 LoadStore (Load_Exclusive (ra 0) (rb 12) ((7 >< 0) ireg2)) 682 | ( F, T, T, F, F, F, T, F,b4) => 683 LoadStore 684 (if b4 then Store_Exclusive_Halfword (ra 0) (rb 0) (rb 12) 685 else Store_Exclusive_Byte (ra 0) (rb 0) (rb 12)) 686 | ( F, T, T, F, F, F, T, T, T) => 687 LoadStore (Store_Exclusive_Doubleword (ra 0) (rb 0) (rb 12) (rb 8)) 688 | ( F, T, T, F, T, F, F, F,b4) => 689 if InITBlock IT /\ ~LastInITBlock IT then 690 Unpredictable 691 else 692 Branch (Table_Branch_Byte (ra 0) b4 (rb 0)) 693 | ( F, T, T, F, T, F, T, F,b4) => 694 LoadStore 695 (if b4 then Load_Exclusive_Halfword (ra 0) (rb 12) 696 else Load_Exclusive_Byte (ra 0) (rb 12)) 697 | ( F, T, T, F, T, F, T, T, T) => 698 LoadStore (Load_Exclusive_Doubleword (ra 0) (rb 12) (rb 8)) 699 | ( F,a7, T, T, F, b7,b6,b5,b4) => 700 LoadStore (Store_Dual F a7 T (ra 0) (rb 12) (rb 8) 701 (Mode3_immediate (((7 >< 0) ireg2) << 2))) 702 | ( T,a7, T,a5, F, b7,b6,b5,b4) => 703 LoadStore (Store_Dual T a7 a5 (ra 0) (rb 12) (rb 8) 704 (Mode3_immediate (((7 >< 0) ireg2) << 2))) 705 | ( F,a7, T, T, T, b7,b6,b5,b4) => 706 LoadStore (Load_Dual F a7 T (ra 0) (rb 12) (rb 8) 707 (Mode3_immediate (((7 >< 0) ireg2) << 2))) 708 | ( T,a7, T,a5, T, b7,b6,b5,b4) => 709 LoadStore (Load_Dual T a7 a5 (ra 0) (rb 12) (rb 8) 710 (Mode3_immediate (((7 >< 0) ireg2) << 2))) 711 | _ => Undefined`; 712 713(* Data-processing (shifted register) *) 714val thumb2_decode_aux2_def = with_flag (priming, SOME "_") Define` 715 thumb2_decode_aux2 (ireg1 : word16, ireg2 : word16) = 716 let a n = ireg1 ' n 717 and b n = ireg2 ' n 718 and ra n = ( n + 3 >< n ) ireg1 : word4 719 and ib2 n = ( n + 1 >< n ) ireg2 : word2 720 and ib3 n = ( n + 2 >< n ) ireg2 : word3 721 and rb n = ( n + 3 >< n ) ireg2 : word4 722 in 723 let S = a 4 and rn = ra 0 and rd = rb 8 724 in 725 case (a 8,a 7,a 6,a 5) 726 of (F, F, F, F) => 727 (if rd = 15w then 728 if S then 729 DP 0b1000w T rn 0w (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)) 730 else 731 Unpredictable 732 else 733 DP 0b0000w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0))) 734 | (F, F, F, T) => 735 DP 0b1110w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)) 736 | (F, F, T, F) => 737 DP (if rn = 15w then 0b1101w else 0b1100w) S rn rd 738 (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)) 739 | (F, F, T, T) => 740 DP 0b1111w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)) 741 | (F, T, F, F) => 742 (if rd = 15w then 743 if S then 744 DP 0b1001w T rn 0w (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)) 745 else 746 Unpredictable 747 else 748 DP 0b0001w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0))) 749 | (F, T, T, F) => 750 (if S \/ b 4 then 751 Undefined 752 else 753 DataProcessing 754 (Pack_Halfword rn rd (ib3 12 @@ ib2 6) (b 5) (rb 0))) 755 | (T, F, F, F) => 756 (if rd = 15w then 757 if S then 758 DP 0b1011w T rn 0w (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)) 759 else 760 Unpredictable 761 else 762 DP 0b0100w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0))) 763 | (T, F, T, F) => 764 DP 0b0101w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)) 765 | (T, F, T, T) => 766 DP 0b0110w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)) 767 | (T, T, F, T) => 768 (if rd = 15w then 769 if S then 770 DP 0b1010w T rn 0w (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)) 771 else 772 Unpredictable 773 else 774 DP 0b0010w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0))) 775 | (T, T, T, F) => 776 DP 0b0011w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)) 777 | _ => Undefined`; 778 779(* Coprocessor *) 780val thumb2_decode_aux3_def = with_flag (priming, SOME "_") Define` 781 thumb2_decode_aux3 (ireg1 : word16, ireg2 : word16) = 782 let a n = ireg1 ' n 783 and b n = ireg2 ' n 784 and ia3 n = ( n + 2 >< n ) ireg1 : word3 785 and ia4 n = ( n + 3 >< n ) ireg1 : word4 786 and ib3 n = ( n + 2 >< n ) ireg2 : word3 787 and ib4 n = ( n + 3 >< n ) ireg2 : word4 788 and ib8 n = ( n + 7 >< n ) ireg2 : word8 789 in 790 let ra = ia4 and rb = ib4 791 in 792 case (a 9,a 8,a 7,a 6,a 5,a 4) 793 of (F,F, F, T, F,a4) => 794 Coprocessor 795 (Coprocessor_Transfer_Two a4 (ra 0) (rb 12) (ib4 8) (ib4 4) (rb 0)) 796 | (F,F, F,a6, T, F) => 797 Coprocessor 798 (Coprocessor_Store F F a6 T (ra 0) (rb 12) (ib4 8) (ib8 0)) 799 | (F,F, T,a6,a5, F) => 800 Coprocessor 801 (Coprocessor_Store F T a6 a5 (ra 0) (rb 12) (ib4 8) (ib8 0)) 802 | (F,T,a7,a6,a5, F) => 803 Coprocessor 804 (Coprocessor_Store T a7 a6 a5 (ra 0) (rb 12) (ib4 8) (ib8 0)) 805 | (F,F, F,a6, T, T) => 806 Coprocessor 807 (Coprocessor_Load F F a6 T (ra 0) (rb 12) (ib4 8) (ib8 0)) 808 | (F,F, T,a6,a5, T) => 809 Coprocessor 810 (Coprocessor_Load F T a6 a5 (ra 0) (rb 12) (ib4 8) (ib8 0)) 811 | (F,T,a7,a6,a5, T) => 812 Coprocessor 813 (Coprocessor_Load T a7 a6 a5 (ra 0) (rb 12) (ib4 8) (ib8 0)) 814 | (T,F,a7,a6,a5,a4) => 815 if b 4 then 816 Coprocessor 817 (Coprocessor_Transfer (ia3 4) a4 (ra 0) (rb 12) (ib4 8) 818 (ib3 5) (rb 0)) 819 else 820 Coprocessor 821 (Coprocessor_Data_Processing (ia4 4) (ra 0) (rb 12) (ib4 8) 822 (ib3 5) (rb 0)) 823 | _ => Undefined`; 824 825val _ = wordsLib.guess_lengths(); 826 827(* Data-processing (modified immediate) *) 828val thumb2_decode_aux4_def = with_flag (priming, SOME "_") Define` 829 thumb2_decode_aux4 (ireg1 : word16, ireg2 : word16) = 830 let a n = ireg1 ' n 831 and ia1 n = ( n + 0 >< n ) ireg1 : word1 832 and ra n = ( n + 3 >< n ) ireg1 : word4 833 and ib3 n = ( n + 2 >< n ) ireg2 : word3 834 and ib8 n = ( n + 7 >< n ) ireg2 : word8 835 and rb n = ( n + 3 >< n ) ireg2 : word4 836 in 837 let S = a 4 and rn = ra 0 and rd = rb 8 838 in 839 case (a 8,a 7,a 6,a 5) 840 of (F, F, F, F) => 841 if rd = 15w then 842 if S then 843 DP 0b1000w T rn 0w (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 844 else 845 Unpredictable 846 else 847 DP 0b0000w S rn rd (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 848 | (F, F, F, T) => 849 DP 0b1110w S rn rd (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 850 | (F, F, T, F) => 851 DP (if rn = 15w then 0b1101w else 0b1100w) S rn rd 852 (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 853 | (F, F, T, T) => 854 DP 0b1111w S rn rd (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 855 | (F, T, F, F) => 856 if rd = 15w then 857 if S then 858 DP 0b1001w T rn 0w (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 859 else 860 Unpredictable 861 else 862 DP 0b0001w S rn rd (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 863 | (T, F, F, F) => 864 if rd = 15w then 865 if S then 866 DP 0b1011w T rn 0w (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 867 else 868 Unpredictable 869 else 870 DP 0b0100w S rn rd (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 871 | (T, F, T, F) => 872 DP 0b0101w S rn rd (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 873 | (T, F, T, T) => 874 DP 0b0110w S rn rd (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 875 | (T, T, F, T) => 876 if rd = 15w then 877 if S then 878 DP 0b1010w T rn 0w (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 879 else 880 Unpredictable 881 else 882 DP 0b0010w S rn rd (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 883 | (T, T, T, F) => 884 DP 0b0011w S rn rd (IMM (ia1 10 @@ ib3 12 @@ ib8 0)) 885 | _ => Undefined`; 886 887(* Data-processing (plain binary immediate) *) 888val thumb2_decode_aux5_def = with_flag (priming, SOME "_") Define` 889 thumb2_decode_aux5 (ireg1 : word16, ireg2 : word16) = 890 let a n = ireg1 ' n 891 and ia1 n = ( n + 0 >< n ) ireg1 : word1 892 and ia4 n = ( n + 3 >< n ) ireg1 : word4 893 and ib2 n = ( n + 1 >< n ) ireg2 : word2 894 and ib3 n = ( n + 2 >< n ) ireg2 : word3 895 and ib4 n = ( n + 3 >< n ) ireg2 : word4 896 and ib5 n = ( n + 4 >< n ) ireg2 : word5 897 and ib8 n = ( n + 7 >< n ) ireg2 : word8 898 in 899 let ra = ia4 and rb = ib4 900 in 901 if a 4 then Undefined else 902 case (a 8,a 7,a 6,a 5) 903 of (F, F, F, F) => 904 DataProcessing (Add_Sub T (ra 0) (rb 8) (ia1 10 @@ ib3 12 @@ ib8 0)) 905 | (F, T, F, T) => 906 DataProcessing (Add_Sub F (ra 0) (rb 8) (ia1 10 @@ ib3 12 @@ ib8 0)) 907 | (F,a7, T, F) => 908 DataProcessing 909 (Move_Halfword a7 (rb 8) (ia4 0 @@ ia1 10 @@ ib3 12 @@ ib8 0)) 910 | (T,a7, F,a5) => 911 (let imm5 = ib3 12 @@ ib2 6 in 912 if a5 /\ (imm5 = 0w) then 913 DataProcessing (Saturate_16 a7 (ib4 0) (rb 8) (ra 0)) 914 else 915 DataProcessing (Saturate a7 (ib5 0) (rb 8) imm5 a5 (ra 0))) 916 | (T,a7, T, F) => 917 DataProcessing 918 (Bit_Field_Extract a7 (ib5 0) (rb 8) (ib3 12 @@ ib2 6) (ra 0)) 919 | (T, F, T, T) => 920 DataProcessing 921 (Bit_Field_Clear_Insert (ib5 0) (rb 8) (ib3 12 @@ ib2 6) (ra 0)) 922 | _ => Undefined`; 923 924(* Branches and miscellaneous control *) 925val thumb2_decode_aux6_def = with_flag (priming, SOME "_") Define` 926 thumb2_decode_aux6 IT (ireg1 : word16, ireg2 : word16) = 927 let a n = ireg1 ' n 928 and b n = ireg2 ' n 929 and ia1 n = ( n + 0 >< n ) ireg1 : word1 930 and ia4 n = ( n + 3 >< n ) ireg1 : word4 931 and ia6 n = ( n + 5 >< n ) ireg1 : word6 932 and ia10 n = ( n + 9 >< n ) ireg1 : word10 933 and ib1 n = ( n + 0 >< n ) ireg2 : word1 934 and ib2 n = ( n + 1 >< n ) ireg2 : word2 935 and ib4 n = ( n + 3 >< n ) ireg2 : word4 936 and ib5 n = ( n + 4 >< n ) ireg2 : word5 937 and ib8 n = ( n + 7 >< n ) ireg2 : word8 938 and ib10 n = ( n + 9 >< n ) ireg2 : word10 939 and ib11 n = ( n + 10 >< n ) ireg2 : word11 940 in 941 let ra = ia4 and rb = ib4 942 and InITBlock = InITBlock IT 943 and LastInITBlock = LastInITBlock IT 944 in 945 case (a 10,a 9,a 8,a 7,a 6,a 5,a 4, 946 b 14,b 13,b 12,b 11,b 10,b 9,b 8,b 7,b 6,b 5,b 4) 947 of (F , T, T, T, F, F, a4, F ,b13, F ,b11,b10,b9,b8,b7,b6,b5,b4) => 948 StatusAccess (Register_to_Status a4 (rb 8) (ra 0)) 949 | (F , T, T, T, F, T, F, F ,b13, F ,b11, F , F, F,b7,b6,b5,b4) => 950 Miscellaneous (Hint (hint_decode (ib8 0))) 951 | (F , T, T, T, F, T, F, F ,b13, F ,b11,b10,b9,b8,b7,b6,b5,b4) => 952 (if InITBlock then 953 Unpredictable 954 else let mode = ib5 0 in 955 if ~b8 /\ (mode <> 0w) then 956 Unpredictable 957 else 958 StatusAccess 959 (Change_Processor_State (ib2 9) b7 b6 b5 960 (if b8 then SOME mode else NONE))) 961 | (F , T, T, T, F, T, T, F ,b13, F ,b11,b10,b9,b8, F, F, F, b4) => 962 if InITBlock then 963 Unpredictable 964 else 965 Miscellaneous (Enterx_Leavex b4) 966 | (F , T, T, T, F, T, T, F ,b13, F ,b11,b10,b9,b8, F, F, T, F) => 967 Miscellaneous Clear_Exclusive 968 | (F , T, T, T, F, T, T, F ,b13, F ,b11,b10,b9,b8, F, T, F, F) => 969 Miscellaneous (Data_Synchronization_Barrier (ib4 0)) 970 | (F , T, T, T, F, T, T, F ,b13, F ,b11,b10,b9,b8, F, T, F, T) => 971 Miscellaneous (Data_Memory_Barrier (ib4 0)) 972 | (F , T, T, T, F, T, T, F ,b13, F ,b11,b10,b9,b8, F, T, T, F) => 973 Miscellaneous (Instruction_Synchronization_Barrier (ib4 0)) 974 | (F , T, T, T, T, F, T, F ,b13, F ,b11,b10,b9,b8,b7,b6,b5,b4) => 975 if InITBlock /\ ~LastInITBlock then 976 Unpredictable 977 else 978 DP 0b0010w T 14w 15w (IMM ((7 >< 0) ireg2)) 979 | (F , T, T, T, T, T,a4, F ,b13, F ,b11,b10,b9,b8,b7,b6,b5,b4) => 980 StatusAccess (Status_to_Register a4 (rb 8)) 981 | (T , T, T, T, T, T, T, F , F , F ,b11,b10,b9,b8,b7,b6,b5,b4) => 982 Miscellaneous (Secure_Monitor_Call (ia4 0)) 983 | (a10, T, T, T,a6,a5,a4, F ,b13, F ,b11,b10,b9,b8,b7,b6,b5,b4) => 984 Undefined 985 | (a10,a9,a8,a7,a6,a5,a4, F ,b13, F ,b11,b10,b9,b8,b7,b6,b5,b4) => 986 (if InITBlock then 987 Unpredictable 988 else let S = ia1 10 and J1 = ib1 13 and J2 = ib1 11 in 989 Branch 990 (Branch_Target (sw2sw (S @@ J2 @@ J1 @@ ia6 0 @@ ib11 0)))) 991 | (a10,a9,a8,a7,a6,a5,a4, F ,b13, T ,b11,b10,b9,b8,b7,b6,b5,b4) => 992 (if InITBlock /\ ~LastInITBlock then 993 Unpredictable 994 else let S = ia1 10 and J1 = ib1 13 and J2 = ib1 11 in 995 let I1 = ~(J1 ?? S) and I2 = ~(J2 ?? S) in 996 Branch (Branch_Target (S @@ I1 @@ I2 @@ ia10 0 @@ ib11 0))) 997 | (a10,a9,a8,a7,a6,a5,a4, T ,b13,b12,b11,b10,b9,b8,b7,b6,b5,b4) => 998 (if ~b12 /\ b 0 then 999 Undefined 1000 else if InITBlock /\ ~LastInITBlock then 1001 Unpredictable 1002 else let S = ia1 10 and J1 = ib1 13 and J2 = ib1 11 in 1003 let I1 = ~(J1 ?? S) and I2 = ~(J2 ?? S) in 1004 Branch 1005 (Branch_Link_Exchange_Immediate (b 0) (~b12) 1006 (S @@ I1 @@ I2 @@ ia10 0 @@ ib10 1)))`; 1007 1008(* Load/store, memory hints *) 1009val thumb2_decode_aux7_def = with_flag (priming, SOME "_") Define` 1010 thumb2_decode_aux7 IT (ireg1 : word16, ireg2 : word16) = 1011 let a n = ireg1 ' n 1012 and b n = ireg2 ' n 1013 and ra n = ( n + 3 >< n ) ireg1 : word4 1014 and ib2 n = ( n + 1 >< n ) ireg2 : word2 1015 and rb n = ( n + 3 >< n ) ireg2 : word4 1016 and ib5 n = ( n + 4 >< n ) ireg2 : word5 1017 and ib12 n = ( n + 11 >< n ) ireg2 : word12 1018 in 1019 let rn = ra 0 and rt = rb 12 1020 in 1021 if a 4 then 1022 if rt = 15w then 1023 if rn = 15w then 1024 case (a 8,a 7,a 6,a 5) 1025 of (F,a7,F , F) => 1026 Miscellaneous 1027 (Preload_Data a7 F rn (Mode2_immediate (ib12 0))) 1028 | (F,a7,F , T) => 1029 Unpredictable 1030 | (F,a7,T , F) => 1031 if InITBlock IT /\ ~LastInITBlock IT then 1032 Unpredictable 1033 else 1034 LoadStore 1035 (Load T a7 F F F rn rt (Mode2_immediate (ib12 0))) 1036 | (T,a7,F , F) => 1037 Miscellaneous 1038 (Preload_Instruction a7 rn (Mode2_immediate (ib12 0))) 1039 | (T,a7,a6,a5) => 1040 Miscellaneous (Hint Hint_nop) 1041 | _ => Undefined 1042 else 1043 case (a 8,a 7,a 6,a 5, b 11,b 10,b 9,b 8,b 7,b 6) 1044 of (F,T,F,a5, b11,b10,b9,b8,b7,b6) => 1045 Miscellaneous 1046 (Preload_Data T a5 rn (Mode2_immediate (ib12 0))) 1047 | (F,F,F,a5, T , T , F, F,b7,b6) => 1048 Miscellaneous 1049 (Preload_Data T a5 rn (Mode2_immediate ((7 >< 0) ireg2))) 1050 | (F,F,F,a5, F , F , F, F, F, F) => 1051 Miscellaneous 1052 (Preload_Data T a5 rn 1053 (Mode2_register ((5 >< 4) ireg2) 0w (rb 0))) 1054 | (F,F,F,a5, T ,b10,b9, T,b7,b6) => 1055 Unpredictable 1056 | (F,F,F,a5, T , T , T, F,b7,b6) => 1057 Unpredictable 1058 | (F,T,T, F, b11,b10,b9,b8,b7,b6) => 1059 if InITBlock IT /\ ~LastInITBlock IT then 1060 Unpredictable 1061 else 1062 LoadStore (Load T T F F F rn rt (Mode2_immediate (ib12 0))) 1063 | (F,F,T, F, T ,b10,b9, T,b7,b6) => 1064 if InITBlock IT /\ ~LastInITBlock IT then 1065 Unpredictable 1066 else 1067 LoadStore 1068 (Load b10 b9 F T F rn rt 1069 (Mode2_immediate ((7 >< 0) ireg2))) 1070 | (F,F,T, F, T , T ,b9, F,b7,b6) => 1071 if InITBlock IT /\ ~LastInITBlock IT then 1072 Unpredictable 1073 else 1074 LoadStore 1075 (Load T b9 F F b9 rn rt (Mode2_immediate ((7 >< 0) ireg2))) 1076 | (F,F,T, F, F , F , F, F, F, F) => 1077 if InITBlock IT /\ ~LastInITBlock IT then 1078 Unpredictable 1079 else 1080 LoadStore 1081 (Load T T F F F rn rt 1082 (Mode2_register ((5 >< 4) ireg2) 0w (rb 0))) 1083 | (T,F,F,F, F , F , F, F, F, F) => 1084 Miscellaneous 1085 (Preload_Instruction F rn 1086 (Mode2_register ((5 >< 4) ireg2) 0w (rb 0))) 1087 | (T,F,F,F, T , T , F, F,b7,b6) => 1088 Miscellaneous 1089 (Preload_Instruction F rn (Mode2_immediate (ib12 0))) 1090 | (T,F,F,T, F , F , F, F, F, F) => 1091 Miscellaneous (Hint Hint_nop) 1092 | (T,F,F,T, T , T , F, F,b7,b6) => 1093 Miscellaneous (Hint Hint_nop) 1094 | (T,F,F,a5, T ,b10,b9, T,b7,b6) => 1095 Unpredictable 1096 | (T,F,F,a5, T , T , T, F,b7,b6) => 1097 Unpredictable 1098 | (T,T,F,T, b11,b10,b9,b8,b7,b6) => 1099 Miscellaneous (Hint Hint_nop) 1100 | _ => Undefined 1101 else 1102 if rn = 15w then 1103 case (a 8,a 7,a 6,a 5) 1104 of (F,a7,a6, F) => 1105 LoadStore 1106 (Load T a7 (~a6) F F rn rt (Mode2_immediate (ib12 0))) 1107 | (F,a7, F, T) => 1108 LoadStore 1109 (Load_Halfword T a7 F F T F rn rt (Mode3_immediate (ib12 0))) 1110 | (T,a7, F,a5) => 1111 LoadStore 1112 (Load_Halfword T a7 F T a5 F rn rt 1113 (Mode3_immediate (ib12 0))) 1114 | _ => Undefined 1115 else 1116 case (a 8,a 7,a 6,a 5, b 11,b 10,b 9,b 8,b 7,b 6) 1117 of ( F, T,a6, F, b11,b10,b9,b8,b7,b6) => 1118 LoadStore (Load T T (~a6) F F rn rt (Mode2_immediate (ib12 0))) 1119 | ( F, F,a6, F, T ,b10,b9, T,b7,b6) => 1120 LoadStore 1121 (Load b10 b9 (~a6) T F rn rt 1122 (Mode2_immediate ((7 >< 0) ireg2))) 1123 | ( F, F,a6, F, T , T ,b9, F,b7,b6) => 1124 LoadStore 1125 (Load T b9 (~a6) F b9 rn rt 1126 (Mode2_immediate ((7 >< 0) ireg2))) 1127 | ( F, F,a6, F, F , F , F, F, F, F) => 1128 LoadStore 1129 (Load T T (~a6) F F rn rt 1130 (Mode2_register ((5 >< 4) ireg2) 0w (rb 0))) 1131 | ( F, T, F, T, b11,b10,b9,b8,b7,b6) => 1132 LoadStore 1133 (Load_Halfword T T F F T F rn rt (Mode3_immediate (ib12 0))) 1134 | ( F, F, F, T, T ,b10,b9, T,b7,b6) => 1135 LoadStore 1136 (Load_Halfword b10 b9 T F T F rn rt 1137 (Mode3_immediate ((7 >< 0) ireg2))) 1138 | ( F, F, F, T, T , T ,b9, F,b7,b6) => 1139 LoadStore 1140 (Load_Halfword T b9 F F T b9 rn rt 1141 (Mode3_immediate ((7 >< 0) ireg2))) 1142 | ( F, F, F, T, F , F , F, F, F, F) => 1143 LoadStore 1144 (Load_Halfword T T F F T F rn rt 1145 (Mode3_register (ib2 4) (rb 0))) 1146 | ( T, T, F,a5, b11,b10,b9,b8,b7,b6) => 1147 LoadStore 1148 (Load_Halfword T T F T a5 F rn rt (Mode3_immediate (ib12 0))) 1149 | ( T, F, F,a5, T ,b10,b9, T,b7,b6) => 1150 LoadStore 1151 (Load_Halfword b10 b9 T T a5 F rn rt 1152 (Mode3_immediate ((7 >< 0) ireg2))) 1153 | ( T, F, F,a5, T , T ,b9, F,b7,b6) => 1154 LoadStore 1155 (Load_Halfword T b9 F T a5 b9 rn rt 1156 (Mode3_immediate ((7 >< 0) ireg2))) 1157 | ( T, F, F,a5, F , F , F, F, F, F) => 1158 LoadStore 1159 (Load_Halfword T T F T a5 F rn rt 1160 (Mode3_register (ib2 4) (rb 0))) 1161 | _ => Undefined 1162 else 1163 if rn = 15w then 1164 Undefined 1165 else 1166 case (a 8,a 7,a 6,a 5, b 11) 1167 of (F, T,a6, F, b11) => 1168 LoadStore (Store T T (~a6) F F rn rt (Mode2_immediate (ib12 0))) 1169 | (F, F,a6, F, T ) => 1170 (let b10 = b 10 and b9 = b 9 and b8 = b 8 in 1171 if b10 \/ b8 then 1172 LoadStore 1173 (Store b10 b9 (~a6) b8 (b10 /\ b9 /\ ~b8) rn rt 1174 (Mode2_immediate ((7 >< 0) ireg2))) 1175 else 1176 Undefined) 1177 | (F, F,a6, F, F ) => 1178 if ib5 6 = 0w then 1179 LoadStore 1180 (Store T T (~a6) F F rn rt 1181 (Mode2_register ((5 >< 4) ireg2) 0w (rb 0))) 1182 else 1183 Undefined 1184 | (F, T, F, T, b11) => 1185 LoadStore 1186 (Store_Halfword T T F F rn rt (Mode3_immediate (ib12 0))) 1187 | (F, F, F, T, T ) => 1188 (let b10 = b 10 and b9 = b 9 and b8 = b 8 in 1189 if b10 \/ b8 then 1190 LoadStore 1191 (Store_Halfword b10 b9 b8 (b10 /\ b9 /\ ~b8) rn rt 1192 (Mode3_immediate ((7 >< 0) ireg2))) 1193 else 1194 Undefined) 1195 | (F, F, F, T, F ) => 1196 if ib5 6 = 0w then 1197 LoadStore 1198 (Store_Halfword T T F F rn rt 1199 (Mode3_register (ib2 4) (rb 0))) 1200 else 1201 Undefined 1202 | _ => Undefined`; 1203 1204(* Data-processing (register) *) 1205val thumb2_decode_aux8_def = with_flag (priming, SOME "_") Define` 1206 thumb2_decode_aux8 (ireg1 : word16, ireg2 : word16) = 1207 let a n = ireg1 ' n 1208 and b n = ireg2 ' n 1209 and ia2 n = ( n + 1 >< n ) ireg1 : word2 1210 and ia3 n = ( n + 2 >< n ) ireg1 : word3 1211 and ia4 n = ( n + 3 >< n ) ireg1 : word4 1212 and ib2 n = ( n + 1 >< n ) ireg2 : word2 1213 and ib3 n = ( n + 2 >< n ) ireg2 : word3 1214 and ib4 n = ( n + 3 >< n ) ireg2 : word4 1215 in 1216 let ra = ia4 and rb = ib4 1217 in 1218 if rb 12 <> 15w then 1219 Undefined 1220 else 1221 case (a 7,b 7,b 6) 1222 of (F,F, F) => 1223 if ib2 4 = 0w then 1224 DP 0b1101w (a 4) 0w (rb 8) (SHIFTED (rb 0) (ia2 5) (ra 0)) 1225 else 1226 Undefined 1227 | (F,T,b6) => 1228 (case (a 6,a 5) 1229 of (F,F) => DataProcessing 1230 (Extend_Halfword (a 4) (ra 0) (rb 8) (ib2 4) (rb 0)) 1231 | (F,T) => DataProcessing 1232 (Extend_Byte_16 (a 4) (ra 0) (rb 8) (ib2 4) (rb 0)) 1233 | (T,F) => DataProcessing 1234 (Extend_Byte (a 4) (ra 0) (rb 8) (ib2 4) (rb 0)) 1235 | (T,T) => Undefined) 1236 | (T,F,b6) => 1237 DataProcessing 1238 (Parallel_Add_Subtract b6 1239 (parallel_add_sub_thumb_decode (ib2 4,ia3 4)) 1240 (ra 0) (rb 8) (rb 0)) 1241 | (T,T, F) => 1242 (let opc2 = ib2 4 in 1243 case (a 6,a 5,a 4) 1244 of (F,F,F) => 1245 (let opc3 = case opc2 1246 of 0b01w => 0b10w 1247 | 0b10w => 0b01w 1248 | _ => opc2 1249 in 1250 DataProcessing 1251 (Saturating_Add_Subtract opc3 (ra 0) (rb 8) (rb 0))) 1252 | (F,F,T) => (let rm1 = ra 0 and rm2 = rb 0 in 1253 if rm1 <> rm2 then 1254 Unpredictable 1255 else 1256 case opc2 1257 of 0b00w => DataProcessing 1258 (Byte_Reverse_Word (rb 8) rm1) 1259 | 0b01w => DataProcessing 1260 (Byte_Reverse_Packed_Halfword (rb 8) rm1) 1261 | 0b10w => DataProcessing 1262 (Reverse_Bits (rb 8) rm1) 1263 | 0b11w => DataProcessing 1264 (Byte_Reverse_Signed_Halfword (rb 8) rm1)) 1265 | (F,T,F) => 1266 if opc2 = 0w then 1267 DataProcessing (Select_Bytes (ra 0) (rb 8) (rb 0)) 1268 else 1269 Undefined 1270 | (F,T,T) => 1271 if opc2 = 0w then 1272 let rm1 = ra 0 and rm2 = rb 0 in 1273 if rm1 <> rm2 then 1274 Unpredictable 1275 else 1276 DataProcessing (Count_Leading_Zeroes (rb 8) rm1) 1277 else 1278 Undefined 1279 | _ => Undefined) 1280 | _ => Undefined`; 1281 1282(* Multiplies, divide and absolute difference *) 1283val thumb2_decode_aux9_def = with_flag (priming, SOME "_") Define` 1284 thumb2_decode_aux9 (ireg1 : word16, ireg2 : word16) = 1285 let a n = ireg1 ' n in 1286 if ~a 8 then thumb2_decode_aux8 (ireg1,ireg2) 1287 else 1288 let b n = ireg2 ' n 1289 and ra n = ( n + 3 >< n ) ireg1 : word4 1290 and rb n = ( n + 3 >< n ) ireg2 : word4 1291 in 1292 let rb12 = rb 12 1293 in 1294 case (a 7,a 6,a 5,a 4, b 7,b 6,b 5,b 4) 1295 of (F, F, F, F, F,F, F, F) => 1296 (let A = rb12 <> 15w in 1297 DataProcessing 1298 (Multiply A F (rb 8) (if A then rb12 else 0w) (rb 0) (ra 0))) 1299 | (F, F, F, F, F,F, F, T) => 1300 DataProcessing (Multiply_Subtract (rb 8) rb12 (rb 0) (ra 0)) 1301 | (F, F, F, T, F,F,b5,b4) => 1302 if rb12 = 15w then 1303 DataProcessing 1304 (Signed_Halfword_Multiply 3w b4 b5 (rb 8) 0w (rb 0) (ra 0)) 1305 else 1306 DataProcessing 1307 (Signed_Halfword_Multiply 0w b4 b5 (rb 8) rb12 (rb 0) (ra 0)) 1308 | (F, F, T, F, F,F, F,b4) => 1309 DataProcessing 1310 (Signed_Multiply_Dual (rb 8) rb12 (rb 0) F b4 (ra 0)) 1311 | (F, F, T, T, F,F, F,b4) => 1312 if rb12 = 15w then 1313 DataProcessing 1314 (Signed_Halfword_Multiply 1w b4 T (rb 8) 0w (rb 0) (ra 0)) 1315 else 1316 DataProcessing 1317 (Signed_Halfword_Multiply 1w b4 F (rb 8) rb12 (rb 0) (ra 0)) 1318 | (F, T, F, F, F,F, F,b4) => 1319 DataProcessing 1320 (Signed_Multiply_Dual (rb 8) rb12 (rb 0) T b4 (ra 0)) 1321 | (F, T, F, T, F,F, F,b4) => 1322 DataProcessing 1323 (Signed_Most_Significant_Multiply (rb 8) rb12 (rb 0) b4 (ra 0)) 1324 | (F, T, T, F, F,F, F,b4) => 1325 DataProcessing 1326 (Signed_Most_Significant_Multiply_Subtract (rb 8) rb12 (rb 0) 1327 b4 (ra 0)) 1328 | (F, T, T, T, F,F, F, F) => 1329 DataProcessing 1330 (Unsigned_Sum_Absolute_Differences (rb 8) rb12 (rb 0) (ra 0)) 1331 | (T,a6,a5, F, F,F, F, F) => 1332 DataProcessing 1333 (Multiply_Long (~a5) a6 F (rb 8) rb12 (rb 0) (ra 0)) 1334 | (T, F,a5, T, T,T, T, T) => 1335 DataProcessing (Divide a5 (ra 0) (rb 8) (rb 0)) 1336 | (T, T, F, F, T,F,b5,b4) => 1337 DataProcessing 1338 (Signed_Halfword_Multiply 2w b4 b5 (rb 8) rb12 (rb 0) (ra 0)) 1339 | (T, T, F,a4, T,T, F,b4) => 1340 DataProcessing 1341 (Signed_Multiply_Long_Dual (rb 8) rb12 (rb 0) a4 b4 (ra 0)) 1342 | (T, T, T, F, F,T, T, F) => 1343 DataProcessing 1344 (Multiply_Accumulate_Accumulate (rb 8) rb12 (rb 0) (ra 0)) 1345 | _ => Undefined`; 1346 1347(* ........................................................................ *) 1348 1349val thumb2_decode_def = with_flag (priming, SOME "_") Define` 1350 thumb2_decode arch IT (ireg1 : word16, ireg2 : word16) = 1351 let IT = if arch IN thumb2_support then IT else 0w 1352 and a n = ireg1 ' n 1353 and b n = ireg2 ' n 1354 in 1355 let a12 = a 12 and a11 = a 11 and a9 = a 9 and b15 = b 15 1356 in 1357 ((if a12 /\ ~a11 /\ ~(a9 /\ a 8 /\ a 7) /\ 1358 b15 /\ ~b 14 /\ ~b 12 1359 then 1360 (9 >< 6) ireg1 : word4 1361 else 1362 if IT = 0w then 0b1110w else (7 >< 4) IT), 1363 case (a12,a11,a 10,a9,b15) of 1364 (F,T,F,F,_) => thumb2_decode_aux1 IT (ireg1,ireg2) 1365 | (F,T,F,T,_) => thumb2_decode_aux2 (ireg1,ireg2) 1366 | (_,T,T,_,_) => thumb2_decode_aux3 (ireg1,ireg2) 1367 | (T,F,_,F,F) => thumb2_decode_aux4 (ireg1,ireg2) 1368 | (T,F,_,T,F) => thumb2_decode_aux5 (ireg1,ireg2) 1369 | (T,F,_,_,T) => thumb2_decode_aux6 IT (ireg1,ireg2) 1370 | (T,T,F,F,_) => thumb2_decode_aux7 IT (ireg1,ireg2) 1371 | (T,T,F,T,_) => thumb2_decode_aux9 (ireg1,ireg2) 1372 | _ => Undefined)`; 1373 1374(* ------------------------------------------------------------------------ *) 1375 1376(* speed up evaluation *) 1377 1378val decode_lem = Q.prove( 1379 `((BIT 27 n,BIT 26 n,BIT 25 n,BIT 24 n,BIT 23 n,BIT 22 n,BIT 21 n, 1380 BIT 20 n,BIT 7 n,BIT 6 n,BIT 5 n,BIT 4 n) = 1381 let (q0,b4) = DIVMOD_2EXP 1 (DIV_2EXP 4 n) in 1382 let (q1,b5) = DIVMOD_2EXP 1 q0 in 1383 let (q2,b6) = DIVMOD_2EXP 1 q1 in 1384 let (q3,b7) = DIVMOD_2EXP 1 q2 in 1385 let (q4,b20) = DIVMOD_2EXP 1 (DIV_2EXP 12 q3) in 1386 let (q5,b21) = DIVMOD_2EXP 1 q4 in 1387 let (q6,b22) = DIVMOD_2EXP 1 q5 in 1388 let (q7,b23) = DIVMOD_2EXP 1 q6 in 1389 let (q8,b24) = DIVMOD_2EXP 1 q7 in 1390 let (q9,b25) = DIVMOD_2EXP 1 q8 in 1391 let (q10,b26) = DIVMOD_2EXP 1 q9 in 1392 (ODD q10,b26 = 1,b25 = 1,b24 = 1,b23 = 1,b22 = 1,b21 = 1,b20 = 1, 1393 b7 = 1,b6 = 1,b5 = 1,b4 = 1)) /\ 1394 ((BIT 15 n,BIT 14 n,BIT 13 n,BIT 12 n,BIT 11 n,BIT 10 n,BIT 9 n, 1395 BIT 8 n,BIT 7 n,BIT 6 n) = 1396 let (q0,b6) = DIVMOD_2EXP 1 (DIV_2EXP 6 n) in 1397 let (q1,b7) = DIVMOD_2EXP 1 q0 in 1398 let (q2,b8) = DIVMOD_2EXP 1 q1 in 1399 let (q3,b9) = DIVMOD_2EXP 1 q2 in 1400 let (q4,b10) = DIVMOD_2EXP 1 q3 in 1401 let (q5,b11) = DIVMOD_2EXP 1 q4 in 1402 let (q6,b12) = DIVMOD_2EXP 1 q5 in 1403 let (q7,b13) = DIVMOD_2EXP 1 q6 in 1404 let (q8,b14) = DIVMOD_2EXP 1 q7 in 1405 (ODD q8,b14 = 1,b13 = 1,b12 = 1,b11 = 1,b10 = 1,b9 = 1,b8 = 1, 1406 b7 = 1,b6 = 1)) /\ 1407 ((BIT 8 m,BIT 7 m,BIT 6 m,BIT 5 m,BIT 4 m,BIT 7 n,BIT 6 n,BIT 5 n, 1408 BIT 4 n) = 1409 let (q0,a4) = DIVMOD_2EXP 1 (DIV_2EXP 4 m) in 1410 let (q1,a5) = DIVMOD_2EXP 1 q0 in 1411 let (q2,a6) = DIVMOD_2EXP 1 q1 in 1412 let (q3,a7) = DIVMOD_2EXP 1 q2 in 1413 let (q0,b4) = DIVMOD_2EXP 1 (DIV_2EXP 4 n) in 1414 let (q1,b5) = DIVMOD_2EXP 1 q0 in 1415 let (q2,b6) = DIVMOD_2EXP 1 q1 in 1416 (ODD q3,a7 = 1,a6 = 1,a5 = 1,a4 = 1, 1417 ODD q2,b6 = 1,b5 = 1,b4 = 1)) /\ 1418 ((BIT 8 m,BIT 7 m,BIT 6 m,BIT 5 m) = 1419 let (q0,a4) = DIVMOD_2EXP 1 (DIV_2EXP 4 m) in 1420 let (q1,a5) = DIVMOD_2EXP 1 q0 in 1421 let (q2,a6) = DIVMOD_2EXP 1 q1 in 1422 let (q3,a7) = DIVMOD_2EXP 1 q2 in 1423 (ODD q3,a7 = 1,a6 = 1,a5 = 1)) /\ 1424 ((BIT 10 m,BIT 9 m,BIT 8 m,BIT 7 m,BIT 6 m,BIT 5 m,BIT 4 m,BIT 14 n, 1425 BIT 13 n,BIT 12 n,BIT 11 n,BIT 10 n,BIT 9 n,BIT 8 n,BIT 7 n, 1426 BIT 6 n,BIT 5 n,BIT 4 n) = 1427 let (q0,a4) = DIVMOD_2EXP 1 (DIV_2EXP 4 m) in 1428 let (q1,a5) = DIVMOD_2EXP 1 q0 in 1429 let (q2,a6) = DIVMOD_2EXP 1 q1 in 1430 let (q3,a7) = DIVMOD_2EXP 1 q2 in 1431 let (q4,a8) = DIVMOD_2EXP 1 q3 in 1432 let (r5,a9) = DIVMOD_2EXP 1 q4 in 1433 let (q0,b4) = DIVMOD_2EXP 1 (DIV_2EXP 4 n) in 1434 let (q1,b5) = DIVMOD_2EXP 1 q0 in 1435 let (q2,b6) = DIVMOD_2EXP 1 q1 in 1436 let (q3,b7) = DIVMOD_2EXP 1 q2 in 1437 let (q4,b8) = DIVMOD_2EXP 1 q3 in 1438 let (q5,b9) = DIVMOD_2EXP 1 q4 in 1439 let (q6,b10) = DIVMOD_2EXP 1 q5 in 1440 let (q7,b11) = DIVMOD_2EXP 1 q6 in 1441 let (q8,b12) = DIVMOD_2EXP 1 q7 in 1442 let (q9,b13) = DIVMOD_2EXP 1 q8 in 1443 (ODD r5,a9 = 1,a8 = 1,a7 = 1,a6 = 1,a5 = 1,a4 = 1, 1444 ODD q9,b13 = 1,b12 = 1,b11 = 1,b10 = 1,b9 = 1,b8 = 1, 1445 b7 = 1,b6 = 1,b5 = 1,b4 = 1)) /\ 1446 ((BIT 9 m,BIT 8 m,BIT 7 m,BIT 6 m,BIT 5 m,BIT 4 m) = 1447 let (q0,a4) = DIVMOD_2EXP 1 (DIV_2EXP 4 m) in 1448 let (q1,a5) = DIVMOD_2EXP 1 q0 in 1449 let (q2,a6) = DIVMOD_2EXP 1 q1 in 1450 let (q3,a7) = DIVMOD_2EXP 1 q2 in 1451 let (q4,a8) = DIVMOD_2EXP 1 q3 in 1452 (ODD q4,a8 = 1,a7 = 1,a6 = 1,a5 = 1,a4 = 1)) /\ 1453 ((BIT 12 m,BIT 11 m,BIT 10 m,BIT 9 m,BIT 15 n) = 1454 let (q0,a9) = DIVMOD_2EXP 1 (DIV_2EXP 9 m) in 1455 let (q1,a10) = DIVMOD_2EXP 1 q0 in 1456 let (q2,a11) = DIVMOD_2EXP 1 q1 in 1457 (ODD q2,a11 = 1,a10 = 1,a9 = 1,BIT 15 n)) /\ 1458 ((BIT 7 m,BIT 6 m,BIT 5 m,BIT 4 m,BIT 7 n,BIT 6 n,BIT 5 n,BIT 4 n) = 1459 let (q0,a4) = DIVMOD_2EXP 1 (DIV_2EXP 4 m) in 1460 let (q1,a5) = DIVMOD_2EXP 1 q0 in 1461 let (r2,a6) = DIVMOD_2EXP 1 q1 in 1462 let (q0,b4) = DIVMOD_2EXP 1 (DIV_2EXP 4 n) in 1463 let (q1,b5) = DIVMOD_2EXP 1 q0 in 1464 let (q2,b6) = DIVMOD_2EXP 1 q1 in 1465 (ODD r2,a6 = 1,a5 = 1,a4 = 1, 1466 ODD q2,b6 = 1,b5 = 1,b4 = 1)) /\ 1467 ((BIT 8 m,BIT 7 m,BIT 6 m,BIT 5 m,BIT 11 n,BIT 10 n,BIT 9 n,BIT 8 n, 1468 BIT 7 n,BIT 6 n) = 1469 let (q0,a5) = DIVMOD_2EXP 1 (DIV_2EXP 5 m) in 1470 let (q1,a6) = DIVMOD_2EXP 1 q0 in 1471 let (r2,a7) = DIVMOD_2EXP 1 q1 in 1472 let (q0,b6) = DIVMOD_2EXP 1 (DIV_2EXP 6 n) in 1473 let (q1,b7) = DIVMOD_2EXP 1 q0 in 1474 let (q2,b8) = DIVMOD_2EXP 1 q1 in 1475 let (q3,b9) = DIVMOD_2EXP 1 q2 in 1476 let (q4,b10) = DIVMOD_2EXP 1 q3 in 1477 (ODD r2,a7 = 1,a6 = 1,a5 = 1, 1478 ODD q4,b10 = 1,b9 = 1,b8 = 1,b7 = 1,b6 = 1)) /\ 1479 ((BIT 8 m,BIT 7 m,BIT 6 m,BIT 5 m,BIT 11 n) = 1480 let (q0,a5) = DIVMOD_2EXP 1 (DIV_2EXP 5 m) in 1481 let (q1,a6) = DIVMOD_2EXP 1 q0 in 1482 let (q2,a7) = DIVMOD_2EXP 1 q1 in 1483 (ODD q2,a7 = 1,a6 = 1,a5 = 1,BIT 11 n))`, 1484 SRW_TAC [boolSimps.LET_ss] 1485 [BIT_def,BITS_THM,DIVMOD_2EXP_def,DIV_2EXP_def,DIV_1, 1486 DIV2_def,ODD_MOD2_LEM,DIV_DIV_DIV_MULT,MOD_2EXP_def]); 1487 1488val n2w = CONJ (INST_TYPE [alpha |-> ``:16``] wordsTheory.word_index) 1489 (INST_TYPE [alpha |-> ``:32``] wordsTheory.word_index) 1490 |> SIMP_RULE (srw_ss()) []; 1491 1492val EQ_BITS = 1493 wordsTheory.word_eq_n2w 1494 |> CONJUNCT1 1495 |> REWRITE_RULE 1496 [MOD_2EXP_EQ_def, MOD_2EXP_def, GSYM wordsTheory.dimword_def, 1497 wordsTheory.MOD_DIMINDEX]; 1498 1499fun rule l = 1500 SIMP_RULE std_ss [decode_lem] o 1501 SIMP_RULE (std_ss++wordsLib.WORD_ss++boolSimps.LET_ss) 1502 [n2w, EQ_BITS, BITS_COMP_THM2, BITS_ZERO2] o 1503 SIMP_RULE (std_ss++wordsLib.SIZES_ss) 1504 [InITBlock_def, LastInITBlock_def, 1505 wordsTheory.word_extract_n2w, 1506 wordsTheory.word_bits_n2w] o 1507 Q.SPECL l; 1508 1509val arm_decode = rule [`v4`,`n2w n`] arm_decode_def; 1510 1511val arm_decode_v4 = save_thm("arm_decode_v4", 1512 arm_decode 1513 |> Q.INST [`v4:bool` |-> `T`] 1514 |> REWRITE_RULE []); 1515 1516val arm_decode_not_v4 = save_thm("arm_decode_not_v4", 1517 arm_decode 1518 |> Q.INST [`v4:bool` |-> `F`] 1519 |> REWRITE_RULE []); 1520 1521val thumb_decode = save_thm("thumb_decode", 1522 rule [`arch`,`it`,`n2w n`] thumb_decode_def); 1523 1524val thumbee_decode = save_thm("thumbee_decode", 1525 rule [`arch`,`it`,`n2w n`] thumbee_decode_def); 1526 1527val thumb2_decode_aux1 = save_thm("thumb2_decode_aux1", 1528 rule [`n2w it`, `n2w m`, `n2w n`] thumb2_decode_aux1_def); 1529 1530val thumb2_decode_aux2 = save_thm("thumb2_decode_aux2", 1531 rule [`n2w m`, `n2w n`] thumb2_decode_aux2_def); 1532 1533val thumb2_decode_aux3 = save_thm("thumb2_decode_aux3", 1534 rule [`n2w m`, `n2w n`] thumb2_decode_aux3_def); 1535 1536val thumb2_decode_aux4 = save_thm("thumb2_decode_aux4", 1537 rule [`n2w m`, `n2w n`] thumb2_decode_aux4_def); 1538 1539val thumb2_decode_aux5 = save_thm("thumb2_decode_aux5", 1540 rule [`n2w m`, `n2w n`] thumb2_decode_aux5_def); 1541 1542val thumb2_decode_aux6 = save_thm("thumb2_decode_aux6", 1543 rule [`n2w it`, `n2w m`, `n2w n`] thumb2_decode_aux6_def); 1544 1545val thumb2_decode_aux7 = save_thm("thumb2_decode_aux7", 1546 rule [`n2w it`, `n2w m`, `n2w n`] thumb2_decode_aux7_def); 1547 1548val thumb2_decode_aux8 = save_thm("thumb2_decode_aux8", 1549 rule [`n2w m`, `n2w n`] thumb2_decode_aux8_def); 1550 1551val thumb2_decode_aux9 = save_thm("thumb2_decode_aux9", 1552 rule [`n2w m`, `n2w n`] thumb2_decode_aux9_def); 1553 1554val thumb2_decode = save_thm("thumb2_decode", 1555 rule [`arch`,`n2w it`, `n2w m`, `n2w n`] thumb2_decode_def); 1556 1557val _ = computeLib.add_persistent_funs 1558 ["arm_decode_v4", 1559 "arm_decode_not_v4", 1560 "thumb_decode", 1561 "thumbee_decode", 1562 "thumb2_decode_aux1", 1563 "thumb2_decode_aux2", 1564 "thumb2_decode_aux3", 1565 "thumb2_decode_aux4", 1566 "thumb2_decode_aux5", 1567 "thumb2_decode_aux6", 1568 "thumb2_decode_aux7", 1569 "thumb2_decode_aux8", 1570 "thumb2_decode_aux9", 1571 "thumb2_decode"]; 1572 1573(* ------------------------------------------------------------------------ *) 1574 1575val _ = export_theory(); 1576