source: Deliverables/D2.3/8051-memoryspaces-branch/cparser/AddCasts.ml @ 460

Last change on this file since 460 was 460, checked in by campbell, 9 years ago

Port memory spaces changes to latest prototype compiler.

File size: 8.3 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(sp1, ty1, _), TPtr(sp2, ty2, _) when sp1 = sp2 -> 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; espace = Any}
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; espace = e.espace }
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; espace = e.espace }
101  | EConditional(e1, e2, e3) ->
102      { edesc = 
103          EConditional(add_expr env e1, add_expr env e2, add_expr env e3);
104        etyp = e.etyp;
105        espace = e.espace }
106  | ECast(ty, e1) ->
107      { edesc = ECast(ty, add_expr env e1); etyp = e.etyp; espace = e.espace }
108  | ECall(e1, el) ->
109      assert false (* not simplified *)
110
111(* Arguments to a prototyped function *)
112
113let rec add_proto env args params =
114  match args, params with
115  | [], _ -> []
116  | _::_, [] -> add_noproto env args
117  | arg1 :: argl, (_, ty_p) :: paraml ->
118      cast env (add_expr env arg1) ty_p ::
119      add_proto env argl paraml
120
121(* Arguments to a non-prototyped function *)
122
123and add_noproto env args =
124  match args with
125  | [] -> []
126  | arg1 :: argl ->
127      cast env (add_expr env arg1) (default_argument_conversion env arg1.etyp) ::
128      add_noproto env argl
129
130(* Arguments to function calls in general *)
131
132let add_arguments env ty_fun args =
133  let ty_args =
134    match unroll env ty_fun with
135    | TFun(res, args, vararg, a) -> args
136    | TPtr(_, ty, a) ->
137        begin match unroll env ty with
138        | TFun(res, args, vararg, a) -> args
139        | _ -> assert false
140        end
141    | _ -> assert false in
142  match ty_args with
143  | None -> add_noproto env args
144  | Some targs -> add_proto env args targs
145
146(* Toplevel expressions (appearing in Sdo statements) *)
147
148let add_topexpr env loc e =
149  match e.edesc with
150  | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty; espace = space}, _) ->
151      let ecall =
152        {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
153         etyp = ty; espace = space} in
154      if cast_not_needed env ty lhs.etyp then
155        sassign loc (add_expr env lhs) ecall
156      else begin
157        let tmp = new_temp (erase_attributes_type env ty) in
158        sseq loc (sassign loc tmp ecall) 
159                 (sassign loc (add_expr env lhs) (cast env tmp lhs.etyp))
160      end
161  | EBinop(Oassign, lhs, rhs, _) ->
162      sassign loc (add_expr env lhs) (cast env (add_expr env rhs) lhs.etyp)
163  | ECall(e1, el) ->
164      let ecall =
165        {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
166         etyp = e.etyp; espace = e.espace} in
167      {sdesc = Sdo ecall; sloc = loc}
168  | _ ->
169      assert false
170
171(* Initializers *)
172
173let rec add_init env tto = function
174  | Init_single e ->
175      Init_single (cast env (add_expr env e) tto)
176  | Init_array il ->
177      let ty_elt =
178        match unroll env tto with
179        | TArray(_,ty, _, _) -> ty | _ -> assert false in
180      Init_array (List.map (add_init env ty_elt) il)
181  | Init_struct(id, fil) ->
182      Init_struct (id, List.map
183                         (fun (fld, i) -> (fld, add_init env fld.fld_typ i))
184                         fil)
185  | Init_union(id, fld, i) ->
186      Init_union(id, fld, add_init env fld.fld_typ i)
187
188(* Declarations *)
189
190let add_decl env (sto, id, ty, optinit) =
191  (sto, id, ty,
192   begin match optinit with
193         | None -> None
194         | Some init -> Some(add_init env ty init)
195   end)
196
197(* Statements *)
198
199let rec add_stmt env f s =
200  match s.sdesc with
201  | Sskip -> s
202  | Sdo e -> add_topexpr env s.sloc e
203  | Sseq(s1, s2) -> 
204      {sdesc = Sseq(add_stmt env f s1, add_stmt env f s2); sloc = s.sloc }
205  | Sif(e, s1, s2) ->
206      {sdesc = Sif(add_expr env e, add_stmt env f s1, add_stmt env f s2);
207       sloc = s.sloc}
208  | Swhile(e, s1) ->
209      {sdesc = Swhile(add_expr env e, add_stmt env f s1);
210       sloc = s.sloc}
211  | Sdowhile(s1, e) ->
212      {sdesc = Sdowhile(add_stmt env f s1, add_expr env e);
213       sloc = s.sloc}
214  | Sfor(s1, e, s2, s3) ->
215      {sdesc = Sfor(add_stmt env f s1, add_expr env e, add_stmt env f s2,
216                    add_stmt env f s3);
217       sloc = s.sloc}
218  | Sbreak -> s
219  | Scontinue -> s
220  | Sswitch(e, s1) ->
221      {sdesc = Sswitch(add_expr env e, add_stmt env f s1); sloc = s.sloc}
222  | Slabeled(lbl, s) ->
223      {sdesc = Slabeled(lbl, add_stmt env f s); sloc = s.sloc}
224  | Sgoto lbl -> s
225  | Sreturn None -> s
226  | Sreturn (Some e) ->
227      {sdesc = Sreturn(Some(cast env (add_expr env e) f.fd_ret)); sloc = s.sloc}
228  | Sblock sl ->
229      {sdesc = Sblock(List.map (add_stmt env f) sl); sloc = s.sloc}
230  | Sdecl d ->
231      {sdesc = Sdecl(add_decl env d); sloc = s.sloc}
232
233let add_fundef env f =
234  reset_temps();
235  let body' = add_stmt env f f.fd_body in
236  let temps = get_temps () in
237  (* fd_locals have no initializers, so no need to transform them *)
238  { f with fd_locals = f.fd_locals @ temps; fd_body = body' }
239
240
241let program ?(all = false) p =
242  omit_widening_casts := not all;
243  Transform.program ~decl:add_decl ~fundef:add_fundef p
Note: See TracBrowser for help on using the repository browser.