1 files changed, 77 insertions, 0 deletions
diff --git a/backend/Profiling.v b/backend/Profiling.v
new file mode 100644
index 00000000..83e96311
--- /dev/null
+++ b/backend/Profiling.v
@@ -0,0 +1,77 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*                                                             *)
+(*  Copyright VERIMAG. All rights reserved.                    *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL.
+
+Local Open Scope positive.
+
+Parameter function_id : function -> AST.profiling_id.
+Parameter branch_id : AST.profiling_id -> node -> AST.profiling_id.
+
+Section PER_FUNCTION_ID.
+  Variable f_id : AST.profiling_id.
+  
+  Definition inject_profiling_call (prog : code)
+             (pc extra_pc ifso ifnot : node) : node * code :=
+    let id := branch_id f_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 ifnot) prog in
+    let prog'':= PTree.set extra_pc'
+                           (Ibuiltin (EF_profiling id 1%Z) nil BR_none ifso) 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 (Pos.succ extra_pc) 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)).
+End PER_FUNCTION_ID.
+
+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 (function_id f) (fn_code f) (Pos.succ max_pc) conditions);
+     fn_entrypoint := f.(fn_entrypoint) |}.
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.