Changeset 1584 for Deliverables/D2.2/8051
- Timestamp:
- Dec 2, 2011, 3:13:04 PM (9 years ago)
- Location:
- Deliverables/D2.2/8051/src
- Files:
-
- 11 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051/src/RTL/RTLConstPropagation.ml
r1580 r1584 333 333 (* in the above case if carry is set add unsets it, that's why we must 334 334 make sure it's unset *) 335 335 336 | Some 255, _, Some 1, I8051.Addc 336 337 | Some 255, _, _, I8051.And -> … … 341 342 | _, Some 255, _, I8051.And -> 342 343 St_move (i, a, l) 344 | _, _, Some 0, I8051.Addc -> 345 (* does not change time, but maybe helps getting better results 346 with liveness analysis *) 347 St_op2 (I8051.Add, i, arg_from_arg prop a, arg_from_arg prop b, l) 343 348 | _ -> 344 349 St_op2 (op, i, arg_from_arg prop a, arg_from_arg prop b, l) -
Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml
r1572 r1584 19 19 20 20 let change_label lbl = function 21 | ERTL.St_skip _ -> ERTL.St_skip lbl22 | ERTL.St_comment (s, _) -> ERTL.St_comment (s, lbl)23 | ERTL.St_cost (cost_lbl, _) -> ERTL.St_cost (cost_lbl, lbl)24 | ERTL.St_ind_0 (i, _) -> ERTL.St_ind_0 (i, lbl)25 | ERTL.St_ind_inc (i, _) -> ERTL.St_ind_inc (i, lbl)26 | ERTL.St_get_hdw (r1, r2, _) -> ERTL.St_get_hdw (r1, r2, lbl)27 | ERTL.St_set_hdw (r1, r2, _) -> ERTL.St_set_hdw (r1, r2, lbl)28 | ERTL.St_hdw_to_hdw (r1, r2, _) -> ERTL.St_hdw_to_hdw (r1, r2, lbl)29 | ERTL.St_newframe _ -> ERTL.St_newframe lbl30 | ERTL.St_delframe _ -> ERTL.St_delframe lbl31 | ERTL.St_framesize (r, _) -> ERTL.St_framesize (r, lbl)32 | ERTL.St_pop (r, _) -> ERTL.St_pop (r, lbl)33 | ERTL.St_push (r, _) -> ERTL.St_push (r, lbl)34 | ERTL.St_addrH (r, id, _) -> ERTL.St_addrH (r, id, lbl)35 | ERTL.St_addrL (r, id, _) -> ERTL.St_addrL (r, id, lbl)36 | ERTL.St_move (r1, a, _) -> ERTL.St_move (r1, a, lbl)37 | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, _) ->38 ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl)39 | ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, _) ->40 ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, lbl)41 | ERTL.St_op1 (op1, dstr, srcr, _) -> ERTL.St_op1 (op1, dstr, srcr, lbl)42 | ERTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->43 ERTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)44 | ERTL.St_clear_carry _ -> ERTL.St_clear_carry lbl45 | ERTL.St_set_carry _ -> ERTL.St_set_carry lbl46 | ERTL.St_load (dstrs, addr1, addr2, _) ->47 ERTL.St_load (dstrs, addr1, addr2, lbl)48 | ERTL.St_store (addr1, addr2, srcrs, _) ->49 ERTL.St_store (addr1, addr2, srcrs, lbl)50 | ERTL.St_call_id (f, nb_args, _) -> ERTL.St_call_id (f, nb_args, lbl)51 | ERTL.St_call_ptr (f1, f2, nb_args, _) ->52 ERTL.St_call_ptr (f1, f2, nb_args, lbl)53 21 | ERTL.St_cond _ as inst -> inst 54 22 | ERTL.St_return _ as inst -> inst 23 | stmt -> ERTLGraph.fill_succs stmt [lbl] 55 24 56 25 (* Add a list of instruction in a graph, from one label to another, by creating -
Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml
r1580 r1584 115 115 116 116 let change_label lbl = function 117 | RTL.St_skip _ -> RTL.St_skip lbl 118 | RTL.St_cost (cost_lbl, _) -> RTL.St_cost (cost_lbl, lbl) 119 | RTL.St_ind_0 (i, _) -> RTL.St_ind_0 (i, lbl) 120 | RTL.St_ind_inc (i, _) -> RTL.St_ind_inc (i, lbl) 121 | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl) 122 | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl) 123 (* | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl) *) 124 | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl) 125 | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, _) -> 126 RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl) 127 | RTL.St_op1 (op1, dstr, srcr, _) -> RTL.St_op1 (op1, dstr, srcr, lbl) 128 | RTL.St_op2 (op2, dstr, srcr1, srcr2, _) -> 129 RTL.St_op2 (op2, dstr, srcr1, srcr2, lbl) 130 | RTL.St_clear_carry _ -> RTL.St_clear_carry lbl 131 | RTL.St_set_carry _ -> RTL.St_set_carry lbl 132 | RTL.St_load (dstrs, addr1, addr2, _) -> 133 RTL.St_load (dstrs, addr1, addr2, lbl) 134 | RTL.St_store (addr1, addr2, srcrs, _) -> 135 RTL.St_store (addr1, addr2, srcrs, lbl) 136 | RTL.St_call_id (f, args, retrs, _) -> RTL.St_call_id (f, args, retrs, lbl) 137 | RTL.St_call_ptr (f1, f2, args, retrs, _) -> 138 RTL.St_call_ptr (f1, f2, args, retrs, lbl) 139 | RTL.St_tailcall_id (f, args) -> RTL.St_tailcall_id (f, args) 140 | RTL.St_tailcall_ptr (f1, f2, args) -> RTL.St_tailcall_ptr (f1, f2, args) 141 | RTL.St_cond _ as inst -> inst 142 | RTL.St_return regs -> RTL.St_return regs 117 | (RTL.St_cond _ | RTL.St_return _) as inst -> inst 118 | stmt -> RTLGraph.fill_succs stmt [lbl] 143 119 144 120 (* Add a list of instruction in a graph, from one label to another, by creating … … 308 284 let (def, tmpr) = fresh_reg def in 309 285 let carry_init = match op with 310 | I8051. Addc | I8051.Sub->286 | I8051.Sub | I8051.Addc -> 311 287 (* depend on carry bit *) 312 288 [RTL.St_clear_carry start_lbl] 313 | I8051.Add -> assert false (* should not call with add, not correct *)314 289 | _ -> [] in 315 let f_add destr srcr1 srcr2 =290 let f_add op destr srcr1 srcr2 = 316 291 RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in 317 292 let insts_add = 318 MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in 293 match op with 294 | I8051.Add -> 295 (* we perform a first add followed by Addc's *) 296 let f destr srcr1 srcr2 (op, insts) = 297 (I8051.Addc, f_add op destr srcr1 srcr2 :: insts) in 298 snd (MiscPottier.fold3_right 299 f destrs_common srcrs1_common srcrs2_common (I8051.Add, [])) 300 | _ -> 301 (* we just do the same operation on all *) 302 MiscPottier.map3 (f_add op) destrs_common srcrs1_common srcrs2_common in 319 303 let f_add_cted destr srcr = 320 304 RTL.St_op2 (op, destr, srcr, RTL.Imm 0, start_lbl) in … … 331 315 start_lbl dest_lbl def 332 316 333 334 let rec translate_mul1 dummy tmpr destrs srcrs1 srcr2 start_lbl =335 match destrs, srcrs1 with336 | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl337 | [destr], [] ->338 adds_graph339 [RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Imm 0, start_lbl)]340 start_lbl341 | destr1 :: destr2 :: destrs, [] ->342 add_translates343 [adds_graph344 [RTL.St_op2 (I8051.Addc, destr1,345 RTL.Reg destr1, RTL.Imm 0, start_lbl) ;346 RTL.St_op2 (I8051.Addc, destr2, RTL.Imm 0, RTL.Imm 0, start_lbl)] ;347 translate_cst (AST.Cst_int 0) destrs]348 start_lbl349 | [destr], srcr1 :: _ ->350 adds_graph351 [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ;352 RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Reg tmpr, start_lbl)]353 start_lbl354 | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 ->355 add_translates356 [adds_graph357 [RTL.St_opaccs358 (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ;359 RTL.St_op2 (I8051.Addc, destr1, RTL.Reg destr1,360 RTL.Reg tmpr, start_lbl)] ;361 translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2]362 start_lbl363 364 let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates365 srcr2i =366 let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in367 translates @368 (match tmp_destrs2 with369 | [] -> []370 | tmp_destr2 :: tmp_destrs2 ->371 [adds_graph [RTL.St_clear_carry dummy_lbl ;372 RTL.St_move (tmp_destr2, RTL.Imm 0, dummy_lbl)] ;373 translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;374 translate_cst (AST.Cst_int 0) tmp_destrs1 ;375 let reg_destrs = List.map (fun r -> RTL.Reg r) destrs in376 let tmp_destrs = List.map (fun r -> RTL.Reg r) tmp_destrs in377 translate_op I8051.Addc destrs reg_destrs tmp_destrs])378 379 317 let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def = 380 let (def, dummy) = fresh_reg def in 381 let (def, tmpr) = fresh_reg def in 382 let (def, tmp_destrs) = fresh_regs def (List.length destrs) in 383 let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in 384 (* let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in *) 385 let reg r = RTL.Reg r in 386 let insts_init = 387 [translate_move fresh_srcrs1 srcrs1 ; 388 (* translate_move fresh_srcrs2 srcrs2 ; *) 389 translate_cst (AST.Cst_int 0) destrs] in 390 let fresh_srcrs1 = List.map reg fresh_srcrs1 in 391 let f = translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in 392 let insts_mul = MiscPottier.foldi f [] srcrs2 in 393 add_translates (insts_init @ insts_mul) start_lbl dest_lbl def 394 318 (* we save those parts of srcrs that could be overwritten *) 319 let save_srcrs a (def, srcrs, init) = match a with 320 | RTL.Reg r when List.mem r destrs -> 321 let (def, new_r) = fresh_reg def in 322 (def, RTL.Reg new_r :: srcrs, 323 adds_graph [RTL.St_move (new_r, a, start_lbl)] :: init) 324 | _ -> (def, a :: srcrs, init) in 325 let (def, fresh_srcrs1, init) = 326 List.fold_right save_srcrs srcrs1 (def, [], []) in 327 let (def, fresh_srcrs2, init) = 328 List.fold_right save_srcrs srcrs2 (def, [], init) in 329 let srcrs1_n = List.length srcrs1 in 330 let srcrs2_n = List.length srcrs2 in 331 let destrs_n = List.length destrs in 332 (* the next must be an invariant *) 333 assert (srcrs1_n = destrs_n && destrs_n = srcrs1_n); 334 (* we pad destrs with a copy of itself that will be added to it at the end 335 (when the multiplication overflows) and then three more. The routine 336 should thus handle overflow nicely, but it must be checked *) 337 let all_destrs = MiscPottier.fill destrs (2 * destrs_n + 3) in 338 let init = translate_cst (AST.Cst_int 0) destrs :: init in 339 (* the registries to hold the temporary results of 8-bit mutliplication *) 340 let (def, a) = fresh_reg def in 341 let (def, b) = fresh_reg def in 342 (* when getting the result, this is what is used (padded to 3 bytes *) 343 let mul_arg = [RTL.Reg a ; RTL.Reg b ; RTL.Imm 0] in 344 let mul i j = 345 let s1i, s2j = List.nth fresh_srcrs1 i, List.nth fresh_srcrs2 i in 346 let k = i + j in 347 let dloc = MiscPottier.sublist all_destrs k (k+3) in 348 let dloc_arg = List.map (fun r -> RTL.Reg r) dloc in 349 [ adds_graph [RTL.St_opaccs (I8051.Mul, a, b, s1i, s2j, start_lbl)] ; 350 translate_op I8051.Add dloc dloc_arg mul_arg ] in 351 let insts = List.flatten (List.flatten 352 (MiscPottier.makei (fun i -> 353 MiscPottier.makei (mul i) srcrs2_n) srcrs1_n)) in 354 add_translates (init @ insts) start_lbl dest_lbl def 395 355 396 356 let translate_divumodu8 order destrs srcr1 srcr2 start_lbl dest_lbl def = … … 457 417 | [] -> adds_graph [] start_lbl dest_lbl def 458 418 | destr :: destrs -> 459 (* not sure that it is the correct thing to do, what about signed?460 can really srcrs1 and srcrs2 be of different length? Are not all461 correct types enforced? *)462 419 let (srcrs1, srcrs2) = pad_with (RTL.Imm 0) srcrs1 srcrs2 in 463 420 let init = RTL.St_clear_carry start_lbl in … … 705 662 add_graph lbl (RTL.St_return (find_local_env r lenv)) def 706 663 664 open BList.Notation 665 707 666 let remove_non_int_immediates def = 708 let load_arg a lbl g rs= match a with667 let load_arg a f = match a with 709 668 | RTLabs.Imm ((AST.Cst_stack _ | AST.Cst_addrsymbol _) as c, t) -> 710 let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in 711 let new_r = Register.fresh def.RTLabs.f_runiverse in 712 let g = Label.Map.add lbl (RTLabs.St_cst (new_r, c, new_l)) g in 713 (new_l, g, (new_r, t) :: rs, RTLabs.Reg new_r) 714 | _ -> (lbl, g, rs, a) in 715 let load_args args lbl g rs = 716 let f a (lbl', g', rs', args') = 717 let (lbl'', g'', rs'', a') = load_arg a lbl' g' rs' in 718 (lbl'', g'', rs'', a' :: args') in 719 List.fold_right f args (lbl, g, rs, []) in 720 let f lbl stmt (g, rs) = 721 match stmt with 722 | RTLabs.St_op2(op, r, a1, a2, l) -> 723 let (lbl', g, rs, a1) = load_arg a1 lbl g rs in 724 let (lbl', g, rs, a2) = load_arg a2 lbl' g rs in 725 let s = RTLabs.St_op2 (op, r, a1, a2, l) in 726 let g = Label.Map.add lbl' s g in 727 (g, rs) 728 | RTLabs.St_store(q, a1, a2, l) -> 729 let (lbl', g, rs, a1) = load_arg a1 lbl g rs in 730 let (lbl', g, rs, a2) = load_arg a2 lbl' g rs in 731 let s = RTLabs.St_store (q, a1, a2, l) in 732 let g = Label.Map.add lbl' s g in 733 (g, rs) 734 | RTLabs.St_load (q, a, r, l) -> 735 let (lbl', g, rs, a) = load_arg a lbl g rs in 736 let s = RTLabs.St_load (q, a, r, l) in 737 let g = Label.Map.add lbl' s g in 738 (g, rs) 739 | RTLabs.St_call_id (f, args, ret, s, l) -> 740 let (lbl', g, rs, args) = load_args args lbl g rs in 741 let s = RTLabs.St_call_id (f, args, ret, s, l) in 742 let g = Label.Map.add lbl' s g in 743 (g, rs) 744 | RTLabs.St_tailcall_id (f, args, s) -> 745 let (lbl', g, rs, args) = load_args args lbl g rs in 746 let s = RTLabs.St_tailcall_id (f, args, s) in 747 let g = Label.Map.add lbl' s g in 748 (g, rs) 749 | RTLabs.St_call_ptr (f, args, ret, s, l) -> 750 let (lbl', g, rs, args) = load_args args lbl g rs in 751 let s = RTLabs.St_call_ptr (f, args, ret, s, l) in 752 let g = Label.Map.add lbl' s g in 753 (g, rs) 754 | RTLabs.St_tailcall_ptr (f, args, s) -> 755 let (lbl', g, rs, args) = load_args args lbl g rs in 756 let s = RTLabs.St_tailcall_ptr (f, args, s) in 757 let g = Label.Map.add lbl' s g in 758 (g, rs) 759 | RTLabs.St_return (Some a) -> 760 let (lbl', g, rs, a) = load_arg a lbl g rs in 761 let s = RTLabs.St_return (Some a) in 762 let g = Label.Map.add lbl' s g in 763 (g, rs) 764 | _ -> (g, rs) in 669 fresh_t t (fun tmp -> 670 RTLabs.St_cst (tmp, c, Label.dummy) ^:: f (RTLabs.Reg tmp)) 671 | _ -> f a in 672 let rec load_args args f = match args with 673 | [] -> f [] 674 | a :: args -> 675 load_arg a (fun a -> load_args args (fun l -> f (a :: l))) in 676 let trans lbl = function 677 | RTLabs.St_op2(op, r, a1, a2, l) -> 678 load_arg a1 (fun a1 -> 679 load_arg a2 (fun a2 -> 680 RTLabs.St_op2 (op, r, a1, a2, l) ^:: bnil)) 681 | RTLabs.St_store(q, a1, a2, l) -> 682 load_arg a1 (fun a1 -> 683 load_arg a2 (fun a2 -> 684 RTLabs.St_store (q, a1, a2, l) ^:: bnil)) 685 | RTLabs.St_load (q, a, r, l) -> 686 load_arg a (fun a -> 687 RTLabs.St_load (q, a, r, l) ^:: bnil) 688 | RTLabs.St_call_id (f, args, ret, s, l) -> 689 load_args args (fun args -> 690 RTLabs.St_call_id (f, args, ret, s, l) ^:: bnil) 691 | RTLabs.St_tailcall_id (f, args, s) -> 692 load_args args (fun args -> 693 RTLabs.St_tailcall_id (f, args, s) ^:: bnil) 694 | RTLabs.St_call_ptr (f, args, ret, s, l) -> 695 load_args args (fun args -> 696 RTLabs.St_call_ptr (f, args, ret, s, l) ^:: bnil) 697 | RTLabs.St_tailcall_ptr (f, args, s) -> 698 load_args args (fun args -> 699 RTLabs.St_tailcall_ptr (f, args, s) ^:: bnil) 700 | RTLabs.St_return (Some a) -> 701 load_arg a (fun a -> 702 RTLabs.St_return (Some a) ^:: bnil) 703 | stmt -> stmt ^:: bnil in 704 let module T = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) in 765 705 let g = def.RTLabs.f_graph in 766 let (g, rs) = Label.Map.fold f g (g, []) in 767 let locals = List.rev_append rs def.RTLabs.f_locals in 768 { def with RTLabs.f_graph = g; RTLabs.f_locals = locals } 706 let fresh_reg def t = 707 let r = Register.fresh def.RTLabs.f_runiverse in 708 let locals = (r, t) :: def.RTLabs.f_locals in 709 ({ def with RTLabs.f_locals = locals }, r) in 710 let fresh_lbl () = Label.Gen.fresh def.RTLabs.f_luniverse in 711 let (def, g) = T.translate' fresh_lbl fresh_reg trans def g in 712 { def with RTLabs.f_graph = g } 769 713 770 714 let translate_internal def = -
Deliverables/D2.2/8051/src/common/label.ml
r1542 r1584 1 1 2 2 include StringTools 3 4 let dummy = "" 3 5 4 6 module ImpMap = struct -
Deliverables/D2.2/8051/src/common/label.mli
r1542 r1584 5 5 include StringSig.S 6 6 7 val dummy : t 8 7 9 (** Imperative label maps for use with Fix *) 8 10 module ImpMap : (Fix.IMPERATIVE_MAPS with type key = t) -
Deliverables/D2.2/8051/src/utilities/bList.ml
r1580 r1584 1 1 (** This module gives lists with internal binders. *) 2 2 3 type ('a, 'b) t =4 | BNil5 | BCons of 'a * ('a, 'b) t6 | BNew of ('b -> ('a, 'b) t)7 3 8 let (^::) x l = BCons (x, l) 4 type ('a, 'b, 'c) t = 5 | Nil 6 | Cons of 'a * ('a, 'b, 'c) t 7 | New of 'c * ('b -> ('a, 'b, 'c) t) 9 8 10 let rec (^@) l1 l2 = match l1 with 11 | BNil -> l2 12 | BCons (x, l1') -> BCons (x, l1' ^@ l2) 13 | BNew f -> BNew (fun x -> f x ^@ l2) 9 type ('a, 'b) t2 = ('a, 'b, unit) t 14 10 15 let (?^) f = BNew f 11 let rec append l1 l2 = match l1 with 12 | Nil -> l2 13 | Cons (x, l1') -> Cons (x, append l1' l2) 14 | New (t, f) -> New (t, fun x -> append (f x) l2) 16 15 17 let b_rev l =16 let rev l = 18 17 let rec rev_acc acc = function 19 | BNil -> acc 20 | BCons (x, l) -> rev_acc (BCons (x, acc)) l 21 | BNew f -> BNew (fun x -> rev_acc acc (f x)) in 22 rev_acc BNil l 18 | Nil -> acc 19 | Cons (x, l) -> rev_acc (Cons (x, acc)) l 20 | New (t, f) -> New (t, fun x -> rev_acc acc (f x)) in 21 rev_acc Nil l 22 23 let of_list l = List.fold_right (fun x l -> Cons (x, l)) l Nil 24 25 let rec compile fresh u l = match l with 26 | Nil -> (u, []) 27 | Cons (a, l) -> 28 let (u', l') = compile fresh u l in 29 (u', a :: l') 30 | New (t, f) -> 31 let (u', r) = fresh u t in 32 compile fresh u' (f r) 33 34 let compile2 fresh = 35 let fresh' u () = fresh u in 36 compile fresh' 37 38 let rec fold_left f f_new init = function 39 | Nil -> init 40 | Cons (a, l) -> fold_left f f_new (f init a) l 41 | New (t, f_l) -> f_new t (fun x -> fold_left f f_new init (f_l x)) 42 43 let rec fold_right f f_new l init = match l with 44 | Nil -> init 45 | Cons (a, l) -> f a (fold_right f f_new l init) 46 | New (t, f_l) -> f_new t (fun x -> fold_right f f_new (f_l x) init) 47 48 let rec concat = function 49 | [] -> Nil 50 | l :: ls -> append l (concat ls) 51 52 let rec fresh_ts ts f = match ts with 53 | [] -> f [] 54 | t :: ts -> New (t, fun x -> (fresh_ts ts (fun l -> f (x :: l)))) 55 56 let rec fresh_n n f = 57 if n <= 0 then f [] else 58 New ((), fun x -> (fresh_n (n - 1) (fun l -> f (x :: l)))) 59 60 module Notation = struct 61 62 let (^::) x l = Cons (x, l) 63 let (^@) = append 64 let bnil = Nil 65 let fresh f = New ((), f) 66 let fresh_n = fresh_n 67 let fresh_t t f = New (t, f) 68 let fresh_ts = fresh_ts 69 70 end -
Deliverables/D2.2/8051/src/utilities/bList.mli
r1580 r1584 1 1 (** This module gives lists with internal binders. *) 2 2 3 type ('a, 'b ) t =4 | BNil5 | BCons of 'a * ('a, 'b) t6 | BNew of ('b -> ('a, 'b) t)3 type ('a, 'b, 'c) t = 4 | Nil 5 | Cons of 'a * ('a, 'b, 'c) t 6 | New of 'c * ('b -> ('a, 'b, 'c) t) 7 7 8 val (^::) : 'a -> ('a, 'b) t -> ('a, 'b) t8 type ('a, 'b) t2 = ('a, 'b, unit) t 9 9 10 val (^@) : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t10 val rev : ('a, 'b, 'c) t -> ('a, 'b, 'c) t 11 11 12 val (?^) : ('b -> ('a, 'b) t) -> ('a, 'b) t12 val append : ('a, 'b, 'c) t -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t 13 13 14 val b_rev : ('a, 'b) t -> ('a, 'b) t 14 val of_list : 'a list -> ('a, 'b, 'c) t 15 16 val compile : ('u -> 'c -> 'u * 'b) -> 'u -> ('a, 'b, 'c) t -> 'u * 'a list 17 val compile2 : ('u -> 'u * 'b) -> 'u -> ('a, 'b) t2 -> 'u * 'a list 18 19 val fold_left : ('a -> 'b -> 'a) -> ('d -> ('c -> 'a) -> 'a) -> 'a -> 20 ('b, 'c, 'd) t -> 'a 21 22 val fold_right : 23 ('a -> 'b -> 'b) -> ('d -> ('c -> 'b) -> 'b) -> ('a, 'c, 'd) t -> 'b -> 'b 24 25 val concat : ('a, 'b, 'c) t list -> ('a, 'b, 'c) t 26 27 val fresh_n : int -> ('b list -> ('a, 'b) t2) -> ('a, 'b) t2 28 29 val fresh_ts : 'c list -> ('b list -> ('a, 'b, 'c) t) -> ('a, 'b, 'c) t 30 31 module Notation : sig 32 val (^::) : 'a -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t 33 val (^@) : ('a, 'b, 'c) t -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t 34 val bnil : ('a, 'b, 'c) t 35 val fresh : ('b -> ('a, 'b) t2) -> ('a, 'b) t2 36 val fresh_n : int -> ('b list -> ('a, 'b) t2) -> ('a, 'b) t2 37 val fresh_t : 'c -> ('b -> ('a, 'b, 'c) t) -> ('a, 'b, 'c) t 38 val fresh_ts : 'c list -> ('b list -> ('a, 'b, 'c) t) -> ('a, 'b, 'c) t 39 end -
Deliverables/D2.2/8051/src/utilities/graphUtilities.ml
r1580 r1584 82 82 NodeMap.filter is_reachable g 83 83 84 let rec put_rev freshl stmts src dests graph = 85 match stmts, dests with 86 | [], [next] -> (src, NodeMap.add src (skip next) graph) 87 | [last], _ -> 88 (src, NodeMap.add src (fill_succs last dests) graph) 89 | last :: stmts, _ -> 90 let new_l = freshl () in 91 let graph = NodeMap.add new_l (fill_succs last dests) graph in 92 (new_l, snd (put_rev freshl stmts src [new_l] graph)) 93 | _ -> 94 invalid_arg "successors of statement and translation do not match" 95 96 let replace freshl lbl stmts succs g = 97 let succs = match succs with 98 | Some x -> x 99 | None -> successors (NodeMap.find lbl g) in 100 101 snd (put_rev freshl (List.rev stmts) lbl succs g) 102 103 let replace' 104 (freshl : unit -> node) 105 (freshr : 'u -> 't -> 'u * 'r) 106 (lbl : node) 107 (stmts : (statement, 'r, 't) BList.t) 108 (succs : node list option) 109 (def : 'u) 110 (g : t) 111 : 'u * t = 112 let succs = match succs with 113 | Some x -> x 114 | None -> successors (NodeMap.find lbl g) in 115 let (def, l) = BList.compile freshr def stmts in 116 (def, snd (put_rev freshl l lbl succs g)) 117 118 let insert freshl lbl stmts g = 119 let stmt = NodeMap.find lbl g in 120 let succs = successors (NodeMap.find lbl g) in 121 put_rev freshl (stmt :: List.rev stmts) lbl succs g 122 123 let insert' freshl freshr lbl stmts def g = 124 let stmt = NodeMap.find lbl g in 125 let succs = successors (NodeMap.find lbl g) in 126 let (def, l) = BList.compile freshr def stmts in 127 let (lbl, g) = put_rev freshl (stmt :: l) lbl succs g in 128 (def, lbl, g) 129 84 130 end 85 131 … … 155 201 156 202 let translate_with_redirects' freshl freshr f def g = 157 158 let rec put_rev stmts src dests def graph = 159 match stmts, dests with 160 | BNil, [next] -> (def, Trg.NodeMap.add src (Trg.skip next) graph) 161 | BCons (last, BNil), _ -> 162 (def, Trg.NodeMap.add src (Trg.fill_succs last dests) graph) 163 | BCons (last, stmts), _ -> 164 let new_l = freshl () in 165 let graph = Trg.NodeMap.add new_l (Trg.fill_succs last dests) graph in 166 put_rev stmts src [new_l] def graph 167 | BNew f_stmts, _ -> 168 let (def, new_r) = freshr def in 169 let stmts = f_stmts new_r in 170 put_rev stmts src dests def graph 171 | _ -> 172 invalid_arg "successors of statement and translation do not match" in 173 174 let trans lbl stmt (def, graph) = 203 let f' def lbl stmt = 175 204 let (stmts, redirects) = f lbl stmt in 176 let succs = match redirects with 177 | Some x -> x 178 | None -> Src.successors stmt in 179 put_rev (b_rev stmts) lbl succs def graph in 180 181 Src.NodeMap.fold trans g (def, Trg.NodeMap.empty) 205 let (def, stmts) = BList.compile freshr def stmts in 206 (def, stmts, redirects) in 207 translate_with_redirects freshl f' def g 182 208 183 209 let translate' freshl freshr f = 184 210 let f' lbl stmt = (f lbl stmt, None) in 185 211 translate_with_redirects' freshl freshr f' 212 186 213 187 214 -
Deliverables/D2.2/8051/src/utilities/graphUtilities.mli
r1580 r1584 64 64 val dead_code_elim : G.t -> G.node -> G.t 65 65 66 val replace : (unit -> G.node) -> 67 G.node -> G.statement list -> G.node list option -> G.t -> G.t 68 69 val replace' : (unit -> G.node) -> ('u -> 't -> 'u * 'r) -> 70 G.node -> (G.statement, 'r, 't) BList.t -> G.node list option -> 71 'u -> G.t -> 'u * G.t 72 73 val insert : (unit -> G.node) -> 74 G.node -> G.statement list -> G.t -> G.node * G.t 75 76 val insert' : (unit -> G.node) -> ('u -> 't -> 'u * 'r) -> 77 G.node -> (G.statement, 'r, 't) BList.t -> 78 'u -> G.t -> 'u * G.node * G.t 79 80 66 81 end 67 82 … … 123 138 translation. 124 139 @see translate *) 125 val translate' : (unit -> node) -> ('u -> ' u * 'reg) ->126 (node -> Src.statement -> (Trg.statement, 'reg ) BList.t) ->140 val translate' : (unit -> node) -> ('u -> 't -> 'u * 'reg) -> 141 (node -> Src.statement -> (Trg.statement, 'reg, 't) BList.t) -> 127 142 'u -> Src.t -> 'u * Trg.t 128 143 … … 131 146 @see translate' 132 147 @see translate_with_redirect *) 133 val translate_with_redirects' : (unit -> node) -> ('u -> ' u * 'reg) ->148 val translate_with_redirects' : (unit -> node) -> ('u -> 't -> 'u * 'reg) -> 134 149 (node -> Src.statement -> 135 (Trg.statement, 'reg ) BList.t * node list option) ->150 (Trg.statement, 'reg, 't) BList.t * node list option) -> 136 151 'u -> Src.t -> 'u * Trg.t 137 152 -
Deliverables/D2.2/8051/src/utilities/miscPottier.ml
r818 r1584 1 1 2 let recmap3 f al bl cl =2 let map3 f al bl cl = 3 3 let f' ((a, b), c) = f a b c in 4 4 List.map f' (List.combine (List.combine al bl) cl) 5 6 let fold3_right f al bl cl = 7 let f' ((a, b), c) d = f a b c d in 8 List.fold_right f' (List.combine (List.combine al bl) cl) 5 9 6 10 let rec max_list = function … … 25 29 26 30 let rec make a n = 27 if n = 0 then []31 if n <= 0 then [] 28 32 else a :: (make a (n-1)) 33 34 let makei f n = 35 let rec app f k = 36 if k >= n then [] 37 else f k :: (app f (k + 1)) in 38 app f 0 29 39 30 40 let index_of x = … … 159 169 in 160 170 aux 171 172 173 let rec sublist l k h = 174 if h < k || h < 0 || k < 0 then 175 invalid_arg "sublist: invalid interval" 176 else 177 match k, h, l with 178 | 0, 0, _ -> [] 179 | 0, _, x :: l -> x :: sublist l 0 (h-1) 180 | _, _, x :: l -> sublist l (k-1) (h-1) 181 | _ -> invalid_arg "sublist: invalid interval" 182 183 let rec fill l n = 184 let k = List.length l in 185 if k = 0 then invalid_arg "fill: list empty" else 186 if n < 0 then invalid_arg "fill: negative argument" else 187 if n <= k then sublist l 0 n else 188 l @ fill l (n - k) -
Deliverables/D2.2/8051/src/utilities/miscPottier.mli
r818 r1584 10 10 size. *) 11 11 val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list 12 val fold3_right : ('a -> 'b -> 'c -> 'd -> 'd) -> 13 'a list -> 'b list -> 'c list -> 'd -> 'd 12 14 13 15 val max_list : 'a list -> 'a … … 16 18 17 19 val make: 'a -> int -> 'a list 20 21 val makei : (int -> 'a) -> int -> 'a list 18 22 19 23 val index_of : 'a -> 'a list -> int … … 84 88 85 89 val string_of_list: string -> ('a -> string) -> 'a list -> string 90 91 (* [sublist h k l] gives the sublist of [l] starting from index [h] to 92 [k] excluded. Can raise [Invalid_argument "sublist: invalid interval"]. *) 93 val sublist : 'a list -> int -> int -> 'a list 94 95 (* [fill l n] makes a list of length [n] using elements from [l], possibly 96 repeating it. Raises Invalid_argument if [n < 0] or [l = []]. *) 97 val fill : 'a list -> int -> 'a list 98
Note: See TracChangeset
for help on using the changeset viewer.