cparser/Transform.ml

   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 (* Generic program transformation *)
  17
  18 open C
  19 open Cutil
  20 open Env
  21
  22 (* Recording fresh temporaries *)
  23
  24 let temporaries = ref ([]: decl list)
  25
  26 let reset_temps () =
  27   temporaries := []
  28
  29 let new_temp_var ?(name = "t") ty =
  30   let id = Env.fresh_ident name in
  31   temporaries := (Storage_default, id, ty, None) :: !temporaries;
  32   id
  33
  34 let new_temp ?(name = "t") ty =
  35   let id = new_temp_var ~name ty in
  36   { edesc = EVar id; etyp = ty }
  37
  38 let get_temps () =
  39   let temps = !temporaries in
  40   temporaries := [];
  41   List.rev temps
  42
  43 (* Generic transformation *)
  44
  45 let program
  46     ?(decl = fun env d -> d)
  47     ?(fundef = fun env fd -> fd)
  48     ?(composite = fun env su id fl -> fl)
  49     ?(typedef = fun env id ty -> ty)
  50     p =
  51
  52 (* In all transformations of interest so far, the environment is used only
  53    for its type definitions and struct/union definitions,
  54    so we do not update it for other definitions. *)
  55
  56   let rec transf_globdecls env accu = function
  57   | [] -> List.rev accu
  58   | g :: gl ->
  59       let (desc', env') =
  60         match g.gdesc with
  61         | Gdecl((sto, id, ty, init) as d) ->
  62            (Gdecl(decl env d), Env.add_ident env id sto ty)
  63         | Gfundef f ->
  64            (Gfundef(fundef env f),
  65             Env.add_ident env f.fd_name f.fd_storage (fundef_typ f))
  66         | Gcompositedecl(su, id) ->
  67             (Gcompositedecl(su, id),
  68              Env.add_composite env id (composite_info_decl env su))
  69         | Gcompositedef(su, id, fl) ->
  70             (Gcompositedef(su, id, composite env su id fl),
  71              Env.add_composite env id (composite_info_def env su fl))
  72         | Gtypedef(id, ty) ->
  73             (Gtypedef(id, typedef env id ty), Env.add_typedef env id ty)
  74         | Genumdef _ as gd -> (gd, env)
  75         | Gpragma _ as gd -> (gd, env)
  76       in
  77         transf_globdecls env' ({g with gdesc = desc'} :: accu) gl
  78
  79   in transf_globdecls (Builtins.environment()) [] p