source: Deliverables/D2.3/8051/cparser/Cleanup.ml @ 453

Last change on this file since 453 was 453, checked in by ayache, 9 years ago

Import of the Paris's sources.

File size: 6.5 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* Removing unused declarations *)
17
18open C
19open Cutil
20
21(* The set of all identifiers referenced so far *)
22let referenced = ref IdentSet.empty
23
24(* Record that a new identifier was added to this set *)
25let ref_changed = ref false
26
27(* Record a reference to an identifier.  If seen for the first time,
28   add it to worklist. *)
29
30let addref id =
31  if not (IdentSet.mem id !referenced) then begin
32(* Printf.printf "Referenced: %s$%d\n" id.name id.stamp; *)
33    referenced := IdentSet.add id !referenced;
34    ref_changed := true
35  end
36
37let needed id =
38  IdentSet.mem id !referenced
39
40(* Iterate [addref] on all syntactic categories. *)
41
42let rec add_typ = function
43  | TPtr(ty, _) -> add_typ ty
44  | TArray(ty, _, _) -> add_typ ty
45  | TFun(res, None, _, _) -> add_typ res
46  | TFun(res, Some params, _, _) -> add_typ res; add_vars params
47  | TNamed(id, _) -> addref id
48  | TStruct(id, _) -> addref id
49  | TUnion(id, _) -> addref id
50  | _ -> ()
51
52and add_vars vl =
53  List.iter (fun (id, ty) -> add_typ ty) vl
54
55let rec add_exp e =
56  add_typ e.etyp; (* perhaps not necessary but play it safe *)
57  match e.edesc with
58  | EConst (CEnum(id, v)) -> addref id
59  | EConst _ -> ()
60  | ESizeof ty -> add_typ ty
61  | EVar id -> addref id
62  | EUnop(op, e1) -> add_exp e1
63  | EBinop(op, e1, e2, ty) -> add_exp e1; add_exp e2
64  | EConditional(e1, e2, e3) -> add_exp e1; add_exp e2; add_exp e3
65  | ECast(ty, e1) -> add_typ ty; add_exp e1
66  | ECall(e1, el) -> add_exp e1; List.iter add_exp el
67
68let rec add_init = function
69  | Init_single e -> add_exp e
70  | Init_array il -> List.iter add_init il
71  | Init_struct(id, il) -> addref id; List.iter (fun (_, i) -> add_init i) il
72  | Init_union(id, _, i) -> addref id; add_init i
73
74let add_decl (sto, id, ty, init) =
75  add_typ ty;
76  match init with None -> () | Some i -> add_init i
77
78let rec add_stmt s =
79  match s.sdesc with
80  | Sskip -> ()
81  | Sdo e -> add_exp e
82  | Sseq(s1, s2) -> add_stmt s1; add_stmt s2
83  | Sif(e, s1, s2) -> add_exp e; add_stmt s1; add_stmt s2
84  | Swhile(e, s1) -> add_exp e; add_stmt s1
85  | Sdowhile(s1, e) -> add_stmt s1; add_exp e
86  | Sfor(e1, e2, e3, s1) -> add_stmt e1; add_exp e2; add_stmt e3; add_stmt s1
87  | Sbreak -> ()
88  | Scontinue -> ()
89  | Sswitch(e, s1) -> add_exp e; add_stmt s1
90  | Slabeled(lbl, s) -> 
91      begin match lbl with Scase e -> add_exp e | _ -> () end;
92      add_stmt s
93  | Sgoto lbl -> ()
94  | Sreturn None -> ()
95  | Sreturn(Some e) -> add_exp e
96  | Sblock sl -> List.iter add_stmt sl
97  | Sdecl d -> add_decl d
98
99let add_fundef f =
100  add_typ f.fd_ret;
101  add_vars f.fd_params;
102  List.iter add_decl f.fd_locals;
103  add_stmt f.fd_body
104
105let add_field f = add_typ f.fld_typ
106
107let add_enum e =
108  List.iter
109    (fun (id, opt_e) -> match opt_e with Some e -> add_exp e | None -> ())
110    e
111
112(* Saturate the set of referenced identifiers, starting with externally
113   visible global declarations *)
114
115let visible_decl (sto, id, ty, init) =
116  sto = Storage_default &&
117  match ty with TFun _ -> false | _ -> true
118
119let rec add_init_globdecls accu = function
120  | [] -> accu
121  | g :: rem ->
122      match g.gdesc with
123      | Gdecl decl when visible_decl decl ->
124          add_decl decl; add_init_globdecls accu rem
125      | Gfundef({fd_storage = Storage_default} as f) ->
126          add_fundef f; add_init_globdecls accu rem
127      | Gdecl _ | Gfundef _ | Gcompositedef _ | Gtypedef _ | Genumdef _ ->
128          (* Keep for later iterations *)
129          add_init_globdecls (g :: accu) rem
130      | Gcompositedecl _ | Gpragma _ ->
131          (* Discard, since these cannot introduce more references later *)
132          add_init_globdecls accu rem
133
134let rec add_needed_globdecls accu = function
135  | [] -> accu
136  | g :: rem ->
137      match g.gdesc with
138      | Gdecl((sto, id, ty, init) as decl) ->
139          if needed id
140          then (add_decl decl; add_needed_globdecls accu rem)
141          else add_needed_globdecls (g :: accu) rem
142      | Gfundef f ->
143          if needed f.fd_name
144          then (add_fundef f; add_needed_globdecls accu rem)
145          else add_needed_globdecls (g :: accu) rem
146      | Gcompositedef(_, id, flds) ->
147          if needed id
148          then (List.iter add_field flds; add_needed_globdecls accu rem)
149          else add_needed_globdecls (g :: accu) rem
150      | Gtypedef(id, ty) ->
151          if needed id
152          then (add_typ ty; add_needed_globdecls accu rem)
153          else add_needed_globdecls (g :: accu) rem
154      | Genumdef(id, enu) ->
155          if List.exists (fun (id, _) -> needed id) enu
156          then (add_enum enu; add_needed_globdecls accu rem)
157          else add_needed_globdecls (g :: accu) rem
158      | _ ->
159          assert false
160
161let saturate p =
162  let rec loop p =
163    if !ref_changed then begin
164      ref_changed := false;
165      loop (add_needed_globdecls [] p)
166    end in
167  ref_changed := false;
168  loop (add_init_globdecls [] p)
169
170(* Remove unreferenced definitions *)
171
172let rec simpl_globdecls accu = function
173  | [] -> accu
174  | g :: rem ->
175      let need =
176        match g.gdesc with
177        | Gdecl((sto, id, ty, init) as decl) -> visible_decl decl || needed id
178        | Gfundef f -> f.fd_storage = Storage_default || needed f.fd_name
179        | Gcompositedecl(_, id) -> needed id
180        | Gcompositedef(_, id, flds) -> needed id
181        | Gtypedef(id, ty) -> needed id
182        | Genumdef(id, enu) -> List.exists (fun (id, _) -> needed id) enu
183        | Gpragma s -> true in
184      if need
185      then simpl_globdecls (g :: accu) rem
186      else simpl_globdecls accu rem
187
188let program p =
189  referenced := IdentSet.empty;
190  saturate p;
191  let p' = simpl_globdecls [] p in
192  referenced := IdentSet.empty;
193  p'
194 
195
196
Note: See TracBrowser for help on using the repository browser.