Ignore:
Timestamp:
Nov 1, 2011, 6:31:24 PM (9 years ago)
Author:
tranquil
Message:
  • corrected a bug
  • implemented copy propagation
  • enhanced constant propagation with some algebraic equalities
  • temporarily added immediates to RTLabs, to be seen if it is useful
File:
1 edited

Legend:

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

    r1473 r1477  
    2222                | T
    2323                | V of Mem.Value.t
     24                | S (* stack: could add offset *)
     25                | A of AST.ident (* address symbol *)
    2426
    2527  type property =
     
    3133  let join_t x y = match x, y with
    3234                | V v1, V v2 when Mem.Value.equal v1 v2 -> V v1
     35                | S, S -> S
     36                | A i, A j when i = j -> A i
    3337                | _ -> T
    3438
     
    4044                Register.FlexMap.merge choose
    4145
    42         let bind i v p =
    43                 let new_binding =
    44                         try
    45                                 join_t v (Register.FlexMap.find i p)
    46                         with
    47                                 | Not_found -> v in
    48                 Register.FlexMap.add i new_binding p
     46        let bind = Register.FlexMap.add
    4947       
    5048        let find = Register.FlexMap.find
     49       
     50        let rem = Register.FlexMap.remove
    5151               
    5252        let mem = Register.FlexMap.mem
     
    5555                try
    5656                        match find i p with
    57                                 | V _ -> true
    5857                                | T -> false
     58                                | _ -> true
    5959                with
    6060                        | Not_found -> false
    6161
    6262  let find_cst i p =
    63           match find i p with
    64               | V v -> v
    65               | T -> raise Not_found
    66 
     63    match find i p with
     64            | T -> raise Not_found
     65            | v -> v
     66
     67               
     68
     69  let is_top i p =
     70    try
     71        match find i p with
     72            | T -> true
     73                                                | _ -> false
     74    with
     75        | Not_found -> false
     76       
     77        let is_zero i p =
     78                try
     79      match find i p with
     80                                | V v -> Mem.Value.is_false v
     81        | _ -> false
     82      with
     83                                | Not_found -> false
     84       
    6785  let equal : property -> property -> bool =
    6886                Register.FlexMap.equal (fun x y -> match x, y with
    69                         | T, T -> true
     87                        | T, T | S, S -> true
    7088                        | V v1, V v2 -> Mem.Value.equal v1 v2
     89                        | A i, A j -> i = j
    7190                        | _ -> false)
    7291
    7392  let is_maximal _ = false
     93       
     94        let print = function
     95    | T -> "T"
     96    | V v -> Mem.Value.to_string v
     97    | S -> "STACK"
     98    | A i -> "*" ^ i
    7499
    75100end
     
    99124  | Cst_sizeof t' ->
    100125          L.V (cast_to_std t (Mem.Value.of_int (MemTarget.concrete_size t')))
     126        | Cst_stack -> L.S
     127        | Cst_addrsymbol i -> L.A i
    101128        | _ -> assert false (* won't call in these cases *)
    102129
    103 let do_the_op1 type_of i j op x = match x with
    104         | L.V v -> L.V (Eval.op1 (type_of i) (type_of j) op v)
     130let do_the_op1 type_of i j op x = match op, x with
     131        | _, L.V v -> L.V (Eval.op1 (type_of i) (type_of j) op v)
     132        | Op_id, _ -> x
    105133  | _ -> L.T
    106134
     
    111139        | L.V v1, L.V v2, _ ->
    112140                L.V (Eval.op2 (type_of i) (type_of j) (type_of k) op v1 v2)
     141        (* ops with stack and address symbols are not considered constant, unless *)
     142        (* clearly so *)
     143        | x, L.V v, (Op_addp | Op_subp) when Mem.Value.is_false v -> x
    113144        | _ -> L.T
     145
     146(* this is used to mark some results of a bin op as constant even if its *)
     147(* operands are not both constant *)
     148let mark_const_op op i j k prop =
     149        match L.is_zero j prop, L.is_zero k prop, op with
     150                | true, _, (Op_mul | Op_div | Op_divu | Op_mod | Op_modu | Op_and |
     151                            Op_shl | Op_shr | Op_shru | Op_cmpu Cmp_gt)
     152          | _, true, (Op_mul | Op_and | Op_cmpu Cmp_lt) ->
     153                  L.bind i (L.V Mem.Value.zero) prop
     154    | true, _, Op_cmpu Cmp_le
     155                | _, true, Op_cmpu Cmp_ge -> L.bind i (L.V (Mem.Value.of_bool true)) prop
     156                | _, _, (Op_cmp Cmp_eq | Op_cmpu Cmp_eq | Op_cmpp Cmp_eq)
     157                  when Register.equal j k -> L.bind i (L.V (Mem.Value.of_bool true)) prop
     158    | _, _, (Op_cmp Cmp_ne | Op_cmp Cmp_gt | Op_cmp Cmp_lt |
     159                         Op_cmpu Cmp_ne | Op_cmpu Cmp_gt | Op_cmpu Cmp_lt |
     160                                                 Op_cmpp Cmp_ne | Op_cmpp Cmp_gt | Op_cmpp Cmp_lt)
     161      when Register.equal j k -> L.bind i (L.V (Mem.Value.of_bool false)) prop
     162                | _ -> L.rem i prop
    114163
    115164let semantics
     
    127176        match Label.Map.find lbl graph with
    128177    | St_cst (_, Cst_float _, _) -> error_float ()
    129                 | St_cst (_, (Cst_addrsymbol _ | Cst_stack), _) -> pred_prop
    130178                | St_cst (i, k, _) -> L.bind i (cst (type_of i) k) pred_prop
    131     | St_op1 (op, i, j, _) when L.mem j pred_prop ->
    132                         L.bind i (do_the_op1 type_of i j op (L.find j pred_prop)) pred_prop
    133     | St_op2 (op,i, j, k, _) when L.mem j pred_prop && L.mem k pred_prop ->
     179    | St_op1 (op, i, j, _) ->
     180      (try
     181                                L.bind i (do_the_op1 type_of i j op (L.find j pred_prop)) pred_prop
     182                        with
     183                                | Not_found -> L.rem i pred_prop)
     184
     185    | St_op2 (op,i,Reg j,Reg k,_) when L.mem j pred_prop && L.mem k pred_prop ->
    134186                        let j_val = L.find j pred_prop in
    135187                        let k_val = L.find k pred_prop in
    136188      L.bind i (do_the_op2 type_of i j k op j_val k_val) pred_prop
     189                | St_op2 (op, i, Reg j, Reg k, _) ->
     190                        mark_const_op op i j k pred_prop
     191                | St_load (_, _, i, _)
     192                | St_call_id (_, _, Some i, _, _)
     193                | St_call_ptr (_, _, Some i, _, _) -> L.rem i pred_prop
    137194    | _ -> pred_prop
    138195
     
    154211(* 1) if we have mapped a register to a value, it must be an integer *)
    155212(* 2) we are turning abstract offsets and sizes into integers *)
    156 let cst_of_value v = Cst_int (Mem.Value.to_int v)
     213(* 3) this shares the problem with AST constants of representability *)
     214(*    with ocaml 31 bits integers *)
     215let cst_of_value = function
     216        | L.V v -> Cst_int (Mem.Value.to_int v)
     217        | L.S -> Cst_stack
     218        | L.A i -> Cst_addrsymbol i
     219        | _ -> invalid_arg "cst_of_value"
     220
     221let simpl_imm_op2 op i j k types prop l =
     222        let f r =
     223                try
     224                        Some (L.find_cst r prop)
     225                with
     226                        | Not_found -> None in
     227        let one = Mem.Value.of_int 1 in
     228        let type_of r = Register.Map.find r types in
     229        match f j, f k, op with
     230  | Some (L.V v), _, (Op_add | Op_or | Op_xor ) when Mem.Value.is_false v ->
     231    St_op1(Op_id, i, k, l)
     232  | Some (L.V v), _, Op_mul when Mem.Value.equal v one ->
     233    St_op1(Op_id, i, k, l)
     234  | _, Some (L.V v), (Op_add | Op_sub | Op_addp | Op_subp | Op_or | Op_xor)
     235          when Mem.Value.is_false v ->
     236    St_op1(Op_id, i, j, l)
     237  | _, Some (L.V v), Op_mul when Mem.Value.equal v one ->
     238    St_op1(Op_id, i, j, l)
     239  | Some (L.V v), _, Op_sub when Mem.Value.is_false v ->
     240                St_op1(Op_negint, i, k, l)
     241  | Some v, Some u, _ ->
     242                let a1 = Imm (cst_of_value v, type_of j) in
     243                let a2 = Imm (cst_of_value u, type_of k) in
     244                St_op2(op, i, a1, a2, l)
     245  | Some v, _, _ -> St_op2(op, i, Imm (cst_of_value v, type_of j), Reg k, l)
     246  | _, Some v, _ -> St_op2(op, i, Reg j, Imm (cst_of_value v, type_of k), l)
     247        | _ -> St_op2(op, i, Reg j, Reg k, l)
     248
     249let simpl_imm_load q i j types prop l =
     250        try
     251                let v = L.find_cst i prop in
     252                St_load(q, Imm (cst_of_value v, Register.Map.find i types), j, l)
     253        with
     254                | Not_found -> St_load (q, Reg i, j, l)
     255
     256let simpl_imm_store q i j types prop l =
     257        let f r =
     258                try
     259                    Some (L.find_cst r prop)
     260                with
     261                    | Not_found -> None in
     262        let type_of r = Register.Map.find r types in
     263        match f i, f j with
     264                | Some v, Some u ->
     265            let a1 = Imm (cst_of_value v, type_of i) in
     266            let a2 = Imm (cst_of_value u, type_of j) in
     267            St_store(q, a1, a2, l)
     268                | Some v, _ ->
     269                        St_store(q, Imm (cst_of_value v, type_of i), Reg j, l)
     270    | _, Some u ->
     271      St_store(q, Reg i, Imm (cst_of_value u, type_of j), l)
     272                | _ -> St_store(q, Reg i, Reg j, l)
    157273
    158274(* we transform statements according to the valuation found out by analyze *)
     
    160276let transform_statement
    161277    (valu : F.valuation)
    162                 (p    : Label.t)
     278                (types: sig_type Register.Map.t)
     279    (p    : Label.t)
    163280                : statement -> statement = function
    164281  | St_cst (i, (Cst_offset _ | Cst_sizeof _), next) ->
     
    168285        | (St_op1 (_,i,_,next) | St_op2(_,i,_,_,next)) when L.is_cst i (valu p) ->
    169286                St_cst (i, cst_of_value (L.find_cst i (valu p)), next)
    170         | St_cond (i, if_true, if_false) when L.is_cst i (valu p) ->
    171                 let next =
    172                   if Mem.Value.is_true (L.find_cst i (valu p)) then if_true else if_false in
    173                 St_skip next
     287        | St_op2 (op, i, Reg j, Reg k, l) ->
     288                simpl_imm_op2 op i j k types (valu p) l
     289  | St_load (q, Reg i, j, l) ->
     290                simpl_imm_load q i j types (valu p) l
     291        | St_store (q, Reg i, Reg j, l) ->
     292                simpl_imm_store q i j types (valu p) l
     293  | St_op2 _ | St_load _ | St_store _ ->
     294          assert false (* there should not be any imm argument *)
     295        | St_cond (i, if_true, if_false) as s when L.is_cst i (valu p) ->
     296                let s = match L.find_cst i (valu p) with
     297                        | L.V v when Mem.Value.is_false v -> St_skip if_false
     298                        | L.V _ | L.A _ -> St_skip if_true
     299                        | _ -> s in s
    174300        | stmt -> stmt
    175301
     
    182308                : internal_function =
    183309        let valu = analyze f_def in
    184         (* we transform the graph according to the analysis *)
    185         let graph = Label.Map.mapi (transform_statement valu) f_def.f_graph in
     310        (* we transform the graph according to the analysis *)
     311        let types = RTLabsUtilities.computes_type_map f_def in
     312        let graph = Label.Map.mapi (transform_statement valu types) f_def.f_graph in
    186313        (* and we eliminate resulting dead code *)
     314        let graph = RTLabsUtilities.dead_code_elim graph f_def.f_entry in
    187315        {f_def with f_graph = graph}
    188316
Note: See TracChangeset for help on using the changeset viewer.