library support for writing profiling information to files

2 files changed, 48 insertions, 0 deletions

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;
+  }
+}