annotate lab4/jumpopt.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 (* lab4/jumpopt.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 Optree
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
5
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
6 (* Disjoint sets of labels *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
7
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
8 type labdata =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
9 LabDef of labrec (* An extant label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
10 | Equiv of codelab (* A label that's been merged *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
11
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
12 and labrec =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
13 { y_id : codelab; (* Name of the label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
14 y_refct : int ref } (* Reference count *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
15
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
16 let label_tab = Hashtbl.create 257
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
17
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
18 (* |get_label| -- find or create a label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
19 let get_label x =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
20 try Hashtbl.find label_tab x with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
21 Not_found ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
22 let y = LabDef { y_id = x; y_refct = ref 0 } in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
23 Hashtbl.add label_tab x y; y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
24
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
25 (* |find_label| -- find equivalent of a label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
26 let rec find_label x =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
27 match get_label x with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
28 LabDef y -> y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
29 | Equiv x' -> find_label x'
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
30
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
31 let rename x = let y = find_label x in y.y_id
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
32
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
33 let ref_count x = let y = find_label x in y.y_refct
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
34
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
35 (* same_lab -- test if two labels are equal *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
36 let same_lab x1 x2 =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
37 let y1 = find_label x1 and y2 = find_label x2 in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
38 y1.y_id = y2.y_id
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
39
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
40 (* equate -- make two labels equal *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
41 let equate x1 x2 =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
42 let y1 = find_label x1 and y2 = find_label x2 in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
43 if y1.y_id = y2.y_id then failwith "equate";
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
44 y2.y_refct := !(y1.y_refct) + !(y2.y_refct);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
45 Hashtbl.add label_tab y1.y_id (Equiv y2.y_id)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
46
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
47 (* do_refs -- call function on each label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
48 let do_refs f =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
49 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
50 <JUMP x> -> f (ref_count x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
51 | <JUMPC (w, x), _, _> -> f (ref_count x)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
52 | <JCASE (labs, def), _> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
53 List.iter (fun x -> f (ref_count x)) labs;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
54 f (ref_count def)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
55 | _ -> ()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
56
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
57 (* rename_labs -- replace each label by its equivalent *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
58 let rename_labs =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
59 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
60 <LABEL x> -> <LABEL (rename x)>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
61 | <JUMP x> -> <JUMP (rename x)>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
62 | <JUMPC (w, x), t1, t2> -> <JUMPC (w, rename x), t1, t2>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
63 | <JCASE (labs, def), t1> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
64 <JCASE (List.map rename labs, rename def), t1>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
65 | t -> t
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
66
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
67 (* optstep -- optimise to fixpoint at current location *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
68 let optstep changed code =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
69 let ch = ref true in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
70
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
71 let replace n inserted =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
72 changed := true; ch := true;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
73 let deleted = Util.take n !code in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
74 List.iter (do_refs decr) deleted;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
75 List.iter (do_refs incr) inserted;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
76 code := inserted @ Util.drop n !code in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
77
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
78 let delete n = replace (n+1) (Util.take n !code) in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
79
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
80 while !ch do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
81 ch := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
82 match !code with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
83 <JUMP lab1> :: <LABEL lab2> :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
84 (* Remove a jump to the next instruction *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
85 if same_lab lab1 lab2 then delete 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
86 | <JUMP lab1> :: <LINE n> :: <LABEL lab2> :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
87 (* Keep a potentially useful line number *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
88 replace 3 [<JUMP lab1>; <LABEL lab2>; <LINE n>]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
89 | <JUMP lab> :: _ :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
90 (* Eliminate dead code *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
91 delete 1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
92 | <JUMPC (w, lab1), t1, t2> :: <JUMP lab2> :: <LABEL lab3> :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
93 (* Simplify a jump over a jump *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
94 if same_lab lab1 lab3 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
95 replace 2 [<JUMPC (negate w, lab2), t1, t2>]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
96 | <LABEL lab1> :: <JUMP lab2> :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
97 (* One jump leads to another *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
98 if not (same_lab lab1 lab2) then begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
99 delete 0; equate lab1 lab2
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
100 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
101 | <LABEL lab1> :: <LABEL lab2> :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
102 (* Merge identical labels *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
103 delete 0; equate lab1 lab2
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
104 | <LABEL lab> :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
105 (* Delete unused labels *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
106 if !(ref_count lab) = 0 then delete 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
107
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
108 (* Tidy up line numbers *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
109 | <LINE m> :: <LINE n> :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
110 delete 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
111 | <LINE n> :: <LABEL lab> :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
112 replace 2 [<LABEL lab>; <LINE n>]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
113 | <LINE n> :: <JUMP lab> :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
114 replace 2 [<JUMP lab>; <LINE n>]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
115 | <LINE n> :: [] ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
116 delete 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
117 | <NOP> :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
118 delete 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
119
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
120 | _ -> ()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
121 done
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
122
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
123 let optimise prog =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
124 Hashtbl.clear label_tab;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
125 let init = prog in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
126 List.iter (do_refs incr) init;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
127 let buf1 = ref init and buf2 = ref [] in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
128 let changed = ref true in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
129 while !changed do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
130 changed := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
131 while !buf1 <> [] do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
132 optstep changed buf1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
133 if !buf1 <> [] then begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
134 buf2 := List.hd !buf1 :: !buf2;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
135 buf1 := List.tl !buf1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
136 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
137 done;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
138 buf1 := List.rev !buf2;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
139 buf2 := []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
140 done;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
141 List.map rename_labs !buf1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
142