1(* ------------------------------------------------------------------------- 2 Assembly code support for the ARMv7-AR architecture specification 3 ------------------------------------------------------------------------- *) 4 5structure armAssemblerLib :> armAssemblerLib = 6struct 7 8open HolKernel boolLib bossLib 9 10local 11 open arm assemblerLib 12in 13end 14 15val ERR = Feedback.mk_HOL_ERR "armAssemblerLib" 16 17fun init () = 18 let 19 open arm 20 in 21 Architecture := ARMv7_A 22 ; Extensions := [Extension_Virtualization] 23 ; VFPExtension := VFPv4 24 ; CPSR := rec'PSR (Option.valOf (BitsN.fromHexString ("10", 32))) 25 end 26 27fun arm_syntax_pass1 q = 28 let 29 open arm 30 val () = init () 31 val pc = ref 0 32 val line = ref 0 33 val errors = ref ([]: assemblerLib.lines) 34 fun addError e = errors := {line = !line, string = e} :: !errors 35 val warnings = ref ([]: assemblerLib.lines) 36 fun addWarning s = warnings := {line = !line, string = s} :: !warnings 37 val labelDict = 38 ref (Redblackmap.mkDict String.compare : (string, int) Redblackmap.dict) 39 fun addLabel s = 40 case p_label (L3.lowercase s) of 41 SOME l => 42 labelDict := Redblackmap.update 43 (!labelDict, l, 44 fn NONE => !pc 45 | SOME otherpc => 46 ( addError ("Duplicate label: " ^ l) 47 ; otherpc )) 48 | NONE => addError ("Bad label: " ^ stripSpaces s) 49 fun pend l = (Portable.inc pc; mlibUseful.INL (!line, l)) 50 fun ok r = (Portable.inc pc; mlibUseful.INR r) 51 val l = 52 List.foldl 53 (fn (s, p1) => 54 let 55 val () = Portable.inc line 56 val (s1, _) = L3.splitl (fn c => c <> #";", s) 57 val (l1, s1) = L3.splitr (fn c => c <> #":", s1) 58 val () = if l1 = "" then () 59 else addLabel (assemblerLib.dropLastChar l1) 60 val s1 = stripSpaces s1 61 in 62 if s1 = "" 63 then p1 64 else case instructionFromString s1 of 65 OK ((c, ""), ast) => 66 (case instructionEncode (c, (ast, Enc_ARM)) of 67 ARM w => 68 (let 69 val () = SetPassCondition c 70 val ast' = DecodeARM w 71 in 72 if ast' = ast 73 then ok w :: p1 74 else (addError "Encoding error"; p1) 75 end 76 handle UNPREDICTABLE _ => 77 ( addWarning s1; ok w :: p1 )) 78 | BadCode err => (addError err; p1) 79 | _ => (addError "Encoding error"; p1)) 80 | OK ((_, x), _) => 81 (addError ("Instruction has ." ^ x ^ " suffix"); p1) 82 | PENDING (s, ((c, ""), ast)) => 83 (pend (s, c, ast) :: p1) 84 | PENDING (_, ((_, x), _)) => 85 (addError ("Instruction has ." ^ x ^ " suffix"); p1) 86 | WORD w => ok w :: p1 87 | FAIL err => (addError err; p1) 88 end) [] (assemblerLib.quote_to_strings q) 89 in 90 if List.null (!errors) 91 then (List.rev l, !labelDict, List.rev (!warnings)) 92 else raise assemblerLib.Assembler 93 (List.rev (!errors) @ 94 List.map (fn {string, line} => 95 {string = "Unpredictable: " ^ string, 96 line = line}) (List.rev (!warnings))) 97 end 98 99fun encode (line, c, ast) = 100 let 101 fun err s = raise assemblerLib.Assembler 102 [{string = "Encode failed" ^ s, line = line}] 103 in 104 case arm.instructionEncode (c, (ast, arm.Enc_ARM)) of 105 arm.ARM w => 106 (let 107 val () = arm.SetPassCondition c 108 val ast' = arm.DecodeARM w 109 in 110 if ast' = ast 111 then BitsN.toHexString w 112 else err "." 113 end 114 handle arm.UNPREDICTABLE _ => err ": UNPREDICTABLE.") 115 | _ => err ": not ARM." 116 end 117 118fun arm_syntax_pass2 ldict l = 119 let 120 open arm 121 val err = ERR "arm_syntax_pass2" "unexpected AST" 122 val r15 = BitsN.fromNat (15, 4) 123 fun check15 x ast = if x = r15 then ast else raise err 124 val pc = ref 0 125 in 126 List.map 127 (fn mlibUseful.INL (line, (label, cond, ast)) => 128 (case Redblackmap.peek (ldict, label) of 129 SOME lpc => 130 let 131 val offset = BitsN.fromNativeInt (4 * (lpc - !pc - 2), 32) 132 val (add, uoffset) = 133 if !pc + 2 <= lpc 134 then (true, offset) 135 else (false, 136 BitsN.fromNativeInt (4 * (!pc + 2 - lpc), 32)) 137 in 138 Portable.inc pc 139 ; encode (line, cond, 140 case ast of 141 Branch 142 (BranchLinkExchangeImmediate (iset, _)) => 143 Branch (BranchLinkExchangeImmediate (iset, offset)) 144 | Branch (BranchTarget (_)) => 145 Branch (BranchTarget offset) 146 | Data (ArithLogicImmediate (_, (false, (d, (x, _))))) => 147 check15 x 148 (case arm.EncodeARMImmediate uoffset of 149 SOME imm12 => 150 Data (ArithLogicImmediate 151 (BitsN.fromInt (if add then 4 else 2, 4), 152 (false, (d, (x, imm12))))) 153 | NONE => 154 raise assemblerLib.Assembler 155 [{string = 156 "Label address not encodable: " ^ label, 157 line = line}]) 158 | Load (LoadLiteral (_, (t, _))) => 159 Load (LoadLiteral (add, (t, uoffset))) 160 | Load (LoadByteLiteral (u, (_, (t, _)))) => 161 Load (LoadByteLiteral (u, (add, (t, uoffset)))) 162 | Load (LoadHalfLiteral (u, (_, (t, _)))) => 163 Load (LoadHalfLiteral (u, (add, (t, uoffset)))) 164 | Load (LoadDualLiteral (_, (t1, (t2, _)))) => 165 Load (LoadDualLiteral (add, (t1, (t2, uoffset)))) 166 | Store 167 (StoreWord 168 (_, 169 (true, 170 (false, (t, (x, immediate_form1 _)))))) => 171 check15 x 172 (Store (StoreWord (add, (true, (false, (t, 173 (x, immediate_form1 uoffset))))))) 174 | Store 175 (StoreByte 176 (_, 177 (true, 178 (false, (t, (x, immediate_form1 _)))))) => 179 check15 x 180 (Store (StoreByte (add, (true, (false, (t, 181 (x, immediate_form1 uoffset))))))) 182 | Store 183 (StoreHalf 184 (_, 185 (true, 186 (false, (t, (x, immediate_form1 _)))))) => 187 check15 x 188 (Store (StoreHalf (add, (true, (false, (t, 189 (x, immediate_form1 uoffset))))))) 190 | Store 191 (StoreDual 192 (_, 193 (true, 194 (false, 195 (t1, (t2, (x, immediate_form2 _))))))) => 196 check15 x 197 (Store (StoreDual (add, (true, (false, (t1, (t2, 198 (x, immediate_form2 uoffset)))))))) 199 | VFP (vldr (s, (_, (d, (x, _))))) => 200 check15 x (VFP (vldr (s, (add, (d, (x, uoffset)))))) 201 | VFP (vstr (s, (_, (d, (x, _))))) => 202 check15 x (VFP (vstr (s, (add, (d, (x, uoffset)))))) 203 | _ => raise err) 204 end 205 | NONE => 206 raise assemblerLib.Assembler 207 [{string = "Missing label: " ^ label, line = line}]) 208 | mlibUseful.INR w => (Portable.inc pc; BitsN.toHexString w)) l 209 end 210 211fun arm_code_with_warnings q = 212 let 213 val (l, ldict, wrns) = arm_syntax_pass1 q 214 in 215 (arm_syntax_pass2 ldict l, wrns) 216 end 217 218fun arm_code q = 219 let 220 val (code, warnings) = arm_code_with_warnings q 221 in 222 if List.null warnings 223 then code 224 else raise assemblerLib.Assembler warnings 225 end 226 227local 228 fun code3 s = 229 let 230 val w = assemblerLib.word 32 s 231 val c = BitsN.bits (31, 28) w 232 val () = (init(); arm.SetPassCondition c) 233 val h = StringCvt.padLeft #"0" 8 (L3.lowercase s) 234 val (m, a) = arm.instructionToString (c, arm.DecodeARM w) 235 handle arm.UNPREDICTABLE _ => ("WORD", h) 236 in 237 (h, m, a) 238 end 239 handle Option => raise ERR "" ("could not decode: " ^ s) 240 fun commentCode (mm, ma) = 241 fn (c, m, a) => 242 c ^ " (* " ^ StringCvt.padRight #" " mm m ^ 243 StringCvt.padRight #" " ma a ^ "*)" 244 fun commentHex (mm, ma) = 245 fn (c, m, a) => 246 StringCvt.padRight #" " mm m ^ 247 StringCvt.padRight #" " ma a ^ "; " ^ c 248 fun codeStrings f l = 249 let 250 val mm = ref 0 251 val ma = ref 0 252 fun iter acc = 253 fn [] => List.map (f (!mm + 1, !ma + 2)) acc 254 | s :: r => 255 let 256 val c as (_, m, a) = code3 s 257 in 258 mm := Int.max (!mm, String.size m) 259 ; ma := Int.max (!ma, String.size a) 260 ; iter (c :: acc) r 261 end 262 in 263 List.rev (iter [] l): string list 264 end 265 open assemblerLib 266in 267 fun print_arm_code q = 268 let 269 val (code, wrns) = arm_code_with_warnings q 270 val code = codeStrings commentCode code 271 in 272 if List.null wrns 273 then () 274 else ( printn ">> Warning: UNPREDICTABLE code." 275 ; printLines wrns 276 ; printn "<<" 277 ) 278 ; List.app printn code 279 end 280 handle Assembler l => ( printn ">> Failed to assemble code." 281 ; printLines l 282 ; printn "<<") 283 val arm_disassemble = 284 codeStrings commentHex o List.concat o 285 List.map (String.tokens Char.isSpace) o assemblerLib.quote_to_strings 286 val print_arm_disassemble = List.app printn o arm_disassemble 287end 288 289end (* structure armParse *) 290 291(* Testing 292 293open armAssemblerLib 294 295val () = print_arm_code 296 `b -#12 297 b -#8 298 b -#4 299 b -#0 300 b +#0 301 b +#4 302 b +#8 303 b +#12 304 ` 305 306val () = print_arm_code 307 `label: 308 adr r1, label2 309 adr r1, -#12 310 adr r1, -#8 311 adr r1, -#4 312 adr r1, -#0 313 adr r1, +#0 314 adr r1, +#4 315 adr r1, +#8 316 adr r1, +#12 317 label2: 318 adr r1, label` 319 320val () = print_arm_code 321 `ldmdbeq r1!, {r3-r6} 322 add r1, r2, r3, lsl r4 323 ` 324 325local 326 val hex = assemblerLib.hex 327 fun immEquiv x y = arm.ExpandImm_C (x, false) = arm.ExpandImm_C (y, false) 328 fun astEquiv a b = 329 a = b orelse 330 case (a, b) of 331 (arm.Data (arm.Move (setflags, (negate, (d, imm12a)))), 332 arm.Data (arm.Move (_, (_, (_, imm12b))))) => 333 b = arm.Data (arm.Move (setflags, (negate, (d, imm12b)))) andalso 334 immEquiv imm12a imm12b 335 | (arm.Data (arm.TestCompareImmediate (opc, (n, imm12a))), 336 arm.Data (arm.TestCompareImmediate (_, (_, imm12b)))) => 337 b = arm.Data (arm.TestCompareImmediate (opc, (n, imm12b))) andalso 338 immEquiv imm12a imm12b 339 | (arm.Data 340 (arm.ArithLogicImmediate (opc, (setflags, (d, (n, imm12a))))), 341 arm.Data (arm.ArithLogicImmediate (_, (_, (_, (_, imm12b)))))) => 342 b = arm.Data 343 (arm.ArithLogicImmediate (opc, (setflags, (d, (n, imm12b))))) 344 andalso immEquiv imm12a imm12b 345 | (arm.Data (arm.RegisterShiftedRegister 346 (opc, (setflags, (d, (n, (m, (shift_t, s))))))), 347 arm.Data (arm.RegisterShiftedRegister 348 (opc', (setflags', (d', (n', (m', (shift_t', s')))))))) => 349 opc = opc' andalso setflags = setflags' andalso 350 (BitsN.bits (3, 2) opc = BitsN.fromNat (2, 2) orelse d = d') 351 andalso n = n' andalso m = m' andalso shift_t = shift_t' andalso 352 s = s' 353 | _ => false 354 val gen = Random.newgenseed 1.0 355 fun random32 () = BitsN.fromNat (Random.range (0, 0x100000000) gen, 32) 356 fun test1 () = 357 let 358 val w = random32 () 359 val c = BitsN.bits (31, 28) w 360 val i = arm.DecodeARM w 361 val (m, a) = arm.instructionToString (c, i) 362 val c = if c = BitsN.fromNat (15, 4) then BitsN.fromNat (14, 4) else c 363 val s = m ^ " " ^ a 364 in 365 if String.isPrefix "nop" m orelse String.isPrefix "udf" m orelse 366 m = "isb" andalso a <> "sy" 367 then NONE 368 else 369 case arm.instructionFromString s of 370 arm.OK ((_, ""), 371 arm.Branch 372 (arm.BranchLinkExchangeImmediate (arm.InstrSet_ARM, _))) => 373 NONE 374 | arm.OK ((c', ""), i') => 375 (case arm.instructionEncode (c', (i', arm.Enc_ARM)) of 376 arm.ARM w' => 377 if w = w' orelse c = c' andalso astEquiv i i' 378 then (* (print (s ^ "\n"); NONE) *) NONE 379 else SOME (hex w, i, s, SOME (hex w', i')) 380 | _ => SOME (hex w, i, s, SOME ("???", i'))) 381 | _ => SOME (hex w, i, s, NONE) 382 end 383 handle arm.UNPREDICTABLE _ => NONE 384in 385 val examine = ref [] 386 fun test n = 387 ( init () 388 ; examine := [] 389 ; Lib.funpow n 390 (fn () => 391 case test1 () of 392 SOME x => examine := Lib.insert x (!examine) 393 | NONE => ()) () 394 ) 395end 396 397(test 100000; !examine) 398 399*) 400