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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
open CSE3analysis
open Maps
open HashedSet
open Camlcoq
let flatten_eq eq =
((P.to_int eq.eq_lhs), eq.eq_op, List.map P.to_int eq.eq_args);;
let imp_add_i_j s i j =
s := PMap.set i (PSet.add j (PMap.get i !s)) !s;;
let string_of_chunk = function
| AST.Mint8signed -> "int8signed"
| AST.Mint8unsigned -> "int8unsigned"
| AST.Mint16signed -> "int16signed"
| AST.Mint16unsigned -> "int16unsigned"
| AST.Mint32 -> "int32"
| AST.Mint64 -> "int64"
| AST.Mfloat32 -> "float32"
| AST.Mfloat64 -> "float64"
| AST.Many32 -> "any32"
| AST.Many64 -> "any64";;
let print_reg channel i =
Printf.fprintf channel "r%d" i;;
let print_eq channel id (lhs, sop, args) =
Printf.printf "%d: " id;
match sop with
| SOp op ->
Printf.printf "%a = %a\n" print_reg lhs (PrintOp.print_operation print_reg) (op, args)
| SLoad(chunk, addr) ->
Printf.printf "%a = %s @ %a\n" print_reg lhs (string_of_chunk chunk)
(PrintOp.print_addressing print_reg) (addr, args);;
let preanalysis (f : RTL.coq_function) =
let cur_eq_id = ref 0
and cur_catalog = ref PTree.empty
and eq_table = Hashtbl.create 100
and rhs_table = Hashtbl.create 100
and cur_kill_reg = ref (PMap.init PSet.empty)
and cur_kill_mem = ref PSet.empty
and cur_moves = ref (PMap.init PSet.empty) in
let eq_find_oracle node eq =
Hashtbl.find_opt eq_table (flatten_eq eq)
and rhs_find_oracle node sop args =
match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with
| None -> PSet.empty
| Some s -> s in
let mutating_eq_find_oracle node eq : P.t option =
let (flat_eq_lhs, flat_eq_op, flat_eq_args) as flat_eq = flatten_eq eq in
match Hashtbl.find_opt eq_table flat_eq with
| Some x -> Some x
| None ->
incr cur_eq_id;
let id = !cur_eq_id in
let coq_id = P.of_int id in
begin
print_eq stderr id flat_eq;
Hashtbl.add eq_table flat_eq coq_id;
Hashtbl.add rhs_table (flat_eq_op, flat_eq_args)
(PSet.add coq_id
(match Hashtbl.find_opt rhs_table (flat_eq_op, flat_eq_args) with
| None -> PSet.empty
| Some s -> s));
List.iter
(fun reg -> imp_add_i_j cur_kill_reg reg coq_id)
(eq.eq_lhs :: eq.eq_args);
(if eq_depends_on_mem eq
then cur_kill_mem := PSet.add coq_id !cur_kill_mem);
(match eq.eq_op, eq.eq_args with
| (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves eq.eq_lhs coq_id
| _, _ -> ());
Some coq_id
end
in
ignore
(internal_analysis
{ eq_catalog = (fun eq_id -> PTree.get eq_id !cur_catalog);
eq_find_oracle = mutating_eq_find_oracle;
eq_rhs_oracle = rhs_find_oracle ;
eq_kill_reg = (fun reg -> PMap.get reg !cur_kill_reg);
eq_kill_mem = (fun () -> !cur_kill_mem);
eq_moves = (fun reg -> PMap.get reg !cur_moves)
} f);
{ hint_eq_catalog = !cur_catalog;
hint_eq_find_oracle= eq_find_oracle;
hint_eq_rhs_oracle = rhs_find_oracle };;
|