fixed a bug in support libraries; reload profiling info

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,