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       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
 114 let 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
 124 and 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
 133 let 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
 149 let 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
 174 let 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
 191 let 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
 200 let 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
 234 let 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
 242 let program ?(all = false) p =
 243   omit_widening_casts := not all;
 244   Transform.program ~decl:add_decl ~fundef:add_fundef p