Changeset 1473 for Deliverables/D2.2
- Timestamp:
- Oct 28, 2011, 4:45:12 PM (9 years ago)
- Location:
- Deliverables/D2.2/8051-indexed-labels-branch/src
- Files:
-
- 8 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsPrinter.ml
r1340 r1473 45 45 46 46 let print_cmp = function 47 | AST.Cmp_eq -> " eq"48 | AST.Cmp_ne -> " ne"49 | AST.Cmp_gt -> " gt"50 | AST.Cmp_ge -> " ge"51 | AST.Cmp_lt -> " lt"52 | AST.Cmp_le -> " le"47 | AST.Cmp_eq -> "=" 48 | AST.Cmp_ne -> "!=" 49 | AST.Cmp_gt -> ">" 50 | AST.Cmp_ge -> ">=" 51 | AST.Cmp_lt -> "<" 52 | AST.Cmp_le -> "<=" 53 53 54 54 let rec print_size = function … … 83 83 Printf.sprintf "%d%s" size (string_of_signedness sign) 84 84 85 let print_op1 = function 85 let print_op1 op r = Printf.sprintf "%s %s" 86 (match op with 86 87 | AST.Op_cast (int_type, dest_size) -> 87 88 Printf.sprintf "int%sto%d" (string_of_int_type int_type) dest_size 88 | AST.Op_negint -> " negint"89 | AST.Op_notbool -> " notbool"90 | AST.Op_notint -> " notint"91 | AST.Op_id -> " id"89 | AST.Op_negint -> "-" 90 | AST.Op_notbool -> "!" 91 | AST.Op_notint -> "!i" 92 | AST.Op_id -> "" 92 93 | AST.Op_ptrofint -> "ptrofint" 93 | AST.Op_intofptr -> "intofptr" 94 95 let print_op2 = function 96 | AST.Op_add -> "add" 97 | AST.Op_sub -> "sub" 98 | AST.Op_mul -> "mul" 99 | AST.Op_div -> "div" 94 | AST.Op_intofptr -> "intofptr") 95 (print_reg r) 96 97 let print_op2 op r s = Printf.sprintf "%s %s %s" 98 (print_reg r) 99 (match op with 100 | AST.Op_add -> "+" 101 | AST.Op_sub -> "-" 102 | AST.Op_mul -> "*" 103 | AST.Op_div -> "/" 100 104 | AST.Op_divu -> "/u" 101 105 | AST.Op_mod -> "mod" … … 104 108 | AST.Op_or -> "or" 105 109 | AST.Op_xor -> "xor" 106 | AST.Op_shl -> " shl"107 | AST.Op_shr -> " shr"108 | AST.Op_shru -> " shru"110 | AST.Op_shl -> "<<" 111 | AST.Op_shr -> ">>" 112 | AST.Op_shru -> ">>u" 109 113 | AST.Op_cmp cmp -> print_cmp cmp 110 | AST.Op_addp -> " addp"111 | AST.Op_subp -> " subp"112 | AST.Op_subpp -> " subpp"114 | AST.Op_addp -> "+p" 115 | AST.Op_subp -> "-p" 116 | AST.Op_subpp -> "-pp" 113 117 | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p" 114 | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u" 118 | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u") 119 (print_reg s) 115 120 116 121 … … 143 148 Printf.sprintf "increment %d --> %s" i lbl 144 149 | RTLabs.St_cst (destr, cst, lbl) -> 145 Printf.sprintf " imm %s,%s --> %s"150 Printf.sprintf "%s := %s --> %s" 146 151 (print_reg destr) 147 152 (print_cst cst) 148 153 lbl 149 154 | RTLabs.St_op1 (op1, destr, srcr, lbl) -> 150 Printf.sprintf "%s %s, %s --> %s" 151 (print_op1 op1) 155 Printf.sprintf "%s := %s --> %s" 152 156 (print_reg destr) 153 (print_regsrcr)157 (print_op1 op1 srcr) 154 158 lbl 155 159 | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) -> 156 Printf.sprintf "%s %s, %s, %s --> %s" 157 (print_op2 op2) 160 Printf.sprintf "%s := %s --> %s" 158 161 (print_reg destr) 159 (print_reg srcr1) 160 (print_reg srcr2) 162 (print_op2 op2 srcr1 srcr2) 161 163 lbl 162 164 | RTLabs.St_load (q, addr, destr, lbl) -> 163 Printf.sprintf "load %s, %s, %s --> %s" 165 Printf.sprintf "%s := *(%s) %s --> %s" 166 (print_reg destr) 164 167 (Memory.string_of_quantity q) 165 168 (print_reg addr) 166 (print_reg destr)167 169 lbl 168 170 | RTLabs.St_store (q, addr, srcr, lbl) -> 169 Printf.sprintf " store %s, %s,%s --> %s"170 171 Printf.sprintf "*(%s)%s := %s --> %s" 172 (Memory.string_of_quantity q) 171 173 (print_reg addr) 172 174 (print_reg srcr) 173 175 lbl 174 | RTLabs.St_call_id (f, args, res, sg, lbl) -> 175 Printf.sprintf "call \"%s\", %s, %s: %s --> %s" 176 f 176 | RTLabs.St_call_id (f, args, Some r, sg, lbl) -> 177 Printf.sprintf "%s := \"%s\"(%s) : %s --> %s" 178 (print_reg r) 179 f 177 180 (print_args args) 178 (print_oreg res)179 181 (Primitive.print_sig sg) 180 182 lbl 181 | RTLabs.St_call_ptr (f, args, res, sg, lbl) -> 182 Printf.sprintf "call_ptr %s, %s, %s: %s --> %s" 183 (print_reg f) 184 (print_args args) 185 (print_oreg res) 186 (Primitive.print_sig sg) 187 lbl 183 | RTLabs.St_call_id (f, args, None, sg, lbl) -> 184 Printf.sprintf "\"%s\"(%s) : %s --> %s" 185 f 186 (print_args args) 187 (Primitive.print_sig sg) 188 lbl 189 | RTLabs.St_call_ptr (f, args, Some r, sg, lbl) -> 190 Printf.sprintf "%s := *%s (%s) : %s --> %s" 191 (print_reg r) 192 (print_reg f) 193 (print_args args) 194 (Primitive.print_sig sg) 195 lbl 196 | RTLabs.St_call_ptr (f, args, None, sg, lbl) -> 197 Printf.sprintf "*%s (%s) : %s --> %s" 198 (print_reg f) 199 (print_args args) 200 (Primitive.print_sig sg) 201 lbl 188 202 | RTLabs.St_tailcall_id (f, args, sg) -> 189 Printf.sprintf "tailcall \"%s\" , %s: %s"203 Printf.sprintf "tailcall \"%s\" (%s) : %s" 190 204 f 191 205 (print_args args) 192 206 (Primitive.print_sig sg) 193 207 | RTLabs.St_tailcall_ptr (f, args, sg) -> 194 Printf.sprintf "tailcall _ptr \"%s\", %s: %s"208 Printf.sprintf "tailcall *%s (%s) : %s" 195 209 (print_reg f) 196 210 (print_args args) … … 230 244 231 245 232 let print_graph n c =246 let print_graph n c entry = 233 247 let f lbl stmt s = 234 248 Printf.sprintf "%s%s: %s\n%s" … … 237 251 (print_statement stmt) 238 252 s in 239 Label.Map.fold f c "" 240 241 253 let f' lbl stmt (reach, s) = 254 (Label.Set.add lbl reach, f lbl stmt s) in 255 let (reachable, str) = 256 RTLabsUtilities.dfs_fold f' c entry (Label.Set.empty, "") in 257 let filter lbl _ = not (Label.Set.mem lbl reachable) in 258 let c_rest = Label.Map.filter filter c in 259 if Label.Map.is_empty c_rest then str else 260 let str' = Label.Map.fold f c_rest "" in 261 str ^ "DEAD NODES:\n" ^ str' 262 242 263 let print_internal_decl n f def = 243 264 … … 257 278 (n_spaces (n+2)) 258 279 def.RTLabs.f_exit 259 (print_graph (n+2) def.RTLabs.f_graph )280 (print_graph (n+2) def.RTLabs.f_graph def.RTLabs.f_entry) 260 281 261 282 -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsPrinter.mli
r740 r1473 4 4 val print_statement : RTLabs.statement -> string 5 5 6 val print_cst : AST.cst -> string 7 8 val print_op1 : AST.op1 -> Register.t -> string 9 10 val print_op2 : AST.op2 -> Register.t -> Register.t -> string 11 6 12 val print_program : RTLabs.program -> string -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsUtilities.ml
r1468 r1473 9 9 match stmt with 10 10 | St_return _ 11 12 13 11 | St_tailcall_id _ 12 | St_tailcall_ptr _ -> 13 [] 14 14 | St_skip l 15 15 | St_cost (_, l) … … 28 28 | St_jumptable (_, ls) -> ls 29 29 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 48 30 49 (** computes a map binding the set of predecessors to each node. The domain 31 50 is guaranteed to be equal to the domain of graph *) 32 51 let compute_predecessors graph = 33 52 let add_to_preds pred map lbl = 34 53 let preds = 35 54 try … … 39 58 Label.Map.add lbl preds map in 40 59 let add_predecessor lbl stmt map = 41 42 60 (* make sure the domain of the map will be equal to dom graph, adding *) 61 (* empty sets if need be *) 43 62 let map = if Label.Map.mem lbl map then map else 44 45 63 Label.Map.add lbl Label.Set.empty map in 64 List.fold_left (add_to_preds lbl) map (statement_successors stmt) in 46 65 Label.Map.fold add_predecessor graph Label.Map.empty 47 66 48 let dead_code_elim 49 (g : graph) 50 (entry : node) 51 : graph = 52 let marked = Label.Set.empty in 53 let rec process marked = function 54 | [] -> marked 55 | next :: worklist -> 56 if Label.Set.mem next marked then process marked worklist else 57 let marked = Label.Set.add next marked in 58 let succs = statement_successors (Label.Map.find next g) in 59 let worklist = succs @ worklist in 60 process marked worklist in 61 let marked = process marked [entry] in 62 let is_marked x _ = Label.Set.mem x marked in 63 Label.Map.filter is_marked g 64 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. *) 65 109 let insert_in_between 66 ( u : Label.Gen.universe)110 (fresh : unit -> node) 67 111 (g : graph) 68 112 (src : node) 69 113 (tgt : node) 70 114 (s : statement) 71 : graph = assert false (* to be implemented *) 72 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 168 (f_def : internal_function) 169 : AST.sig_type Register.Map.t = 170 let types = Register.Map.empty in 171 let add map (r, typ) = Register.Map.add r typ map in 172 let types = List.fold_left add types f_def.f_params in 173 let types = List.fold_left add types f_def.f_locals in 174 match f_def.f_result with 175 | None -> types 176 | Some x -> add types x -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsUtilities.mli
r1468 r1473 6 6 val statement_successors : statement -> node list 7 7 8 (** computes a map binding the set of predecessors to each node. The domain9 is guaranteed to be equal to the domain of graph *)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 10 val compute_predecessors : graph -> Label.Set.t Label.Map.t 11 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 11 20 12 21 (** Given a graph and an entry point, this function deletes all unreachable … … 15 24 16 25 (** [insert_in_between u g src tgt s] inserts [s] between [src] and [tgt]. 17 [tgt] must be a successor of [src], and the provided [s] should already be 18 linked to [tgt]. This function just generates a new node containing [s] 19 and updates [src]'s links to [tgt] to be pointing to this new node. 20 If [src] is linked to [tgt] multiple times, all such links are updated. *) 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. *) 21 31 val insert_in_between : 22 Label.Gen.universe -> graph -> node -> node -> statement -> graph32 (unit -> node) -> graph -> node -> node -> statement -> Label.t * graph 23 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 -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/constPropagation.ml
r1468 r1473 141 141 : F.valuation = 142 142 (* extract types of registers from the definition *) 143 let types = Register.Map.empty in 144 let add map (r, typ) = Register.Map.add r typ map in 145 let types = List.fold_left add types f_def.f_params in 146 let types = List.fold_left add types f_def.f_locals in 147 let types = match f_def.f_result with 148 | None -> types 149 | Some x -> add types x in 150 143 let types = RTLabsUtilities.computes_type_map f_def in 144 151 145 let graph = f_def.f_graph in 152 146 -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/redundancyElimination.ml
r1468 r1473 1 (** This module implements partial redundancy elimination, which subsumes 2 common subexpression elimination and loop-invariant code motion. 3 This is a reformulation of material found in Muchnick, Advanced compiler 4 design and implementation. *) 5 1 6 open RTLabs 2 7 open AST … … 9 14 let error_shift () = error "Shift operations not supported." 10 15 11 type expr = 12 | UnOp of op1 * Register.t 13 | BinOp of op2 * Register.t * Register.t 16 (* ----- PHASE 0 : critical edge elimination ------ *) 17 18 (* a critical edge is one between a node with several successors and a node*) 19 (* with several predecessors. In order for the optimization to work best *) 20 (* these must be avoided, inserting an empty node in-between. *) 21 (* Note: maybe in our case we can avoid this, as branchings will have *) 22 (* emit cost nodes afterwards. To be checked. *) 14 23 15 24 let count_predecessors 16 25 (g : graph) 17 : int Label.Map.t = 18 let f lbl s m = 19 let succs = RTLabsUtilities.statement_successors s in 20 let f' m succ = 21 try 22 Label.Map.add succ (1 + Label.Map.find succ m) m 23 with 24 | Not_found -> Label.Map.add succ 1 m in 25 let m = List.fold_left f' m succs in 26 if Label.Map.mem lbl m then m else Label.Map.add lbl 0 m in 27 Label.Map.fold f g Label.Map.empty 28 29 (* the following functions are in fact useless!! Levaing it here as I will*) 30 (* probably reuse some of this code elsewhere *) 31 32 let erase_critical 33 (u : Label.Gen.universe) 34 (g : graph) 35 (pred_count : int Label.Map.t) 36 (src : Label.t) 37 (tgt : Label.t) 38 : bool * Label.t * graph = 39 if Label.Map.find tgt pred_count < 2 then 40 (false, tgt, g) 41 else 42 let lbl = Label.Gen.fresh u in 43 let g = Label.Map.add lbl (St_skip tgt) g in 44 (true, lbl, g) 26 : int Label.Map.t = 27 let f lbl s m = 28 let succs = RTLabsUtilities.statement_successors s in 29 let f' m succ = 30 try 31 Label.Map.add succ (1 + Label.Map.find succ m) m 32 with 33 | Not_found -> Label.Map.add succ 1 m in 34 let m = List.fold_left f' m succs in 35 if Label.Map.mem lbl m then m else Label.Map.add lbl 0 m in 36 Label.Map.fold f g Label.Map.empty 37 38 module LabelPairSet = Set.Make(struct 39 type t = Label.t * Label.t 40 let compare = compare 41 end) 42 43 let find_critical_edges (g : graph) : LabelPairSet.t = 44 let pred_count = count_predecessors g in 45 let add_if_2_preds l1 s l2 = 46 if Label.Map.find l2 pred_count < 2 then s else 47 LabelPairSet.add (l1, l2) s in 48 let f l stmt s = match stmt with 49 | St_cond(_, l1, l2) -> 50 add_if_2_preds l (add_if_2_preds l s l1) l2 51 | St_jumptable (_, ls) when List.length ls > 1 -> 52 List.fold_left (add_if_2_preds l) s ls 53 | _ -> s in 54 Label.Map.fold f g LabelPairSet.empty 55 56 (* note to self: there is a degenrate case that is not eliminated by the *) 57 (* following, namely (top to bottom) *) 58 (* src *) 59 (* / \ *) 60 (* | | *) 61 (* \ / *) 62 (* tgt *) 63 (* In this case the result will be *) 64 (* src *) 65 (* / \ *) 66 (* \ / *) 67 (* new *) 68 (* | *) 69 (* tgt *) 70 (* with two critical edges still in place. To be checked whether it *) 71 (* compromises the optimization, I think not *) 45 72 46 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 let critical_edges = find_critical_edges g in 79 let rem (src, tgt) g = 80 snd (RTLabsUtilities.insert_in_between fresh g src tgt (St_skip tgt)) in 81 { f_def with f_graph = LabelPairSet.fold rem critical_edges g } 82 83 (* Expressions, expression sets, and operations thereof *) 84 85 (* Load and store ops are not taken into account, maybe later *) 86 type expr = 87 (* | Cst of cst (* do we need to consider constants? maybe only big ones? *)*) 88 | UnOp of op1 * Register.t 89 | BinOp of op2 * Register.t * Register.t 90 91 let expr_of_stmt (s : statement) : expr option = match s with 92 (* | St_cst (_, c, _) -> Some (Cst c)*) 93 | St_op1 (op, _, s, _) -> Some (UnOp (op, s)) 94 | St_op2 (op, _, s, t, _) -> Some (BinOp (op, s, t)) 95 | _ -> None 96 97 let expr_of (g : graph) (n : Label.t) : expr option = 98 expr_of_stmt (Label.Map.find n g) 99 100 (* the register modified by a node *) 101 let modified_at_stmt stmt = 102 match stmt with 103 | St_op1 (_, r, _, _) 104 | St_op2 (_, r, _, _, _) 105 | St_cst (r, _, _) 106 | St_load (_, r, _, _) 107 | St_call_id (_, _, Some r, _, _) 108 | St_call_ptr (_, _, Some r, _, _) -> Some r 109 | _ -> None 110 111 let modified_at (g : graph) (n : Label.t) : Register.t option = 112 modified_at_stmt (Label.Map.find n g) 113 114 module ExprOrdered = struct 115 type t = expr 116 let compare = compare 117 end 118 119 module ExprSet = Set.Make(ExprOrdered) 120 module ExprMap = Map.Make(ExprOrdered) 121 122 type expr_set = ExprSet.t 123 124 let ( ^^ ) = ExprSet.inter 125 126 let ( ++ ) = ExprSet.union 127 128 let ( ++* ) s = function 129 | None -> s 130 | Some e -> ExprSet.add e s 131 132 let ( --* ) s = function 133 | None -> s 134 | Some e -> ExprSet.remove e s 135 136 let ( -- ) = ExprSet.diff 137 138 let big_inter (f : Label.t -> ExprSet.t) (ls : Label.t list) : ExprSet.t = 139 (* generalized intersection, but in case of empty list it is empty *) 140 match ls with 141 | [] -> ExprSet.empty 142 (* these two cases are singled out for speed, as they will be common *) 143 | [l] -> f l 144 | [l1 ; l2] -> f l1 ^^ f l2 145 | l :: ls -> 146 let inter s l' = s ^^ f l' in 147 List.fold_left inter (f l) ls 148 149 let filter_unchanged (r : Register.t option) (s : expr_set) : expr_set = 150 match r with 151 | None -> s 152 | Some r -> 153 let filter = function 154 | UnOp (_, s) when r = s -> false 155 | BinOp (_, s, t) when r = s || r = t -> false 156 | _ -> true in 157 ExprSet.filter filter s 158 159 module Lpair = struct 160 161 (* A property is a pair of sets of expressions. *) 162 type property = expr_set * expr_set 163 164 let bottom = (ExprSet.empty, ExprSet.empty) 165 166 let equal (ant1, nea1) (ant2, nea2) = 167 ExprSet.equal ant1 ant2 && ExprSet.equal nea1 nea2 168 169 let is_maximal _ = false 170 171 end 172 173 module Lsing = struct 174 175 (* A property is a set of expressions. *) 176 type property = expr_set 177 178 let bottom = ExprSet.empty 179 180 let equal = ExprSet.equal 181 182 let is_maximal _ = false 183 184 end 185 186 module Fpair = Fix.Make (Label.ImpMap) (Lpair) 187 188 module Fsing = Fix.Make (Label.ImpMap) (Lsing) 189 190 (* printing tools to debug *) 191 192 let print_expr = function 193 (* | Cst c -> 194 (RTLabsPrinter.print_cst c)*) 195 | UnOp (op, r) -> 196 (RTLabsPrinter.print_op1 op r) 197 | BinOp (op, r, s) -> 198 (RTLabsPrinter.print_op2 op r s) 199 200 let print_prop_pair (p : Fpair.property) = let (ant, nea) = p in 201 let f e = Printf.printf "%s, " (print_expr e) in 202 Printf.printf "{ "; 203 ExprSet.iter f ant; 204 Printf.printf "}; { "; 205 ExprSet.iter f nea; 206 Printf.printf "}\n" 207 208 let print_valu_pair (valu : Fpair.valuation) (g : graph) (entry : Label.t) = 209 let f lbl _ = 210 Printf.printf "%s: " lbl; 211 print_prop_pair (valu lbl) in 212 RTLabsUtilities.dfs_iter f g entry 213 214 let print_prop_sing (p : Fsing.property) = 215 let f e = Printf.printf "%s, " (print_expr e) in 216 Printf.printf "{ "; 217 ExprSet.iter f p; 218 Printf.printf "}\n" 219 220 let print_valu_sing (valu : Fsing.valuation) (g : graph) (entry : Label.t) = 221 let f lbl _ = 222 Printf.printf "%s: " lbl; 223 print_prop_sing (valu lbl) in 224 RTLabsUtilities.dfs_iter f g entry 225 226 227 (* ----- PHASE 1 : Anticipatability and erliestness ------ *) 228 (* An expression e is anticipatable at point p if every path from p contains *) 229 (* a computation of e and evaluating e at p holds the same result as all such *) 230 (* computations. *) 231 (* An expression e is earliest at point p if there is no computation of e *) 232 (* preceding p giving the same value. *) 233 (* We will compute anticipatable expressions and *non*-earliest ones for every*) 234 (* point with a single invocation to a fixpoint calculation. *) 235 236 237 let semantics_ant_nea 47 238 (g : graph) 48 (u : Label.Gen.universe) 49 : graph = 50 (* a critical edge is one between a node with several successors and one *) 51 (* with several predecessors *) 52 let pred_count = count_predecessors g in 53 let f l stmt g = 54 match stmt with 55 | St_cond(r, l1, l2) -> 56 let (b1, l1, g) = erase_critical u g pred_count l l1 in 57 let (b2, l2, g) = erase_critical u g pred_count l l2 in 58 if b1 || b2 then Label.Map.add l (St_cond(r,l1,l2)) g else g 59 | St_jumptable(r, ls) when List.length ls > 1 -> 60 let f' l' (b, ls', g) = 61 let (b', l', g) = erase_critical u g pred_count l l' in 62 (b || b', l' :: ls', g) in 63 let starting = (false, [], g) in 64 let (b, ls', g) = List.fold_right f' ls starting in 65 if b then Label.Map.add l (St_jumptable(r, ls')) g else g 66 | _ -> g in 67 Label.Map.fold f g g 68 239 (pred_table : Label.t list Label.Map.t) 240 (lbl : Label.t) 241 (valu : Fpair.valuation) 242 : Fpair.property = 243 let succs = RTLabsUtilities.statement_successors (Label.Map.find lbl g) in 244 let preds = Label.Map.find lbl pred_table in 245 246 (* anticipatable expressions at entry *) 247 (* take anticipatable expressions of successors... *) 248 let ant l = fst (valu l) in 249 let nea l = snd (valu l) in 250 let ant_in = big_inter ant succs in 251 (* ... filter out those that contain the register being changed ...*) 252 let ant_in = filter_unchanged (modified_at g lbl) ant_in in 253 (* ... and add the expression being calculated ... *) 254 let ant_in = ant_in ++* expr_of g lbl in 255 256 (* non-earliest expressions at entry *) 257 (* take non-earliest or anticipatable expressions of predecessors, *) 258 (* filtered so that just unchanged expressions leak *) 259 let ant_or_nea l = 260 filter_unchanged (modified_at g l) (ant l ++ nea l) in 261 let nea_in = big_inter ant_or_nea preds in 69 262 70 71 72 73 (* am implementing *) 74 let trans = Languages.RTLabs, fun _ -> assert false 263 (ant_in, nea_in) 264 265 let compute_anticipatable_and_non_earliest 266 (f_def : internal_function) 267 (pred_table : Label.t list Label.Map.t) 268 : Fpair.valuation = 269 270 Fpair.lfp (semantics_ant_nea f_def.f_graph pred_table) 271 272 (* ------------ PHASE 2 : delayedness and lateness ----------- *) 273 (* An expression e is delayable at position p there is a point p' preceding it*) 274 (* in the control flow where e could be safely placed, and between p'and p *) 275 (* excluded e is never used. *) 276 277 278 let semantics_delay 279 (g : graph) 280 (pred_table : Label.t list Label.Map.t) 281 (ant_nea : Fpair.valuation) 282 (lbl : Label.t) 283 (valu : Fsing.valuation) 284 : Fsing.property = 285 let preds = Label.Map.find lbl pred_table in 286 287 (* delayed expressions at entry *) 288 (* take delayed expressions of predecessors which are not the expressions *) 289 (* of such predecessors... *) 290 let rem_pred lbl' = valu lbl' --* expr_of g lbl' in 291 let delay_in = big_inter rem_pred preds in 292 (* ... and add in anticipatable and earliest expressions *) 293 let (ant, nea) = ant_nea lbl in 294 delay_in ++ (ant -- nea) 295 296 let compute_delayed 297 (f_def : internal_function) 298 (pred_table : Label.t list Label.Map.t) 299 (ant_nea : Fpair.valuation) 300 : Fsing.valuation = 301 302 Fsing.lfp (semantics_delay f_def.f_graph pred_table ant_nea) 303 304 (* An expression is latest at p if it cannot be delayed further *) 305 let late (g : graph) (delay : Fsing.valuation) 306 : Fsing.valuation = fun lbl -> 307 let stmt = Label.Map.find lbl g in 308 let succs = RTLabsUtilities.statement_successors stmt in 309 310 let eo = match expr_of g lbl with 311 | Some e when ExprSet.mem e (delay lbl) -> Some e 312 | _ -> None in 313 314 (delay lbl -- big_inter delay succs) ++* eo 315 316 317 (* --------------- PHASE 3 : isolatedness, optimality and redudancy --------*) 318 319 (* An expression e is isolated at point p if on every path from p a use of *) 320 (* e is preceded by an optimal computation point for it. These are expressions*) 321 (* which will not be touched *) 322 let semantics_isolated 323 (g : graph) 324 (late : Fsing.valuation) 325 (lbl : Label.t) 326 (valu : Fsing.valuation) 327 : Fsing.property = 328 329 let stmt = Label.Map.find lbl g in 330 let succs = RTLabsUtilities.statement_successors stmt in 331 let f l = late l ++ (valu l --* expr_of g l) in 332 big_inter f succs 333 334 let compute_isolated 335 (f_def : internal_function) 336 (delayed : Fsing.valuation) 337 : Fsing.valuation = 338 339 let graph = f_def.f_graph in 340 341 Fsing.lfp (semantics_isolated graph (late graph delayed)) 342 343 (* expressions that are optimally placed at point p, without being isolated *) 344 let optimal (late : Fsing.valuation) (isol : Fsing.valuation) 345 : Fsing.valuation = fun lbl -> 346 late lbl -- isol lbl 347 348 (* mark instructions that are redundant and can be removed *) 349 let redundant g late isol lbl = 350 match expr_of g lbl with 351 | Some e when ExprSet.mem e (late lbl) || ExprSet.mem e (isol lbl) -> 352 false 353 | Some _ -> true 354 | _ -> false 355 356 (*------ PHASE 4 : place expressions, remove reduntant ones -------------*) 357 358 let remove_redundant def is_redundant = 359 let g = def.f_graph in 360 let types = RTLabsUtilities.computes_type_map def in 361 let f lbl stmt (g', s) = 362 if is_redundant lbl then 363 match modified_at_stmt stmt, expr_of_stmt stmt with 364 | Some r, Some e -> 365 let succs = RTLabsUtilities.statement_successors stmt in 366 let (s, (tmp, _)) = 367 try 368 (s, ExprMap.find e s) 369 with 370 | Not_found -> 371 let tmp = Register.fresh def.f_runiverse in 372 let typ = Register.Map.find r types in 373 let s = ExprMap.add e (tmp, typ) s in 374 (s, (tmp, typ)) in 375 let new_stmt = St_op1 (Op_id, r, tmp, lbl) in 376 let new_stmt = RTLabsUtilities.fill_labels new_stmt succs in 377 (Label.Map.add lbl new_stmt g', s) 378 | _ -> assert false 379 else (g', s) in 380 let (g, s) = Label.Map.fold f g (g, ExprMap.empty) in 381 ({ def with f_graph = g }, s) 382 383 let stmt_of_expr 384 (r : Register.t) 385 (e : expr) 386 (l : Label.t) 387 : statement = 388 match e with 389 (* | Cst c -> St_cst (r, c, l)*) 390 | UnOp (op, s) -> St_op1 (op, r, s, l) 391 | BinOp (op, s, t) -> St_op2 (op, r, s, t, l) 392 393 let store_optimal_computation (def, redundants) optimal = 394 (* first add the temporaries' declarations *) 395 let f _ (r, typ) vars = (r, typ) :: vars in 396 let f_locals = ExprMap.fold f redundants def.f_locals in 397 398 (* now the actual replacement *) 399 let g = def.f_graph in 400 let freshl () = Label.Gen.fresh def.f_luniverse in 401 let f lbl stmt g' = 402 match RTLabsUtilities.statement_successors stmt with 403 | next :: rest -> 404 (* I am supposing optimal expressions are only at single-successor *) 405 (* nodes. To be checked. Also to be checked if putting it after the*) 406 (* node changes things or not. I do that because otherwise a *) 407 (* computation might find itself before the first cost_label after a*) 408 (* branching, breaking well labeling *) 409 let f' e (next', g'') = 410 assert (rest = []); (* when I am assured this must go *) 411 if not (ExprMap.mem e redundants) then (next', g'') else 412 let (tmp, _) = ExprMap.find e redundants in 413 let opt_calc = 414 match modified_at_stmt stmt, expr_of_stmt stmt with 415 | Some r, Some e' when e = e' -> 416 St_op1 (Op_id, tmp, r, next') 417 | _ -> stmt_of_expr tmp e next' in 418 RTLabsUtilities.insert_in_between freshl g'' lbl next' opt_calc in 419 snd (ExprSet.fold f' (optimal lbl) (next, g')) 420 | _ -> g' in 421 { def with f_locals = f_locals; f_graph = Label.Map.fold f g g } 422 423 424 (* piecing it all together *) 425 let transform_internal f_def = 426 let pred_table = RTLabsUtilities.compute_predecessor_lists f_def.f_graph in 427 let ant_nea = compute_anticipatable_and_non_earliest f_def pred_table in 428 (*Printf.printf "Ant + Nearl:\n"; 429 print_valu_pair ant_nea f_def.f_graph f_def.f_entry;*) 430 let delay = compute_delayed f_def pred_table ant_nea in 431 (*Printf.printf "Delayed:\n"; 432 print_valu_sing delay f_def.f_graph f_def.f_entry;*) 433 let late = late f_def.f_graph delay in 434 (*Printf.printf "Late:\n"; 435 print_valu_sing late f_def.f_graph f_def.f_entry;*) 436 let isol = compute_isolated f_def delay in 437 (*Printf.printf "isolated:\n"; 438 print_valu_sing isol f_def.f_graph f_def.f_entry;*) 439 let opt = optimal late isol in 440 let redn = redundant f_def.f_graph late isol in 441 (*Printf.printf "optimal:\n"; 442 print_valu_sing opt f_def.f_graph f_def.f_entry; 443 Printf.printf "redundant:\n"; 444 let f lbl _ = 445 Printf.printf "%s : %s\n" lbl (if redn lbl then "yes" else "no") in 446 RTLabsUtilities.dfs_iter f f_def.f_graph f_def.f_entry;*) 447 store_optimal_computation (remove_redundant f_def redn) opt 448 449 let transform_funct = function 450 | (f, F_int f_def) -> (f, F_int (transform_internal f_def)) 451 | f -> f 452 453 let trans = Languages.RTLabs, function 454 | Languages.AstRTLabs p -> 455 Languages.AstRTLabs { p with functs = List.map transform_funct p.functs } 456 | _ -> assert false (* wrong language *) -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightToCminor.ml
r1433 r1473 535 535 let e = translate_expr var_locs e in 536 536 let jmp lbl = Cminor.St_goto lbl in 537 let econd =538 Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in539 537 let scond = 540 Cminor.St_ifthenelse (e cond, jmp exit_lbl, Cminor.St_skip) in538 Cminor.St_ifthenelse (e, Cminor.St_skip, jmp exit_lbl) in 541 539 let loop = 542 540 Cminor.St_seq(scond,Cminor.St_seq (stmt, ind_inc i (jmp loop_lbl))) in -
Deliverables/D2.2/8051-indexed-labels-branch/src/options.ml
r1468 r1473 95 95 " Apply constant propagation."; 96 96 97 "- red-elim", Arg.Unit (add_transformation RedundancyElimination.trans),97 "-pre", Arg.Unit (add_transformation RedundancyElimination.trans), 98 98 " Apply partial redundancy elimination."; 99 99
Note: See TracChangeset
for help on using the changeset viewer.