source: Deliverables/D2.2/8051/src/RTL/RTLConstPropagation.ml @ 1580

Last change on this file since 1580 was 1580, checked in by tranquil, 8 years ago

implemented constant propagation in LTL
cleaned up translations in optimizations, a new module for translations is available

File size: 14.4 KB
Line 
1open RTL
2
3let error_prefix = "RTLabs to RTL"
4let error = Error.global_error error_prefix
5
6let error_int () = error "int16 and int32 not supported."
7let error_float () = error "float not supported."
8let error_shift () = error "Shift operations not supported."
9
10
11(* The analysis uses the lattice of maps from registers to values with a top *)
12(* element which indicates the register is known not to be constant. *)
13(* The lattice's join operation is pointwise join, where pointwise bottom is *)
14(* represented by the absence of a binding in the map. *)
15
16module Mem = Driver.RTLMemory
17module Val = Mem.Value
18
19let to_opt_2 f x y = try Some (f x y) with Not_found -> None
20
21module L : sig
22
23  type t =
24    | T
25    | V of Val.t
26
27  type property
28
29  val bottom : property
30  val join : property -> property -> property
31
32  val bind : Register.t -> t option -> property -> property
33  val bind_carry : t option -> property -> property
34  val set_carry : property -> property
35  val clear_carry : property -> property
36  val bind_reg_n_carry
37    : Register.t -> t option * t option -> property -> property
38  val bind_2
39    : Register.t -> Register.t -> t option * t option -> property -> property
40  val find : Register.t -> property -> t option
41  val find_carry_in : property -> t option
42  val equal : property -> property -> bool
43  val is_maximal : property -> bool
44  val is_cst : Register.t -> property -> bool
45  val find_cst : Register.t -> property -> int
46  val find_cst_opt : Register.t -> property -> int option
47  val find_cst_carry_in : property -> int option
48
49end = struct
50
51  (* bottom will be when the map is undefined, so we do not need it explicitly*)
52  type t =
53    | T
54    | V of Val.t
55
56
57  type property = {
58    regs : t Register.FlexMap.t ; (* no need to have out and in *)
59    in_c : t option ;
60    out_c : t option
61  }
62
63  let bottom : property =
64    { regs = Register.FlexMap.empty; in_c = None; out_c = None }
65
66  let join_t x y = match x, y with
67    | Some (V v1), Some (V v2) when Mem.Value.equal v1 v2 -> Some (V v1)
68    | Some _, Some _ -> Some T
69    | None, x | x, None -> x
70
71  let join (p : property) (q : property) : property =
72    let choose _ = join_t in
73    let carry = join_t p.out_c q.out_c in
74    { regs = Register.FlexMap.merge choose p.regs q.regs;
75      in_c = carry;
76      out_c = carry
77    }
78
79  let bind r t p =
80    let regs = match t with
81      | Some v -> Register.FlexMap.add r v p.regs
82      | None -> Register.FlexMap.remove r p.regs in
83    { p with regs = regs }
84
85  let bind_carry t p = { p with out_c = t }
86  let set_carry  = bind_carry (Some (V (Val.of_bool true)))
87  let clear_carry = bind_carry (Some (V (Val.of_bool false)))
88
89  let bind_reg_n_carry  r (v, c) p =
90    bind_carry c (bind r v p)
91
92  let bind_2 r s (v, u) p =
93    (* beware, order is first r, then s (possibly overwriting r) *)
94    bind s u (bind r v p)
95
96  let find r p = to_opt_2 Register.FlexMap.find r p.regs
97  let find_carry_in p = p.in_c
98
99  let equal_t x y = match x, y with
100    | T, T -> true
101    | V v1, V v2 -> Val.equal v1 v2
102    | _ -> false
103
104  let equal_t_opt_as_bool x y = match x, y with
105    | Some T, Some T -> true
106    | Some (V v1), Some (V v2) when Val.is_true v1 -> Val.is_true v2
107    | Some (V _), Some (V v2) -> Val.is_false v2
108    | None, None -> true
109    | _ -> false
110
111  let equal p q : bool =
112    equal_t_opt_as_bool p.in_c q.in_c &&
113      equal_t_opt_as_bool p.out_c q.out_c &&
114      Register.FlexMap.equal equal_t p.regs q.regs
115
116  let is_maximal _ = false
117
118  let is_cst r p =
119    try
120      match Register.FlexMap.find r p.regs with
121        | V _ -> true
122        | T -> false
123    with
124      | Not_found -> false
125
126  let find_cst r p =
127    match find r p with
128      | Some (V v) -> Val.to_int v
129      | _ -> raise Not_found
130
131  let find_cst_opt r p =
132    try Some (find_cst r p) with
133      | Not_found -> None
134
135  let find_cst_carry_in p =
136    match find_carry_in p with
137      | Some (V v) when Val.to_int v > 0 -> Some 1
138      | Some (V _) -> Some 0
139      | _ -> None
140  (* let print = function *)
141  (*   | T -> "T" *)
142  (*   | V v -> Val.to_string v *)
143
144end
145
146module F = Fix.Make (Label.ImpMap) (L)
147
148module Eval = I8051.Eval (Val)
149
150let cst i =  L.V (Val.of_int i)
151
152let find_arg a prop = match a with
153  | Reg r -> L.find r prop
154  | Imm k -> Some (cst k)
155
156let do_the_op1
157    (op : I8051.op1)
158    (prop : F.property)
159    (j : Register.t)
160    : L.t option =
161  let x = L.find j prop in
162  match x with
163    | Some (L.V v) -> Some (L.V (Eval.op1 op v))
164    | _ -> x
165
166
167(* as the carry bit could be known to be set or unset or unchanged even
168   if arguments are bottom, the case for op2 is more complicated *)
169let do_the_op2
170    (op : I8051.op2)
171    (prop : F.property)
172    (a : argument)
173    (b : argument)
174    : L.t option * L.t option =
175  let x = find_arg a prop in
176  let y = find_arg b prop in
177  let c = L.find_carry_in prop in
178  match x, y, c, op with
179  | Some (L.V v1), Some(L.V v2), Some(L.V vc), _ ->
180    let (v', c') = Eval.op2 vc op v1 v2 in
181    (Some (L.V v'), Some (L.V c'))
182  | Some (L.V v1), Some (L.V v2), _, (I8051.And | I8051.Xor | I8051.Or) ->
183    (* carry bit does not matter and is unchanged *)
184    let (v', _) = Eval.op2 (Val.of_bool false) op v1 v2 in
185    (Some (L.V v'), c)
186  | Some _, _, _, (I8051.And | I8051.Xor | I8051.Or)
187  | _, Some _, _, (I8051.And | I8051.Xor | I8051.Or) ->
188    (* carry bit unchanged, result variable *)
189    (Some L.T, c)
190  | None, None, _, (I8051.And | I8051.Xor | I8051.Or) ->
191    (* carry bit unchanged, result unknown *)
192    (None, c)
193  | Some (L.V v1), Some (L.V v2), _, I8051.Add ->
194    (* carry bit does not matter and is changed *)
195    let (v', c') = Eval.op2 (Val.of_bool false) op v1 v2 in
196    (Some (L.V v'), Some (L.V c'))
197  | Some (L.V v1), Some (L.V v2), _, (I8051.Addc | I8051.Sub) ->
198    (* we can predict at least the carry bit in some cases *)
199    (* c must be either Some L.T or None, can be reused for results *)
200    (* if it becomes clear when set, it will always be clear *)
201    let (_, c') = Eval.op2 (Val.of_bool true) op v1 v2 in
202    if Val.is_false c' then (c, Some (L.V c')) else
203    (* if it becomes set when clear, it will always be set *)
204    let (_, c') = Eval.op2 (Val.of_bool false) op v1 v2 in
205    if Val.is_true c' then (c, Some (L.V c'))
206    else (c, c)
207  | _, Some (L.V v1), Some (L.V v2), (I8051.Addc | I8051.Sub)
208    when Val.is_false v1 && Val.is_false v2 ->
209    (* result unknown or variable, but carry bit surely unset
210       [x] must be either None or Some L.T, can be reused for result *)
211    (x, Some (L.V (Val.of_bool false)))
212  | Some (L.V v1), _, Some (L.V v2), I8051.Addc
213    when Val.is_false v1 && Val.is_false v2 ->
214    (* result unknown or variable, but carry bit surely unset
215       [y] must be either None or Some L.T, can be reused for result *)
216    (y, Some (L.V (Val.of_bool false)))
217  | Some (L.V v1), _, Some (L.V v2), I8051.Sub
218    when Val.is_false v1 && Val.is_true v2 ->
219    (* result unknown or variable, but carry bit surely set
220       [y] must be either None or Some L.T, can be reused for result *)
221    (y, Some (L.V (Val.of_bool true)))
222  | (Some (L.V v), None, _, I8051.Add |
223     None, Some (L.V v), _, I8051.Add )
224     when Val.is_false v ->
225    (* result unknown, but carry bit surely unset *)
226    (None, Some (L.V (Val.of_bool false)))
227  | (Some (L.V v), _, _, I8051.Add |
228     _, Some (L.V v), _, I8051.Add )
229     when Val.is_false v ->
230    (* result variable, but carry bit surely unset *)
231    (Some L.T, Some (L.V (Val.of_bool false)))
232  | None, _, _, _ | _, None, _, _ | _, _, None, _ ->
233    (* in these other cases, both are unknown *)
234    (None, None)
235  | _ ->
236    (* otherwise, it means both are variable *)
237    (Some L.T, Some L.T)
238
239let do_the_opaccs
240    (op : I8051.opaccs)
241    (prop : F.property)
242    (a : argument)
243    (b : argument)
244    : L.t option * L.t option =
245  let x = find_arg a prop in
246  let y = find_arg b prop in
247  match x, y, op with
248    | _, Some (L.V v2), I8051.DivuModu when Val.is_false v2 ->
249      (* undefined, we put top *)
250      (Some L.T, Some L.T)
251    | Some (L.V v1), Some (L.V v2), _ ->
252      let (a, b) = Eval.opaccs op v1 v2 in
253      (Some (L.V a), Some (L.V b))
254    (* some cases where the result is known regardless *)
255    | (Some (L.V v), _, _ | _, Some (L.V v), _) when Val.is_false v ->
256      (* case _ / 0 already crossed out *)
257      let zero = Val.of_int 0 in
258      (Some (L.V zero), Some (L.V zero))
259    | (Some (L.V v), x, I8051.Mul | x, Some (L.V v), I8051.Mul)
260      when Val.eq v (Val.of_int 1) ->
261      (* second acc will be surely 0, first is equal to non-1 argument *)
262      (x, Some (L.V (Val.of_int 0)))
263    | None, _, _ | _, None, _ -> (None, None)
264    | _ -> (Some L.T, Some L.T)
265
266let print_deb x =
267      (match x with
268        | Some (L.V v) ->
269          Printf.sprintf "%d" (Val.to_int v)
270        | Some (L.T) ->
271          Printf.sprintf "variable"
272        | None ->
273          Printf.sprintf "unknown")
274
275let semantics
276    (graph : statement Label.Map.t)
277    (pred_table : Label.t list Label.Map.t)
278    (lbl : Label.t)
279    (valu : F.valuation)
280    : F.property =
281  let pred_prop = (* the situation at the entry of the statement (in [valu]) *)
282    let f prop pred =
283      L.join (valu pred) prop in
284    List.fold_left f L.bottom (Label.Map.find lbl pred_table) in
285  match Label.Map.find lbl graph with
286
287    | St_move (r, a, _) -> L.bind r (find_arg a pred_prop) pred_prop
288    | St_op1 (op, r, s, _) -> L.bind r (do_the_op1 op pred_prop s) pred_prop
289    | St_op2 (op, r, a, b, _) ->
290      let (x, c) = do_the_op2 op pred_prop a b in
291      L.bind_reg_n_carry r (x, c) pred_prop
292    | St_opaccs (op, r, s, a, b, _) ->
293      L.clear_carry (L.bind_2 r s (do_the_opaccs op pred_prop a b) pred_prop)
294    | St_clear_carry _ -> L.clear_carry pred_prop
295    | St_set_carry _ -> L.set_carry pred_prop
296    | St_load (r, _, _, _) -> L.bind r None pred_prop
297    | St_call_id (_, _, rets, _)
298    | St_call_ptr (_, _, _, rets, _) ->
299      List.fold_left (fun p x -> L.bind x None p) pred_prop rets
300    | St_addr (r, s, _, _)
301    | St_stackaddr (r, s, _) -> L.bind_2 r s (None, None) pred_prop
302    | _ -> pred_prop
303
304let analyze
305    (f_def : internal_function)
306    : F.valuation =
307  (* extract types of registers from the definition *)
308
309  let graph = f_def.f_graph in
310
311  let module U = GraphUtilities.Util(RTLGraph) in
312
313  let pred_table = U.compute_predecessor_lists graph in
314
315  F.lfp (semantics graph pred_table)
316
317(* now that the info for constants can be gathered, let's put that to use *)
318
319let find_cst_arg prop = function
320  | Imm k -> Some k
321  | Reg r -> L.find_cst_opt r prop
322
323let arg_from_arg prop a =
324  match find_cst_arg prop a with
325    | Some k -> Imm k
326    | None -> a
327
328let simpl_imm_op2 op i a b prop l =
329  match find_cst_arg prop a, find_cst_arg prop b,
330    L.find_cst_carry_in prop, op with
331    | Some 0, _, _, (I8051.Or | I8051.Xor)
332    | Some 0, _, Some 0, (I8051.Addc | I8051.Add)
333      (* in the above case if carry is set add unsets it, that's why we must
334         make sure it's unset *)
335    | Some 255, _, Some 1, I8051.Addc
336    | Some 255, _, _, I8051.And ->
337      St_move (i, b, l)
338    | _, Some 0, _, (I8051.Or | I8051.Xor)
339    | _, Some 0, Some 0, (I8051.Addc | I8051.Sub | I8051.Add)
340    | _, Some 255, Some 1, I8051.Addc
341    | _, Some 255, _, I8051.And ->
342      St_move (i, a, l)
343    | _ ->
344      St_op2 (op, i, arg_from_arg prop a, arg_from_arg prop b, l)
345
346let simpl_imm_opaccs op i j a b prop l =
347  match find_cst_arg prop a, find_cst_arg prop b, op with
348    | Some 1, _, I8051.Mul ->
349      [St_move (i, b, l) ; St_move (j, Imm 0, l)]
350    |  _, Some 1, (I8051.Mul | I8051.DivuModu) ->
351      [St_move (i, a, l) ; St_move (j, Imm 0, l)]
352    | _ ->
353      [St_opaccs (op, i, j, arg_from_arg prop a, arg_from_arg prop b, l)]
354
355(* we transform statements according to the valuation found out by analyze *)
356(* We also turn branchings into redirections if the guard is constant. We *)
357(* need the label to extract the property. The label in the output is for *)
358(* compliance with GraphUtilities. *)
359(* we transform statements according to the valuation found out by analyze *)
360(* We also turn branchings into redirections if the guard is constant. *)
361let transform
362    (valu : F.valuation)
363    (p    : Label.t)
364    (stmt : statement) : statement list * Label.t list option =
365  match stmt with
366    | (St_op1 (_,i,_,l) | St_op2(_,i,_,_,l) | St_move (i, _, l))
367        when L.is_cst i (valu p) ->
368      ([St_move (i, Imm (L.find_cst i (valu p)), p)], None)
369    | St_op2 (op, i, a, b, l) ->
370      ([simpl_imm_op2 op i a b (valu p) l], None)
371    | St_opaccs (op, i, j, a, b, l) ->
372      (simpl_imm_opaccs op i j a b (valu p) l, None)
373    | St_load (i, a, b, l) ->
374      ([St_load(i, arg_from_arg (valu p) a, arg_from_arg (valu p) b, l)], None)
375    | St_store (a, b, c, l) ->
376      ([St_store (arg_from_arg (valu p) a,
377                 arg_from_arg (valu p) b,
378                 arg_from_arg (valu p) c, l)], None)
379    | St_cond (i, if_true, if_false) as s ->
380      (match L.find_cst_opt i (valu p) with
381        | Some 0 -> ([], Some [if_false])
382        | Some _ -> ([], Some [if_true])
383        | None -> ([s], Some [if_true ; if_false]))
384    | St_return rets ->
385      let rets' = List.map (arg_from_arg (valu p)) rets in
386      ([St_return rets'], None)
387    | St_call_id (f, args, rets, l) ->
388      let args' = List.map (arg_from_arg (valu p)) args in
389      ([St_call_id (f, args', rets, l)], None)
390    | St_call_ptr (f1, f2, args, rets, l) ->
391      let args' = List.map (arg_from_arg (valu p)) args in
392      ([St_call_ptr (f1, f2, args', rets, l)], None)
393    | St_tailcall_id (f, args) ->
394      let args' = List.map (arg_from_arg (valu p)) args in
395      ([St_tailcall_id (f, args')], None)
396    | St_tailcall_ptr (f1, f2, args) ->
397      let args' = List.map (arg_from_arg (valu p)) args in
398      ([St_tailcall_ptr (f1, f2, args')], None)
399    | stmt -> ([stmt], None)
400
401let transform_int_function
402    (f_def  : internal_function)
403    : internal_function =
404  let valu = analyze f_def in
405        (* we transform the graph according to the analysis *)
406  let module U = GraphUtilities.Util(RTLGraph) in
407  let module T = GraphUtilities.Trans(RTLGraph)(RTLGraph) in
408  let trans = transform valu in
409  let fresh () = Label.Gen.fresh f_def.f_luniverse in
410  let graph = T.translate_pure_with_redirects fresh trans f_def.f_graph in
411  (* and we eliminate resulting dead code *)
412  let graph = U.dead_code_elim graph f_def.f_entry in
413  {f_def with f_graph = graph}
414
415let transform_function = function
416  | (id, F_int f_def) -> (id, F_int (transform_int_function f_def))
417  | f -> f
418
419let trans = Languages.RTL, function
420  | Languages.AstRTL p ->
421    Languages.AstRTL {p with functs = List.map transform_function p.functs}
422  | _ -> assert false
423
424
Note: See TracBrowser for help on using the repository browser.