From d3a8a8870050810a7bc3fb5e004059197ec364f8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 13:06:00 +0200 Subject: print hashes --- backend/Profilingaux.ml | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) (limited to 'backend/Profilingaux.ml') 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;; -- cgit