annotate ppc/peepopt.ml @ 0:bfdcc3820b32

Basis
author Mike Spivey <mike@cs.ox.ac.uk>
date Thu, 05 Oct 2017 08:04:15 +0100
parents
children
rev   line source
0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1 (* ppc/peepopt.ml *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
2 (* Copyright (c) 2017 J. M. Spivey *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
3
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
4 open Keiko
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
5 open Print
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
6
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
7 let debug = ref 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
8
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
9 (* Disjoint sets of labels *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
10
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
11 type lab_data =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
12 LabDef of labrec (* An extant label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
13 | Equiv of codelab (* A label that's been merged *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
14
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
15 and labrec =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
16 { y_id: codelab; (* Name of the label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
17 y_refct: int ref } (* Reference count *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
18
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
19 (* |label_tab| -- map labels to their equivalents *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
20 let label_tab = Hashtbl.create 257
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
21
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
22 (* |get_label| -- get equivalence cell for a label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
23 let get_label x =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
24 try !(Hashtbl.find label_tab x) with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
25 Not_found ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
26 let y = LabDef { y_id = x; y_refct = ref 0 } in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
27 Hashtbl.add label_tab x (ref y); y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
28
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
29 (* |find_label| -- find data about equivalence class of a label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
30 let rec find_label x =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
31 match get_label x with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
32 LabDef y -> y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
33 | Equiv x' -> find_label x'
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
34
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
35 (* |rename| -- get canonical equivalent of a label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
36 let rename x = let y = find_label x in y.y_id
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
37
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
38 (* |ref_count| -- get reference count cell for a label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
39 let ref_count x = let y = find_label x in y.y_refct
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
40
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
41 (* |same_lab| -- test if two labels are equivalent *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
42 let same_lab x1 x2 = (rename x1 = rename x2)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
43
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
44 (* |equate| -- make two labels equivalent *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
45 let equate x1 x2 =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
46 let y1 = find_label x1 and y2 = find_label x2 in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
47 if y1.y_id = y2.y_id then failwith "equate";
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
48 y2.y_refct := !(y1.y_refct) + !(y2.y_refct);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
49 Hashtbl.find label_tab y1.y_id := Equiv y2.y_id
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
50
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
51 (* |do_refs| -- call function on refcount of each label in an instruction *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
52 let do_refs f =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
53 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
54 JUMP x -> f (ref_count x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
55 | JUMPC (w, x) -> f (ref_count x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
56 | JUMPCZ (w, x) -> f (ref_count x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
57 | JCASE labs -> List.iter (fun x -> f (ref_count x)) labs
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
58 | _ -> ()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
59
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
60 (* |rename_labs| -- replace each label by its equivalent *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
61 let rename_labs =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
62 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
63 LABEL x -> LABEL (rename x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
64 | JUMP x -> JUMP (rename x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
65 | JUMPC (w, x) -> JUMPC (w, rename x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
66 | JUMPCZ (w, x) -> JUMPCZ (w, rename x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
67 | JCASE labs -> JCASE (List.map rename labs)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
68 | i -> i
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
69
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
70 let opposite =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
71 function Eq -> Neq | Neq -> Eq | Lt -> Geq
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
72 | Leq -> Gt | Gt -> Leq | Geq -> Lt
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
73 | _ -> failwith "opposite"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
74
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
75 (* |ruleset| -- simplify and introduce abbreviations *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
76 let ruleset replace =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
77 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
78 LOCAL a :: CONST b :: OFFSET :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
79 replace 3 [LOCAL (a+b)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
80 | CONST a :: OFFSET :: CONST b :: OFFSET :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
81 replace 4 [CONST (a+b); OFFSET]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
82 | CONST 0 :: OFFSET :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
83 replace 2 []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
84 | CONST a :: CONST b :: BINOP w :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
85 replace 3 [CONST (do_binop w a b)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
86
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
87 | LOCAL n :: LOAD s :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
88 replace 2 [LDL (n, s)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
89 | LOCAL n :: STORE s :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
90 replace 2 [STL (n, s)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
91 | LOCAL o :: LDNW n :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
92 replace 2 [LDL (o+n, 4)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
93 | LOCAL o :: STNW n :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
94 replace 2 [STL (o+n, 4)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
95 | GLOBAL x :: LOAD s :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
96 replace 2 [LDG (x, s)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
97 | GLOBAL x :: STORE s :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
98 replace 2 [STG (x, s)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
99 | CONST n :: OFFSET :: LOAD 4 :: _->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
100 replace 3 [LDNW n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
101 | CONST n :: OFFSET :: STORE 4 :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
102 replace 3 [STNW n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
103 | CONST s :: BINOP Times :: OFFSET :: LOAD s1 :: _ when s = s1 ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
104 replace 4 [LDI s]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
105 | CONST s :: BINOP Times :: OFFSET :: STORE s1 :: _ when s = s1 ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
106 replace 4 [STI s]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
107
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
108 | CONST 0 :: JUMPC (w, lab) :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
109 replace 2 [JUMPCZ (w, lab)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
110
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
111 | LINE n :: LABEL a :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
112 replace 2 [LABEL a; LINE n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
113 | LINE n :: LINE m :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
114 replace 1 []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
115 | LABEL a :: LABEL b :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
116 equate a b; replace 2 [LABEL a]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
117 | LABEL a :: JUMP b :: _ when not (same_lab a b) ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
118 equate a b; replace 2 [JUMP b]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
119 | JUMPC (w, a) :: JUMP b :: LABEL c :: _ when same_lab a c ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
120 replace 2 [JUMPC (opposite w, b)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
121 | JUMP a :: LABEL b :: _ when same_lab a b ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
122 replace 1 []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
123 | JUMP a :: LABEL b :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
124 ()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
125 | JUMP a :: _ :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
126 replace 2 [JUMP a]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
127 | RETURN s :: LABEL a :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
128 ()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
129 | RETURN s :: _ :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
130 replace 2 [RETURN s]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
131 | LABEL a :: _ when !(ref_count a) = 0 ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
132 replace 1 []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
133
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
134 | _ -> ()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
135
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
136
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
137 (* |optstep| -- apply rules at one place in the buffer *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
138 let optstep rules changed code =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
139 let ch = ref true in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
140 let replace n c =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
141 changed := true; ch := true;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
142 if !debug > 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
143 printf "! $ --> $\n" [fList(fInst) (Util.take n !code); fList(fInst) c];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
144 List.iter (do_refs decr) (Util.take n !code);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
145 List.iter (do_refs incr) c;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
146 code := c @ Util.drop n !code in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
147 while !ch do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
148 ch := false; rules replace !code
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
149 done
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
150
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
151 (* |rewrite| -- iterate over the code and apply rules *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
152 let rewrite rules prog =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
153 let code1 = ref prog and code2 = ref [] in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
154 let changed = ref true in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
155 while !changed do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
156 changed := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
157 while !code1 <> [] do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
158 optstep rules changed code1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
159 if !code1 <> [] then begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
160 code2 := rename_labs (List.hd !code1) :: !code2;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
161 code1 := List.tl !code1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
162 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
163 done;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
164 code1 := List.rev !code2;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
165 code2 := []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
166 done;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
167 !code1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
168
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
169 (* |optimise| -- rewrite list of instructions *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
170 let optimise prog =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
171 match Keiko.canon prog with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
172 SEQ code ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
173 List.iter (do_refs incr) code;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
174 let code2 = rewrite ruleset code in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
175 Hashtbl.clear label_tab;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
176 SEQ code2
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
177 | _ -> failwith "optimise"