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