diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 13:06:00 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 13:06:00 +0200 |
commit | d3a8a8870050810a7bc3fb5e004059197ec364f8 (patch) | |
tree | 8368172ddd21e31aea993c80a9740e8b1a2d9706 /backend | |
parent | cce39d8408cfa33ae4cc7c586e35546a5b731dbf (diff) | |
download | compcert-kvx-d3a8a8870050810a7bc3fb5e004059197ec364f8.tar.gz compcert-kvx-d3a8a8870050810a7bc3fb5e004059197ec364f8.zip |
print hashes
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Profiling.v | 8 | ||||
-rw-r--r-- | backend/Profilingaux.ml | 20 |
2 files changed, 20 insertions, 8 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;; |