1structure arm8AssemblerLib :> arm8AssemblerLib = 2struct 3 4open HolKernel boolLib bossLib 5 6local 7 open arm8 8in end 9 10val ERR = Feedback.mk_HOL_ERR "arm8AssemblerLib" 11 12(* Validity check for EncodeBitMask 13 14local 15 val b0 = BitsN.B (0, 1) 16 val b1 = BitsN.B (1, 1) 17 fun mask (m, n) (s, r) = 18 Option.map fst 19 (arm8.DecodeBitMasks m 20 (BitsN.fromNat (n, 1), 21 (BitsN.fromNat (s, 6), (BitsN.fromNat (r, 6), true)))) 22 fun checkMask (m, n) (s, r) = 23 case mask (m, n) (s, r) of 24 SOME imm => Option.isSome (arm8.EncodeBitMask m imm) 25 | NONE => false 26 val mask32 = checkMask (32, 0) 27 val mask64_0 = checkMask (64, 0) 28 val mask64_1 = checkMask (64, 1) 29 val d64 = 30 (List.tabulate 31 (64, 32 fn i => List.tabulate (64, fn j => (mask64_1 (i, j), (b1, i, j)))) 33 @ 34 List.tabulate 35 (62, 36 fn i => List.tabulate (64, fn j => (mask64_0 (i, j), (b0, i, j))))) 37 |> List.concat 38 val d32 = 39 (List.tabulate 40 (62, fn i => List.tabulate (64, fn j => (mask32 (i, j), (b0, i, j))))) 41 |> List.concat 42in 43 val fail64 = 44 List.filter (not o fst) d64 45 |> List.map (fn (_, (n, s, r)) => mask (64, BitsN.toNat n) (s, r)) 46 |> List.filter Option.isSome 47 val fail32 = 48 List.filter (not o fst) d32 49 |> List.map (fn (_, (n, s, r)) => mask (32, BitsN.toNat n) (s, r)) 50 |> List.filter Option.isSome 51end 52 53*) 54 55fun arm_syntax_pass1 q = 56 let 57 open arm8 58 val pc = ref 0 59 val line = ref 0 60 val errors = ref ([]: assemblerLib.lines) 61 fun addError e = errors := {line = !line, string = e} :: !errors 62 val labelDict = 63 ref (Redblackmap.mkDict String.compare : (string, int) Redblackmap.dict) 64 fun addLabel s = 65 case p_label (L3.lowercase s) of 66 SOME l => 67 labelDict := Redblackmap.update 68 (!labelDict, l, 69 fn NONE => !pc 70 | SOME otherpc => 71 ( addError ("Duplicate label: " ^ l) 72 ; otherpc )) 73 | NONE => addError ("Bad label: " ^ stripSpaces s) 74 fun pend l = (Portable.inc pc; mlibUseful.INL (!line, l)) 75 fun ok r = (Portable.inc pc; mlibUseful.INR r) 76 val l = 77 List.foldl 78 (fn (s, p1) => 79 let 80 val () = Portable.inc line 81 val (s1, _) = L3.splitl (fn c => c <> #";", s) 82 val (l1, s1) = L3.splitr (fn c => c <> #":", s1) 83 val () = if l1 = "" then () 84 else addLabel (assemblerLib.dropLastChar l1) 85 val s1 = stripSpaces s1 86 in 87 if s1 = "" 88 then p1 89 else case instructionFromString s1 of 90 OK ast => 91 (case arm8.Encode ast of 92 ARM8 w => 93 let 94 val ast' = Decode w 95 in 96 if ast' = ast 97 then ok w :: p1 98 else (addError "Encoding error"; p1) 99 end 100 | BadCode err => (addError err; p1)) 101 | PENDING (s, ast) => (pend (s, ast) :: p1) 102 | WORD w => ok w :: p1 103 | FAIL err => (addError err; p1) 104 end) [] (assemblerLib.quote_to_strings q) 105 in 106 if List.null (!errors) 107 then (List.rev l, !labelDict) 108 else raise assemblerLib.Assembler (List.rev (!errors)) 109 end 110 111fun encode (line, ast) = 112 let 113 fun err s = raise assemblerLib.Assembler 114 [{string = "Encode failed" ^ s, line = line}] 115 in 116 case arm8.Encode ast of 117 arm8.ARM8 w => 118 let 119 val ast' = arm8.Decode w 120 in 121 if ast' = ast 122 then BitsN.toHexString w 123 else err "." 124 end 125 | _ => err ": not ARM." 126 end 127 128fun arm_syntax_pass2 (l, ldict) = 129 let 130 open arm8 131 val err = ERR "arm_syntax_pass2" "unexpected AST" 132 val pc = ref 0 133 in 134 List.map 135 (fn mlibUseful.INL (line, (label, ast)) => 136 (case Redblackmap.peek (ldict, label) of 137 SOME lpc => 138 let 139 val offset = BitsN.fromNativeInt (4 * (lpc - !pc), 64) 140 in 141 Portable.inc pc 142 ; encode (line, 143 case ast of 144 LoadStore 145 (LoadLiteral''32 (sz, (memop, (signed, (_, rt))))) => 146 LoadStore 147 (LoadLiteral''32 148 (sz, (memop, (signed, (offset, rt))))) 149 | LoadStore 150 (LoadLiteral''64 (sz, (memop, (signed, (_, rt))))) => 151 LoadStore 152 (LoadLiteral''64 153 (sz, (memop, (signed, (offset, rt))))) 154 | Address (page, (_, xd)) => Address (page, (offset, xd)) 155 | Branch (BranchConditional (_, cd)) => 156 Branch (BranchConditional (offset, cd)) 157 | Branch (BranchImmediate (_, branch_type)) => 158 Branch (BranchImmediate (offset, branch_type)) 159 | Branch 160 (CompareAndBranch''32 (sz, (iszero, (_, rt)))) => 161 Branch 162 (CompareAndBranch''32 (sz, (iszero, (offset, rt)))) 163 | Branch 164 (CompareAndBranch''64 (sz, (iszero, (_, rt)))) => 165 Branch 166 (CompareAndBranch''64 (sz, (iszero, (offset, rt)))) 167 | Branch 168 (TestBitAndBranch''32 169 (sz, (bit_pos, (bit_val, (_, rt))))) => 170 Branch 171 (TestBitAndBranch''32 172 (sz, (bit_pos, (bit_val, (offset, rt))))) 173 | Branch 174 (TestBitAndBranch''64 175 (sz, (bit_pos, (bit_val, (_, rt))))) => 176 Branch 177 (TestBitAndBranch''64 178 (sz, (bit_pos, (bit_val, (offset, rt))))) 179 | _ => raise err) 180 end 181 | NONE => 182 raise assemblerLib.Assembler 183 [{string = "Missing label: " ^ label, line = line}]) 184 | mlibUseful.INR w => (Portable.inc pc; BitsN.toHexString w)) l 185 end 186 187val arm8_code = arm_syntax_pass2 o arm_syntax_pass1 188 189local 190 fun code3 s = 191 let 192 val w = assemblerLib.word 32 s 193 val h = StringCvt.padLeft #"0" 8 (L3.lowercase s) 194 val (m, a) = arm8.instructionToString (arm8.Decode w) 195 val (m, a) = 196 if String.isPrefix "??" m then ("WORD", "0x" ^ h) else (m, a) 197 in 198 (h, m, a) 199 end 200 handle Option => raise ERR "" ("could not decode: " ^ s) 201 fun commentCode (mm, ma) = 202 fn (c, m, a) => 203 c ^ " (* " ^ StringCvt.padRight #" " mm m ^ 204 StringCvt.padRight #" " ma a ^ "*)" 205 fun commentHex (mm, ma) = 206 fn (c, m, a) => 207 StringCvt.padRight #" " mm m ^ 208 StringCvt.padRight #" " ma a ^ "; " ^ c 209 fun codeStrings f l = 210 let 211 val mm = ref 0 212 val ma = ref 0 213 fun iter acc = 214 fn [] => List.map (f (!mm + 1, !ma + 2)) acc 215 | s :: r => 216 let 217 val c as (_, m, a) = code3 s 218 in 219 mm := Int.max (!mm, String.size m) 220 ; ma := Int.max (!ma, String.size a) 221 ; iter (c :: acc) r 222 end 223 in 224 List.rev (iter [] l): string list 225 end 226 open assemblerLib 227in 228 fun print_arm8_code q = 229 List.app printn (codeStrings commentCode (arm8_code q)) 230 handle Assembler l => ( printn ">> Failed to assemble code." 231 ; printLines l 232 ; printn "<<") 233 val arm8_disassemble = 234 codeStrings commentHex o List.concat o 235 List.map (String.tokens Char.isSpace) o assemblerLib.quote_to_strings 236 val print_arm8_disassemble = List.app printn o arm8_disassemble 237end 238 239(* Testing - round-trip 240 241open arm8AssemblerLib 242 243local 244 val hex = assemblerLib.hex 245 fun astEquiv a b = 246 a = b orelse 247 case (a, b) of 248 (arm8.LoadStore (arm8.LoadStoreAcquire''8 249 (size, (memop, (acctype, (excl, (_, (_, (_, r)))))))), 250 arm8.LoadStore (arm8.LoadStoreAcquire''8 251 (size2, (memop2, (acctype2, (excl2, (_, (_, (_, r2))))))))) => 252 size = size2 andalso memop = memop2 andalso 253 acctype = acctype2 andalso excl = excl2 andalso r = r2 254 | (arm8.LoadStore (arm8.LoadStoreAcquire''16 255 (size, (memop, (acctype, (excl, (_, (_, (_, r)))))))), 256 arm8.LoadStore (arm8.LoadStoreAcquire''16 257 (size2, (memop2, (acctype2, (excl2, (_, (_, (_, r2))))))))) => 258 size = size2 andalso memop = memop2 andalso 259 acctype = acctype2 andalso excl = excl2 andalso r = r2 260 | (arm8.LoadStore (arm8.LoadStoreAcquire''32 261 (size, (memop, (acctype, (excl, (_, (_, (_, r)))))))), 262 arm8.LoadStore (arm8.LoadStoreAcquire''32 263 (size2, (memop2, (acctype2, (excl2, (_, (_, (_, r2))))))))) => 264 size = size2 andalso memop = memop2 andalso 265 acctype = acctype2 andalso excl = excl2 andalso r = r2 266 | (arm8.LoadStore (arm8.LoadStoreAcquire''64 267 (size, (memop, (acctype, (excl, (_, (_, (_, r)))))))), 268 arm8.LoadStore (arm8.LoadStoreAcquire''64 269 (size2, (memop2, (acctype2, (excl2, (_, (_, (_, r2))))))))) => 270 size = size2 andalso memop = memop2 andalso 271 acctype = acctype2 andalso excl = excl2 andalso r = r2 272 | (arm8.LoadStore 273 (arm8.LoadStoreAcquirePair''64 274 (size, (memop, (acctype, (_, (_, (rs, r))))))), 275 arm8.LoadStore 276 (arm8.LoadStoreAcquirePair''64 277 (size2, (memop2, (acctype2, (_, (_, (rs2, r2)))))))) => 278 size = size2 andalso memop = memop2 andalso acctype = acctype2 279 andalso r = r2 andalso (memop <> arm8.MemOp_STORE orelse rs = rs2) 280 | (arm8.LoadStore 281 (arm8.LoadStoreAcquirePair''128 282 (size, (memop, (acctype, (_, (_, (rs, r))))))), 283 arm8.LoadStore 284 (arm8.LoadStoreAcquirePair''128 285 (size2, (memop2, (acctype2, (_, (_, (rs2, r2)))))))) => 286 size = size2 andalso memop = memop2 andalso acctype = acctype2 287 andalso r = r2 andalso (memop <> arm8.MemOp_STORE orelse rs = rs2) 288 | _ => false 289 val gen = Random.newgenseed 1.0 290 fun random32 () = BitsN.fromNat (Random.range (0, 0x100000000) gen, 32) 291 fun test1 () = 292 let 293 val w = random32 () 294 val i = arm8.Decode w 295 val (m, a) = arm8.instructionToString i 296 in 297 if String.isPrefix "??" m 298 then NONE 299 else let 300 val s = m ^ " " ^ a 301 in 302 case arm8.instructionFromString s of 303 arm8.OK i' => 304 (case arm8.Encode i' of 305 arm8.ARM8 w' => 306 if w = w' orelse astEquiv i i' 307 then (* (print (s ^ "\n"); NONE) *) NONE 308 else SOME (hex w, i, s, SOME (hex w', i')) 309 | _ => SOME (hex w, i, s, SOME ("???", i'))) 310 | _ => SOME (hex w, i, s, NONE) 311 end 312 end 313in 314 val examine = ref [] 315 fun test n = 316 let 317 val () = examine := [] 318 in 319 Lib.funpow n 320 (fn () => 321 case test1 () of 322 SOME x => examine := Lib.insert x (!examine) 323 | NONE => ()) () 324 end 325end 326 327arm8.instructionFromString "mov w26, w12, lsr #0" 328 329fun bin s = 330 StringCvt.padLeft #"0" 32 331 (BitsN.toBinString (Option.valOf (BitsN.fromHexString (s, 32)))) 332 333bin"b8ef4961" 334bin"b8af4961" 335 336arm8.diss "d3403e6d" 337arm8.diss "53003e6d" 338 339(test 100000; !examine) 340 341*) 342 343end 344