diff options
| -rw-r--r-- | backend/Profilingaux.ml | 2 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 28 | ||||
| -rw-r--r-- | test/monniaux/minisat/Makefile.profiled | 4 |
3 files changed, 21 insertions, 13 deletions
diff --git a/backend/Profilingaux.ml b/backend/Profilingaux.ml index 51718303..a1d41ceb 100644 --- a/backend/Profilingaux.ml +++ b/backend/Profilingaux.ml @@ -55,6 +55,6 @@ let load_profiling_info (filename : string) : unit = let condition_oracle (id : identifier) : bool option = let (count0, count1) = get_counts id in - Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id count0 count1; + (* Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id count0 count1; *) if count0 = count1 then None else Some(count1 > count0);; diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 355696de..e154894b 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -272,9 +272,19 @@ module Target (*: TARGET*) = let profiling_counter_table_name = ".compcert_profiling_counters" and profiling_id_table_name = ".compcert_profiling_ids" and profiling_write_table = ".compcert_profiling_write_table" - and profiling_write_table_helper = "_compcert_write_profiling_table";; - - let print_profiling oc = + and profiling_write_table_helper = "_compcert_write_profiling_table" + and dtor_section = ".dtors.65435";; + + let k1c_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name = + fprintf oc " make $r0 = %d\n" nr_items; + fprintf oc " make $r1 = %s\n" profiling_id_table_name; + fprintf oc " make $r2 = %s\n" profiling_counter_table_name; + fprintf oc " goto %s\n" profiling_write_table_helper; + fprintf oc " ;;\n";; + + let print_profiling finalizer_section print_profiling_stub oc = let nr_items = !next_profiling_position in if nr_items > 0 then @@ -286,12 +296,10 @@ module Target (*: TARGET*) = Array.iter (print_profiling_id oc) (profiling_ids ()); fprintf oc " .text\n"; fprintf oc "%s:\n" profiling_write_table; - fprintf oc " make $r0 = %d\n" nr_items; - fprintf oc " make $r1 = %s\n" profiling_id_table_name; - fprintf oc " make $r2 = %s\n" profiling_counter_table_name; - fprintf oc " goto %s\n" profiling_write_table_helper; - fprintf oc " ;;\n"; - fprintf oc " .section .dtors.65435,\"aw\",@progbits\n"; + print_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name; + fprintf oc " .section %s,\"aw\",@progbits\n" finalizer_section; fprintf oc " .align 8\n"; fprintf oc " .8byte %s\n" profiling_write_table end;; @@ -860,7 +868,7 @@ module Target (*: TARGET*) = end let print_epilogue oc = - print_profiling oc; + print_profiling dtor_section k1c_profiling_stub oc; if !Clflags.option_g then begin Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); section oc Section_text; diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled index 860dcb7e..840261b4 100644 --- a/test/monniaux/minisat/Makefile.profiled +++ b/test/monniaux/minisat/Makefile.profiled @@ -7,7 +7,7 @@ PROFILING_DAT=compcert_profiling.dat EXECUTE=k1-cluster -- EXECUTE_CYCLES=k1-cluster --cycle-based -- EXAMPLE=sudoku.sat - +CCOMPFLAGS=-finline-auto-threshold 50 ALL=minisat.ccomp.log minisat.ccomp.trace-linearize.log minisat.ccomp.profiled.log minisat.gcc-O3.log minisat.gcc-O3.profiled.log all: $(ALL) @@ -46,7 +46,7 @@ minisat.ccomp.profiled.exe: $(CFILES) $(PROFILING_DAT) $(EXECUTE_CYCLES) $< $(EXAMPLE) 2>&1 | tee $@ clean: - -rm -f $(ALL) $(PROFILING_DAT) $(GCDAFILES) + -rm -f *.log *.exe $(PROFILING_DAT) $(GCDAFILES) .PHONY: clean gcda |