diff options
| -rw-r--r-- | backend/PrintAsmaux.ml | 54 | ||||
| -rw-r--r-- | backend/Profilingaux.ml | 38 | ||||
| -rw-r--r-- | common/PrintAST.ml | 9 | ||||
| -rw-r--r-- | test/monniaux/minisat/Makefile.profiled | 10 |
4 files changed, 65 insertions, 46 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 25792df5..7a281684 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -363,33 +363,35 @@ let write_symbol_pointer oc sym = else fprintf oc " .4byte %s\n" sym;; let print_profiling_epilogue declare_function finalizer_call_method print_profiling_stub oc = - let nr_items = !next_profiling_position in - if nr_items > 0 + if !Clflags.option_profile_arcs then - begin - fprintf oc " .lcomm %s, %d\n" - profiling_counter_table_name (nr_items * 16); - fprintf oc " .section .rodata\n"; - fprintf oc "%s:\n" profiling_id_table_name; - Array.iter (print_profiling_id oc) (profiling_ids ()); - fprintf oc " .text\n"; - fprintf oc "%s:\n" profiling_write_table; - print_profiling_stub oc nr_items - profiling_id_table_name - profiling_counter_table_name; - declare_function oc profiling_write_table; - match finalizer_call_method with - | Dtors -> - fprintf oc " .section %s\n" dtor_section; - write_symbol_pointer oc profiling_write_table - | Init_atexit(atexit_call) -> - fprintf oc " .section %s\n" init_section; - write_symbol_pointer oc profiling_init; - fprintf oc " .text\n"; - fprintf oc "%s:\n" profiling_init; - atexit_call oc profiling_write_table; - declare_function oc profiling_init - end;; + let nr_items = !next_profiling_position in + if nr_items > 0 + then + begin + fprintf oc " .lcomm %s, %d\n" + profiling_counter_table_name (nr_items * 16); + fprintf oc " .section .rodata\n"; + fprintf oc "%s:\n" profiling_id_table_name; + Array.iter (print_profiling_id oc) (profiling_ids ()); + fprintf oc " .text\n"; + fprintf oc "%s:\n" profiling_write_table; + print_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name; + declare_function oc profiling_write_table; + match finalizer_call_method with + | Dtors -> + fprintf oc " .section %s\n" dtor_section; + write_symbol_pointer oc profiling_write_table + | Init_atexit(atexit_call) -> + fprintf oc " .section %s\n" init_section; + write_symbol_pointer oc profiling_init; + fprintf oc " .text\n"; + fprintf oc "%s:\n" profiling_init; + atexit_call oc profiling_write_table; + declare_function oc profiling_init + end;; let profiling_offset id kind = ((profiling_position id)*2 + kind)*8;; diff --git a/backend/Profilingaux.ml b/backend/Profilingaux.ml index 0ba739c2..f8fc5d6b 100644 --- a/backend/Profilingaux.ml +++ b/backend/Profilingaux.ml @@ -1,25 +1,35 @@ open Camlcoq open RTL - +open Maps + type identifier = Digest.t - -let function_id (f : coq_function) : identifier = - Digest.string (Marshal.to_string f []);; - -let branch_id (f_id : identifier) (node : P.t) : identifier = - Digest.string (f_id ^ (Int64.to_string (P.to_int64 node)));; let pp_id channel (x : identifier) = + assert(String.length x = 16); for i=0 to 15 do Printf.fprintf channel "%02x" (Char.code (String.get x i)) done -let spp_id () (x : identifier) : string = - let s = ref "" in - for i=0 to 15 do - s := Printf.sprintf "%02x%s" (Char.code (String.get x i)) !s - done; - !s;; +let print_anonymous_function pp f = + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements f.fn_code)) in + PrintRTL.print_succ pp f.fn_entrypoint + (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1); + List.iter (PrintRTL.print_instruction pp) instrs; + Printf.fprintf pp "}\n\n" + +let function_id (f : coq_function) : identifier = + let digest = Digest.string (Marshal.to_string f []) in + Printf.fprintf stderr "FUNCTION hash = %a\n" pp_id digest; + print_anonymous_function stderr f; + digest + +let branch_id (f_id : identifier) (node : P.t) : identifier = + Digest.string (f_id ^ (Int64.to_string (P.to_int64 node)));; let profiling_counts : (identifier, (Int64.t*Int64.t)) Hashtbl.t = Hashtbl.create 1000;; @@ -55,7 +65,7 @@ let load_profiling_info (filename : string) : unit = let condition_oracle (id : identifier) : bool option = let (count0, count1) = get_counts id in - (if count0 <> 0L || count1 <> 0L then + ( (* if count0 <> 0L || count1 <> 0L then *) Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id count0 count1); if count0 = count1 then None else Some(count1 > count0);; diff --git a/common/PrintAST.ml b/common/PrintAST.ml index e24607ee..38bbfa47 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -47,6 +47,13 @@ let name_of_chunk = function | Many32 -> "any32" | Many64 -> "any64" +let spp_profiling_id () (x : Digest.t) : string = + let s = Buffer.create 32 in + for i=0 to 15 do + Printf.bprintf s "%02x" (Char.code (String.get x i)) + done; + Buffer.contents s;; + let name_of_external = function | EF_external(name, sg) -> sprintf "extern %S" (camlstring_of_coqstring name) | EF_builtin(name, sg) -> sprintf "builtin %S" (camlstring_of_coqstring name) @@ -63,7 +70,7 @@ let name_of_external = function | EF_debug(kind, text, targs) -> sprintf "debug%d %S" (P.to_int kind) (extern_atom text) | EF_profiling(id, kind) -> - sprintf "profiling %a %d" Profilingaux.spp_id id (Z.to_int kind) + sprintf "profiling %a %d" spp_profiling_id id (Z.to_int kind) let rec print_builtin_arg px oc = function | BA x -> px oc x diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled index e66db1db..85e5c246 100644 --- a/test/monniaux/minisat/Makefile.profiled +++ b/test/monniaux/minisat/Makefile.profiled @@ -3,17 +3,17 @@ CFILES=main.c solver.c clock.c CCOMP=../../../ccomp -GCC=aarch64-linux-gnu-gcc -#GCC=k1-cos-gcc -EXECUTE=qemu-aarch64 +#GCC=aarch64-linux-gnu-gcc +GCC=k1-cos-gcc +#EXECUTE=qemu-aarch64 #EXECUTE=qemu-arm -#EXECUTE=k1-cluster -- +EXECUTE=k1-cluster -- EXECUTE_CYCLES=k1-cluster --cycle-based -- LIBS=-lm PROFILING_DAT=compcert_profiling.dat EXAMPLE=sudoku.sat -CCOMPFLAGS=-finline-auto-threshold 50 -static -finline-asm +CCOMPFLAGS=-static -finline-asm -finline-auto-threshold 50 GCCFLAGS=-static ALL=minisat.ccomp.log minisat.ccomp.trace-linearize.log minisat.ccomp.profiled.log minisat.gcc-O3.log minisat.gcc-O3.profiled.log |