From 5659daa886559566fdb6306d989578707838a267 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Apr 2020 16:47:51 +0200
Subject: profiling still crashes on Aarch64

---
 aarch64/TargetPrinter.ml                | 1 -
 runtime/Makefile                        | 2 +-
 runtime/c/write_profiling_table.c       | 8 ++++----
 test/monniaux/cycles.h                  | 4 ++--
 test/monniaux/minisat/Makefile.profiled | 4 ++--
 5 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index bd26a45f..0eaf3923 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -602,7 +602,6 @@ module Target : TARGET =
     let aarch64_profiling_stub oc nr_items
           profiling_id_table_name
           profiling_counter_table_name =
-	fprintf oc "	ret\n";
 	fprintf oc "	adrp	x2, %s\n" profiling_counter_table_name;
 	fprintf oc "	adrp	x1, %s\n" profiling_id_table_name;
 	fprintf oc "	add	x2, x2, :lo12:%s\n" profiling_counter_table_name;
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");
 }
diff --git a/test/monniaux/cycles.h b/test/monniaux/cycles.h
index 097d6882..36de6cc5 100644
--- a/test/monniaux/cycles.h
+++ b/test/monniaux/cycles.h
@@ -50,7 +50,7 @@ static inline cycle_t get_cycle(void) {
 typedef uint32_t cycle_t;
 #define PRcycle PRId32
 
-#ifdef ARM_NOPRIVILEGE
+#ifdef ARM_NO_PRIVILEGE
 static inline cycle_t get_cycle(void) {
   return 0;
 }
@@ -67,7 +67,7 @@ static inline cycle_t get_cycle(void) {
 #define PRcycle PRId64
 typedef uint64_t cycle_t;
 
-#ifdef ARM_NOPRIVILEGE
+#ifdef ARM_NO_PRIVILEGE
 static inline cycle_t get_cycle(void) {
   return 0;
 }
diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled
index 349089b7..2c078f28 100644
--- a/test/monniaux/minisat/Makefile.profiled
+++ b/test/monniaux/minisat/Makefile.profiled
@@ -20,13 +20,13 @@ minisat.ccomp.exe: $(CFILES)
 	$(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@ $(LIBS)
 
 minisat.ccomp.profile-arcs.exe: $(CFILES)
-	$(CCOMP) -DAMD_NO_PRIVILEGE $(CCOMPFLAGS) -fprofile-arcs $(CFILES) -o $@ $(LIBS)
+	$(CCOMP) -DARM_NO_PRIVILEGE $(CCOMPFLAGS) -fprofile-arcs $(CFILES) -o $@ $(LIBS)
 
 minisat.gcc-O3.exe: $(CFILES)
 	$(GCC) $(GCCFLAGS) -O3 $(CFILES) -o $@ $(LIBS)
 
 minisat.gcc-O3.profile-arcs.exe: $(CFILES)
-	$(GCC) -DAMD_NO_PRIVILEGE $(GCCFLAGS) -fprofile-arcs -O3 $(CFILES) -o $@ $(LIBS)
+	$(GCC) -DARM_NO_PRIVILEGE $(GCCFLAGS) -fprofile-arcs -O3 $(CFILES) -o $@ $(LIBS)
 
 gcda: minisat.gcc-O3.profile-arcs.exe
 	$(EXECUTE) $< $(EXAMPLE)
-- 
cgit