1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
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. *)
14 (* *********************************************************************)
16 (* Simplification of blocks and initializers within functions *)
19 Produces: unblocked code *)
25 (* Convert an initializer to a list of assignments.
26 Prepend those assignments to the given statement. *)
29 sseq loc {sdesc = Sdo e; sloc = loc} s
31 let rec local_initializer loc env path init k =
35 { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp }
39 match unroll env path.etyp with
40 | TArray(ty_elt, _, _) -> ty_elt
41 | _ -> fatal_error "%aWrong type for array initializer"
43 let rec array_init pos = function
46 local_initializer loc env
47 { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(ty_elt, []));
50 (array_init (Int64.succ pos) il) in
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 }
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 }
63 (* Record new variables to be locally defined *)
65 let local_variables = ref ([]: decl list)
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
72 let remove_const env ty = remove_attributes_type env [AConst] ty
74 (* Process a variable declaration.
75 The variable is entered in [local_variables].
76 The initializer, if any, is converted into assignments and
79 let 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;
85 local_initializer loc env { edesc = EVar id; etyp = ty' } init k
87 (* Simplification of blocks within a statement *)
89 let rec unblock_stmt env s =
94 {s with sdesc = Sseq(unblock_stmt env s1, unblock_stmt env s2)}
96 {s with sdesc = Sif(e, unblock_stmt env s1, unblock_stmt env s2)}
98 {s with sdesc = Swhile(e, unblock_stmt env s1)}
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)}
106 {s with sdesc = Sswitch(e, unblock_stmt env s1)}
107 | Slabeled(lbl, s1) ->
108 {s with sdesc = Slabeled(lbl, unblock_stmt env s1)}
111 | Sblock sl -> unblock_block env sl
112 | Sdecl d -> assert false
114 and unblock_block env = function
116 | {sdesc = Sdecl d; sloc = loc} :: sl ->
117 process_decl loc env d (unblock_block env sl)
119 sseq s.sloc (unblock_stmt env s) (unblock_block env sl)
121 (* Simplification of blocks within a function *)
123 let 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 }
133 Transform.program ~fundef:unblock_fundef p