Recording of prediction stats with COMPCERT_PROFILING_STATS environment flag

It only works correctly if both profiling and static prediction are
used: it then compares both and gives stats in COMPCERT_PREDICT_STATS
file.

The stats are of the form:
  total correct mispredicts missed

total = number of total CBs encountered
correct = number of correct predictions
mispredicts = times when static prediction did a wrong guess (predicted
    the opposite from profiling, or predicted Some _ when profiling said
    None)
missed = times when static prediction was not able to give a verdict,
       though the profiling gave one

1 files changed, 93 insertions, 33 deletions

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index b3635527..62805d5b 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -24,6 +24,45 @@ open Maps
 open Camlcoq
 open DebugPrint
 
+let stats_oc = ref None
+
+let set_stats_oc () =
+  try
+    let name = Sys.getenv "COMPCERT_PREDICT_STATS" in
+    let oc = open_out_gen [Open_append; Open_creat; Open_text] 0o666 name in
+    stats_oc := Some oc
+  with Not_found -> ()
+
+(* number of total CBs *)
+let stats_nb_total = ref 0
+(* we predicted the same thing as the profiling *)
+let stats_nb_correct_predicts = ref 0
+(* we predicted something (say Some true), but the profiling predicted the opposite (say Some false, or None) *)
+let stats_nb_mispredicts = ref 0
+(* we did not predict anything (None) even though the profiling did predict something *)
+let stats_nb_missed_opportunities = ref 0
+
+let reset_stats () = begin
+  stats_nb_total := 0;
+  stats_nb_correct_predicts := 0;
+  stats_nb_mispredicts := 0;
+  stats_nb_missed_opportunities := 0;
+end
+
+let incr theref = theref := !theref + 1
+
+let has_some o = match o with Some _ -> true | None -> false
+
+let stats_oc_recording () = has_some !stats_oc
+
+let write_stats_oc () =
+  match !stats_oc with
+  | None -> ()
+  | Some oc -> begin
+      Printf.fprintf oc "%d %d %d %d\n" !stats_nb_total !stats_nb_correct_predicts !stats_nb_mispredicts !stats_nb_missed_opportunities;
+      close_out oc
+    end
+
 let get_loop_headers = LICMaux.get_loop_headers
 let get_some = LICMaux.get_some
 let rtl_successors = LICMaux.rtl_successors
@@ -397,28 +436,27 @@ let get_directions f code entrypoint = begin
     (* debug "\n"; *)
     List.iter (fun n ->
       match (get_some @@ PTree.get n code) with
-      | Icond (cond, lr, ifso, ifnot, pred) ->
-          (match pred with Some _ -> debug "RTL node %d already has prediction information\n" (P.to_int n)
-          | None ->
-          (* debug "Analyzing %d.." (P.to_int n); *)
-          let heuristics = [ do_opcode_heuristic;
-            do_return_heuristic; do_loop2_heuristic loop_info n; do_loop_heuristic; do_call_heuristic;
-             (* do_store_heuristic *) ] in
-          let preferred = ref None in
-          begin
-            debug "Deciding condition for RTL node %d\n" (P.to_int n);
-            List.iter (fun do_heur ->
-              match !preferred with
-              | None -> preferred := do_heur code cond ifso ifnot is_loop_header
-              | Some _ -> ()
-            ) heuristics;
-            directions := PTree.set n !preferred !directions;
-            (match !preferred with | Some false -> debug "\tFALLTHROUGH\n"
-                                   | Some true -> debug "\tBRANCH\n"
-                                   | None -> debug "\tUNSURE\n");
-            debug "---------------------------------------\n"
-          end
-          )
+      | Icond (cond, lr, ifso, ifnot, pred) -> begin
+          if stats_oc_recording () || not @@ has_some pred then
+            (* debug "Analyzing %d.." (P.to_int n); *)
+            let heuristics = [ do_opcode_heuristic;
+              do_return_heuristic; do_loop2_heuristic loop_info n; do_loop_heuristic; do_call_heuristic;
+               (* do_store_heuristic *) ] in
+            let preferred = ref None in
+            begin
+              debug "Deciding condition for RTL node %d\n" (P.to_int n);
+              List.iter (fun do_heur ->
+                match !preferred with
+                | None -> preferred := do_heur code cond ifso ifnot is_loop_header
+                | Some _ -> ()
+              ) heuristics;
+              directions := PTree.set n !preferred !directions;
+              (match !preferred with | Some false -> debug "\tFALLTHROUGH\n"
+                                     | Some true -> debug "\tBRANCH\n"
+                                     | None -> debug "\tUNSURE\n");
+              debug "---------------------------------------\n"
+            end
+        end
       | _ -> ()
     ) bfs_order;
     !directions
@@ -426,11 +464,28 @@ let get_directions f code entrypoint = begin
 end
 
 let update_direction direction = function
-| Icond (cond, lr, n, n', pred) ->
+| Icond (cond, lr, n, n', pred) -> begin
+    (* Counting stats from profiling *)
+    if stats_oc_recording () then begin
+      incr stats_nb_total;
+      match pred, direction with
+      | None, None -> incr stats_nb_correct_predicts
+      | None, Some _ -> incr stats_nb_mispredicts
+      | Some _, None -> incr stats_nb_missed_opportunities
+      | Some false, Some false -> incr stats_nb_correct_predicts
+      | Some false, Some true -> incr stats_nb_mispredicts
+      | Some true, Some false -> incr stats_nb_mispredicts
+      | Some true, Some true -> incr stats_nb_correct_predicts
+    end;
+
     (* only update if there is no prior existing branch prediction *)
     (match pred with
     | None -> Icond (cond, lr, n, n', direction)
-    | Some _ -> Icond (cond, lr, n, n', pred) )
+    | Some _ -> begin
+        Icond (cond, lr, n, n', pred) 
+      end
+    )
+    end
 | i -> i
 
 (* Uses branch prediction to write prediction annotations in Icond *)
@@ -1026,15 +1081,20 @@ let static_predict f =
   let entrypoint = f.fn_entrypoint in
   let code = f.fn_code in
   let revmap = make_identity_ptree code in
-  let code =
-    if !Clflags.option_fpredict then
-      update_directions f code entrypoint
-    else code in
-  let code =
-    if !Clflags.option_fpredict then
-      invert_iconds code
-    else code in
-  ((code, entrypoint), revmap)
+  begin
+    reset_stats ();
+    set_stats_oc ();
+    let code =
+      if !Clflags.option_fpredict then
+        update_directions f code entrypoint
+      else code in
+    write_stats_oc ();
+    let code =
+      if !Clflags.option_fpredict then
+        invert_iconds code
+      else code in
+    ((code, entrypoint), revmap)
+  end
 
 let unroll_single f =
   let entrypoint = f.fn_entrypoint in