blob: 51718303f102571fa1e9e35c72ba17016aa1e2ad (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
open Camlcoq
open RTL
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) =
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 profiling_counts : (identifier, (Int64.t*Int64.t)) Hashtbl.t = Hashtbl.create 1000;;
let get_counts id =
match Hashtbl.find_opt profiling_counts id with
| Some x -> x
| None -> (0L, 0L);;
let add_profiling_counts id counter0 counter1 =
let (old0, old1) = get_counts id in
Hashtbl.replace profiling_counts id (Int64.add old0 counter0,
Int64.add old1 counter1);;
let input_counter (ic : in_channel) : Int64.t =
let r = ref Int64.zero in
for i=0 to 7
do
r := Int64.add !r (Int64.shift_left (Int64.of_int (input_byte ic)) (8*i))
done;
!r;;
let load_profiling_info (filename : string) : unit =
let ic = open_in filename in
try
while true do
let id : identifier = really_input_string ic 16 in
let counter0 = input_counter ic in
let counter1 = input_counter ic in
(* Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id counter0 counter1; *)
add_profiling_counts id counter0 counter1
done
with End_of_file -> close_in ic;;
let condition_oracle (id : identifier) : bool option =
let (count0, count1) = get_counts id in
Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id count0 count1;
if count0 = count1 then None
else Some(count1 > count0);;
|