source: Deliverables/D2.3/8051-memoryspaces-branch/cparser/Transform.ml @ 460

Last change on this file since 460 was 460, checked in by campbell, 9 years ago

Port memory spaces changes to latest prototype compiler.

File size: 2.9 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(* Generic program transformation *)
17
18open C
19open Cutil
20open Env
21
22(* Recording fresh temporaries *)
23
24let temporaries = ref ([]: decl list)
25
26let reset_temps () =
27  temporaries := []
28
29let 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
34let new_temp ?(name = "t") ty =
35  let id = new_temp_var ~name ty in
36  { edesc = EVar id; etyp = ty; espace = Any (* Always stack allocated? *) }
37
38let get_temps () =
39  let temps = !temporaries in
40  temporaries := [];
41  List.rev temps
42
43(* Generic transformation *)
44
45let 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 (sp, ((sto, id, ty, init) as d)) ->
62           (Gdecl(sp, decl env d), Env.add_ident env id sto ty sp)
63        | Gfundef f ->
64           (Gfundef(fundef env f),
65            Env.add_ident env f.fd_name f.fd_storage (fundef_typ f) Code)
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
Note: See TracBrowser for help on using the repository browser.