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