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 (lt, rhs) = dest_let exp;
170            val (lhs, rest) = dest_pabs lt;
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 convert_ESEQ (Tree.ESEQ(s1, Tree.ESEQ(s2,e))) =
240        convert_ESEQ (Tree.ESEQ (Tree.SEQ(s1, s2), e))
241 |  convert_ESEQ s = s;
242
243
244fun linearize (stm:Tree.stm) : Tree.stm list =
245  let
246    fun linear (Tree.SEQ(a,b),l) = linear (a, linear(b,l))
247     |  linear (s,l) = s::l
248
249    fun discompose_move(Tree.MOVE(Tree.PAIR(e1,e2), Tree.PAIR(e3,e4))) =
250        discompose_move(Tree.MOVE(e1,e3)) @ discompose_move(Tree.MOVE(e2,e4))
251     |   discompose_move exp = [exp]
252
253  in
254    List.foldl (fn (exp, L) => L @ discompose_move exp) [] (linear (stm, []))
255  end
256
257
258fun linerize_IR ir =
259  let
260    fun get_stm (Tree.ESEQ(s,e)) = s
261    fun get_exp (Tree.ESEQ(s,e)) = e
262    val ir = convert_ESEQ ir
263  in
264    (linearize (get_stm ir), get_exp ir)
265  end
266
267
268fun convert_to_IR prog =
269   let
270       fun buildArgs args =
271           if is_pair args then
272                let val (arg1,arg2) = dest_pair args
273                in  Tree.PAIR(analyzeExp arg1, analyzeExp arg2) end
274           else analyzeExp args
275
276       val (decl,body) =
277           dest_eq(concl(SPEC_ALL prog))
278           handle HOL_ERR _
279           => (print "not an program in function format\n";
280             raise ERR "buildCFG" "invalid program format");
281       val (f, args) = dest_comb decl;
282       val (f_name, f_type) = dest_const f;
283
284       val _ = (tmpT := T.empty; Polyhash.filter (fn _ => false) (!symbolT));
285
286       val start_lab = Temp.namedlabel (f_name);
287       val ir = linerize_IR (Tree.ESEQ(Tree.LABEL (start_lab), analyzeExp body))
288   in
289       (f_name, f_type, buildArgs args, #1 ir, #2 ir)
290        handle HOL_ERR _
291           => (print "the program body includes invalid expression\n";
292             raise ERR "IR" "invalid expression in program body")
293   end
294
295
296fun print_stm ir =
297  let val indent = "      ";
298      val ((f_name,args,stms,outs):string * Tree.exp * Tree.stm list * Tree.exp) = ir
299
300  fun print_bop Tree.PLUS = "ADD"
301   |  print_bop Tree.MINUS = "SUB"
302   |  print_bop Tree.MUL = "MUL"
303   |  print_bop Tree.DIV = "DIV"
304   |  print_bop Tree.AND = "AND"
305   |  print_bop Tree.OR = "OR"
306   |  print_bop Tree.LSHIFT = "LSL"
307   |  print_bop Tree.RSHIFT = "LSR"
308   |  print_bop Tree.ARSHIFT = "ASR"
309   |  print_bop Tree.XOR = "EOR"
310   |  print_bop Tree.ROR = "ROR"
311
312   fun print_rop Tree.GT = ">"
313   |  print_rop Tree.EQ = "="
314   |  print_rop Tree.LT = "<"
315   |  print_rop Tree.NE = "!="
316   |  print_rop Tree.GE = ">="
317   |  print_rop Tree.LE = "<="
318   |  print_rop Tree.CS = ">=+"
319   |  print_rop Tree.HI = ">+"
320   |  print_rop Tree.CC = "<+"
321   |  print_rop Tree.LS = "<=+"
322   |  print_rop _ = raise ERR "IR" "invalid relational operator";
323
324
325  fun one_exp (Tree.BINOP(bop,e1,e2)) =
326        (print_bop bop) ^ " " ^ one_exp e1 ^ ", " ^ one_exp e2
327   |  one_exp (Tree.RELOP(rop, e1,e2)) =
328        (one_exp e1) ^ " " ^ (print_rop rop) ^ " " ^ one_exp e2
329   |  one_exp (Tree.MEM e) =
330        "MEM[" ^ one_exp e ^ "]"
331   |  one_exp (Tree.TEMP e) =
332        getTmp e
333   |  one_exp (Tree.NAME e) =
334        Symbol.name e
335   |  one_exp (Tree.NCONST e) =
336        Arbint.toString e
337   |  one_exp (Tree.WCONST e) =
338        (Arbint.toString e) ^ "w"
339   |  one_exp (Tree.CALL(f, args)) =
340        "CALL " ^ (one_exp f)
341   |  one_exp (Tree.PAIR(e1,e2)) =
342        "(" ^ one_exp e1 ^ "," ^ one_exp e2 ^ ")"
343   |  one_exp _ =
344        ""
345   ;
346
347  fun one_stm (Tree.MOVE(v1,v2)) =
348        indent ^ "MOV " ^ (one_exp v1) ^ ", " ^ (one_exp v2)
349   |  one_stm (Tree.LABEL lab) =
350        (Symbol.name lab) ^ ":"
351   |  one_stm (Tree.JUMP lab) =
352        indent ^ "JMP " ^ Symbol.name lab
353   |  one_stm (Tree.CJUMP(c,lab)) =
354        indent ^ "JNE " ^ Symbol.name lab
355   |  one_stm (Tree.EXP exp) =
356        one_exp exp
357   |  one_stm _ =
358        ""
359  in
360
361    List.map (fn stm => print(one_stm stm ^ "\n")) stms
362  end
363
364end
365