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 (* Materialize implicit casts *)
18 (* Assumes: simplified code
19 Produces: simplified code
20 Preserves: unblocked code *)
26 (* We have the option of materializing all casts or leave "widening"
27 casts implicit. Widening casts are:
28 - from a small integer type to a larger integer type,
29 - from a small float type to a larger float type,
30 - from a pointer type to void *.
33 let omit_widening_casts = ref false
35 let widening_cast env tfrom tto =
36 begin match unroll env tfrom, unroll env tto with
37 | TInt(k1, _), TInt(k2, _) ->
38 let r1 = integer_rank k1 and r2 = integer_rank k2 in
39 r1 < r2 || (r1 = r2 && is_signed_ikind k1 = is_signed_ikind k2)
40 | TFloat(k1, _), TFloat(k2, _) ->
41 float_rank k1 <= float_rank k2
42 | TPtr(ty1, _), TPtr(ty2, _) -> is_void_type env ty2
46 let cast_not_needed env tfrom tto =
47 let tfrom = pointer_decay env tfrom
48 and tto = pointer_decay env tto in
49 compatible_types env tfrom tto
50 || (!omit_widening_casts && widening_cast env tfrom tto)
53 if cast_not_needed env e.etyp tto
55 else {edesc = ECast(tto, e); etyp = tto}
57 (* Note: this pass applies only to simplified expressions
58 because casts cannot be materialized in op= expressions... *)
60 let rec add_expr env e =
66 let e1' = add_expr env e1 in
69 | Ominus | Oplus | Onot ->
70 EUnop(op, cast env e1' e.etyp)
71 | Olognot | Oderef | Oaddrof
72 | Odot _ | Oarrow _ ->
74 | Opreincr | Opredecr | Opostincr | Opostdecr ->
75 assert false (* not simplified *)
76 in { edesc = desc; etyp = e.etyp }
77 | EBinop(op, e1, e2, ty) ->
78 let e1' = add_expr env e1 in
79 let e2' = add_expr env e2 in
83 if is_pointer_type env ty
84 then EBinop(Oadd, e1', e2', ty)
85 else EBinop(Oadd, cast env e1' ty, cast env e2' ty, ty)
87 if is_pointer_type env ty
88 then EBinop(Osub, e1', e2', ty)
89 else EBinop(Osub, cast env e1' ty, cast env e2' ty, ty)
90 | Omul|Odiv|Omod|Oand|Oor|Oxor|Oeq|One|Olt|Ogt|Ole|Oge ->
91 EBinop(op, cast env e1' ty, cast env e2' ty, ty)
93 EBinop(op, cast env e1' ty, e2', ty)
94 | Oindex | Ologand | Ologor | Ocomma ->
95 EBinop(op, e1', e2', ty)
97 | Oadd_assign|Osub_assign|Omul_assign|Odiv_assign|Omod_assign
98 | Oand_assign|Oor_assign|Oxor_assign|Oshl_assign|Oshr_assign ->
99 assert false (* not simplified *)
100 in { edesc = desc; etyp = e.etyp }
101 | EConditional(e1, e2, e3) ->
103 EConditional(add_expr env e1, add_expr env e2, add_expr env e3);
106 { edesc = ECast(ty, add_expr env e1); etyp = e.etyp }
108 assert false (* not simplified *)
110 (* Arguments to a prototyped function *)
112 let rec add_proto env args params =
113 match args, params with
115 | _::_, [] -> add_noproto env args
116 | arg1 :: argl, (_, ty_p) :: paraml ->
117 cast env (add_expr env arg1) ty_p ::
118 add_proto env argl paraml
120 (* Arguments to a non-prototyped function *)
122 and add_noproto env args =
126 cast env (add_expr env arg1) (default_argument_conversion env arg1.etyp) ::
129 (* Arguments to function calls in general *)
131 let add_arguments env ty_fun args =
133 match unroll env ty_fun with
134 | TFun(res, args, vararg, a) -> args
136 begin match unroll env ty with
137 | TFun(res, args, vararg, a) -> args
140 | _ -> assert false in
142 | None -> add_noproto env args
143 | Some targs -> add_proto env args targs
145 (* Toplevel expressions (appearing in Sdo statements) *)
147 let add_topexpr env loc e =
149 | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty}, _) ->
151 {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
153 if cast_not_needed env ty lhs.etyp then
154 sassign loc (add_expr env lhs) ecall
156 let tmp = new_temp (erase_attributes_type env ty) in
157 sseq loc (sassign loc tmp ecall)
158 (sassign loc (add_expr env lhs) (cast env tmp lhs.etyp))
160 | EBinop(Oassign, lhs, rhs, _) ->
161 sassign loc (add_expr env lhs) (cast env (add_expr env rhs) lhs.etyp)
164 {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
166 {sdesc = Sdo ecall; sloc = loc}
172 let rec add_init env tto = function
174 Init_single (cast env (add_expr env e) tto)
177 match unroll env tto with
178 | TArray(ty, _, _) -> ty | _ -> assert false in
179 Init_array (List.map (add_init env ty_elt) il)
180 | Init_struct(id, fil) ->
181 Init_struct (id, List.map
182 (fun (fld, i) -> (fld, add_init env fld.fld_typ i))
184 | Init_union(id, fld, i) ->
185 Init_union(id, fld, add_init env fld.fld_typ i)
189 let add_decl env (sto, id, ty, optinit) =
191 begin match optinit with
193 | Some init -> Some(add_init env ty init)
198 let rec add_stmt env f s =
201 | Sdo e -> add_topexpr env s.sloc e
203 {sdesc = Sseq(add_stmt env f s1, add_stmt env f s2); sloc = s.sloc }
205 {sdesc = Sif(add_expr env e, add_stmt env f s1, add_stmt env f s2);
208 {sdesc = Swhile(add_expr env e, add_stmt env f s1);
211 {sdesc = Sdowhile(add_stmt env f s1, add_expr env e);
213 | Sfor(s1, e, s2, s3) ->
214 {sdesc = Sfor(add_stmt env f s1, add_expr env e, add_stmt env f s2,
220 {sdesc = Sswitch(add_expr env e, add_stmt env f s1); sloc = s.sloc}
221 | Slabeled(lbl, s) ->
222 {sdesc = Slabeled(lbl, add_stmt env f s); sloc = s.sloc}
225 | Sreturn (Some e) ->
226 {sdesc = Sreturn(Some(cast env (add_expr env e) f.fd_ret)); sloc = s.sloc}
228 {sdesc = Sblock(List.map (add_stmt env f) sl); sloc = s.sloc}
230 {sdesc = Sdecl(add_decl env d); sloc = s.sloc}
232 let add_fundef env f =
234 let body' = add_stmt env f f.fd_body in
235 let temps = get_temps () in
236 (* fd_locals have no initializers, so no need to transform them *)
237 { f with fd_locals = f.fd_locals @ temps; fd_body = body' }
240 let program ?(all = false) p =
241 omit_widening_casts := not all;
242 Transform.program ~decl:add_decl ~fundef:add_fundef p