source: Deliverables/D2.2/8051/cparser/AddCasts.ml @ 2430

Last change on this file since 2430 was 2430, checked in by campbell, 7 years ago

Fix casting for conditionals in CompCert?-derived C parser.

File size: 8.2 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(* Materialize implicit casts *)
17
18(* Assumes: simplified code
19   Produces: simplified code
20   Preserves: unblocked code *)
21
22open C
23open Cutil
24open Transform
25
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 *.
31*)
32
33let omit_widening_casts = ref false
34
35let 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
43  | _, _ -> false
44  end
45
46let 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)
51
52let cast env e tto =
53  if cast_not_needed env e.etyp tto
54  then e
55  else {edesc = ECast(tto, e); etyp = tto}
56
57(* Note: this pass applies only to simplified expressions
58   because casts cannot be materialized in op= expressions... *)
59
60let rec add_expr env e =
61  match e.edesc with
62  | EConst _ -> e
63  | EVar _ -> e
64  | ESizeof _ -> e
65  | EUnop(op, e1) ->
66      let e1' = add_expr env e1 in
67      let desc =
68        match op with
69        | Ominus | Oplus | Onot ->
70            EUnop(op, cast env e1' e.etyp)
71        | Olognot | Oderef | Oaddrof
72        | Odot _ | Oarrow _ ->
73            EUnop(op, e1')
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
80      let desc =
81        match op with
82        | Oadd ->
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)
86        | Osub ->
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)
92        | Oshl|Oshr ->
93            EBinop(op, cast env e1' ty, e2', ty)
94        | Oindex | Ologand | Ologor | Ocomma ->
95            EBinop(op, e1', e2', ty)
96        | Oassign
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) ->
102      let e2' = add_expr env e2 in
103      let e3' = add_expr env e3 in
104      { edesc = 
105          EConditional(add_expr env e1, cast env e2' e.etyp, cast env e3' e.etyp);
106        etyp = e.etyp }
107  | ECast(ty, e1) ->
108      { edesc = ECast(ty, add_expr env e1); etyp = e.etyp }
109  | ECall(e1, el) ->
110      assert false (* not simplified *)
111
112(* Arguments to a prototyped function *)
113
114let rec add_proto env args params =
115  match args, params with
116  | [], _ -> []
117  | _::_, [] -> add_noproto env args
118  | arg1 :: argl, (_, ty_p) :: paraml ->
119      cast env (add_expr env arg1) ty_p ::
120      add_proto env argl paraml
121
122(* Arguments to a non-prototyped function *)
123
124and add_noproto env args =
125  match args with
126  | [] -> []
127  | arg1 :: argl ->
128      cast env (add_expr env arg1) (default_argument_conversion env arg1.etyp) ::
129      add_noproto env argl
130
131(* Arguments to function calls in general *)
132
133let add_arguments env ty_fun args =
134  let ty_args =
135    match unroll env ty_fun with
136    | TFun(res, args, vararg, a) -> args
137    | TPtr(ty, a) ->
138        begin match unroll env ty with
139        | TFun(res, args, vararg, a) -> args
140        | _ -> assert false
141        end
142    | _ -> assert false in
143  match ty_args with
144  | None -> add_noproto env args
145  | Some targs -> add_proto env args targs
146
147(* Toplevel expressions (appearing in Sdo statements) *)
148
149let add_topexpr env loc e =
150  match e.edesc with
151  | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty}, _) ->
152      let ecall =
153        {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
154         etyp = ty} in
155      if cast_not_needed env ty lhs.etyp then
156        sassign loc (add_expr env lhs) ecall
157      else begin
158        let tmp = new_temp (erase_attributes_type env ty) in
159        sseq loc (sassign loc tmp ecall) 
160                 (sassign loc (add_expr env lhs) (cast env tmp lhs.etyp))
161      end
162  | EBinop(Oassign, lhs, rhs, _) ->
163      sassign loc (add_expr env lhs) (cast env (add_expr env rhs) lhs.etyp)
164  | ECall(e1, el) ->
165      let ecall =
166        {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
167         etyp = e.etyp} in
168      {sdesc = Sdo ecall; sloc = loc}
169  | _ ->
170      assert false
171
172(* Initializers *)
173
174let rec add_init env tto = function
175  | Init_single e ->
176      Init_single (cast env (add_expr env e) tto)
177  | Init_array il ->
178      let ty_elt =
179        match unroll env tto with
180        | TArray(ty, _, _) -> ty | _ -> assert false in
181      Init_array (List.map (add_init env ty_elt) il)
182  | Init_struct(id, fil) ->
183      Init_struct (id, List.map
184                         (fun (fld, i) -> (fld, add_init env fld.fld_typ i))
185                         fil)
186  | Init_union(id, fld, i) ->
187      Init_union(id, fld, add_init env fld.fld_typ i)
188
189(* Declarations *)
190
191let add_decl env (sto, id, ty, optinit) =
192  (sto, id, ty,
193   begin match optinit with
194         | None -> None
195         | Some init -> Some(add_init env ty init)
196   end)
197
198(* Statements *)
199
200let rec add_stmt env f s =
201  match s.sdesc with
202  | Sskip -> s
203  | Sdo e -> add_topexpr env s.sloc e
204  | Sseq(s1, s2) -> 
205      {sdesc = Sseq(add_stmt env f s1, add_stmt env f s2); sloc = s.sloc }
206  | Sif(e, s1, s2) ->
207      {sdesc = Sif(add_expr env e, add_stmt env f s1, add_stmt env f s2);
208       sloc = s.sloc}
209  | Swhile(e, s1) ->
210      {sdesc = Swhile(add_expr env e, add_stmt env f s1);
211       sloc = s.sloc}
212  | Sdowhile(s1, e) ->
213      {sdesc = Sdowhile(add_stmt env f s1, add_expr env e);
214       sloc = s.sloc}
215  | Sfor(s1, e, s2, s3) ->
216      {sdesc = Sfor(add_stmt env f s1, add_expr env e, add_stmt env f s2,
217                    add_stmt env f s3);
218       sloc = s.sloc}
219  | Sbreak -> s
220  | Scontinue -> s
221  | Sswitch(e, s1) ->
222      {sdesc = Sswitch(add_expr env e, add_stmt env f s1); sloc = s.sloc}
223  | Slabeled(lbl, s) ->
224      {sdesc = Slabeled(lbl, add_stmt env f s); sloc = s.sloc}
225  | Sgoto lbl -> s
226  | Sreturn None -> s
227  | Sreturn (Some e) ->
228      {sdesc = Sreturn(Some(cast env (add_expr env e) f.fd_ret)); sloc = s.sloc}
229  | Sblock sl ->
230      {sdesc = Sblock(List.map (add_stmt env f) sl); sloc = s.sloc}
231  | Sdecl d ->
232      {sdesc = Sdecl(add_decl env d); sloc = s.sloc}
233
234let add_fundef env f =
235  reset_temps();
236  let body' = add_stmt env f f.fd_body in
237  let temps = get_temps () in
238  (* fd_locals have no initializers, so no need to transform them *)
239  { f with fd_locals = f.fd_locals @ temps; fd_body = body' }
240
241
242let program ?(all = false) p =
243  omit_widening_casts := not all;
244  Transform.program ~decl:add_decl ~fundef:add_fundef p
Note: See TracBrowser for help on using the repository browser.