From da923568ad5085654b8db034310c4db50848e16e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 15:45:05 +0200 Subject: library support for writing profiling information to files --- runtime/Makefile | 2 ++ runtime/c/write_profiling_table.c | 46 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 48 insertions(+) create mode 100644 runtime/c/write_profiling_table.c (limited to 'runtime') 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 +#include +#include + +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 Date: Wed, 8 Apr 2020 16:28:00 +0200 Subject: fixed a bug in support libraries; reload profiling info --- runtime/c/write_profiling_table.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'runtime') diff --git a/runtime/c/write_profiling_table.c b/runtime/c/write_profiling_table.c index 54044016..5c55c4b6 100644 --- a/runtime/c/write_profiling_table.c +++ b/runtime/c/write_profiling_table.c @@ -18,7 +18,7 @@ static void write_counter(FILE *fp, uint64_t counter) { putc(BYTE(counter, 4), fp); putc(BYTE(counter, 5), fp); putc(BYTE(counter, 6), fp); - putc(BYTE(counter, 8), fp); + putc(BYTE(counter, 7), fp); } void _compcert_write_profiling_table(unsigned int nr_items, -- cgit From 76f48469c4b4ca49159dc736830cd806f8dbbf07 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Apr 2020 14:57:37 +0200 Subject: fix write table --- runtime/c/write_profiling_table.c | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'runtime') diff --git a/runtime/c/write_profiling_table.c b/runtime/c/write_profiling_table.c index 5c55c4b6..06cb15da 100644 --- a/runtime/c/write_profiling_table.c +++ b/runtime/c/write_profiling_table.c @@ -27,6 +27,7 @@ void _compcert_write_profiling_table(unsigned int nr_items, errno = 0; FILE *fp = fopen("compcert_profiling.dat", "a"); + fprintf(stderr, "successfully opened profiling file\n"); if (fp == NULL) { perror("open CompCert profiling data for writing"); return; @@ -37,10 +38,13 @@ void _compcert_write_profiling_table(unsigned int nr_items, 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, "no error\n"); } -- cgit From 5659daa886559566fdb6306d989578707838a267 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Apr 2020 16:47:51 +0200 Subject: profiling still crashes on Aarch64 --- runtime/Makefile | 2 +- runtime/c/write_profiling_table.c | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'runtime') diff --git a/runtime/Makefile b/runtime/Makefile index c9883577..bf979d5f 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -73,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 index 06cb15da..3c7303e4 100644 --- a/runtime/c/write_profiling_table.c +++ b/runtime/c/write_profiling_table.c @@ -27,7 +27,7 @@ void _compcert_write_profiling_table(unsigned int nr_items, errno = 0; FILE *fp = fopen("compcert_profiling.dat", "a"); - fprintf(stderr, "successfully opened profiling file\n"); + //fprintf(stderr, "successfully opened profiling file\n"); if (fp == NULL) { perror("open CompCert profiling data for writing"); return; @@ -38,13 +38,13 @@ void _compcert_write_profiling_table(unsigned int nr_items, write_counter(fp, counter_table[i][0]); write_counter(fp, counter_table[i][1]); } - fprintf(stderr, "successfully written profiling file\n"); + //fprintf(stderr, "successfully written profiling file\n"); fclose(fp); - fprintf(stderr, "successfully closed profiling file\n"); + //fprintf(stderr, "successfully closed profiling file\n"); if (errno != 0) { perror("write CompCert profiling data"); return; } - fprintf(stderr, "no error\n"); + //fprintf(stderr, "no error\n"); } -- cgit From b19b9defebf96ba8599f481d4c617d43c21642ef Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Apr 2020 18:09:34 +0200 Subject: use proper local labels --- runtime/c/write_profiling_table.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'runtime') diff --git a/runtime/c/write_profiling_table.c b/runtime/c/write_profiling_table.c index 3c7303e4..60bae3d7 100644 --- a/runtime/c/write_profiling_table.c +++ b/runtime/c/write_profiling_table.c @@ -46,5 +46,5 @@ void _compcert_write_profiling_table(unsigned int nr_items, perror("write CompCert profiling data"); return; } - //fprintf(stderr, "no error\n"); + fprintf(stderr, "write CompCert profiling data: no error\n"); } -- cgit From d48af10f5a2ef06b518e86398d504706e4995e09 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 12 Apr 2020 09:05:26 +0200 Subject: now use COMPCERT_PROFILING_DATA and don't print stuff --- runtime/c/write_profiling_table.c | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'runtime') diff --git a/runtime/c/write_profiling_table.c b/runtime/c/write_profiling_table.c index 60bae3d7..0ce7a948 100644 --- a/runtime/c/write_profiling_table.c +++ b/runtime/c/write_profiling_table.c @@ -1,5 +1,6 @@ #include #include +#include #include typedef uint8_t md5_hash[16]; @@ -25,8 +26,15 @@ 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("compcert_profiling.dat", "a"); + FILE *fp = fopen(filename, "a"); //fprintf(stderr, "successfully opened profiling file\n"); if (fp == NULL) { perror("open CompCert profiling data for writing"); @@ -46,5 +54,5 @@ void _compcert_write_profiling_table(unsigned int nr_items, perror("write CompCert profiling data"); return; } - fprintf(stderr, "write CompCert profiling data: no error\n"); + // fprintf(stderr, "write CompCert profiling data: no error\n"); } -- cgit