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

Last change on this file since 1572 was 1572, checked in by tranquil, 9 years ago
  • corrected previous bug
  • finished propagating immediates
File size: 11.3 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.Set.t 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 pred prop =
216      L.join (valu pred) prop in
217    Label.Set.fold f (Label.Map.find lbl pred_table) L.bottom 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 = RTLabsUtilities.computes_type_map f_def in
242
243  let graph = f_def.f_graph in
244
245  let pred_table = RTLabsUtilities.compute_predecessors graph in
246
247  F.lfp (semantics types graph pred_table)
248
249(* now that the info for constants can be gathered, let's put that to use *)
250
251(* this will be used to turn values back into constants. Notice: *)
252(* 1) we are turning abstract offsets and sizes into integers *)
253(* 2) this shares the problem with AST constants of representability *)
254(*    with ocaml 31 bits integers *)
255let cst_of_value = function
256  | L.V v -> Cst_int (Mem.Value.to_int v)
257  | L.S -> Cst_stack
258  | L.A a -> Cst_addrsymbol a
259  | _ -> invalid_arg "cst_of_value"
260
261let arg_from_reg prop types r =
262  try
263    Imm (cst_of_value (L.find_cst r prop), Register.Map.find r types)
264  with
265    | Not_found -> Reg r
266
267let arg_from_arg prop types = function
268  | Reg i -> arg_from_reg prop types i
269  | _ as a -> a
270
271let copy i a l = match a with
272  | Reg j -> St_op1 (Op_id, i, j, l)
273  | _ -> assert false (* should already have been substituted *)
274
275let negate i a l = match a with
276  | Reg j -> St_op1 (Op_negint, i, j, l)
277  | _ -> assert false (* should already have been substituted *)
278
279let simpl_imm_op2 op i j k types prop l =
280  let f = function
281    | Imm _ -> None
282    | Reg r ->
283      try
284        Some (L.find_cst r prop)
285      with
286        | Not_found -> None in
287  let one = Mem.Value.of_int 1 in
288  match f j, f k, op with
289    | Some (L.V v), _, (Op_add | Op_addp | Op_or | Op_xor )
290      when Mem.Value.is_false v ->
291      copy i k l
292    | Some (L.V v), _, Op_mul when Mem.Value.equal v one ->
293      copy i j l
294    | _, Some (L.V v), (Op_add | Op_sub | Op_addp | Op_subp | Op_or | Op_xor)
295      when Mem.Value.is_false v ->
296      copy i j l
297    | _, Some (L.V v), (Op_mul | Op_div)  when Mem.Value.equal v one ->
298      copy i j l
299    | Some (L.V v), _, Op_sub when Mem.Value.is_false v ->
300      negate i j l
301    | _ ->
302      St_op2(op, i, arg_from_arg prop types j, arg_from_arg prop types k, l)
303
304(* we transform statements according to the valuation found out by analyze *)
305(* We also turn branchings into redirections if the guard is constant. *)
306let transform_statement
307    (valu : F.valuation)
308    (types: sig_type Register.Map.t)
309    (p    : Label.t)
310    : statement -> statement = function
311      | St_cst (i, (Cst_offset _ | Cst_sizeof _), next) ->
312        (* we are sure valu has a binding for i, we change the abstract
313           quantities into actual integers *)
314        St_cst (i, cst_of_value (L.find_cst i (valu p)), next)
315      | (St_op1 (_,i,_,next) | St_op2(_,i,_,_,next)) when L.is_cst i (valu p) ->
316        St_cst (i, cst_of_value (L.find_cst i (valu p)), next)
317      | St_op2 (op, i, a, b, l) ->
318        simpl_imm_op2 op i a b types (valu p) l
319      | St_load (q, a, j, l) ->
320        St_load(q, arg_from_arg (valu p) types a, j, l)
321      | St_store (q, a, b, l) ->
322        St_store (q, arg_from_arg (valu p) types a,
323                     arg_from_arg (valu p) types b, l)
324      | St_cond (i, if_true, if_false) as s when L.is_cst i (valu p) ->
325        let s = match L.find_cst i (valu p) with
326          | L.V v when Mem.Value.is_false v -> St_skip if_false
327          | L.V _ | L.A _ -> St_skip if_true
328          | _ -> s in s
329      | St_return (Some a) ->
330        St_return (Some (arg_from_arg (valu p) types a))
331      | St_call_id (f, args, ret, sg, l) ->
332        St_call_id (f, List.map (arg_from_arg (valu p) types) args, ret, sg, l)
333      | St_call_ptr (f, args, ret, sg, l) ->
334        St_call_ptr (f, List.map (arg_from_arg (valu p) types) args, ret, sg, l)
335      | St_tailcall_id (f, args, sg) ->
336        St_tailcall_id (f, List.map (arg_from_arg (valu p) types) args, sg)
337      | St_tailcall_ptr (f, args, sg) ->
338        St_tailcall_ptr (f, List.map (arg_from_arg (valu p) types) args, sg)
339      | stmt -> stmt
340
341let transform_int_function
342    (f_def  : internal_function)
343    : internal_function =
344  let valu = analyze f_def in
345        (* we transform the graph according to the analysis *)
346  let types = RTLabsUtilities.computes_type_map f_def in
347  let graph = Label.Map.mapi (transform_statement valu types) f_def.f_graph in
348        (* and we eliminate resulting dead code *)
349  let graph = RTLabsUtilities.dead_code_elim graph f_def.f_entry in
350  {f_def with f_graph = graph}
351
352let transform_function = function
353  | (id, F_int f_def) -> (id, F_int (transform_int_function f_def))
354  | f -> f
355
356let trans = Languages.RTLabs, function
357  | Languages.AstRTLabs p ->
358    Languages.AstRTLabs {p with functs = List.map transform_function p.functs}
359  | _ -> assert false
360
361
Note: See TracBrowser for help on using the repository browser.