1structure arm_parserLib :> arm_parserLib = 2struct 3 4(* interactive use: 5 app load ["armSyntax", "arm_astSyntax", "integer_wordSyntax", 6 "wordsLib", "intLib", "intSyntax"]; 7*) 8 9open HolKernel boolLib bossLib intLib integer_wordTheory; 10open armSyntax arm_astSyntax; 11 12(* ------------------------------------------------------------------------- *) 13 14val _ = numLib.prefer_num(); 15val _ = wordsLib.prefer_word(); 16 17val ERR = Feedback.mk_HOL_ERR "arm_parserLib"; 18 19local 20 val tm_g = Parse.term_grammar () 21 val ty_g = Parse.type_grammar () 22in 23 val term_to_string = 24 PP.pp_to_string 70 25 (Parse.mlower o term_pp.pp_term tm_g ty_g PPBackEnd.raw_terminal) 26end 27 28fun quote_to_string l = 29let fun recurse [] s = s 30 | recurse (QUOTE q :: t) s = recurse t (s ^ q) 31 | recurse (ANTIQUOTE q :: t) s = recurse t (s ^ q) 32in 33 recurse l "" 34end; 35 36(* ------------------------------------------------------------------------- *) 37 38datatype instruction_mnemonic 39 = ADC | ADD | ADDW | ADR | AND | ASR 40 | B | BFC | BFI | BIC | BKPT | BL | BLX | BX 41 | CBZ | CBNZ | CDP | CDP2 | CHKA | CLREX | CLZ | CMN 42 | CMP | CPS | CPSIE | CPSID 43 | DBG | DMB | DSB 44 | ENTERX | EOR 45 | HB | HBL | HBLP | HBP 46 | ISB | IT 47 | LDC | LDCL | LDC2 | LDC2L | LDMIA | LDMDA | LDMDB | LDMIB 48 | LDR | LDRB | LDRBT | LDRD | LDREX | LDREXB 49 | LDREXD | LDREXH | LDRH | LDRHT | LDRSB | LDRSBT 50 | LDRSH | LDRSHT | LDRT | LEAVEX | LSL | LSR 51 | MCR | MCR2 | MCRR | MCRR2 | MLA | MLS | MOV | MOVT | MOVW 52 | MRC | MRC2 | MRRC | MRRC2 | MRS | MSR | MUL | MVN 53 | NOP 54 | ORN | ORR 55 | PKHBT | PKHTB | PLD | PLDW | PLI | POP | PUSH 56 | QADD | QADD16 | QADD8 | QASX | QDADD | QDSUB | QSAX 57 | QSUB | QSUB16 | QSUB8 58 | RBIT | REV | REV16 | REVSH | RFEIA | RFEDA 59 | RFEDB | RFEIB | ROR | RRX | RSB | RSC 60 | SADD16 | SADD8 | SASX | SBC | SBFX | SDIV | SEL 61 | SETEND | SEV | SHADD16 | SHADD8 | SHASX | SHSAX | SHSUB16 62 | SHSUB8 | SMC 63 | SMLABB | SMLABT | SMLATB | SMLATT 64 | SMLALBB | SMLALBT | SMLALTB | SMLALTT 65 | SMULBB | SMULBT | SMULTB | SMULTT 66 | SMLAWB | SMLAWT | SMULWB | SMULWT 67 | SMUAD | SMUADX 68 | SMUSD | SMUSDX 69 | SMLAD | SMLADX 70 | SMLALD | SMLALDX 71 | SMLSD | SMLSDX 72 | SMLSLD | SMLSLDX 73 | SMMUL | SMMULR 74 | SMMLA | SMMLAR 75 | SMMLS | SMMLSR 76 | SMULL | SMLAL 77 | SRSIA | SRSDA | SRSDB | SRSIB | SSAT | SSAT16 | SSAX 78 | SSUB16 | SSUB8 | STC | STCL | STC2 | STC2L 79 | STMIA | STMDA | STMDB | STMIB | STR | STRB | STRBT 80 | STRD | STREX | STREXB | STREXD | STREXH | STRH | STRHT 81 | STRT | SUB | SUBW | SVC 82 | SWP | SWPB | SXTAB | SXTAB16 | SXTAH | SXTB | SXTB16 | SXTH 83 | TBB | TBH | TEQ | TST 84 | UADD16 | UADD8 | UASX | UBFX | UDIV | UHADD16 | UHADD8 85 | UHASX | UHSAX | UHSUB16 | UHSUB8 | UMAAL | UMLAL | UMULL 86 | UQADD16 | UQADD8 | UQASX | UQSAX | UQSUB16 | UQSUB8 | USAD8 87 | USADA8 | USAT | USAT16 | USAX | USUB16 | USUB8 | UXTAB 88 | UXTAB16 | UXTAH | UXTB | UXTB16 | UXTH 89 | WFE | WFI 90 | YIELD; 91 92datatype arch = ARMv4 | ARMv4T 93 | ARMv5T | ARMv5TE 94 | ARMv6 | ARMv6K | ARMv6T2 95 | ARMv7_A | ARMv7_R; 96 97datatype qualifier = Narrow | Wide | Either; 98 99datatype code = ARM_CODE | THUMB_CODE | THUMBX_CODE; 100 101type instruction = 102 {sflag : term, cond : term, qual : qualifier, 103 mnemonic : instruction_mnemonic }; 104 105type state = 106 {instruction : instruction option, 107 code : code, 108 linenumber : int, 109 itstate : term * bool list, 110 arch : arch, 111 tokens : Substring.substring list }; 112 113datatype 'a error_okay = 114 Error of { origin_function : string, message : string } | Okay of 'a; 115 116type 'a M = state -> ('a * state) error_okay; 117 118infix >>= >>-; 119 120val op >>= : 'a M * ('a -> 'b M) -> 'b M = 121 fn (f,g) => fn s => 122 case f s 123 of Error e => Error e 124 | Okay (x,t) => g x t; 125 126val return : 'a -> 'a M = fn x => fn s => Okay (x,s); 127 128val op >>- = fn (f,g) => f >>= (fn _ => g); 129 130val raiseT : string * string -> 'a M = 131 fn (x,y) => fn _ => Error { origin_function = x, message = y }; 132 133val tryT : 'a M -> ('a -> 'b M) -> (unit -> 'b M) -> 'b M = 134 fn f => fn g => fn h => fn s => 135 case f s 136 of Error e => h () s 137 | Okay (x,t) => g x t; 138 139val optionT : unit M -> unit M = 140 fn f => tryT f return (fn _ => return ()); 141 142val readT : (state -> 'a) -> 'a M = fn f => fn (s:state) => Okay (f s,s); 143val writeT : (state -> state) -> unit M = fn f => fn (s:state) => Okay ((),f s); 144 145val read_instruction = readT (#instruction); 146val read_linenumber = readT (#linenumber); 147val read_itstate = readT (#itstate); 148val read_thumb = readT (fn s => #code s <> ARM_CODE); 149val read_thumbee = readT (fn s => #code s = THUMBX_CODE); 150val read_arch = readT (#arch); 151val read_tokens = readT (#tokens); 152val read_token = read_tokens >>= (fn l => return (total hd l)); 153 154val read_cond : term M = 155 read_instruction >>= (fn i => return (#cond (valOf i))); 156 157val read_sflag : term M = 158 read_instruction >>= (fn i => return (#sflag (valOf i))); 159 160val read_qualifier : qualifier M = 161 read_instruction >>= (fn i => return (#qual (valOf i))); 162 163val read_mnemonic : instruction_mnemonic M = 164 read_instruction >>= (fn i => return (#mnemonic (valOf i))); 165 166val read_InITBlock : bool M = 167 read_itstate >>= (fn (c,l) => 168 return (not (null l) andalso c !~ boolSyntax.arb)); 169 170val read_OutsideOrLastInITBlock : bool M = 171 read_itstate >>= (fn (_,l) => return (length l <= 1)); 172 173val write_instruction = fn i => writeT (fn s => 174 { instruction = i, 175 code = #code s, 176 linenumber = #linenumber s, 177 arch = #arch s, 178 itstate = #itstate s, 179 tokens = #tokens s }); 180 181val write_cond = fn c => writeT (fn s => 182let val i = #instruction s in 183 { instruction = if isSome i then 184 let val i = valOf i in 185 SOME { sflag = #sflag i, cond = c, qual = #qual i, 186 mnemonic = # mnemonic i } 187 end 188 else 189 raise ERR "write_cond" "no instruction", 190 code = #code s, 191 linenumber = #linenumber s, 192 arch = #arch s, 193 itstate = #itstate s, 194 tokens = #tokens s } 195end); 196 197val write_code = fn c => writeT (fn s => 198 { instruction = #instruction s, 199 code = c, 200 linenumber = #linenumber s, 201 arch = #arch s, 202 itstate = (boolSyntax.arb,[]), 203 tokens = #tokens s }); 204 205val write_arch = fn a => writeT (fn s => 206 { instruction = #instruction s, 207 code = if a = ARMv4 then ARM_CODE else #code s, 208 linenumber = #linenumber s, 209 arch = a, 210 itstate = (boolSyntax.arb,[]), 211 tokens = #tokens s }); 212 213val write_itcond = fn c => writeT (fn s => 214 { instruction = #instruction s, 215 code = #code s, 216 linenumber = #linenumber s, 217 arch = #arch s, 218 itstate = (c, snd (#itstate s)), 219 tokens = #tokens s }); 220 221val write_itlist = fn l => writeT (fn s => 222 { instruction = #instruction s, 223 code = #code s, 224 linenumber = #linenumber s, 225 arch = #arch s, 226 itstate = (fst (#itstate s), l), 227 tokens = #tokens s }); 228 229val write_token = fn t => writeT (fn s => 230 { instruction = #instruction s, 231 code = #code s, 232 linenumber = #linenumber s, 233 arch = #arch s, 234 itstate = #itstate s, 235 tokens = t::tl (#tokens s) }); 236 237val next_linenumber = writeT (fn s => 238 { instruction = #instruction s, 239 code = #code s, 240 linenumber = #linenumber s + 1, 241 arch = #arch s, 242 itstate = #itstate s, 243 tokens = #tokens s }); 244 245val next_itstate = writeT (fn s => 246 { instruction = #instruction s, 247 code = #code s, 248 linenumber = #linenumber s, 249 arch = #arch s, 250 itstate = let val (c,l) = #itstate s in 251 if length l < 2 then 252 (boolSyntax.arb,[]) 253 else 254 (c, tl l) 255 end, 256 tokens = #tokens s }); 257 258val next_token = writeT (fn s => 259 { instruction = #instruction s, 260 code = #code s, 261 linenumber = #linenumber s, 262 arch = #arch s, 263 itstate = #itstate s, 264 tokens = case #tokens s of [] => [] | h::t => t }); 265 266datatype shift = ROR_shift | LSR_shift | ASR_shift | LSL_shift | RRX_shift; 267 268fun syntax_errorT (e,g) : 'a M = 269 read_linenumber >>= 270 (fn n => raiseT ("parse " ^ e, 271 "syntax error at line " ^ Int.toString n ^ 272 ": expecting " ^ e ^ " got " ^ g)); 273 274fun other_errorT (e,m) : 'a M = 275 read_linenumber >>= 276 (fn n => raiseT (e, "error at line " ^ Int.toString n ^ ": " ^ m)); 277 278val assertT : bool -> (string * string) -> 'a M -> 'a M = 279 fn b => fn x => fn f => 280 if b then f else other_errorT x; 281 282(* ------------------------------------------------------------------------- *) 283 284fun whitespace c = Char.isSpace c andalso c <> #"\n"; 285fun alphanum c = Char.isAlphaNum c orelse mem c (explode "._'"); 286fun variable c = alphanum c andalso not (Char.isDigit c); 287val isBinDigit = Lib.C mem (explode "01"); 288val isOctDigit = Lib.C mem (explode "01234567"); 289 290val lower_explode = map Char.toLower o Substring.explode; 291val lower_string = String.implode o lower_explode; 292val lower_substring = Substring.full o lower_string; 293 294local 295 val sstr = Substring.full o String.str 296 297 fun split_at_end_quote s = 298 let fun recurse i = 299 case (total Substring.sub (s,i),total Substring.sub (s,i + 1)) 300 of (NONE, SOME #"\"") => i + 1 301 | (SOME c, SOME #"\"") => if c <> #"\\" then i + 1 else recurse (i + 1) 302 | (_, SOME c) => recurse (i + 1) 303 | _ => i + 1 304 in 305 Substring.splitAt (s,Int.min (recurse ~1 + 1, Substring.size s)) 306 end 307 308 fun skip_block left right s = 309 let 310 val sleft = String.size left 311 val sright = String.size right 312 313 fun recurse n (ls,rs) = 314 let val (l,r) = Substring.position left rs 315 val (ll,rl) = Substring.position right l 316 in 317 if Substring.isPrefix right rl orelse Substring.size r < sleft then 318 if n = 0 orelse Substring.size rl < sright then 319 (Substring.span (ls,ll), Substring.span(rl,r)) 320 else let val (lrl,rrl) = Substring.splitAt (rl,sright) in 321 recurse (n - 1) 322 (Substring.span (ls,Substring.span (ll,lrl)), 323 Substring.span (rrl,r)) 324 end 325 else let val (lr,rr) = Substring.splitAt (r,sleft) in 326 recurse (n + 1) (Substring.span (ls,Substring.span (l,lr)), rr) 327 end 328 end 329 in 330 recurse 0 (Substring.slice(s,0,SOME 0), s) 331 end 332 333 fun skip_to_newline s = snd (Substring.splitl (not o curry (op =) #"\n") s) 334 335 fun get_newlines s = 336 s |> Substring.explode 337 |> List.filter (curry (op =) #"\n") 338 |> map sstr 339 340 fun lex s a = 341 let val s0 = Substring.dropl whitespace s in 342 case Substring.getc s0 343 of SOME (#"/",s1) => 344 (case Substring.getc s1 345 of SOME (#"*",s2) => 346 let val (s3,s4) = skip_block "/*" "*/" s2 347 val _ = Substring.isPrefix "*/" s4 orelse 348 raise ERR "lex" "missing closing */" 349 in 350 lex (Substring.triml 2 s4) (get_newlines s3 @ a) 351 end 352 | SOME (#"/",s2) => lex (skip_to_newline s0) a 353 | _ => lex s1 ((sstr #"/")::a)) 354 | SOME (#"(",s1) => 355 (case Substring.getc s1 356 of SOME (#"*",s2) => 357 let val (s3,s4) = skip_block "(*" "*)" s2 358 val _ = Substring.isPrefix "*)" s4 orelse 359 raise ERR "lex" "missing closing *)" 360 in 361 lex (Substring.triml 2 s4) (get_newlines s3 @ a) 362 end 363 | _ => lex s1 ((sstr #"(")::a)) 364 | SOME (#"@",s1) => lex (skip_to_newline s0) a 365 | SOME (#";",s1) => lex (skip_to_newline s0) a 366 | SOME (#"\"",s1) => 367 let val (l,r) = split_at_end_quote s1 in 368 lex r (Substring.full ("\"" ^ Substring.string l)::a) 369 end 370 | SOME (c,s1) => 371 if alphanum c then 372 let val (l,r) = Substring.splitl alphanum s0 in 373 lex r (l::a) 374 end 375 else 376 lex s1 ((sstr c)::a) 377 | NONE => List.rev a 378 end 379in 380 fun arm_lex s = lex (Substring.full s) [] 381end; 382 383val arm_lex_quote = arm_lex o quote_to_string; 384 385(* ------------------------------------------------------------------------- *) 386 387fun arm_parse (f:'a M) s = 388let val init = { instruction = NONE, 389 code = ARM_CODE, 390 arch = ARMv7_A, 391 linenumber = 1, 392 itstate = (boolSyntax.arb,[]), 393 tokens = arm_lex s } 394in 395 case f init 396 of Error e => raise ERR (#origin_function e) (#message e) 397 | Okay (v,t) => v 398end; 399 400fun arm_parse_quote f q = arm_parse f (quote_to_string q); 401 402fun expr i = if i < 0 then "-" ^ Int.toString (Int.abs i) else Int.toString i; 403 404(* ------------------------------------------------------------------------- *) 405 406val eval = rhs o concl o EVAL; 407 408fun cast_var ty v = mk_var (fst (dest_var v),ty); 409 410fun mk_bool b = if b then T else F; 411fun mk_word2 i = wordsSyntax.mk_wordii (i,2); 412fun mk_word3 i = wordsSyntax.mk_wordii (i,3); 413fun mk_word4 i = wordsSyntax.mk_wordii (i,4); 414fun mk_word5 i = wordsSyntax.mk_wordii (i,5); 415fun mk_word6 i = wordsSyntax.mk_wordii (i,6); 416fun mk_word8 i = wordsSyntax.mk_wordii (i,8); 417fun mk_word12 i = wordsSyntax.mk_wordii (i,12); 418fun mk_word16 i = wordsSyntax.mk_wordii (i,16); 419fun mk_word24 i = wordsSyntax.mk_wordii (i,24); 420fun mk_word32 n = wordsSyntax.mk_wordi (n,32); 421val mk_integer = intSyntax.mk_injected o numSyntax.mk_numeral; 422val uint_of_word = wordsSyntax.uint_of_word; 423 424fun sint_of_term tm = 425 tm |> intSyntax.int_of_term |> Arbint.toInt 426 handle Overflow => raise ERR "sint_of_term" 427 ("integer " ^ term_to_string tm ^ " too large") 428 | HOL_ERR _ => raise ERR "sint_of_term" 429 ("could not convert ``" ^ term_to_string tm ^ 430 "`` to an integer"); 431 432fun list_to_int l = 433let fun recurse [] a = a 434 | recurse (h::t) a = recurse t (if h = 1 then 2 * a + 1 else 2 * a) 435in 436 recurse l 0 437end; 438 439val is_T = term_eq T; 440val is_F = term_eq F; 441val is_R9 = term_eq (mk_word4 9); 442val is_R10 = term_eq (mk_word4 10); 443val is_SP = term_eq (mk_word4 13); 444val is_AL = term_eq (mk_word4 14); 445val is_PC = term_eq (mk_word4 15); 446 447infix pow 448 449fun op pow (x,y) = 450 if y mod 2 = 1 then 451 x * (x pow (y - 1)) 452 else 453 if y = 0 then 454 1 455 else 456 (x * x) pow (y div 2); 457 458fun bit i n = n div (2 pow i) mod 2 = 1; 459 460fun int_to_word n tm = 461let val r = eval (integer_wordSyntax.mk_i2w (tm,n)) 462 val _ = mk_disj (mk_eq (tm,integer_wordSyntax.mk_w2i r), 463 mk_eq (tm,r |> wordsSyntax.mk_w2n 464 |> intSyntax.mk_injected)) 465 |> EVAL |> EQT_ELIM 466 handle HOL_ERR _ => raise ERR "int_to_word" 467 ("Failed to convert integer " ^ term_to_string tm ^ 468 " to a signed " ^ 469 (n |> fcpLib.index_to_num |> Arbnum.toString) ^ "-bit word") 470in 471 r 472end; 473 474fun uint_to_word n tm = 475let val r = eval (integer_wordSyntax.mk_i2w (tm,n)) 476 val _ = mk_eq (tm,r |> wordsSyntax.mk_w2n |> intSyntax.mk_injected) 477 |> EVAL |> EQT_ELIM 478 handle HOL_ERR _ => raise ERR "uint_to_word" 479 ("Failed to convert integer " ^ term_to_string tm ^ 480 " to an unsigned " ^ 481 (n |> fcpLib.index_to_num |> Arbnum.toString) ^ "-bit word") 482in 483 r 484end; 485 486local 487 val n4 = Arbnum.fromInt 4 488 val n128 = Arbnum.fromInt 128 489 val n256 = Arbnum.fromInt 256 490 val msb30 = Arbnum.pow (Arbnum.two, Arbnum.fromInt 30) 491 val msb32 = Arbnum.pow (Arbnum.two, Arbnum.fromInt 32) 492 493 fun rol_two32 n = 494 let val n' = Arbnum.mod (Arbnum.*(n,n4), msb32) in 495 Arbnum.+(n',Arbnum.div (n, msb30)) 496 end 497 498 fun num_to_imm x n = 499 let val x' = Arbnum.mod (x,n256) in 500 if x' = x then 501 (n, x') 502 else 503 if n < 15 then 504 num_to_imm (rol_two32 x) (n + 1) 505 else 506 raise ERR "num_to_imm" "cannot be represented as an immediate" 507 end 508 509 fun num_to_immediate n = 510 let open Arbnum 511 val (s,n) = num_to_imm n 0 512 in 513 (fromInt s * n256) + n 514 end 515 516 fun num_to_bytes n = 517 let val (r,b0) = Arbnum.divmod (n, n256) 518 val (r,b1) = Arbnum.divmod (r, n256) 519 val (r,b2) = Arbnum.divmod (r, n256) 520 in 521 (Arbnum.mod (r,n256), b2, b1, b0) 522 end 523 524 fun num_to_thumb2_immediate n = 525 let val error = "cannot be represented as an Thumb2 immediate" 526 val (b3,b2,b1,b0) = num_to_bytes n 527 fun is_zero x = x = Arbnum.zero 528 fun imm (x,y) = Arbnum.+(Arbnum.*(Arbnum.fromInt x,n256),y) 529 in 530 case (is_zero b3, is_zero b2, is_zero b1, is_zero b0) 531 of (true,true,true,_) => 532 b0 533 | (true,false,true,false) => 534 if b2 = b0 then imm (1,b0) else 535 raise ERR "num_to_thumb2_immediate" error 536 | (false,true,false,true) => 537 if b3 = b1 then imm (2,b1) else 538 raise ERR "num_to_thumb2_immediate" error 539 | (false,false,false,false) => 540 if b3 = b2 andalso b2 = b1 andalso b1 = b0 then imm (3,b0) else 541 raise ERR "num_to_thumb2_immediate" error 542 | _ => 543 let val m = Arbnum.log2 n 544 val lsr_n = funpow (Arbnum.toInt m + 1 - 8) Arbnum.div2 n 545 val s = Arbnum.fromInt (31 - Arbnum.toInt m + 8) 546 in 547 if Arbnum.<(lsr_n, n256) then 548 Arbnum.+(Arbnum.*(s,n128),Arbnum.mod (lsr_n,n128)) 549 else 550 raise ERR "num_to_thumb2_immediate" error 551 end 552 end 553 554 fun int_to_imm f tm = 555 (tm |> int_to_word ``:32`` 556 |> wordsSyntax.dest_n2w 557 |> fst 558 |> numSyntax.dest_numeral 559 |> f 560 |> Arbnum.toInt 561 |> mk_word12) handle HOL_ERR _ => 562 raise ERR "int_to_immediate" 563 ("cannot represent " ^ term_to_string tm ^ 564 " as a mode1 immediate") 565in 566 val int_to_mode1_immediate = int_to_imm num_to_immediate 567 val int_to_thumb2_mode1_immediate = int_to_imm num_to_thumb2_immediate 568end; 569 570fun offset_to_imm24 i = 571 if 0 <= i then 572 mk_word24 i 573 else 574 i |> Int.~ 575 |> mk_word24 576 |> wordsSyntax.mk_word_2comp 577 |> eval; 578 579(* ------------------------------------------------------------------------- *) 580 581local 582 val mnemonic_strings = 583 [("adc", ADC), ("add", ADD), ("addw", ADDW), ("adr", ADR), ("and", AND), 584 ("asr", ASR), 585 ("b", B), ("bfc", BFC), ("bfi", BFI), ("bic", BIC), ("bkpt", BKPT), 586 ("bl", BL), ("blx", BLX), ("bx", BX), 587 ("cbz", CBZ), ("cbnz", CBNZ), ("cdp", CDP), ("cdp2", CDP2), ("chka", CHKA), 588 ("clrex", CLREX), 589 ("clz", CLZ), ("cmn", CMN), ("cmp", CMP), 590 ("cps", CPS), ("cpsie", CPSIE), ("cpsid", CPSID), 591 ("dbg", DBG), ("dmb", DMB), ("dsb", DSB), 592 ("enterx",ENTERX), ("eor", EOR), 593 ("hb", HB), ("hbl", HBL), ("hblp", HBLP), ("hbp", HBP), 594 ("isb", ISB), ("it", IT), 595 ("ldc", LDC), ("ldcl", LDCL), ("ldc2", LDC2), ("ldc2l", LDC2L), 596 ("ldm", LDMIA), ("ldmia", LDMIA), ("ldmfd", LDMIA), 597 ("ldmda", LDMDA), ("ldmfa", LDMDA), 598 ("ldmdb", LDMDB), ("ldmea", LDMDB), 599 ("ldmib", LDMIB), ("ldmed", LDMIB), 600 ("ldr", LDR), ("ldrb", LDRB), 601 ("ldrbt", LDRBT), ("ldrht", LDRHT), 602 ("ldrd", LDRD), ("ldrex", LDREX), ("ldrexb", LDREXB), ("ldrexd", LDREXD), 603 ("ldrexh", LDREXH), ("ldrh", LDRH), 604 ("ldrsb", LDRSB), ("ldrsbt", LDRSBT), ("ldrsh", LDRSH), ("ldrsht", LDRSHT), 605 ("ldrt", LDRT), 606 ("leavex", LEAVEX), ("lsl", LSL), ("lsr", LSR), 607 ("mcr", MCR), ("mcr2", MCR2), ("mcrr", MCRR), ("mcrr2", MCRR2), ("mla", MLA), 608 ("mls", MLS), ("mov", MOV), ("movt", MOVT), ("movw", MOVW), 609 ("mrc", MRC), ("mrc2", MRC2), ("mrrc", MRRC), ("mrrc2", MRRC2), ("mrs", MRS), 610 ("msr", MSR), ("mul", MUL), ("mvn", MVN), 611 ("nop", NOP), 612 ("orn", ORN), ("orr", ORR), 613 ("pkhbt", PKHBT), ("pkhtb", PKHTB), ("pld", PLD), ("pldw", PLDW), 614 ("pli", PLI), ("pop", POP), ("push", PUSH), 615 ("qadd", QADD), ("qadd16", QADD16), ("qadd8", QADD8), ("qasx", QASX), 616 ("qdadd", QDADD), ("qdsub", QDSUB), ("qsax", QSAX), 617 ("qsub", QSUB), ("qsub16", QSUB16), ("qsub8", QSUB8), 618 ("rbit", RBIT), ("rev", REV), ("rev16", REV16), ("revsh", REVSH), 619 ("rfe", RFEIA), ("rfeia", RFEIA), ("rfeda", RFEDA), ("rfedb", RFEDB), 620 ("rfeib", RFEIB), ("ror", ROR), ("rrx", RRX), ("rsb", RSB), ("rsc", RSC), 621 ("sadd16", SADD16), ("sadd8", SADD8), ("sasx", SASX), ("sbc", SBC), 622 ("sbfx", SBFX), ("sdiv", SDIV), ("sel", SEL), 623 ("setend", SETEND), ("sev", SEV), ("shadd16", SHADD16), ("shadd8", SHADD8), 624 ("shasx", SHASX), ("shsax", SHSAX), ("shsub16", SHSUB16), 625 ("shsub8", SHSUB8), ("smc", SMC), ("smlabb", SMLABB), ("smlabt", SMLABT), 626 ("smlatb", SMLATB), ("smlatt", SMLATT), 627 ("smlad", SMLAD), ("smladx", SMLADX), ("smlal", SMLAL), ("smlalbb", SMLALBB), 628 ("smlalbt", SMLALBT), ("smlaltb", SMLALTB), ("smlaltt", SMLALTT), 629 ("smlald", SMLALD), ("smlaldx", SMLALDX), 630 ("smlawb", SMLAWB), ("smlawt", SMLAWT), 631 ("smlsd", SMLSD), ("smlsdx", SMLSDX), ("smlsld", SMLSLD), 632 ("smlsldx", SMLSLDX), ("smmla", SMMLA), ("smmlar", SMMLAR), ("smmls", SMMLS), 633 ("smmlsr", SMMLSR), ("smmul", SMMUL), ("smmulr", SMMULR), ("smuad", SMUAD), 634 ("smuadx", SMUADX), ("smulbb", SMULBB), 635 ("smulbt", SMULBT), ("smultb", SMULTB), ("smultt", SMULTT), ("smull", SMULL), 636 ("smulwb", SMULWB), ("smulwt", SMULWT), ("smusd", SMUSD), ("smusdx", SMUSDX), 637 ("srs", SRSIA), ("srsia", SRSIA), ("srsda", SRSDA), ("srsdb", SRSDB), 638 ("srsib", SRSIB), ("ssat", SSAT), ("ssat16", SSAT16), ("ssax", SSAX), 639 ("ssub16", SSUB16), ("ssub8", SSUB8), ("stc", STC), ("stcl", STCL), 640 ("stc2", STC2), ("stc2l", STC2L), 641 ("stm", STMIA), ("stmia", STMIA), ("stmea", STMIA), 642 ("stmda", STMDA), ("stmed", STMDA), 643 ("stmdb", STMDB), ("stmfd", STMDB), 644 ("stmib", STMIB), ("stmfa", STMIB), 645 ("str", STR), ("strb", STRB), 646 ("strbt", STRBT), ("strd", STRD), ("strex", STREX), ("strexb", STREXB), 647 ("strexd", STREXD), ("strexh", STREXH), ("strh", STRH), 648 ("strht", STRHT), ("strt", STRT), ("sub", SUB), ("subw", SUBW), 649 ("svc", SVC), ("swp", SWP), ("swpb", SWPB), ("sxtab", SXTAB), 650 ("sxtab16", SXTAB16), ("sxtah", SXTAH), ("sxtb", SXTB), ("sxtb16", SXTB16), 651 ("sxth", SXTH), 652 ("tbb", TBB), ("tbh", TBH), ("teq", TEQ), ("tst", TST), 653 ("uadd16", UADD16), ("uadd8", UADD8), ("uasx", UASX), ("ubfx", UBFX), 654 ("udiv", UDIV), ("uhadd16", UHADD16), ("uhadd8", UHADD8), 655 ("uhasx", UHASX), ("uhsax", UHSAX), ("uhsub16", UHSUB16), 656 ("uhsub8", UHSUB8), ("umaal", UMAAL), ("umlal", UMLAL), ("umull", UMULL), 657 ("uqadd16", UQADD16), ("uqadd8", UQADD8), ("uqasx", UQASX), 658 ("uqsax", UQSAX), ("uqsub16", UQSUB16), ("uqsub8", UQSUB8), ("usad8", USAD8), 659 ("usada8", USADA8), ("usax", USAX), ("usat", USAT), ("usat16", USAT16), 660 ("usub16", USUB16), ("usub8", USUB8), ("uxtab", UXTAB), 661 ("uxtab16", UXTAB16), ("uxtah", UXTAH), 662 ("uxtb", UXTB), ("uxtb16", UXTB16), ("uxth", UXTH), 663 ("wfe", WFE), ("wfi", WFI), 664 ("yield", YIELD)]; 665 666 fun mnemonic_compare ((x,_),(y,_)) = 667 Int.compare (String.size y, String.size x) 668 669 val mnemonic_strings = Listsort.sort mnemonic_compare mnemonic_strings 670in 671 fun find_mnemonic s = 672 let fun find_prefix [] = NONE 673 | find_prefix ((l,r)::t) = 674 if Substring.isPrefix l s andalso 675 (l <> "bl" orelse Lib.mem (Substring.size s) [2, 4]) 676 then 677 SOME (Substring.triml (String.size l) s,r) 678 else 679 find_prefix t 680 in 681 find_prefix mnemonic_strings 682 end 683end; 684 685fun condition_to_word4 s = 686 mk_word4 687 (case s 688 of "eq" => 0 689 | "ne" => 1 690 | "cs" => 2 691 | "hs" => 2 692 | "cc" => 3 693 | "lo" => 3 694 | "mi" => 4 695 | "pl" => 5 696 | "vs" => 6 697 | "vc" => 7 698 | "hi" => 8 699 | "ls" => 9 700 | "ge" => 10 701 | "lt" => 11 702 | "gt" => 12 703 | "le" => 13 704 | "al" => 14 705 | _ => raise ERR "condition_to_word4" (s ^ " is not a condition")); 706 707fun opposite_condition (tm1,tm2) = 708let val n1 = uint_of_word tm1 709 val n2 = uint_of_word tm2 710in 711 not (n1 = 14 orelse n2 = 14) andalso 712 n1 div 2 = n2 div 2 andalso n1 mod 2 <> n2 mod 2 713end; 714 715local 716 val condition_strings = 717 ["eq","ne","cs","hs","cc","lo","mi","pl","vs", 718 "vc","hi","ls","ge","lt","gt","le","al"] 719in 720 fun find_condition s = 721 let fun find_prefix [] = NONE 722 | find_prefix (l::t) = 723 if Substring.isPrefix l s then 724 SOME (l,Substring.triml 2 s) 725 else 726 find_prefix t 727 in 728 find_prefix condition_strings 729 end 730end; 731 732(* ------------------------------------------------------------------------- *) 733 734val has_thumb2 = Lib.C mem [ARMv6T2, ARMv7_A, ARMv7_R]; 735val has_dsp = not o Lib.C mem [ARMv4, ARMv4T, ARMv5T]; 736 737fun version_number ARMv4 = 4 738 | version_number ARMv4T = 4 739 | version_number ARMv5T = 5 740 | version_number ARMv5TE = 5 741 | version_number ARMv6 = 6 742 | version_number ARMv6K = 6 743 | version_number ARMv6T2 = 6 744 | version_number _ = 7; 745 746fun word_aligned (tm1,i) = 747 can EQT_ELIM (armSyntax.mk_aligned (tm1,numSyntax.term_of_int i) |> EVAL); 748 749fun word_lower_same (tm1,tm2) = 750 can EQT_ELIM (wordsSyntax.mk_word_ls (tm1,tm2) |> EVAL); 751 752fun narrow_register tm = 753 type_of tm = ``:word4`` andalso 754 (is_var tm orelse word_lower_same (tm,mk_word4 7)); 755 756val narrow_registers = Lib.all narrow_register; 757 758val arch_version : int M = 759 read_arch >>= (fn arch => return (version_number arch)); 760 761val arch_okay : string * string -> (arch -> bool) -> 'a M -> 'a M = 762 fn s => fn P => fn f => 763 read_arch >>= (fn arch => assertT (P arch) s f); 764 765val not_narrow : string -> 'a M -> 'a M = 766 fn s => fn f => 767 read_qualifier >>= (fn q => 768 assertT (q <> Narrow) (s,"not available as narrow thumb instruction") f); 769 770val thumb2_okay : string -> 'a M -> 'a M = 771 fn s => fn f => 772 not_narrow s 773 (read_thumb >>= (fn thumb => 774 arch_okay (s,"Thumb2 only") 775 (fn a => thumb andalso has_thumb2 a) f)); 776 777val thumb2_or_arm_okay : string -> (term -> 'a M) -> 'a M = 778 fn s => fn f => 779 read_thumb >>= (fn thumb => 780 if thumb then 781 not_narrow s (arch_okay (s,"requires Thumb2") has_thumb2 782 (f Encoding_Thumb2_tm)) 783 else 784 f Encoding_ARM_tm); 785 786val thumb_or_arm_okay : (term -> 'a M) -> 'a M = 787 fn f => 788 read_thumb >>= (fn thumb => 789 if thumb then 790 f Encoding_Thumb_tm 791 else 792 f Encoding_ARM_tm); 793 794fun need_t2 s = 795 arch_okay (s,"requires architecture with Thumb2 support") has_thumb2; 796 797fun need_dsp s = 798 arch_okay (s,"requires architecture with DSP support") has_dsp; 799 800fun need_v5 s = 801 arch_okay (s,"requires architecture version >= 5") 802 (fn a => version_number a >= 5); 803 804fun need_v6 s = 805 arch_okay (s,"requires architecture version >= 6") 806 (fn a => version_number a >= 6); 807 808fun need_v7 s = 809 arch_okay (s,"requires architecture version >= 7") 810 (fn a => version_number a >= 7); 811 812(* ------------------------------------------------------------------------- *) 813 814val arm_parse_variable : hol_type -> term M = 815 fn ty => 816 read_token >>= 817 (fn h => 818 case h 819 of NONE => syntax_errorT ("variable", "end-of-input") 820 | SOME s => if variable (Substring.sub (s,0)) then 821 next_token >>- return (mk_var (Substring.string s,ty)) 822 else 823 syntax_errorT ("variable", Substring.string s)); 824 825fun char_list_to_word4 l x = 826 case l 827 of [#"0"] => return (mk_word4 0) 828 | [#"1"] => return (mk_word4 1) 829 | [#"2"] => return (mk_word4 2) 830 | [#"3"] => return (mk_word4 3) 831 | [#"4"] => return (mk_word4 4) 832 | [#"5"] => return (mk_word4 5) 833 | [#"6"] => return (mk_word4 6) 834 | [#"7"] => return (mk_word4 7) 835 | [#"8"] => return (mk_word4 8) 836 | [#"9"] => return (mk_word4 9) 837 | [#"1", #"0"] => return (mk_word4 10) 838 | [#"1", #"1"] => return (mk_word4 11) 839 | [#"1", #"2"] => return (mk_word4 12) 840 | [#"1", #"3"] => return (mk_word4 13) 841 | [#"1", #"4"] => return (mk_word4 14) 842 | [#"1", #"5"] => return (mk_word4 15) 843 | _ => syntax_errorT x; 844 845val arm_parse_register : term M = 846 read_token >>= 847 (fn h => 848 case h 849 of NONE => syntax_errorT ("register", "end-of-input") 850 | SOME h => next_token >>- 851 (case lower_explode h 852 of #"r"::l => char_list_to_word4 l ("register", Substring.string h) 853 | [#"s", #"p"] => return (mk_word4 13) 854 | [#"l", #"r"] => return (mk_word4 14) 855 | [#"p", #"c"] => return (mk_word4 15) 856 | _ => syntax_errorT ("register", Substring.string h))); 857 858val arm_parse_coprocessor : term M = 859 read_token >>= 860 (fn h => 861 case h 862 of NONE => syntax_errorT ("coprocessor", "end-of-input") 863 | SOME h => next_token >>- 864 (case lower_explode h 865 of #"p"::l => char_list_to_word4 l 866 ("coprocessor", Substring.string h) 867 | _ => syntax_errorT ("coprocessor", Substring.string h))); 868 869val arm_parse_cregister : term M = 870 read_token >>= 871 (fn h => 872 case h 873 of NONE => syntax_errorT ("coprocessor register", "end-of-input") 874 | SOME h => next_token >>- 875 (case lower_explode h 876 of #"c"::l => char_list_to_word4 l 877 ("coprocessor register", Substring.string h) 878 | _ => syntax_errorT 879 ("coprocessor register", Substring.string h))); 880 881val arm_parse_number : term M = 882 read_token >>= 883 (fn h => 884 case h 885 of NONE => syntax_errorT ("register", "end-of-input") 886 | SOME h => next_token >>- 887 let fun number P f l = 888 if Lib.all P l then 889 return (mk_integer (f (implode l))) 890 else 891 syntax_errorT ("number", Substring.string h) 892 in 893 case Substring.explode h 894 of [#"0"] => return intSyntax.zero_tm 895 | (#"0"::(#"b"::cs)) => 896 number isBinDigit Arbnum.fromBinString cs 897 | (#"0"::(#"x"::cs)) => 898 number Char.isHexDigit Arbnum.fromHexString cs 899 | #"0"::cs => 900 number isOctDigit Arbnum.fromOctString cs 901 | c::cs => 902 number Char.isDigit Arbnum.fromString (c::cs) 903 | _ => syntax_errorT ("number", Substring.string h) 904 end); 905 906val arm_parse_string : string -> unit M = 907 fn s => 908 read_token >>= 909 (fn h => 910 case h 911 of NONE => syntax_errorT (s, "end-of-input") 912 | SOME h => if String.compare (lower_string h, s) = EQUAL then 913 next_token 914 else 915 syntax_errorT (s, Substring.string h)); 916 917val arm_parse_hash = arm_parse_string "#"; 918val arm_parse_plus = arm_parse_string "+"; 919val arm_parse_minus = arm_parse_string "-"; 920val arm_parse_comma = arm_parse_string ","; 921val arm_parse_lbrace = arm_parse_string "{"; 922val arm_parse_rbrace = arm_parse_string "}"; 923val arm_parse_lsquare = arm_parse_string "["; 924val arm_parse_rsquare = arm_parse_string "]"; 925val arm_parse_exclaim = arm_parse_string "!"; 926val arm_parse_colon = arm_parse_string ":"; 927val arm_parse_hat = arm_parse_string "^"; 928 929val arm_parse_strings : string list -> string M = 930 fn l => 931 read_token >>= 932 (fn h => 933 case h 934 of NONE => syntax_errorT (quote (String.concat (Lib.commafy l)), 935 "end-of-input") 936 | SOME h => let val s = lower_string h in 937 if mem s l then 938 next_token >>- return s 939 else 940 syntax_errorT 941 ("``" ^ (String.concat (Lib.commafy l) ^ "``"), 942 Substring.string h) 943 end); 944 945val arm_parse_string_const : string M = 946 read_token >>= 947 (fn h => 948 case h 949 of NONE => syntax_errorT ("string", "end-of-input") 950 | SOME h => let val s = Substring.size h in 951 if s >= 2 andalso 952 Substring.sub (h,0) = #"\"" andalso 953 Substring.sub (h,s - 1) = #"\"" 954 then 955 next_token >>- 956 return 957 (Substring.string (h |> Substring.triml 1 958 |> Substring.trimr 1)) 959 else 960 syntax_errorT ("string", Substring.string h) 961 end); 962 963val arm_parse_endline : unit M = 964 read_token >>= 965 (fn h => 966 case h 967 of NONE => return () 968 | SOME h => if Substring.compare (Substring.full "\n", h) = EQUAL then 969 next_token >>- next_linenumber 970 else 971 syntax_errorT 972 ("newline or end-of-input", Substring.string h)); 973 974val arm_parse_endoffile : bool M = 975 read_token >>= (fn h => return (not (isSome h))); 976 977val arm_parse_plus_minus : bool M = 978 tryT arm_parse_plus (fn _ => return true) (fn _ => 979 tryT arm_parse_minus (fn _ => return false) 980 (fn _ => return true)); 981 982val arm_parse_signed_number : term M = 983 arm_parse_plus_minus >>= 984 (fn pos => 985 arm_parse_number >>= 986 (fn i => return (if pos then i else intSyntax.mk_negated i))); 987 988val arm_parse_constant : term M = 989 arm_parse_hash >>- arm_parse_signed_number; 990 991val arm_parse_branch_offset : term M = 992 tryT arm_parse_plus 993 (fn _ => arm_parse_hash >>- arm_parse_number >>= return) 994 (fn _ => tryT arm_parse_minus 995 (fn _ => arm_parse_hash >>- arm_parse_number >>= 996 (return o intSyntax.mk_negated)) 997 (fn _ => arm_parse_variable ``:int``)); 998 999(* ------------------------------------------------------------------------- *) 1000 1001local 1002 val has_sflags = 1003 [AND,EOR,ADC,SBC,ORR,BIC,ADD,SUB,RSB,RSC,MOV,MVN,ORN, 1004 LSL,LSR,ASR,ROR,RRX,MUL] 1005 1006 val arm_only_sflags = [MLA,UMULL,UMLAL,SMULL,SMLAL] 1007in 1008 val arm_parse_sflag : instruction_mnemonic -> term M = 1009 fn m => 1010 read_token >>= 1011 (fn t => 1012 case t 1013 of NONE => return F 1014 | SOME h => 1015 read_thumb >>= 1016 (fn thumb => 1017 if (mem m has_sflags orelse not thumb andalso 1018 mem m arm_only_sflags) andalso Substring.isPrefix "s" h 1019 then 1020 write_token (Substring.triml 1 h) >>- return T 1021 else 1022 return (mk_bool (mem m [TST,CMN,TEQ,CMP])))) 1023end; 1024 1025local 1026 fun then_else s = 1027 let val (te,r) = Substring.splitl (fn c => c = #"t" orelse c = #"e") s 1028 val lte = Substring.explode te 1029 in 1030 (true::(List.map (fn c => case c of #"t" => true | _ => false) lte), r) 1031 end 1032in 1033 val arm_parse_it_conditions : unit M = 1034 read_InITBlock >>= (fn InITBlock => 1035 assertT (not InITBlock) 1036 ("arm_parse_it_conditions", 1037 "IT instruction not allowed in IT block") 1038 (read_token >>= 1039 (fn t => 1040 case t 1041 of NONE => return () 1042 | SOME h => 1043 let val (te,r) = then_else h in 1044 assertT (length te <= 4) 1045 ("arm_parse_it_conditions", "unknown mnemonic") 1046 (write_token r >>- write_itlist te) 1047 end))) 1048end; 1049 1050local 1051 val coproc2 = [CDP2, STC2, STC2L, LDC2, LDC2L, MRC2, MRRC2, MCR2, MCRR2] 1052 1053 val is_unconditional = not o (Lib.C mem 1054 ([PLI, CLREX, DSB, DMB, ISB, PLD, PLDW, 1055 SRSIA, SRSDA, SRSDB, SRSIB, 1056 RFEIA, RFEDA, RFEDB, RFEIB, 1057 SETEND, CPS, CPSIE, CPSID] @ coproc2)) 1058 1059 val is_thumb_unconditional = not o (Lib.C mem [SETEND, CPS, CBZ, CBNZ, IT]) 1060in 1061 val arm_parse_condition : instruction_mnemonic -> term M = 1062 fn m => 1063 read_token >>= 1064 (fn t => 1065 case t 1066 of NONE => return (mk_word4 14) 1067 | SOME h => 1068 read_thumb >>= (fn thumb => 1069 case find_condition h 1070 of SOME (s,r) => 1071 if thumb then 1072 read_arch >>= (fn arch => 1073 read_itstate >>= (fn (itcond,l) => 1074 let val outside = null l in 1075 assertT 1076 (s = "al" orelse m = B orelse 1077 has_thumb2 arch andalso 1078 is_thumb_unconditional m andalso not outside) 1079 ("arm_parse_condition", 1080 "condition suffix not allowed or outside IT block") 1081 (let val cond = condition_to_word4 s 1082 val cond' = if m = B andalso not outside orelse 1083 mem m coproc2 1084 then 1085 mk_var (s,``:word4``) 1086 else 1087 cond 1088 in 1089 assertT 1090 (outside orelse 1091 (m <> B orelse length l = 1) andalso 1092 if hd l then 1093 itcond ~~ cond 1094 else 1095 opposite_condition (itcond,cond)) 1096 ("arm_parse_condition", 1097 "wrong condition in IT block or branch not\ 1098 \ last in IT block") 1099 (write_token r >>- return cond') 1100 end) 1101 end)) 1102 else 1103 assertT 1104 (s = "al" orelse m <> BKPT andalso is_unconditional m) 1105 ("arm_parse_condition", "condition suffix not allowed") 1106 (write_token r >>- return (condition_to_word4 s)) 1107 | NONE => 1108 if thumb then 1109 read_itstate >>= (fn (itcond,l) => 1110 assertT (null l orelse hd l andalso is_AL itcond) 1111 ("arm_parse_condition", 1112 "condition suffix missing in IT block") 1113 (return 1114 (mk_word4 (if mem m coproc2 then 15 else 14)))) 1115 else 1116 return 1117 (mk_word4 (if is_unconditional m then 14 else 15)))) 1118end; 1119 1120val arm_parse_qualifier : instruction_mnemonic -> qualifier M = 1121 fn m => 1122 read_token >>= 1123 (fn t => 1124 case t 1125 of NONE => return Either 1126 | SOME h => 1127 (read_arch >>= (fn arch => 1128 read_thumb >>= (fn thumb => 1129 if Substring.compare (Substring.full "", h) = EQUAL then 1130 next_token >>- 1131 return (if thumb andalso m <> BL then 1132 if m <> BLX andalso not (has_thumb2 arch) then 1133 Narrow 1134 else 1135 Either 1136 else 1137 Wide) 1138 else if not (thumb andalso has_thumb2 arch) then 1139 other_errorT ("arm_parse_qualifier", 1140 "unexpected trailing characters: " ^ Substring.string h) 1141 else if Substring.compare (Substring.full ".n", h) = EQUAL then 1142 next_token >>-return Narrow 1143 else if Substring.compare (Substring.full ".w", h) = EQUAL then 1144 next_token >>- return Wide 1145 else 1146 other_errorT ("arm_parse_qualifier", 1147 "unexpected trailing characters: " ^ Substring.string h))))); 1148 1149val arm_parse_mnemonic : instruction_mnemonic M = 1150 read_token >>= 1151 (fn t => 1152 case t 1153 of NONE => syntax_errorT ("mnemonic", "end-of-input") 1154 | SOME h => 1155 let val lh = lower_substring h in 1156 case find_mnemonic lh 1157 of SOME (r,M) => 1158 (write_token r >>- 1159 (if M = IT then 1160 arm_parse_it_conditions >>- 1161 arm_parse_string "" >>- 1162 write_instruction 1163 (SOME {sflag = F, cond = mk_word4 14, 1164 qual = Narrow, mnemonic = M}) >>- 1165 return M 1166 else 1167 arm_parse_sflag M >>= (fn sflag => 1168 arm_parse_condition M >>= (fn cond => 1169 arm_parse_qualifier M >>= (fn qual => 1170 let val i = {sflag = sflag, cond = cond, 1171 qual = qual, mnemonic = M} 1172 in 1173 write_instruction (SOME i) >>- return M 1174 end))))) 1175 | NONE => syntax_errorT ("mnemonic", Substring.string h) 1176 end); 1177 1178(* ------------------------------------------------------------------------- *) 1179 1180fun pick_enc_ee thumb narrow_okay ee = 1181 if thumb then 1182 if narrow_okay then 1183 if ee then 1184 Encoding_ThumbEE_tm 1185 else 1186 Encoding_Thumb_tm 1187 else 1188 Encoding_Thumb2_tm 1189 else 1190 Encoding_ARM_tm; 1191 1192fun pick_enc thumb narrow_okay = 1193 if thumb then 1194 if narrow_okay then 1195 Encoding_Thumb_tm 1196 else 1197 Encoding_Thumb2_tm 1198 else 1199 Encoding_ARM_tm; 1200 1201fun pick_var_enc thumb q narrow_okay = 1202 if thumb then 1203 case q 1204 of Narrow => Encoding_Thumb_tm 1205 | Wide => Encoding_Thumb2_tm 1206 | Either => if narrow_okay then 1207 genvar ``:Encoding`` 1208 else 1209 Encoding_Thumb2_tm 1210 else 1211 Encoding_ARM_tm; 1212 1213(* ------------------------------------------------------------------------- *) 1214 1215fun dp_opcode AND = mk_word4 0 1216 | dp_opcode EOR = mk_word4 1 1217 | dp_opcode SUB = mk_word4 2 1218 | dp_opcode RSB = mk_word4 3 1219 | dp_opcode ADD = mk_word4 4 1220 | dp_opcode ADC = mk_word4 5 1221 | dp_opcode SBC = mk_word4 6 1222 | dp_opcode RSC = mk_word4 7 1223 | dp_opcode TST = mk_word4 8 1224 | dp_opcode TEQ = mk_word4 9 1225 | dp_opcode CMP = mk_word4 10 1226 | dp_opcode CMN = mk_word4 11 1227 | dp_opcode ORR = mk_word4 12 1228 | dp_opcode MOV = mk_word4 13 1229 | dp_opcode BIC = mk_word4 14 1230 | dp_opcode MVN = mk_word4 15 1231 | dp_opcode ORN = mk_word4 15 1232 | dp_opcode _ = raise ERR "dp_opcode" ""; 1233 1234fun swap_opcode m = 1235 case m 1236 of ADD => SUB | SUB => ADD 1237 | ADC => SBC | SBC => ADC 1238 | CMN => CMP | CMP => CMN 1239 | MOV => MVN | MVN => MOV 1240 | BIC => AND | AND => BIC 1241 | _ => raise ERR "swap_opcode" "cannot swap opcode"; 1242 1243fun int_one_comp tm = 1244 intSyntax.mk_negated (intSyntax.mk_plus (tm, intSyntax.one_tm)); 1245 1246fun mode1_immediate1 thumb m i = 1247 if thumb then 1248 (dp_opcode m,int_to_thumb2_mode1_immediate i) 1249 handle HOL_ERR {message,origin_function,...} => 1250 (dp_opcode (swap_opcode m),int_to_thumb2_mode1_immediate (int_one_comp i)) 1251 handle HOL_ERR _ => raise ERR origin_function message 1252 else 1253 (dp_opcode m,int_to_mode1_immediate i) 1254 handle HOL_ERR {message,origin_function,...} => 1255 (dp_opcode (swap_opcode m),int_to_mode1_immediate (int_one_comp i)) 1256 handle HOL_ERR _ => raise ERR origin_function message; 1257 1258fun mode1_immediate2 thumb m i = 1259 if thumb then 1260 (dp_opcode m,int_to_thumb2_mode1_immediate i) 1261 handle HOL_ERR {message,origin_function,...} => 1262 (dp_opcode (swap_opcode m), 1263 int_to_thumb2_mode1_immediate (intSyntax.mk_negated i)) 1264 handle HOL_ERR _ => raise ERR origin_function message 1265 else 1266 (dp_opcode m,int_to_mode1_immediate i) 1267 handle HOL_ERR {message,origin_function,...} => 1268 (dp_opcode (swap_opcode m), 1269 int_to_mode1_immediate (intSyntax.mk_negated i)) 1270 handle HOL_ERR _ => raise ERR origin_function message; 1271 1272fun mode1_register rm = mk_Mode1_register (mk_word5 0,mk_word2 0,rm); 1273 1274fun is_mode1_register mode1 = 1275 is_Mode1_register mode1 andalso 1276 let val (sh,typ,_) = dest_Mode1_register mode1 in 1277 sh ~~ mk_word5 0 andalso typ ~~ mk_word2 0 1278 end; 1279 1280fun shift_to_word2 LSL_shift = mk_word2 0 1281 | shift_to_word2 LSR_shift = mk_word2 1 1282 | shift_to_word2 ASR_shift = mk_word2 2 1283 | shift_to_word2 ROR_shift = mk_word2 3 1284 | shift_to_word2 RRX_shift = mk_word2 3; 1285 1286fun shift_type LSL = shift_to_word2 LSL_shift 1287 | shift_type ASR = shift_to_word2 ASR_shift 1288 | shift_type LSR = shift_to_word2 LSR_shift 1289 | shift_type ROR = shift_to_word2 ROR_shift 1290 | shift_type RRX = shift_to_word2 RRX_shift 1291 | shift_type _ = raise ERR "shift_type" ""; 1292 1293val arm_parse_shift : shift M = 1294 read_token >>= 1295 (fn h => 1296 case h 1297 of NONE => syntax_errorT ("shift", "end-of-input") 1298 | SOME s => 1299 (next_token >>- 1300 (case lower_string s 1301 of "asr" => return ASR_shift 1302 | "lsl" => return LSL_shift 1303 | "lsr" => return LSR_shift 1304 | "ror" => return ROR_shift 1305 | "rrx" => return RRX_shift 1306 | _ => syntax_errorT ("shift",Substring.string s)))); 1307 1308val arm_parse_mode1_shift : term -> term M = 1309 fn rm => 1310 arm_parse_shift >>= (fn s => 1311 let val stype = shift_to_word2 s 1312 val szero = mk_word5 0 1313 in 1314 if s = RRX_shift then 1315 return (mk_Mode1_register (szero,stype,rm)) 1316 else 1317 tryT arm_parse_constant 1318 (fn i => 1319 let val shift32 = i ~~ ``32i`` 1320 val imm5 = if shift32 then 1321 szero 1322 else 1323 uint_to_word ``:5`` i 1324 val stype = if not shift32 andalso imm5 ~~ szero then 1325 mk_word2 0 1326 else 1327 stype 1328 in 1329 assertT (not shift32 orelse mem s [LSR_shift,ASR_shift]) 1330 ("arm_parse_mode1_shift", "cannot shift by 32") 1331 (return (mk_Mode1_register (imm5,stype,rm))) 1332 end handle HOL_ERR {message,...} => 1333 other_errorT ("arm_parse_mode1_shift", message)) 1334 (fn _ => 1335 arm_parse_register >>= (fn rs => 1336 return (mk_Mode1_register_shifted_register (rs,stype,rm)))) 1337 end); 1338 1339val arm_parse_comma_mode1_shift : term -> term M = 1340 fn rm => 1341 tryT arm_parse_comma 1342 (fn _ => arm_parse_mode1_shift rm) 1343 (fn _ => return (mode1_register rm)); 1344 1345fun assertT_thumb s q narrow_okay wide_okay f = 1346 assertT (case q 1347 of Narrow => narrow_okay 1348 | Either => narrow_okay orelse wide_okay 1349 | Wide => wide_okay) 1350 (s,"not a valid Thumb instruction") f; 1351 1352(* ....................................................................... *) 1353 1354fun add_sub_literal m (rd,i) = 1355 read_thumb >>= (fn thumb => 1356 if thumb then 1357 read_qualifier >>= (fn q => 1358 let val v = sint_of_term i 1359 val imm12 = mk_word12 (Int.abs v) 1360 val narrow_okay = q <> Wide andalso narrow_register rd andalso 1361 v mod 4 = 0 andalso 1362 if m = ADD then 1363 0 <= v andalso v <= 1020 1364 else 1365 ~1020 <= v andalso v <= 0 1366 val wide_okay = ~4095 <= v andalso v <= 4095 1367 val add = narrow_okay orelse 1368 if 0 <= v andalso not (i ~~ ``-0i``) then 1369 m = ADD 1370 else 1371 m <> ADD 1372 in 1373 assertT_thumb "add_sub_literal" q narrow_okay wide_okay 1374 (return (pick_enc true narrow_okay, 1375 mk_Add_Sub (mk_bool add,mk_word4 15,rd,imm12))) 1376 end handle HOL_ERR {message,...} => 1377 other_errorT ("arm_parse_add_sub", message)) 1378 else 1379 let val (opc,imm12) = mode1_immediate2 false m i in 1380 return (Encoding_ARM_tm, 1381 mk_Add_Sub (mk_bool (opc ~~ mk_word4 4),mk_word4 15,rd,imm12)) 1382 end handle HOL_ERR {message,...} => 1383 other_errorT ("arm_parse_add_sub", message)); 1384 1385fun narrow_okay_imm m i (rd,rn) = 1386let val v = sint_of_term i handle HOL_ERR _ => 1024 in 1387 if m = ADD orelse m = SUB then 1388 if is_SP rn then 1389 v mod 4 = 0 andalso 1390 if is_SP rd then 1391 ~508 <= v andalso v <= 508 1392 else 1393 narrow_register rd andalso ~1020 <= v andalso v <= 1020 andalso 1394 fst (mode1_immediate2 false m i) ~~ dp_opcode ADD 1395 else 1396 narrow_register rn andalso 1397 if rd ~~ rn then 1398 ~255 <= v andalso v <= 255 1399 else 1400 ~7 <= v andalso v <= 7 1401 else 1402 m = RSB andalso v = 0 andalso narrow_registers [rd,rn] 1403end 1404 1405fun narrow_okay_reg m q sflag has_thumb2 InITBlock OutsideOrLastInITBlock 1406 (rd,rn,rm,mode1) = 1407 q <> Wide andalso 1408 is_mode1_register mode1 andalso 1409 (case m 1410 of ADD => if narrow_registers [rd,rn] then 1411 sflag = not InITBlock andalso narrow_register rm orelse 1412 not sflag andalso rd ~~ rn andalso 1413 (not (narrow_register rm) orelse has_thumb2) 1414 else 1415 not sflag andalso rd ~~ rn andalso 1416 (not (is_PC rd) orelse OutsideOrLastInITBlock) 1417 | SUB => sflag = not InITBlock andalso narrow_registers [rd,rn,rm] 1418 | RSC => false 1419 | RSB => false 1420 | ORN => false 1421 | _ => sflag = not InITBlock andalso rd ~~ rn andalso 1422 narrow_registers [rn,rm]); 1423 1424fun wide_okay_reg m mode1 = 1425 m <> RSC andalso not (is_Mode1_register_shifted_register mode1); 1426 1427fun data_processing_immediate m (rd,rn,i) = 1428 read_sflag >>= (fn sflag => 1429 if (m = ADD orelse m = SUB) andalso is_F sflag andalso is_PC rn then 1430 add_sub_literal m (rd,i) 1431 else 1432 read_thumb >>= (fn thumb => 1433 if thumb then 1434 read_qualifier >>= (fn q => 1435 read_InITBlock >>= (fn InITBlock => 1436 let val thumb_sflag = mk_bool (not InITBlock andalso 1437 not (is_SP rn)) 1438 val narrow_okay = q <> Wide andalso thumb_sflag ~~ sflag 1439 andalso narrow_okay_imm m i (rd,rn) 1440 val enc = pick_enc true narrow_okay 1441 val (opc,imm12) = 1442 mode1_immediate2 (enc ~~ Encoding_Thumb2_tm) m i 1443 in 1444 assertT_thumb "data_processing_immediate" q narrow_okay (m <> RSC) 1445 (return (enc, 1446 mk_Data_Processing 1447 (opc,sflag,rn,rd,mk_Mode1_immediate imm12))) 1448 end handle HOL_ERR {message,...} => 1449 other_errorT ("data_processing_immediate", message))) 1450 else 1451 assertT (m <> ORN) 1452 ("data_processing_immediate", "not a valid ARM instruction") 1453 (let val (opc,imm12) = mode1_immediate2 false m i in 1454 return (Encoding_ARM_tm, 1455 mk_Data_Processing (opc,sflag,rn,rd,mk_Mode1_immediate imm12)) 1456 end))); 1457 1458fun data_processing_register m (rd,rn,rm,mode1) = 1459 read_thumb >>= (fn thumb => 1460 read_sflag >>= (fn sflag => 1461 if thumb then 1462 read_arch >>= (fn arch => 1463 read_qualifier >>= (fn q => 1464 read_InITBlock >>= (fn InITBlock => 1465 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 1466 let val mode1' = mode1_register rn 1467 val thumb_test = narrow_okay_reg m q (is_T sflag) (has_thumb2 arch) 1468 InITBlock OutsideOrLastInITBlock 1469 val narrow_okay = thumb_test (rd,rn,rm,mode1) 1470 val swap_okay = not narrow_okay andalso 1471 m <> SUB andalso is_mode1_register mode1 andalso 1472 thumb_test (rd,rm,rn,mode1') 1473 val wide_okay = wide_okay_reg m mode1 1474 val (mode1,rn) = if swap_okay then (mode1',rm) else (mode1,rn) 1475 val narrow_okay = narrow_okay orelse swap_okay 1476 in 1477 assertT_thumb "data_processing_register" q narrow_okay wide_okay 1478 (return (pick_enc true narrow_okay, 1479 mk_Data_Processing (dp_opcode m,sflag,rn,rd,mode1))) 1480 end handle HOL_ERR {message,...} => 1481 other_errorT ("data_processing_register", message))))) 1482 else 1483 assertT (m <> ORN) 1484 ("data_processing_immediate", "not a valid ARM instruction") 1485 (return (Encoding_ARM_tm, 1486 mk_Data_Processing (dp_opcode m,sflag,rn,rd,mode1))))); 1487 1488fun is_data_processing3 m = 1489 case m 1490 of ADD => true | SUB => true | RSB => true | RSC => true | ORN => true 1491 | AND => true | EOR => true | ADC => true | SBC => true | ORR => true 1492 | BIC => true | _ => false; 1493 1494val arm_parse_data_processing3 : instruction_mnemonic -> (term * term) M = 1495 fn m => 1496 arm_parse_register >>= (fn rd => 1497 arm_parse_comma >>- 1498 tryT arm_parse_constant 1499 (fn i => data_processing_immediate m (rd,rd,i)) 1500 (fn _ => 1501 arm_parse_register >>= (fn rn => 1502 tryT arm_parse_comma 1503 (fn _ => 1504 tryT arm_parse_constant 1505 (fn i => data_processing_immediate m (rd,rn,i)) 1506 (fn _ => 1507 tryT arm_parse_register 1508 (fn rm => 1509 arm_parse_comma_mode1_shift rm >>= (fn mode1 => 1510 data_processing_register m (rd,rn,rm,mode1))) 1511 (fn _ => 1512 (tryT (arm_parse_mode1_shift rn) return 1513 (fn _ => return (mode1_register rn))) >>= 1514 (fn mode1 => 1515 data_processing_register m (rd,rd,rn,mode1))))) 1516 (fn _ => 1517 data_processing_register m (rd,rd,rn,mode1_register rn))))); 1518 1519(* ....................................................................... *) 1520 1521fun narrow_okay_imm m i rdn = 1522let val v = sint_of_term i handle HOL_ERR _ => 1024 in 1523 (m = CMP orelse m = MOV) andalso 1524 0 <= v andalso v <= 255 andalso 1525 narrow_register rdn 1526end; 1527 1528fun narrow_okay_reg m (rdn,rm,mode1) = 1529 if m = MOV then 1530 if is_Mode1_register_shifted_register mode1 then 1531 let val (rs,typ,_) = dest_Mode1_register_shifted_register mode1 in 1532 rdn ~~ rm andalso narrow_registers [rdn,rs] 1533 end 1534 else 1535 let val (imm5,typ,_) = dest_Mode1_register mode1 in 1536 if narrow_registers [rdn,rm] then 1537 typ !~ mk_word2 3 1538 else 1539 typ ~~ mk_word2 0 andalso imm5 ~~ mk_word5 0 1540 end 1541 else 1542 m <> TEQ andalso is_mode1_register mode1 andalso narrow_registers [rdn,rm]; 1543 1544fun wide_okay_reg m (rm,mode1) = 1545 not (is_PC rm) andalso (m = MOV orelse is_Mode1_register mode1); 1546 1547fun move_test_immediate m (rdn,i) = 1548 read_thumb >>= (fn thumb => 1549 read_sflag >>= (fn sflag => 1550 if thumb then 1551 read_qualifier >>= (fn q => 1552 read_InITBlock >>= (fn InITBlock => 1553 let val thumb_sflag = mk_bool (not InITBlock orelse 1554 m <> MOV andalso m <> MVN) 1555 val narrow_okay = q <> Wide andalso thumb_sflag ~~ sflag andalso 1556 narrow_okay_imm m i rdn 1557 val enc = pick_enc true narrow_okay 1558 val (opc,imm12) = mode1_immediate2 (enc ~~ Encoding_Thumb2_tm) m i 1559 val r15 = mk_word4 15 1560 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r15) else (r15,rdn) 1561 in 1562 assertT_thumb "move_test_immediate" q narrow_okay true 1563 (return (enc, 1564 mk_Data_Processing (opc,sflag,rn,rd,mk_Mode1_immediate imm12))) 1565 end handle HOL_ERR {message,...} => 1566 other_errorT ("data_processing_immediate", message))) 1567 else 1568 let val (opc,imm12) = mode1_immediate2 false m i 1569 val r0 = mk_word4 0 1570 val (rd,rn) = if m = MOV orelse m = MVN then (rdn,r0) else (r0,rdn) 1571 in 1572 return (Encoding_ARM_tm, 1573 mk_Data_Processing (opc,sflag,rn,rd,mk_Mode1_immediate imm12)) 1574 end)); 1575 1576fun move_test_reg m (rdn,rm,mode1) = 1577 read_thumb >>= (fn thumb => 1578 read_sflag >>= (fn sflag => 1579 if thumb then 1580 read_qualifier >>= (fn q => 1581 read_InITBlock >>= (fn InITBlock => 1582 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 1583 arch_version >>= (fn version => 1584 let val thumb_sflag = mk_bool (m <> MOV andalso m <> MVN orelse 1585 not InITBlock andalso 1586 narrow_registers [rdn,rm] andalso 1587 (m <> MOV orelse version < 6 orelse 1588 is_T sflag)) 1589 val narrow_okay = q <> Wide andalso thumb_sflag ~~ sflag andalso 1590 (OutsideOrLastInITBlock orelse not (is_PC rdn)) 1591 andalso narrow_okay_reg m (rdn,rm,mode1) 1592 val wide_okay = wide_okay_reg m (rm,mode1) 1593 val r15 = mk_word4 15 1594 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r15) else (r15,rdn) 1595 in 1596 assertT_thumb "data_processing_register" q narrow_okay wide_okay 1597 (return (pick_enc true narrow_okay, 1598 mk_Data_Processing (dp_opcode m,sflag,rn,rd,mode1))) 1599 end handle HOL_ERR {message,...} => 1600 other_errorT ("data_processing_register", message))))) 1601 else 1602 let val r0 = mk_word4 0 1603 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r0) else (r0,rdn) 1604 in 1605 return (Encoding_ARM_tm, 1606 mk_Data_Processing (dp_opcode m,sflag,rn,rd,mode1)) 1607 end)); 1608 1609fun is_data_processing2 m = 1610 case m 1611 of MOV => true | CMP => true | TST => true | MVN => true | CMN => true 1612 | TEQ => true | _ => false; 1613 1614val arm_parse_data_processing2 : instruction_mnemonic -> (term * term) M = 1615 fn m => 1616 arm_parse_register >>= (fn rdn => 1617 arm_parse_comma >>- 1618 tryT arm_parse_constant 1619 (fn i => move_test_immediate m (rdn,i)) 1620 (fn _ => 1621 arm_parse_register >>= (fn rm => 1622 arm_parse_comma_mode1_shift rm >>= (fn mode1 => 1623 move_test_reg m (rdn,rm,mode1))))); 1624 1625(* ....................................................................... *) 1626 1627fun shift_immediate m thumb q InITBlock sflag (rd,rm,i) = 1628let val v = sint_of_term i 1629 val wide_okay = 1 <= v andalso v <= (if mem m [LSR,ASR] then 32 else 31) 1630 val narrow_okay = q <> Wide andalso wide_okay andalso m <> ROR andalso 1631 mk_bool InITBlock !~ sflag andalso 1632 narrow_registers [rd,rm] 1633 val imm5 = mk_word5 (if v = 32 then 0 else Int.abs v) 1634 val rn = mk_word4 (if thumb then 15 else 0) 1635in 1636 assertT wide_okay 1637 ("shift_immediate", 1638 "shift must be in range 1-31 (lsl and ror) or 1-32 (lsr and asr)") 1639 (assertT_thumb "shift_immediate" q narrow_okay wide_okay 1640 (return (pick_enc thumb narrow_okay, 1641 mk_Data_Processing (dp_opcode MOV,sflag,rn,rd, 1642 mk_Mode1_register (imm5,shift_type m,rm))))) 1643end handle HOL_ERR {message,...} => other_errorT ("shift_immediate", message); 1644 1645fun shift_register m thumb q InITBlock sflag (rd,rn,rm) = 1646let val narrow_okay = q <> Wide andalso rd ~~ rn andalso 1647 mk_bool InITBlock !~ sflag andalso 1648 narrow_registers [rd,rn,rm] 1649 val rn' = mk_word4 (if thumb then 15 else 0) 1650in 1651 assertT_thumb "shift_register" q narrow_okay true 1652 (return (pick_enc thumb narrow_okay, 1653 mk_Data_Processing (dp_opcode MOV,sflag,rn',rd, 1654 mk_Mode1_register_shifted_register (rm,shift_type m,rn)))) 1655end handle HOL_ERR {message,...} => other_errorT ("shift_register", message); 1656 1657val arm_parse_mov_shift : instruction_mnemonic -> (term * term) M = 1658 fn m => 1659 arm_parse_register >>= (fn rd => 1660 arm_parse_comma >>- 1661 read_thumb >>= (fn thumb => 1662 read_qualifier >>= (fn q => 1663 read_sflag >>= (fn sflag => 1664 read_InITBlock >>= (fn InITBlock => 1665 tryT arm_parse_constant 1666 (fn i => shift_immediate m thumb q InITBlock sflag (rd,rd,i)) 1667 (fn _ => 1668 arm_parse_register >>= (fn rn => 1669 tryT arm_parse_comma 1670 (fn _ => 1671 tryT arm_parse_constant 1672 (fn i => shift_immediate m thumb q InITBlock sflag (rd,rn,i)) 1673 (fn _ => 1674 arm_parse_register >>= (fn rm => 1675 shift_register m thumb q InITBlock sflag (rd,rn,rm)))) 1676 (fn _ => shift_register m thumb q InITBlock sflag (rd,rd,rn))))))))); 1677 1678val arm_parse_rrx : (term * term) M = 1679 thumb2_or_arm_okay "arm_parse_rrx" 1680 (fn enc => 1681 arm_parse_register >>= (fn rd => 1682 tryT arm_parse_comma 1683 (fn _ => arm_parse_register) 1684 (fn _ => return rd) >>= 1685 (fn rm => 1686 read_sflag >>= (fn sflag => 1687 return (enc, 1688 mk_Data_Processing (dp_opcode MOV,sflag,mk_word4 0,rd, 1689 mk_Mode1_register (mk_word5 0,shift_type RRX,rm))))))); 1690 1691(* ------------------------------------------------------------------------- *) 1692 1693val arm_parse_mov_halfword : term -> (term * term) M = 1694 fn high => 1695 need_t2 "arm_parse_mov_halfword" 1696 (thumb2_or_arm_okay "arm_parse_mov_halfword" 1697 (fn enc => 1698 arm_parse_register >>= (fn rd => 1699 arm_parse_comma >>- 1700 arm_parse_constant >>= (fn i => 1701 let val imm16 = uint_to_word ``:16`` i in 1702 return (enc,mk_Move_Halfword (high,rd,imm16)) 1703 end handle HOL_ERR {message,...} => 1704 other_errorT ("arm_parse_mov_halfword", message))))); 1705 1706val arm_parse_addw_subw : term -> (term * term) M = 1707 fn add => 1708 thumb2_okay "arm_parse_addw_subw" 1709 (arm_parse_register >>= (fn rd => 1710 arm_parse_comma >>- 1711 tryT arm_parse_register 1712 (fn rn => arm_parse_comma >>- return rn) 1713 (fn _ => return rd) >>= (fn rn => 1714 arm_parse_constant >>= (fn i => 1715 let val (add,i) = if intSyntax.is_negated i then 1716 (if is_T add then F else T, 1717 intSyntax.dest_negated i) 1718 else 1719 (add,i) 1720 val imm12 = uint_to_word ``:12`` i 1721 in 1722 return (Encoding_Thumb2_tm, mk_Add_Sub (add,rn,rd,imm12)) 1723 end handle HOL_ERR {message,...} => 1724 other_errorT ("arm_parse_addw_subw", message))))); 1725 1726val arm_parse_adr : (term * term) M = 1727 arm_parse_register >>= (fn rd => 1728 arm_parse_comma >>- 1729 arm_parse_branch_offset >>= (fn i => 1730 read_thumb >>= (fn thumb => 1731 if is_var i then 1732 read_qualifier >>= (fn q => 1733 return 1734 (pick_var_enc thumb q (narrow_register rd), 1735 mk_Add_Sub (boolSyntax.arb,mk_word4 15,rd,cast_var ``:word12`` i))) 1736 else 1737 if thumb then 1738 read_qualifier >>= (fn q => 1739 let val offset = sint_of_term i - 4 1740 val narrow_okay = q <> Wide andalso narrow_register rd andalso 1741 offset mod 4 = 0 andalso 1742 0 <= offset andalso offset <= 1020 1743 val wide_okay = q <> Narrow andalso 1744 ~4095 <= offset andalso offset <= 4095 1745 in 1746 if narrow_okay orelse wide_okay then 1747 return 1748 (if narrow_okay then Encoding_Thumb_tm else Encoding_Thumb2_tm, 1749 mk_Add_Sub (mk_bool (0 <= offset andalso not (i ~~ ``-0i``)), 1750 mk_word4 15,rd,mk_word12 offset)) 1751 else 1752 other_errorT ("arm_parse_adr", 1753 "bad register, unaligned or offset beyond permitted range") 1754 end handle HOL_ERR {message,...} => 1755 other_errorT ("arm_parse_adr", message)) 1756 else 1757 let open intSyntax 1758 val offset = eval (mk_minus(i, ``8i``)) 1759 val absoffset = eval (mk_absval offset) 1760 in 1761 return (Encoding_ARM_tm, 1762 mk_Add_Sub (mk_bool (not (is_negated offset)),mk_word4 15,rd, 1763 int_to_mode1_immediate absoffset)) 1764 end handle HOL_ERR {message, ...} => 1765 other_errorT ("arm_parse_adr", message)))); 1766 1767(* ------------------------------------------------------------------------- *) 1768 1769val arm_parse_branch_target : (term * term) M = 1770 arm_parse_branch_offset >>= (fn i => 1771 read_thumb >>= (fn thumb => 1772 read_qualifier >>= (fn q => 1773 if is_var i then 1774 return (pick_var_enc thumb q true, 1775 mk_Branch_Target (cast_var ``:word24`` i)) 1776 else 1777 if thumb then 1778 read_cond >>= (fn cond => 1779 let val offset = sint_of_term i - 4 1780 val narrow_okay = q <> Wide andalso 1781 if is_var cond orelse is_AL cond then 1782 ~2048 <= offset andalso offset <= 2046 1783 else 1784 ~256 <= offset andalso offset <= 254 1785 val wide_okay = if is_var cond orelse is_AL cond then 1786 ~16777216 <= offset andalso offset <= 16777214 1787 else 1788 ~1048576 <= offset andalso offset <= 1048574 1789 in 1790 assertT (offset mod 2 = 0) 1791 ("arm_parse_branch_target", 1792 "branch offset not half-word aligned") 1793 (assertT_thumb "arm_parse_branch_target" q narrow_okay wide_okay 1794 (return (pick_enc true narrow_okay, 1795 mk_Branch_Target (offset_to_imm24 (offset div 2))))) 1796 end handle HOL_ERR {message,...} => 1797 other_errorT ("arm_parse_branch_target", message)) 1798 else 1799 let val offset = sint_of_term i - 8 in 1800 assertT (offset mod 4 = 0) 1801 ("arm_parse_branch_target", "branch offset not word aligned") 1802 (assertT (~33554432 <= offset andalso offset <= 33554428) 1803 ("arm_parse_branch_target", "offset beyond permitted range") 1804 (return (Encoding_ARM_tm, 1805 mk_Branch_Target (offset_to_imm24 (offset div 4))))) 1806 end handle HOL_ERR {message,...} => 1807 other_errorT ("arm_parse_branch_target", message)))); 1808 1809val arm_parse_branch_link : (term * term) M = 1810 arm_parse_branch_offset >>= (fn i => 1811 read_thumb >>= (fn thumb => 1812 if thumb then 1813 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 1814 read_qualifier >>= (fn q => 1815 assertT (q <> Narrow andalso OutsideOrLastInITBlock) 1816 ("arm_parse_branch_link", 1817 "must be wide, and outside or last in IT block") 1818 (if is_var i then 1819 return (Encoding_Thumb2_tm, 1820 mk_Branch_Link_Exchange_Immediate 1821 (boolSyntax.arb,F,cast_var ``:word24`` i)) 1822 else 1823 let val offset = sint_of_term i - 4 1824 val H = mk_bool ((offset div 2) mod 2 = 1) 1825 in 1826 assertT (offset mod 2 = 0) 1827 ("arm_parse_branch_target", 1828 "branch offset not half-word aligned") 1829 (assertT (~16777216 <= offset andalso offset <= 16777214) 1830 ("arm_parse_branch_target", "offset beyond permitted range") 1831 (return (Encoding_Thumb2_tm, 1832 mk_Branch_Link_Exchange_Immediate 1833 (H,F,offset_to_imm24 (offset div 4))))) 1834 end handle HOL_ERR {message,...} => 1835 other_errorT ("arm_parse_branch_link", message)))) 1836 else 1837 if is_var i then 1838 return (Encoding_ARM_tm, 1839 mk_Branch_Link_Exchange_Immediate 1840 (boolSyntax.arb,T,cast_var ``:word24`` i)) 1841 else 1842 let val offset = sint_of_term i - 8 in 1843 assertT (offset mod 4 = 0) 1844 ("arm_parse_branch_target", "branch offset not word aligned") 1845 (assertT (~33554432 <= offset andalso offset <= 33554428) 1846 ("arm_parse_branch_target", "offset beyond permitted range") 1847 (return (Encoding_ARM_tm, 1848 mk_Branch_Link_Exchange_Immediate 1849 (F,T,offset_to_imm24 (offset div 4))))) 1850 end handle HOL_ERR {message,...} => 1851 other_errorT ("arm_parse_branch_link", message))); 1852 1853val arm_parse_branch_link_exchange : (term * term) M = 1854 need_v5 "arm_parse_branch_link_exchange" 1855 (tryT arm_parse_register 1856 (fn rm => 1857 read_thumb >>= (fn thumb => 1858 if thumb then 1859 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 1860 read_qualifier >>= (fn q => 1861 assertT (q <> Wide andalso OutsideOrLastInITBlock) 1862 ("arm_parse_branch_link_exchange", 1863 "must be narrow, and outside or last in IT block") 1864 (return (Encoding_Thumb_tm, 1865 mk_Branch_Link_Exchange_Register rm)))) 1866 else 1867 return (Encoding_ARM_tm, mk_Branch_Link_Exchange_Register rm))) 1868 (fn _ => 1869 arm_parse_branch_offset >>= (fn i => 1870 read_thumb >>= (fn thumb => 1871 if thumb then 1872 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 1873 read_qualifier >>= (fn q => 1874 assertT (q <> Narrow andalso OutsideOrLastInITBlock) 1875 ("arm_parse_branch_target", 1876 "must be wide, and outside or last in IT block") 1877 (if is_var i then 1878 return (Encoding_Thumb2_tm, 1879 mk_Branch_Link_Exchange_Immediate 1880 (F,T,cast_var ``:word24`` i)) 1881 else 1882 let val offset = sint_of_term i - 4 in 1883 assertT (offset mod 4 = 0) 1884 ("arm_parse_branch_target", 1885 "branch offset not word aligned") 1886 (assertT (~16777216 <= offset andalso offset <= 16777212) 1887 ("arm_parse_branch_target", 1888 "offset beyond permitted range") 1889 (return (Encoding_Thumb2_tm, 1890 mk_Branch_Link_Exchange_Immediate 1891 (F,T,offset_to_imm24 (offset div 4))))) 1892 end handle HOL_ERR {message,...} => 1893 other_errorT ("arm_parse_branch_link_exchange", message)))) 1894 else 1895 read_cond >>= (fn cond => 1896 assertT (is_AL cond) 1897 ("arm_parse_branch_link_exchange", "must be uncoditional") 1898 (write_cond (mk_word4 15) >>- 1899 (if is_var i then 1900 return (Encoding_ARM_tm, 1901 mk_Branch_Link_Exchange_Immediate 1902 (boolSyntax.arb,F,cast_var ``:word24`` i)) 1903 else 1904 let val offset = sint_of_term i - 8 1905 val H = mk_bool ((offset div 2) mod 2 = 1) 1906 in 1907 assertT (offset mod 2 = 0) 1908 ("arm_parse_branch_target", 1909 "branch offset not half-word aligned") 1910 (assertT (~33554432 <= offset andalso offset <= 33554430) 1911 ("arm_parse_branch_target", 1912 "offset beyond permitted range") 1913 (return (Encoding_ARM_tm, 1914 mk_Branch_Link_Exchange_Immediate 1915 (H,F,offset_to_imm24 (offset div 4))))) 1916 end handle HOL_ERR {message,...} => 1917 other_errorT 1918 ("arm_parse_branch_link_exchange", message)))))))); 1919 1920val arm_parse_bx : (term * term) M = 1921 thumb_or_arm_okay (fn enc => 1922 arm_parse_register >>= (fn rm => 1923 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 1924 assertT (enc ~~ Encoding_ARM_tm orelse OutsideOrLastInITBlock) 1925 ("arm_parse_bx", "must be outside or last in IT block") 1926 (return (enc,mk_Branch_Exchange rm))))); 1927 1928val arm_parse_setend : (term * term) M = 1929 need_v6 "arm_parse_setend" 1930 (thumb_or_arm_okay 1931 (fn enc => 1932 tryT (arm_parse_string "be") (K (return T)) (fn _ => 1933 arm_parse_string "le" >>- return F) >>= (fn bigend => 1934 return (enc,mk_Set_Endianness bigend)))); 1935 1936val arm_parse_cbz_cbnz : term -> (term * term) M = 1937 fn nonzero => 1938 thumb2_okay "arm_parse_cnz" 1939 (read_qualifier >>= (fn q => 1940 assertT (q <> Wide) 1941 ("arm_parse_cbz_cbnz", "wide version not available") 1942 (arm_parse_register >>= (fn rn => 1943 assertT (narrow_register rn) 1944 ("arm_parse_cbz_cbnz", "register must be r0-r7") 1945 (arm_parse_comma >>- 1946 arm_parse_branch_offset >>= (fn i => 1947 if is_var i then 1948 return (Encoding_Thumb_tm, 1949 mk_Compare_Branch (nonzero,cast_var ``:word6`` i, 1950 mk_word3 (uint_of_word rn))) 1951 else 1952 let val offset = sint_of_term i - 4 in 1953 assertT (offset mod 2 = 0) 1954 ("arm_parse_cbz_cbnz", "offset not half-word aligned") 1955 (assertT (0 <= offset andalso offset <= 126) 1956 ("arm_parse_cbz_cbnz", "offset beyond permitted range") 1957 (return (Encoding_Thumb_tm, 1958 mk_Compare_Branch (nonzero, 1959 mk_word6 (Int.abs (offset div 2)), 1960 mk_word3 (uint_of_word rn))))) 1961 end handle HOL_ERR {message,...} => 1962 other_errorT ("arm_parse_cbz_cbnz", message))))))); 1963 1964val arm_parse_clz : (term * term) M = 1965 need_v5 "arm_parse_clz" 1966 (thumb2_or_arm_okay "arm_parse_clz" 1967 (fn enc => 1968 arm_parse_register >>= (fn rd => 1969 arm_parse_comma >>- 1970 arm_parse_register >>= (fn rm => 1971 return (enc,mk_Count_Leading_Zeroes (rd,rm)))))); 1972 1973val arm_parse_clrex : (term * term) M = 1974 read_thumb >>= (fn thumb => 1975 read_qualifier >>= (fn q => 1976 arch_okay ("arm_parse_clrex", "not supported by architecture") 1977 (fn a => if thumb then 1978 q <> Narrow andalso version_number a >= 7 1979 else 1980 a = ARMv6K orelse version_number a >= 7) 1981 (return (if thumb then Encoding_Thumb2_tm else Encoding_ARM_tm, 1982 mk_Miscellaneous Clear_Exclusive_tm)))); 1983 1984local 1985 fun mk_it_mask (cond,l) = 1986 let val cond0 = wordsSyntax.mk_index (cond,numSyntax.zero_tm) |> eval 1987 val (c0,nc0) = if is_T cond0 then (1,0) else (0,1) 1988 in 1989 mk_word4 (list_to_int 1990 (case l 1991 of [] => [1 , 0 , 0 , 0] 1992 | [true] => [c0 , 1 , 0 , 0] 1993 | [false] => [nc0, 1 , 0 , 0] 1994 | [true,true] => [c0 , c0 , 1 , 0] 1995 | [false,true] => [nc0, c0 , 1 , 0] 1996 | [true,false] => [c0 , nc0, 1 , 0] 1997 | [false,false] => [nc0, nc0, 1 , 0] 1998 | [true,true,true] => [c0 , c0 , c0 , 1] 1999 | [false,true,true] => [nc0, c0 , c0 , 1] 2000 | [true,false,true] => [c0 , nc0, c0 , 1] 2001 | [false,false,true] => [nc0, nc0, c0 , 1] 2002 | [true,true,false] => [c0 , c0 , nc0, 1] 2003 | [false,true,false] => [nc0, c0 , nc0, 1] 2004 | [true,false,false] => [c0 , nc0, nc0, 1] 2005 | [false,false,false] => [nc0, nc0, nc0, 1] 2006 | _ => raise ERR "mk_it_mask" "")) 2007 end 2008 2009 fun is_then "then" = true 2010 | is_then "t" = true 2011 | is_then "else" = false 2012 | is_then "e" = false 2013 | is_then _ = raise ERR "mk_itstate" "unexpected input" 2014 2015in 2016 fun calc_itstate (c,s) = let 2017 val toks = String.tokens (equal #"-") s 2018 val l = Lib.mapfilter is_then toks 2019 val itstate = 2020 case l 2021 of [] => mk_word8 0 2022 | (b::t) => let 2023 val cond = condition_to_word4 c 2024 val mask = mk_it_mask (cond,t) 2025 val cond = if b then 2026 cond 2027 else 2028 wordsSyntax.mk_word_xor (mk_word4 1,cond) 2029 in 2030 eval (wordsSyntax.mk_word_concat (cond,mask)) 2031 end 2032 in 2033 uint_of_word itstate 2034 end 2035 2036 val arm_parse_it : (term * term) M = 2037 need_t2 "arm_parse_it" 2038 (read_thumb >>= (fn thumb => 2039 read_qualifier >>= (fn q => 2040 assertT (thumb andalso q <> Wide) 2041 ("arm_parse_it", "only available as narrow thumb instruction") 2042 (read_token >>= 2043 (fn h => 2044 case h 2045 of NONE => syntax_errorT ("condition","end-of_input") 2046 | SOME s => 2047 case find_condition s 2048 of SOME (c,r) => 2049 if Substring.compare (r,Substring.full "") = EQUAL 2050 then 2051 let val cond = condition_to_word4 c in 2052 read_itstate >>= (fn (_,l) => 2053 assertT (not (is_AL cond) orelse Lib.all I l) 2054 ("arm_parse_it", 2055 "Cannot have -else- cases for AL condition") 2056 (write_itcond cond >>- 2057 next_token >>- 2058 tryT arm_parse_exclaim 2059 (K (return boolSyntax.arb)) 2060 (K (return Encoding_Thumb_tm)) >>= 2061 (fn enc => 2062 return (enc, 2063 mk_If_Then 2064 (cond,mk_it_mask (cond,tl l)))))) 2065 end 2066 else 2067 syntax_errorT ("condition",Substring.string s) 2068 | NONE => 2069 syntax_errorT ("condition",Substring.string s)))))); 2070end; 2071 2072val arm_parse_tbb : (term * term) M = 2073 thumb2_okay "arm_parse_tbb" 2074 (arm_parse_lsquare >>- 2075 arm_parse_register >>= (fn rn => 2076 arm_parse_comma >>- 2077 arm_parse_register >>= (fn rm => 2078 arm_parse_rsquare >>- 2079 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 2080 assertT OutsideOrLastInITBlock 2081 ("arm_parse_tbb", "must be outside or last in IT block") 2082 (return (Encoding_Thumb2_tm,mk_Table_Branch_Byte (rn,F,rm))))))); 2083 2084val arm_parse_tbh : (term * term) M = 2085 thumb2_okay "arm_parse_tbb" 2086 (arm_parse_lsquare >>- 2087 arm_parse_register >>= (fn rn => 2088 arm_parse_comma >>- 2089 arm_parse_register >>= (fn rm => 2090 arm_parse_comma >>- 2091 arm_parse_string "lsl" >>- 2092 arm_parse_constant >>= (fn i => 2093 let val v = sint_of_term i in 2094 if v = 1 then 2095 arm_parse_rsquare >>- 2096 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 2097 assertT OutsideOrLastInITBlock 2098 ("arm_parse_tbh", "must be outside or last in IT block") 2099 (return (Encoding_Thumb2_tm,mk_Table_Branch_Byte (rn,T,rm)))) 2100 else 2101 syntax_errorT ("#1","#" ^ term_to_string i) 2102 end handle HOL_ERR {message,...} => 2103 other_errorT ("arm_parse_tbh", message))))); 2104 2105val arm_parse_mul : (term * term) M = 2106 arm_parse_register >>= (fn rd => 2107 arm_parse_comma >>- 2108 arm_parse_register >>= (fn rn => 2109 tryT arm_parse_comma 2110 (fn _ => arm_parse_register >>= (fn rm => return (rd,rn,rm))) 2111 (fn _ => return (rd,rd,rn)) >>= 2112 (fn (rd,rn,rm) => 2113 read_thumb >>= (fn thumb => 2114 read_sflag >>= (fn sflag => 2115 if thumb then 2116 read_InITBlock >>= (fn InITBlock => 2117 read_qualifier >>= (fn q => 2118 let val thumb_sflag = mk_bool (not InITBlock) 2119 val narrow_okay = 2120 q <> Wide andalso thumb_sflag ~~ sflag andalso 2121 (rd ~~ rn orelse rd ~~ rm) andalso 2122 narrow_registers [rn,rm] 2123 val wide_okay = is_F sflag 2124 val (rn,rm) = if narrow_okay andalso rd !~ rm 2125 then (rm,rn) else (rn,rm) 2126 in 2127 assertT_thumb "arm_parse_mul" q narrow_okay wide_okay 2128 (return (pick_enc true narrow_okay, 2129 mk_Multiply (F,sflag,rd,mk_word4 0,rm,rn))) 2130 end)) 2131 else 2132 return 2133 (Encoding_ARM_tm, mk_Multiply (F,sflag,rd,mk_word4 0,rm,rn))))))); 2134 2135local 2136 fun pas SADD16 = (F,Parallel_normal_tm,Parallel_add_16_tm) 2137 | pas SASX = (F,Parallel_normal_tm,Parallel_add_sub_exchange_tm) 2138 | pas SSAX = (F,Parallel_normal_tm,Parallel_sub_add_exchange_tm) 2139 | pas SSUB16 = (F,Parallel_normal_tm,Parallel_sub_16_tm) 2140 | pas SADD8 = (F,Parallel_normal_tm,Parallel_add_8_tm) 2141 | pas SSUB8 = (F,Parallel_normal_tm,Parallel_sub_8_tm) 2142 | pas QADD16 = (F,Parallel_saturating_tm,Parallel_add_16_tm) 2143 | pas QASX = (F,Parallel_saturating_tm,Parallel_add_sub_exchange_tm) 2144 | pas QSAX = (F,Parallel_saturating_tm,Parallel_sub_add_exchange_tm) 2145 | pas QSUB16 = (F,Parallel_saturating_tm,Parallel_sub_16_tm) 2146 | pas QADD8 = (F,Parallel_saturating_tm,Parallel_add_8_tm) 2147 | pas QSUB8 = (F,Parallel_saturating_tm,Parallel_sub_8_tm) 2148 | pas SHADD16 = (F,Parallel_halving_tm,Parallel_add_16_tm) 2149 | pas SHASX = (F,Parallel_halving_tm,Parallel_add_sub_exchange_tm) 2150 | pas SHSAX = (F,Parallel_halving_tm,Parallel_sub_add_exchange_tm) 2151 | pas SHSUB16 = (F,Parallel_halving_tm,Parallel_sub_16_tm) 2152 | pas SHADD8 = (F,Parallel_halving_tm,Parallel_add_8_tm) 2153 | pas SHSUB8 = (F,Parallel_halving_tm,Parallel_sub_8_tm) 2154 | pas UADD16 = (T,Parallel_normal_tm,Parallel_add_16_tm) 2155 | pas UASX = (T,Parallel_normal_tm,Parallel_add_sub_exchange_tm) 2156 | pas USAX = (T,Parallel_normal_tm,Parallel_sub_add_exchange_tm) 2157 | pas USUB16 = (T,Parallel_normal_tm,Parallel_sub_16_tm) 2158 | pas UADD8 = (T,Parallel_normal_tm,Parallel_add_8_tm) 2159 | pas USUB8 = (T,Parallel_normal_tm,Parallel_sub_8_tm) 2160 | pas UQADD16 = (T,Parallel_saturating_tm,Parallel_add_16_tm) 2161 | pas UQASX = (T,Parallel_saturating_tm,Parallel_add_sub_exchange_tm) 2162 | pas UQSAX = (T,Parallel_saturating_tm,Parallel_sub_add_exchange_tm) 2163 | pas UQSUB16 = (T,Parallel_saturating_tm,Parallel_sub_16_tm) 2164 | pas UQADD8 = (T,Parallel_saturating_tm,Parallel_add_8_tm) 2165 | pas UQSUB8 = (T,Parallel_saturating_tm,Parallel_sub_8_tm) 2166 | pas UHADD16 = (T,Parallel_halving_tm,Parallel_add_16_tm) 2167 | pas UHASX = (T,Parallel_halving_tm,Parallel_add_sub_exchange_tm) 2168 | pas UHSAX = (T,Parallel_halving_tm,Parallel_sub_add_exchange_tm) 2169 | pas UHSUB16 = (T,Parallel_halving_tm,Parallel_sub_16_tm) 2170 | pas UHADD8 = (T,Parallel_halving_tm,Parallel_add_8_tm) 2171 | pas UHSUB8 = (T,Parallel_halving_tm,Parallel_sub_8_tm) 2172 | pas _ = raise ERR "pas" "unknown mnemonic" 2173in 2174 val is_par_add_sub = Lib.can pas 2175 2176 fun is_thumb2_3 m = is_par_add_sub m orelse mem m 2177 [SMULBB, SMULBT, SMULTB, SMULTT, SMULWB, SMULWT, SMUAD, 2178 SMUADX, SMUSD, SMUSDX, SMMUL, SMMULR, SEL, USAD8, 2179 QADD, QSUB, QDADD, QDSUB]; 2180 2181 val is_thumb2_4 = Lib.C mem 2182 [MLA, MLS, UMULL, UMLAL, SMULL, SMLAL, UMAAL, SMLABB, SMLABT, SMLATB, 2183 SMLATT, SMLAWB, SMLAWT, SMLALBB, SMLALBT, SMLALTB, SMLALTT, SMLAD, 2184 SMLADX, SMLSD, SMLSDX, SMLALD, SMLALDX, SMLSLD, SMLSLDX, SMMLA, SMMLAR, 2185 SMMLS, SMMLSR, USADA8]; 2186 2187 fun par_add_sub m = 2188 let val (u,t1,t2) = pas m in (u, pairSyntax.mk_pair (t1,t2)) end 2189end; 2190 2191val arm_parse_thumb2_3 : (term * term) M = 2192 thumb2_or_arm_okay "arm_parse_thumb2_3" 2193 (fn enc => 2194 arm_parse_register >>= (fn rd => 2195 arm_parse_comma >>- 2196 arm_parse_register >>= (fn rn => 2197 tryT arm_parse_comma 2198 (fn _ => arm_parse_register >>= (fn rm => return (rd,rn,rm))) 2199 (fn _ => return (rd,rd,rn)) >>= (fn (rd,rn,rm) => 2200 read_mnemonic >>= (fn m => 2201 let val r0 = mk_word4 0 2202 val r15 = mk_word4 15 2203 fun v6 (tm:term) = need_v6 "arm_parse_thumb2_3" (return (enc,tm)) 2204 fun dsp (tm:term) = need_dsp "arm_parse_thumb2_3" (return (enc,tm)) 2205 val return_mk_shm = dsp o mk_Signed_Halfword_Multiply 2206 fun return_mk_pas () = 2207 let val (u,opc) = par_add_sub m in 2208 v6 (mk_Parallel_Add_Subtract (u,opc,rn,rd,rm)) 2209 end 2210 in 2211 case m 2212 of SMULBB => return_mk_shm (mk_word2 3,F,F,rd,r0,rm,rn) 2213 | SMULTB => return_mk_shm (mk_word2 3,F,T,rd,r0,rm,rn) 2214 | SMULBT => return_mk_shm (mk_word2 3,T,F,rd,r0,rm,rn) 2215 | SMULTT => return_mk_shm (mk_word2 3,T,T,rd,r0,rm,rn) 2216 | SMULWB => return_mk_shm (mk_word2 1,F,T,rd,r0,rm,rn) 2217 | SMULWT => return_mk_shm (mk_word2 1,T,T,rd,r0,rm,rn) 2218 | SMUAD => v6 (mk_Signed_Multiply_Dual (rd,r15,rm,F,F,rn)) 2219 | SMUADX => v6 (mk_Signed_Multiply_Dual (rd,r15,rm,F,T,rn)) 2220 | SMUSD => v6 (mk_Signed_Multiply_Dual (rd,r15,rm,T,F,rn)) 2221 | SMUSDX => v6 (mk_Signed_Multiply_Dual (rd,r15,rm,T,T,rn)) 2222 | SMMUL => v6 (mk_Signed_Most_Significant_Multiply (rd,r15,rm,F,rn)) 2223 | SMMULR => v6 (mk_Signed_Most_Significant_Multiply (rd,r15,rm,T,rn)) 2224 | SEL => v6 (mk_Select_Bytes (rn,rd,rm)) 2225 | USAD8 => v6 (mk_Unsigned_Sum_Absolute_Differences (rd,r15,rm,rn)) 2226 | QADD => dsp (mk_Saturating_Add_Subtract (mk_word2 0,rm,rd,rn)) 2227 | QSUB => dsp (mk_Saturating_Add_Subtract (mk_word2 1,rm,rd,rn)) 2228 | QDADD => dsp (mk_Saturating_Add_Subtract (mk_word2 2,rm,rd,rn)) 2229 | QDSUB => dsp (mk_Saturating_Add_Subtract (mk_word2 3,rm,rd,rn)) 2230 | _ => if is_par_add_sub m then return_mk_pas () else 2231 raise ERR "arm_parse_thumb2_3" "unknown mnemonic" 2232 end))))); 2233 2234val arm_parse_thumb2_4 : (term * term) M = 2235 thumb2_or_arm_okay "arm_parse_thumb2_4" 2236 (fn enc => 2237 arm_parse_register >>= (fn rd => 2238 arm_parse_comma >>- 2239 arm_parse_register >>= (fn rn => 2240 arm_parse_comma >>- 2241 arm_parse_register >>= (fn rm => 2242 arm_parse_comma >>- 2243 arm_parse_register >>= (fn ra => 2244 read_sflag >>= (fn sflag => 2245 read_mnemonic >>= (fn m => 2246 let fun t2 (tm:term) = need_t2 "arm_parse_thumb2_4" (return (enc,tm)) 2247 fun v6 (tm:term) = need_v6 "arm_parse_thumb2_4" (return (enc,tm)) 2248 fun return_mk_shm x = need_dsp "arm_parse_thumb2_4" 2249 (return (enc,mk_Signed_Halfword_Multiply x)) 2250 in 2251 case m 2252 of MLA => return (enc,mk_Multiply (T,sflag,rd,ra,rm,rn)) 2253 | MLS => t2 (mk_Multiply_Subtract (rd,ra,rm,rn)) 2254 | UMULL => return (enc,mk_Multiply_Long (F,F,sflag,rn,rd,ra,rm)) 2255 | UMLAL => return (enc,mk_Multiply_Long (F,T,sflag,rn,rd,ra,rm)) 2256 | SMULL => return (enc,mk_Multiply_Long (T,F,sflag,rn,rd,ra,rm)) 2257 | SMLAL => return (enc,mk_Multiply_Long (T,T,sflag,rn,rd,ra,rm)) 2258 | UMAAL => v6 (mk_Multiply_Accumulate_Accumulate (rn,rd,ra,rm)) 2259 | SMLABB => return_mk_shm (mk_word2 0,F,F,rd,ra,rm,rn) 2260 | SMLATB => return_mk_shm (mk_word2 0,F,T,rd,ra,rm,rn) 2261 | SMLABT => return_mk_shm (mk_word2 0,T,F,rd,ra,rm,rn) 2262 | SMLATT => return_mk_shm (mk_word2 0,T,T,rd,ra,rm,rn) 2263 | SMLAWB => return_mk_shm (mk_word2 1,F,F,rd,ra,rm,rn) 2264 | SMLAWT => return_mk_shm (mk_word2 1,T,F,rd,ra,rm,rn) 2265 | SMLALBB => return_mk_shm (mk_word2 2,F,F,rd,ra,rm,rn) 2266 | SMLALTB => return_mk_shm (mk_word2 2,F,T,rd,ra,rm,rn) 2267 | SMLALBT => return_mk_shm (mk_word2 2,T,F,rd,ra,rm,rn) 2268 | SMLALTT => return_mk_shm (mk_word2 2,T,T,rd,ra,rm,rn) 2269 | SMLAD => v6 (mk_Signed_Multiply_Dual (rd,ra,rm,F,F,rn)) 2270 | SMLADX => v6 (mk_Signed_Multiply_Dual (rd,ra,rm,F,T,rn)) 2271 | SMLSD => v6 (mk_Signed_Multiply_Dual (rd,ra,rm,T,F,rn)) 2272 | SMLSDX => v6 (mk_Signed_Multiply_Dual (rd,ra,rm,T,T,rn)) 2273 | SMLALD => v6 (mk_Signed_Multiply_Long_Dual (rn,rd,ra,F,F,rm)) 2274 | SMLALDX => v6 (mk_Signed_Multiply_Long_Dual (rn,rd,ra,F,T,rm)) 2275 | SMLSLD => v6 (mk_Signed_Multiply_Long_Dual (rn,rd,ra,T,F,rm)) 2276 | SMLSLDX => v6 (mk_Signed_Multiply_Long_Dual (rn,rd,ra,T,T,rm)) 2277 | SMMLA => v6 (mk_Signed_Most_Significant_Multiply (rd,ra,rm,F,rn)) 2278 | SMMLAR => v6 (mk_Signed_Most_Significant_Multiply (rd,ra,rm,T,rn)) 2279 | SMMLS => v6 (mk_Signed_Most_Significant_Multiply_Subtract 2280 (rd,ra,rm,F,rn)) 2281 | SMMLSR => v6 (mk_Signed_Most_Significant_Multiply_Subtract 2282 (rd,ra,rm,T,rn)) 2283 | USADA8 => v6 (mk_Unsigned_Sum_Absolute_Differences (rd,ra,rm,rn)) 2284 | _ => raise ERR "arm_parse_thumb2_4" "unknown mnemonic" 2285 end))))))); 2286 2287val arm_parse_div : term -> (term * term) M = 2288 fn u => 2289 arch_okay ("arm_parse_div", "only supported by ARMv7-R") 2290 (curry (op =) ARMv7_R) 2291 (read_thumb >>= (fn thumb => 2292 assertT thumb ("arm_parse_div", "Thumb2 instruction only") 2293 (arm_parse_register >>= (fn rd => 2294 arm_parse_comma >>- 2295 arm_parse_register >>= (fn rn => 2296 tryT arm_parse_comma 2297 (fn _ => arm_parse_register >>= (fn rm => return (rd,rn,rm))) 2298 (fn _ => return (rd,rd,rn)) >>= 2299 (fn (rd,rn,rm) => 2300 return (Encoding_Thumb2_tm,mk_Divide (u,rn,rd,rm)))))))); 2301 2302val arm_parse_pkh : term -> (term * term) M = 2303 fn tbform => 2304 thumb2_or_arm_okay "arm_parse_pkh" 2305 (fn enc => 2306 need_v6 "arm_parse_pkh" 2307 (arm_parse_register >>= (fn rd => 2308 arm_parse_comma >>- 2309 arm_parse_register >>= (fn rn => 2310 tryT (arm_parse_comma >>- arm_parse_register) 2311 (fn rm => return (rd,rn,rm)) 2312 (fn _ => return (rd,rd,rn)) >>= 2313 (fn (rd,rn,rm) => 2314 tryT arm_parse_comma 2315 (fn _ => 2316 arm_parse_string (if is_T tbform then "asr" else "lsl") >>- 2317 arm_parse_constant >>= (fn i => 2318 let val imm5 = if is_T tbform andalso i ~~ ``32i`` then 2319 mk_word5 0 2320 else 2321 uint_to_word ``:5`` i 2322 in 2323 return (enc,mk_Pack_Halfword (rn,rd,imm5,tbform,rm)) 2324 end handle HOL_ERR {message,...} => 2325 other_errorT ("arm_parse_pkh", message))) 2326 (fn _ => 2327 if is_T tbform then 2328 return (enc,mk_Pack_Halfword (rm,rd,mk_word5 0,F,rn)) 2329 else 2330 return (enc,mk_Pack_Halfword (rn,rd,mk_word5 0,F,rm)))))))); 2331 2332(* ------------------------------------------------------------------------- *) 2333 2334val arm_parse_mode2_shift : bool -> qualifier -> term -> term M = 2335 fn thumb => fn q => fn rm => 2336 tryT arm_parse_comma 2337 (fn _ => 2338 arm_parse_shift >>= (fn s => 2339 assertT (q <> Narrow andalso (not thumb orelse s = LSL_shift)) 2340 ("arm_parse_mode2_shift", "shift not available") 2341 (if s = RRX_shift then 2342 return (mk_Mode2_register (mk_word5 0, shift_to_word2 s, rm)) 2343 else 2344 arm_parse_constant >>= (fn i => 2345 let val v = sint_of_term i 2346 val stype = shift_to_word2 (if v = 0 then LSL_shift else s) 2347 val imm5 = mk_word5 (if v = 32 then 0 else Int.abs v) 2348 val max = if thumb then 3 else 2349 if mem s [LSR_shift,ASR_shift] then 32 else 31 2350 in 2351 assertT (0 <= v andalso v <= max) 2352 ("arm_parse_mode2_shift", "shift out of range") 2353 (return (mk_Mode2_register (imm5, stype, rm))) 2354 end handle HOL_ERR {message,...} => 2355 other_errorT ("arm_parse_mode2_shift", message))))) 2356 (fn _ => 2357 return (mk_Mode2_register (mk_word5 0, shift_to_word2 LSL_shift, rm))); 2358 2359val arm_parse_mode2_offset : 2360 (bool * bool * term * term * term * term) -> (term * term) M = 2361 fn (ld,indx,byte,unpriv,rt,rn) => 2362 read_thumb >>= (fn thumb => 2363 read_thumbee >>= (fn thumbee => 2364 read_qualifier >>= (fn q => 2365 assertT (indx orelse q <> Narrow) 2366 ("arm_parse_mode2_offset", 2367 "post indexing not possible for narrow Thumb instruction") 2368 (tryT arm_parse_constant 2369 (fn i => 2370 (if indx then 2371 arm_parse_rsquare >>- 2372 tryT arm_parse_exclaim (K (return T)) (K (return F)) 2373 else 2374 return (mk_bool (thumb orelse not thumb andalso is_T unpriv))) >>= 2375 (fn w => 2376 let val v = sint_of_term i 2377 val u = mk_bool (0 <= v andalso not (i ~~ ``-0i``)) 2378 val thumbee_okay = thumbee andalso q <> Wide andalso 2379 narrow_register rt andalso is_F byte andalso 2380 is_F w andalso v mod 4 = 0 andalso 2381 if ld then 2382 is_R9 rn andalso 0 <= v andalso v <= 252 2383 orelse 2384 is_R10 rn andalso 0 <= v andalso v <= 124 2385 orelse 2386 narrow_register rn andalso ~28 <= v 2387 andalso v <= 124 2388 else 2389 0 <= v andalso 2390 (is_R9 rn andalso v <= 252 orelse 2391 narrow_register rn andalso v <= 124) 2392 val narrow_okay = q <> Wide andalso narrow_register rt andalso 2393 is_F w andalso 0 <= v andalso 2394 if is_T byte then 2395 narrow_register rn andalso v <= 31 2396 else 2397 v mod 4 = 0 andalso 2398 if is_SP rn orelse ld andalso is_PC rn 2399 then 2400 is_F byte andalso v <= 1020 2401 else 2402 narrow_register rn andalso v <= 124 2403 val narrow_or_thumbee = thumbee_okay orelse narrow_okay 2404 val wide_okay = ~255 <= v andalso 2405 if indx andalso is_T u andalso is_F w then 2406 v <= 4095 2407 else 2408 v <= 255 andalso not (is_T byte andalso 2409 is_PC rt andalso indx andalso is_F u 2410 andalso is_F w) 2411 val arm_okay = ~4095 <= v andalso v <= 4095 2412 val imm12 = mk_word12 (Int.abs v) 2413 in 2414 assertT 2415 (q = Narrow andalso narrow_or_thumbee orelse 2416 q <> Narrow andalso thumb andalso wide_okay orelse 2417 not thumb andalso arm_okay) 2418 ("arm_parse_mode2_offset", 2419 "invalid argument(s) (check registers, alignment and range)") 2420 (return 2421 (pick_enc_ee thumb narrow_or_thumbee 2422 (not narrow_okay andalso thumbee_okay), 2423 (if ld then mk_Load else mk_Store) 2424 (mk_bool indx,u,byte,w,unpriv,rn,rt, 2425 mk_Mode2_immediate imm12))) 2426 end handle HOL_ERR {message,...} => 2427 other_errorT ("arm_parse_mode2_offset", message))) 2428 (fn _ => 2429 arm_parse_plus_minus >>= (fn pos => 2430 arm_parse_register >>= (fn rm => 2431 arm_parse_mode2_shift thumb q rm >>= (fn mode2 => 2432 (if indx then 2433 arm_parse_rsquare >>- 2434 tryT arm_parse_exclaim (K (return T)) (K (return F)) 2435 else 2436 return 2437 (mk_bool (thumb orelse not thumb andalso is_T unpriv))) >>= 2438 (fn w => 2439 let val (sh,_,_) = dest_Mode2_register mode2 2440 val narrow_okay = q <> Wide andalso indx andalso 2441 narrow_registers [rt,rn,rm] andalso 2442 sh ~~ mk_word5 (if thumbee then 2 else 0) 2443 andalso is_F w 2444 in 2445 assertT ((not thumb orelse pos andalso is_F w) andalso 2446 (q <> Narrow orelse narrow_okay)) 2447 ("arm_parse_mode2_offset", "invalid argument(s)") 2448 (return 2449 (pick_enc_ee thumb narrow_okay thumbee, 2450 (if ld then mk_Load else mk_Store) 2451 (mk_bool indx,mk_bool pos,byte,w,unpriv,rn,rt,mode2))) 2452 end))))))))); 2453 2454val arm_parse_mode2 : bool -> term -> (term * term) M = 2455 fn ld => fn byte => 2456 arm_parse_register >>= (fn rt => 2457 arm_parse_comma >>- 2458 read_thumb >>= (fn thumb => 2459 read_qualifier >>= (fn q => 2460 tryT arm_parse_lsquare 2461 (fn _ => 2462 arm_parse_register >>= (fn rn => 2463 tryT arm_parse_comma 2464 (fn _ => arm_parse_mode2_offset (ld,true,byte,F,rt,rn)) 2465 (fn _ => 2466 arm_parse_rsquare >>- 2467 tryT arm_parse_comma 2468 (fn _ => arm_parse_mode2_offset (ld,false,byte,F,rt,rn)) 2469 (fn _ => 2470 let val narrow_okay = q <> Wide andalso narrow_register rt 2471 andalso (narrow_register rn orelse 2472 is_F byte andalso is_SP rn) 2473 in 2474 assertT (q <> Narrow orelse narrow_okay) 2475 ("arm_parse_mode2", 2476 "invalid register(s) for narrow Thumb instruction") 2477 (return 2478 (pick_enc thumb narrow_okay, 2479 (if ld then mk_Load else mk_Store) 2480 (T,T,byte,F,F,rn,rt, 2481 mk_Mode2_immediate (mk_word12 0)))) 2482 end)))) 2483 (fn _ => 2484 arm_parse_branch_offset >>= (fn i => 2485 let val narrow_okay = narrow_register rt andalso is_F byte in 2486 assertT (ld andalso (q <> Narrow orelse narrow_okay)) 2487 ("arm_parse_mode2", "not a valid instruction") 2488 (if is_var i then 2489 return 2490 (pick_var_enc thumb q narrow_okay, 2491 mk_Load (T,boolSyntax.arb,byte,F,F,mk_word4 15,rt, 2492 cast_var ``:addressing_mode2`` i)) 2493 else 2494 let val v = sint_of_term i - (if thumb then 4 else 8) 2495 val narrow_okay = q <> Wide andalso v mod 4 = 0 andalso 2496 0 <= v andalso v <= 1020 2497 val wide_okay = q <> Narrow andalso ~4095 <= v andalso 2498 v <= 4095 2499 val mode2 = mk_Mode2_immediate (mk_word12 (Int.abs v)) 2500 in 2501 assertT (not thumb orelse narrow_okay orelse wide_okay) 2502 ("arm_parse_mode2", "not a valid instruction") 2503 (return 2504 (pick_enc thumb narrow_okay, 2505 mk_Load (T,mk_bool (0 <= v andalso not (i ~~ ``-0i``)), 2506 byte,F,F,mk_word4 15,rt,mode2))) 2507 end handle HOL_ERR {message,...} => 2508 other_errorT ("arm_parse_mode2", message)) 2509 end)))) >>= (fn result => 2510 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 2511 assertT (not (is_PC rt) orelse OutsideOrLastInITBlock) 2512 ("arm_parse_mode2", "must be outside or last in IT block") 2513 (return result)))); 2514 2515val arm_parse_mode2_unpriv : bool -> term -> (term * term) M = 2516 fn ld => fn byte => 2517 thumb2_or_arm_okay "arm_parse_mode2_unpriv" 2518 (fn enc => 2519 arm_parse_register >>= (fn rt => 2520 arm_parse_comma >>- 2521 arm_parse_lsquare >>- 2522 arm_parse_register >>= (fn rn => 2523 tryT arm_parse_comma 2524 (fn _ => 2525 (arm_parse_constant >>= (fn i => 2526 arm_parse_rsquare >>- 2527 let val v = sint_of_term i 2528 val mode2 = mk_Mode2_immediate (mk_word12 (Int.abs v)) 2529 in 2530 assertT (enc ~~ Encoding_Thumb2_tm andalso 2531 0 <= v andalso v <= 255) 2532 ("arm_parse_mode2_unpriv", 2533 "must be Thumb2 with offset in range 0-255") 2534 (return (enc, 2535 if ld then 2536 mk_Load (T,T,byte,F,T,rn,rt,mode2) 2537 else 2538 mk_Store (T,T,byte,F,T,rn,rt,mode2))) 2539 end handle HOL_ERR {message,...} => 2540 other_errorT ("arm_parse_mode2_unpriv", message)))) 2541 (fn _ => 2542 arm_parse_rsquare >>- 2543 tryT arm_parse_comma 2544 (fn _ => 2545 assertT (enc ~~ Encoding_ARM_tm) 2546 ("arm_parse_mode2_unpriv", "unexpected comma") 2547 (arm_parse_mode2_offset (ld,false,byte,T,rt,rn))) 2548 (fn _ => 2549 return (enc, 2550 (if ld then mk_Load else mk_Store) 2551 (mk_bool (enc ~~ Encoding_Thumb2_tm),T,byte,F,T,rn,rt, 2552 mk_Mode2_immediate (mk_word12 0)))))))); 2553 2554(* ------------------------------------------------------------------------- *) 2555 2556val mode3_register = curry mk_Mode3_register (mk_word2 0); 2557 2558val arm_parse_mode3_shift : bool -> qualifier -> term -> term M = 2559 fn thumb => fn q => fn rm => 2560 tryT arm_parse_comma 2561 (fn _ => 2562 assertT (thumb andalso q <> Narrow) 2563 ("arm_parse_mode3_shift", "unexpected comma") 2564 (arm_parse_string "lsl" >>- 2565 arm_parse_constant >>= (fn i => 2566 let val imm2 = uint_to_word ``:2`` i in 2567 return (mk_Mode3_register (imm2, rm)) 2568 end handle HOL_ERR {message,...} => 2569 other_errorT ("arm_parse_mode3_shift", message)))) 2570 (fn _ => return (mode3_register rm)); 2571 2572val arm_parse_mode3_offset : 2573 ((term * term) option * bool * term * term * term) -> (term * term) M = 2574 fn (opt,indx,unpriv,rt,rn) => 2575 read_thumb >>= (fn thumb => 2576 read_qualifier >>= (fn q => 2577 assertT (indx orelse q <> Narrow) 2578 ("arm_parse_mode3_offset", 2579 "post indexing not possible for narrow Thumb instruction") 2580 (tryT arm_parse_constant 2581 (fn i => 2582 (if indx then 2583 arm_parse_rsquare >>- 2584 tryT arm_parse_exclaim (K (return T)) (K (return F)) 2585 else 2586 return (mk_bool thumb)) >>= 2587 (fn w => 2588 let val v = sint_of_term i 2589 val u = mk_bool (0 <= v andalso not (i ~~ ``-0i``)) 2590 val narrow_okay = q <> Wide andalso narrow_registers [rt,rn] 2591 andalso is_F w andalso v mod 2 = 0 andalso 2592 0 <= v andalso v <= 62 andalso 2593 case opt of 2594 SOME (s,h) => is_F s andalso is_T h 2595 | NONE => true 2596 val wide_okay = ~255 <= v andalso 2597 if indx andalso is_T u andalso is_F w then 2598 v <= 4095 2599 else 2600 v <= 255 andalso not (is_PC rt andalso 2601 indx andalso is_F u andalso is_F w) 2602 val arm_okay = ~255 <= v andalso v <= 255 2603 val imm12 = mk_word12 (Int.abs v) 2604 in 2605 assertT 2606 (q = Narrow andalso narrow_okay orelse 2607 q <> Narrow andalso thumb andalso wide_okay orelse 2608 not thumb andalso arm_okay) 2609 ("arm_parse_mode3_offset", 2610 "invalid argument(s) (check registers, alignment and range)") 2611 (return 2612 (pick_enc thumb narrow_okay, 2613 case opt 2614 of SOME (signed,half) => 2615 mk_Load_Halfword 2616 (mk_bool indx,u,w,signed,half,unpriv,rn,rt, 2617 mk_Mode3_immediate imm12) 2618 | NONE => 2619 mk_Store_Halfword (mk_bool indx,u,w,unpriv,rn,rt, 2620 mk_Mode3_immediate imm12))) 2621 end handle HOL_ERR {message,...} => 2622 other_errorT ("arm_parse_mode3_offset", message))) 2623 (fn _ => 2624 arm_parse_plus_minus >>= (fn pos => 2625 arm_parse_register >>= (fn rm => 2626 arm_parse_mode3_shift thumb q rm >>= (fn mode3 => 2627 read_thumbee >>= (fn thumbee => 2628 (if indx then 2629 arm_parse_rsquare >>- 2630 tryT arm_parse_exclaim (K (return T)) (K (return F)) 2631 else 2632 return (mk_bool thumb)) >>= 2633 (fn w => 2634 let val (sh,_) = dest_Mode3_register mode3 2635 val narrow_okay = q <> Wide andalso indx andalso 2636 narrow_registers [rt,rn,rm] andalso 2637 sh ~~ mk_word2 (if thumbee then 1 else 0) 2638 andalso is_F w 2639 in 2640 assertT ((not thumb orelse pos andalso is_F w) andalso 2641 (q <> Narrow orelse narrow_okay)) 2642 ("arm_parse_mode3_offset", "invalid argument(s)") 2643 (return 2644 (pick_enc_ee thumb narrow_okay thumbee, 2645 case opt 2646 of SOME (signed,half) => 2647 mk_Load_Halfword 2648 (mk_bool indx,mk_bool pos,w,signed,half,unpriv, 2649 rn,rt,mode3) 2650 | NONE => 2651 mk_Store_Halfword 2652 (mk_bool indx,mk_bool pos,w,unpriv,rn,rt,mode3))) 2653 end))))))))); 2654 2655val arm_parse_mode3 : (term * term) option -> (term * term) M = 2656 fn opt => 2657 arm_parse_register >>= (fn rt => 2658 arm_parse_comma >>- 2659 read_thumb >>= (fn thumb => 2660 read_qualifier >>= (fn q => 2661 tryT arm_parse_lsquare 2662 (fn _ => 2663 arm_parse_register >>= (fn rn => 2664 tryT arm_parse_comma 2665 (fn _ => arm_parse_mode3_offset (opt,true,F,rt,rn)) 2666 (fn _ => 2667 arm_parse_rsquare >>- 2668 tryT arm_parse_comma 2669 (fn _ => arm_parse_mode3_offset (opt,false,F,rt,rn)) 2670 (fn _ => 2671 let val narrow_okay = q <> Wide andalso 2672 narrow_registers [rt,rn] andalso 2673 case opt of 2674 SOME (s,h) => is_F s andalso is_T h 2675 | NONE => true 2676 in 2677 assertT (q <> Narrow orelse narrow_okay) 2678 ("arm_parse_mode3", "invalid narrow Thumb instruction") 2679 (return 2680 (pick_enc thumb narrow_okay, 2681 case opt 2682 of SOME (signed,half) => 2683 mk_Load_Halfword 2684 (T,T,F,signed,half,F,rn,rt, 2685 mk_Mode3_immediate (mk_word12 0)) 2686 | NONE => 2687 mk_Store_Halfword 2688 (T,T,F,F,rn,rt, 2689 mk_Mode3_immediate (mk_word12 0)))) 2690 end)))) 2691 (fn _ => 2692 arm_parse_branch_offset >>= (fn i => 2693 assertT (isSome opt andalso q <> Narrow) 2694 ("arm_parse_mode3", "not a valid instruction") 2695 (let val (signed,half) = case opt 2696 of SOME x => x 2697 | _ => (boolSyntax.arb,boolSyntax.arb) 2698 in 2699 if is_var i then 2700 return 2701 (if thumb then Encoding_Thumb2_tm else Encoding_ARM_tm, 2702 mk_Load_Halfword (T,boolSyntax.arb,F,signed,half,F, 2703 mk_word4 15,rt,cast_var ``:addressing_mode3`` i)) 2704 else 2705 let val v = sint_of_term i - (if thumb then 4 else 8) 2706 val wide_okay = thumb andalso ~4095 <= v andalso v <= 4095 2707 val arm_okay = not thumb andalso ~255 <= v andalso v <= 255 2708 val mode3 = mk_Mode3_immediate (mk_word12 (Int.abs v)) 2709 in 2710 assertT (wide_okay orelse arm_okay) 2711 ("arm_parse_mode3", "offset beyond permitted range") 2712 (return 2713 (if thumb then Encoding_Thumb2_tm else Encoding_ARM_tm, 2714 mk_Load_Halfword (T, 2715 mk_bool (0 <= v andalso not (i ~~ ``-0i``)),F, 2716 signed,half,F,mk_word4 15,rt,mode3))) 2717 end handle HOL_ERR {message,...} => 2718 other_errorT ("arm_parse_mode3", message) 2719 end)))))); 2720 2721val arm_parse_mode3_unpriv : (term * term) option -> (term * term) M = 2722 fn opt => 2723 thumb2_or_arm_okay "arm_parse_mode3_unpriv" 2724 (fn enc => 2725 arm_parse_register >>= (fn rt => 2726 arm_parse_comma >>- 2727 arm_parse_lsquare >>- 2728 arm_parse_register >>= (fn rn => 2729 tryT arm_parse_comma 2730 (fn _ => 2731 (arm_parse_constant >>= (fn i => 2732 arm_parse_rsquare >>- 2733 let val v = sint_of_term i 2734 val mode3 = mk_Mode3_immediate (mk_word12 (Int.abs v)) 2735 in 2736 assertT (enc ~~ Encoding_Thumb2_tm andalso 2737 0 <= v andalso v <= 255) 2738 ("arm_parse_mode3_unpriv", 2739 "must be Thumb2 with offset in range 0-255") 2740 (return (enc, 2741 case opt 2742 of SOME (signed,half) => 2743 mk_Load_Halfword (T,T,F,signed,half,T,rn,rt,mode3) 2744 | NONE => 2745 mk_Store_Halfword (T,T,F,T,rn,rt,mode3))) 2746 end handle HOL_ERR {message,...} => 2747 other_errorT ("arm_parse_mode3_unpriv", message)))) 2748 (fn _ => 2749 arm_parse_rsquare >>- 2750 tryT arm_parse_comma 2751 (fn _ => 2752 assertT (enc ~~ Encoding_ARM_tm) 2753 ("arm_parse_mode3_unpriv", "unexpected comma") 2754 (tryT (arm_parse_plus_minus >>= (fn pos => 2755 arm_parse_register >>= (fn rm => return (pos,rm)))) 2756 (fn (pos,rm) => 2757 return 2758 (mk_bool pos, mk_Mode3_register (mk_word2 0,rm))) 2759 (fn _ => 2760 arm_parse_constant >>= (fn i => 2761 let val v = sint_of_term i in 2762 assertT (~255 <= v andalso v <= 255) 2763 ("arm_parse_mode3_unpriv", 2764 "offset must be in range -255-255") 2765 (return 2766 (mk_bool (0 <= v andalso not (i ~~ ``-0i``)), 2767 mk_Mode3_immediate (mk_word12 (Int.abs v)))) 2768 end handle HOL_ERR {message,...} => 2769 other_errorT ("arm_parse_mode3_unpriv", message))))) 2770 (fn _ => return (T,mk_Mode3_immediate (mk_word12 0))) >>= 2771 (fn (add,tm) => 2772 let val thumb = enc ~~ Encoding_Thumb2_tm 2773 val indx = mk_bool thumb 2774 val w = mk_bool (not thumb) 2775 in 2776 return (enc, 2777 case opt 2778 of SOME (signed,half) => 2779 mk_Load_Halfword (indx,add,w,signed,half,T,rn,rt,tm) 2780 | NONE => 2781 mk_Store_Halfword (indx,add,w,T,rn,rt,tm)) 2782 end))))); 2783 2784(* ------------------------------------------------------------------------- *) 2785 2786val arm_parse_mode3_dual_offset : bool -> (term * term) M = 2787 fn thumb => 2788 tryT arm_parse_constant 2789 (fn i => 2790 let val offset = sint_of_term i in 2791 if thumb then 2792 assertT (offset mod 4 = 0) 2793 ("arm_parse_mode3_dual_offset", "offset must be word aligned") 2794 (assertT (~1020 <= offset andalso offset <= 1020) 2795 ("arm_parse_mode3_dual_offset", 2796 "offset beyond permitted range (-1020 to +1020)") 2797 (return 2798 (mk_bool (0 <= offset andalso not (i ~~ ``-0i``)), 2799 mk_Mode3_immediate (mk_word12 (Int.abs offset))))) 2800 else 2801 assertT (~255 <= offset andalso offset <= 255) 2802 ("arm_parse_mode3_dual_offset", 2803 "offset beyond permitted range (-255 to +255)") 2804 (return (mk_bool (0 <= offset andalso not (i ~~ ``-0i``)), 2805 mk_Mode3_immediate (mk_word12 (Int.abs offset)))) 2806 end handle HOL_ERR {message,...} => 2807 other_errorT ("arm_parse_mode3_dual_offset", message)) 2808 (fn _ => 2809 assertT (not thumb) 2810 ("arm_parse_mode3_dual_offset", "expecting a constant") 2811 (arm_parse_plus_minus >>= (fn pos => 2812 arm_parse_register >>= (fn rm => 2813 return (mk_bool pos,mode3_register rm))))); 2814 2815val arm_parse_mode3_dual : bool -> (term * term) M = 2816 fn ld => 2817 need_dsp "arm_parse_mode3_dual" (thumb2_or_arm_okay "arm_parse_mode3_dual" 2818 (fn enc => 2819 arm_parse_register >>= (fn rt => 2820 arm_parse_comma >>- 2821 arm_parse_register >>= (fn rt2 => 2822 arm_parse_comma >>- 2823 let val thumb = enc ~~ Encoding_Thumb2_tm 2824 val t1 = uint_of_word rt 2825 val t2 = uint_of_word rt2 2826 in 2827 assertT (thumb orelse t1 mod 2 = 0 andalso t2 = t1 + 1) 2828 ("arm_parse_mode3_dual", 2829 "first register must be even and second consecutive") 2830 (tryT arm_parse_lsquare 2831 (fn _ => 2832 arm_parse_register >>= (fn rn => 2833 tryT arm_parse_comma 2834 (fn _ => 2835 arm_parse_mode3_dual_offset thumb >>= (fn (add,tm) => 2836 arm_parse_rsquare >>- 2837 tryT arm_parse_exclaim (K (return T)) (K (return F)) >>= 2838 (fn wb => 2839 return 2840 (if ld then 2841 (enc, mk_Load_Dual (T,add,wb,rn,rt,rt2,tm)) 2842 else 2843 (enc, mk_Store_Dual (T,add,wb,rn,rt,rt2,tm)))))) 2844 (fn _ => 2845 arm_parse_rsquare >>- 2846 tryT (arm_parse_comma >>- arm_parse_mode3_dual_offset thumb) 2847 (fn (a,t) => return (F,a,t)) 2848 (fn _ => 2849 return (T,T,mk_Mode3_immediate (mk_word12 0))) >>= 2850 (fn (indx,add,tm) => 2851 let val w = mk_bool 2852 (enc ~~ Encoding_Thumb2_tm andalso is_F indx) 2853 in 2854 return 2855 (if ld then 2856 (enc, mk_Load_Dual (indx,add,w,rn,rt,rt2,tm)) 2857 else 2858 (enc, mk_Store_Dual (indx,add,w,rn,rt,rt2,tm))) 2859 end)))) 2860 (fn _ => 2861 assertT ld ("arm_parse_mode3_dual","expecting [") 2862 (arm_parse_branch_offset >>= (fn i => 2863 if is_var i then 2864 return (enc, 2865 mk_Load_Dual (T,boolSyntax.arb,F,mk_word4 15,rt,rt2, 2866 cast_var ``:addressing_mode3`` i)) 2867 else 2868 let val v = sint_of_term i - (if thumb then 4 else 8) 2869 val wide_okay = ~1020 <= v andalso v <= 1020 2870 val arm_okay = ~255 <= v andalso v <= 255 2871 val mode3 = mk_Mode3_immediate 2872 (mk_word12 (Int.abs v)) 2873 in 2874 assertT 2875 (if enc ~~ Encoding_Thumb2_tm 2876 then wide_okay else arm_okay) 2877 ("arm_parse_mode3_dual", 2878 "offset beyond permitted range") 2879 (return (enc, 2880 mk_Load_Dual 2881 (T,mk_bool (0 <= v andalso not (i ~~ ``-0i``)), 2882 F,mk_word4 15,rt,rt2,mode3))) 2883 end handle HOL_ERR {message,...} => 2884 other_errorT ("arm_parse_mode3_dual", message))))) 2885 end)))); 2886 2887(* ------------------------------------------------------------------------- *) 2888 2889val arm_parse_ldrex : (term * term) M = 2890 need_v6 "arm_parse_ldrex" 2891 (thumb2_or_arm_okay "arm_parse_ldrex" 2892 (fn enc => 2893 arm_parse_register >>= (fn rt => 2894 arm_parse_comma >>- 2895 arm_parse_lsquare >>- 2896 arm_parse_register >>= (fn rn => 2897 tryT arm_parse_comma 2898 (fn _ => 2899 arm_parse_constant >>= (fn i => 2900 arm_parse_rsquare >>- 2901 let val v = sint_of_term i in 2902 assertT (if enc ~~ Encoding_Thumb2_tm then 2903 0 <= v andalso v <= 1020 andalso v mod 4 = 0 2904 else 2905 v = 0) 2906 ("arm_parse_ldrex", "offset unaligned or out of range") 2907 (return (enc, 2908 mk_Load_Exclusive (rn,rt,mk_word8 (Int.abs (v div 4))))) 2909 end handle HOL_ERR {message,...} => 2910 other_errorT ("arm_parse_ldrex", message))) 2911 (fn _ => 2912 arm_parse_rsquare >>- 2913 return (enc, mk_Load_Exclusive (rn,rt,mk_word8 0))))))); 2914 2915val arm_parse_strex : (term * term) M = 2916 need_v6 "arm_parse_strex" 2917 (thumb2_or_arm_okay "arm_parse_strex" 2918 (fn enc => 2919 arm_parse_register >>= (fn rd => 2920 arm_parse_comma >>- 2921 arm_parse_register >>= (fn rt => 2922 arm_parse_comma >>- 2923 arm_parse_lsquare >>- 2924 arm_parse_register >>= (fn rn => 2925 tryT arm_parse_comma 2926 (fn _ => 2927 arm_parse_constant >>= (fn i => 2928 arm_parse_rsquare >>- 2929 let val v = sint_of_term i in 2930 assertT (if enc ~~ Encoding_Thumb2_tm then 2931 0 <= v andalso v <= 1020 andalso v mod 4 = 0 2932 else 2933 v = 0) 2934 ("arm_parse_strex", "offset unaligned or out of range") 2935 (return (enc, 2936 mk_Store_Exclusive 2937 (rn,rd,rt,mk_word8 (Int.abs (v div 4))))) 2938 end handle HOL_ERR {message,...} => 2939 other_errorT ("arm_parse_strex", message))) 2940 (fn _ => 2941 arm_parse_rsquare >>- 2942 return (enc, mk_Store_Exclusive (rn,rd,rt,mk_word8 0)))))))); 2943 2944val arm_parse_ldrexd : (term * term) M = 2945 read_thumb >>= (fn thumb => 2946 arch_okay ("arm_parse_ldrexd", "not supported by selected architecture") 2947 (fn a => version_number a >= 7 orelse not thumb andalso a = ARMv6K) 2948 (arm_parse_register >>= (fn rt => 2949 arm_parse_comma >>- 2950 arm_parse_register >>= (fn rt2 => 2951 arm_parse_comma >>- 2952 arm_parse_lsquare >>- 2953 arm_parse_register >>= (fn rn => 2954 arm_parse_rsquare >>- 2955 let val t1 = uint_of_word rt 2956 val t2 = uint_of_word rt2 2957 in 2958 assertT (thumb orelse t1 mod 2 = 0 andalso t2 = t1 + 1) 2959 ("arm_parse_ldrexd", 2960 "first register must be even and second consecutive") 2961 (return (if thumb then Encoding_Thumb2_tm else Encoding_ARM_tm, 2962 mk_Load_Exclusive_Doubleword (rn,rt,rt2))) 2963 end))))); 2964 2965val arm_parse_strexd : (term * term) M = 2966 read_thumb >>= (fn thumb => 2967 arch_okay ("arm_parse_strexd", "not supported by selected architecture") 2968 (fn a => version_number a >= 7 orelse not thumb andalso a = ARMv6K) 2969 (arm_parse_register >>= (fn rd => 2970 arm_parse_comma >>- 2971 arm_parse_register >>= (fn rt => 2972 arm_parse_comma >>- 2973 arm_parse_register >>= (fn rt2 => 2974 arm_parse_comma >>- 2975 arm_parse_lsquare >>- 2976 arm_parse_register >>= (fn rn => 2977 arm_parse_rsquare >>- 2978 let val t1 = uint_of_word rt 2979 val t2 = uint_of_word rt2 2980 in 2981 assertT (thumb orelse t1 mod 2 = 0 andalso t2 = t1 + 1) 2982 ("arm_parse_strexd", 2983 "first register must be even and second consecutive") 2984 (return (if thumb then Encoding_Thumb2_tm else Encoding_ARM_tm, 2985 mk_Store_Exclusive_Doubleword (rn,rd,rt,rt2))) 2986 end)))))); 2987 2988val arm_parse_ldrexb_ldrexh : bool -> (term * term) M = 2989 fn half => 2990 read_thumb >>= (fn thumb => 2991 arch_okay ("arm_parse_ldrexb_ldrexh", 2992 "not supported by selected architecture") 2993 (fn a => version_number a >= 7 orelse not thumb andalso a = ARMv6K) 2994 (arm_parse_register >>= (fn rt => 2995 arm_parse_comma >>- 2996 arm_parse_lsquare >>- 2997 arm_parse_register >>= (fn rn => 2998 arm_parse_rsquare >>- 2999 return (if thumb then Encoding_Thumb2_tm else Encoding_ARM_tm, 3000 if half then 3001 mk_Load_Exclusive_Halfword (rn,rt) 3002 else 3003 mk_Load_Exclusive_Byte (rn,rt)))))); 3004 3005val arm_parse_strexb_strexh : bool -> (term * term) M = 3006 fn half => 3007 read_thumb >>= (fn thumb => 3008 arch_okay ("arm_parse_strexb_strexh", 3009 "not supported by selected architecture") 3010 (fn a => version_number a >= 7 orelse not thumb andalso a = ARMv6K) 3011 (arm_parse_register >>= (fn rd => 3012 arm_parse_comma >>- 3013 arm_parse_register >>= (fn rt => 3014 arm_parse_comma >>- 3015 arm_parse_lsquare >>- 3016 arm_parse_register >>= (fn rn => 3017 arm_parse_rsquare >>- 3018 return (if thumb then Encoding_Thumb2_tm else Encoding_ARM_tm, 3019 if half then 3020 mk_Store_Exclusive_Halfword (rn,rd,rt) 3021 else 3022 mk_Store_Exclusive_Byte (rn,rd,rt))))))); 3023 3024val arm_parse_swp : term -> (term * term) M = 3025 fn byte => 3026 read_thumb >>= (fn thumb => 3027 assertT (not thumb) 3028 ("arm_parse_swp", "not available as Thumb instruction") 3029 (arm_parse_register >>= (fn rt => 3030 arm_parse_comma >>- 3031 arm_parse_register >>= (fn rt2 => 3032 arm_parse_comma >>- 3033 arm_parse_lsquare >>- 3034 arm_parse_register >>= (fn rn => 3035 arm_parse_rsquare >>- 3036 return (Encoding_ARM_tm, mk_Swap (byte,rn,rt,rt2))))))); 3037 3038(* ------------------------------------------------------------------------- *) 3039 3040val arm_parse_register_list_entry : (int * int) M = 3041 arm_parse_register >>= (fn ra => 3042 tryT arm_parse_minus 3043 (fn _ => 3044 arm_parse_register >>= (fn rb => 3045 return (uint_of_word ra,uint_of_word rb))) 3046 (fn _ => let val i = uint_of_word ra in (return (i,i)) end)); 3047 3048fun arm_parse_register_list_entries 3049 (l : (int * int) list) : (int * int) list M = 3050 tryT arm_parse_register_list_entry 3051 (fn h => 3052 tryT arm_parse_comma 3053 (fn _ => arm_parse_register_list_entries (h::l) >>= return) 3054 (fn _ => return (h::l))) 3055 (fn _ => 3056 assertT (not (null l)) 3057 ("arm_parse_register_list_entries", "not a valid register list") 3058 (return l)); 3059 3060fun valid_register_list [] = true 3061 | valid_register_list [(x,y)] = x <= y 3062 | valid_register_list ((x,y)::t) = 3063 x <= y andalso fst (hd t) < x andalso valid_register_list t; 3064 3065local 3066 fun in_register_list _ [] = false 3067 | in_register_list r ((x,y)::t) = 3068 x <= r andalso r <= y orelse in_register_list r t; 3069in 3070 fun register_list_to_word16 l = 3071 let fun recurse 0 a = a 3072 | recurse i a = recurse (i - 1) 3073 (if in_register_list (i - 1) l then 2 * a + 1 else 2 * a) 3074 in 3075 mk_word16 (recurse 16 0) 3076 end 3077end; 3078 3079val arm_parse_register_list : term M = 3080 arm_parse_lbrace >>- 3081 arm_parse_register_list_entries [] >>= (fn l => 3082 arm_parse_rbrace >>- 3083 (assertT (valid_register_list l) 3084 ("arm_parse_register_list", "not a valid register list") 3085 (return (register_list_to_word16 l)))); 3086 3087val singleton_list_to_reg = 3088 mk_word4 o uint_of_word o eval o wordsSyntax.mk_word_log2; 3089 3090fun bit_count tm = numSyntax.int_of_term (eval (wordsSyntax.mk_bit_count tm)) 3091 3092val arm_parse_pop_push : bool -> (term * term) M = 3093 fn pop => 3094 arm_parse_register_list >>= (fn list => 3095 let val count = bit_count list in 3096 read_thumb >>= (fn thumb => 3097 if thumb then 3098 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 3099 read_qualifier >>= (fn q => 3100 let val high_bits = (uint_of_word list) div 256 3101 val pc = bit 7 high_bits 3102 val lr = bit 6 high_bits 3103 val sp = bit 5 high_bits 3104 val narrow_okay = q <> Wide andalso 3105 (not pc orelse OutsideOrLastInITBlock) 3106 andalso (high_bits = 0 orelse 3107 (high_bits = (if pop then 128 else 64))) 3108 val wide_okay = q <> Narrow andalso not sp andalso 3109 (pop orelse not pc) andalso 3110 (not pc orelse not lr andalso 3111 OutsideOrLastInITBlock) 3112 in 3113 if count = 1 andalso not narrow_okay then 3114 assertT wide_okay 3115 ("arm_parse_pop_push", 3116 "invalid register list, or must be outside or\ 3117 \ last in IT block") 3118 (return (Encoding_Thumb2_tm, 3119 if pop then 3120 mk_Load (F,T,F,T,F,mk_word4 13, 3121 singleton_list_to_reg list, 3122 mk_Mode2_immediate (mk_word12 4)) 3123 else 3124 mk_Store (T,F,F,T,F,mk_word4 13, 3125 singleton_list_to_reg list, 3126 mk_Mode2_immediate (mk_word12 4)))) 3127 else 3128 assertT (narrow_okay orelse wide_okay) 3129 ("arm_parse_pop_push", 3130 "invalid register list, or must be outside or\ 3131 \ last in IT block") 3132 (return 3133 (if narrow_okay then 3134 Encoding_Thumb_tm 3135 else 3136 Encoding_Thumb2_tm, 3137 if pop then 3138 mk_Load_Multiple (F,T,F,T,mk_word4 13,list) 3139 else 3140 mk_Store_Multiple (T,F,F,T,mk_word4 13,list))) 3141 end)) 3142 else 3143 return (Encoding_ARM_tm, 3144 if count = 1 then 3145 if pop then 3146 mk_Load (F,T,F,F,F,mk_word4 13,singleton_list_to_reg list, 3147 mk_Mode1_immediate (mk_word12 4)) 3148 else 3149 mk_Store (T,F,F,T,F,mk_word4 13,singleton_list_to_reg list, 3150 mk_Mode1_immediate (mk_word12 4)) 3151 else 3152 if pop then 3153 mk_Load_Multiple (F,T,F,T,mk_word4 13,list) 3154 else 3155 mk_Store_Multiple (T,F,F,T,mk_word4 13,list))) 3156 end); 3157 3158val arm_parse_ldm_stm : bool -> term -> term -> (term * term) M = 3159 fn ldm => fn indx => fn add => 3160 arm_parse_register >>= (fn rn => 3161 tryT arm_parse_exclaim (K (return T)) (K (return F)) >>= (fn w => 3162 arm_parse_comma >>- 3163 arm_parse_register_list >>= (fn list => 3164 read_thumb >>= (fn thumb => 3165 read_thumbee >>= (fn thumbee => 3166 if thumb then 3167 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 3168 read_qualifier >>= (fn q => 3169 let 3170 val count = bit_count list 3171 val l = uint_of_word list 3172 val n = uint_of_word rn 3173 val high_bits = l div 256 3174 val pc = bit 7 high_bits 3175 val lr = bit 6 high_bits 3176 val sp = bit 5 high_bits 3177 val narrow_okay = 3178 q <> Wide andalso not thumbee andalso 3179 if ldm then 3180 is_F indx andalso is_T add andalso 3181 is_T w <> bit n l andalso 3182 (narrow_register rn andalso high_bits = 0 orelse 3183 is_SP rn andalso mem high_bits [0,128] andalso 3184 (not pc orelse OutsideOrLastInITBlock)) 3185 else 3186 is_T w andalso 3187 (is_F indx andalso is_T add andalso 3188 narrow_register rn andalso high_bits = 0 orelse 3189 is_T indx andalso is_F add andalso 3190 is_SP rn andalso mem high_bits [0,64]) 3191 val wide_okay = q <> Narrow andalso 3192 (is_F indx andalso is_T add orelse 3193 is_T indx andalso is_F add) andalso 3194 not sp andalso (ldm orelse not pc) andalso 3195 (not pc orelse not lr andalso 3196 OutsideOrLastInITBlock) 3197 in 3198 if count = 1 andalso not narrow_okay then 3199 assertT wide_okay 3200 ("arm_parse_ldm_stm", "invalid instruction") 3201 (return 3202 (Encoding_Thumb2_tm, 3203 if ldm then 3204 mk_Load (indx,add,F,F,w,rn,singleton_list_to_reg list, 3205 mk_Mode2_immediate (mk_word12 4)) 3206 else 3207 mk_Store (indx,add,F,w,F,rn,singleton_list_to_reg list, 3208 mk_Mode2_immediate (mk_word12 4)))) 3209 else 3210 assertT (narrow_okay orelse wide_okay) 3211 ("arm_parse_ldm_stm", "invalid instruction") 3212 (return 3213 (if narrow_okay then 3214 Encoding_Thumb_tm 3215 else 3216 Encoding_Thumb2_tm, 3217 if ldm then 3218 mk_Load_Multiple (indx,add,F,w,rn,list) 3219 else 3220 mk_Store_Multiple (indx,add,F,w,rn,list))) 3221 end)) 3222 else 3223 (tryT arm_parse_hat (K (return T)) (K (return F)) >>= (fn sys => 3224 return 3225 (Encoding_ARM_tm, 3226 if ldm then 3227 mk_Load_Multiple (indx,add,sys,w,rn,list) 3228 else 3229 mk_Store_Multiple (indx,add,sys,w,rn,list))))))))); 3230 3231(* ------------------------------------------------------------------------- *) 3232 3233val arm_parse_pld_pli : bool option -> (term * term) M = 3234 fn opt => 3235 (case opt of SOME false => need_dsp | _ => need_v7) "arm_parse_pld_pli" 3236 (thumb2_or_arm_okay "arm_parse_pld_pli" 3237 (fn enc => 3238 tryT arm_parse_lsquare 3239 (fn _ => 3240 arm_parse_register >>= (fn rn => 3241 tryT arm_parse_comma 3242 (fn _ => 3243 tryT arm_parse_constant 3244 (fn i => 3245 arm_parse_rsquare >>- 3246 let val v = sint_of_term i 3247 val mode2 = mk_Mode2_immediate 3248 (mk_word12 (Int.abs v)) 3249 in 3250 assertT 3251 ((if enc ~~ Encoding_Thumb2_tm then 3252 ~255 <= v 3253 else 3254 ~4095 <= v) andalso v <= 4095) 3255 ("arm_parse_pld_pli", 3256 "offset beyond permitted range") 3257 (return (enc, 3258 case opt 3259 of SOME wide => 3260 mk_Preload_Data 3261 (mk_bool (0 <= v andalso 3262 not (i ~~ ``-0i``)), 3263 mk_bool wide,rn,mode2) 3264 | NONE => 3265 mk_Preload_Instruction 3266 (mk_bool (0 <= v andalso 3267 not (i ~~ ``-0i``)), 3268 rn,mode2))) 3269 end handle HOL_ERR {message,...} => 3270 other_errorT ("arm_parse_pld_pli", message)) 3271 (fn _ => 3272 let val thumb = enc ~~ Encoding_Thumb2_tm in 3273 arm_parse_plus_minus >>= (fn pos => 3274 arm_parse_register >>= (fn rm => 3275 assertT (not thumb orelse pos) 3276 ("arm_parse_pld_pli", 3277 "register offset must be positive in Thumb mode") 3278 (arm_parse_mode2_shift thumb Either rm >>= 3279 (fn mode2 => 3280 arm_parse_rsquare >>- 3281 return (enc, 3282 case opt 3283 of SOME wide => 3284 mk_Preload_Data 3285 (mk_bool pos,mk_bool wide,rn,mode2) 3286 | NONE => 3287 mk_Preload_Instruction 3288 (mk_bool pos,rn,mode2)))))) 3289 end)) 3290 (fn _ => 3291 arm_parse_rsquare >>- 3292 (return (enc, 3293 case opt 3294 of SOME wide => 3295 mk_Preload_Data (T,mk_bool wide,rn, 3296 mk_Mode2_immediate (mk_word12 0)) 3297 | NONE => 3298 mk_Preload_Instruction (T,rn, 3299 mk_Mode2_immediate (mk_word12 0))))))) 3300 (fn _ => 3301 arm_parse_branch_offset >>= (fn i => 3302 assertT (opt <> SOME true) 3303 ("arm_parse_pld_pli", "literal form not available for pldw") 3304 (if is_var i then 3305 return (enc, 3306 case opt 3307 of SOME wide => 3308 mk_Preload_Data 3309 (boolSyntax.arb,mk_bool wide,mk_word4 15, 3310 cast_var ``:addressing_mode2`` i) 3311 | NONE => 3312 mk_Preload_Instruction 3313 (boolSyntax.arb,mk_word4 15, 3314 cast_var ``:addressing_mode2`` i)) 3315 else 3316 let val v = sint_of_term i - 3317 (if enc ~~ Encoding_Thumb2_tm then 4 else 8) 3318 val up = mk_bool (0 <= v andalso not (i ~~ ``-0i``)) 3319 val mode2 = mk_Mode2_immediate (mk_word12 (Int.abs v)) 3320 in 3321 assertT (~4095 <= v andalso v <= 4095) 3322 ("arm_parse_pld_pli", "offset beyond permitted range") 3323 (return (enc, 3324 case opt 3325 of SOME wide => 3326 mk_Preload_Data 3327 (up,mk_bool wide,mk_word4 15,mode2) 3328 | NONE => 3329 mk_Preload_Instruction (up,mk_word4 15,mode2))) 3330 end handle HOL_ERR {message,...} => 3331 other_errorT ("arm_parse_mode3", message)))))); 3332 3333(* ------------------------------------------------------------------------- *) 3334 3335val arm_parse_ssat_usat : bool -> (term * term) M = 3336 fn unsigned => 3337 need_v6 "arm_parse_ssat_usat" 3338 (thumb2_or_arm_okay "arm_parse_ssat_usat" 3339 (fn enc => 3340 arm_parse_register >>= (fn rd => 3341 arm_parse_comma >>- 3342 arm_parse_constant >>= (fn i => 3343 arm_parse_comma >>- 3344 let val sat_imm = sint_of_term i - (if unsigned then 0 else 1) in 3345 assertT (0 <= sat_imm andalso sat_imm <= 31) 3346 ("arm_parse_ssat_usat", "can only saturate in range " ^ 3347 (if unsigned then "0-31" else "1-32")) 3348 (arm_parse_register >>= (fn rn => 3349 tryT arm_parse_comma 3350 (fn _ => 3351 arm_parse_shift >>= (fn stype => 3352 assertT (mem stype [LSL_shift, ASR_shift]) 3353 ("arm_parse_ssat_usat", "only lsl and asr permitted") 3354 (arm_parse_constant >>= (fn j => 3355 let val shift32 = j ~~ ``32i`` 3356 val imm5 = if shift32 then 3357 mk_word5 0 3358 else 3359 uint_to_word ``:5`` j 3360 val sh = mk_bool (shift32 orelse 3361 not (imm5 ~~ mk_word5 0) andalso 3362 stype = ASR_shift) 3363 in 3364 assertT (not shift32 orelse stype = ASR_shift 3365 andalso enc ~~ Encoding_ARM_tm) 3366 ("arm_parse_ssat_usat", "invalid shift") 3367 (return (enc, 3368 mk_Saturate (mk_bool unsigned, 3369 mk_word5 sat_imm,rd,imm5,sh,rn))) 3370 end handle HOL_ERR {message,...} => 3371 other_errorT ("arm_parse_ssat_usat",message))))) 3372 (fn _ => 3373 return (enc, mk_Saturate 3374 (mk_bool unsigned,mk_word5 sat_imm,rd,mk_word5 0,F,rn))))) 3375 end handle HOL_ERR {message,...} => 3376 other_errorT ("arm_parse_ssat_usat", message))))); 3377 3378val arm_parse_ssat16_usat16 : bool -> (term * term) M = 3379 fn unsigned => 3380 need_v6 "arm_parse_ssat_usat" 3381 (thumb2_or_arm_okay "arm_parse_ssat_usat" 3382 (fn enc => 3383 arm_parse_register >>= (fn rd => 3384 arm_parse_comma >>- 3385 arm_parse_constant >>= (fn i => 3386 let val sat_imm = sint_of_term i - (if unsigned then 0 else 1) in 3387 assertT (0 <= sat_imm andalso sat_imm <= 15) 3388 ("arm_parse_ssat_usat", "can only saturate in range " ^ 3389 (if unsigned then "0-15" else "1-16")) 3390 (arm_parse_comma >>- 3391 arm_parse_register >>= (fn rn => 3392 return 3393 (enc,mk_Saturate_16 3394 (mk_bool unsigned,mk_word4 sat_imm,rd,rn)))) 3395 end handle HOL_ERR {message,...} => 3396 other_errorT ("arm_parse_ssat16_usat16", message))))); 3397 3398val arm_parse_ror248 : term M = 3399 arm_parse_string "ror" >>- 3400 arm_parse_constant >>= (fn i => 3401 (case sint_of_term i 3402 of 0 => return (mk_word2 0) 3403 | 8 => return (mk_word2 1) 3404 | 16 => return (mk_word2 2) 3405 | 24 => return (mk_word2 3) 3406 | _ => other_errorT ("arm_parse_ror248", 3407 "shift must be 0, 8, 16 or 24")) 3408 handle HOL_ERR {message,...} => 3409 other_errorT ("arm_parse_ror248", message)); 3410 3411val arm_parse_sxtb_etc : instruction_mnemonic -> (term * term) M = 3412 fn m => 3413 need_v6 "arm_parse_sxtb_etc" 3414 (arm_parse_register >>= (fn rd => 3415 tryT (arm_parse_comma >>- arm_parse_register) 3416 return (fn _ => return rd) >>= (fn rm => 3417 read_qualifier >>= (fn q => 3418 read_thumb >>= (fn thumb => 3419 tryT arm_parse_comma 3420 (fn _ => 3421 assertT (q <> Narrow) 3422 ("arm_parse_sxtb_etc", "unexpected trailing comma") 3423 (arm_parse_ror248 >>= 3424 (fn rot => 3425 return 3426 (if thumb then Encoding_Thumb2_tm else Encoding_ARM_tm, 3427 case m 3428 of SXTB => mk_Extend_Byte (F,mk_word4 15,rd,rot,rm) 3429 | UXTB => mk_Extend_Byte (T,mk_word4 15,rd,rot,rm) 3430 | SXTH => mk_Extend_Halfword (F,mk_word4 15,rd,rot,rm) 3431 | UXTH => mk_Extend_Halfword (T,mk_word4 15,rd,rot,rm) 3432 | _ => raise ERR "arm_parse_sxtb_etc" 3433 "unexpected mnemonic")))) 3434 (fn _ => 3435 let val narrow_okay = q <> Wide andalso narrow_registers [rd, rm] in 3436 assertT (q <> Narrow orelse narrow_okay) 3437 ("arm_parse_sxtb_etc", 3438 "invalid registers for narrow thumb instruction") 3439 (return 3440 (pick_enc thumb narrow_okay, 3441 case m 3442 of SXTB => mk_Extend_Byte (F,mk_word4 15,rd,mk_word2 0,rm) 3443 | UXTB => mk_Extend_Byte (T,mk_word4 15,rd,mk_word2 0,rm) 3444 | SXTH => mk_Extend_Halfword (F,mk_word4 15,rd,mk_word2 0,rm) 3445 | UXTH => mk_Extend_Halfword (T,mk_word4 15,rd,mk_word2 0,rm) 3446 | _ => raise ERR "arm_parse_sxtb_etc" "unexpected mnemonic")) 3447 end)))))); 3448 3449val arm_parse_sxtab_etc : instruction_mnemonic -> (term * term) M = 3450 fn m => 3451 need_v6 "arm_parse_sxtab_etc" 3452 (thumb2_or_arm_okay "arm_parse_sxtab_etc" 3453 (fn enc => 3454 arm_parse_register >>= (fn rd => 3455 arm_parse_comma >>- 3456 arm_parse_register >>= (fn rn => 3457 tryT (arm_parse_comma >>- arm_parse_register) 3458 (fn rm => return (rd,rn,rm)) 3459 (fn _ => return (rd,rd,rn)) >>= (fn (rd,rn,rm) => 3460 tryT arm_parse_comma 3461 (fn _ => arm_parse_ror248) 3462 (fn _ => return (mk_word2 0)) >>= 3463 (fn rot => 3464 return (enc, 3465 case m 3466 of SXTAB => mk_Extend_Byte (F,rn,rd,rot,rm) 3467 | UXTAB => mk_Extend_Byte (T,rn,rd,rot,rm) 3468 | SXTAB16 => mk_Extend_Byte_16 (F,rn,rd,rot,rm) 3469 | UXTAB16 => mk_Extend_Byte_16 (T,rn,rd,rot,rm) 3470 | SXTAH => mk_Extend_Halfword (F,rn,rd,rot,rm) 3471 | UXTAH => mk_Extend_Halfword (T,rn,rd,rot,rm) 3472 | _ => raise ERR "arm_parse_sxtab_etc" 3473 "unexpected mnemonic"))))))); 3474 3475val arm_parse_sxtb16_uxtb16 : term -> (term * term) M = 3476 fn unsigned => 3477 need_v6 "arm_parse_sxtb16_uxtb16" 3478 (thumb2_or_arm_okay "arm_parse_sxtb16_uxtb16" 3479 (fn enc => 3480 arm_parse_register >>= (fn rd => 3481 tryT (arm_parse_comma >>- arm_parse_register) 3482 return (fn _ => return rd) >>= (fn rm => 3483 tryT arm_parse_comma 3484 (K arm_parse_ror248) 3485 (K (return (mk_word2 0))) >>= 3486 (fn rot => 3487 return 3488 (enc, mk_Extend_Byte_16 (unsigned,mk_word4 15,rd,rot,rm))))))); 3489 3490val arm_parse_rev : instruction_mnemonic -> (term * term) M = 3491 fn m => 3492 need_v6 "arm_parse_sxtab_etc" 3493 (arm_parse_register >>= (fn rd => 3494 arm_parse_comma >>- 3495 arm_parse_register >>= (fn rm => 3496 read_qualifier >>= (fn q => 3497 read_thumb >>= (fn thumb => 3498 let val narrow_okay = q <> Wide andalso narrow_registers [rd,rm] in 3499 assertT (q <> Narrow orelse narrow_okay) 3500 ("arm_parse_rev", "invalid registers for narrow thumb instruction") 3501 (return 3502 (pick_enc thumb narrow_okay, 3503 case m 3504 of REV => mk_Byte_Reverse_Word (rd,rm) 3505 | REV16 => mk_Byte_Reverse_Packed_Halfword (rd,rm) 3506 | REVSH => mk_Byte_Reverse_Signed_Halfword (rd,rm) 3507 | _ => raise ERR "arm_parse_sxtab_etc" "unexpected mnemonic")) 3508 end))))); 3509 3510val arm_parse_rbit : (term * term) M = 3511 need_v6 "arm_parse_rbit" 3512 (thumb2_or_arm_okay "arm_parse_rbit" 3513 (fn enc => 3514 arm_parse_register >>= (fn rd => 3515 arm_parse_comma >>- 3516 arm_parse_register >>= (fn rm => 3517 return (enc,mk_Reverse_Bits (rd,rm)))))); 3518 3519val arm_parse_sbfx_etc : instruction_mnemonic -> (term * term) M = 3520 fn m => 3521 need_t2 "arm_parse_sbfx_etc" 3522 (thumb2_or_arm_okay "arm_parse_sbfx_etc" 3523 (fn enc => 3524 arm_parse_register >>= (fn rd => 3525 (if m = BFC then 3526 return (mk_word4 15) 3527 else 3528 arm_parse_comma >>- 3529 arm_parse_register) >>= (fn rn => 3530 arm_parse_comma >>- 3531 arm_parse_constant >>= (fn lsb => 3532 arm_parse_comma >>- 3533 arm_parse_constant >>= (fn width => 3534 let val l = sint_of_term lsb 3535 val w = sint_of_term width 3536 val lsb = mk_word5 l 3537 val v = w - 1 3538 in 3539 assertT (0 <= l andalso l <= 31 andalso 3540 1 <= w andalso w <= 32 - l) 3541 ("arm_parse_sbfx_etc", "invalid bit range") 3542 (return (enc, 3543 case m 3544 of SBFX => mk_Bit_Field_Extract (F,mk_word5 v,rd,lsb,rn) 3545 | UBFX => mk_Bit_Field_Extract (T,mk_word5 v,rd,lsb,rn) 3546 | BFC => mk_Bit_Field_Clear_Insert 3547 (mk_word5 (l + v),rd,lsb,rn) 3548 | BFI => mk_Bit_Field_Clear_Insert 3549 (mk_word5 (l + v),rd,lsb,rn) 3550 | _ => raise ERR "arm_parse_sbfx_etc" "invalid mnemonic")) 3551 end handle HOL_ERR {message,...} => 3552 other_errorT ("arm_parse_sbfx_etc", message))))))); 3553 3554local 3555 fun barrier_option s = 3556 mk_word4 3557 (case s 3558 of "sy" => 15 3559 | "st" => 14 3560 | "ish" => 11 3561 | "ishst" => 10 3562 | "nsh" => 7 3563 | "nshst" => 6 3564 | "osh" => 3 3565 | "oshst" => 2 3566 | _ => raise ERR "barrier_option" (s ^ "is not a barrier option")) 3567 3568 val barrier_strings = 3569 ["sy", "st", "ish", "ishst", "nsh", "nshst", "osh", "oshst"] 3570in 3571 val arm_parse_barrier : instruction_mnemonic -> (term * term) M = 3572 fn m => 3573 need_v7 "arm_parse_barrier" 3574 (thumb2_or_arm_okay "arm_parse_barrier" 3575 (fn enc => 3576 tryT (arm_parse_strings barrier_strings) 3577 return (fn _ => return "sy") >>= 3578 (fn s => 3579 assertT (m <> ISB orelse s = "sy") 3580 ("arm_parse_barrier", "sy is the only option available") 3581 (let val option = barrier_option s in 3582 return (enc, 3583 case m 3584 of DMB => mk_Data_Memory_Barrier option 3585 | DSB => mk_Data_Synchronization_Barrier option 3586 | ISB => mk_Instruction_Synchronization_Barrier option 3587 | _ => raise ERR "arm_parse_barrier" "invalid mnemonic") 3588 end)))) 3589end; 3590 3591val arm_parse_mrs : (term * term) M = 3592 thumb2_or_arm_okay "arm_parse_mrs" 3593 (fn enc => 3594 arm_parse_register >>= (fn rd => 3595 arm_parse_comma >>- 3596 arm_parse_strings ["apsr","cpsr","spsr"] >>= (fn s => 3597 return (enc, mk_Status_to_Register (mk_bool (s = "spsr"),rd))))); 3598 3599local 3600 fun psr_fields l = 3601 let fun recurse [] x = x 3602 | recurse (#"f"::t) [0,s,x,c] = recurse t [1,s,x,c] 3603 | recurse (#"s"::t) [f,0,x,c] = recurse t [f,1,x,c] 3604 | recurse (#"x"::t) [f,s,0,c] = recurse t [f,s,1,c] 3605 | recurse (#"c"::t) [f,s,x,0] = recurse t [f,s,x,1] 3606 | recurse _ _ = raise ERR "psr_fields" "" 3607 in 3608 mk_word4 (list_to_int (recurse l [0,0,0,0])) 3609 end 3610in 3611 fun decode_spec_reg s = 3612 let val ls = lower_string s in 3613 if ls = "apsr_nzcvq" then 3614 (F,mk_word4 8) 3615 else if ls = "apsr_g" then 3616 (F,mk_word4 4) 3617 else if ls = "apsr_nzcvqg" then 3618 (F,mk_word4 12) 3619 else if ls = "apsr" then 3620 (F,mk_word4 12) 3621 else if ls = "cpsr" then 3622 (F,mk_word4 15) 3623 else if ls = "spsr" then 3624 (T,mk_word4 15) 3625 else if String.isPrefix "cpsr_" ls then 3626 (F,psr_fields (List.drop (String.explode ls,5))) 3627 else if String.isPrefix "spsr_" ls then 3628 (T,psr_fields (List.drop (String.explode ls,5))) 3629 else 3630 raise ERR "decode_spec_reg" "" 3631 end 3632end; 3633 3634val arm_parse_msr : (term * term) M = 3635 thumb2_or_arm_okay "arm_parse_msr" 3636 (fn enc => 3637 (read_token >>= 3638 (fn h => 3639 case h 3640 of NONE => syntax_errorT ("psr","end-of_input") 3641 | SOME s => 3642 let val (spsr,mask) = decode_spec_reg s in 3643 next_token >>- return (spsr,mask) 3644 end handle HOL_ERR _ => 3645 syntax_errorT ("psr", Substring.string s)) >>= 3646 (fn (spsr,mask) => 3647 arm_parse_comma >>- 3648 tryT arm_parse_register 3649 (fn rn => 3650 return (enc,mk_Register_to_Status (spsr,mask,rn))) 3651 (fn _ => 3652 assertT (enc ~~ Encoding_ARM_tm) 3653 ("arm_parse_msr", "not a Thumb instruction") 3654 (arm_parse_constant >>= (fn i => 3655 let val imm12 = int_to_mode1_immediate i in 3656 return (enc, mk_Immediate_to_Status (spsr,mask,imm12)) 3657 end handle HOL_ERR {message,...} => 3658 other_errorT ("arm_parse_msr", message))))))); 3659 3660val arm_parse_cps : (term * term) M = 3661 need_v6 "arm_parse_cps" 3662 (thumb2_or_arm_okay "arm_parse_cps" 3663 (fn enc => 3664 arm_parse_constant >>= (fn i => 3665 let val imm5 = optionSyntax.mk_some (uint_to_word ``:5`` i) in 3666 return (enc,mk_Change_Processor_State (mk_word2 0,F,F,F,imm5)) 3667 end handle HOL_ERR {message,...} => 3668 other_errorT ("arm_parse_cps", message)))); 3669 3670fun cps_iflags s = 3671let fun recurse [] x = x 3672 | recurse (#"a"::t) (false,i,f) = recurse t (true,i,f) 3673 | recurse (#"i"::t) (a,false,f) = recurse t (a,true,f) 3674 | recurse (#"f"::t) (a,i,false) = recurse t (a,i,true) 3675 | recurse _ _ = raise ERR "cps_iflags" "" 3676 val (a,i,f) = recurse (String.explode (lower_string s)) (false,false,false) 3677in 3678 (mk_bool a, mk_bool i, mk_bool f) 3679end 3680 3681val arm_parse_cpsie_cpsid : term -> (term * term) M = 3682 fn imod => 3683 need_v6 "arm_parse_cps" 3684 (read_token >>= 3685 (fn h => 3686 case h 3687 of NONE => syntax_errorT ("interrupt flags", "end-of_input") 3688 | SOME s => 3689 let val (affectA,affectI,affectF) = cps_iflags s in 3690 next_token >>- return (affectA,affectI,affectF) 3691 end handle HOL_ERR _ => 3692 syntax_errorT ("interrupt flags", Substring.string s)) >>= 3693 (fn (affectA,affectI,affectF) => 3694 tryT arm_parse_comma 3695 (fn _ => 3696 arm_parse_constant >>= (fn i => 3697 let val imm5 = optionSyntax.mk_some (uint_to_word ``:5`` i) in 3698 return (false,imm5) 3699 end handle HOL_ERR {message,...} => 3700 other_errorT ("arm_parse_cpsie_cpsid", message))) 3701 (fn _ => return (true,optionSyntax.mk_none ``:word5``)) >>= 3702 (fn (narrow_okay,mode) => 3703 read_thumb >>= (fn thumb => 3704 if thumb then 3705 read_qualifier >>= (fn q => 3706 assertT (q <> Narrow orelse narrow_okay) 3707 ("arm_parse_cpsie_cpsid", 3708 "cannot set mode with narrow Thumb instruction") 3709 (return 3710 (if narrow_okay andalso q <> Wide then 3711 Encoding_Thumb_tm 3712 else 3713 Encoding_Thumb2_tm, 3714 mk_Change_Processor_State 3715 (imod,affectA,affectI,affectF,mode)))) 3716 else 3717 return (Encoding_ARM_tm, 3718 mk_Change_Processor_State 3719 (imod,affectA,affectI,affectF,mode)))))); 3720 3721val arm_parse_srs : term -> term -> (term * term) M = 3722 fn p => fn inc => 3723 need_v6 "arm_parse_srs" 3724 (thumb2_or_arm_okay "arm_parse_srs" 3725 (fn enc => 3726 assertT (enc ~~ Encoding_ARM_tm orelse p !~ inc) 3727 ("arm_parse_srs", "not available as a Thumb instruction") 3728 (arm_parse_register >>= (fn sp => 3729 assertT (is_SP sp) 3730 ("arm_parse_srs", "expecting sp") 3731 (tryT arm_parse_exclaim (K (return T)) (K (return F)) >>= 3732 (fn w => 3733 arm_parse_comma >>- 3734 arm_parse_constant >>= (fn i => 3735 let val imm5 = uint_to_word ``:5`` i in 3736 return (enc, mk_Store_Return_State (p,inc,w,imm5)) 3737 end handle HOL_ERR {message,...} => 3738 other_errorT ("arm_parse_srs", message)))))))); 3739 3740val arm_parse_rfe : term -> term -> (term * term) M = 3741 fn p => fn inc => 3742 need_v6 "arm_parse_rfe" 3743 (thumb2_or_arm_okay "arm_parse_rfe" 3744 (fn enc => 3745 assertT (enc ~~ Encoding_ARM_tm orelse p !~ inc) 3746 ("arm_parse_rfe", "not available as a Thumb instruction") 3747 (arm_parse_register >>= (fn rn => 3748 tryT arm_parse_exclaim (K (return T)) (K (return F)) >>= (fn w => 3749 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 3750 assertT OutsideOrLastInITBlock 3751 ("arm_parse_rfe", "must be outside or last in IT block") 3752 (return (enc, mk_Return_From_Exception (p,inc,w,rn))))))))); 3753 3754val arm_parse_svc : (term * term) M = 3755 arm_parse_constant >>= (fn i => 3756 read_thumb >>= (fn thumb => 3757 if thumb then 3758 read_qualifier >>= (fn q => 3759 let val v = sint_of_term i in 3760 assertT (q <> Wide andalso 0 <= v andalso v <= 255) 3761 ("arm_parse_svc", "narrow only with contant 0-255") 3762 (return (Encoding_Thumb_tm, 3763 mk_Supervisor_Call (uint_to_word ``:24`` i))) 3764 end handle HOL_ERR {message,...} => 3765 other_errorT ("arm_parse_svc", message)) 3766 else 3767 let val imm24 = uint_to_word ``:24`` i in 3768 return (Encoding_ARM_tm, mk_Supervisor_Call imm24) 3769 end handle HOL_ERR {message,...} => 3770 other_errorT ("arm_parse_svc", message))); 3771 3772val arm_parse_smc : (term * term) M = 3773 thumb2_or_arm_okay "arm_parse_smc" 3774 (fn enc => 3775 arm_parse_constant >>= (fn i => 3776 read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => 3777 let val imm4 = uint_to_word ``:4`` i in 3778 assertT OutsideOrLastInITBlock 3779 ("arm_parse_smc", "must be outside or last in IT block") 3780 (return (enc, mk_Secure_Monitor_Call imm4)) 3781 end handle HOL_ERR {message,...} => 3782 other_errorT ("arm_parse_smc", message)))); 3783 3784val arm_parse_bkpt : (term * term) M = 3785 need_v5 "arm_parse_bkpt" 3786 (arm_parse_constant >>= (fn i => 3787 read_thumb >>= (fn thumb => 3788 if thumb then 3789 read_qualifier >>= (fn q => 3790 let val v = sint_of_term i in 3791 assertT (q <> Wide andalso 0 <= v andalso v <= 255) 3792 ("arm_parse_bkpt", "narrow only with contant 0-255") 3793 (return (Encoding_Thumb_tm, 3794 mk_Breakpoint (uint_to_word ``:16`` i))) 3795 end handle HOL_ERR {message,...} => 3796 other_errorT ("arm_parse_bkpt", message)) 3797 else 3798 let val imm16 = uint_to_word ``:16`` i in 3799 return (Encoding_ARM_tm, mk_Breakpoint imm16) 3800 end handle HOL_ERR {message,...} => 3801 other_errorT ("arm_parse_bkpt", message)))); 3802 3803val arm_parse_nop : (term * term) M = 3804 read_thumb >>= (fn thumb => 3805 arch_okay ("arm_parse_nop", "not supported by selected architecture") 3806 (fn a => has_thumb2 a orelse not thumb andalso a = ARMv6K) 3807 (if thumb then 3808 read_qualifier >>= (fn q => 3809 return (if q <> Wide then Encoding_Thumb_tm else Encoding_Thumb2_tm, 3810 mk_Hint Hint_nop_tm)) 3811 else 3812 return (Encoding_ARM_tm, mk_Hint Hint_nop_tm))); 3813 3814fun hint YIELD = Hint_yield_tm 3815 | hint WFE = Hint_wait_for_event_tm 3816 | hint WFI = Hint_wait_for_interrupt_tm 3817 | hint SEV = Hint_send_event_tm 3818 | hint _ = raise ERR "hint" "invalid mnemonic"; 3819 3820val arm_parse_hint : instruction_mnemonic -> (term * term) M = 3821 fn m => 3822 read_thumb >>= (fn thumb => 3823 arch_okay ("arm_parse_hint", "not supported by selected architecture") 3824 (fn a => a = ARMv6T2 orelse version_number a >= 7 orelse 3825 not thumb andalso a = ARMv6K) 3826 (if thumb then 3827 read_qualifier >>= (fn q => 3828 return 3829 (if q <> Wide then Encoding_Thumb_tm else Encoding_Thumb2_tm, 3830 mk_Hint (hint m))) 3831 else 3832 return (Encoding_ARM_tm, mk_Hint (hint m)))); 3833 3834val arm_parse_dbg : (term * term) M = 3835 read_thumb >>= (fn thumb => 3836 arch_okay ("arm_parse_dbg", "not supported by selected architecture") 3837 (fn a => a = ARMv6T2 orelse version_number a >= 7 orelse 3838 not thumb andalso a = ARMv6K) 3839 (arm_parse_constant >>= (fn i => 3840 let val v = sint_of_term i in 3841 assertT (0 <= v andalso v <= 15) 3842 ("arm_parse_dbg", "constant must be in range 0-15") 3843 (let val instr = mk_Hint (mk_Hint_debug (mk_word4 v)) in 3844 if thumb then 3845 not_narrow "arm_parse_dbg" 3846 (return (Encoding_Thumb2_tm, instr)) 3847 else 3848 return (Encoding_ARM_tm, instr) 3849 end) 3850 end))); 3851 3852(* ------------------------------------------------------------------------- *) 3853 3854val arm_parse_enterx_leavex : term -> (term * term) M = 3855 fn is_enterx => 3856 need_v7 "arm_parse_enterx" 3857 (thumb2_okay "arm_parse_enterx" 3858 (return (Encoding_Thumb2_tm, mk_Enterx_Leavex is_enterx))); 3859 3860val arm_parse_check_array : (term * term) M = 3861 read_thumbee >>= (fn thumbee => 3862 read_qualifier >>= (fn q => 3863 assertT (thumbee andalso q <> Wide) 3864 ("arm_parse_check_array", "only available as narrow ThumbEE instruction") 3865 (arm_parse_register >>= (fn rn => 3866 arm_parse_comma >>- 3867 arm_parse_register >>= (fn rm => 3868 return (Encoding_ThumbEE_tm, mk_Check_Array (rn,rm))))))); 3869 3870val arm_parse_handler_branch_link : term -> (term * term) M = 3871 fn link => 3872 read_thumbee >>= (fn thumbee => 3873 read_qualifier >>= (fn q => 3874 assertT (thumbee andalso q <> Wide) 3875 ("arm_parse_handler_branch_link", 3876 "only available as narrow ThumbEE instruction") 3877 (arm_parse_constant >>= (fn i => 3878 let val h = uint_to_word ``:8`` i in 3879 return (Encoding_ThumbEE_tm, mk_Handler_Branch_Link (link,h)) 3880 end handle HOL_ERR {message,...} => 3881 other_errorT ("arm_parse_handler_branch_link", message))))); 3882 3883val arm_parse_handler_branch_parameter : (term * term) M = 3884 read_thumbee >>= (fn thumbee => 3885 read_qualifier >>= (fn q => 3886 assertT (thumbee andalso q <> Wide) 3887 ("arm_parse_handler_branch_parameter", 3888 "only available as narrow ThumbEE instruction") 3889 (arm_parse_constant >>= (fn i => 3890 arm_parse_comma >>- 3891 arm_parse_constant >>= (fn j => 3892 let val imm3 = uint_to_word ``:3`` i 3893 val h = uint_to_word ``:5`` j 3894 in 3895 return (Encoding_ThumbEE_tm, mk_Handler_Branch_Parameter (imm3,h)) 3896 end handle HOL_ERR {message,...} => 3897 other_errorT ("arm_parse_handler_branch_parameter", message)))))); 3898 3899val arm_parse_handler_branch_link_parameter : (term * term) M = 3900 read_thumbee >>= (fn thumbee => 3901 read_qualifier >>= (fn q => 3902 assertT (thumbee andalso q <> Wide) 3903 ("arm_parse_handler_branch_link_parameter", 3904 "only available as narrow ThumbEE instruction") 3905 (arm_parse_constant >>= (fn i => 3906 arm_parse_comma >>- 3907 arm_parse_constant >>= (fn j => 3908 let val imm5 = uint_to_word ``:5`` i 3909 val h = uint_to_word ``:5`` j 3910 in 3911 return 3912 (Encoding_ThumbEE_tm, 3913 mk_Handler_Branch_Link_Parameter (imm5,h)) 3914 end handle HOL_ERR {message,...} => 3915 other_errorT 3916 ("arm_parse_handler_branch_link_parameter", message)))))); 3917 3918(* ------------------------------------------------------------------------- *) 3919 3920val arm_parse_ldc_stc : instruction_mnemonic -> (term * term) M = 3921 fn m => 3922 thumb2_or_arm_okay "arm_parse_smc" 3923 (fn enc => 3924 arm_parse_coprocessor >>= (fn coproc => 3925 arm_parse_comma >>- 3926 arm_parse_cregister >>= (fn crd => 3927 arm_parse_comma >>- 3928 arm_parse_lsquare >>- 3929 arm_parse_register >>= (fn rn => 3930 tryT arm_parse_rsquare 3931 (fn _ => 3932 tryT arm_parse_comma 3933 (fn _ => 3934 tryT arm_parse_constant 3935 (fn i => 3936 let val v = sint_of_term i in 3937 assertT 3938 (v mod 4 = 0 andalso ~1020 <= v andalso v <= 1020) 3939 ("arm_parse_ldc_stc", 3940 "offset not aligned or beyond permitted range\ 3941 \ (+/-1020)") 3942 (return 3943 (F,mk_bool (0 <= v andalso not (i ~~ ``-0i``)),T, 3944 mk_word8 (Int.abs (v div 4)))) 3945 end handle HOL_ERR {message,...} => 3946 other_errorT ("arm_parse_ldc_stc", message)) 3947 (fn _ => 3948 arm_parse_lbrace >>- 3949 arm_parse_number >>= (fn i => 3950 arm_parse_rbrace >>- 3951 let val imm8 = int_to_word ``:8`` i in 3952 return (F,T,F,imm8) 3953 end handle HOL_ERR {message,...} => 3954 other_errorT ("arm_parse_ldc_stc", message)))) 3955 (fn _ => return (T,T,F,mk_word8 0))) 3956 (fn _ => 3957 arm_parse_comma >>- 3958 arm_parse_constant >>= (fn i => 3959 arm_parse_rsquare >>- 3960 tryT arm_parse_exclaim (K (return T)) (K (return F)) >>= (fn w => 3961 let val v = sint_of_term i in 3962 assertT 3963 (v mod 4 = 0 andalso ~1020 <= v andalso v <= 1020) 3964 ("arm_parse_ldc_stc", 3965 "offset not aligned or beyond permitted range (+/-1020)") 3966 (return (T,mk_bool (0 <= v andalso not (i ~~ ``-0i``)),w, 3967 mk_word8 (Int.abs (v div 4)))) 3968 end handle HOL_ERR {message,...} => 3969 other_errorT ("arm_parse_ldc_stc", message)))) >>= 3970 (fn (p,u,w,imm8) => 3971 return (enc, 3972 case m 3973 of LDC => mk_Coprocessor_Load (p,u,F,w,rn,crd,coproc,imm8) 3974 | LDC2 => mk_Coprocessor_Load (p,u,F,w,rn,crd,coproc,imm8) 3975 | LDCL => mk_Coprocessor_Load (p,u,T,w,rn,crd,coproc,imm8) 3976 | LDC2L => mk_Coprocessor_Load (p,u,T,w,rn,crd,coproc,imm8) 3977 | STC => mk_Coprocessor_Store (p,u,F,w,rn,crd,coproc,imm8) 3978 | STC2 => mk_Coprocessor_Store (p,u,F,w,rn,crd,coproc,imm8) 3979 | STCL => mk_Coprocessor_Store (p,u,T,w,rn,crd,coproc,imm8) 3980 | STC2L => mk_Coprocessor_Store (p,u,T,w,rn,crd,coproc,imm8) 3981 | _ => raise ERR "arm_parse_ldc_stc" "unexpected mnemonic")))))); 3982 3983val arm_parse_cdp : (term * term) M = 3984 thumb2_or_arm_okay "arm_parse_smc" 3985 (fn enc => 3986 arm_parse_coprocessor >>= (fn coproc => 3987 arm_parse_comma >>- 3988 arm_parse_constant >>= (fn opc1 => 3989 arm_parse_comma >>- 3990 arm_parse_cregister >>= (fn crd => 3991 arm_parse_comma >>- 3992 arm_parse_cregister >>= (fn crn => 3993 arm_parse_comma >>- 3994 arm_parse_cregister >>= (fn crm => 3995 tryT (arm_parse_comma >>- arm_parse_constant) 3996 (fn i => 3997 let val imm3 = int_to_word ``:3`` i in 3998 return imm3 3999 end handle HOL_ERR {message,...} => 4000 other_errorT ("arm_parse_cdp", message)) 4001 (fn _ => return (mk_word3 0)) >>= (fn opc2 => 4002 let val imm4 = int_to_word ``:4`` opc1 in 4003 return (enc, 4004 mk_Coprocessor_Data_Processing (imm4,crn,crd,coproc,opc2,crm)) 4005 end handle HOL_ERR {message,...} => 4006 other_errorT ("arm_parse_cdp", message)))))))); 4007 4008val arm_parse_mrc_mcr : instruction_mnemonic -> (term * term) M = 4009 fn m => 4010 thumb2_or_arm_okay "arm_parse_smc" 4011 (fn enc => 4012 arm_parse_coprocessor >>= (fn coproc => 4013 arm_parse_comma >>- 4014 arm_parse_constant >>= (fn opc1 => 4015 arm_parse_comma >>- 4016 arm_parse_register >>= (fn rt => 4017 arm_parse_comma >>- 4018 arm_parse_cregister >>= (fn crn => 4019 arm_parse_comma >>- 4020 arm_parse_cregister >>= (fn crm => 4021 tryT (arm_parse_comma >>- arm_parse_constant) 4022 (fn i => 4023 let val imm3 = int_to_word ``:3`` i in 4024 return imm3 4025 end handle HOL_ERR {message,...} => 4026 other_errorT ("arm_parse_mrc_mcr", message)) 4027 (fn _ => return (mk_word3 0)) >>= (fn opc2 => 4028 let val imm3 = int_to_word ``:3`` opc1 4029 val b = mk_bool (m = MRC orelse m = MRC2) 4030 in 4031 return (enc, mk_Coprocessor_Transfer (imm3,b,crn,rt,coproc,opc2,crm)) 4032 end handle HOL_ERR {message,...} => 4033 other_errorT ("arm_parse_mrc_mcr", message)))))))); 4034 4035val arm_parse_mrrc_mcrr : instruction_mnemonic -> (term * term) M = 4036 fn m => 4037 thumb2_or_arm_okay "arm_parse_smc" 4038 (fn enc => 4039 arm_parse_coprocessor >>= (fn coproc => 4040 arm_parse_comma >>- 4041 arm_parse_constant >>= (fn opc1 => 4042 arm_parse_comma >>- 4043 arm_parse_register >>= (fn rt => 4044 arm_parse_comma >>- 4045 arm_parse_register >>= (fn rt2 => 4046 arm_parse_comma >>- 4047 arm_parse_cregister >>= (fn crm => 4048 let val imm4 = int_to_word ``:4`` opc1 4049 val b = mk_bool (m = MRRC orelse m = MRRC2) 4050 in 4051 return (enc, mk_Coprocessor_Transfer_Two (b,rt2,rt,coproc,imm4,crm)) 4052 end handle HOL_ERR {message,...} => 4053 other_errorT ("arm_parse_mrrc_mcrr", message))))))); 4054 4055(* ------------------------------------------------------------------------- *) 4056 4057datatype line 4058 = Align of int 4059 | Ascii1 of string 4060 | Label of int * string 4061 | Byte1 of term list 4062 | Short1 of term list 4063 | Word1 of term list 4064 | Space of term 4065 | Instruction1 of int * term * term * term; 4066 4067val arm_parse_instruction : line M = 4068 arm_parse_mnemonic >>= (fn m => 4069 (case m 4070 of B => arm_parse_branch_target 4071 | BL => arm_parse_branch_link 4072 | BLX => arm_parse_branch_link_exchange 4073 | BX => arm_parse_bx 4074 | BFC => arm_parse_sbfx_etc m 4075 | BFI => arm_parse_sbfx_etc m 4076 | CBZ => arm_parse_cbz_cbnz F 4077 | CBNZ => arm_parse_cbz_cbnz T 4078 | CLZ => arm_parse_clz 4079 | CLREX => arm_parse_clrex 4080 | CDP => arm_parse_cdp 4081 | CDP2 => arm_parse_cdp 4082 | CHKA => arm_parse_check_array 4083 | ENTERX => arm_parse_enterx_leavex T 4084 | LEAVEX => arm_parse_enterx_leavex F 4085 | HB => arm_parse_handler_branch_link F 4086 | HBL => arm_parse_handler_branch_link T 4087 | HBLP => arm_parse_handler_branch_link_parameter 4088 | HBP => arm_parse_handler_branch_parameter 4089 | IT => arm_parse_it 4090 | ADR => arm_parse_adr 4091 | ADDW => arm_parse_addw_subw T 4092 | SUBW => arm_parse_addw_subw F 4093 | RRX => arm_parse_rrx 4094 | MOVW => arm_parse_mov_halfword F 4095 | MOVT => arm_parse_mov_halfword T 4096 | MUL => arm_parse_mul 4097 | PKHBT => arm_parse_pkh F 4098 | PKHTB => arm_parse_pkh T 4099 | REV => arm_parse_rev m 4100 | REV16 => arm_parse_rev m 4101 | REVSH => arm_parse_rev m 4102 | RBIT => arm_parse_rbit 4103 | UDIV => arm_parse_div T 4104 | SDIV => arm_parse_div F 4105 | SSAT => arm_parse_ssat_usat false 4106 | USAT => arm_parse_ssat_usat true 4107 | SSAT16 => arm_parse_ssat16_usat16 false 4108 | USAT16 => arm_parse_ssat16_usat16 true 4109 | SXTB => arm_parse_sxtb_etc m 4110 | UXTB => arm_parse_sxtb_etc m 4111 | SXTH => arm_parse_sxtb_etc m 4112 | UXTH => arm_parse_sxtb_etc m 4113 | SXTB16 => arm_parse_sxtb16_uxtb16 F 4114 | UXTB16 => arm_parse_sxtb16_uxtb16 T 4115 | SBFX => arm_parse_sbfx_etc m 4116 | UBFX => arm_parse_sbfx_etc m 4117 | DMB => arm_parse_barrier m 4118 | DSB => arm_parse_barrier m 4119 | ISB => arm_parse_barrier m 4120 | CPS => arm_parse_cps 4121 | CPSIE => arm_parse_cpsie_cpsid (mk_word2 2) 4122 | CPSID => arm_parse_cpsie_cpsid (mk_word2 3) 4123 | SETEND => arm_parse_setend 4124 | SVC => arm_parse_svc 4125 | SMC => arm_parse_smc 4126 | BKPT => arm_parse_bkpt 4127 | NOP => arm_parse_nop 4128 | DBG => arm_parse_dbg 4129 | LDMIA => arm_parse_ldm_stm true F T 4130 | LDMDA => arm_parse_ldm_stm true F F 4131 | LDMDB => arm_parse_ldm_stm true T F 4132 | LDMIB => arm_parse_ldm_stm true T T 4133 | LDR => arm_parse_mode2 true F 4134 | LDRB => arm_parse_mode2 true T 4135 | LDRH => arm_parse_mode3 (SOME (F,T)) 4136 | LDRSB => arm_parse_mode3 (SOME (T,F)) 4137 | LDRSH => arm_parse_mode3 (SOME (T,T)) 4138 | LDRD => arm_parse_mode3_dual true 4139 | LDREX => arm_parse_ldrex 4140 | LDREXB => arm_parse_ldrexb_ldrexh false 4141 | LDREXD => arm_parse_ldrexd 4142 | LDREXH => arm_parse_ldrexb_ldrexh true 4143 | MRS => arm_parse_mrs 4144 | MSR => arm_parse_msr 4145 | POP => arm_parse_pop_push true 4146 | PUSH => arm_parse_pop_push false 4147 | RFEIA => arm_parse_rfe F T 4148 | RFEDA => arm_parse_rfe F F 4149 | RFEDB => arm_parse_rfe T F 4150 | RFEIB => arm_parse_rfe T T 4151 | STMIA => arm_parse_ldm_stm false F T 4152 | STMDA => arm_parse_ldm_stm false F F 4153 | STMDB => arm_parse_ldm_stm false T F 4154 | STMIB => arm_parse_ldm_stm false T T 4155 | STR => arm_parse_mode2 false F 4156 | STRB => arm_parse_mode2 false T 4157 | STRH => arm_parse_mode3 NONE 4158 | STRD => arm_parse_mode3_dual false 4159 | STRT => arm_parse_mode2_unpriv false F 4160 | STRBT => arm_parse_mode2_unpriv false T 4161 | STRHT => arm_parse_mode3_unpriv NONE 4162 | STREX => arm_parse_strex 4163 | STREXB => arm_parse_strexb_strexh false 4164 | STREXD => arm_parse_strexd 4165 | STREXH => arm_parse_strexb_strexh true 4166 | SWP => arm_parse_swp F 4167 | SWPB => arm_parse_swp T 4168 | SRSIA => arm_parse_srs F T 4169 | SRSDA => arm_parse_srs F F 4170 | SRSDB => arm_parse_srs T F 4171 | SRSIB => arm_parse_srs T T 4172 | TBB => arm_parse_tbb 4173 | TBH => arm_parse_tbh 4174 | PLD => arm_parse_pld_pli (SOME false) 4175 | PLDW => arm_parse_pld_pli (SOME true) 4176 | PLI => arm_parse_pld_pli NONE 4177 | LDRT => arm_parse_mode2_unpriv true F 4178 | LDRBT => arm_parse_mode2_unpriv true T 4179 | LDRHT => arm_parse_mode3_unpriv (SOME (F,T)) 4180 | LDRSBT => arm_parse_mode3_unpriv (SOME (T,F)) 4181 | LDRSHT => arm_parse_mode3_unpriv (SOME (T,T)) 4182 | _ => (if is_data_processing3 m then 4183 arm_parse_data_processing3 m 4184 else if is_data_processing2 m then 4185 arm_parse_data_processing2 m 4186 else if mem m [LSL,ASR,LSR,ROR] then 4187 arm_parse_mov_shift m 4188 else if is_thumb2_3 m then 4189 arm_parse_thumb2_3 4190 else if is_thumb2_4 m then 4191 arm_parse_thumb2_4 4192 else if mem m [SXTAB,UXTAB,SXTAB16,UXTAB16,SXTAH,UXTAH] then 4193 arm_parse_sxtab_etc m 4194 else if mem m [YIELD,WFI,WFE,SEV] then 4195 arm_parse_hint m 4196 else if mem m [LDC,LDCL,LDC2,LDC2L,STC,STCL,STC2,STC2L] then 4197 arm_parse_ldc_stc m 4198 else if mem m [MRC,MRC2,MCR,MCR2] then 4199 arm_parse_mrc_mcr m 4200 else if mem m [MRRC,MRRC2,MCRR,MCRR2] then 4201 arm_parse_mrrc_mcrr m 4202 else 4203 other_errorT 4204 ("arm_parse_instruction", "not supported yet"))) >>= 4205 (fn (enc,tm) => 4206 if m = IT andalso enc ~~ boolSyntax.arb then 4207 write_instruction NONE >>- return (Space ``0i``) 4208 else 4209 read_cond >>= (fn cond => 4210 write_instruction NONE >>- 4211 (if m <> IT then next_itstate else return ()) >>- 4212 read_linenumber >>= (fn line => 4213 return (Instruction1 (line,enc,cond,tm)))))); 4214 4215local 4216 val arch_versions = 4217 ["armv4", "armv4t", "armv5t", "armv5te", 4218 "armv6", "armv6k", "armv6t2", "armv7"] 4219in 4220 val arm_parse_arch : unit M = 4221 arm_parse_strings arch_versions >>= (fn v => 4222 case v 4223 of "armv4" => write_arch ARMv4 4224 | "armv4t" => write_arch ARMv4T 4225 | "armv5t" => write_arch ARMv5T 4226 | "armv5te" => write_arch ARMv5TE 4227 | "armv6" => write_arch ARMv6 4228 | "armv6k" => write_arch ARMv6K 4229 | "armv6t2" => write_arch ARMv6T2 4230 | "armv7" => tryT arm_parse_minus 4231 (fn _ => 4232 arm_parse_strings ["a","m","r"] >>= (fn s => 4233 case s 4234 of "a" => write_arch ARMv7_A 4235 | "r" => write_arch ARMv7_R 4236 | _ => raise ERR "arm_parse_arch" "")) 4237 (fn _ => write_arch ARMv7_A) 4238 | _ => raise ERR "arm_parse_arch" "") 4239end; 4240 4241val switch_to_arm : unit M = write_code ARM_CODE; 4242 4243val switch_to_thumb : unit M = 4244 read_arch >>= (fn a => 4245 assertT (a <> ARMv4) 4246 ("switch_to_thumb", "ARMv4 does not support Thumb") 4247 (write_code THUMB_CODE)); 4248 4249val switch_to_thumbx : unit M = 4250 read_arch >>= (fn a => 4251 assertT (a = ARMv7_A orelse a = ARMv7_R) 4252 ("switch_to_thumb", "ThumbEE not supported before ARMv7") 4253 (write_code THUMBX_CODE)); 4254 4255local 4256 fun arm_parse_number_list (l : term list) (P : term -> bool) : term list M = 4257 tryT arm_parse_signed_number 4258 (fn h => 4259 assertT (P h) 4260 ("arm_parse_number_list", "number not in expected range") 4261 (tryT arm_parse_comma 4262 (fn _ => arm_parse_number_list (l @ [h]) P) 4263 (fn _ => return (l @ [h])))) 4264 (fn _ => 4265 assertT (not (null l)) 4266 ("arm_parse_number_list", "not a valid number list") 4267 (return l)) 4268 4269 fun in_range (mn,mx) tm = 4270 let val v = sint_of_term tm in 4271 mn <= v andalso v <= mx 4272 end handle HOL_ERR _ => false | Overflow => false; 4273 4274 val word_min = Arbint.~ (Arbint.fromString "2147483648") 4275 val word_max = Arbint.fromString "4294967295" 4276in 4277 val arm_parse_number_list = arm_parse_number_list [] 4278 4279 val is_byte = in_range (~128,255) 4280 val is_short = in_range (~32768,65535) 4281 fun is_word tm = 4282 let open Arbint 4283 val v = intSyntax.int_of_term tm 4284 in 4285 word_min <= v andalso v <= word_max 4286 end handle HOL_ERR _ => false; 4287end; 4288 4289val arm_parse_align : line M = 4290 tryT (arm_parse_strings ["2","4","8"]) 4291 (fn i => 4292 case i 4293 of "2" => return (Align 2) 4294 | "4" => return (Align 4) 4295 | "8" => return (Align 8) 4296 | _ => raise ERR "arm_parse_align" "") 4297 (fn _ => 4298 read_thumb >>= (fn thumb => return (Align (if thumb then 2 else 4)))); 4299 4300local 4301 val directives = 4302 ["arch","code","code16","code32","arm","thumb","thumbx", 4303 "ascii","byte","short","word","align","space"] 4304in 4305 val arm_parse_line : line list M = 4306 tryT (arm_parse_strings directives) 4307 (fn s => 4308 (case s 4309 of "arch" => arm_parse_arch >>- return [] 4310 | "code" => arm_parse_strings ["16","32"] >>= (fn i => 4311 (case i 4312 of "16" => switch_to_thumb >>- return ([Align 2]) 4313 | "32" => switch_to_arm >>- return ([Align 4]) 4314 | _ => raise ERR "arm_parse_directive" "")) 4315 | "arm" => switch_to_arm >>- return ([Align 4]) 4316 | "code32" => switch_to_arm >>- return ([Align 4]) 4317 | "thumb" => switch_to_thumb >>- return ([Align 2]) 4318 | "code16" => switch_to_thumb >>- return ([Align 2]) 4319 | "thumbx" => switch_to_thumbx >>- return ([Align 2]) 4320 | "ascii" => arm_parse_string_const >>= (fn s => 4321 assertT (Lib.all Char.isAscii (explode s)) 4322 ("arm_parse_line", "not an Ascii string") 4323 (return ([Ascii1 s]))) 4324 | "byte" => arm_parse_number_list is_byte >>= (fn l => 4325 return ([Byte1 l])) 4326 | "short" => arm_parse_number_list is_short >>= (fn l => 4327 return ([Short1 l])) 4328 | "word" => arm_parse_number_list is_word >>= (fn l => 4329 return ([Word1 l])) 4330 | "space" => arm_parse_number >>= (fn i => return ([Space i])) 4331 | "align" => arm_parse_align >>= (fn l => return ([l])) 4332 | _ => raise ERR "arm_parse_directive" "")) 4333 (fn _ => arm_parse_instruction >>= (fn instr => return ([instr]))) >>= 4334 (fn l => arm_parse_endline >>- return l) 4335end; 4336 4337val arm_parse_label : line list M = 4338 arm_parse_variable ``:unit`` >>= (fn label => 4339 arm_parse_colon >>- 4340 read_linenumber >>= (fn line => 4341 return ([Label (line,label |> dest_var |> fst)]))); 4342 4343val arm_parse_labelled_line : line list M = 4344 tryT arm_parse_endline (fn _ => return []) (fn _ => 4345 tryT arm_parse_label return (fn _ => return []) >>= 4346 (fn label => 4347 tryT arm_parse_endline (fn _ => return label) 4348 (fn _ => arm_parse_line >>= (fn l => return (label @ l))))); 4349 4350fun arm_parse_lines (l1 : line list) : line list M = 4351 arm_parse_endoffile >>= (fn endoffile => 4352 if endoffile then 4353 read_InITBlock >>= (fn InITBlock => 4354 let val _ = if InITBlock then 4355 HOL_WARNING "arm_parserLib" "arm_parse_lines" 4356 "code finished before end of IT block" 4357 else () 4358 in 4359 return l1 4360 end) 4361 else 4362 arm_parse_labelled_line >>= (fn l2 => arm_parse_lines (l1 @ l2))); 4363 4364(* ------------------------------------------------------------------------- *) 4365 4366datatype arm_code 4367 = Ascii of string 4368 | Byte of term list 4369 | Short of term list 4370 | Word of term list 4371 | Instruction of term * term * term; 4372 4373fun arm_code_cmp (Ascii s1, Ascii s2) = String.compare (s1,s2) 4374 | arm_code_cmp (Ascii _, _) = LESS 4375 | arm_code_cmp (_, Ascii _) = GREATER 4376 | arm_code_cmp (Byte tl1, Byte tl2) = list_compare Term.compare (tl1, tl2) 4377 | arm_code_cmp (Byte _, _) = LESS 4378 | arm_code_cmp (_, Byte _) = GREATER 4379 | arm_code_cmp (Short tl1, Short tl2) = list_compare Term.compare (tl1, tl2) 4380 | arm_code_cmp (Short _, _) = LESS 4381 | arm_code_cmp (_, Short _) = GREATER 4382 | arm_code_cmp (Word tl1, Word tl2) = list_compare Term.compare (tl1, tl2) 4383 | arm_code_cmp (Word _, _) = LESS 4384 | arm_code_cmp (_, Word _) = GREATER 4385 | arm_code_cmp (Instruction(t1,t2,t3), Instruction(ta, tb, tc)) = 4386 list_compare Term.compare ([t1,t2,t3], [ta,tb,tc]) 4387 4388fun arm_code_eq ac1 ac2 = arm_code_cmp(ac1,ac2) = EQUAL 4389 4390 4391local 4392 open Arbnum 4393 val n4 = fromInt 4 4394in 4395 fun align (line,e) = 4396 line + (if e ~~ Encoding_ARM_tm then 4397 (n4 - (line mod n4)) mod n4 4398 else 4399 (two - (line mod two)) mod two) 4400 4401 fun inc_code_width line (Label _) = line 4402 | inc_code_width line (Ascii1 s) = line + (s |> String.size |> fromInt) 4403 | inc_code_width line (Byte1 l) = line + (l |> List.length |> fromInt) 4404 | inc_code_width line (Short1 l) = 4405 line + (l |> List.length |> fromInt |> times2) 4406 | inc_code_width line (Word1 l) = 4407 line + (l |> List.length |> fromInt) * n4 4408 | inc_code_width line (Space n) = 4409 line + (n |> intSyntax.int_of_term |> Arbint.toNat) 4410 | inc_code_width line (Align i) = 4411 let val n = fromInt i in line + (n - (line mod n)) mod n end 4412 | inc_code_width line (Instruction1 (_,e,_,_)) = 4413 align (line,e) + 4414 (if e ~~ Encoding_Thumb_tm orelse e ~~ Encoding_ThumbEE_tm then 4415 two 4416 else 4417 n4) 4418end; 4419 4420local 4421 val n4 = Arbnum.fromInt 4 4422 val vname = fst o dest_var 4423 4424 fun Add_Sub_label tm = 4425 let val (_,_,_,imm12) = dest_Add_Sub tm in vname imm12 end 4426 4427 fun Load_label tm = 4428 let val (_,_,_,_,_,_,_,mode2) = dest_Load tm in vname mode2 end 4429 4430 fun find_forward _ _ [] = raise ERR "find_forward" "label not found" 4431 | find_forward (x as (line,v)) n ((Label (_,s))::t) = 4432 if v = s then 4433 SOME (Arbint.-(Arbint.fromNat n,Arbint.fromNat (Arbnum.+(line,n4)))) 4434 else 4435 find_forward x n t 4436 | find_forward x n ((c as Instruction1 (_,enc,_,_))::t) = 4437 if is_genvar enc then 4438 NONE 4439 else 4440 find_forward x (inc_code_width n c) t 4441 | find_forward x n (h::t) = find_forward x (inc_code_width n h) t; 4442 4443 fun inst_enc (Instruction1 (_,e,_,_)) = e 4444 | inst_enc _ = raise ERR "inst_enc" ""; 4445 4446 fun number_lines [] (line,code,lmap) = (code,lmap) 4447 | number_lines (h::t) (line,code,lmap) = 4448 number_lines t 4449 (case h 4450 of Align n => (inc_code_width line h,code,lmap) 4451 | Space t => (inc_code_width line h,code,lmap) 4452 | Ascii1 s => (inc_code_width line h,(line,h)::code,lmap) 4453 | Byte1 t => (inc_code_width line h,(line,h)::code,lmap) 4454 | Short1 t => (inc_code_width line h,(line,h)::code,lmap) 4455 | Word1 t => (inc_code_width line h,(line,h)::code,lmap) 4456 | Label (i,s) => 4457 let val _ = not (isSome (Redblackmap.peek (lmap,s))) orelse 4458 raise ERR "number_lines" 4459 ("label " ^ s ^ " duplicated on line " ^ Int.toString i) 4460 in 4461 (line,code,Redblackmap.insert (lmap,s,line)) 4462 end 4463 | Instruction1 (i,enc,cond,tm) => 4464 let val h' = 4465 if not (is_genvar enc) then 4466 h 4467 else 4468 let fun pick b = Instruction1 4469 (i,if b then Encoding_Thumb_tm 4470 else Encoding_Thumb2_tm,cond,tm) 4471 in 4472 if is_Branch_Target tm then 4473 let val v = vname (dest_Branch_Target tm) in 4474 case Redblackmap.peek (lmap,v) 4475 of SOME address => 4476 let open Arbnum 4477 val offset = line + n4 - address 4478 val narrow_okay = 4479 if is_AL cond then 4480 offset <= (fromString "2048") 4481 else 4482 offset <= (fromString "256") 4483 in 4484 pick narrow_okay 4485 end 4486 | NONE => 4487 let open Arbint in 4488 case find_forward (line,v) 4489 (inc_code_width line (pick true)) t 4490 of SOME offset => 4491 let val narrow_okay = 4492 if is_AL cond then 4493 (fromString "-2048") <= offset 4494 andalso 4495 offset <= (fromString "2046") 4496 else 4497 (fromString "-256") <= offset 4498 andalso 4499 offset <= (fromString "254") 4500 in 4501 pick narrow_okay 4502 end 4503 | NONE => pick false 4504 end handle HOL_ERR _ => 4505 raise ERR "number_lines" ("cannot find label " ^ 4506 v ^ " on line " ^ Int.toString i) 4507 end 4508 else if is_Add_Sub tm orelse is_Load tm then 4509 let val v = if is_Add_Sub tm then 4510 Add_Sub_label tm 4511 else 4512 Load_label tm 4513 in 4514 case Redblackmap.peek (lmap,v) 4515 of SOME _ => pick false 4516 | NONE => 4517 let open Arbint in 4518 case find_forward (line,v) 4519 (inc_code_width line (pick true)) t 4520 of SOME offset => 4521 let val narrow_okay = 4522 offset mod (fromInt 4) = zero 4523 andalso 4524 (fromString "0") <= offset 4525 andalso 4526 offset <= (fromString "1020") 4527 in 4528 pick narrow_okay 4529 end 4530 | NONE => pick false 4531 end handle HOL_ERR _ => 4532 raise ERR "number_lines" ("cannot find label " ^ 4533 v ^ " on line " ^ Int.toString i) 4534 end 4535 else raise ERR "number_lines" "unexpected genvar" 4536 end 4537 in 4538 (inc_code_width line h',(align (line,inst_enc h'),h')::code, 4539 lmap) 4540 end) 4541 4542 fun link_lines (l1,lmap) = 4543 let 4544 fun in_range (mn,mx) i = mn <= i andalso i <= mx 4545 fun aligned (i,n) = i mod n = 0 4546 fun enc_pc n enc = 4547 let open Arbint in 4548 fromNat n + fromInt (if enc ~~ Encoding_ARM_tm then 8 else 4) 4549 end 4550 fun align_pc n enc = 4551 let open Arbint 4552 val i4 = fromInt 4 4553 val pc = enc_pc n enc 4554 in 4555 (pc div i4) * i4 4556 end 4557 fun link_instruction i pc v f = 4558 case Redblackmap.peek (lmap,v) 4559 of SOME target => 4560 let open Arbint 4561 in f (intSyntax.term_of_int (fromNat target - pc)) end 4562 | NONE => raise ERR "link_instruction" 4563 ("failed to find label " ^ v ^ " on line " ^ Int.toString i) 4564 fun offset_to_int i offset = 4565 sint_of_term offset handle Overflow => raise ERR "link_instruction" 4566 ("offset caused overflow on line " ^ Int.toString i) 4567 fun ilink_instruction i pc v f = 4568 link_instruction i pc v (f o offset_to_int i) 4569 fun recurse [] code = code 4570 | recurse ((x,Ascii1 s)::t) code = recurse t ((x,Ascii s)::code) 4571 | recurse ((x,Byte1 l)::t) code = recurse t ((x,Byte l)::code) 4572 | recurse ((x,Short1 l)::t) code = recurse t ((x,Short l)::code) 4573 | recurse ((x,Word1 l)::t) code = recurse t ((x,Word l)::code) 4574 | recurse ((x,Instruction1 (i,enc,cond,tm))::t) code = 4575 if null (free_vars tm) then 4576 recurse t ((x,Instruction (enc,cond,tm))::code) 4577 else 4578 let val tm' = 4579 if is_Branch_Target tm then 4580 let val v = vname (dest_Branch_Target tm) in 4581 ilink_instruction i (enc_pc x enc) v 4582 (fn offset => 4583 let val narrow_okay = 4584 aligned (offset,2) andalso 4585 if is_var cond orelse is_AL cond then 4586 in_range (~2048,2046) offset 4587 else 4588 in_range (~256,254) offset 4589 val wide_okay = 4590 aligned (offset,2) andalso 4591 if is_var cond orelse is_AL cond then 4592 in_range (~16777216,16777214) offset 4593 else 4594 in_range (~1048576,1048574) offset 4595 val arm_okay = 4596 aligned (offset,4) andalso 4597 in_range (~33554432,33554428) offset 4598 val imm24 = offset_to_imm24 (offset div 4599 (if enc ~~ Encoding_ARM_tm 4600 then 4 else 2)) 4601 in 4602 if enc ~~ Encoding_Thumb_tm andalso narrow_okay 4603 orelse 4604 enc ~~ Encoding_Thumb2_tm andalso wide_okay 4605 orelse 4606 enc ~~ Encoding_ARM_tm andalso arm_okay 4607 then 4608 mk_Branch_Target imm24 4609 else 4610 raise ERR "link_lines" ("branch target " ^ v ^ 4611 " unaligned or beyond permitted range on\ 4612 \ line " ^ Int.toString i) 4613 end) 4614 end 4615 else if is_Branch_Link_Exchange_Immediate tm then 4616 let val (h,toARM,imm24) = 4617 dest_Branch_Link_Exchange_Immediate tm 4618 val v = vname imm24 4619 in 4620 ilink_instruction i 4621 ((if is_T toARM then align_pc else enc_pc) x enc) v 4622 (fn offset => 4623 let val wide_okay = 4624 if is_T toARM then 4625 aligned (offset,4) andalso 4626 in_range (~16777216,16777212) offset 4627 else 4628 aligned (offset,2) andalso 4629 in_range (~16777216,16777214) offset 4630 val arm_okay = 4631 if is_T toARM then 4632 aligned (offset,4) andalso 4633 in_range (~33554432,33554428) offset 4634 else 4635 aligned (offset,2) andalso 4636 in_range (~33554432,33554430) offset 4637 val h' = mk_bool ((offset div 2) mod 2 = 1) 4638 val imm24 = offset_to_imm24 (offset div 4) 4639 in 4640 if (is_arb h orelse is_F h') andalso 4641 (enc ~~ Encoding_Thumb2_tm andalso wide_okay 4642 orelse 4643 enc ~~ Encoding_ARM_tm andalso arm_okay) 4644 then 4645 mk_Branch_Link_Exchange_Immediate 4646 (h',toARM,imm24) 4647 else 4648 raise ERR "link_lines" ("branch target " ^ v ^ 4649 " unaligned or beyond permitted range\ 4650 \ on line " ^ Int.toString i) 4651 end) 4652 end 4653 else if is_Compare_Branch tm then 4654 let val (nonzero,imm6,n) = dest_Compare_Branch tm 4655 val v = vname imm6 4656 in 4657 ilink_instruction i (enc_pc x enc) v 4658 (fn offset => 4659 if enc ~~ Encoding_Thumb_tm andalso 4660 aligned (offset,2) andalso 4661 in_range (0,126) offset 4662 then 4663 mk_Compare_Branch (nonzero, 4664 wordsSyntax.mk_wordii (offset div 2,6),n) 4665 else 4666 raise ERR "link_lines" ("branch target " ^ v ^ 4667 " unaligned or beyond permitted range on\ 4668 \ line " ^ Int.toString i)) 4669 end 4670 else if is_Add_Sub tm then 4671 let val (a,n,d,imm12) = dest_Add_Sub tm 4672 val v = vname imm12 4673 in 4674 link_instruction i (align_pc x enc) v 4675 (fn tm => 4676 if enc ~~ Encoding_ARM_tm then 4677 case total (mode1_immediate2 false ADD) tm 4678 of SOME (opc,imm12) => 4679 mk_Add_Sub 4680 (mk_bool (opc ~~ dp_opcode ADD),n,d,imm12) 4681 | NONE => 4682 raise ERR "link_lines" ("cannot represent\ 4683 \ offset to label " ^ v ^ " as a mode1\ 4684 \ immmediate on line " ^ Int.toString i) 4685 else 4686 let val offset = offset_to_int i tm 4687 val narrow_okay = 4688 aligned (offset,4) andalso 4689 in_range (0,1020) offset 4690 val wide_okay = 4691 in_range (~4095,4095) offset 4692 val imm12 = mk_word12 (Int.abs offset) 4693 in 4694 if enc ~~ Encoding_Thumb_tm andalso narrow_okay 4695 orelse 4696 enc ~~ Encoding_Thumb2_tm andalso wide_okay 4697 then 4698 mk_Add_Sub (mk_bool (0 <= offset),n,d,imm12) 4699 else 4700 raise ERR "link_lines" 4701 ("address target " ^ v ^ 4702 " unaligned or beyond permitted range on\ 4703 \ line " ^ Int.toString i) 4704 end) 4705 end 4706 else if is_Preload_Data tm then 4707 let val (a,w,n,mode2) = dest_Preload_Data tm 4708 val v = vname mode2 4709 in 4710 ilink_instruction i (align_pc x enc) v 4711 (fn offset => 4712 if in_range (~4095,4095) offset andalso 4713 (enc ~~ Encoding_Thumb2_tm orelse 4714 enc ~~ Encoding_ARM_tm) 4715 then 4716 mk_Preload_Data (mk_bool (0 <= offset),w,n, 4717 mk_Mode2_immediate (mk_word12 (Int.abs offset))) 4718 else 4719 raise ERR "link_lines" ("load target " ^ v ^ 4720 " unaligned or beyond permitted range\ 4721 \ on line " ^ Int.toString i)) 4722 end 4723 else if is_Preload_Instruction tm then 4724 let val (a,n,mode2) = dest_Preload_Instruction tm 4725 val v = vname mode2 4726 in 4727 ilink_instruction i (align_pc x enc) v 4728 (fn offset => 4729 if in_range (~4095,4095) offset andalso 4730 (enc ~~ Encoding_Thumb2_tm orelse 4731 enc ~~ Encoding_ARM_tm) 4732 then 4733 mk_Preload_Instruction (mk_bool (0 <= offset),n, 4734 mk_Mode2_immediate (mk_word12 (Int.abs offset))) 4735 else 4736 raise ERR "link_lines" ("load target " ^ v ^ 4737 " unaligned or beyond permitted range\ 4738 \ on line " ^ Int.toString i)) 4739 end 4740 else if is_Load tm then 4741 let val (indx,a,b,w,u,n,t,mode2) = dest_Load tm 4742 val v = vname mode2 4743 in 4744 ilink_instruction i (align_pc x enc) v 4745 (fn offset => 4746 let val narrow_okay = 4747 aligned (offset,4) andalso 4748 in_range (0,1020) offset 4749 val wide_okay = 4750 in_range (~4095,4095) offset 4751 val mode2 = mk_Mode2_immediate 4752 (mk_word12 (Int.abs offset)) 4753 in 4754 if enc ~~ Encoding_Thumb_tm andalso narrow_okay 4755 orelse (enc ~~ Encoding_Thumb2_tm orelse 4756 enc ~~ Encoding_ARM_tm) andalso wide_okay 4757 then 4758 mk_Load (indx,mk_bool (0 <= offset),b,w,u,n,t, 4759 mode2) 4760 else 4761 raise ERR "link_lines" ("load target " ^ v ^ 4762 " unaligned or beyond permitted range on\ 4763 \ line " ^ Int.toString i) 4764 end) 4765 end 4766 else if is_Load_Halfword tm then 4767 let val (indx,a,w,s,h,u,n,t,mode3) = dest_Load_Halfword tm 4768 val v = vname mode3 4769 in 4770 ilink_instruction i (align_pc x enc) v 4771 (fn offset => 4772 let val wide_okay = 4773 in_range (~4095,4095) offset 4774 val arm_okay = 4775 in_range (~255,255) offset 4776 val mode3 = mk_Mode3_immediate 4777 (mk_word12 (Int.abs offset)) 4778 in 4779 if enc ~~ Encoding_Thumb2_tm andalso wide_okay 4780 orelse 4781 enc ~~ Encoding_ARM_tm andalso arm_okay 4782 then 4783 mk_Load_Halfword (indx,mk_bool (0 <= offset),w, 4784 s,h,u,n,t,mode3) 4785 else 4786 raise ERR "link_lines" ("load target " ^ v ^ 4787 " beyond permitted range on line " ^ 4788 Int.toString i) 4789 end) 4790 end 4791 else if is_Load_Dual tm then 4792 let val (indx,a,w,n,t,t2,mode3) = dest_Load_Dual tm 4793 val v = vname mode3 4794 in 4795 ilink_instruction i (align_pc x enc) v 4796 (fn offset => 4797 let val wide_okay = 4798 in_range (~1020,1020) offset 4799 val arm_okay = 4800 in_range (~255,255) offset 4801 val mode3 = mk_Mode3_immediate 4802 (mk_word12 (Int.abs offset)) 4803 in 4804 if enc ~~ Encoding_Thumb2_tm andalso wide_okay 4805 orelse 4806 enc ~~ Encoding_ARM_tm andalso arm_okay 4807 then 4808 mk_Load_Dual (indx,mk_bool (0 <= offset),w, 4809 n,t,t2,mode3) 4810 else 4811 raise ERR "link_lines" ("load target " ^ v ^ 4812 " beyond permitted range on line " ^ 4813 Int.toString i) 4814 end) 4815 end 4816 else raise ERR "recurse" 4817 ("unexpected free variable on line " ^ Int.toString i) 4818 in 4819 recurse t ((x,Instruction (enc,cond,tm'))::code) 4820 end 4821 | recurse (_::t) code = recurse t code 4822 in 4823 recurse l1 [] 4824 end 4825in 4826 fun link_code c = let 4827 val x as (code,lmap) = 4828 number_lines c (Arbnum.zero,[],Redblackmap.mkDict String.compare) 4829 in 4830 (link_lines x, lmap) 4831 end 4832end; 4833 4834fun arm_parse_from_string s = 4835 s |> arm_parse (arm_parse_lines []) |> link_code; 4836 4837fun arm_parse_from_quote s = 4838 s |> arm_parse_quote (arm_parse_lines []) |> link_code; 4839 4840fun arm_parse_from_file s = 4841let val instream = TextIO.openIn s 4842 val input = TextIO.inputAll instream before TextIO.closeIn instream 4843in 4844 arm_parse_from_string input 4845end; 4846 4847(* for testing *) 4848fun arm_lex_from_file s = 4849let val instream = TextIO.openIn s 4850 val input = TextIO.inputAll instream before TextIO.closeIn instream 4851in 4852 arm_lex input 4853end; 4854 4855(* ------------------------------------------------------------------------- *) 4856 4857end 4858