1structure funCall = 2struct 3 4local 5(* 6quietdec := true; 7*) 8 9 10open HolKernel Parse boolLib IRSyntax annotatedIR 11structure T = IntMapTable(type key = int fun getInt n = n); 12structure S = Binaryset 13structure IR = IRSyntax 14 15(* 16 open funCall; 17 quietdec := false; 18*) 19in 20 21exception invalidArgs; 22exception argPassing; 23 24val numAvaiRegs = ref 10; 25 26fun strOrder (s1:string,s2:string) = 27 if s1 > s2 then GREATER 28 else if s1 = s2 then EQUAL 29 else LESS; 30 31(* ---------------------------------------------------------------------------------------------------------------------*) 32(* The configuaration for passing parameters, returning results and allocating stack space *) 33(* The stack goes upward. *) 34(* ---------------------------------------------------------------------------------------------------------------------*) 35(* 36 Address goes upward (i.e. from low address to high address)!!! 37 38 Content Address 39 caller's ip | saved pc | 0 40 caller's fp | saved lr | 1 41 | save sp | 2 42 | save fp | 3 43 | modified reg k | 44 | modified reg k-1 | 45 | ... | 46 | local variable 0 | 4 47 | local variable 1 | 5 48 | ... | . 49 | local variable n | . 50 | output k from callee | . 51 | ... | 52 | output 1 from callee | 53 | output 0 from callee | 54 | argument m' | 55 | ... | 56 | argument 1 | 57 | argument 0 | 58 caller's sp callee's ip | saved pc | 59 callee's fp | saved lr | 60 | save sp | 61 | save fp | 62 | modified reg k | 63 | modified reg k-1 | 64 | ... | 65 | local variable 0 | 66 | local variable 1 | 67 | ... | 68 callee's sp | local variable n' | 69*) 70 71 72(* Distinguish inputs and local variables *) 73(* Calculate the offset based on fp of the temporaries bebing read in a callee *) 74(* If a temporary is an input, then read it from the stack where the caller sets *) 75(* If it is a local variable, then read it from the current frame *) 76 77fun calculate_relative_address (args,ir,outs,numSavedRegs) = 78 let 79 (* Identify those TMEMs that are actually arguments *) 80 val argT = #1 (List.foldl (fn (IR.TMEM n, (t,i)) => 81 (T.enter(t, n, i), i+1) 82 | (arg, (t,i)) => (t, i+1) 83 ) 84 (T.empty, 0) 85 (IR.pair2list args) 86 ); 87 88 val i = ref 0 89 val localT = ref (T.empty); (* Table for the local variables *) 90 91 (* For those TMEMs that are local variables, assign them in the stack according to the order of their apprearance *) 92 93 fun filter_mems (IR.TMEM n) = 94 ( case T.peek (argT, n) of 95 SOME k => IR.MEM (IR.fromAlias IR.fp, ~2 - k) (* inputs *) 96 | NONE => 97 ( case T.peek(!localT, n) of 98 SOME j => IR.MEM (IR.fromAlias IR.fp, 3 + j + numSavedRegs) (* existing local variable *) 99 | NONE => 100 ( localT := T.enter(!localT, n, !i); 101 i := !i + 1; 102 IR.MEM (IR.fromAlias IR.fp, 3 + (!i - 1) + numSavedRegs) (* local variables *) 103 ) 104 ) 105 ) 106 | filter_mems v = v 107 108 fun one_stm ({oper = op1, dst = dst1, src = src1}) = 109 {oper = op1, dst = List.map filter_mems dst1, src = List.map filter_mems src1} 110 111 fun adjust_exp (IR.PAIR (e1,e2)) = 112 IR.PAIR(adjust_exp e1, adjust_exp e2) 113 | adjust_exp e = 114 filter_mems e 115 116 fun adjust_info {ins = ins', outs = outs', context = context', fspec = fspec'} = 117 {ins = adjust_exp ins', outs = adjust_exp outs', context = List.map adjust_exp context', fspec = fspec'} 118 119 fun visit (SC(ir1,ir2,info)) = 120 SC (visit ir1, visit ir2, adjust_info info) 121 | visit (TR((e1,rop,e2),ir,info)) = 122 TR ((adjust_exp e1,rop,adjust_exp e2), visit ir, adjust_info info) 123 | visit (CJ((e1,rop,e2),ir1,ir2,info)) = 124 CJ ((adjust_exp e1,rop,adjust_exp e2), visit ir1, visit ir2, adjust_info info) 125 | visit (CALL(fname,pre,body,post,info)) = 126 CALL(fname, pre, body, post, adjust_info info) 127 | visit (STM l) = 128 STM (List.map one_stm l) 129 | visit (BLK (l,info)) = 130 BLK (List.map one_stm l, adjust_info info); 131 132 in 133 (adjust_exp args, visit ir, adjust_exp outs, T.numItems (!localT)) 134 end 135 136(* ---------------------------------------------------------------------------------------------------------------------*) 137(* Decrease and increase the value of a register by 4*n *) 138(* These functions are used for modification of base registers for load ans stores. Since *) 139(* loads and stores always consider 32bit words, the address had to be deviable by 4 *) 140(* Therefore n is the number of words the register should change. *) 141(* ---------------------------------------------------------------------------------------------------------------------*) 142 143fun dec_p pt n = {oper = IR.msub, dst = [IR.REG pt], src = [IR.REG pt, IR.WCONST (Arbint.fromInt (4*n))]} 144 145fun inc_p pt n = {oper = IR.madd, dst = [IR.REG pt], src = [IR.REG pt, IR.WCONST (Arbint.fromInt (4*n))]}; 146 147 148(* ---------------------------------------------------------------------------------------------------------------------*) 149(* Pre-call and post-call processing in compilance with the ARM Procedure Call standard *) 150(* ---------------------------------------------------------------------------------------------------------------------*) 151 152(* MOV ip, sp 153 STMFA sp!, {..., fp,ip,lr,pc} 154 SUB fp, ip, #1 155 SUB sp, sp, #var (* skip local variables *) 156*) 157 158fun entry_blk rs n = 159 [ {oper = IR.mmov, dst = [IR.REG (IR.fromAlias IR.ip)], src = [IR.REG (IR.fromAlias IR.sp)]}, 160 {oper = IR.mpush, dst = [IR.REG (IR.fromAlias IR.sp)], 161 src = rs @ [IR.REG (IR.fromAlias IR.fp), IR.REG (IR.fromAlias IR.ip), 162 IR.REG (IR.fromAlias IR.lr), IR.REG (IR.fromAlias IR.pc)] 163 }, 164 {oper = IR.msub, dst = [IR.REG (IR.fromAlias IR.fp)], src = [IR.REG (IR.fromAlias IR.ip), IR.WCONST (Arbint.fromInt 4)]}, 165 dec_p (IR.fromAlias IR.sp) n (* skip local variables *) 166 ] 167 168(* 169 ADD sp, fp, 3 + #modified registers (* Skip saved lr, sp, fp and modified registers *) 170 LDMFD sp, {..., fp,sp,pc} 171*) 172 173fun exit_blk rs = 174 [ 175 {oper = IR.msub, dst = [IR.REG (IR.fromAlias IR.sp)], src = [IR.REG (IR.fromAlias IR.fp), IR.WCONST (Arbint.fromInt (4* (3 + length rs)))]}, 176 {oper = IR.mpop, dst = rs @ [IR.REG (IR.fromAlias IR.fp), IR.REG (IR.fromAlias IR.sp), IR.REG (IR.fromAlias IR.pc)], 177 src = [IR.REG (IR.fromAlias IR.sp)]} 178 ]; 179 180 181(* ---------------------------------------------------------------------------------------------------------------------*) 182(* Given a list of registers and memory slots, group consecutive registers together to be used by mpush and mpop *) 183(* For example, [r1,r2,m1,m3,r3,4w,r4,r5] is segmented to *) 184(* ([r1,r2],true, 0),(m1,false,2),(m3,false,3),([r3],true,4),(4w,false,5),([r4,r5],true,6) *) 185(* ---------------------------------------------------------------------------------------------------------------------*) 186 187fun mk_reg_segments argL = 188 let val isBroken = ref false; 189 190 (* proceeds in reverse order of the list *) 191 fun one_arg (IR.REG r, (invRegLs, i)) = 192 let val flag = !isBroken 193 val _ = isBroken := false 194 in 195 if null invRegLs orelse flag then 196 (([IR.REG r], true, i) :: invRegLs, i-1) 197 else 198 let val (cur_segL, a, j) = hd invRegLs 199 in 200 if null cur_segL then (([IR.REG r], true, i) :: (tl invRegLs), i-1) 201 else ((IR.REG r :: cur_segL, true, i) :: (tl invRegLs), i-1) 202 end 203 end 204 | one_arg (exp, (invRegLs, i)) = 205 (isBroken := true; (([exp],false, i) :: invRegLs, i-1)) 206 207 val (invRegLs, i) = List.foldr one_arg ([], length argL - 1) argL 208 209 in 210 invRegLs 211 end 212 213(* ---------------------------------------------------------------------------------------------------------------------*) 214(* Given a list of registers, generate a mpush or mpop statement *) 215(* The sp is assumed to be in the right position *) 216(* If the list contain only one resiter, then use mldr and mstr instead *) 217(* ---------------------------------------------------------------------------------------------------------------------*) 218 219fun mk_ldm_stm isPop r dataL = 220 if isPop then 221 if length dataL = 1 then 222 {oper = IR.mldr, dst = dataL, src = [IR.MEM (r,1)]} 223 else 224 {oper = IR.mpop, dst = dataL, src = [IR.REG r]} 225 else 226 if length dataL = 1 then 227 {oper = IR.mstr, dst = [IR.MEM(r,0)], src = dataL} 228 else 229 {oper = IR.mpush, dst = [IR.REG r], src = dataL} 230 231(* ---------------------------------------------------------------------------------------------------------------------*) 232(* Write one argument to the memory slot referred by regNo and offset *) 233(* Push arguments to the stack. If the argument comes from a register, and store it into the stack directly; *) 234(* if it comes from memory, then first load it into R10, and then store it into the stack; *) 235(* if it is a constant, then assign it to R10 first then store it into the stack. *) 236(* ---------------------------------------------------------------------------------------------------------------------*) 237 238fun write_one_arg (IR.MEM v) (regNo,offset) = 239 [ {oper = IR.mldr, dst = [IR.REG (!numAvaiRegs)], src = [IR.MEM v]}, 240 {oper = IR.mstr, dst = [IR.MEM (regNo,offset)], src = [IR.REG (!numAvaiRegs)]} ] 241 | write_one_arg (IR.REG r) (regNo,offset) = 242 [ {oper = IR.mstr, dst = [IR.MEM (regNo,offset)], src = [IR.REG r]} ] 243 | write_one_arg v (regNo,offset) = (* v = NONCST n or WCONST w *) 244 [ {oper = IR.mmov, dst = [IR.REG 10], src = [v]}, 245 {oper = IR.mstr, dst = [IR.MEM (regNo,offset)], src = [IR.REG 10]} ] 246 247(* ---------------------------------------------------------------------------------------------------------------------*) 248(* Read one argument from the memory slot referred by regNo and offset *) 249(* If the destination is a register, then load it into the register directly; *) 250(* if it is in the memory, then first load the value into R10, and then store it into that memory location; *) 251(* The destination couldn't be a constant *) 252(* ---------------------------------------------------------------------------------------------------------------------*) 253 254fun read_one_arg (IR.REG r) (regNo,offset) = 255 [ {oper = IR.mldr, dst = [IR.REG r], src = [IR.MEM(regNo,offset)]} ] 256 | read_one_arg (IR.MEM v) (regNo,offset) = 257 [ {oper = IR.mldr, dst = [IR.REG (!numAvaiRegs)], src = [IR.MEM(regNo,offset)]}, 258 {oper = IR.mstr, dst = [IR.MEM v], src = [IR.REG (!numAvaiRegs)]} ] 259 | read_one_arg _ _ = 260 raise invalidArgs 261 262(* ---------------------------------------------------------------------------------------------------------------------*) 263(* Push a list of values that may be constants or in registers or in memory into the stack *) 264(* [1,2,3,...] *) 265(* old pointer | 1 | *) 266(* | 2 | *) 267(* | 3 | *) 268(* ... *) 269(* new pointer *) 270(* Note that the elements in the list are stored in the memory from low addresses to high addresses *) 271(* ---------------------------------------------------------------------------------------------------------------------*) 272 273fun pushL regNo argL = 274 let 275 val offset = ref 0; 276 277 fun one_seg (regL, true, i) = 278 if length regL = 1 then 279 write_one_arg (hd regL) (regNo, !offset - i) (* relative offset should be negative *) 280 else 281 let val k = !offset in 282 ( offset := i + length regL; 283 [dec_p regNo (i - k), 284 (* reverse the regL in accordance with the order of STM *) 285 mk_ldm_stm false regNo (List.rev regL)]) 286 end 287 | one_seg ([v], false, i) = 288 write_one_arg v (regNo, !offset - i) 289 | one_seg _ = raise invalidArgs 290 in 291 (List.foldl (fn (x,s) => s @ one_seg x) [] (mk_reg_segments argL)) @ 292 [dec_p regNo (length argL - !offset)] 293 end 294 295(* ---------------------------------------------------------------------------------------------------------------------*) 296(* Pop from the stack a list of values that may be in registers or in memory into the stack *) 297(* ... *) 298(* | 3 | *) 299(* | 2 | *) 300(* | 1 | *) 301(* pointer *) 302(* be read to the list [1,2,3,...] *) 303(* ---------------------------------------------------------------------------------------------------------------------*) 304 305fun popL regNo argL = 306 let 307 val offset = ref 0; 308 309 fun one_seg (regL, true, i) = 310 if length regL = 1 then 311 read_one_arg (hd regL) (regNo, i - !offset + 1) (* relative address should be positive *) 312 else 313 let val k = !offset in 314 ( offset := i; 315 [inc_p regNo (i - k), 316 mk_ldm_stm true regNo regL]) 317 end 318 | one_seg ([v], false, i) = 319 read_one_arg v (regNo, i - !offset + 1) 320 | one_seg _ = raise invalidArgs 321 in 322 (List.foldl (fn (x,s) => s @ one_seg x) [] (mk_reg_segments argL)) @ 323 [inc_p regNo (length argL - !offset)] 324 end 325 326(* ---------------------------------------------------------------------------------------------------------------------*) 327(* Pass by the caller the parameters to the callee *) 328(* All arguments are passed through the stack *) 329(* Stack status after passing *) 330(* ... *) 331(* | arg 3 | *) 332(* | arg 2 | *) 333(* sp | arg 1 | *) 334(* ---------------------------------------------------------------------------------------------------------------------*) 335 336fun pass_args argL = 337 pushL (IR.fromAlias IR.sp) (List.rev argL) 338 339(* ---------------------------------------------------------------------------------------------------------------------*) 340(* The callee obtains the arguments passed by the caller though the stack *) 341(* By default, the first four arguments are loaded into r0-r4 *) 342(* The rest arguments has been in the right positions. That is, we need not to get them explicitly *) 343(* Note that the register allocation assumes above convention *) 344(* ---------------------------------------------------------------------------------------------------------------------*) 345 346fun get_args argL = 347 let 348 val len = length argL; 349 val len1 = if len < (!numAvaiRegs) then len else (!numAvaiRegs) 350 351 fun mk_regL 0 = [IR.REG 0] 352 | mk_regL n = mk_regL (n-1) @ [IR.REG n]; 353 354 in 355 popL (IR.fromAlias (IR.ip)) argL 356 (* Note that callee's IP equals to caller's SP, we use the IP here to load the arguments *) 357 end; 358 359(* ---------------------------------------------------------------------------------------------------------------------*) 360(* Pass by the callee the results to the caller *) 361(* All results are passed through the stack *) 362(* Stack status after passing *) 363(* *) 364(* ... *) 365(* | result 3 | *) 366(* | result 2 | *) 367(* | result 1 | *) 368(* sp *) 369(* ---------------------------------------------------------------------------------------------------------------------*) 370 371fun send_results outL numArgs = 372 let 373 (* skip the arguments and the stored pc, then go to the position right before the first output*) 374 val sOffset = numArgs + length outL + 1; 375 val stms = pushL (IR.fromAlias IR.sp) (List.rev outL) 376 in 377 { oper = IR.madd, 378 dst = [IR.REG (IR.fromAlias IR.sp)], 379 src = [IR.REG (IR.fromAlias IR.fp), IR.WCONST (Arbint.fromInt (4* sOffset))] 380 } 381 :: stms 382 end 383 384(* ---------------------------------------------------------------------------------------------------------------------*) 385(* The caller retreives the results passed by the callee though the stack *) 386(* Stack status *) 387(* *) 388(* ... *) 389(* | result 3 | *) 390(* | result 2 | *) 391(* | result 1 | *) 392(* sp | | *) 393(* ---------------------------------------------------------------------------------------------------------------------*) 394 395fun get_results outL = 396 popL (IR.fromAlias IR.sp) outL 397 398(* ---------------------------------------------------------------------------------------------------------------------*) 399(* Function Call: Pre-processing, Post-processing and Adjusted Body *) 400(* ---------------------------------------------------------------------------------------------------------------------*) 401 402fun compute_fcall_info ((outer_ins,outer_outs),(caller_src,caller_dst),(callee_ins,callee_outs),rs,context) = 403 let 404 fun to_stack expL = 405 let val len = length expL 406 val i = ref 0; 407 in 408 List.map (fn exp => ( i := !i + 1; MEM(11, ~(3 + (len - !i))))) expL 409 end 410 411 val to_be_stored = S.difference (list2set (List.map REG (S.listItems rs)), pair2set caller_dst); 412 val rs' = S.intersection(to_be_stored, S.union (pair2set outer_outs, list2set context)); 413 val pre_ins = trim_pair (PAIR (caller_src, set2pair rs')); 414 val stored = (list2pair o to_stack o set2list) rs'; 415 val pre_outs = trim_pair (PAIR (callee_ins, stored)); 416 val body_ins = pre_outs; 417 val body_outs = trim_pair(PAIR (callee_outs, stored)); 418 val post_ins = body_outs; 419 val post_outs = trim_pair(PAIR (caller_dst, set2pair rs')); 420 val context' = set2list (S.difference (list2set context, rs')) 421 in 422 ((pre_ins,pre_outs),(body_ins,body_outs),(post_ins,post_outs),set2list rs',context') 423 end 424 425 426 427 (*This function gets to lists of registers. The values of the 428 registers in scrL are moved to the registers in destL. Thereby, 429 the dummy registers are used for intermediate storage, if necessary. 430 The result is a list of move statements that have to be executed. 431 For example 432 destL = [REG 0, REG 2, REG 1] 433 srcL = [REG 0, REG 1, REG 2] 434 dummyL = [REG 3, ...] 435 should result in something like 436 (REG 3 <- REG 2), (REG 2 <- REG 1), (REG 1 <- REG 3) 437 *) 438 439local 440 fun remove_reg (REG r) = r 441 fun is_reg (REG r) = true | 442 is_reg _ = false; 443 444 val sortdata = 445 sort (fn (dest:int, src:int, beforeL:int list) => fn (dest':int, src':int, beforeL':int list) => (length beforeL < length beforeL')) 446 447 fun extract_next dummyL (data):(int * int * int list) list = 448 if ((#3 (hd data)) = []) then data else 449 let 450 val data' = sortdata data 451 in 452 if ((#3 (hd data')) = []) then data' else 453 let 454 val (dest, src, beforeL) = hd data'; 455 val dummy_reg = remove_reg (hd dummyL) 456 val new_elem = (dummy_reg, dest, []:int list); 457 (*security check*) 458 val _ = if (exists (fn e:(int*int*int list) => (#1 e = dummy_reg) orelse (#2 e = dummy_reg)) data) then 459 raise argPassing else () 460 in 461 new_elem :: data' 462 end 463 end 464 465 fun process_next (data:(int*int*int list) list) = 466 let 467 val (dest, src, beforeL) = hd data; 468 val _ = if (beforeL = []) then () else raise argPassing; 469 val data' = map (fn (e_dest, e_src, e_beforeL) => 470 let 471 val e_src' = if (e_src = src) then dest else e_src; 472 val e_beforeL' = if (e_dest = src) then [] else filter (fn e => not (e = dest)) e_beforeL; 473 in 474 (e_dest, e_src', e_beforeL') 475 end) (tl data) 476 in 477 ((dest, src), data') 478 end 479in 480 fun mk_mov_ir destL srcL dummyL = 481 let 482 val copyL = zip destL srcL; 483 val (regL, nonRegL) = partition (fn (x, y) => is_reg y) copyL; 484 val regL = map (fn (x, y) => (remove_reg x, remove_reg y)) regL; 485 val regL = filter (fn (x, y) => not (x = y)) regL; 486 487 488 (*calculates, which registers have to be updated before, 489 because they directly depend on the value, that should be 490 overwritten*) 491 fun direct_before r = 492 let 493 val regL_filter = filter (fn (dest, src) => (src = r)) regL; 494 in 495 map (fn (dest, src) => dest) regL_filter 496 end 497 498 val data = map (fn (dest, src) => (dest, src, direct_before dest)) regL 499 500 fun process_data dummyL resultL [] = resultL | 501 process_data dummyL resultL data = 502 let 503 val data' = extract_next dummyL data; 504 val (res, data'') = (process_next data'); 505 in 506 process_data dummyL (resultL@[res]) data'' 507 end; 508 509 val aL = process_data dummyL [] data; 510 val aL = map (fn (x, y) => (REG x, REG y)) aL 511 fun mov_ir (dst, src) = {oper = IR.mmov, dst = [dst], src = [src]} 512 in 513 map mov_ir (aL@nonRegL) 514 end; 515 516end; 517 518 519val involved_defs = ref ([] : thm list); 520 521(* 522fun extract (SC(s1,s2,info)) = (s1,s2,info) 523val (s1,s2,info) = extract ir1 524val (s1,s2,info) = extract s2 525 526fun extract (CJ(cond,s1,s2,info)) = (cond,s1,s2,info); 527val (cond,s1,s2,info) = extract ir1 528 529fun extract (CALL(fname, pre, body, post, outer_info)) = 530(fname, pre, body, post, outer_info) 531val (fname, pre, body, post, outer_info) = extract s2 532 533*) 534 535fun convert_fcall (CALL(fname, pre, body, post, outer_info)) = 536 let 537 (* pass the arguments to the callee, and callee will save and restore anything *) 538 (* create the BL statement *) 539 (* then modify the sp to point to the real position of the returning arguments *) 540 541 val (outer_ins,outer_outs) = (#ins outer_info, #outs outer_info); 542 val (caller_dst,caller_src) = let val x = get_annt body in (#outs x, #ins x) end; 543 val {ir = (callee_ins, callee_ir, callee_outs), regs = rs, localNum = n, def = f_def, ...} = declFuncs.getFunc fname; 544 val _ = involved_defs := (!involved_defs) @ [f_def]; 545 546 547 548 val ((pre_ins,pre_outs),(body_ins,body_outs),(post_ins,post_outs),rs',context) = 549 compute_fcall_info ((outer_ins,outer_outs),(caller_src,caller_dst),(callee_ins,callee_outs),rs,#context outer_info); 550 551 fun to_stack 0 = [] | 552 to_stack n = (MEM(13, n))::(to_stack(n-1)) 553 554 val preserve_list = filter (fn r => not (mem r (pair2list caller_dst))) (pair2list outer_outs); 555 556 557 val dummy_reg_list = 558 let 559 val dummy_list = [REG 0, REG 1, REG 2, REG 3, REG 4, 560 REG 5, REG 6, REG 7, REG 8, REG 9, REG 10]; 561 val dummy_list = filter (fn r => not (mem r (pair2list outer_outs))) dummy_list 562 val dummy_list = preserve_list@dummy_list; 563 564 val not_use_list = (pair2list caller_src) @ 565 (pair2list caller_dst) @ 566 (pair2list callee_ins) @ 567 (pair2list callee_outs) 568 val dummy_list = filter (fn r => not (mem r not_use_list)) 569 dummy_list 570 in 571 dummy_list 572 end; 573 574 val in_mov_ir = mk_mov_ir (pair2list callee_ins) (pair2list caller_src) dummy_reg_list 575 val out_mov_ir = mk_mov_ir (pair2list caller_dst) (pair2list callee_outs) dummy_reg_list 576 577 val mpop_ir = if (preserve_list = []) then [] else 578 [{dst = preserve_list, oper = mpop, src = [REG 13]}] 579 val mpush_ir = if (preserve_list = []) then [] else 580 [{dst = [REG 13], oper = mpush, src = preserve_list}] 581 582 val stack_ir_list = to_stack (length preserve_list) 583 val ins_stack = trim_pair(list2pair(stack_ir_list @ (pair2list callee_ins))); 584 val outs_stack = trim_pair(list2pair(stack_ir_list @ (pair2list callee_outs))); 585 586 val pre' = BLK ( 587 mpush_ir @ in_mov_ir, 588 {ins = outer_ins, 589 outs = ins_stack, context = context, fspec = thm_t}); 590 591 val callee_ir' = convert_fcall callee_ir; 592 val body' = apply_to_info callee_ir' (fn info' => {ins = ins_stack, outs = outs_stack, context = context, fspec = thm_t}); 593 594 val post' = BLK ( 595 out_mov_ir @ mpop_ir, 596 {ins = outs_stack, outs = outer_outs, context = context, fspec = thm_t}) 597 in 598 CALL(fname, pre' , body', post', outer_info) 599 end 600 601 | convert_fcall (SC(s1,s2,info)) = SC (convert_fcall s1, convert_fcall s2, info) 602 | convert_fcall (CJ(cond,s1,s2,info)) = CJ (cond, convert_fcall s1, convert_fcall s2, info) 603 | convert_fcall (TR(cond,s,info)) = TR (cond, convert_fcall s, info) 604 | convert_fcall ir = ir; 605 606 607(* ---------------------------------------------------------------------------------------------------------------------*) 608(* Link caller and callees together *) 609(* ---------------------------------------------------------------------------------------------------------------------*) 610(*val prog = def*) 611fun link_ir prog = 612 let 613 val (fname, ftype, f_ir as (ins,ir0,outs), defs) = sfl2ir prog; 614 val rs = S.addList (S.empty regAllocation.intOrder, get_modified_regs ir0); 615 616 val (ins1,ir1,outs1, localNum) = calculate_relative_address (ins,ir0,outs,S.numItems rs); 617 val ir2 = convert_fcall ir1 618 (*val ir3 = match_ins_outs ir1*) 619 val ir3 = ir2 620 621 val rs' = S.addList (S.empty regAllocation.intOrder, get_modified_regs ir3); 622 val _ = (involved_defs := []; 623 declFuncs.putFunc (fname, ftype, (ins1,ir1,outs1), rs', localNum, (hd defs))); 624 in 625 (fname,ftype,(ins1,ir3,outs1), defs @ (!involved_defs)) 626 end; 627 628 629end (* local structure ... *) 630 631end (* structure *) 632