1structure IR =
2struct
3
4open HolKernel Parse boolLib wordsTheory pairLib
5     numSyntax
6
7val w32 = Type `:word32`;
8val n2w_tm = Term `n2w:num -> word32`;
9
10fun is_binop op1 =
11  if not (is_comb op1) then false
12  else let val (uncur, oper) = dest_comb op1 in
13       if not (is_const uncur andalso is_const oper) then false
14       else let val (uncur_name, uncur_type) = dest_const uncur;
15                val (oper_name, oper_type) = dest_const oper
16            in
17                if not (uncur_name = "UNCURRY") then false
18                else if oper_name = "+" orelse
19                        oper_name = "-" orelse
20                        oper_name = "*" orelse
21                        oper_name = "/" orelse
22                        oper_name = "&&" orelse
23                        oper_name = "!!" orelse
24                        oper_name = "<<" orelse
25                        oper_name = ">>" orelse
26                        oper_name = ">>#" orelse
27                        oper_name = ">>>" orelse
28                        oper_name = "??" orelse
29            oper_name = "word_or" orelse
30            oper_name = "word_and" orelse
31            oper_name = "word_xor" orelse
32            oper_name = "word_add" orelse
33                        oper_name = "word_sub" orelse
34                        oper_name = "word_mul" orelse
35                        oper_name = "bitwise_and" orelse
36                        oper_name = "bitwise_or" orelse
37                        oper_name = "word_lsl" orelse
38                        oper_name = "word_lsr" orelse
39                        oper_name = "word_asr" orelse
40                        oper_name = "word_ror" orelse
41                        oper_name = "bitwise_eor"
42                        then true
43                else false
44            end
45       end;
46
47fun is_relop op1 =
48  if not (is_comb op1) then false
49  else let val (uncur, oper) = dest_comb op1 in
50       if not (is_const uncur andalso is_const oper) then false
51       else let val (uncur_name, uncur_type) = dest_const uncur;
52                val (oper_name, oper_type) = dest_const oper
53            in
54                if not (uncur_name = "UNCURRY") then false
55                else if oper_name = ">" orelse
56                        oper_name = ">=" orelse
57                        oper_name = "!=" orelse
58                        oper_name = "<" orelse
59                        oper_name = "<=" orelse
60                        oper_name = "=" orelse
61                        oper_name = "word_gt" orelse
62                        oper_name = "word_lt" orelse
63                        oper_name = "word_ge" orelse
64                        oper_name = "word_le" orelse
65                        oper_name = "word_hs" orelse
66                        oper_name = "word_hi" orelse
67                        oper_name = "word_lo" orelse
68                        oper_name = "word_ls"
69                        then true
70                else false
71            end
72       end;
73
74
75fun convert_binop bop =
76  let val (uncur, oper) = dest_comb bop;
77      val (oper_name, oper_type) = dest_const oper
78  in
79      if oper_name = "+" then Tree.PLUS
80      else if oper_name = "-" then Tree.MINUS
81      else if oper_name = "*" then Tree.MUL
82      else if oper_name = "/" then Tree.DIV
83      else if oper_name = "&&" then Tree.AND
84      else if oper_name = "!!" then Tree.OR
85      else if oper_name = "<<" then Tree.LSHIFT
86      else if oper_name = ">>" then Tree.RSHIFT
87      else if oper_name = ">>#" then Tree.ARSHIFT
88      else if oper_name = ">>>" then Tree.ROR
89      else if oper_name = "??" then Tree.XOR
90
91      else if oper_name = "word_and" then Tree.AND
92      else if oper_name = "word_or" then Tree.OR
93      else if oper_name = "word_xor" then Tree.XOR
94      else if oper_name = "word_add" then Tree.PLUS
95      else if oper_name = "word_sub" then Tree.MINUS
96      else if oper_name = "word_mul" then Tree.MUL
97      else if oper_name = "bitwise_and" then Tree.AND
98      else if oper_name = "bitwise_or" then Tree.OR
99      else if oper_name = "word_lsl" then Tree.LSHIFT
100      else if oper_name = "word_lsr" then Tree.RSHIFT
101      else if oper_name = "word_asr" then Tree.ARSHIFT
102      else if oper_name = "word_ror" then Tree.ROR
103      else if oper_name = "bitwise_eor" then Tree.XOR
104
105      else raise ERR "IR" ("invalid bi-operator : " ^ oper_name)
106  end;
107
108fun convert_relop rop =
109  let val (uncur, oper) = dest_comb rop;
110      val (oper_name, oper_type) = dest_const oper
111  in
112      if oper_name = "=" then Tree.EQ
113      else if oper_name = "!=" then Tree.NE
114      else if oper_name = "word_ge" then Tree.GE
115      else if oper_name = "word_gt" then Tree.GT
116      else if oper_name = "word_lt" then Tree.LT
117      else if oper_name = "word_le" then Tree.LE
118      else if oper_name = "word_hs" then Tree.CS
119      else if oper_name = "word_hi" then Tree.HI
120      else if oper_name = "word_lo" then Tree.CC
121      else if oper_name = "word_ls" then Tree.LS
122      else raise ERR "IR" ("invalid relation operator" ^ oper_name)
123  end;
124
125structure H = Polyhash
126structure T = IntMapTable(type key = int  fun getInt n = n);
127
128val tmpT : (string T.table) ref  = ref (T.empty);
129fun getTmp i = T.look(!tmpT,i);
130
131
132exception Symbol
133
134val sizeHint = 128
135val symbolT : ((string,int) H.hash_table) ref =
136                ref (H.mkTable(H.hash, op = ) (sizeHint,Symbol));
137
138 fun inspectVar str  =
139  case H.peek (!symbolT) str of
140     SOME d =>  d
141   | NONE => let
142        val i = T.numItems (!tmpT) in
143            tmpT := T.enter(!tmpT, i, str);
144            H.insert (!symbolT) (str, i);
145            i
146        end
147
148
149 fun flow [] exp = exp
150  |  flow (h::t) exp = Tree.ESEQ(h, flow t exp);
151
152
153fun mk_MOVE e1 (Tree.ESEQ(s1, Tree.ESEQ(s2,e2))) =
154        Tree.SEQ(s1, mk_MOVE e1 (Tree.ESEQ(s2,e2)))
155 |  mk_MOVE e1 (Tree.ESEQ(s1, e2)) =
156        Tree.SEQ(s1, Tree.MOVE (e1,e2))
157 |  mk_MOVE e1 s = Tree.MOVE (e1,s);
158
159
160 fun mk_PAIR (Tree.ESEQ(s1,s2)) = mk_PAIR s2
161  |  mk_PAIR (Tree.PAIR (e1,e2)) =
162        Tree.PAIR(mk_PAIR e1, mk_PAIR e2)
163  |  mk_PAIR exp =
164          Tree.TEMP (inspectVar(Temp.makestring(Temp.newtemp())));
165
166 fun analyzeExp exp =
167
168     if is_let exp then
169        let val (var, rhs) = dest_let exp;
170            val (lhs, rest) = dest_pabs var;
171            val rt = analyzeExp rhs
172        in
173            Tree.ESEQ(Tree.MOVE(analyzeExp lhs, analyzeExp rhs), analyzeExp rest)
174        end
175
176     else if is_numeral exp then
177        Tree.NCONST (Arbint.fromNat (dest_numeral exp))
178
179     else if not (is_comb exp) then
180        if is_var exp then
181            let val (v,ty) = dest_var exp in
182                Tree.TEMP (inspectVar v)
183            end
184        else
185            Tree.NCONST Arbint.zero
186
187     else if is_cond exp then
188        let val (c,t,f) = dest_cond exp;
189            val (t_lab, r_lab) = (Temp.newlabel(), Temp.newlabel());
190            val new_exp = mk_PAIR (analyzeExp t);
191
192            val insts = flow [ Tree.CJUMP(analyzeExp c, t_lab),
193                               mk_MOVE new_exp (analyzeExp f),
194                               Tree.JUMP r_lab,
195                               Tree.LABEL t_lab,
196                               mk_MOVE new_exp (analyzeExp t),
197                               Tree.LABEL r_lab]
198                              new_exp
199        in
200          insts
201        end
202
203     else if is_pair exp then
204        let val (t1,t2) = dest_pair exp
205        in  Tree.PAIR(analyzeExp t1, analyzeExp t2)
206        end
207
208     else if is_comb exp then
209
210        let val (operator, operands) = dest_comb exp in
211
212        if is_relop operator then
213            let val (t1, t2) = dest_pair operands
214            in
215                Tree.RELOP(convert_relop operator, analyzeExp t1, analyzeExp t2)
216            end
217
218        else if is_binop operator then
219            if is_pair operands then                                            (* BINOP of binop * exp * exp   *)
220                  let val (t1, t2) = dest_pair operands in
221                  Tree.BINOP (convert_binop operator, analyzeExp t1, analyzeExp t2)
222                  end
223            else Tree.BINOP (convert_binop operator, analyzeExp operands, analyzeExp operands)    (* UNIOP of uniop * exp  *)
224
225        else if same_const operator n2w_tm then                         (* words                *)
226                Tree.WCONST (Arbint.fromNat (dest_numeral operands))
227        else                                                            (* function call                *)
228            let val (fun_name, fun_type) = dest_const operator in
229                Tree.CALL (Tree.NAME (Temp.namedlabel fun_name),
230                           analyzeExp operands)
231            end
232        end
233
234     else                                                               (*      0       *)
235            raise ERR "buildIR" "the expression is invalid"
236
237
238(*
239fun
240        convert_ESEQ (Tree.ESEQ(Tree.MOVE(e1, e2), Tree.ESEQ(s2,e))) =
241   convert_ESEQ (Tree.ESEQ (Tree.SEQ(
242                Tree.MOVE(e1, convert_ESEQ e2), s2), convert_ESEQ e))
243 |
244        convert_ESEQ (Tree.ESEQ(s1, Tree.ESEQ(s2,e))) =
245        convert_ESEQ (Tree.ESEQ (Tree.SEQ(s1, s2), convert_ESEQ e))
246 |  convert_ESEQ s = s;
247
248convert_ESEQ ir
249
250fun linearize (stm:Tree.stm) : Tree.stm list =
251  let
252    fun linear (Tree.SEQ(a,b),l) = linear (a, linear(b,l))
253     |  linear (s,l) = s::l
254
255    fun discompose_move(Tree.MOVE(Tree.PAIR(e1,e2), Tree.PAIR(e3,e4))) =
256              discompose_move(Tree.MOVE(e1,e3)) @ discompose_move(Tree.MOVE(e2,e4))
257     |   discompose_move exp = [exp]
258     |   discompose_move exp = [exp]
259
260  in
261    List.foldl (fn (exp, L) => L @ discompose_move exp) [] (linear (stm, []))
262  end
263
264*)
265
266fun
267  linerize_IR_stm (Tree.MOVE (e1, Tree.ESEQ (s, e2))) =
268                (linerize_IR_stm s) @ linerize_IR_stm (Tree.MOVE (e1, e2)) |
269  linerize_IR_stm (Tree.SEQ (s1, s2)) = (linerize_IR_stm s1) @ (linerize_IR_stm s2) |
270  linerize_IR_stm (Tree.MOVE(Tree.PAIR(e1,e2), Tree.PAIR(e3,e4))) =
271          linerize_IR_stm (Tree.MOVE(e1,e3)) @ linerize_IR_stm (Tree.MOVE(e2,e4))
272  |
273  linerize_IR_stm stm = [stm]
274
275
276fun linerize_IR (Tree.ESEQ (s, e)) =
277                let
278                        val (stmL, e') = linerize_IR e
279                in
280                        (((linerize_IR_stm s) @ stmL), e')
281                end |
282        linerize_IR e = ([], e)
283
284
285fun convert_to_IR prog =
286   let
287       fun buildArgs args =
288           if is_pair args then
289                let val (arg1,arg2) = dest_pair args
290                in  Tree.PAIR(analyzeExp arg1, analyzeExp arg2) end
291           else analyzeExp args
292
293       val (decl,body) =
294           dest_eq(concl(SPEC_ALL prog))
295           handle HOL_ERR _
296           => (print "not an program in function format\n";
297             raise ERR "buildCFG" "invalid program format");
298       val (f, args) = dest_comb decl;
299       val (f_name, f_type) = dest_const f;
300
301       val _ = (tmpT := T.empty; Polyhash.filter (fn _ => false) (!symbolT));
302
303       val start_lab = Temp.namedlabel (f_name);
304       val ir = linerize_IR (Tree.ESEQ(Tree.LABEL (start_lab), analyzeExp body))
305   in
306       (f_name, f_type, buildArgs args, #1 ir, #2 ir)
307        handle HOL_ERR _
308           => (print "the program body includes invalid expression\n";
309             raise ERR "IR" "invalid expression in program body")
310   end
311
312
313fun print_stm ir =
314  let val indent = "      ";
315      val ((f_name,args,stms,outs):string * Tree.exp * Tree.stm list * Tree.exp) = ir
316
317  fun print_bop Tree.PLUS = "ADD"
318   |  print_bop Tree.MINUS = "SUB"
319   |  print_bop Tree.MUL = "MUL"
320   |  print_bop Tree.DIV = "DIV"
321   |  print_bop Tree.AND = "AND"
322   |  print_bop Tree.OR = "OR"
323   |  print_bop Tree.LSHIFT = "LSL"
324   |  print_bop Tree.RSHIFT = "LSR"
325   |  print_bop Tree.ARSHIFT = "ASR"
326   |  print_bop Tree.XOR = "EOR"
327   |  print_bop Tree.ROR = "ROR"
328
329   fun print_rop Tree.GT = ">"
330   |  print_rop Tree.EQ = "="
331   |  print_rop Tree.LT = "<"
332   |  print_rop Tree.NE = "!="
333   |  print_rop Tree.GE = ">="
334   |  print_rop Tree.LE = "<="
335   |  print_rop Tree.CS = ">=+"
336   |  print_rop Tree.HI = ">+"
337   |  print_rop Tree.CC = "<+"
338   |  print_rop Tree.LS = "<=+"
339   |  print_rop _ = raise ERR "IR" "invalid relational operator";
340
341
342  fun one_exp (Tree.BINOP(bop,e1,e2)) =
343        (print_bop bop) ^ " " ^ one_exp e1 ^ ", " ^ one_exp e2
344   |  one_exp (Tree.RELOP(rop, e1,e2)) =
345        (one_exp e1) ^ " " ^ (print_rop rop) ^ " " ^ one_exp e2
346   |  one_exp (Tree.MEM e) =
347        "MEM[" ^ one_exp e ^ "]"
348   |  one_exp (Tree.TEMP e) =
349        getTmp e
350   |  one_exp (Tree.NAME e) =
351        Symbol.name e
352   |  one_exp (Tree.NCONST e) =
353        Arbint.toString e
354   |  one_exp (Tree.WCONST e) =
355        (Arbint.toString e) ^ "w"
356   |  one_exp (Tree.CALL(f, args)) =
357        "CALL " ^ (one_exp f)
358   |  one_exp (Tree.PAIR(e1,e2)) =
359        "(" ^ one_exp e1 ^ "," ^ one_exp e2 ^ ")"
360   |  one_exp _ =
361        ""
362   ;
363
364  fun one_stm (Tree.MOVE(v1,v2)) =
365        indent ^ "MOV " ^ (one_exp v1) ^ ", " ^ (one_exp v2)
366   |  one_stm (Tree.LABEL lab) =
367        (Symbol.name lab) ^ ":"
368   |  one_stm (Tree.JUMP lab) =
369        indent ^ "JMP " ^ Symbol.name lab
370   |  one_stm (Tree.CJUMP(c,lab)) =
371        indent ^ "JNE " ^ Symbol.name lab
372   |  one_stm (Tree.EXP exp) =
373        one_exp exp
374   |  one_stm _ =
375        ""
376  in
377
378    List.map (fn stm => print(one_stm stm ^ "\n")) stms
379  end
380
381end
382