1structure arm_encoderLib :> arm_encoderLib = 2struct 3 4(* interactive use: 5 app load ["arm_parserLib"]; 6*) 7 8open HolKernel boolLib bossLib; 9open armSyntax arm_astSyntax; 10 11(* ------------------------------------------------------------------------- *) 12 13val _ = numLib.prefer_num(); 14val _ = wordsLib.prefer_word(); 15 16val ERR = Feedback.mk_HOL_ERR "arm_encoderLib"; 17 18local 19 val tm_g = Parse.term_grammar () 20 val ty_g = Parse.type_grammar () 21in 22 val term_to_string = 23 PP.pp_to_string 70 24 (Parse.mlower o term_pp.pp_term tm_g ty_g PPBackEnd.raw_terminal) 25end 26 27(* ------------------------------------------------------------------------- *) 28 29val eval = boolSyntax.rhs o Thm.concl o bossLib.EVAL; 30 31val pad = StringCvt.padLeft #"0" 32 33val uint_of_word = wordsSyntax.uint_of_word; 34val sint_of_term = Arbint.toInt o intSyntax.int_of_term; 35 36fun mk_bool b = if b then T else F; 37fun mk_word4 i = wordsSyntax.mk_wordii (i,4); 38 39val PC = mk_word4 15; 40 41val is_T = Term.term_eq T; 42val is_F = Term.term_eq F; 43val is_R9 = Term.term_eq (mk_word4 9); 44val is_R10 = Term.term_eq (mk_word4 10); 45val is_SP = Term.term_eq (mk_word4 13); 46val is_AL = Term.term_eq (mk_word4 14); 47val is_PC = Term.term_eq PC; 48val is_LR = is_AL; 49 50fun NOT tm = if is_T tm then F else if is_F tm then T else raise ERR "NOT" ""; 51 52val dest_strip = armSyntax.dest_strip; 53 54infix $; 55 56fun op $ (n,(h,l)) = 57 wordsSyntax.mk_word_bits (numSyntax.term_of_int h, numSyntax.term_of_int l, n) 58 |> eval; 59 60local 61 open Arbnum 62 infix pow 63 64 fun term_to_num tm = 65 let open wordsSyntax in 66 if is_word_type (Term.type_of tm) then 67 tm |> dest_n2w |> fst |> numSyntax.dest_numeral 68 else if is_T tm then 69 Arbnum.one 70 else if is_F tm then 71 Arbnum.zero 72 else 73 raise ERR "term_to_num" "" 74 end 75 76 fun lsl (n,i) = n * (two pow (fromInt i)) 77in 78 fun is_0 tm = term_to_num tm = zero 79 80 fun width_okay w tm = 81 let val n = term_to_num tm in 82 if n = zero then Int.<(0,w) else Int.<(toInt (log2 n),w) 83 end 84 85 val term_list_to_num = 86 List.foldl (fn ((tm,i),n) => n + lsl (term_to_num tm,i)) zero 87end; 88 89fun check (f,m) b = (b () orelse raise ERR f (term_to_string m); I); 90 91fun check_is_15 s tm = check (s,tm) (fn _ => is_PC tm); 92 93(* ------------------------------------------------------------------------- *) 94 95fun encode_ascii s = 96 s |> String.explode 97 |> List.map (pad 2 o Int.fmt StringCvt.HEX o Char.ord) 98 |> Lib.separate " " 99 |> String.concat; 100 101fun encode_byte l = 102let fun byte_to_int tm = 103 let val i = sint_of_term tm in 104 if i < 0 then i + 256 else i 105 end 106in 107 l |> map (pad 2 o Int.fmt StringCvt.HEX o byte_to_int) 108 |> Lib.separate " " 109 |> String.concat 110end; 111 112fun encode_short l = 113let fun short_to_int tm = 114 let val i = sint_of_term tm in 115 if i < 0 then i + 65536 else i 116 end 117in 118 l |> List.map (pad 4 o Int.fmt StringCvt.HEX o short_to_int) 119 |> Lib.separate " " 120 |> String.concat 121end; 122 123fun encode_word l = 124let open Arbint 125 fun int_to_num_string tm = 126 let val i = intSyntax.int_of_term tm in 127 (if i < zero then i + fromString "4294967296" else i) 128 |> toNat |> Arbnum.toHexString |> pad 8 129 end 130in 131 l |> List.map int_to_num_string 132 |> Lib.separate " " 133 |> String.concat 134end; 135 136(* ------------------------------------------------------------------------- *) 137 138fun encode_mode1 tm = 139 case dest_strip tm 140 of ("Mode1_immediate", [imm12]) => 141 [(T,25), (imm12,0)] 142 | ("Mode1_register", [imm5,typ,rm]) => 143 [(imm5,7), (typ,5), (rm,0)] 144 | ("Mode1_register_shifted_register", [rs,typ,rm]) => 145 [(rs,8), (typ,5), (T,4), (rm,0)] 146 | _ => raise ERR "encode_mode1" ""; 147 148fun encode_mode2 tm = 149 case dest_strip tm 150 of ("Mode2_immediate", [imm12]) => [(imm12,0)] 151 | ("Mode2_register", [imm5,typ,rm]) => [(T,25), (imm5,7), (typ,5), (rm,0)] 152 | _ => raise ERR "encode_mode2" ""; 153 154fun encode_mode3 tm = 155 case dest_strip tm 156 of ("Mode3_immediate", [imm12]) => 157 check ("encode_mode3", tm) (fn _ => width_okay 8 imm12) 158 [(T,22), (imm12$(7,4),8), (imm12$(3,0),0)] 159 | ("Mode3_register", [imm2,rm]) => 160 check ("encode_mode3", tm) (fn _ => is_0 imm2) 161 [(rm,0)] 162 | _ => raise ERR "encode_mode3" ""; 163 164fun parallel_add_sub_op1 tm = 165 case fst (Term.dest_const tm) 166 of "Parallel_normal" => ``0b01w:word2`` 167 | "Parallel_saturating" => ``0b10w:word2`` 168 | "Parallel_halving" => ``0b11w:word2`` 169 | _ => raise ERR "parallel_add_sub_op1" ""; 170 171fun thumb_parallel_add_sub_op1 tm = 172 case fst (Term.dest_const tm) 173 of "Parallel_normal" => ``0b00w:word2`` 174 | "Parallel_saturating" => ``0b01w:word2`` 175 | "Parallel_halving" => ``0b10w:word2`` 176 | _ => raise ERR "thumb_parallel_add_sub_op1" ""; 177 178fun parallel_add_sub_op2 tm = 179 case fst (Term.dest_const tm) 180 of "Parallel_add_16" => ``0b000w:word3`` 181 | "Parallel_add_sub_exchange" => ``0b001w:word3`` 182 | "Parallel_sub_add_exchange" => ``0b010w:word3`` 183 | "Parallel_sub_16" => ``0b011w:word3`` 184 | "Parallel_add_8" => ``0b100w:word3`` 185 | "Parallel_sub_8" => ``0b111w:word3`` 186 | _ => raise ERR "parallel_add_sub_op2" ""; 187 188fun thumb_parallel_add_sub_op2 tm = 189 case fst (Term.dest_const tm) 190 of "Parallel_add_16" => ``0b001w:word3`` 191 | "Parallel_add_sub_exchange" => ``0b010w:word3`` 192 | "Parallel_sub_add_exchange" => ``0b110w:word3`` 193 | "Parallel_sub_16" => ``0b101w:word3`` 194 | "Parallel_add_8" => ``0b000w:word3`` 195 | "Parallel_sub_8" => ``0b100w:word3`` 196 | _ => raise ERR "thumb_parallel_add_sub_op2" ""; 197 198val parallel_add_sub = 199 (parallel_add_sub_op1 ## parallel_add_sub_op2) o pairSyntax.dest_pair; 200 201val thumb_parallel_add_sub = 202 (thumb_parallel_add_sub_op1 ## thumb_parallel_add_sub_op2) o 203 pairSyntax.dest_pair; 204 205fun hint tm = 206 case dest_strip tm 207 of ("Hint_nop", []) => [] 208 | ("Hint_yield", []) => [(T,0)] 209 | ("Hint_wait_for_event", []) => [(T,1)] 210 | ("Hint_wait_for_interrupt", []) => [(``0b11w:word2``,0)] 211 | ("Hint_send_event", []) => [(T,2)] 212 | ("Hint_debug", [opt]) => [(PC,4),(opt,0)] 213 | _ => raise ERR "hint" ""; 214 215fun thumb_hint tm = 216 case dest_strip tm 217 of ("Hint_nop", []) => [] 218 | ("Hint_yield", []) => [(T,4)] 219 | ("Hint_wait_for_event", []) => [(T,5)] 220 | ("Hint_wait_for_interrupt", []) => [(``0b11w:word2``,4)] 221 | ("Hint_send_event", []) => [(T,6)] 222 | _ => raise ERR "thumb_hint" "cannot encode"; 223 224(* ------------------------------------------------------------------------- *) 225 226fun encode_branch (cond,tm) = term_list_to_num ((cond,28):: 227 (case dest_strip tm 228 of ("Branch_Target", [imm24]) => 229 [(T,27), (T,25), (imm24,0)] 230 | ("Branch_Exchange", [rm]) => 231 [(T,24), (T,21), (PC,16),(PC,12),(PC,8), (T,4), (rm,0)] 232 | ("Branch_Link_Exchange_Immediate", [h,toarm,imm24]) => 233 check ("encode_branch", tm) (fn _ => is_T toarm orelse is_PC cond) 234 [(T,27), (T,25), (if is_T toarm then T else h,24), (imm24,0)] 235 | ("Branch_Link_Exchange_Register", [rm]) => 236 [(T,24), (T,21), (PC,16),(PC,12),(PC,8), (T,5), (T,4), (rm,0)] 237 | _ => raise ERR "encode_branch" ("cannot encode: " ^ term_to_string tm))); 238 239fun check_dp (tm,rd,rn) = 240 case uint_of_word tm 241 of 8 => is_0 rd 242 | 9 => is_0 rd 243 | 10 => is_0 rd 244 | 11 => is_0 rd 245 | 13 => is_0 rn 246 | 15 => is_0 rn 247 | _ => true; 248 249fun encode_data_processing (cond,tm) = term_list_to_num ((cond,28):: 250 (case dest_strip tm 251 of ("Data_Processing", [opc,s,n,d,mode1]) => 252 check ("encode_data_processing", tm) (fn _ => check_dp (opc,d,n)) 253 [(opc,21), (s,20), (n,16), (d,12)] @ encode_mode1 mode1 254 | ("Move_Halfword", [h,d,imm16]) => 255 [(T,25), (T,24), (h,22), (imm16$(15,12),16), (d,12), (imm16$(11,0),0)] 256 | ("Add_Sub", [a,n,d,imm12]) => 257 [(a,23), (NOT a,22), (n,16), (d,12)] @ 258 encode_mode1 (mk_Mode1_immediate imm12) 259 | ("Multiply", [acc,s,d,a,m,n]) => 260 [(acc,21), (s,20), (d,16), (if is_T acc then a else mk_word4 0,12), 261 (m,8), (T,7), (T, 4), (n,0)] 262 | ("Multiply_Subtract", [d,a,m,n]) => 263 [(T,22), (T,21), (d,16), (a,12), (m,8), (T,7), (T, 4), (n,0)] 264 | ("Signed_Halfword_Multiply", [opc,M,N,d,a,m,n]) => 265 let val a = case uint_of_word opc 266 of 1 => if is_T N then mk_word4 0 else a 267 | 3 => mk_word4 0 268 | _ => a 269 in 270 [(T,24), (opc,21), (d,16), (a,12), (m,8), (T,7), (M,6), (N,5), (n,0)] 271 end 272 | ("Signed_Multiply_Dual", [d,a,m,M,N,n]) => 273 [(``7w:word3``,24), (d,16), (a,12), (m,8), (M,6), (N,5), (T,4), (n,0)] 274 | ("Signed_Multiply_Long_Dual", [dhi,dlo,m,M,N,n]) => 275 [(``7w:word3``,24), (T,22), (dhi,16), (dlo,12), (m,8), 276 (M,6), (N,5), (T,4), (n,0)] 277 | ("Signed_Most_Significant_Multiply", [d,a,m,r,n]) => 278 [(``7w:word3``,24), (T,22), (T,20), (d,16), (a,12), (m,8), 279 (r,5), (T,4), (n,0)] 280 | ("Signed_Most_Significant_Multiply_Subtract", [d,a,m,r,n]) => 281 [(``7w:word3``,24), (T,22), (T,20), (d,16), (a,12), (m,8), 282 (T,7), (T,6), (r,5), (T,4), (n,0)] 283 | ("Multiply_Long", [sgnd,a,s,dhi,dlo,m,n]) => 284 [(T,23), (sgnd,22), (a,21), (s,20), (dhi,16), (dlo,12), (m,8), 285 (T,7), (T,4), (n,0)] 286 | ("Multiply_Accumulate_Accumulate", [dhi,dlo,m,n]) => 287 [(T,22), (dhi,16), (dlo,12), (m,8), (T,7), (T,4), (n,0)] 288 | ("Saturate", [u,sat,d,imm5,sh,n]) => 289 [(T,26), (T,25), (T,23), (u,22), (T,21), (sat,16), (d,12), (imm5,7), 290 (sh,6), (T,4), (n,0)] 291 | ("Saturate_16", [u,imm4,d,n]) => 292 [(T,26), (T,25), (T,23), (u,22), (T,21), (imm4,16), (d,12), (PC,8), 293 (T,5), (T,4), (n,0)] 294 | ("Saturating_Add_Subtract", [opc,n,d,m]) => 295 [(T,24), (opc,21), (n,16), (d,12), (T,6), (T,4), (m,0)] 296 | ("Pack_Halfword", [n,d,imm5,t,m]) => 297 [(T,26), (T,25), (T,23), (n,16), (d,12), (imm5,7), (t,6), (T,4), (m,0)] 298 | ("Extend_Byte", [u,n,d,rot,m]) => 299 [(T,26), (T,25), (T,23), (u,22), (T,21), (n,16), (d,12), 300 (rot,10), (T,6), (T,5), (T,4), (m,0)] 301 | ("Extend_Byte_16", [u,n,d,rot,m]) => 302 [(T,26), (T,25), (T,23), (u,22), (n,16), (d,12), 303 (rot,10), (T,6), (T,5), (T,4), (m,0)] 304 | ("Extend_Halfword", [u,n,d,rot,m]) => 305 [(T,26), (T,25), (T,23), (u,22), (T,21), (T,20), (n,16), (d,12), 306 (rot,10), (T,6), (T,5), (T,4), (m,0)] 307 | ("Bit_Field_Clear_Insert", [msb,d,lsb,n]) => 308 [(``0b11111w:word5``,22), (msb,16), (d,12), (lsb,7), (T,4), (n,0)] 309 | ("Count_Leading_Zeroes", [d,m]) => 310 [(T,24), (T,22), (T,21), (PC,16), (d,12), (PC,8), (T,4), (m, 0)] 311 | ("Reverse_Bits", [d,m]) => 312 [(T,26), (T,25), (PC,20), (PC,16), (d,12), (PC,8), (T,5), (T,4), (m, 0)] 313 | ("Byte_Reverse_Word", [d,m]) => 314 [(T,26), (T,25), (``0b1011w:word4``,20), (PC,16), (d,12), (PC,8), 315 (T,5), (T,4), (m, 0)] 316 | ("Byte_Reverse_Packed_Halfword", [d,m]) => 317 [(T,26), (T,25), (``0b1011w:word4``,20), (PC,16), (d,12), (PC,8), 318 (T,7), (T,5), (T,4), (m, 0)] 319 | ("Byte_Reverse_Signed_Halfword", [d,m]) => 320 [(T,26), (T,25), (PC,20), (PC,16), (d,12), (PC,8), 321 (T,7), (T,5), (T,4), (m, 0)] 322 | ("Bit_Field_Extract", [u,w,d,lsb,n]) => 323 [(PC,23), (u,22), (T,21), (w,16), (d,12), (lsb,7), (T,6), (T,4), (n, 0)] 324 | ("Select_Bytes", [n,d,m]) => 325 [(T,26), (T,25), (T,23), (n,16), (d,12), (PC,8), 326 (T,7), (T,5), (T,4), (m, 0)] 327 | ("Unsigned_Sum_Absolute_Differences", [d,a,m,n]) => 328 [(PC,23), (d,16), (a,12), (m,8), (T,4), (n, 0)] 329 | ("Parallel_Add_Subtract", [u,opc,n,d,m]) => 330 let val (opc1,opc2) = parallel_add_sub opc in 331 [(T,26), (T,25), (u,22), (opc1,20), (n,16), (d,12), (PC,8), 332 (opc2,5), (T,4), (m, 0)] 333 end 334 | _ => raise ERR "encode_data_processing" 335 ("cannot encode: " ^ term_to_string tm))); 336 337fun encode_status_access (cond,tm) = term_list_to_num ((cond,28):: 338 (case dest_strip tm 339 of ("Status_to_Register", [r,d]) => 340 [(T,24), (r,22), (PC, 16), (d,12)] 341 | ("Immediate_to_Status", [r,mask,imm12]) => 342 [(T,25), (T,24), (r,22), (T,21), (mask,16), (PC, 12), (imm12,0)] 343 | ("Register_to_Status", [r,mask,n]) => 344 [(T,24), (r,22), (T,21), (mask,16), (PC, 12), (n,0)] 345 | ("Change_Processor_State", [imod,a,i,f,mode]) => 346 let val (M,m) = if optionSyntax.is_some mode then 347 (T,optionSyntax.dest_some mode) 348 else 349 (F,mk_word4 0) 350 in 351 check_is_15 "encode_status_access: cond" cond 352 [(T,24), (imod,18), (M,17), (a,8), (i,7), (f,6), (m,0)] 353 end 354 | ("Set_Endianness", [e]) => 355 check_is_15 "encode_status_access: cond" cond [(T,24), (T,16), (e, 9)] 356 | _ => raise ERR "encode_status_access" 357 ("cannot encode: " ^ term_to_string tm))); 358 359fun encode_load_store (cond,tm) = term_list_to_num ((cond,28):: 360 (case dest_strip tm 361 of ("Load", [p,u,b,w,_,n,t,mode2]) => 362 [(T,26), (p,24), (u,23), (b,22), (w,21), (T,20), (n,16), (t,12)] @ 363 encode_mode2 mode2 364 | ("Store", [p,u,b,w,_,n,t,mode2]) => 365 [(T,26), (p,24), (u,23), (b,22), (w,21), (n,16), (t,12)] @ 366 encode_mode2 mode2 367 | ("Load_Halfword", [p,u,w,s,h,_,n,t,mode3]) => 368 [(p,24), (u,23), (w,21), (T,20), (n,16), (t,12), (T,7), (s,6), 369 (h,5), (T,4)] @ encode_mode3 mode3 370 | ("Store_Halfword", [p,u,w,_,n,t,mode3]) => 371 [(p,24), (u,23), (w,21), (n,16), (t,12), (T,7), (T,5), (T,4)] @ 372 encode_mode3 mode3 373 | ("Load_Dual", [p,u,w,n,t,t2,mode3]) => 374 [(p,24), (u,23), (w,21), (n,16), (t,12), (T,7), (T,6), (T,4)] @ 375 encode_mode3 mode3 376 | ("Store_Dual", [p,u,w,n,t,t2,mode3]) => 377 [(p,24), (u,23), (w,21), (n,16), (t,12), (PC,4)] @ encode_mode3 mode3 378 | ("Load_Multiple", [p,u,s,w,n,registers]) => 379 [(T,27), (p,24), (u,23), (s,22), (w,21), (T,20), (n,16), (registers,0)] 380 | ("Store_Multiple", [p,u,s,w,n,registers]) => 381 [(T,27), (p,24), (u,23), (s,22), (w,21), (n,16), (registers,0)] 382 | ("Load_Exclusive", [n,t,imm8]) => 383 check ("encode_load_store", tm) (fn _ => is_0 imm8) 384 [(``0b11001w:word5``,20), (n,16), (t,12), 385 (``0b111110011111w:word12``,0)] 386 | ("Store_Exclusive", [n,d,t,imm8]) => 387 check ("encode_load_store", tm) (fn _ => is_0 imm8) 388 [(T,24), (T,23), (n,16), (d,12), (``0b11111001w:word8``,4), (t,0)] 389 | ("Load_Exclusive_Doubleword", [n,t,t2]) => 390 [(``0b11011w:word5``,20), (n,16), (t,12), 391 (``0b111110011111w:word12``,0)] 392 | ("Store_Exclusive_Doubleword", [n,d,t,t2]) => 393 [(``0b1101w:word4``,21), (n,16), (d,12), 394 (``0b11111001w:word8``,4), (t,0)] 395 | ("Load_Exclusive_Halfword", [n,t]) => 396 [(``0b11111w:word5``,20), (n,16), (t,12), 397 (``0b111110011111w:word12``,0)] 398 | ("Store_Exclusive_Halfword", [n,d,t]) => 399 [(PC,21), (n,16), (d,12), (``0b11111001w:word8``,4), (t,0)] 400 | ("Load_Exclusive_Byte", [n,t]) => 401 [(``0b11101w:word5``,20), (n,16), (t,12), 402 (``0b111110011111w:word12``,0)] 403 | ("Store_Exclusive_Byte", [n,d,t]) => 404 [(``0b1110w:word4``,21), (n,16), (d,12), 405 (``0b11111001w:word8``,4), (t,0)] 406 | ("Store_Return_State", [p,u,w,mode]) => 407 check_is_15 "encode_load_store: cond" cond 408 [(T,27), (p,24), (u,23), (T,22), (w,21), 409 (``0b110100000101w:word12``,8), (mode,0)] 410 | ("Return_From_Exception", [p,u,w,n]) => 411 check_is_15 "encode_load_store: cond" cond 412 [(T,27), (p,24), (u,23), (w,21), (T,20), (n,16), 413 (``0b1010w:word4``,8)] 414 | _ => raise ERR "encode_load_store" 415 ("cannot encode: " ^ term_to_string tm))); 416 417fun encode_miscellaneous (cond,tm) = term_list_to_num ((cond,28):: 418 (case dest_strip tm 419 of ("Hint", [h]) => 420 [(T,25), (T,24), (T,21), (PC,12)] @ hint h 421 | ("Breakpoint", [imm16]) => 422 check ("encode_miscellaneous", pairSyntax.mk_pair (cond,tm)) 423 (fn _ => is_AL cond) 424 [(T,24), (T,21), (imm16$(15,4),8), (``0b111w:word3``,4), 425 (imm16$(3,0),0)] 426 | ("Data_Memory_Barrier", [opt]) => 427 check_is_15 "encode_miscellaneous: cond" cond 428 [(``0b010101111111111100000101w:word24``,4), (opt,0)] 429 | ("Data_Synchronization_Barrier", [opt]) => 430 check_is_15 "encode_miscellaneous: cond" cond 431 [(``0b010101111111111100000100w:word24``,4), (opt,0)] 432 | ("Instruction_Synchronization_Barrier", [opt]) => 433 check_is_15 "encode_miscellaneous: cond" cond 434 [(``0b010101111111111100000110w:word24``,4), (opt,0)] 435 | ("Swap", [b,n,t,t2]) => 436 [(T,24), (b,22), (n,16), (t,12), (``0b1001w:word4``,4), (t2,0)] 437 | ("Preload_Data", [u,r,n,mode2]) => 438 check_is_15 "encode_miscellaneous: cond" cond 439 ([(T,26), (T,24), (u,23), (NOT r,22), (T,20), (n,16), (PC,12)] @ 440 encode_mode2 mode2) 441 | ("Preload_Instruction", [u,n,mode2]) => 442 check_is_15 "encode_miscellaneous: cond" cond 443 ([(T,26), (u,23), (T,22), (T,20), (n,16), (PC,12)] @ 444 encode_mode2 mode2) 445 | ("Supervisor_Call", [imm24]) => 446 [(PC,24), (imm24,0)] 447 | ("Secure_Monitor_Call", [imm4]) => 448 [(``0b000101100000000000000111w:word24``,4), (imm4,0)] 449 | ("Clear_Exclusive", []) => 450 check_is_15 "encode_miscellaneous: cond" cond 451 [(``0b0101011111111111000000011111w:word28``,0)] 452 | _ => raise ERR "encode_miscellaneous" 453 ("cannot encode: " ^ term_to_string tm))); 454 455fun encode_coprocessor (cond,tm) = term_list_to_num ((cond,28):: 456 (case dest_strip tm 457 of ("Coprocessor_Load", [p,u,d,w,n,cd,coproc,imm8]) => 458 [(T,27), (T,26), (p,24), (u,23), (d,22), (w,21), (T,20), 459 (n,16), (cd,12), (coproc,8), (imm8,0)] 460 | ("Coprocessor_Store", [p,u,d,w,n,cd,coproc,imm8]) => 461 [(T,27), (T,26), (p,24), (u,23), (d,22), (w,21), 462 (n,16), (cd,12), (coproc,8), (imm8,0)] 463 | ("Coprocessor_Data_Processing", [opc1,n,d,coproc,opc2,m]) => 464 [(``0b111w:word3``,25), (opc1,20), (n,16), (d,12), 465 (coproc, 8), (opc2,5), (m,0)] 466 | ("Coprocessor_Transfer", [opc1,mrc,n,t,coproc,opc2,m]) => 467 [(``0b111w:word3``,25), (opc1,21), (mrc,20), (n,16), (t,12), 468 (coproc, 8), (opc2,5), (T,4), (m,0)] 469 | ("Coprocessor_Transfer_Two", [mrrc,t2,t,coproc,opc,m]) => 470 [(``0b110001w:word6``,22), (mrrc,20), (t2,16), (t,12), 471 (coproc, 8), (opc,4), (m,0)] 472 | _ => raise ERR "encode_coprocessor" 473 ("cannot encode: " ^ term_to_string tm))); 474 475(* ------------------------------------------------------------------------- *) 476 477fun thumb_encode_branch (cond,tm) = 478let val checkbr = check ("thumb_encode_branch", tm) in 479 term_list_to_num 480 (case dest_strip tm 481 of ("Branch_Target", [imm24]) => 482 if is_var cond orelse is_AL cond then 483 let val high_bits = uint_of_word (imm24$(23,11)) in 484 checkbr (fn _ => high_bits = 0 orelse high_bits = 8191) 485 [(``0b111w:word3``,13), (imm24$(10,0),0)] 486 end 487 else 488 let val high_bits = uint_of_word (imm24$(23,8)) in 489 checkbr (fn _ => high_bits = 0 orelse high_bits = 65535) 490 [(``0b1101w:word4``,12), (cond,8), (imm24$(7,0),0)] 491 end 492 | ("Branch_Exchange", [m]) => 493 [(``0b10001110w:word8``,7), (m, 3)] 494 | ("Branch_Link_Exchange_Register", [m]) => 495 [(``0b10001111w:word8``,7), (m, 3)] 496 | ("Compare_Branch", [nzero,imm6,n]) => 497 checkbr (fn _ => width_okay 3 n) 498 [(``0b1011w:word4``,12), (nzero,11), (imm6$(5,5),9), (T,8), 499 (imm6$(4,0),3), (n,0)] 500 | _ => raise ERR "thumb_encode_branch" 501 ("cannot encode: " ^ term_to_string tm)) 502end; 503 504local 505 fun thumb_encode_register (opc,n,d,mode1) s = 506 let val (imm5,typ,m) = dest_Mode1_register mode1 in 507 check ("thumb_encode_register", mode1) 508 (fn _ => is_0 imm5 andalso is_0 typ andalso 509 (is_PC n orelse d ~~ n) andalso Lib.all (width_okay 3) [d,m]) 510 [(T,14), (opc,6), (m,3), (d,0)] 511 end 512 513 fun arm_expand_imm tm = 514 ``(((7 >< 0) ^tm) #>> (2 * (w2n ((11 -- 8) ^tm)))) : word32`` 515 |> eval 516 517 fun aligned tm = (uint_of_word tm) mod 4 = 0 518in 519 fun thumb_encode_data_processing tm = 520 let val checkdp = check ("thumb_encode_data_processing",tm) in 521 term_list_to_num 522 (case dest_strip tm 523 of ("Data_Processing", [opc,sflag,n,d,mode1]) => 524 (case uint_of_word opc 525 of 0 => thumb_encode_register (opc,n,d,mode1) "add" 526 | 1 => thumb_encode_register (opc,n,d,mode1) "eor" 527 | 2 => if is_Mode1_immediate mode1 then 528 let val imm = dest_Mode1_immediate mode1 in 529 if is_SP n then 530 let val imm32 = arm_expand_imm imm in 531 checkdp 532 (fn _ => is_SP d andalso width_okay 9 imm32 533 andalso aligned imm32) 534 [(``0b101100001w:9 word``,7), (imm32$(8,2),0)] 535 end 536 else if d ~~ n then 537 checkdp (fn _ => width_okay 3 d andalso 538 width_okay 8 imm) 539 [(``0b111w:word3``,11), (d,8), (imm,0)] 540 else 541 checkdp (fn _ => Lib.all (width_okay 3) [imm,n,d]) 542 [(``0b1111w:word4``,9), (imm,6), (n,3), (d,0)] 543 end 544 else 545 let val (imm5,typ,m) = dest_Mode1_register mode1 in 546 checkdp 547 (fn _ => is_0 imm5 andalso is_0 typ andalso 548 Lib.all (width_okay 3) [m,n,d]) 549 [(``0b1101w:word4``,9), (m,6), (n,3), (d,0)] 550 end 551 | 3 => let val imm = dest_Mode1_immediate mode1 in 552 checkdp 553 (fn _ => is_0 imm andalso Lib.all (width_okay 3) [n,d]) 554 [(``0b100001001w:9 word``,6), (n,3), (d,0)] 555 end 556 | 4 => if is_Mode1_immediate mode1 then 557 let val imm = dest_Mode1_immediate mode1 in 558 if is_SP n then 559 let val imm32 = arm_expand_imm imm in 560 if is_SP d then 561 checkdp 562 (fn _ => aligned imm32 andalso 563 width_okay 9 imm32) (* ADD(7) *) 564 [(``0b1011w:word4``,12), (imm32$(8,2),0)] 565 else 566 checkdp (* ADD(6) *) 567 (fn _ => aligned imm32 andalso width_okay 3 d 568 andalso width_okay 10 imm32) 569 [(``0b10101w:word5``,11), (d,8), 570 (imm32$(9,2),0)] 571 end 572 else if d ~~ n then 573 checkdp (* ADD(2) *) 574 (fn _ => width_okay 8 imm andalso width_okay 3 d) 575 [(``0b11w:word2``,12), (d,8), (imm,0)] 576 else 577 checkdp (* ADD(1) *) 578 (fn _ => Lib.all (width_okay 3) [imm,n,d]) 579 [(``0b111w:word3``,10), (imm,6), (n,3), (d,0)] 580 end 581 else 582 let val (imm5,typ,m) = dest_Mode1_register mode1 583 val _ = checkdp 584 (fn _ => is_0 imm5 andalso is_0 typ) [] 585 in 586 if is_F sflag andalso d ~~ n then (* ADD(4) *) 587 [(``0b10001w:word5``,10), (d$(3,3),7), (m,3), 588 (d$(2,0),0)] 589 else if is_F sflag andalso d ~~ m then (* ADD(4) *) 590 [(``0b10001w:word5``,10), (d$(3,3),7), (n,3), 591 (d$(2,0),0)] 592 else 593 checkdp (* ADD(3) *) 594 (fn _ => Lib.all (width_okay 3) [m,n,d]) 595 [(``0b11w:word2``,11), (m,6), (n,3), (d,0)] 596 end 597 | 5 => thumb_encode_register (opc,n,d,mode1) "adc" 598 | 6 => thumb_encode_register (opc,n,d,mode1) "sbc" 599 | 7 => raise ERR "thumb_encode_data_processing" "invalid opcode" 600 | 8 => thumb_encode_register (opc,d,n,mode1) "tst" 601 | 9 => raise ERR "thumb_encode_data_processing" "invalid opcode" 602 | 10 => if is_Mode1_immediate mode1 then 603 let val imm = dest_Mode1_immediate mode1 in 604 checkdp 605 (fn _ => width_okay 8 imm andalso width_okay 3 n) 606 [(``0b101w:word3``,11), (n,8), (imm,0)] 607 end 608 else 609 let val (imm5,typ,m) = dest_Mode1_register mode1 610 val _ = checkdp 611 (fn _ => is_0 imm5 andalso is_0 typ) [] 612 in 613 if Lib.all (width_okay 3) [n,m] then 614 [(``0b100001010w:9 word``,6), (m,3), (n,0)] 615 else 616 [(``0b1000101w:word7``,8), (n$(3,3),7), (m,3), 617 (n$(2,0),0)] 618 end 619 | 11 => thumb_encode_register (opc,d,n,mode1) "cmn" 620 | 12 => thumb_encode_register (opc,n,d,mode1) "orr" 621 | 13 => if is_Mode1_immediate mode1 then 622 let val imm = dest_Mode1_immediate mode1 in 623 checkdp 624 (fn _ => width_okay 8 imm andalso width_okay 3 d) 625 [(T,13), (d,8), (imm,0)] 626 end 627 else if is_Mode1_register mode1 then 628 let val (imm5,typ,m) = dest_Mode1_register mode1 in 629 if Lib.all (width_okay 3) [d,m] then 630 checkdp 631 (fn _ => not (Term.term_eq typ ``0b11w:word2``)) 632 [(typ,11), (imm5,6), (m,3), (d,0)] 633 else 634 checkdp (fn _ => is_0 imm5 andalso is_0 typ) 635 [(``0b100011w:word6``,9), (d$(3,3),7), (m,3), 636 (d$(2,0),0)] 637 end 638 else 639 let val (s,typ,m) = 640 dest_Mode1_register_shifted_register mode1 641 val sh = case uint_of_word typ 642 of 0 => ``0b010w:word3`` 643 | 1 => ``0b011w:word3`` 644 | 2 => ``0b100w:word3`` 645 | 3 => ``0b111w:word3`` 646 | _ => raise ERR 647 "thumb_encode_data_processing" 648 "not a valid mov (shift register)" 649 in 650 checkdp 651 (fn _ => d ~~ m andalso Lib.all (width_okay 3) [s,m]) 652 [(T,14), (sh,6), (s,3), (m,0)] 653 end 654 | 14 => thumb_encode_register (opc,n,d,mode1) "bic" 655 | 15 => thumb_encode_register (opc,n,d,mode1) "mvn" 656 | _ => raise ERR "thumb_encode_data_processing" "invalid opcode") 657 | ("Add_Sub", [a,n,d,imm12]) => 658 let val imm8 = imm12$(9,2) in 659 checkdp 660 (fn _ => aligned imm12 andalso is_T a andalso is_PC n andalso 661 width_okay 3 d) 662 [(``0b1010w:word3``,12), (d,8), (imm8,0)] (* ADD(5) *) 663 end 664 | ("Multiply", [acc,_,d,_,m,n]) => 665 checkdp (fn _ => is_F acc andalso d ~~ m andalso 666 Lib.all (width_okay 3) [m,n]) 667 [(``0b0100001101w:word10``,6), (n,3), (m,0)] 668 | ("Extend_Byte", [u,n,d,rot,m]) => 669 checkdp (fn _ => is_0 rot andalso is_PC n andalso 670 Lib.all (width_okay 3) [m,d]) 671 [(``0b10110010w:word8``,8), (u,7), (T,6), (m,3), (d,0)] 672 | ("Extend_Halfword", [u,n,d,rot,m]) => 673 checkdp (fn _ => is_0 rot andalso is_PC n andalso 674 Lib.all (width_okay 3) [m,d]) 675 [(``0b10110010w:word8``,8), (u,7), (m,3), (d,0)] 676 | ("Byte_Reverse_Word", [d,m]) => 677 checkdp (fn _ => Lib.all (width_okay 3) [m,d]) 678 [(``0b10111010w:word8``,8), (m,3), (d,0)] 679 | ("Byte_Reverse_Packed_Halfword", [d,m]) => 680 checkdp (fn _ => Lib.all (width_okay 3) [m,d]) 681 [(``0b10111010w:word8``,8), (T,6), (m,3), (d,0)] 682 | ("Byte_Reverse_Signed_Halfword", [d,m]) => 683 checkdp (fn _ => Lib.all (width_okay 3) [m,d]) 684 [(``0b1011101011w:word10``,6), (m,3), (d,0)] 685 | _ => raise ERR "thumb_encode_data_processing" 686 ("cannot encode: " ^ term_to_string tm)) 687 end 688end; 689 690fun thumb_encode_status_access tm = term_list_to_num 691 (case dest_strip tm 692 of ("Change_Processor_State", [imod,a,i,f,mode]) => 693 let val im = case uint_of_word imod 694 of 2 => T 695 | 3 => F 696 | _ => raise ERR "thumb_encode_status_access" 697 "invalid imod" 698 in 699 check ("encode_status_access", tm) (fn _ => optionSyntax.is_none mode) 700 [(``0b10110110011w:word11``,5), (im,4), (a,2), (i,1), (f,0)] 701 end 702 | ("Set_Endianness", [e]) => 703 [(``0b101101100101w:word12``,4), (e,3)] 704 | _ => raise ERR "thumb_encode_status_access" 705 ("cannot encode: " ^ term_to_string tm)); 706 707fun thumb_encode_load_store tm = term_list_to_num 708let val checkls = check ("thumb_encode_load_store",tm) in 709 (case dest_strip tm 710 of ("Load", [p,u,b,w,unpriv,n,t,mode2]) => 711 checkls (fn _ => is_F unpriv) 712 (if is_Mode2_immediate mode2 then 713 let val imm12 = dest_Mode2_immediate mode2 in 714 if is_PC n orelse is_SP n then 715 let val imm8 = imm12$(10,2) 716 val x = if is_PC n then ``0b01001w:word5`` 717 else ``0b10011w:word5`` 718 in 719 checkls 720 (fn _ => is_T p andalso is_T u andalso is_F b andalso 721 is_F w andalso width_okay 3 t andalso 722 is_0 (imm12$(1,0)) andalso width_okay 8 imm8) 723 [(x,11), (t,8), (imm8,0)] 724 end 725 else 726 let val imm5 = if is_T b then imm12 else imm12$(11,2) in 727 checkls 728 (fn _ => is_T p andalso is_T u andalso is_F w andalso 729 (is_T b orelse is_0 (imm12$(1,0))) andalso 730 width_okay 5 imm5 andalso 731 Lib.all (width_okay 3) [n,t]) 732 [(T,14), (T,13), (b,12), (T,11), (imm5,6), (n,3), (t,0)] 733 end 734 end 735 else 736 let val (imm5,typ,m) = dest_Mode2_register mode2 in 737 checkls 738 (fn _ => is_T p andalso is_T u andalso is_F w andalso 739 is_0 imm5 andalso is_0 typ andalso 740 Lib.all (width_okay 3) [m,n,t]) 741 [(``0b1011w:word4``,11), (b,10), (m,6), (n,3), (t,0)] 742 end) 743 | ("Store", [p,u,b,w,unpriv,n,t,mode2]) => 744 checkls (fn _ => is_F unpriv) 745 (if is_Mode2_immediate mode2 then 746 let val imm12 = dest_Mode2_immediate mode2 in 747 if is_SP n then 748 let val imm8 = imm12$(10,2) in 749 checkls 750 (fn _ => is_T p andalso is_T u andalso is_F b andalso 751 is_F w andalso width_okay 3 t andalso 752 is_0 (imm12$(1,0)) andalso width_okay 8 imm8) 753 [(``0b1001w:word4``,12), (t,8), (imm8,0)] 754 end 755 else 756 let val imm5 = if is_T b then imm12 else imm12$(11,2) in 757 checkls 758 (fn _ => is_T p andalso is_T u andalso is_F w andalso 759 (is_T b orelse is_0 (imm12$(1,0))) andalso 760 width_okay 5 imm5 andalso 761 Lib.all (width_okay 3) [n,t]) 762 [(T,14), (T,13), (b,12), (imm5,6), (n,3), (t,0)] 763 end 764 end 765 else 766 let val (imm5,typ,m) = dest_Mode2_register mode2 in 767 checkls 768 (fn _ => is_T p andalso is_T u andalso is_F w andalso 769 is_0 imm5 andalso is_0 typ andalso 770 Lib.all (width_okay 3) [m,n,t]) 771 [(``0b101w:word4``,12), (b,10), (m,6), (n,3), (t,0)] 772 end) 773 | ("Load_Halfword", [p,u,w,s,h,unpriv,n,t,mode3]) => 774 checkls (fn _ => is_F unpriv) 775 (if is_Mode3_immediate mode3 then 776 let val imm12 = dest_Mode3_immediate mode3 777 val imm5 = imm12$(11,1) 778 in 779 checkls 780 (fn _ => is_T p andalso is_T u andalso is_F w andalso 781 is_T h andalso is_F s andalso 782 is_0 (imm12$(0,0)) andalso width_okay 5 imm5 andalso 783 Lib.all (width_okay 3) [n,t]) 784 [(T,15), (T,11), (imm5,6), (n,3), (t,0)] 785 end 786 else 787 let val (imm2,m) = dest_Mode3_register mode3 in 788 checkls 789 (fn _ => is_T p andalso is_T u andalso is_F w andalso 790 (is_T s orelse is_T h) andalso 791 is_0 imm2 andalso Lib.all (width_okay 3) [m,n,t]) 792 [(``0b101w:word3``,12), (h,11), (s,10), (T,9), (m,6), (n,3), 793 (t,0)] 794 end) 795 | ("Store_Halfword", [p,u,w,unpriv,n,t,mode3]) => 796 checkls (fn _ => is_F unpriv) 797 (if is_Mode3_immediate mode3 then 798 let val imm12 = dest_Mode3_immediate mode3 799 val imm5 = imm12$(11,1) 800 in 801 checkls 802 (fn _ => is_T p andalso is_T u andalso is_F w andalso 803 is_0 (imm12$(0,0)) andalso width_okay 5 imm5 andalso 804 Lib.all (width_okay 3) [n,t]) 805 [(T,15), (imm5,6), (n,3), (t,0)] 806 end 807 else 808 let val (imm2,m) = dest_Mode3_register mode3 in 809 checkls 810 (fn _ => is_T p andalso is_T u andalso is_F w andalso 811 is_0 imm2 andalso Lib.all (width_okay 3) [m,n,t]) 812 [(``0b101001w:word6``,9), (m,6), (n,3), (t,0)] 813 end) 814 | ("Load_Multiple", [p,u,s,w,n,registers]) => 815 if is_SP n then 816 checkls 817 (fn _ => is_F p andalso is_T u andalso is_F s andalso 818 is_T w andalso is_0 (registers$(14,8))) 819 [(``0b101111w:word6``,10), (registers$(15,15),8), 820 (registers$(7,0),0)] 821 else 822 checkls 823 (fn _ => let val rn = uint_of_word n in 824 is_F p andalso is_T u andalso is_F s andalso 825 is_T w = is_0 (registers$(rn,rn)) andalso 826 is_0 (registers$(15,8)) andalso width_okay 3 n 827 end) 828 [(``0b11001w:word5``,11), (n,8), (registers$(7,0),0)] 829 | ("Store_Multiple", [p,u,s,w,n,registers]) => 830 if is_SP n then 831 checkls 832 (fn _ => is_T p andalso is_F u andalso is_F s andalso 833 is_T w andalso is_0 (registers$(13,8)) andalso 834 is_0 (registers$(15,15))) 835 [(``0b101101w:word6``,10), (registers$(14,14),8), 836 (registers$(7,0),0)] 837 else 838 checkls 839 (fn _ => is_F p andalso is_T u andalso is_F s andalso 840 is_T w andalso is_0 (registers$(15,8)) andalso 841 width_okay 3 n) 842 [(``0b11w:word2``,14), (n,8), (registers$(7,0),0)] 843 | _ => raise ERR "thumb_encode_load_store" 844 ("cannot encode: " ^ term_to_string tm)) 845end; 846 847fun thumb_encode_miscellaneous tm = 848let val checkmisc = check ("thumb_encode_miscellaneous",tm) in 849 term_list_to_num 850 (case dest_strip tm 851 of ("Hint", [h]) => 852 (``0b10111111w:word8``,8)::(thumb_hint h) 853 | ("Breakpoint", [imm16]) => 854 checkmisc (fn _ => is_0 (imm16$(15,8))) 855 [(``0b1011111w:word7``,9), (imm16$(7,0),0)] 856 | ("Supervisor_Call", [imm24]) => 857 checkmisc (fn _ => is_0 (imm24$(23,8))) 858 [(``0b11011111w:word8``,8), (imm24$(7,0),0)] 859 | ("If_Then", [firstcond,mask]) => 860 checkmisc (fn _ => not (is_PC firstcond orelse is_0 mask)) 861 [(``0b10111111w:word8``,8), (firstcond,4), (mask,0)] 862 | _ => raise ERR "thumb_encode_miscellaneous" 863 ("cannot encode: " ^ term_to_string tm)) 864end; 865 866(* ------------------------------------------------------------------------- *) 867 868fun thumb2_encode_branch (cond,tm) = 869let val checkb = check ("thumb2_encode_branch", tm) 870 val is_1 = Term.term_eq ``1w:word24`` 871 val is_1s = Term.term_eq ``0b1111w:word24`` 872in 873 term_list_to_num 874 (case dest_strip tm 875 of ("Branch_Target", [imm24]) => 876 if is_var cond orelse is_AL cond then 877 let val s = imm24$(23,23) 878 val S = is_1 s 879 val i1 = is_1 (imm24$(21,21)) 880 val i2 = is_1 (imm24$(22,22)) 881 val j1 = mk_bool (i1 = S) 882 val j2 = mk_bool (i2 = S) 883 in 884 [(PC,28), (s,26), (imm24$(20,11),16), (T,15), (j1,13), (T,12), 885 (j2,11), (imm24$(10,0),0)] 886 end 887 else 888 let val top_bits = imm24$(23,20) in 889 checkb (fn _ => is_1s top_bits orelse is_0 top_bits) 890 [(PC,28), (imm24$(19,19),26), (cond,22), (imm24$(16,11),16), 891 (T,15), (imm24$(17,17),13), (imm24$(18,18),11), 892 (imm24$(10,0),0)] 893 end 894 | ("Branch_Link_Exchange_Immediate", [h,toarm,imm24]) => 895 let val s = imm24$(22,22) 896 val S = is_1 s 897 val i1 = is_1 (imm24$(20,20)) 898 val i2 = is_1 (imm24$(21,21)) 899 val j1 = mk_bool (i1 = S) 900 val j2 = mk_bool (i2 = S) 901 in 902 checkb (fn _ => is_F toarm orelse is_F h) 903 [(PC,28), (s,26), (imm24$(19,10),16), (T,15), (T,14), (j1,13), 904 (NOT toarm,12), (j2,11), (imm24$(9,0),1), (h,0)] 905 end 906 | ("Table_Branch_Byte", [n,h,m]) => 907 [(``0b111010001101w:word12``,20), (n,16), (PC,12), (h,4), (m,0)] 908 | _ => raise ERR "encode_branch" ("cannot encode: " ^ term_to_string tm)) 909end; 910 911fun thumb2_opcode tm = 912 case uint_of_word tm 913 of 0 => ``0b0000w:word4`` (* AND *) 914 | 1 => ``0b0100w:word4`` (* EOR *) 915 | 2 => ``0b1101w:word4`` (* SUB *) 916 | 3 => ``0b1110w:word4`` (* RSB *) 917 | 4 => ``0b1000w:word4`` (* ADD *) 918 | 5 => ``0b1010w:word4`` (* ADC *) 919 | 6 => ``0b1011w:word4`` (* SBC *) 920 | 7 => raise ERR "thumb2_opcode" "rsc not available" 921 | 8 => ``0b0000w:word4`` (* TST *) 922 | 9 => ``0b0100w:word4`` (* TEQ *) 923 | 10 => ``0b1101w:word4`` (* CMP *) 924 | 11 => ``0b1000w:word4`` (* CMN *) 925 | 12 => ``0b0010w:word4`` (* ORR *) 926 | 13 => ``0b0010w:word4`` (* MOV *) 927 | 14 => ``0b0001w:word4`` (* BIC *) 928 | 15 => ``0b0011w:word4`` (* MVN/ORN *) 929 | _ => raise ERR "thumb2_opcode" "cannot encode" 930 931fun check_thumb2_dp (tm,rd,rn) = 932 case uint_of_word tm 933 of 8 => is_PC rd 934 | 9 => is_PC rd 935 | 10 => is_PC rd 936 | 11 => is_PC rd 937 | 13 => is_PC rn 938 | _ => true; 939 940fun thumb2_encode_data_processing tm = 941let val checkdp = check ("thumb2_encode_data_processing",tm) in 942 term_list_to_num ((``0b111w:word3``,29):: 943 (case dest_strip tm 944 of ("Data_Processing", [opc,s,n,d,mode1]) => 945 checkdp (fn _ => check_thumb2_dp (opc,d,n)) 946 (if is_Mode1_immediate mode1 then 947 let val imm12 = dest_Mode1_immediate mode1 in 948 if is_PC d andalso is_LR n andalso is_T s then 949 checkdp (fn _ => width_okay 8 imm12) 950 [(``0b100111101111010001111w:21 word``,8), (imm12$(7,0),0)] 951 else 952 let val (i,imm3,imm8) = (imm12$(11,11),imm12$(10,8),imm12$(7,0)) 953 in 954 [(T,28), (i,26), (thumb2_opcode opc,21), (s,20), (n,16), 955 (imm3,12), (d,8), (imm8,0)] 956 end 957 end 958 else if is_Mode1_register mode1 then 959 let val (imm5,typ,m) = dest_Mode1_register mode1 960 val (imm3,imm2) = (imm5$(4,2),imm5$(1,0)) 961 in 962 [(``0b101w:word3``,25), (thumb2_opcode opc,21), (s,20), (n,16), 963 (imm3,12), (d,8), (imm2,6), (typ,4), (m,0)] 964 end 965 else 966 let val (rs,typ,m) = dest_Mode1_register_shifted_register mode1 in 967 checkdp (fn _ => is_SP opc) 968 [(``0b1101w:word4``,25), (typ,21), (s,20), (m,16), 969 (PC,12), (d,8), (rs,0)] 970 end) 971 | ("Move_Halfword", [h,d,imm16]) => 972 [(T,28), (imm16$(11,11),26), (T,25), (h,23), (T,22), 973 (imm16$(15,12),16), (imm16$(10,8),12), (d,8), (imm16$(7,0),0)] 974 | ("Add_Sub", [a,n,d,imm12]) => 975 [(T,28), (imm12$(11,11),26), (T,25), (NOT a,23), (NOT a,21), (n,16), 976 (imm12$(10,8),12), (d,8), (imm12$(7,0),0)] 977 | ("Multiply", [acc,s,d,a,m,n]) => 978 checkdp (fn _ => is_F s) 979 [(``0b11011w:word5``,24), (n,16), (if is_T acc then a else PC,12), 980 (d,8), (m,0)] 981 | ("Multiply_Subtract", [d,a,m,n]) => 982 [(``0b11011w:word5``,24), (n,16), (a,12), (d,8), (T,4), (m,0)] 983 | ("Signed_Halfword_Multiply", [opc,M,N,d,a,m,n]) => 984 let val (opc1,opc2,acc,N') = 985 case uint_of_word opc 986 of 0 => (``0b01w:word2``,F,a,N) 987 | 1 => (``0b11w:word2``,F,if is_T N then PC else a,F) 988 | 2 => (``0b1100w:word4``,T,a,N) 989 | 3 => (``0b01w:word2``,F,PC,N) 990 | _ => raise ERR "thumb2_encode_data_processing" 991 "cannot encode" 992 in 993 [(``0b11011w:word5``,24), (opc1,20), (n,16), (acc,12), (d,8), 994 (opc2,7), (N',5), (M,4), (m,0)] 995 end 996 | ("Signed_Multiply_Dual", [d,a,m,M,N,n]) => 997 [(``0b11011w:word5``,24), (M,22), (NOT M,21), (n,16), (a,12), (d,8), 998 (N,4), (m,0)] 999 | ("Signed_Multiply_Long_Dual", [dhi,dlo,m,M,N,n]) => 1000 [(``0b1101111w:word7``,22), (M,20), (n,16), (dlo,12), (dhi,8), 1001 (``0b11w:word2``,6), (N,4), (m,0)] 1002 | ("Signed_Most_Significant_Multiply", [d,a,m,r,n]) => 1003 [(``0b110110101w:9 word``,20), (n,16), (a,12), (d,8), (r,4), (m,0)] 1004 | ("Signed_Most_Significant_Multiply_Subtract", [d,a,m,r,n]) => 1005 [(``0b11011011w:word8``,21), (n,16), (a,12), (d,8), (r,4), (m,0)] 1006 | ("Multiply_Long", [sgnd,a,s,dhi,dlo,m,n]) => 1007 checkdp (fn _ => is_F s) 1008 [(``0b110111w:word6``,23), (a,22), (NOT sgnd,21), (n,16), 1009 (dlo,12), (dhi,8), (m,0)] 1010 | ("Multiply_Accumulate_Accumulate", [dhi,dlo,m,n]) => 1011 [(``0b11011111w:word8``,21), (n,16), (dlo,12), (dhi,8), 1012 (``0b11w:word2``,5), (m,0)] 1013 | ("Saturate", [u,sat,d,imm5,sh,n]) => 1014 [(``0b10011w:word4``,24), (u,23), (sh,21), (n,16), 1015 (imm5$(4,2),12), (d,8), (imm5$(1,0),6), (sat,0)] 1016 | ("Saturate_16", [u,imm4,d,n]) => 1017 [(``0b10011w:word4``,24), (u,23), (T,21), (n,16), (d,8), (imm4,0)] 1018 | ("Saturating_Add_Subtract", [opc,n,d,m]) => 1019 let val opc1 = case uint_of_word opc 1020 of 1 => ``0b10w:word2`` 1021 | 2 => ``0b01w:word2`` 1022 | _ => opc 1023 in 1024 [(``0b110101w:word6``,23), (n,16), (PC,12), (d,8), (T,7), 1025 (opc1,4), (m,0)] 1026 end 1027 | ("Pack_Halfword", [n,d,imm5,t,m]) => 1028 [(``0b101011w:word6``,22), (n,16), (imm5$(4,2),12), (d,8), 1029 (imm5$(1,0),6), (t,5), (m,0)] 1030 | ("Extend_Byte", [u,n,d,rot,m]) => 1031 [(``0b1101001w:word7``,22), (u,20), (n,16), (PC,12), (d,8), 1032 (T,7), (rot,4), (m,0)] 1033 | ("Extend_Byte_16", [u,n,d,rot,m]) => 1034 [(``0b11010001w:word7``,21), (u,20), (n,16), (PC,12), (d,8), 1035 (T,7), (rot,4), (m,0)] 1036 | ("Extend_Halfword", [u,n,d,rot,m]) => 1037 [(``0b1101w:word4``,25), (u,20), (n,16), (PC,12), (d,8), 1038 (T,7), (rot,4), (m,0)] 1039 | ("Bit_Field_Clear_Insert", [msb,d,lsb,n]) => 1040 [(``0b10011011w:word7``,21), (n,16), (lsb$(4,2),12), (d,8), 1041 (lsb$(1,0),6), (msb,0)] 1042 | ("Count_Leading_Zeroes", [d,m]) => 1043 [(``0b110101011w:9 word``,20), (m,16), (PC,12), (d,8), (T,7), (m,0)] 1044 | ("Reverse_Bits", [d,m]) => 1045 [(``0b110101001w:9 word``,20), (m,16), (PC,12), (d,8), 1046 (T,7), (T,5), (m,0)] 1047 | ("Byte_Reverse_Word", [d,m]) => 1048 [(``0b110101001w:9 word``,20), (m,16), (PC,12), (d,8), (T,7), (m,0)] 1049 | ("Byte_Reverse_Packed_Halfword", [d,m]) => 1050 [(``0b110101001w:9 word``,20), (m,16), (PC,12), (d,8), 1051 (T,7), (T,4), (m,0)] 1052 | ("Byte_Reverse_Signed_Halfword", [d,m]) => 1053 [(``0b110101001w:9 word``,20), (m,16), (PC,12), (d,8), 1054 (``0b1011w:word4``,4), (m,0)] 1055 | ("Bit_Field_Extract", [u,w,d,lsb,n]) => 1056 [(``0b10011w:word5``,24), (u,23), (T,22), (n,16), (lsb$(4,2),12), 1057 (d,8), (lsb$(1,0),6), (w,0)] 1058 | ("Select_Bytes", [n,d,m]) => 1059 [(``0b11010101w:word8``,21), (n,16), (PC,12), (d,8), (T,7), (m,0)] 1060 | ("Unsigned_Sum_Absolute_Differences", [d,a,m,n]) => 1061 [(``0b110110111w:9 word``,20), (n,16), (a,12), (d,8), (m,0)] 1062 | ("Parallel_Add_Subtract", [u,opc,n,d,m]) => 1063 let val (opc1,opc2) = thumb_parallel_add_sub opc in 1064 [(``0b110101w:word6``,23), (opc2,20), (n,16), (PC,12), (d,8), 1065 (u,6), (opc1,4), (m,0)] 1066 end 1067 | ("Divide", [u,n,d,m]) => 1068 [(``0b110111w:word6``,23), (u,21), (T,20), (n,16), (PC,12), 1069 (d,8), (PC,4), (m,0)] 1070 | _ => raise ERR "thumb2_encode_data_processing" 1071 ("cannot encode: " ^ term_to_string tm))) 1072end; 1073 1074fun thumb2_encode_status_access tm = term_list_to_num 1075 (case dest_strip tm 1076 of ("Status_to_Register", [r,d]) => 1077 [(``0b11110011111w:word11``,21), (r,20), (PC,16), (T,15), (d,8)] 1078 | ("Register_to_Status", [r,mask,n]) => 1079 [(``0b111100111w:9 word``,23), (r,20), (n,16), (T,15), (mask,8)] 1080 | ("Change_Processor_State", [imod,a,i,f,mode]) => 1081 let val (M,m) = if optionSyntax.is_some mode then 1082 (T,optionSyntax.dest_some mode) 1083 else 1084 (F,mk_word4 0) 1085 in 1086 [(``0b11110011101011111w:17 word``,15), (imod,9), 1087 (M,8), (a,7), (i,6), (f,5), (m,0)] 1088 end 1089 | _ => raise ERR "thumb2_encode_status_access" 1090 ("cannot encode: " ^ term_to_string tm)); 1091 1092fun thumb2_encode_load_store tm = 1093let val checkls = check ("thumb2_encode_load_store",tm) in 1094 term_list_to_num ((``0b111w:word3``,29):: 1095 (case dest_strip tm 1096 of ("Load", [p,u,b,w,priv,n,t,mode2]) => 1097 if is_Mode2_immediate mode2 then 1098 let val imm12 = dest_Mode2_immediate mode2 in 1099 if is_T p andalso is_F w andalso (is_T u orelse is_PC n) andalso 1100 is_F priv 1101 then 1102 [(``0b11w:word2``,27), (u,23), (NOT b,22), (T,20), (n,16), 1103 (t,12), (imm12,0)] 1104 else 1105 checkls (fn _ => width_okay 8 imm12 andalso 1106 not (is_T b andalso is_PC t andalso is_T p andalso is_F u 1107 andalso is_F w)) 1108 [(``0b11w:word2``,27), (NOT b,22), (T,20), (n,16), (t,12), 1109 (T,11), (p,10), (u,9), (w,8), (imm12,0)] 1110 end 1111 else 1112 let val (imm5,typ,m) = dest_Mode2_register mode2 in 1113 checkls 1114 (fn _ => is_T p andalso is_T u andalso is_F w andalso 1115 is_0 typ andalso width_okay 2 imm5) 1116 [(``0b11w:word2``,27), (NOT b,22), (T,20), (n,16), (t,12), 1117 (imm5,4), (m,0)] 1118 end 1119 | ("Store", [p,u,b,w,priv,n,t,mode2]) => 1120 if is_Mode2_immediate mode2 then 1121 let val imm12 = dest_Mode2_immediate mode2 in 1122 if is_T p andalso is_F w andalso (is_T u orelse is_PC n) andalso 1123 is_F priv 1124 then 1125 [(``0b11w:word2``,27), (u,23), (NOT b,22), (n,16), 1126 (t,12), (imm12,0)] 1127 else 1128 checkls (fn _ => width_okay 8 imm12) 1129 [(``0b11w:word2``,27), (NOT b,22), (n,16), (t,12), 1130 (T,11), (p,10), (u,9), (w,8), (imm12,0)] 1131 end 1132 else 1133 let val (imm5,typ,m) = dest_Mode2_register mode2 in 1134 checkls 1135 (fn _ => is_T p andalso is_T u andalso is_F w andalso 1136 is_0 typ andalso width_okay 2 imm5) 1137 [(``0b11w:word2``,27), (NOT b,22), (n,16), (t,12), 1138 (imm5,4), (m,0)] 1139 end 1140 | ("Load_Halfword", [p,u,w,s,h,priv,n,t,mode3]) => 1141 if is_Mode3_immediate mode3 then 1142 let val imm12 = dest_Mode3_immediate mode3 in 1143 if is_T p andalso is_F w andalso (is_T u orelse is_PC n) andalso 1144 is_F priv 1145 then 1146 [(``0b11w:word2``,27), (s,24), (u,23), (h,21), (T,20), (n,16), 1147 (t,12), (imm12,0)] 1148 else 1149 checkls (fn _ => width_okay 8 imm12 andalso 1150 not (is_PC t andalso is_T p andalso is_F u andalso is_F w)) 1151 [(``0b11w:word2``,27), (s,24), (h,21), (T,20), (n,16), (t,12), 1152 (T,11), (p,10), (u,9), (w,8), (imm12,0)] 1153 end 1154 else 1155 let val (imm2,m) = dest_Mode3_register mode3 in 1156 checkls 1157 (fn _ => is_T p andalso is_T u andalso is_F w) 1158 [(``0b11w:word2``,27), (s,24), (h,21), (T,20), (n,16), (t,12), 1159 (imm2,4), (m,0)] 1160 end 1161 | ("Store_Halfword", [p,u,w,priv,n,t,mode3]) => 1162 if is_Mode3_immediate mode3 then 1163 let val imm12 = dest_Mode3_immediate mode3 in 1164 if is_T p andalso is_F w andalso (is_T u orelse is_PC n) andalso 1165 is_F priv 1166 then 1167 [(``0b11w:word2``,27), (u,23), (T,21), (n,16), 1168 (t,12), (imm12,0)] 1169 else 1170 checkls (fn _ => width_okay 8 imm12) 1171 [(``0b11w:word2``,27), (T,21), (n,16), (t,12), 1172 (T,11), (p,10), (u,9), (w,8), (imm12,0)] 1173 end 1174 else 1175 let val (imm2,m) = dest_Mode3_register mode3 in 1176 checkls 1177 (fn _ => is_T p andalso is_T u andalso is_F w) 1178 [(``0b11w:word2``,27), (T,21), (n,16), (t,12), (imm2,4), (m,0)] 1179 end 1180 | ("Load_Dual", [p,u,w,n,t,t2,mode3]) => 1181 let val imm12 = dest_Mode3_immediate mode3 1182 val imm8 = imm12$(9,2) 1183 in 1184 checkls (fn _ => width_okay 10 imm12 andalso is_0 (imm12$(1,0))) 1185 [(T,27), (p,24), (u,23), (T,22), (w,21), (T,20), (n,16), (t,12), 1186 (t2,8), (imm8,0)] 1187 end 1188 | ("Store_Dual", [p,u,w,n,t,t2,mode3]) => 1189 let val imm12 = dest_Mode3_immediate mode3 1190 val imm8 = imm12$(9,2) 1191 in 1192 checkls (fn _ => width_okay 8 imm12 andalso is_0 (imm12$(1,0))) 1193 [(T,27), (p,24), (u,23), (T,22), (w,21), (n,16), (t,12), 1194 (t2,8), (imm8,0)] 1195 end 1196 | ("Load_Multiple", [p,u,s,w,n,registers]) => 1197 checkls 1198 (fn _ => is_F s andalso p ~~ NOT u andalso is_0 (registers$(13,13))) 1199 [(T,27), (p,24), (u,23), (w,21), (T,20), (n,16), (registers,0)] 1200 | ("Store_Multiple", [p,u,s,w,n,registers]) => 1201 checkls 1202 (fn _ => is_F s andalso p ~~ NOT u andalso 1203 is_0 (registers$(13,13)) andalso is_0 (registers$(15,15))) 1204 [(T,27), (p,24), (u,23), (w,21), (n,16), (registers,0)] 1205 | ("Load_Exclusive", [n,t,imm8]) => 1206 [(``0b10000101w:word8``,20), (n,16), (t,12), (PC, 8), (imm8,0)] 1207 | ("Store_Exclusive", [n,d,t,imm8]) => 1208 [(``0b10000100w:word8``,20), (n,16), (t,12), (d, 8), (imm8,0)] 1209 | ("Load_Exclusive_Doubleword", [n,t,t2]) => 1210 [(``0b10001101w:word8``,20), (n,16), (t,12), (t2, 8), 1211 (``0b1111111w:word7``,0)] 1212 | ("Store_Exclusive_Doubleword", [n,d,t,t2]) => 1213 [(``0b10001100w:word8``,20), (n,16), (t,12), (t2, 8), 1214 (``0b111w:word3``,4), (d,0)] 1215 | ("Load_Exclusive_Halfword", [n,t]) => 1216 [(``0b10001101w:word8``,20), (n,16), (t,12), 1217 (``0b111101011111w:word12``,0)] 1218 | ("Store_Exclusive_Halfword", [n,d,t]) => 1219 [(``0b10001100w:word8``,20), (n,16), (t,12), 1220 (``0b11110101w:word8``,4), (d,0)] 1221 | ("Load_Exclusive_Byte", [n,t]) => 1222 [(``0b10001101w:word8``,20), (n,16), (t,12), 1223 (``0b111101001111w:word12``,0)] 1224 | ("Store_Exclusive_Byte", [n,d,t]) => 1225 [(``0b10001100w:word8``,20), (n,16), (t,12), 1226 (``0b11110100w:word8``,4), (d,0)] 1227 | ("Store_Return_State", [p,u,w,mode]) => 1228 checkls (fn _ => p ~~ NOT u) 1229 [(T,27), (u,24), (u,23), (w,21), (``0b110111w:word6``,14), (mode,0)] 1230 | ("Return_From_Exception", [p,u,w,n]) => 1231 checkls (fn _ => p ~~ NOT u) 1232 [(T,27), (u,24), (u,23), (w,22), (T,20), (n,16), 1233 (``0b11w:word2``,14)] 1234 | _ => raise ERR "thumb2_encode_load_store" 1235 ("cannot encode: " ^ term_to_string tm))) 1236end; 1237 1238fun thumb2_encode_miscellaneous tm = 1239let val checkmisc = check ("thumb2_encode_miscellaneous",tm) in 1240 term_list_to_num ((``0b111w:word3``,29):: 1241 (case dest_strip tm 1242 of ("Hint", [h]) => 1243 (``0b10011101011111w:14 word``,15)::(hint h) 1244 | ("Data_Memory_Barrier", [opt]) => 1245 [(``0b1001110111111100011110101w:25 word``,4), (opt,0)] 1246 | ("Data_Synchronization_Barrier", [opt]) => 1247 [(``0b1001110111111100011110100w:25 word``,4), (opt,0)] 1248 | ("Instruction_Synchronization_Barrier", [opt]) => 1249 [(``0b1001110111111100011110110w:25 word``,4), (opt,0)] 1250 | ("Preload_Data", [u,r,n,mode2]) => 1251 if is_Mode2_immediate mode2 then 1252 let val imm12 = dest_Mode2_immediate mode2 in 1253 if is_T u orelse is_PC n then 1254 [(``0b11w:word2``,27), (u,23), (r,21), (T,20), (n,16), 1255 (PC,12), (imm12,0)] 1256 else 1257 checkmisc (fn _ => width_okay 8 imm12) 1258 [(``0b11w:word2``,27), (r,21), (T,20), (n,16), 1259 (PC,12), (``0b11w:word2``,10), (imm12,0)] 1260 end 1261 else 1262 let val (imm5,typ,m) = dest_Mode2_register mode2 in 1263 checkmisc 1264 (fn _ => is_T u andalso is_0 typ andalso width_okay 2 imm5) 1265 [(``0b11w:word2``,27), (r,21), (T,20), (n,16), (PC,12), 1266 (imm5,4), (m,0)] 1267 end 1268 | ("Preload_Instruction", [u,n,mode2]) => 1269 if is_Mode2_immediate mode2 then 1270 let val imm12 = dest_Mode2_immediate mode2 in 1271 if is_T u orelse is_PC n then 1272 [(``0b11w:word2``,27), (T,24), (u,23), (T,20), (n,16), 1273 (PC,12), (imm12,0)] 1274 else 1275 checkmisc (fn _ => width_okay 8 imm12) 1276 [(``0b11w:word2``,27), (T,24), (T,20), (n,16), 1277 (PC,12), (``0b11w:word2``,10), (imm12,0)] 1278 end 1279 else 1280 let val (imm5,typ,m) = dest_Mode2_register mode2 in 1281 checkmisc 1282 (fn _ => is_T u andalso is_0 typ andalso width_okay 2 imm5) 1283 [(``0b11w:word2``,27), (T,24), (T,20), (n,16), (PC,12), 1284 (imm5,4), (m,0)] 1285 end 1286 | ("Secure_Monitor_Call", [imm4]) => 1287 [(``0b101111111w:9 word``,20), (imm4,16), (T,15)] 1288 | ("Enterx_Leavex", [l]) => 1289 [(``0b100111011111110001111000w:word24``,5), (l,4), (PC,0)] 1290 | ("Clear_Exclusive", []) => 1291 [(``0b10011101111111000111100101111w:29 word``,0)] 1292 | _ => raise ERR "thumb2_encode_miscellaneous" 1293 ("cannot encode: " ^ term_to_string tm))) 1294end; 1295 1296(* ------------------------------------------------------------------------- *) 1297 1298fun thumbee_encode_branch tm = 1299let val checkbr = check ("thumbee_encode_branch", tm) in 1300 term_list_to_num 1301 (case dest_strip tm 1302 of ("Check_Array", [n,m]) => 1303 [(``0b11001010w:word8``,8), (n$(3,3), 7), (m,3), (n$(2,0),0)] 1304 | ("Handler_Branch_Link", [l,h]) => 1305 [(``0b1100001w:word7``,9), (l,8), (h,0)] 1306 | ("Handler_Branch_Link_Parameter", [imm5,h]) => 1307 [(``0b110001w:word6``,10), (imm5,5), (h,0)] 1308 | ("Handler_Branch_Parameter", [imm3,h]) => 1309 [(``0b11w:word2``,14), (imm3,5), (h,0)] 1310 | _ => raise ERR "thumbee_encode_branch" 1311 ("cannot encode: " ^ term_to_string tm)) 1312end; 1313 1314fun thumbee_encode_load_store tm = term_list_to_num 1315let val checkls = check ("thumbee_encode_load_store",tm) in 1316 (case dest_strip tm 1317 of ("Load", [p,u,b,w,unpriv,n,t,mode2]) => 1318 checkls (fn _ => is_F unpriv) 1319 (if is_Mode2_immediate mode2 then 1320 let val imm12 = dest_Mode2_immediate mode2 in 1321 if is_R9 n then 1322 let val imm6 = imm12$(11,2) in 1323 checkls 1324 (fn _ => is_F b andalso is_T p andalso is_T u andalso 1325 is_F w andalso is_0 (imm12$(1,0)) andalso 1326 width_okay 6 imm6 andalso width_okay 3 t) 1327 [(``0b110011w:word6``,10), (imm6,3), (t,0)] 1328 end 1329 else if is_R10 n then 1330 let val imm5 = imm12$(11,2) in 1331 checkls 1332 (fn _ => is_F b andalso is_T p andalso is_T u andalso 1333 is_F w andalso is_0 (imm12$(1,0)) andalso 1334 width_okay 5 imm5 andalso width_okay 3 t) 1335 [(``0b11001011w:word8``,8), (imm5,3), (t,0)] 1336 end 1337 else 1338 let val imm3 = imm12$(11,2) in 1339 checkls 1340 (fn _ => is_F b andalso is_T p andalso is_F u andalso 1341 is_F w andalso is_0 (imm12$(1,0)) andalso 1342 width_okay 3 imm3 andalso 1343 Lib.all (width_okay 3) [n,t]) 1344 [(``0b11001w:word5``,11), (imm3,6), (n,3), (t,0)] 1345 end 1346 end 1347 else 1348 let val (imm5,typ,m) = dest_Mode2_register mode2 in 1349 checkls 1350 (fn _ => is_T p andalso is_T u andalso is_F w andalso 1351 is_F b andalso term_eq imm5 ``2w:word5`` andalso 1352 is_0 typ andalso Lib.all (width_okay 3) [m,n,t]) 1353 [(``0b1011w:word4``,11), (m,6), (n,3), (t,0)] 1354 end) 1355 | ("Store", [p,u,b,w,unpriv,n,t,mode2]) => 1356 checkls (fn _ => is_F unpriv) 1357 (if is_Mode2_immediate mode2 then 1358 let val imm12 = dest_Mode2_immediate mode2 1359 val imm6 = imm12$(11,2) 1360 in 1361 checkls 1362 (fn _ => is_F b andalso is_T p andalso is_T u andalso 1363 is_F w andalso is_0 (imm12$(1,0)) andalso 1364 width_okay 6 imm6 andalso is_R9 n andalso 1365 width_okay 3 t) 1366 [(``0b1100111w:word7``,9), (imm6,3), (t,0)] 1367 end 1368 else 1369 let val (imm5,typ,m) = dest_Mode2_register mode2 in 1370 checkls 1371 (fn _ => is_F b andalso is_T p andalso is_T u andalso 1372 is_F w andalso term_eq imm5 ``2w:word5`` andalso 1373 is_0 typ andalso Lib.all (width_okay 3) [m,n,t]) 1374 [(``0b101w:word4``,12), (m,6), (n,3), (t,0)] 1375 end) 1376 | ("Load_Halfword", [p,u,w,s,h,unpriv,n,t,mode3]) => 1377 checkls (fn _ => is_F unpriv andalso is_T p andalso is_T u andalso 1378 is_F w andalso is_T h andalso 1379 Lib.all (width_okay 3) [n,t] andalso 1380 Lib.can dest_Mode3_register mode3) 1381 (let val (imm2,m) = dest_Mode3_register mode3 in 1382 checkls 1383 (fn _ => term_eq imm2 ``1w:word2`` andalso width_okay 3 m) 1384 [(``0b1011w:word4``,11), (s,10), (T,9), (m,6), (n,3), (t,0)] 1385 end) 1386 | ("Store_Halfword", [p,u,w,unpriv,n,t,mode3]) => 1387 checkls (fn _ => is_F unpriv andalso is_T p andalso is_T u andalso 1388 is_F w andalso Lib.all (width_okay 3) [n,t] andalso 1389 Lib.can dest_Mode3_register mode3) 1390 (let val (imm2,m) = dest_Mode3_register mode3 in 1391 checkls 1392 (fn _ => term_eq imm2 ``1w:word2`` andalso width_okay 3 m) 1393 [(``0b101001w:word6``,9), (m,6), (n,3), (t,0)] 1394 end) 1395 | _ => raise ERR "thumbee_encode_load_store" 1396 ("cannot encode: " ^ term_to_string tm)) 1397end; 1398 1399(* ------------------------------------------------------------------------- *) 1400 1401fun encode_instruction (enc,cond,tm) = 1402 (case (fst (Term.dest_const enc), dest_strip tm) 1403 of ("Encoding_ARM",("Branch", [i])) => 1404 encode_branch (cond,i) 1405 | ("Encoding_ARM",("DataProcessing", [i])) => 1406 encode_data_processing (cond,i) 1407 | ("Encoding_ARM",("StatusAccess", [i])) => 1408 encode_status_access (cond,i) 1409 | ("Encoding_ARM",("LoadStore", [i])) => 1410 encode_load_store (cond,i) 1411 | ("Encoding_ARM",("Miscellaneous", [i])) => 1412 encode_miscellaneous (cond,i) 1413 | ("Encoding_ARM",("Coprocessor", [i])) => 1414 encode_coprocessor (cond,i) 1415 | ("Encoding_ARM",("Undefined", [])) => 1416 term_list_to_num [(cond,28), (``0x6000010w:word28``,0)] 1417 | ("Encoding_Thumb",("Branch", [i])) => 1418 thumb_encode_branch (cond,i) 1419 | ("Encoding_Thumb",("DataProcessing", [i])) => 1420 thumb_encode_data_processing i 1421 | ("Encoding_Thumb",("StatusAccess", [i])) => 1422 thumb_encode_status_access i 1423 | ("Encoding_Thumb",("LoadStore", [i])) => 1424 thumb_encode_load_store i 1425 | ("Encoding_Thumb",("Miscellaneous", [i])) => 1426 thumb_encode_miscellaneous i 1427 | ("Encoding_Thumb",("Undefined", [])) => 1428 term_list_to_num [(``0b1101111w:word7``,9)] 1429 | ("Encoding_Thumb2",("Branch", [i])) => 1430 thumb2_encode_branch (cond,i) 1431 | ("Encoding_Thumb2",("DataProcessing", [i])) => 1432 thumb2_encode_data_processing i 1433 | ("Encoding_Thumb2",("StatusAccess", [i])) => 1434 thumb2_encode_status_access i 1435 | ("Encoding_Thumb2",("LoadStore", [i])) => 1436 thumb2_encode_load_store i 1437 | ("Encoding_Thumb2",("Miscellaneous", [i])) => 1438 thumb2_encode_miscellaneous i 1439 | ("Encoding_Thumb2",("Coprocessor", [i])) => 1440 encode_coprocessor 1441 (mk_word4 (if is_var cond orelse is_PC cond then 15 else 14),i) 1442 | ("Encoding_Thumb2",("Undefined", [])) => 1443 term_list_to_num [(``0b1111011111110000101w:19 word``,13)] 1444 | ("Encoding_ThumbEE",("Branch", [i])) => 1445 thumbee_encode_branch i 1446 | ("Encoding_ThumbEE",("LoadStore", [i])) => 1447 thumbee_encode_load_store i 1448 | ("Encoding_ThumbEE",("Undefined", [])) => 1449 term_list_to_num [(``0b1101111w:word7``,9)] 1450 | _ => raise ERR "encode_instruction" ("cannot encode: " ^ 1451 term_to_string (pairSyntax.mk_pair (enc,tm)))) 1452 |> Arbnum.toHexString 1453 |> (if enc ~~ Encoding_Thumb_tm orelse enc ~~ Encoding_ThumbEE_tm then 1454 pad 4 1455 else if enc ~~ Encoding_ARM_tm then 1456 pad 8 1457 else 1458 (fn s => String.concat [String.substring (s, 0, 4), " ", 1459 String.substring (s, 4, 4)])); 1460 1461(* ------------------------------------------------------------------------- *) 1462 1463fun arm_encode (arm_parserLib.Ascii s) = encode_ascii s 1464 | arm_encode (arm_parserLib.Byte l) = encode_byte l 1465 | arm_encode (arm_parserLib.Short l) = encode_short l 1466 | arm_encode (arm_parserLib.Word l) = encode_word l 1467 | arm_encode (arm_parserLib.Instruction i) = encode_instruction i; 1468 1469val arm_assemble_parse = List.map ((I:Arbnum.num -> Arbnum.num) ## arm_encode); 1470 1471val arm_assemble_from_quote = 1472 (arm_assemble_parse ## I) o arm_parserLib.arm_parse_from_quote; 1473 1474val arm_assemble_from_string = 1475 (arm_assemble_parse ## I) o arm_parserLib.arm_parse_from_string; 1476 1477val arm_assemble_from_file = 1478 (arm_assemble_parse ## I) o arm_parserLib.arm_parse_from_file; 1479 1480fun arm_encode_from_string s = 1481 case Lib.total arm_assemble_from_string s 1482 of SOME ([(_,opc)],_) => opc 1483 | _ => raise ERR "arm_encode_from_string" "could not encode assembler"; 1484 1485(* 1486fun print_code_from s = 1487let open Arbnum 1488 val start = fromHexString s 1489 val lower = String.map Char.toLower 1490 val count = StringCvt.padLeft #" " 8 o pad 4 o lower o toHexString 1491in 1492 app (fn (n,i) => print (count (start + n) ^ " " ^ i ^ "\n")) 1493end; 1494*) 1495 1496end 1497