1(* ========================================================================= *) 2(* FILE : instructionSyntax.sml *) 3(* DESCRIPTION : Support for working with ARM instructions *) 4(* *) 5(* AUTHORS : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2006 *) 7(* ========================================================================= *) 8 9(* interactive use: 10 app load ["Nonstdio","wordsSyntax", "instructionTheory", 11 "assemblerML", "Data"]; 12*) 13 14structure instructionSyntax :> instructionSyntax = struct 15 16open HolKernel boolLib Parse bossLib; 17open Q wordsSyntax instructionTheory Data assemblerML; 18 19(* ------------------------------------------------------------------------- *) 20 21val ERR = mk_HOL_ERR "instructionSyntax" 22fun mk_bool b = if b then T else F; 23 24fun mk_word t n = mk_n2w(numLib.mk_numeral n, t); 25 26val mk_word3 = mk_word ``:3``; 27val mk_word4 = mk_word ``:4``; 28val mk_word5 = mk_word ``:5``; 29val mk_word8 = mk_word ``:8``; 30val mk_word12 = mk_word ``:12``; 31val mk_word16 = mk_word ``:16``; 32val mk_word24 = mk_word ``:24``; 33val mk_word32 = mk_word ``:32``; 34 35fun mk_register (NReg n) = (mk_word4 o Arbnum.fromInt o register2int) n 36 | mk_register (VReg x) = mk_var (x, ``:word4``); 37 38fun mk_condition cond = 39 case cond of 40 EQ => ``EQ`` | NE => ``NE`` | CS => ``CS`` | CC => ``CC`` 41 | MI => ``MI`` | PL => ``PL`` | VS => ``VS`` | VC => ``VC`` 42 | HI => ``HI`` | LS => ``LS`` | GE => ``GE`` | LT => ``LT`` 43 | GT => ``GT`` | LE => ``LE`` | AL => ``AL`` | NV => ``NV``; 44 45fun mk_opcode opc = 46 case opc of 47 AND => ``instruction$AND`` | EOR => ``instruction$EOR`` 48 | SUB => ``instruction$SUB`` | RSB => ``instruction$RSB`` 49 | ADD => ``instruction$ADD`` | ADC => ``instruction$ADC`` 50 | SBC => ``instruction$SBC`` | RSC => ``instruction$RSC`` 51 | TST => ``instruction$TST`` | TEQ => ``instruction$TEQ`` 52 | CMP => ``instruction$CMP`` | CMN => ``instruction$CMN`` 53 | ORR => ``instruction$ORR`` | MOV => ``instruction$MOV`` 54 | BIC => ``instruction$BIC`` | MVN => ``instruction$MVN``; 55 56fun mk_br (Instruction (x,c)) = 57 (case x of 58 Br y => 59 subst [``c:condition`` |-> mk_condition c, 60 ``offset:word24`` |-> mk_word24 (Arbnum.fromInt (#offset y))] 61 (if #L y then ``instruction$BL c offset`` 62 else ``instruction$B c offset``) 63 | _ => raise ERR "mk_br" "not a branch instruction") 64 | mk_br _ = raise ERR "mk_br" "not a branch instruction"; 65 66fun mk_swi_ex c = subst [``c:condition`` |-> mk_condition c] ``SWI c``; 67 68local 69 fun num2imm(x,n) = 70 let val x8 = Arbnum.mod(x,Arbnum.fromInt 256) in 71 if x8 = x then 72 (Arbnum.fromInt n, x8) 73 else 74 if n < 15 then 75 num2imm(rol32 x 2, n + 1) 76 else 77 raise ERR "num2immediate" "number cannot be represented as an immediate" 78 end 79in 80 fun num2immediate n = num2imm(n, 0) 81end; 82 83fun mk_shift r s = 84 subst [``r:word4`` |-> mk_register r] 85 (case s of 86 LSL => ``instruction$LSL r`` 87 | LSR => ``instruction$LSR r`` 88 | ASR => ``instruction$ASR r`` 89 | ROR => ``instruction$ROR r``); 90 91local 92 fun mk_dp_immediate x = 93 let val (n,m) = num2immediate x in 94 subst [``n:word4`` |-> mk_word4 n, 95 ``m:word8`` |-> mk_word8 m] ``Dp_immediate n m`` 96 end 97 98 fun mk_addr_mode1 x = 99 case x of 100 DpImmediate n => mk_dp_immediate n 101 | DpShiftImmediate i => 102 subst [``sh:shift`` |-> mk_shift (#Rm i) (#Sh i), 103 ``imm:word5`` |-> mk_word5 (Arbnum.fromInt (#Imm i))] 104 ``Dp_shift_immediate sh imm`` 105 | DpShiftRegister r => 106 subst [``sh:shift`` |-> mk_shift (#Rm r) (#Sh r), 107 ``rs:word4`` |-> mk_register (#Rs r)] 108 ``Dp_shift_register sh rs`` 109 val err = ERR "mk_data_proc" "not a data processing instruction" 110in 111 fun mk_data_proc (Instruction (x,c)) = 112 (case x of 113 Data_proc y => let val opc = #opc y in 114 if mem opc [TST,TEQ,CMP,CMN] then 115 subst [``f:condition -> word4 -> addr_mode1 -> arm_instruction`` |-> 116 mk_opcode opc, ``c:condition`` |-> mk_condition c, 117 ``rn:word4`` |-> mk_register (#Rn y), 118 ``op2:addr_mode1`` |-> mk_addr_mode1 (#op2 y)] 119 ``(f (c:condition) (rn:word4) 120 (op2:addr_mode1)):arm_instruction`` 121 else if opc = MOV orelse opc = MVN then 122 subst [``f:condition -> bool -> word4 -> addr_mode1 -> 123 arm_instruction`` |-> mk_opcode opc, 124 ``c:condition`` |-> mk_condition c, 125 ``s:bool`` |-> mk_bool (#S y), 126 ``rd:word4`` |-> mk_register (#Rd y), 127 ``op2:addr_mode1`` |-> mk_addr_mode1 (#op2 y)] 128 ``(f (c:condition) (s:bool) (rd:word4) 129 (op2:addr_mode1)):arm_instruction`` 130 else 131 subst [``f:condition -> bool -> word4 -> word4 -> addr_mode1 -> 132 arm_instruction`` |-> mk_opcode opc, 133 ``c:condition`` |-> mk_condition c, 134 ``s:bool`` |-> mk_bool (#S y), 135 ``rd:word4`` |-> mk_register (#Rd y), 136 ``rn:word4`` |-> mk_register (#Rn y), 137 ``op2:addr_mode1`` |-> mk_addr_mode1 (#op2 y)] 138 ``(f (c:condition) (s:bool) (rd:word4) (rn:word4) 139 (op2:addr_mode1)):arm_instruction`` 140 end 141 | _ => raise err) 142 | mk_data_proc _ = raise err 143end; 144 145fun mk_mla_mul (Instruction (x,c)) = 146 (case x of 147 Mla_mul y => 148 subst [``c:condition`` |-> mk_condition c, 149 ``s:bool`` |-> mk_bool (#S y), 150 ``rd:word4`` |-> mk_register (#Rd y), 151 ``rm:word4`` |-> mk_register (#Rm y), 152 ``rs:word4`` |-> mk_register (#Rs y), 153 ``rn:word4`` |-> mk_register (#Rn y)] 154 (case (#L y, #Signed y, #A y) of 155 (false,_,false) => ``MUL c s rd rm rs`` 156 | (false,_,true) => ``MLA c s rd rm rs rn`` 157 | (true,false,false) => ``UMULL c s rn rd rm rs`` 158 | (true,false,true) => ``UMLAL c s rn rd rm rs`` 159 | (true,true,false) => ``SMULL c s rn rd rm rs`` 160 | (true,true,true) => ``SMLAL c s rn rd rm rs``) 161 | _ => raise ERR "mk_mla_mul" "not a multiply instruction") 162 | mk_mla_mul _ = raise ERR "mk_mla_mul" "not a multiply instruction"; 163 164local 165 fun mk_addr_mode2 x = 166 case x of 167 DtImmediate n => 168 subst [``i:word12`` |-> mk_word12 (Arbnum.fromInt n)] ``Dt_immediate i`` 169 | DtShiftImmediate i => 170 subst [``sh:shift`` |-> mk_shift (#Rm i) (#Sh i), 171 ``imm:word5`` |-> mk_word5 (Arbnum.fromInt (#Imm i))] 172 ``Dt_shift_immediate sh imm`` 173 174 fun mk_options (Ldr_str y) = 175 subst [``p:bool`` |-> mk_bool (#P y), 176 ``u:bool`` |-> mk_bool (#U y), 177 ``w:bool`` |-> mk_bool (#W y)] 178 ``<| Pre := p; Up := u; Wb := w |>`` 179 | mk_options _ = raise ERR "mk_ldr_str" "not a load/store instruction" 180 val err = ERR "mk_ldr_str" "not a load/store instruction" 181in 182 fun mk_ldr_str (Instruction(x,c)) = 183 (case x of 184 Ldr_str y => 185 subst [``c:condition`` |-> mk_condition c, 186 ``b:bool`` |-> mk_bool (#B y), 187 ``opt:transfer_options`` |-> mk_options x, 188 ``rd:word4`` |-> mk_register (#Rd y), 189 ``rn:word4`` |-> mk_register (#Rn y), 190 ``offset:addr_mode2`` |-> mk_addr_mode2 (#offset y)] 191 (if #L y then 192 ``instruction$LDR c b opt rd rn offset`` 193 else 194 ``instruction$STR c b opt rd rn offset``) 195 | _ => raise err) 196 | mk_ldr_str _ = raise err 197end; 198 199local 200 fun mk_addr_mode3 x = 201 case x of 202 DthImmediate n => 203 subst [``i:word8`` |-> mk_word8 (Arbnum.fromInt n)] ``Dth_immediate i`` 204 | DthRegister r => 205 subst [``rm:word4`` |-> mk_register r] ``Dth_register rm`` 206 207 fun mk_options (Ldrh_strh y) = 208 subst [``p:bool`` |-> mk_bool (#P y), 209 ``u:bool`` |-> mk_bool (#U y), 210 ``w:bool`` |-> mk_bool (#W y)] 211 ``<| Pre := p; Up := u; Wb := w |>`` 212 | mk_options _ = raise ERR "mk_ldrh_strh" 213 "not a load/store (half) instruction" 214 val err = ERR "mk_ldrh_strh" "not a load/store (half) instruction" 215in 216 fun mk_ldrh_strh (Instruction(x,c)) = 217 (case x of 218 Ldrh_strh y => 219 subst [``c:condition`` |-> mk_condition c, 220 ``s:bool`` |-> mk_bool (#S y), 221 ``h:bool`` |-> mk_bool (#H y), 222 ``opt:transfer_options`` |-> mk_options x, 223 ``rd:word4`` |-> mk_register (#Rd y), 224 ``rn:word4`` |-> mk_register (#Rn y), 225 ``offset:addr_mode3`` |-> mk_addr_mode3 (#offset y)] 226 (if #L y then 227 subst [``s:bool`` |-> mk_bool (#S y)] 228 ``instruction$LDRH c s h opt rd rn offset`` 229 else 230 ``instruction$STRH c opt rd rn offset``) 231 | _ => raise err) 232 | mk_ldrh_strh _ = raise err 233end; 234 235local 236 fun mk_options (Ldm_stm y) = 237 subst [``p:bool`` |-> mk_bool (#P y), 238 ``u:bool`` |-> mk_bool (#U y), 239 ``w:bool`` |-> mk_bool (#W y)] 240 ``<| Pre := p; Up := u; Wb := w |>`` 241 | mk_options _ = raise ERR "mk_ldm_stm" "not a block transfer instruction" 242 val err = ERR "mk_ldm_stm" "not a block transfer instruction" 243in 244 fun mk_ldm_stm (Instruction(x,c)) = 245 (case x of 246 Ldm_stm y => 247 subst [``c:condition`` |-> mk_condition c, 248 ``s:bool`` |-> mk_bool (#S y), 249 ``opt:transfer_options`` |-> mk_options x, 250 ``rn:word4`` |-> mk_register (#Rn y), 251 ``list:word16`` |-> mk_word16 (Arbnum.fromInt (#list y))] 252 (if #L y then 253 ``instruction$LDM c s opt rn list`` 254 else 255 ``instruction$STM c s opt rn list``) 256 | _ => raise err) 257 | mk_ldm_stm _ = raise err 258end; 259 260fun mk_swp (Instruction(x,c)) = 261 (case x of 262 Swp y => 263 subst [``c:condition`` |-> mk_condition c, 264 ``b:bool`` |-> mk_bool (#B y), 265 ``rd:word4`` |-> mk_register (#Rd y), 266 ``rm:word4`` |-> mk_register (#Rm y), 267 ``rn:word4`` |-> mk_register (#Rn y)] 268 ``instruction$SWP c b rd rm rn`` 269 | _ => raise ERR "mk_swp" "not a swap instruction") 270 | mk_swp _ = raise ERR "mk_swp" "not a swap instruction"; 271 272fun mk_mrs (Instruction(x,c)) = 273 (case x of 274 Mrs y => 275 subst [``c:condition`` |-> mk_condition c, 276 ``r:bool`` |-> mk_bool (#R y), 277 ``rd:word4`` |-> mk_register (#Rd y)] 278 ``instruction$MRS c r rd`` 279 | _ => raise ERR "mk_mrs" "not an mrs instruction") 280 | mk_mrs _ = raise ERR "mk_mrs" "not an mrs instruction"; 281 282local 283 fun mk_msr_psr (Msr y) = 284 (case (#R y,#bit19 y,#bit16 y) of 285 (_,false,false) => 286 raise ERR "mk_msr" "either bit19 or bit16 must be set" 287 | (false,false,true) => ``CPSR_c`` 288 | (false,true,false) => ``CPSR_f`` 289 | (false,true,true) => ``CPSR_a`` 290 | (true,false,true) => ``SPSR_c`` 291 | (true,true,false) => ``SPSR_f`` 292 | (true,true,true) => ``SPSR_a``) 293 | mk_msr_psr _ = raise ERR "mk_msr" "not an msr instruction" 294 295 fun mk_msr_immediate x = 296 let val (n,m) = num2immediate x in 297 subst [``n:word4`` |-> mk_word4 n, 298 ``m:word8`` |-> mk_word8 m] ``Msr_immediate n m`` 299 end 300 301 fun mk_msr_mode x = 302 case x of 303 MsrImmediate n => mk_msr_immediate n 304 | MsrRegister r => subst [``r:word4`` |-> mk_register r] 305 ``Msr_register r`` 306 307 val err = ERR "mk_msr" "not an msr instruction" 308in 309 fun mk_msr (Instruction(x,c)) = 310 (case x of 311 Msr y => 312 subst [``c:condition`` |-> mk_condition c, 313 ``psrd:msr_psr`` |-> mk_msr_psr x, 314 ``op:msr_mode`` |-> mk_msr_mode (#Op y)] 315 ``instruction$MSR c psrd op`` 316 | _ => raise err) 317 | mk_msr _ = raise err 318end; 319 320fun mk_cdp (Instruction(x,c)) = 321 (case x of 322 Cdp y => 323 subst [``c:condition`` |-> mk_condition c, 324 ``cpn:word4`` |-> mk_word4 (Arbnum.fromInt (#CP y)), 325 ``cop1:word4`` |-> mk_word4 (Arbnum.fromInt (#Cop1 y)), 326 ``crd:word4`` |-> mk_register (#CRd y), 327 ``crn:word4`` |-> mk_register (#CRn y), 328 ``crm:word4`` |-> mk_register (#CRm y), 329 ``cop2:word3`` |-> mk_word3 (Arbnum.fromInt (#Cop2 y))] 330 ``instruction$CDP c cpn cop1 crd crn crm cop2`` 331 | _ => raise ERR "mk_cdp" "not a cdp instruction") 332 | mk_cdp _ = raise ERR "mk_cdp" "not a cdp instruction"; 333 334fun mk_mcr_mrc (Instruction(x,c)) = 335 (case x of 336 Mcr_mrc y => 337 subst [``c:condition`` |-> mk_condition c, 338 ``cpn:word4`` |-> mk_word4 (Arbnum.fromInt (#CP y)), 339 ``cop1:word3`` |-> mk_word3 (Arbnum.fromInt (#Cop1 y)), 340 ``rd:word4`` |-> mk_register (#Rd y), 341 ``crn:word4`` |-> mk_register (#CRn y), 342 ``crm:word4`` |-> mk_register (#CRm y), 343 ``cop2:word3`` |-> mk_word3 (Arbnum.fromInt (#Cop2 y))] 344 (if #L y then 345 ``instruction$MRC c cpn cop1 rd crn crm cop2`` 346 else 347 ``instruction$MCR c cpn cop1 rd crn crm cop2``) 348 | _ => raise ERR "mk_mcr_mrc" "not an mcr or mrc instruction") 349 | mk_mcr_mrc _ = raise ERR "mk_mcr_mrc" "not an mcr or mrc instruction"; 350 351local 352 fun mk_options (Ldc_stc y) = 353 subst [``p:bool`` |-> mk_bool (#P y), 354 ``u:bool`` |-> mk_bool (#U y), 355 ``w:bool`` |-> mk_bool (#W y)] 356 ``<| Pre := p; Up := u; Wb := w |>`` 357 | mk_options _ = raise ERR "mk_ldc_stc" "not an ldc or stc instruction" 358 val err = ERR "mk_ldc_stc" "not an ldc or stc instruction" 359in 360 fun mk_ldc_stc (Instruction(x,c)) = 361 (case x of 362 Ldc_stc y => 363 subst [``c:condition`` |-> mk_condition c, 364 ``n:bool`` |-> mk_bool (#N y), 365 ``opt:transfer_options`` |-> mk_options x, 366 ``cpn:word4`` |-> mk_word4 (Arbnum.fromInt (#CP y)), 367 ``crd:word4`` |-> mk_register (#CRd y), 368 ``rn:word4`` |-> mk_register (#Rn y), 369 ``offset:word8`` |-> mk_word8 (Arbnum.fromInt (#offset y))] 370 (if #L y then 371 ``instruction$LDC c n opt cpn crd rn offset`` 372 else 373 ``instruction$STC c n opt cpn crd rn offset``) 374 | _ => raise err) 375 | mk_ldc_stc _ = raise err 376end; 377 378fun mk_undef c = subst [``c:condition`` |-> mk_condition c] ``UND c``; 379 380(* ------------------------------------------------------------------------- *) 381 382fun arm_to_term (i as Instruction (x,c)) = 383 (case x of 384 Br y => mk_br i 385 | Swi_ex => mk_swi_ex c 386 | Data_proc y => mk_data_proc i 387 | Mla_mul y => mk_mla_mul i 388 | Ldr_str y => mk_ldr_str i 389 | Ldrh_strh y => mk_ldrh_strh i 390 | Ldm_stm y => mk_ldm_stm i 391 | Swp y => mk_swp i 392 | Mrs y => mk_mrs i 393 | Msr y => mk_msr i 394 | Cdp y => mk_cdp i 395 | Mcr_mrc y => mk_mcr_mrc i 396 | Ldc_stc y => mk_ldc_stc i 397 | Undef => mk_undef c) 398 | arm_to_term (Data n) = mk_word32 n; 399 400(* ------------------------------------------------------------------------- *) 401 402fun index_size t = let open Arbnum in 403 if t = ``:3`` then fromInt 8 else 404 if t = ``:4`` then fromInt 16 else 405 if t = ``:5`` then fromInt 32 else 406 if t = ``:8`` then fromInt 256 else 407 if t = ``:12`` then fromInt 4096 else 408 if t = ``:16`` then fromInt 65536 else 409 if t = ``:24`` then fromInt 16777216 else 410 if t = ``:32`` then fromString "4294967296" else 411 raise ERR "index_mod_size" "unknown word size" 412end; 413 414fun dest_word t = let val (n,typ) = dest_n2w t in 415 Arbnum.mod(numLib.dest_numeral n,index_size typ) end; 416 417val dest_wordi = Arbnum.toInt o dest_word; 418 419fun dest_register t = NReg (int2register (dest_wordi t)) 420 handle HOL_ERR e => 421 let val (x, t) = dest_var t in 422 if t = ``:word4`` then VReg x else Raise (HOL_ERR e) 423 end; 424 425fun dest_bool t = 426 if term_eq t T then true else 427 if term_eq t F then false else 428 raise ERR "dest_bool" "neither T nor F"; 429 430fun dest_condition t = let val eqt = term_eq t 431in 432 if eqt ``EQ`` then EQ else 433 if eqt ``NE`` then NE else 434 if eqt ``CS`` then CS else 435 if eqt ``CC`` then CC else 436 if eqt ``MI`` then MI else 437 if eqt ``PL`` then PL else 438 if eqt ``VS`` then VS else 439 if eqt ``VC`` then VC else 440 if eqt ``HI`` then HI else 441 if eqt ``LS`` then LS else 442 if eqt ``GE`` then GE else 443 if eqt ``LT`` then LT else 444 if eqt ``GT`` then GT else 445 if eqt ``LE`` then LE else 446 if eqt ``AL`` then AL else 447 if eqt ``NV`` then NV else 448 raise ERR "dest_condition" "not an instance of :condition" 449end; 450 451local 452 val err = ERR "dest_br" "not a variable-free branch instruction" 453in 454 fun dest_br t = 455 (case strip_comb t of 456 (i, [c, offset]) => let val l = term_eq i ``instruction$BL`` in 457 if l orelse term_eq i ``instruction$B`` then 458 Instruction(Br {L = l,offset = dest_wordi offset},dest_condition c) 459 else 460 raise err 461 end 462 | _ => raise err) 463 handle HOL_ERR _ => raise err 464end; 465 466local 467 val err = ERR "dest_swi_ex" "not a valid swi_ex instruction" 468in 469 fun dest_swi_ex t = 470 let val (i,c) = dest_comb t in 471 if term_eq i ``instruction$SWI`` then 472 Instruction(Swi_ex, dest_condition c) 473 else 474 raise err 475 end handle HOL_ERR _ => raise err 476end; 477 478local 479 val err = ERR "dest_undef" "not a valid undefined instruction" 480in 481 fun dest_undef t = 482 let val (i,c) = dest_comb t in 483 if term_eq i ``instruction$UND`` then 484 Instruction(Undef, dest_condition c) 485 else 486 raise err 487 end handle HOL_ERR _ => raise err 488end; 489 490fun dest_opc1 t = let val eqt = term_eq t 491in 492 if eqt ``instruction$AND`` then AND else 493 if eqt ``instruction$EOR`` then EOR else 494 if eqt ``instruction$SUB`` then SUB else 495 if eqt ``instruction$RSB`` then RSB else 496 if eqt ``instruction$ADD`` then ADD else 497 if eqt ``instruction$ADC`` then ADC else 498 if eqt ``instruction$SBC`` then SBC else 499 if eqt ``instruction$RSC`` then RSC else 500 if eqt ``instruction$ORR`` then ORR else 501 if eqt ``instruction$BIC`` then BIC else raise ERR "dest_opc1" 502 "term is not: AND, EOR, SUB, RSB, ADD, ADC, SBC, RSC, ORR or BIC" 503end; 504 505fun dest_opc2 t = let val eqt = term_eq t 506in 507 if eqt ``instruction$TST`` then TST else 508 if eqt ``instruction$TEQ`` then TEQ else 509 if eqt ``instruction$CMP`` then CMP else 510 if eqt ``instruction$CMN`` then CMN else 511 raise ERR "dest_opc2" "term is not: TST, TEQ, CMP or CMN" 512end; 513 514fun dest_opc3 t = 515 if term_eq t ``instruction$MOV`` then MOV else 516 if term_eq t ``instruction$MVN`` then MVN else 517 raise ERR "dest_opc3" "term is not: MOV or MVN"; 518 519fun dest_shift t = 520let val (s,r) = dest_comb t in 521 if term_eq s ``instruction$LSL`` then (LSL, dest_register r) else 522 if term_eq s ``instruction$LSR`` then (LSR, dest_register r) else 523 if term_eq s ``instruction$ASR`` then (ASR, dest_register r) else 524 if term_eq s ``instruction$ROR`` then (ROR, dest_register r) else 525 raise ERR "dest_shift" "not a valid term of type :shift" 526end; 527 528local 529 val err = ERR "dest_addr_mode1" "not a valid instance of :addr_mode1" 530in 531 fun dest_addr_mode1 t = 532 case strip_comb t of 533 (m, [x, y]) => 534 if term_eq m ``Dp_immediate`` then 535 DpImmediate (mk_immediate (dest_wordi x) (dest_word y)) 536 else let val (s,rm) = dest_shift x in 537 if term_eq m ``Dp_shift_immediate`` then 538 DpShiftImmediate {Imm = dest_wordi y, Sh = s, Rm = rm} 539 else if term_eq m ``Dp_shift_register`` then 540 DpShiftRegister {Rs = dest_register y, Sh = s, Rm = rm} 541 else raise err 542 end 543 | _ => raise err 544end; 545 546local 547 val err = ERR "dest_data_proc" "not a variable-free data_proc instruction" 548in 549 fun dest_data_proc t = 550 (case strip_comb t of 551 (opc, [c,s,rd,rn,op2]) => 552 Instruction(Data_proc {opc = dest_opc1 opc, S = dest_bool s, 553 Rd = dest_register rd, Rn = dest_register rn, 554 op2 = dest_addr_mode1 op2},dest_condition c) 555 | (opc, [c,rn,op2]) => 556 Instruction(Data_proc {opc = dest_opc2 opc, S = true, 557 Rd = NReg R0, Rn = dest_register rn, 558 op2 = dest_addr_mode1 op2},dest_condition c) 559 | (opc, [c,s,rd,op2]) => 560 Instruction(Data_proc {opc = dest_opc3 opc, S = dest_bool s, 561 Rd = dest_register rd, Rn = NReg R0, 562 op2 = dest_addr_mode1 op2},dest_condition c) 563 | _ => raise err) 564 handle HOL_ERR _ => raise err 565end; 566 567local 568 val err = ERR "dest_mla_mul" "not a variable-free multiply instruction" 569in 570 fun dest_mla_mul t = 571 (case strip_comb t of 572 (i, [c,s,rd,rm,rs]) => 573 if term_eq i ``instruction$MUL`` then 574 Instruction(Mla_mul {L = false, Signed = false, 575 A = false, S = dest_bool s, 576 Rd = dest_register rd, Rm = dest_register rm, 577 Rs = dest_register rs, Rn = NReg R0},dest_condition c) 578 else 579 raise err 580 | (i, [c,s,rd,rm,rs,rn]) => 581 if term_eq i ``instruction$MLA`` then 582 Instruction(Mla_mul {L = false, Signed = false, 583 A = true, S = dest_bool s, 584 Rd = dest_register rd, Rm = dest_register rm, 585 Rs = dest_register rs, Rn = dest_register rn},dest_condition c) 586 else if term_eq i ``instruction$UMULL`` then 587 Instruction(Mla_mul {L = true, Signed = false, 588 A = false, S = dest_bool s, 589 Rd = dest_register rm, Rm = dest_register rs, 590 Rs = dest_register rn, Rn = dest_register rd},dest_condition c) 591 else if term_eq i ``instruction$UMLAL`` then 592 Instruction(Mla_mul {L = true, Signed = false, 593 A = true, S = dest_bool s, 594 Rd = dest_register rm, Rm = dest_register rs, 595 Rs = dest_register rn, Rn = dest_register rd},dest_condition c) 596 else if term_eq i ``instruction$SMULL`` then 597 Instruction(Mla_mul {L = true, Signed = true, 598 A = false, S = dest_bool s, 599 Rd = dest_register rm, Rm = dest_register rs, 600 Rs = dest_register rn, Rn = dest_register rd},dest_condition c) 601 else if term_eq i ``instruction$SMLAL`` then 602 Instruction(Mla_mul {L = true, Signed = true, 603 A = true, S = dest_bool s, 604 Rd = dest_register rm, Rm = dest_register rs, 605 Rs = dest_register rn, Rn = dest_register rd},dest_condition c) 606 else 607 raise err 608 | _ => raise err) 609 handle HOL_ERR _ => raise err 610end; 611 612fun dest_options t = 613 case snd (TypeBase.dest_record t) of 614 [("Pre", p), ("Up", u), ("Wb", w)] => 615 (dest_bool p, dest_bool u, dest_bool w) 616 | _ => raise ERR "dest_options" "not an instance of type :transfer_options"; 617 618local 619 val err = ERR "dest_addr_mode2" "not a valid instance of :addr_mode2" 620in 621 fun dest_addr_mode2 t = 622 (case strip_comb t of 623 (m, [n]) => 624 if term_eq m ``Dt_immediate`` then 625 DtImmediate (dest_wordi n) 626 else 627 raise err 628 | (m, [sh, i]) => 629 if term_eq m ``Dt_shift_immediate`` then 630 let val (s,rm) = dest_shift sh in 631 DtShiftImmediate {Imm = dest_wordi i, Sh = s, Rm = rm} 632 end 633 else 634 raise err 635 | _ => raise err) 636 handle HOL_ERR _ => raise err 637end; 638 639local 640 val err = ERR "dest_ldr_str" "not a variable-free load/store instruction" 641in 642 fun dest_ldr_str t = 643 (case strip_comb t of 644 (i, [c,b,opt,rd,rn,offset]) => 645 let val l = term_eq i ``instruction$LDR`` 646 val (p,u,w) = dest_options opt 647 in 648 if l orelse term_eq i ``instruction$STR`` then 649 Instruction(Ldr_str {L = l,offset = dest_addr_mode2 offset, 650 Rd = dest_register rd, Rn = dest_register rn, 651 P = p, U = u, B = dest_bool b, W = w},dest_condition c) 652 else 653 raise err 654 end 655 | _ => raise err) 656 handle HOL_ERR _ => raise err 657end; 658 659local 660 val err = ERR "dest_addr_mode3" "not a valid instance of :addr_mode3" 661in 662 fun dest_addr_mode3 t = 663 (case strip_comb t of 664 (m, [n]) => 665 if term_eq m ``Dth_immediate`` then 666 DthImmediate (dest_wordi n) 667 else if term_eq m ``Dth_register`` then 668 DthRegister (dest_register n) 669 else 670 raise err 671 | _ => raise err) 672 handle HOL_ERR _ => raise err 673end; 674 675local 676 val err = ERR "dest_ldr_str" "not a variable-free load/store instruction" 677in 678 fun dest_ldrh_strh t = 679 (case strip_comb t of 680 (i, [c,s,h,opt,rd,rn,offset]) => 681 let val (p,u,w) = dest_options opt in 682 if term_eq i ``instruction$LDRH`` then 683 Instruction(Ldrh_strh {L = true,offset = dest_addr_mode3 offset, 684 Rd = dest_register rd, Rn = dest_register rn, P = p, U = u, 685 W = w, S = dest_bool s, H = dest_bool h},dest_condition c) 686 else 687 raise err 688 end 689 | (i, [c,opt,rd,rn,offset]) => 690 let val (p,u,w) = dest_options opt in 691 if term_eq i ``instruction$STRH`` then 692 Instruction(Ldrh_strh {L = false,offset = dest_addr_mode3 offset, 693 Rd = dest_register rd, Rn = dest_register rn, 694 P = p, U = u, W = w, S = false, H = true},dest_condition c) 695 else 696 raise err 697 end 698 | _ => raise err) 699 handle HOL_ERR _ => raise err 700end; 701 702local 703 val err = ERR "dest_ldm_stm" "not a variable-free block transfer instruction" 704in 705 fun dest_ldm_stm t = 706 (case strip_comb t of 707 (i, [c,s,opt,rn,list]) => 708 let val l = term_eq i ``instruction$LDM`` 709 val (p,u,w) = dest_options opt 710 in 711 if l orelse term_eq i ``instruction$STM`` then 712 Instruction(Ldm_stm {L = l,list = dest_wordi list, 713 Rn = dest_register rn, P = p, U = u, S = dest_bool s, W = w}, 714 dest_condition c) 715 else 716 raise err 717 end 718 | _ => raise err) 719 handle HOL_ERR _ => raise err 720end; 721 722local 723 val err = ERR "dest_swp" "not a variable-free swap instruction" 724in 725 fun dest_swp t = 726 (case strip_comb t of 727 (i, [c,b,rd,rm,rn]) => 728 if term_eq i ``instruction$SWP`` then 729 Instruction(Swp {B = dest_bool b,Rd = dest_register rd, 730 Rm = dest_register rm, Rn = dest_register rn},dest_condition c) 731 else 732 raise err 733 | _ => raise err) 734 handle HOL_ERR _ => raise err 735end; 736 737local 738 val err = ERR "dest_mrs" "not a variable-free mrs instruction" 739in 740 fun dest_mrs t = 741 (case strip_comb t of 742 (i, [c,r,rd]) => 743 if term_eq i ``instruction$MRS`` then 744 Instruction(Mrs {R = dest_bool r,Rd = dest_register rd}, 745 dest_condition c) 746 else 747 raise err 748 | _ => raise err) 749 handle HOL_ERR _ => raise err 750end; 751 752fun dest_msr_psr t = let val eqt = term_eq t 753in 754 if eqt ``CPSR_c`` then (false,false,true) else 755 if eqt ``CPSR_f`` then (false,true,false) else 756 if eqt ``CPSR_a`` then (false,true,true) else 757 if eqt ``SPSR_c`` then (true,false,true) else 758 if eqt ``SPSR_f`` then (true,true,false) else 759 if eqt ``SPSR_a`` then (true,true,true) else 760 raise ERR "dest_msr_psr" "not a valid instance of :msr_psr" 761end; 762 763local 764 val err = ERR "dest_addr_mode1" "not a valid instance of :msr_mode" 765in 766 fun dest_msr_mode t = 767 (case strip_comb t of 768 (m, [x, y]) => 769 if term_eq m ``Msr_immediate`` then 770 MsrImmediate (mk_immediate (dest_wordi x) (dest_word y)) 771 else 772 raise err 773 | (m, [x]) => 774 if term_eq m ``Msr_register`` then 775 MsrRegister (dest_register x) 776 else 777 raise err 778 | _ => raise err) handle HOL_ERR _ => raise err 779end; 780 781local 782 val err = ERR "dest_msr" "not a variable-free mrs instruction" 783in 784 fun dest_msr t = 785 (case strip_comb t of 786 (i, [c,psrd,opnd]) => 787 if term_eq i ``instruction$MSR`` then 788 let val (r,b19,b16) = dest_msr_psr psrd in 789 Instruction(Msr {R = r, bit19 = b19, bit16 = b16, 790 Op = dest_msr_mode opnd},dest_condition c) 791 end 792 else 793 raise err 794 | _ => raise err) 795 handle HOL_ERR _ => raise err 796end; 797 798local 799 val err = ERR "dest_cdp" "not a variable-free cdp instruction" 800in 801 fun dest_cdp t = 802 (case strip_comb t of 803 (i, [c,cpn,cop1,crd,crn,crm,cop2]) => 804 if term_eq i ``instruction$CDP`` then 805 Instruction(Cdp {CP = dest_wordi cpn, CRd = dest_register crd, 806 CRn = dest_register crn, CRm = dest_register crm, 807 Cop1 = dest_wordi cop1, Cop2 = dest_wordi cop2},dest_condition c) 808 else 809 raise err 810 | _ => raise err) 811 handle HOL_ERR _ => raise err 812end; 813 814local 815 val err = ERR "dest_ldc_stc" "not a variable-free ldc/stc instruction" 816in 817 fun dest_ldc_stc t = 818 (case strip_comb t of 819 (i, [c,n,opt,cpn,crd,rn,offset]) => 820 let val l = term_eq i ``instruction$LDC`` 821 val (p,u,w) = dest_options opt 822 in 823 if l orelse term_eq i ``instruction$STC`` then 824 Instruction(Ldc_stc {CP = dest_wordi cpn, CRd = dest_register crd, 825 L = l, P = p, U = u, N = dest_bool n, W = w, 826 Rn = dest_register rn, offset = dest_wordi offset}, 827 dest_condition c) 828 else 829 raise err 830 end 831 | _ => raise err) 832 handle HOL_ERR _ => raise err 833end; 834 835local 836 val err = ERR "dest_mcr_mrc" "not a variable-free mcr/mrc instruction" 837in 838 fun dest_mcr_mrc t = 839 (case strip_comb t of 840 (i, [c,cpn,cop1,rd,crn,crm,cop2]) => 841 let val l = term_eq i ``instruction$MCR`` in 842 if l orelse term_eq i ``instruction$MRC`` then 843 Instruction(Mcr_mrc {CP = dest_wordi cpn, L = l, 844 CRn = dest_register crn, CRm = dest_register crm, 845 Rd = dest_register rd, Cop1 = dest_wordi cop1, 846 Cop2 = dest_wordi cop2},dest_condition c) 847 else 848 raise err 849 end 850 | _ => raise err) 851 handle HOL_ERR _ => raise err 852end; 853 854(* ------------------------------------------------------------------------- *) 855 856fun term_to_arm t = 857 if type_of t = ``:word32`` then 858 Data (dest_word t) 859 else let val opc = fst (strip_comb t) 860 val eqt = term_eq opc 861 in 862 if eqt ``instruction$SWI`` then 863 dest_swi_ex t 864 else if eqt ``instruction$B`` orelse eqt ``instruction$BL`` then 865 dest_br t 866 else if eqt ``instruction$MUL`` orelse eqt ``instruction$MLA`` orelse 867 eqt ``instruction$UMULL`` orelse eqt ``instruction$UMLAL`` orelse 868 eqt ``instruction$SMULL`` orelse eqt ``instruction$SMLAL`` then 869 dest_mla_mul t 870 else if eqt ``instruction$LDRH`` orelse eqt ``instruction$STRH`` then 871 dest_ldrh_strh t 872 else if eqt ``instruction$LDR`` orelse eqt ``instruction$STR`` then 873 dest_ldr_str t 874 else if eqt ``instruction$LDM`` orelse eqt ``instruction$STM`` then 875 dest_ldm_stm t 876 else if eqt ``instruction$SWP`` then 877 dest_swp t 878 else if eqt ``instruction$MRS`` then 879 dest_mrs t 880 else if eqt ``instruction$MSR`` then 881 dest_msr t 882 else if eqt ``instruction$CDP`` then 883 dest_cdp t 884 else if eqt ``instruction$LDC`` orelse eqt ``instruction$STC`` then 885 dest_ldc_stc t 886 else if eqt ``instruction$MCR`` orelse eqt ``instruction$MRC`` then 887 dest_mcr_mrc t 888 else if eqt ``instruction$UND`` then 889 dest_undef t 890 else 891 dest_data_proc t 892 end 893handle HOL_ERR _ => 894 raise ERR "term_to_arm" "not a variable-free ARM instruction"; 895 896(* ------------------------------------------------------------------------- *) 897 898val encode_instruction = arm_to_num o term_to_arm; 899val decode_instruction = arm_to_term o num_to_arm; 900val decode_instruction_dec = decode_instruction o Arbnum.fromString; 901val decode_instruction_hex = decode_instruction o Arbnum.fromHexString; 902 903val mk_instruction = arm_to_term o string_to_arm; 904fun dest_instruction i t = arm_to_string i false (term_to_arm t); 905 906(* ------------------------------------------------------------------------- *) 907end; 908