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

Last change on this file since 1569 was 1569, checked in by tranquil, 9 years ago
  • added in repository some missing files...
File size: 10.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               
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       
85  let equal : property -> property -> bool =
86                Register.FlexMap.equal (fun x y -> match x, y with
87                        | T, T | S, S -> true
88                        | V v1, V v2 -> Mem.Value.equal v1 v2
89                        | A i, A j -> i = j
90                        | _ -> false)
91
92  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
99
100end
101
102module F = Fix.Make (Label.ImpMap) (L)
103
104module Eval = CminorInterpret.Eval_op (Mem)
105  (* evaluation happens in RTLabs memory model ... *)
106
107module MemTarget = Memory.Make (Driver.TargetArch)
108  (* ... but for sizeof and offsets, which rely on the target memory model *)
109
110open AST
111
112let ext_fun_of_sign = function
113  | Signed -> Mem.Value.sign_ext
114  | Unsigned -> Mem.Value.zero_ext
115
116let cast_to_std t v = match t with
117  | Sig_int (size, sign) -> (ext_fun_of_sign sign) v size Mem.int_size
118  | Sig_float _ -> error_float ()
119  | Sig_offset | Sig_ptr -> v
120
121let cst t = function
122  | Cst_int i -> L.V (cast_to_std t (Mem.Value.of_int i))
123  | Cst_offset off -> L.V (Mem.Value.of_int (MemTarget.concrete_offset off))
124  | Cst_sizeof t' ->
125          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
128        | _ -> assert false (* won't call in these cases *)
129
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
133  | _ -> L.T
134
135let do_the_op2 type_of i j k op x y = match x, y, op with
136        (* consider a constant division by 0 as not constant *)
137        | L.V _, L.V v2, (Op_div | Op_divu | Op_mod | Op_modu)
138          when Mem.Value.is_false v2 -> L.T
139        | L.V v1, L.V v2, _ ->
140                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
144        | _ -> 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
163
164let semantics
165    (types : sig_type Register.Map.t)
166    (graph : statement Label.Map.t)
167                (pred_table : Label.Set.t Label.Map.t)
168                (lbl : Label.t)
169                (valu : F.valuation)
170                : F.property =
171        let pred_prop = (* the situation at the entry of the statement (in [valu]) *)
172                let f pred prop =
173                        L.join (valu pred) prop in
174                Label.Set.fold f (Label.Map.find lbl pred_table) L.bottom in
175        let type_of r = Register.Map.find r types in
176        match Label.Map.find lbl graph with
177    | St_cst (_, Cst_float _, _) -> error_float ()
178                | St_cst (i, k, _) -> L.bind i (cst (type_of i) 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 ->
186                        let j_val = L.find j pred_prop in
187                        let k_val = L.find k pred_prop in
188      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
194    | _ -> pred_prop
195
196let analyze
197    (f_def : internal_function)
198                : F.valuation =
199        (* extract types of registers from the definition *)
200  let types = RTLabsUtilities.computes_type_map f_def in
201               
202        let graph = f_def.f_graph in
203       
204        let pred_table = RTLabsUtilities.compute_predecessors graph in
205       
206        F.lfp (semantics types graph pred_table)
207               
208(* now that the info for constants can be gathered, let's put that to use *)
209
210(* this will be used to turn values back into constants. Notice: *)
211(* 1) if we have mapped a register to a value, it must be an integer *)
212(* 2) we are turning abstract offsets and sizes into integers *)
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)
273
274(* we transform statements according to the valuation found out by analyze *)
275(* We also turn branchings into redirections if the guard is constant. *)
276let transform_statement
277    (valu : F.valuation)
278                (types: sig_type Register.Map.t)
279    (p    : Label.t)
280                : statement -> statement = function
281  | St_cst (i, (Cst_offset _ | Cst_sizeof _), next) ->
282                (* we are sure valu has a binding for i, we change the abstract quantities*)
283                (* into actual integers *)
284                St_cst (i, cst_of_value (L.find_cst i (valu p)), next) 
285        | (St_op1 (_,i,_,next) | St_op2(_,i,_,_,next)) when L.is_cst i (valu p) ->
286                St_cst (i, cst_of_value (L.find_cst i (valu p)), 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
300        | stmt -> stmt
301
302let dom (map : 'a Label.Map.t) : Label.Set.t =
303        let add key _ = Label.Set.add key in
304        Label.Map.fold add map Label.Set.empty
305
306let transform_int_function
307    (f_def  : internal_function)
308                : internal_function =
309        let valu = analyze f_def 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
313        (* and we eliminate resulting dead code *)
314        let graph = RTLabsUtilities.dead_code_elim graph f_def.f_entry in
315        {f_def with f_graph = graph}
316
317let transform_function = function
318        | (id, F_int f_def) -> (id, F_int (transform_int_function f_def))
319        | f -> f
320
321let trans = Languages.RTLabs, function
322        | Languages.AstRTLabs p ->
323                Languages.AstRTLabs {p with functs = List.map transform_function p.functs}
324        | _ -> assert false 
325
326         
Note: See TracBrowser for help on using the repository browser.