From da923568ad5085654b8db034310c4db50848e16e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Apr 2020 15:45:05 +0200
Subject: library support for writing profiling information to files

---
 mppa_k1c/TargetPrinter.ml         | 21 ++++++++++++++----
 runtime/Makefile                  |  2 ++
 runtime/c/write_profiling_table.c | 46 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 65 insertions(+), 4 deletions(-)
 create mode 100644 runtime/c/write_profiling_table.c

diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 5b66cc26..19537bc0 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -241,9 +241,7 @@ module Target (*: TARGET*) =
   *)
 
     (* Profiling *)
-
-    let profiling_counter_table_name = ".compcert_profiling_counters"
-    and profiling_id_table_name = ".compcert_profiling_ids"
+    
     let profiling_table : (Digest.t, int) Hashtbl.t = Hashtbl.create 1000;;
     let next_profiling_position = ref 0;;
     let profiling_position (x : Digest.t) : int =
@@ -270,6 +268,11 @@ module Target (*: TARGET*) =
         if i < 15 then output_char oc ','
       done;
       output_char oc '\n';;
+
+    let profiling_counter_table_name = ".compcert_profiling_counters"
+    and profiling_id_table_name = ".compcert_profiling_ids"
+    and profiling_write_table = ".compcert_profiling_write_table"
+    and profiling_write_table_helper = "_compcert_write_profiling_table";;
       
     let print_profiling oc =
       let nr_items = !next_profiling_position in
@@ -280,7 +283,17 @@ module Target (*: TARGET*) =
             profiling_counter_table_name (nr_items * 16);
           fprintf oc "	.section	.rodata\n";
           fprintf oc "%s:\n" profiling_id_table_name;
-          Array.iter (print_profiling_id oc) (profiling_ids ())
+          Array.iter (print_profiling_id oc) (profiling_ids ());
+          fprintf oc "	.text\n";
+          fprintf oc "%s:\n" profiling_write_table;
+          fprintf oc "	make $r0 = %d\n" nr_items;
+          fprintf oc "	make $r1 = %s\n" profiling_id_table_name;
+          fprintf oc "	make $r2 = %s\n" profiling_counter_table_name;
+          fprintf oc "	goto	%s\n" profiling_write_table_helper;
+          fprintf oc "	;;\n";
+          fprintf oc "	.section	.dtors.65435,\"aw\",@progbits\n";
+          fprintf oc "	.align 8\n";
+          fprintf oc "	.8byte	%s\n" profiling_write_table
         end;;
     
     (* Offset part of a load or store *)
diff --git a/runtime/Makefile b/runtime/Makefile
index 3b1cabc4..c9883577 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -38,6 +38,8 @@ OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \
   vararg.o
 endif
 
+OBJS+=write_profiling_table.o
+
 LIB=libcompcert.a
 
 INCLUDES=include/float.h include/stdarg.h include/stdbool.h \
diff --git a/runtime/c/write_profiling_table.c b/runtime/c/write_profiling_table.c
new file mode 100644
index 00000000..54044016
--- /dev/null
+++ b/runtime/c/write_profiling_table.c
@@ -0,0 +1,46 @@
+#include <stdint.h>
+#include <stdio.h>
+#include <errno.h>
+
+typedef uint8_t md5_hash[16];
+typedef uint64_t condition_counters[2];
+
+static void write_id(FILE *fp, md5_hash *hash) {
+  fwrite(hash, 16, 1, fp);
+}
+
+#define BYTE(counter, i) ((counter >> (8*i)) & 0xFF)
+static void write_counter(FILE *fp, uint64_t counter) {
+  putc(BYTE(counter, 0), fp);
+  putc(BYTE(counter, 1), fp);
+  putc(BYTE(counter, 2), fp);
+  putc(BYTE(counter, 3), fp);
+  putc(BYTE(counter, 4), fp);
+  putc(BYTE(counter, 5), fp);
+  putc(BYTE(counter, 6), fp);
+  putc(BYTE(counter, 8), fp);
+}
+
+void _compcert_write_profiling_table(unsigned int nr_items,
+				      md5_hash id_table[],
+				      condition_counters counter_table[]) {
+  errno = 0;
+  
+  FILE *fp = fopen("compcert_profiling.dat", "a");
+  if (fp == NULL) {
+    perror("open CompCert profiling data for writing");
+    return;
+  }
+  
+  for(unsigned int i=0; i<nr_items; i++) {
+    write_id(fp, &id_table[i]);
+    write_counter(fp, counter_table[i][0]);
+    write_counter(fp, counter_table[i][1]);
+  }
+
+  fclose(fp);
+  if (errno != 0) {
+    perror("write CompCert profiling data");
+    return;
+  }
+}
-- 
cgit