source: Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/constPropagation.ml @ 1468

Last change on this file since 1468 was 1468, checked in by tranquil, 9 years ago
  • implemented constant propagation
  • implementing partial redundancy elimination
File size: 6.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
25  type property =
26      t Register.FlexMap.t
27
28  let bottom : property =
29                Register.FlexMap.empty
30
31  let join_t x y = match x, y with
32                | V v1, V v2 when Mem.Value.equal v1 v2 -> V v1
33                | _ -> T
34
35  let join : property -> property -> property =
36                let choose i b1 b2 = match b1, b2 with
37                        | Some v, Some v' -> Some (join_t v v')
38                        | Some v, None | None, Some v -> Some v
39                        | _ -> None in
40                Register.FlexMap.merge choose
41
42        let bind i v p =
43                let new_binding = 
44                        try
45                                join_t v (Register.FlexMap.find i p)
46                        with
47                                | Not_found -> v in
48                Register.FlexMap.add i new_binding p
49       
50        let find = Register.FlexMap.find
51               
52        let mem = Register.FlexMap.mem
53       
54        let is_cst i p =
55                try
56                        match find i p with
57                                | V _ -> true
58                                | T -> false
59                with
60                        | Not_found -> false
61
62  let find_cst i p =
63          match find i p with
64              | V v -> v
65              | T -> raise Not_found
66
67  let equal : property -> property -> bool =
68                Register.FlexMap.equal (fun x y -> match x, y with
69                        | T, T -> true
70                        | V v1, V v2 -> Mem.Value.equal v1 v2
71                        | _ -> false)
72
73  let is_maximal _ = false
74
75end
76
77module F = Fix.Make (Label.ImpMap) (L)
78
79module Eval = CminorInterpret.Eval_op (Mem)
80  (* evaluation happens in RTLabs memory model ... *)
81
82module MemTarget = Memory.Make (Driver.TargetArch)
83  (* ... but for sizeof and offsets, which rely on the target memory model *)
84
85open AST
86
87let ext_fun_of_sign = function
88  | Signed -> Mem.Value.sign_ext
89  | Unsigned -> Mem.Value.zero_ext
90
91let cast_to_std t v = match t with
92  | Sig_int (size, sign) -> (ext_fun_of_sign sign) v size Mem.int_size
93  | Sig_float _ -> error_float ()
94  | Sig_offset | Sig_ptr -> v
95
96let cst t = function
97  | Cst_int i -> L.V (cast_to_std t (Mem.Value.of_int i))
98  | Cst_offset off -> L.V (Mem.Value.of_int (MemTarget.concrete_offset off))
99  | Cst_sizeof t' ->
100          L.V (cast_to_std t (Mem.Value.of_int (MemTarget.concrete_size t')))
101        | _ -> assert false (* won't call in these cases *)
102
103let do_the_op1 type_of i j op x = match x with
104        | L.V v -> L.V (Eval.op1 (type_of i) (type_of j) op v)
105  | _ -> L.T
106
107let do_the_op2 type_of i j k op x y = match x, y, op with
108        (* consider a constant division by 0 as not constant *)
109        | L.V _, L.V v2, (Op_div | Op_divu | Op_mod | Op_modu)
110          when Mem.Value.is_false v2 -> L.T
111        | L.V v1, L.V v2, _ ->
112                L.V (Eval.op2 (type_of i) (type_of j) (type_of k) op v1 v2)
113        | _ -> L.T
114
115let semantics
116    (types : sig_type Register.Map.t)
117    (graph : statement Label.Map.t)
118                (pred_table : Label.Set.t Label.Map.t)
119                (lbl : Label.t)
120                (valu : F.valuation)
121                : F.property =
122        let pred_prop = (* the situation at the entry of the statement (in [valu]) *)
123                let f pred prop =
124                        L.join (valu pred) prop in
125                Label.Set.fold f (Label.Map.find lbl pred_table) L.bottom in
126        let type_of r = Register.Map.find r types in
127        match Label.Map.find lbl graph with
128    | St_cst (_, Cst_float _, _) -> error_float ()
129                | St_cst (_, (Cst_addrsymbol _ | Cst_stack), _) -> pred_prop
130                | St_cst (i, k, _) -> L.bind i (cst (type_of i) k) pred_prop
131    | St_op1 (op, i, j, _) when L.mem j pred_prop ->
132                        L.bind i (do_the_op1 type_of i j op (L.find j pred_prop)) pred_prop
133    | St_op2 (op,i, j, k, _) when L.mem j pred_prop && L.mem k pred_prop ->
134                        let j_val = L.find j pred_prop in
135                        let k_val = L.find k pred_prop in
136      L.bind i (do_the_op2 type_of i j k op j_val k_val) pred_prop
137    | _ -> pred_prop
138
139let analyze
140    (f_def : internal_function)
141                : F.valuation =
142        (* extract types of registers from the definition *)
143        let types = Register.Map.empty in 
144        let add map (r, typ)  = Register.Map.add r typ map in
145        let types = List.fold_left add types f_def.f_params in
146        let types = List.fold_left add types f_def.f_locals in
147        let types = match f_def.f_result with
148                | None -> types
149                | Some x -> add types x in
150       
151        let graph = f_def.f_graph in
152       
153        let pred_table = RTLabsUtilities.compute_predecessors graph in
154       
155        F.lfp (semantics types graph pred_table)
156               
157(* now that the info for constants can be gathered, let's put that to use *)
158
159(* this will be used to turn values back into constants. Notice: *)
160(* 1) if we have mapped a register to a value, it must be an integer *)
161(* 2) we are turning abstract offsets and sizes into integers *)
162let cst_of_value v = Cst_int (Mem.Value.to_int v)
163
164(* we transform statements according to the valuation found out by analyze *)
165(* We also turn branchings into redirections if the guard is constant. *)
166let transform_statement
167    (valu : F.valuation)
168                (p    : Label.t)
169                : statement -> statement = function
170  | St_cst (i, (Cst_offset _ | Cst_sizeof _), next) ->
171                (* we are sure valu has a binding for i, we change the abstract quantities*)
172                (* into actual integers *)
173                St_cst (i, cst_of_value (L.find_cst i (valu p)), next) 
174        | (St_op1 (_,i,_,next) | St_op2(_,i,_,_,next)) when L.is_cst i (valu p) ->
175                St_cst (i, cst_of_value (L.find_cst i (valu p)), next)
176        | St_cond (i, if_true, if_false) when L.is_cst i (valu p) ->
177                let next =
178                  if Mem.Value.is_true (L.find_cst i (valu p)) then if_true else if_false in
179                St_skip next
180        | stmt -> stmt
181
182let dom (map : 'a Label.Map.t) : Label.Set.t =
183        let add key _ = Label.Set.add key in
184        Label.Map.fold add map Label.Set.empty
185
186let transform_int_function
187    (f_def  : internal_function)
188                : internal_function =
189        let valu = analyze f_def in
190        (* we transform the graph according to the analysis *) 
191        let graph = Label.Map.mapi (transform_statement valu) f_def.f_graph in
192        (* and we eliminate resulting dead code *)
193        {f_def with f_graph = graph}
194
195let transform_function = function
196        | (id, F_int f_def) -> (id, F_int (transform_int_function f_def))
197        | f -> f
198
199let trans = Languages.RTLabs, function
200        | Languages.AstRTLabs p ->
201                Languages.AstRTLabs {p with functs = List.map transform_function p.functs}
202        | _ -> assert false 
203
204         
Note: See TracBrowser for help on using the repository browser.