annotate lab1/peepopt.ml @ 1:b5139af1a420 tip basis

Fixed permissions on compile scripts
author Mike Spivey <mike@cs.ox.ac.uk>
date Fri, 13 Oct 2017 17:27:58 +0100
parents bfdcc3820b32
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 | CASEARM (n, x) -> f (ref_count x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
57 | _ -> ()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
58
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
59 (* |rename_labs| -- replace each label by its equivalent *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
60 let rename_labs =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
61 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
62 LABEL x -> LABEL (rename x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
63 | JUMP x -> JUMP (rename x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
64 | JUMPC (w, x) -> JUMPC (w, rename x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
65 | CASEARM (n, x) -> CASEARM (n, rename x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
66 | i -> i
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
67
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
68 let opposite =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
69 function Eq -> Neq | Neq -> Eq | Lt -> Geq
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
70 | Leq -> Gt | Gt -> Leq | Geq -> Lt
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
71 | _ -> failwith "opposite"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
72
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
73 (* |ruleset| -- simplify and introduce abbreviations *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
74 let ruleset replace =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
75 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
76 LOCAL a :: CONST b :: OFFSET :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
77 replace 3 [LOCAL (a+b)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
78 | CONST a :: OFFSET :: CONST b :: OFFSET :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
79 replace 4 [CONST (a+b); OFFSET]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
80 | CONST 0 :: OFFSET :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
81 replace 2 []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
82
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
83 | GLOBAL x :: LOADW :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
84 replace 2 [LDGW x]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
85 | GLOBAL x :: STOREW :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
86 replace 2 [STGW x]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
87 | LOCAL n :: LOADW :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
88 replace 2 [LDLW n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
89 | LOCAL n :: STOREW :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
90 replace 2 [STLW n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
91 | CONST n :: OFFSET :: LOADW :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
92 replace 3 [LDNW n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
93 | CONST n :: OFFSET :: STOREW :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
94 replace 3 [STNW n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
95
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
96 | CONST x :: CONST n :: BOUND _ :: _ when x >= 0 && x < n ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
97 replace 3 [CONST x]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
98
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
99 | LINE n :: LABEL a :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
100 replace 2 [LABEL a; LINE n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
101 | LINE n :: LINE m :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
102 replace 1 []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
103 | LABEL a :: LABEL b :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
104 equate a b; replace 2 [LABEL a]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
105 | LABEL a :: JUMP b :: _ when not (same_lab a b) ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
106 equate a b; replace 2 [JUMP b]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
107 | JUMPC (w, a) :: JUMP b :: LABEL c :: _ when same_lab a c ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
108 replace 2 [JUMPC (opposite w, b)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
109 | JUMP a :: LABEL b :: _ when same_lab a b ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
110 replace 1 []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
111 | JUMP a :: LABEL b :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
112 ()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
113 | JUMP a :: _ :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
114 replace 2 [JUMP a]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
115 | LABEL a :: _ when !(ref_count a) = 0 ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
116 replace 1 []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
117
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
118 | _ -> ()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
119
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
120 (* |take n [x1; x2; ...] = [x1; x2; ...; xn]| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
121 let rec take n =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
122 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
123 [] -> []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
124 | x::xs -> if n = 0 then [] else x :: take (n-1) xs
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
125
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
126 (* |drop n [x1; x2; ...] = [x_{n+1}; x_{n+2}; ...]| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
127 let rec drop n =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
128 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
129 [] -> []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
130 | x::xs -> if n = 0 then x::xs else drop (n-1) xs
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
131
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
132 (* |optstep| -- apply rules at one place in the buffer *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
133 let optstep rules changed code =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
134 let ch = ref true in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
135 let replace n c =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
136 changed := true; ch := true;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
137 if !debug > 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
138 printf "! $ --> $\n" [fList(fInst) (take n !code); fList(fInst) c];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
139 List.iter (do_refs decr) (take n !code);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
140 List.iter (do_refs incr) c;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
141 code := c @ drop n !code in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
142 while !ch do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
143 ch := false; rules replace !code
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
144 done
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
145
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
146 (* |rewrite| -- iterate over the code and apply rules *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
147 let rewrite rules prog =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
148 let code1 = ref prog and code2 = ref [] in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
149 let changed = ref true in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
150 while !changed do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
151 changed := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
152 while !code1 <> [] do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
153 optstep rules changed code1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
154 if !code1 <> [] then begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
155 code2 := rename_labs (List.hd !code1) :: !code2;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
156 code1 := List.tl !code1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
157 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
158 done;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
159 code1 := List.rev !code2;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
160 code2 := []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
161 done;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
162 !code1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
163
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
164 (* |optimise| -- rewrite list of instructions *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
165 let optimise prog =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
166 match Keiko.canon prog with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
167 SEQ code ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
168 List.iter (do_refs incr) code;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
169 let code2 = rewrite ruleset code in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
170 Hashtbl.clear label_tab;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
171 SEQ code2
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
172 | _ -> failwith "optimise"