Switching to the new C parser/elaborator/simplifier

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 196 insertions, 0 deletions

diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
new file mode 100644
index 0000000..be28989
--- /dev/null
+++ b/cparser/Cleanup.ml
@@ -0,0 +1,196 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Removing unused declarations *)
+
+open C
+open Cutil
+
+(* The set of all identifiers referenced so far *)
+let referenced = ref IdentSet.empty
+
+(* Record that a new identifier was added to this set *)
+let ref_changed = ref false
+
+(* Record a reference to an identifier.  If seen for the first time,
+   add it to worklist. *)
+
+let addref id =
+  if not (IdentSet.mem id !referenced) then begin
+(* Printf.printf "Referenced: %s$%d\n" id.name id.stamp; *)
+    referenced := IdentSet.add id !referenced;
+    ref_changed := true
+  end
+
+let needed id =
+  IdentSet.mem id !referenced
+
+(* Iterate [addref] on all syntactic categories. *)
+
+let rec add_typ = function
+  | TPtr(ty, _) -> add_typ ty
+  | TArray(ty, _, _) -> add_typ ty
+  | TFun(res, None, _, _) -> add_typ res
+  | TFun(res, Some params, _, _) -> add_typ res; add_vars params
+  | TNamed(id, _) -> addref id
+  | TStruct(id, _) -> addref id
+  | TUnion(id, _) -> addref id
+  | _ -> ()
+
+and add_vars vl =
+  List.iter (fun (id, ty) -> add_typ ty) vl
+
+let rec add_exp e =
+  add_typ e.etyp; (* perhaps not necessary but play it safe *)
+  match e.edesc with
+  | EConst (CEnum(id, v)) -> addref id
+  | EConst _ -> ()
+  | ESizeof ty -> add_typ ty
+  | EVar id -> addref id
+  | EUnop(op, e1) -> add_exp e1
+  | EBinop(op, e1, e2, ty) -> add_exp e1; add_exp e2
+  | EConditional(e1, e2, e3) -> add_exp e1; add_exp e2; add_exp e3
+  | ECast(ty, e1) -> add_typ ty; add_exp e1
+  | ECall(e1, el) -> add_exp e1; List.iter add_exp el
+
+let rec add_init = function
+  | Init_single e -> add_exp e
+  | Init_array il -> List.iter add_init il
+  | Init_struct(id, il) -> addref id; List.iter (fun (_, i) -> add_init i) il
+  | Init_union(id, _, i) -> addref id; add_init i
+
+let add_decl (sto, id, ty, init) =
+  add_typ ty;
+  match init with None -> () | Some i -> add_init i
+
+let rec add_stmt s =
+  match s.sdesc with
+  | Sskip -> ()
+  | Sdo e -> add_exp e
+  | Sseq(s1, s2) -> add_stmt s1; add_stmt s2
+  | Sif(e, s1, s2) -> add_exp e; add_stmt s1; add_stmt s2
+  | Swhile(e, s1) -> add_exp e; add_stmt s1
+  | Sdowhile(s1, e) -> add_stmt s1; add_exp e
+  | Sfor(e1, e2, e3, s1) -> add_stmt e1; add_exp e2; add_stmt e3; add_stmt s1
+  | Sbreak -> ()
+  | Scontinue -> ()
+  | Sswitch(e, s1) -> add_exp e; add_stmt s1
+  | Slabeled(lbl, s) -> 
+      begin match lbl with Scase e -> add_exp e | _ -> () end;
+      add_stmt s
+  | Sgoto lbl -> ()
+  | Sreturn None -> ()
+  | Sreturn(Some e) -> add_exp e
+  | Sblock sl -> List.iter add_stmt sl
+  | Sdecl d -> add_decl d
+
+let add_fundef f =
+  add_typ f.fd_ret;
+  add_vars f.fd_params;
+  List.iter add_decl f.fd_locals;
+  add_stmt f.fd_body
+
+let add_field f = add_typ f.fld_typ
+
+let add_enum e =
+  List.iter
+    (fun (id, opt_e) -> match opt_e with Some e -> add_exp e | None -> ())
+    e
+
+(* Saturate the set of referenced identifiers, starting with externally
+   visible global declarations *)
+
+let visible_decl (sto, id, ty, init) =
+  sto = Storage_default &&
+  match ty with TFun _ -> false | _ -> true
+
+let rec add_init_globdecls accu = function
+  | [] -> accu
+  | g :: rem ->
+      match g.gdesc with
+      | Gdecl decl when visible_decl decl ->
+          add_decl decl; add_init_globdecls accu rem
+      | Gfundef({fd_storage = Storage_default} as f) ->
+          add_fundef f; add_init_globdecls accu rem
+      | Gdecl _ | Gfundef _ | Gcompositedef _ | Gtypedef _ | Genumdef _ ->
+          (* Keep for later iterations *)
+          add_init_globdecls (g :: accu) rem
+      | Gcompositedecl _ | Gpragma _ ->
+          (* Discard, since these cannot introduce more references later *)
+          add_init_globdecls accu rem
+
+let rec add_needed_globdecls accu = function
+  | [] -> accu
+  | g :: rem ->
+      match g.gdesc with
+      | Gdecl((sto, id, ty, init) as decl) ->
+          if needed id
+          then (add_decl decl; add_needed_globdecls accu rem)
+          else add_needed_globdecls (g :: accu) rem
+      | Gfundef f ->
+          if needed f.fd_name
+          then (add_fundef f; add_needed_globdecls accu rem)
+          else add_needed_globdecls (g :: accu) rem
+      | Gcompositedef(_, id, flds) ->
+          if needed id
+          then (List.iter add_field flds; add_needed_globdecls accu rem)
+          else add_needed_globdecls (g :: accu) rem
+      | Gtypedef(id, ty) ->
+          if needed id
+          then (add_typ ty; add_needed_globdecls accu rem)
+          else add_needed_globdecls (g :: accu) rem
+      | Genumdef(id, enu) ->
+          if List.exists (fun (id, _) -> needed id) enu
+          then (add_enum enu; add_needed_globdecls accu rem)
+          else add_needed_globdecls (g :: accu) rem
+      | _ ->
+          assert false
+
+let saturate p =
+  let rec loop p =
+    if !ref_changed then begin
+      ref_changed := false;
+      loop (add_needed_globdecls [] p)
+    end in
+  ref_changed := false;
+  loop (add_init_globdecls [] p)
+
+(* Remove unreferenced definitions *)
+
+let rec simpl_globdecls accu = function
+  | [] -> accu
+  | g :: rem ->
+      let need =
+        match g.gdesc with
+        | Gdecl((sto, id, ty, init) as decl) -> visible_decl decl || needed id
+        | Gfundef f -> f.fd_storage = Storage_default || needed f.fd_name
+        | Gcompositedecl(_, id) -> needed id
+        | Gcompositedef(_, id, flds) -> needed id
+        | Gtypedef(id, ty) -> needed id
+        | Genumdef(id, enu) -> List.exists (fun (id, _) -> needed id) enu
+        | Gpragma s -> true in
+      if need
+      then simpl_globdecls (g :: accu) rem
+      else simpl_globdecls accu rem
+
+let program p =
+  referenced := IdentSet.empty;
+  saturate p;
+  let p' = simpl_globdecls [] p in
+  referenced := IdentSet.empty;
+  p'
+  
+
+