From 96165dbec88ab4c951d99e64e51f5c55a1244137 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 16:28:00 +0200 Subject: fixed a bug in support libraries; reload profiling info --- backend/Profilingaux.ml | 44 ++++++++++++++++++++++++++++++++++----- driver/Clflags.ml | 1 - driver/Driver.ml | 1 + mppa_k1c/TargetPrinter.ml | 2 +- runtime/c/write_profiling_table.c | 2 +- 5 files changed, 42 insertions(+), 8 deletions(-) diff --git a/backend/Profilingaux.ml b/backend/Profilingaux.ml index d57a38be..0644e843 100644 --- a/backend/Profilingaux.ml +++ b/backend/Profilingaux.ml @@ -1,20 +1,54 @@ open Camlcoq open RTL - -let function_id (f : coq_function) : Digest.t = + +type identifier = Digest.t + +let function_id (f : coq_function) : identifier = Digest.string (Marshal.to_string f []);; -let branch_id (f_id : Digest.t) (node : P.t) : Digest.t = +let branch_id (f_id : identifier) (node : P.t) : identifier = Digest.string (f_id ^ (Int64.to_string (P.to_int64 node)));; -let pp_id channel (x : Digest.t) = +let pp_id channel (x : identifier) = for i=0 to 15 do Printf.fprintf channel "%02x" (Char.code (String.get x i)) done -let spp_id () (x : Digest.t) : string = +let spp_id () (x : identifier) : string = let s = ref "" in for i=0 to 15 do s := Printf.sprintf "%02x%s" (Char.code (String.get x i)) !s done; !s;; + +let profiling_counts : (identifier, (Int64.t*Int64.t)) Hashtbl.t = Hashtbl.create 1000;; + +let get_counts id = + match Hashtbl.find_opt profiling_counts id with + | Some x -> x + | None -> (0L, 0L);; + +let add_profiling_counts id counter0 counter1 = + let (old0, old1) = get_counts id in + Hashtbl.replace profiling_counts id (Int64.add old0 counter0, + Int64.add old1 counter1);; + +let input_counter (ic : in_channel) : Int64.t = + let r = ref Int64.zero in + for i=0 to 7 + do + r := Int64.add !r (Int64.shift_left (Int64.of_int (input_byte ic)) (8*i)) + done; + !r;; + +let load_profiling_info (filename : string) : unit = + let ic = open_in filename in + try + while true do + let id : identifier = really_input_string ic 16 in + let counter0 = input_counter ic in + let counter1 = input_counter ic in + Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id counter0 counter1; + add_profiling_counts id counter0 counter1 + done + with End_of_file -> close_in ic;; diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 87c8d9c8..600c3371 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -84,4 +84,3 @@ let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 let option_profile_arcs = ref false - diff --git a/driver/Driver.ml b/driver/Driver.ml index 909ef0d5..7fbcb025 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -328,6 +328,7 @@ let cmdline_actions = _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-Obranchless", Set option_Obranchless; + Exact "-fprofile-use=", String (fun s -> Profilingaux.load_profiling_info s); Exact "-finline-auto-threshold", Integer (fun n -> option_inline_auto_threshold := n); Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 19537bc0..355696de 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -248,7 +248,7 @@ module Target (*: TARGET*) = match Hashtbl.find_opt profiling_table x with | None -> let y = !next_profiling_position in next_profiling_position := succ y; - Hashtbl.add profiling_table x y; + Hashtbl.replace profiling_table x y; y | Some y -> y;; diff --git a/runtime/c/write_profiling_table.c b/runtime/c/write_profiling_table.c index 54044016..5c55c4b6 100644 --- a/runtime/c/write_profiling_table.c +++ b/runtime/c/write_profiling_table.c @@ -18,7 +18,7 @@ static void write_counter(FILE *fp, uint64_t counter) { putc(BYTE(counter, 4), fp); putc(BYTE(counter, 5), fp); putc(BYTE(counter, 6), fp); - putc(BYTE(counter, 8), fp); + putc(BYTE(counter, 7), fp); } void _compcert_write_profiling_table(unsigned int nr_items, -- cgit