begin installing profiling

10 files changed, 73 insertions, 54 deletions

diff --git a/Makefile b/Makefile
index 2cd40800..cad61d9d 100644
--- a/Makefile
+++ b/Makefile
@@ -79,6 +79,7 @@ BACKEND=\
   RTLgen.v RTLgenspec.v RTLgenproof.v \
   Tailcall.v Tailcallproof.v \
   Inlining.v Inliningspec.v Inliningproof.v \
+  Profiling.v Profilingproof.v \
   Renumber.v Renumberproof.v \
   Duplicate.v Duplicateproof.v \
   RTLtyping.v \
diff --git a/backend/CSE.v b/backend/CSE.v
index 9ba50a34..838d96a6 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -493,7 +493,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
               | _ =>
                   empty_numbering
               end
-          | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ | EF_profiling _ =>
+          | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ | EF_profiling _ _ =>
               set_res_unknown before res
           end
       | Icond cond args ifso ifnot _ =>
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.
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 609689a7..fbf9bbeb 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -535,7 +535,7 @@ Definition do_external (ef: external_function):
   | EF_annot_val kind text targ => do_ef_annot_val text targ
   | EF_inline_asm text sg clob => do_inline_assembly text sg ge
   | EF_debug kind text targs => do_ef_debug kind text targs
-  | EF_profiling id => do_ef_profiling id
+  | EF_profiling id kind => do_ef_profiling id
   end.
 
 Lemma do_ef_external_sound:
diff --git a/common/AST.v b/common/AST.v
index 595ace01..846678c2 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -466,6 +466,7 @@ Qed.
 
 (* Identifiers for profiling information *)
 Definition profiling_id := Z.t.
+Definition profiling_kind := Z.t.
 
 (** For most languages, the functions composing the program are either
   internal functions, defined within the language, or external functions,
@@ -521,8 +522,8 @@ Inductive external_function : Type :=
      (** Transport debugging information from the front-end to the generated
          assembly.  Takes zero, one or several arguments like [EF_annot].
          Unlike [EF_annot], produces no observable event. *)
-  | EF_profiling (id: profiling_id).
-     (** Count one profiling event for this identifier.
+  | EF_profiling (id: profiling_id) (kind : profiling_kind).
+     (** Count one profiling event for this identifier and kind.
          Takes no argument. Produces no observable event. *)
 
 (** The type signature of an external function. *)
@@ -541,7 +542,7 @@ Definition ef_sig (ef: external_function): signature :=
   | EF_annot_val kind text targ => mksignature (targ :: nil) targ cc_default
   | EF_inline_asm text sg clob => sg
   | EF_debug kind text targs => mksignature targs Tvoid cc_default
-  | EF_profiling id => mksignature nil Tvoid cc_default
+  | EF_profiling id kind => mksignature nil Tvoid cc_default
   end.
 
 (** Whether an external function should be inlined by the compiler. *)
@@ -560,7 +561,7 @@ Definition ef_inline (ef: external_function) : bool :=
   | EF_annot_val kind Text rg => true
   | EF_inline_asm text sg clob => true
   | EF_debug kind text targs => true
-  | EF_profiling id => true
+  | EF_profiling id kind => true
   end.
 
 (** Whether an external function must reload its arguments. *)
diff --git a/common/Events.v b/common/Events.v
index 16efd89c..033e2e03 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1569,7 +1569,7 @@ Definition external_call (ef: external_function): extcall_sem :=
   | EF_annot_val kind txt targ => extcall_annot_val_sem txt targ
   | EF_inline_asm txt sg clb => inline_assembly_sem txt sg
   | EF_debug kind txt targs => extcall_debug_sem
-  | EF_profiling id       => extcall_profiling_sem
+  | EF_profiling id kind  => extcall_profiling_sem
   end.
 
 Theorem external_call_spec:
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 7f15bc91..69939428 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -62,8 +62,8 @@ let name_of_external = function
   | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (camlstring_of_coqstring text)
   | EF_debug(kind, text, targs) ->
      sprintf "debug%d %S" (P.to_int kind) (extern_atom text)
-  | EF_profiling(id) ->
-     sprintf "profiling %LX" (Z.to_int64 id)
+  | EF_profiling(id, kind) ->
+     sprintf "profiling %LX %d" (Z.to_int64 id) (Z.to_int kind)
 
 let rec print_builtin_arg px oc = function
   | BA x -> px oc x
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 6986fb96..87c8d9c8 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -82,3 +82,6 @@ let option_fcoalesce_mem = ref true
 let option_fforward_moves = ref true
 let option_all_loads_nontrap = ref false
 let option_inline_auto_threshold = ref 0
+
+let option_profile_arcs = ref false
+                            
diff --git a/driver/Compopts.v b/driver/Compopts.v
index 848657e5..245322ef 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -75,6 +75,9 @@ Parameter all_loads_nontrap: unit -> bool.
 (** Flag -fforward-moves. Forward moves after CSE. *)
 Parameter optim_forward_moves: unit -> bool.
 
+(** Flag -fprofile-arcs. Add profiling logger. *)
+Parameter profile_arcs : unit -> bool.
+
 (* TODO is there a more appropriate place? *)
 Require Import Coqlib.
 Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 388482a0..909ef0d5 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -223,6 +223,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)
   -falign-branch-targets <n>  Set alignment (in bytes) of branch targets
   -falign-cond-branches <n>  Set alignment (in bytes) of conditional branches
   -fcommon       Put uninitialized globals in the common section [on].
+  -fprofile-arcs  Profile branches [off].
 |} ^
  target_help ^
  toolchain_help ^
@@ -412,7 +413,8 @@ let cmdline_actions =
   @ f_opt "coalesce-mem" option_fcoalesce_mem
   @ f_opt "all-loads-nontrap" option_all_loads_nontrap
   @ f_opt "forward-moves" option_fforward_moves
-(* Code generation options *)
+ (* Code generation options *)
+  @ f_opt "profile-arcs" option_profile_arcs  
   @ f_opt "fpu" option_ffpu
   @ f_opt "sse" option_ffpu (* backward compatibility *)
   @ [