1structure armLib :> armLib =
2struct
3
4(* interactive use:
5  app load ["arm_disassemblerLib", "arm_stepLib"];
6*)
7
8open HolKernel boolLib bossLib;
9open armSyntax arm_astSyntax;
10open arm_parserLib arm_encoderLib arm_disassemblerLib arm_stepLib;
11
12(* ------------------------------------------------------------------------- *)
13
14val _ = numLib.prefer_num();
15val _ = wordsLib.prefer_word();
16
17val ERR = Feedback.mk_HOL_ERR "armLib";
18
19val trace_progress = ref 1;
20val label_step_theorems = ref true;
21val disassemble = ref true;
22
23val _ = Feedback.register_trace  ("arm steps", trace_progress, 3);
24val _ = Feedback.register_btrace ("label arm steps", label_step_theorems);
25val _ = Feedback.register_btrace ("add disassembler comments", disassemble);
26
27(* ------------------------------------------------------------------------- *)
28
29val eval = boolSyntax.rhs o Thm.concl o bossLib.EVAL;
30
31local
32  fun mk_word4 i = wordsSyntax.mk_wordii (i,4)
33
34  val is_AL = Term.term_eq (mk_word4 14)
35  val is_PC = Term.term_eq (mk_word4 15)
36
37  infix **
38
39  fun opt1 ** opt2 = if opt2 = "" then opt1 else opt1 ^ "," ^ opt2
40
41  val dest_itstate = eval o wordsSyntax.mk_word_concat o dest_If_Then
42
43  val ITAdvance = eval o armSyntax.mk_ITAdvance
44
45  val w2s =
46    Arbnum.toString o numSyntax.dest_numeral o fst o wordsSyntax.dest_n2w
47
48  fun condition_to_word4 tm =
49    mk_word4
50      (case fst (Term.dest_var tm)
51       of "eq" => 0
52        | "ne" => 1
53        | "cs" => 2
54        | "hs" => 2
55        | "cc" => 3
56        | "lo" => 3
57        | "mi" => 4
58        | "pl" => 5
59        | "vs" => 6
60        | "vc" => 7
61        | "hi" => 8
62        | "ls" => 9
63        | "ge" => 10
64        | "lt" => 11
65        | "gt" => 12
66        | "le" => 13
67        | "al" => 14
68        | s    => raise ERR "condition_to_word4" (s ^ " is not a condition"));
69
70  fun fix_condition tm = if is_var tm then condition_to_word4 tm else tm
71
72  fun encoding tm =
73        case fst (Term.dest_const tm)
74        of "Encoding_ARM"     => "; ARM"
75         | "Encoding_Thumb"   => "; 16-bit Thumb"
76         | "Encoding_Thumb2"  => "; 32-bit Thumb"
77         | "Encoding_ThumbEE" => "; 16-bit ThumbEE"
78         | _ => raise ERR "encoding" "unexpected encoding"
79
80  val spaces = String.concat o Lib.separate " "
81
82  fun print_progress x c opt opc =
83        case x
84        of NONE => arm_step opt opc
85         | SOME ((m,a),e) =>
86             let val label = spaces (List.filter (fn s => s <> "") [m,a,e,c])
87                 val _ = if !trace_progress mod 2 = 1 then
88                           print (spaces ["step:", label, "...\n"])
89                         else
90                           ()
91                 val thm = if (!trace_progress div 2) mod 2 = 1 then
92                             Lib.real_time (arm_step opt) opc
93                           else
94                             arm_step opt opc
95             in
96               if !label_step_theorems then
97                 markerLib.MK_LABEL(label,thm)
98               else
99                 thm
100             end
101in
102  fun arm_steps_from_parse s l =
103  let fun arm_step_from_code (itstate,instr as Instruction (enc,cond,tm)) =
104            let val opc = arm_encoderLib.arm_encode instr
105                val pp = print_progress
106                           (if !trace_progress mod 2 = 1 orelse
107                               !label_step_theorems
108                            then
109                              SOME (arm_disassemble instr,encoding enc)
110                            else
111                              NONE)
112            in
113              SOME
114                (if enc = Encoding_ARM_tm then
115                   if is_AL cond orelse is_PC cond then
116                     (itstate, pp "" ("arm,pass" ** s) opc, NONE)
117                   else
118                     (itstate,
119                      pp "(pass condition)" ("arm,pass" ** s) opc,
120                      SOME (pp "(fail condition)" ("arm,fail" ** s) opc))
121                 else
122                   let val itstate' = if is_If_Then tm then
123                                        dest_itstate tm
124                                      else
125                                        ITAdvance itstate
126                       val its = "it:" ^ w2s itstate
127                       val cond' = fix_condition cond
128                       val x = if enc = Encoding_ThumbEE_tm then
129                                 "thumbee"
130                               else
131                                 "thumb"
132                   in
133                     if is_AL cond' orelse is_PC cond' then
134                       (itstate', pp "" (x ** "pass" ** its ** s) opc,
135                        NONE)
136                     else
137                       (itstate',
138                        pp "(pass condition)" ("thumb,pass" ** its ** s) opc,
139                        SOME (pp "(fail condition)"
140                                 (x ** "fail" ** its ** s) opc))
141                   end)
142            end
143        | arm_step_from_code _ = NONE
144      fun recurse [] _ a = List.rev a
145        | recurse (h::t) itstate a =
146            case arm_step_from_code (itstate,h)
147            of SOME (itstate',pass,fail) =>
148                 recurse t itstate' ((pass,fail)::a)
149             | NONE =>
150                 recurse t itstate a
151  in
152    recurse l (wordsSyntax.mk_wordii(0,8)) []
153  end
154end;
155
156fun arm_steps_from f opt qs =
157  arm_steps_from_parse opt (Lib.mk_set (List.map snd (fst (f qs))));
158
159val arm_steps_from_string = arm_steps_from arm_parse_from_string;
160val arm_steps_from_file   = arm_steps_from arm_parse_from_file;
161val arm_steps_from_quote  = arm_steps_from arm_parse_from_quote;
162
163fun bits32 (n,h,l) =
164let val s = StringCvt.padLeft #"0" 32 (Arbnum.toBinString n)
165    val ss = Substring.slice (Substring.full s, 31 - h, SOME (h + 1 - l))
166in
167  Arbnum.fromBinString (Substring.string ss)
168end;
169
170fun decode_opcode opt opc =
171  case opt
172  of SOME (itstate, ee) =>
173      let val n = wordsSyntax.mk_wordi (bits32 (opc,15,0),16)
174          val IT = wordsSyntax.mk_wordii (itstate,8)
175      in
176        if bits32 (opc,31,29) = Arbnum.fromBinString "111" andalso
177           bits32 (opc,28,27) <> Arbnum.zero
178        then
179          pairSyntax.mk_pair (Encoding_Thumb2_tm,
180            mk_thumb2_decode (``arm_coretypes$ARMv7_A``,IT,
181              wordsSyntax.mk_wordi (bits32 (opc,31,16),16),n))
182        else if ee then
183          mk_thumbee_decode (``arm_coretypes$ARMv7_A``,IT,n)
184        else
185          pairSyntax.mk_pair (Encoding_Thumb_tm,
186            mk_thumb_decode (``arm_coretypes$ARMv7_A``,IT,n))
187      end
188   | NONE =>
189       pairSyntax.mk_pair (Encoding_ARM_tm,
190         mk_arm_decode (boolSyntax.F, wordsSyntax.mk_wordi (opc,32)));
191
192fun decode_from_string opt s =
193let val tm = decode_opcode opt (Arbnum.fromHexString s) in
194  Instruction
195    (case tm |> eval |> pairSyntax.strip_pair
196       of [enc,cond,tm] => (enc,cond,tm)
197        | _ => raise ERR "decode_from_string" "failed to evaluate decoding")
198end handle Option =>
199  raise ERR "decode_from_string" "could not parse HEX string";
200
201val arm_decode       = decode_from_string NONE;
202fun thumb_decode i   = decode_from_string (SOME (i,false));
203fun thumbee_decode i = decode_from_string (SOME (i,true));
204
205(* ------------------------------------------------------------------------- *)
206
207fun output_code ostrm line (c as Instruction _) =
208      let val i = arm_encoderLib.arm_encode c
209          val pad = StringCvt.padRight #" "
210          val comment = if !disassemble then
211                          let val (m,a) = arm_disassemble c in
212                            String.concat ["\t\t; ", pad 8 m, a]
213                          end
214                        else
215                          ""
216      in
217        TextIO.output (ostrm, String.concat [line, " ", pad 8 i, comment, "\n"])
218      end
219  | output_code ostrm line c =
220      TextIO.output(ostrm,
221        String.concat [line, " ", arm_encoderLib.arm_encode c, "\n"]);
222
223fun output_arm_assemble_parse ostrm s =
224let open Arbnum
225    val start = fromHexString s
226                  handle Option =>
227                    raise ERR "output_arm_assemble_parse" "expecting Hex string"
228    val lower = String.map Char.toLower
229    val pad   = StringCvt.padLeft #" "
230    val pad0  = StringCvt.padLeft #"0"
231    val count = pad 8 o pad0 4 o lower o toHexString
232in
233  List.app (fn (n,i) => output_code ostrm (count (start + n)) i)
234end;
235
236fun arm_assemble_to_file_parse start filename c =
237let val ostrm = TextIO.openOut filename in
238  output_arm_assemble_parse ostrm start c before TextIO.closeOut ostrm
239end;
240
241fun print_arm_assemble_from_quote s =
242  output_arm_assemble_parse TextIO.stdOut s o fst o arm_parse_from_quote;
243
244fun print_arm_assemble_from_string s =
245  output_arm_assemble_parse TextIO.stdOut s o fst o arm_parse_from_string;
246
247fun print_arm_assemble_from_file s =
248  output_arm_assemble_parse TextIO.stdOut s o fst o arm_parse_from_file;
249
250fun arm_assemble_to_file_from_quote s f =
251  arm_assemble_to_file_parse s f o fst o arm_parse_from_quote;
252
253fun arm_assemble_to_file_from_string s f =
254  arm_assemble_to_file_parse s f o fst o arm_parse_from_string;
255
256fun arm_assemble_to_file_from_file s f =
257  arm_assemble_to_file_parse s f o fst o arm_parse_from_file;
258
259fun join s (a,b) =
260   if a = "WORD" orelse a = "SHORT"
261      then "UDF; (" ^ s ^ ")"
262   else case b of "" => a | _ => String.concat [a, " ", b];
263
264fun arm_disassemble_decode s     = join s (arm_disassemble (arm_decode s))
265fun thumb_disassemble_decode i s = join s (arm_disassemble (thumb_decode i s))
266
267fun thumbee_disassemble_decode i s =
268   join s (arm_disassemble (thumbee_decode i s))
269
270end
271