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