Merge remote-tracking branch 'origin/mppa-profiling' into mppa-features

5 files changed, 56 insertions, 2 deletions

diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index e850fed6..669d8c0c 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -177,6 +177,7 @@ let pp_instructions pp ic =
         | EF_annot_val _
         | EF_builtin _
         | EF_debug _
+        | EF_profiling _
         | EF_external _
         | EF_free
         | EF_malloc
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 89aab5c7..6996c9bb 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -619,7 +619,7 @@ let expand_instruction instr =
 	   | EF_memcpy(sz, al) ->
 	      expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz))
 		(Int32.to_int (camlint_of_coqint al)) args
-	   | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
+	   | EF_annot _ | EF_debug _ | EF_inline_asm _ | EF_profiling _ ->
               emit instr
 	   | _ ->
               assert false
diff --git a/arm/Constantexpand.ml b/arm/Constantexpand.ml
index 408b291e..8cc32c1f 100644
--- a/arm/Constantexpand.ml
+++ b/arm/Constantexpand.ml
@@ -106,6 +106,7 @@ let estimate_size = function
   | Pbuiltin (ef,_,_) ->
     begin match ef with
     | EF_inline_asm _ -> 256
+    | EF_profiling _ -> 40
     | _ -> 0 end
   | Pcfi_adjust _
   | Pcfi_rel_offset _
diff --git a/arm/Machregs.v b/arm/Machregs.v
index ae0ff6bf..1ec8f0a1 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -153,6 +153,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_memcpy sz al => R2 :: R3 :: R12 :: F7 :: nil
   | EF_inline_asm txt sg clob => destroyed_by_clobber clob
+  | EF_profiling _ _ => R2 :: R3 :: R12 :: nil
   | _ => nil
   end.
 
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 54af7cd5..839530c6 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -204,6 +204,38 @@ struct
     | SOasr(r, n) -> fprintf oc "%a, asr #%a" ireg r coqint n
     | SOror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n
 
+
+    let next_profiling_label =
+      let profiling_label_counter = ref 0 in
+      fun () ->
+      let r = sprintf ".Lprofiling_label%d" !profiling_label_counter in
+      incr profiling_label_counter; r;;
+                   
+    let print_profiling_logger oc id kind =
+      assert (kind >= 0);
+      assert (kind <= 1);
+      let ofs = profiling_offset id kind and olbl = next_profiling_label () in
+      fprintf oc "%s begin profiling %a %d: non-atomic increment\n" comment
+        Profilingaux.pp_id id kind;
+      fprintf oc "	ldr	r2, %s\n" olbl;
+      fprintf oc "	ldr	r3, [r2, #%d]\n"
+        (if Configuration.is_big_endian then 8 else 0);
+      fprintf oc "	ldr	r12, [r2, #%d]\n"
+        (if Configuration.is_big_endian then 0 else 8);
+      fprintf oc "	adds	r3, r3, #1\n";
+      fprintf oc "	adc	r12, r12, #0\n";
+      fprintf oc "	str	r3, [r2, #%d]\n"
+        (if Configuration.is_big_endian then 8 else 0);
+      fprintf oc "	str	r12, [r2, #%d]\n"
+        (if Configuration.is_big_endian then 0 else 8);
+      let jlbl = next_profiling_label () in
+      fprintf oc "	b	%s\n" jlbl;
+      fprintf oc "%s:\n" olbl;
+      fprintf oc "	.word	%s + %d\n" profiling_counter_table_name ofs;
+      fprintf oc "%s:\n" jlbl;
+      fprintf oc "%s end profiling %a %d\n" comment
+        Profilingaux.pp_id id kind;;
+
   let print_instruction oc = function
     (* Core instructions *)
     | Padc (r1,r2,so) ->
@@ -484,6 +516,7 @@ struct
           fprintf oc "%s begin inline assembly\n\t" comment;
           print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res;
           fprintf oc "%s end inline assembly\n" comment
+        | EF_profiling(id, coq_kind) -> print_profiling_logger oc id  (Z.to_int coq_kind)
         | _ ->
           assert false
       end
@@ -551,6 +584,11 @@ struct
     if !Clflags.option_mthumb then
       fprintf oc "	.thumb_func\n"
 
+
+  let text_print_fun_info oc name =
+    fprintf oc "	.type	%s, %%function\n" name;
+    fprintf oc "	.size	%s, . - %s\n" name name
+
   let print_fun_info oc name =
     fprintf oc "	.type	%a, %%function\n" symbol name;
     fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
@@ -598,9 +636,22 @@ struct
     if !Clflags.option_g then begin
       section oc Section_text;
       cfi_section oc
-    end
+      end
+
+  let arm_profiling_stub oc nr_items
+          profiling_id_table_name
+          profiling_counter_table_name =
+        fprintf oc "	ldr	r2, = %s\n" profiling_counter_table_name;
+        fprintf oc "	ldr	r1, = %s\n" profiling_id_table_name;
+	fprintf oc "	mov	r0, #%d\n" nr_items;
+	fprintf oc "	b	%s\n" profiling_write_table_helper;;
+  
+  let print_atexit oc to_be_called =
+      	fprintf oc "	ldr	r0, = %s\n" to_be_called;
+	fprintf oc "	b	atexit\n";;
 
   let print_epilogue oc =
+    print_profiling_epilogue text_print_fun_info (Init_atexit print_atexit) arm_profiling_stub oc;
     if !Clflags.option_g then begin
       Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
       section oc Section_text;