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

2 files changed, 61 insertions, 1 deletions

diff --git a/runtime/Makefile b/runtime/Makefile
index 3b1cabc4..bf979d5f 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 \
@@ -71,7 +73,7 @@ $(LIB): $(OBJS)
 # generated assembly
 
 %.o: c/%.c c/i64.h ../ccomp
-	../ccomp -O2 -S -o $*.s -I./c c/$*.c
+	../ccomp -g -O2 -S -o $*.s -I./c c/$*.c
 	sed -i -e 's/i64_/__compcert_i64_/g' $*.s
 	$(CASMRUNTIME) -o $*.o $*.s
 	@rm $*.s
diff --git a/runtime/c/write_profiling_table.c b/runtime/c/write_profiling_table.c
new file mode 100644
index 00000000..0ce7a948
--- /dev/null
+++ b/runtime/c/write_profiling_table.c
@@ -0,0 +1,58 @@
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.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, 7), fp);
+}
+
+void _compcert_write_profiling_table(unsigned int nr_items,
+				      md5_hash id_table[],
+				      condition_counters counter_table[]) {
+  errno = 0;
+
+  const char *filename = getenv("COMPCERT_PROFILING_DATA");
+  if (filename) {
+    if (!*filename) return;
+  } else {
+    filename = "compcert_profiling.dat";
+  }
+  
+  FILE *fp = fopen(filename, "a");
+  //fprintf(stderr, "successfully opened profiling file\n");
+  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]);
+  }
+  //fprintf(stderr, "successfully written profiling file\n");
+
+  fclose(fp);
+  //fprintf(stderr, "successfully closed profiling file\n");
+  if (errno != 0) {
+    perror("write CompCert profiling data");
+    return;
+  }
+  // fprintf(stderr, "write CompCert profiling data: no error\n");
+}