diff options
| -rw-r--r-- | backend/Profiling.v | 8 | ||||
| -rw-r--r-- | backend/Profilingaux.ml | 20 | ||||
| -rw-r--r-- | common/AST.v | 5 | ||||
| -rw-r--r-- | common/PrintAST.ml | 2 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 4 |
6 files changed, 28 insertions, 13 deletions
diff --git a/backend/Profiling.v b/backend/Profiling.v index 1840af6e..0dfc0a0b 100644 --- a/backend/Profiling.v +++ b/backend/Profiling.v @@ -4,15 +4,15 @@ Require Import Memory Registers Op RTL. Local Open Scope positive. -Parameter function_id : function -> Z. -Parameter branch_id : Z -> node -> Z. +Parameter function_id : function -> AST.profiling_id. +Parameter branch_id : AST.profiling_id -> node -> AST.profiling_id. Section PER_FUNCTION_ID. - Variable function_id : Z. + Variable f_id : AST.profiling_id. Definition inject_profiling_call (prog : code) (pc extra_pc ifso ifnot : node) : node * code := - let id := branch_id function_id pc in + let id := branch_id f_id pc in let extra_pc' := Pos.succ extra_pc in let prog' := PTree.set extra_pc (Ibuiltin (EF_profiling id 0%Z) nil BR_none ifso) prog in diff --git a/backend/Profilingaux.ml b/backend/Profilingaux.ml index ad963a48..d57a38be 100644 --- a/backend/Profilingaux.ml +++ b/backend/Profilingaux.ml @@ -1,8 +1,20 @@ open Camlcoq open RTL -let function_id (f : coq_function) : Z.t = - Z.of_uint 0;; +let function_id (f : coq_function) : Digest.t = + Digest.string (Marshal.to_string f []);; -let branch_id (f_id : Z.t) (node : P.t) = - Z.of_uint 0;; +let branch_id (f_id : Digest.t) (node : P.t) : Digest.t = + Digest.string (f_id ^ (Int64.to_string (P.to_int64 node)));; + +let pp_id channel (x : Digest.t) = + for i=0 to 15 do + Printf.fprintf channel "%02x" (Char.code (String.get x i)) + done + +let spp_id () (x : Digest.t) : 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;; diff --git a/common/AST.v b/common/AST.v index 846678c2..268e13d5 100644 --- a/common/AST.v +++ b/common/AST.v @@ -465,7 +465,8 @@ Qed. (** * External functions *) (* Identifiers for profiling information *) -Definition profiling_id := Z.t. +Parameter profiling_id : Type. +Axiom profiling_id_eq : forall (x y : profiling_id), {x=y} + {x<>y}. Definition profiling_kind := Z.t. (** For most languages, the functions composing the program are either @@ -577,7 +578,7 @@ Definition ef_reloads (ef: external_function) : bool := Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}. Proof. - generalize ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. + generalize profiling_id_eq ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. decide equality. Defined. Global Opaque external_function_eq. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 69939428..e24607ee 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -63,7 +63,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 %LX %d" (Z.to_int64 id) (Z.to_int kind) + sprintf "profiling %a %d" Profilingaux.spp_id id (Z.to_int kind) let rec print_builtin_arg px oc = function | BA x -> px oc x diff --git a/extraction/extraction.v b/extraction/extraction.v index c2b5d83e..72c19385 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -152,6 +152,8 @@ Extract Constant Compopts.time => "Timing.time_coq". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) (* Profiling *) +Extract Constant AST.profiling_id => "Digest.t". +Extract Constant AST.profiling_id_eq => "Digest.equal". Extract Constant Profiling.function_id => "Profilingaux.function_id". Extract Constant Profiling.branch_id => "Profilingaux.branch_id". diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 491d2c14..eb2d7a97 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -329,8 +329,8 @@ module Target (*: TARGET*) = print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment | EF_profiling(id, kind) -> - fprintf oc "%s profiling %LX %d\n" comment - (Z.to_int64 id) (Z.to_int kind) + fprintf oc "%s profiling %a %d\n" comment + Profilingaux.pp_id id (Z.to_int kind) | _ -> assert false end |