1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(* Simplification of blocks and initializers within functions *)
(* Assumes: nothing
Produces: unblocked code *)
open C
open Cutil
open Cerrors
(* Convert an initializer to a list of assignments.
Prepend those assignments to the given statement. *)
let sdoseq loc e s =
sseq loc {sdesc = Sdo e; sloc = loc} s
let rec local_initializer loc env path init k =
match init with
| Init_single e ->
sdoseq loc
{ edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp }
k
| Init_array il ->
let (ty_elt, sz) =
match unroll env path.etyp with
| TArray(ty_elt, Some sz, _) -> (ty_elt, sz)
| _ -> fatal_error "%aWrong type for array initializer"
formatloc loc in
let rec array_init pos il =
if pos >= sz then k else begin
let (i1, il') =
match il with
| [] -> (default_init env ty_elt, [])
| i1 :: il' -> (i1, il') in
local_initializer loc env
{ edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(ty_elt, []));
etyp = ty_elt }
i1
(array_init (Int64.succ pos) il')
end in
array_init 0L il
| Init_struct(id, fil) ->
let field_init (fld, i) k =
local_initializer loc env
{ edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
i k in
List.fold_right field_init fil k
| Init_union(id, fld, i) ->
local_initializer loc env
{ edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
i k
(* Record new variables to be locally defined *)
let local_variables = ref ([]: decl list)
(* Note: "const int x = y - 1;" is legal, but we turn it into
"const int x; x = y - 1;", which is not. Therefore, remove
top-level 'const' attribute. Also remove it on element type of
array type. *)
let remove_const env ty = remove_attributes_type env [AConst] ty
(* Process a variable declaration.
The variable is entered in [local_variables].
The initializer, if any, is converted into assignments and
prepended to [k]. *)
let process_decl loc env (sto, id, ty, optinit) k =
let ty' = remove_const env ty in
local_variables := (sto, id, ty', None) :: !local_variables;
match optinit with
| None -> k
| Some init ->
local_initializer loc env { edesc = EVar id; etyp = ty' } init k
(* Simplification of blocks within a statement *)
let rec unblock_stmt env s =
match s.sdesc with
| Sskip -> s
| Sdo e -> s
| Sseq(s1, s2) ->
{s with sdesc = Sseq(unblock_stmt env s1, unblock_stmt env s2)}
| Sif(e, s1, s2) ->
{s with sdesc = Sif(e, unblock_stmt env s1, unblock_stmt env s2)}
| Swhile(e, s1) ->
{s with sdesc = Swhile(e, unblock_stmt env s1)}
| Sdowhile(s1, e) ->
{s with sdesc = Sdowhile(unblock_stmt env s1, e)}
| Sfor(s1, e, s2, s3) ->
{s with sdesc = Sfor(unblock_stmt env s1, e, unblock_stmt env s2, unblock_stmt env s3)}
| Sbreak -> s
| Scontinue -> s
| Sswitch(e, s1) ->
{s with sdesc = Sswitch(e, unblock_stmt env s1)}
| Slabeled(lbl, s1) ->
{s with sdesc = Slabeled(lbl, unblock_stmt env s1)}
| Sgoto lbl -> s
| Sreturn opte -> s
| Sblock sl -> unblock_block env sl
| Sdecl d -> assert false
| Sasm _ -> s
and unblock_block env = function
| [] -> sskip
| {sdesc = Sdecl d; sloc = loc} :: sl ->
process_decl loc env d (unblock_block env sl)
| s :: sl ->
sseq s.sloc (unblock_stmt env s) (unblock_block env sl)
(* Simplification of blocks within a function *)
let unblock_fundef env f =
local_variables := [];
let body = unblock_stmt env f.fd_body in
let decls = !local_variables in
local_variables := [];
{ f with fd_locals = f.fd_locals @ decls; fd_body = body }
(* Entry point *)
let program p =
Transform.program ~fundef:unblock_fundef p
|
