source: Deliverables/D2.2/8051/src/RTLabs/constPropagation.ml @ 1580

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

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

File size: 11.6 KB
Line 
1open RTLabs
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.RTLabsMemory
17
18module L  = struct
19
20  (* bottom will be when the map is undefined, so we do not need it explicitly*)
21  type t =
22    | T
23    | V of Mem.Value.t
24    | S (* stack: could add offset *)
25    | A of AST.ident (* address symbol *)
26
27  type property =
28      t Register.FlexMap.t
29
30  let bottom : property =
31    Register.FlexMap.empty
32
33  let join_t x y = match x, y with
34    | 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
37    | _ -> T
38
39  let join : property -> property -> property =
40    let choose i b1 b2 = match b1, b2 with
41      | Some v, Some v' -> Some (join_t v v')
42      | Some v, None | None, Some v -> Some v
43      | _ -> None in
44    Register.FlexMap.merge choose
45
46  let bind = Register.FlexMap.add
47
48  let find = Register.FlexMap.find
49
50  let rem = Register.FlexMap.remove
51
52  let mem = Register.FlexMap.mem
53
54  let is_cst i p =
55    try
56      match find i p with
57        | T -> false
58        | _ -> true
59    with
60      | Not_found -> false
61
62  let find_cst i p =
63    match find i p with
64      | T -> raise Not_found
65      | v -> v
66
67  let is_top i p =
68    try
69      match find i p with
70        | T -> true
71        | _ -> false
72    with
73      | Not_found -> false
74
75  let is_zero i p =
76    try
77      match find i p with
78        | V v -> Mem.Value.is_false v
79        | _ -> false
80    with
81      | Not_found -> false
82
83  let equal : property -> property -> bool =
84    Register.FlexMap.equal (fun x y -> match x, y with
85      | T, T | S, S -> true
86      | V v1, V v2 -> Mem.Value.equal v1 v2
87      | A i, A j -> i = j
88      | _ -> false)
89
90  let is_maximal _ = false
91
92  let print = function
93    | T -> "T"
94    | V v -> Mem.Value.to_string v
95    | S -> "STACK"
96    | A i -> "*" ^ i
97
98end
99
100module F = Fix.Make (Label.ImpMap) (L)
101
102module Eval = CminorInterpret.Eval_op (Mem)
103(* evaluation happens in RTLabs memory model ... *)
104
105module MemTarget = Memory.Make (Driver.TargetArch)
106(* ... but for sizeof and offsets, which rely on the target memory model *)
107
108open AST
109
110let ext_fun_of_sign = function
111  | Signed -> Mem.Value.sign_ext
112  | Unsigned -> Mem.Value.zero_ext
113
114let cast_to_std t v = match t with
115  | Sig_int (size, sign) -> (ext_fun_of_sign sign) v size Mem.int_size
116  | Sig_float _ -> error_float ()
117  | Sig_offset | Sig_ptr -> v
118
119let cst t = function
120  | Cst_int i -> L.V (cast_to_std t (Mem.Value.of_int i))
121  | Cst_offset off -> L.V (Mem.Value.of_int (MemTarget.concrete_offset off))
122  | Cst_sizeof t' ->
123    L.V (cast_to_std t (Mem.Value.of_int (MemTarget.concrete_size t')))
124  | Cst_stack -> L.S
125  | Cst_addrsymbol i -> L.A i
126  | _ -> assert false (* won't call in these cases *)
127
128let arg_type type_of = function
129  | Reg r -> type_of r
130  | Imm (_, t) -> t
131
132let find_arg a prop = match a with
133  | Reg r -> L.find r prop
134  | Imm (k, t) -> cst t k
135
136let do_the_op1
137    (op : op1)
138    (type_of : Register.t -> sig_type)
139    (prop : F.property)
140    (i : Register.t)
141    (j : Register.t)
142    : L.t =
143  let x = L.find j prop in
144  match op, x with
145  | _, L.V v -> L.V (Eval.op1 (type_of i) (type_of j) op v)
146  | Op_id, _ -> x
147  | _ -> L.T
148
149let do_the_op2
150    (op : op2)
151    (type_of : Register.t -> sig_type)
152    (prop : F.property)
153    (i : Register.t)
154    (a : argument)
155    (b : argument)
156    : L.t =
157  let x = find_arg a prop in
158  let y = find_arg b prop in
159  match x, y, op with
160  (* consider a constant division by 0 as not constant *)
161  | L.V _, L.V v2, (Op_div | Op_divu | Op_mod | Op_modu)
162    when Mem.Value.is_false v2 -> L.T
163  | L.V v1, L.V v2, _ ->
164    L.V (Eval.op2
165           (type_of i)
166           (arg_type type_of a)
167           (arg_type type_of b) op v1 v2)
168  (* ops with stack and address symbols are not considered constant, unless *)
169  (* clearly so *)
170  | x, L.V v, (Op_addp | Op_subp) when Mem.Value.is_false v -> x
171  | _ -> L.T
172
173let is_zero_arg a prop = match a with
174  | Reg r -> L.is_zero r prop
175  | Imm (Cst_int i, _) -> i = 0
176  | _ -> false
177
178(* this is used to mark some results of a bin op as constant even if its *)
179(* operands are not both constant *)
180let mark_const_op op i a b prop =
181  match is_zero_arg a prop, is_zero_arg b prop, op with
182    | true, _, (Op_mul | Op_div | Op_divu | Op_mod | Op_modu | Op_and |
183        Op_shl | Op_shr | Op_shru | Op_cmpu Cmp_gt)
184    | _, true, (Op_mul | Op_and | Op_cmpu Cmp_lt) ->
185      L.bind i (L.V Mem.Value.zero) prop
186    | true, _, Op_cmpu Cmp_le
187    | _, true, Op_cmpu Cmp_ge -> L.bind i (L.V (Mem.Value.of_bool true)) prop
188    | _, _, (Op_cmp Cmp_eq | Op_cmpu Cmp_eq | Op_cmpp Cmp_eq) ->
189      (match a, b with
190        | Reg j, Reg k when Register.equal j k ->
191          L.bind i (L.V (Mem.Value.of_bool true)) prop
192        | _ -> L.rem i prop)
193    | _, _, (Op_cmp Cmp_ne | Op_cmp Cmp_gt | Op_cmp Cmp_lt |
194             Op_cmpu Cmp_ne | Op_cmpu Cmp_gt | Op_cmpu Cmp_lt |
195             Op_cmpp Cmp_ne | Op_cmpp Cmp_gt | Op_cmpp Cmp_lt |
196             Op_xor) ->
197      (match a, b with
198        | Reg j, Reg k when Register.equal j k ->
199          L.bind i (L.V (Mem.Value.of_bool false)) prop
200        | _ -> L.rem i prop)
201    | _ -> L.rem i prop
202
203let is_cst_arg prop = function
204  | Reg r -> L.mem r prop
205  | Imm _ -> true
206
207let semantics
208    (types : sig_type Register.Map.t)
209    (graph : statement Label.Map.t)
210    (pred_table : Label.t list Label.Map.t)
211    (lbl : Label.t)
212    (valu : F.valuation)
213    : F.property =
214  let pred_prop = (* the situation at the entry of the statement (in [valu]) *)
215    let f prop pred =
216      L.join (valu pred) prop in
217    List.fold_left f L.bottom (Label.Map.find lbl pred_table) in
218  let type_of r = Register.Map.find r types in
219  match Label.Map.find lbl graph with
220    | St_cst (_, Cst_float _, _) -> error_float ()
221    | St_cst (i, k, _) -> L.bind i (cst (type_of i) k) pred_prop
222    | St_op1 (op, i, j, _) ->
223      (try
224         L.bind i (do_the_op1 op type_of pred_prop i j) pred_prop
225       with
226         | Not_found -> L.rem i pred_prop)
227    | St_op2 (op, i, a, b, _)
228      when is_cst_arg pred_prop a && is_cst_arg pred_prop b ->
229      L.bind i (do_the_op2 op type_of pred_prop i a b) pred_prop
230    | St_op2 (op, i, a, b, _) ->
231      mark_const_op op i a b pred_prop
232    | St_load (_, _, i, _)
233    | St_call_id (_, _, Some i, _, _)
234    | St_call_ptr (_, _, Some i, _, _) -> L.rem i pred_prop
235    | _ -> pred_prop
236
237let analyze
238    (f_def : internal_function)
239    : F.valuation =
240  (* extract types of registers from the definition *)
241  let types = RTLabsGraph.compute_type_map f_def in
242
243  let graph = f_def.f_graph in
244  let pred_table =
245    let module U = GraphUtilities.Util(RTLabsGraph) in
246    U.compute_predecessor_lists graph in
247
248  F.lfp (semantics types graph pred_table)
249
250(* now that the info for constants can be gathered, let's put that to use *)
251
252(* this will be used to turn values back into constants. Notice: *)
253(* 1) we are turning abstract offsets and sizes into integers *)
254(* 2) this shares the problem with AST constants of representability *)
255(*    with ocaml 31 bits integers *)
256let cst_of_value = function
257  | L.V v -> Cst_int (Mem.Value.to_int v)
258  | L.S -> Cst_stack
259  | L.A a -> Cst_addrsymbol a
260  | _ -> invalid_arg "cst_of_value"
261
262let arg_from_reg prop types r =
263  try
264    Imm (cst_of_value (L.find_cst r prop), Register.Map.find r types)
265  with
266    | Not_found -> Reg r
267
268let arg_from_arg prop types = function
269  | Reg i -> arg_from_reg prop types i
270  | _ as a -> a
271
272let args_from_args prop types =
273  List.map (arg_from_arg prop types)
274
275let copy i a l = match a with
276  | Reg j -> St_op1 (Op_id, i, j, l)
277  | _ -> assert false (* should already have been substituted *)
278
279let negate i a l = match a with
280  | Reg j -> St_op1 (Op_negint, i, j, l)
281  | _ -> assert false (* should already have been substituted *)
282
283let simpl_imm_op2 op i j k types prop l =
284  let f = function
285    | Imm _ -> None
286    | Reg r ->
287      try
288        Some (L.find_cst r prop)
289      with
290        | Not_found -> None in
291  let one = Mem.Value.of_int 1 in
292  match f j, f k, op with
293    | Some (L.V v), _, (Op_add | Op_addp | Op_or | Op_xor )
294      when Mem.Value.is_false v ->
295      copy i k l
296    | Some (L.V v), _, Op_mul when Mem.Value.equal v one ->
297      copy i j l
298    | _, Some (L.V v), (Op_add | Op_sub | Op_addp | Op_subp | Op_or | Op_xor)
299      when Mem.Value.is_false v ->
300      copy i j l
301    | _, Some (L.V v), (Op_mul | Op_div)  when Mem.Value.equal v one ->
302      copy i j l
303    | Some (L.V v), _, Op_sub when Mem.Value.is_false v ->
304      negate i j l
305    | _ ->
306      St_op2(op, i, arg_from_arg prop types j, arg_from_arg prop types k, l)
307
308(* we transform statements according to the valuation found out by analyze *)
309(* We also turn branchings into redirections if the guard is constant. *)
310let transform
311    (valu : F.valuation)
312    (types: sig_type Register.Map.t)
313    (p    : Label.t)
314    (stmt : statement) : statement list * Label.t list option =
315  match stmt with
316    | St_cst (i, (Cst_offset _ | Cst_sizeof _), next) ->
317      (* we are sure valu has a binding for i, we change the abstract
318         quantities into actual integers *)
319      ([St_cst (i, cst_of_value (L.find_cst i (valu p)), next)] , None)
320    | (St_op1 (_,i,_,next) | St_op2(_,i,_,_,next)) when L.is_cst i (valu p) ->
321      ([St_cst (i, cst_of_value (L.find_cst i (valu p)), next)], None)
322    | St_op2 (op, i, a, b, l) ->
323      ([simpl_imm_op2 op i a b types (valu p) l], None)
324    | St_load (q, a, j, l) ->
325      ([St_load(q, arg_from_arg (valu p) types a, j, l)], None)
326    | St_store (q, a, b, l) ->
327      ([St_store (q, arg_from_arg (valu p) types a,
328                arg_from_arg (valu p) types b, l)], None)
329    | St_cond (i, if_true, if_false) as s when L.is_cst i (valu p) ->
330      (match L.find_cst i (valu p) with
331        | L.V v when Mem.Value.is_false v -> ([], Some [if_false])
332        | L.V _ | L.A _ -> ([], Some [if_true])
333        | _ -> ([s], Some [if_true ; if_false]))
334    | St_return (Some a) ->
335      ([St_return (Some (arg_from_arg (valu p) types a))], None)
336    | St_call_id (f, args, ret, sg, l) ->
337      ([St_call_id (f, args_from_args (valu p) types args, ret, sg, l)], None)
338    | St_call_ptr (f, args, ret, sg, l) ->
339      ([St_call_ptr (f, args_from_args (valu p) types args, ret, sg, l)], None)
340    | St_tailcall_id (f, args, sg) ->
341      ([St_tailcall_id (f, args_from_args (valu p) types args, sg)], None)
342    | St_tailcall_ptr (f, args, sg) ->
343      ([St_tailcall_ptr (f, args_from_args (valu p) types args, sg)], None)
344    | stmt -> ([stmt], None)
345
346let transform_int_function
347    (f_def  : internal_function)
348    : internal_function =
349  let valu = analyze f_def in
350        (* we transform the graph according to the analysis *)
351  let types = RTLabsGraph.compute_type_map f_def in
352  let module U = GraphUtilities.Util(RTLabsGraph) in
353  let module T = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) in
354  let trans =  transform valu types in
355  let fresh () = Label.Gen.fresh f_def.f_luniverse in
356  let graph = T.translate_pure_with_redirects fresh trans f_def.f_graph in
357  let graph = U.dead_code_elim graph f_def.f_entry in
358  {f_def with f_graph = graph}
359
360let transform_function = function
361  | (id, F_int f_def) -> (id, F_int (transform_int_function f_def))
362  | f -> f
363
364let trans = Languages.RTLabs, function
365  | Languages.AstRTLabs p ->
366    Languages.AstRTLabs {p with functs = List.map transform_function p.functs}
367  | _ -> assert false
368
369
Note: See TracBrowser for help on using the repository browser.