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/Profilingaux.ml | |
| parent | cce39d8408cfa33ae4cc7c586e35546a5b731dbf (diff) | |
| download | compcert-kvx-d3a8a8870050810a7bc3fb5e004059197ec364f8.tar.gz compcert-kvx-d3a8a8870050810a7bc3fb5e004059197ec364f8.zip | |
print hashes
Diffstat (limited to 'backend/Profilingaux.ml')
| -rw-r--r-- | backend/Profilingaux.ml | 20 |
1 files changed, 16 insertions, 4 deletions
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;; |