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 10exception undeclFuncIR; 11 12val sizeHint = 128; 13val hashtable : ((string, (Tree.stm list * Tree.exp * Tree.exp)) Polyhash.hash_table) ref = 14 ref (Polyhash.mkTable(Polyhash.hash, op = ) (sizeHint, undeclFuncIR)) 15 16val inline_funcs = (ref []) : string list ref 17 18fun is_binop op1 = 19 if not (is_comb op1) then false 20 else let val (uncur, oper) = dest_comb op1 in 21 if not (is_const uncur andalso is_const oper) then false 22 else let val (uncur_name, uncur_type) = dest_const uncur; 23 val (oper_name, oper_type) = dest_const oper 24 in 25 if not (uncur_name = "UNCURRY") then false 26 else if oper_name = "+" orelse 27 oper_name = "-" orelse 28 oper_name = "*" orelse 29 oper_name = "/" orelse 30 oper_name = "&&" orelse 31 oper_name = "!!" orelse 32 oper_name = "<<" orelse 33 oper_name = ">>" orelse 34 oper_name = ">>#" orelse 35 oper_name = ">>>" orelse 36 oper_name = "??" orelse 37 oper_name = "word_or" orelse 38 oper_name = "word_and" orelse 39 oper_name = "word_xor" orelse 40 oper_name = "word_add" orelse 41 oper_name = "word_sub" orelse 42 oper_name = "word_mul" orelse 43 oper_name = "bitwise_and" orelse 44 oper_name = "bitwise_or" orelse 45 oper_name = "word_lsl" orelse 46 oper_name = "word_lsr" orelse 47 oper_name = "word_asr" orelse 48 oper_name = "word_ror" orelse 49 oper_name = "bitwise_eor" 50 then true 51 else false 52 end 53 end; 54 55fun is_relop op1 = 56 if not (is_comb op1) then false 57 else let val (uncur, oper) = dest_comb op1 in 58 if not (is_const uncur andalso is_const oper) then false 59 else let val (uncur_name, uncur_type) = dest_const uncur; 60 val (oper_name, oper_type) = dest_const oper 61 in 62 if not (uncur_name = "UNCURRY") then false 63 else if oper_name = ">" orelse 64 oper_name = ">=" orelse 65 oper_name = "!=" orelse 66 oper_name = "<" orelse 67 oper_name = "<=" orelse 68 oper_name = "=" orelse 69 oper_name = "word_gt" orelse 70 oper_name = "word_lt" orelse 71 oper_name = "word_ge" orelse 72 oper_name = "word_le" orelse 73 oper_name = "word_hs" orelse 74 oper_name = "word_hi" orelse 75 oper_name = "word_lo" orelse 76 oper_name = "word_ls" 77 then true 78 else false 79 end 80 end; 81 82 83fun convert_binop bop = 84 let val (uncur, oper) = dest_comb bop; 85 val (oper_name, oper_type) = dest_const oper 86 in 87 if oper_name = "+" then Tree.PLUS 88 else if oper_name = "-" then Tree.MINUS 89 else if oper_name = "*" then Tree.MUL 90 else if oper_name = "/" then Tree.DIV 91 else if oper_name = "&&" then Tree.AND 92 else if oper_name = "!!" then Tree.OR 93 else if oper_name = "<<" then Tree.LSHIFT 94 else if oper_name = ">>" then Tree.RSHIFT 95 else if oper_name = ">>#" then Tree.ARSHIFT 96 else if oper_name = ">>>" then Tree.ROR 97 else if oper_name = "??" then Tree.XOR 98 99 else if oper_name = "word_and" then Tree.AND 100 else if oper_name = "word_or" then Tree.OR 101 else if oper_name = "word_xor" then Tree.XOR 102 else if oper_name = "word_add" then Tree.PLUS 103 else if oper_name = "word_sub" then Tree.MINUS 104 else if oper_name = "word_mul" then Tree.MUL 105 else if oper_name = "bitwise_and" then Tree.AND 106 else if oper_name = "bitwise_or" then Tree.OR 107 else if oper_name = "word_lsl" then Tree.LSHIFT 108 else if oper_name = "word_lsr" then Tree.RSHIFT 109 else if oper_name = "word_asr" then Tree.ARSHIFT 110 else if oper_name = "word_ror" then Tree.ROR 111 else if oper_name = "bitwise_eor" then Tree.XOR 112 113 else raise ERR "IR" ("invalid bi-operator : " ^ oper_name) 114 end; 115 116fun convert_relop rop = 117 let val (uncur, oper) = dest_comb rop; 118 val (oper_name, oper_type) = dest_const oper 119 in 120 if oper_name = "=" then Tree.EQ 121 else if oper_name = "!=" then Tree.NE 122 else if oper_name = "word_ge" then Tree.GE 123 else if oper_name = "word_gt" then Tree.GT 124 else if oper_name = "word_lt" then Tree.LT 125 else if oper_name = "word_le" then Tree.LE 126 else if oper_name = "word_hs" then Tree.CS 127 else if oper_name = "word_hi" then Tree.HI 128 else if oper_name = "word_lo" then Tree.CC 129 else if oper_name = "word_ls" then Tree.LS 130 else raise ERR "IR" ("invalid relation operator" ^ oper_name) 131 end; 132 133structure H = Polyhash 134structure T = IntMapTable(type key = int fun getInt n = n); 135 136 137val tmpT : (string T.table) ref = ref (T.empty); 138fun getTmp i = T.look(!tmpT,i); 139 140 141exception Symbol 142 143val sizeHint = 128 144val symbolT : ((string,int) H.hash_table) ref = 145 ref (H.mkTable(H.hash, op = ) (sizeHint,Symbol)); 146 147 fun inspectVar str = 148 case H.peek (!symbolT) str of 149 SOME d => d 150 | NONE => let 151 val i = T.numItems (!tmpT) in 152 tmpT := T.enter(!tmpT, i, str); 153 H.insert (!symbolT) (str, i); 154 i 155 end 156 157 158 fun flow [] exp = exp 159 | flow (h::t) exp = Tree.ESEQ(h, flow t exp); 160 161 162fun mk_MOVE e1 (Tree.ESEQ(s1, Tree.ESEQ(s2,e2))) = 163 Tree.SEQ(s1, mk_MOVE e1 (Tree.ESEQ(s2,e2))) 164 | mk_MOVE e1 (Tree.ESEQ(s1, e2)) = 165 Tree.SEQ(s1, Tree.MOVE (e1,e2)) 166 | mk_MOVE e1 s = Tree.MOVE (e1,s); 167 168 169 fun mk_PAIR (Tree.ESEQ(s1,s2)) = mk_PAIR s2 170 | mk_PAIR (Tree.PAIR (e1,e2)) = 171 Tree.PAIR(mk_PAIR e1, mk_PAIR e2) 172 | mk_PAIR exp = 173 Tree.TEMP (inspectVar(Temp.makestring(Temp.newtemp()))); 174 175 fun analyzeExp exp = 176 177 if is_let exp then 178 let val (var, rhs) = dest_let exp; 179 val (lhs, rest) = dest_pabs var; 180 val rt = analyzeExp rhs 181 in 182 Tree.ESEQ(Tree.MOVE(analyzeExp lhs, analyzeExp rhs), analyzeExp rest) 183 end 184 185 else if is_numeral exp then 186 Tree.NCONST (Arbint.fromNat (dest_numeral exp)) 187 188 else if not (is_comb exp) then 189 if is_var exp then 190 let val (v,ty) = dest_var exp in 191 Tree.TEMP (inspectVar v) 192 end 193 else 194 Tree.NCONST Arbint.zero 195 196 else if is_cond exp then 197 let val (c,t,f) = dest_cond exp; 198 val (t_lab, r_lab) = (Temp.newlabel(), Temp.newlabel()); 199 val new_exp = mk_PAIR (analyzeExp t); 200 201 val insts = flow [ Tree.CJUMP(analyzeExp c, t_lab), 202 mk_MOVE new_exp (analyzeExp f), 203 Tree.JUMP r_lab, 204 Tree.LABEL t_lab, 205 mk_MOVE new_exp (analyzeExp t), 206 Tree.LABEL r_lab] 207 new_exp 208 in 209 insts 210 end 211 else if is_pair exp then 212 let val (t1,t2) = dest_pair exp 213 in Tree.PAIR(analyzeExp t1, analyzeExp t2) 214 end 215 216 else if is_comb exp then 217 218 let val (operator, operands) = dest_comb exp in 219 220 if is_relop operator then 221 let val (t1, t2) = dest_pair operands 222 in 223 Tree.RELOP(convert_relop operator, analyzeExp t1, analyzeExp t2) 224 end 225 226 else if is_binop operator then 227 if is_pair operands then (* BINOP of binop * exp * exp *) 228 let val (t1, t2) = dest_pair operands in 229 Tree.BINOP (convert_binop operator, analyzeExp t1, analyzeExp t2) 230 end 231 else Tree.BINOP (convert_binop operator, analyzeExp operands, analyzeExp operands) (* UNIOP of uniop * exp *) 232 233 else if same_const operator n2w_tm then (* words *) 234 Tree.WCONST (Arbint.fromNat (dest_numeral operands)) 235 else (* function call *) 236 let val (fun_name, fun_type) = dest_const operator in 237 Tree.CALL (Tree.NAME (Temp.namedlabel fun_name), 238 analyzeExp operands) 239 end 240 end 241 242 else (* 0 *) 243 raise ERR "buildIR" "the expression is invalid" 244 245 246(* 247fun 248 convert_ESEQ (Tree.ESEQ(Tree.MOVE(e1, e2), Tree.ESEQ(s2,e))) = 249 convert_ESEQ (Tree.ESEQ (Tree.SEQ( 250 Tree.MOVE(e1, convert_ESEQ e2), s2), convert_ESEQ e)) 251 | 252 convert_ESEQ (Tree.ESEQ(s1, Tree.ESEQ(s2,e))) = 253 convert_ESEQ (Tree.ESEQ (Tree.SEQ(s1, s2), convert_ESEQ e)) 254 | convert_ESEQ s = s; 255 256convert_ESEQ ir 257 258fun linearize (stm:Tree.stm) : Tree.stm list = 259 let 260 fun linear (Tree.SEQ(a,b),l) = linear (a, linear(b,l)) 261 | linear (s,l) = s::l 262 263 fun discompose_move(Tree.MOVE(Tree.PAIR(e1,e2), Tree.PAIR(e3,e4))) = 264 discompose_move(Tree.MOVE(e1,e3)) @ discompose_move(Tree.MOVE(e2,e4)) 265 | discompose_move exp = [exp] 266 | discompose_move exp = [exp] 267 268 in 269 List.foldl (fn (exp, L) => L @ discompose_move exp) [] (linear (stm, [])) 270 end 271 272*) 273 274val nextFreeTemp = ref 0 275 276 277fun rename_temp_stm (Tree.SEQ (s1, s2)) offset = 278 let 279 val (s1', m1) = rename_temp_stm s1 offset; 280 val (s2', m2) = rename_temp_stm s2 offset; 281 in 282 (Tree.SEQ (s1', s2'), Int.max (m1, m2)) 283 end 284 | rename_temp_stm (Tree.CJUMP (e, l)) offset = 285 let 286 val (e', m) = rename_temp_exp e offset; 287 in 288 (Tree.CJUMP(e', l), m) 289 end 290 | rename_temp_stm (Tree.MOVE (e1, e2)) offset = 291 let 292 val (e1', m1) = rename_temp_exp e1 offset; 293 val (e2', m2) = rename_temp_exp e2 offset; 294 in 295 (Tree.MOVE (e1', e2'), Int.max (m1, m2)) 296 end 297 | rename_temp_stm (Tree.EXP e) offset = 298 let 299 val (e', m) = rename_temp_exp e offset; 300 in 301 (Tree.EXP e', m) 302 end 303 | rename_temp_stm X offset = 304 (X, 0) 305and 306 rename_temp_exp (Tree.BINOP (binop, e1, e2)) offset = 307 let 308 val (e1', m1) = rename_temp_exp e1 offset; 309 val (e2', m2) = rename_temp_exp e2 offset; 310 in 311 (Tree.BINOP (binop, e1', e2'), Int.max (m1, m2)) 312 end 313 | rename_temp_exp (Tree.MEM e) offset = 314 let 315 val (e', m) = rename_temp_exp e offset; 316 in 317 (Tree.MEM e', m) 318 end 319 | rename_temp_exp (Tree.TEMP t) offset = 320 let 321 val new_t = t + offset; 322 val var_name = "v"^(Int.toString (new_t +1)) 323 val _ = tmpT := T.enter(!tmpT, new_t, var_name); 324 in 325 (Tree.TEMP new_t, t) 326 end 327 328 329 | rename_temp_exp (Tree.RELOP (relop, e1, e2)) offset = 330 let 331 val (e1', m1) = rename_temp_exp e1 offset; 332 val (e2', m2) = rename_temp_exp e2 offset; 333 in 334 (Tree.RELOP (relop, e1', e2'), Int.max (m1, m2)) 335 end 336 | rename_temp_exp (Tree.ESEQ (s, e)) offset = 337 let 338 val (s', m1) = rename_temp_stm s offset; 339 val (e', m2) = rename_temp_exp e offset; 340 in 341 (Tree.ESEQ (s', e'), Int.max (m1, m2)) 342 end 343 | rename_temp_exp (Tree.CALL (e1, e2)) offset = 344 let 345 val (e1', m1) = rename_temp_exp e1 offset; 346 val (e2', m2) = rename_temp_exp e2 offset; 347 in 348 (Tree.CALL (e1', e2'), Int.max (m1, m2)) 349 end 350 | rename_temp_exp (Tree.PAIR (e1, e2)) offset = 351 let 352 val (e1', m1) = rename_temp_exp e1 offset; 353 val (e2', m2) = rename_temp_exp e2 offset; 354 in 355 (Tree.PAIR (e1', e2'), Int.max (m1, m2)) 356 end 357 | rename_temp_exp X offset = (X, 0); 358 359 360 361fun 362 linerize_IR_stm (Tree.MOVE (e1, Tree.ESEQ (s, e2))) = 363 (linerize_IR_stm s) @ linerize_IR_stm (Tree.MOVE (e1, e2)) | 364 linerize_IR_stm (Tree.SEQ (s1, s2)) = (linerize_IR_stm s1) @ (linerize_IR_stm s2) | 365 linerize_IR_stm (Tree.MOVE(Tree.PAIR(e1,e2), Tree.PAIR(e3,e4))) = 366 linerize_IR_stm (Tree.MOVE(e1,e3)) @ linerize_IR_stm (Tree.MOVE(e2,e4)) 367 | 368 linerize_IR_stm (Tree.MOVE (e1, Tree.CALL (Tree.NAME s, e2))) = 369 if (mem (Symbol.name s) (!inline_funcs)) then 370 let 371 val fun_name = (Symbol.name s); 372 val (fun_ir, fun_in, fun_out) = Polyhash.find (!hashtable) fun_name 373 val offset = !nextFreeTemp; 374 val fun_ir' = map (fn stm => rename_temp_stm stm offset) fun_ir; 375 val max = foldl (fn ((x, n1), n2) => Int.max (n1,n2)) 0 fun_ir'; 376 val fun_ir'' = map fst fun_ir' 377 val (fun_in'', max_in) = rename_temp_exp fun_in offset; 378 val max = Int.max (max, max_in); 379 val (fun_out'', max_out) = rename_temp_exp fun_out offset; 380 val max = Int.max (max, max_out); 381 val _ = nextFreeTemp := !nextFreeTemp + max 382 in 383 (linerize_IR_stm (Tree.MOVE (fun_in'', e2)))@fun_ir''@(linerize_IR_stm (Tree.MOVE (e1, fun_out''))) 384 end 385 else [Tree.MOVE (e1, Tree.CALL (Tree.NAME s, e2))] 386 | 387 linerize_IR_stm stm = [stm] 388 389 390fun linerize_IR (Tree.ESEQ (s, e)) = 391 let 392 val (stmL, e') = linerize_IR e 393 in 394 (((linerize_IR_stm s) @ stmL), e') 395 end 396 | linerize_IR (Tree.CALL (Tree.NAME s, e)) = 397 let 398 val exp = (Tree.CALL (Tree.NAME s, e)); 399 val temp_exp = mk_PAIR exp; 400 val new_exp = Tree.ESEQ (Tree.MOVE (temp_exp, exp), temp_exp); 401 in 402 linerize_IR (new_exp) 403 end 404 | linerize_IR e = ([], e) 405 406fun convert_to_IR prog = 407 let 408 fun buildArgs args = 409 if is_pair args then 410 let val (arg1,arg2) = dest_pair args 411 in Tree.PAIR(analyzeExp arg1, analyzeExp arg2) end 412 else analyzeExp args 413 414 val (decl,body) = 415 dest_eq(concl(SPEC_ALL prog)) 416 handle HOL_ERR _ 417 => (print "not an program in function format\n"; 418 raise ERR "buildCFG" "invalid program format"); 419 val (f, args) = dest_comb decl; 420 val (f_name, f_type) = dest_const f; 421 422 val _ = (tmpT := T.empty; Polyhash.filter (fn _ => false) (!symbolT)); 423 424 val start_lab = Temp.namedlabel (f_name); 425 val end_lab = Temp.namedlabel ("end___"^f_name); 426 val body_exp = analyzeExp body; (*updates tempT*) 427 428 val ir = linerize_IR (Tree.ESEQ(Tree.LABEL (start_lab), body_exp)); 429 val ir_stmL = (#1 ir)@[Tree.LABEL (end_lab)]; 430 val ir_exp = #2 ir 431 val args_exp = buildArgs args; 432 val _ = Polyhash.insert (!hashtable) (f_name, (ir_stmL, args_exp, ir_exp)) 433 in 434 (f_name, f_type, args_exp, ir_stmL, ir_exp) 435 handle HOL_ERR _ 436 => (print "the program body includes invalid expression\n"; 437 raise ERR "IR" "invalid expression in program body") 438 end 439 440 441fun print_stm ir = 442 let val indent = " "; 443 val ((f_name,args,stms,outs):string * Tree.exp * Tree.stm list * Tree.exp) = ir 444 445 fun print_bop Tree.PLUS = "ADD" 446 | print_bop Tree.MINUS = "SUB" 447 | print_bop Tree.MUL = "MUL" 448 | print_bop Tree.DIV = "DIV" 449 | print_bop Tree.AND = "AND" 450 | print_bop Tree.OR = "OR" 451 | print_bop Tree.LSHIFT = "LSL" 452 | print_bop Tree.RSHIFT = "LSR" 453 | print_bop Tree.ARSHIFT = "ASR" 454 | print_bop Tree.XOR = "EOR" 455 | print_bop Tree.ROR = "ROR" 456 457 fun print_rop Tree.GT = ">" 458 | print_rop Tree.EQ = "=" 459 | print_rop Tree.LT = "<" 460 | print_rop Tree.NE = "!=" 461 | print_rop Tree.GE = ">=" 462 | print_rop Tree.LE = "<=" 463 | print_rop Tree.CS = ">=+" 464 | print_rop Tree.HI = ">+" 465 | print_rop Tree.CC = "<+" 466 | print_rop Tree.LS = "<=+" 467 | print_rop _ = raise ERR "IR" "invalid relational operator"; 468 469 470 fun one_exp (Tree.BINOP(bop,e1,e2)) = 471 (print_bop bop) ^ " " ^ one_exp e1 ^ ", " ^ one_exp e2 472 | one_exp (Tree.RELOP(rop, e1,e2)) = 473 (one_exp e1) ^ " " ^ (print_rop rop) ^ " " ^ one_exp e2 474 | one_exp (Tree.MEM e) = 475 "MEM[" ^ one_exp e ^ "]" 476 | one_exp (Tree.TEMP e) = 477 getTmp e 478 | one_exp (Tree.NAME e) = 479 Symbol.name e 480 | one_exp (Tree.NCONST e) = 481 Arbint.toString e 482 | one_exp (Tree.WCONST e) = 483 (Arbint.toString e) ^ "w" 484 | one_exp (Tree.CALL(f, args)) = 485 "CALL " ^ (one_exp f) 486 | one_exp (Tree.PAIR(e1,e2)) = 487 "(" ^ one_exp e1 ^ "," ^ one_exp e2 ^ ")" 488 | one_exp _ = 489 "" 490 ; 491 492 fun one_stm (Tree.MOVE(v1,v2)) = 493 indent ^ "MOV " ^ (one_exp v1) ^ ", " ^ (one_exp v2) 494 | one_stm (Tree.LABEL lab) = 495 (Symbol.name lab) ^ ":" 496 | one_stm (Tree.JUMP lab) = 497 indent ^ "JMP " ^ Symbol.name lab 498 | one_stm (Tree.CJUMP(c,lab)) = 499 indent ^ "JNE " ^ Symbol.name lab 500 | one_stm (Tree.EXP exp) = 501 one_exp exp 502 | one_stm _ = 503 "" 504 in 505 506 List.map (fn stm => print(one_stm stm ^ "\n")) stms 507 end 508 509end 510