Changeset 1473 for Deliverables/D2.2


Ignore:
Timestamp:
Oct 28, 2011, 4:45:12 PM (8 years ago)
Author:
tranquil
Message:
  • implemented partial redundancy elimination
  • added some tools for RTLabs, with a depth-first fold
  • prettier printing of RTLabs
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  
    4545
    4646let 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 -> "<="
    5353
    5454let rec print_size = function
    … …  
    8383  Printf.sprintf "%d%s" size (string_of_signedness sign)
    8484
    85 let print_op1 = function
     85let print_op1 op r = Printf.sprintf "%s %s"
     86  (match op with
    8687  | AST.Op_cast (int_type, dest_size) ->
    8788    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 -> ""
    9293  | 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
     97let 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 -> "/"
    100104  | AST.Op_divu -> "/u"
    101105  | AST.Op_mod -> "mod"
    … …  
    104108  | AST.Op_or -> "or"
    105109  | 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"
    109113  | 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"
    113117  | 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)
    115120
    116121
    … …  
    143148    Printf.sprintf "increment %d --> %s" i lbl
    144149  | RTLabs.St_cst (destr, cst, lbl) ->
    145       Printf.sprintf "imm %s, %s --> %s"
     150      Printf.sprintf "%s := %s --> %s"
    146151        (print_reg destr)
    147152        (print_cst cst)
    148153        lbl
    149154  | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
    150       Printf.sprintf "%s %s, %s --> %s"
    151         (print_op1 op1)
     155      Printf.sprintf "%s := %s --> %s"
    152156        (print_reg destr)
    153         (print_reg srcr)
     157  (print_op1 op1 srcr)
    154158        lbl
    155159  | 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"
    158161        (print_reg destr)
    159         (print_reg srcr1)
    160         (print_reg srcr2)
     162  (print_op2 op2 srcr1 srcr2)
    161163        lbl
    162164  | 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)
    164167        (Memory.string_of_quantity q)
    165168        (print_reg addr)
    166         (print_reg destr)
    167169        lbl
    168170  | RTLabs.St_store (q, addr, srcr, lbl) ->
    169       Printf.sprintf "store %s, %s, %s --> %s"
    170         (Memory.string_of_quantity q)
     171      Printf.sprintf "*(%s)%s := %s --> %s"
     172  (Memory.string_of_quantity q)
    171173        (print_reg addr)
    172174        (print_reg srcr)
    173175        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
    177180        (print_args args)
    178         (print_oreg res)
    179181        (Primitive.print_sig sg)
    180182        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
    188202  | RTLabs.St_tailcall_id (f, args, sg) ->
    189       Printf.sprintf "tailcall \"%s\", %s: %s"
     203      Printf.sprintf "tailcall \"%s\" (%s) : %s"
    190204        f
    191205        (print_args args)
    192206        (Primitive.print_sig sg)
    193207  | RTLabs.St_tailcall_ptr (f, args, sg) ->
    194       Printf.sprintf "tailcall_ptr \"%s\", %s: %s"
     208      Printf.sprintf "tailcall *%s (%s) : %s"
    195209        (print_reg f)
    196210        (print_args args)
    … …  
    230244
    231245
    232 let print_graph n c =
     246let print_graph n c entry =
    233247  let f lbl stmt s =
    234248    Printf.sprintf "%s%s: %s\n%s"
    … …  
    237251      (print_statement stmt)
    238252      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       
    242263let print_internal_decl n f def =
    243264
    … …  
    257278    (n_spaces (n+2))
    258279    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)
    260281
    261282

  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsPrinter.mli

    r740 r1473  
    44val print_statement : RTLabs.statement -> string
    55
     6val print_cst : AST.cst -> string
     7
     8val print_op1 : AST.op1 -> Register.t -> string
     9
     10val print_op2 : AST.op2 -> Register.t -> Register.t -> string
     11
    612val print_program : RTLabs.program -> string

  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsUtilities.ml

    r1468 r1473  
    99  match stmt with
    1010  | St_return _
    11     | St_tailcall_id _
    12     | St_tailcall_ptr _ ->
    13     []
     11        | St_tailcall_id _
     12        | St_tailcall_ptr _ ->
     13          []
    1414  | St_skip l
    1515  | St_cost (_, l)
    … …  
    2828  | St_jumptable (_, ls) -> ls
    2929
     30let 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
    3049(** computes a map binding the set of predecessors to each node. The domain
    3150    is guaranteed to be equal to the domain of graph *)
    3251let compute_predecessors graph =
    33     let add_to_preds pred map lbl =
     52  let add_to_preds pred map lbl =
    3453    let preds =
    3554        try
    … …  
    3958    Label.Map.add lbl preds map in
    4059  let add_predecessor lbl stmt map =
    41                 (* make sure the domain of the map will be equal to dom graph, adding *)
    42                 (* empty sets if need be *)
     60        (* make sure the domain of the map will be equal to dom graph, adding *)
     61        (* empty sets if need be *)
    4362    let map = if Label.Map.mem lbl map then map else
    44                         Label.Map.add lbl Label.Set.empty map in
    45                 List.fold_left (add_to_preds lbl) map (statement_successors stmt) in
     63            Label.Map.add lbl Label.Set.empty map in
     64        List.fold_left (add_to_preds lbl) map (statement_successors stmt) in
    4665  Label.Map.fold add_predecessor graph Label.Map.empty
    4766
    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        
     67let 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
     83let 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. *)
    65109let insert_in_between
    66     (u : Label.Gen.universe)
     110    (fresh : unit -> node)
    67111                (g : graph)
    68112                (src : node)
    69113                (tgt : node)
    70114                (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
     124let 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       
     141let 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
     150let 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   
     167let 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  
    66val statement_successors : statement -> node list
    77
    8 (** computes a map binding the set of predecessors to each node. The domain
    9     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 *)
    1010val 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 *)
     14val 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 *)
     19val fill_labels : statement -> Label.t list -> statement
    1120
    1221(** Given a graph and an entry point, this function deletes all unreachable
    … …  
    1524
    1625(** [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. *)
    2131val insert_in_between :
    22     Label.Gen.universe -> graph -> node -> node -> statement -> graph
     32    (unit -> node) -> graph -> node -> node -> statement -> Label.t * graph
    2333
     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. *)
     37val 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. *)
     42val 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? *)
     46val computes_type_map : internal_function -> AST.sig_type Register.Map.t

  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/constPropagation.ml

    r1468 r1473  
    141141                : F.valuation =
    142142        (* 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               
    151145        let graph = f_def.f_graph in
    152146       

  • 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
    16open RTLabs
    27open AST
    … …  
    914let error_shift () = error "Shift operations not supported."
    1015
    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. *)
    1423
    1524let count_predecessors
    1625    (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
     38module LabelPairSet = Set.Make(struct
     39  type t = Label.t * Label.t
     40  let compare = compare
     41end)
     42
     43let 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 *)
    4572
    4673let 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 *)
     86type 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
     91let 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
     97let 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 *)
     101let 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
     111let modified_at (g : graph) (n : Label.t) : Register.t option =
     112        modified_at_stmt (Label.Map.find n g)
     113
     114module ExprOrdered = struct
     115        type t = expr
     116        let compare = compare
     117end
     118
     119module ExprSet = Set.Make(ExprOrdered)
     120module ExprMap = Map.Make(ExprOrdered)
     121
     122type expr_set = ExprSet.t
     123
     124let ( ^^ ) = ExprSet.inter
     125
     126let ( ++ ) = ExprSet.union
     127
     128let ( ++* ) s = function
     129  | None -> s
     130  | Some e -> ExprSet.add e s
     131
     132let ( --* ) s = function
     133  | None -> s
     134  | Some e -> ExprSet.remove e s
     135
     136let ( -- ) = ExprSet.diff
     137
     138let 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
     149let 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                       
     159module 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       
     171end
     172
     173module 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   
     184end
     185
     186module Fpair = Fix.Make (Label.ImpMap) (Lpair)
     187
     188module Fsing = Fix.Make (Label.ImpMap) (Lsing)
     189
     190(* printing tools to debug *)
     191
     192let 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                       
     200let 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
     208let 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
     214let 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
     220let 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
     237let semantics_ant_nea
    47238    (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
    69262                       
    70        
    71 
    72 
    73 (* am implementing *)
    74 let trans = Languages.RTLabs, fun _ -> assert false
     263        (ant_in, nea_in)
     264       
     265let 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
     278let 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   
     296let 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 *)
     305let 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 *)
     322let 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       
     334let 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 *)
     344let 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 *)
     349let 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
     358let 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
     383let 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
     393let 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 *)           
     425let 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       
     449let transform_funct = function
     450        | (f, F_int f_def) -> (f, F_int (transform_internal f_def))
     451        | f -> f
     452
     453let 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  
    535535                        let e = translate_expr var_locs e in
    536536                        let jmp lbl = Cminor.St_goto lbl in
    537       let econd =               
    538         Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
    539537      let scond =
    540         Cminor.St_ifthenelse (econd, jmp exit_lbl, Cminor.St_skip) in
     538        Cminor.St_ifthenelse (e, Cminor.St_skip, jmp exit_lbl) in
    541539            let loop =
    542540                                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  
    9595    " Apply constant propagation.";
    9696
    97     "-red-elim", Arg.Unit (add_transformation RedundancyElimination.trans),
     97    "-pre", Arg.Unit (add_transformation RedundancyElimination.trans),
    9898    " Apply partial redundancy elimination.";
    9999
Note: See TracChangeset for help on using the changeset viewer.