begin installing profiling

1 files changed, 53 insertions, 44 deletions

diff --git a/backend/Profiling.v b/backend/Profiling.v
index ce0e4e38..4995c507 100644
--- a/backend/Profiling.v
+++ b/backend/Profiling.v
@@ -4,54 +4,63 @@ Require Import Memory Registers Op RTL.
 
 Local Open Scope positive.
 
-Definition inject_profiling_call (prog : code)
-           (pc extra_pc ifso ifnot : node) : node * code :=
-  let extra_pc' := Pos.succ extra_pc in
-  let prog' := PTree.set extra_pc
-                   (Ibuiltin (EF_profiling 0%Z) nil BR_none ifso) prog in
-  let prog'':= PTree.set extra_pc'
-                   (Ibuiltin (EF_profiling 0%Z) nil BR_none ifnot) prog' in
-  (Pos.succ extra_pc', prog'').
-                          
-Definition inject_at (prog : code) (pc extra_pc : node) : node * code :=
-  match PTree.get pc prog with
-  | Some (Icond cond args ifso ifnot expected) =>
-    inject_profiling_call
-      (PTree.set pc
-        (Icond cond args extra_pc (Pos.succ extra_pc) expected) prog)
+Parameter fundef_id : fundef -> Z.
+Parameter branch_id : Z -> node -> Z.
+
+Section PER_FUNCTION_ID.
+  Variable function_id : Z.
+  
+  Definition inject_profiling_call (prog : code)
+             (pc extra_pc ifso ifnot : node) : node * code :=
+    let id := branch_id function_id pc in
+    let extra_pc' := Pos.succ extra_pc in
+    let prog' := PTree.set extra_pc
+                           (Ibuiltin (EF_profiling id 0%Z) nil BR_none ifso) prog in
+    let prog'':= PTree.set extra_pc'
+                           (Ibuiltin (EF_profiling id 1%Z) nil BR_none ifnot) prog' in
+    (Pos.succ extra_pc', prog'').
+  
+  Definition inject_at (prog : code) (pc extra_pc : node) : node * code :=
+    match PTree.get pc prog with
+    | Some (Icond cond args ifso ifnot expected) =>
+      inject_profiling_call
+        (PTree.set pc
+                   (Icond cond args extra_pc (Pos.succ extra_pc) expected) prog)
         pc extra_pc ifso ifnot
-  | _ => inject_profiling_call prog pc extra_pc 1 1 (* does not happen *)
-  end.
-
-Definition inject_at' (already : node * code) pc :=
-  let (extra_pc, prog) := already in
-  inject_at prog pc extra_pc.
-
-Definition inject_l (prog : code) extra_pc injections :=
-  List.fold_left (fun already (inject_pc : node) =>
-                    inject_at' already inject_pc)
-    injections
-    (extra_pc, prog).
-
-Definition gen_conditions (prog : code) :=
-  List.map fst (PTree.elements (PTree.filter1
-    (fun instr =>
-       match instr with
-       | Icond cond args ifso ifnot expected => true
-       | _ => false
-       end) prog)).
-
-Definition transf_function (f : function) : function :=
-  let max_pc := max_pc_function f in
-  let conditions := gen_conditions (fn_code f) in
+    | _ => inject_profiling_call prog pc extra_pc 1 1 (* does not happen *)
+    end.
+
+  Definition inject_at' (already : node * code) pc :=
+    let (extra_pc, prog) := already in
+    inject_at prog pc extra_pc.
+
+  Definition inject_l (prog : code) extra_pc injections :=
+    List.fold_left (fun already (inject_pc : node) =>
+                      inject_at' already inject_pc)
+                   injections
+                   (extra_pc, prog).
+
+  Definition gen_conditions (prog : code) :=
+    List.map fst (PTree.elements (PTree.filter1
+                                    (fun instr =>
+                                       match instr with
+                                       | Icond cond args ifso ifnot expected => true
+                                       | _ => false
+                                       end) prog)).
+
+  Definition transf_function (f : function) : function :=
+    let max_pc := max_pc_function f in
+    let conditions := gen_conditions (fn_code f) in
     {| fn_sig := f.(fn_sig);
-          fn_params := f.(fn_params);
-          fn_stacksize := f.(fn_stacksize);
-          fn_code := snd (inject_l (fn_code f) (Pos.succ max_pc) conditions);
-          fn_entrypoint := f.(fn_entrypoint) |}.
+       fn_params := f.(fn_params);
+       fn_stacksize := f.(fn_stacksize);
+       fn_code := snd (inject_l (fn_code f) (Pos.succ max_pc) conditions);
+       fn_entrypoint := f.(fn_entrypoint) |}.
+
+End PER_FUNCTION_ID.
 
 Definition transf_fundef (fd: fundef) : fundef :=
-  AST.transf_fundef transf_function fd.
+  AST.transf_fundef (transf_function (fundef_id fd)) fd.
 
 Definition transf_program (p: program) : program :=
   transform_program transf_fundef p.