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