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