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

Last change on this file since 1585 was 1585, checked in by tranquil, 9 years ago

fighting with a bug of the translation from RTL to ERTL

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