source: Deliverables/D2.2/8051/cparser/Unblock.ml @ 486

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

Deliverable D2.2

File size: 4.6 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 }
36        k
37  | Init_array il ->
38      let ty_elt =
39        match unroll env path.etyp with
40        | TArray(ty_elt, _, _) -> 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(ty_elt, []));
48                etyp = ty_elt }
49              i
50              (array_init (Int64.succ pos) il) in
51      array_init 0L il
52  | Init_struct(id, fil) ->
53      let field_init (fld, i) k =
54        local_initializer loc env
55          { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ } 
56          i k in
57      List.fold_right field_init fil k
58  | Init_union(id, fld, i) ->
59      local_initializer loc env
60        { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
61        i k
62
63(* Record new variables to be locally defined *)
64
65let local_variables = ref ([]: decl list)
66
67(* Note: "const int x = y - 1;" is legal, but we turn it into
68   "const int x; x = y - 1;", which is not.  Therefore, remove
69   top-level 'const' attribute.  Also remove it on element type of
70   array type. *)
71
72let remove_const env ty = remove_attributes_type env [AConst] ty
73
74(* Process a variable declaration.
75   The variable is entered in [local_variables].
76   The initializer, if any, is converted into assignments and
77   prepended to [k]. *)
78
79let process_decl loc env (sto, id, ty, optinit) k =
80  let ty' = remove_const env ty in
81  local_variables := (sto, id, ty', None) :: !local_variables;
82  match optinit with
83  | None -> k
84  | Some init ->
85      local_initializer loc env { edesc = EVar id; etyp = ty' } init k
86
87(* Simplification of blocks within a statement *)
88
89let rec unblock_stmt env s =
90  match s.sdesc with
91  | Sskip -> s
92  | Sdo e -> s
93  | Sseq(s1, s2) ->
94      {s with sdesc = Sseq(unblock_stmt env s1, unblock_stmt env s2)}
95  | Sif(e, s1, s2) -> 
96      {s with sdesc = Sif(e, unblock_stmt env s1, unblock_stmt env s2)}
97  | Swhile(e, s1) -> 
98      {s with sdesc = Swhile(e, unblock_stmt env s1)}
99  | Sdowhile(s1, e) ->
100      {s with sdesc = Sdowhile(unblock_stmt env s1, e)}
101  | Sfor(s1, e, s2, s3) ->
102      {s with sdesc = Sfor(unblock_stmt env s1, e, unblock_stmt env s2, unblock_stmt env s3)}
103  | Sbreak -> s
104  | Scontinue -> s
105  | Sswitch(e, s1) ->
106      {s with sdesc = Sswitch(e, unblock_stmt env s1)}
107  | Slabeled(lbl, s1) -> 
108      {s with sdesc = Slabeled(lbl, unblock_stmt env s1)}
109  | Sgoto lbl -> s
110  | Sreturn opte -> s
111  | Sblock sl -> unblock_block env sl
112  | Sdecl d -> assert false
113
114and unblock_block env = function
115  | [] -> sskip
116  | {sdesc = Sdecl d; sloc = loc} :: sl ->
117      process_decl loc env d (unblock_block env sl)
118  | s :: sl ->
119      sseq s.sloc (unblock_stmt env s) (unblock_block env sl)
120
121(* Simplification of blocks within a function *)
122
123let unblock_fundef env f =
124  local_variables := [];
125  let body = unblock_stmt env f.fd_body in
126  let decls = !local_variables in
127  local_variables := [];
128  { f with fd_locals = f.fd_locals @ decls; fd_body = body }
129
130(* Entry point *)
131
132let program p =
133  Transform.program ~fundef:unblock_fundef p
Note: See TracBrowser for help on using the repository browser.