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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(* Materialize implicit casts *)
(* Assumes: simplified code
Produces: simplified code
Preserves: unblocked code *)
open C
open Cutil
open Transform
(* We have the option of materializing all casts or leave "widening"
casts implicit. Widening casts are:
- from a small integer type to a larger integer type,
- from a small float type to a larger float type,
- from a pointer type to void *.
*)
let omit_widening_casts = ref false
let widening_cast env tfrom tto =
begin match unroll env tfrom, unroll env tto with
| TInt(k1, _), TInt(k2, _) ->
let r1 = integer_rank k1 and r2 = integer_rank k2 in
r1 < r2 || (r1 = r2 && is_signed_ikind k1 = is_signed_ikind k2)
| TFloat(k1, _), TFloat(k2, _) ->
float_rank k1 <= float_rank k2
| TPtr(ty1, _), TPtr(ty2, _) -> is_void_type env ty2
| _, _ -> false
end
let cast_not_needed env tfrom tto =
let tfrom = pointer_decay env tfrom
and tto = pointer_decay env tto in
compatible_types env tfrom tto
|| (!omit_widening_casts && widening_cast env tfrom tto)
let cast env e tto =
if cast_not_needed env e.etyp tto
then e
else {edesc = ECast(tto, e); etyp = tto}
(* Note: this pass applies only to simplified expressions
because casts cannot be materialized in op= expressions... *)
let rec add_expr env e =
match e.edesc with
| EConst _ -> e
| EVar _ -> e
| ESizeof _ -> e
| EUnop(op, e1) ->
let e1' = add_expr env e1 in
let desc =
match op with
| Ominus | Oplus | Onot ->
EUnop(op, cast env e1' e.etyp)
| Olognot | Oderef | Oaddrof
| Odot _ | Oarrow _ ->
EUnop(op, e1')
| Opreincr | Opredecr | Opostincr | Opostdecr ->
assert false (* not simplified *)
in { edesc = desc; etyp = e.etyp }
| EBinop(op, e1, e2, ty) ->
let e1' = add_expr env e1 in
let e2' = add_expr env e2 in
let desc =
match op with
| Oadd ->
if is_pointer_type env ty
then EBinop(Oadd, e1', e2', ty)
else EBinop(Oadd, cast env e1' ty, cast env e2' ty, ty)
| Osub ->
if is_pointer_type env ty
then EBinop(Osub, e1', e2', ty)
else EBinop(Osub, cast env e1' ty, cast env e2' ty, ty)
| Omul|Odiv|Omod|Oand|Oor|Oxor|Oeq|One|Olt|Ogt|Ole|Oge ->
EBinop(op, cast env e1' ty, cast env e2' ty, ty)
| Oshl|Oshr ->
EBinop(op, cast env e1' ty, e2', ty)
| Oindex | Ologand | Ologor | Ocomma ->
EBinop(op, e1', e2', ty)
| Oassign
| Oadd_assign|Osub_assign|Omul_assign|Odiv_assign|Omod_assign
| Oand_assign|Oor_assign|Oxor_assign|Oshl_assign|Oshr_assign ->
assert false (* not simplified *)
in { edesc = desc; etyp = e.etyp }
| EConditional(e1, e2, e3) ->
{ edesc =
EConditional(add_expr env e1, add_expr env e2, add_expr env e3);
etyp = e.etyp }
| ECast(ty, e1) ->
{ edesc = ECast(ty, add_expr env e1); etyp = e.etyp }
| ECall(e1, el) ->
assert false (* not simplified *)
(* Arguments to a prototyped function *)
let rec add_proto env args params =
match args, params with
| [], _ -> []
| _::_, [] -> add_noproto env args
| arg1 :: argl, (_, ty_p) :: paraml ->
cast env (add_expr env arg1) ty_p ::
add_proto env argl paraml
(* Arguments to a non-prototyped function *)
and add_noproto env args =
match args with
| [] -> []
| arg1 :: argl ->
cast env (add_expr env arg1) (default_argument_conversion env arg1.etyp) ::
add_noproto env argl
(* Arguments to function calls in general *)
let add_arguments env ty_fun args =
let ty_args =
match unroll env ty_fun with
| TFun(res, args, vararg, a) -> args
| TPtr(ty, a) ->
begin match unroll env ty with
| TFun(res, args, vararg, a) -> args
| _ -> assert false
end
| _ -> assert false in
match ty_args with
| None -> add_noproto env args
| Some targs -> add_proto env args targs
(* Toplevel expressions (appearing in Sdo statements) *)
let add_topexpr env loc e =
match e.edesc with
| EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty}, _) ->
let ecall =
{edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
etyp = ty} in
if cast_not_needed env ty lhs.etyp then
sassign loc (add_expr env lhs) ecall
else begin
let tmp = new_temp (erase_attributes_type env ty) in
sseq loc (sassign loc tmp ecall)
(sassign loc (add_expr env lhs) (cast env tmp lhs.etyp))
end
| EBinop(Oassign, lhs, rhs, _) ->
sassign loc (add_expr env lhs) (cast env (add_expr env rhs) lhs.etyp)
| ECall(e1, el) ->
let ecall =
{edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
etyp = e.etyp} in
{sdesc = Sdo ecall; sloc = loc}
| _ ->
assert false
(* Initializers *)
let rec add_init env tto = function
| Init_single e ->
Init_single (cast env (add_expr env e) tto)
| Init_array il ->
let ty_elt =
match unroll env tto with
| TArray(ty, _, _) -> ty | _ -> assert false in
Init_array (List.map (add_init env ty_elt) il)
| Init_struct(id, fil) ->
Init_struct (id, List.map
(fun (fld, i) -> (fld, add_init env fld.fld_typ i))
fil)
| Init_union(id, fld, i) ->
Init_union(id, fld, add_init env fld.fld_typ i)
(* Declarations *)
let add_decl env (sto, id, ty, optinit) =
(sto, id, ty,
begin match optinit with
| None -> None
| Some init -> Some(add_init env ty init)
end)
(* Statements *)
let rec add_stmt env s =
match s.sdesc with
| Sskip -> s
| Sdo e -> add_topexpr env s.sloc e
| Sseq(s1, s2) ->
{sdesc = Sseq(add_stmt env s1, add_stmt env s2); sloc = s.sloc }
| Sif(e, s1, s2) ->
{sdesc = Sif(add_expr env e, add_stmt env s1, add_stmt env s2);
sloc = s.sloc}
| Swhile(e, s1) ->
{sdesc = Swhile(add_expr env e, add_stmt env s1);
sloc = s.sloc}
| Sdowhile(s1, e) ->
{sdesc = Sdowhile(add_stmt env s1, add_expr env e);
sloc = s.sloc}
| Sfor(s1, e, s2, s3) ->
{sdesc = Sfor(add_stmt env s1, add_expr env e, add_stmt env s2,
add_stmt env s3);
sloc = s.sloc}
| Sbreak -> s
| Scontinue -> s
| Sswitch(e, s1) ->
{sdesc = Sswitch(add_expr env e, add_stmt env s1); sloc = s.sloc}
| Slabeled(lbl, s) ->
{sdesc = Slabeled(lbl, add_stmt env s); sloc = s.sloc}
| Sgoto lbl -> s
| Sreturn None -> s
| Sreturn (Some e) ->
{sdesc = Sreturn(Some(add_expr env e)); sloc = s.sloc}
| Sblock sl ->
{sdesc = Sblock(List.map (add_stmt env) sl); sloc = s.sloc}
| Sdecl d ->
{sdesc = Sdecl(add_decl env d); sloc = s.sloc}
let add_fundef env f =
reset_temps();
let body' = add_stmt env f.fd_body in
let temps = get_temps () in
(* fd_locals have no initializers, so no need to transform them *)
{ f with fd_locals = f.fd_locals @ temps; fd_body = body' }
let program ?(all = false) p =
omit_widening_casts := not all;
Transform.program ~decl:add_decl ~fundef:add_fundef p
|
