cparser/AddCasts.ml

   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
  22 open C
  23 open Cutil
  24 open 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
  33 let omit_widening_casts = ref false
  34
  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
  43   | _, _ -> false
  44   end
  45
  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)
  51
  52 let 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
  60 let 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       { edesc =
 103           EConditional(add_expr env e1, add_expr env e2, add_expr env e3);
 104         etyp = e.etyp }
 105   | ECast(ty, e1) ->
 106       { edesc = ECast(ty, add_expr env e1); etyp = e.etyp }
 107   | ECall(e1, el) ->
 108       assert false (* not simplified *)
 109
 110 (* Arguments to a prototyped function *)
 111
 112 let rec add_proto env args params =
 113   match args, params with
 114   | [], _ -> []
 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
 119
 120 (* Arguments to a non-prototyped function *)
 121
 122 and add_noproto env args =
 123   match args with
 124   | [] -> []
 125   | arg1 :: argl ->
 126       cast env (add_expr env arg1) (default_argument_conversion env arg1.etyp) ::
 127       add_noproto env argl
 128
 129 (* Arguments to function calls in general *)
 130
 131 let add_arguments env ty_fun args =
 132   let ty_args =
 133     match unroll env ty_fun with
 134     | TFun(res, args, vararg, a) -> args
 135     | TPtr(ty, a) ->
 136         begin match unroll env ty with
 137         | TFun(res, args, vararg, a) -> args
 138         | _ -> assert false
 139         end
 140     | _ -> assert false in
 141   match ty_args with
 142   | None -> add_noproto env args
 143   | Some targs -> add_proto env args targs
 144
 145 (* Toplevel expressions (appearing in Sdo statements) *)
 146
 147 let add_topexpr env loc e =
 148   match e.edesc with
 149   | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty}, _) ->
 150       let ecall =
 151         {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
 152          etyp = ty} in
 153       if cast_not_needed env ty lhs.etyp then
 154         sassign loc (add_expr env lhs) ecall
 155       else begin
 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))
 159       end
 160   | EBinop(Oassign, lhs, rhs, _) ->
 161       sassign loc (add_expr env lhs) (cast env (add_expr env rhs) lhs.etyp)
 162   | ECall(e1, el) ->
 163       let ecall =
 164         {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
 165          etyp = e.etyp} in
 166       {sdesc = Sdo ecall; sloc = loc}
 167   | _ ->
 168       assert false
 169
 170 (* Initializers *)
 171
 172 let rec add_init env tto = function
 173   | Init_single e ->
 174       Init_single (cast env (add_expr env e) tto)
 175   | Init_array il ->
 176       let ty_elt =
 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))
 183                          fil)
 184   | Init_union(id, fld, i) ->
 185       Init_union(id, fld, add_init env fld.fld_typ i)
 186
 187 (* Declarations *)
 188
 189 let add_decl env (sto, id, ty, optinit) =
 190   (sto, id, ty,
 191    begin match optinit with
 192          | None -> None
 193          | Some init -> Some(add_init env ty init)
 194    end)
 195
 196 (* Statements *)
 197
 198 let rec add_stmt env f s =
 199   match s.sdesc with
 200   | Sskip -> s
 201   | Sdo e -> add_topexpr env s.sloc e
 202   | Sseq(s1, s2) ->
 203       {sdesc = Sseq(add_stmt env f s1, add_stmt env f s2); sloc = s.sloc }
 204   | Sif(e, s1, s2) ->
 205       {sdesc = Sif(add_expr env e, add_stmt env f s1, add_stmt env f s2);
 206        sloc = s.sloc}
 207   | Swhile(e, s1) ->
 208       {sdesc = Swhile(add_expr env e, add_stmt env f s1);
 209        sloc = s.sloc}
 210   | Sdowhile(s1, e) ->
 211       {sdesc = Sdowhile(add_stmt env f s1, add_expr env e);
 212        sloc = s.sloc}
 213   | Sfor(s1, e, s2, s3) ->
 214       {sdesc = Sfor(add_stmt env f s1, add_expr env e, add_stmt env f s2,
 215                     add_stmt env f s3);
 216        sloc = s.sloc}
 217   | Sbreak -> s
 218   | Scontinue -> s
 219   | Sswitch(e, s1) ->
 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}
 223   | Sgoto lbl -> s
 224   | Sreturn None -> s
 225   | Sreturn (Some e) ->
 226       {sdesc = Sreturn(Some(cast env (add_expr env e) f.fd_ret)); sloc = s.sloc}
 227   | Sblock sl ->
 228       {sdesc = Sblock(List.map (add_stmt env f) sl); sloc = s.sloc}
 229   | Sdecl d ->
 230       {sdesc = Sdecl(add_decl env d); sloc = s.sloc}
 231
 232 let add_fundef env f =
 233   reset_temps();
 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' }
 238
 239
 240 let program ?(all = false) p =
 241   omit_widening_casts := not all;
 242   Transform.program ~decl:add_decl ~fundef:add_fundef p