source: Deliverables/D2.2/8051/src/RTLabs/copyPropagation.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: 3.5 KB
Line 
1open RTLabs
2open AST
3
4let error_prefix = "RTLabs to RTL"
5let error = Error.global_error error_prefix
6
7let error_int () = error "int16 and int32 not supported."
8let error_float () = error "float not supported."
9let error_shift () = error "Shift operations not supported."
10
11
12(* The analysis uses the lattice of maps from registers to values with a top *)
13(* element which indicates the register is known not to be constant. *)
14(* The lattice's join operation is pointwise join, where pointwise bottom is *)
15(* represented by the absence of a binding in the map. *)
16
17module Mem = Driver.RTLabsMemory
18
19module L  = struct
20       
21  type property =
22      Register.t Register.FlexMap.t
23
24  let bottom : property =
25                Register.FlexMap.empty
26               
27        let meet =
28                let choose r ro1 ro2 = match ro1, ro2 with
29                        | Some r1, Some r2 when r1 = r2 -> Some r1
30                        | _ -> None in 
31                Register.FlexMap.merge choose
32
33  let big_meet f = function
34                | [] -> bottom
35                | x :: xs ->
36                        let f' s y = meet s (f y) in
37                        List.fold_left f' (f x) xs
38       
39  let equal : property -> property -> bool =
40                Register.FlexMap.equal Register.equal
41
42  let is_maximal _ = false
43       
44end
45
46let ( --* ) m = function
47        | None -> m
48        | Some r ->
49                let filter s t = not (Register.equal s r || Register.equal t r) in
50                Register.FlexMap.filter filter m
51
52module F = Fix.Make (Label.ImpMap) (L)
53
54let semantics
55    (graph : statement Label.Map.t)
56                (pred_table : Label.t list Label.Map.t)
57                (lbl : Label.t)
58                (valu : F.valuation)
59                : F.property =
60  let copies_out l =
61                let copies_out = valu l in
62                match Label.Map.find l graph with
63                        | St_op1 (Op_id, r, s, _) ->
64                                let copy_of x =
65                                        (try
66                                                Register.FlexMap.find x copies_out
67                                        with
68                                                | Not_found -> x) in
69                                if Register.equal (copy_of r) (copy_of s) then copies_out else
70                                Register.FlexMap.add r s (copies_out --* (Some r))
71                        | stmt -> copies_out --* RTLabsUtilities.modified_at_stmt stmt in
72        L.big_meet copies_out (Label.Map.find lbl pred_table)
73
74let analyze
75    (f_def : internal_function)
76                : F.valuation =
77               
78        let graph = f_def.f_graph in
79       
80        let pred_table = RTLabsUtilities.compute_predecessor_lists graph in
81       
82        F.lfp (semantics graph pred_table)
83
84(* we transform statements according to the valuation found out by analyze *)
85let transform_statement
86    (valu : F.valuation)
87    (p    : Label.t)
88                : statement -> statement =
89        let copy_of x =
90                try
91                        Register.FlexMap.find x (valu p)
92                with
93                        | Not_found -> x in
94        let copy_of_arg = function
95                | Reg x -> Reg (copy_of x)
96                | Imm _ as a -> a in 
97        function
98                | St_op1 (o,i,j,next) -> St_op1(o,i,copy_of j,next)
99                | St_op2 (o,i,j,k,next) -> St_op2(o,i,copy_of_arg j, copy_of_arg k,next)
100          | St_load (q, a, j, l) -> St_load (q, copy_of_arg a, j, l)
101                | St_store (q, a1, a2, l) -> St_store(q, copy_of_arg a1, copy_of_arg a2, l)
102                | St_cond (i, if_true, if_false) -> St_cond (copy_of i, if_true, if_false)
103                | St_call_id (f, args, ret, sign, l) ->
104                        St_call_id (f, List.map copy_of args, ret, sign, l)
105                | St_call_ptr (f, args, ret, sign, l) ->
106            St_call_ptr (f, List.map copy_of args, ret, sign, l)
107                | stmt -> stmt
108
109let transform_int_function
110    (f_def  : internal_function)
111                : internal_function =
112        let valu = analyze f_def in
113        (* we transform the graph according to the analysis *)
114        let graph = Label.Map.mapi (transform_statement valu) f_def.f_graph in
115        {f_def with f_graph = graph}
116
117let transform_function = function
118        | (id, F_int f_def) -> (id, F_int (transform_int_function f_def))
119        | f -> f
120
121let trans = Languages.RTLabs, function
122        | Languages.AstRTLabs p ->
123                Languages.AstRTLabs {p with functs = List.map transform_function p.functs}
124        | _ -> assert false 
125
126         
Note: See TracBrowser for help on using the repository browser.