--- /dev/null
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+(* Materialize implicit casts *)
+
+(* Assumes: simplified code
+ Produces: simplified code
+ Preserves: unblocked code *)
+
+open C
+open Cutil
+open Transform
+
+(* We have the option of materializing all casts or leave "widening"
+ casts implicit. Widening casts are:
+- from a small integer type to a larger integer type,
+- from a small float type to a larger float type,
+- from a pointer type to void *.
+*)
+
+let omit_widening_casts = ref false
+
+let widening_cast env tfrom tto =
+ begin match unroll env tfrom, unroll env tto with
+ | TInt(k1, _), TInt(k2, _) ->
+ let r1 = integer_rank k1 and r2 = integer_rank k2 in
+ r1 < r2 || (r1 = r2 && is_signed_ikind k1 = is_signed_ikind k2)
+ | TFloat(k1, _), TFloat(k2, _) ->
+ float_rank k1 <= float_rank k2
+ | TPtr(ty1, _), TPtr(ty2, _) -> is_void_type env ty2
+ | _, _ -> false
+ end
+
+let cast_not_needed env tfrom tto =
+ let tfrom = pointer_decay env tfrom
+ and tto = pointer_decay env tto in
+ compatible_types env tfrom tto
+ || (!omit_widening_casts && widening_cast env tfrom tto)
+
+let cast env e tto =
+ if cast_not_needed env e.etyp tto
+ then e
+ else {edesc = ECast(tto, e); etyp = tto}
+
+(* Note: this pass applies only to simplified expressions
+ because casts cannot be materialized in op= expressions... *)
+
+let rec add_expr env e =
+ match e.edesc with
+ | EConst _ -> e
+ | EVar _ -> e
+ | ESizeof _ -> e
+ | EUnop(op, e1) ->
+ let e1' = add_expr env e1 in
+ let desc =
+ match op with
+ | Ominus | Oplus | Onot ->
+ EUnop(op, cast env e1' e.etyp)
+ | Olognot | Oderef | Oaddrof
+ | Odot _ | Oarrow _ ->
+ EUnop(op, e1')
+ | Opreincr | Opredecr | Opostincr | Opostdecr ->
+ assert false (* not simplified *)
+ in { edesc = desc; etyp = e.etyp }
+ | EBinop(op, e1, e2, ty) ->
+ let e1' = add_expr env e1 in
+ let e2' = add_expr env e2 in
+ let desc =
+ match op with
+ | Oadd ->
+ if is_pointer_type env ty
+ then EBinop(Oadd, e1', e2', ty)
+ else EBinop(Oadd, cast env e1' ty, cast env e2' ty, ty)
+ | Osub ->
+ if is_pointer_type env ty
+ then EBinop(Osub, e1', e2', ty)
+ else EBinop(Osub, cast env e1' ty, cast env e2' ty, ty)
+ | Omul|Odiv|Omod|Oand|Oor|Oxor|Oeq|One|Olt|Ogt|Ole|Oge ->
+ EBinop(op, cast env e1' ty, cast env e2' ty, ty)
+ | Oshl|Oshr ->
+ EBinop(op, cast env e1' ty, e2', ty)
+ | Oindex | Ologand | Ologor | Ocomma ->
+ EBinop(op, e1', e2', ty)
+ | Oassign
+ | Oadd_assign|Osub_assign|Omul_assign|Odiv_assign|Omod_assign
+ | Oand_assign|Oor_assign|Oxor_assign|Oshl_assign|Oshr_assign ->
+ assert false (* not simplified *)
+ in { edesc = desc; etyp = e.etyp }
+ | EConditional(e1, e2, e3) ->
+ let e2' = add_expr env e2 in
+ let e3' = add_expr env e3 in
+ { edesc =
+ EConditional(add_expr env e1, cast env e2' e.etyp, cast env e3' e.etyp);
+ etyp = e.etyp }
+ | ECast(ty, e1) ->
+ { edesc = ECast(ty, add_expr env e1); etyp = e.etyp }
+ | ECall(e1, el) ->
+ assert false (* not simplified *)
+
+(* Arguments to a prototyped function *)
+
+let rec add_proto env args params =
+ match args, params with
+ | [], _ -> []
+ | _::_, [] -> add_noproto env args
+ | arg1 :: argl, (_, ty_p) :: paraml ->
+ cast env (add_expr env arg1) ty_p ::
+ add_proto env argl paraml
+
+(* Arguments to a non-prototyped function *)
+
+and add_noproto env args =
+ match args with
+ | [] -> []
+ | arg1 :: argl ->
+ cast env (add_expr env arg1) (default_argument_conversion env arg1.etyp) ::
+ add_noproto env argl
+
+(* Arguments to function calls in general *)
+
+let add_arguments env ty_fun args =
+ let ty_args =
+ match unroll env ty_fun with
+ | TFun(res, args, vararg, a) -> args
+ | TPtr(ty, a) ->
+ begin match unroll env ty with
+ | TFun(res, args, vararg, a) -> args
+ | _ -> assert false
+ end
+ | _ -> assert false in
+ match ty_args with
+ | None -> add_noproto env args
+ | Some targs -> add_proto env args targs
+
+(* Toplevel expressions (appearing in Sdo statements) *)
+
+let add_topexpr env loc e =
+ match e.edesc with
+ | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty}, _) ->
+ let ecall =
+ {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
+ etyp = ty} in
+ if cast_not_needed env ty lhs.etyp then
+ sassign loc (add_expr env lhs) ecall
+ else begin
+ let tmp = new_temp (erase_attributes_type env ty) in
+ sseq loc (sassign loc tmp ecall)
+ (sassign loc (add_expr env lhs) (cast env tmp lhs.etyp))
+ end
+ | EBinop(Oassign, lhs, rhs, _) ->
+ sassign loc (add_expr env lhs) (cast env (add_expr env rhs) lhs.etyp)
+ | ECall(e1, el) ->
+ let ecall =
+ {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
+ etyp = e.etyp} in
+ {sdesc = Sdo ecall; sloc = loc}
+ | _ ->
+ assert false
+
+(* Initializers *)
+
+let rec add_init env tto = function
+ | Init_single e ->
+ Init_single (cast env (add_expr env e) tto)
+ | Init_array il ->
+ let ty_elt =
+ match unroll env tto with
+ | TArray(ty, _, _) -> ty | _ -> assert false in
+ Init_array (List.map (add_init env ty_elt) il)
+ | Init_struct(id, fil) ->
+ Init_struct (id, List.map
+ (fun (fld, i) -> (fld, add_init env fld.fld_typ i))
+ fil)
+ | Init_union(id, fld, i) ->
+ Init_union(id, fld, add_init env fld.fld_typ i)
+
+(* Declarations *)
+
+let add_decl env (sto, id, ty, optinit) =
+ (sto, id, ty,
+ begin match optinit with
+ | None -> None
+ | Some init -> Some(add_init env ty init)
+ end)
+
+(* Statements *)
+
+let rec add_stmt env f s =
+ match s.sdesc with
+ | Sskip -> s
+ | Sdo e -> add_topexpr env s.sloc e
+ | Sseq(s1, s2) ->
+ {sdesc = Sseq(add_stmt env f s1, add_stmt env f s2); sloc = s.sloc }
+ | Sif(e, s1, s2) ->
+ {sdesc = Sif(add_expr env e, add_stmt env f s1, add_stmt env f s2);
+ sloc = s.sloc}
+ | Swhile(e, s1) ->
+ {sdesc = Swhile(add_expr env e, add_stmt env f s1);
+ sloc = s.sloc}
+ | Sdowhile(s1, e) ->
+ {sdesc = Sdowhile(add_stmt env f s1, add_expr env e);
+ sloc = s.sloc}
+ | Sfor(s1, e, s2, s3) ->
+ {sdesc = Sfor(add_stmt env f s1, add_expr env e, add_stmt env f s2,
+ add_stmt env f s3);
+ sloc = s.sloc}
+ | Sbreak -> s
+ | Scontinue -> s
+ | Sswitch(e, s1) ->
+ {sdesc = Sswitch(add_expr env e, add_stmt env f s1); sloc = s.sloc}
+ | Slabeled(lbl, s) ->
+ {sdesc = Slabeled(lbl, add_stmt env f s); sloc = s.sloc}
+ | Sgoto lbl -> s
+ | Sreturn None -> s
+ | Sreturn (Some e) ->
+ {sdesc = Sreturn(Some(cast env (add_expr env e) f.fd_ret)); sloc = s.sloc}
+ | Sblock sl ->
+ {sdesc = Sblock(List.map (add_stmt env f) sl); sloc = s.sloc}
+ | Sdecl d ->
+ {sdesc = Sdecl(add_decl env d); sloc = s.sloc}
+
+let add_fundef env f =
+ reset_temps();
+ let body' = add_stmt env f f.fd_body in
+ let temps = get_temps () in
+ (* fd_locals have no initializers, so no need to transform them *)
+ { f with fd_locals = f.fd_locals @ temps; fd_body = body' }
+
+
+let program ?(all = false) p =
+ omit_widening_casts := not all;
+ Transform.program ~decl:add_decl ~fundef:add_fundef p
projects / pkg-cerco / acc-trusted.git / blobdiff