Changeset 1580
- Timestamp:
- Dec 1, 2011, 2:50:27 PM (9 years ago)
- Location:
- Deliverables/D2.2/8051/src
- Files:
-
- 12 added
- 13 edited
- 2 moved
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml
r1572 r1580 155 155 (print_statement stmt) 156 156 s in 157 ERTLUtilities.dfs_fold f c entry "" 157 let module U = GraphUtilities.Util(ERTLGraph) in 158 U.dfs_fold f c entry "" 158 159 (* Label.Map.fold f c "" *) 159 160 -
Deliverables/D2.2/8051/src/ERTL/liveness.ml
r1572 r1580 108 108 | St_op2 (I8051.Sub, r, _, _, _) -> 109 109 L.join (L.hsingleton I8051.carry) (L.psingleton r) 110 | St_op1 (I8051.Inc, r, _, _)111 110 | St_get_hdw (r, _, _) 112 111 | St_framesize (r, _) -
Deliverables/D2.2/8051/src/LIN/LINToASM.ml
r1568 r1580 76 76 | LIN.St_ind_0 i -> [`Index i ; `NOP (* TODO: hack! *)] 77 77 | LIN.St_ind_inc i -> [`Inc i ; `NOP (* TODO: hack! *)] 78 | LIN.St_int (r, 0) when I8051.eq_reg r I8051.a -> 79 [`CLR `A] 78 80 | LIN.St_int (r, i) -> 79 81 [`MOV (`U3 (I8051.reg_addr r, data_of_int i))] -
Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml
r1572 r1580 78 78 (print_statement stmt) 79 79 s in 80 LTLUtilities.dfs_fold f c entry "" 80 let module U = GraphUtilities.Util(LTLGraph) in 81 U.dfs_fold f c entry "" 81 82 (* Label.Map.fold f c "" *) 82 83 -
Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml
r1572 r1580 129 129 130 130 131 let print_graph n c =131 let print_graph n c entry = 132 132 let f lbl stmt s = 133 133 Printf.sprintf "%s%s: %s\n%s" … … 136 136 (print_statement stmt) 137 137 s in 138 Label.Map.fold f c "" 138 let module U = GraphUtilities.Util(RTLGraph) in 139 U.dfs_fold f c entry "" 139 140 140 141 … … 156 157 (n_spaces (n+2)) 157 158 def.RTL.f_exit 158 (print_graph (n+2) def.RTL.f_graph )159 (print_graph (n+2) def.RTL.f_graph def.RTL.f_entry) 159 160 160 161 -
Deliverables/D2.2/8051/src/RTL/RTLPrinter.mli
r486 r1580 1 1 2 2 (** This module provides a function to print [RTL] programs. *) 3 val print_statement : RTL.statement -> string 3 4 4 5 val print_program : RTL.program -> string -
Deliverables/D2.2/8051/src/RTLabs/RTLabsGraph.ml
r1572 r1580 1 1 (** this module provides some utilities relative to RTLabs graphs *) 2 3 type node = Label.t 4 type statement = RTLabs.statement 5 6 module NodeMap = Label.Map 7 module NodeSet = Label.Set 8 9 type t = RTLabs.graph 2 10 3 11 open RTLabs 4 12 5 type node = Label.t6 7 13 (** Successors of a statement *) 8 let s tatement_successors (stmt : statement) =14 let successors (stmt : statement) = 9 15 match stmt with 10 | St_return _ 16 | St_return _ 11 17 | St_tailcall_id _ 12 18 | St_tailcall_ptr _ -> … … 28 34 | St_jumptable (_, ls) -> ls 29 35 30 let count_statement_successors (stmt : statement) = 31 match stmt with 32 | St_return _ 33 | St_tailcall_id _ 34 | St_tailcall_ptr _ -> 0 35 | St_skip _ 36 | St_cost _ 37 | St_ind_0 _ 38 | St_ind_inc _ 39 | St_cst _ 40 | St_op1 _ 41 | St_op2 _ 42 | St_load _ 43 | St_store _ 44 | St_call_ptr _ 45 | St_call_id _ -> 1 46 | St_cond _ -> 2 47 | St_jumptable (_, ls) -> List.length ls 36 let skip lbl = St_skip lbl 48 37 49 (** computes a map binding the set of predecessors to each node. The domain 50 is guaranteed to be equal to the domain of graph *) 51 let compute_predecessors graph = 52 let add_to_preds pred map lbl = 53 let preds = 54 try 55 Label.Set.add pred (Label.Map.find lbl map) 56 with 57 | Not_found -> Label.Set.singleton pred in 58 Label.Map.add lbl preds map in 59 let add_predecessor lbl stmt map = 60 (* make sure the domain of the map will be equal to dom graph, adding *) 61 (* empty sets if need be *) 62 let map = if Label.Map.mem lbl map then map else 63 Label.Map.add lbl Label.Set.empty map in 64 List.fold_left (add_to_preds lbl) map (statement_successors stmt) in 65 Label.Map.fold add_predecessor graph Label.Map.empty 38 let fill_succs stmt succs = match stmt, succs with 39 | (St_return _ 40 | St_tailcall_id _ 41 | St_tailcall_ptr _) as inst, [] -> inst 42 | St_skip _, [lbl] -> St_skip lbl 43 | St_cost (cost_lbl, _), [lbl] -> St_cost (cost_lbl, lbl) 44 | St_ind_0 (i, _), [lbl] -> St_ind_0 (i, lbl) 45 | St_ind_inc (i, _), [lbl] -> St_ind_inc (i, lbl) 46 | St_cst (r, k, _), [lbl] -> St_cst (r, k, lbl) 47 | St_op1 (o, r, s, _), [lbl] -> St_op1 (o, r, s, lbl) 48 | St_op2 (o, r, a, b, _), [lbl] -> St_op2 (o, r, a, b, lbl) 49 | St_load (r, a, b, _), [lbl] -> St_load (r, a, b, lbl) 50 | St_store (a, b, c, _), [lbl] -> St_store (a, b, c, lbl) 51 | St_call_ptr (f, args, ret, s, _), [lbl] -> St_call_ptr (f, args, ret, s, lbl) 52 | St_call_id (f, args, ret, s, _), [lbl] -> St_call_id (f, args, ret, s, lbl) 53 | St_cond (r, _, _), [lbl1; lbl2] -> St_cond (r, lbl1, lbl2) 54 | St_jumptable (r, _), ls -> St_jumptable (r, ls) 55 | _ -> invalid_arg "fill_succs: provided successors do not match statement" 66 56 67 let compute_predecessor_lists graph = 68 let add_to_preds pred map lbl = 69 let preds = 70 try 71 pred :: Label.Map.find lbl map 72 with 73 | Not_found -> [pred] in 74 Label.Map.add lbl preds map in 75 let add_predecessors lbl stmt map = 76 (* make sure the domain of the map will be equal to dom graph, adding *) 77 (* empty sets if need be *) 78 let map = if Label.Map.mem lbl map then map else 79 Label.Map.add lbl [] map in 80 List.fold_left (add_to_preds lbl) map (statement_successors stmt) in 81 Label.Map.fold add_predecessors graph Label.Map.empty 82 83 let fill_labels stmt lbls = match stmt, lbls with 84 | St_return _, _ 85 | St_tailcall_id _, _ 86 | St_tailcall_ptr _, _ -> stmt 87 | St_skip _, lbl :: _ -> St_skip lbl 88 | St_cost (cost_lbl, _), lbl :: _ -> St_cost (cost_lbl, lbl) 89 | St_ind_0 (i, _), lbl :: _ -> St_ind_0 (i, lbl) 90 | St_ind_inc (i, _), lbl :: _ -> St_ind_inc (i, lbl) 91 | St_cst (r, c, _), lbl :: _ -> St_cst (r, c, lbl) 92 | St_op1 (op, r, s, _), lbl :: _ -> St_op1 (op, r, s, lbl) 93 | St_op2 (op, r, s, t, _), lbl :: _ -> St_op2 (op, r, s, t, lbl) 94 | St_load (q, r, s, _), lbl :: _ -> St_load (q, r, s, lbl) 95 | St_store (q, r, s, _), lbl :: _ -> St_store (q, r, s, lbl) 96 | St_call_ptr (r, args, ret, sg, _), lbl :: _ -> 97 St_call_ptr (r, args, ret, sg, lbl) 98 | St_call_id (i, args, ret, sg, _), lbl :: _ -> 99 St_call_id (i, args, ret, sg, lbl) 100 | St_cond (r, _, _), lbl1 :: lbl2 :: _ -> St_cond (r, lbl1, lbl2) 101 | St_jumptable (r, _), lbls -> St_jumptable (r, lbls) 102 | _ -> invalid_arg "fill_labels: not enough successors to fill" 103 104 (** [insert_in_between u g src tgt s] inserts [s] between [src] and [tgt]. 105 [tgt] should be a successor of [src], and the provided [s] should already be 106 linked to [tgt]. This function just generates a new node containing [s] 107 and updates [src]'s links to [tgt] to be pointing to this new node. 108 If [src] is linked to [tgt] multiple times, all such links are updated. *) 109 let insert_in_between 110 (fresh : unit -> node) 111 (g : graph) 112 (src : node) 113 (tgt : node) 114 (s : statement) 115 : Label.t * graph = 116 let new_lbl = fresh () in 117 let src_stmt = Label.Map.find src g in 118 let succs = statement_successors src_stmt in 119 let repl lbl = if lbl = tgt then new_lbl else lbl in 120 let new_succs = List.map repl succs in 121 let new_src_stmt = fill_labels src_stmt new_succs in 122 (new_lbl, Label.Map.add new_lbl s (Label.Map.add src new_src_stmt g)) 123 124 let dfs_fold 125 (f : node -> statement -> 'a -> 'a) 126 (g : graph) 127 (entry : node) 128 (init : 'a) 129 : 'a = 130 assert (Label.Map.mem entry g); 131 let rec process done_set = function 132 | [] -> init 133 | next :: worklist when Label.Set.mem next done_set -> 134 process done_set worklist 135 | next :: worklist -> 136 let stmt = Label.Map.find next g in 137 let succs = statement_successors stmt in 138 f next stmt (process (Label.Set.add next done_set) (succs @ worklist)) in 139 process Label.Set.empty [entry] 140 141 let dead_code_elim 142 (g : graph) 143 (entry : node) 144 : graph = 145 let add lbl _ = Label.Set.add lbl in 146 let reachable = dfs_fold add g entry Label.Set.empty in 147 let is_reachable x _ = Label.Set.mem x reachable in 148 Label.Map.filter is_reachable g 149 150 let dfs_iter 151 (f : node -> statement -> unit) 152 (g : graph) 153 (entry : node) 154 : unit = 155 assert (Label.Map.mem entry g); 156 let rec process done_set = function 157 | [] -> (); 158 | next :: worklist when Label.Set.mem next done_set -> 159 process done_set worklist 160 | next :: worklist -> 161 let stmt = Label.Map.find next g in 162 let succs = statement_successors stmt in 163 f next stmt; 164 process (Label.Set.add next done_set) (succs @ worklist) in 165 process Label.Set.empty [entry] 166 167 let computes_type_map 57 (** Exported helper functions *) 58 let compute_type_map 168 59 (f_def : internal_function) 169 60 : AST.sig_type Register.Map.t = 170 let types = Register.Map.empty in 61 let types = Register.Map.empty in 171 62 let add map (r, typ) = Register.Map.add r typ map in 172 63 let types = List.fold_left add types f_def.f_params in … … 176 67 | Some x -> add types x 177 68 178 (* the register modified by a node *)69 (* the register directly modified by a node *) 179 70 let modified_at_stmt stmt = 180 71 match stmt with … … 189 80 let modified_at (g : graph) (n : Label.t) : Register.t option = 190 81 modified_at_stmt (Label.Map.find n g) 191 -
Deliverables/D2.2/8051/src/RTLabs/RTLabsGraph.mli
r1569 r1580 1 open RTLabs2 1 3 type node = Label.t 2 include GraphUtilities.GraphType 3 with type node = Label.t 4 and type statement = RTLabs.statement 5 and module NodeMap = Label.Map 6 and module NodeSet = Label.Set 4 7 5 (** Successors of a statement*)6 val statement_successors : statement -> node list8 (** Compute a map from registers to their type in the function declaration. *) 9 val compute_type_map : RTLabs.internal_function -> AST.sig_type Register.Map.t 7 10 8 (** computes a map binding each node to its set of predecessors. The domain 9 is guaranteed to be equal to the domain of the input graph *) 10 val compute_predecessors : graph -> Label.Set.t Label.Map.t 11 (** The register directly modified in a statement *) 12 val modified_at_stmt : RTLabs.statement -> Register.t option 11 13 12 (** computes a map binding each node to its list of predecessors. The domain 13 is guaranteed to be equal to the domain of the input graph *) 14 val compute_predecessor_lists : graph -> Label.t list Label.Map.t 15 16 (** Fills the labels of the statement with ones provided as argument. If not 17 enough labels are provided it raises Invalid_arguement. If more than enough 18 labels are provided, exceeding labels are ignored *) 19 val fill_labels : statement -> Label.t list -> statement 20 21 (** Given a graph and an entry point, this function deletes all unreachable 22 nodes *) 23 val dead_code_elim : graph -> node -> graph 24 25 (** [insert_in_between u g src tgt s] inserts [s] between [src] and [tgt]. 26 [tgt] should be a successor of [src], and the provided [s] should already be 27 linked to [tgt]. This function just generates a new node containing [s] 28 and updates [src]'s links to [tgt] to be pointing to this new node. 29 If [src] is linked to [tgt] multiple times, all such links are updated. 30 The generated label is provided alongside the new graph. *) 31 val insert_in_between : 32 (unit -> node) -> graph -> node -> node -> statement -> Label.t * graph 33 34 (** [dfs_fold f g entry a] preforms a fold with function [f] and initial value 35 [a] doing a depth-first sweep of [g] from entry node [entry]. In particular 36 all unreachable nodes are ignored. *) 37 val dfs_fold : (node -> statement -> 'a -> 'a) -> graph -> node -> 'a -> 'a 38 39 (** [dfs_fold f g entry a] preforms an iteration of function [f] performing a 40 depth-first sweep of [g] from entry node [entry]. In particular 41 all unreachable nodes are ignored. *) 42 val dfs_iter : (node -> statement -> unit) -> graph -> node -> unit 43 44 (** Computes a map from register to their types in the function 45 TODO: are gloabl variables registers too? *) 46 val computes_type_map : internal_function -> AST.sig_type Register.Map.t 47 48 (** Tells what local register is directly modified by the statement, if any *) 49 val modified_at_stmt : statement -> Register.t option 50 51 (** [modified_at g l] is the same as [modified_at_stmt s] where [s] is the 52 statement in [g] at [l]. *) 53 val modified_at : graph -> node -> Register.t option 14 (** [modified_at g lbl] is equivalent to [modified_at_stmt stmt] 15 where [lbl] is mapped to [stmt] in [g]. 16 @see modified_at_stmt *) 17 val modified_at : RTLabs.graph -> Label.t -> Register.t option -
Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml
r1572 r1580 258 258 let f' lbl stmt (reach, s) = 259 259 (Label.Set.add lbl reach, f lbl stmt s) in 260 let module U = GraphUtilities.Util(RTLabsGraph) in 260 261 let (reachable, str) = 261 RTLabsUtilities.dfs_fold f' c entry (Label.Set.empty, "") in262 U.dfs_fold f' c entry (Label.Set.empty, "") in 262 263 let filter lbl _ = not (Label.Set.mem lbl reachable) in 263 264 let c_rest = Label.Map.filter filter c in -
Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml
r1572 r1580 705 705 add_graph lbl (RTL.St_return (find_local_env r lenv)) def 706 706 707 (* let remove_non_int_immediates def = *) 708 (* let load_arg a lbl g rs = match a with *) 709 (* | RTLabs.Reg r -> (lbl, g, rs, r) *) 710 (* | RTLabs.Imm ((AST.Cst_stack _ | AST.Cst_addrsymbol _) as c, t) -> *) 711 (* let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in *) 712 (* let new_r = Register.fresh def.RTLabs.f_runiverse in *) 713 (* let g = Label.Map.add lbl (RTLabs.St_cst (new_r, c, new_l)) g in *) 714 (* (new_l, g, (new_r, t) :: rs, new_r) in *) 715 (* let f lbl stmt (g, rs) = *) 716 (* match stmt with *) 717 (* | RTLabs.St_op2(op, r, a1, a2, l) -> *) 718 (* let (lbl', g, rs, r1) = load_arg a1 lbl g rs in *) 719 (* let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in *) 720 (* let s = RTLabs.St_op2 (op, r, RTLabs.Reg r1, RTLabs.Reg r2, l) in *) 721 (* let g = Label.Map.add lbl' s g in *) 722 (* (g, rs) *) 723 (* | RTLabs.St_store(q, a1, a2, l) -> *) 724 (* let (lbl', g, rs, r1) = load_arg a1 lbl g rs in *) 725 (* let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in *) 726 (* let s = RTLabs.St_store (q, RTLabs.Reg r1, RTLabs.Reg r2, l) in *) 727 (* let g = Label.Map.add lbl' s g in *) 728 (* (g, rs) *) 729 (* | RTLabs.St_load (q, a, r, l) -> *) 730 (* let (lbl', g, rs, r1) = load_arg a lbl g rs in *) 731 (* let s = RTLabs.St_load (q, RTLabs.Reg r1, r, l) in *) 732 (* let g = Label.Map.add lbl' s g in *) 733 (* (g, rs) *) 734 (* | _ -> (g, rs) in *) 735 (* let g = def.RTLabs.f_graph in *) 736 (* let (g, rs) = Label.Map.fold f g (g, []) in *) 737 (* let locals = List.rev_append rs def.RTLabs.f_locals in *) 738 (* { def with RTLabs.f_graph = g; RTLabs.f_locals = locals } *) 707 let remove_non_int_immediates def = 708 let load_arg a lbl g rs = match a with 709 | 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 765 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 } 739 769 740 770 let translate_internal def = 771 let def = remove_non_int_immediates def in 741 772 let runiverse = def.RTLabs.f_runiverse in 742 773 let lenv = -
Deliverables/D2.2/8051/src/RTLabs/constPropagation.ml
r1572 r1580 208 208 (types : sig_type Register.Map.t) 209 209 (graph : statement Label.Map.t) 210 (pred_table : Label. Set.t Label.Map.t)210 (pred_table : Label.t list Label.Map.t) 211 211 (lbl : Label.t) 212 212 (valu : F.valuation) 213 213 : F.property = 214 214 let pred_prop = (* the situation at the entry of the statement (in [valu]) *) 215 let f pr ed prop=215 let f prop pred = 216 216 L.join (valu pred) prop in 217 L abel.Set.fold f (Label.Map.find lbl pred_table) L.bottomin217 List.fold_left f L.bottom (Label.Map.find lbl pred_table) in 218 218 let type_of r = Register.Map.find r types in 219 219 match Label.Map.find lbl graph with … … 239 239 : F.valuation = 240 240 (* extract types of registers from the definition *) 241 let types = RTLabs Utilities.computes_type_map f_def in241 let types = RTLabsGraph.compute_type_map f_def in 242 242 243 243 let graph = f_def.f_graph in 244 245 let pred_table = RTLabsUtilities.compute_predecessors graph in 244 let pred_table = 245 let module U = GraphUtilities.Util(RTLabsGraph) in 246 U.compute_predecessor_lists graph in 246 247 247 248 F.lfp (semantics types graph pred_table) … … 268 269 | Reg i -> arg_from_reg prop types i 269 270 | _ as a -> a 271 272 let args_from_args prop types = 273 List.map (arg_from_arg prop types) 270 274 271 275 let copy i a l = match a with … … 304 308 (* we transform statements according to the valuation found out by analyze *) 305 309 (* We also turn branchings into redirections if the guard is constant. *) 306 let transform _statement310 let transform 307 311 (valu : F.valuation) 308 312 (types: sig_type Register.Map.t) 309 313 (p : Label.t) 310 : statement -> statement = function 311 | St_cst (i, (Cst_offset _ | Cst_sizeof _), next) -> 312 (* we are sure valu has a binding for i, we change the abstract 313 quantities into actual integers *) 314 St_cst (i, cst_of_value (L.find_cst i (valu p)), next) 315 | (St_op1 (_,i,_,next) | St_op2(_,i,_,_,next)) when L.is_cst i (valu p) -> 316 St_cst (i, cst_of_value (L.find_cst i (valu p)), next) 317 | St_op2 (op, i, a, b, l) -> 318 simpl_imm_op2 op i a b types (valu p) l 319 | St_load (q, a, j, l) -> 320 St_load(q, arg_from_arg (valu p) types a, j, l) 321 | St_store (q, a, b, l) -> 322 St_store (q, arg_from_arg (valu p) types a, 323 arg_from_arg (valu p) types b, l) 324 | St_cond (i, if_true, if_false) as s when L.is_cst i (valu p) -> 325 let s = match L.find_cst i (valu p) with 326 | L.V v when Mem.Value.is_false v -> St_skip if_false 327 | L.V _ | L.A _ -> St_skip if_true 328 | _ -> s in s 329 | St_return (Some a) -> 330 St_return (Some (arg_from_arg (valu p) types a)) 331 | St_call_id (f, args, ret, sg, l) -> 332 St_call_id (f, List.map (arg_from_arg (valu p) types) args, ret, sg, l) 333 | St_call_ptr (f, args, ret, sg, l) -> 334 St_call_ptr (f, List.map (arg_from_arg (valu p) types) args, ret, sg, l) 335 | St_tailcall_id (f, args, sg) -> 336 St_tailcall_id (f, List.map (arg_from_arg (valu p) types) args, sg) 337 | St_tailcall_ptr (f, args, sg) -> 338 St_tailcall_ptr (f, List.map (arg_from_arg (valu p) types) args, sg) 339 | stmt -> stmt 314 (stmt : statement) : statement list * Label.t list option = 315 match stmt with 316 | St_cst (i, (Cst_offset _ | Cst_sizeof _), next) -> 317 (* we are sure valu has a binding for i, we change the abstract 318 quantities into actual integers *) 319 ([St_cst (i, cst_of_value (L.find_cst i (valu p)), next)] , None) 320 | (St_op1 (_,i,_,next) | St_op2(_,i,_,_,next)) when L.is_cst i (valu p) -> 321 ([St_cst (i, cst_of_value (L.find_cst i (valu p)), next)], None) 322 | St_op2 (op, i, a, b, l) -> 323 ([simpl_imm_op2 op i a b types (valu p) l], None) 324 | St_load (q, a, j, l) -> 325 ([St_load(q, arg_from_arg (valu p) types a, j, l)], None) 326 | St_store (q, a, b, l) -> 327 ([St_store (q, arg_from_arg (valu p) types a, 328 arg_from_arg (valu p) types b, l)], None) 329 | St_cond (i, if_true, if_false) as s when L.is_cst i (valu p) -> 330 (match L.find_cst i (valu p) with 331 | L.V v when Mem.Value.is_false v -> ([], Some [if_false]) 332 | L.V _ | L.A _ -> ([], Some [if_true]) 333 | _ -> ([s], Some [if_true ; if_false])) 334 | St_return (Some a) -> 335 ([St_return (Some (arg_from_arg (valu p) types a))], None) 336 | St_call_id (f, args, ret, sg, l) -> 337 ([St_call_id (f, args_from_args (valu p) types args, ret, sg, l)], None) 338 | St_call_ptr (f, args, ret, sg, l) -> 339 ([St_call_ptr (f, args_from_args (valu p) types args, ret, sg, l)], None) 340 | St_tailcall_id (f, args, sg) -> 341 ([St_tailcall_id (f, args_from_args (valu p) types args, sg)], None) 342 | St_tailcall_ptr (f, args, sg) -> 343 ([St_tailcall_ptr (f, args_from_args (valu p) types args, sg)], None) 344 | stmt -> ([stmt], None) 340 345 341 346 let transform_int_function … … 344 349 let valu = analyze f_def in 345 350 (* we transform the graph according to the analysis *) 346 let types = RTLabsUtilities.computes_type_map f_def in 347 let graph = Label.Map.mapi (transform_statement valu types) f_def.f_graph in 348 (* and we eliminate resulting dead code *) 349 let graph = RTLabsUtilities.dead_code_elim graph f_def.f_entry in 351 let types = RTLabsGraph.compute_type_map f_def in 352 let module U = GraphUtilities.Util(RTLabsGraph) in 353 let module T = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) in 354 let trans = transform valu types in 355 let fresh () = Label.Gen.fresh f_def.f_luniverse in 356 let graph = T.translate_pure_with_redirects fresh trans f_def.f_graph in 357 let graph = U.dead_code_elim graph f_def.f_entry in 350 358 {f_def with f_graph = graph} 351 359 -
Deliverables/D2.2/8051/src/RTLabs/copyPropagation.ml
r1572 r1580 69 69 if Register.equal (copy_of r) (copy_of s) then copies_out else 70 70 Register.FlexMap.add r s (copies_out --* (Some r)) 71 | stmt -> copies_out --* RTLabs Utilities.modified_at_stmt stmt in71 | stmt -> copies_out --* RTLabsGraph.modified_at_stmt stmt in 72 72 L.big_meet copies_out (Label.Map.find lbl pred_table) 73 73 … … 78 78 let graph = f_def.f_graph in 79 79 80 let pred_table = RTLabsUtilities.compute_predecessor_lists graph in 80 let pred_table = 81 let module U = GraphUtilities.Util(RTLabsGraph) in 82 U.compute_predecessor_lists graph in 81 83 82 84 F.lfp (semantics graph pred_table) -
Deliverables/D2.2/8051/src/RTLabs/redundancyElimination.ml
r1572 r1580 2 2 common subexpression elimination and loop-invariant code motion. 3 3 This is a reformulation of material found in Muchnick, Advanced compiler 4 design and implementation. 5 Along the way we also perform a first rough liveness analysis. *) 4 design and implementation. *) 6 5 7 6 8 7 open RTLabs 9 8 open AST 9 10 module Trans = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) 11 module Util = GraphUtilities.Util(RTLabsGraph) 10 12 11 13 (* Notes: To move loop-invariant computation, peeling is needed. It would *) … … 15 17 (* array addresses. *) 16 18 17 (* ----- PHASE 0 : critical edge elimination ------ *) 18 19 (* a critical edge is one between a node with several successors and a node*) 20 (* with several predecessors. In order for the optimization to work best *) 21 (* these must be avoided, inserting an empty node in-between. *) 22 (* Note: maybe in our case we can avoid this, as branchings will have *) 23 (* emit cost nodes afterwards. To be checked. Empirically I haven't found *) 24 (* an example where this transformation really applies. *) 25 26 let count_predecessors 27 (g : graph) 28 : int Label.Map.t = 29 let f lbl s m = 30 let succs = RTLabsUtilities.statement_successors s in 31 let f' m succ = 32 try 33 Label.Map.add succ (1 + Label.Map.find succ m) m 34 with 35 | Not_found -> Label.Map.add succ 1 m in 36 let m = List.fold_left f' m succs in 37 if Label.Map.mem lbl m then m else Label.Map.add lbl 0 m in 38 Label.Map.fold f g Label.Map.empty 39 40 module LabelPairSet = Set.Make(struct 41 type t = Label.t * Label.t 42 let compare = compare 43 end) 44 45 let find_critical_edges (g : graph) : LabelPairSet.t = 46 let pred_count = count_predecessors g in 47 let add_if_2_preds l1 s l2 = 48 if Label.Map.find l2 pred_count < 2 then s else 49 LabelPairSet.add (l1, l2) s in 50 let f l stmt s = match stmt with 51 | St_cond(_, l1, l2) -> 52 add_if_2_preds l (add_if_2_preds l s l1) l2 53 | St_jumptable (_, ls) when List.length ls > 1 -> 54 List.fold_left (add_if_2_preds l) s ls 55 | _ -> s in 56 Label.Map.fold f g LabelPairSet.empty 57 58 (* note to self: there is a degenrate case that is not eliminated by the *) 59 (* following, namely (top to bottom) *) 60 (* src *) 61 (* / \ *) 62 (* | | *) 63 (* \ / *) 64 (* tgt *) 65 (* In this case the result will be *) 66 (* src *) 67 (* / \ *) 68 (* \ / *) 69 (* new *) 70 (* | *) 71 (* tgt *) 72 (* with two critical edges still in place. To be checked whether it *) 73 (* compromises the optimization, I think not *) 74 75 let critical_edge_elimination 76 (f_def : internal_function) 77 : internal_function = 78 let g = f_def.f_graph in 79 let fresh () = Label.Gen.fresh f_def.f_luniverse in 80 let critical_edges = find_critical_edges g in 81 let rem (src, tgt) g = 82 snd (RTLabsUtilities.insert_in_between fresh g src tgt (St_skip tgt)) in 83 { f_def with f_graph = LabelPairSet.fold rem critical_edges g } 19 (* Why I'm removing critical edge elimination: 20 It seems to me that the invariant about the presence of labels after 21 every branching prevents critical edges from appearing: every time a node 22 has more than one successor, all of its successors are cost emit statements. 23 24 We cannot jump directly to such a cost emittance from elsewhere. *) 25 26 (* (\* ----- PHASE 0 : critical edge elimination ------ *\) *) 27 28 (* (\* a critical edge is one between a node with several successors and a node*\) *) 29 (* (\* with several predecessors. In order for the optimization to work best *\) *) 30 (* (\* these must be avoided, inserting an empty node in-between. *\) *) 31 (* (\* Note: maybe in our case we can avoid this, as branchings will have *\) *) 32 (* (\* emit cost nodes afterwards. To be checked. Empirically I haven't found *\) *) 33 (* (\* an example where this transformation really applies. *\) *) 34 35 (* (\* a labels will not be in the domain of the map if it does not have any *) 36 (* predecessor. It will be bound to false if it has just one of them, *) 37 (* and it will bound to true is it has more than two *\) *) 38 (* let mark_multi_predecessor *) 39 (* (g : graph) *) 40 (* : bool Label.Map.t = *) 41 (* let f lbl s m = *) 42 (* let f' m succ = *) 43 (* try *) 44 (* if Label.Map.find succ m then *) 45 (* m *) 46 (* else *) 47 (* Label.Map.add succ true m *) 48 (* with *) 49 (* | Not_found -> Label.Map.add succ false m in *) 50 (* List.fold_left f' m (RTLabsGraph.successors s) in *) 51 (* Label.Map.fold f g Label.Map.empty *) 52 53 (* (\* will give the set of nodes that *) 54 (* 1) have more than one successor *) 55 (* 2) at least one of those successors has more *) 56 (* than one predecessor *\) *) 57 (* let remove_critical_edges fresh g = *) 58 (* let multi_pred_marks = mark_multi_predecessor g in *) 59 (* let is_multi_pred lbl = *) 60 (* try Label.Map.find lbl multi_pred_marks with *) 61 (* | Not_found -> false in *) 62 (* let trans () l = function *) 63 (* | St_cond (r, l1, l2) when is_multi_pred l1 || is_multi_pred l2 -> *) 64 (* ((), [St_cond (r, l, l)], [[] ; []], [[l1] ; [l2]]) *) 65 (* | St_jumptable (r, ls) *) 66 (* when List.length ls > 1 && List.exists is_multi_pred ls -> *) 67 (* let blocks = MiscPottier.make [] (List.length ls) in *) 68 (* let succs = List.map (fun l -> [l]) ls in *) 69 (* ((), [St_jumptable (r, [])], blocks, succs) *) 70 (* | stmt -> ((), [], [[stmt]], [RTLabsGraph.successors stmt]) in *) 71 (* snd (Trans.translate_general trans fresh () g) *) 72 73 (* let critical_edge_elimination *) 74 (* (f_def : internal_function) *) 75 (* : internal_function = *) 76 (* let g = f_def.f_graph in *) 77 (* let fresh () = Label.Gen.fresh f_def.f_luniverse in *) 78 (* { f_def with f_graph = remove_critical_edges fresh g } *) 84 79 85 80 (* Expressions, expression sets, and operations thereof *) … … 87 82 (* Load and store ops are not taken into account, maybe later *) 88 83 type expr = 89 (* | Cst of cst (* do we need to consider constants? maybe only big ones? *)*) 90 | UnOp of op1 * Register.t 91 | BinOp of op2 * argument * argument 92 93 let expr_of_stmt (s : statement) : expr option = match s with 94 (* | St_cst (_, c, _) -> Some (Cst c)*) 95 | St_op1 (op, _, s, _) when op <> Op_id -> Some (UnOp (op, s)) 96 | St_op2 (op, _, s, t, _) -> Some (BinOp (op, s, t)) 84 (* | Cst of cst (\* do we need to consider constants? only big ones? *\) *) 85 | UnOp of op1 * Register.t * AST.sig_type 86 | BinOp of op2 * argument * argument * AST.sig_type 87 88 let expr_of_stmt type_of (s : statement) : expr option = match s with 89 (* | St_cst (_, c, _) -> Some (Cst c) *) 90 | St_op1 (op, r, s, _) when op <> Op_id -> 91 Some (UnOp (op, s, type_of r)) 92 | St_op2 (op, r, s, t, _) -> Some (BinOp (op, s, t, type_of r)) 97 93 | _ -> None 98 94 99 let expr_of (g : graph) (n : Label.t) : expr option =100 expr_of_stmt (Label.Map.find n g)95 let expr_of type_of (g : graph) (n : Label.t) : expr option = 96 expr_of_stmt type_of (Label.Map.find n g) 101 97 102 98 (* the register modified by a node *) 103 let modified_at_stmt = RTLabs Utilities.modified_at_stmt104 105 let modified_at = RTLabs Utilities.modified_at99 let modified_at_stmt = RTLabsGraph.modified_at_stmt 100 101 let modified_at = RTLabsGraph.modified_at 106 102 107 103 (* registers on which the value computed at the statement depends, which are*) … … 186 182 | Some r -> 187 183 let filter = function 188 | UnOp (_, s ) when r = s -> false189 | BinOp (_, s, t ) when s = Reg r || t = Reg r -> false184 | UnOp (_, s, _) when r = s -> false 185 | BinOp (_, s, t, _) when s = Reg r || t = Reg r -> false 190 186 | _ -> true in 191 187 ExprSet.filter filter s … … 242 238 (* | Cst c -> 243 239 (RTLabsPrinter.print_cst c)*) 244 | UnOp (op, r) -> 245 (RTLabsPrinter.print_op1 op r) 246 | BinOp (op, r, s) -> 247 (RTLabsPrinter.print_op2 op r s) 248 249 let print_prop_pair (p : Fpair.property) = let (ant, nea) = p in 250 let f e = Printf.printf "%s, " (print_expr e) in 251 Printf.printf "{ "; 252 ExprSet.iter f ant; 253 Printf.printf "}; { "; 254 ExprSet.iter f nea; 255 Printf.printf "}\n" 240 | UnOp (op, r, t) -> 241 (RTLabsPrinter.print_op1 op r ^ " : " ^ Primitive.print_type t) 242 | BinOp (op, r, s, t) -> 243 (RTLabsPrinter.print_op2 op r s ^ " : " ^ Primitive.print_type t) 244 245 let print_prop_pair (p : Fpair.property) = 246 let (ant, nea) = p in 247 let f e = Printf.printf "%s, " (print_expr e) in 248 Printf.printf "{ "; 249 ExprSet.iter f ant; 250 Printf.printf "}; { "; 251 ExprSet.iter f nea; 252 Printf.printf "}\n" 256 253 257 254 let print_valu_pair (valu : Fpair.valuation) (g : graph) (entry : Label.t) = … … 259 256 Printf.printf "%s: " lbl; 260 257 print_prop_pair (valu lbl) in 261 RTLabsUtilities.dfs_iter f g entry258 Util.dfs_iter f g entry 262 259 263 260 let print_prop_sing (p : Fsing.property) = … … 271 268 Printf.printf "%s: " lbl; 272 269 print_prop_sing (valu lbl) in 273 RTLabsUtilities.dfs_iter f g entry270 Util.dfs_iter f g entry 274 271 275 272 … … 286 283 let semantics_ant_nea 287 284 (g : graph) 285 (type_of : Register.t -> AST.sig_type) 288 286 (pred_table : Label.t list Label.Map.t) 289 287 (lbl : Label.t) 290 288 (valu : Fpair.valuation) 291 289 : Fpair.property = 292 let succs = RTLabs Utilities.statement_successors (Label.Map.find lbl g) in290 let succs = RTLabsGraph.successors (Label.Map.find lbl g) in 293 291 let preds = Label.Map.find lbl pred_table in 294 292 … … 301 299 let ant_in = filter_unchanged (modified_at g lbl) ant_in in 302 300 (* ... and add the expression being calculated ... *) 303 let ant_in = ant_in ++* expr_of g lbl in301 let ant_in = ant_in ++* expr_of type_of g lbl in 304 302 305 303 (* non-earliest expressions at entry *) … … 314 312 let compute_anticipatable_and_non_earliest 315 313 (f_def : internal_function) 314 (type_of : Register.t -> AST.sig_type) 316 315 (pred_table : Label.t list Label.Map.t) 317 316 : Fpair.valuation = 318 317 319 Fpair.lfp (semantics_ant_nea f_def.f_graph pred_table)318 Fpair.lfp (semantics_ant_nea f_def.f_graph type_of pred_table) 320 319 321 320 (* ------------ PHASE 2 : delayedness and lateness ----------- *) … … 327 326 let semantics_delay 328 327 (g : graph) 328 (type_of : Register.t -> AST.sig_type) 329 329 (pred_table : Label.t list Label.Map.t) 330 330 (ant_nea : Fpair.valuation) … … 334 334 let preds = Label.Map.find lbl pred_table in 335 335 336 337 338 339 let rem_pred lbl' = valu lbl' --* expr_of g lbl' in336 (* delayed expressions at entry *) 337 (* take delayed expressions of predecessors which are not the expressions *) 338 (* of such predecessors... *) 339 let rem_pred lbl' = valu lbl' --* expr_of type_of g lbl' in 340 340 let delay_in = big_inter rem_pred preds in 341 341 (* ... and add in anticipatable and earliest expressions *) … … 345 345 let compute_delayed 346 346 (f_def : internal_function) 347 (type_of : Register.t -> AST.sig_type) 347 348 (pred_table : Label.t list Label.Map.t) 348 349 (ant_nea : Fpair.valuation) 349 350 : Fsing.valuation = 350 351 351 Fsing.lfp (semantics_delay f_def.f_graph pred_table ant_nea)352 Fsing.lfp (semantics_delay f_def.f_graph type_of pred_table ant_nea) 352 353 353 354 (* An expression is latest at p if it cannot be delayed further *) 354 let late (g : graph) (delay : Fsing.valuation) 355 let late 356 (g : graph) 357 (type_of : Register.t -> AST.sig_type) 358 (delay : Fsing.valuation) 355 359 : Fsing.valuation = fun lbl -> 356 360 let stmt = Label.Map.find lbl g in 357 let succs = RTLabs Utilities.statement_successors stmt in358 359 let eo = match expr_of g lbl with361 let succs = RTLabsGraph.successors stmt in 362 363 let eo = match expr_of type_of g lbl with 360 364 | Some e when ExprSet.mem e (delay lbl) -> Some e 361 365 | _ -> None in … … 373 377 let semantics_isolated_used 374 378 (g : graph) 379 (type_of : Register.t -> AST.sig_type) 375 380 (late : Fsing.valuation) 376 381 (lbl : Label.t) … … 379 384 380 385 let stmt = Label.Map.find lbl g in 381 let succs = RTLabs Utilities.statement_successors stmt in382 let f l = late l ++ (fst (valu l) --* expr_of g l) in386 let succs = RTLabsGraph.successors stmt in 387 let f l = late l ++ (fst (valu l) --* expr_of type_of g l) in 383 388 let isol = big_inter f succs in 384 389 … … 396 401 let compute_isolated_used 397 402 (f_def : internal_function) 403 (type_of : Register.t -> AST.sig_type) 398 404 (delayed : Fsing.valuation) 399 405 : Fexprid.valuation = … … 401 407 let graph = f_def.f_graph in 402 408 403 Fexprid.lfp (semantics_isolated_used graph (late graph delayed)) 409 Fexprid.lfp 410 (semantics_isolated_used graph type_of (late graph type_of delayed)) 404 411 405 412 (* expressions that are optimally placed at point p, without being isolated *) … … 408 415 late lbl -- isol lbl 409 416 410 (* mark instructions that are redundant and can be re moved*)411 let redundant g late isol lbl =412 match expr_of g lbl with417 (* mark instructions that are redundant and can be replaced by a copy *) 418 let redundant g type_of late isol lbl = 419 match expr_of type_of g lbl with 413 420 | Some e when ExprSet.mem e (isol lbl) -> 414 421 false … … 426 433 (*------ PHASE 4 : place expressions, remove reduntant ones -------------*) 427 434 428 let remove_redundant def is_redundant is_unused =429 let g = def.f_graph in430 let types = RTLabsUtilities.computes_type_map def in431 let f lbl stmt (g', s) =432 if is_unused lbl then433 let succ = List.hd (RTLabsUtilities.statement_successors stmt) in434 (Label.Map.add lbl (St_skip succ) g', s) else435 if is_redundant lbl then436 match modified_at_stmt stmt, expr_of_stmt stmt with437 | Some r, Some e ->438 let succ = List.hd (RTLabsUtilities.statement_successors stmt) in439 let (s, (tmp, _)) =440 try441 (s, ExprMap.find e s)442 with443 | Not_found ->444 let tmp = Register.fresh def.f_runiverse in445 let typ = Register.Map.find r types in446 let s = ExprMap.add e (tmp, typ) s in447 (s, (tmp, typ)) in448 let new_stmt = St_op1 (Op_id, r, tmp, succ) in449 (Label.Map.add lbl new_stmt g', s)450 | _ -> assert false451 else (g', s) in452 let (g, s) = Label.Map.fold f g (g, ExprMap.empty) in453 ({ def with f_graph = g }, s)454 455 435 let stmt_of_expr 456 436 (r : Register.t) … … 459 439 : statement = 460 440 match e with 461 (* | Cst c -> St_cst (r, c, l)*)462 | UnOp (op, s ) -> St_op1 (op, r, s, l)463 | BinOp (op, s, t ) -> St_op2 (op, r, s, t, l)464 465 let insert_after exprs redundants g freshl lbl next =466 let f e (next', g')=441 (* | Cst c -> St_cst (r, c, l) *) 442 | UnOp (op, s, _) -> St_op1 (op, r, s, l) 443 | BinOp (op, s, t, _) -> St_op2 (op, r, s, t, l) 444 445 let trans freshr type_of is_redundant is_unused optimal tmps lbl stmt = 446 let get_r expr tmps = 467 447 try 468 let (tmp, _) = ExprMap.find e redundants in 469 let opt_calc = stmt_of_expr tmp e next' in 470 RTLabsUtilities.insert_in_between freshl g' lbl next' opt_calc 448 (tmps, ExprMap.find expr tmps) 471 449 with 472 | Not_found -> (next', g') in 473 snd (ExprSet.fold f exprs (next, g)) 474 475 let insert_before exprs redundants g freshl lbl stmt = 476 let f e (stmt', g') = 477 try 478 let (tmp, _) = ExprMap.find e redundants in 479 let n_lbl = freshl () in 480 let opt_calc = stmt_of_expr tmp e n_lbl in 481 let g' = Label.Map.add n_lbl stmt' g' in 482 let g' = Label.Map.add lbl opt_calc g' in 483 (opt_calc, g') 484 with 485 | Not_found -> (stmt', g') in 486 snd (ExprSet.fold f exprs (stmt, g)) 487 488 let store_optimal_computation (def, redundants) optimal = 489 (* first add the temporaries' declarations *) 490 let f _ (r, typ) vars = (r, typ) :: vars in 491 let f_locals = ExprMap.fold f redundants def.f_locals in 492 493 (* now the actual replacement *) 494 let g = def.f_graph in 495 let freshl () = Label.Gen.fresh def.f_luniverse in 496 let f lbl stmt g' = 497 match stmt with 498 (* in case of cost emittance the optimal calculations are inserted *) 499 (* after, to preserve preciness *) 500 | St_cost (_, next) -> 501 insert_after (optimal lbl) redundants g' freshl lbl next 502 | _ -> 503 insert_before (optimal lbl) redundants g' freshl lbl stmt in 504 { def with f_locals = f_locals; f_graph = Label.Map.fold f g g } 505 450 | Not_found -> 451 let r = freshr () in 452 (ExprMap.add expr r tmps, r) in 453 let f expr (tmps, instrs) = 454 let (tmps, r) = get_r expr tmps in 455 (tmps, stmt_of_expr r expr lbl :: instrs) in 456 let (tmps, optimals) = ExprSet.fold f (optimal lbl) (tmps, []) in 457 match stmt, is_unused lbl, is_redundant lbl with 458 | St_cost (cost_lbl, next) as s, _, _ -> 459 (* in this case we place optimal calculations after the cost one *) 460 (tmps, s :: optimals) 461 | _, true, _ -> 462 (* here we can remove the statement altogether *) 463 (tmps, optimals) 464 | _, _, false -> 465 (tmps, optimals @ [stmt]) 466 | _, _, true -> 467 match modified_at_stmt stmt, expr_of_stmt type_of stmt with 468 | Some s, Some e -> 469 let (tmps, r) = get_r e tmps in 470 (tmps, optimals @ [St_op1 (Op_id, s, r, lbl)]) 471 | _ -> assert false (* if redundant must be an expression *) 472 473 let type_of_expr = function 474 | UnOp (_, _, t) -> t 475 | BinOp (_, _, _, t) -> t 476 477 let add_decls expr_regs decls = 478 let f e r decls = (r, type_of_expr e) :: decls in 479 ExprMap.fold f expr_regs decls 506 480 507 481 (* piecing it all together *) 508 482 let transform_internal f_def = 509 let pred_table = RTLabsUtilities.compute_predecessor_lists f_def.f_graph in 510 let ant_nea = compute_anticipatable_and_non_earliest f_def pred_table in 511 let delay = compute_delayed f_def pred_table ant_nea in 512 let late = late f_def.f_graph delay in 513 let isol_used = compute_isolated_used f_def delay in 483 let pred_table = Util.compute_predecessor_lists f_def.f_graph in 484 let type_table = RTLabsGraph.compute_type_map f_def in 485 let type_of r = Register.Map.find r type_table in 486 (* analysis *) 487 let ant_nea = 488 compute_anticipatable_and_non_earliest f_def type_of pred_table in 489 let delay = compute_delayed f_def type_of pred_table ant_nea in 490 let late = late f_def.f_graph type_of delay in 491 let isol_used = compute_isolated_used f_def type_of delay in 514 492 let isol = fun lbl -> fst (isol_used lbl) in 515 493 let used = fun lbl -> snd (isol_used lbl) in 516 494 let opt = optimal late isol in 517 let redn = redundant f_def.f_graph late isol in495 let redn = redundant f_def.f_graph type_of late isol in 518 496 let unusd = unused f_def.f_graph used in 519 let f lbl _ s = Register.Set.union (used lbl) s in 520 let regs_used = 521 RTLabsUtilities.dfs_fold f f_def.f_graph f_def.f_entry Register.Set.empty in 522 let filter (r, _) = Register.Set.mem r regs_used in 523 let f_def = { f_def with f_locals = List.filter filter f_def.f_locals } in 524 store_optimal_computation (remove_redundant f_def redn unusd) opt 525 497 (* end of analysis *) 498 let freshr () = Register.fresh f_def.f_runiverse in 499 let freshl () = Label.Gen.fresh f_def.f_luniverse in 500 let trans = trans freshr type_of redn unusd opt in 501 let expr_regs = ExprMap.empty in 502 let (expr_regs, g) = Trans.translate freshl trans expr_regs f_def.f_graph in 503 let d = add_decls expr_regs f_def.f_locals in 504 505 { f_def with f_locals = d ; f_graph = g } 526 506 527 507 let transform_funct = function -
Deliverables/D2.2/8051/src/clight/loopPeeling.ml
r1569 r1580 8 8 9 9 (* this function tells when to perform the optimization on a statement. It *) 10 (* should always return [false] when the optimization cannot be applied *) 10 (* should always return [false] when the optimization cannot be applied *) 11 11 let heuristics 12 12 (_ : heuristics_info) 13 14 15 16 13 : Clight.statement -> bool = function 14 | Clight.Swhile (Some _, _, _) | Clight.Sfor (Some _, _, _, _, _) 15 | Clight.Sdowhile (Some _, _, _) -> true 16 | _ -> false 17 17 18 18 let zero_sexpr = CostLabel.Sexpr(0,0) … … 21 21 22 22 let f_expr_reindex i s e expr_res = 23 24 25 26 27 23 match e, expr_res with 24 | Clight.Expr (Clight.Ecost (lbl, _), t), e::_ -> 25 let lbl = CostLabel.comp_index i s lbl in 26 Clight.Expr (Clight.Ecost (lbl, e), t) 27 | _ -> ClightFold.expr_fill_exprs e expr_res 28 28 29 29 (** compose the mapping i |--> s with all labels in a statement *) 30 30 let reindex_stmt i s = 31 31 let f_stmt stmt expr_res stmt_res = 32 33 32 match stmt, stmt_res with 33 | Clight.Scost(lbl, _), stmt' :: _ -> 34 34 let lbl = CostLabel.comp_index i s lbl in 35 36 35 Clight.Scost(lbl,stmt') 36 | _ -> ClightFold.statement_fill_subs stmt expr_res stmt_res in 37 37 ClightFold.statement2 (f_expr_reindex i s) f_stmt 38 38 … … 42 42 43 43 let labels_of = 44 45 46 47 48 49 50 44 let f_expr _ _ = () in 45 let f_stmt stmt _ res_stmts = 46 let s = match stmt with 47 | Clight.Slabel(lbl, _) -> Label.Set.singleton lbl 48 | _ -> Label.Set.empty in 49 List.fold_left Label.Set.union s res_stmts in 50 ClightFold.statement2 f_expr f_stmt 51 51 52 52 let create_fresh_labels fresh lbl_set = 53 54 55 53 let f_lbl lbl = Label.Map.add lbl (fresh ()) in 54 Label.Set.fold f_lbl lbl_set Label.Map.empty 55 56 56 let apply_label_map map = 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 57 let f_stmt stmt exprs stmts = 58 match stmt, stmts with 59 | Clight.Slabel (lbl, _), s :: _ -> 60 (* lbl must be in domain of map *) 61 Clight.Slabel (Label.Map.find lbl map, s) 62 | Clight.Sgoto lbl, _ -> 63 Clight.Sgoto ( 64 try 65 Label.Map.find lbl map 66 with 67 | Not_found -> (* means it is an outgoing goto *) 68 lbl) 69 | _ -> ClightFold.statement_fill_subs stmt exprs stmts in 70 ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt 71 72 72 let peel fresh info = 73 let f_stmt stmt exprs stmts = 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 (* put a guard before the (second and onwards) iteration of the loop *) 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 73 let f_stmt stmt exprs stmts = 74 if heuristics info stmt then 75 match stmt, exprs, stmts with 76 | Clight.Swhile (Some i, _, _), e :: _, s :: _ -> 77 (* we can suppose no label in stmt is target of a goto outside of stmt, *) 78 (* as loop is indexed and thus single entry. So we can freely rename *) 79 (* labels in stmt. Notice outgoing gotos are not changed *) 80 let label_map = create_fresh_labels fresh (labels_of s) in 81 let s_first = apply_label_map label_map s in 82 (* reindex to zero the copies of s and e *) 83 let s_first = reindex_stmt i zero_sexpr s_first in 84 let e_first = reindex_expr i zero_sexpr e in 85 (* reindex to successor the other copies of s and e *) 86 let s_next = reindex_stmt i succ_sexpr s in 87 let e_next = reindex_expr i succ_sexpr e in 88 (* rebuild the loop *) 89 let loop = Clight.Swhile(Some i, e_next, s_next) in 90 (* build the peeled loop *) 91 let peeled = Clight.Ssequence(s_first, loop) in 92 (* add the guard at the start *) 93 Clight.Sifthenelse(e_first, peeled, Clight.Sskip) 94 | Clight.Sdowhile (Some i, _, _), e :: _, s :: _ -> 95 (* we can suppose no label in stmt is target of a goto outside of stmt, *) 96 (* as loop is indexed and thus single entry. So we can freely rename *) 97 (* labels in stmt. *) 98 let label_map = create_fresh_labels fresh (labels_of s) in 99 let s_first = apply_label_map label_map s in 100 (* reindex to zero the copies of s and e *) 101 let s_first = reindex_stmt i zero_sexpr s_first in 102 let e_first = reindex_expr i zero_sexpr e in 103 (* reindex to successor the other copies of s and e *) 104 let s_next = reindex_stmt i succ_sexpr s in 105 let e_next = reindex_expr i succ_sexpr e in 106 (* rebuild the loop *) 107 let loop = Clight.Sdowhile(Some i, e_next, s_next) in 108 (* put a guard before the following iterations of the loop *) 109 let guarded_loop = Clight.Sifthenelse(e_first, loop, Clight.Sskip) in 110 (* build the peeled loop *) 111 Clight.Ssequence(s_first, guarded_loop) 112 | Clight.Sfor (Some i, _, _, _, _), e :: _, s1 :: s2 :: s3 ::_ -> 113 (* we can suppose no label in s3 is target of a goto outside of stmt, *) 114 (* as loop is indexed and thus single entry. So we can freely rename *) 115 (* labels in stmt. *) 116 (* IMPORTANT: I am supposing no labels are in s1 and s2 *) 117 let label_map = create_fresh_labels fresh (labels_of s3) in 118 let s3_first = apply_label_map label_map s3 in 119 (* reindex to zero the copies of s2, s3 and e *) 120 let s2_first = reindex_stmt i zero_sexpr s2 in 121 let s3_first = reindex_stmt i zero_sexpr s3_first in 122 let e_first = reindex_expr i zero_sexpr e in 123 (* reindex to successor the other copies of s2, s3 and e *) 124 let s2_next = reindex_stmt i succ_sexpr s2 in 125 let s3_next = reindex_stmt i succ_sexpr s3 in 126 let e_next = reindex_expr i succ_sexpr e in 127 (* rebuild the loop *) 128 let loop = Clight.Sfor(Some i, s2_first, e_next, s2_next, s3_next) in 129 (* build the peeled loop *) 130 let peeled = Clight.Ssequence(s3_first, loop) in 131 (* add the guard at the start *) 132 Clight.Ssequence(s1,Clight.Sifthenelse(e_first, peeled, Clight.Sskip)) 133 | _ -> assert false (* heuristics should have crossed out other cases *) 134 else ClightFold.statement_fill_subs stmt exprs stmts in 135 ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt 136 136 137 137 let peel_funct fresh info = function 138 139 140 141 138 | (id, Clight.Internal def) -> 139 let body = peel fresh info def.Clight.fn_body in 140 (id, Clight.Internal {def with Clight.fn_body = body}) 141 | _ as p -> p 142 142 143 143 let apply p = 144 145 146 147 {p with Clight.prog_funct = functs} 148 144 let fresh = ClightAnnotator.make_fresh "_l" p in 145 let info = mk_heuristics_info p in 146 let functs = List.map (peel_funct fresh info) p.Clight.prog_funct in 147 {p with Clight.prog_funct = functs} 148 149 149 open Languages 150 150 151 151 let trans = 152 (Clight, function (AstClight p) -> AstClight (apply p) | _ -> assert false) 153 152 (Clight, function (AstClight p) -> AstClight (apply p) | _ -> assert false) -
Deliverables/D2.2/8051/src/options.ml
r1546 r1580 120 120 RedundancyElimination.trans; 121 121 CopyPropagation.trans; 122 RedundancyElimination.trans 122 RedundancyElimination.trans; 123 RTLConstPropagation.trans; 124 SimplePeephole.trans 123 125 ],[ 124 126 LoopPeeling.trans … … 187 189 help_specify_opt_stage ~reind:true LoopPeeling.trans; 188 190 189 "-cst-prop", Arg.Unit (add_transformation ConstPropagation.trans), 191 "-cst-prop", Arg.Unit (add_transformations 192 ([ConstPropagation.trans; 193 RTLConstPropagation.trans], [])), 190 194 " Apply constant propagation."; 191 195 help_specify_opt_stage ConstPropagation.trans; 196 help_specify_opt_stage RTLConstPropagation.trans; 192 197 193 198 "-cpy-prop", Arg.Unit (add_transformation CopyPropagation.trans), … … 208 213 " Apply loop unrolling."; 209 214 help_specify_opt_stage ~reind:true (LoopUnrolling.trans ()); 215 216 "-peeph", Arg.Unit (add_transformation SimplePeephole.trans), 217 " Apply some basic peephole optimizations."; 218 help_specify_opt_stage (SimplePeephole.trans); 210 219 211 220 "-O", Arg.Unit (add_transformations basic_optimizations),
Note: See TracChangeset
for help on using the changeset viewer.