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
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
open RTL;;
open Camlcoq;;
open Maps;;
open Kildall;;
open HashedSet;;
type reg = P.t;;
module Dominator =
struct
type t = Unreachable | Dominated of int | Multiple
let bot = Unreachable and top = Multiple
let beq a b =
match a, b with
| Unreachable, Unreachable
| Multiple, Multiple -> true
| (Dominated x), (Dominated y) -> x = y
| _ -> false
let lub a b =
match a, b with
| Multiple, _
| _, Multiple -> Multiple
| Unreachable, x
| x, Unreachable -> x
| (Dominated x), (Dominated y) when x=y -> a
| (Dominated _), (Dominated _) -> Multiple
let pp oc = function
| Unreachable -> output_string oc "unreachable"
| Multiple -> output_string oc "multiple"
| Dominated x -> Printf.fprintf oc "%d" x;;
end
module Dominator_Solver = Dataflow_Solver(Dominator)(NodeSetForward)
let apply_dominator (is_marked : node -> bool) (pc : node)
(before : Dominator.t) : Dominator.t =
match before with
| Dominator.Unreachable -> before
| _ ->
if is_marked pc
then Dominator.Dominated (P.to_int pc)
else before;;
let dominated_parts1 (f : coq_function) :
(bool PTree.t) * (Dominator.t PMap.t option) =
let headers = Duplicateaux.get_loop_headers f.fn_code f.fn_entrypoint in
let dominated = Dominator_Solver.fixpoint f.fn_code RTL.successors_instr
(apply_dominator (fun pc -> match PTree.get pc headers with
| Some x -> x
| None -> false)) f.fn_entrypoint
Dominator.top in
(headers, dominated);;
(* unfinished *)
let dominated_parts (f : coq_function) :
PSet.t PTree.t =
let (headers, dominated) = dominated_parts1 f in
match dominated with
| None -> failwith "dominated_parts 1"
| Some dominated ->
let singletons =
PTree.fold (fun before pc flag ->
if flag
then PTree.set pc (PSet.add pc PSet.empty) before
else before) headers PTree.empty in
PTree.fold (fun before pc ii ->
match PMap.get pc dominated with
| Dominator.Dominated x ->
let px = P.of_int x in
(match PTree.get px before with
| None -> failwith "dominated_parts 2"
| Some old ->
PTree.set px (PSet.add pc old) before)
| _ -> before) f.fn_code singletons;;
let pp_pset oc s =
output_string oc "{ ";
let first = ref true in
List.iter (fun x ->
(if !first
then first := false
else output_string oc ", ");
Printf.printf "%d" x)
(List.sort (fun x y -> y - x) (List.map P.to_int (PSet.elements s)));
output_string oc " }";;
let print_dominated_parts oc f =
List.iter (fun (header, nodes) ->
Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes)
(PTree.elements (dominated_parts f));;
let print_dominated_parts1 oc f =
match snd (dominated_parts1 f) with
| None -> output_string oc "error\n"
| Some parts ->
List.iter
(fun (pc, instr) ->
Printf.fprintf oc "%d : %a\n" (P.to_int pc) Dominator.pp
(PMap.get pc parts)
)
(PTree.elements f.fn_code);;
let loop_headers (f : coq_function) : RTL.node list =
List.map fst (List.filter snd (PTree.elements (Duplicateaux.get_loop_headers f.fn_code f.fn_entrypoint)));;
let print_loop_headers f =
print_endline "Loop headers";
List.iter
(fun i -> Printf.printf "%d " (P.to_int i))
(loop_headers f);
print_newline ();;
let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg):
(Inject.inj_instr list) PTree.t =
let _ = print_dominated_parts stdout f in
PTree.empty;;
(*
let max_reg = P.to_int coq_max_reg in
PTree.set coq_max_pc [Inject.INJload(AST.Mint32, (Op.Aindexed (Ptrofs.of_int (Z.of_sint 0))), [P.of_int 1], P.of_int (max_reg+1))] PTree.empty;;
*)
|
