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