1structure file_readerLib :> file_readerLib =
2struct
3
4open HolKernel boolLib bossLib Parse;
5open helperLib backgroundLib writerLib;
6
7datatype arch = ARM | M0 | RISCV
8
9(* refs begin *)
10
11val arch_name = ref ARM;
12val skip_names = ref ["halt"];
13val missing_sigs = ref ([]:string list);
14val complete_sections = ref ([]:(string * (* sec_name *)
15                                 (int list * int * bool) * (* signature *)
16                                 string * (* location as hex string *)
17                                 (int * string * string) list * (* body *)
18                                 string list) list); (* dependencies *)
19
20(* refs end *)
21
22fun arch_str () =
23  case (!arch_name) of ARM => "ARM" | M0 => "M0" | RISCV => "RISC-V"
24
25fun HOL_commit () = let
26  val path = Globals.HOLDIR
27  val exec = OS.Process.system
28  val filename = "/tmp/hol_commit"
29  val _ = exec ("cd " ^ path ^
30                "; git log --abbrev-commit -n 1 | head -n 1 > " ^ filename)
31  val t = TextIO.openIn(filename)
32  val commit = case TextIO.inputLine(t) of SOME s => s | NONE => fail()
33  val _ = TextIO.closeIn(t)
34  val _ = exec ("/bin/rm -f " ^ filename)
35  val remove_newline =
36    String.translate (fn c => if c = #"\n" then "" else implode [c])
37  in remove_newline commit end handle Interrupt => raise Interrupt
38                     | _ => failwith("Cannot read commit number.")
39
40fun HOL_version () =
41  Globals.release ^ " " ^ int_to_string Globals.version ^
42  " (" ^ Thm.kernelid ^ ") " ^ (HOL_commit () handle HOL_ERR e => #message e)
43
44fun add_missing_sig x = let
45  val _ = print ("No signature info for section: " ^ x ^ "\n")
46  in (missing_sigs := x :: (!missing_sigs)) end;
47
48fun read_sections filename = let
49  val xs = lines_from_file filename
50  fun is_hex_char c = mem c (explode "0123456789abcdefABCDEF")
51  fun is_hex_string str = every is_hex_char (explode str)
52  fun dest_section_declaration line = let
53    val _ = String.substring(line,8,2) = " <" orelse
54            String.substring(line,16,2) = " <" orelse fail()
55    val rest = if String.substring(line,8,2) = " <"
56               then String.substring(line,10,size line - 10)
57               else String.substring(line,18,size line - 18)
58    val sec_name = hd (String.tokens (fn x => x = #">") rest)
59    val hex = if String.substring(line,8,2) = " <"
60              then String.substring(line,0,8)
61              else String.substring(line,0,16)
62    in (hex,sec_name) end handle Empty => fail()
63                               | Subscript => fail()
64  val ys = drop_until (can dest_section_declaration) xs
65  fun split_by_sections [] = []
66    | split_by_sections (y::ys) =
67        if y = "\n" then split_by_sections ys else (let
68          val (location,sec_name) = dest_section_declaration y
69          val body = take_until (fn x => x = "\n" orelse x="\r\n") ys
70          val ys = drop_until (fn x => x = "\n" orelse x="\r\n") ys
71          in (sec_name,location,body) :: split_by_sections ys end
72          handle HOL_ERR _ => split_by_sections ys)
73  in split_by_sections ys end
74
75(* function that cleans names *)
76val remove_dot =
77  String.translate (fn c => if mem c [#".",#" "] then "_" else implode [c])
78
79fun format_line sec_name = let
80  fun find_first i c s = if String.sub(s,i) = c then i else find_first (i+1) c s
81  fun split_at c s =
82    (String.substring(s,0,find_first 0 c s),
83     String.extract(s,find_first 0 c s+1,NONE))
84  fun is_subroutine_call s3 =
85    not (String.isPrefix "addi" s3) andalso
86    not (String.isPrefix "sd" s3) andalso
87    not (String.isPrefix "sw" s3) andalso
88    not (String.isPrefix "lw" s3) andalso
89    not (String.isPrefix "ld" s3) andalso
90    not (String.isPrefix "lbu" s3) andalso
91    ((String.isPrefix "bl" s3 andalso not (String.isPrefix "bls" s3)
92                              andalso not (String.isPrefix "ble" s3)
93                              andalso not (String.isPrefix "blt" s3)) orelse let
94     val ts = String.tokens (fn c => mem c [#"<",#">"]) s3
95     in 1 < length ts andalso not (el 2 ts = sec_name) andalso
96        length (String.tokens (fn x => x = #"+") (el 2 ts)) < 2 end)
97  fun format_line_aux line = let
98    val (s1,s2) = split_at #":" line
99    val s2 = String.extract(s2,1,NONE)
100    val (s2,s3) = split_at #"\t" s2
101    val s3 = String.extract(s3,0,SOME (size s3 - 1))
102    val s1 = if size s1 < 16 then s1 else String.substring(s1,8,size s1 - 8)
103    val i = Arbnum.toInt(Arbnum.fromHexString s1)
104    val s2 = if String.isPrefix ".word" s3 then "const:" ^ s2 else s2
105    val s2 = if String.isPrefix "ldrls\tpc," s3 then "switch:" ^ s2 else s2
106    val s2 = ((if is_subroutine_call s3
107               then "call:" ^ remove_dot
108                 (el 2 (String.tokens (fn x => mem x [#"<",#">"]) s3)) ^ ":" ^ s2
109               else s2)
110              handle HOL_ERR _ => s2)
111    val f = String.translate (fn c => if c = #" " then "" else
112              implode [c])
113    in (i,f s2,s3) end
114    handle Subscript => (fail())
115  in format_line_aux end
116
117fun read_complete_sections filename filename_sigs ignore = let
118  (* helper functions *)
119  fun try_map f [] = []
120    | try_map f (x::xs) = (f x :: try_map f xs) handle HOL_ERR _ => try_map f xs
121  (* read basic section info *)
122  val all_sections = read_sections filename
123  val is_riscv = let
124    val xs = lines_from_file filename
125    in exists (fn s => String.isSubstring "riscv" s) xs end
126  (* read in signature file *)
127  val ss = lines_from_file filename_sigs
128  fun every p [] = true
129    | every p (x::xs) = p x andalso every p xs
130  val is_blank = every (fn c => mem c [#" ",#"\n",#"\t"]) o explode
131  val ss = filter (not o is_blank) ss
132  val bytes_in_word = (if is_riscv then 8 else 4)
133  fun process_sig_line line = let
134    val ts0 = String.tokens (fn x => mem x [#" ",#"\n"]) line
135    val ts = filter (fn s => s <> "struct") ts0
136    val sec_name = el 2 ts
137    val returns_struct = (hd ts0 = "struct")
138    val ret_length = if hd ts = "0" then 0 else
139                     max(string_to_int (hd ts),bytes_in_word) div bytes_in_word
140    val arg_lengths = map string_to_int (tl (tl ts))
141    val arg_lengths = map (fn x => max(x,bytes_in_word) div bytes_in_word) arg_lengths
142    in (sec_name,(arg_lengths,ret_length,returns_struct)) end
143  val ss_alist = map process_sig_line ss
144  (* combine section info with signatures *)
145  val default_sig = ([]:int list,0,false)
146  fun lookup x [] = (add_missing_sig x; default_sig(*fail()*))
147    | lookup x ((y,z)::ys) = if x = y then z else lookup x ys
148  fun combine_ss (sec_name,location,body) =
149    (sec_name,lookup (hd (String.tokens (fn x => x = #".") sec_name)) ss_alist,location,body)
150  val all_sections = try_map combine_ss all_sections
151  (* process section bodies *)
152  fun process_body (sec_name,io,location,body) =
153    (remove_dot sec_name,io,location,
154        if mem sec_name ignore then [] else try_map (format_line sec_name) body)
155  val all_sections = map process_body all_sections
156  (* location function *)
157  fun update x y f a = if x = a then y else f a
158  val find_section = foldl (fn ((sec_name,_,location,_),x) => update location sec_name x) (fn x => fail()) all_sections
159  (* calculate dependencies *)
160  fun get_deps (sec_name,io,location,body) = let
161    val calls = body
162          |> filter (fn (_,s,_) => String.isPrefix "call:" s)
163          |> map (fn (_,s,_) => el 2 (String.tokens (fn x => x = #":") s) handle Subscript => "")
164          |> filter (fn s => length (String.tokens (fn x => x = #"+") s) < 2)
165    val consts = body
166          |> filter (fn (_,s,_) => String.isPrefix "const:" s)
167          |> map (fn (_,s,_) => el 2 (String.tokens (fn x => x = #":") s) handle Subscript => "")
168          |> try_map find_section
169    val deps = all_distinct (calls @ consts)
170    in (sec_name,io,location,body,deps) end
171  val all_sections = map get_deps all_sections
172  (* annotate constants with function names whenever they match *)
173  fun annotate_consts (sec_name,io,location,body,deps) = let
174    fun annotate (x,line,y) = let
175      val _ = String.isPrefix "const:" line orelse fail()
176      val c = el 2 (String.tokens (fn x => x = #":") line)
177      val sec_name = find_section c
178      in (x,line ^ ":" ^ sec_name,y) end handle HOL_ERR _ => (x,line,y)
179   in (sec_name,io,location,map annotate body,deps) end
180  val all_sections = map annotate_consts all_sections
181  fun compare_secs (_,_,_,body1,deps1) (_,_,_,body2,deps2) =
182    if length deps1 < length deps2 then true else
183    if length deps2 < length deps1 then false else
184      (length body1 <= length deps2)
185  (* guess arch *)
186  val arch = let
187    fun has_short_instr (_,_,_,lines,_) =
188      exists (fn (_,hex,_) => size hex < 8) lines
189    in if is_riscv then RISCV else
190       if exists has_short_instr all_sections then M0 else ARM end
191  val _ = (arch_name := arch)
192  in complete_sections := sort compare_secs all_sections end
193
194fun section_info sec_name = let
195  fun f [] = failwith ("Can't find info for section: " ^ sec_name)
196    | f ((name,io,location,body,deps)::xs) =
197        if sec_name = name then (io,(location,(body,deps))) else f xs
198  in f (!complete_sections) end
199
200fun section_names () =
201  map (fn (sec_name,io,location,body,deps) => sec_name) (!complete_sections);
202
203val section_io = fst o section_info
204val section_location = fst o snd o section_info
205val section_body = fst o snd o snd o section_info
206fun section_deps name = (snd o snd o snd o section_info) name handle HOL_ERR _ => []
207fun section_length name = length (section_body name) handle HOL_ERR _ => 0
208
209(*
210  val base_name = "loop-riscv/example"
211  val base_name = "kernel-riscv/kernel-riscv"
212  val ignore = [""]
213*)
214
215fun read_files base_name ignore = let
216  val _ = set_base (base_name ^ "_")
217  fun n_times 0 f x = x | n_times n f x = n_times (n-1) f (f x)
218  val long_line = n_times 70 (fn x => "=" ^ x) "\n"
219  val _ = print long_line
220  val _ = print ("  Base name: "^base_name^"\n")
221  val _ = print ("  Poly/ML: "^(int_to_string (PolyML.rtsVersion()))^"\n")
222  val _ = print ("  HOL: "^(HOL_version ())^"\n")
223  val _ = print long_line
224  (* file names *)
225  fun get_filename suffix = base_name ^ suffix;
226  val filename = get_filename ".elf.txt";
227  val filename_sigs = get_filename ".sigs";
228  (* read sections *)
229  val () = read_complete_sections filename filename_sigs ignore
230  (* print stats *)
231  val f = print
232  val names = section_names ()
233  val lengths = map (fn n => (n, (length o section_body) n)) names
234  val _ = print long_line
235  val names_count = (int_to_string (length names))
236  val inst_count = (int_to_string (sum (map snd lengths)))
237  val _ = f ("  Total: " ^ names_count ^ " functions, " ^ inst_count ^
238             " " ^ arch_str () ^ " instructions\n")
239  fun list_max [] = fail()
240    | list_max [x] = x
241    | list_max ((x,x1)::(y,y1)::xs) =
242        if x1 < y1 then list_max ((y,y1)::xs) else list_max ((x,x1)::xs)
243  val (longest_name,l) = list_max lengths
244  val _ = f ("  Longest function: " ^ longest_name ^ " (" ^(int_to_string l) ^
245             " instructions)\n")
246  val dep_counts = map (length o section_deps) names |> all_distinct
247  fun print_dep_count_line n = let
248    fun max_string_length n [] s = s
249      | max_string_length n (x::xs) s =
250          if size (s ^ ", " ^ x) < n then
251            max_string_length n xs (s ^ ", " ^ x) else s ^ ", ..."
252    val deps = filter (fn s => length (section_deps s) = n) names
253    val s = "  " ^ int_to_string n ^ " deps: " ^ int_to_string (length deps) ^
254            " functions ("
255    in max_string_length 65 (tl deps) (s ^ hd deps) ^ ")\n" end
256  val _ = map (print o print_dep_count_line) dep_counts
257  val _ = print long_line
258  in () end;
259
260val int_to_hex = (fn s => "0x" ^ s) o to_lower o
261                 Arbnum.toHexString o Arbnum.fromInt
262
263fun show_annotated_code ann sec_name = let
264  val code = section_body sec_name
265  val l = hd code |> #1
266  val code = map (fn (x,y,z) => (x,x-l,z)) code
267  val loc_width = last code |> #1 |> int_to_hex |> size
268  val offset_width = (last code |> #2 |> int_to_hex |> size) + 4
269  fun left_pad k s = if size s < k then left_pad k (" " ^ s) else s
270  fun right_pad k s = if size s < k then right_pad k (s ^ " ") else s
271  fun line (loc,offset,asm) = let
272    val s1 = left_pad loc_width (int_to_hex loc)
273    val s2 = left_pad offset_width (int_to_hex offset)
274    val asm = String.tokens (fn c => c = #";") asm |> hd
275              |> String.translate (fn c => if c = #"\r" then "" else
276                                           if c = #"\t" then " " else implode [c])
277    val s3 = right_pad 20 asm ^ "  ; " ^ ann loc handle HOL_ERR _ => asm
278    in s1 ^ s2 ^ "    " ^ s3 ^ "\n" end
279  val _ = write_blank_line ()
280  val _ = write_indented_block (concat (map line code))
281  val _ = write_blank_line ()
282  in () end
283
284val show_code = show_annotated_code (fn x => fail())
285
286(* tools *)
287
288val () = arm_progLib.arm_config "vfpv3" "mapped"
289val arm_tools = arm_decompLib.l3_arm_tools
290val (arm_spec,_,_,_) = arm_tools
291
292val () = m0_progLib.m0_config false (* not bigendian *) "mapped"
293val m0_tools = m0_decompLib.l3_m0_tools
294val (m0_spec,_,_,_) = m0_tools
295
296val () = riscv_progLib.riscv_config true (* set id yo 0 *)
297val riscv_tools = riscv_decompLib.riscv_tools
298val (riscv_spec,_,_,_) = riscv_tools
299
300fun get_tools () =
301  case !arch_name of
302    ARM   => arm_tools
303  | M0    => m0_tools
304  | RISCV => riscv_tools ;
305
306fun tysize () =
307  case !arch_name of
308    ARM   => ``:32``
309  | M0    => ``:32``
310  | RISCV => ``:64`` ;
311
312fun wsize () = ``:^(tysize ()) word``;
313
314end
315