source: Deliverables/D2.3/8051-memoryspaces-branch/cparser/Unblock.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: 4.8 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(* Simplification of blocks and initializers within functions *)
17
18(* Assumes: nothing
19   Produces: unblocked code *)
20
21open C
22open Cutil
23open Errors
24
25(* Convert an initializer to a list of assignments.
26   Prepend those assignments to the given statement. *)
27
28let sdoseq loc e s =
29  sseq loc {sdesc = Sdo e; sloc = loc} s
30
31let rec local_initializer loc env path init k =
32  match init with
33  | Init_single e ->
34      sdoseq loc
35        { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp; espace = path.espace }
36        k
37  | Init_array il ->
38      let space, ty_elt =
39        match unroll env path.etyp with
40        | TArray(space, ty_elt, _, _) -> space, ty_elt
41        | _ -> fatal_error "%aWrong type for array initializer" 
42                           formatloc loc in
43      let rec array_init pos = function
44        | [] -> k
45        | i :: il ->
46            local_initializer loc env
47              { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(space, ty_elt, []));
48                etyp = ty_elt;
49                espace = Any }
50              i
51              (array_init (Int64.succ pos) il) in
52      array_init 0L il
53  | Init_struct(id, fil) ->
54      let field_init (fld, i) k =
55        local_initializer loc env
56          { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ; espace = Any } 
57          i k in
58      List.fold_right field_init fil k
59  | Init_union(id, fld, i) ->
60      local_initializer loc env
61        { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ; espace = Any }
62        i k
63
64(* Record new variables to be locally defined *)
65
66let local_variables = ref ([]: decl list)
67
68(* Note: "const int x = y - 1;" is legal, but we turn it into
69   "const int x; x = y - 1;", which is not.  Therefore, remove
70   top-level 'const' attribute.  Also remove it on element type of
71   array type. *)
72
73let remove_const env ty = remove_attributes_type env [AConst] ty
74
75(* Process a variable declaration.
76   The variable is entered in [local_variables].
77   The initializer, if any, is converted into assignments and
78   prepended to [k]. *)
79
80let process_decl loc env (sto, id, ty, optinit) k =
81  let ty' = remove_const env ty in
82  local_variables := (sto, id, ty', None) :: !local_variables;
83  match optinit with
84  | None -> k
85  | Some init ->
86      local_initializer loc env { edesc = EVar id; etyp = ty'; espace = Any } init k
87
88(* Simplification of blocks within a statement *)
89
90let rec unblock_stmt env s =
91  match s.sdesc with
92  | Sskip -> s
93  | Sdo e -> s
94  | Sseq(s1, s2) ->
95      {s with sdesc = Sseq(unblock_stmt env s1, unblock_stmt env s2)}
96  | Sif(e, s1, s2) -> 
97      {s with sdesc = Sif(e, unblock_stmt env s1, unblock_stmt env s2)}
98  | Swhile(e, s1) -> 
99      {s with sdesc = Swhile(e, unblock_stmt env s1)}
100  | Sdowhile(s1, e) ->
101      {s with sdesc = Sdowhile(unblock_stmt env s1, e)}
102  | Sfor(s1, e, s2, s3) ->
103      {s with sdesc = Sfor(unblock_stmt env s1, e, unblock_stmt env s2, unblock_stmt env s3)}
104  | Sbreak -> s
105  | Scontinue -> s
106  | Sswitch(e, s1) ->
107      {s with sdesc = Sswitch(e, unblock_stmt env s1)}
108  | Slabeled(lbl, s1) -> 
109      {s with sdesc = Slabeled(lbl, unblock_stmt env s1)}
110  | Sgoto lbl -> s
111  | Sreturn opte -> s
112  | Sblock sl -> unblock_block env sl
113  | Sdecl d -> assert false
114
115and unblock_block env = function
116  | [] -> sskip
117  | {sdesc = Sdecl d; sloc = loc} :: sl ->
118      process_decl loc env d (unblock_block env sl)
119  | s :: sl ->
120      sseq s.sloc (unblock_stmt env s) (unblock_block env sl)
121
122(* Simplification of blocks within a function *)
123
124let unblock_fundef env f =
125  local_variables := [];
126  let body = unblock_stmt env f.fd_body in
127  let decls = !local_variables in
128  local_variables := [];
129  { f with fd_locals = f.fd_locals @ decls; fd_body = body }
130
131(* Entry point *)
132
133let program p =
134  Transform.program ~fundef:unblock_fundef p
Note: See TracBrowser for help on using the repository browser.