1(* ------------------------------------------------------------------------- 2 Assembly code support for the ARMv6-M architecture specification 3 ------------------------------------------------------------------------- *) 4 5structure m0AssemblerLib :> m0AssemblerLib = 6struct 7 8open HolKernel boolLib bossLib 9 10local 11 open m0 12in end 13 14val ERR = Feedback.mk_HOL_ERR "m0AssemblerLib" 15 16val hex = assemblerLib.hex 17fun hex32 w = hex (BitsN.bits (31, 16) w) ^ " " ^ hex (BitsN.bits (15, 0) w) 18val w16 = assemblerLib.word 16 19 20fun isBranchLink (m0.Branch (m0.BranchLinkImmediate _)) = true 21 | isBranchLink _ = false 22 23fun m0_syntax_pass1 q = 24 let 25 open m0 26 val pc = ref 0 27 val line = ref 0 28 val errors = ref ([]: assemblerLib.lines) 29 fun addError e = errors := {line = !line, string = e} :: !errors 30 val labelDict = 31 ref (Redblackmap.mkDict String.compare : (string, int) Redblackmap.dict) 32 fun addLabel s = 33 case p_label (L3.lowercase s) of 34 SOME l => 35 labelDict := Redblackmap.update 36 (!labelDict, l, 37 fn NONE => !pc 38 | SOME otherpc => 39 ( addError ("Duplicate label: " ^ l) 40 ; otherpc )) 41 | NONE => addError ("Bad label: " ^ stripSpaces s) 42 fun encoding e = 43 case e of 44 "w" => Enc_Wide 45 | "n" => Enc_Narrow 46 | "" => Enc_Thumb 47 | x => (addError ( "Instruction has ." ^ x ^ " suffix"); Enc_Thumb) 48 fun incpc e = 49 (Portable.inc pc; if e = Enc_Wide then Portable.inc pc else ()) 50 fun pend e l = (incpc e; mlibUseful.INL (!line, l)) 51 fun ok e r = (incpc e; mlibUseful.INR r) 52 fun wide e = 53 ( if e = Enc_Narrow 54 then addError "narrow branch link not available" 55 else () 56 ; Enc_Wide 57 ) 58 fun narrow e = 59 ( if e = Enc_Wide 60 then addError "wide version not available" 61 else () 62 ; Enc_Narrow 63 ) 64 val l = 65 List.foldl 66 (fn (s, p1) => 67 let 68 val () = Portable.inc line 69 val (s1, _) = L3.splitl (fn c => c <> #";", s) 70 val (l1, s1) = L3.splitr (fn c => c <> #":", s1) 71 val () = if l1 = "" then () 72 else addLabel (assemblerLib.dropLastChar l1) 73 val s1 = stripSpaces s1 74 in 75 if s1 = "" 76 then p1 77 else case instructionFromString s1 of 78 OK ((c, e), ast) => 79 ((case Encode (c, (ast, encoding e)) of 80 Thumb16 w => ok Enc_Narrow w :: p1 81 | Thumb32 (w1, w2) => 82 ok Enc_Wide (BitsN.@@ (w1, w2)) :: p1 83 | BadCode err => (addError err; p1)) 84 handle UNPREDICTABLE _ => 85 (addError "UNPREDICTABLE"; p1)) 86 | PENDING (s, ((c, e), ast)) => 87 let 88 val enc0 = encoding e 89 val enc = if isBranchLink ast 90 then wide enc0 91 else narrow enc0 92 in 93 pend enc (s, c, enc, ast) :: p1 94 end 95 | HALFWORD w => ok Enc_Narrow w :: p1 96 | FAIL err => (addError err; p1) 97 end) [] (assemblerLib.quote_to_strings q) 98 in 99 if List.null (!errors) 100 then (List.rev l, !labelDict) 101 else raise assemblerLib.Assembler (List.rev (!errors)) 102 end 103 104fun encode (line, pc, c, enc, ast) = 105 let 106 fun err s = raise assemblerLib.Assembler 107 [{string = "Encode failed" ^ s, line = line}] 108 in 109 (case m0.Encode (c, (ast, enc)) of 110 m0.Thumb16 w => (Portable.inc pc; hex w) 111 | m0.Thumb32 (w1, w2) => 112 (Portable.inc pc; Portable.inc pc; hex w1 ^ " " ^ hex w2) 113 | m0.BadCode e => err e) 114 handle m0.UNPREDICTABLE _ => err ": UNPREDICTABLE." 115 end 116 117fun offErr (label, line) = 118 raise assemblerLib.Assembler 119 [{string = "bad reference to: " ^ label, line = line}] 120 121fun m0_syntax_pass2 (l, ldict) = 122 let 123 open m0 124 val err = ERR "m0_syntax_pass2" "unexpected AST" 125 val r15 = BitsN.fromNat (15, 4) 126 fun check (add, label, line) x ast = 127 if x = r15 128 then if add then ast else offErr (label, line) 129 else raise err 130 val pc = ref 0 131 in 132 List.map 133 (fn mlibUseful.INL (line, (label, cond, enc, ast)) => 134 (case Redblackmap.peek (ldict, label) of 135 SOME lpc => 136 let 137 val offset = BitsN.fromNativeInt (2 * (lpc - !pc - 2), 32) 138 val chk = check (!pc + 1 <= lpc, label, line) 139 in 140 encode (line, pc, cond, enc, 141 case ast of 142 Branch (BranchLinkImmediate _) => 143 Branch (BranchLinkImmediate (offset)) 144 | Branch (BranchTarget (_)) => 145 Branch (BranchTarget offset) 146 | Data (ArithLogicImmediate (_, (false, (d, (x, _))))) => 147 chk x 148 (Data (ArithLogicImmediate 149 (BitsN.fromInt (4, 4), 150 (false, (d, (x, offset)))))) 151 | Load (LoadLiteral (t, _)) => 152 chk r15 (Load (LoadLiteral (t, offset))) 153 | Load (LoadByte (u, (t, (x, _)))) => 154 chk x 155 (Load (LoadByte 156 (u, (t, (x, immediate_form offset))))) 157 | Load (LoadHalf (u, (t, (x, _)))) => 158 chk x 159 (Load (LoadHalf 160 (u, (t, (x, immediate_form offset))))) 161 | Store (StoreWord (t, (x, immediate_form _))) => 162 chk x 163 (Store (StoreWord (t, (x, immediate_form offset)))) 164 | Store (StoreByte (t, (x, immediate_form offset))) => 165 chk x 166 (Store (StoreByte (t, (x, immediate_form offset)))) 167 | Store (StoreHalf (t, (x, immediate_form _))) => 168 chk x 169 (Store (StoreHalf (t, (x, immediate_form offset)))) 170 | _ => raise err) 171 end 172 | NONE => 173 raise assemblerLib.Assembler 174 [{string = "Missing label: " ^ label, line = line}]) 175 | mlibUseful.INR w => 176 ( Portable.inc pc 177 ; if BitsN.size w = 32 178 then (Portable.inc pc; hex32 w) 179 else hex w 180 )) l 181 end 182 183fun m0_code q = m0_syntax_pass2 (m0_syntax_pass1 q) 184 185local 186 val al = BitsN.fromNat (14, 4) 187 val mask = BitsN.fromNat (0xD000, 16) 188 fun canEncodeAsThumb ast = (* should just pick up UDF.W *) 189 (case m0.Encode (al, (ast, m0.Enc_Narrow)) of 190 m0.Thumb16 _ => true 191 | _ => false) handle m0.UNPREDICTABLE _ => true 192 fun pad16 s = StringCvt.padLeft #"0" 4 (L3.lowercase s) 193in 194 fun thumbCondition opc = 195 if BitsN.toNat (BitsN.bits (15, 12) opc) = 13 196 then let 197 val code = BitsN.bits (11, 8) opc 198 in 199 m0.SetPassCondition code 200 ; code 201 end 202 else al 203 fun decode s = 204 case String.tokens Char.isSpace s of 205 [w] => let 206 val opc = w16 w 207 val c = thumbCondition opc (* has side-effect *) 208 val ast = m0.Decode (m0.Thumb opc) 209 val (m, a) = m0.instructionToString (c, ast) 210 in 211 (" " ^ pad16 w, m, a) 212 end 213 | [w1, w2] => 214 let 215 val opc = (w16 w1, w16 w2) 216 val ast = m0.Decode (m0.Thumb2 opc) 217 val w = if canEncodeAsThumb ast then ".w" else "" 218 val (m, a) = m0.instructionToString (al, ast) 219 in 220 (pad16 w1 ^ " " ^ pad16 w2, m ^ w, a) 221 end 222 | _ => raise ERR "decode" "bad string" 223end 224 225fun commentCode (mm, ma) = 226 fn (c, m, a) => 227 c ^ " (* " ^ StringCvt.padRight #" " mm m ^ 228 StringCvt.padRight #" " ma a ^ "*)" 229 230fun commentHex (mm, ma) = 231 fn (c, m, a) => 232 StringCvt.padRight #" " mm m ^ 233 StringCvt.padRight #" " ma a ^ "; " ^ c 234 235fun codeStrings f l = 236 let 237 val mm = ref 0 238 val ma = ref 0 239 fun iter acc = 240 fn [] => List.map (f (!mm + 1, !ma + 2)) acc 241 | s :: r => 242 let 243 val c as (_, m, a) = decode s 244 in 245 mm := Int.max (!mm, String.size m) 246 ; ma := Int.max (!ma, String.size a) 247 ; iter (c :: acc) r 248 end 249 in 250 List.rev (iter [] l): string list 251 end 252 253local 254 open assemblerLib 255in 256 fun print_m0_code q = 257 List.app printn (codeStrings commentCode (m0_code q)) 258 handle Assembler l => 259 ( printn ">> Failed to assemble code." 260 ; printLines l 261 ; printn "<<") 262end 263 264val m0_disassemble = codeStrings commentHex o assemblerLib.quote_to_strings 265 266val print_m0_disassemble = List.app assemblerLib.printn o m0_disassemble 267 268end (* structure m0Parse *) 269 270(* Testing 271 272open m0AssemblerLib 273 274print_m0_code` 275 b -#2 276 b -#0 277 b +#0 278 b +#2 279 b +#4 280 ` 281 282print_m0_code` 283 adr r1, +#4 284 adr r1, +#8 285 adr r1, +#12 286 ` 287 288print_m0_code` 289 ldr r1, +#4 290 ldr r1, +#8 291 ldr r1, +#12 292 ` 293 294print_m0_code 295 ` adr r1, label 296 nop 297 nop 298 nop 299label: nop` 300 301print_m0_code 302 `label: nop 303 b label 304 b label 305 bl label 306 bl label 307 label2: b label2` 308 309print_m0_code 310 `b.n label 311 adr r1, label 312 nop 313 nop 314 nop 315 add.n r1, r2 316 movs r0, r0 317 bl.w label 318 label: muls r2, r3`; 319 320local 321 open assemblerLib 322 val al = BitsN.fromNat (14, 4) 323 fun astEquiv a b = a = b 324 val gen = Random.newgenseed 1.0 325 fun random16 () = BitsN.fromNat (Random.range (0, 0x10000) gen, 16) 326 fun test1 () = 327 let 328 val w = random16 () 329 val c = thumbCondition w 330 val i = m0.DecodeThumb w 331 val (m, a) = m0.instructionToString (c, i) 332 val s = m ^ " " ^ a 333 in 334 if String.isPrefix "nop" m orelse String.isPrefix "udf" m 335 then NONE 336 else 337 case m0.instructionFromString s of 338 m0.OK ((c', ""), i') => 339 (case m0.instructionEncode (c', (i', m0.Enc_Narrow)) of 340 m0.Thumb16 w' => 341 if w = w' orelse c = c' andalso astEquiv i i' 342 then (* (print (s ^ "\n"); NONE) *) NONE 343 else SOME (hex w, i, s, SOME (hex w', i')) 344 | _ => SOME (hex w, i, s, SOME ("???", i'))) 345 | _ => SOME (hex w, i, s, NONE) 346 end 347 handle m0.UNPREDICTABLE _ => NONE 348 fun test2 () = 349 let 350 val opc as (w1, w2) = 351 (BitsN.|| (BitsN.fromNat (0xF000, 16), random16 ()), random16 ()) 352 val i = m0.DecodeThumb2 opc 353 val (m, a) = m0.instructionToString (al, i) 354 val s = m ^ " " ^ a 355 in 356 if String.isPrefix "udf" m orelse m = "isb" andalso a <> "sy" 357 then NONE 358 else 359 case m0.instructionFromString s of 360 m0.OK ((c', _), i') => 361 (case m0.instructionEncode (c', (i', m0.Enc_Wide)) of 362 m0.Thumb32 (opc' as (w1', w2')) => 363 if opc = opc' orelse al = c' andalso astEquiv i i' 364 then (* (print (s ^ "\n"); NONE) *) NONE 365 else SOME (hex w1, hex w2, i, s, 366 SOME (hex w1', hex w2', i')) 367 | _ => SOME (hex w1, hex w2, i, s, 368 SOME ("???", "???", i'))) 369 | _ => SOME (hex w1, hex w2, i, s, NONE) 370 end 371 handle m0.UNPREDICTABLE _ => NONE 372in 373 val examine16 = ref [] 374 val examine32 = ref [] 375 fun test16 n = 376 let 377 val () = examine16 := [] 378 in 379 Lib.funpow n 380 (fn () => 381 case test1 () of 382 SOME x => examine16 := Lib.insert x (!examine16) 383 | NONE => ()) () 384 end 385 fun test32 n = 386 let 387 val () = examine32 := [] 388 in 389 Lib.funpow n 390 (fn () => 391 case test2 () of 392 SOME x => examine32 := Lib.insert x (!examine32) 393 | NONE => ()) () 394 end 395end 396 397(test16 1000000; !examine16) 398(test32 1000000; !examine32) 399 400 401*) 402