x86-64 profiling

3 files changed, 65 insertions, 8 deletions

diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled
index 85e5c246..77ba8b43 100644
--- a/test/monniaux/minisat/Makefile.profiled
+++ b/test/monniaux/minisat/Makefile.profiled
@@ -7,8 +7,8 @@ CCOMP=../../../ccomp
 GCC=k1-cos-gcc
 #EXECUTE=qemu-aarch64
 #EXECUTE=qemu-arm
-EXECUTE=k1-cluster --
-EXECUTE_CYCLES=k1-cluster --cycle-based --
+#EXECUTE=k1-cluster --
+#EXECUTE_CYCLES=k1-cluster --cycle-based --
 
 LIBS=-lm
 PROFILING_DAT=compcert_profiling.dat
@@ -36,7 +36,7 @@ minisat.gcc-O3.profile-arcs.exe: main.c solver.c clock.gcc-O3.noprofile.o
 	$(GCC) -DARM_NO_PRIVILEGE $(GCCFLAGS) -fprofile-arcs -O3 $+ -o $@ $(LIBS)
 
 gcda: minisat.gcc-O3.profile-arcs.exe
-	$(EXECUTE) $< $(EXAMPLE)
+	$(EXECUTE) ./$< $(EXAMPLE)
 
 main.gcda solver.gcda: gcda
 
@@ -48,7 +48,7 @@ minisat.ccomp.trace-linearize.exe: $(CFILES)
 
 $(PROFILING_DAT): minisat.ccomp.profile-arcs.exe
 	-rm -f $(PROFILING_DAT)
-	$(EXECUTE) $< $(EXAMPLE)
+	$(EXECUTE) ./$< $(EXAMPLE)
 
 minisat.ccomp.profiled.exe: $(CFILES) $(PROFILING_DAT)
 	$(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -ftracelinearize $(CFILES) -o $@ $(LIBS)
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index b8353046..ad667e3d 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -552,7 +552,7 @@ let expand_instruction instr =
           expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
        | EF_annot_val(kind,txt, targ) ->
           expand_annot_val kind txt targ args res
-       | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
+       | EF_annot _ | EF_debug _ | EF_inline_asm _ | EF_profiling _ ->
           emit instr
        | _ ->
           assert false
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 6159437e..3ffad3d0 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -165,7 +165,42 @@ module ELF_System : SYSTEM =
 
     let print_var_info = elf_print_var_info
 
-    let print_epilogue _ = ()
+    let print_atexit oc to_be_called =
+      if Archi.ptr64
+      then
+        begin
+          fprintf oc "	leaq	%s(%%rip), %%rdi\n" to_be_called;
+	  fprintf oc "	jmp	atexit\n"
+        end
+      else
+        begin
+          fprintf oc "	pushl	$%s\n" to_be_called;
+          fprintf oc "	call	atexit\n";
+          fprintf oc "	addl	$4, %%esp\n"
+        end
+
+    let x86_profiling_stub oc nr_items
+          profiling_id_table_name
+          profiling_counter_table_name =
+      if Archi.ptr64
+      then
+        begin
+	  fprintf oc "  leaq	%s(%%rip), %%rdx\n" profiling_counter_table_name;
+	  fprintf oc "  leaq	%s(%%rip), %%rsi\n" profiling_id_table_name;
+          fprintf oc "  movl	$%d, %%edi\n" nr_items;
+          fprintf oc "  jmp	%s\n" profiling_write_table_helper
+        end
+      else
+        begin
+          fprintf oc "	pushl	$%s\n" profiling_counter_table_name;
+	  fprintf oc "	pushl	$%s\n" profiling_id_table_name;
+	  fprintf oc "	pushl	$%d\n" nr_items;
+          fprintf oc "	call	%s\n" profiling_write_table_helper ;
+          fprintf oc "	addl	$12, %%esp\n"
+        end;;
+    
+    let print_epilogue oc =
+      print_profiling_epilogue elf_text_print_fun_info (Init_atexit print_atexit) x86_profiling_stub oc;;
 
     let print_comm_decl oc name sz al =
       fprintf oc "	.comm	%a, %s, %d\n" symbol name (Z.to_string sz) al
@@ -395,8 +430,28 @@ module Target(System: SYSTEM):TARGET =
         fprintf oc "%a(%%rip)" label lbl
       end
 
-
-
+    let print_profiling_logger oc id kind =
+      assert (kind >= 0);
+      assert (kind <= 1);
+      let ofs = profiling_offset id kind in
+      if Archi.ptr64
+      then
+        begin
+          fprintf oc "%s profiling %a %d: atomic increment\n" comment
+            Profilingaux.pp_id id kind;
+          fprintf oc "	lock addq	$1, %s+%d(%%rip)\n"
+            profiling_counter_table_name ofs
+        end
+      else
+        begin
+          fprintf oc "%s begin profiling %a %d: increment\n" comment
+            Profilingaux.pp_id id kind;
+          fprintf oc "	addl	$1, %s+%d\n" profiling_counter_table_name ofs;
+          fprintf oc "	adcl	$1, %s+%d\n" profiling_counter_table_name (ofs+4);
+          fprintf oc "%s end profiling %a %d: increment\n" comment
+            Profilingaux.pp_id id kind;
+        end
+      
 (* Printing of instructions *)
 
 (* Reminder on X86 assembly syntaxes:
@@ -834,6 +889,8 @@ module Target(System: SYSTEM):TARGET =
               fprintf oc "%s begin inline assembly\n\t" comment;
               print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
+          | EF_profiling(id, coq_kind) ->
+            print_profiling_logger oc id (Z.to_int coq_kind)          
           | _ ->
               assert false
           end